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 ) )