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