Theorem sge0ltfirpmpt

Description: If the extended sum of nonnegative reals is not +oo , then it can be approximated from below by finite subsums. (Contributed by Glauco Siliprandi, 17-Aug-2020)

	Ref	Expression
Hypotheses	sge0ltfirpmpt.xph	⊢ Ⅎ 𝑥 𝜑
	sge0ltfirpmpt.a	⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
	sge0ltfirpmpt.b	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐵 ∈ ( 0 [,] +∞ ) )
	sge0ltfirpmpt.rp	⊢ ( 𝜑 → 𝑌 ∈ ℝ+ )
	sge0ltfirpmpt.re	⊢ ( 𝜑 → ( Σ^ ‘ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ) ∈ ℝ )
Assertion	sge0ltfirpmpt	⊢ ( 𝜑 → ∃ 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) ( Σ^ ‘ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ) < ( ( Σ^ ‘ ( 𝑥 ∈ 𝑦 ↦ 𝐵 ) ) + 𝑌 ) )

Proof

Step	Hyp	Ref	Expression
1		sge0ltfirpmpt.xph	⊢ Ⅎ 𝑥 𝜑
2		sge0ltfirpmpt.a	⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
3		sge0ltfirpmpt.b	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐵 ∈ ( 0 [,] +∞ ) )
4		sge0ltfirpmpt.rp	⊢ ( 𝜑 → 𝑌 ∈ ℝ+ )
5		sge0ltfirpmpt.re	⊢ ( 𝜑 → ( Σ^ ‘ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ) ∈ ℝ )
6		eqid	⊢ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) = ( 𝑥 ∈ 𝐴 ↦ 𝐵 )
7	1 3 6	fmptdf	⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) : 𝐴 ⟶ ( 0 [,] +∞ ) )
8	2 7 4 5	sge0ltfirp	⊢ ( 𝜑 → ∃ 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) ( Σ^ ‘ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ) < ( ( Σ^ ‘ ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ↾ 𝑦 ) ) + 𝑌 ) )
9		simpr	⊢ ( ( 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) ∧ ( Σ^ ‘ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ) < ( ( Σ^ ‘ ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ↾ 𝑦 ) ) + 𝑌 ) ) → ( Σ^ ‘ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ) < ( ( Σ^ ‘ ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ↾ 𝑦 ) ) + 𝑌 ) )
10		elpwinss	⊢ ( 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) → 𝑦 ⊆ 𝐴 )
11	10	resmptd	⊢ ( 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) → ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ↾ 𝑦 ) = ( 𝑥 ∈ 𝑦 ↦ 𝐵 ) )
12	11	fveq2d	⊢ ( 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) → ( Σ^ ‘ ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ↾ 𝑦 ) ) = ( Σ^ ‘ ( 𝑥 ∈ 𝑦 ↦ 𝐵 ) ) )
13	12	oveq1d	⊢ ( 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) → ( ( Σ^ ‘ ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ↾ 𝑦 ) ) + 𝑌 ) = ( ( Σ^ ‘ ( 𝑥 ∈ 𝑦 ↦ 𝐵 ) ) + 𝑌 ) )
14	13	adantr	⊢ ( ( 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) ∧ ( Σ^ ‘ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ) < ( ( Σ^ ‘ ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ↾ 𝑦 ) ) + 𝑌 ) ) → ( ( Σ^ ‘ ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ↾ 𝑦 ) ) + 𝑌 ) = ( ( Σ^ ‘ ( 𝑥 ∈ 𝑦 ↦ 𝐵 ) ) + 𝑌 ) )
15	9 14	breqtrd	⊢ ( ( 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) ∧ ( Σ^ ‘ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ) < ( ( Σ^ ‘ ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ↾ 𝑦 ) ) + 𝑌 ) ) → ( Σ^ ‘ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ) < ( ( Σ^ ‘ ( 𝑥 ∈ 𝑦 ↦ 𝐵 ) ) + 𝑌 ) )
16	15	ex	⊢ ( 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) → ( ( Σ^ ‘ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ) < ( ( Σ^ ‘ ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ↾ 𝑦 ) ) + 𝑌 ) → ( Σ^ ‘ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ) < ( ( Σ^ ‘ ( 𝑥 ∈ 𝑦 ↦ 𝐵 ) ) + 𝑌 ) ) )
17	16	reximia	⊢ ( ∃ 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) ( Σ^ ‘ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ) < ( ( Σ^ ‘ ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ↾ 𝑦 ) ) + 𝑌 ) → ∃ 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) ( Σ^ ‘ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ) < ( ( Σ^ ‘ ( 𝑥 ∈ 𝑦 ↦ 𝐵 ) ) + 𝑌 ) )
18	17	a1i	⊢ ( 𝜑 → ( ∃ 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) ( Σ^ ‘ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ) < ( ( Σ^ ‘ ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ↾ 𝑦 ) ) + 𝑌 ) → ∃ 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) ( Σ^ ‘ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ) < ( ( Σ^ ‘ ( 𝑥 ∈ 𝑦 ↦ 𝐵 ) ) + 𝑌 ) ) )
19	8 18	mpd	⊢ ( 𝜑 → ∃ 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) ( Σ^ ‘ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ) < ( ( Σ^ ‘ ( 𝑥 ∈ 𝑦 ↦ 𝐵 ) ) + 𝑌 ) )