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