Step
*
1
1
1
1
2
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)))
21. c : ℝ
22. ∀x:ℝ. (f(x) = rcos(c * x))
23. c ≠ r0
24. e : ℝ
25. g(e) ≠ 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))))))
BY
{ (Assert ∃C:ℝ. ∀x:ℝ. (g(x) = (C * rsin(c * x))) BY
(D 0 With ⌜(rsin(c * e)/g(e))⌝
THEN Auto
THEN (InstHyp [⌜x⌝;⌜e⌝] 5⋅ THENA Auto)
THEN (RWO "-6" (-1) THENA Auto)
THEN (Assert (c * (x - e)) = ((c * x) - c * e) BY
Auto)
THEN (RWO "-1" (-2) THENA Auto)
THEN (RWO "rcos-rsub" (-2) THENA Auto)
THEN (nRAdd ⌜-(rcos(c * x) * rcos(c * e))⌝ (-2)⋅ THENA Auto)
THEN nRMul ⌜g(e)⌝ 0⋅
THEN Auto)) }
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. c : ℝ
22. ∀x:ℝ. (f(x) = rcos(c * x))
23. c ≠ r0
24. e : ℝ
25. g(e) ≠ r0
26. ∃C:ℝ. ∀x:ℝ. (g(x) = (C * rsin(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)))
21. c : \mBbbR{}
22. \mforall{}x:\mBbbR{}. (f(x) = rcos(c * x))
23. c \mneq{} r0
24. e : \mBbbR{}
25. g(e) \mneq{} r0
\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:
(Assert \mexists{}C:\mBbbR{}. \mforall{}x:\mBbbR{}. (g(x) = (C * rsin(c * x))) BY
(D 0 With \mkleeneopen{}(rsin(c * e)/g(e))\mkleeneclose{}
THEN Auto
THEN (InstHyp [\mkleeneopen{}x\mkleeneclose{};\mkleeneopen{}e\mkleeneclose{}] 5\mcdot{} THENA Auto)
THEN (RWO "-6" (-1) THENA Auto)
THEN (Assert (c * (x - e)) = ((c * x) - c * e) BY
Auto)
THEN (RWO "-1" (-2) THENA Auto)
THEN (RWO "rcos-rsub" (-2) THENA Auto)
THEN (nRAdd \mkleeneopen{}-(rcos(c * x) * rcos(c * e))\mkleeneclose{} (-2)\mcdot{} THENA Auto)
THEN nRMul \mkleeneopen{}g(e)\mkleeneclose{} 0\mcdot{}
THEN Auto))
Home
Index