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

Proof

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