sge0pnffsumgt

Description: If the sum of nonnegative extended reals is +oo , then any real number can be dominated by finite subsums. (Contributed by Glauco Siliprandi, 21-Nov-2020)

	Ref	Expression
Hypotheses	sge0pnffsumgt.k	⊢ Ⅎ 𝑘 𝜑
	sge0pnffsumgt.a	⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
	sge0pnffsumgt.b	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → 𝐵 ∈ ( 0 [,) +∞ ) )
	sge0pnffsumgt.p	⊢ ( 𝜑 → ( Σ^{^} ‘ ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ) = +∞ )
	sge0pnffsumgt.y	⊢ ( 𝜑 → 𝑌 ∈ ℝ )
Assertion	sge0pnffsumgt	⊢ ( 𝜑 → ∃ 𝑥 ∈ ( 𝒫 𝐴 ∩ Fin ) 𝑌 < Σ 𝑘 ∈ 𝑥 𝐵 )

Proof

Step	Hyp	Ref	Expression
1		sge0pnffsumgt.k	⊢ Ⅎ 𝑘 𝜑
2		sge0pnffsumgt.a	⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
3		sge0pnffsumgt.b	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → 𝐵 ∈ ( 0 [,) +∞ ) )
4		sge0pnffsumgt.p	⊢ ( 𝜑 → ( Σ^{^} ‘ ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ) = +∞ )
5		sge0pnffsumgt.y	⊢ ( 𝜑 → 𝑌 ∈ ℝ )
6		icossicc	⊢ ( 0 [,) +∞ ) ⊆ ( 0 [,] +∞ )
7	6 3	sseldi	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → 𝐵 ∈ ( 0 [,] +∞ ) )
8	1 2 7 4 5	sge0pnffigtmpt	⊢ ( 𝜑 → ∃ 𝑥 ∈ ( 𝒫 𝐴 ∩ Fin ) 𝑌 < ( Σ^{^} ‘ ( 𝑘 ∈ 𝑥 ↦ 𝐵 ) ) )
9		simpr	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝒫 𝐴 ∩ Fin ) ) ∧ 𝑌 < ( Σ^{^} ‘ ( 𝑘 ∈ 𝑥 ↦ 𝐵 ) ) ) → 𝑌 < ( Σ^{^} ‘ ( 𝑘 ∈ 𝑥 ↦ 𝐵 ) ) )
10		nfv	⊢ Ⅎ 𝑘 𝑥 ∈ ( 𝒫 𝐴 ∩ Fin )
11	1 10	nfan	⊢ Ⅎ 𝑘 ( 𝜑 ∧ 𝑥 ∈ ( 𝒫 𝐴 ∩ Fin ) )
12		elinel2	⊢ ( 𝑥 ∈ ( 𝒫 𝐴 ∩ Fin ) → 𝑥 ∈ Fin )
13	12	adantl	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝒫 𝐴 ∩ Fin ) ) → 𝑥 ∈ Fin )
14		simpll	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝒫 𝐴 ∩ Fin ) ) ∧ 𝑘 ∈ 𝑥 ) → 𝜑 )
15		elpwinss	⊢ ( 𝑥 ∈ ( 𝒫 𝐴 ∩ Fin ) → 𝑥 ⊆ 𝐴 )
16	15	sselda	⊢ ( ( 𝑥 ∈ ( 𝒫 𝐴 ∩ Fin ) ∧ 𝑘 ∈ 𝑥 ) → 𝑘 ∈ 𝐴 )
17	16	adantll	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝒫 𝐴 ∩ Fin ) ) ∧ 𝑘 ∈ 𝑥 ) → 𝑘 ∈ 𝐴 )
18	14 17 3	syl2anc	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝒫 𝐴 ∩ Fin ) ) ∧ 𝑘 ∈ 𝑥 ) → 𝐵 ∈ ( 0 [,) +∞ ) )
19	11 13 18	sge0fsummptf	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝒫 𝐴 ∩ Fin ) ) → ( Σ^{^} ‘ ( 𝑘 ∈ 𝑥 ↦ 𝐵 ) ) = Σ 𝑘 ∈ 𝑥 𝐵 )
20	19	adantr	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝒫 𝐴 ∩ Fin ) ) ∧ 𝑌 < ( Σ^{^} ‘ ( 𝑘 ∈ 𝑥 ↦ 𝐵 ) ) ) → ( Σ^{^} ‘ ( 𝑘 ∈ 𝑥 ↦ 𝐵 ) ) = Σ 𝑘 ∈ 𝑥 𝐵 )
21	9 20	breqtrd	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝒫 𝐴 ∩ Fin ) ) ∧ 𝑌 < ( Σ^{^} ‘ ( 𝑘 ∈ 𝑥 ↦ 𝐵 ) ) ) → 𝑌 < Σ 𝑘 ∈ 𝑥 𝐵 )
22	21	ex	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝒫 𝐴 ∩ Fin ) ) → ( 𝑌 < ( Σ^{^} ‘ ( 𝑘 ∈ 𝑥 ↦ 𝐵 ) ) → 𝑌 < Σ 𝑘 ∈ 𝑥 𝐵 ) )
23	22	reximdva	⊢ ( 𝜑 → ( ∃ 𝑥 ∈ ( 𝒫 𝐴 ∩ Fin ) 𝑌 < ( Σ^{^} ‘ ( 𝑘 ∈ 𝑥 ↦ 𝐵 ) ) → ∃ 𝑥 ∈ ( 𝒫 𝐴 ∩ Fin ) 𝑌 < Σ 𝑘 ∈ 𝑥 𝐵 ) )
24	8 23	mpd	⊢ ( 𝜑 → ∃ 𝑥 ∈ ( 𝒫 𝐴 ∩ Fin ) 𝑌 < Σ 𝑘 ∈ 𝑥 𝐵 )

Metamath Proof Explorer

Theorem sge0pnffsumgt

Proof