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 }