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	⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) → ( 1 ... 𝑁 ) = ( ( 1 ... 2 ) ∪ ( 3 ... 𝑁 ) ) )

Proof

Step	Hyp	Ref	Expression
1		1le2	⊢ 1 ≤ 2
2	1	a1i	⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) → 1 ≤ 2 )
3		eluzle	⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) → 2 ≤ 𝑁 )
4		2z	⊢ 2 ∈ ℤ
5		1z	⊢ 1 ∈ ℤ
6		eluzelz	⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) → 𝑁 ∈ ℤ )
7		elfz	⊢ ( ( 2 ∈ ℤ ∧ 1 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( 2 ∈ ( 1 ... 𝑁 ) ↔ ( 1 ≤ 2 ∧ 2 ≤ 𝑁 ) ) )
8	4 5 6 7	mp3an12i	⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) → ( 2 ∈ ( 1 ... 𝑁 ) ↔ ( 1 ≤ 2 ∧ 2 ≤ 𝑁 ) ) )
9	2 3 8	mpbir2and	⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) → 2 ∈ ( 1 ... 𝑁 ) )
10		fzsplit	⊢ ( 2 ∈ ( 1 ... 𝑁 ) → ( 1 ... 𝑁 ) = ( ( 1 ... 2 ) ∪ ( ( 2 + 1 ) ... 𝑁 ) ) )
11	9 10	syl	⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) → ( 1 ... 𝑁 ) = ( ( 1 ... 2 ) ∪ ( ( 2 + 1 ) ... 𝑁 ) ) )
12		df-3	⊢ 3 = ( 2 + 1 )
13	12	oveq1i	⊢ ( 3 ... 𝑁 ) = ( ( 2 + 1 ) ... 𝑁 )
14	13	uneq2i	⊢ ( ( 1 ... 2 ) ∪ ( 3 ... 𝑁 ) ) = ( ( 1 ... 2 ) ∪ ( ( 2 + 1 ) ... 𝑁 ) )
15	11 14	eqtr4di	⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) → ( 1 ... 𝑁 ) = ( ( 1 ... 2 ) ∪ ( 3 ... 𝑁 ) ) )