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 )