Metamath Proof Explorer


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 ≤ 𝑁 )