Theorem 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	⊢ ( 𝑁 ∈ ℤ → ( 0 ... ( 𝑁 − 1 ) ) ≈ ( 1 ... 𝑁 ) )

Proof

Step	Hyp	Ref	Expression
1		peano2zm	⊢ ( 𝑁 ∈ ℤ → ( 𝑁 − 1 ) ∈ ℤ )
2		0z	⊢ 0 ∈ ℤ
3		1z	⊢ 1 ∈ ℤ
4		fzen	⊢ ( ( 0 ∈ ℤ ∧ ( 𝑁 − 1 ) ∈ ℤ ∧ 1 ∈ ℤ ) → ( 0 ... ( 𝑁 − 1 ) ) ≈ ( ( 0 + 1 ) ... ( ( 𝑁 − 1 ) + 1 ) ) )
5	2 3 4	mp3an13	⊢ ( ( 𝑁 − 1 ) ∈ ℤ → ( 0 ... ( 𝑁 − 1 ) ) ≈ ( ( 0 + 1 ) ... ( ( 𝑁 − 1 ) + 1 ) ) )
6	1 5	syl	⊢ ( 𝑁 ∈ ℤ → ( 0 ... ( 𝑁 − 1 ) ) ≈ ( ( 0 + 1 ) ... ( ( 𝑁 − 1 ) + 1 ) ) )
7		0p1e1	⊢ ( 0 + 1 ) = 1
8	7	a1i	⊢ ( 𝑁 ∈ ℤ → ( 0 + 1 ) = 1 )
9		zcn	⊢ ( 𝑁 ∈ ℤ → 𝑁 ∈ ℂ )
10		ax-1cn	⊢ 1 ∈ ℂ
11		npcan	⊢ ( ( 𝑁 ∈ ℂ ∧ 1 ∈ ℂ ) → ( ( 𝑁 − 1 ) + 1 ) = 𝑁 )
12	9 10 11	sylancl	⊢ ( 𝑁 ∈ ℤ → ( ( 𝑁 − 1 ) + 1 ) = 𝑁 )
13	8 12	oveq12d	⊢ ( 𝑁 ∈ ℤ → ( ( 0 + 1 ) ... ( ( 𝑁 − 1 ) + 1 ) ) = ( 1 ... 𝑁 ) )
14	6 13	breqtrd	⊢ ( 𝑁 ∈ ℤ → ( 0 ... ( 𝑁 − 1 ) ) ≈ ( 1 ... 𝑁 ) )