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 
|- F/ k ph
sge0reuz.m 
|- ( ph -> M e. ZZ )
sge0reuz.z 
|- Z = ( ZZ>= ` M )
sge0reuz.b 
|- ( ( ph /\ k e. Z ) -> B e. ( 0 [,) +oo ) )
Assertion sge0reuz 
|- ( ph -> ( sum^ ` ( k e. Z |-> B ) ) = sup ( ran ( n e. Z |-> sum_ k e. ( M ... n ) B ) , RR* , < ) )

Proof

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