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

Metamath Proof Explorer

Theorem fzo0to2pr

Description: A half-open integer range from 0 to 2 is an unordered pair. (Contributed by Alexander van der Vekens, 4-Dec-2017)

Ref Expression
Assertion fzo0to2pr ⊢ 0 ..^ 2 = 0 1

Proof

Step Hyp Ref Expression
1 2z ⊢ 2 ∈ ℤ
2 fzoval ⊢ 2 ∈ ℤ → 0 ..^ 2 = 0 … 2 − 1
3 1 2 ax-mp ⊢ 0 ..^ 2 = 0 … 2 − 1
4 2m1e1 ⊢ 2 − 1 = 1
5 0p1e1 ⊢ 0 + 1 = 1
6 4 5 eqtr4i ⊢ 2 − 1 = 0 + 1
7 6 oveq2i ⊢ 0 … 2 − 1 = 0 … 0 + 1
8 0z ⊢ 0 ∈ ℤ
9 fzpr ⊢ 0 ∈ ℤ → 0 … 0 + 1 = 0 0 + 1
10 5 preq2i ⊢ 0 0 + 1 = 0 1
11 9 10 eqtrdi ⊢ 0 ∈ ℤ → 0 … 0 + 1 = 0 1
12 8 11 ax-mp ⊢ 0 … 0 + 1 = 0 1
13 3 7 12 3eqtri ⊢ 0 ..^ 2 = 0 1