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

Metamath Proof Explorer

Theorem fz0sn0fz1

Description: A finite set of sequential nonnegative integers is the union of the singleton containing 0 and a finite set of sequential positive integers. (Contributed by AV, 20-Mar-2021)

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

Proof

Step Hyp Ref Expression
1 0elfz ⊢ ( 𝑁 ∈ ℕ0 → 0 ∈ ( 0 ... 𝑁 ) )
2 fzsplit ⊢ ( 0 ∈ ( 0 ... 𝑁 ) → ( 0 ... 𝑁 ) = ( ( 0 ... 0 ) ∪ ( ( 0 + 1 ) ... 𝑁 ) ) )
3 0p1e1 ⊢ ( 0 + 1 ) = 1
4 3 oveq1i ⊢ ( ( 0 + 1 ) ... 𝑁 ) = ( 1 ... 𝑁 )
5 4 uneq2i ⊢ ( ( 0 ... 0 ) ∪ ( ( 0 + 1 ) ... 𝑁 ) ) = ( ( 0 ... 0 ) ∪ ( 1 ... 𝑁 ) )
6 2 5 eqtrdi ⊢ ( 0 ∈ ( 0 ... 𝑁 ) → ( 0 ... 𝑁 ) = ( ( 0 ... 0 ) ∪ ( 1 ... 𝑁 ) ) )
7 1 6 syl ⊢ ( 𝑁 ∈ ℕ0 → ( 0 ... 𝑁 ) = ( ( 0 ... 0 ) ∪ ( 1 ... 𝑁 ) ) )
8 0z ⊢ 0 ∈ ℤ
9 fzsn ⊢ ( 0 ∈ ℤ → ( 0 ... 0 ) = { 0 } )
10 8 9 mp1i ⊢ ( 𝑁 ∈ ℕ0 → ( 0 ... 0 ) = { 0 } )
11 10 uneq1d ⊢ ( 𝑁 ∈ ℕ0 → ( ( 0 ... 0 ) ∪ ( 1 ... 𝑁 ) ) = ( { 0 } ∪ ( 1 ... 𝑁 ) ) )
12 7 11 eqtrd ⊢ ( 𝑁 ∈ ℕ0 → ( 0 ... 𝑁 ) = ( { 0 } ∪ ( 1 ... 𝑁 ) ) )