---

Step * 1 1 of Lemma small-ctrex1-bounds


1. 0 < 10^1143
⊢ |small-ctrex1() - (r(23)/r(2 * 10^1143))| ≤ (r1/r(10^1143))
BY
{ TACTIC:(RWO  "ctrex1-calculation<" 0
          THEN (RW (AddrC [1] (SweepUpC (RevLemmaC `int-rdiv-req`))) 0 THENA Auto)
          THEN Fold `rational-approx` 0
          THEN BLemma `rational-approx-property`
          THEN EAuto 1) }

---

Latex:

---

Latex:

1.  0  <  10\^{}1143
\mvdash{}  |small-ctrex1()  -  (r(23)/r(2  *  10\^{}1143))|  \mleq{}  (r1/r(10\^{}1143))


By

---

Latex:
TACTIC:(RWO    "ctrex1-calculation<"  0
                THEN  (RW  (AddrC  [1]  (SweepUpC  (RevLemmaC  `int-rdiv-req`)))  0  THENA  Auto)
                THEN  Fold  `rational-approx`  0
                THEN  BLemma  `rational-approx-property`
                THEN  EAuto  1)

---

Home Index