---

Step * 1 1 2 of Lemma DAlembert-equation-lemma

.....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)))
BY
{ (((Assert m ∈ ℕ BY (Lemmaize [-2] THEN Auto)) THEN (Assert m - 1 ∈ ℕ BY (Lemmaize [-3] THEN Auto)))
   THEN (InstHyp [⌜m⌝] (-7)⋅ THENA Auto)
   THEN D -1) }

1
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))))
25. m ∈ ℕ
26. m - 1 ∈ ℕ
27. r0 < f((a/r(2^m)))
28. r0 < g((a/r(2^m)))
⊢ f((a/r(2^m))) = g((a/r(2^m)))

---

Latex:

---

Latex:
.....upcase..... 
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)))
22.  m  :  \mBbbZ{}
23.  0  <  m
24.  f((a/r(2\^{}(m  -  1))))  =  g((a/r(2\^{}(m  -  1))))
\mvdash{}  f((a/r(2\^{}m)))  =  g((a/r(2\^{}m)))


By

---

Latex:
(((Assert  m  \mmember{}  \mBbbN{}  BY  (Lemmaize  [-2]  THEN  Auto))  THEN  (Assert  m  -  1  \mmember{}  \mBbbN{}  BY  (Lemmaize  [-3]  THEN  Auto)))
  THEN  (InstHyp  [\mkleeneopen{}m\mkleeneclose{}]  (-7)\mcdot{}  THENA  Auto)
  THEN  D  -1)

---

Home Index