Theorem sge0gerpmpt

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	sge0gerpmpt.xph	⊢ Ⅎ 𝑥 𝜑
	sge0gerpmpt.a	⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
	sge0gerpmpt.b	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐵 ∈ ( 0 [,] +∞ ) )
	sge0gerpmpt.c	⊢ ( 𝜑 → 𝐶 ∈ ℝ* )
	sge0gerpmpt.rp	⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℝ+ ) → ∃ 𝑧 ∈ ( 𝒫 𝐴 ∩ Fin ) 𝐶 ≤ ( ( Σ^ ‘ ( 𝑥 ∈ 𝑧 ↦ 𝐵 ) ) +e 𝑦 ) )
Assertion	sge0gerpmpt	⊢ ( 𝜑 → 𝐶 ≤ ( Σ^ ‘ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ) )

Proof

Step	Hyp	Ref	Expression
1		sge0gerpmpt.xph	⊢ Ⅎ 𝑥 𝜑
2		sge0gerpmpt.a	⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
3		sge0gerpmpt.b	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐵 ∈ ( 0 [,] +∞ ) )
4		sge0gerpmpt.c	⊢ ( 𝜑 → 𝐶 ∈ ℝ* )
5		sge0gerpmpt.rp	⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℝ+ ) → ∃ 𝑧 ∈ ( 𝒫 𝐴 ∩ Fin ) 𝐶 ≤ ( ( Σ^ ‘ ( 𝑥 ∈ 𝑧 ↦ 𝐵 ) ) +e 𝑦 ) )
6		eqid	⊢ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) = ( 𝑥 ∈ 𝐴 ↦ 𝐵 )
7	1 3 6	fmptdf	⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) : 𝐴 ⟶ ( 0 [,] +∞ ) )
8		elpwinss	⊢ ( 𝑧 ∈ ( 𝒫 𝐴 ∩ Fin ) → 𝑧 ⊆ 𝐴 )
9	8	resmptd	⊢ ( 𝑧 ∈ ( 𝒫 𝐴 ∩ Fin ) → ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ↾ 𝑧 ) = ( 𝑥 ∈ 𝑧 ↦ 𝐵 ) )
10	9	eqcomd	⊢ ( 𝑧 ∈ ( 𝒫 𝐴 ∩ Fin ) → ( 𝑥 ∈ 𝑧 ↦ 𝐵 ) = ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ↾ 𝑧 ) )
11	10	fveq2d	⊢ ( 𝑧 ∈ ( 𝒫 𝐴 ∩ Fin ) → ( Σ^ ‘ ( 𝑥 ∈ 𝑧 ↦ 𝐵 ) ) = ( Σ^ ‘ ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ↾ 𝑧 ) ) )
12	11	oveq1d	⊢ ( 𝑧 ∈ ( 𝒫 𝐴 ∩ Fin ) → ( ( Σ^ ‘ ( 𝑥 ∈ 𝑧 ↦ 𝐵 ) ) +e 𝑦 ) = ( ( Σ^ ‘ ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ↾ 𝑧 ) ) +e 𝑦 ) )
13	12	breq2d	⊢ ( 𝑧 ∈ ( 𝒫 𝐴 ∩ Fin ) → ( 𝐶 ≤ ( ( Σ^ ‘ ( 𝑥 ∈ 𝑧 ↦ 𝐵 ) ) +e 𝑦 ) ↔ 𝐶 ≤ ( ( Σ^ ‘ ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ↾ 𝑧 ) ) +e 𝑦 ) ) )
14	13	biimpd	⊢ ( 𝑧 ∈ ( 𝒫 𝐴 ∩ Fin ) → ( 𝐶 ≤ ( ( Σ^ ‘ ( 𝑥 ∈ 𝑧 ↦ 𝐵 ) ) +e 𝑦 ) → 𝐶 ≤ ( ( Σ^ ‘ ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ↾ 𝑧 ) ) +e 𝑦 ) ) )
15	14	adantl	⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ+ ) ∧ 𝑧 ∈ ( 𝒫 𝐴 ∩ Fin ) ) → ( 𝐶 ≤ ( ( Σ^ ‘ ( 𝑥 ∈ 𝑧 ↦ 𝐵 ) ) +e 𝑦 ) → 𝐶 ≤ ( ( Σ^ ‘ ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ↾ 𝑧 ) ) +e 𝑦 ) ) )
16	15	reximdva	⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℝ+ ) → ( ∃ 𝑧 ∈ ( 𝒫 𝐴 ∩ Fin ) 𝐶 ≤ ( ( Σ^ ‘ ( 𝑥 ∈ 𝑧 ↦ 𝐵 ) ) +e 𝑦 ) → ∃ 𝑧 ∈ ( 𝒫 𝐴 ∩ Fin ) 𝐶 ≤ ( ( Σ^ ‘ ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ↾ 𝑧 ) ) +e 𝑦 ) ) )
17	5 16	mpd	⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℝ+ ) → ∃ 𝑧 ∈ ( 𝒫 𝐴 ∩ Fin ) 𝐶 ≤ ( ( Σ^ ‘ ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ↾ 𝑧 ) ) +e 𝑦 ) )
18	2 7 4 17	sge0gerp	⊢ ( 𝜑 → 𝐶 ≤ ( Σ^ ‘ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ) )