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