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 +∞