Metamath Proof Explorer


Theorem elznn

Description: Integer property expressed in terms of positive integers and nonnegative integers. (Contributed by NM, 12-Jul-2005)

Ref Expression
Assertion elznn N N N N 0

Proof

Step Hyp Ref Expression
1 elz N N N = 0 N N
2 3orrot N = 0 N N N N N = 0
3 3orass N N N = 0 N N N = 0
4 2 3 bitri N = 0 N N N N N = 0
5 elnn0 N 0 N N = 0
6 recn N N
7 6 negeq0d N N = 0 N = 0
8 7 orbi2d N N N = 0 N N = 0
9 5 8 bitr4id N N 0 N N = 0
10 9 orbi2d N N N 0 N N N = 0
11 4 10 bitr4id N N = 0 N N N N 0
12 11 pm5.32i N N = 0 N N N N N 0
13 1 12 bitri N N N N 0