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∈AB∈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∈AB∈0+∞