How would you write ∀ y ∈ R+, ∃ z ∈ R, e^z = y in pseudocode?

I’m reading about proofs, currently reading Mathematics for Computer Science by Eric Lehman and Tom Leighton, they illustrate in a sample proposition that "as z ranges over the real numbers, e^z takes on every positive, real value at least once". I'm having trouble fully grasping this proposition.

I am trying to approach this is as a programmer and think of what it would look like in pseudocode if I were to see if it was true.

pr = [ N naught ]
r  = [ all real numbers ]

for y in pr:
    for z in r:

        e = pow(y, z)
        if e != y:
            goto outer
    
        print "this is true";

    outer

Is this what they are proposing?

Solution

∀ y ∈ R+, ∃ z ∈ R, e^z = y

Is saying that for all y in the set of positive real numbers, there exists a z in the set of real numbers, such that exp(z) = y.

You can't really create a program to verify that this is true. Most basically because you will encounter one of the following problems

Floating point math imprecision (essential read Is floating point math broken?)
The reals are infinite

You could check this over every floating point number (which would take a very long time but is still theoretically able to be computed), but you would

Likely come up with a situation where there is no z such that exp(z) = y because such a z does not exist exactly enough in the set of floating point numbers to give you exp(z) = y
Even if there was a z for every y in the set of floating point numbers, this would not prove exp(z) = y for all y in R+ and z in R.

So on the whole, yes you're pseudocode somewhat represents the idea, but it's not viable or logical to check this on a computer or really as much think about this as a computing problem.

Edit: The best way to think about this programmatically would be like this

R = [SET OF ALL REALS]
R+ = FILTER (> 0) R
(MAP (exp) R) == R+

N.B. exp means e^n where e^x = SUM [ (x^k)/(k!) | k <- [SET OF ALL NATURALS]] which is approximately 2.718^x.