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

Metamath Proof Explorer

Theorem xnn0le2is012

Description: An extended nonnegative integer which is less than or equal to 2 is either 0 or 1 or 2. (Contributed by AV, 24-Nov-2021)

Ref Expression
Assertion xnn0le2is012 ⊢ N ∈ ℕ 0 * ∧ N ≤ 2 → N = 0 ∨ N = 1 ∨ N = 2

Proof

Step Hyp Ref Expression
1 2nn0 ⊢ 2 ∈ ℕ 0
2 xnn0lenn0nn0 ⊢ N ∈ ℕ 0 * ∧ 2 ∈ ℕ 0 ∧ N ≤ 2 → N ∈ ℕ 0
3 1 2 mp3an2 ⊢ N ∈ ℕ 0 * ∧ N ≤ 2 → N ∈ ℕ 0
4 nn0le2is012 ⊢ N ∈ ℕ 0 ∧ N ≤ 2 → N = 0 ∨ N = 1 ∨ N = 2
5 3 4 sylancom ⊢ N ∈ ℕ 0 * ∧ N ≤ 2 → N = 0 ∨ N = 1 ∨ N = 2