Step
*
1
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 = 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)) ∈ ℝ
BY
{ Thin (-1) }
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)
⊢ 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  =  expr(x)
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{}  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))  \mmember{}  \mBbbR{}
By
Latex:
Thin  (-1)
Home
Index