Theorem nn0n0n1ge2

Description: A nonnegative integer which is neither 0 nor 1 is greater than or equal to 2. (Contributed by Alexander van der Vekens, 6-Dec-2017)

	Ref	Expression
Assertion	nn0n0n1ge2	⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑁 ≠ 0 ∧ 𝑁 ≠ 1 ) → 2 ≤ 𝑁 )

Proof

Step	Hyp	Ref	Expression
1		nn0cn	⊢ ( 𝑁 ∈ ℕ0 → 𝑁 ∈ ℂ )
2		1cnd	⊢ ( 𝑁 ∈ ℕ0 → 1 ∈ ℂ )
3	1 2 2	subsub4d	⊢ ( 𝑁 ∈ ℕ0 → ( ( 𝑁 − 1 ) − 1 ) = ( 𝑁 − ( 1 + 1 ) ) )
4		1p1e2	⊢ ( 1 + 1 ) = 2
5	4	oveq2i	⊢ ( 𝑁 − ( 1 + 1 ) ) = ( 𝑁 − 2 )
6	3 5	eqtr2di	⊢ ( 𝑁 ∈ ℕ0 → ( 𝑁 − 2 ) = ( ( 𝑁 − 1 ) − 1 ) )
7	6	3ad2ant1	⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑁 ≠ 0 ∧ 𝑁 ≠ 1 ) → ( 𝑁 − 2 ) = ( ( 𝑁 − 1 ) − 1 ) )
8		3simpa	⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑁 ≠ 0 ∧ 𝑁 ≠ 1 ) → ( 𝑁 ∈ ℕ0 ∧ 𝑁 ≠ 0 ) )
9		elnnne0	⊢ ( 𝑁 ∈ ℕ ↔ ( 𝑁 ∈ ℕ0 ∧ 𝑁 ≠ 0 ) )
10	8 9	sylibr	⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑁 ≠ 0 ∧ 𝑁 ≠ 1 ) → 𝑁 ∈ ℕ )
11		nnm1nn0	⊢ ( 𝑁 ∈ ℕ → ( 𝑁 − 1 ) ∈ ℕ0 )
12	10 11	syl	⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑁 ≠ 0 ∧ 𝑁 ≠ 1 ) → ( 𝑁 − 1 ) ∈ ℕ0 )
13	1 2	subeq0ad	⊢ ( 𝑁 ∈ ℕ0 → ( ( 𝑁 − 1 ) = 0 ↔ 𝑁 = 1 ) )
14	13	biimpd	⊢ ( 𝑁 ∈ ℕ0 → ( ( 𝑁 − 1 ) = 0 → 𝑁 = 1 ) )
15	14	necon3d	⊢ ( 𝑁 ∈ ℕ0 → ( 𝑁 ≠ 1 → ( 𝑁 − 1 ) ≠ 0 ) )
16	15	imp	⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑁 ≠ 1 ) → ( 𝑁 − 1 ) ≠ 0 )
17	16	3adant2	⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑁 ≠ 0 ∧ 𝑁 ≠ 1 ) → ( 𝑁 − 1 ) ≠ 0 )
18		elnnne0	⊢ ( ( 𝑁 − 1 ) ∈ ℕ ↔ ( ( 𝑁 − 1 ) ∈ ℕ0 ∧ ( 𝑁 − 1 ) ≠ 0 ) )
19	12 17 18	sylanbrc	⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑁 ≠ 0 ∧ 𝑁 ≠ 1 ) → ( 𝑁 − 1 ) ∈ ℕ )
20		nnm1nn0	⊢ ( ( 𝑁 − 1 ) ∈ ℕ → ( ( 𝑁 − 1 ) − 1 ) ∈ ℕ0 )
21	19 20	syl	⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑁 ≠ 0 ∧ 𝑁 ≠ 1 ) → ( ( 𝑁 − 1 ) − 1 ) ∈ ℕ0 )
22	7 21	eqeltrd	⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑁 ≠ 0 ∧ 𝑁 ≠ 1 ) → ( 𝑁 − 2 ) ∈ ℕ0 )
23		2nn0	⊢ 2 ∈ ℕ0
24	23	jctl	⊢ ( 𝑁 ∈ ℕ0 → ( 2 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ) )
25	24	3ad2ant1	⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑁 ≠ 0 ∧ 𝑁 ≠ 1 ) → ( 2 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ) )
26		nn0sub	⊢ ( ( 2 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ) → ( 2 ≤ 𝑁 ↔ ( 𝑁 − 2 ) ∈ ℕ0 ) )
27	25 26	syl	⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑁 ≠ 0 ∧ 𝑁 ≠ 1 ) → ( 2 ≤ 𝑁 ↔ ( 𝑁 − 2 ) ∈ ℕ0 ) )
28	22 27	mpbird	⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑁 ≠ 0 ∧ 𝑁 ≠ 1 ) → 2 ≤ 𝑁 )