Metamath Proof Explorer

Theorem xnn0xrnemnf

Description: The extended nonnegative integers are extended reals without negative infinity. (Contributed by AV, 10-Dec-2020)

Ref Expression
Assertion xnn0xrnemnf 
|- ( A e. NN0* -> ( A e. RR* /\ A =/= -oo ) )

Proof

Step Hyp Ref Expression
1 xnn0xr 
 |-  ( A e. NN0* -> A e. RR* )
2 xnn0nemnf 
 |-  ( A e. NN0* -> A =/= -oo )
3 1 2 jca 
 |-  ( A e. NN0* -> ( A e. RR* /\ A =/= -oo ) )