Metamath Proof Explorer

Theorem fzopred

Description: Join a predecessor to the beginning of an open integer interval. Generalization of fzo0sn0fzo1 . (Contributed by AV, 14-Jul-2020)

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

Proof

Step Hyp Ref Expression
1 fzolb 
 |-  ( M e. ( M ..^ N ) <-> ( M e. ZZ /\ N e. ZZ /\ M < N ) )
2 fzofzp1 
 |-  ( M e. ( M ..^ N ) -> ( M + 1 ) e. ( M ... N ) )
3 1 2 sylbir 
 |-  ( ( M e. ZZ /\ N e. ZZ /\ M < N ) -> ( M + 1 ) e. ( M ... N ) )
4 fzosplit 
 |-  ( ( M + 1 ) e. ( M ... N ) -> ( M ..^ N ) = ( ( M ..^ ( M + 1 ) ) u. ( ( M + 1 ) ..^ N ) ) )
5 3 4 syl 
 |-  ( ( M e. ZZ /\ N e. ZZ /\ M < N ) -> ( M ..^ N ) = ( ( M ..^ ( M + 1 ) ) u. ( ( M + 1 ) ..^ N ) ) )
6 fzosn 
 |-  ( M e. ZZ -> ( M ..^ ( M + 1 ) ) = { M } )
7 6 3ad2ant1 
 |-  ( ( M e. ZZ /\ N e. ZZ /\ M < N ) -> ( M ..^ ( M + 1 ) ) = { M } )
8 7 uneq1d 
 |-  ( ( M e. ZZ /\ N e. ZZ /\ M < N ) -> ( ( M ..^ ( M + 1 ) ) u. ( ( M + 1 ) ..^ N ) ) = ( { M } u. ( ( M + 1 ) ..^ N ) ) )
9 5 8 eqtrd 
 |-  ( ( M e. ZZ /\ N e. ZZ /\ M < N ) -> ( M ..^ N ) = ( { M } u. ( ( M + 1 ) ..^ N ) ) )