Metamath Proof Explorer

Theorem elnnnn0

Description: The positive integer property expressed in terms of nonnegative integers. (Contributed by NM, 10-May-2004)

Ref Expression
Assertion elnnnn0 
|- ( N e. NN <-> ( N e. CC /\ ( N - 1 ) e. NN0 ) )

Proof

Step Hyp Ref Expression
1 nncn 
 |-  ( N e. NN -> N e. CC )
2 npcan1 
 |-  ( N e. CC -> ( ( N - 1 ) + 1 ) = N )
3 2 eleq1d 
 |-  ( N e. CC -> ( ( ( N - 1 ) + 1 ) e. NN <-> N e. NN ) )
4 peano2cnm 
 |-  ( N e. CC -> ( N - 1 ) e. CC )
5 4 biantrurd 
 |-  ( N e. CC -> ( ( ( N - 1 ) + 1 ) e. NN <-> ( ( N - 1 ) e. CC /\ ( ( N - 1 ) + 1 ) e. NN ) ) )
6 3 5 bitr3d 
 |-  ( N e. CC -> ( N e. NN <-> ( ( N - 1 ) e. CC /\ ( ( N - 1 ) + 1 ) e. NN ) ) )
7 elnn0nn 
 |-  ( ( N - 1 ) e. NN0 <-> ( ( N - 1 ) e. CC /\ ( ( N - 1 ) + 1 ) e. NN ) )
8 6 7 bitr4di 
 |-  ( N e. CC -> ( N e. NN <-> ( N - 1 ) e. NN0 ) )
9 1 8 biadanii 
 |-  ( N e. NN <-> ( N e. CC /\ ( N - 1 ) e. NN0 ) )