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

Metamath Proof Explorer

Theorem elfzp1b

Description: An integer is a member of a 0-based finite set of sequential integers iff its successor is a member of the corresponding 1-based set. (Contributed by Paul Chapman, 22-Jun-2011)

Ref Expression
Assertion elfzp1b ( ( 𝐾 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( 𝐾 ∈ ( 0 ... ( 𝑁 − 1 ) ) ↔ ( 𝐾 + 1 ) ∈ ( 1 ... 𝑁 ) ) )

Proof

Step Hyp Ref Expression
1 peano2z ⊢ ( 𝐾 ∈ ℤ → ( 𝐾 + 1 ) ∈ ℤ )
2 1z ⊢ 1 ∈ ℤ
3 fzsubel ⊢ ( ( ( 1 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ( ( 𝐾 + 1 ) ∈ ℤ ∧ 1 ∈ ℤ ) ) → ( ( 𝐾 + 1 ) ∈ ( 1 ... 𝑁 ) ↔ ( ( 𝐾 + 1 ) − 1 ) ∈ ( ( 1 − 1 ) ... ( 𝑁 − 1 ) ) ) )
4 2 3 mpanl1 ⊢ ( ( 𝑁 ∈ ℤ ∧ ( ( 𝐾 + 1 ) ∈ ℤ ∧ 1 ∈ ℤ ) ) → ( ( 𝐾 + 1 ) ∈ ( 1 ... 𝑁 ) ↔ ( ( 𝐾 + 1 ) − 1 ) ∈ ( ( 1 − 1 ) ... ( 𝑁 − 1 ) ) ) )
5 2 4 mpanr2 ⊢ ( ( 𝑁 ∈ ℤ ∧ ( 𝐾 + 1 ) ∈ ℤ ) → ( ( 𝐾 + 1 ) ∈ ( 1 ... 𝑁 ) ↔ ( ( 𝐾 + 1 ) − 1 ) ∈ ( ( 1 − 1 ) ... ( 𝑁 − 1 ) ) ) )
6 1 5 sylan2 ⊢ ( ( 𝑁 ∈ ℤ ∧ 𝐾 ∈ ℤ ) → ( ( 𝐾 + 1 ) ∈ ( 1 ... 𝑁 ) ↔ ( ( 𝐾 + 1 ) − 1 ) ∈ ( ( 1 − 1 ) ... ( 𝑁 − 1 ) ) ) )
7 6 ancoms ⊢ ( ( 𝐾 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( ( 𝐾 + 1 ) ∈ ( 1 ... 𝑁 ) ↔ ( ( 𝐾 + 1 ) − 1 ) ∈ ( ( 1 − 1 ) ... ( 𝑁 − 1 ) ) ) )
8 zcn ⊢ ( 𝐾 ∈ ℤ → 𝐾 ∈ ℂ )
9 ax-1cn ⊢ 1 ∈ ℂ
10 pncan ⊢ ( ( 𝐾 ∈ ℂ ∧ 1 ∈ ℂ ) → ( ( 𝐾 + 1 ) − 1 ) = 𝐾 )
11 8 9 10 sylancl ⊢ ( 𝐾 ∈ ℤ → ( ( 𝐾 + 1 ) − 1 ) = 𝐾 )
12 1m1e0 ⊢ ( 1 − 1 ) = 0
13 12 oveq1i ⊢ ( ( 1 − 1 ) ... ( 𝑁 − 1 ) ) = ( 0 ... ( 𝑁 − 1 ) )
14 13 a1i ⊢ ( 𝐾 ∈ ℤ → ( ( 1 − 1 ) ... ( 𝑁 − 1 ) ) = ( 0 ... ( 𝑁 − 1 ) ) )
15 11 14 eleq12d ⊢ ( 𝐾 ∈ ℤ → ( ( ( 𝐾 + 1 ) − 1 ) ∈ ( ( 1 − 1 ) ... ( 𝑁 − 1 ) ) ↔ 𝐾 ∈ ( 0 ... ( 𝑁 − 1 ) ) ) )
16 15 adantr ⊢ ( ( 𝐾 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( ( ( 𝐾 + 1 ) − 1 ) ∈ ( ( 1 − 1 ) ... ( 𝑁 − 1 ) ) ↔ 𝐾 ∈ ( 0 ... ( 𝑁 − 1 ) ) ) )
17 7 16 bitr2d ⊢ ( ( 𝐾 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( 𝐾 ∈ ( 0 ... ( 𝑁 − 1 ) ) ↔ ( 𝐾 + 1 ) ∈ ( 1 ... 𝑁 ) ) )