---

Step * 1 1 1 1 2 1 1 1 1 1 2 2 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
26. C : ℝ
27. ∀x:ℝ. (g(x) = (C * rsin(c * x)))
28. C = r(-1)
29. -(c) ≠ r0
30. ∀x:ℝ. (f(x) = rcos(-(c) * x))
31. x : ℝ
32. (-(c) * x) = -(c * x)
⊢ g(x) = -(rsin(c * x))
BY
{ (RWW "-6 -5" 0 THEN Auto) }

---

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
26.  C  :  \mBbbR{}
27.  \mforall{}x:\mBbbR{}.  (g(x)  =  (C  *  rsin(c  *  x)))
28.  C  =  r(-1)
29.  -(c)  \mneq{}  r0
30.  \mforall{}x:\mBbbR{}.  (f(x)  =  rcos(-(c)  *  x))
31.  x  :  \mBbbR{}
32.  (-(c)  *  x)  =  -(c  *  x)
\mvdash{}  g(x)  =  -(rsin(c  *  x))


By

---

Latex:
(RWW  "-6  -5"  0  THEN  Auto)

---

Home Index