Intuitionistic Logic Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  ILE Home  >  Th. List  >  ser0 Unicode version

Theorem ser0 9945
 Description: The value of the partial sums in a zero-valued infinite series. (Contributed by Mario Carneiro, 31-Aug-2013.) (Revised by Mario Carneiro, 15-Dec-2014.)
Hypothesis
Ref Expression
ser0.1
Assertion
Ref Expression
ser0

Proof of Theorem ser0
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 eluzel2 9022 . . . . 5
2 ser0.1 . . . . 5
31, 2eleq2s 2182 . . . 4
4 0cn 7478 . . . . . 6
52eleq2i 2154 . . . . . . . 8
65biimpri 131 . . . . . . 7
76adantl 271 . . . . . 6
8 fvconst2g 5511 . . . . . 6
94, 7, 8sylancr 405 . . . . 5
109, 4syl6eqel 2178 . . . 4
113, 10iseqseq3 9898 . . 3
1211fveq1d 5307 . 2
13 00id 7621 . . . 4
1413a1i 9 . . 3
152eleq2i 2154 . . . 4
1615biimpi 118 . . 3
17 elfzuz 9434 . . . . . 6
1817, 2syl6eleqr 2181 . . . . 5
1918adantl 271 . . . 4
204, 19, 8sylancr 405 . . 3
21 0cnd 7479 . . 3
22 addcl 7465 . . . 4