---

Step * 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)))))
⊢ f(x) = g(x)
BY
{ (Assert ∀m:ℕ+. ((a/r(2^m)) = ((a/r(2^(m - 1)))/r(2))) BY
         (Auto
          THEN (Assert 1 ≤ 2^(m - 1) BY
                      Auto)
          THEN BLemma `fractions-req`
          THEN Auto
          THEN nRMul ⌜r(2^(m - 1))⌝ 0⋅
          THEN Auto
          THEN (RWW "rmul-assoc rmul-int" 0 THENA Auto)
          THEN BLemma `rmul_functionality`
          THEN Auto)) }

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)))
⊢ 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)))))
\mvdash{}  f(x)  =  g(x)


By

---

Latex:
(Assert  \mforall{}m:\mBbbN{}\msupplus{}.  ((a/r(2\^{}m))  =  ((a/r(2\^{}(m  -  1)))/r(2)))  BY
              (Auto
                THEN  (Assert  1  \mleq{}  2\^{}(m  -  1)  BY
                                        Auto)
                THEN  BLemma  `fractions-req`
                THEN  Auto
                THEN  nRMul  \mkleeneopen{}r(2\^{}(m  -  1))\mkleeneclose{}  0\mcdot{}
                THEN  Auto
                THEN  (RWW  "rmul-assoc  rmul-int"  0  THENA  Auto)
                THEN  BLemma  `rmul\_functionality`
                THEN  Auto))

---

Home Index