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

Metamath Proof Explorer

Theorem fzo0to2pr

Description: A half-open integer range from 0 to 2 is an unordered pair. (Contributed by Alexander van der Vekens, 4-Dec-2017)

Ref Expression
Assertion fzo0to2pr 
|- ( 0 ..^ 2 ) = { 0 , 1 }

Proof

Step Hyp Ref Expression
1 2z 
 |-  2 e. ZZ
2 fzoval 
 |-  ( 2 e. ZZ -> ( 0 ..^ 2 ) = ( 0 ... ( 2 - 1 ) ) )
3 1 2 ax-mp 
 |-  ( 0 ..^ 2 ) = ( 0 ... ( 2 - 1 ) )
4 2m1e1 
 |-  ( 2 - 1 ) = 1
5 0p1e1 
 |-  ( 0 + 1 ) = 1
6 4 5 eqtr4i 
 |-  ( 2 - 1 ) = ( 0 + 1 )
7 6 oveq2i 
 |-  ( 0 ... ( 2 - 1 ) ) = ( 0 ... ( 0 + 1 ) )
8 0z 
 |-  0 e. ZZ
9 fzpr 
 |-  ( 0 e. ZZ -> ( 0 ... ( 0 + 1 ) ) = { 0 , ( 0 + 1 ) } )
10 5 preq2i 
 |-  { 0 , ( 0 + 1 ) } = { 0 , 1 }
11 9 10 eqtrdi 
 |-  ( 0 e. ZZ -> ( 0 ... ( 0 + 1 ) ) = { 0 , 1 } )
12 8 11 ax-mp 
 |-  ( 0 ... ( 0 + 1 ) ) = { 0 , 1 }
13 3 7 12 3eqtri 
 |-  ( 0 ..^ 2 ) = { 0 , 1 }