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\}$

Step	Hyp	Ref	Expression
1		3z	$⊢ 3 \in ℤ$
2		fzoval	$⊢ 3 \in ℤ \to (1 ..^3) = (1 \dots 3 - 1)$
3	1 2	ax-mp	$⊢ (1 ..^3) = (1 \dots 3 - 1)$
4		3m1e2	$⊢ 3 - 1 = 2$
5		1p1e2	$⊢ 1 + 1 = 2$
6	4 5	eqtr4i	$⊢ 3 - 1 = 1 + 1$
7	6	oveq2i	$⊢ (1 \dots 3 - 1) = (1 \dots 1 + 1)$
8		1z	$⊢ 1 \in ℤ$
9		fzpr	$⊢ 1 \in ℤ \to (1 \dots 1 + 1) = \{1, 1 + 1\}$
10	8 9	ax-mp	$⊢ (1 \dots 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\}$

Metamath Proof Explorer