---

Step * of Lemma cosine-exists

No Annotations
∀x:ℝ. ∃a:ℝ. Σi.-1^i * (x^2 * i)/(2 * i)! = a
BY
{ ((D 0 THENA Auto)
   THEN (Evaluate ⌜y = x ∈ ℝ⌝⋅ THENA (Auto THEN D 0 THEN With ⌜1⌝ (D 0)⋅ THEN Auto))⋅
   THEN RWO "-1<" 0
   THEN Auto'
   THEN ThinVar `x'
   THEN RenameVar `x' 1
   THEN Auto
   THEN (InstLemma `r-archimedean-rabs` [⌜x⌝]⋅ THENA Auto)
   THEN ExRepD
   THEN RenameVar `b' (-2)
   THEN (Evaluate ⌜c = b ∈ ℕ⌝⋅ THENA Auto)
   THEN (Assert |x| ≤ r(c) BY
               (HypSubst' (-1) 0 THEN Trivial))
   THEN ThinVar `b'
   THEN RenameTo `b' `c'
   THEN (InstLemma `rdiv-factorial-lemma2` [⌜x⌝]⋅ THENA Auto)
   THEN (Assert ⌜∃a:ℝ. Σi.-1^i * (x^2 * i)/(2 * i)! = a⌝⋅ THENM (D (-1) THEN With ⌜a⌝ (D 0)⋅ THEN Auto' THEN Auto))
   THEN Fold `series-converges` 0) }

1
1. x : ℝ
2. b : ℕ
3. |x| ≤ r(b)
4. ∀b:ℕ. (((x * x) ≤ r(b * b)) ⇒ (∀n:ℕ. (((b ÷ 2) ≤ n) ⇒ ((x * x) ≤ (r((2 * (n + 1))!)/r((2 * n)!))))))
⊢ Σi.-1^i * (x^2 * i)/(2 * i)!↓

---

Latex:

---

Latex:
No  Annotations
\mforall{}x:\mBbbR{}.  \mexists{}a:\mBbbR{}.  \mSigma{}i.-1\^{}i  *  (x\^{}2  *  i)/(2  *  i)!  =  a


By

---

Latex:
((D  0  THENA  Auto)
  THEN  (Evaluate  \mkleeneopen{}y  =  x\mkleeneclose{}\mcdot{}  THENA  (Auto  THEN  D  0  THEN  With  \mkleeneopen{}1\mkleeneclose{}  (D  0)\mcdot{}  THEN  Auto))\mcdot{}
  THEN  RWO  "-1<"  0
  THEN  Auto'
  THEN  ThinVar  `x'
  THEN  RenameVar  `x'  1
  THEN  Auto
  THEN  (InstLemma  `r-archimedean-rabs`  [\mkleeneopen{}x\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  ExRepD
  THEN  RenameVar  `b'  (-2)
  THEN  (Evaluate  \mkleeneopen{}c  =  b\mkleeneclose{}\mcdot{}  THENA  Auto)
  THEN  (Assert  |x|  \mleq{}  r(c)  BY
                          (HypSubst'  (-1)  0  THEN  Trivial))
  THEN  ThinVar  `b'
  THEN  RenameTo  `b'  `c'
  THEN  (InstLemma  `rdiv-factorial-lemma2`  [\mkleeneopen{}x\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  (Assert  \mkleeneopen{}\mexists{}a:\mBbbR{}.  \mSigma{}i.-1\^{}i  *  (x\^{}2  *  i)/(2  *  i)!  =  a\mkleeneclose{}\mcdot{}
  THENM  (D  (-1)  THEN  With  \mkleeneopen{}a\mkleeneclose{}  (D  0)\mcdot{}  THEN  Auto'  THEN  Auto)
  )
  THEN  Fold  `series-converges`  0)

---

Home Index