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 ) )