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 ⊢ φ → A ∈ Fin
fsumrp0cl.2 ⊢ φ ∧ k ∈ A → B ∈ 0 +∞
Assertion fsumrp0cl ⊢ φ → ∑ k ∈ A B ∈ 0 +∞

Proof

Step Hyp Ref Expression
1 fsumrp0cl.1 ⊢ φ → A ∈ Fin
2 fsumrp0cl.2 ⊢ φ ∧ k ∈ A → B ∈ 0 +∞
3 rge0ssre ⊢ 0 +∞ ⊆ ℝ
4 ax-resscn ⊢ ℝ ⊆ ℂ
5 3 4 sstri ⊢ 0 +∞ ⊆ ℂ
6 5 a1i ⊢ φ → 0 +∞ ⊆ ℂ
7 simprl ⊢ φ ∧ x ∈ 0 +∞ ∧ y ∈ 0 +∞ → x ∈ 0 +∞
8 3 7 sselid ⊢ φ ∧ x ∈ 0 +∞ ∧ y ∈ 0 +∞ → x ∈ ℝ
9 simprr ⊢ φ ∧ x ∈ 0 +∞ ∧ y ∈ 0 +∞ → y ∈ 0 +∞
10 3 9 sselid ⊢ φ ∧ x ∈ 0 +∞ ∧ y ∈ 0 +∞ → y ∈ ℝ
11 8 10 readdcld ⊢ φ ∧ x ∈ 0 +∞ ∧ y ∈ 0 +∞ → x + y ∈ ℝ
12 11 rexrd ⊢ φ ∧ x ∈ 0 +∞ ∧ y ∈ 0 +∞ → x + y ∈ ℝ *
13 0xr ⊢ 0 ∈ ℝ *
14 pnfxr ⊢ +∞ ∈ ℝ *
15 elico1 ⊢ 0 ∈ ℝ * ∧ +∞ ∈ ℝ * → x ∈ 0 +∞ ↔ x ∈ ℝ * ∧ 0 ≤ x ∧ x < +∞
16 13 14 15 mp2an ⊢ x ∈ 0 +∞ ↔ x ∈ ℝ * ∧ 0 ≤ x ∧ x < +∞
17 16 simp2bi ⊢ x ∈ 0 +∞ → 0 ≤ x
18 7 17 syl ⊢ φ ∧ x ∈ 0 +∞ ∧ y ∈ 0 +∞ → 0 ≤ x
19 elico1 ⊢ 0 ∈ ℝ * ∧ +∞ ∈ ℝ * → y ∈ 0 +∞ ↔ y ∈ ℝ * ∧ 0 ≤ y ∧ y < +∞
20 13 14 19 mp2an ⊢ y ∈ 0 +∞ ↔ y ∈ ℝ * ∧ 0 ≤ y ∧ y < +∞
21 20 simp2bi ⊢ y ∈ 0 +∞ → 0 ≤ y
22 9 21 syl ⊢ φ ∧ x ∈ 0 +∞ ∧ y ∈ 0 +∞ → 0 ≤ y
23 8 10 18 22 addge0d ⊢ φ ∧ x ∈ 0 +∞ ∧ y ∈ 0 +∞ → 0 ≤ x + y
24 ltpnf ⊢ x + y ∈ ℝ → x + y < +∞
25 11 24 syl ⊢ φ ∧ x ∈ 0 +∞ ∧ y ∈ 0 +∞ → x + y < +∞
26 elico1 ⊢ 0 ∈ ℝ * ∧ +∞ ∈ ℝ * → x + y ∈ 0 +∞ ↔ x + y ∈ ℝ * ∧ 0 ≤ x + y ∧ x + y < +∞
27 13 14 26 mp2an ⊢ x + y ∈ 0 +∞ ↔ x + y ∈ ℝ * ∧ 0 ≤ x + y ∧ x + y < +∞
28 12 23 25 27 syl3anbrc ⊢ φ ∧ x ∈ 0 +∞ ∧ y ∈ 0 +∞ → x + y ∈ 0 +∞
29 0e0icopnf ⊢ 0 ∈ 0 +∞
30 29 a1i ⊢ φ → 0 ∈ 0 +∞
31 6 28 1 2 30 fsumcllem ⊢ φ → ∑ k ∈ A B ∈ 0 +∞