Metamath Proof Explorer


Theorem xnn0xr

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

Ref Expression
Assertion xnn0xr
|- ( A e. NN0* -> A e. RR* )

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 pnfxr
 |-  +oo e. RR*
5 eleq1
 |-  ( A = +oo -> ( A e. RR* <-> +oo e. RR* ) )
6 4 5 mpbiri
 |-  ( A = +oo -> A e. RR* )
7 3 6 jaoi
 |-  ( ( A e. NN0 \/ A = +oo ) -> A e. RR* )
8 1 7 sylbi
 |-  ( A e. NN0* -> A e. RR* )