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