Metamath Proof Explorer

Theorem elfzm1b

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

Ref Expression
Assertion elfzm1b ⊢ K ∈ ℤ ∧ N ∈ ℤ → K ∈ 1 … N ↔ K − 1 ∈ 0 … N − 1

Proof

Step Hyp Ref Expression
1 1z ⊢ 1 ∈ ℤ
2 fzsubel ⊢ 1 ∈ ℤ ∧ N ∈ ℤ ∧ K ∈ ℤ ∧ 1 ∈ ℤ → K ∈ 1 … N ↔ K − 1 ∈ 1 − 1 … N − 1
3 1 2 mpanl1 ⊢ N ∈ ℤ ∧ K ∈ ℤ ∧ 1 ∈ ℤ → K ∈ 1 … N ↔ K − 1 ∈ 1 − 1 … N − 1
4 1 3 mpanr2 ⊢ N ∈ ℤ ∧ K ∈ ℤ → K ∈ 1 … N ↔ K − 1 ∈ 1 − 1 … N − 1
5 1m1e0 ⊢ 1 − 1 = 0
6 5 oveq1i ⊢ 1 − 1 … N − 1 = 0 … N − 1
7 6 eleq2i ⊢ K − 1 ∈ 1 − 1 … N − 1 ↔ K − 1 ∈ 0 … N − 1
8 4 7 bitrdi ⊢ N ∈ ℤ ∧ K ∈ ℤ → K ∈ 1 … N ↔ K − 1 ∈ 0 … N − 1
9 8 ancoms ⊢ K ∈ ℤ ∧ N ∈ ℤ → K ∈ 1 … N ↔ K − 1 ∈ 0 … N − 1