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 
|- ( M e. ZZ -> ( M ... ( M + 1 ) ) = { M , ( M + 1 ) } )

Proof

Step Hyp Ref Expression
1 uzid 
 |-  ( M e. ZZ -> M e. ( ZZ>= ` M ) )
2 elfzp1 
 |-  ( M e. ( ZZ>= ` M ) -> ( m e. ( M ... ( M + 1 ) ) <-> ( m e. ( M ... M ) \/ m = ( M + 1 ) ) ) )
3 1 2 syl 
 |-  ( M e. ZZ -> ( m e. ( M ... ( M + 1 ) ) <-> ( m e. ( M ... M ) \/ m = ( M + 1 ) ) ) )
4 fzsn 
 |-  ( M e. ZZ -> ( M ... M ) = { M } )
5 4 eleq2d 
 |-  ( M e. ZZ -> ( m e. ( M ... M ) <-> m e. { M } ) )
6 velsn 
 |-  ( m e. { M } <-> m = M )
7 5 6 bitrdi 
 |-  ( M e. ZZ -> ( m e. ( M ... M ) <-> m = M ) )
8 7 orbi1d 
 |-  ( M e. ZZ -> ( ( m e. ( M ... M ) \/ m = ( M + 1 ) ) <-> ( m = M \/ m = ( M + 1 ) ) ) )
9 3 8 bitrd 
 |-  ( M e. ZZ -> ( m e. ( M ... ( M + 1 ) ) <-> ( m = M \/ m = ( M + 1 ) ) ) )
10 vex 
 |-  m e. _V
11 10 elpr 
 |-  ( m e. { M , ( M + 1 ) } <-> ( m = M \/ m = ( M + 1 ) ) )
12 9 11 bitr4di 
 |-  ( M e. ZZ -> ( m e. ( M ... ( M + 1 ) ) <-> m e. { M , ( M + 1 ) } ) )
13 12 eqrdv 
 |-  ( M e. ZZ -> ( M ... ( M + 1 ) ) = { M , ( M + 1 ) } )