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

Metamath Proof Explorer

Theorem fzo0sn0fzo1

Description: A half-open range of nonnegative integers is the union of the singleton set containing 0 and a half-open range of positive integers. (Contributed by Alexander van der Vekens, 18-May-2018)

Ref Expression
Assertion fzo0sn0fzo1 ( 𝑁 ∈ ℕ → ( 0 ..^ 𝑁 ) = ( { 0 } ∪ ( 1 ..^ 𝑁 ) ) )

Proof

Step Hyp Ref Expression
1 1nn0 ⊢ 1 ∈ ℕ0
2 1 a1i ⊢ ( 𝑁 ∈ ℕ → 1 ∈ ℕ0 )
3 nnnn0 ⊢ ( 𝑁 ∈ ℕ → 𝑁 ∈ ℕ0 )
4 nnge1 ⊢ ( 𝑁 ∈ ℕ → 1 ≤ 𝑁 )
5 elfz2nn0 ⊢ ( 1 ∈ ( 0 ... 𝑁 ) ↔ ( 1 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ∧ 1 ≤ 𝑁 ) )
6 2 3 4 5 syl3anbrc ⊢ ( 𝑁 ∈ ℕ → 1 ∈ ( 0 ... 𝑁 ) )
7 fzosplit ⊢ ( 1 ∈ ( 0 ... 𝑁 ) → ( 0 ..^ 𝑁 ) = ( ( 0 ..^ 1 ) ∪ ( 1 ..^ 𝑁 ) ) )
8 6 7 syl ⊢ ( 𝑁 ∈ ℕ → ( 0 ..^ 𝑁 ) = ( ( 0 ..^ 1 ) ∪ ( 1 ..^ 𝑁 ) ) )
9 fzo01 ⊢ ( 0 ..^ 1 ) = { 0 }
10 9 a1i ⊢ ( 𝑁 ∈ ℕ → ( 0 ..^ 1 ) = { 0 } )
11 10 uneq1d ⊢ ( 𝑁 ∈ ℕ → ( ( 0 ..^ 1 ) ∪ ( 1 ..^ 𝑁 ) ) = ( { 0 } ∪ ( 1 ..^ 𝑁 ) ) )
12 8 11 eqtrd ⊢ ( 𝑁 ∈ ℕ → ( 0 ..^ 𝑁 ) = ( { 0 } ∪ ( 1 ..^ 𝑁 ) ) )