---

Step * 1 of Lemma small-ctrex1_wf


un-ctrex1(un-ctrex1((r1)/10^126)) ∈ ℝ
BY
{ ((Assert 0 < 10^126 BY
          EAuto 1)
   THEN (Assert un-ctrex1((r1)/10^126) ∈ ℝ BY
               (Auto THEN MemTypeCD THEN Auto THEN RWO "int-rdiv-req" 0 THEN Auto))
   ) }

1
1. 0 < 10^126
2. un-ctrex1((r1)/10^126) ∈ ℝ
⊢ un-ctrex1(un-ctrex1((r1)/10^126)) ∈ ℝ

---

Latex:

---

Latex:

un-ctrex1(un-ctrex1((r1)/10\^{}126))  \mmember{}  \mBbbR{}


By

---

Latex:
((Assert  0  <  10\^{}126  BY
                EAuto  1)
  THEN  (Assert  un-ctrex1((r1)/10\^{}126)  \mmember{}  \mBbbR{}  BY
                          (Auto  THEN  MemTypeCD  THEN  Auto  THEN  RWO  "int-rdiv-req"  0  THEN  Auto))
  )

---

Home Index