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 e. ZZ
2		fzoval	|- ( 3 e. ZZ -> ( 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 e. ZZ
9		fzpr	|- ( 1 e. ZZ -> ( 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 }