Metamath Proof Explorer


Theorem eluz2b1

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

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

Proof

Step Hyp Ref Expression
1 2z
 |-  2 e. ZZ
2 1 eluz1i
 |-  ( N e. ( ZZ>= ` 2 ) <-> ( N e. ZZ /\ 2 <_ N ) )
3 1z
 |-  1 e. ZZ
4 zltp1le
 |-  ( ( 1 e. ZZ /\ N e. ZZ ) -> ( 1 < N <-> ( 1 + 1 ) <_ N ) )
5 3 4 mpan
 |-  ( N e. ZZ -> ( 1 < N <-> ( 1 + 1 ) <_ N ) )
6 df-2
 |-  2 = ( 1 + 1 )
7 6 breq1i
 |-  ( 2 <_ N <-> ( 1 + 1 ) <_ N )
8 5 7 bitr4di
 |-  ( N e. ZZ -> ( 1 < N <-> 2 <_ N ) )
9 8 pm5.32i
 |-  ( ( N e. ZZ /\ 1 < N ) <-> ( N e. ZZ /\ 2 <_ N ) )
10 2 9 bitr4i
 |-  ( N e. ( ZZ>= ` 2 ) <-> ( N e. ZZ /\ 1 < N ) )