Theorem sge0rernmpt

Description: If the sum of nonnegative extended reals is not +oo then no term is +oo . (Contributed by Glauco Siliprandi, 11-Oct-2020)

	Ref	Expression
Hypotheses	sge0rernmpt.xph	⊢ Ⅎ 𝑥 𝜑
	sge0rernmpt.a	⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
	sge0rernmpt.b	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐵 ∈ ( 0 [,] +∞ ) )
	sge0rernmpt.re	⊢ ( 𝜑 → ( Σ^ ‘ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ) ∈ ℝ )
Assertion	sge0rernmpt	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐵 ∈ ( 0 [,) +∞ ) )

Proof

Step	Hyp	Ref	Expression
1		sge0rernmpt.xph	⊢ Ⅎ 𝑥 𝜑
2		sge0rernmpt.a	⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
3		sge0rernmpt.b	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐵 ∈ ( 0 [,] +∞ ) )
4		sge0rernmpt.re	⊢ ( 𝜑 → ( Σ^ ‘ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ) ∈ ℝ )
5		0xr	⊢ 0 ∈ ℝ*
6	5	a1i	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 0 ∈ ℝ* )
7		pnfxr	⊢ +∞ ∈ ℝ*
8	7	a1i	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → +∞ ∈ ℝ* )
9		iccssxr	⊢ ( 0 [,] +∞ ) ⊆ ℝ*
10	9 3	sselid	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐵 ∈ ℝ* )
11		iccgelb	⊢ ( ( 0 ∈ ℝ* ∧ +∞ ∈ ℝ* ∧ 𝐵 ∈ ( 0 [,] +∞ ) ) → 0 ≤ 𝐵 )
12	6 8 3 11	syl3anc	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 0 ≤ 𝐵 )
13		simpr	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) ∧ ¬ 𝐵 < +∞ ) → ¬ 𝐵 < +∞ )
14		nltpnft	⊢ ( 𝐵 ∈ ℝ* → ( 𝐵 = +∞ ↔ ¬ 𝐵 < +∞ ) )
15	10 14	syl	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( 𝐵 = +∞ ↔ ¬ 𝐵 < +∞ ) )
16	15	adantr	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) ∧ ¬ 𝐵 < +∞ ) → ( 𝐵 = +∞ ↔ ¬ 𝐵 < +∞ ) )
17	13 16	mpbird	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) ∧ ¬ 𝐵 < +∞ ) → 𝐵 = +∞ )
18	17	eqcomd	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) ∧ ¬ 𝐵 < +∞ ) → +∞ = 𝐵 )
19		simpr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝑥 ∈ 𝐴 )
20		eqid	⊢ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) = ( 𝑥 ∈ 𝐴 ↦ 𝐵 )
21	20	elrnmpt1	⊢ ( ( 𝑥 ∈ 𝐴 ∧ 𝐵 ∈ ( 0 [,] +∞ ) ) → 𝐵 ∈ ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) )
22	19 3 21	syl2anc	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐵 ∈ ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) )
23	22	adantr	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) ∧ ¬ 𝐵 < +∞ ) → 𝐵 ∈ ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) )
24	18 23	eqeltrd	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) ∧ ¬ 𝐵 < +∞ ) → +∞ ∈ ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) )
25	1 3 20	fmptdf	⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) : 𝐴 ⟶ ( 0 [,] +∞ ) )
26	2 25 4	sge0rern	⊢ ( 𝜑 → ¬ +∞ ∈ ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) )
27	26	ad2antrr	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) ∧ ¬ 𝐵 < +∞ ) → ¬ +∞ ∈ ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) )
28	24 27	condan	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐵 < +∞ )
29	6 8 10 12 28	elicod	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐵 ∈ ( 0 [,) +∞ ) )