esumcvgre

Description: All terms of a converging extended sum shall be finite. (Contributed by Thierry Arnoux, 23-Sep-2019)

	Ref	Expression
Hypotheses	esumcvgre.0	⊢ Ⅎ 𝑘 𝜑
	esumcvgre.1	⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
	esumcvgre.2	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → 𝐵 ∈ ( 0 [,] +∞ ) )
	esumcvgre.3	⊢ ( 𝜑 → Σ^* 𝑘 ∈ 𝐴 𝐵 ∈ ℝ )
Assertion	esumcvgre	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → 𝐵 ∈ ℝ )

Proof

Step	Hyp	Ref	Expression
1		esumcvgre.0	⊢ Ⅎ 𝑘 𝜑
2		esumcvgre.1	⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
3		esumcvgre.2	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → 𝐵 ∈ ( 0 [,] +∞ ) )
4		esumcvgre.3	⊢ ( 𝜑 → Σ^* 𝑘 ∈ 𝐴 𝐵 ∈ ℝ )
5		nfre1	⊢ Ⅎ 𝑘 ∃ 𝑘 ∈ 𝐴 𝐵 = +∞
6	1 5	nfan	⊢ Ⅎ 𝑘 ( 𝜑 ∧ ∃ 𝑘 ∈ 𝐴 𝐵 = +∞ )
7	2	adantr	⊢ ( ( 𝜑 ∧ ∃ 𝑘 ∈ 𝐴 𝐵 = +∞ ) → 𝐴 ∈ 𝑉 )
8	3	adantlr	⊢ ( ( ( 𝜑 ∧ ∃ 𝑘 ∈ 𝐴 𝐵 = +∞ ) ∧ 𝑘 ∈ 𝐴 ) → 𝐵 ∈ ( 0 [,] +∞ ) )
9		simpr	⊢ ( ( 𝜑 ∧ ∃ 𝑘 ∈ 𝐴 𝐵 = +∞ ) → ∃ 𝑘 ∈ 𝐴 𝐵 = +∞ )
10	6 7 8 9	esumpinfval	⊢ ( ( 𝜑 ∧ ∃ 𝑘 ∈ 𝐴 𝐵 = +∞ ) → Σ^* 𝑘 ∈ 𝐴 𝐵 = +∞ )
11		ltpnf	⊢ ( Σ^* 𝑘 ∈ 𝐴 𝐵 ∈ ℝ → Σ^* 𝑘 ∈ 𝐴 𝐵 < +∞ )
12	4 11	syl	⊢ ( 𝜑 → Σ^* 𝑘 ∈ 𝐴 𝐵 < +∞ )
13	4 12	gtned	⊢ ( 𝜑 → +∞ ≠ Σ^* 𝑘 ∈ 𝐴 𝐵 )
14	13	adantr	⊢ ( ( 𝜑 ∧ ∃ 𝑘 ∈ 𝐴 𝐵 = +∞ ) → +∞ ≠ Σ^* 𝑘 ∈ 𝐴 𝐵 )
15		necom	⊢ ( +∞ ≠ Σ^* 𝑘 ∈ 𝐴 𝐵 ↔ Σ^* 𝑘 ∈ 𝐴 𝐵 ≠ +∞ )
16	15	imbi2i	⊢ ( ( ( 𝜑 ∧ ∃ 𝑘 ∈ 𝐴 𝐵 = +∞ ) → +∞ ≠ Σ^* 𝑘 ∈ 𝐴 𝐵 ) ↔ ( ( 𝜑 ∧ ∃ 𝑘 ∈ 𝐴 𝐵 = +∞ ) → Σ^* 𝑘 ∈ 𝐴 𝐵 ≠ +∞ ) )
17	14 16	mpbi	⊢ ( ( 𝜑 ∧ ∃ 𝑘 ∈ 𝐴 𝐵 = +∞ ) → Σ^* 𝑘 ∈ 𝐴 𝐵 ≠ +∞ )
18	17	neneqd	⊢ ( ( 𝜑 ∧ ∃ 𝑘 ∈ 𝐴 𝐵 = +∞ ) → ¬ Σ^* 𝑘 ∈ 𝐴 𝐵 = +∞ )
19	10 18	pm2.65da	⊢ ( 𝜑 → ¬ ∃ 𝑘 ∈ 𝐴 𝐵 = +∞ )
20		ralnex	⊢ ( ∀ 𝑘 ∈ 𝐴 ¬ 𝐵 = +∞ ↔ ¬ ∃ 𝑘 ∈ 𝐴 𝐵 = +∞ )
21	19 20	sylibr	⊢ ( 𝜑 → ∀ 𝑘 ∈ 𝐴 ¬ 𝐵 = +∞ )
22	21	r19.21bi	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → ¬ 𝐵 = +∞ )
23		eliccxr	⊢ ( 𝐵 ∈ ( 0 [,] +∞ ) → 𝐵 ∈ ℝ^* )
24		xrge0neqmnf	⊢ ( 𝐵 ∈ ( 0 [,] +∞ ) → 𝐵 ≠ -∞ )
25		xrnemnf	⊢ ( ( 𝐵 ∈ ℝ^* ∧ 𝐵 ≠ -∞ ) ↔ ( 𝐵 ∈ ℝ ∨ 𝐵 = +∞ ) )
26	25	biimpi	⊢ ( ( 𝐵 ∈ ℝ^* ∧ 𝐵 ≠ -∞ ) → ( 𝐵 ∈ ℝ ∨ 𝐵 = +∞ ) )
27	23 24 26	syl2anc	⊢ ( 𝐵 ∈ ( 0 [,] +∞ ) → ( 𝐵 ∈ ℝ ∨ 𝐵 = +∞ ) )
28	3 27	syl	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → ( 𝐵 ∈ ℝ ∨ 𝐵 = +∞ ) )
29	28	orcomd	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → ( 𝐵 = +∞ ∨ 𝐵 ∈ ℝ ) )
30	29	orcanai	⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) ∧ ¬ 𝐵 = +∞ ) → 𝐵 ∈ ℝ )
31	22 30	mpdan	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → 𝐵 ∈ ℝ )

Metamath Proof Explorer

Theorem esumcvgre

Proof