---

Step * 1 1 of Lemma DAlembert-equation-iff


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)))
2. f : ℝ ⟶ ℝ
3. ∀x,y:ℝ.  ((x = y) ⇒ (f(x) = f(y)))
4. ∀x,y:ℝ.  ((f(x + y) + f(x - y)) = (r(2) * f(x) * f(y)))
5. f(r0) = r1
6. x : ℝ
⊢ f(-(x)) = f(x)
BY
{ (Thin 1
   THEN (InstHyp [⌜r0⌝;⌜x⌝] 3⋅ THENA Auto)
   THEN (nRNorm (-1) THENA Auto)
   THEN Try ((Fold `rfun-ap` 0 THEN BHyp 2  THEN Auto))
   THEN RWO "4" (-1)
   THEN Auto) }

---

Latex:

---

Latex:

1.  \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)))
2.  f  :  \mBbbR{}  {}\mrightarrow{}  \mBbbR{}
3.  \mforall{}x,y:\mBbbR{}.    ((x  =  y)  {}\mRightarrow{}  (f(x)  =  f(y)))
4.  \mforall{}x,y:\mBbbR{}.    ((f(x  +  y)  +  f(x  -  y))  =  (r(2)  *  f(x)  *  f(y)))
5.  f(r0)  =  r1
6.  x  :  \mBbbR{}
\mvdash{}  f(-(x))  =  f(x)


By

---

Latex:
(Thin  1
  THEN  (InstHyp  [\mkleeneopen{}r0\mkleeneclose{};\mkleeneopen{}x\mkleeneclose{}]  3\mcdot{}  THENA  Auto)
  THEN  (nRNorm  (-1)  THENA  Auto)
  THEN  Try  ((Fold  `rfun-ap`  0  THEN  BHyp  2    THEN  Auto))
  THEN  RWO  "4"  (-1)
  THEN  Auto)

---

Home Index