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 ∈ ℤ | |
| 4 | fzpr | ⊢ ( 0 ∈ ℤ → ( 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 } |