Step
*
1
1
1
1
of Lemma
cos-sin-equation
1. f : ℝ ⟶ ℝ
2. g : ℝ ⟶ ℝ
3. ∀x,y:ℝ. ((x = y) ⇒ (f(x) = f(y)))
4. ∀x,y:ℝ. ((x = y) ⇒ (g(x) = g(y)))
5. ∀x,y:ℝ. (f(x - y) = ((f(x) * f(y)) + (g(x) * g(y))))
6. a : ℝ
7. f(a) ≠ f(r0)
8. b : ℝ
9. g(-(b)) ≠ g(b)
10. ∀x,y:ℝ. (f(x - y) = f(y - x))
11. ∀y:ℝ. (f(-(y)) = f(y))
12. ∀y:ℝ. (g(-(y)) = -(g(y)))
13. g(r0) = r0
14. d : ℝ
15. f(d) ≠ r0
16. f(r0) = r1
17. ∀x:ℝ. ((f(x)^2 + g(x)^2) = r1)
18. ∀x:ℝ. (|f(x)| ≤ r1)
19. ∀x,y:ℝ. ((f(x - -(y)) + f(x - y)) = (r(2) * f(x) * f(y)))
20. ∀x,y:ℝ. ((f(x + y) + f(x - y)) = (r(2) * f(x) * f(y)))
⊢ ¬¬((∃c:ℝ
((r0 ≤ (c - c^2)) ∧ (∀x:ℝ. (f(x) = c)) ∧ ((∀x:ℝ. (g(x) = rsqrt(c - c^2))) ∨ (∀x:ℝ. (g(x) = -(rsqrt(c - c^2)))))))
∨ (∃a:ℝ. (a ≠ r0 ∧ (∀x:ℝ. (f(x) = rcos(a * x))) ∧ (∀x:ℝ. (g(x) = rsin(a * x))))))
BY
{ ((InstLemma `DAlembert-equation-iff` [⌜f⌝]⋅ THENA Auto) THEN D -1 THEN Thin (-1) THEN D -1 THEN Auto THEN D -1) }
1
1. f : ℝ ⟶ ℝ
2. g : ℝ ⟶ ℝ
3. ∀x,y:ℝ. ((x = y) ⇒ (f(x) = f(y)))
4. ∀x,y:ℝ. ((x = y) ⇒ (g(x) = g(y)))
5. ∀x,y:ℝ. (f(x - y) = ((f(x) * f(y)) + (g(x) * g(y))))
6. a : ℝ
7. f(a) ≠ f(r0)
8. b : ℝ
9. g(-(b)) ≠ g(b)
10. ∀x,y:ℝ. (f(x - y) = f(y - x))
11. ∀y:ℝ. (f(-(y)) = f(y))
12. ∀y:ℝ. (g(-(y)) = -(g(y)))
13. g(r0) = r0
14. d : ℝ
15. f(d) ≠ r0
16. f(r0) = r1
17. ∀x:ℝ. ((f(x)^2 + g(x)^2) = r1)
18. ∀x:ℝ. (|f(x)| ≤ r1)
19. ∀x,y:ℝ. ((f(x - -(y)) + f(x - y)) = (r(2) * f(x) * f(y)))
20. ∀x,y:ℝ. ((f(x + y) + f(x - y)) = (r(2) * f(x) * f(y)))
21. ∀x:ℝ. (f(x) = r0)
⊢ ¬¬((∃c:ℝ
((r0 ≤ (c - c^2)) ∧ (∀x:ℝ. (f(x) = c)) ∧ ((∀x:ℝ. (g(x) = rsqrt(c - c^2))) ∨ (∀x:ℝ. (g(x) = -(rsqrt(c - c^2)))))))
∨ (∃a:ℝ. (a ≠ r0 ∧ (∀x:ℝ. (f(x) = rcos(a * x))) ∧ (∀x:ℝ. (g(x) = rsin(a * x))))))
2
1. f : ℝ ⟶ ℝ
2. g : ℝ ⟶ ℝ
3. ∀x,y:ℝ. ((x = y) ⇒ (f(x) = f(y)))
4. ∀x,y:ℝ. ((x = y) ⇒ (g(x) = g(y)))
5. ∀x,y:ℝ. (f(x - y) = ((f(x) * f(y)) + (g(x) * g(y))))
6. a : ℝ
7. f(a) ≠ f(r0)
8. b : ℝ
9. g(-(b)) ≠ g(b)
10. ∀x,y:ℝ. (f(x - y) = f(y - x))
11. ∀y:ℝ. (f(-(y)) = f(y))
12. ∀y:ℝ. (g(-(y)) = -(g(y)))
13. g(r0) = r0
14. d : ℝ
15. f(d) ≠ r0
16. f(r0) = r1
17. ∀x:ℝ. ((f(x)^2 + g(x)^2) = r1)
18. ∀x:ℝ. (|f(x)| ≤ r1)
19. ∀x,y:ℝ. ((f(x - -(y)) + f(x - y)) = (r(2) * f(x) * f(y)))
20. ∀x,y:ℝ. ((f(x + y) + f(x - y)) = (r(2) * f(x) * f(y)))
21. ¬¬((∃c:ℝ. ∀x:ℝ. (f(x) = rcos(c * x))) ∨ (∃c:ℝ. ∀x:ℝ. (f(x) = cosh(c * x))))
⊢ ¬¬((∃c:ℝ
((r0 ≤ (c - c^2)) ∧ (∀x:ℝ. (f(x) = c)) ∧ ((∀x:ℝ. (g(x) = rsqrt(c - c^2))) ∨ (∀x:ℝ. (g(x) = -(rsqrt(c - c^2)))))))
∨ (∃a:ℝ. (a ≠ r0 ∧ (∀x:ℝ. (f(x) = rcos(a * x))) ∧ (∀x:ℝ. (g(x) = rsin(a * x))))))
Latex:
Latex:
1. f : \mBbbR{} {}\mrightarrow{} \mBbbR{}
2. g : \mBbbR{} {}\mrightarrow{} \mBbbR{}
3. \mforall{}x,y:\mBbbR{}. ((x = y) {}\mRightarrow{} (f(x) = f(y)))
4. \mforall{}x,y:\mBbbR{}. ((x = y) {}\mRightarrow{} (g(x) = g(y)))
5. \mforall{}x,y:\mBbbR{}. (f(x - y) = ((f(x) * f(y)) + (g(x) * g(y))))
6. a : \mBbbR{}
7. f(a) \mneq{} f(r0)
8. b : \mBbbR{}
9. g(-(b)) \mneq{} g(b)
10. \mforall{}x,y:\mBbbR{}. (f(x - y) = f(y - x))
11. \mforall{}y:\mBbbR{}. (f(-(y)) = f(y))
12. \mforall{}y:\mBbbR{}. (g(-(y)) = -(g(y)))
13. g(r0) = r0
14. d : \mBbbR{}
15. f(d) \mneq{} r0
16. f(r0) = r1
17. \mforall{}x:\mBbbR{}. ((f(x)\^{}2 + g(x)\^{}2) = r1)
18. \mforall{}x:\mBbbR{}. (|f(x)| \mleq{} r1)
19. \mforall{}x,y:\mBbbR{}. ((f(x - -(y)) + f(x - y)) = (r(2) * f(x) * f(y)))
20. \mforall{}x,y:\mBbbR{}. ((f(x + y) + f(x - y)) = (r(2) * f(x) * f(y)))
\mvdash{} \mneg{}\mneg{}((\mexists{}c:\mBbbR{}
((r0 \mleq{} (c - c\^{}2))
\mwedge{} (\mforall{}x:\mBbbR{}. (f(x) = c))
\mwedge{} ((\mforall{}x:\mBbbR{}. (g(x) = rsqrt(c - c\^{}2))) \mvee{} (\mforall{}x:\mBbbR{}. (g(x) = -(rsqrt(c - c\^{}2)))))))
\mvee{} (\mexists{}a:\mBbbR{}. (a \mneq{} r0 \mwedge{} (\mforall{}x:\mBbbR{}. (f(x) = rcos(a * x))) \mwedge{} (\mforall{}x:\mBbbR{}. (g(x) = rsin(a * x))))))
By
Latex:
((InstLemma `DAlembert-equation-iff` [\mkleeneopen{}f\mkleeneclose{}]\mcdot{} THENA Auto)
THEN D -1
THEN Thin (-1)
THEN D -1
THEN Auto
THEN D -1)
Home
Index