This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ( 𝑁 ∈ ℤ → ( 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 ... 𝑁 ) )