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

Metamath Proof Explorer

Theorem fzo0to3tp

Description: A half-open integer range from 0 to 3 is an unordered triple. (Contributed by Alexander van der Vekens, 9-Nov-2017)

Ref Expression
Assertion fzo0to3tp ( 0 ..^ 3 ) = { 0 , 1 , 2 }

Proof

Step Hyp Ref Expression
1 3z ⊢ 3 ∈ ℤ
2 fzoval ⊢ ( 3 ∈ ℤ → ( 0 ..^ 3 ) = ( 0 ... ( 3 − 1 ) ) )
3 1 2 ax-mp ⊢ ( 0 ..^ 3 ) = ( 0 ... ( 3 − 1 ) )
4 3m1e2 ⊢ ( 3 − 1 ) = 2
5 2cn ⊢ 2 ∈ ℂ
6 5 addlidi ⊢ ( 0 + 2 ) = 2
7 4 6 eqtr4i ⊢ ( 3 − 1 ) = ( 0 + 2 )
8 7 oveq2i ⊢ ( 0 ... ( 3 − 1 ) ) = ( 0 ... ( 0 + 2 ) )
9 0z ⊢ 0 ∈ ℤ
10 fztp ⊢ ( 0 ∈ ℤ → ( 0 ... ( 0 + 2 ) ) = { 0 , ( 0 + 1 ) , ( 0 + 2 ) } )
11 eqidd ⊢ ( 0 ∈ ℤ → 0 = 0 )
12 0p1e1 ⊢ ( 0 + 1 ) = 1
13 12 a1i ⊢ ( 0 ∈ ℤ → ( 0 + 1 ) = 1 )
14 6 a1i ⊢ ( 0 ∈ ℤ → ( 0 + 2 ) = 2 )
15 11 13 14 tpeq123d ⊢ ( 0 ∈ ℤ → { 0 , ( 0 + 1 ) , ( 0 + 2 ) } = { 0 , 1 , 2 } )
16 10 15 eqtrd ⊢ ( 0 ∈ ℤ → ( 0 ... ( 0 + 2 ) ) = { 0 , 1 , 2 } )
17 9 16 ax-mp ⊢ ( 0 ... ( 0 + 2 ) ) = { 0 , 1 , 2 }
18 3 8 17 3eqtri ⊢ ( 0 ..^ 3 ) = { 0 , 1 , 2 }