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

Metamath Proof Explorer

Theorem fzo13pr

Description: A 1-based half-open integer interval up to, but not including, 3 is a pair. (Contributed by Thierry Arnoux, 11-Jul-2020)

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

Proof

Step Hyp Ref Expression
1 3z ⊢ 3 ∈ ℤ
2 fzoval ⊢ ( 3 ∈ ℤ → ( 1 ..^ 3 ) = ( 1 ... ( 3 − 1 ) ) )
3 1 2 ax-mp ⊢ ( 1 ..^ 3 ) = ( 1 ... ( 3 − 1 ) )
4 3m1e2 ⊢ ( 3 − 1 ) = 2
5 1p1e2 ⊢ ( 1 + 1 ) = 2
6 4 5 eqtr4i ⊢ ( 3 − 1 ) = ( 1 + 1 )
7 6 oveq2i ⊢ ( 1 ... ( 3 − 1 ) ) = ( 1 ... ( 1 + 1 ) )
8 1z ⊢ 1 ∈ ℤ
9 fzpr ⊢ ( 1 ∈ ℤ → ( 1 ... ( 1 + 1 ) ) = { 1 , ( 1 + 1 ) } )
10 8 9 ax-mp ⊢ ( 1 ... ( 1 + 1 ) ) = { 1 , ( 1 + 1 ) }
11 3 7 10 3eqtri ⊢ ( 1 ..^ 3 ) = { 1 , ( 1 + 1 ) }
12 5 preq2i ⊢ { 1 , ( 1 + 1 ) } = { 1 , 2 }
13 11 12 eqtri ⊢ ( 1 ..^ 3 ) = { 1 , 2 }