Metamath Proof Explorer


Theorem reelznn0nn

Description: elznn0nn restated using df-resub . (Contributed by SN, 25-Jan-2025)

Ref Expression
Assertion reelznn0nn
|- ( N e. ZZ <-> ( N e. NN0 \/ ( N e. RR /\ ( 0 -R N ) e. NN ) ) )

Proof

Step Hyp Ref Expression
1 elznn0nn
 |-  ( N e. ZZ <-> ( N e. NN0 \/ ( N e. RR /\ -u N e. NN ) ) )
2 df-neg
 |-  -u N = ( 0 - N )
3 0re
 |-  0 e. RR
4 resubeqsub
 |-  ( ( 0 e. RR /\ N e. RR ) -> ( 0 -R N ) = ( 0 - N ) )
5 3 4 mpan
 |-  ( N e. RR -> ( 0 -R N ) = ( 0 - N ) )
6 2 5 eqtr4id
 |-  ( N e. RR -> -u N = ( 0 -R N ) )
7 6 eleq1d
 |-  ( N e. RR -> ( -u N e. NN <-> ( 0 -R N ) e. NN ) )
8 7 pm5.32i
 |-  ( ( N e. RR /\ -u N e. NN ) <-> ( N e. RR /\ ( 0 -R N ) e. NN ) )
9 8 orbi2i
 |-  ( ( N e. NN0 \/ ( N e. RR /\ -u N e. NN ) ) <-> ( N e. NN0 \/ ( N e. RR /\ ( 0 -R N ) e. NN ) ) )
10 1 9 bitri
 |-  ( N e. ZZ <-> ( N e. NN0 \/ ( N e. RR /\ ( 0 -R N ) e. NN ) ) )