Theorem fzpr

Description: A finite interval of integers with two elements. (Contributed by Jeff Madsen, 2-Sep-2009)

	Ref	Expression
Assertion	fzpr	⊢ ( 𝑀 ∈ ℤ → ( 𝑀 ... ( 𝑀 + 1 ) ) = { 𝑀 , ( 𝑀 + 1 ) } )

Proof

Step	Hyp	Ref	Expression
1		uzid	⊢ ( 𝑀 ∈ ℤ → 𝑀 ∈ ( ℤ≥ ‘ 𝑀 ) )
2		elfzp1	⊢ ( 𝑀 ∈ ( ℤ≥ ‘ 𝑀 ) → ( 𝑚 ∈ ( 𝑀 ... ( 𝑀 + 1 ) ) ↔ ( 𝑚 ∈ ( 𝑀 ... 𝑀 ) ∨ 𝑚 = ( 𝑀 + 1 ) ) ) )
3	1 2	syl	⊢ ( 𝑀 ∈ ℤ → ( 𝑚 ∈ ( 𝑀 ... ( 𝑀 + 1 ) ) ↔ ( 𝑚 ∈ ( 𝑀 ... 𝑀 ) ∨ 𝑚 = ( 𝑀 + 1 ) ) ) )
4		fzsn	⊢ ( 𝑀 ∈ ℤ → ( 𝑀 ... 𝑀 ) = { 𝑀 } )
5	4	eleq2d	⊢ ( 𝑀 ∈ ℤ → ( 𝑚 ∈ ( 𝑀 ... 𝑀 ) ↔ 𝑚 ∈ { 𝑀 } ) )
6		velsn	⊢ ( 𝑚 ∈ { 𝑀 } ↔ 𝑚 = 𝑀 )
7	5 6	bitrdi	⊢ ( 𝑀 ∈ ℤ → ( 𝑚 ∈ ( 𝑀 ... 𝑀 ) ↔ 𝑚 = 𝑀 ) )
8	7	orbi1d	⊢ ( 𝑀 ∈ ℤ → ( ( 𝑚 ∈ ( 𝑀 ... 𝑀 ) ∨ 𝑚 = ( 𝑀 + 1 ) ) ↔ ( 𝑚 = 𝑀 ∨ 𝑚 = ( 𝑀 + 1 ) ) ) )
9	3 8	bitrd	⊢ ( 𝑀 ∈ ℤ → ( 𝑚 ∈ ( 𝑀 ... ( 𝑀 + 1 ) ) ↔ ( 𝑚 = 𝑀 ∨ 𝑚 = ( 𝑀 + 1 ) ) ) )
10		vex	⊢ 𝑚 ∈ V
11	10	elpr	⊢ ( 𝑚 ∈ { 𝑀 , ( 𝑀 + 1 ) } ↔ ( 𝑚 = 𝑀 ∨ 𝑚 = ( 𝑀 + 1 ) ) )
12	9 11	bitr4di	⊢ ( 𝑀 ∈ ℤ → ( 𝑚 ∈ ( 𝑀 ... ( 𝑀 + 1 ) ) ↔ 𝑚 ∈ { 𝑀 , ( 𝑀 + 1 ) } ) )
13	12	eqrdv	⊢ ( 𝑀 ∈ ℤ → ( 𝑀 ... ( 𝑀 + 1 ) ) = { 𝑀 , ( 𝑀 + 1 ) } )