Metamath Proof Explorer

Theorem fztp

Description: A finite interval of integers with three elements. (Contributed by NM, 13-Sep-2011) (Revised by Mario Carneiro, 7-Mar-2014)

Ref Expression
Assertion fztp 
|- ( M e. ZZ -> ( M ... ( M + 2 ) ) = { M , ( M + 1 ) , ( M + 2 ) } )

Proof

Step Hyp Ref Expression
1 uzid 
 |-  ( M e. ZZ -> M e. ( ZZ>= ` M ) )
2 peano2uz 
 |-  ( M e. ( ZZ>= ` M ) -> ( M + 1 ) e. ( ZZ>= ` M ) )
3 fzsuc 
 |-  ( ( M + 1 ) e. ( ZZ>= ` M ) -> ( M ... ( ( M + 1 ) + 1 ) ) = ( ( M ... ( M + 1 ) ) u. { ( ( M + 1 ) + 1 ) } ) )
4 1 2 3 3syl 
 |-  ( M e. ZZ -> ( M ... ( ( M + 1 ) + 1 ) ) = ( ( M ... ( M + 1 ) ) u. { ( ( M + 1 ) + 1 ) } ) )
5 zcn 
 |-  ( M e. ZZ -> M e. CC )
6 ax-1cn 
 |-  1 e. CC
7 addass 
 |-  ( ( M e. CC /\ 1 e. CC /\ 1 e. CC ) -> ( ( M + 1 ) + 1 ) = ( M + ( 1 + 1 ) ) )
8 6 6 7 mp3an23 
 |-  ( M e. CC -> ( ( M + 1 ) + 1 ) = ( M + ( 1 + 1 ) ) )
9 5 8 syl 
 |-  ( M e. ZZ -> ( ( M + 1 ) + 1 ) = ( M + ( 1 + 1 ) ) )
10 df-2 
 |-  2 = ( 1 + 1 )
11 10 oveq2i 
 |-  ( M + 2 ) = ( M + ( 1 + 1 ) )
12 9 11 eqtr4di 
 |-  ( M e. ZZ -> ( ( M + 1 ) + 1 ) = ( M + 2 ) )
13 12 oveq2d 
 |-  ( M e. ZZ -> ( M ... ( ( M + 1 ) + 1 ) ) = ( M ... ( M + 2 ) ) )
14 fzpr 
 |-  ( M e. ZZ -> ( M ... ( M + 1 ) ) = { M , ( M + 1 ) } )
15 12 sneqd 
 |-  ( M e. ZZ -> { ( ( M + 1 ) + 1 ) } = { ( M + 2 ) } )
16 14 15 uneq12d 
 |-  ( M e. ZZ -> ( ( M ... ( M + 1 ) ) u. { ( ( M + 1 ) + 1 ) } ) = ( { M , ( M + 1 ) } u. { ( M + 2 ) } ) )
17 df-tp 
 |-  { M , ( M + 1 ) , ( M + 2 ) } = ( { M , ( M + 1 ) } u. { ( M + 2 ) } )
18 16 17 eqtr4di 
 |-  ( M e. ZZ -> ( ( M ... ( M + 1 ) ) u. { ( ( M + 1 ) + 1 ) } ) = { M , ( M + 1 ) , ( M + 2 ) } )
19 4 13 18 3eqtr3d 
 |-  ( M e. ZZ -> ( M ... ( M + 2 ) ) = { M , ( M + 1 ) , ( M + 2 ) } )