Theorem sge0lefimpt

Description: A sum of nonnegative extended reals is smaller than a given extended real if and only if every finite subsum is smaller than it. (Contributed by Glauco Siliprandi, 11-Oct-2020)

	Ref	Expression
Hypotheses	sge0lefimpt.xph	⊢ Ⅎ 𝑥 𝜑
	sge0lefimpt.a	⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
	sge0lefimpt.b	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐵 ∈ ( 0 [,] +∞ ) )
	sge0lefimpt.c	⊢ ( 𝜑 → 𝐶 ∈ ℝ* )
Assertion	sge0lefimpt	⊢ ( 𝜑 → ( ( Σ^ ‘ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ) ≤ 𝐶 ↔ ∀ 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) ( Σ^ ‘ ( 𝑥 ∈ 𝑦 ↦ 𝐵 ) ) ≤ 𝐶 ) )

Proof

Step	Hyp	Ref	Expression
1		sge0lefimpt.xph	⊢ Ⅎ 𝑥 𝜑
2		sge0lefimpt.a	⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
3		sge0lefimpt.b	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐵 ∈ ( 0 [,] +∞ ) )
4		sge0lefimpt.c	⊢ ( 𝜑 → 𝐶 ∈ ℝ* )
5		eqid	⊢ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) = ( 𝑥 ∈ 𝐴 ↦ 𝐵 )
6	1 3 5	fmptdf	⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) : 𝐴 ⟶ ( 0 [,] +∞ ) )
7	2 6 4	sge0lefi	⊢ ( 𝜑 → ( ( Σ^ ‘ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ) ≤ 𝐶 ↔ ∀ 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) ( Σ^ ‘ ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ↾ 𝑦 ) ) ≤ 𝐶 ) )
8		elpwinss	⊢ ( 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) → 𝑦 ⊆ 𝐴 )
9	8	resmptd	⊢ ( 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) → ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ↾ 𝑦 ) = ( 𝑥 ∈ 𝑦 ↦ 𝐵 ) )
10	9	fveq2d	⊢ ( 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) → ( Σ^ ‘ ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ↾ 𝑦 ) ) = ( Σ^ ‘ ( 𝑥 ∈ 𝑦 ↦ 𝐵 ) ) )
11	10	breq1d	⊢ ( 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) → ( ( Σ^ ‘ ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ↾ 𝑦 ) ) ≤ 𝐶 ↔ ( Σ^ ‘ ( 𝑥 ∈ 𝑦 ↦ 𝐵 ) ) ≤ 𝐶 ) )
12	11	ralbiia	⊢ ( ∀ 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) ( Σ^ ‘ ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ↾ 𝑦 ) ) ≤ 𝐶 ↔ ∀ 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) ( Σ^ ‘ ( 𝑥 ∈ 𝑦 ↦ 𝐵 ) ) ≤ 𝐶 )
13	12	a1i	⊢ ( 𝜑 → ( ∀ 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) ( Σ^ ‘ ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ↾ 𝑦 ) ) ≤ 𝐶 ↔ ∀ 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) ( Σ^ ‘ ( 𝑥 ∈ 𝑦 ↦ 𝐵 ) ) ≤ 𝐶 ) )
14	7 13	bitrd	⊢ ( 𝜑 → ( ( Σ^ ‘ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ) ≤ 𝐶 ↔ ∀ 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) ( Σ^ ‘ ( 𝑥 ∈ 𝑦 ↦ 𝐵 ) ) ≤ 𝐶 ) )