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 ( ( 𝐾 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( 𝐾 ∈ ( 1 ... 𝑁 ) ↔ ( 𝐾 − 1 ) ∈ ( 0 ... ( 𝑁 − 1 ) ) ) )

Proof

Step Hyp Ref Expression
1 1z 1 ∈ ℤ
2 fzsubel ( ( ( 1 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ( 𝐾 ∈ ℤ ∧ 1 ∈ ℤ ) ) → ( 𝐾 ∈ ( 1 ... 𝑁 ) ↔ ( 𝐾 − 1 ) ∈ ( ( 1 − 1 ) ... ( 𝑁 − 1 ) ) ) )
3 1 2 mpanl1 ( ( 𝑁 ∈ ℤ ∧ ( 𝐾 ∈ ℤ ∧ 1 ∈ ℤ ) ) → ( 𝐾 ∈ ( 1 ... 𝑁 ) ↔ ( 𝐾 − 1 ) ∈ ( ( 1 − 1 ) ... ( 𝑁 − 1 ) ) ) )
4 1 3 mpanr2 ( ( 𝑁 ∈ ℤ ∧ 𝐾 ∈ ℤ ) → ( 𝐾 ∈ ( 1 ... 𝑁 ) ↔ ( 𝐾 − 1 ) ∈ ( ( 1 − 1 ) ... ( 𝑁 − 1 ) ) ) )
5 1m1e0 ( 1 − 1 ) = 0
6 5 oveq1i ( ( 1 − 1 ) ... ( 𝑁 − 1 ) ) = ( 0 ... ( 𝑁 − 1 ) )
7 6 eleq2i ( ( 𝐾 − 1 ) ∈ ( ( 1 − 1 ) ... ( 𝑁 − 1 ) ) ↔ ( 𝐾 − 1 ) ∈ ( 0 ... ( 𝑁 − 1 ) ) )
8 4 7 bitrdi ( ( 𝑁 ∈ ℤ ∧ 𝐾 ∈ ℤ ) → ( 𝐾 ∈ ( 1 ... 𝑁 ) ↔ ( 𝐾 − 1 ) ∈ ( 0 ... ( 𝑁 − 1 ) ) ) )
9 8 ancoms ( ( 𝐾 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( 𝐾 ∈ ( 1 ... 𝑁 ) ↔ ( 𝐾 − 1 ) ∈ ( 0 ... ( 𝑁 − 1 ) ) ) )