Metamath Proof Explorer

Theorem eluz2b2

Description: Two ways to say "an integer greater than or equal to 2". (Contributed by Paul Chapman, 23-Nov-2012)

Ref Expression
Assertion eluz2b2 
|- ( N e. ( ZZ>= ` 2 ) <-> ( N e. NN /\ 1 < N ) )

Proof

Step Hyp Ref Expression
1 eluz2b1 
 |-  ( N e. ( ZZ>= ` 2 ) <-> ( N e. ZZ /\ 1 < N ) )
2 1re 
 |-  1 e. RR
3 zre 
 |-  ( N e. ZZ -> N e. RR )
4 ltle 
 |-  ( ( 1 e. RR /\ N e. RR ) -> ( 1 < N -> 1 <_ N ) )
5 2 3 4 sylancr 
 |-  ( N e. ZZ -> ( 1 < N -> 1 <_ N ) )
6 5 imdistani 
 |-  ( ( N e. ZZ /\ 1 < N ) -> ( N e. ZZ /\ 1 <_ N ) )
7 elnnz1 
 |-  ( N e. NN <-> ( N e. ZZ /\ 1 <_ N ) )
8 6 7 sylibr 
 |-  ( ( N e. ZZ /\ 1 < N ) -> N e. NN )
9 simpr 
 |-  ( ( N e. ZZ /\ 1 < N ) -> 1 < N )
10 8 9 jca 
 |-  ( ( N e. ZZ /\ 1 < N ) -> ( N e. NN /\ 1 < N ) )
11 nnz 
 |-  ( N e. NN -> N e. ZZ )
12 11 anim1i 
 |-  ( ( N e. NN /\ 1 < N ) -> ( N e. ZZ /\ 1 < N ) )
13 10 12 impbii 
 |-  ( ( N e. ZZ /\ 1 < N ) <-> ( N e. NN /\ 1 < N ) )
14 1 13 bitri 
 |-  ( N e. ( ZZ>= ` 2 ) <-> ( N e. NN /\ 1 < N ) )