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 sselid 
 |-  ( ( ( 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 sselid 
 |-  ( ( 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 bilani 
 |-  ( ( 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 )
49 2 3ad2ant1 
 |-  ( ( ph /\ x e. ( ~P Z i^i Fin ) /\ y = sum_ k e. x B ) -> M e. ZZ )
50 17 3ad2ant2 
 |-  ( ( ph /\ x e. ( ~P Z i^i Fin ) /\ y = sum_ k e. x B ) -> x C_ Z )
51 14 3adant3 
 |-  ( ( ph /\ x e. ( ~P Z i^i Fin ) /\ y = sum_ k e. x B ) -> x e. Fin )
52 49 3 50 51 uzfissfz 
 |-  ( ( ph /\ x e. ( ~P Z i^i Fin ) /\ y = sum_ k e. x B ) -> E. n e. Z x C_ ( M ... n ) )
53 nfv 
 |-  F/ n ( ph /\ x e. ( ~P Z i^i Fin ) /\ y = sum_ k e. x B )
54 nfmpt1 
 |-  F/_ n ( n e. Z |-> sum_ k e. ( M ... n ) B )
55 54 nfrn 
 |-  F/_ n ran ( n e. Z |-> sum_ k e. ( M ... n ) B )
56 nfv 
 |-  F/ n y <_ w
57 55 56 nfrexw 
 |-  F/ n E. w e. ran ( n e. Z |-> sum_ k e. ( M ... n ) B ) y <_ w
58 id 
 |-  ( n e. Z -> n e. Z )
59 sumex 
 |-  sum_ k e. ( M ... n ) B e. _V
60 59 a1i 
 |-  ( n e. Z -> sum_ k e. ( M ... n ) B e. _V )
61 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 ) )
62 58 60 61 syl2anc 
 |-  ( n e. Z -> sum_ k e. ( M ... n ) B e. ran ( n e. Z |-> sum_ k e. ( M ... n ) B ) )
63 62 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 ) )
64 simplr 
 |-  ( ( ( ph /\ y = sum_ k e. x B ) /\ x C_ ( M ... n ) ) -> y = sum_ k e. x B )
65 nfcv 
 |-  F/_ k y
66 nfcv 
 |-  F/_ k x
67 66 nfsum1 
 |-  F/_ k sum_ k e. x B
68 65 67 nfeq 
 |-  F/ k y = sum_ k e. x B
69 1 68 nfan 
 |-  F/ k ( ph /\ y = sum_ k e. x B )
70 nfv 
 |-  F/ k x C_ ( M ... n )
71 69 70 nfan 
 |-  F/ k ( ( ph /\ y = sum_ k e. x B ) /\ x C_ ( M ... n ) )
72 fzfid 
 |-  ( ( ( ph /\ y = sum_ k e. x B ) /\ x C_ ( M ... n ) ) -> ( M ... n ) e. Fin )
73 38 ad4ant14 
 |-  ( ( ( ( ph /\ y = sum_ k e. x B ) /\ x C_ ( M ... n ) ) /\ k e. ( M ... n ) ) -> B e. RR )
74 simplll 
 |-  ( ( ( ( ph /\ y = sum_ k e. x B ) /\ x C_ ( M ... n ) ) /\ k e. ( M ... n ) ) -> ph )
75 35 adantl 
 |-  ( ( ( ( ph /\ y = sum_ k e. x B ) /\ x C_ ( M ... n ) ) /\ k e. ( M ... n ) ) -> k e. Z )
76 0xr 
 |-  0 e. RR*
77 76 a1i 
 |-  ( ( ph /\ k e. Z ) -> 0 e. RR* )
78 pnfxr 
 |-  +oo e. RR*
79 78 a1i 
 |-  ( ( ph /\ k e. Z ) -> +oo e. RR* )
80 icogelb 
 |-  ( ( 0 e. RR* /\ +oo e. RR* /\ B e. ( 0 [,) +oo ) ) -> 0 <_ B )
81 77 79 4 80 syl3anc 
 |-  ( ( ph /\ k e. Z ) -> 0 <_ B )
82 74 75 81 syl2anc 
 |-  ( ( ( ( ph /\ y = sum_ k e. x B ) /\ x C_ ( M ... n ) ) /\ k e. ( M ... n ) ) -> 0 <_ B )
83 simpr 
 |-  ( ( ( ph /\ y = sum_ k e. x B ) /\ x C_ ( M ... n ) ) -> x C_ ( M ... n ) )
84 71 72 73 82 83 fsumlessf 
 |-  ( ( ( ph /\ y = sum_ k e. x B ) /\ x C_ ( M ... n ) ) -> sum_ k e. x B <_ sum_ k e. ( M ... n ) B )
85 64 84 eqbrtrd 
 |-  ( ( ( ph /\ y = sum_ k e. x B ) /\ x C_ ( M ... n ) ) -> y <_ sum_ k e. ( M ... n ) B )
86 85 3adant2 
 |-  ( ( ( ph /\ y = sum_ k e. x B ) /\ n e. Z /\ x C_ ( M ... n ) ) -> y <_ sum_ k e. ( M ... n ) B )
87 breq2 
 |-  ( w = sum_ k e. ( M ... n ) B -> ( y <_ w <-> y <_ sum_ k e. ( M ... n ) B ) )
88 87 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 )
89 63 86 88 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 )
90 89 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 ) ) )
91 90 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 ) ) )
92 53 57 91 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 ) )
93 52 92 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 )
94 93 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 ) ) )
95 94 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 ) )
96 95 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 )
97 48 96 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 )
98 26 42 97 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* , < ) )
99 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 ) )
100 45 99 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 )
101 100 bilani 
 |-  ( ( ph /\ y e. ran ( n e. Z |-> sum_ k e. ( M ... n ) B ) ) -> E. n e. Z y = sum_ k e. ( M ... n ) B )
