Theorem axlowdimlem3

Description: Lemma for axlowdim . Set up a union property for an interval of integers. (Contributed by Scott Fenton, 29-Jun-2013)

	Ref	Expression
Assertion	axlowdimlem3	$$⊢N\in {\mathbb{Z}}_{\ge 2}\to \left(1\dots N\right)=\left(1\dots 2\right)\cup \left(3\dots N\right)$$

Proof

Step	Hyp	Ref	Expression
1		1le2	$$⊢1\le 2$$
2	1	a1i	$$⊢N\in {\mathbb{Z}}_{\ge 2}\to 1\le 2$$
3		eluzle	$$⊢N\in {\mathbb{Z}}_{\ge 2}\to 2\le N$$
4		2z	$$⊢2\in \mathbb{Z}$$
5		1z	$$⊢1\in \mathbb{Z}$$
6		eluzelz	$$⊢N\in {\mathbb{Z}}_{\ge 2}\to N\in \mathbb{Z}$$
7		elfz	$$⊢\left(2\in \mathbb{Z}\wedge 1\in \mathbb{Z}\wedge N\in \mathbb{Z}\right)\to \left(2\in \left(1\dots N\right)\leftrightarrow \left(1\le 2\wedge 2\le N\right)\right)$$
8	4 5 6 7	mp3an12i	$$⊢N\in {\mathbb{Z}}_{\ge 2}\to \left(2\in \left(1\dots N\right)\leftrightarrow \left(1\le 2\wedge 2\le N\right)\right)$$
9	2 3 8	mpbir2and	$$⊢N\in {\mathbb{Z}}_{\ge 2}\to 2\in \left(1\dots N\right)$$
10		fzsplit	$$⊢2\in \left(1\dots N\right)\to \left(1\dots N\right)=\left(1\dots 2\right)\cup \left(2+1\dots N\right)$$
11	9 10	syl	$$⊢N\in {\mathbb{Z}}_{\ge 2}\to \left(1\dots N\right)=\left(1\dots 2\right)\cup \left(2+1\dots N\right)$$
12		df-3	$$⊢3=2+1$$
13	12	oveq1i	$$⊢\left(3\dots N\right)=\left(2+1\dots N\right)$$
14	13	uneq2i	$$⊢\left(1\dots 2\right)\cup \left(3\dots N\right)=\left(1\dots 2\right)\cup \left(2+1\dots N\right)$$
15	11 14	eqtr4di	$$⊢N\in {\mathbb{Z}}_{\ge 2}\to \left(1\dots N\right)=\left(1\dots 2\right)\cup \left(3\dots N\right)$$