---

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


1. N : ℕ+
2. 10^1141 = N ∈ ℕ+
3. v : ℝ
4. small-ctrex1() = v ∈ ℝ
5. |v - (r(23)/r(2 * 100 * N))| ≤ (r1/r(100 * N))
⊢ (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 : ℕ+
2. 10^1141 = N ∈ ℕ+
3. v : ℝ
4. small-ctrex1() = v ∈ ℝ
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{}
2.  10\^{}1141  =  N
3.  v  :  \mBbbR{}
4.  small-ctrex1()  =  v
5.  |v  -  (r(23)/r(2  *  100  *  N))|  \mleq{}  (r1/r(100  *  N))
\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