Metamath Proof Explorer

Theorem fzsuc2

Description: Join a successor to the end of a finite set of sequential integers. (Contributed by Mario Carneiro, 7-Mar-2014)

Ref Expression
Assertion fzsuc2 
|- ( ( M e. ZZ /\ N e. ( ZZ>= ` ( M - 1 ) ) ) -> ( M ... ( N + 1 ) ) = ( ( M ... N ) u. { ( N + 1 ) } ) )

Proof

Step Hyp Ref Expression
1 uzp1 
 |-  ( N e. ( ZZ>= ` ( M - 1 ) ) -> ( N = ( M - 1 ) \/ N e. ( ZZ>= ` ( ( M - 1 ) + 1 ) ) ) )
2 zcn 
 |-  ( M e. ZZ -> M e. CC )
3 ax-1cn 
 |-  1 e. CC
4 npcan 
 |-  ( ( M e. CC /\ 1 e. CC ) -> ( ( M - 1 ) + 1 ) = M )
5 2 3 4 sylancl 
 |-  ( M e. ZZ -> ( ( M - 1 ) + 1 ) = M )
6 5 oveq2d 
 |-  ( M e. ZZ -> ( M ... ( ( M - 1 ) + 1 ) ) = ( M ... M ) )
7 uncom 
 |-  ( (/) u. { M } ) = ( { M } u. (/) )
8 un0 
 |-  ( { M } u. (/) ) = { M }
9 7 8 eqtri 
 |-  ( (/) u. { M } ) = { M }
10 zre 
 |-  ( M e. ZZ -> M e. RR )
11 10 ltm1d 
 |-  ( M e. ZZ -> ( M - 1 ) < M )
12 peano2zm 
 |-  ( M e. ZZ -> ( M - 1 ) e. ZZ )
13 fzn 
 |-  ( ( M e. ZZ /\ ( M - 1 ) e. ZZ ) -> ( ( M - 1 ) < M <-> ( M ... ( M - 1 ) ) = (/) ) )
14 12 13 mpdan 
 |-  ( M e. ZZ -> ( ( M - 1 ) < M <-> ( M ... ( M - 1 ) ) = (/) ) )
15 11 14 mpbid 
 |-  ( M e. ZZ -> ( M ... ( M - 1 ) ) = (/) )
16 5 sneqd 
 |-  ( M e. ZZ -> { ( ( M - 1 ) + 1 ) } = { M } )
17 15 16 uneq12d 
 |-  ( M e. ZZ -> ( ( M ... ( M - 1 ) ) u. { ( ( M - 1 ) + 1 ) } ) = ( (/) u. { M } ) )
18 fzsn 
 |-  ( M e. ZZ -> ( M ... M ) = { M } )
19 9 17 18 3eqtr4a 
 |-  ( M e. ZZ -> ( ( M ... ( M - 1 ) ) u. { ( ( M - 1 ) + 1 ) } ) = ( M ... M ) )
20 6 19 eqtr4d 
 |-  ( M e. ZZ -> ( M ... ( ( M - 1 ) + 1 ) ) = ( ( M ... ( M - 1 ) ) u. { ( ( M - 1 ) + 1 ) } ) )
21 oveq1 
 |-  ( N = ( M - 1 ) -> ( N + 1 ) = ( ( M - 1 ) + 1 ) )
22 21 oveq2d 
 |-  ( N = ( M - 1 ) -> ( M ... ( N + 1 ) ) = ( M ... ( ( M - 1 ) + 1 ) ) )
23 oveq2 
 |-  ( N = ( M - 1 ) -> ( M ... N ) = ( M ... ( M - 1 ) ) )
24 21 sneqd 
 |-  ( N = ( M - 1 ) -> { ( N + 1 ) } = { ( ( M - 1 ) + 1 ) } )
25 23 24 uneq12d 
 |-  ( N = ( M - 1 ) -> ( ( M ... N ) u. { ( N + 1 ) } ) = ( ( M ... ( M - 1 ) ) u. { ( ( M - 1 ) + 1 ) } ) )
26 22 25 eqeq12d 
 |-  ( N = ( M - 1 ) -> ( ( M ... ( N + 1 ) ) = ( ( M ... N ) u. { ( N + 1 ) } ) <-> ( M ... ( ( M - 1 ) + 1 ) ) = ( ( M ... ( M - 1 ) ) u. { ( ( M - 1 ) + 1 ) } ) ) )
27 20 26 syl5ibrcom 
 |-  ( M e. ZZ -> ( N = ( M - 1 ) -> ( M ... ( N + 1 ) ) = ( ( M ... N ) u. { ( N + 1 ) } ) ) )
28 27 imp 
 |-  ( ( M e. ZZ /\ N = ( M - 1 ) ) -> ( M ... ( N + 1 ) ) = ( ( M ... N ) u. { ( N + 1 ) } ) )
29 5 fveq2d 
 |-  ( M e. ZZ -> ( ZZ>= ` ( ( M - 1 ) + 1 ) ) = ( ZZ>= ` M ) )
30 29 eleq2d 
 |-  ( M e. ZZ -> ( N e. ( ZZ>= ` ( ( M - 1 ) + 1 ) ) <-> N e. ( ZZ>= ` M ) ) )
31 30 biimpa 
 |-  ( ( M e. ZZ /\ N e. ( ZZ>= ` ( ( M - 1 ) + 1 ) ) ) -> N e. ( ZZ>= ` M ) )
32 fzsuc 
 |-  ( N e. ( ZZ>= ` M ) -> ( M ... ( N + 1 ) ) = ( ( M ... N ) u. { ( N + 1 ) } ) )
33 31 32 syl 
 |-  ( ( M e. ZZ /\ N e. ( ZZ>= ` ( ( M - 1 ) + 1 ) ) ) -> ( M ... ( N + 1 ) ) = ( ( M ... N ) u. { ( N + 1 ) } ) )
34 28 33 jaodan 
 |-  ( ( M e. ZZ /\ ( N = ( M - 1 ) \/ N e. ( ZZ>= ` ( ( M - 1 ) + 1 ) ) ) ) -> ( M ... ( N + 1 ) ) = ( ( M ... N ) u. { ( N + 1 ) } ) )
35 1 34 sylan2 
 |-  ( ( M e. ZZ /\ N e. ( ZZ>= ` ( M - 1 ) ) ) -> ( M ... ( N + 1 ) ) = ( ( M ... N ) u. { ( N + 1 ) } ) )