Metamath Proof Explorer

Theorem elfzom1b

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 Mario Carneiro, 27-Sep-2015)

Ref Expression
Assertion elfzom1b ⊢ K ∈ ℤ ∧ N ∈ ℤ → K ∈ 1 ..^ N ↔ K − 1 ∈ 0 ..^ N − 1

Proof

Step Hyp Ref Expression
1 peano2zm ⊢ N ∈ ℤ → N − 1 ∈ ℤ
2 elfzm1b ⊢ K ∈ ℤ ∧ N − 1 ∈ ℤ → K ∈ 1 … N − 1 ↔ K − 1 ∈ 0 … N - 1 - 1
3 1 2 sylan2 ⊢ K ∈ ℤ ∧ N ∈ ℤ → K ∈ 1 … N − 1 ↔ K − 1 ∈ 0 … N - 1 - 1
4 fzoval ⊢ N ∈ ℤ → 1 ..^ N = 1 … N − 1
5 4 adantl ⊢ K ∈ ℤ ∧ N ∈ ℤ → 1 ..^ N = 1 … N − 1
6 5 eleq2d ⊢ K ∈ ℤ ∧ N ∈ ℤ → K ∈ 1 ..^ N ↔ K ∈ 1 … N − 1
7 1 adantl ⊢ K ∈ ℤ ∧ N ∈ ℤ → N − 1 ∈ ℤ
8 fzoval ⊢ N − 1 ∈ ℤ → 0 ..^ N − 1 = 0 … N - 1 - 1
9 7 8 syl ⊢ K ∈ ℤ ∧ N ∈ ℤ → 0 ..^ N − 1 = 0 … N - 1 - 1
10 9 eleq2d ⊢ K ∈ ℤ ∧ N ∈ ℤ → K − 1 ∈ 0 ..^ N − 1 ↔ K − 1 ∈ 0 … N - 1 - 1
11 3 6 10 3bitr4d ⊢ K ∈ ℤ ∧ N ∈ ℤ → K ∈ 1 ..^ N ↔ K − 1 ∈ 0 ..^ N − 1