---

Step * 1 1 3 2 1 2 2 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)))
22. ∀m:ℕ. (f((a/r(2^m))) = g((a/r(2^m))))
23. ∀m:ℕ. ∀x:ℝ.  ((f(x) = g(x)) ⇒ (f(r(m) * x) = g(r(m) * x)))
24. ∀n:ℕ. ∀m:ℕ+.  (f(r(n) * (a/r(2^m))) = g(r(n) * (a/r(2^m))))
25. ∀n:ℤ. ∀m:ℕ+.  (f(r(n) * (a/r(2^m))) = g(r(n) * (a/r(2^m))))
26. u : {a:ℝ| a ∈ (-∞, ∞)} 
27. v : {a:ℝ| a ∈ (-∞, ∞)} 
28. u ≠ v
29. x1 : {x:ℝ| True} 
30. n : ℤ
31. m : ℕ+
32. x1 = (r(n) * (a/r(2^m)))
⊢ f(x1) = g(x1)
BY
{ (Unfold `r-ap` 0
   THEN Fold `rfun-ap` 0
   THEN RWO "-1" 0
   THEN Auto
   THEN Fold
   `rfun-ap` 0⋅
   THEN BackThruSomeHyp
   THEN Auto) }

---

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)))
22.  \mforall{}m:\mBbbN{}.  (f((a/r(2\^{}m)))  =  g((a/r(2\^{}m))))
23.  \mforall{}m:\mBbbN{}.  \mforall{}x:\mBbbR{}.    ((f(x)  =  g(x))  {}\mRightarrow{}  (f(r(m)  *  x)  =  g(r(m)  *  x)))
24.  \mforall{}n:\mBbbN{}.  \mforall{}m:\mBbbN{}\msupplus{}.    (f(r(n)  *  (a/r(2\^{}m)))  =  g(r(n)  *  (a/r(2\^{}m))))
25.  \mforall{}n:\mBbbZ{}.  \mforall{}m:\mBbbN{}\msupplus{}.    (f(r(n)  *  (a/r(2\^{}m)))  =  g(r(n)  *  (a/r(2\^{}m))))
26.  u  :  \{a:\mBbbR{}|  a  \mmember{}  (-\minfty{},  \minfty{})\} 
27.  v  :  \{a:\mBbbR{}|  a  \mmember{}  (-\minfty{},  \minfty{})\} 
28.  u  \mneq{}  v
29.  x1  :  \{x:\mBbbR{}|  True\} 
30.  n  :  \mBbbZ{}
31.  m  :  \mBbbN{}\msupplus{}
32.  x1  =  (r(n)  *  (a/r(2\^{}m)))
\mvdash{}  f(x1)  =  g(x1)


By

---

Latex:
(Unfold  `r-ap`  0
  THEN  Fold  `rfun-ap`  0
  THEN  RWO  "-1"  0
  THEN  Auto
  THEN  Fold
  `rfun-ap`  0\mcdot{}
  THEN  BackThruSomeHyp
  THEN  Auto)

---

Home Index