Metamath Proof Explorer

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 e. ( ZZ>= ` 2 ) -> ( 1 ... N ) = ( ( 1 ... 2 ) u. ( 3 ... N ) ) )

Proof

Step Hyp Ref Expression
1 1le2 
 |-  1 <_ 2
2 1 a1i 
 |-  ( N e. ( ZZ>= ` 2 ) -> 1 <_ 2 )
3 eluzle 
 |-  ( N e. ( ZZ>= ` 2 ) -> 2 <_ N )
4 2z 
 |-  2 e. ZZ
5 1z 
 |-  1 e. ZZ
6 eluzelz 
 |-  ( N e. ( ZZ>= ` 2 ) -> N e. ZZ )
7 elfz 
 |-  ( ( 2 e. ZZ /\ 1 e. ZZ /\ N e. ZZ ) -> ( 2 e. ( 1 ... N ) <-> ( 1 <_ 2 /\ 2 <_ N ) ) )
8 4 5 6 7 mp3an12i 
 |-  ( N e. ( ZZ>= ` 2 ) -> ( 2 e. ( 1 ... N ) <-> ( 1 <_ 2 /\ 2 <_ N ) ) )
9 2 3 8 mpbir2and 
 |-  ( N e. ( ZZ>= ` 2 ) -> 2 e. ( 1 ... N ) )
10 fzsplit 
 |-  ( 2 e. ( 1 ... N ) -> ( 1 ... N ) = ( ( 1 ... 2 ) u. ( ( 2 + 1 ) ... N ) ) )
11 9 10 syl 
 |-  ( N e. ( ZZ>= ` 2 ) -> ( 1 ... N ) = ( ( 1 ... 2 ) u. ( ( 2 + 1 ) ... N ) ) )
12 df-3 
 |-  3 = ( 2 + 1 )
13 12 oveq1i 
 |-  ( 3 ... N ) = ( ( 2 + 1 ) ... N )
14 13 uneq2i 
 |-  ( ( 1 ... 2 ) u. ( 3 ... N ) ) = ( ( 1 ... 2 ) u. ( ( 2 + 1 ) ... N ) )
15 11 14 eqtr4di 
 |-  ( N e. ( ZZ>= ` 2 ) -> ( 1 ... N ) = ( ( 1 ... 2 ) u. ( 3 ... N ) ) )