---

Step * 2 2 1 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(2 * 100 * N))| ≤ (r1/r(100 * N))@i
⊢ (r1/r(10))≤r(N) * v≤(r1/r(4))
BY
{ ((Subst' 2 * 100 * N ~ 200 * N -1 THENA Auto) THEN (RWO "rmul-int<" (-1) THENA EAuto 1)) }

1
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(200) * r(N) ≠ r0

2
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

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

---

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(2  *  100  *  N))|  \mleq{}  (r1/r(100  *  N))@i
\mvdash{}  (r1/r(10))\mleq{}r(N)  *  v\mleq{}(r1/r(4))


By

---

Latex:
((Subst'  2  *  100  *  N  \msim{}  200  *  N  -1  THENA  Auto)  THEN  (RWO  "rmul-int<"  (-1)  THENA  EAuto  1))

---

Home Index