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 ℤ_{\geq 2} \to (1 \dots N) = (1 \dots 2) \cup (3 \dots N)$

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

Metamath Proof Explorer