---

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

∀f,g:ℝ ⟶ ℝ.
  ((∀x,y:ℝ.  ((x = y) ⇒ (f(x) = f(y))))
  ⇒ (∀x,y:ℝ.  ((x = y) ⇒ (g(x) = g(y))))
  ⇒ (∃a,b:ℝ. f(a) ≠ f(b))
  ⇒ (∀x,y:ℝ.  (f(x - y) = ((f(x) * f(y)) + (g(x) * g(y)))))
  ⇒ (∃b:ℝ. (r0_∫-b -(g(x)) dx ≠ r0 ∧ f(b) ≠ r1))
  ⇒ (∃a:ℝ. (a ≠ r0 ∧ (∀x:ℝ. (f(x) = rcos(a * x))) ∧ (∀x:ℝ. (g(x) = rsin(a * x))))))
BY
{ ((InstLemma `cos-sin-equation-non-constant1` []⋅ THENA Auto)
   THEN RepeatFor 6 ((ParallelLast' THENA Auto))
   THEN DupHyp 4
   THEN Unfold `rfun-ap` -1
   THEN (D 0 THENA Auto)
   THEN Thin (-5)
   THEN RepeatFor 2 (D -1)
   THEN (Assert f(b) - r1 ≠ r0 BY
               (RepeatFor 2 (ParallelLast) THEN Auto))
   THEN Assert ⌜∃a:ℝ. ((∀x:ℝ. (f(x) = rcos(a * x))) ∧ (∀x:ℝ. (g(x) = rsin(a * x))))⌝⋅) }

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
⊢ ∃a:ℝ. ((∀x:ℝ. (f(x) = rcos(a * x))) ∧ (∀x:ℝ. (g(x) = rsin(a * x))))

2
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:ℝ. ((∀x:ℝ. (f(x) = rcos(a * x))) ∧ (∀x:ℝ. (g(x) = rsin(a * x))))
⊢ ∃a:ℝ. (a ≠ r0 ∧ (∀x:ℝ. (f(x) = rcos(a * x))) ∧ (∀x:ℝ. (g(x) = rsin(a * x))))

---

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{}a,b:\mBbbR{}.  f(a)  \mneq{}  f(b))
    {}\mRightarrow{}  (\mforall{}x,y:\mBbbR{}.    (f(x  -  y)  =  ((f(x)  *  f(y))  +  (g(x)  *  g(y)))))
    {}\mRightarrow{}  (\mexists{}b:\mBbbR{}.  (r0\_\mint{}\msupminus{}b  -(g(x))  dx  \mneq{}  r0  \mwedge{}  f(b)  \mneq{}  r1))
    {}\mRightarrow{}  (\mexists{}a:\mBbbR{}.  (a  \mneq{}  r0  \mwedge{}  (\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`  []\mcdot{}  THENA  Auto)
  THEN  RepeatFor  6  ((ParallelLast'  THENA  Auto))
  THEN  DupHyp  4
  THEN  Unfold  `rfun-ap`  -1
  THEN  (D  0  THENA  Auto)
  THEN  Thin  (-5)
  THEN  RepeatFor  2  (D  -1)
  THEN  (Assert  f(b)  -  r1  \mneq{}  r0  BY
                          (RepeatFor  2  (ParallelLast)  THEN  Auto))
  THEN  Assert  \mkleeneopen{}\mexists{}a:\mBbbR{}.  ((\mforall{}x:\mBbbR{}.  (f(x)  =  rcos(a  *  x)))  \mwedge{}  (\mforall{}x:\mBbbR{}.  (g(x)  =  rsin(a  *  x))))\mkleeneclose{}\mcdot{})

---

Home Index