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 
|- ( ph -> M e. ZZ )
sge0seq.z 
|- Z = ( ZZ>= ` M )
sge0seq.f 
|- ( ph -> F : Z --> ( 0 [,) +oo ) )
sge0seq.g 
|- G = seq M ( + , F )
Assertion sge0seq 
|- ( ph -> ( sum^ ` F ) = sup ( ran G , RR* , < ) )

Proof

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