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 ⊢ N ∈ ℕ → 0 ..^ N = 0 ∪ 1 ..^ N

Proof

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