Metamath Proof Explorer

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 ⊢ N ∈ ℤ → 0 … N − 1 ≈ 1 … N

Proof

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