Metamath Proof Explorer


Theorem sge0seq

Description: A series of nonnegative reals agrees with the generalized sum of nonnegative reals. (Contributed by Glauco Siliprandi, 3-Mar-2021)

Ref Expression
Hypotheses sge0seq.m φ M
sge0seq.z Z = M
sge0seq.f φ F : Z 0 +∞
sge0seq.g G = seq M + F
Assertion sge0seq φ sum^ F = sup ran G * <

Proof

Step Hyp Ref Expression
1 sge0seq.m φ M
2 sge0seq.z Z = M
3 sge0seq.f φ F : Z 0 +∞
4 sge0seq.g G = seq M + F
5 rge0ssre 0 +∞
6 3 ffvelrnda φ k Z F k 0 +∞
7 5 6 sseldi φ k Z F k
8 readdcl k i k + i
9 8 adantl φ k i k + i
10 2 1 7 9 seqf φ seq M + F : Z
11 4 a1i φ G = seq M + F
12 11 feq1d φ G : Z seq M + F : Z
13 10 12 mpbird φ G : Z
14 13 frnd φ ran G
15 ressxr *
16 15 a1i φ *
17 14 16 sstrd φ ran G *
18 2 fvexi Z V
19 18 a1i φ Z V
20 icossicc 0 +∞ 0 +∞
21 20 a1i φ 0 +∞ 0 +∞
22 3 21 fssd φ F : Z 0 +∞
23 19 22 sge0xrcl φ sum^ F *
24 simpr φ z ran G z ran G
25 13 ffnd φ G Fn Z
26 fvelrnb G Fn Z z ran G j Z G j = z
27 25 26 syl φ z ran G j Z G j = z
28 27 adantr φ z ran G z ran G j Z G j = z
29 24 28 mpbid φ z ran G j Z G j = z
30 20 6 sseldi φ k Z F k 0 +∞
31 elfzuz k M j k M
32 31 2 eleqtrrdi k M j k Z
33 32 ssriv M j Z
34 33 a1i φ M j Z
35 19 30 34 sge0lessmpt φ sum^ k M j F k sum^ k Z F k
36 35 3ad2ant1 φ j Z G j = z sum^ k M j F k sum^ k Z F k
37 fzfid φ M j Fin
38 32 6 sylan2 φ k M j F k 0 +∞
39 37 38 sge0fsummpt φ sum^ k M j F k = k = M j F k
40 39 3ad2ant1 φ j Z G j = z sum^ k M j F k = k = M j F k
41 simpll φ j Z k M j φ
42 32 adantl φ j Z k M j k Z
43 eqidd φ k Z F k = F k
44 41 42 43 syl2anc φ j Z k M j F k = F k
45 2 eleq2i j Z j M
46 45 biimpi j Z j M
47 46 adantl φ j Z j M
48 7 recnd φ k Z F k
49 41 42 48 syl2anc φ j Z k M j F k
50 44 47 49 fsumser φ j Z k = M j F k = seq M + F j
51 50 3adant3 φ j Z G j = z k = M j F k = seq M + F j
52 40 51 eqtrd φ j Z G j = z sum^ k M j F k = seq M + F j
53 4 eqcomi seq M + F = G
54 53 fveq1i seq M + F j = G j
55 54 a1i φ j Z G j = z seq M + F j = G j
56 simp3 φ j Z G j = z G j = z
57 52 55 56 3eqtrrd φ j Z G j = z z = sum^ k M j F k
58 3 feqmptd φ F = k Z F k
59 58 fveq2d φ sum^ F = sum^ k Z F k
60 59 3ad2ant1 φ j Z G j = z sum^ F = sum^ k Z F k
61 57 60 breq12d φ j Z G j = z z sum^ F sum^ k M j F k sum^ k Z F k
62 36 61 mpbird φ j Z G j = z z sum^ F
63 62 3exp φ j Z G j = z z sum^ F
64 63 adantr φ z ran G j Z G j = z z sum^ F
65 64 rexlimdv φ z ran G j Z G j = z z sum^ F
66 29 65 mpd φ z ran G z sum^ F
67 66 ralrimiva φ z ran G z sum^ F
68 nfv k φ z z < sum^ F
69 18 a1i φ z z < sum^ F Z V
70 6 ad4ant14 φ z z < sum^ F k Z F k 0 +∞
71 simplr φ z z < sum^ F z
72 simpr φ z < sum^ F z < sum^ F
73 59 adantr φ z < sum^ F sum^ F = sum^ k Z F k
74 72 73 breqtrd φ z < sum^ F z < sum^ k Z F k
75 74 adantlr φ z z < sum^ F z < sum^ k Z F k
76 68 69 70 71 75 sge0gtfsumgt φ z z < sum^ F w 𝒫 Z Fin z < k w F k
77 1 3ad2ant1 φ w 𝒫 Z Fin z < k w F k M
78 elpwinss w 𝒫 Z Fin w Z
79 78 3ad2ant2 φ w 𝒫 Z Fin z < k w F k w Z
80 elinel2 w 𝒫 Z Fin w Fin
81 80 3ad2ant2 φ w 𝒫 Z Fin z < k w F k w Fin
82 77 2 79 81 uzfissfz φ w 𝒫 Z Fin z < k w F k j Z w M j
83 82 3adant1r φ z w 𝒫 Z Fin z < k w F k j Z w M j
84 simpl1r φ z w 𝒫 Z Fin z < k w F k w M j z
85 80 adantl φ w 𝒫 Z Fin w Fin
86 58 7 fmpt3d φ F : Z
87 86 ad2antrr φ w 𝒫 Z Fin k w F : Z
88 78 sselda w 𝒫 Z Fin k w k Z
89 88 adantll φ w 𝒫 Z Fin k w k Z
90 87 89 ffvelrnd φ w 𝒫 Z Fin k w F k
91 85 90 fsumrecl φ w 𝒫 Z Fin k w F k
92 91 ad4ant13 φ z w 𝒫 Z Fin w M j k w F k
93 92 3adantl3 φ z w 𝒫 Z Fin z < k w F k w M j k w F k
94 32 7 sylan2 φ k M j F k
95 37 94 fsumrecl φ k = M j F k
96 95 ad3antrrr φ z w 𝒫 Z Fin w M j k = M j F k
97 96 3adantl3 φ z w 𝒫 Z Fin z < k w F k w M j k = M j F k
98 simpl3 φ z w 𝒫 Z Fin z < k w F k w M j z < k w F k
99 37 adantr φ w M j M j Fin
100 94 adantlr φ w M j k M j F k
101 0xr 0 *
102 101 a1i φ k Z 0 *
103 pnfxr +∞ *
104 103 a1i φ k Z +∞ *
105 icogelb 0 * +∞ * F k 0 +∞ 0 F k
106 102 104 6 105 syl3anc φ k Z 0 F k
107 32 106 sylan2 φ k M j 0 F k
108 107 adantlr φ w M j k M j 0 F k
109 simpr φ w M j w M j
110 99 100 108 109 fsumless φ w M j k w F k k = M j F k
111 110 adantlr φ z w M j k w F k k = M j F k
112 111 3ad2antl1 φ z w 𝒫 Z Fin z < k w F k w M j k w F k k = M j F k
113 84 93 97 98 112 ltletrd φ z w 𝒫 Z Fin z < k w F k w M j z < k = M j F k
114 113 ex φ z w 𝒫 Z Fin z < k w F k w M j z < k = M j F k
115 114 reximdv φ z w 𝒫 Z Fin z < k w F k j Z w M j j Z z < k = M j F k
116 83 115 mpd φ z w 𝒫 Z Fin z < k w F k j Z z < k = M j F k
117 116 3exp φ z w 𝒫 Z Fin z < k w F k j Z z < k = M j F k
118 117 adantr φ z z < sum^ F w 𝒫 Z Fin z < k w F k j Z z < k = M j F k
119 118 rexlimdv φ z z < sum^ F w 𝒫 Z Fin z < k w F k j Z z < k = M j F k
120 76 119 mpd φ z z < sum^ F j Z z < k = M j F k
121 10 ffnd φ seq M + F Fn Z
122 121 adantr φ j Z seq M + F Fn Z
123 47 45 sylibr φ j Z j Z
124 fnfvelrn seq M + F Fn Z j Z seq M + F j ran seq M + F
125 122 123 124 syl2anc φ j Z seq M + F j ran seq M + F
126 4 a1i φ j Z G = seq M + F
127 126 rneqd φ j Z ran G = ran seq M + F
128 50 127 eleq12d φ j Z k = M j F k ran G seq M + F j ran seq M + F
129 125 128 mpbird φ j Z k = M j F k ran G
130 129 adantlr φ z j Z k = M j F k ran G
131 130 3adant3 φ z j Z z < k = M j F k k = M j F k ran G
132 simp3 φ z j Z z < k = M j F k z < k = M j F k
133 breq2 y = k = M j F k z < y z < k = M j F k
134 133 rspcev k = M j F k ran G z < k = M j F k y ran G z < y
135 131 132 134 syl2anc φ z j Z z < k = M j F k y ran G z < y
136 135 3exp φ z j Z z < k = M j F k y ran G z < y
137 136 rexlimdv φ z j Z z < k = M j F k y ran G z < y
138 137 adantr φ z z < sum^ F j Z z < k = M j F k y ran G z < y
139 120 138 mpd φ z z < sum^ F y ran G z < y
140 139 ex φ z z < sum^ F y ran G z < y
141 140 ralrimiva φ z z < sum^ F y ran G z < y
142 supxr2 ran G * sum^ F * z ran G z sum^ F z z < sum^ F y ran G z < y sup ran G * < = sum^ F
143 17 23 67 141 142 syl22anc φ sup ran G * < = sum^ F
144 143 eqcomd φ sum^ F = sup ran G * <