---

Step * 2 2 1 2 of Lemma small-ctrex1-bounds


1. N : ℕ+@i
2. 10^1141 = N ∈ ℕ+@i
3. v : ℝ@i
4. small-ctrex1() = v ∈ ℝ@i
5. |v - (r(23)/r(200 * N))| ≤ (r1/r(100 * N))@i
⊢ r(100) * r(N) ≠ r0
BY
{ CondAuto1 }

---

Latex:

---

Latex:

1.  N  :  \mBbbN{}\msupplus{}@i
2.  10\^{}1141  =  N@i
3.  v  :  \mBbbR{}@i
4.  small-ctrex1()  =  v@i
5.  |v  -  (r(23)/r(200  *  N))|  \mleq{}  (r1/r(100  *  N))@i
\mvdash{}  r(100)  *  r(N)  \mneq{}  r0


By

---

Latex:
CondAuto1

---

Home Index