Metamath Proof Explorer


Theorem elznn0

Description: Integer property expressed in terms of nonnegative integers. (Contributed by NM, 9-May-2004)

Ref Expression
Assertion elznn0 N N N 0 N 0

Proof

Step Hyp Ref Expression
1 elz N N N = 0 N N
2 elnn0 N 0 N N = 0
3 2 a1i N N 0 N N = 0
4 elnn0 N 0 N N = 0
5 recn N N
6 0cn 0
7 negcon1 N 0 N = 0 0 = N
8 5 6 7 sylancl N N = 0 0 = N
9 neg0 0 = 0
10 9 eqeq1i 0 = N 0 = N
11 eqcom 0 = N N = 0
12 10 11 bitri 0 = N N = 0
13 8 12 bitrdi N N = 0 N = 0
14 13 orbi2d N N N = 0 N N = 0
15 4 14 syl5bb N N 0 N N = 0
16 3 15 orbi12d N N 0 N 0 N N = 0 N N = 0
17 3orass N = 0 N N N = 0 N N
18 orcom N = 0 N N N N N = 0
19 orordir N N N = 0 N N = 0 N N = 0
20 17 18 19 3bitrri N N = 0 N N = 0 N = 0 N N
21 16 20 bitr2di N N = 0 N N N 0 N 0
22 21 pm5.32i N N = 0 N N N N 0 N 0
23 1 22 bitri N N N 0 N 0