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

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