Theorem sge0gerp

Description: The arbitrary sum of nonnegative extended reals is greater than or equal to a given extended real number if this number can be approximated from below by finite subsums. (Contributed by Glauco Siliprandi, 17-Aug-2020)

	Ref	Expression
Hypotheses	sge0gerp.x	⊢ ( 𝜑 → 𝑋 ∈ 𝑉 )
	sge0gerp.f	⊢ ( 𝜑 → 𝐹 : 𝑋 ⟶ ( 0 [,] +∞ ) )
	sge0gerp.a	⊢ ( 𝜑 → 𝐴 ∈ ℝ* )
	sge0gerp.z	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) → ∃ 𝑧 ∈ ( 𝒫 𝑋 ∩ Fin ) 𝐴 ≤ ( ( Σ^ ‘ ( 𝐹 ↾ 𝑧 ) ) +𝑒 𝑥 ) )
Assertion	sge0gerp	⊢ ( 𝜑 → 𝐴 ≤ ( Σ^ ‘ 𝐹 ) )

Proof

Step	Hyp	Ref	Expression
1		sge0gerp.x	⊢ ( 𝜑 → 𝑋 ∈ 𝑉 )
2		sge0gerp.f	⊢ ( 𝜑 → 𝐹 : 𝑋 ⟶ ( 0 [,] +∞ ) )
3		sge0gerp.a	⊢ ( 𝜑 → 𝐴 ∈ ℝ* )
4		sge0gerp.z	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) → ∃ 𝑧 ∈ ( 𝒫 𝑋 ∩ Fin ) 𝐴 ≤ ( ( Σ^ ‘ ( 𝐹 ↾ 𝑧 ) ) +𝑒 𝑥 ) )
5		nfv	⊢ Ⅎ 𝑥 𝜑
6		simpr	⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( 𝒫 𝑋 ∩ Fin ) ) → 𝑧 ∈ ( 𝒫 𝑋 ∩ Fin ) )
7	2	adantr	⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( 𝒫 𝑋 ∩ Fin ) ) → 𝐹 : 𝑋 ⟶ ( 0 [,] +∞ ) )
8		elinel1	⊢ ( 𝑧 ∈ ( 𝒫 𝑋 ∩ Fin ) → 𝑧 ∈ 𝒫 𝑋 )
9		elpwi	⊢ ( 𝑧 ∈ 𝒫 𝑋 → 𝑧 ⊆ 𝑋 )
10	8 9	syl	⊢ ( 𝑧 ∈ ( 𝒫 𝑋 ∩ Fin ) → 𝑧 ⊆ 𝑋 )
11	10	adantl	⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( 𝒫 𝑋 ∩ Fin ) ) → 𝑧 ⊆ 𝑋 )
12	7 11	fssresd	⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( 𝒫 𝑋 ∩ Fin ) ) → ( 𝐹 ↾ 𝑧 ) : 𝑧 ⟶ ( 0 [,] +∞ ) )
13	6 12	sge0xrcl	⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( 𝒫 𝑋 ∩ Fin ) ) → ( Σ^ ‘ ( 𝐹 ↾ 𝑧 ) ) ∈ ℝ* )
14	13	ralrimiva	⊢ ( 𝜑 → ∀ 𝑧 ∈ ( 𝒫 𝑋 ∩ Fin ) ( Σ^ ‘ ( 𝐹 ↾ 𝑧 ) ) ∈ ℝ* )
15		eqid	⊢ ( 𝑧 ∈ ( 𝒫 𝑋 ∩ Fin ) ↦ ( Σ^ ‘ ( 𝐹 ↾ 𝑧 ) ) ) = ( 𝑧 ∈ ( 𝒫 𝑋 ∩ Fin ) ↦ ( Σ^ ‘ ( 𝐹 ↾ 𝑧 ) ) )
16	15	rnmptss	⊢ ( ∀ 𝑧 ∈ ( 𝒫 𝑋 ∩ Fin ) ( Σ^ ‘ ( 𝐹 ↾ 𝑧 ) ) ∈ ℝ* → ran ( 𝑧 ∈ ( 𝒫 𝑋 ∩ Fin ) ↦ ( Σ^ ‘ ( 𝐹 ↾ 𝑧 ) ) ) ⊆ ℝ* )
17	14 16	syl	⊢ ( 𝜑 → ran ( 𝑧 ∈ ( 𝒫 𝑋 ∩ Fin ) ↦ ( Σ^ ‘ ( 𝐹 ↾ 𝑧 ) ) ) ⊆ ℝ* )
18		nfv	⊢ Ⅎ 𝑧 ( 𝜑 ∧ 𝑥 ∈ ℝ+ )
19		nfmpt1	⊢ Ⅎ 𝑧 ( 𝑧 ∈ ( 𝒫 𝑋 ∩ Fin ) ↦ ( Σ^ ‘ ( 𝐹 ↾ 𝑧 ) ) )
20	19	nfrn	⊢ Ⅎ 𝑧 ran ( 𝑧 ∈ ( 𝒫 𝑋 ∩ Fin ) ↦ ( Σ^ ‘ ( 𝐹 ↾ 𝑧 ) ) )
21		nfv	⊢ Ⅎ 𝑧 𝐴 ≤ ( 𝑦 +𝑒 𝑥 )
22	20 21	nfrex	⊢ Ⅎ 𝑧 ∃ 𝑦 ∈ ran ( 𝑧 ∈ ( 𝒫 𝑋 ∩ Fin ) ↦ ( Σ^ ‘ ( 𝐹 ↾ 𝑧 ) ) ) 𝐴 ≤ ( 𝑦 +𝑒 𝑥 )
23		id	⊢ ( 𝑧 ∈ ( 𝒫 𝑋 ∩ Fin ) → 𝑧 ∈ ( 𝒫 𝑋 ∩ Fin ) )
24		fvexd	⊢ ( 𝑧 ∈ ( 𝒫 𝑋 ∩ Fin ) → ( Σ^ ‘ ( 𝐹 ↾ 𝑧 ) ) ∈ V )
25	15	elrnmpt1	⊢ ( ( 𝑧 ∈ ( 𝒫 𝑋 ∩ Fin ) ∧ ( Σ^ ‘ ( 𝐹 ↾ 𝑧 ) ) ∈ V ) → ( Σ^ ‘ ( 𝐹 ↾ 𝑧 ) ) ∈ ran ( 𝑧 ∈ ( 𝒫 𝑋 ∩ Fin ) ↦ ( Σ^ ‘ ( 𝐹 ↾ 𝑧 ) ) ) )
26	23 24 25	syl2anc	⊢ ( 𝑧 ∈ ( 𝒫 𝑋 ∩ Fin ) → ( Σ^ ‘ ( 𝐹 ↾ 𝑧 ) ) ∈ ran ( 𝑧 ∈ ( 𝒫 𝑋 ∩ Fin ) ↦ ( Σ^ ‘ ( 𝐹 ↾ 𝑧 ) ) ) )
27	26	3ad2ant2	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑧 ∈ ( 𝒫 𝑋 ∩ Fin ) ∧ 𝐴 ≤ ( ( Σ^ ‘ ( 𝐹 ↾ 𝑧 ) ) +𝑒 𝑥 ) ) → ( Σ^ ‘ ( 𝐹 ↾ 𝑧 ) ) ∈ ran ( 𝑧 ∈ ( 𝒫 𝑋 ∩ Fin ) ↦ ( Σ^ ‘ ( 𝐹 ↾ 𝑧 ) ) ) )
28		simp3	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑧 ∈ ( 𝒫 𝑋 ∩ Fin ) ∧ 𝐴 ≤ ( ( Σ^ ‘ ( 𝐹 ↾ 𝑧 ) ) +𝑒 𝑥 ) ) → 𝐴 ≤ ( ( Σ^ ‘ ( 𝐹 ↾ 𝑧 ) ) +𝑒 𝑥 ) )
29		nfv	⊢ Ⅎ 𝑦 𝐴 ≤ ( ( Σ^ ‘ ( 𝐹 ↾ 𝑧 ) ) +𝑒 𝑥 )
30		oveq1	⊢ ( 𝑦 = ( Σ^ ‘ ( 𝐹 ↾ 𝑧 ) ) → ( 𝑦 +𝑒 𝑥 ) = ( ( Σ^ ‘ ( 𝐹 ↾ 𝑧 ) ) +𝑒 𝑥 ) )
31	30	breq2d	⊢ ( 𝑦 = ( Σ^ ‘ ( 𝐹 ↾ 𝑧 ) ) → ( 𝐴 ≤ ( 𝑦 +𝑒 𝑥 ) ↔ 𝐴 ≤ ( ( Σ^ ‘ ( 𝐹 ↾ 𝑧 ) ) +𝑒 𝑥 ) ) )
32	29 31	rspce	⊢ ( ( ( Σ^ ‘ ( 𝐹 ↾ 𝑧 ) ) ∈ ran ( 𝑧 ∈ ( 𝒫 𝑋 ∩ Fin ) ↦ ( Σ^ ‘ ( 𝐹 ↾ 𝑧 ) ) ) ∧ 𝐴 ≤ ( ( Σ^ ‘ ( 𝐹 ↾ 𝑧 ) ) +𝑒 𝑥 ) ) → ∃ 𝑦 ∈ ran ( 𝑧 ∈ ( 𝒫 𝑋 ∩ Fin ) ↦ ( Σ^ ‘ ( 𝐹 ↾ 𝑧 ) ) ) 𝐴 ≤ ( 𝑦 +𝑒 𝑥 ) )
33	27 28 32	syl2anc	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑧 ∈ ( 𝒫 𝑋 ∩ Fin ) ∧ 𝐴 ≤ ( ( Σ^ ‘ ( 𝐹 ↾ 𝑧 ) ) +𝑒 𝑥 ) ) → ∃ 𝑦 ∈ ran ( 𝑧 ∈ ( 𝒫 𝑋 ∩ Fin ) ↦ ( Σ^ ‘ ( 𝐹 ↾ 𝑧 ) ) ) 𝐴 ≤ ( 𝑦 +𝑒 𝑥 ) )
34	33	3exp	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) → ( 𝑧 ∈ ( 𝒫 𝑋 ∩ Fin ) → ( 𝐴 ≤ ( ( Σ^ ‘ ( 𝐹 ↾ 𝑧 ) ) +𝑒 𝑥 ) → ∃ 𝑦 ∈ ran ( 𝑧 ∈ ( 𝒫 𝑋 ∩ Fin ) ↦ ( Σ^ ‘ ( 𝐹 ↾ 𝑧 ) ) ) 𝐴 ≤ ( 𝑦 +𝑒 𝑥 ) ) ) )
35	18 22 34	rexlimd	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) → ( ∃ 𝑧 ∈ ( 𝒫 𝑋 ∩ Fin ) 𝐴 ≤ ( ( Σ^ ‘ ( 𝐹 ↾ 𝑧 ) ) +𝑒 𝑥 ) → ∃ 𝑦 ∈ ran ( 𝑧 ∈ ( 𝒫 𝑋 ∩ Fin ) ↦ ( Σ^ ‘ ( 𝐹 ↾ 𝑧 ) ) ) 𝐴 ≤ ( 𝑦 +𝑒 𝑥 ) ) )
36	4 35	mpd	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) → ∃ 𝑦 ∈ ran ( 𝑧 ∈ ( 𝒫 𝑋 ∩ Fin ) ↦ ( Σ^ ‘ ( 𝐹 ↾ 𝑧 ) ) ) 𝐴 ≤ ( 𝑦 +𝑒 𝑥 ) )
37	5 17 3 36	supxrge	⊢ ( 𝜑 → 𝐴 ≤ sup ( ran ( 𝑧 ∈ ( 𝒫 𝑋 ∩ Fin ) ↦ ( Σ^ ‘ ( 𝐹 ↾ 𝑧 ) ) ) , ℝ* , < ) )
38	1 2	sge0sup	⊢ ( 𝜑 → ( Σ^ ‘ 𝐹 ) = sup ( ran ( 𝑧 ∈ ( 𝒫 𝑋 ∩ Fin ) ↦ ( Σ^ ‘ ( 𝐹 ↾ 𝑧 ) ) ) , ℝ* , < ) )
39	38	eqcomd	⊢ ( 𝜑 → sup ( ran ( 𝑧 ∈ ( 𝒫 𝑋 ∩ Fin ) ↦ ( Σ^ ‘ ( 𝐹 ↾ 𝑧 ) ) ) , ℝ* , < ) = ( Σ^ ‘ 𝐹 ) )
40	37 39	breqtrd	⊢ ( 𝜑 → 𝐴 ≤ ( Σ^ ‘ 𝐹 ) )