This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem isumnn0nn

Description: Sum from 0 to infinity in terms of sum from 1 to infinity. (Contributed by NM, 2-Jan-2006) (Revised by Mario Carneiro, 24-Apr-2014)

Ref Expression
Hypotheses isumnn0nn.1 
|- ( k = 0 -> A = B )
isumnn0nn.2 
|- ( ( ph /\ k e. NN0 ) -> ( F ` k ) = A )
isumnn0nn.3 
|- ( ( ph /\ k e. NN0 ) -> A e. CC )
isumnn0nn.4 
|- ( ph -> seq 0 ( + , F ) e. dom ~~> )
Assertion isumnn0nn 
|- ( ph -> sum_ k e. NN0 A = ( B + sum_ k e. NN A ) )

Proof

Step Hyp Ref Expression
1 isumnn0nn.1 
 |-  ( k = 0 -> A = B )
2 isumnn0nn.2 
 |-  ( ( ph /\ k e. NN0 ) -> ( F ` k ) = A )
3 isumnn0nn.3 
 |-  ( ( ph /\ k e. NN0 ) -> A e. CC )
4 isumnn0nn.4 
 |-  ( ph -> seq 0 ( + , F ) e. dom ~~> )
5 nn0uz 
 |-  NN0 = ( ZZ>= ` 0 )
6 0zd 
 |-  ( ph -> 0 e. ZZ )
7 5 6 2 3 4 isum1p 
 |-  ( ph -> sum_ k e. NN0 A = ( ( F ` 0 ) + sum_ k e. ( ZZ>= ` ( 0 + 1 ) ) A ) )
8 fveq2 
 |-  ( k = 0 -> ( F ` k ) = ( F ` 0 ) )
9 8 1 eqeq12d 
 |-  ( k = 0 -> ( ( F ` k ) = A <-> ( F ` 0 ) = B ) )
10 2 ralrimiva 
 |-  ( ph -> A. k e. NN0 ( F ` k ) = A )
11 0nn0 
 |-  0 e. NN0
12 11 a1i 
 |-  ( ph -> 0 e. NN0 )
13 9 10 12 rspcdva 
 |-  ( ph -> ( F ` 0 ) = B )
14 0p1e1 
 |-  ( 0 + 1 ) = 1
15 14 fveq2i 
 |-  ( ZZ>= ` ( 0 + 1 ) ) = ( ZZ>= ` 1 )
16 nnuz 
 |-  NN = ( ZZ>= ` 1 )
17 15 16 eqtr4i 
 |-  ( ZZ>= ` ( 0 + 1 ) ) = NN
18 17 sumeq1i 
 |-  sum_ k e. ( ZZ>= ` ( 0 + 1 ) ) A = sum_ k e. NN A
19 18 a1i 
 |-  ( ph -> sum_ k e. ( ZZ>= ` ( 0 + 1 ) ) A = sum_ k e. NN A )
20 13 19 oveq12d 
 |-  ( ph -> ( ( F ` 0 ) + sum_ k e. ( ZZ>= ` ( 0 + 1 ) ) A ) = ( B + sum_ k e. NN A ) )
21 7 20 eqtrd 
 |-  ( ph -> sum_ k e. NN0 A = ( B + sum_ k e. NN A ) )