This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 \dots 1) = \{0, 1\}$

Step	Hyp	Ref	Expression
1		1e0p1	$⊢ 1 = 0 + 1$
2	1	oveq2i	$⊢ (0 \dots 1) = (0 \dots 0 + 1)$
3		0z	$⊢ 0 \in ℤ$
4		fzpr	$⊢ 0 \in ℤ \to (0 \dots 0 + 1) = \{0, 0 + 1\}$
5	3 4	ax-mp	$⊢ (0 \dots 0 + 1) = \{0, 0 + 1\}$
6		0p1e1	$⊢ 0 + 1 = 1$
7	6	preq2i	$⊢ \{0, 0 + 1\} = \{0, 1\}$
8	2 5 7	3eqtri	$⊢ (0 \dots 1) = \{0, 1\}$