Metamath Proof Explorer

Theorem zsum

Description: Series sum with index set a subset of the upper integers. (Contributed by Mario Carneiro, 13-Jun-2019)

Ref Expression
Hypotheses zsum.1 
|- Z = ( ZZ>= ` M )
zsum.2 
|- ( ph -> M e. ZZ )
zsum.3 
|- ( ph -> A C_ Z )
zsum.4 
|- ( ( ph /\ k e. Z ) -> ( F ` k ) = if ( k e. A , B , 0 ) )
zsum.5 
|- ( ( ph /\ k e. A ) -> B e. CC )
Assertion zsum 
|- ( ph -> sum_ k e. A B = ( ~~> ` seq M ( + , F ) ) )

Proof

Step Hyp Ref Expression
1 zsum.1 
 |-  Z = ( ZZ>= ` M )
2 zsum.2 
 |-  ( ph -> M e. ZZ )
3 zsum.3 
 |-  ( ph -> A C_ Z )
4 zsum.4 
 |-  ( ( ph /\ k e. Z ) -> ( F ` k ) = if ( k e. A , B , 0 ) )
5 zsum.5 
 |-  ( ( ph /\ k e. A ) -> B e. CC )
6 eleq1w 
 |-  ( n = i -> ( n e. A <-> i e. A ) )
7 csbeq1 
 |-  ( n = i -> [_ n / k ]_ B = [_ i / k ]_ B )
8 6 7 ifbieq1d 
 |-  ( n = i -> if ( n e. A , [_ n / k ]_ B , 0 ) = if ( i e. A , [_ i / k ]_ B , 0 ) )
9 8 cbvmptv 
 |-  ( n e. ZZ |-> if ( n e. A , [_ n / k ]_ B , 0 ) ) = ( i e. ZZ |-> if ( i e. A , [_ i / k ]_ B , 0 ) )
10 simpll 
 |-  ( ( ( ph /\ m e. ZZ ) /\ A C_ ( ZZ>= ` m ) ) -> ph )
11 5 ralrimiva 
 |-  ( ph -> A. k e. A B e. CC )
12 nfcsb1v 
 |-  F/_ k [_ i / k ]_ B
13 12 nfel1 
 |-  F/ k [_ i / k ]_ B e. CC
14 csbeq1a 
 |-  ( k = i -> B = [_ i / k ]_ B )
15 14 eleq1d 
 |-  ( k = i -> ( B e. CC <-> [_ i / k ]_ B e. CC ) )
16 13 15 rspc 
 |-  ( i e. A -> ( A. k e. A B e. CC -> [_ i / k ]_ B e. CC ) )
17 11 16 syl5 
 |-  ( i e. A -> ( ph -> [_ i / k ]_ B e. CC ) )
