Theorem elfzp1b

Description: An integer is a member of a 0-based finite set of sequential integers iff its successor is a member of the corresponding 1-based set. (Contributed by Paul Chapman, 22-Jun-2011)

	Ref	Expression
Assertion	elfzp1b	⊢ ( ( 𝐾 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( 𝐾 ∈ ( 0 ... ( 𝑁 − 1 ) ) ↔ ( 𝐾 + 1 ) ∈ ( 1 ... 𝑁 ) ) )

Proof

Step	Hyp	Ref	Expression
1		peano2z	⊢ ( 𝐾 ∈ ℤ → ( 𝐾 + 1 ) ∈ ℤ )
2		1z	⊢ 1 ∈ ℤ
3		fzsubel	⊢ ( ( ( 1 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ( ( 𝐾 + 1 ) ∈ ℤ ∧ 1 ∈ ℤ ) ) → ( ( 𝐾 + 1 ) ∈ ( 1 ... 𝑁 ) ↔ ( ( 𝐾 + 1 ) − 1 ) ∈ ( ( 1 − 1 ) ... ( 𝑁 − 1 ) ) ) )
4	2 3	mpanl1	⊢ ( ( 𝑁 ∈ ℤ ∧ ( ( 𝐾 + 1 ) ∈ ℤ ∧ 1 ∈ ℤ ) ) → ( ( 𝐾 + 1 ) ∈ ( 1 ... 𝑁 ) ↔ ( ( 𝐾 + 1 ) − 1 ) ∈ ( ( 1 − 1 ) ... ( 𝑁 − 1 ) ) ) )
5	2 4	mpanr2	⊢ ( ( 𝑁 ∈ ℤ ∧ ( 𝐾 + 1 ) ∈ ℤ ) → ( ( 𝐾 + 1 ) ∈ ( 1 ... 𝑁 ) ↔ ( ( 𝐾 + 1 ) − 1 ) ∈ ( ( 1 − 1 ) ... ( 𝑁 − 1 ) ) ) )
6	1 5	sylan2	⊢ ( ( 𝑁 ∈ ℤ ∧ 𝐾 ∈ ℤ ) → ( ( 𝐾 + 1 ) ∈ ( 1 ... 𝑁 ) ↔ ( ( 𝐾 + 1 ) − 1 ) ∈ ( ( 1 − 1 ) ... ( 𝑁 − 1 ) ) ) )
7	6	ancoms	⊢ ( ( 𝐾 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( ( 𝐾 + 1 ) ∈ ( 1 ... 𝑁 ) ↔ ( ( 𝐾 + 1 ) − 1 ) ∈ ( ( 1 − 1 ) ... ( 𝑁 − 1 ) ) ) )
8		zcn	⊢ ( 𝐾 ∈ ℤ → 𝐾 ∈ ℂ )
9		ax-1cn	⊢ 1 ∈ ℂ
10		pncan	⊢ ( ( 𝐾 ∈ ℂ ∧ 1 ∈ ℂ ) → ( ( 𝐾 + 1 ) − 1 ) = 𝐾 )
11	8 9 10	sylancl	⊢ ( 𝐾 ∈ ℤ → ( ( 𝐾 + 1 ) − 1 ) = 𝐾 )
12		1m1e0	⊢ ( 1 − 1 ) = 0
13	12	oveq1i	⊢ ( ( 1 − 1 ) ... ( 𝑁 − 1 ) ) = ( 0 ... ( 𝑁 − 1 ) )
14	13	a1i	⊢ ( 𝐾 ∈ ℤ → ( ( 1 − 1 ) ... ( 𝑁 − 1 ) ) = ( 0 ... ( 𝑁 − 1 ) ) )
15	11 14	eleq12d	⊢ ( 𝐾 ∈ ℤ → ( ( ( 𝐾 + 1 ) − 1 ) ∈ ( ( 1 − 1 ) ... ( 𝑁 − 1 ) ) ↔ 𝐾 ∈ ( 0 ... ( 𝑁 − 1 ) ) ) )
16	15	adantr	⊢ ( ( 𝐾 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( ( ( 𝐾 + 1 ) − 1 ) ∈ ( ( 1 − 1 ) ... ( 𝑁 − 1 ) ) ↔ 𝐾 ∈ ( 0 ... ( 𝑁 − 1 ) ) ) )
17	7 16	bitr2d	⊢ ( ( 𝐾 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( 𝐾 ∈ ( 0 ... ( 𝑁 − 1 ) ) ↔ ( 𝐾 + 1 ) ∈ ( 1 ... 𝑁 ) ) )