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