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

Metamath Proof Explorer

Theorem nn0ge2m1nn

Description: If a nonnegative integer is greater than or equal to two, the integer decreased by 1 is a positive integer. (Contributed by Alexander van der Vekens, 1-Aug-2018) (Revised by AV, 4-Jan-2020)

Ref Expression
Assertion nn0ge2m1nn 
|- ( ( N e. NN0 /\ 2 <_ N ) -> ( N - 1 ) e. NN )

Proof

Step Hyp Ref Expression
1 simpl 
 |-  ( ( N e. NN0 /\ 2 <_ N ) -> N e. NN0 )
2 1red 
 |-  ( N e. NN0 -> 1 e. RR )
3 2re 
 |-  2 e. RR
4 3 a1i 
 |-  ( N e. NN0 -> 2 e. RR )
5 nn0re 
 |-  ( N e. NN0 -> N e. RR )
6 2 4 5 3jca 
 |-  ( N e. NN0 -> ( 1 e. RR /\ 2 e. RR /\ N e. RR ) )
7 6 adantr 
 |-  ( ( N e. NN0 /\ 2 <_ N ) -> ( 1 e. RR /\ 2 e. RR /\ N e. RR ) )
8 simpr 
 |-  ( ( N e. NN0 /\ 2 <_ N ) -> 2 <_ N )
9 1lt2 
 |-  1 < 2
10 8 9 jctil 
 |-  ( ( N e. NN0 /\ 2 <_ N ) -> ( 1 < 2 /\ 2 <_ N ) )
11 ltleletr 
 |-  ( ( 1 e. RR /\ 2 e. RR /\ N e. RR ) -> ( ( 1 < 2 /\ 2 <_ N ) -> 1 <_ N ) )
12 7 10 11 sylc 
 |-  ( ( N e. NN0 /\ 2 <_ N ) -> 1 <_ N )
13 elnnnn0c 
 |-  ( N e. NN <-> ( N e. NN0 /\ 1 <_ N ) )
14 1 12 13 sylanbrc 
 |-  ( ( N e. NN0 /\ 2 <_ N ) -> N e. NN )
15 nn1m1nn 
 |-  ( N e. NN -> ( N = 1 \/ ( N - 1 ) e. NN ) )
16 14 15 syl 
 |-  ( ( N e. NN0 /\ 2 <_ N ) -> ( N = 1 \/ ( N - 1 ) e. NN ) )
17 breq2 
 |-  ( N = 1 -> ( 2 <_ N <-> 2 <_ 1 ) )
18 1re 
 |-  1 e. RR
19 18 3 ltnlei 
 |-  ( 1 < 2 <-> -. 2 <_ 1 )
20 pm2.21 
 |-  ( -. 2 <_ 1 -> ( 2 <_ 1 -> ( N - 1 ) e. NN ) )
21 19 20 sylbi 
 |-  ( 1 < 2 -> ( 2 <_ 1 -> ( N - 1 ) e. NN ) )
22 9 21 ax-mp 
 |-  ( 2 <_ 1 -> ( N - 1 ) e. NN )
23 17 22 biimtrdi 
 |-  ( N = 1 -> ( 2 <_ N -> ( N - 1 ) e. NN ) )
24 23 adantld 
 |-  ( N = 1 -> ( ( N e. NN0 /\ 2 <_ N ) -> ( N - 1 ) e. NN ) )
25 ax-1 
 |-  ( ( N - 1 ) e. NN -> ( ( N e. NN0 /\ 2 <_ N ) -> ( N - 1 ) e. NN ) )
26 24 25 jaoi 
 |-  ( ( N = 1 \/ ( N - 1 ) e. NN ) -> ( ( N e. NN0 /\ 2 <_ N ) -> ( N - 1 ) e. NN ) )
27 16 26 mpcom 
 |-  ( ( N e. NN0 /\ 2 <_ N ) -> ( N - 1 ) e. NN )