---

Step * 2 of Lemma small-ctrex1-bounds


1. |small-ctrex1() - (r(23)/r(2 * 10^1143))| ≤ (r1/r(10^1143))
⊢ (r1/r(10))≤r(10^1141) * small-ctrex1()≤(r1/r(4))
BY
{ Subst ⌜10^1143 ~ 100 * 10^1141⌝ (-1)⋅ }

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

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

---

Latex:

---

Latex:

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


By

---

Latex:
Subst  \mkleeneopen{}10\^{}1143  \msim{}  100  *  10\^{}1141\mkleeneclose{}  (-1)\mcdot{}

---

Home Index