Theorem fz12pr

Description: An integer range between 1 and 2 is a pair. (Contributed by AV, 11-Jan-2023)

	Ref	Expression
Assertion	fz12pr	⊢ ( 1 ... 2 ) = { 1 , 2 }

Proof

Step	Hyp	Ref	Expression
1		df-2	⊢ 2 = ( 1 + 1 )
2	1	oveq2i	⊢ ( 1 ... 2 ) = ( 1 ... ( 1 + 1 ) )
3		1z	⊢ 1 ∈ ℤ
4		fzpr	⊢ ( 1 ∈ ℤ → ( 1 ... ( 1 + 1 ) ) = { 1 , ( 1 + 1 ) } )
5	3 4	ax-mp	⊢ ( 1 ... ( 1 + 1 ) ) = { 1 , ( 1 + 1 ) }
6		1p1e2	⊢ ( 1 + 1 ) = 2
7	6	preq2i	⊢ { 1 , ( 1 + 1 ) } = { 1 , 2 }
8	2 5 7	3eqtri	⊢ ( 1 ... 2 ) = { 1 , 2 }