Metamath Proof Explorer


Theorem sge0reuzb

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

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

Proof

Step Hyp Ref Expression
1 sge0reuzb.k k φ
2 sge0reuzb.p x φ
3 sge0reuzb.m φ M
4 sge0reuzb.z Z = M
5 sge0reuzb.b φ k Z B 0 +∞
6 sge0reuzb.x φ x n Z k = M n B x
7 1 3 4 5 sge0reuz φ sum^ k Z B = sup ran n Z k = M n B * <
8 nfv n φ
9 eqid n Z k = M n B = n Z k = M n B
10 nfv k n Z
11 1 10 nfan k φ n Z
12 fzfid φ n Z M n Fin
13 elfzuz k M n k M
14 13 4 eleqtrrdi k M n k Z
15 14 adantl φ k M n k Z
16 rge0ssre 0 +∞
17 16 5 sseldi φ k Z B
18 15 17 syldan φ k M n B
19 18 adantlr φ n Z k M n B
20 11 12 19 fsumreclf φ n Z k = M n B
21 8 9 20 rnmptssd φ ran n Z k = M n B
22 uzid M M M
23 3 22 syl φ M M
24 23 4 eleqtrrdi φ M Z
25 eqidd φ k = M M B = k = M M B
26 oveq2 n = M M n = M M
27 26 sumeq1d n = M k = M n B = k = M M B
28 27 rspceeqv M Z k = M M B = k = M M B n Z k = M M B = k = M n B
29 24 25 28 syl2anc φ n Z k = M M B = k = M n B
30 sumex k = M M B V
31 30 a1i φ k = M M B V
32 9 29 31 elrnmptd φ k = M M B ran n Z k = M n B
33 32 ne0d φ ran n Z k = M n B
34 vex y V
35 9 elrnmpt y V y ran n Z k = M n B n Z y = k = M n B
36 34 35 ax-mp y ran n Z k = M n B n Z y = k = M n B
37 36 biimpi y ran n Z k = M n B n Z y = k = M n B
38 37 adantl φ x n Z k = M n B x y ran n Z k = M n B n Z y = k = M n B
39 nfv n φ x
40 nfra1 n n Z k = M n B x
41 39 40 nfan n φ x n Z k = M n B x
42 nfv n y x
43 rspa n Z k = M n B x n Z k = M n B x
44 simpr k = M n B x y = k = M n B y = k = M n B
45 simpl k = M n B x y = k = M n B k = M n B x
46 44 45 eqbrtrd k = M n B x y = k = M n B y x
47 46 ex k = M n B x y = k = M n B y x
48 43 47 syl n Z k = M n B x n Z y = k = M n B y x
49 48 ex n Z k = M n B x n Z y = k = M n B y x
50 49 adantl φ x n Z k = M n B x n Z y = k = M n B y x
51 41 42 50 rexlimd φ x n Z k = M n B x n Z y = k = M n B y x
52 51 adantr φ x n Z k = M n B x y ran n Z k = M n B n Z y = k = M n B y x
53 38 52 mpd φ x n Z k = M n B x y ran n Z k = M n B y x
54 53 ralrimiva φ x n Z k = M n B x y ran n Z k = M n B y x
55 54 ex φ x n Z k = M n B x y ran n Z k = M n B y x
56 55 ex φ x n Z k = M n B x y ran n Z k = M n B y x
57 2 56 reximdai φ x n Z k = M n B x x y ran n Z k = M n B y x
58 6 57 mpd φ x y ran n Z k = M n B y x
59 supxrre ran n Z k = M n B ran n Z k = M n B x y ran n Z k = M n B y x sup ran n Z k = M n B * < = sup ran n Z k = M n B <
60 21 33 58 59 syl3anc φ sup ran n Z k = M n B * < = sup ran n Z k = M n B <
61 7 60 eqtrd φ sum^ k Z B = sup ran n Z k = M n B <