---

Step * of Lemma DAlembert-equation-lemma

∀f,g:ℝ ⟶ ℝ.
  ((∀x,y:ℝ.  ((x = y) ⇒ (f(x) = f(y))))
  ⇒ (∀x,y:ℝ.  ((x = y) ⇒ (g(x) = g(y))))
  ⇒ ((∀x:ℝ. (f(-(x)) = f(x)))
     ∧ (∀n:ℤ. ∀y:ℝ.  (f(r(n + 1) * y) = ((r(2) * f(y) * f(r(n) * y)) - f(r(n - 1) * y))))
     ∧ (∀t:ℝ. ((f((t/r(2))) * f((t/r(2)))) = (f(t) + r1/r(2)))))
  ⇒ ((∀x:ℝ. (g(-(x)) = g(x)))
     ∧ (∀n:ℤ. ∀y:ℝ.  (g(r(n + 1) * y) = ((r(2) * g(y) * g(r(n) * y)) - g(r(n - 1) * y))))
     ∧ (∀t:ℝ. ((g((t/r(2))) * g((t/r(2)))) = (g(t) + r1/r(2)))))
  ⇒ (f(r0) = g(r0))
  ⇒ (∀a:ℝ
        ((r0 < a)
        ⇒ (f(a) = g(a))
        ⇒ (∀x:{x:ℝ| x ∈ [-(a), a]} . (r0 < f(x)))
        ⇒ (∀x:{x:ℝ| x ∈ [-(a), a]} . (r0 < g(x)))
        ⇒ (∀x:ℝ. (f(x) = g(x))))))
BY
{ (Auto
   THEN (Assert ∀m:ℕ. (r1 ≤ r(2^m)) BY
               Auto)
   THEN (Assert ∀m:ℕ. ((a/r(2^m)) ∈ [-(a), a]) BY
               (ParallelLast
                THEN Reduce 0
                THEN D 0
                THEN nRMul ⌜r(2^m)⌝ 0⋅
                THEN Auto
                THEN nRMul ⌜a⌝ (-1)⋅
                THEN Auto
                THEN (nRMul ⌜r(-1)⌝ 0⋅ THEN Auto)
                THEN (RWO "-1<" 0 THEN Auto)
                THEN RWO "13<" 0
                THEN Auto))
   THEN (Assert ∀m:ℕ. ((r0 < f((a/r(2^m)))) ∧ (r0 < g((a/r(2^m))))) BY
               (ParallelLast THEN D 0 THEN BackThruSomeHyp))) }

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)))))
⊢ f(x) = g(x)

---

Latex:

---

Latex:
\mforall{}f,g:\mBbbR{}  {}\mrightarrow{}  \mBbbR{}.
    ((\mforall{}x,y:\mBbbR{}.    ((x  =  y)  {}\mRightarrow{}  (f(x)  =  f(y))))
    {}\mRightarrow{}  (\mforall{}x,y:\mBbbR{}.    ((x  =  y)  {}\mRightarrow{}  (g(x)  =  g(y))))
    {}\mRightarrow{}  ((\mforall{}x:\mBbbR{}.  (f(-(x))  =  f(x)))
          \mwedge{}  (\mforall{}n:\mBbbZ{}.  \mforall{}y:\mBbbR{}.    (f(r(n  +  1)  *  y)  =  ((r(2)  *  f(y)  *  f(r(n)  *  y))  -  f(r(n  -  1)  *  y))))
          \mwedge{}  (\mforall{}t:\mBbbR{}.  ((f((t/r(2)))  *  f((t/r(2))))  =  (f(t)  +  r1/r(2)))))
    {}\mRightarrow{}  ((\mforall{}x:\mBbbR{}.  (g(-(x))  =  g(x)))
          \mwedge{}  (\mforall{}n:\mBbbZ{}.  \mforall{}y:\mBbbR{}.    (g(r(n  +  1)  *  y)  =  ((r(2)  *  g(y)  *  g(r(n)  *  y))  -  g(r(n  -  1)  *  y))))
          \mwedge{}  (\mforall{}t:\mBbbR{}.  ((g((t/r(2)))  *  g((t/r(2))))  =  (g(t)  +  r1/r(2)))))
    {}\mRightarrow{}  (f(r0)  =  g(r0))
    {}\mRightarrow{}  (\mforall{}a:\mBbbR{}
                ((r0  <  a)
                {}\mRightarrow{}  (f(a)  =  g(a))
                {}\mRightarrow{}  (\mforall{}x:\{x:\mBbbR{}|  x  \mmember{}  [-(a),  a]\}  .  (r0  <  f(x)))
                {}\mRightarrow{}  (\mforall{}x:\{x:\mBbbR{}|  x  \mmember{}  [-(a),  a]\}  .  (r0  <  g(x)))
                {}\mRightarrow{}  (\mforall{}x:\mBbbR{}.  (f(x)  =  g(x))))))


By

---

Latex:
(Auto
  THEN  (Assert  \mforall{}m:\mBbbN{}.  (r1  \mleq{}  r(2\^{}m))  BY
                          Auto)
  THEN  (Assert  \mforall{}m:\mBbbN{}.  ((a/r(2\^{}m))  \mmember{}  [-(a),  a])  BY
                          (ParallelLast
                            THEN  Reduce  0
                            THEN  D  0
                            THEN  nRMul  \mkleeneopen{}r(2\^{}m)\mkleeneclose{}  0\mcdot{}
                            THEN  Auto
                            THEN  nRMul  \mkleeneopen{}a\mkleeneclose{}  (-1)\mcdot{}
                            THEN  Auto
                            THEN  (nRMul  \mkleeneopen{}r(-1)\mkleeneclose{}  0\mcdot{}  THEN  Auto)
                            THEN  (RWO  "-1<"  0  THEN  Auto)
                            THEN  RWO  "13<"  0
                            THEN  Auto))
  THEN  (Assert  \mforall{}m:\mBbbN{}.  ((r0  <  f((a/r(2\^{}m))))  \mwedge{}  (r0  <  g((a/r(2\^{}m)))))  BY
                          (ParallelLast  THEN  D  0  THEN  BackThruSomeHyp)))

---

Home Index