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 = M
zsum.2 φ M
zsum.3 φ A Z
zsum.4 φ k Z F k = if k A B 0
zsum.5 φ k A B
Assertion zsum φ k A B = seq M + F

Proof

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