This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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