Metamath Proof Explorer


Theorem reelznn0nn

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

Ref Expression
Assertion reelznn0nn N N 0 N 0 - N

Proof

Step Hyp Ref Expression
1 elznn0nn N N 0 N N
2 df-neg N = 0 N
3 0re 0
4 resubeqsub 0 N 0 - N = 0 N
5 3 4 mpan N 0 - N = 0 N
6 2 5 eqtr4id N N = 0 - N
7 6 eleq1d N N 0 - N
8 7 pm5.32i N N N 0 - N
9 8 orbi2i N 0 N N N 0 N 0 - N
10 1 9 bitri N N 0 N 0 - N