Step
*
1
of Lemma
exp-series-converges
.....assertion.....
1. x : ℝ
⊢ ∃N:ℕ. ∀n:{N...}. (|(x^n + 1)/(n + 1)!| ≤ (|(x^n)/(n)!|/r(2)))
BY
{ ((InstLemma `r-archimedean2` [⌜x⌝]⋅ THENA Auto) THEN ParallelLast THEN Try (ParallelLast) THEN Auto) }
1
1. x : ℝ
2. N : ℕ
3. n : {N...}
4. |(x/r(n + 1))| ≤ (r1/r(2))
⊢ |(x^n + 1)/(n + 1)!| ≤ (|(x^n)/(n)!|/r(2))
Latex:
Latex:
.....assertion.....
1. x : \mBbbR{}
\mvdash{} \mexists{}N:\mBbbN{}. \mforall{}n:\{N...\}. (|(x\^{}n + 1)/(n + 1)!| \mleq{} (|(x\^{}n)/(n)!|/r(2)))
By
Latex:
((InstLemma `r-archimedean2` [\mkleeneopen{}x\mkleeneclose{}]\mcdot{} THENA Auto) THEN ParallelLast THEN Try (ParallelLast) THEN Auto)
Home
Index