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