---

Step * 1 1 1 1 1 1 1 1 of Lemma cos-sin-equation-non-constant3


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:ℝ. (a ≠ r0 ∧ (∀x:ℝ. (f(x) = rcos(a * x))) ∧ (∀x:ℝ. (g(x) = rsin(a * x)))))
7. ∀x,y:ℝ.  ((x = y) ⇒ ((g x) = (g y)))
8. b : ℝ
9. r0_∫-b -(g(x)) dx ≠ r0
10. f(b) ≠ r1
11. f(b) - r1 ≠ r0
12. a : ℝ
13. a ≠ r0
14. ∀x:ℝ. (g(x) = rsin(a * x))
15. f(r0) = r1
16. a1 : ℝ
17. a1 ≠ r0
18. ∀x:ℝ. (f(x) = rcos(a1 * x))
19. ∀x:ℝ. (g(x) = rsin(a1 * x))
20. d(rcos(a1 * x))/dx = λx.a1 * -(rsin(a1 * x)) on (-∞, ∞)
21. d(f(x))/dx = λx.a1 * -(g(x)) on (-∞, ∞)
22. d((r1/a) * f(x))/dx = λx.((r1/a) * a1 * -(g(x))) + (f(x) * r0) on (-∞, ∞)
23. x : {x:ℝ| x ∈ (-∞, ∞)} 
⊢ -(g(x) * a1) = -(g(x) * a)
BY
{ (Assert ⌜a1 = a⌝⋅ THENM (RWO "-1" 0 THEN Auto)) }

1
.....assertion..... 
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:ℝ. (a ≠ r0 ∧ (∀x:ℝ. (f(x) = rcos(a * x))) ∧ (∀x:ℝ. (g(x) = rsin(a * x)))))
7. ∀x,y:ℝ.  ((x = y) ⇒ ((g x) = (g y)))
8. b : ℝ
9. r0_∫-b -(g(x)) dx ≠ r0
10. f(b) ≠ r1
11. f(b) - r1 ≠ r0
12. a : ℝ
13. a ≠ r0
14. ∀x:ℝ. (g(x) = rsin(a * x))
15. f(r0) = r1
16. a1 : ℝ
17. a1 ≠ r0
18. ∀x:ℝ. (f(x) = rcos(a1 * x))
19. ∀x:ℝ. (g(x) = rsin(a1 * x))
20. d(rcos(a1 * x))/dx = λx.a1 * -(rsin(a1 * x)) on (-∞, ∞)
21. d(f(x))/dx = λx.a1 * -(g(x)) on (-∞, ∞)
22. d((r1/a) * f(x))/dx = λx.((r1/a) * a1 * -(g(x))) + (f(x) * r0) on (-∞, ∞)
23. x : {x:ℝ| x ∈ (-∞, ∞)} 
⊢ a1 = a

---

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.  \mneg{}\mneg{}(\mexists{}a:\mBbbR{}.  (a  \mneq{}  r0  \mwedge{}  (\mforall{}x:\mBbbR{}.  (f(x)  =  rcos(a  *  x)))  \mwedge{}  (\mforall{}x:\mBbbR{}.  (g(x)  =  rsin(a  *  x)))))
7.  \mforall{}x,y:\mBbbR{}.    ((x  =  y)  {}\mRightarrow{}  ((g  x)  =  (g  y)))
8.  b  :  \mBbbR{}
9.  r0\_\mint{}\msupminus{}b  -(g(x))  dx  \mneq{}  r0
10.  f(b)  \mneq{}  r1
11.  f(b)  -  r1  \mneq{}  r0
12.  a  :  \mBbbR{}
13.  a  \mneq{}  r0
14.  \mforall{}x:\mBbbR{}.  (g(x)  =  rsin(a  *  x))
15.  f(r0)  =  r1
16.  a1  :  \mBbbR{}
17.  a1  \mneq{}  r0
18.  \mforall{}x:\mBbbR{}.  (f(x)  =  rcos(a1  *  x))
19.  \mforall{}x:\mBbbR{}.  (g(x)  =  rsin(a1  *  x))
20.  d(rcos(a1  *  x))/dx  =  \mlambda{}x.a1  *  -(rsin(a1  *  x))  on  (-\minfty{},  \minfty{})
21.  d(f(x))/dx  =  \mlambda{}x.a1  *  -(g(x))  on  (-\minfty{},  \minfty{})
22.  d((r1/a)  *  f(x))/dx  =  \mlambda{}x.((r1/a)  *  a1  *  -(g(x)))  +  (f(x)  *  r0)  on  (-\minfty{},  \minfty{})
23.  x  :  \{x:\mBbbR{}|  x  \mmember{}  (-\minfty{},  \minfty{})\} 
\mvdash{}  -(g(x)  *  a1)  =  -(g(x)  *  a)


By

---

Latex:
(Assert  \mkleeneopen{}a1  =  a\mkleeneclose{}\mcdot{}  THENM  (RWO  "-1"  0  THEN  Auto))

---

Home Index