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

Metamath Proof Explorer

Theorem nn0split

Description: Express the set of nonnegative integers as the disjoint (see nn0disj ) union of the first N + 1 values and the rest. (Contributed by AV, 8-Nov-2019)

Ref Expression
Assertion nn0split ⊢ N ∈ ℕ 0 → ℕ 0 = 0 … N ∪ ℤ ≥ N + 1

Proof

Step Hyp Ref Expression
1 nn0uz ⊢ ℕ 0 = ℤ ≥ 0
2 1 a1i ⊢ N ∈ ℕ 0 → ℕ 0 = ℤ ≥ 0
3 peano2nn0 ⊢ N ∈ ℕ 0 → N + 1 ∈ ℕ 0
4 3 1 eleqtrdi ⊢ N ∈ ℕ 0 → N + 1 ∈ ℤ ≥ 0
5 uzsplit ⊢ N + 1 ∈ ℤ ≥ 0 → ℤ ≥ 0 = 0 … N + 1 - 1 ∪ ℤ ≥ N + 1
6 4 5 syl ⊢ N ∈ ℕ 0 → ℤ ≥ 0 = 0 … N + 1 - 1 ∪ ℤ ≥ N + 1
7 nn0cn ⊢ N ∈ ℕ 0 → N ∈ ℂ
8 pncan1 ⊢ N ∈ ℂ → N + 1 - 1 = N
9 7 8 syl ⊢ N ∈ ℕ 0 → N + 1 - 1 = N
10 9 oveq2d ⊢ N ∈ ℕ 0 → 0 … N + 1 - 1 = 0 … N
11 10 uneq1d ⊢ N ∈ ℕ 0 → 0 … N + 1 - 1 ∪ ℤ ≥ N + 1 = 0 … N ∪ ℤ ≥ N + 1
12 2 6 11 3eqtrd ⊢ N ∈ ℕ 0 → ℕ 0 = 0 … N ∪ ℤ ≥ N + 1