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

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