---

Step * of Lemma sine-exists

No Annotations
∀x:ℝ. ∃a:ℝ. Σi.-1^i * (x^(2 * i) + 1)/((2 * i) + 1)! = 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-lemma3` [⌜x⌝]⋅ THENA Auto)
   THEN Assert ⌜∃a:ℝ. Σi.-1^i * (x^2 * i)/((2 * i) + 1)! = a⌝⋅) }

1
.....assertion..... 
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)) + 1)!)/r(((2 * n) + 1)!))))))
⊢ ∃a:ℝ. Σi.-1^i * (x^2 * i)/((2 * i) + 1)! = a

2
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)) + 1)!)/r(((2 * n) + 1)!))))))
5. ∃a:ℝ. Σi.-1^i * (x^2 * i)/((2 * i) + 1)! = a
⊢ ∃a:ℝ. Σi.-1^i * (x^(2 * i) + 1)/((2 * i) + 1)! = a

---

Latex:

---

Latex:
No  Annotations
\mforall{}x:\mBbbR{}.  \mexists{}a:\mBbbR{}.  \mSigma{}i.-1\^{}i  *  (x\^{}(2  *  i)  +  1)/((2  *  i)  +  1)!  =  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-lemma3`  [\mkleeneopen{}x\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  Assert  \mkleeneopen{}\mexists{}a:\mBbbR{}.  \mSigma{}i.-1\^{}i  *  (x\^{}2  *  i)/((2  *  i)  +  1)!  =  a\mkleeneclose{}\mcdot{})

---

Home Index