Metamath Proof Explorer

Theorem fzdifsuc

Description: Remove a successor from the end of a finite set of sequential integers. (Contributed by AV, 4-Sep-2019)

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

Proof

Step Hyp Ref Expression
1 fzsuc 
 |-  ( N e. ( ZZ>= ` M ) -> ( M ... ( N + 1 ) ) = ( ( M ... N ) u. { ( N + 1 ) } ) )
2 1 difeq1d 
 |-  ( N e. ( ZZ>= ` M ) -> ( ( M ... ( N + 1 ) ) \ { ( N + 1 ) } ) = ( ( ( M ... N ) u. { ( N + 1 ) } ) \ { ( N + 1 ) } ) )
3 uncom 
 |-  ( { ( N + 1 ) } u. ( M ... N ) ) = ( ( M ... N ) u. { ( N + 1 ) } )
4 ssun2 
 |-  { ( N + 1 ) } C_ ( ( M ... N ) u. { ( N + 1 ) } )
5 incom 
 |-  ( { ( N + 1 ) } i^i ( M ... N ) ) = ( ( M ... N ) i^i { ( N + 1 ) } )
6 fzp1disj 
 |-  ( ( M ... N ) i^i { ( N + 1 ) } ) = (/)
7 5 6 eqtri 
 |-  ( { ( N + 1 ) } i^i ( M ... N ) ) = (/)
8 7 a1i 
 |-  ( N e. ( ZZ>= ` M ) -> ( { ( N + 1 ) } i^i ( M ... N ) ) = (/) )
9 uneqdifeq 
 |-  ( ( { ( N + 1 ) } C_ ( ( M ... N ) u. { ( N + 1 ) } ) /\ ( { ( N + 1 ) } i^i ( M ... N ) ) = (/) ) -> ( ( { ( N + 1 ) } u. ( M ... N ) ) = ( ( M ... N ) u. { ( N + 1 ) } ) <-> ( ( ( M ... N ) u. { ( N + 1 ) } ) \ { ( N + 1 ) } ) = ( M ... N ) ) )
10 4 8 9 sylancr 
 |-  ( N e. ( ZZ>= ` M ) -> ( ( { ( N + 1 ) } u. ( M ... N ) ) = ( ( M ... N ) u. { ( N + 1 ) } ) <-> ( ( ( M ... N ) u. { ( N + 1 ) } ) \ { ( N + 1 ) } ) = ( M ... N ) ) )
11 3 10 mpbii 
 |-  ( N e. ( ZZ>= ` M ) -> ( ( ( M ... N ) u. { ( N + 1 ) } ) \ { ( N + 1 ) } ) = ( M ... N ) )
12 2 11 eqtr2d 
 |-  ( N e. ( ZZ>= ` M ) -> ( M ... N ) = ( ( M ... ( N + 1 ) ) \ { ( N + 1 ) } ) )