Step
*
1
4
1
1
1
1
2
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))
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. a : ℝ
11. r0 < a
12. ∀x:{x:ℝ| x ∈ [-(a), a]} . (r0 < f(x))
13. r0 < f(a)
14. r1 < f(a)
⊢ ¬¬((∃c:ℝ. ∀x:ℝ. (f(x) = rcos(c * x))) ∨ (∃c:ℝ. ∀x:ℝ. (f(x) = cosh(c * x))))
BY
{ ((RemoveDoubleNegation THENA Auto) THEN (OrRight THENA 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. a : ℝ
11. r0 < a
12. ∀x:{x:ℝ| x ∈ [-(a), a]} . (r0 < f(x))
13. r0 < f(a)
14. r1 < f(a)
⊢ ∃c:ℝ. ∀x:ℝ. (f(x) = cosh(c * 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))
8. \mforall{}n:\mBbbZ{}. \mforall{}y:\mBbbR{}. (f(r(n + 1) * y) = ((r(2) * f(y) * f(r(n) * y)) - f(r(n - 1) * y)))
9. \mforall{}t:\mBbbR{}. ((f((t/r(2))) * f((t/r(2)))) = (f(t) + r1/r(2)))
10. a : \mBbbR{}
11. r0 < a
12. \mforall{}x:\{x:\mBbbR{}| x \mmember{} [-(a), a]\} . (r0 < f(x))
13. r0 < f(a)
14. r1 < f(a)
\mvdash{} \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:
((RemoveDoubleNegation THENA Auto) THEN (OrRight THENA Auto))
Home
Index