---

Step * of Lemma cos-sin-equation

∀f,g:ℝ ⟶ ℝ.
  (((∀x,y:ℝ.  ((x = y) ⇒ (f(x) = f(y)))) ∧ (∀x,y:ℝ.  ((x = y) ⇒ (g(x) = g(y)))))
   ∧ (∀x,y:ℝ.  (f(x - y) = ((f(x) * f(y)) + (g(x) * g(y)))))
  ⇐⇒ ¬¬((∃c:ℝ
           ((r0 ≤ (c - c^2))
           ∧ (∀x:ℝ. (f(x) = c))
           ∧ ((∀x:ℝ. (g(x) = rsqrt(c - c^2))) ∨ (∀x:ℝ. (g(x) = -(rsqrt(c - c^2)))))))
      ∨ (∃a:ℝ. (a ≠ r0 ∧ (∀x:ℝ. (f(x) = rcos(a * x))) ∧ (∀x:ℝ. (g(x) = rsin(a * x)))))))
BY
{ ((UnivCD THENA Auto) THEN (RepeatFor 2 (D 0) THENA Auto)) }

1
1. f : ℝ ⟶ ℝ
2. g : ℝ ⟶ ℝ
3. ((∀x,y:ℝ.  ((x = y) ⇒ (f(x) = f(y)))) ∧ (∀x,y:ℝ.  ((x = y) ⇒ (g(x) = g(y)))))
∧ (∀x,y:ℝ.  (f(x - y) = ((f(x) * f(y)) + (g(x) * g(y)))))
⊢ ¬¬((∃c:ℝ
       ((r0 ≤ (c - c^2)) ∧ (∀x:ℝ. (f(x) = c)) ∧ ((∀x:ℝ. (g(x) = rsqrt(c - c^2))) ∨ (∀x:ℝ. (g(x) = -(rsqrt(c - c^2)))))))
∨ (∃a:ℝ. (a ≠ r0 ∧ (∀x:ℝ. (f(x) = rcos(a * x))) ∧ (∀x:ℝ. (g(x) = rsin(a * x))))))

2
1. f : ℝ ⟶ ℝ
2. g : ℝ ⟶ ℝ
3. ¬¬((∃c:ℝ
        ((r0 ≤ (c - c^2))
        ∧ (∀x:ℝ. (f(x) = c))
        ∧ ((∀x:ℝ. (g(x) = rsqrt(c - c^2))) ∨ (∀x:ℝ. (g(x) = -(rsqrt(c - c^2)))))))
∨ (∃a:ℝ. (a ≠ r0 ∧ (∀x:ℝ. (f(x) = rcos(a * x))) ∧ (∀x:ℝ. (g(x) = rsin(a * x))))))
⊢ ((∀x,y:ℝ.  ((x = y) ⇒ (f(x) = f(y)))) ∧ (∀x,y:ℝ.  ((x = y) ⇒ (g(x) = g(y)))))
∧ (∀x,y:ℝ.  (f(x - y) = ((f(x) * f(y)) + (g(x) * g(y)))))

---

Latex:

---

Latex:
\mforall{}f,g:\mBbbR{}  {}\mrightarrow{}  \mBbbR{}.
    (((\mforall{}x,y:\mBbbR{}.    ((x  =  y)  {}\mRightarrow{}  (f(x)  =  f(y))))  \mwedge{}  (\mforall{}x,y:\mBbbR{}.    ((x  =  y)  {}\mRightarrow{}  (g(x)  =  g(y)))))
      \mwedge{}  (\mforall{}x,y:\mBbbR{}.    (f(x  -  y)  =  ((f(x)  *  f(y))  +  (g(x)  *  g(y)))))
    \mLeftarrow{}{}\mRightarrow{}  \mneg{}\mneg{}((\mexists{}c:\mBbbR{}
                      ((r0  \mleq{}  (c  -  c\^{}2))
                      \mwedge{}  (\mforall{}x:\mBbbR{}.  (f(x)  =  c))
                      \mwedge{}  ((\mforall{}x:\mBbbR{}.  (g(x)  =  rsqrt(c  -  c\^{}2)))  \mvee{}  (\mforall{}x:\mBbbR{}.  (g(x)  =  -(rsqrt(c  -  c\^{}2)))))))
            \mvee{}  (\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:
((UnivCD  THENA  Auto)  THEN  (RepeatFor  2  (D  0)  THENA  Auto))

---

Home Index