Metamath Proof Explorer

Theorem fzpred

Description: Join a predecessor to the beginning of a finite set of sequential integers. (Contributed by AV, 24-Aug-2019)

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

Proof

Step Hyp Ref Expression
1 eluzel2 
 |-  ( N e. ( ZZ>= ` M ) -> M e. ZZ )
2 uzid 
 |-  ( M e. ZZ -> M e. ( ZZ>= ` M ) )
3 peano2uz 
 |-  ( M e. ( ZZ>= ` M ) -> ( M + 1 ) e. ( ZZ>= ` M ) )
4 1 2 3 3syl 
 |-  ( N e. ( ZZ>= ` M ) -> ( M + 1 ) e. ( ZZ>= ` M ) )
5 fzsplit2 
 |-  ( ( ( M + 1 ) e. ( ZZ>= ` M ) /\ N e. ( ZZ>= ` M ) ) -> ( M ... N ) = ( ( M ... M ) u. ( ( M + 1 ) ... N ) ) )
6 4 5 mpancom 
 |-  ( N e. ( ZZ>= ` M ) -> ( M ... N ) = ( ( M ... M ) u. ( ( M + 1 ) ... N ) ) )
7 fzsn 
 |-  ( M e. ZZ -> ( M ... M ) = { M } )
8 1 7 syl 
 |-  ( N e. ( ZZ>= ` M ) -> ( M ... M ) = { M } )
9 8 uneq1d 
 |-  ( N e. ( ZZ>= ` M ) -> ( ( M ... M ) u. ( ( M + 1 ) ... N ) ) = ( { M } u. ( ( M + 1 ) ... N ) ) )
10 6 9 eqtrd 
 |-  ( N e. ( ZZ>= ` M ) -> ( M ... N ) = ( { M } u. ( ( M + 1 ) ... N ) ) )