---

Step * 1 1 of Lemma real_exp_wf


1. x : ℝ
2. N : ℕ+
3. |4 * x| ≤ r(N)
⊢ rexp-small((x)/N)^N ∈ {y:ℝ| y = e^x} 
BY
{ ((Assert r0 < |r(N)| BY
          (RWO "rabs-int" 0 THEN Auto THEN Subst' |N| ~ N 0 THEN Auto))
   THEN (Assert |(x)/N| ≤ (r1/r(4)) BY
               ((RWO  "int-rdiv-req" 0 THENA Auto)
                THEN (RWO "rabs-rdiv" 0 THENA Auto)
                THEN RWO "rabs-int" 0
                THEN Auto
                THEN Subst' |N| ~ N 0
                THEN Auto
                THEN nRMul ⌜r(N)⌝ 0⋅
                THEN nRMul ⌜r(4)⌝ 0⋅
                THEN (RWO  "-2<" 0 THENA Auto)
                THEN (RWW "int-rmul-req rabs-rmul rabs-int" 0 THENA Auto)
                THEN Subst' |4| ~ 4 0
                THEN Auto))
   ) }

1
1. x : ℝ
2. N : ℕ+
3. |4 * x| ≤ r(N)
4. r0 < |r(N)|
5. |(x)/N| ≤ (r1/r(4))
⊢ rexp-small((x)/N)^N ∈ {y:ℝ| y = e^x} 

---

Latex:

---

Latex:

1.  x  :  \mBbbR{}
2.  N  :  \mBbbN{}\msupplus{}
3.  |4  *  x|  \mleq{}  r(N)
\mvdash{}  rexp-small((x)/N)\^{}N  \mmember{}  \{y:\mBbbR{}|  y  =  e\^{}x\} 


By

---

Latex:
((Assert  r0  <  |r(N)|  BY
                (RWO  "rabs-int"  0  THEN  Auto  THEN  Subst'  |N|  \msim{}  N  0  THEN  Auto))
  THEN  (Assert  |(x)/N|  \mleq{}  (r1/r(4))  BY
                          ((RWO    "int-rdiv-req"  0  THENA  Auto)
                            THEN  (RWO  "rabs-rdiv"  0  THENA  Auto)
                            THEN  RWO  "rabs-int"  0
                            THEN  Auto
                            THEN  Subst'  |N|  \msim{}  N  0
                            THEN  Auto
                            THEN  nRMul  \mkleeneopen{}r(N)\mkleeneclose{}  0\mcdot{}
                            THEN  nRMul  \mkleeneopen{}r(4)\mkleeneclose{}  0\mcdot{}
                            THEN  (RWO    "-2<"  0  THENA  Auto)
                            THEN  (RWW  "int-rmul-req  rabs-rmul  rabs-int"  0  THENA  Auto)
                            THEN  Subst'  |4|  \msim{}  4  0
                            THEN  Auto))
  )

---

Home Index