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 ⊢ K ∈ ℤ ∧ N ∈ ℤ → K ∈ 0 … N − 1 ↔ K + 1 ∈ 1 … N

Proof

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