This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem fzodif1

Description: Set difference of two half-open range of sequential integers sharing the same starting value. (Contributed by Thierry Arnoux, 2-Oct-2023)

Ref Expression
Assertion fzodif1 
|- ( K e. ( M ... N ) -> ( ( M ..^ N ) \ ( M ..^ K ) ) = ( K ..^ N ) )

Proof

Step Hyp Ref Expression
1 fzosplit 
 |-  ( K e. ( M ... N ) -> ( M ..^ N ) = ( ( M ..^ K ) u. ( K ..^ N ) ) )
2 1 difeq1d 
 |-  ( K e. ( M ... N ) -> ( ( M ..^ N ) \ ( M ..^ K ) ) = ( ( ( M ..^ K ) u. ( K ..^ N ) ) \ ( M ..^ K ) ) )
3 difundir 
 |-  ( ( ( M ..^ K ) u. ( K ..^ N ) ) \ ( M ..^ K ) ) = ( ( ( M ..^ K ) \ ( M ..^ K ) ) u. ( ( K ..^ N ) \ ( M ..^ K ) ) )
4 difid 
 |-  ( ( M ..^ K ) \ ( M ..^ K ) ) = (/)
5 incom 
 |-  ( ( K ..^ N ) i^i ( M ..^ K ) ) = ( ( M ..^ K ) i^i ( K ..^ N ) )
6 fzodisj 
 |-  ( ( M ..^ K ) i^i ( K ..^ N ) ) = (/)
7 5 6 eqtri 
 |-  ( ( K ..^ N ) i^i ( M ..^ K ) ) = (/)
8 disj3 
 |-  ( ( ( K ..^ N ) i^i ( M ..^ K ) ) = (/) <-> ( K ..^ N ) = ( ( K ..^ N ) \ ( M ..^ K ) ) )
9 7 8 mpbi 
 |-  ( K ..^ N ) = ( ( K ..^ N ) \ ( M ..^ K ) )
10 9 eqcomi 
 |-  ( ( K ..^ N ) \ ( M ..^ K ) ) = ( K ..^ N )
11 4 10 uneq12i 
 |-  ( ( ( M ..^ K ) \ ( M ..^ K ) ) u. ( ( K ..^ N ) \ ( M ..^ K ) ) ) = ( (/) u. ( K ..^ N ) )
12 0un 
 |-  ( (/) u. ( K ..^ N ) ) = ( K ..^ N )
13 3 11 12 3eqtri 
 |-  ( ( ( M ..^ K ) u. ( K ..^ N ) ) \ ( M ..^ K ) ) = ( K ..^ N )
14 2 13 eqtrdi 
 |-  ( K e. ( M ... N ) -> ( ( M ..^ N ) \ ( M ..^ K ) ) = ( K ..^ N ) )