Metamath Proof Explorer

Theorem nn0n0n1ge2b

Description: A nonnegative integer is neither 0 nor 1 if and only if it is greater than or equal to 2. (Contributed by Alexander van der Vekens, 17-Jan-2018)

Ref Expression
Assertion nn0n0n1ge2b ( 𝑁 ∈ ℕ0 → ( ( 𝑁 ≠ 0 ∧ 𝑁 ≠ 1 ) ↔ 2 ≤ 𝑁 ) )

Proof

Step Hyp Ref Expression
1 nn0n0n1ge2 ⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑁 ≠ 0 ∧ 𝑁 ≠ 1 ) → 2 ≤ 𝑁 )
2 1 3expib ⊢ ( 𝑁 ∈ ℕ0 → ( ( 𝑁 ≠ 0 ∧ 𝑁 ≠ 1 ) → 2 ≤ 𝑁 ) )
3 ianor ⊢ ( ¬ ( 𝑁 ≠ 0 ∧ 𝑁 ≠ 1 ) ↔ ( ¬ 𝑁 ≠ 0 ∨ ¬ 𝑁 ≠ 1 ) )
4 nne ⊢ ( ¬ 𝑁 ≠ 0 ↔ 𝑁 = 0 )
5 nne ⊢ ( ¬ 𝑁 ≠ 1 ↔ 𝑁 = 1 )
6 4 5 orbi12i ⊢ ( ( ¬ 𝑁 ≠ 0 ∨ ¬ 𝑁 ≠ 1 ) ↔ ( 𝑁 = 0 ∨ 𝑁 = 1 ) )
7 3 6 bitri ⊢ ( ¬ ( 𝑁 ≠ 0 ∧ 𝑁 ≠ 1 ) ↔ ( 𝑁 = 0 ∨ 𝑁 = 1 ) )
8 2pos ⊢ 0 < 2
9 breq1 ⊢ ( 𝑁 = 0 → ( 𝑁 < 2 ↔ 0 < 2 ) )
10 8 9 mpbiri ⊢ ( 𝑁 = 0 → 𝑁 < 2 )
11 10 a1d ⊢ ( 𝑁 = 0 → ( 𝑁 ∈ ℕ0 → 𝑁 < 2 ) )
12 1lt2 ⊢ 1 < 2
13 breq1 ⊢ ( 𝑁 = 1 → ( 𝑁 < 2 ↔ 1 < 2 ) )
14 12 13 mpbiri ⊢ ( 𝑁 = 1 → 𝑁 < 2 )
15 14 a1d ⊢ ( 𝑁 = 1 → ( 𝑁 ∈ ℕ0 → 𝑁 < 2 ) )
16 11 15 jaoi ⊢ ( ( 𝑁 = 0 ∨ 𝑁 = 1 ) → ( 𝑁 ∈ ℕ0 → 𝑁 < 2 ) )
17 16 impcom ⊢ ( ( 𝑁 ∈ ℕ0 ∧ ( 𝑁 = 0 ∨ 𝑁 = 1 ) ) → 𝑁 < 2 )
18 nn0re ⊢ ( 𝑁 ∈ ℕ0 → 𝑁 ∈ ℝ )
19 2re ⊢ 2 ∈ ℝ
20 18 19 jctir ⊢ ( 𝑁 ∈ ℕ0 → ( 𝑁 ∈ ℝ ∧ 2 ∈ ℝ ) )
21 20 adantr ⊢ ( ( 𝑁 ∈ ℕ0 ∧ ( 𝑁 = 0 ∨ 𝑁 = 1 ) ) → ( 𝑁 ∈ ℝ ∧ 2 ∈ ℝ ) )
22 ltnle ⊢ ( ( 𝑁 ∈ ℝ ∧ 2 ∈ ℝ ) → ( 𝑁 < 2 ↔ ¬ 2 ≤ 𝑁 ) )
23 21 22 syl ⊢ ( ( 𝑁 ∈ ℕ0 ∧ ( 𝑁 = 0 ∨ 𝑁 = 1 ) ) → ( 𝑁 < 2 ↔ ¬ 2 ≤ 𝑁 ) )
24 17 23 mpbid ⊢ ( ( 𝑁 ∈ ℕ0 ∧ ( 𝑁 = 0 ∨ 𝑁 = 1 ) ) → ¬ 2 ≤ 𝑁 )
25 24 ex ⊢ ( 𝑁 ∈ ℕ0 → ( ( 𝑁 = 0 ∨ 𝑁 = 1 ) → ¬ 2 ≤ 𝑁 ) )
26 7 25 biimtrid ⊢ ( 𝑁 ∈ ℕ0 → ( ¬ ( 𝑁 ≠ 0 ∧ 𝑁 ≠ 1 ) → ¬ 2 ≤ 𝑁 ) )
27 2 26 impcon4bid ⊢ ( 𝑁 ∈ ℕ0 → ( ( 𝑁 ≠ 0 ∧ 𝑁 ≠ 1 ) ↔ 2 ≤ 𝑁 ) )