Metamath Proof Explorer

Theorem sge0rernmpt

Description: If the sum of nonnegative extended reals is not +oo then no term is +oo . (Contributed by Glauco Siliprandi, 11-Oct-2020)

Ref Expression
Hypotheses sge0rernmpt.xph 
|- F/ x ph
sge0rernmpt.a 
|- ( ph -> A e. V )
sge0rernmpt.b 
|- ( ( ph /\ x e. A ) -> B e. ( 0 [,] +oo ) )
sge0rernmpt.re 
|- ( ph -> ( sum^ ` ( x e. A |-> B ) ) e. RR )
Assertion sge0rernmpt 
|- ( ( ph /\ x e. A ) -> B e. ( 0 [,) +oo ) )

Proof

Step Hyp Ref Expression
1 sge0rernmpt.xph 
 |-  F/ x ph
2 sge0rernmpt.a 
 |-  ( ph -> A e. V )
3 sge0rernmpt.b 
 |-  ( ( ph /\ x e. A ) -> B e. ( 0 [,] +oo ) )
4 sge0rernmpt.re 
 |-  ( ph -> ( sum^ ` ( x e. A |-> B ) ) e. RR )
5 0xr 
 |-  0 e. RR*
6 5 a1i 
 |-  ( ( ph /\ x e. A ) -> 0 e. RR* )
7 pnfxr 
 |-  +oo e. RR*
8 7 a1i 
 |-  ( ( ph /\ x e. A ) -> +oo e. RR* )
9 iccssxr 
 |-  ( 0 [,] +oo ) C_ RR*
10 9 3 sselid 
 |-  ( ( ph /\ x e. A ) -> B e. RR* )
11 iccgelb 
 |-  ( ( 0 e. RR* /\ +oo e. RR* /\ B e. ( 0 [,] +oo ) ) -> 0 <_ B )
12 6 8 3 11 syl3anc 
 |-  ( ( ph /\ x e. A ) -> 0 <_ B )
13 simpr 
 |-  ( ( ( ph /\ x e. A ) /\ -. B < +oo ) -> -. B < +oo )
14 nltpnft 
 |-  ( B e. RR* -> ( B = +oo <-> -. B < +oo ) )
15 10 14 syl 
 |-  ( ( ph /\ x e. A ) -> ( B = +oo <-> -. B < +oo ) )
16 15 adantr 
 |-  ( ( ( ph /\ x e. A ) /\ -. B < +oo ) -> ( B = +oo <-> -. B < +oo ) )
17 13 16 mpbird 
 |-  ( ( ( ph /\ x e. A ) /\ -. B < +oo ) -> B = +oo )
18 17 eqcomd 
 |-  ( ( ( ph /\ x e. A ) /\ -. B < +oo ) -> +oo = B )
19 simpr 
 |-  ( ( ph /\ x e. A ) -> x e. A )
20 eqid 
 |-  ( x e. A |-> B ) = ( x e. A |-> B )
21 20 elrnmpt1 
 |-  ( ( x e. A /\ B e. ( 0 [,] +oo ) ) -> B e. ran ( x e. A |-> B ) )
22 19 3 21 syl2anc 
 |-  ( ( ph /\ x e. A ) -> B e. ran ( x e. A |-> B ) )
23 22 adantr 
 |-  ( ( ( ph /\ x e. A ) /\ -. B < +oo ) -> B e. ran ( x e. A |-> B ) )
24 18 23 eqeltrd 
 |-  ( ( ( ph /\ x e. A ) /\ -. B < +oo ) -> +oo e. ran ( x e. A |-> B ) )
25 1 3 20 fmptdf 
 |-  ( ph -> ( x e. A |-> B ) : A --> ( 0 [,] +oo ) )
26 2 25 4 sge0rern 
 |-  ( ph -> -. +oo e. ran ( x e. A |-> B ) )
27 26 ad2antrr 
 |-  ( ( ( ph /\ x e. A ) /\ -. B < +oo ) -> -. +oo e. ran ( x e. A |-> B ) )
28 24 27 condan 
 |-  ( ( ph /\ x e. A ) -> B < +oo )
29 6 8 10 12 28 elicod 
 |-  ( ( ph /\ x e. A ) -> B e. ( 0 [,) +oo ) )