---

Step * of Lemma DAlembert-equation-iff

∀f:ℝ ⟶ ℝ
  ((∀x,y:ℝ.  ((x = y) ⇒ (f(x) = f(y)))) ∧ (∀x,y:ℝ.  ((f(x + y) + f(x - y)) = (r(2) * f(x) * f(y))))
  ⇐⇒ (∀x:ℝ. (f(x) = r0)) ∨ (¬¬((∃c:ℝ. ∀x:ℝ. (f(x) = rcos(c * x))) ∨ (∃c:ℝ. ∀x:ℝ. (f(x) = cosh(c * x))))))
BY
{ (Assert ∀f:ℝ ⟶ ℝ
            (((∃c:ℝ. ∀x:ℝ. (f(x) = rcos(c * x))) ∨ (∃c:ℝ. ∀x:ℝ. (f(x) = cosh(c * x))))
            ⇒ (((∀x,y:ℝ.  ((x = y) ⇒ (f(x) = f(y)))) ∧ (∀x,y:ℝ.  ((f(x + y) + f(x - y)) = (r(2) * f(x) * f(y)))))
               ∧ (f(r0) = r1))) BY
         (Auto
          THEN SplitOrHyps
          THEN ExRepD
          THEN Try (Fold `rfun-ap` 0)
          THEN Try ((RWO "2 3" 0 THEN Auto))
          THEN Try (((Assert (c * (x + y)) = ((c * x) + (c * y)) BY
                            Auto)
                     THEN (Assert (c * (x - y)) = ((c * x) + -(c * y)) BY
                                 Auto)
                     THEN (RWW "-1 -2 rcos-radd cosh-radd" 0 THENA Auto)
                     THEN RWW "rcos-rminus rsin-rminus cosh-rminus sinh-rminus" 0
                     THEN Auto))
          THEN nRNorm 0
          THEN Auto)) }

1
1. ∀f:ℝ ⟶ ℝ
     (((∃c:ℝ. ∀x:ℝ. (f(x) = rcos(c * x))) ∨ (∃c:ℝ. ∀x:ℝ. (f(x) = cosh(c * x))))
     ⇒ (((∀x,y:ℝ.  ((x = y) ⇒ (f(x) = f(y)))) ∧ (∀x,y:ℝ.  ((f(x + y) + f(x - y)) = (r(2) * f(x) * f(y)))))
        ∧ (f(r0) = r1)))
⊢ ∀f:ℝ ⟶ ℝ
    ((∀x,y:ℝ.  ((x = y) ⇒ (f(x) = f(y)))) ∧ (∀x,y:ℝ.  ((f(x + y) + f(x - y)) = (r(2) * f(x) * f(y))))
    ⇐⇒ (∀x:ℝ. (f(x) = r0)) ∨ (¬¬((∃c:ℝ. ∀x:ℝ. (f(x) = rcos(c * x))) ∨ (∃c:ℝ. ∀x:ℝ. (f(x) = cosh(c * x))))))

---

Latex:

---

Latex:
\mforall{}f:\mBbbR{}  {}\mrightarrow{}  \mBbbR{}
    ((\mforall{}x,y:\mBbbR{}.    ((x  =  y)  {}\mRightarrow{}  (f(x)  =  f(y))))  \mwedge{}  (\mforall{}x,y:\mBbbR{}.    ((f(x  +  y)  +  f(x  -  y))  =  (r(2)  *  f(x)  *  f(y))))
    \mLeftarrow{}{}\mRightarrow{}  (\mforall{}x:\mBbbR{}.  (f(x)  =  r0))
            \mvee{}  (\mneg{}\mneg{}((\mexists{}c:\mBbbR{}.  \mforall{}x:\mBbbR{}.  (f(x)  =  rcos(c  *  x)))  \mvee{}  (\mexists{}c:\mBbbR{}.  \mforall{}x:\mBbbR{}.  (f(x)  =  cosh(c  *  x))))))


By

---

Latex:
(Assert  \mforall{}f:\mBbbR{}  {}\mrightarrow{}  \mBbbR{}
                    (((\mexists{}c:\mBbbR{}.  \mforall{}x:\mBbbR{}.  (f(x)  =  rcos(c  *  x)))  \mvee{}  (\mexists{}c:\mBbbR{}.  \mforall{}x:\mBbbR{}.  (f(x)  =  cosh(c  *  x))))
                    {}\mRightarrow{}  (((\mforall{}x,y:\mBbbR{}.    ((x  =  y)  {}\mRightarrow{}  (f(x)  =  f(y))))
                          \mwedge{}  (\mforall{}x,y:\mBbbR{}.    ((f(x  +  y)  +  f(x  -  y))  =  (r(2)  *  f(x)  *  f(y)))))
                          \mwedge{}  (f(r0)  =  r1)))  BY
              (Auto
                THEN  SplitOrHyps
                THEN  ExRepD
                THEN  Try  (Fold  `rfun-ap`  0)
                THEN  Try  ((RWO  "2  3"  0  THEN  Auto))
                THEN  Try  (((Assert  (c  *  (x  +  y))  =  ((c  *  x)  +  (c  *  y))  BY
                                                    Auto)
                                      THEN  (Assert  (c  *  (x  -  y))  =  ((c  *  x)  +  -(c  *  y))  BY
                                                              Auto)
                                      THEN  (RWW  "-1  -2  rcos-radd  cosh-radd"  0  THENA  Auto)
                                      THEN  RWW  "rcos-rminus  rsin-rminus  cosh-rminus  sinh-rminus"  0
                                      THEN  Auto))
                THEN  nRNorm  0
                THEN  Auto))

---

Home Index