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\in \mathbb{N}\to \left(0..^N\right)=\left\{0\right\}\cup \left(1..^N\right)$$

Proof

Step	Hyp	Ref	Expression
1		1nn0	$$⊢1\in {\mathbb{N}}_0$$
2	1	a1i	$$⊢N\in \mathbb{N}\to 1\in {\mathbb{N}}_0$$
3		nnnn0	$$⊢N\in \mathbb{N}\to N\in {\mathbb{N}}_0$$
4		nnge1	$$⊢N\in \mathbb{N}\to 1\le N$$
5		elfz2nn0	$$⊢1\in \left(0\dots N\right)\leftrightarrow \left(1\in {\mathbb{N}}_0\wedge N\in {\mathbb{N}}_0\wedge 1\le N\right)$$
6	2 3 4 5	syl3anbrc	$$⊢N\in \mathbb{N}\to 1\in \left(0\dots N\right)$$
7		fzosplit	$$⊢1\in \left(0\dots N\right)\to \left(0..^N\right)=\left(0..^1\right)\cup \left(1..^N\right)$$
8	6 7	syl	$$⊢N\in \mathbb{N}\to \left(0..^N\right)=\left(0..^1\right)\cup \left(1..^N\right)$$
9		fzo01	$$⊢\left(0..^1\right)=\left\{0\right\}$$
10	9	a1i	$$⊢N\in \mathbb{N}\to \left(0..^1\right)=\left\{0\right\}$$
11	10	uneq1d	$$⊢N\in \mathbb{N}\to \left(0..^1\right)\cup \left(1..^N\right)=\left\{0\right\}\cup \left(1..^N\right)$$
12	8 11	eqtrd	$$⊢N\in \mathbb{N}\to \left(0..^N\right)=\left\{0\right\}\cup \left(1..^N\right)$$