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 ( 𝑁 ∈ ℕ → ℕ = ( ( 1 ... 𝑁 ) ∪ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ) )

Proof

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