---

Step * 1 of Lemma expr_wf


1. x : ℝ
2. λk.(k + (k ÷ if ((((x 1) + 1) ÷ 2) + 1) < (0)  then 1  else 3^(((x 1) + 1) ÷ 2) + 1) + 1)
   ∈ lim n→∞.approx-rexp(x;n) = e^x
3. e^x
= cauchy-limit(n.approx-rexp(x;n);λk.((2 * k)
                                     + ((2 * k) ÷ if ((((x 1) + 1) ÷ 2) + 1) < (0)
                                                     then 1
                                                     else 3^(((x 1) + 1) ÷ 2) + 1)
                                     + 1))
4. cauchy-limit(n.approx-rexp(x;n);λk.((2 * k)
                                      + ((2 * k) ÷ if ((((x 1) + 1) ÷ 2) + 1) < (0)
                                                      then 1
                                                      else 3^(((x 1) + 1) ÷ 2) + 1)
                                      + 1)) ~ expr(x)
⊢ expr(x) ∈ {y:ℝ| y = e^x} 
BY
{ ((HypSubst' -1 -2 THEN (Assert ⌜expr(x) ∈ ℝ⌝⋅ THENM (MemTypeCD THEN Auto))) THEN RevHypSubst (-1) 0) }

1
1. x : ℝ
2. λk.(k + (k ÷ if ((((x 1) + 1) ÷ 2) + 1) < (0)  then 1  else 3^(((x 1) + 1) ÷ 2) + 1) + 1)
   ∈ lim n→∞.approx-rexp(x;n) = e^x
3. e^x = expr(x)
4. cauchy-limit(n.approx-rexp(x;n);λk.((2 * k)
                                      + ((2 * k) ÷ if ((((x 1) + 1) ÷ 2) + 1) < (0)
                                                      then 1
                                                      else 3^(((x 1) + 1) ÷ 2) + 1)
                                      + 1)) ~ expr(x)
⊢ cauchy-limit(n.approx-rexp(x;n);λk.((2 * k)
                                     + ((2 * k) ÷ if ((((x 1) + 1) ÷ 2) + 1) < (0)
                                                     then 1
                                                     else 3^(((x 1) + 1) ÷ 2) + 1)
                                     + 1)) ∈ ℝ

---

Latex:

---

Latex:

1.  x  :  \mBbbR{}
2.  \mlambda{}k.(k  +  (k  \mdiv{}  if  ((((x  1)  +  1)  \mdiv{}  2)  +  1)  <  (0)    then  1    else  3\^{}(((x  1)  +  1)  \mdiv{}  2)  +  1)  +  1)
      \mmember{}  lim  n\mrightarrow{}\minfty{}.approx-rexp(x;n)  =  e\^{}x
3.  e\^{}x
=  cauchy-limit(n.approx-rexp(x;n);\mlambda{}k.((2  *  k)
                                                                          +  ((2  *  k)  \mdiv{}  if  ((((x  1)  +  1)  \mdiv{}  2)  +  1)  <  (0)
                                                                                                          then  1
                                                                                                          else  3\^{}(((x  1)  +  1)  \mdiv{}  2)  +  1)
                                                                          +  1))
4.  cauchy-limit(n.approx-rexp(x;n);\mlambda{}k.((2  *  k)
                                                                            +  ((2  *  k)  \mdiv{}  if  ((((x  1)  +  1)  \mdiv{}  2)  +  1)  <  (0)
                                                                                                            then  1
                                                                                                            else  3\^{}(((x  1)  +  1)  \mdiv{}  2)  +  1)
                                                                            +  1))  \msim{}  expr(x)
\mvdash{}  expr(x)  \mmember{}  \{y:\mBbbR{}|  y  =  e\^{}x\} 


By

---

Latex:
((HypSubst'  -1  -2  THEN  (Assert  \mkleeneopen{}expr(x)  \mmember{}  \mBbbR{}\mkleeneclose{}\mcdot{}  THENM  (MemTypeCD  THEN  Auto)))  THEN  RevHypSubst  (-1)  0)

---

Home Index