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 ffvelcdmda 
 |-  ( ( ph /\ k e. Z ) -> ( F ` k ) e. ( 0 [,) +oo ) )
7 5 6 sselid 
 |-  ( ( 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 sselid 
 |-  ( ( 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 bilani 
 |-  ( ( ph /\ j e. Z ) -> j e. ( ZZ>= ` M ) )
47 7 recnd 
 |-  ( ( ph /\ k e. Z ) -> ( F ` k ) e. CC )
48 41 42 47 syl2anc 
 |-  ( ( ( ph /\ j e. Z ) /\ k e. ( M ... j ) ) -> ( F ` k ) e. CC )
49 44 46 48 fsumser 
 |-  ( ( ph /\ j e. Z ) -> sum_ k e. ( M ... j ) ( F ` k ) = ( seq M ( + , F ) ` j ) )
50 49 3adant3 
 |-  ( ( ph /\ j e. Z /\ ( G ` j ) = z ) -> sum_ k e. ( M ... j ) ( F ` k ) = ( seq M ( + , F ) ` j ) )
51 40 50 eqtrd 
 |-  ( ( ph /\ j e. Z /\ ( G ` j ) = z ) -> ( sum^ ` ( k e. ( M ... j ) |-> ( F ` k ) ) ) = ( seq M ( + , F ) ` j ) )
52 4 eqcomi 
 |-  seq M ( + , F ) = G
53 52 fveq1i 
 |-  ( seq M ( + , F ) ` j ) = ( G ` j )
54 53 a1i 
 |-  ( ( ph /\ j e. Z /\ ( G ` j ) = z ) -> ( seq M ( + , F ) ` j ) = ( G ` j ) )
