Theorem esumpinfval

Description: The value of the extended sum of nonnegative terms, with at least one infinite term. (Contributed by Thierry Arnoux, 19-Jun-2017)

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

Proof

Step	Hyp	Ref	Expression
1		esumpinfval.0	⊢ Ⅎ 𝑘 𝜑
2		esumpinfval.1	⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
3		esumpinfval.2	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → 𝐵 ∈ ( 0 [,] +∞ ) )
4		esumpinfval.3	⊢ ( 𝜑 → ∃ 𝑘 ∈ 𝐴 𝐵 = +∞ )
5		iccssxr	⊢ ( 0 [,] +∞ ) ⊆ ℝ*
6	3	ex	⊢ ( 𝜑 → ( 𝑘 ∈ 𝐴 → 𝐵 ∈ ( 0 [,] +∞ ) ) )
7	1 6	ralrimi	⊢ ( 𝜑 → ∀ 𝑘 ∈ 𝐴 𝐵 ∈ ( 0 [,] +∞ ) )
8		nfcv	⊢ Ⅎ 𝑘 𝐴
9	8	esumcl	⊢ ( ( 𝐴 ∈ 𝑉 ∧ ∀ 𝑘 ∈ 𝐴 𝐵 ∈ ( 0 [,] +∞ ) ) → Σ* 𝑘 ∈ 𝐴 𝐵 ∈ ( 0 [,] +∞ ) )
10	2 7 9	syl2anc	⊢ ( 𝜑 → Σ* 𝑘 ∈ 𝐴 𝐵 ∈ ( 0 [,] +∞ ) )
11	5 10	sseldi	⊢ ( 𝜑 → Σ* 𝑘 ∈ 𝐴 𝐵 ∈ ℝ* )
12		nfrab1	⊢ Ⅎ 𝑘 { 𝑘 ∈ 𝐴 ∣ 𝐵 = +∞ }
13		ssrab2	⊢ { 𝑘 ∈ 𝐴 ∣ 𝐵 = +∞ } ⊆ 𝐴
14	13	a1i	⊢ ( 𝜑 → { 𝑘 ∈ 𝐴 ∣ 𝐵 = +∞ } ⊆ 𝐴 )
15		0xr	⊢ 0 ∈ ℝ*
16		pnfxr	⊢ +∞ ∈ ℝ*
17		0lepnf	⊢ 0 ≤ +∞
18		ubicc2	⊢ ( ( 0 ∈ ℝ* ∧ +∞ ∈ ℝ* ∧ 0 ≤ +∞ ) → +∞ ∈ ( 0 [,] +∞ ) )
19	15 16 17 18	mp3an	⊢ +∞ ∈ ( 0 [,] +∞ )
20	19	a1i	⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) ∧ 𝐵 = +∞ ) → +∞ ∈ ( 0 [,] +∞ ) )
21		0e0iccpnf	⊢ 0 ∈ ( 0 [,] +∞ )
22	21	a1i	⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) ∧ ¬ 𝐵 = +∞ ) → 0 ∈ ( 0 [,] +∞ ) )
23	20 22	ifclda	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → if ( 𝐵 = +∞ , +∞ , 0 ) ∈ ( 0 [,] +∞ ) )
24		eldif	⊢ ( 𝑘 ∈ ( 𝐴 ∖ { 𝑘 ∈ 𝐴 ∣ 𝐵 = +∞ } ) ↔ ( 𝑘 ∈ 𝐴 ∧ ¬ 𝑘 ∈ { 𝑘 ∈ 𝐴 ∣ 𝐵 = +∞ } ) )
25		rabid	⊢ ( 𝑘 ∈ { 𝑘 ∈ 𝐴 ∣ 𝐵 = +∞ } ↔ ( 𝑘 ∈ 𝐴 ∧ 𝐵 = +∞ ) )
26	25	simplbi2	⊢ ( 𝑘 ∈ 𝐴 → ( 𝐵 = +∞ → 𝑘 ∈ { 𝑘 ∈ 𝐴 ∣ 𝐵 = +∞ } ) )
27	26	con3dimp	⊢ ( ( 𝑘 ∈ 𝐴 ∧ ¬ 𝑘 ∈ { 𝑘 ∈ 𝐴 ∣ 𝐵 = +∞ } ) → ¬ 𝐵 = +∞ )
28	24 27	sylbi	⊢ ( 𝑘 ∈ ( 𝐴 ∖ { 𝑘 ∈ 𝐴 ∣ 𝐵 = +∞ } ) → ¬ 𝐵 = +∞ )
29	28	adantl	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝐴 ∖ { 𝑘 ∈ 𝐴 ∣ 𝐵 = +∞ } ) ) → ¬ 𝐵 = +∞ )
30	29	iffalsed	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝐴 ∖ { 𝑘 ∈ 𝐴 ∣ 𝐵 = +∞ } ) ) → if ( 𝐵 = +∞ , +∞ , 0 ) = 0 )
31	1 12 8 14 2 23 30	esumss	⊢ ( 𝜑 → Σ* 𝑘 ∈ { 𝑘 ∈ 𝐴 ∣ 𝐵 = +∞ } if ( 𝐵 = +∞ , +∞ , 0 ) = Σ* 𝑘 ∈ 𝐴 if ( 𝐵 = +∞ , +∞ , 0 ) )
32		eqidd	⊢ ( 𝜑 → { 𝑘 ∈ 𝐴 ∣ 𝐵 = +∞ } = { 𝑘 ∈ 𝐴 ∣ 𝐵 = +∞ } )
33	25	simprbi	⊢ ( 𝑘 ∈ { 𝑘 ∈ 𝐴 ∣ 𝐵 = +∞ } → 𝐵 = +∞ )
34	33	iftrued	⊢ ( 𝑘 ∈ { 𝑘 ∈ 𝐴 ∣ 𝐵 = +∞ } → if ( 𝐵 = +∞ , +∞ , 0 ) = +∞ )
35	34	adantl	⊢ ( ( 𝜑 ∧ 𝑘 ∈ { 𝑘 ∈ 𝐴 ∣ 𝐵 = +∞ } ) → if ( 𝐵 = +∞ , +∞ , 0 ) = +∞ )
36	1 32 35	esumeq12dvaf	⊢ ( 𝜑 → Σ* 𝑘 ∈ { 𝑘 ∈ 𝐴 ∣ 𝐵 = +∞ } if ( 𝐵 = +∞ , +∞ , 0 ) = Σ* 𝑘 ∈ { 𝑘 ∈ 𝐴 ∣ 𝐵 = +∞ } +∞ )
37	2 14	ssexd	⊢ ( 𝜑 → { 𝑘 ∈ 𝐴 ∣ 𝐵 = +∞ } ∈ V )
38		nfcv	⊢ Ⅎ 𝑘 +∞
39	12 38	esumcst	⊢ ( ( { 𝑘 ∈ 𝐴 ∣ 𝐵 = +∞ } ∈ V ∧ +∞ ∈ ( 0 [,] +∞ ) ) → Σ* 𝑘 ∈ { 𝑘 ∈ 𝐴 ∣ 𝐵 = +∞ } +∞ = ( ( ♯ ‘ { 𝑘 ∈ 𝐴 ∣ 𝐵 = +∞ } ) ·e +∞ ) )
40	37 19 39	sylancl	⊢ ( 𝜑 → Σ* 𝑘 ∈ { 𝑘 ∈ 𝐴 ∣ 𝐵 = +∞ } +∞ = ( ( ♯ ‘ { 𝑘 ∈ 𝐴 ∣ 𝐵 = +∞ } ) ·e +∞ ) )
41		hashxrcl	⊢ ( { 𝑘 ∈ 𝐴 ∣ 𝐵 = +∞ } ∈ V → ( ♯ ‘ { 𝑘 ∈ 𝐴 ∣ 𝐵 = +∞ } ) ∈ ℝ* )
42	37 41	syl	⊢ ( 𝜑 → ( ♯ ‘ { 𝑘 ∈ 𝐴 ∣ 𝐵 = +∞ } ) ∈ ℝ* )
43		rabn0	⊢ ( { 𝑘 ∈ 𝐴 ∣ 𝐵 = +∞ } ≠ ∅ ↔ ∃ 𝑘 ∈ 𝐴 𝐵 = +∞ )
44	4 43	sylibr	⊢ ( 𝜑 → { 𝑘 ∈ 𝐴 ∣ 𝐵 = +∞ } ≠ ∅ )
45		hashgt0	⊢ ( ( { 𝑘 ∈ 𝐴 ∣ 𝐵 = +∞ } ∈ V ∧ { 𝑘 ∈ 𝐴 ∣ 𝐵 = +∞ } ≠ ∅ ) → 0 < ( ♯ ‘ { 𝑘 ∈ 𝐴 ∣ 𝐵 = +∞ } ) )
46	37 44 45	syl2anc	⊢ ( 𝜑 → 0 < ( ♯ ‘ { 𝑘 ∈ 𝐴 ∣ 𝐵 = +∞ } ) )
47		xmulpnf1	⊢ ( ( ( ♯ ‘ { 𝑘 ∈ 𝐴 ∣ 𝐵 = +∞ } ) ∈ ℝ* ∧ 0 < ( ♯ ‘ { 𝑘 ∈ 𝐴 ∣ 𝐵 = +∞ } ) ) → ( ( ♯ ‘ { 𝑘 ∈ 𝐴 ∣ 𝐵 = +∞ } ) ·e +∞ ) = +∞ )
48	42 46 47	syl2anc	⊢ ( 𝜑 → ( ( ♯ ‘ { 𝑘 ∈ 𝐴 ∣ 𝐵 = +∞ } ) ·e +∞ ) = +∞ )
49	36 40 48	3eqtrd	⊢ ( 𝜑 → Σ* 𝑘 ∈ { 𝑘 ∈ 𝐴 ∣ 𝐵 = +∞ } if ( 𝐵 = +∞ , +∞ , 0 ) = +∞ )
50	31 49	eqtr3d	⊢ ( 𝜑 → Σ* 𝑘 ∈ 𝐴 if ( 𝐵 = +∞ , +∞ , 0 ) = +∞ )
51		breq1	⊢ ( +∞ = if ( 𝐵 = +∞ , +∞ , 0 ) → ( +∞ ≤ 𝐵 ↔ if ( 𝐵 = +∞ , +∞ , 0 ) ≤ 𝐵 ) )
52		breq1	⊢ ( 0 = if ( 𝐵 = +∞ , +∞ , 0 ) → ( 0 ≤ 𝐵 ↔ if ( 𝐵 = +∞ , +∞ , 0 ) ≤ 𝐵 ) )
53		pnfge	⊢ ( +∞ ∈ ℝ* → +∞ ≤ +∞ )
54	16 53	ax-mp	⊢ +∞ ≤ +∞
55		breq2	⊢ ( 𝐵 = +∞ → ( +∞ ≤ 𝐵 ↔ +∞ ≤ +∞ ) )
56	54 55	mpbiri	⊢ ( 𝐵 = +∞ → +∞ ≤ 𝐵 )
57	56	adantl	⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) ∧ 𝐵 = +∞ ) → +∞ ≤ 𝐵 )
58	3	adantr	⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) ∧ ¬ 𝐵 = +∞ ) → 𝐵 ∈ ( 0 [,] +∞ ) )
59		iccgelb	⊢ ( ( 0 ∈ ℝ* ∧ +∞ ∈ ℝ* ∧ 𝐵 ∈ ( 0 [,] +∞ ) ) → 0 ≤ 𝐵 )
60	15 16 59	mp3an12	⊢ ( 𝐵 ∈ ( 0 [,] +∞ ) → 0 ≤ 𝐵 )
61	58 60	syl	⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) ∧ ¬ 𝐵 = +∞ ) → 0 ≤ 𝐵 )
62	51 52 57 61	ifbothda	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → if ( 𝐵 = +∞ , +∞ , 0 ) ≤ 𝐵 )
63	1 8 2 23 3 62	esumlef	⊢ ( 𝜑 → Σ* 𝑘 ∈ 𝐴 if ( 𝐵 = +∞ , +∞ , 0 ) ≤ Σ* 𝑘 ∈ 𝐴 𝐵 )
64	50 63	eqbrtrrd	⊢ ( 𝜑 → +∞ ≤ Σ* 𝑘 ∈ 𝐴 𝐵 )
65		xgepnf	⊢ ( Σ* 𝑘 ∈ 𝐴 𝐵 ∈ ℝ* → ( +∞ ≤ Σ* 𝑘 ∈ 𝐴 𝐵 ↔ Σ* 𝑘 ∈ 𝐴 𝐵 = +∞ ) )
66	65	biimpd	⊢ ( Σ* 𝑘 ∈ 𝐴 𝐵 ∈ ℝ* → ( +∞ ≤ Σ* 𝑘 ∈ 𝐴 𝐵 → Σ* 𝑘 ∈ 𝐴 𝐵 = +∞ ) )
67	11 64 66	sylc	⊢ ( 𝜑 → Σ* 𝑘 ∈ 𝐴 𝐵 = +∞ )