---

Step * 1 of Lemma cos-sin-equation-non-constant1


1. f : ℝ ⟶ ℝ
2. g : ℝ ⟶ ℝ
3. ∀x,y:ℝ.  ((x = y) ⇒ (f(x) = f(y)))
4. ∀x,y:ℝ.  ((x = y) ⇒ (g(x) = g(y)))
5. a : ℝ
6. b : ℝ
7. f(a) ≠ f(b)
8. ∀x,y:ℝ.  (f(x - y) = ((f(x) * f(y)) + (g(x) * g(y))))
9. c : ℝ
10. r0 ≤ (c - c^2)
11. ∀x:ℝ. (f(x) = c)
12. (∀x:ℝ. (g(x) = rsqrt(c - c^2))) ∨ (∀x:ℝ. (g(x) = -(rsqrt(c - c^2))))
⊢ False
BY
{ ((RWO "-2" 7 THENA Auto) THEN FLemma `rneq_irreflexivity` [-1] 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.  a  :  \mBbbR{}
6.  b  :  \mBbbR{}
7.  f(a)  \mneq{}  f(b)
8.  \mforall{}x,y:\mBbbR{}.    (f(x  -  y)  =  ((f(x)  *  f(y))  +  (g(x)  *  g(y))))
9.  c  :  \mBbbR{}
10.  r0  \mleq{}  (c  -  c\^{}2)
11.  \mforall{}x:\mBbbR{}.  (f(x)  =  c)
12.  (\mforall{}x:\mBbbR{}.  (g(x)  =  rsqrt(c  -  c\^{}2)))  \mvee{}  (\mforall{}x:\mBbbR{}.  (g(x)  =  -(rsqrt(c  -  c\^{}2))))
\mvdash{}  False


By

---

Latex:
((RWO  "-2"  7  THENA  Auto)  THEN  FLemma  `rneq\_irreflexivity`  [-1]  THEN  Auto)

---

Home Index