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

Metamath Proof Explorer

Theorem nnsplit

Description: Express the set of positive integers as the disjoint (see nnuzdisj ) union of the first N values and the rest. (Contributed by Glauco Siliprandi, 21-Nov-2020)

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

Proof

Step Hyp Ref Expression
1 nnuz ⊢ ℕ = ℤ ≥ 1
2 1 a1i ⊢ N ∈ ℕ → ℕ = ℤ ≥ 1
3 peano2nn ⊢ N ∈ ℕ → N + 1 ∈ ℕ
4 3 1 eleqtrdi ⊢ N ∈ ℕ → N + 1 ∈ ℤ ≥ 1
5 uzsplit ⊢ N + 1 ∈ ℤ ≥ 1 → ℤ ≥ 1 = 1 … N + 1 - 1 ∪ ℤ ≥ N + 1
6 4 5 syl ⊢ N ∈ ℕ → ℤ ≥ 1 = 1 … N + 1 - 1 ∪ ℤ ≥ N + 1
7 nncn ⊢ N ∈ ℕ → N ∈ ℂ
8 1cnd ⊢ N ∈ ℕ → 1 ∈ ℂ
9 7 8 pncand ⊢ N ∈ ℕ → N + 1 - 1 = N
10 9 oveq2d ⊢ N ∈ ℕ → 1 … N + 1 - 1 = 1 … N
11 10 uneq1d ⊢ N ∈ ℕ → 1 … N + 1 - 1 ∪ ℤ ≥ N + 1 = 1 … N ∪ ℤ ≥ N + 1
12 2 6 11 3eqtrd ⊢ N ∈ ℕ → ℕ = 1 … N ∪ ℤ ≥ N + 1