---

Step * 2 3 1 1 1 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:ℝ| (ratreal(a) ≤ x) ∧ (x ≤ ratreal(b))} .  ((x = y) ⇒ ((g x) = (g y)))
9. ∀r:ℤ × ℕ+. (((ratreal(a) ≤ ratreal(r)) ∧ (ratreal(r) ≤ ratreal(b))) ⇒ ((g ratreal(r)) = ratreal(f r)))
10. s : ℕ ⟶ (ℤ × ℕ+ × ℤ × ℕ+)
11. ∀i:ℕ
      (((ratreal(a) ≤ ratreal(fst((s i)))) ∧ (ratreal(fst((s i))) ≤ ratreal(b)))
      ∧ ((ratreal(a) ≤ ratreal(snd((s i)))) ∧ (ratreal(snd((s i))) ≤ 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. y : ℝ
13. lim n→∞.ratreal(fst((s n))) = y
14. lim n→∞.ratreal(snd((s n))) = y
15. y ∈ [ratreal(a), ratreal(b)]
16. lim n→∞.g ratreal(fst((s n))) = g y
17. lim n→∞.g ratreal(snd((s n))) = g y
18. (g y) ≤ r0
19. r0 ≤ (g y)
⊢ (g y) = r0
BY
{ (RepeatFor 2 (MoveToConcl (-1)) THEN (GenConclTerm ⌜g y⌝⋅ THENA Auto) THEN All  Thin) }

1
1. v : ℝ
⊢ (v ≤ r0) ⇒ (r0 ≤ v) ⇒ (v = r0)

---

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{}|  (ratreal(a)  \mleq{}  x)  \mwedge{}  (x  \mleq{}  ratreal(b))\}  .    ((x  =  y)  {}\mRightarrow{}  ((g  x)  =  (g  y)))
9.  \mforall{}r:\mBbbZ{}  \mtimes{}  \mBbbN{}\msupplus{}
          (((ratreal(a)  \mleq{}  ratreal(r))  \mwedge{}  (ratreal(r)  \mleq{}  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(a)  \mleq{}  ratreal(fst((s  i))))  \mwedge{}  (ratreal(fst((s  i)))  \mleq{}  ratreal(b)))
            \mwedge{}  ((ratreal(a)  \mleq{}  ratreal(snd((s  i))))  \mwedge{}  (ratreal(snd((s  i)))  \mleq{}  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.  y  :  \mBbbR{}
13.  lim  n\mrightarrow{}\minfty{}.ratreal(fst((s  n)))  =  y
14.  lim  n\mrightarrow{}\minfty{}.ratreal(snd((s  n)))  =  y
15.  y  \mmember{}  [ratreal(a),  ratreal(b)]
16.  lim  n\mrightarrow{}\minfty{}.g  ratreal(fst((s  n)))  =  g  y
17.  lim  n\mrightarrow{}\minfty{}.g  ratreal(snd((s  n)))  =  g  y
18.  (g  y)  \mleq{}  r0
19.  r0  \mleq{}  (g  y)
\mvdash{}  (g  y)  =  r0


By

---

Latex:
(RepeatFor  2  (MoveToConcl  (-1))  THEN  (GenConclTerm  \mkleeneopen{}g  y\mkleeneclose{}\mcdot{}  THENA  Auto)  THEN  All    Thin)

---

Home Index