---

Step * 7 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. ∃b:ℝ. g(-(b)) ≠ g(b)
8. ∀x,y:ℝ.  (f(x - y) = f(y - x))
9. ∀y:ℝ. (f(-(y)) = f(y))
10. ∀y:ℝ. (g(-(y)) = -(g(y)))
11. g(r0) = r0
12. ∃d:ℝ. f(d) ≠ r0
13. f(r0) = r1
14. x : ℝ
⊢ (f(x)^2 + g(x)^2) = r1
BY
{ ((InstHyp [⌜x⌝] 5⋅ THENA Auto)
   THEN (D -1 With ⌜x⌝  THENA Auto)
   THEN (RWO "rnexp2<" (-1) THENA Auto)
   THEN (RWO "-1< -3<" 0 THENA Auto)
   THEN BackThruSomeHyp
   THEN Auto) }

---

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.  \mexists{}b:\mBbbR{}.  g(-(b))  \mneq{}  g(b)
8.  \mforall{}x,y:\mBbbR{}.    (f(x  -  y)  =  f(y  -  x))
9.  \mforall{}y:\mBbbR{}.  (f(-(y))  =  f(y))
10.  \mforall{}y:\mBbbR{}.  (g(-(y))  =  -(g(y)))
11.  g(r0)  =  r0
12.  \mexists{}d:\mBbbR{}.  f(d)  \mneq{}  r0
13.  f(r0)  =  r1
14.  x  :  \mBbbR{}
\mvdash{}  (f(x)\^{}2  +  g(x)\^{}2)  =  r1


By

---

Latex:
((InstHyp  [\mkleeneopen{}x\mkleeneclose{}]  5\mcdot{}  THENA  Auto)
  THEN  (D  -1  With  \mkleeneopen{}x\mkleeneclose{}    THENA  Auto)
  THEN  (RWO  "rnexp2<"  (-1)  THENA  Auto)
  THEN  (RWO  "-1<  -3<"  0  THENA  Auto)
  THEN  BackThruSomeHyp
  THEN  Auto)

---

Home Index