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

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 ) ) ) )