Step
*
1
1
1
1
2
1
1
of Lemma
rational-IVT
1. a : ℝ
2. b : ℝ
3. f : (ℤ × ℕ+) ⟶ (ℤ × ℕ+)
4. g : {x:ℝ| x ∈ [a, b]} ⟶ ℝ
5. (a < b)
∧ ((g[a] * g[b]) < r0)
∧ (∀x,y:{x:ℝ| x ∈ [a, b]} . ((x = y) ⇒ (g[x] = g[y])))
∧ (∀r:ℤ × ℕ+. ((ratreal(r) ∈ [a, b]) ⇒ (g[ratreal(r)] = ratreal(f[r]))))
6. ∀n:ℕ+. (ratreal(<(a (2 * n)) + 2, 4 * n>) = above a within 1/n)
7. ∀n:ℕ+. (ratreal(<(b (2 * n)) - 2, 4 * n>) = (below b within 1/n))
8. ∃m:{1...}. (↑((λn.((a (2 * n)) + 4 ≤z b (2 * n) ∧b fst(ratmul(f[<(a (2 * n)) + 2, 4 * n>];f[<(b (2 * n)) - 2, 4 * n>]\000C)) <z 0)) m))
9. N : ℕ+
10. mu-ge(λn.((a (2 * n)) + 4 ≤z b (2 * n) ∧b fst(ratmul(f[<(a (2 * n)) + 2, 4 * n>];f[<(b (2 * n)) - 2, 4 * n>])) <z 0)\000C;1) = N ∈ ℕ+
11. (↑((λn.((a (2 * n)) + 4 ≤z b (2 * n) ∧b fst(ratmul(f[<(a (2 * n)) + 2, 4 * n>];f[<(b (2 * n)) - 2, 4 * n>])) <z 0)) \000CN))
∧ (∀[i:ℕ+N]. (¬↑((λn.((a (2 * n)) + 4 ≤z b (2 * n) ∧b fst(ratmul(f[<(a (2 * n)) + 2, 4 * n>];f[<(b (2 * n)) - 2, 4 * n>]\000C)) <z 0)) i)))
⊢ (ratreal(ratmul(f[<(a (2 * N)) + 2, 4 * N>];f[<(b (2 * N)) - 2, 4 * N>])) < r0) ∧ (((a (2 * N)) + 4) ≤ (b (2 * N)))
BY
{ (D -1 THEN Thin (-1) THEN Thin (-2) THEN Reduce -1) }
1
1. a : ℝ
2. b : ℝ
3. f : (ℤ × ℕ+) ⟶ (ℤ × ℕ+)
4. g : {x:ℝ| x ∈ [a, b]} ⟶ ℝ
5. (a < b)
∧ ((g[a] * g[b]) < r0)
∧ (∀x,y:{x:ℝ| x ∈ [a, b]} . ((x = y) ⇒ (g[x] = g[y])))
∧ (∀r:ℤ × ℕ+. ((ratreal(r) ∈ [a, b]) ⇒ (g[ratreal(r)] = ratreal(f[r]))))
6. ∀n:ℕ+. (ratreal(<(a (2 * n)) + 2, 4 * n>) = above a within 1/n)
7. ∀n:ℕ+. (ratreal(<(b (2 * n)) - 2, 4 * n>) = (below b within 1/n))
8. ∃m:{1...}. (↑((λn.((a (2 * n)) + 4 ≤z b (2 * n) ∧b fst(ratmul(f[<(a (2 * n)) + 2, 4 * n>];f[<(b (2 * n)) - 2, 4 * n>]\000C)) <z 0)) m))
9. N : ℕ+
10. ↑((a (2 * N)) + 4 ≤z b (2 * N) ∧b fst(ratmul(f[<(a (2 * N)) + 2, 4 * N>];f[<(b (2 * N)) - 2, 4 * N>])) <z 0)
⊢ (ratreal(ratmul(f[<(a (2 * N)) + 2, 4 * N>];f[<(b (2 * N)) - 2, 4 * N>])) < r0) ∧ (((a (2 * N)) + 4) ≤ (b (2 * N)))
Latex:
Latex:
1. a : \mBbbR{}
2. b : \mBbbR{}
3. f : (\mBbbZ{} \mtimes{} \mBbbN{}\msupplus{}) {}\mrightarrow{} (\mBbbZ{} \mtimes{} \mBbbN{}\msupplus{})
4. g : \{x:\mBbbR{}| x \mmember{} [a, b]\} {}\mrightarrow{} \mBbbR{}
5. (a < b)
\mwedge{} ((g[a] * g[b]) < r0)
\mwedge{} (\mforall{}x,y:\{x:\mBbbR{}| x \mmember{} [a, b]\} . ((x = y) {}\mRightarrow{} (g[x] = g[y])))
\mwedge{} (\mforall{}r:\mBbbZ{} \mtimes{} \mBbbN{}\msupplus{}. ((ratreal(r) \mmember{} [a, b]) {}\mRightarrow{} (g[ratreal(r)] = ratreal(f[r]))))
6. \mforall{}n:\mBbbN{}\msupplus{}. (ratreal(<(a (2 * n)) + 2, 4 * n>) = above a within 1/n)
7. \mforall{}n:\mBbbN{}\msupplus{}. (ratreal(<(b (2 * n)) - 2, 4 * n>) = (below b within 1/n))
8. \mexists{}m:\{1...\}
(\muparrow{}((\mlambda{}n.((a (2 * n)) + 4 \mleq{}z b (2 * n) \mwedge{}\msubb{} fst(ratmul(f[<(a (2 * n)) + 2, 4 * n>];f[<(b (2 * n)) - \000C2, 4 * n>])) <z 0)) m))
9. N : \mBbbN{}\msupplus{}
10. mu-ge(\mlambda{}n.((a (2 * n)) + 4 \mleq{}z b (2 * n) \mwedge{}\msubb{} fst(ratmul(f[<(a (2 * n)) + 2, 4 * n>];f[<(b (2 * n)) \000C- 2, 4 * n>])) <z 0);1) = N
11. (\muparrow{}((\mlambda{}n.((a (2 * n)) + 4 \mleq{}z b (2 * n) \mwedge{}\msubb{} fst(ratmul(f[<(a (2 * n)) + 2, 4 * n>];f[<(b (2 * n)) - \000C2, 4 * n>])) <z 0)) N))
\mwedge{} (\mforall{}[i:\mBbbN{}\msupplus{}N]
(\mneg{}\muparrow{}((\mlambda{}n.((a (2 * n)) + 4 \mleq{}z b (2 * n) \mwedge{}\msubb{} fst(ratmul(f[<(a (2 * n)) + 2, 4 * n>];f[<(b (2 * n)) \000C- 2, 4 * n>])) <z 0)) i)))
\mvdash{} (ratreal(ratmul(f[<(a (2 * N)) + 2, 4 * N>];f[<(b (2 * N)) - 2, 4 * N>])) < r0) \mwedge{} (((a (2 * N)) + \000C4) \mleq{} (b (2 * N)))
By
Latex:
(D -1 THEN Thin (-1) THEN Thin (-2) THEN Reduce -1)
Home
Index