---

Step * 3 1 of Lemma cos-sin-equation-nc


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:ℝ. f(a) ≠ f(r0)
7. ∀x,y:ℝ.  (f(x - y) = f(y - x))
8. ∀y:ℝ. (f(-(y)) = f(y))
9. ∃b:ℝ. g(-(b)) ≠ g(b)
⊢ ∀y:ℝ. (g(-(y)) = -(g(y)))
BY
{ (Assert ∀x,y:ℝ.  (f(x - y) = ((f(x) * f(y)) + (g(-(x)) * g(-(y))))) BY
         ((Assert ∀x,y:ℝ.  (f(-(x) - -(y)) = ((f(x) * f(y)) + (g(-(x)) * g(-(y))))) BY
                 (RWW "5 8" 0 THEN Auto))
          THEN RWO "-1<" 0
          THEN Auto
          THEN (RW (AddrC [1] (HypC 7)) 0 THENA Auto)
          THEN BackThruSomeHyp
          THEN 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. ∀x,y:ℝ.  (f(x - y) = ((f(x) * f(y)) + (g(x) * g(y))))
6. ∃a:ℝ. f(a) ≠ f(r0)
7. ∀x,y:ℝ.  (f(x - y) = f(y - x))
8. ∀y:ℝ. (f(-(y)) = f(y))
9. ∃b:ℝ. g(-(b)) ≠ g(b)
10. ∀x,y:ℝ.  (f(x - y) = ((f(x) * f(y)) + (g(-(x)) * g(-(y)))))
⊢ ∀y:ℝ. (g(-(y)) = -(g(y)))

---

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.  \mforall{}x,y:\mBbbR{}.    (f(x  -  y)  =  ((f(x)  *  f(y))  +  (g(x)  *  g(y))))
6.  \mexists{}a:\mBbbR{}.  f(a)  \mneq{}  f(r0)
7.  \mforall{}x,y:\mBbbR{}.    (f(x  -  y)  =  f(y  -  x))
8.  \mforall{}y:\mBbbR{}.  (f(-(y))  =  f(y))
9.  \mexists{}b:\mBbbR{}.  g(-(b))  \mneq{}  g(b)
\mvdash{}  \mforall{}y:\mBbbR{}.  (g(-(y))  =  -(g(y)))


By

---

Latex:
(Assert  \mforall{}x,y:\mBbbR{}.    (f(x  -  y)  =  ((f(x)  *  f(y))  +  (g(-(x))  *  g(-(y)))))  BY
              ((Assert  \mforall{}x,y:\mBbbR{}.    (f(-(x)  -  -(y))  =  ((f(x)  *  f(y))  +  (g(-(x))  *  g(-(y)))))  BY
                              (RWW  "5  8"  0  THEN  Auto))
                THEN  RWO  "-1<"  0
                THEN  Auto
                THEN  (RW  (AddrC  [1]  (HypC  7))  0  THENA  Auto)
                THEN  BackThruSomeHyp
                THEN  Auto))

---

Home Index