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 ) )