18 10 17 mpan9 
 |-  ( ( ( ( ph /\ m e. ZZ ) /\ A C_ ( ZZ>= ` m ) ) /\ i e. A ) -> [_ i / k ]_ B e. CC )
19 simplr 
 |-  ( ( ( ph /\ m e. ZZ ) /\ A C_ ( ZZ>= ` m ) ) -> m e. ZZ )
20 2 ad2antrr 
 |-  ( ( ( ph /\ m e. ZZ ) /\ A C_ ( ZZ>= ` m ) ) -> M e. ZZ )
21 simpr 
 |-  ( ( ( ph /\ m e. ZZ ) /\ A C_ ( ZZ>= ` m ) ) -> A C_ ( ZZ>= ` m ) )
22 3 1 sseqtrdi 
 |-  ( ph -> A C_ ( ZZ>= ` M ) )
23 22 ad2antrr 
 |-  ( ( ( ph /\ m e. ZZ ) /\ A C_ ( ZZ>= ` m ) ) -> A C_ ( ZZ>= ` M ) )
24 9 18 19 20 21 23 sumrb 
 |-  ( ( ( ph /\ m e. ZZ ) /\ A C_ ( ZZ>= ` m ) ) -> ( seq m ( + , ( n e. ZZ |-> if ( n e. A , [_ n / k ]_ B , 0 ) ) ) ~~> x <-> seq M ( + , ( n e. ZZ |-> if ( n e. A , [_ n / k ]_ B , 0 ) ) ) ~~> x ) )
25 24 biimpd 
 |-  ( ( ( ph /\ m e. ZZ ) /\ A C_ ( ZZ>= ` m ) ) -> ( seq m ( + , ( n e. ZZ |-> if ( n e. A , [_ n / k ]_ B , 0 ) ) ) ~~> x -> seq M ( + , ( n e. ZZ |-> if ( n e. A , [_ n / k ]_ B , 0 ) ) ) ~~> x ) )
26 25 expimpd 
 |-  ( ( ph /\ m e. ZZ ) -> ( ( A C_ ( ZZ>= ` m ) /\ seq m ( + , ( n e. ZZ |-> if ( n e. A , [_ n / k ]_ B , 0 ) ) ) ~~> x ) -> seq M ( + , ( n e. ZZ |-> if ( n e. A , [_ n / k ]_ B , 0 ) ) ) ~~> x ) )
27 26 rexlimdva 
 |-  ( ph -> ( E. m e. ZZ ( A C_ ( ZZ>= ` m ) /\ seq m ( + , ( n e. ZZ |-> if ( n e. A , [_ n / k ]_ B , 0 ) ) ) ~~> x ) -> seq M ( + , ( n e. ZZ |-> if ( n e. A , [_ n / k ]_ B , 0 ) ) ) ~~> x ) )
28 3 ad2antrr 
 |-  ( ( ( ph /\ m e. NN ) /\ f : ( 1 ... m ) -1-1-onto-> A ) -> A C_ Z )
29 uzssz 
 |-  ( ZZ>= ` M ) C_ ZZ
30 1 29 eqsstri 
 |-  Z C_ ZZ
31 zssre 
 |-  ZZ C_ RR
32 30 31 sstri 
 |-  Z C_ RR
33 ltso 
 |-  < Or RR
34 soss 
 |-  ( Z C_ RR -> ( < Or RR -> < Or Z ) )
35 32 33 34 mp2 
 |-  < Or Z
36 soss 
 |-  ( A C_ Z -> ( < Or Z -> < Or A ) )
37 28 35 36 mpisyl 
 |-  ( ( ( ph /\ m e. NN ) /\ f : ( 1 ... m ) -1-1-onto-> A ) -> < Or A )
38 fzfi 
 |-  ( 1 ... m ) e. Fin
39 ovex 
 |-  ( 1 ... m ) e. _V
40 39 f1oen 
 |-  ( f : ( 1 ... m ) -1-1-onto-> A -> ( 1 ... m ) ~~ A )
41 40 adantl 
 |-  ( ( ( ph /\ m e. NN ) /\ f : ( 1 ... m ) -1-1-onto-> A ) -> ( 1 ... m ) ~~ A )
42 41 ensymd 
 |-  ( ( ( ph /\ m e. NN ) /\ f : ( 1 ... m ) -1-1-onto-> A ) -> A ~~ ( 1 ... m ) )
43 enfii 
 |-  ( ( ( 1 ... m ) e. Fin /\ A ~~ ( 1 ... m ) ) -> A e. Fin )
44 38 42 43 sylancr 
 |-  ( ( ( ph /\ m e. NN ) /\ f : ( 1 ... m ) -1-1-onto-> A ) -> A e. Fin )
45 fz1iso 
 |-  ( ( < Or A /\ A e. Fin ) -> E. g g Isom < , < ( ( 1 ... ( # ` A ) ) , A ) )
