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

Metamath Proof Explorer

Theorem xnn0n0n1ge2b

Description: An extended nonnegative integer is neither 0 nor 1 if and only if it is greater than or equal to 2. (Contributed by AV, 5-Apr-2021)

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

Proof

Step Hyp Ref Expression
1 elxnn0 ⊢ ( 𝑁 ∈ ℕ0* ↔ ( 𝑁 ∈ ℕ0 ∨ 𝑁 = +∞ ) )
2 nn0n0n1ge2b ⊢ ( 𝑁 ∈ ℕ0 → ( ( 𝑁 ≠ 0 ∧ 𝑁 ≠ 1 ) ↔ 2 ≤ 𝑁 ) )
3 0nn0 ⊢ 0 ∈ ℕ0
4 nn0nepnf ⊢ ( 0 ∈ ℕ0 → 0 ≠ +∞ )
5 3 4 ax-mp ⊢ 0 ≠ +∞
6 5 necomi ⊢ +∞ ≠ 0
7 neeq1 ⊢ ( 𝑁 = +∞ → ( 𝑁 ≠ 0 ↔ +∞ ≠ 0 ) )
8 6 7 mpbiri ⊢ ( 𝑁 = +∞ → 𝑁 ≠ 0 )
9 1nn0 ⊢ 1 ∈ ℕ0
10 nn0nepnf ⊢ ( 1 ∈ ℕ0 → 1 ≠ +∞ )
11 9 10 ax-mp ⊢ 1 ≠ +∞
12 11 necomi ⊢ +∞ ≠ 1
13 neeq1 ⊢ ( 𝑁 = +∞ → ( 𝑁 ≠ 1 ↔ +∞ ≠ 1 ) )
14 12 13 mpbiri ⊢ ( 𝑁 = +∞ → 𝑁 ≠ 1 )
15 8 14 jca ⊢ ( 𝑁 = +∞ → ( 𝑁 ≠ 0 ∧ 𝑁 ≠ 1 ) )
16 2re ⊢ 2 ∈ ℝ
17 16 rexri ⊢ 2 ∈ ℝ*
18 pnfge ⊢ ( 2 ∈ ℝ* → 2 ≤ +∞ )
19 17 18 ax-mp ⊢ 2 ≤ +∞
20 breq2 ⊢ ( 𝑁 = +∞ → ( 2 ≤ 𝑁 ↔ 2 ≤ +∞ ) )
21 19 20 mpbiri ⊢ ( 𝑁 = +∞ → 2 ≤ 𝑁 )
22 15 21 2thd ⊢ ( 𝑁 = +∞ → ( ( 𝑁 ≠ 0 ∧ 𝑁 ≠ 1 ) ↔ 2 ≤ 𝑁 ) )
23 2 22 jaoi ⊢ ( ( 𝑁 ∈ ℕ0 ∨ 𝑁 = +∞ ) → ( ( 𝑁 ≠ 0 ∧ 𝑁 ≠ 1 ) ↔ 2 ≤ 𝑁 ) )
24 1 23 sylbi ⊢ ( 𝑁 ∈ ℕ0* → ( ( 𝑁 ≠ 0 ∧ 𝑁 ≠ 1 ) ↔ 2 ≤ 𝑁 ) )