---

Step * of Lemma small-ctrex1-bounds

(r1/r(10))≤r(10^1141) * small-ctrex1()≤(r1/r(4))
BY
{ Assert ⌜|small-ctrex1() - (r(23)/r(2 * 10^1143))| ≤ (r1/r(10^1143))⌝⋅ }

1
.....assertion..... 
|small-ctrex1() - (r(23)/r(2 * 10^1143))| ≤ (r1/r(10^1143))

2
1. |small-ctrex1() - (r(23)/r(2 * 10^1143))| ≤ (r1/r(10^1143))
⊢ (r1/r(10))≤r(10^1141) * small-ctrex1()≤(r1/r(4))

---

Latex:

---

Latex:
(r1/r(10))\mleq{}r(10\^{}1141)  *  small-ctrex1()\mleq{}(r1/r(4))


By

---

Latex:
Assert  \mkleeneopen{}|small-ctrex1()  -  (r(23)/r(2  *  10\^{}1143))|  \mleq{}  (r1/r(10\^{}1143))\mkleeneclose{}\mcdot{}

---

Home Index