Theorem 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 ... 2 ) = { 0 , 1 , 2 }

Proof

Step	Hyp	Ref	Expression
1		2cn	⊢ 2 ∈ ℂ
2	1	addid2i	⊢ ( 0 + 2 ) = 2
3	2	eqcomi	⊢ 2 = ( 0 + 2 )
4	3	oveq2i	⊢ ( 0 ... 2 ) = ( 0 ... ( 0 + 2 ) )
5		0z	⊢ 0 ∈ ℤ
6		fztp	⊢ ( 0 ∈ ℤ → ( 0 ... ( 0 + 2 ) ) = { 0 , ( 0 + 1 ) , ( 0 + 2 ) } )
7	5 6	ax-mp	⊢ ( 0 ... ( 0 + 2 ) ) = { 0 , ( 0 + 1 ) , ( 0 + 2 ) }
8		eqid	⊢ 0 = 0
9		id	⊢ ( 0 = 0 → 0 = 0 )
10		0p1e1	⊢ ( 0 + 1 ) = 1
11	10	a1i	⊢ ( 0 = 0 → ( 0 + 1 ) = 1 )
12	2	a1i	⊢ ( 0 = 0 → ( 0 + 2 ) = 2 )
13	9 11 12	tpeq123d	⊢ ( 0 = 0 → { 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 ... 2 ) = { 0 , 1 , 2 }