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