fz01en

Description: 0-based and 1-based finite sets of sequential integers are equinumerous. (Contributed by Paul Chapman, 11-Apr-2009)

		Ref	Expression
	Assertion	fz01en	$⊢ N \in ℤ \to (0 \dots N - 1) \approx (1 \dots N)$

Step	Hyp	Ref	Expression
1		peano2zm	$⊢ N \in ℤ \to N - 1 \in ℤ$
2		0z	$⊢ 0 \in ℤ$
3		1z	$⊢ 1 \in ℤ$
4		fzen	$⊢ (0 \in ℤ \land N - 1 \in ℤ \land 1 \in ℤ) \to (0 \dots N - 1) \approx (0 + 1 \dots N - 1 + 1)$
5	2 3 4	mp3an13	$⊢ N - 1 \in ℤ \to (0 \dots N - 1) \approx (0 + 1 \dots N - 1 + 1)$
6	1 5	syl	$⊢ N \in ℤ \to (0 \dots N - 1) \approx (0 + 1 \dots N - 1 + 1)$
7		0p1e1	$⊢ 0 + 1 = 1$
8	7	a1i	$⊢ N \in ℤ \to 0 + 1 = 1$
9		zcn	$⊢ N \in ℤ \to N \in ℂ$
10		ax-1cn	$⊢ 1 \in ℂ$
11		npcan	$⊢ (N \in ℂ \land 1 \in ℂ) \to N - 1 + 1 = N$
12	9 10 11	sylancl	$⊢ N \in ℤ \to N - 1 + 1 = N$
13	8 12	oveq12d	$⊢ N \in ℤ \to (0 + 1 \dots N - 1 + 1) = (1 \dots N)$
14	6 13	breqtrd	$⊢ N \in ℤ \to (0 \dots N - 1) \approx (1 \dots N)$

Metamath Proof Explorer