This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 
|- ( ph -> A e. Fin )
fsumrp0cl.2 
|- ( ( ph /\ k e. A ) -> B e. ( 0 [,) +oo ) )
Assertion fsumrp0cl 
|- ( ph -> sum_ k e. A B e. ( 0 [,) +oo ) )

Proof

Step Hyp Ref Expression
1 fsumrp0cl.1 
 |-  ( ph -> A e. Fin )
2 fsumrp0cl.2 
 |-  ( ( ph /\ k e. A ) -> B e. ( 0 [,) +oo ) )
3 rge0ssre 
 |-  ( 0 [,) +oo ) C_ RR
4 ax-resscn 
 |-  RR C_ CC
5 3 4 sstri 
 |-  ( 0 [,) +oo ) C_ CC
6 5 a1i 
 |-  ( ph -> ( 0 [,) +oo ) C_ CC )
7 simprl 
 |-  ( ( ph /\ ( x e. ( 0 [,) +oo ) /\ y e. ( 0 [,) +oo ) ) ) -> x e. ( 0 [,) +oo ) )
8 3 7 sselid 
 |-  ( ( ph /\ ( x e. ( 0 [,) +oo ) /\ y e. ( 0 [,) +oo ) ) ) -> x e. RR )
9 simprr 
 |-  ( ( ph /\ ( x e. ( 0 [,) +oo ) /\ y e. ( 0 [,) +oo ) ) ) -> y e. ( 0 [,) +oo ) )
10 3 9 sselid 
 |-  ( ( ph /\ ( x e. ( 0 [,) +oo ) /\ y e. ( 0 [,) +oo ) ) ) -> y e. RR )
11 8 10 readdcld 
 |-  ( ( ph /\ ( x e. ( 0 [,) +oo ) /\ y e. ( 0 [,) +oo ) ) ) -> ( x + y ) e. RR )
12 11 rexrd 
 |-  ( ( ph /\ ( x e. ( 0 [,) +oo ) /\ y e. ( 0 [,) +oo ) ) ) -> ( x + y ) e. RR* )
13 0xr 
 |-  0 e. RR*
14 pnfxr 
 |-  +oo e. RR*
15 elico1 
 |-  ( ( 0 e. RR* /\ +oo e. RR* ) -> ( x e. ( 0 [,) +oo ) <-> ( x e. RR* /\ 0 <_ x /\ x < +oo ) ) )
16 13 14 15 mp2an 
 |-  ( x e. ( 0 [,) +oo ) <-> ( x e. RR* /\ 0 <_ x /\ x < +oo ) )
17 16 simp2bi 
 |-  ( x e. ( 0 [,) +oo ) -> 0 <_ x )
18 7 17 syl 
 |-  ( ( ph /\ ( x e. ( 0 [,) +oo ) /\ y e. ( 0 [,) +oo ) ) ) -> 0 <_ x )
19 elico1 
 |-  ( ( 0 e. RR* /\ +oo e. RR* ) -> ( y e. ( 0 [,) +oo ) <-> ( y e. RR* /\ 0 <_ y /\ y < +oo ) ) )
20 13 14 19 mp2an 
 |-  ( y e. ( 0 [,) +oo ) <-> ( y e. RR* /\ 0 <_ y /\ y < +oo ) )
21 20 simp2bi 
 |-  ( y e. ( 0 [,) +oo ) -> 0 <_ y )
22 9 21 syl 
 |-  ( ( ph /\ ( x e. ( 0 [,) +oo ) /\ y e. ( 0 [,) +oo ) ) ) -> 0 <_ y )
23 8 10 18 22 addge0d 
 |-  ( ( ph /\ ( x e. ( 0 [,) +oo ) /\ y e. ( 0 [,) +oo ) ) ) -> 0 <_ ( x + y ) )
24 ltpnf 
 |-  ( ( x + y ) e. RR -> ( x + y ) < +oo )
25 11 24 syl 
 |-  ( ( ph /\ ( x e. ( 0 [,) +oo ) /\ y e. ( 0 [,) +oo ) ) ) -> ( x + y ) < +oo )
26 elico1 
 |-  ( ( 0 e. RR* /\ +oo e. RR* ) -> ( ( x + y ) e. ( 0 [,) +oo ) <-> ( ( x + y ) e. RR* /\ 0 <_ ( x + y ) /\ ( x + y ) < +oo ) ) )
27 13 14 26 mp2an 
 |-  ( ( x + y ) e. ( 0 [,) +oo ) <-> ( ( x + y ) e. RR* /\ 0 <_ ( x + y ) /\ ( x + y ) < +oo ) )
28 12 23 25 27 syl3anbrc 
 |-  ( ( ph /\ ( x e. ( 0 [,) +oo ) /\ y e. ( 0 [,) +oo ) ) ) -> ( x + y ) e. ( 0 [,) +oo ) )
29 0e0icopnf 
 |-  0 e. ( 0 [,) +oo )
30 29 a1i 
 |-  ( ph -> 0 e. ( 0 [,) +oo ) )
31 6 28 1 2 30 fsumcllem 
 |-  ( ph -> sum_ k e. A B e. ( 0 [,) +oo ) )