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

Metamath Proof Explorer

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 addlidi ⊢ ( 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 }