---

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

∀f,g:ℝ ⟶ ℝ.
  ((∀x,y:ℝ.  ((x = y) ⇒ (f(x) = f(y))))
  ⇒ (∀x,y:ℝ.  ((x = y) ⇒ (g(x) = g(y))))
  ⇒ (∃u,v:ℝ. f(u) ≠ f(v))
  ⇒ (∀x,y:ℝ.  (f(x - y) = ((f(x) * f(y)) + (g(x) * g(y)))))
  ⇒ (∃I:Interval. (iproper(I) ∧ (r0 ∈ I) ∧ (∃g':I ⟶ℝ. d(g(x))/dx = λx.g' x on I)))
  ⇒ (∃a:ℝ. ((∀x:ℝ. (f(x) = rcos(a * x))) ∧ (∀x:ℝ. (g(x) = rsin(a * x))))))
BY
{ (InstLemma `cos-sin-equation-non-constant1` []
   THEN RepeatFor 6 ((ParallelLast' THENA Auto))
   THEN (D 0 THENA Auto)
   THEN ((ExRepD THEN D 0 With ⌜g' r0⌝ ) THENA Auto)
   THEN (StableCases ⌜∃a:ℝ. (a ≠ r0 ∧ (∀x:ℝ. (f(x) = rcos(a * x))) ∧ (∀x:ℝ. (g(x) = rsin(a * x))))⌝⋅
         THENA (Auto THEN (BLemma `stable__and` THEN Auto) THEN BLemma `stable__all` THEN Auto)
         )
   THEN (Trivial ORELSE (ExRepD THEN (Assert ⌜(g' r0) = 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. 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

---

Latex:

---

Latex:
\mforall{}f,g:\mBbbR{}  {}\mrightarrow{}  \mBbbR{}.
    ((\mforall{}x,y:\mBbbR{}.    ((x  =  y)  {}\mRightarrow{}  (f(x)  =  f(y))))
    {}\mRightarrow{}  (\mforall{}x,y:\mBbbR{}.    ((x  =  y)  {}\mRightarrow{}  (g(x)  =  g(y))))
    {}\mRightarrow{}  (\mexists{}u,v:\mBbbR{}.  f(u)  \mneq{}  f(v))
    {}\mRightarrow{}  (\mforall{}x,y:\mBbbR{}.    (f(x  -  y)  =  ((f(x)  *  f(y))  +  (g(x)  *  g(y)))))
    {}\mRightarrow{}  (\mexists{}I:Interval.  (iproper(I)  \mwedge{}  (r0  \mmember{}  I)  \mwedge{}  (\mexists{}g':I  {}\mrightarrow{}\mBbbR{}.  d(g(x))/dx  =  \mlambda{}x.g'  x  on  I)))
    {}\mRightarrow{}  (\mexists{}a:\mBbbR{}.  ((\mforall{}x:\mBbbR{}.  (f(x)  =  rcos(a  *  x)))  \mwedge{}  (\mforall{}x:\mBbbR{}.  (g(x)  =  rsin(a  *  x))))))


By

---

Latex:
(InstLemma  `cos-sin-equation-non-constant1`  []
  THEN  RepeatFor  6  ((ParallelLast'  THENA  Auto))
  THEN  (D  0  THENA  Auto)
  THEN  ((ExRepD  THEN  D  0  With  \mkleeneopen{}g'  r0\mkleeneclose{}  )  THENA  Auto)
  THEN  (StableCases  \mkleeneopen{}\mexists{}a:\mBbbR{}.  (a  \mneq{}  r0  \mwedge{}  (\mforall{}x:\mBbbR{}.  (f(x)  =  rcos(a  *  x)))  \mwedge{}  (\mforall{}x:\mBbbR{}.  (g(x)  =  rsin(a  *  x))))\mkleeneclose{}\mcdot{}
              THENA  (Auto  THEN  (BLemma  `stable\_\_and`  THEN  Auto)  THEN  BLemma  `stable\_\_all`  THEN  Auto)
              )
  THEN  (Trivial  ORELSE  (ExRepD  THEN  (Assert  \mkleeneopen{}(g'  r0)  =  a\mkleeneclose{}\mcdot{}  THENM  (RWO  "-1"  0  THEN  Auto)))))

---

Home Index