Step
*
1
4
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))))
⊢ ¬¬((∃c:ℝ. ∀x:ℝ. (f(x) = rcos(c * x))) ∨ (∃c:ℝ. ∀x:ℝ. (f(x) = cosh(c * x))))
BY
{ Assert ⌜∃a:ℝ. ((r0 < a) ∧ (∀x:{x:ℝ| x ∈ [-(a), a]} . (r0 < f(x))))⌝⋅ }
1
.....assertion.....
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))))
⊢ ∃a:ℝ. ((r0 < a) ∧ (∀x:{x:ℝ| x ∈ [-(a), a]} . (r0 < f(x))))
2
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. ∃a:ℝ. ((r0 < a) ∧ (∀x:{x:ℝ| x ∈ [-(a), a]} . (r0 < f(x))))
⊢ ¬¬((∃c:ℝ. ∀x:ℝ. (f(x) = rcos(c * x))) ∨ (∃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)))
\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))))
\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:
Assert \mkleeneopen{}\mexists{}a:\mBbbR{}. ((r0 < a) \mwedge{} (\mforall{}x:\{x:\mBbbR{}| x \mmember{} [-(a), a]\} . (r0 < f(x))))\mkleeneclose{}\mcdot{}
Home
Index