---

Step * 1 2 1 1 1 of Lemma cos-sin-equation

.....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:ℝ. f(a) ≠ f(r0))
7. ∀x:ℝ. (f(x) = f(r0))
8. ∀x:ℝ. ((g(x) * g(r0)) = (f(r0) - f(r0)^2))
9. (g(r0) * g(r0)) = (f(r0) - f(r0)^2)
10. f(r0) = ((f(r0) * f(r0)) + (g(r0) * g(r0)))
11. r0 ≤ (f(r0) - f(r0)^2)
⊢ ∀x:ℝ. (g(x) = g(r0))
BY
{ (Auto THEN (StableCases ⌜g(r0) ≠ r0⌝⋅ THENA 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:ℝ. (f(x) = f(r0))
8. ∀x:ℝ. ((g(x) * g(r0)) = (f(r0) - f(r0)^2))
9. (g(r0) * g(r0)) = (f(r0) - f(r0)^2)
10. f(r0) = ((f(r0) * f(r0)) + (g(r0) * g(r0)))
11. r0 ≤ (f(r0) - f(r0)^2)
12. x : ℝ
13. g(r0) ≠ r0
⊢ g(x) = g(r0)

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:ℝ. f(a) ≠ f(r0))
7. ∀x:ℝ. (f(x) = f(r0))
8. ∀x:ℝ. ((g(x) * g(r0)) = (f(r0) - f(r0)^2))
9. (g(r0) * g(r0)) = (f(r0) - f(r0)^2)
10. f(r0) = ((f(r0) * f(r0)) + (g(r0) * g(r0)))
11. r0 ≤ (f(r0) - f(r0)^2)
12. x : ℝ
13. ¬g(r0) ≠ r0
⊢ g(x) = g(r0)

---

Latex:

---

Latex:
.....assertion..... 
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.  \mneg{}(\mexists{}a:\mBbbR{}.  f(a)  \mneq{}  f(r0))
7.  \mforall{}x:\mBbbR{}.  (f(x)  =  f(r0))
8.  \mforall{}x:\mBbbR{}.  ((g(x)  *  g(r0))  =  (f(r0)  -  f(r0)\^{}2))
9.  (g(r0)  *  g(r0))  =  (f(r0)  -  f(r0)\^{}2)
10.  f(r0)  =  ((f(r0)  *  f(r0))  +  (g(r0)  *  g(r0)))
11.  r0  \mleq{}  (f(r0)  -  f(r0)\^{}2)
\mvdash{}  \mforall{}x:\mBbbR{}.  (g(x)  =  g(r0))


By

---

Latex:
(Auto  THEN  (StableCases  \mkleeneopen{}g(r0)  \mneq{}  r0\mkleeneclose{}\mcdot{}  THENA  Auto))

---

Home Index