Theorem uz3m2nn

Description: An integer greater than or equal to 3 decreased by 2 is a positive integer, analogous to uz2m1nn . (Contributed by Alexander van der Vekens, 17-Sep-2018)

	Ref	Expression
Assertion	uz3m2nn	|- ( N e. ( ZZ>= ` 3 ) -> ( N - 2 ) e. NN )

Proof

Step	Hyp	Ref	Expression
1		eluz2	|- ( N e. ( ZZ>= ` 3 ) <-> ( 3 e. ZZ /\ N e. ZZ /\ 3 <_ N ) )
2		2lt3	|- 2 < 3
3		2re	|- 2 e. RR
4		3re	|- 3 e. RR
5		zre	|- ( N e. ZZ -> N e. RR )
6		ltletr	|- ( ( 2 e. RR /\ 3 e. RR /\ N e. RR ) -> ( ( 2 < 3 /\ 3 <_ N ) -> 2 < N ) )
7	3 4 5 6	mp3an12i	|- ( N e. ZZ -> ( ( 2 < 3 /\ 3 <_ N ) -> 2 < N ) )
8	2 7	mpani	|- ( N e. ZZ -> ( 3 <_ N -> 2 < N ) )
9	8	imp	|- ( ( N e. ZZ /\ 3 <_ N ) -> 2 < N )
10	9	3adant1	|- ( ( 3 e. ZZ /\ N e. ZZ /\ 3 <_ N ) -> 2 < N )
11	1 10	sylbi	|- ( N e. ( ZZ>= ` 3 ) -> 2 < N )
12		2nn	|- 2 e. NN
13		eluzge3nn	|- ( N e. ( ZZ>= ` 3 ) -> N e. NN )
14		nnsub	|- ( ( 2 e. NN /\ N e. NN ) -> ( 2 < N <-> ( N - 2 ) e. NN ) )
15	12 13 14	sylancr	|- ( N e. ( ZZ>= ` 3 ) -> ( 2 < N <-> ( N - 2 ) e. NN ) )
16	11 15	mpbid	|- ( N e. ( ZZ>= ` 3 ) -> ( N - 2 ) e. NN )