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	⊢ Ⅎ 𝑘 𝜑
	sge0reuzb.p	⊢ Ⅎ 𝑥 𝜑
	sge0reuzb.m	⊢ ( 𝜑 → 𝑀 ∈ ℤ )
	sge0reuzb.z	⊢ 𝑍 = ( ℤ≥ ‘ 𝑀 )
	sge0reuzb.b	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → 𝐵 ∈ ( 0 [,) +∞ ) )
	sge0reuzb.x	⊢ ( 𝜑 → ∃ 𝑥 ∈ ℝ ∀ 𝑛 ∈ 𝑍 Σ 𝑘 ∈ ( 𝑀 ... 𝑛 ) 𝐵 ≤ 𝑥 )
Assertion	sge0reuzb	⊢ ( 𝜑 → ( Σ^ ‘ ( 𝑘 ∈ 𝑍 ↦ 𝐵 ) ) = sup ( ran ( 𝑛 ∈ 𝑍 ↦ Σ 𝑘 ∈ ( 𝑀 ... 𝑛 ) 𝐵 ) , ℝ , < ) )

Proof

Step	Hyp	Ref	Expression
1		sge0reuzb.k	⊢ Ⅎ 𝑘 𝜑
2		sge0reuzb.p	⊢ Ⅎ 𝑥 𝜑
3		sge0reuzb.m	⊢ ( 𝜑 → 𝑀 ∈ ℤ )
4		sge0reuzb.z	⊢ 𝑍 = ( ℤ≥ ‘ 𝑀 )
5		sge0reuzb.b	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → 𝐵 ∈ ( 0 [,) +∞ ) )
6		sge0reuzb.x	⊢ ( 𝜑 → ∃ 𝑥 ∈ ℝ ∀ 𝑛 ∈ 𝑍 Σ 𝑘 ∈ ( 𝑀 ... 𝑛 ) 𝐵 ≤ 𝑥 )
7	1 3 4 5	sge0reuz	⊢ ( 𝜑 → ( Σ^ ‘ ( 𝑘 ∈ 𝑍 ↦ 𝐵 ) ) = sup ( ran ( 𝑛 ∈ 𝑍 ↦ Σ 𝑘 ∈ ( 𝑀 ... 𝑛 ) 𝐵 ) , ℝ* , < ) )
8		nfv	⊢ Ⅎ 𝑛 𝜑
9		eqid	⊢ ( 𝑛 ∈ 𝑍 ↦ Σ 𝑘 ∈ ( 𝑀 ... 𝑛 ) 𝐵 ) = ( 𝑛 ∈ 𝑍 ↦ Σ 𝑘 ∈ ( 𝑀 ... 𝑛 ) 𝐵 )
10		nfv	⊢ Ⅎ 𝑘 𝑛 ∈ 𝑍
11	1 10	nfan	⊢ Ⅎ 𝑘 ( 𝜑 ∧ 𝑛 ∈ 𝑍 )
12		fzfid	⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝑍 ) → ( 𝑀 ... 𝑛 ) ∈ Fin )
13		elfzuz	⊢ ( 𝑘 ∈ ( 𝑀 ... 𝑛 ) → 𝑘 ∈ ( ℤ≥ ‘ 𝑀 ) )
14	13 4	eleqtrrdi	⊢ ( 𝑘 ∈ ( 𝑀 ... 𝑛 ) → 𝑘 ∈ 𝑍 )
15	14	adantl	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝑀 ... 𝑛 ) ) → 𝑘 ∈ 𝑍 )
16		rge0ssre	⊢ ( 0 [,) +∞ ) ⊆ ℝ
17	16 5	sseldi	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → 𝐵 ∈ ℝ )
18	15 17	syldan	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝑀 ... 𝑛 ) ) → 𝐵 ∈ ℝ )
19	18	adantlr	⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ 𝑍 ) ∧ 𝑘 ∈ ( 𝑀 ... 𝑛 ) ) → 𝐵 ∈ ℝ )
20	11 12 19	fsumreclf	⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝑍 ) → Σ 𝑘 ∈ ( 𝑀 ... 𝑛 ) 𝐵 ∈ ℝ )
21	8 9 20	rnmptssd	⊢ ( 𝜑 → ran ( 𝑛 ∈ 𝑍 ↦ Σ 𝑘 ∈ ( 𝑀 ... 𝑛 ) 𝐵 ) ⊆ ℝ )
22		uzid	⊢ ( 𝑀 ∈ ℤ → 𝑀 ∈ ( ℤ≥ ‘ 𝑀 ) )
23	3 22	syl	⊢ ( 𝜑 → 𝑀 ∈ ( ℤ≥ ‘ 𝑀 ) )
24	23 4	eleqtrrdi	⊢ ( 𝜑 → 𝑀 ∈ 𝑍 )
25		eqidd	⊢ ( 𝜑 → Σ 𝑘 ∈ ( 𝑀 ... 𝑀 ) 𝐵 = Σ 𝑘 ∈ ( 𝑀 ... 𝑀 ) 𝐵 )
26		oveq2	⊢ ( 𝑛 = 𝑀 → ( 𝑀 ... 𝑛 ) = ( 𝑀 ... 𝑀 ) )
27	26	sumeq1d	⊢ ( 𝑛 = 𝑀 → Σ 𝑘 ∈ ( 𝑀 ... 𝑛 ) 𝐵 = Σ 𝑘 ∈ ( 𝑀 ... 𝑀 ) 𝐵 )
28	27	rspceeqv	⊢ ( ( 𝑀 ∈ 𝑍 ∧ Σ 𝑘 ∈ ( 𝑀 ... 𝑀 ) 𝐵 = Σ 𝑘 ∈ ( 𝑀 ... 𝑀 ) 𝐵 ) → ∃ 𝑛 ∈ 𝑍 Σ 𝑘 ∈ ( 𝑀 ... 𝑀 ) 𝐵 = Σ 𝑘 ∈ ( 𝑀 ... 𝑛 ) 𝐵 )
29	24 25 28	syl2anc	⊢ ( 𝜑 → ∃ 𝑛 ∈ 𝑍 Σ 𝑘 ∈ ( 𝑀 ... 𝑀 ) 𝐵 = Σ 𝑘 ∈ ( 𝑀 ... 𝑛 ) 𝐵 )
30		sumex	⊢ Σ 𝑘 ∈ ( 𝑀 ... 𝑀 ) 𝐵 ∈ V
31	30	a1i	⊢ ( 𝜑 → Σ 𝑘 ∈ ( 𝑀 ... 𝑀 ) 𝐵 ∈ V )
32	9 29 31	elrnmptd	⊢ ( 𝜑 → Σ 𝑘 ∈ ( 𝑀 ... 𝑀 ) 𝐵 ∈ ran ( 𝑛 ∈ 𝑍 ↦ Σ 𝑘 ∈ ( 𝑀 ... 𝑛 ) 𝐵 ) )
33	32	ne0d	⊢ ( 𝜑 → ran ( 𝑛 ∈ 𝑍 ↦ Σ 𝑘 ∈ ( 𝑀 ... 𝑛 ) 𝐵 ) ≠ ∅ )
34		vex	⊢ 𝑦 ∈ V
35	9	elrnmpt	⊢ ( 𝑦 ∈ V → ( 𝑦 ∈ ran ( 𝑛 ∈ 𝑍 ↦ Σ 𝑘 ∈ ( 𝑀 ... 𝑛 ) 𝐵 ) ↔ ∃ 𝑛 ∈ 𝑍 𝑦 = Σ 𝑘 ∈ ( 𝑀 ... 𝑛 ) 𝐵 ) )
36	34 35	ax-mp	⊢ ( 𝑦 ∈ ran ( 𝑛 ∈ 𝑍 ↦ Σ 𝑘 ∈ ( 𝑀 ... 𝑛 ) 𝐵 ) ↔ ∃ 𝑛 ∈ 𝑍 𝑦 = Σ 𝑘 ∈ ( 𝑀 ... 𝑛 ) 𝐵 )
37	36	biimpi	⊢ ( 𝑦 ∈ ran ( 𝑛 ∈ 𝑍 ↦ Σ 𝑘 ∈ ( 𝑀 ... 𝑛 ) 𝐵 ) → ∃ 𝑛 ∈ 𝑍 𝑦 = Σ 𝑘 ∈ ( 𝑀 ... 𝑛 ) 𝐵 )
38	37	adantl	⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ ∀ 𝑛 ∈ 𝑍 Σ 𝑘 ∈ ( 𝑀 ... 𝑛 ) 𝐵 ≤ 𝑥 ) ∧ 𝑦 ∈ ran ( 𝑛 ∈ 𝑍 ↦ Σ 𝑘 ∈ ( 𝑀 ... 𝑛 ) 𝐵 ) ) → ∃ 𝑛 ∈ 𝑍 𝑦 = Σ 𝑘 ∈ ( 𝑀 ... 𝑛 ) 𝐵 )
39		nfv	⊢ Ⅎ 𝑛 ( 𝜑 ∧ 𝑥 ∈ ℝ )
40		nfra1	⊢ Ⅎ 𝑛 ∀ 𝑛 ∈ 𝑍 Σ 𝑘 ∈ ( 𝑀 ... 𝑛 ) 𝐵 ≤ 𝑥
41	39 40	nfan	⊢ Ⅎ 𝑛 ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ ∀ 𝑛 ∈ 𝑍 Σ 𝑘 ∈ ( 𝑀 ... 𝑛 ) 𝐵 ≤ 𝑥 )
42		nfv	⊢ Ⅎ 𝑛 𝑦 ≤ 𝑥
43		rspa	⊢ ( ( ∀ 𝑛 ∈ 𝑍 Σ 𝑘 ∈ ( 𝑀 ... 𝑛 ) 𝐵 ≤ 𝑥 ∧ 𝑛 ∈ 𝑍 ) → Σ 𝑘 ∈ ( 𝑀 ... 𝑛 ) 𝐵 ≤ 𝑥 )
44		simpr	⊢ ( ( Σ 𝑘 ∈ ( 𝑀 ... 𝑛 ) 𝐵 ≤ 𝑥 ∧ 𝑦 = Σ 𝑘 ∈ ( 𝑀 ... 𝑛 ) 𝐵 ) → 𝑦 = Σ 𝑘 ∈ ( 𝑀 ... 𝑛 ) 𝐵 )
45		simpl	⊢ ( ( Σ 𝑘 ∈ ( 𝑀 ... 𝑛 ) 𝐵 ≤ 𝑥 ∧ 𝑦 = Σ 𝑘 ∈ ( 𝑀 ... 𝑛 ) 𝐵 ) → Σ 𝑘 ∈ ( 𝑀 ... 𝑛 ) 𝐵 ≤ 𝑥 )
46	44 45	eqbrtrd	⊢ ( ( Σ 𝑘 ∈ ( 𝑀 ... 𝑛 ) 𝐵 ≤ 𝑥 ∧ 𝑦 = Σ 𝑘 ∈ ( 𝑀 ... 𝑛 ) 𝐵 ) → 𝑦 ≤ 𝑥 )
47	46	ex	⊢ ( Σ 𝑘 ∈ ( 𝑀 ... 𝑛 ) 𝐵 ≤ 𝑥 → ( 𝑦 = Σ 𝑘 ∈ ( 𝑀 ... 𝑛 ) 𝐵 → 𝑦 ≤ 𝑥 ) )
48	43 47	syl	⊢ ( ( ∀ 𝑛 ∈ 𝑍 Σ 𝑘 ∈ ( 𝑀 ... 𝑛 ) 𝐵 ≤ 𝑥 ∧ 𝑛 ∈ 𝑍 ) → ( 𝑦 = Σ 𝑘 ∈ ( 𝑀 ... 𝑛 ) 𝐵 → 𝑦 ≤ 𝑥 ) )
49	48	ex	⊢ ( ∀ 𝑛 ∈ 𝑍 Σ 𝑘 ∈ ( 𝑀 ... 𝑛 ) 𝐵 ≤ 𝑥 → ( 𝑛 ∈ 𝑍 → ( 𝑦 = Σ 𝑘 ∈ ( 𝑀 ... 𝑛 ) 𝐵 → 𝑦 ≤ 𝑥 ) ) )
50	49	adantl	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ ∀ 𝑛 ∈ 𝑍 Σ 𝑘 ∈ ( 𝑀 ... 𝑛 ) 𝐵 ≤ 𝑥 ) → ( 𝑛 ∈ 𝑍 → ( 𝑦 = Σ 𝑘 ∈ ( 𝑀 ... 𝑛 ) 𝐵 → 𝑦 ≤ 𝑥 ) ) )
51	41 42 50	rexlimd	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ ∀ 𝑛 ∈ 𝑍 Σ 𝑘 ∈ ( 𝑀 ... 𝑛 ) 𝐵 ≤ 𝑥 ) → ( ∃ 𝑛 ∈ 𝑍 𝑦 = Σ 𝑘 ∈ ( 𝑀 ... 𝑛 ) 𝐵 → 𝑦 ≤ 𝑥 ) )
52	51	adantr	⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ ∀ 𝑛 ∈ 𝑍 Σ 𝑘 ∈ ( 𝑀 ... 𝑛 ) 𝐵 ≤ 𝑥 ) ∧ 𝑦 ∈ ran ( 𝑛 ∈ 𝑍 ↦ Σ 𝑘 ∈ ( 𝑀 ... 𝑛 ) 𝐵 ) ) → ( ∃ 𝑛 ∈ 𝑍 𝑦 = Σ 𝑘 ∈ ( 𝑀 ... 𝑛 ) 𝐵 → 𝑦 ≤ 𝑥 ) )
53	38 52	mpd	⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ ∀ 𝑛 ∈ 𝑍 Σ 𝑘 ∈ ( 𝑀 ... 𝑛 ) 𝐵 ≤ 𝑥 ) ∧ 𝑦 ∈ ran ( 𝑛 ∈ 𝑍 ↦ Σ 𝑘 ∈ ( 𝑀 ... 𝑛 ) 𝐵 ) ) → 𝑦 ≤ 𝑥 )
54	53	ralrimiva	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ ∀ 𝑛 ∈ 𝑍 Σ 𝑘 ∈ ( 𝑀 ... 𝑛 ) 𝐵 ≤ 𝑥 ) → ∀ 𝑦 ∈ ran ( 𝑛 ∈ 𝑍 ↦ Σ 𝑘 ∈ ( 𝑀 ... 𝑛 ) 𝐵 ) 𝑦 ≤ 𝑥 )
55	54	ex	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) → ( ∀ 𝑛 ∈ 𝑍 Σ 𝑘 ∈ ( 𝑀 ... 𝑛 ) 𝐵 ≤ 𝑥 → ∀ 𝑦 ∈ ran ( 𝑛 ∈ 𝑍 ↦ Σ 𝑘 ∈ ( 𝑀 ... 𝑛 ) 𝐵 ) 𝑦 ≤ 𝑥 ) )
56	55	ex	⊢ ( 𝜑 → ( 𝑥 ∈ ℝ → ( ∀ 𝑛 ∈ 𝑍 Σ 𝑘 ∈ ( 𝑀 ... 𝑛 ) 𝐵 ≤ 𝑥 → ∀ 𝑦 ∈ ran ( 𝑛 ∈ 𝑍 ↦ Σ 𝑘 ∈ ( 𝑀 ... 𝑛 ) 𝐵 ) 𝑦 ≤ 𝑥 ) ) )
57	2 56	reximdai	⊢ ( 𝜑 → ( ∃ 𝑥 ∈ ℝ ∀ 𝑛 ∈ 𝑍 Σ 𝑘 ∈ ( 𝑀 ... 𝑛 ) 𝐵 ≤ 𝑥 → ∃ 𝑥 ∈ ℝ ∀ 𝑦 ∈ ran ( 𝑛 ∈ 𝑍 ↦ Σ 𝑘 ∈ ( 𝑀 ... 𝑛 ) 𝐵 ) 𝑦 ≤ 𝑥 ) )
58	6 57	mpd	⊢ ( 𝜑 → ∃ 𝑥 ∈ ℝ ∀ 𝑦 ∈ ran ( 𝑛 ∈ 𝑍 ↦ Σ 𝑘 ∈ ( 𝑀 ... 𝑛 ) 𝐵 ) 𝑦 ≤ 𝑥 )
59		supxrre	⊢ ( ( ran ( 𝑛 ∈ 𝑍 ↦ Σ 𝑘 ∈ ( 𝑀 ... 𝑛 ) 𝐵 ) ⊆ ℝ ∧ ran ( 𝑛 ∈ 𝑍 ↦ Σ 𝑘 ∈ ( 𝑀 ... 𝑛 ) 𝐵 ) ≠ ∅ ∧ ∃ 𝑥 ∈ ℝ ∀ 𝑦 ∈ ran ( 𝑛 ∈ 𝑍 ↦ Σ 𝑘 ∈ ( 𝑀 ... 𝑛 ) 𝐵 ) 𝑦 ≤ 𝑥 ) → sup ( ran ( 𝑛 ∈ 𝑍 ↦ Σ 𝑘 ∈ ( 𝑀 ... 𝑛 ) 𝐵 ) , ℝ* , < ) = sup ( ran ( 𝑛 ∈ 𝑍 ↦ Σ 𝑘 ∈ ( 𝑀 ... 𝑛 ) 𝐵 ) , ℝ , < ) )
60	21 33 58 59	syl3anc	⊢ ( 𝜑 → sup ( ran ( 𝑛 ∈ 𝑍 ↦ Σ 𝑘 ∈ ( 𝑀 ... 𝑛 ) 𝐵 ) , ℝ* , < ) = sup ( ran ( 𝑛 ∈ 𝑍 ↦ Σ 𝑘 ∈ ( 𝑀 ... 𝑛 ) 𝐵 ) , ℝ , < ) )
61	7 60	eqtrd	⊢ ( 𝜑 → ( Σ^ ‘ ( 𝑘 ∈ 𝑍 ↦ 𝐵 ) ) = sup ( ran ( 𝑛 ∈ 𝑍 ↦ Σ 𝑘 ∈ ( 𝑀 ... 𝑛 ) 𝐵 ) , ℝ , < ) )