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