46 37 44 45 syl2anc 
 |-  ( ( ( ph /\ m e. NN ) /\ f : ( 1 ... m ) -1-1-onto-> A ) -> E. g g Isom < , < ( ( 1 ... ( # ` A ) ) , A ) )
47 simpll 
 |-  ( ( ( ph /\ m e. NN ) /\ ( f : ( 1 ... m ) -1-1-onto-> A /\ g Isom < , < ( ( 1 ... ( # ` A ) ) , A ) ) ) -> ph )
48 47 17 mpan9 
 |-  ( ( ( ( ph /\ m e. NN ) /\ ( f : ( 1 ... m ) -1-1-onto-> A /\ g Isom < , < ( ( 1 ... ( # ` A ) ) , A ) ) ) /\ i e. A ) -> [_ i / k ]_ B e. CC )
49 fveq2 
 |-  ( n = j -> ( f ` n ) = ( f ` j ) )
50 49 csbeq1d 
 |-  ( n = j -> [_ ( f ` n ) / k ]_ B = [_ ( f ` j ) / k ]_ B )
51 csbcow 
 |-  [_ ( f ` j ) / i ]_ [_ i / k ]_ B = [_ ( f ` j ) / k ]_ B
52 50 51 eqtr4di 
 |-  ( n = j -> [_ ( f ` n ) / k ]_ B = [_ ( f ` j ) / i ]_ [_ i / k ]_ B )
53 52 cbvmptv 
 |-  ( n e. NN |-> [_ ( f ` n ) / k ]_ B ) = ( j e. NN |-> [_ ( f ` j ) / i ]_ [_ i / k ]_ B )
54 eqid 
 |-  ( j e. NN |-> [_ ( g ` j ) / i ]_ [_ i / k ]_ B ) = ( j e. NN |-> [_ ( g ` j ) / i ]_ [_ i / k ]_ B )
55 simplr 
 |-  ( ( ( ph /\ m e. NN ) /\ ( f : ( 1 ... m ) -1-1-onto-> A /\ g Isom < , < ( ( 1 ... ( # ` A ) ) , A ) ) ) -> m e. NN )
56 2 ad2antrr 
 |-  ( ( ( ph /\ m e. NN ) /\ ( f : ( 1 ... m ) -1-1-onto-> A /\ g Isom < , < ( ( 1 ... ( # ` A ) ) , A ) ) ) -> M e. ZZ )
57 22 ad2antrr 
 |-  ( ( ( ph /\ m e. NN ) /\ ( f : ( 1 ... m ) -1-1-onto-> A /\ g Isom < , < ( ( 1 ... ( # ` A ) ) , A ) ) ) -> A C_ ( ZZ>= ` M ) )
58 simprl 
 |-  ( ( ( ph /\ m e. NN ) /\ ( f : ( 1 ... m ) -1-1-onto-> A /\ g Isom < , < ( ( 1 ... ( # ` A ) ) , A ) ) ) -> f : ( 1 ... m ) -1-1-onto-> A )
59 simprr 
 |-  ( ( ( ph /\ m e. NN ) /\ ( f : ( 1 ... m ) -1-1-onto-> A /\ g Isom < , < ( ( 1 ... ( # ` A ) ) , A ) ) ) -> g Isom < , < ( ( 1 ... ( # ` A ) ) , A ) )
60 9 48 53 54 55 56 57 58 59 summolem2a 
 |-  ( ( ( ph /\ m e. NN ) /\ ( f : ( 1 ... m ) -1-1-onto-> A /\ g Isom < , < ( ( 1 ... ( # ` A ) ) , A ) ) ) -> seq M ( + , ( n e. ZZ |-> if ( n e. A , [_ n / k ]_ B , 0 ) ) ) ~~> ( seq 1 ( + , ( n e. NN |-> [_ ( f ` n ) / k ]_ B ) ) ` m ) )
61 60 expr 
 |-  ( ( ( ph /\ m e. NN ) /\ f : ( 1 ... m ) -1-1-onto-> A ) -> ( g Isom < , < ( ( 1 ... ( # ` A ) ) , A ) -> seq M ( + , ( n e. ZZ |-> if ( n e. A , [_ n / k ]_ B , 0 ) ) ) ~~> ( seq 1 ( + , ( n e. NN |-> [_ ( f ` n ) / k ]_ B ) ) ` m ) ) )
62 61 exlimdv 
 |-  ( ( ( ph /\ m e. NN ) /\ f : ( 1 ... m ) -1-1-onto-> A ) -> ( E. g g Isom < , < ( ( 1 ... ( # ` A ) ) , A ) -> seq M ( + , ( n e. ZZ |-> if ( n e. A , [_ n / k ]_ B , 0 ) ) ) ~~> ( seq 1 ( + , ( n e. NN |-> [_ ( f ` n ) / k ]_ B ) ) ` m ) ) )
63 46 62 mpd 
 |-  ( ( ( ph /\ m e. NN ) /\ f : ( 1 ... m ) -1-1-onto-> A ) -> seq M ( + , ( n e. ZZ |-> if ( n e. A , [_ n / k ]_ B , 0 ) ) ) ~~> ( seq 1 ( + , ( n e. NN |-> [_ ( f ` n ) / k ]_ B ) ) ` m ) )
64 breq2 
 |-  ( x = ( seq 1 ( + , ( n e. NN |-> [_ ( f ` n ) / k ]_ B ) ) ` m ) -> ( seq M ( + , ( n e. ZZ |-> if ( n e. A , [_ n / k ]_ B , 0 ) ) ) ~~> x <-> seq M ( + , ( n e. ZZ |-> if ( n e. A , [_ n / k ]_ B , 0 ) ) ) ~~> ( seq 1 ( + , ( n e. NN |-> [_ ( f ` n ) / k ]_ B ) ) ` m ) ) )
65 63 64 syl5ibrcom 
 |-  ( ( ( ph /\ m e. NN ) /\ f : ( 1 ... m ) -1-1-onto-> A ) -> ( x = ( seq 1 ( + , ( n e. NN |-> [_ ( f ` n ) / k ]_ B ) ) ` m ) -> seq M ( + , ( n e. ZZ |-> if ( n e. A , [_ n / k ]_ B , 0 ) ) ) ~~> x ) )
66 65 expimpd 
 |-  ( ( ph /\ m e. NN ) -> ( ( f : ( 1 ... m ) -1-1-onto-> A /\ x = ( seq 1 ( + , ( n e. NN |-> [_ ( f ` n ) / k ]_ B ) ) ` m ) ) -> seq M ( + , ( n e. ZZ |-> if ( n e. A , [_ n / k ]_ B , 0 ) ) ) ~~> x ) )
67 66 exlimdv 
 |-  ( ( ph /\ m e. NN ) -> ( E. f ( f : ( 1 ... m ) -1-1-onto-> A /\ x = ( seq 1 ( + , ( n e. NN |-> [_ ( f ` n ) / k ]_ B ) ) ` m ) ) -> seq M ( + , ( n e. ZZ |-> if ( n e. A , [_ n / k ]_ B , 0 ) ) ) ~~> x ) )
68 67 rexlimdva 
 |-  ( ph -> ( E. m e. NN E. f ( f : ( 1 ... m ) -1-1-onto-> A /\ x = ( seq 1 ( + , ( n e. NN |-> [_ ( f ` n ) / k ]_ B ) ) ` m ) ) -> seq M ( + , ( n e. ZZ |-> if ( n e. A , [_ n / k ]_ B , 0 ) ) ) ~~> x ) )
69 27 68 jaod 
 |-  ( ph -> ( ( E. m e. ZZ ( A C_ ( ZZ>= ` m ) /\ seq m ( + , ( n e. ZZ |-> if ( n e. A , [_ n / k ]_ B , 0 ) ) ) ~~> x ) \/ E. m e. NN E. f ( f : ( 1 ... m ) -1-1-onto-> A /\ x = ( seq 1 ( + , ( n e. NN |-> [_ ( f ` n ) / k ]_ B ) ) ` m ) ) ) -> seq M ( + , ( n e. ZZ |-> if ( n e. A , [_ n / k ]_ B , 0 ) ) ) ~~> x ) )
70 2 adantr 
 |-  ( ( ph /\ seq M ( + , ( n e. ZZ |-> if ( n e. A , [_ n / k ]_ B , 0 ) ) ) ~~> x ) -> M e. ZZ )
71 22 adantr 
 |-  ( ( ph /\ seq M ( + , ( n e. ZZ |-> if ( n e. A , [_ n / k ]_ B , 0 ) ) ) ~~> x ) -> A C_ ( ZZ>= ` M ) )
72 simpr 
 |-  ( ( ph /\ seq M ( + , ( n e. ZZ |-> if ( n e. A , [_ n / k ]_ B , 0 ) ) ) ~~> x ) -> seq M ( + , ( n e. ZZ |-> if ( n e. A , [_ n / k ]_ B , 0 ) ) ) ~~> x )
73 fveq2 
 |-  ( m = M -> ( ZZ>= ` m ) = ( ZZ>= ` M ) )
74 73 sseq2d 
 |-  ( m = M -> ( A C_ ( ZZ>= ` m ) <-> A C_ ( ZZ>= ` M ) ) )
75 seqeq1 
 |-  ( m = M -> seq m ( + , ( n e. ZZ |-> if ( n e. A , [_ n / k ]_ B , 0 ) ) ) = seq M ( + , ( n e. ZZ |-> if ( n e. A , [_ n / k ]_ B , 0 ) ) ) )
76 75 breq1d 
 |-  ( m = M -> ( seq m ( + , ( n e. ZZ |-> if ( n e. A , [_ n / k ]_ B , 0 ) ) ) ~~> x <-> seq M ( + , ( n e. ZZ |-> if ( n e. A , [_ n / k ]_ B , 0 ) ) ) ~~> x ) )
77 74 76 anbi12d 
 |-  ( m = M -> ( ( A C_ ( ZZ>= ` m ) /\ seq m ( + , ( n e. ZZ |-> if ( n e. A , [_ n / k ]_ B , 0 ) ) ) ~~> x ) <-> ( A C_ ( ZZ>= ` M ) /\ seq M ( + , ( n e. ZZ |-> if ( n e. A , [_ n / k ]_ B , 0 ) ) ) ~~> x ) ) )
78 77 rspcev 
 |-  ( ( M e. ZZ /\ ( A C_ ( ZZ>= ` M ) /\ seq M ( + , ( n e. ZZ |-> if ( n e. A , [_ n / k ]_ B , 0 ) ) ) ~~> x ) ) -> E. m e. ZZ ( A C_ ( ZZ>= ` m ) /\ seq m ( + , ( n e. ZZ |-> if ( n e. A , [_ n / k ]_ B , 0 ) ) ) ~~> x ) )
79 70 71 72 78 syl12anc 
 |-  ( ( ph /\ seq M ( + , ( n e. ZZ |-> if ( n e. A , [_ n / k ]_ B , 0 ) ) ) ~~> x ) -> E. m e. ZZ ( A C_ ( ZZ>= ` m ) /\ seq m ( + , ( n e. ZZ |-> if ( n e. A , [_ n / k ]_ B , 0 ) ) ) ~~> x ) )
80 79 orcd 
 |-  ( ( ph /\ seq M ( + , ( n e. ZZ |-> if ( n e. A , [_ n / k ]_ B , 0 ) ) ) ~~> x ) -> ( E. m e. ZZ ( A C_ ( ZZ>= ` m ) /\ seq m ( + , ( n e. ZZ |-> if ( n e. A , [_ n / k ]_ B , 0 ) ) ) ~~> x ) \/ E. m e. NN E. f ( f : ( 1 ... m ) -1-1-onto-> A /\ x = ( seq 1 ( + , ( n e. NN |-> [_ ( f ` n ) / k ]_ B ) ) ` m ) ) ) )
81 80 ex 
 |-  ( ph -> ( seq M ( + , ( n e. ZZ |-> if ( n e. A , [_ n / k ]_ B , 0 ) ) ) ~~> x -> ( E. m e. ZZ ( A C_ ( ZZ>= ` m ) /\ seq m ( + , ( n e. ZZ |-> if ( n e. A , [_ n / k ]_ B , 0 ) ) ) ~~> x ) \/ E. m e. NN E. f ( f : ( 1 ... m ) -1-1-onto-> A /\ x = ( seq 1 ( + , ( n e. NN |-> [_ ( f ` n ) / k ]_ B ) ) ` m ) ) ) ) )
82 69 81 impbid 
 |-  ( ph -> ( ( E. m e. ZZ ( A C_ ( ZZ>= ` m ) /\ seq m ( + , ( n e. ZZ |-> if ( n e. A , [_ n / k ]_ B , 0 ) ) ) ~~> x ) \/ E. m e. NN E. f ( f : ( 1 ... m ) -1-1-onto-> A /\ x = ( seq 1 ( + , ( n e. NN |-> [_ ( f ` n ) / k ]_ B ) ) ` m ) ) ) <-> seq M ( + , ( n e. ZZ |-> if ( n e. A , [_ n / k ]_ B , 0 ) ) ) ~~> x ) )
83 simpr 
 |-  ( ( ph /\ j e. ( ZZ>= ` M ) ) -> j e. ( ZZ>= ` M ) )
84 29 83 sseldi 
 |-  ( ( ph /\ j e. ( ZZ>= ` M ) ) -> j e. ZZ )
85 83 1 eleqtrrdi 
 |-  ( ( ph /\ j e. ( ZZ>= ` M ) ) -> j e. Z )
86 4 ralrimiva 
 |-  ( ph -> A. k e. Z ( F ` k ) = if ( k e. A , B , 0 ) )
87 86 adantr 
 |-  ( ( ph /\ j e. ( ZZ>= ` M ) ) -> A. k e. Z ( F ` k ) = if ( k e. A , B , 0 ) )
88 nfcsb1v 
 |-  F/_ k [_ j / k ]_ if ( k e. A , B , 0 )
89 88 nfeq2 
 |-  F/ k ( F ` j ) = [_ j / k ]_ if ( k e. A , B , 0 )
90 fveq2 
 |-  ( k = j -> ( F ` k ) = ( F ` j ) )
91 csbeq1a 
 |-  ( k = j -> if ( k e. A , B , 0 ) = [_ j / k ]_ if ( k e. A , B , 0 ) )
92 90 91 eqeq12d 
 |-  ( k = j -> ( ( F ` k ) = if ( k e. A , B , 0 ) <-> ( F ` j ) = [_ j / k ]_ if ( k e. A , B , 0 ) ) )
93 89 92 rspc 
 |-  ( j e. Z -> ( A. k e. Z ( F ` k ) = if ( k e. A , B , 0 ) -> ( F ` j ) = [_ j / k ]_ if ( k e. A , B , 0 ) ) )
94 85 87 93 sylc 
 |-  ( ( ph /\ j e. ( ZZ>= ` M ) ) -> ( F ` j ) = [_ j / k ]_ if ( k e. A , B , 0 ) )
95 fvex 
 |-  ( F ` j ) e. _V
96 94 95 eqeltrrdi 
 |-  ( ( ph /\ j e. ( ZZ>= ` M ) ) -> [_ j / k ]_ if ( k e. A , B , 0 ) e. _V )
97 nfcv 
 |-  F/_ n if ( k e. A , B , 0 )
98 nfv 
 |-  F/ k n e. A
99 nfcsb1v 
 |-  F/_ k [_ n / k ]_ B
100 nfcv 
 |-  F/_ k 0
101 98 99 100 nfif 
 |-  F/_ k if ( n e. A , [_ n / k ]_ B , 0 )
102 eleq1w 
 |-  ( k = n -> ( k e. A <-> n e. A ) )
103 csbeq1a 
 |-  ( k = n -> B = [_ n / k ]_ B )
104 102 103 ifbieq1d 
 |-  ( k = n -> if ( k e. A , B , 0 ) = if ( n e. A , [_ n / k ]_ B , 0 ) )
105 97 101 104 cbvmpt 
 |-  ( k e. ZZ |-> if ( k e. A , B , 0 ) ) = ( n e. ZZ |-> if ( n e. A , [_ n / k ]_ B , 0 ) )
106 105 eqcomi 
 |-  ( n e. ZZ |-> if ( n e. A , [_ n / k ]_ B , 0 ) ) = ( k e. ZZ |-> if ( k e. A , B , 0 ) )
107 106 fvmpts 
 |-  ( ( j e. ZZ /\ [_ j / k ]_ if ( k e. A , B , 0 ) e. _V ) -> ( ( n e. ZZ |-> if ( n e. A , [_ n / k ]_ B , 0 ) ) ` j ) = [_ j / k ]_ if ( k e. A , B , 0 ) )
108 84 96 107 syl2anc 
 |-  ( ( ph /\ j e. ( ZZ>= ` M ) ) -> ( ( n e. ZZ |-> if ( n e. A , [_ n / k ]_ B , 0 ) ) ` j ) = [_ j / k ]_ if ( k e. A , B , 0 ) )
109 108 94 eqtr4d 
 |-  ( ( ph /\ j e. ( ZZ>= ` M ) ) -> ( ( n e. ZZ |-> if ( n e. A , [_ n / k ]_ B , 0 ) ) ` j ) = ( F ` j ) )
110 2 109 seqfeq 
 |-  ( ph -> seq M ( + , ( n e. ZZ |-> if ( n e. A , [_ n / k ]_ B , 0 ) ) ) = seq M ( + , F ) )
111 110 breq1d 
 |-  ( ph -> ( seq M ( + , ( n e. ZZ |-> if ( n e. A , [_ n / k ]_ B , 0 ) ) ) ~~> x <-> seq M ( + , F ) ~~> x ) )
112 82 111 bitrd 
 |-  ( ph -> ( ( E. m e. ZZ ( A C_ ( ZZ>= ` m ) /\ seq m ( + , ( n e. ZZ |-> if ( n e. A , [_ n / k ]_ B , 0 ) ) ) ~~> x ) \/ E. m e. NN E. f ( f : ( 1 ... m ) -1-1-onto-> A /\ x = ( seq 1 ( + , ( n e. NN |-> [_ ( f ` n ) / k ]_ B ) ) ` m ) ) ) <-> seq M ( + , F ) ~~> x ) )
113 112 iotabidv 
 |-  ( ph -> ( iota x ( E. m e. ZZ ( A C_ ( ZZ>= ` m ) /\ seq m ( + , ( n e. ZZ |-> if ( n e. A , [_ n / k ]_ B , 0 ) ) ) ~~> x ) \/ E. m e. NN E. f ( f : ( 1 ... m ) -1-1-onto-> A /\ x = ( seq 1 ( + , ( n e. NN |-> [_ ( f ` n ) / k ]_ B ) ) ` m ) ) ) ) = ( iota x seq M ( + , F ) ~~> x ) )
114 df-sum 
 |-  sum_ k e. A B = ( iota x ( E. m e. ZZ ( A C_ ( ZZ>= ` m ) /\ seq m ( + , ( n e. ZZ |-> if ( n e. A , [_ n / k ]_ B , 0 ) ) ) ~~> x ) \/ E. m e. NN E. f ( f : ( 1 ... m ) -1-1-onto-> A /\ x = ( seq 1 ( + , ( n e. NN |-> [_ ( f ` n ) / k ]_ B ) ) ` m ) ) ) )
115 df-fv 
 |-  ( ~~> ` seq M ( + , F ) ) = ( iota x seq M ( + , F ) ~~> x )
116 113 114 115 3eqtr4g 
 |-  ( ph -> sum_ k e. A B = ( ~~> ` seq M ( + , F ) ) )