Metamath Proof Explorer

Theorem fz12pr

Description: An integer range between 1 and 2 is a pair. (Contributed by AV, 11-Jan-2023)

Ref Expression
Assertion fz12pr 
|- ( 1 ... 2 ) = { 1 , 2 }

Proof

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