102 35 ssriv 
 |-  ( M ... n ) C_ Z
103 ovex 
 |-  ( M ... n ) e. _V
104 103 elpw 
 |-  ( ( M ... n ) e. ~P Z <-> ( M ... n ) C_ Z )
105 102 104 mpbir 
 |-  ( M ... n ) e. ~P Z
106 fzfi 
 |-  ( M ... n ) e. Fin
107 105 106 elini 
 |-  ( M ... n ) e. ( ~P Z i^i Fin )
108 107 a1i 
 |-  ( y = sum_ k e. ( M ... n ) B -> ( M ... n ) e. ( ~P Z i^i Fin ) )
109 id 
 |-  ( y = sum_ k e. ( M ... n ) B -> y = sum_ k e. ( M ... n ) B )
110 sumeq1 
 |-  ( x = ( M ... n ) -> sum_ k e. x B = sum_ k e. ( M ... n ) B )
111 110 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 )
112 108 109 111 syl2anc 
 |-  ( y = sum_ k e. ( M ... n ) B -> E. x e. ( ~P Z i^i Fin ) y = sum_ k e. x B )
113 45 a1i 
 |-  ( y = sum_ k e. ( M ... n ) B -> y e. _V )
114 10 112 113 elrnmptd 
 |-  ( y = sum_ k e. ( M ... n ) B -> y e. ran ( x e. ( ~P Z i^i Fin ) |-> sum_ k e. x B ) )
115 114 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 ) ) ) )
116 115 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 ) ) )
117 116 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 ) ) )
118 101 117 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 ) )
119 118 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 ) )
120 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 ) )
121 119 120 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 ) )
122 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* , < ) )
123 121 26 122 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* , < ) )
124 28 44 98 123 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* , < ) )
125 8 124 eqtrd 
 |-  ( ph -> ( sum^ ` ( k e. Z |-> B ) ) = sup ( ran ( n e. Z |-> sum_ k e. ( M ... n ) B ) , RR* , < ) )