Metamath Proof Explorer

Theorem ge0xrre

Description: A nonnegative extended real that is not +oo is a real. (Contributed by Glauco Siliprandi, 17-Aug-2020)

Ref Expression
Assertion ge0xrre 
|- ( ( A e. ( 0 [,] +oo ) /\ A =/= +oo ) -> A e. RR )

Proof

Step Hyp Ref Expression
1 rge0ssre 
 |-  ( 0 [,) +oo ) C_ RR
2 0xr 
 |-  0 e. RR*
3 2 a1i 
 |-  ( ( A e. ( 0 [,] +oo ) /\ A =/= +oo ) -> 0 e. RR* )
4 pnfxr 
 |-  +oo e. RR*
5 4 a1i 
 |-  ( ( A e. ( 0 [,] +oo ) /\ A =/= +oo ) -> +oo e. RR* )
6 eliccxr 
 |-  ( A e. ( 0 [,] +oo ) -> A e. RR* )
7 6 adantr 
 |-  ( ( A e. ( 0 [,] +oo ) /\ A =/= +oo ) -> A e. RR* )
8 2 a1i 
 |-  ( A e. ( 0 [,] +oo ) -> 0 e. RR* )
9 4 a1i 
 |-  ( A e. ( 0 [,] +oo ) -> +oo e. RR* )
10 id 
 |-  ( A e. ( 0 [,] +oo ) -> A e. ( 0 [,] +oo ) )
11 iccgelb 
 |-  ( ( 0 e. RR* /\ +oo e. RR* /\ A e. ( 0 [,] +oo ) ) -> 0 <_ A )
12 8 9 10 11 syl3anc 
 |-  ( A e. ( 0 [,] +oo ) -> 0 <_ A )
13 12 adantr 
 |-  ( ( A e. ( 0 [,] +oo ) /\ A =/= +oo ) -> 0 <_ A )
14 pnfge 
 |-  ( A e. RR* -> A <_ +oo )
15 6 14 syl 
 |-  ( A e. ( 0 [,] +oo ) -> A <_ +oo )
16 15 adantr 
 |-  ( ( A e. ( 0 [,] +oo ) /\ A =/= +oo ) -> A <_ +oo )
17 simpr 
 |-  ( ( A e. ( 0 [,] +oo ) /\ A =/= +oo ) -> A =/= +oo )
18 7 5 16 17 xrleneltd 
 |-  ( ( A e. ( 0 [,] +oo ) /\ A =/= +oo ) -> A < +oo )
19 3 5 7 13 18 elicod 
 |-  ( ( A e. ( 0 [,] +oo ) /\ A =/= +oo ) -> A e. ( 0 [,) +oo ) )
20 1 19 sselid 
 |-  ( ( A e. ( 0 [,] +oo ) /\ A =/= +oo ) -> A e. RR )