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 ) ) )