Step
*
1
2
1
1
1
of Lemma
sine-exists
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. lim n→∞.(|x|^n/r((n + 1)!)) = r0
6. ∀y:ℕ ⟶ ℝ
((∃N:ℕ. ∀n:ℕ. ∃m:ℕ. ((n ≤ m) ∧ (y[n] = (|x|^m/r((m + 1)!)))) supposing N ≤ n)
⇒ lim n→∞.(|x|^n/r((n + 1)!)) = r0
⇒ lim n→∞.y[n] = r0)
7. i : ℕ
8. 0 ≤ i
9. i ≤ (2 * i)
⊢ (x^2 * i)/((2 * i) + 1)! = (|x|^2 * i/r(((2 * i) + 1)!))
BY
{ (RWO "int-rdiv-req" 0 THEN Auto THEN nRMul ⌜r(((2 * i) + 1)!)⌝ 0⋅ THEN Auto) }
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)) + 1)!)/r(((2 * n) + 1)!))))))
5. lim n→∞.(|x|^n/r((n + 1)!)) = r0
6. ∀y:ℕ ⟶ ℝ
((∃N:ℕ. ∀n:ℕ. ∃m:ℕ. ((n ≤ m) ∧ (y[n] = (|x|^m/r((m + 1)!)))) supposing N ≤ n)
⇒ lim n→∞.(|x|^n/r((n + 1)!)) = r0
⇒ lim n→∞.y[n] = r0)
7. i : ℕ
8. 0 ≤ i
9. i ≤ (2 * i)
10. ¬(r0 ≤ x)
⊢ x^2 * i = |x|^2 * i
Latex:
Latex:
1. x : \mBbbR{}
2. b : \mBbbN{}
3. |x| \mleq{} r(b)
4. \mforall{}b:\mBbbN{}
(((x * x) \mleq{} r(b * b))
{}\mRightarrow{} (\mforall{}n:\mBbbN{}. (((b \mdiv{} 2) \mleq{} n) {}\mRightarrow{} ((x * x) \mleq{} (r(((2 * (n + 1)) + 1)!)/r(((2 * n) + 1)!))))))
5. lim n\mrightarrow{}\minfty{}.(|x|\^{}n/r((n + 1)!)) = r0
6. \mforall{}y:\mBbbN{} {}\mrightarrow{} \mBbbR{}
((\mexists{}N:\mBbbN{}. \mforall{}n:\mBbbN{}. \mexists{}m:\mBbbN{}. ((n \mleq{} m) \mwedge{} (y[n] = (|x|\^{}m/r((m + 1)!)))) supposing N \mleq{} n)
{}\mRightarrow{} lim n\mrightarrow{}\minfty{}.(|x|\^{}n/r((n + 1)!)) = r0
{}\mRightarrow{} lim n\mrightarrow{}\minfty{}.y[n] = r0)
7. i : \mBbbN{}
8. 0 \mleq{} i
9. i \mleq{} (2 * i)
\mvdash{} (x\^{}2 * i)/((2 * i) + 1)! = (|x|\^{}2 * i/r(((2 * i) + 1)!))
By
Latex:
(RWO "int-rdiv-req" 0 THEN Auto THEN nRMul \mkleeneopen{}r(((2 * i) + 1)!)\mkleeneclose{} 0\mcdot{} THEN Auto)
Home
Index