---

Step * 1 4 1 1 1 1 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:ℝ ⟶ ℝ
     (((∀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))
     ⇒ ((∀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))))))
3. f : ℝ ⟶ ℝ
4. ∀x,y:ℝ.  ((x = y) ⇒ (f(x) = f(y)))
5. ∀x,y:ℝ.  ((f(x + y) + f(x - y)) = (r(2) * f(x) * f(y)))
6. f(r0) = r1
7. (∀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))))
8. f[x] continuous for x ∈ (-∞, ∞)
⊢ ∃a:ℝ. ((r0 < a) ∧ (∀x:{x:ℝ| x ∈ [-(a), a]} . (r0 < f(x))))
BY
{ (((D -1 With ⌜1⌝  THENM (RepUR ``i-approx`` -1 THEN (D -1 With ⌜2⌝  THENA Auto)))
    THENA (MemTypeCD THEN Auto THEN RepUR ``i-approx`` 0 THEN Auto)
    )
   THEN D -1
   THEN D 0 With ⌜rmin(d;r1)⌝ 
   THEN Auto
   THEN Unhide
   THEN Auto
   THEN Try ((BLemma `rmin_strict_ub` 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)))
2. ∀f:ℝ ⟶ ℝ
     (((∀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))
     ⇒ ((∀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))))))
3. f : ℝ ⟶ ℝ
4. ∀x,y:ℝ.  ((x = y) ⇒ (f(x) = f(y)))
5. ∀x,y:ℝ.  ((f(x + y) + f(x - y)) = (r(2) * f(x) * f(y)))
6. f(r0) = r1
7. ∀x:ℝ. (f(-(x)) = f(x))
8. ∀n:ℤ. ∀y:ℝ.  (f(r(n + 1) * y) = ((r(2) * f(y) * f(r(n) * y)) - f(r(n - 1) * y)))
9. ∀t:ℝ. ((f((t/r(2))) * f((t/r(2)))) = (f(t) + r1/r(2)))
10. d : ℝ
11. r0 < d
12. ∀x,y:ℝ.  (((r(-1) ≤ x) ∧ (x ≤ r1)) ⇒ ((r(-1) ≤ y) ∧ (y ≤ r1)) ⇒ (|x - y| ≤ d) ⇒ (|f[x] - f[y]| ≤ (r1/r(2))))
13. r0 < rmin(d;r1)
14. x : {x:ℝ| x ∈ [-(rmin(d;r1)), rmin(d;r1)]} 
⊢ r0 < f(x)

---

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.  \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))))
          \mwedge{}  (f(r0)  =  r1))
          {}\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))))))
3.  f  :  \mBbbR{}  {}\mrightarrow{}  \mBbbR{}
4.  \mforall{}x,y:\mBbbR{}.    ((x  =  y)  {}\mRightarrow{}  (f(x)  =  f(y)))
5.  \mforall{}x,y:\mBbbR{}.    ((f(x  +  y)  +  f(x  -  y))  =  (r(2)  *  f(x)  *  f(y)))
6.  f(r0)  =  r1
7.  (\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))))
8.  f[x]  continuous  for  x  \mmember{}  (-\minfty{},  \minfty{})
\mvdash{}  \mexists{}a:\mBbbR{}.  ((r0  <  a)  \mwedge{}  (\mforall{}x:\{x:\mBbbR{}|  x  \mmember{}  [-(a),  a]\}  .  (r0  <  f(x))))


By

---

Latex:
(((D  -1  With  \mkleeneopen{}1\mkleeneclose{}    THENM  (RepUR  ``i-approx``  -1  THEN  (D  -1  With  \mkleeneopen{}2\mkleeneclose{}    THENA  Auto)))
    THENA  (MemTypeCD  THEN  Auto  THEN  RepUR  ``i-approx``  0  THEN  Auto)
    )
  THEN  D  -1
  THEN  D  0  With  \mkleeneopen{}rmin(d;r1)\mkleeneclose{} 
  THEN  Auto
  THEN  Unhide
  THEN  Auto
  THEN  Try  ((BLemma  `rmin\_strict\_ub`  THEN  Auto)))

---

Home Index