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