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

Metamath Proof Explorer

Theorem nn0split01

Description: Split 0 and 1 from the nonnegative integers. (Contributed by Thierry Arnoux, 8-Jun-2025)

Ref Expression
Assertion nn0split01 ⊢ ℕ 0 = 0 1 ∪ ℤ ≥ 2

Proof

Step Hyp Ref Expression
1 nn0uz ⊢ ℕ 0 = ℤ ≥ 0
2 2eluzge0 ⊢ 2 ∈ ℤ ≥ 0
3 fzouzsplit ⊢ 2 ∈ ℤ ≥ 0 → ℤ ≥ 0 = 0 ..^ 2 ∪ ℤ ≥ 2
4 2 3 ax-mp ⊢ ℤ ≥ 0 = 0 ..^ 2 ∪ ℤ ≥ 2
5 fzo0to2pr ⊢ 0 ..^ 2 = 0 1
6 5 uneq1i ⊢ 0 ..^ 2 ∪ ℤ ≥ 2 = 0 1 ∪ ℤ ≥ 2
7 1 4 6 3eqtri ⊢ ℕ 0 = 0 1 ∪ ℤ ≥ 2