Metamath Proof Explorer

Theorem elnnz1

Description: Positive integer property expressed in terms of integers. (Contributed by NM, 10-May-2004) (Proof shortened by Mario Carneiro, 16-May-2014)

Ref Expression
Assertion elnnz1 
|- ( N e. NN <-> ( N e. ZZ /\ 1 <_ N ) )

Proof

Step Hyp Ref Expression
1 nnz 
 |-  ( N e. NN -> N e. ZZ )
2 nnge1 
 |-  ( N e. NN -> 1 <_ N )
3 1 2 jca 
 |-  ( N e. NN -> ( N e. ZZ /\ 1 <_ N ) )
4 0lt1 
 |-  0 < 1
5 0re 
 |-  0 e. RR
6 1re 
 |-  1 e. RR
7 zre 
 |-  ( N e. ZZ -> N e. RR )
8 ltletr 
 |-  ( ( 0 e. RR /\ 1 e. RR /\ N e. RR ) -> ( ( 0 < 1 /\ 1 <_ N ) -> 0 < N ) )
9 5 6 7 8 mp3an12i 
 |-  ( N e. ZZ -> ( ( 0 < 1 /\ 1 <_ N ) -> 0 < N ) )
10 4 9 mpani 
 |-  ( N e. ZZ -> ( 1 <_ N -> 0 < N ) )
11 10 imdistani 
 |-  ( ( N e. ZZ /\ 1 <_ N ) -> ( N e. ZZ /\ 0 < N ) )
12 elnnz 
 |-  ( N e. NN <-> ( N e. ZZ /\ 0 < N ) )
13 11 12 sylibr 
 |-  ( ( N e. ZZ /\ 1 <_ N ) -> N e. NN )
14 3 13 impbii 
 |-  ( N e. NN <-> ( N e. ZZ /\ 1 <_ N ) )