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 [,) +∞ ) )