Metamath Proof Explorer


Theorem fsumrp0cl

Description: Closure of a finite sum of nonnegative reals. (Contributed by Thierry Arnoux, 25-Jun-2017)

Ref Expression
Hypotheses fsumrp0cl.1 ( 𝜑𝐴 ∈ Fin )
fsumrp0cl.2 ( ( 𝜑𝑘𝐴 ) → 𝐵 ∈ ( 0 [,) +∞ ) )
Assertion fsumrp0cl ( 𝜑 → Σ 𝑘𝐴 𝐵 ∈ ( 0 [,) +∞ ) )

Proof

Step Hyp Ref Expression
1 fsumrp0cl.1 ( 𝜑𝐴 ∈ Fin )
2 fsumrp0cl.2 ( ( 𝜑𝑘𝐴 ) → 𝐵 ∈ ( 0 [,) +∞ ) )
3 rge0ssre ( 0 [,) +∞ ) ⊆ ℝ
4 ax-resscn ℝ ⊆ ℂ
5 3 4 sstri ( 0 [,) +∞ ) ⊆ ℂ
6 5 a1i ( 𝜑 → ( 0 [,) +∞ ) ⊆ ℂ )
7 simprl ( ( 𝜑 ∧ ( 𝑥 ∈ ( 0 [,) +∞ ) ∧ 𝑦 ∈ ( 0 [,) +∞ ) ) ) → 𝑥 ∈ ( 0 [,) +∞ ) )
8 3 7 sselid ( ( 𝜑 ∧ ( 𝑥 ∈ ( 0 [,) +∞ ) ∧ 𝑦 ∈ ( 0 [,) +∞ ) ) ) → 𝑥 ∈ ℝ )
9 simprr ( ( 𝜑 ∧ ( 𝑥 ∈ ( 0 [,) +∞ ) ∧ 𝑦 ∈ ( 0 [,) +∞ ) ) ) → 𝑦 ∈ ( 0 [,) +∞ ) )
10 3 9 sselid ( ( 𝜑 ∧ ( 𝑥 ∈ ( 0 [,) +∞ ) ∧ 𝑦 ∈ ( 0 [,) +∞ ) ) ) → 𝑦 ∈ ℝ )
11 8 10 readdcld ( ( 𝜑 ∧ ( 𝑥 ∈ ( 0 [,) +∞ ) ∧ 𝑦 ∈ ( 0 [,) +∞ ) ) ) → ( 𝑥 + 𝑦 ) ∈ ℝ )
12 11 rexrd ( ( 𝜑 ∧ ( 𝑥 ∈ ( 0 [,) +∞ ) ∧ 𝑦 ∈ ( 0 [,) +∞ ) ) ) → ( 𝑥 + 𝑦 ) ∈ ℝ* )
13 0xr 0 ∈ ℝ*
14 pnfxr +∞ ∈ ℝ*
15 elico1 ( ( 0 ∈ ℝ* ∧ +∞ ∈ ℝ* ) → ( 𝑥 ∈ ( 0 [,) +∞ ) ↔ ( 𝑥 ∈ ℝ* ∧ 0 ≤ 𝑥𝑥 < +∞ ) ) )
16 13 14 15 mp2an ( 𝑥 ∈ ( 0 [,) +∞ ) ↔ ( 𝑥 ∈ ℝ* ∧ 0 ≤ 𝑥𝑥 < +∞ ) )
17 16 simp2bi ( 𝑥 ∈ ( 0 [,) +∞ ) → 0 ≤ 𝑥 )
18 7 17 syl ( ( 𝜑 ∧ ( 𝑥 ∈ ( 0 [,) +∞ ) ∧ 𝑦 ∈ ( 0 [,) +∞ ) ) ) → 0 ≤ 𝑥 )
19 elico1 ( ( 0 ∈ ℝ* ∧ +∞ ∈ ℝ* ) → ( 𝑦 ∈ ( 0 [,) +∞ ) ↔ ( 𝑦 ∈ ℝ* ∧ 0 ≤ 𝑦𝑦 < +∞ ) ) )
20 13 14 19 mp2an ( 𝑦 ∈ ( 0 [,) +∞ ) ↔ ( 𝑦 ∈ ℝ* ∧ 0 ≤ 𝑦𝑦 < +∞ ) )
21 20 simp2bi ( 𝑦 ∈ ( 0 [,) +∞ ) → 0 ≤ 𝑦 )
22 9 21 syl ( ( 𝜑 ∧ ( 𝑥 ∈ ( 0 [,) +∞ ) ∧ 𝑦 ∈ ( 0 [,) +∞ ) ) ) → 0 ≤ 𝑦 )
23 8 10 18 22 addge0d ( ( 𝜑 ∧ ( 𝑥 ∈ ( 0 [,) +∞ ) ∧ 𝑦 ∈ ( 0 [,) +∞ ) ) ) → 0 ≤ ( 𝑥 + 𝑦 ) )
24 ltpnf ( ( 𝑥 + 𝑦 ) ∈ ℝ → ( 𝑥 + 𝑦 ) < +∞ )
25 11 24 syl ( ( 𝜑 ∧ ( 𝑥 ∈ ( 0 [,) +∞ ) ∧ 𝑦 ∈ ( 0 [,) +∞ ) ) ) → ( 𝑥 + 𝑦 ) < +∞ )
26 elico1 ( ( 0 ∈ ℝ* ∧ +∞ ∈ ℝ* ) → ( ( 𝑥 + 𝑦 ) ∈ ( 0 [,) +∞ ) ↔ ( ( 𝑥 + 𝑦 ) ∈ ℝ* ∧ 0 ≤ ( 𝑥 + 𝑦 ) ∧ ( 𝑥 + 𝑦 ) < +∞ ) ) )
27 13 14 26 mp2an ( ( 𝑥 + 𝑦 ) ∈ ( 0 [,) +∞ ) ↔ ( ( 𝑥 + 𝑦 ) ∈ ℝ* ∧ 0 ≤ ( 𝑥 + 𝑦 ) ∧ ( 𝑥 + 𝑦 ) < +∞ ) )
28 12 23 25 27 syl3anbrc ( ( 𝜑 ∧ ( 𝑥 ∈ ( 0 [,) +∞ ) ∧ 𝑦 ∈ ( 0 [,) +∞ ) ) ) → ( 𝑥 + 𝑦 ) ∈ ( 0 [,) +∞ ) )
29 0e0icopnf 0 ∈ ( 0 [,) +∞ )
30 29 a1i ( 𝜑 → 0 ∈ ( 0 [,) +∞ ) )
31 6 28 1 2 30 fsumcllem ( 𝜑 → Σ 𝑘𝐴 𝐵 ∈ ( 0 [,) +∞ ) )