Step
*
1
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. ∀p:x:{x:ℤ × ℕ+| (ratreal(x) ∈ [ratreal(a), ratreal(b)]) ∧ (g[ratreal(x)] ≤ r0)} × {y:ℤ × ℕ+|
(ratreal(y)
∈ [ratreal(a), ratreal(b)])
∧ (ratreal(x) ≤ ratreal(y))
∧ (r0 ≤ g[ratreal(y)])}
∃q:x:{x:ℤ × ℕ+| (ratreal(x) ∈ [ratreal(a), ratreal(b)]) ∧ (g[ratreal(x)] ≤ r0)} × {y:ℤ × ℕ+|
(ratreal(y)
∈ [ratreal(a), ratreal(b)])
∧ (ratreal(x) ≤ ratreal(y))
∧ (r0 ≤ g[ratreal(y)])}
((ratreal(fst(p)) ≤ ratreal(fst(q)))
∧ (ratreal(snd(q)) ≤ ratreal(snd(p)))
∧ ((ratreal(snd(q)) - ratreal(fst(q))) = (rinv(r(2)) * (ratreal(snd(p)) - ratreal(fst(p))))))
⊢ ∃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)))))
BY
{ (Skolemize (-1) `s' THENA Auto) }
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. ∀p:x:{x:ℤ × ℕ+| (ratreal(x) ∈ [ratreal(a), ratreal(b)]) ∧ (g[ratreal(x)] ≤ r0)} × {y:ℤ × ℕ+|
(ratreal(y)
∈ [ratreal(a), ratreal(b)])
∧ (ratreal(x) ≤ ratreal(y))
∧ (r0 ≤ g[ratreal(y)])}
∃q:x:{x:ℤ × ℕ+| (ratreal(x) ∈ [ratreal(a), ratreal(b)]) ∧ (g[ratreal(x)] ≤ r0)} × {y:ℤ × ℕ+|
(ratreal(y)
∈ [ratreal(a), ratreal(b)])
∧ (ratreal(x) ≤ ratreal(y))
∧ (r0 ≤ g[ratreal(y)])}
((ratreal(fst(p)) ≤ ratreal(fst(q)))
∧ (ratreal(snd(q)) ≤ ratreal(snd(p)))
∧ ((ratreal(snd(q)) - ratreal(fst(q))) = (rinv(r(2)) * (ratreal(snd(p)) - ratreal(fst(p))))))
7. s : p:(x:{x:ℤ × ℕ+| (ratreal(x) ∈ [ratreal(a), ratreal(b)]) ∧ (g[ratreal(x)] ≤ r0)} × {y:ℤ × ℕ+|
(ratreal(y) ∈ [ratreal(a), ratreal(b)])
∧ (ratreal(x) ≤ ratreal(y))
∧ (r0 ≤ g[ratreal(y)])} )
⟶ (x:{x:ℤ × ℕ+| (ratreal(x) ∈ [ratreal(a), ratreal(b)]) ∧ (g[ratreal(x)] ≤ r0)} × {y:ℤ × ℕ+|
(ratreal(y) ∈ [ratreal(a), ratreal(b)])
∧ (ratreal(x) ≤ ratreal(y))
∧ (r0 ≤ g[ratreal(y)])} )
8. ∀p:x:{x:ℤ × ℕ+| (ratreal(x) ∈ [ratreal(a), ratreal(b)]) ∧ (g[ratreal(x)] ≤ r0)} × {y:ℤ × ℕ+|
(ratreal(y)
∈ [ratreal(a), ratreal(b)])
∧ (ratreal(x) ≤ ratreal(y))
∧ (r0 ≤ g[ratreal(y)])}
((ratreal(fst(p)) ≤ ratreal(fst((s p))))
∧ (ratreal(snd((s p))) ≤ ratreal(snd(p)))
∧ ((ratreal(snd((s p))) - ratreal(fst((s p)))) = (rinv(r(2)) * (ratreal(snd(p)) - ratreal(fst(p))))))
⊢ ∃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)))))
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. \mforall{}p:x:\{x:\mBbbZ{} \mtimes{} \mBbbN{}\msupplus{}| (ratreal(x) \mmember{} [ratreal(a), ratreal(b)]) \mwedge{} (g[ratreal(x)] \mleq{} r0)\}
\mtimes{} \{y:\mBbbZ{} \mtimes{} \mBbbN{}\msupplus{}|
(ratreal(y) \mmember{} [ratreal(a), ratreal(b)])
\mwedge{} (ratreal(x) \mleq{} ratreal(y))
\mwedge{} (r0 \mleq{} g[ratreal(y)])\}
\mexists{}q:x:\{x:\mBbbZ{} \mtimes{} \mBbbN{}\msupplus{}| (ratreal(x) \mmember{} [ratreal(a), ratreal(b)]) \mwedge{} (g[ratreal(x)] \mleq{} r0)\}
\mtimes{} \{y:\mBbbZ{} \mtimes{} \mBbbN{}\msupplus{}|
(ratreal(y) \mmember{} [ratreal(a), ratreal(b)])
\mwedge{} (ratreal(x) \mleq{} ratreal(y))
\mwedge{} (r0 \mleq{} g[ratreal(y)])\}
((ratreal(fst(p)) \mleq{} ratreal(fst(q)))
\mwedge{} (ratreal(snd(q)) \mleq{} ratreal(snd(p)))
\mwedge{} ((ratreal(snd(q)) - ratreal(fst(q))) = (rinv(r(2)) * (ratreal(snd(p)) - ratreal(fst(p))))))
\mvdash{} \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)))))
By
Latex:
(Skolemize (-1) `s' THENA Auto)
Home
Index