Step
*
1
1
of Lemma
DAlembert-equation-lemma
1. f : ℝ ⟶ ℝ
2. g : ℝ ⟶ ℝ
3. ∀x,y:ℝ. ((x = y) ⇒ (f(x) = f(y)))
4. ∀x,y:ℝ. ((x = y) ⇒ (g(x) = g(y)))
5. ∀x:ℝ. (f(-(x)) = f(x))
6. ∀n:ℤ. ∀y:ℝ. (f(r(n + 1) * y) = ((r(2) * f(y) * f(r(n) * y)) - f(r(n - 1) * y)))
7. ∀t:ℝ. ((f((t/r(2))) * f((t/r(2)))) = (f(t) + r1/r(2)))
8. ∀x:ℝ. (g(-(x)) = g(x))
9. ∀n:ℤ. ∀y:ℝ. (g(r(n + 1) * y) = ((r(2) * g(y) * g(r(n) * y)) - g(r(n - 1) * y)))
10. ∀t:ℝ. ((g((t/r(2))) * g((t/r(2)))) = (g(t) + r1/r(2)))
11. f(r0) = g(r0)
12. a : ℝ
13. r0 < a
14. f(a) = g(a)
15. ∀x:{x:ℝ| x ∈ [-(a), a]} . (r0 < f(x))
16. ∀x:{x:ℝ| x ∈ [-(a), a]} . (r0 < g(x))
17. x : ℝ
18. ∀m:ℕ. (r1 ≤ r(2^m))
19. ∀m:ℕ. ((a/r(2^m)) ∈ [-(a), a])
20. ∀m:ℕ. ((r0 < f((a/r(2^m)))) ∧ (r0 < g((a/r(2^m)))))
21. ∀m:ℕ+. ((a/r(2^m)) = ((a/r(2^(m - 1)))/r(2)))
⊢ f(x) = g(x)
BY
{ (Assert ∀m:ℕ. (f((a/r(2^m))) = g((a/r(2^m)))) BY
InductionOnNat) }
1
.....basecase.....
1. f : ℝ ⟶ ℝ
2. g : ℝ ⟶ ℝ
3. ∀x,y:ℝ. ((x = y) ⇒ (f(x) = f(y)))
4. ∀x,y:ℝ. ((x = y) ⇒ (g(x) = g(y)))
5. ∀x:ℝ. (f(-(x)) = f(x))
6. ∀n:ℤ. ∀y:ℝ. (f(r(n + 1) * y) = ((r(2) * f(y) * f(r(n) * y)) - f(r(n - 1) * y)))
7. ∀t:ℝ. ((f((t/r(2))) * f((t/r(2)))) = (f(t) + r1/r(2)))
8. ∀x:ℝ. (g(-(x)) = g(x))
9. ∀n:ℤ. ∀y:ℝ. (g(r(n + 1) * y) = ((r(2) * g(y) * g(r(n) * y)) - g(r(n - 1) * y)))
10. ∀t:ℝ. ((g((t/r(2))) * g((t/r(2)))) = (g(t) + r1/r(2)))
11. f(r0) = g(r0)
12. a : ℝ
13. r0 < a
14. f(a) = g(a)
15. ∀x:{x:ℝ| x ∈ [-(a), a]} . (r0 < f(x))
16. ∀x:{x:ℝ| x ∈ [-(a), a]} . (r0 < g(x))
17. x : ℝ
18. ∀m:ℕ. (r1 ≤ r(2^m))
19. ∀m:ℕ. ((a/r(2^m)) ∈ [-(a), a])
20. ∀m:ℕ. ((r0 < f((a/r(2^m)))) ∧ (r0 < g((a/r(2^m)))))
21. ∀m:ℕ+. ((a/r(2^m)) = ((a/r(2^(m - 1)))/r(2)))
22. m : ℤ
⊢ f((a/r(2^0))) = g((a/r(2^0)))
2
.....upcase.....
1. f : ℝ ⟶ ℝ
2. g : ℝ ⟶ ℝ
3. ∀x,y:ℝ. ((x = y) ⇒ (f(x) = f(y)))
4. ∀x,y:ℝ. ((x = y) ⇒ (g(x) = g(y)))
5. ∀x:ℝ. (f(-(x)) = f(x))
6. ∀n:ℤ. ∀y:ℝ. (f(r(n + 1) * y) = ((r(2) * f(y) * f(r(n) * y)) - f(r(n - 1) * y)))
7. ∀t:ℝ. ((f((t/r(2))) * f((t/r(2)))) = (f(t) + r1/r(2)))
8. ∀x:ℝ. (g(-(x)) = g(x))
9. ∀n:ℤ. ∀y:ℝ. (g(r(n + 1) * y) = ((r(2) * g(y) * g(r(n) * y)) - g(r(n - 1) * y)))
10. ∀t:ℝ. ((g((t/r(2))) * g((t/r(2)))) = (g(t) + r1/r(2)))
11. f(r0) = g(r0)
12. a : ℝ
13. r0 < a
14. f(a) = g(a)
15. ∀x:{x:ℝ| x ∈ [-(a), a]} . (r0 < f(x))
16. ∀x:{x:ℝ| x ∈ [-(a), a]} . (r0 < g(x))
17. x : ℝ
18. ∀m:ℕ. (r1 ≤ r(2^m))
19. ∀m:ℕ. ((a/r(2^m)) ∈ [-(a), a])
20. ∀m:ℕ. ((r0 < f((a/r(2^m)))) ∧ (r0 < g((a/r(2^m)))))
21. ∀m:ℕ+. ((a/r(2^m)) = ((a/r(2^(m - 1)))/r(2)))
22. m : ℤ
23. 0 < m
24. f((a/r(2^(m - 1)))) = g((a/r(2^(m - 1))))
⊢ f((a/r(2^m))) = g((a/r(2^m)))
3
1. f : ℝ ⟶ ℝ
2. g : ℝ ⟶ ℝ
3. ∀x,y:ℝ. ((x = y) ⇒ (f(x) = f(y)))
4. ∀x,y:ℝ. ((x = y) ⇒ (g(x) = g(y)))
5. ∀x:ℝ. (f(-(x)) = f(x))
6. ∀n:ℤ. ∀y:ℝ. (f(r(n + 1) * y) = ((r(2) * f(y) * f(r(n) * y)) - f(r(n - 1) * y)))
7. ∀t:ℝ. ((f((t/r(2))) * f((t/r(2)))) = (f(t) + r1/r(2)))
8. ∀x:ℝ. (g(-(x)) = g(x))
9. ∀n:ℤ. ∀y:ℝ. (g(r(n + 1) * y) = ((r(2) * g(y) * g(r(n) * y)) - g(r(n - 1) * y)))
10. ∀t:ℝ. ((g((t/r(2))) * g((t/r(2)))) = (g(t) + r1/r(2)))
11. f(r0) = g(r0)
12. a : ℝ
13. r0 < a
14. f(a) = g(a)
15. ∀x:{x:ℝ| x ∈ [-(a), a]} . (r0 < f(x))
16. ∀x:{x:ℝ| x ∈ [-(a), a]} . (r0 < g(x))
17. x : ℝ
18. ∀m:ℕ. (r1 ≤ r(2^m))
19. ∀m:ℕ. ((a/r(2^m)) ∈ [-(a), a])
20. ∀m:ℕ. ((r0 < f((a/r(2^m)))) ∧ (r0 < g((a/r(2^m)))))
21. ∀m:ℕ+. ((a/r(2^m)) = ((a/r(2^(m - 1)))/r(2)))
22. ∀m:ℕ. (f((a/r(2^m))) = g((a/r(2^m))))
⊢ f(x) = g(x)
Latex:
Latex:
1. f : \mBbbR{} {}\mrightarrow{} \mBbbR{}
2. g : \mBbbR{} {}\mrightarrow{} \mBbbR{}
3. \mforall{}x,y:\mBbbR{}. ((x = y) {}\mRightarrow{} (f(x) = f(y)))
4. \mforall{}x,y:\mBbbR{}. ((x = y) {}\mRightarrow{} (g(x) = g(y)))
5. \mforall{}x:\mBbbR{}. (f(-(x)) = f(x))
6. \mforall{}n:\mBbbZ{}. \mforall{}y:\mBbbR{}. (f(r(n + 1) * y) = ((r(2) * f(y) * f(r(n) * y)) - f(r(n - 1) * y)))
7. \mforall{}t:\mBbbR{}. ((f((t/r(2))) * f((t/r(2)))) = (f(t) + r1/r(2)))
8. \mforall{}x:\mBbbR{}. (g(-(x)) = g(x))
9. \mforall{}n:\mBbbZ{}. \mforall{}y:\mBbbR{}. (g(r(n + 1) * y) = ((r(2) * g(y) * g(r(n) * y)) - g(r(n - 1) * y)))
10. \mforall{}t:\mBbbR{}. ((g((t/r(2))) * g((t/r(2)))) = (g(t) + r1/r(2)))
11. f(r0) = g(r0)
12. a : \mBbbR{}
13. r0 < a
14. f(a) = g(a)
15. \mforall{}x:\{x:\mBbbR{}| x \mmember{} [-(a), a]\} . (r0 < f(x))
16. \mforall{}x:\{x:\mBbbR{}| x \mmember{} [-(a), a]\} . (r0 < g(x))
17. x : \mBbbR{}
18. \mforall{}m:\mBbbN{}. (r1 \mleq{} r(2\^{}m))
19. \mforall{}m:\mBbbN{}. ((a/r(2\^{}m)) \mmember{} [-(a), a])
20. \mforall{}m:\mBbbN{}. ((r0 < f((a/r(2\^{}m)))) \mwedge{} (r0 < g((a/r(2\^{}m)))))
21. \mforall{}m:\mBbbN{}\msupplus{}. ((a/r(2\^{}m)) = ((a/r(2\^{}(m - 1)))/r(2)))
\mvdash{} f(x) = g(x)
By
Latex:
(Assert \mforall{}m:\mBbbN{}. (f((a/r(2\^{}m))) = g((a/r(2\^{}m)))) BY
InductionOnNat)
Home
Index