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 ( 𝑀 ∈ ℤ → ( 𝑀 ... ( 𝑀 + 2 ) ) = { 𝑀 , ( 𝑀 + 1 ) , ( 𝑀 + 2 ) } )

Proof

Step Hyp Ref Expression
1 uzid ( 𝑀 ∈ ℤ → 𝑀 ∈ ( ℤ𝑀 ) )
2 peano2uz ( 𝑀 ∈ ( ℤ𝑀 ) → ( 𝑀 + 1 ) ∈ ( ℤ𝑀 ) )
3 fzsuc ( ( 𝑀 + 1 ) ∈ ( ℤ𝑀 ) → ( 𝑀 ... ( ( 𝑀 + 1 ) + 1 ) ) = ( ( 𝑀 ... ( 𝑀 + 1 ) ) ∪ { ( ( 𝑀 + 1 ) + 1 ) } ) )
4 1 2 3 3syl ( 𝑀 ∈ ℤ → ( 𝑀 ... ( ( 𝑀 + 1 ) + 1 ) ) = ( ( 𝑀 ... ( 𝑀 + 1 ) ) ∪ { ( ( 𝑀 + 1 ) + 1 ) } ) )
5 zcn ( 𝑀 ∈ ℤ → 𝑀 ∈ ℂ )
6 ax-1cn 1 ∈ ℂ
7 addass ( ( 𝑀 ∈ ℂ ∧ 1 ∈ ℂ ∧ 1 ∈ ℂ ) → ( ( 𝑀 + 1 ) + 1 ) = ( 𝑀 + ( 1 + 1 ) ) )
8 6 6 7 mp3an23 ( 𝑀 ∈ ℂ → ( ( 𝑀 + 1 ) + 1 ) = ( 𝑀 + ( 1 + 1 ) ) )
9 5 8 syl ( 𝑀 ∈ ℤ → ( ( 𝑀 + 1 ) + 1 ) = ( 𝑀 + ( 1 + 1 ) ) )
10 df-2 2 = ( 1 + 1 )
11 10 oveq2i ( 𝑀 + 2 ) = ( 𝑀 + ( 1 + 1 ) )
12 9 11 eqtr4di ( 𝑀 ∈ ℤ → ( ( 𝑀 + 1 ) + 1 ) = ( 𝑀 + 2 ) )
13 12 oveq2d ( 𝑀 ∈ ℤ → ( 𝑀 ... ( ( 𝑀 + 1 ) + 1 ) ) = ( 𝑀 ... ( 𝑀 + 2 ) ) )
14 fzpr ( 𝑀 ∈ ℤ → ( 𝑀 ... ( 𝑀 + 1 ) ) = { 𝑀 , ( 𝑀 + 1 ) } )
15 12 sneqd ( 𝑀 ∈ ℤ → { ( ( 𝑀 + 1 ) + 1 ) } = { ( 𝑀 + 2 ) } )
16 14 15 uneq12d ( 𝑀 ∈ ℤ → ( ( 𝑀 ... ( 𝑀 + 1 ) ) ∪ { ( ( 𝑀 + 1 ) + 1 ) } ) = ( { 𝑀 , ( 𝑀 + 1 ) } ∪ { ( 𝑀 + 2 ) } ) )
17 df-tp { 𝑀 , ( 𝑀 + 1 ) , ( 𝑀 + 2 ) } = ( { 𝑀 , ( 𝑀 + 1 ) } ∪ { ( 𝑀 + 2 ) } )
18 16 17 eqtr4di ( 𝑀 ∈ ℤ → ( ( 𝑀 ... ( 𝑀 + 1 ) ) ∪ { ( ( 𝑀 + 1 ) + 1 ) } ) = { 𝑀 , ( 𝑀 + 1 ) , ( 𝑀 + 2 ) } )
19 4 13 18 3eqtr3d ( 𝑀 ∈ ℤ → ( 𝑀 ... ( 𝑀 + 2 ) ) = { 𝑀 , ( 𝑀 + 1 ) , ( 𝑀 + 2 ) } )