---

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


1. f : ℝ ⟶ ℝ
2. g : ℝ ⟶ ℝ
3. ∀x,y:ℝ.  ((x = y) ⇒ (f(x) = f(y)))
4. ∀x,y:ℝ.  ((x = y) ⇒ (g(x) = g(y)))
5. u : ℝ
6. v : ℝ
7. f(u) ≠ f(v)
8. ∀x,y:ℝ.  (f(x - y) = ((f(x) * f(y)) + (g(x) * g(y))))
9. ¬¬(∃a:ℝ. (a ≠ r0 ∧ (∀x:ℝ. (f(x) = rcos(a * x))) ∧ (∀x:ℝ. (g(x) = rsin(a * x)))))
10. I : Interval
11. iproper(I)
12. r0 ∈ I
13. g' : I ⟶ℝ
14. d(g(x))/dx = λx.g' x on I
15. a : ℝ
16. a ≠ r0
17. ∀x:ℝ. (f(x) = rcos(a * x))
18. ∀x:ℝ. (g(x) = rsin(a * x))
19. d(rsin(a * x))/dx = λx.g' x on I
⊢ d(rsin(a * x))/dx = λx.a * rcos(a * x) on I
BY
{ Assert ⌜d(rsin(a * x))/dx = λx.a * rcos(a * x) on (-∞, ∞)⌝⋅ }

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. u : ℝ
6. v : ℝ
7. f(u) ≠ f(v)
8. ∀x,y:ℝ.  (f(x - y) = ((f(x) * f(y)) + (g(x) * g(y))))
9. ¬¬(∃a:ℝ. (a ≠ r0 ∧ (∀x:ℝ. (f(x) = rcos(a * x))) ∧ (∀x:ℝ. (g(x) = rsin(a * x)))))
10. I : Interval
11. iproper(I)
12. r0 ∈ I
13. g' : I ⟶ℝ
14. d(g(x))/dx = λx.g' x on I
15. a : ℝ
16. a ≠ r0
17. ∀x:ℝ. (f(x) = rcos(a * x))
18. ∀x:ℝ. (g(x) = rsin(a * x))
19. d(rsin(a * x))/dx = λx.g' x on I
⊢ d(rsin(a * x))/dx = λx.a * rcos(a * x) on (-∞, ∞)

2
1. f : ℝ ⟶ ℝ
2. g : ℝ ⟶ ℝ
3. ∀x,y:ℝ.  ((x = y) ⇒ (f(x) = f(y)))
4. ∀x,y:ℝ.  ((x = y) ⇒ (g(x) = g(y)))
5. u : ℝ
6. v : ℝ
7. f(u) ≠ f(v)
8. ∀x,y:ℝ.  (f(x - y) = ((f(x) * f(y)) + (g(x) * g(y))))
9. ¬¬(∃a:ℝ. (a ≠ r0 ∧ (∀x:ℝ. (f(x) = rcos(a * x))) ∧ (∀x:ℝ. (g(x) = rsin(a * x)))))
10. I : Interval
11. iproper(I)
12. r0 ∈ I
13. g' : I ⟶ℝ
14. d(g(x))/dx = λx.g' x on I
15. a : ℝ
16. a ≠ r0
17. ∀x:ℝ. (f(x) = rcos(a * x))
18. ∀x:ℝ. (g(x) = rsin(a * x))
19. d(rsin(a * x))/dx = λx.g' x on I
20. d(rsin(a * x))/dx = λx.a * rcos(a * x) on (-∞, ∞)
⊢ d(rsin(a * x))/dx = λx.a * rcos(a * x) on I

---

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.  u  :  \mBbbR{}
6.  v  :  \mBbbR{}
7.  f(u)  \mneq{}  f(v)
8.  \mforall{}x,y:\mBbbR{}.    (f(x  -  y)  =  ((f(x)  *  f(y))  +  (g(x)  *  g(y))))
9.  \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)))))
10.  I  :  Interval
11.  iproper(I)
12.  r0  \mmember{}  I
13.  g'  :  I  {}\mrightarrow{}\mBbbR{}
14.  d(g(x))/dx  =  \mlambda{}x.g'  x  on  I
15.  a  :  \mBbbR{}
16.  a  \mneq{}  r0
17.  \mforall{}x:\mBbbR{}.  (f(x)  =  rcos(a  *  x))
18.  \mforall{}x:\mBbbR{}.  (g(x)  =  rsin(a  *  x))
19.  d(rsin(a  *  x))/dx  =  \mlambda{}x.g'  x  on  I
\mvdash{}  d(rsin(a  *  x))/dx  =  \mlambda{}x.a  *  rcos(a  *  x)  on  I


By

---

Latex:
Assert  \mkleeneopen{}d(rsin(a  *  x))/dx  =  \mlambda{}x.a  *  rcos(a  *  x)  on  (-\minfty{},  \minfty{})\mkleeneclose{}\mcdot{}

---

Home Index