Metamath Proof Explorer

Theorem esumpinfsum

Description: The value of the extended sum of infinitely many terms greater than one. (Contributed by Thierry Arnoux, 29-Jun-2017)

Ref Expression
Hypotheses esumpinfsum.p ⊢ Ⅎ 𝑘 𝜑
esumpinfsum.a ⊢ Ⅎ 𝑘 𝐴
esumpinfsum.1 ⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
esumpinfsum.2 ⊢ ( 𝜑 → ¬ 𝐴 ∈ Fin )
esumpinfsum.3 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → 𝐵 ∈ ( 0 [,] +∞ ) )
esumpinfsum.4 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → 𝑀 ≤ 𝐵 )
esumpinfsum.5 ⊢ ( 𝜑 → 𝑀 ∈ ℝ* )
esumpinfsum.6 ⊢ ( 𝜑 → 0 < 𝑀 )
Assertion esumpinfsum ( 𝜑 → Σ* 𝑘 ∈ 𝐴 𝐵 = +∞ )

Proof

Step Hyp Ref Expression
1 esumpinfsum.p ⊢ Ⅎ 𝑘 𝜑
2 esumpinfsum.a ⊢ Ⅎ 𝑘 𝐴
3 esumpinfsum.1 ⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
4 esumpinfsum.2 ⊢ ( 𝜑 → ¬ 𝐴 ∈ Fin )
5 esumpinfsum.3 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → 𝐵 ∈ ( 0 [,] +∞ ) )
6 esumpinfsum.4 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → 𝑀 ≤ 𝐵 )
7 esumpinfsum.5 ⊢ ( 𝜑 → 𝑀 ∈ ℝ* )
8 esumpinfsum.6 ⊢ ( 𝜑 → 0 < 𝑀 )
9 iccssxr ⊢ ( 0 [,] +∞ ) ⊆ ℝ*
10 5 ex ⊢ ( 𝜑 → ( 𝑘 ∈ 𝐴 → 𝐵 ∈ ( 0 [,] +∞ ) ) )
11 1 10 ralrimi ⊢ ( 𝜑 → ∀ 𝑘 ∈ 𝐴 𝐵 ∈ ( 0 [,] +∞ ) )
12 2 esumcl ⊢ ( ( 𝐴 ∈ 𝑉 ∧ ∀ 𝑘 ∈ 𝐴 𝐵 ∈ ( 0 [,] +∞ ) ) → Σ* 𝑘 ∈ 𝐴 𝐵 ∈ ( 0 [,] +∞ ) )
13 3 11 12 syl2anc ⊢ ( 𝜑 → Σ* 𝑘 ∈ 𝐴 𝐵 ∈ ( 0 [,] +∞ ) )
14 9 13 sselid ⊢ ( 𝜑 → Σ* 𝑘 ∈ 𝐴 𝐵 ∈ ℝ* )
15 0xr ⊢ 0 ∈ ℝ*
16 xrltle ⊢ ( ( 0 ∈ ℝ* ∧ 𝑀 ∈ ℝ* ) → ( 0 < 𝑀 → 0 ≤ 𝑀 ) )
17 15 7 16 sylancr ⊢ ( 𝜑 → ( 0 < 𝑀 → 0 ≤ 𝑀 ) )
18 8 17 mpd ⊢ ( 𝜑 → 0 ≤ 𝑀 )
19 pnfge ⊢ ( 𝑀 ∈ ℝ* → 𝑀 ≤ +∞ )
20 7 19 syl ⊢ ( 𝜑 → 𝑀 ≤ +∞ )
21 pnfxr ⊢ +∞ ∈ ℝ*
22 elicc1 ⊢ ( ( 0 ∈ ℝ* ∧ +∞ ∈ ℝ* ) → ( 𝑀 ∈ ( 0 [,] +∞ ) ↔ ( 𝑀 ∈ ℝ* ∧ 0 ≤ 𝑀 ∧ 𝑀 ≤ +∞ ) ) )
23 15 21 22 mp2an ⊢ ( 𝑀 ∈ ( 0 [,] +∞ ) ↔ ( 𝑀 ∈ ℝ* ∧ 0 ≤ 𝑀 ∧ 𝑀 ≤ +∞ ) )
24 7 18 20 23 syl3anbrc ⊢ ( 𝜑 → 𝑀 ∈ ( 0 [,] +∞ ) )
25 nfcv ⊢ Ⅎ 𝑘 𝑀
26 2 25 esumcst ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝑀 ∈ ( 0 [,] +∞ ) ) → Σ* 𝑘 ∈ 𝐴 𝑀 = ( ( ♯ ‘ 𝐴 ) ·e 𝑀 ) )
27 3 24 26 syl2anc ⊢ ( 𝜑 → Σ* 𝑘 ∈ 𝐴 𝑀 = ( ( ♯ ‘ 𝐴 ) ·e 𝑀 ) )
28 hashinf ⊢ ( ( 𝐴 ∈ 𝑉 ∧ ¬ 𝐴 ∈ Fin ) → ( ♯ ‘ 𝐴 ) = +∞ )
29 3 4 28 syl2anc ⊢ ( 𝜑 → ( ♯ ‘ 𝐴 ) = +∞ )
30 29 oveq1d ⊢ ( 𝜑 → ( ( ♯ ‘ 𝐴 ) ·e 𝑀 ) = ( +∞ ·e 𝑀 ) )
31 xmulpnf2 ⊢ ( ( 𝑀 ∈ ℝ* ∧ 0 < 𝑀 ) → ( +∞ ·e 𝑀 ) = +∞ )
32 7 8 31 syl2anc ⊢ ( 𝜑 → ( +∞ ·e 𝑀 ) = +∞ )
33 27 30 32 3eqtrd ⊢ ( 𝜑 → Σ* 𝑘 ∈ 𝐴 𝑀 = +∞ )
34 24 adantr ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → 𝑀 ∈ ( 0 [,] +∞ ) )
35 1 2 3 34 5 6 esumlef ⊢ ( 𝜑 → Σ* 𝑘 ∈ 𝐴 𝑀 ≤ Σ* 𝑘 ∈ 𝐴 𝐵 )
36 33 35 eqbrtrrd ⊢ ( 𝜑 → +∞ ≤ Σ* 𝑘 ∈ 𝐴 𝐵 )
37 xgepnf ⊢ ( Σ* 𝑘 ∈ 𝐴 𝐵 ∈ ℝ* → ( +∞ ≤ Σ* 𝑘 ∈ 𝐴 𝐵 ↔ Σ* 𝑘 ∈ 𝐴 𝐵 = +∞ ) )
38 37 biimpd ⊢ ( Σ* 𝑘 ∈ 𝐴 𝐵 ∈ ℝ* → ( +∞ ≤ Σ* 𝑘 ∈ 𝐴 𝐵 → Σ* 𝑘 ∈ 𝐴 𝐵 = +∞ ) )
39 14 36 38 sylc ⊢ ( 𝜑 → Σ* 𝑘 ∈ 𝐴 𝐵 = +∞ )