Step
*
2
of Lemma
triangular-reciprocal-series-sum
1. lim n→∞.r(2) - (r(2)/r(n + 2)) = r(2)
⊢ Σn.(r1/r(t(n + 1))) = r(2)
BY
{ (Assert ∀i:ℕ. (1 ≤ t(i + 1)) BY
(Auto
THEN (InstLemma `triangular-num-le` [⌜1⌝;⌜i + 1⌝]⋅ THENA Auto)
THEN Unfold `triangular-num` -1
THEN Reduce (-1)
THEN Fold `triangular-num` (-1)
THEN Auto)) }
1
1. lim n→∞.r(2) - (r(2)/r(n + 2)) = r(2)
2. ∀i:ℕ. (1 ≤ t(i + 1))
⊢ Σn.(r1/r(t(n + 1))) = r(2)
Latex:
Latex:
1. lim n\mrightarrow{}\minfty{}.r(2) - (r(2)/r(n + 2)) = r(2)
\mvdash{} \mSigma{}n.(r1/r(t(n + 1))) = r(2)
By
Latex:
(Assert \mforall{}i:\mBbbN{}. (1 \mleq{} t(i + 1)) BY
(Auto
THEN (InstLemma `triangular-num-le` [\mkleeneopen{}1\mkleeneclose{};\mkleeneopen{}i + 1\mkleeneclose{}]\mcdot{} THENA Auto)
THEN Unfold `triangular-num` -1
THEN Reduce (-1)
THEN Fold `triangular-num` (-1)
THEN Auto))
Home
Index