Step
*
1
2
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))
∧ (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)])} )
⊢ ∀i:ℕ
((ratreal(fst(((λn.primrec(n;<a, b>;λi,r. (s r))) i))) ∈ [ratreal(a), ratreal(b)])
∧ (ratreal(snd(((λn.primrec(n;<a, b>;λi,r. (s r))) i))) ∈ [ratreal(a), ratreal(b)])
∧ (ratreal(fst(((λn.primrec(n;<a, b>;λi,r. (s r))) i))) ≤ ratreal(fst(((λn.primrec(n;<a, b>;λi,r. (s r))) (i + 1))))\000C)
∧ (ratreal(fst(((λn.primrec(n;<a, b>;λi,r. (s r))) i))) ≤ ratreal(snd(((λn.primrec(n;<a, b>;λi,r. (s r))) i))))
∧ (ratreal(snd(((λn.primrec(n;<a, b>;λi,r. (s r))) (i + 1)))) ≤ ratreal(snd(((λn.primrec(n;<a, b>;λi,r. (s r))) i)))\000C)
∧ (g[ratreal(fst(((λn.primrec(n;<a, b>;λi,r. (s r))) i)))] ≤ r0)
∧ (r0 ≤ g[ratreal(snd(((λn.primrec(n;<a, b>;λi,r. (s r))) 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)))))
BY
{ ((D 0 THENA Auto)
THEN (Subst' (λn.primrec(n;<a, b>;λi,r. (s r))) (i + 1) ~ s ((λn.primrec(n;<a, b>;λi,r. (s r))) i) 0
THENM (GenConclTerm ⌜(λn.primrec(n;<a, b>;λi,r. (s r))) i⌝⋅ THENA Auto)
)
) }
1
.....equality.....
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 : ℕ
⊢ (λn.primrec(n;<a, b>;λi,r. (s r))) (i + 1) ~ s ((λn.primrec(n;<a, b>;λi,r. (s r))) i)
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. v : 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)])}
12. ((λn.primrec(n;<a, b>;λi,r. (s r))) i)
= v
∈ (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(v)) ∈ [ratreal(a), ratreal(b)])
∧ (ratreal(snd(v)) ∈ [ratreal(a), ratreal(b)])
∧ (ratreal(fst(v)) ≤ ratreal(fst((s v))))
∧ (ratreal(fst(v)) ≤ ratreal(snd(v)))
∧ (ratreal(snd((s v))) ≤ ratreal(snd(v)))
∧ (g[ratreal(fst(v))] ≤ r0)
∧ (r0 ≤ g[ratreal(snd(v))])
∧ ((ratreal(snd(v)) - ratreal(fst(v))) = (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)])\} )
\mvdash{} \mforall{}i:\mBbbN{}
((ratreal(fst(((\mlambda{}n.primrec(n;<a, b>\mlambda{}i,r. (s r))) i))) \mmember{} [ratreal(a), ratreal(b)])
\mwedge{} (ratreal(snd(((\mlambda{}n.primrec(n;<a, b>\mlambda{}i,r. (s r))) i))) \mmember{} [ratreal(a), ratreal(b)])
\mwedge{} (ratreal(fst(((\mlambda{}n.primrec(n;<a, b>\mlambda{}i,r. (s r))) i))) \mleq{} ratreal(fst(((\mlambda{}n.primrec(n;<a, b>\mlambda{}i,r\000C. (s r)))
(i + 1)))))
\mwedge{} (ratreal(fst(((\mlambda{}n.primrec(n;<a, b>\mlambda{}i,r. (s r))) i))) \mleq{} ratreal(snd(((\mlambda{}n.primrec(n;<a, b>\mlambda{}i,r\000C. (s r)))
i))))
\mwedge{} (ratreal(snd(((\mlambda{}n.primrec(n;<a, b>\mlambda{}i,r. (s r)))
(i + 1)))) \mleq{} ratreal(snd(((\mlambda{}n.primrec(n;<a, b>\mlambda{}i,r. (s r))) i))))
\mwedge{} (g[ratreal(fst(((\mlambda{}n.primrec(n;<a, b>\mlambda{}i,r. (s r))) i)))] \mleq{} r0)
\mwedge{} (r0 \mleq{} g[ratreal(snd(((\mlambda{}n.primrec(n;<a, b>\mlambda{}i,r. (s r))) i)))])
\mwedge{} ((ratreal(snd(((\mlambda{}n.primrec(n;<a, b>\mlambda{}i,r. (s r))) i))) - ratreal(fst(((\mlambda{}n.primrec(n;<a, b>\mlambda{}i,\000Cr. (s r)))
i))))
= (rinv(r(2))\^{}i * (ratreal(b) - ratreal(a)))))
By
Latex:
((D 0 THENA Auto)
THEN (Subst' (\mlambda{}n.primrec(n;<a, b>\mlambda{}i,r. (s r))) (i + 1) \msim{} s ((\mlambda{}n.primrec(n;<a, b>\mlambda{}i,r. (s r))) i) \000C0
THENM (GenConclTerm \mkleeneopen{}(\mlambda{}n.primrec(n;<a, b>\mlambda{}i,r. (s r))) i\mkleeneclose{}\mcdot{} THENA Auto)
)
)
Home
Index