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 }