---

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

.....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))
⊢ (g' r0) = a
BY
{ ((InstLemma `derivative_functionality` [⌜I⌝;⌜λ2x.g(x)⌝;⌜λ2x.rsin(a * x)⌝;⌜λ2x.g' x⌝;⌜λ2x.g' x⌝]⋅
    THENA (Auto THEN (D 0 THEN RepUR ``r-ap so_lambda`` 0) THEN Auto)
    )
   THEN (InstLemma `derivative_unique` [⌜I⌝;⌜λx.rsin(a * x)⌝;⌜λx.(g' x)⌝;⌜λx.(a * rcos(a * x))⌝]⋅
         THENA (Auto THEN RepUR ``so_apply`` 0)
         )
   ) }

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
⊢ d(rsin(a * x))/dx = λx.a * rcos(a * x) on I

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. rfun-eq(I;λx.(g' x);λx.(a * rcos(a * x)))
⊢ (g' r0) = a

---

Latex:

---

Latex:
.....assertion..... 
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))
\mvdash{}  (g'  r0)  =  a


By

---

Latex:
((InstLemma  `derivative\_functionality`  [\mkleeneopen{}I\mkleeneclose{};\mkleeneopen{}\mlambda{}\msubtwo{}x.g(x)\mkleeneclose{};\mkleeneopen{}\mlambda{}\msubtwo{}x.rsin(a  *  x)\mkleeneclose{};\mkleeneopen{}\mlambda{}\msubtwo{}x.g'  x\mkleeneclose{};\mkleeneopen{}\mlambda{}\msubtwo{}x.g'  x\mkleeneclose{}]\mcdot{}
    THENA  (Auto  THEN  (D  0  THEN  RepUR  ``r-ap  so\_lambda``  0)  THEN  Auto)
    )
  THEN  (InstLemma  `derivative\_unique`  [\mkleeneopen{}I\mkleeneclose{};\mkleeneopen{}\mlambda{}x.rsin(a  *  x)\mkleeneclose{};\mkleeneopen{}\mlambda{}x.(g'  x)\mkleeneclose{};\mkleeneopen{}\mlambda{}x.(a  *  rcos(a  *  x))\mkleeneclose{}]\mcdot{}
              THENA  (Auto  THEN  RepUR  ``so\_apply``  0)
              )
  )

---

Home Index