55 simp3 
 |-  ( ( ph /\ j e. Z /\ ( G ` j ) = z ) -> ( G ` j ) = z )
56 51 54 55 3eqtrrd 
 |-  ( ( ph /\ j e. Z /\ ( G ` j ) = z ) -> z = ( sum^ ` ( k e. ( M ... j ) |-> ( F ` k ) ) ) )
57 3 feqmptd 
 |-  ( ph -> F = ( k e. Z |-> ( F ` k ) ) )
58 57 fveq2d 
 |-  ( ph -> ( sum^ ` F ) = ( sum^ ` ( k e. Z |-> ( F ` k ) ) ) )
59 58 3ad2ant1 
 |-  ( ( ph /\ j e. Z /\ ( G ` j ) = z ) -> ( sum^ ` F ) = ( sum^ ` ( k e. Z |-> ( F ` k ) ) ) )
60 56 59 breq12d 
 |-  ( ( ph /\ j e. Z /\ ( G ` j ) = z ) -> ( z <_ ( sum^ ` F ) <-> ( sum^ ` ( k e. ( M ... j ) |-> ( F ` k ) ) ) <_ ( sum^ ` ( k e. Z |-> ( F ` k ) ) ) ) )
61 36 60 mpbird 
 |-  ( ( ph /\ j e. Z /\ ( G ` j ) = z ) -> z <_ ( sum^ ` F ) )
62 61 3exp 
 |-  ( ph -> ( j e. Z -> ( ( G ` j ) = z -> z <_ ( sum^ ` F ) ) ) )
63 62 adantr 
 |-  ( ( ph /\ z e. ran G ) -> ( j e. Z -> ( ( G ` j ) = z -> z <_ ( sum^ ` F ) ) ) )
64 63 rexlimdv 
 |-  ( ( ph /\ z e. ran G ) -> ( E. j e. Z ( G ` j ) = z -> z <_ ( sum^ ` F ) ) )
65 29 64 mpd 
 |-  ( ( ph /\ z e. ran G ) -> z <_ ( sum^ ` F ) )
66 65 ralrimiva 
 |-  ( ph -> A. z e. ran G z <_ ( sum^ ` F ) )
67 nfv 
 |-  F/ k ( ( ph /\ z e. RR ) /\ z < ( sum^ ` F ) )
68 18 a1i 
 |-  ( ( ( ph /\ z e. RR ) /\ z < ( sum^ ` F ) ) -> Z e. _V )
69 6 ad4ant14 
 |-  ( ( ( ( ph /\ z e. RR ) /\ z < ( sum^ ` F ) ) /\ k e. Z ) -> ( F ` k ) e. ( 0 [,) +oo ) )
70 simplr 
 |-  ( ( ( ph /\ z e. RR ) /\ z < ( sum^ ` F ) ) -> z e. RR )
71 simpr 
 |-  ( ( ph /\ z < ( sum^ ` F ) ) -> z < ( sum^ ` F ) )
72 58 adantr 
 |-  ( ( ph /\ z < ( sum^ ` F ) ) -> ( sum^ ` F ) = ( sum^ ` ( k e. Z |-> ( F ` k ) ) ) )
73 71 72 breqtrd 
 |-  ( ( ph /\ z < ( sum^ ` F ) ) -> z < ( sum^ ` ( k e. Z |-> ( F ` k ) ) ) )
74 73 adantlr 
 |-  ( ( ( ph /\ z e. RR ) /\ z < ( sum^ ` F ) ) -> z < ( sum^ ` ( k e. Z |-> ( F ` k ) ) ) )
75 67 68 69 70 74 sge0gtfsumgt 
 |-  ( ( ( ph /\ z e. RR ) /\ z < ( sum^ ` F ) ) -> E. w e. ( ~P Z i^i Fin ) z < sum_ k e. w ( F ` k ) )
76 1 3ad2ant1 
 |-  ( ( ph /\ w e. ( ~P Z i^i Fin ) /\ z < sum_ k e. w ( F ` k ) ) -> M e. ZZ )
77 elpwinss 
 |-  ( w e. ( ~P Z i^i Fin ) -> w C_ Z )
78 77 3ad2ant2 
 |-  ( ( ph /\ w e. ( ~P Z i^i Fin ) /\ z < sum_ k e. w ( F ` k ) ) -> w C_ Z )
79 elinel2 
 |-  ( w e. ( ~P Z i^i Fin ) -> w e. Fin )
80 79 3ad2ant2 
 |-  ( ( ph /\ w e. ( ~P Z i^i Fin ) /\ z < sum_ k e. w ( F ` k ) ) -> w e. Fin )
81 76 2 78 80 uzfissfz 
 |-  ( ( ph /\ w e. ( ~P Z i^i Fin ) /\ z < sum_ k e. w ( F ` k ) ) -> E. j e. Z w C_ ( M ... j ) )
82 81 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 ) )
83 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 )
84 79 adantl 
 |-  ( ( ph /\ w e. ( ~P Z i^i Fin ) ) -> w e. Fin )
85 57 7 fmpt3d 
 |-  ( ph -> F : Z --> RR )
86 85 ad2antrr 
 |-  ( ( ( ph /\ w e. ( ~P Z i^i Fin ) ) /\ k e. w ) -> F : Z --> RR )
87 77 sselda 
 |-  ( ( w e. ( ~P Z i^i Fin ) /\ k e. w ) -> k e. Z )
88 87 adantll 
 |-  ( ( ( ph /\ w e. ( ~P Z i^i Fin ) ) /\ k e. w ) -> k e. Z )
89 86 88 ffvelcdmd 
 |-  ( ( ( ph /\ w e. ( ~P Z i^i Fin ) ) /\ k e. w ) -> ( F ` k ) e. RR )
90 84 89 fsumrecl 
 |-  ( ( ph /\ w e. ( ~P Z i^i Fin ) ) -> sum_ k e. w ( F ` k ) e. RR )
91 90 ad4ant13 
 |-  ( ( ( ( ph /\ z e. RR ) /\ w e. ( ~P Z i^i Fin ) ) /\ w C_ ( M ... j ) ) -> sum_ k e. w ( F ` k ) e. RR )
92 91 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 )
93 32 7 sylan2 
 |-  ( ( ph /\ k e. ( M ... j ) ) -> ( F ` k ) e. RR )
94 37 93 fsumrecl 
 |-  ( ph -> sum_ k e. ( M ... j ) ( F ` k ) e. RR )
95 94 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 )
96 95 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 )
97 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 ) )
98 37 adantr 
 |-  ( ( ph /\ w C_ ( M ... j ) ) -> ( M ... j ) e. Fin )
99 93 adantlr 
 |-  ( ( ( ph /\ w C_ ( M ... j ) ) /\ k e. ( M ... j ) ) -> ( F ` k ) e. RR )
100 0xr 
 |-  0 e. RR*
101 100 a1i 
 |-  ( ( ph /\ k e. Z ) -> 0 e. RR* )
102 pnfxr 
 |-  +oo e. RR*
103 102 a1i 
 |-  ( ( ph /\ k e. Z ) -> +oo e. RR* )
104 icogelb 
 |-  ( ( 0 e. RR* /\ +oo e. RR* /\ ( F ` k ) e. ( 0 [,) +oo ) ) -> 0 <_ ( F ` k ) )
105 101 103 6 104 syl3anc 
 |-  ( ( ph /\ k e. Z ) -> 0 <_ ( F ` k ) )
106 32 105 sylan2 
 |-  ( ( ph /\ k e. ( M ... j ) ) -> 0 <_ ( F ` k ) )
107 106 adantlr 
 |-  ( ( ( ph /\ w C_ ( M ... j ) ) /\ k e. ( M ... j ) ) -> 0 <_ ( F ` k ) )
108 simpr 
 |-  ( ( ph /\ w C_ ( M ... j ) ) -> w C_ ( M ... j ) )
109 98 99 107 108 fsumless 
 |-  ( ( ph /\ w C_ ( M ... j ) ) -> sum_ k e. w ( F ` k ) <_ sum_ k e. ( M ... j ) ( F ` k ) )
110 109 adantlr 
 |-  ( ( ( ph /\ z e. RR ) /\ w C_ ( M ... j ) ) -> sum_ k e. w ( F ` k ) <_ sum_ k e. ( M ... j ) ( F ` k ) )
111 110 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 ) )
112 83 92 96 97 111 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 ) )
113 112 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 ) ) )
114 113 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 ) ) )
115 82 114 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 ) )
116 115 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 ) ) ) )
117 116 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 ) ) ) )
118 117 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 ) ) )
119 75 118 mpd 
 |-  ( ( ( ph /\ z e. RR ) /\ z < ( sum^ ` F ) ) -> E. j e. Z z < sum_ k e. ( M ... j ) ( F ` k ) )
120 10 ffnd 
 |-  ( ph -> seq M ( + , F ) Fn Z )
121 120 adantr 
 |-  ( ( ph /\ j e. Z ) -> seq M ( + , F ) Fn Z )
122 46 45 sylibr 
 |-  ( ( ph /\ j e. Z ) -> j e. Z )
123 fnfvelrn 
 |-  ( ( seq M ( + , F ) Fn Z /\ j e. Z ) -> ( seq M ( + , F ) ` j ) e. ran seq M ( + , F ) )
124 121 122 123 syl2anc 
 |-  ( ( ph /\ j e. Z ) -> ( seq M ( + , F ) ` j ) e. ran seq M ( + , F ) )
125 4 a1i 
 |-  ( ( ph /\ j e. Z ) -> G = seq M ( + , F ) )
126 125 rneqd 
 |-  ( ( ph /\ j e. Z ) -> ran G = ran seq M ( + , F ) )
127 49 126 eleq12d 
 |-  ( ( ph /\ j e. Z ) -> ( sum_ k e. ( M ... j ) ( F ` k ) e. ran G <-> ( seq M ( + , F ) ` j ) e. ran seq M ( + , F ) ) )
128 124 127 mpbird 
 |-  ( ( ph /\ j e. Z ) -> sum_ k e. ( M ... j ) ( F ` k ) e. ran G )
129 128 adantlr 
 |-  ( ( ( ph /\ z e. RR ) /\ j e. Z ) -> sum_ k e. ( M ... j ) ( F ` k ) e. ran G )
130 129 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 )
131 simp3 
 |-  ( ( ( ph /\ z e. RR ) /\ j e. Z /\ z < sum_ k e. ( M ... j ) ( F ` k ) ) -> z < sum_ k e. ( M ... j ) ( F ` k ) )
132 breq2 
 |-  ( y = sum_ k e. ( M ... j ) ( F ` k ) -> ( z < y <-> z < sum_ k e. ( M ... j ) ( F ` k ) ) )
133 132 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 )
134 130 131 133 syl2anc 
 |-  ( ( ( ph /\ z e. RR ) /\ j e. Z /\ z < sum_ k e. ( M ... j ) ( F ` k ) ) -> E. y e. ran G z < y )
135 134 3exp 
 |-  ( ( ph /\ z e. RR ) -> ( j e. Z -> ( z < sum_ k e. ( M ... j ) ( F ` k ) -> E. y e. ran G z < y ) ) )
136 135 rexlimdv 
 |-  ( ( ph /\ z e. RR ) -> ( E. j e. Z z < sum_ k e. ( M ... j ) ( F ` k ) -> E. y e. ran G z < y ) )
137 136 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 ) )
138 119 137 mpd 
 |-  ( ( ( ph /\ z e. RR ) /\ z < ( sum^ ` F ) ) -> E. y e. ran G z < y )
139 138 ex 
 |-  ( ( ph /\ z e. RR ) -> ( z < ( sum^ ` F ) -> E. y e. ran G z < y ) )
140 139 ralrimiva 
 |-  ( ph -> A. z e. RR ( z < ( sum^ ` F ) -> E. y e. ran G z < y ) )
141 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 ) )
142 17 23 66 140 141 syl22anc 
 |-  ( ph -> sup ( ran G , RR* , < ) = ( sum^ ` F ) )
143 142 eqcomd 
 |-  ( ph -> ( sum^ ` F ) = sup ( ran G , RR* , < ) )