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 }