---

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

∀f,g:ℝ ⟶ ℝ.
  ((∀x,y:ℝ.  ((x = y) ⇒ (f(x) = f(y))))
  ⇒ (∀x,y:ℝ.  ((x = y) ⇒ (g(x) = g(y))))
  ⇒ (∃a,b:ℝ. f(a) ≠ f(b))
  ⇒ (∀x,y:ℝ.  (f(x - y) = ((f(x) * f(y)) + (g(x) * g(y)))))
  ⇒ (¬¬(∃a:ℝ. (a ≠ r0 ∧ (∀x:ℝ. (f(x) = rcos(a * x))) ∧ (∀x:ℝ. (g(x) = rsin(a * x)))))))
BY
{ (Auto
   THEN (InstLemma `cos-sin-equation` [⌜f⌝;⌜g⌝]⋅ THENA Auto)
   THEN D -1
   THEN Thin (-1)
   THEN (D -1 THENA Auto)
   THEN ExRepD
   THEN (SupposeMore (-1) THENA Auto)
   THEN D -1
   THEN (((RemoveDoubleNegation THENM Trivial) THEN Auto) ORELSE ((Assert ⌜False⌝⋅ THEN Auto) THEN ExRepD))) }

1
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

---

Latex:

---

Latex:
\mforall{}f,g:\mBbbR{}  {}\mrightarrow{}  \mBbbR{}.
    ((\mforall{}x,y:\mBbbR{}.    ((x  =  y)  {}\mRightarrow{}  (f(x)  =  f(y))))
    {}\mRightarrow{}  (\mforall{}x,y:\mBbbR{}.    ((x  =  y)  {}\mRightarrow{}  (g(x)  =  g(y))))
    {}\mRightarrow{}  (\mexists{}a,b:\mBbbR{}.  f(a)  \mneq{}  f(b))
    {}\mRightarrow{}  (\mforall{}x,y:\mBbbR{}.    (f(x  -  y)  =  ((f(x)  *  f(y))  +  (g(x)  *  g(y)))))
    {}\mRightarrow{}  (\mneg{}\mneg{}(\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:
(Auto
  THEN  (InstLemma  `cos-sin-equation`  [\mkleeneopen{}f\mkleeneclose{};\mkleeneopen{}g\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  D  -1
  THEN  Thin  (-1)
  THEN  (D  -1  THENA  Auto)
  THEN  ExRepD
  THEN  (SupposeMore  (-1)  THENA  Auto)
  THEN  D  -1
  THEN  (((RemoveDoubleNegation  THENM  Trivial)  THEN  Auto)
  ORELSE  ((Assert  \mkleeneopen{}False\mkleeneclose{}\mcdot{}  THEN  Auto)  THEN  ExRepD)
  ))

---

Home Index