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