---

Step * 2 2 of Lemma rational-IVT-1


1. a : ℤ × ℕ+
2. b : ℤ × ℕ+
3. f : (ℤ × ℕ+) ⟶ (ℤ × ℕ+)
4. g : {x:ℝ| x ∈ [ratreal(a), ratreal(b)]}  ⟶ ℝ
5. ratreal(a) ≤ ratreal(b)
6. ratreal(f[a]) ≤ r0
7. r0 ≤ ratreal(f[b])
8. ∀x,y:{x:ℝ| x ∈ [ratreal(a), ratreal(b)]} .  ((x = y) ⇒ (g[x] = g[y]))
9. ∀r:ℤ × ℕ+. ((ratreal(r) ∈ [ratreal(a), ratreal(b)]) ⇒ (g[ratreal(r)] = ratreal(f[r])))
10. s : ℕ ⟶ (ℤ × ℕ+ × ℤ × ℕ+)
11. ∀i:ℕ
      ((ratreal(fst((s i))) ∈ [ratreal(a), ratreal(b)])
      ∧ (ratreal(snd((s i))) ∈ [ratreal(a), ratreal(b)])
      ∧ (ratreal(fst((s i))) ≤ ratreal(fst((s (i + 1)))))
      ∧ (ratreal(fst((s i))) ≤ ratreal(snd((s i))))
      ∧ (ratreal(snd((s (i + 1)))) ≤ ratreal(snd((s i))))
      ∧ (g[ratreal(fst((s i)))] ≤ r0)
      ∧ (r0 ≤ g[ratreal(snd((s i)))])
      ∧ ((ratreal(snd((s i))) - ratreal(fst((s i)))) = (rinv(r(2))^i * (ratreal(b) - ratreal(a)))))
12. n : ℕ
⊢ r0≤ratreal(snd((s n))) - ratreal(fst((s n)))≤rinv(r(2))^n * (ratreal(b) - ratreal(a))
BY
{ (Assert (ratreal(snd((s n))) - ratreal(fst((s n)))) = (rinv(r(2))^n * (ratreal(b) - ratreal(a))) BY
         Auto) }

1
1. a : ℤ × ℕ+
2. b : ℤ × ℕ+
3. f : (ℤ × ℕ+) ⟶ (ℤ × ℕ+)
4. g : {x:ℝ| x ∈ [ratreal(a), ratreal(b)]}  ⟶ ℝ
5. ratreal(a) ≤ ratreal(b)
6. ratreal(f[a]) ≤ r0
7. r0 ≤ ratreal(f[b])
8. ∀x,y:{x:ℝ| x ∈ [ratreal(a), ratreal(b)]} .  ((x = y) ⇒ (g[x] = g[y]))
9. ∀r:ℤ × ℕ+. ((ratreal(r) ∈ [ratreal(a), ratreal(b)]) ⇒ (g[ratreal(r)] = ratreal(f[r])))
10. s : ℕ ⟶ (ℤ × ℕ+ × ℤ × ℕ+)
11. ∀i:ℕ
      ((ratreal(fst((s i))) ∈ [ratreal(a), ratreal(b)])
      ∧ (ratreal(snd((s i))) ∈ [ratreal(a), ratreal(b)])
      ∧ (ratreal(fst((s i))) ≤ ratreal(fst((s (i + 1)))))
      ∧ (ratreal(fst((s i))) ≤ ratreal(snd((s i))))
      ∧ (ratreal(snd((s (i + 1)))) ≤ ratreal(snd((s i))))
      ∧ (g[ratreal(fst((s i)))] ≤ r0)
      ∧ (r0 ≤ g[ratreal(snd((s i)))])
      ∧ ((ratreal(snd((s i))) - ratreal(fst((s i)))) = (rinv(r(2))^i * (ratreal(b) - ratreal(a)))))
12. n : ℕ
13. (ratreal(snd((s n))) - ratreal(fst((s n)))) = (rinv(r(2))^n * (ratreal(b) - ratreal(a)))
⊢ r0≤ratreal(snd((s n))) - ratreal(fst((s n)))≤rinv(r(2))^n * (ratreal(b) - ratreal(a))

---

Latex:

---

Latex:

1.  a  :  \mBbbZ{}  \mtimes{}  \mBbbN{}\msupplus{}
2.  b  :  \mBbbZ{}  \mtimes{}  \mBbbN{}\msupplus{}
3.  f  :  (\mBbbZ{}  \mtimes{}  \mBbbN{}\msupplus{})  {}\mrightarrow{}  (\mBbbZ{}  \mtimes{}  \mBbbN{}\msupplus{})
4.  g  :  \{x:\mBbbR{}|  x  \mmember{}  [ratreal(a),  ratreal(b)]\}    {}\mrightarrow{}  \mBbbR{}
5.  ratreal(a)  \mleq{}  ratreal(b)
6.  ratreal(f[a])  \mleq{}  r0
7.  r0  \mleq{}  ratreal(f[b])
8.  \mforall{}x,y:\{x:\mBbbR{}|  x  \mmember{}  [ratreal(a),  ratreal(b)]\}  .    ((x  =  y)  {}\mRightarrow{}  (g[x]  =  g[y]))
9.  \mforall{}r:\mBbbZ{}  \mtimes{}  \mBbbN{}\msupplus{}.  ((ratreal(r)  \mmember{}  [ratreal(a),  ratreal(b)])  {}\mRightarrow{}  (g[ratreal(r)]  =  ratreal(f[r])))
10.  s  :  \mBbbN{}  {}\mrightarrow{}  (\mBbbZ{}  \mtimes{}  \mBbbN{}\msupplus{}  \mtimes{}  \mBbbZ{}  \mtimes{}  \mBbbN{}\msupplus{})
11.  \mforall{}i:\mBbbN{}
            ((ratreal(fst((s  i)))  \mmember{}  [ratreal(a),  ratreal(b)])
            \mwedge{}  (ratreal(snd((s  i)))  \mmember{}  [ratreal(a),  ratreal(b)])
            \mwedge{}  (ratreal(fst((s  i)))  \mleq{}  ratreal(fst((s  (i  +  1)))))
            \mwedge{}  (ratreal(fst((s  i)))  \mleq{}  ratreal(snd((s  i))))
            \mwedge{}  (ratreal(snd((s  (i  +  1))))  \mleq{}  ratreal(snd((s  i))))
            \mwedge{}  (g[ratreal(fst((s  i)))]  \mleq{}  r0)
            \mwedge{}  (r0  \mleq{}  g[ratreal(snd((s  i)))])
            \mwedge{}  ((ratreal(snd((s  i)))  -  ratreal(fst((s  i))))  =  (rinv(r(2))\^{}i  *  (ratreal(b)  -  ratreal(a)))))
12.  n  :  \mBbbN{}
\mvdash{}  r0\mleq{}ratreal(snd((s  n)))  -  ratreal(fst((s  n)))\mleq{}rinv(r(2))\^{}n  *  (ratreal(b)  -  ratreal(a))


By

---

Latex:
(Assert  (ratreal(snd((s  n)))  -  ratreal(fst((s  n))))  =  (rinv(r(2))\^{}n  *  (ratreal(b)  -  ratreal(a)))  BY
              Auto)

---

Home Index