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

Metamath Proof Explorer

Theorem fz12pr

Description: An integer range between 1 and 2 is a pair. (Contributed by AV, 11-Jan-2023)

		Ref	Expression
	Assertion	fz12pr	$⊢ (1 \dots 2) = \{1, 2\}$

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