Metamath Proof Explorer

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 ⊢ Ⅎ k φ
esumpinfval.1 ⊢ φ → A ∈ V
esumpinfval.2 ⊢ φ ∧ k ∈ A → B ∈ 0 +∞
esumpinfval.3 ⊢ φ → ∃ k ∈ A B = +∞
Assertion esumpinfval ⊢ φ → ∑ * k ∈ A B = +∞

Proof

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