---

Step * 1 2 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
20. rfun-eq(I;λx.(g' x);λx.(a * rcos(a * x)))
⊢ (g' r0) = a
BY
{ (D -1 With ⌜r0⌝  THEN Auto THEN RepUR ``r-ap`` -1 THEN (RWO "-1" 0 THENA 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. 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. (g' r0) = (a * rcos(a * r0))
⊢ (a * rcos(a * r0)) = 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.  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
20.  rfun-eq(I;\mlambda{}x.(g'  x);\mlambda{}x.(a  *  rcos(a  *  x)))
\mvdash{}  (g'  r0)  =  a


By

---

Latex:
(D  -1  With  \mkleeneopen{}r0\mkleeneclose{}    THEN  Auto  THEN  RepUR  ``r-ap``  -1  THEN  (RWO  "-1"  0  THENA  Auto))

---

Home Index