Metamath Proof Explorer


Theorem sge0reuz

Description: Value of the generalized sum of nonnegative reals, when the domain is a set of upper integers. (Contributed by Glauco Siliprandi, 8-Apr-2021)

Ref Expression
Hypotheses sge0reuz.k k φ
sge0reuz.m φ M
sge0reuz.z Z = M
sge0reuz.b φ k Z B 0 +∞
Assertion sge0reuz φ sum^ k Z B = sup ran n Z k = M n B * <

Proof

Step Hyp Ref Expression
1 sge0reuz.k k φ
2 sge0reuz.m φ M
3 sge0reuz.z Z = M
4 sge0reuz.b φ k Z B 0 +∞
5 3 a1i φ Z = M
6 fvex M V
7 5 6 eqeltrdi φ Z V
8 1 7 4 sge0revalmpt φ sum^ k Z B = sup ran x 𝒫 Z Fin k x B * <
9 nfv x φ
10 eqid x 𝒫 Z Fin k x B = x 𝒫 Z Fin k x B
11 nfv k x 𝒫 Z Fin
12 1 11 nfan k φ x 𝒫 Z Fin
13 elinel2 x 𝒫 Z Fin x Fin
14 13 adantl φ x 𝒫 Z Fin x Fin
15 rge0ssre 0 +∞
16 simpll φ x 𝒫 Z Fin k x φ
17 elpwinss x 𝒫 Z Fin x Z
18 17 adantr x 𝒫 Z Fin k x x Z
19 simpr x 𝒫 Z Fin k x k x
20 18 19 sseldd x 𝒫 Z Fin k x k Z
21 20 adantll φ x 𝒫 Z Fin k x k Z
22 16 21 4 syl2anc φ x 𝒫 Z Fin k x B 0 +∞
23 15 22 sseldi φ x 𝒫 Z Fin k x B
24 12 14 23 fsumreclf φ x 𝒫 Z Fin k x B
25 24 rexrd φ x 𝒫 Z Fin k x B *
26 9 10 25 rnmptssd φ ran x 𝒫 Z Fin k x B *
27 supxrcl ran x 𝒫 Z Fin k x B * sup ran x 𝒫 Z Fin k x B * < *
28 26 27 syl φ sup ran x 𝒫 Z Fin k x B * < *
29 nfv n φ
30 eqid n Z k = M n B = n Z k = M n B
31 nfv k n Z
32 1 31 nfan k φ n Z
33 fzfid φ n Z M n Fin
34 elfzuz k M n k M
35 34 3 eleqtrrdi k M n k Z
36 35 adantl φ k M n k Z
37 15 4 sseldi φ k Z B
38 36 37 syldan φ k M n B
39 38 adantlr φ n Z k M n B
40 32 33 39 fsumreclf φ n Z k = M n B
41 40 rexrd φ n Z k = M n B *
42 29 30 41 rnmptssd φ ran n Z k = M n B *
43 supxrcl ran n Z k = M n B * sup ran n Z k = M n B * < *
44 42 43 syl φ sup ran n Z k = M n B * < *
45 vex y V
46 10 elrnmpt y V y ran x 𝒫 Z Fin k x B x 𝒫 Z Fin y = k x B
47 45 46 ax-mp y ran x 𝒫 Z Fin k x B x 𝒫 Z Fin y = k x B
48 47 biimpi y ran x 𝒫 Z Fin k x B x 𝒫 Z Fin y = k x B
49 48 adantl φ y ran x 𝒫 Z Fin k x B x 𝒫 Z Fin y = k x B
50 2 3ad2ant1 φ x 𝒫 Z Fin y = k x B M
51 17 3ad2ant2 φ x 𝒫 Z Fin y = k x B x Z
52 14 3adant3 φ x 𝒫 Z Fin y = k x B x Fin
53 50 3 51 52 uzfissfz φ x 𝒫 Z Fin y = k x B n Z x M n
54 nfv n φ x 𝒫 Z Fin y = k x B
55 nfmpt1 _ n n Z k = M n B
56 55 nfrn _ n ran n Z k = M n B
57 nfv n y w
58 56 57 nfrex n w ran n Z k = M n B y w
59 id n Z n Z
60 sumex k = M n B V
61 60 a1i n Z k = M n B V
62 30 elrnmpt1 n Z k = M n B V k = M n B ran n Z k = M n B
63 59 61 62 syl2anc n Z k = M n B ran n Z k = M n B
64 63 3ad2ant2 φ y = k x B n Z x M n k = M n B ran n Z k = M n B
65 simplr φ y = k x B x M n y = k x B
66 nfcv _ k y
67 nfcv _ k x
68 67 nfsum1 _ k k x B
69 66 68 nfeq k y = k x B
70 1 69 nfan k φ y = k x B
71 nfv k x M n
72 70 71 nfan k φ y = k x B x M n
73 fzfid φ y = k x B x M n M n Fin
74 38 ad4ant14 φ y = k x B x M n k M n B
75 simplll φ y = k x B x M n k M n φ
76 35 adantl φ y = k x B x M n k M n k Z
77 0xr 0 *
78 77 a1i φ k Z 0 *
79 pnfxr +∞ *
80 79 a1i φ k Z +∞ *
81 icogelb 0 * +∞ * B 0 +∞ 0 B
82 78 80 4 81 syl3anc φ k Z 0 B
83 75 76 82 syl2anc φ y = k x B x M n k M n 0 B
84 simpr φ y = k x B x M n x M n
85 72 73 74 83 84 fsumlessf φ y = k x B x M n k x B k = M n B
86 65 85 eqbrtrd φ y = k x B x M n y k = M n B
87 86 3adant2 φ y = k x B n Z x M n y k = M n B
88 breq2 w = k = M n B y w y k = M n B
89 88 rspcev k = M n B ran n Z k = M n B y k = M n B w ran n Z k = M n B y w
90 64 87 89 syl2anc φ y = k x B n Z x M n w ran n Z k = M n B y w
91 90 3exp φ y = k x B n Z x M n w ran n Z k = M n B y w
92 91 3adant2 φ x 𝒫 Z Fin y = k x B n Z x M n w ran n Z k = M n B y w
93 54 58 92 rexlimd φ x 𝒫 Z Fin y = k x B n Z x M n w ran n Z k = M n B y w
94 53 93 mpd φ x 𝒫 Z Fin y = k x B w ran n Z k = M n B y w
95 94 3exp φ x 𝒫 Z Fin y = k x B w ran n Z k = M n B y w
96 95 rexlimdv φ x 𝒫 Z Fin y = k x B w ran n Z k = M n B y w
97 96 imp φ x 𝒫 Z Fin y = k x B w ran n Z k = M n B y w
98 49 97 syldan φ y ran x 𝒫 Z Fin k x B w ran n Z k = M n B y w
99 26 42 98 suplesup2 φ sup ran x 𝒫 Z Fin k x B * < sup ran n Z k = M n B * <
100 30 elrnmpt y V y ran n Z k = M n B n Z y = k = M n B
101 45 100 ax-mp y ran n Z k = M n B n Z y = k = M n B
102 101 biimpi y ran n Z k = M n B n Z y = k = M n B
103 102 adantl φ y ran n Z k = M n B n Z y = k = M n B
104 35 ssriv M n Z
105 ovex M n V
106 105 elpw M n 𝒫 Z M n Z
107 104 106 mpbir M n 𝒫 Z
108 fzfi M n Fin
109 107 108 elini M n 𝒫 Z Fin
110 109 a1i y = k = M n B M n 𝒫 Z Fin
111 id y = k = M n B y = k = M n B
112 sumeq1 x = M n k x B = k = M n B
113 112 rspceeqv M n 𝒫 Z Fin y = k = M n B x 𝒫 Z Fin y = k x B
114 110 111 113 syl2anc y = k = M n B x 𝒫 Z Fin y = k x B
115 45 a1i y = k = M n B y V
116 10 114 115 elrnmptd y = k = M n B y ran x 𝒫 Z Fin k x B
117 116 2a1i φ n Z y = k = M n B y ran x 𝒫 Z Fin k x B
118 117 rexlimdv φ n Z y = k = M n B y ran x 𝒫 Z Fin k x B
119 118 adantr φ y ran n Z k = M n B n Z y = k = M n B y ran x 𝒫 Z Fin k x B
120 103 119 mpd φ y ran n Z k = M n B y ran x 𝒫 Z Fin k x B
121 120 ralrimiva φ y ran n Z k = M n B y ran x 𝒫 Z Fin k x B
122 dfss3 ran n Z k = M n B ran x 𝒫 Z Fin k x B y ran n Z k = M n B y ran x 𝒫 Z Fin k x B
123 121 122 sylibr φ ran n Z k = M n B ran x 𝒫 Z Fin k x B
124 supxrss ran n Z k = M n B ran x 𝒫 Z Fin k x B ran x 𝒫 Z Fin k x B * sup ran n Z k = M n B * < sup ran x 𝒫 Z Fin k x B * <
125 123 26 124 syl2anc φ sup ran n Z k = M n B * < sup ran x 𝒫 Z Fin k x B * <
126 28 44 99 125 xrletrid φ sup ran x 𝒫 Z Fin k x B * < = sup ran n Z k = M n B * <
127 8 126 eqtrd φ sum^ k Z B = sup ran n Z k = M n B * <