Metamath Proof Explorer

Theorem xnn0nemnf

Description: No extended nonnegative integer equals negative infinity. (Contributed by AV, 10-Dec-2020)

Ref Expression
Assertion xnn0nemnf 
|- ( A e. NN0* -> A =/= -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 renemnfd 
 |-  ( A e. NN0 -> A =/= -oo )
4 pnfnemnf 
 |-  +oo =/= -oo
5 neeq1 
 |-  ( A = +oo -> ( A =/= -oo <-> +oo =/= -oo ) )
6 4 5 mpbiri 
 |-  ( A = +oo -> A =/= -oo )
7 3 6 jaoi 
 |-  ( ( A e. NN0 \/ A = +oo ) -> A =/= -oo )
8 1 7 sylbi 
 |-  ( A e. NN0* -> A =/= -oo )