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

Metamath Proof Explorer

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