Step
*
1
2
1
1
2
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))
∧ (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 : 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)])} )
7. ∀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))))))
8. <a, b> ∈ 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)])}
9. λn.primrec(n;<a, b>;λi,r. (s r)) ∈ ℕ ⟶ (x:{x:ℤ × ℕ+| (ratreal(x) ∈ [ratreal(a), ratreal(b)]) ∧ (g[ratreal(x)] ≤ r0)}\000C
× {y:ℤ × ℕ+|
(ratreal(y) ∈ [ratreal(a), ratreal(b)])
∧ (ratreal(x) ≤ ratreal(y))
∧ (r0 ≤ g[ratreal(y)])} )
10. i : ℕ
11. x : {x:ℤ × ℕ+| (ratreal(x) ∈ [ratreal(a), ratreal(b)]) ∧ (g[ratreal(x)] ≤ r0)}
12. v1 : {y:ℤ × ℕ+| (ratreal(y) ∈ [ratreal(a), ratreal(b)]) ∧ (ratreal(x) ≤ ratreal(y)) ∧ (r0 ≤ g[ratreal(y)])}
13. ((λn.primrec(n;<a, b>;λi,r. (s r))) i)
= <x, v1>
∈ (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)])} )
14. ratreal(fst(<x, v1>)) ∈ [ratreal(a), ratreal(b)]
15. ratreal(snd(<x, v1>)) ∈ [ratreal(a), ratreal(b)]
16. ratreal(fst(<x, v1>)) ≤ ratreal(fst((s <x, v1>)))
17. ratreal(fst(<x, v1>)) ≤ ratreal(snd(<x, v1>))
18. ratreal(snd((s <x, v1>))) ≤ ratreal(snd(<x, v1>))
19. g[ratreal(fst(<x, v1>))] ≤ r0
20. r0 ≤ g[ratreal(snd(<x, v1>))]
⊢ (ratreal(v1) - ratreal(x)) = (rinv(r(2))^i * (ratreal(b) - ratreal(a)))
BY
{ Assert ⌜∀i:ℕ
((ratreal(snd(((λn.primrec(n;<a, b>;λi,r. (s r))) i))) - ratreal(fst(((λn.primrec(n;<a, b>;λi,r. (s r))) i))\000C))
= (rinv(r(2))^i * (ratreal(b) - ratreal(a))))⌝⋅ }
1
.....assertion.....
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 : 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)])} )
7. ∀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))))))
8. <a, b> ∈ 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)])}
9. λn.primrec(n;<a, b>;λi,r. (s r)) ∈ ℕ ⟶ (x:{x:ℤ × ℕ+| (ratreal(x) ∈ [ratreal(a), ratreal(b)]) ∧ (g[ratreal(x)] ≤ r0)}\000C
× {y:ℤ × ℕ+|
(ratreal(y) ∈ [ratreal(a), ratreal(b)])
∧ (ratreal(x) ≤ ratreal(y))
∧ (r0 ≤ g[ratreal(y)])} )
10. i : ℕ
11. x : {x:ℤ × ℕ+| (ratreal(x) ∈ [ratreal(a), ratreal(b)]) ∧ (g[ratreal(x)] ≤ r0)}
12. v1 : {y:ℤ × ℕ+| (ratreal(y) ∈ [ratreal(a), ratreal(b)]) ∧ (ratreal(x) ≤ ratreal(y)) ∧ (r0 ≤ g[ratreal(y)])}
13. ((λn.primrec(n;<a, b>;λi,r. (s r))) i)
= <x, v1>
∈ (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)])} )
14. ratreal(fst(<x, v1>)) ∈ [ratreal(a), ratreal(b)]
15. ratreal(snd(<x, v1>)) ∈ [ratreal(a), ratreal(b)]
16. ratreal(fst(<x, v1>)) ≤ ratreal(fst((s <x, v1>)))
17. ratreal(fst(<x, v1>)) ≤ ratreal(snd(<x, v1>))
18. ratreal(snd((s <x, v1>))) ≤ ratreal(snd(<x, v1>))
19. g[ratreal(fst(<x, v1>))] ≤ r0
20. r0 ≤ g[ratreal(snd(<x, v1>))]
⊢ ∀i:ℕ
((ratreal(snd(((λn.primrec(n;<a, b>;λi,r. (s r))) i))) - ratreal(fst(((λn.primrec(n;<a, b>;λi,r. (s r))) i))))
= (rinv(r(2))^i * (ratreal(b) - ratreal(a))))
2
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 : 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)])} )
7. ∀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))))))
8. <a, b> ∈ 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)])}
9. λn.primrec(n;<a, b>;λi,r. (s r)) ∈ ℕ ⟶ (x:{x:ℤ × ℕ+| (ratreal(x) ∈ [ratreal(a), ratreal(b)]) ∧ (g[ratreal(x)] ≤ r0)}\000C
× {y:ℤ × ℕ+|
(ratreal(y) ∈ [ratreal(a), ratreal(b)])
∧ (ratreal(x) ≤ ratreal(y))
∧ (r0 ≤ g[ratreal(y)])} )
10. i : ℕ
11. x : {x:ℤ × ℕ+| (ratreal(x) ∈ [ratreal(a), ratreal(b)]) ∧ (g[ratreal(x)] ≤ r0)}
12. v1 : {y:ℤ × ℕ+| (ratreal(y) ∈ [ratreal(a), ratreal(b)]) ∧ (ratreal(x) ≤ ratreal(y)) ∧ (r0 ≤ g[ratreal(y)])}
13. ((λn.primrec(n;<a, b>;λi,r. (s r))) i)
= <x, v1>
∈ (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)])} )
14. ratreal(fst(<x, v1>)) ∈ [ratreal(a), ratreal(b)]
15. ratreal(snd(<x, v1>)) ∈ [ratreal(a), ratreal(b)]
16. ratreal(fst(<x, v1>)) ≤ ratreal(fst((s <x, v1>)))
17. ratreal(fst(<x, v1>)) ≤ ratreal(snd(<x, v1>))
18. ratreal(snd((s <x, v1>))) ≤ ratreal(snd(<x, v1>))
19. g[ratreal(fst(<x, v1>))] ≤ r0
20. r0 ≤ g[ratreal(snd(<x, v1>))]
21. ∀i:ℕ
((ratreal(snd(((λn.primrec(n;<a, b>;λi,r. (s r))) i))) - ratreal(fst(((λn.primrec(n;<a, b>;λi,r. (s r))) i))))
= (rinv(r(2))^i * (ratreal(b) - ratreal(a))))
⊢ (ratreal(v1) - ratreal(x)) = (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. s : 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)])\} )
{}\mrightarrow{} (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)])\} )
7. \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)])\}
((ratreal(fst(p)) \mleq{} ratreal(fst((s p))))
\mwedge{} (ratreal(snd((s p))) \mleq{} ratreal(snd(p)))
\mwedge{} ((ratreal(snd((s p))) - ratreal(fst((s p))))
= (rinv(r(2)) * (ratreal(snd(p)) - ratreal(fst(p))))))
8. <a, b> \mmember{} 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)])\}
9. \mlambda{}n.primrec(n;<a, b>\mlambda{}i,r. (s r)) \mmember{} \mBbbN{} {}\mrightarrow{} (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)])\} )
10. i : \mBbbN{}
11. x : \{x:\mBbbZ{} \mtimes{} \mBbbN{}\msupplus{}| (ratreal(x) \mmember{} [ratreal(a), ratreal(b)]) \mwedge{} (g[ratreal(x)] \mleq{} r0)\}
12. v1 : \{y:\mBbbZ{} \mtimes{} \mBbbN{}\msupplus{}|
(ratreal(y) \mmember{} [ratreal(a), ratreal(b)])
\mwedge{} (ratreal(x) \mleq{} ratreal(y))
\mwedge{} (r0 \mleq{} g[ratreal(y)])\}
13. ((\mlambda{}n.primrec(n;<a, b>\mlambda{}i,r. (s r))) i) = <x, v1>
14. ratreal(fst(<x, v1>)) \mmember{} [ratreal(a), ratreal(b)]
15. ratreal(snd(<x, v1>)) \mmember{} [ratreal(a), ratreal(b)]
16. ratreal(fst(<x, v1>)) \mleq{} ratreal(fst((s <x, v1>)))
17. ratreal(fst(<x, v1>)) \mleq{} ratreal(snd(<x, v1>))
18. ratreal(snd((s <x, v1>))) \mleq{} ratreal(snd(<x, v1>))
19. g[ratreal(fst(<x, v1>))] \mleq{} r0
20. r0 \mleq{} g[ratreal(snd(<x, v1>))]
\mvdash{} (ratreal(v1) - ratreal(x)) = (rinv(r(2))\^{}i * (ratreal(b) - ratreal(a)))
By
Latex:
Assert \mkleeneopen{}\mforall{}i:\mBbbN{}
((ratreal(snd(((\mlambda{}n.primrec(n;<a, b>\mlambda{}i,r. (s r))) i)))
- ratreal(fst(((\mlambda{}n.primrec(n;<a, b>\mlambda{}i,r. (s r))) i))))
= (rinv(r(2))\^{}i * (ratreal(b) - ratreal(a))))\mkleeneclose{}\mcdot{}
Home
Index