Metamath Proof Explorer

Theorem fz01pr

Description: An integer range between 0 and 1 is a pair. (Contributed by AV, 11-Sep-2025)

Ref Expression
Assertion fz01pr 
|- ( 0 ... 1 ) = { 0 , 1 }

Proof

Step Hyp Ref Expression
1 1e0p1 
 |-  1 = ( 0 + 1 )
2 1 oveq2i 
 |-  ( 0 ... 1 ) = ( 0 ... ( 0 + 1 ) )
3 0z 
 |-  0 e. ZZ
4 fzpr 
 |-  ( 0 e. ZZ -> ( 0 ... ( 0 + 1 ) ) = { 0 , ( 0 + 1 ) } )
5 3 4 ax-mp 
 |-  ( 0 ... ( 0 + 1 ) ) = { 0 , ( 0 + 1 ) }
6 0p1e1 
 |-  ( 0 + 1 ) = 1
7 6 preq2i 
 |-  { 0 , ( 0 + 1 ) } = { 0 , 1 }
8 2 5 7 3eqtri 
 |-  ( 0 ... 1 ) = { 0 , 1 }