Theorem sge0reuzb

Description: Value of the generalized sum of uniformly bounded nonnegative reals, when the domain is a set of upper integers. (Contributed by Glauco Siliprandi, 8-Apr-2021)

	Ref	Expression
Hypotheses	sge0reuzb.k	|- F/ k ph
	sge0reuzb.p	|- F/ x ph
	sge0reuzb.m	|- ( ph -> M e. ZZ )
	sge0reuzb.z	|- Z = ( ZZ>= ` M )
	sge0reuzb.b	|- ( ( ph /\ k e. Z ) -> B e. ( 0 [,) +oo ) )
	sge0reuzb.x	|- ( ph -> E. x e. RR A. n e. Z sum_ k e. ( M ... n ) B <_ x )
Assertion	sge0reuzb	|- ( ph -> ( sum^ ` ( k e. Z |-> B ) ) = sup ( ran ( n e. Z |-> sum_ k e. ( M ... n ) B ) , RR , < ) )

Proof

Step	Hyp	Ref	Expression
1		sge0reuzb.k	|- F/ k ph
2		sge0reuzb.p	|- F/ x ph
3		sge0reuzb.m	|- ( ph -> M e. ZZ )
4		sge0reuzb.z	|- Z = ( ZZ>= ` M )
5		sge0reuzb.b	|- ( ( ph /\ k e. Z ) -> B e. ( 0 [,) +oo ) )
6		sge0reuzb.x	|- ( ph -> E. x e. RR A. n e. Z sum_ k e. ( M ... n ) B <_ x )
7	1 3 4 5	sge0reuz	|- ( ph -> ( sum^ ` ( k e. Z |-> B ) ) = sup ( ran ( n e. Z |-> sum_ k e. ( M ... n ) B ) , RR* , < ) )
8		nfv	|- F/ n ph
9		eqid	|- ( n e. Z |-> sum_ k e. ( M ... n ) B ) = ( n e. Z |-> sum_ k e. ( M ... n ) B )
10		nfv	|- F/ k n e. Z
11	1 10	nfan	|- F/ k ( ph /\ n e. Z )
12		fzfid	|- ( ( ph /\ n e. Z ) -> ( M ... n ) e. Fin )
13		elfzuz	|- ( k e. ( M ... n ) -> k e. ( ZZ>= ` M ) )
14	13 4	eleqtrrdi	|- ( k e. ( M ... n ) -> k e. Z )
15	14	adantl	|- ( ( ph /\ k e. ( M ... n ) ) -> k e. Z )
16		rge0ssre	|- ( 0 [,) +oo ) C_ RR
17	16 5	sselid	|- ( ( ph /\ k e. Z ) -> B e. RR )
18	15 17	syldan	|- ( ( ph /\ k e. ( M ... n ) ) -> B e. RR )
19	18	adantlr	|- ( ( ( ph /\ n e. Z ) /\ k e. ( M ... n ) ) -> B e. RR )
20	11 12 19	fsumreclf	|- ( ( ph /\ n e. Z ) -> sum_ k e. ( M ... n ) B e. RR )
21	8 9 20	rnmptssd	|- ( ph -> ran ( n e. Z |-> sum_ k e. ( M ... n ) B ) C_ RR )
22		uzid	|- ( M e. ZZ -> M e. ( ZZ>= ` M ) )
23	3 22	syl	|- ( ph -> M e. ( ZZ>= ` M ) )
24	23 4	eleqtrrdi	|- ( ph -> M e. Z )
25		eqidd	|- ( ph -> sum_ k e. ( M ... M ) B = sum_ k e. ( M ... M ) B )
26		oveq2	|- ( n = M -> ( M ... n ) = ( M ... M ) )
27	26	sumeq1d	|- ( n = M -> sum_ k e. ( M ... n ) B = sum_ k e. ( M ... M ) B )
28	27	rspceeqv	|- ( ( M e. Z /\ sum_ k e. ( M ... M ) B = sum_ k e. ( M ... M ) B ) -> E. n e. Z sum_ k e. ( M ... M ) B = sum_ k e. ( M ... n ) B )
29	24 25 28	syl2anc	|- ( ph -> E. n e. Z sum_ k e. ( M ... M ) B = sum_ k e. ( M ... n ) B )
30		sumex	|- sum_ k e. ( M ... M ) B e. _V
31	30	a1i	|- ( ph -> sum_ k e. ( M ... M ) B e. _V )
32	9 29 31	elrnmptd	|- ( ph -> sum_ k e. ( M ... M ) B e. ran ( n e. Z |-> sum_ k e. ( M ... n ) B ) )
33	32	ne0d	|- ( ph -> ran ( n e. Z |-> sum_ k e. ( M ... n ) B ) =/= (/) )
34		vex	|- y e. _V
35	9	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 ) )
36	34 35	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 )
37	36	biimpi	|- ( y e. ran ( n e. Z |-> sum_ k e. ( M ... n ) B ) -> E. n e. Z y = sum_ k e. ( M ... n ) B )
38	37	adantl	|- ( ( ( ( ph /\ x e. RR ) /\ A. n e. Z sum_ k e. ( M ... n ) B <_ x ) /\ y e. ran ( n e. Z |-> sum_ k e. ( M ... n ) B ) ) -> E. n e. Z y = sum_ k e. ( M ... n ) B )
39		nfv	|- F/ n ( ph /\ x e. RR )
40		nfra1	|- F/ n A. n e. Z sum_ k e. ( M ... n ) B <_ x
41	39 40	nfan	|- F/ n ( ( ph /\ x e. RR ) /\ A. n e. Z sum_ k e. ( M ... n ) B <_ x )
42		nfv	|- F/ n y <_ x
43		rspa	|- ( ( A. n e. Z sum_ k e. ( M ... n ) B <_ x /\ n e. Z ) -> sum_ k e. ( M ... n ) B <_ x )
44		simpr	|- ( ( sum_ k e. ( M ... n ) B <_ x /\ y = sum_ k e. ( M ... n ) B ) -> y = sum_ k e. ( M ... n ) B )
45		simpl	|- ( ( sum_ k e. ( M ... n ) B <_ x /\ y = sum_ k e. ( M ... n ) B ) -> sum_ k e. ( M ... n ) B <_ x )
46	44 45	eqbrtrd	|- ( ( sum_ k e. ( M ... n ) B <_ x /\ y = sum_ k e. ( M ... n ) B ) -> y <_ x )
47	46	ex	|- ( sum_ k e. ( M ... n ) B <_ x -> ( y = sum_ k e. ( M ... n ) B -> y <_ x ) )
48	43 47	syl	|- ( ( A. n e. Z sum_ k e. ( M ... n ) B <_ x /\ n e. Z ) -> ( y = sum_ k e. ( M ... n ) B -> y <_ x ) )
49	48	ex	|- ( A. n e. Z sum_ k e. ( M ... n ) B <_ x -> ( n e. Z -> ( y = sum_ k e. ( M ... n ) B -> y <_ x ) ) )
50	49	adantl	|- ( ( ( ph /\ x e. RR ) /\ A. n e. Z sum_ k e. ( M ... n ) B <_ x ) -> ( n e. Z -> ( y = sum_ k e. ( M ... n ) B -> y <_ x ) ) )
51	41 42 50	rexlimd	|- ( ( ( ph /\ x e. RR ) /\ A. n e. Z sum_ k e. ( M ... n ) B <_ x ) -> ( E. n e. Z y = sum_ k e. ( M ... n ) B -> y <_ x ) )
52	51	adantr	|- ( ( ( ( ph /\ x e. RR ) /\ A. n e. Z sum_ k e. ( M ... n ) B <_ x ) /\ y e. ran ( n e. Z |-> sum_ k e. ( M ... n ) B ) ) -> ( E. n e. Z y = sum_ k e. ( M ... n ) B -> y <_ x ) )
53	38 52	mpd	|- ( ( ( ( ph /\ x e. RR ) /\ A. n e. Z sum_ k e. ( M ... n ) B <_ x ) /\ y e. ran ( n e. Z |-> sum_ k e. ( M ... n ) B ) ) -> y <_ x )
54	53	ralrimiva	|- ( ( ( ph /\ x e. RR ) /\ A. n e. Z sum_ k e. ( M ... n ) B <_ x ) -> A. y e. ran ( n e. Z |-> sum_ k e. ( M ... n ) B ) y <_ x )
55	54	ex	|- ( ( ph /\ x e. RR ) -> ( A. n e. Z sum_ k e. ( M ... n ) B <_ x -> A. y e. ran ( n e. Z |-> sum_ k e. ( M ... n ) B ) y <_ x ) )
56	55	ex	|- ( ph -> ( x e. RR -> ( A. n e. Z sum_ k e. ( M ... n ) B <_ x -> A. y e. ran ( n e. Z |-> sum_ k e. ( M ... n ) B ) y <_ x ) ) )
57	2 56	reximdai	|- ( ph -> ( E. x e. RR A. n e. Z sum_ k e. ( M ... n ) B <_ x -> E. x e. RR A. y e. ran ( n e. Z |-> sum_ k e. ( M ... n ) B ) y <_ x ) )
58	6 57	mpd	|- ( ph -> E. x e. RR A. y e. ran ( n e. Z |-> sum_ k e. ( M ... n ) B ) y <_ x )
59		supxrre	|- ( ( ran ( n e. Z |-> sum_ k e. ( M ... n ) B ) C_ RR /\ ran ( n e. Z |-> sum_ k e. ( M ... n ) B ) =/= (/) /\ E. x e. RR A. y e. ran ( n e. Z |-> sum_ k e. ( M ... n ) B ) y <_ x ) -> sup ( ran ( n e. Z |-> sum_ k e. ( M ... n ) B ) , RR* , < ) = sup ( ran ( n e. Z |-> sum_ k e. ( M ... n ) B ) , RR , < ) )
60	21 33 58 59	syl3anc	|- ( ph -> sup ( ran ( n e. Z |-> sum_ k e. ( M ... n ) B ) , RR* , < ) = sup ( ran ( n e. Z |-> sum_ k e. ( M ... n ) B ) , RR , < ) )
61	7 60	eqtrd	|- ( ph -> ( sum^ ` ( k e. Z |-> B ) ) = sup ( ran ( n e. Z |-> sum_ k e. ( M ... n ) B ) , RR , < ) )