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