Proof of Nuprl Lemma : rational-IVT-1

Step * 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))
∧ (ratreal(f[a]) ≤ r0)
∧ (r0 ≤ ratreal(f[b]))
∧ (∀x,y:{x:ℝ| x ∈ [ratreal(a), ratreal(b)]} .  ((x = y) ⇒ (g[x] = g[y])))
∧ (∀r:ℤ × ℕ⁺. ((ratreal(r) ∈ [ratreal(a), ratreal(b)]) ⇒ (g[ratreal(r)] = ratreal(f[r]))))
6. ∃s:ℕ ⟶ (ℤ × ℕ⁺ × ℤ × ℕ⁺)
    ∀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)))))
⊢ ∃c:{c:ℝ| c ∈ [ratreal(a), ratreal(b)]}  [(g[c] = r0)]
BY
{ (ExRepD

   THEN (InstLemma `common-limit-squeeze` [⌜λ₂i.ratreal(fst((s i)))⌝;⌜λ₂i.ratreal(snd((s i)))⌝;⌜λ₂i.rinv(r(2))^i

                                                                                                * (ratreal(b)

                                                                                                  - ratreal(a))⌝]⋅

         THENA Auto
         )
   ) }

1
.....antecedent.....
1. a : ℤ × ℕ⁺
2. b : ℤ × ℕ⁺
3. f : (ℤ × ℕ⁺) ⟶ (ℤ × ℕ⁺)
4. [g] : {x:ℝ| x ∈ [ratreal(a), ratreal(b)]}  ⟶ ℝ
5. [%] : (ratreal(a) ≤ ratreal(b))
∧ (ratreal(f[a]) ≤ r0)
∧ (r0 ≤ ratreal(f[b]))
∧ (∀x,y:{x:ℝ| x ∈ [ratreal(a), ratreal(b)]} .  ((x = y) ⇒ (g[x] = g[y])))
∧ (∀r:ℤ × ℕ⁺. ((ratreal(r) ∈ [ratreal(a), ratreal(b)]) ⇒ (g[ratreal(r)] = ratreal(f[r]))))
6. s : ℕ ⟶ (ℤ × ℕ⁺ × ℤ × ℕ⁺)
7. ∀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)))))
⊢ lim n→∞.rinv(r(2))^n * (ratreal(b) - ratreal(a)) = r0

2
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))

3
1. a : ℤ × ℕ⁺
2. b : ℤ × ℕ⁺
3. f : (ℤ × ℕ⁺) ⟶ (ℤ × ℕ⁺)
4. [g] : {x:ℝ| x ∈ [ratreal(a), ratreal(b)]}  ⟶ ℝ
5. [%] : (ratreal(a) ≤ ratreal(b))
∧ (ratreal(f[a]) ≤ r0)
∧ (r0 ≤ ratreal(f[b]))
∧ (∀x,y:{x:ℝ| x ∈ [ratreal(a), ratreal(b)]} .  ((x = y) ⇒ (g[x] = g[y])))
∧ (∀r:ℤ × ℕ⁺. ((ratreal(r) ∈ [ratreal(a), ratreal(b)]) ⇒ (g[ratreal(r)] = ratreal(f[r]))))
6. s : ℕ ⟶ (ℤ × ℕ⁺ × ℤ × ℕ⁺)
7. ∀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)))))
8. ∃y:ℝ. (lim n→∞.ratreal(fst((s n))) = y ∧ lim n→∞.ratreal(snd((s n))) = y)
⊢ ∃c:{c:ℝ| c ∈ [ratreal(a), ratreal(b)]}  [(g[c] = 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)) \mwedge{} (ratreal(f[a]) \mleq{} r0) \mwedge{} (r0 \mleq{} ratreal(f[b])) \mwedge{} (\mforall{}x,y:\{x:\mBbbR{}| x \mmember{} [ratreal(a), ratreal(b)]\} . ((x = y) {}\mRightarrow{} (g[x] = g[y]))) \mwedge{} (\mforall{}r:\mBbbZ{} \mtimes{} \mBbbN{}\msupplus{}. ((ratreal(r) \mmember{} [ratreal(a), ratreal(b)]) {}\mRightarrow{} (g[ratreal(r)] = ratreal(f[r])))) 6. \mexists{}s:\mBbbN{} {}\mrightarrow{} (\mBbbZ{} \mtimes{} \mBbbN{}\msupplus{} \mtimes{} \mBbbZ{} \mtimes{} \mBbbN{}\msupplus{}) \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))))) \mvdash{} \mexists{}c:\{c:\mBbbR{}| c \mmember{} [ratreal(a), ratreal(b)]\} [(g[c] = r0)] By Latex: (ExRepD THEN (InstLemma `common-limit-squeeze` [\mkleeneopen{}\mlambda{}\msubtwo{}i.ratreal(fst((s i)))\mkleeneclose{};\mkleeneopen{}\mlambda{}\msubtwo{}i.ratreal(snd((s i)))\mkleeneclose{}; \mkleeneopen{}\mlambda{}\msubtwo{}i.rinv(r(2))\^{}i * (ratreal(b) - ratreal(a))\mkleeneclose{}]\mcdot{} THENA Auto ) ) Home Index