---

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


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 : ℝ
7. f(a) ≠ f(r0)
8. ¬(∃b:ℝ. g(-(b)) ≠ g(b))
9. ∀b:ℝ. (g(-(b)) = g(b))
10. ∀x,y:ℝ.  (f(x - y) = f(y - x))
11. ∀y:ℝ. (f(-(y)) = f(y))
12. ∀x,y:ℝ.  (f(x - -(y)) = f(x - y))
13. f(a) = f(r0)
⊢ ¬¬((∃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
{ ((RWO "-1" 7 THENA Auto) THEN FLemma `rneq_irreflexivity` [7] 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.  a  :  \mBbbR{}
7.  f(a)  \mneq{}  f(r0)
8.  \mneg{}(\mexists{}b:\mBbbR{}.  g(-(b))  \mneq{}  g(b))
9.  \mforall{}b:\mBbbR{}.  (g(-(b))  =  g(b))
10.  \mforall{}x,y:\mBbbR{}.    (f(x  -  y)  =  f(y  -  x))
11.  \mforall{}y:\mBbbR{}.  (f(-(y))  =  f(y))
12.  \mforall{}x,y:\mBbbR{}.    (f(x  -  -(y))  =  f(x  -  y))
13.  f(a)  =  f(r0)
\mvdash{}  \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:
((RWO  "-1"  7  THENA  Auto)  THEN  FLemma  `rneq\_irreflexivity`  [7]  THEN  Auto)

---

Home Index