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

Metamath Proof Explorer

Theorem xnn0xrge0

Description: An extended nonnegative integer is an extended nonnegative real. (Contributed by AV, 10-Dec-2020)

Ref Expression
Assertion xnn0xrge0 
|- ( A e. NN0* -> A e. ( 0 [,] +oo ) )

Proof

Step Hyp Ref Expression
1 elxnn0 
 |-  ( A e. NN0* <-> ( A e. NN0 \/ A = +oo ) )
2 nn0re 
 |-  ( A e. NN0 -> A e. RR )
3 2 rexrd 
 |-  ( A e. NN0 -> A e. RR* )
4 nn0ge0 
 |-  ( A e. NN0 -> 0 <_ A )
5 elxrge0 
 |-  ( A e. ( 0 [,] +oo ) <-> ( A e. RR* /\ 0 <_ A ) )
6 3 4 5 sylanbrc 
 |-  ( A e. NN0 -> A e. ( 0 [,] +oo ) )
7 0xr 
 |-  0 e. RR*
8 pnfxr 
 |-  +oo e. RR*
9 0lepnf 
 |-  0 <_ +oo
10 ubicc2 
 |-  ( ( 0 e. RR* /\ +oo e. RR* /\ 0 <_ +oo ) -> +oo e. ( 0 [,] +oo ) )
11 7 8 9 10 mp3an 
 |-  +oo e. ( 0 [,] +oo )
12 eleq1 
 |-  ( A = +oo -> ( A e. ( 0 [,] +oo ) <-> +oo e. ( 0 [,] +oo ) ) )
13 11 12 mpbiri 
 |-  ( A = +oo -> A e. ( 0 [,] +oo ) )
14 6 13 jaoi 
 |-  ( ( A e. NN0 \/ A = +oo ) -> A e. ( 0 [,] +oo ) )
15 1 14 sylbi 
 |-  ( A e. NN0* -> A e. ( 0 [,] +oo ) )