---

Step * 1 2 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:ℝ. 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
{ ((Assert ∀x:ℝ. (f(x) = f(r0)) BY
          (Auto THEN (BLemma `not-rneq` THENA Auto) THEN ParallelOp -2 THEN Auto))
   THEN (Assert ∀x:ℝ. ((g(x) * g(r0)) = (f(r0) - f(r0)^2)) BY
               (ParallelOp 5
                THEN (D -1 With ⌜r0⌝  THENA Auto)
                THEN (RWO "-3" (-1) THENA Auto)
                THEN RWO "rnexp2<" (-1)
                THEN Auto
                THEN (nRAdd ⌜f(r0)^2⌝ 0⋅ THEN Auto)
                THEN nRNorm (-1)
                THEN Auto))
   THEN (InstHyp [⌜r0⌝] (-1)⋅ THENA Auto)
   THEN (InstHyp [⌜r0⌝;⌜r0⌝] 5⋅ THENA Auto)
   THEN (nRNorm (-1) THENA Auto)
   THEN Try ((Fold `rfun-ap` 0 THEN BackThruSomeHyp THEN 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)))
⊢ ¬¬((∃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))))))

---

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.  \mneg{}(\mexists{}a:\mBbbR{}.  f(a)  \mneq{}  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:
((Assert  \mforall{}x:\mBbbR{}.  (f(x)  =  f(r0))  BY
                (Auto  THEN  (BLemma  `not-rneq`  THENA  Auto)  THEN  ParallelOp  -2  THEN  Auto))
  THEN  (Assert  \mforall{}x:\mBbbR{}.  ((g(x)  *  g(r0))  =  (f(r0)  -  f(r0)\^{}2))  BY
                          (ParallelOp  5
                            THEN  (D  -1  With  \mkleeneopen{}r0\mkleeneclose{}    THENA  Auto)
                            THEN  (RWO  "-3"  (-1)  THENA  Auto)
                            THEN  RWO  "rnexp2<"  (-1)
                            THEN  Auto
                            THEN  (nRAdd  \mkleeneopen{}f(r0)\^{}2\mkleeneclose{}  0\mcdot{}  THEN  Auto)
                            THEN  nRNorm  (-1)
                            THEN  Auto))
  THEN  (InstHyp  [\mkleeneopen{}r0\mkleeneclose{}]  (-1)\mcdot{}  THENA  Auto)
  THEN  (InstHyp  [\mkleeneopen{}r0\mkleeneclose{};\mkleeneopen{}r0\mkleeneclose{}]  5\mcdot{}  THENA  Auto)
  THEN  (nRNorm  (-1)  THENA  Auto)
  THEN  Try  ((Fold  `rfun-ap`  0  THEN  BackThruSomeHyp  THEN  Auto)))

---

Home Index