fz0tp

Description: An integer range from 0 to 2 is an unordered triple. (Contributed by Alexander van der Vekens, 1-Feb-2018)

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

Step	Hyp	Ref	Expression
1		2cn	$⊢ 2 \in ℂ$
2	1	addlidi	$⊢ 0 + 2 = 2$
3	2	eqcomi	$⊢ 2 = 0 + 2$
4	3	oveq2i	$⊢ (0 \dots 2) = (0 \dots 0 + 2)$
5		0z	$⊢ 0 \in ℤ$
6		fztp	$⊢ 0 \in ℤ \to (0 \dots 0 + 2) = \{0, 0 + 1, 0 + 2\}$
7	5 6	ax-mp	$⊢ (0 \dots 0 + 2) = \{0, 0 + 1, 0 + 2\}$
8		eqid	$⊢ 0 = 0$
9		id	$⊢ 0 = 0 \to 0 = 0$
10		0p1e1	$⊢ 0 + 1 = 1$
11	10	a1i	$⊢ 0 = 0 \to 0 + 1 = 1$
12	2	a1i	$⊢ 0 = 0 \to 0 + 2 = 2$
13	9 11 12	tpeq123d	$⊢ 0 = 0 \to \{0, 0 + 1, 0 + 2\} = \{0, 1, 2\}$
14	8 13	ax-mp	$⊢ \{0, 0 + 1, 0 + 2\} = \{0, 1, 2\}$
15	4 7 14	3eqtri	$⊢ (0 \dots 2) = \{0, 1, 2\}$

Metamath Proof Explorer