Metamath Proof Explorer


Theorem esumcl

Description: Closure for extended sum in the extended positive reals. (Contributed by Thierry Arnoux, 2-Jan-2017)

Ref Expression
Hypothesis esumcl.1 𝑘 𝐴
Assertion esumcl ( ( 𝐴𝑉 ∧ ∀ 𝑘𝐴 𝐵 ∈ ( 0 [,] +∞ ) ) → Σ* 𝑘𝐴 𝐵 ∈ ( 0 [,] +∞ ) )

Proof

Step Hyp Ref Expression
1 esumcl.1 𝑘 𝐴
2 xrge0base ( 0 [,] +∞ ) = ( Base ‘ ( ℝ*𝑠s ( 0 [,] +∞ ) ) )
3 xrge0cmn ( ℝ*𝑠s ( 0 [,] +∞ ) ) ∈ CMnd
4 3 a1i ( ( 𝐴𝑉 ∧ ∀ 𝑘𝐴 𝐵 ∈ ( 0 [,] +∞ ) ) → ( ℝ*𝑠s ( 0 [,] +∞ ) ) ∈ CMnd )
5 xrge0tps ( ℝ*𝑠s ( 0 [,] +∞ ) ) ∈ TopSp
6 5 a1i ( ( 𝐴𝑉 ∧ ∀ 𝑘𝐴 𝐵 ∈ ( 0 [,] +∞ ) ) → ( ℝ*𝑠s ( 0 [,] +∞ ) ) ∈ TopSp )
7 simpl ( ( 𝐴𝑉 ∧ ∀ 𝑘𝐴 𝐵 ∈ ( 0 [,] +∞ ) ) → 𝐴𝑉 )
8 1 nfel1 𝑘 𝐴𝑉
9 nfra1 𝑘𝑘𝐴 𝐵 ∈ ( 0 [,] +∞ )
10 8 9 nfan 𝑘 ( 𝐴𝑉 ∧ ∀ 𝑘𝐴 𝐵 ∈ ( 0 [,] +∞ ) )
11 nfcv 𝑘 ( 0 [,] +∞ )
12 simpr ( ( 𝐴𝑉 ∧ ∀ 𝑘𝐴 𝐵 ∈ ( 0 [,] +∞ ) ) → ∀ 𝑘𝐴 𝐵 ∈ ( 0 [,] +∞ ) )
13 12 r19.21bi ( ( ( 𝐴𝑉 ∧ ∀ 𝑘𝐴 𝐵 ∈ ( 0 [,] +∞ ) ) ∧ 𝑘𝐴 ) → 𝐵 ∈ ( 0 [,] +∞ ) )
14 eqid ( 𝑘𝐴𝐵 ) = ( 𝑘𝐴𝐵 )
15 10 1 11 13 14 fmptdF ( ( 𝐴𝑉 ∧ ∀ 𝑘𝐴 𝐵 ∈ ( 0 [,] +∞ ) ) → ( 𝑘𝐴𝐵 ) : 𝐴 ⟶ ( 0 [,] +∞ ) )
16 2 4 6 7 15 tsmscl ( ( 𝐴𝑉 ∧ ∀ 𝑘𝐴 𝐵 ∈ ( 0 [,] +∞ ) ) → ( ( ℝ*𝑠s ( 0 [,] +∞ ) ) tsums ( 𝑘𝐴𝐵 ) ) ⊆ ( 0 [,] +∞ ) )
17 df-esum Σ* 𝑘𝐴 𝐵 = ( ( ℝ*𝑠s ( 0 [,] +∞ ) ) tsums ( 𝑘𝐴𝐵 ) )
18 eqid ( ℝ*𝑠s ( 0 [,] +∞ ) ) = ( ℝ*𝑠s ( 0 [,] +∞ ) )
19 18 7 15 xrge0tsmsbi ( ( 𝐴𝑉 ∧ ∀ 𝑘𝐴 𝐵 ∈ ( 0 [,] +∞ ) ) → ( Σ* 𝑘𝐴 𝐵 ∈ ( ( ℝ*𝑠s ( 0 [,] +∞ ) ) tsums ( 𝑘𝐴𝐵 ) ) ↔ Σ* 𝑘𝐴 𝐵 = ( ( ℝ*𝑠s ( 0 [,] +∞ ) ) tsums ( 𝑘𝐴𝐵 ) ) ) )
20 17 19 mpbiri ( ( 𝐴𝑉 ∧ ∀ 𝑘𝐴 𝐵 ∈ ( 0 [,] +∞ ) ) → Σ* 𝑘𝐴 𝐵 ∈ ( ( ℝ*𝑠s ( 0 [,] +∞ ) ) tsums ( 𝑘𝐴𝐵 ) ) )
21 16 20 sseldd ( ( 𝐴𝑉 ∧ ∀ 𝑘𝐴 𝐵 ∈ ( 0 [,] +∞ ) ) → Σ* 𝑘𝐴 𝐵 ∈ ( 0 [,] +∞ ) )