Step |
Hyp |
Ref |
Expression |
1 |
|
gsumncl.k |
|- K = ( Base ` M ) |
2 |
|
gsumncl.w |
|- ( ph -> M e. Mnd ) |
3 |
|
gsumncl.p |
|- ( ph -> P e. ( ZZ>= ` N ) ) |
4 |
|
gsumncl.b |
|- ( ( ph /\ k e. ( N ... P ) ) -> B e. K ) |
5 |
|
gsumnunsn.a |
|- .+ = ( +g ` M ) |
6 |
|
gsumnunsn.l |
|- ( ph -> C e. K ) |
7 |
|
gsumnunsn.c |
|- ( ( ph /\ k = ( P + 1 ) ) -> B = C ) |
8 |
|
seqp1 |
|- ( P e. ( ZZ>= ` N ) -> ( seq N ( .+ , ( k e. ( N ... ( P + 1 ) ) |-> B ) ) ` ( P + 1 ) ) = ( ( seq N ( .+ , ( k e. ( N ... ( P + 1 ) ) |-> B ) ) ` P ) .+ ( ( k e. ( N ... ( P + 1 ) ) |-> B ) ` ( P + 1 ) ) ) ) |
9 |
3 8
|
syl |
|- ( ph -> ( seq N ( .+ , ( k e. ( N ... ( P + 1 ) ) |-> B ) ) ` ( P + 1 ) ) = ( ( seq N ( .+ , ( k e. ( N ... ( P + 1 ) ) |-> B ) ) ` P ) .+ ( ( k e. ( N ... ( P + 1 ) ) |-> B ) ` ( P + 1 ) ) ) ) |
10 |
|
peano2uz |
|- ( P e. ( ZZ>= ` N ) -> ( P + 1 ) e. ( ZZ>= ` N ) ) |
11 |
3 10
|
syl |
|- ( ph -> ( P + 1 ) e. ( ZZ>= ` N ) ) |
12 |
4
|
adantlr |
|- ( ( ( ph /\ k e. ( N ... ( P + 1 ) ) ) /\ k e. ( N ... P ) ) -> B e. K ) |
13 |
7
|
adantlr |
|- ( ( ( ph /\ k e. ( N ... ( P + 1 ) ) ) /\ k = ( P + 1 ) ) -> B = C ) |
14 |
6
|
ad2antrr |
|- ( ( ( ph /\ k e. ( N ... ( P + 1 ) ) ) /\ k = ( P + 1 ) ) -> C e. K ) |
15 |
13 14
|
eqeltrd |
|- ( ( ( ph /\ k e. ( N ... ( P + 1 ) ) ) /\ k = ( P + 1 ) ) -> B e. K ) |
16 |
|
elfzp1 |
|- ( P e. ( ZZ>= ` N ) -> ( k e. ( N ... ( P + 1 ) ) <-> ( k e. ( N ... P ) \/ k = ( P + 1 ) ) ) ) |
17 |
3 16
|
syl |
|- ( ph -> ( k e. ( N ... ( P + 1 ) ) <-> ( k e. ( N ... P ) \/ k = ( P + 1 ) ) ) ) |
18 |
17
|
biimpa |
|- ( ( ph /\ k e. ( N ... ( P + 1 ) ) ) -> ( k e. ( N ... P ) \/ k = ( P + 1 ) ) ) |
19 |
12 15 18
|
mpjaodan |
|- ( ( ph /\ k e. ( N ... ( P + 1 ) ) ) -> B e. K ) |
20 |
19
|
fmpttd |
|- ( ph -> ( k e. ( N ... ( P + 1 ) ) |-> B ) : ( N ... ( P + 1 ) ) --> K ) |
21 |
1 5 2 11 20
|
gsumval2 |
|- ( ph -> ( M gsum ( k e. ( N ... ( P + 1 ) ) |-> B ) ) = ( seq N ( .+ , ( k e. ( N ... ( P + 1 ) ) |-> B ) ) ` ( P + 1 ) ) ) |
22 |
4
|
fmpttd |
|- ( ph -> ( k e. ( N ... P ) |-> B ) : ( N ... P ) --> K ) |
23 |
1 5 2 3 22
|
gsumval2 |
|- ( ph -> ( M gsum ( k e. ( N ... P ) |-> B ) ) = ( seq N ( .+ , ( k e. ( N ... P ) |-> B ) ) ` P ) ) |
24 |
|
fvres |
|- ( i e. ( N ... P ) -> ( ( ( k e. ( N ... ( P + 1 ) ) |-> B ) |` ( N ... P ) ) ` i ) = ( ( k e. ( N ... ( P + 1 ) ) |-> B ) ` i ) ) |
25 |
24
|
adantl |
|- ( ( ph /\ i e. ( N ... P ) ) -> ( ( ( k e. ( N ... ( P + 1 ) ) |-> B ) |` ( N ... P ) ) ` i ) = ( ( k e. ( N ... ( P + 1 ) ) |-> B ) ` i ) ) |
26 |
|
fzssp1 |
|- ( N ... P ) C_ ( N ... ( P + 1 ) ) |
27 |
|
resmpt |
|- ( ( N ... P ) C_ ( N ... ( P + 1 ) ) -> ( ( k e. ( N ... ( P + 1 ) ) |-> B ) |` ( N ... P ) ) = ( k e. ( N ... P ) |-> B ) ) |
28 |
26 27
|
ax-mp |
|- ( ( k e. ( N ... ( P + 1 ) ) |-> B ) |` ( N ... P ) ) = ( k e. ( N ... P ) |-> B ) |
29 |
28
|
fveq1i |
|- ( ( ( k e. ( N ... ( P + 1 ) ) |-> B ) |` ( N ... P ) ) ` i ) = ( ( k e. ( N ... P ) |-> B ) ` i ) |
30 |
25 29
|
eqtr3di |
|- ( ( ph /\ i e. ( N ... P ) ) -> ( ( k e. ( N ... ( P + 1 ) ) |-> B ) ` i ) = ( ( k e. ( N ... P ) |-> B ) ` i ) ) |
31 |
3 30
|
seqfveq |
|- ( ph -> ( seq N ( .+ , ( k e. ( N ... ( P + 1 ) ) |-> B ) ) ` P ) = ( seq N ( .+ , ( k e. ( N ... P ) |-> B ) ) ` P ) ) |
32 |
23 31
|
eqtr4d |
|- ( ph -> ( M gsum ( k e. ( N ... P ) |-> B ) ) = ( seq N ( .+ , ( k e. ( N ... ( P + 1 ) ) |-> B ) ) ` P ) ) |
33 |
|
eqidd |
|- ( ph -> ( k e. ( N ... ( P + 1 ) ) |-> B ) = ( k e. ( N ... ( P + 1 ) ) |-> B ) ) |
34 |
|
eluzfz2 |
|- ( ( P + 1 ) e. ( ZZ>= ` N ) -> ( P + 1 ) e. ( N ... ( P + 1 ) ) ) |
35 |
11 34
|
syl |
|- ( ph -> ( P + 1 ) e. ( N ... ( P + 1 ) ) ) |
36 |
33 7 35 6
|
fvmptd |
|- ( ph -> ( ( k e. ( N ... ( P + 1 ) ) |-> B ) ` ( P + 1 ) ) = C ) |
37 |
36
|
eqcomd |
|- ( ph -> C = ( ( k e. ( N ... ( P + 1 ) ) |-> B ) ` ( P + 1 ) ) ) |
38 |
32 37
|
oveq12d |
|- ( ph -> ( ( M gsum ( k e. ( N ... P ) |-> B ) ) .+ C ) = ( ( seq N ( .+ , ( k e. ( N ... ( P + 1 ) ) |-> B ) ) ` P ) .+ ( ( k e. ( N ... ( P + 1 ) ) |-> B ) ` ( P + 1 ) ) ) ) |
39 |
9 21 38
|
3eqtr4d |
|- ( ph -> ( M gsum ( k e. ( N ... ( P + 1 ) ) |-> B ) ) = ( ( M gsum ( k e. ( N ... P ) |-> B ) ) .+ C ) ) |