Theorem fzm1ne1

Description: Elementhood of an integer and its predecessor in finite intervals of integers. (Contributed by Thierry Arnoux, 1-Jan-2024)

	Ref	Expression
Assertion	fzm1ne1	⊢ ( ( 𝐾 ∈ ( 𝑀 ... 𝑁 ) ∧ 𝐾 ≠ 𝑀 ) → ( 𝐾 − 1 ) ∈ ( 𝑀 ... ( 𝑁 − 1 ) ) )

Proof

Step	Hyp	Ref	Expression
1		fzne1	⊢ ( ( 𝐾 ∈ ( 𝑀 ... 𝑁 ) ∧ 𝐾 ≠ 𝑀 ) → 𝐾 ∈ ( ( 𝑀 + 1 ) ... 𝑁 ) )
2		elfzel1	⊢ ( 𝐾 ∈ ( ( 𝑀 + 1 ) ... 𝑁 ) → ( 𝑀 + 1 ) ∈ ℤ )
3		elfzel2	⊢ ( 𝐾 ∈ ( ( 𝑀 + 1 ) ... 𝑁 ) → 𝑁 ∈ ℤ )
4		elfzelz	⊢ ( 𝐾 ∈ ( ( 𝑀 + 1 ) ... 𝑁 ) → 𝐾 ∈ ℤ )
5		1zzd	⊢ ( 𝐾 ∈ ( ( 𝑀 + 1 ) ... 𝑁 ) → 1 ∈ ℤ )
6		id	⊢ ( 𝐾 ∈ ( ( 𝑀 + 1 ) ... 𝑁 ) → 𝐾 ∈ ( ( 𝑀 + 1 ) ... 𝑁 ) )
7		fzsubel	⊢ ( ( ( ( 𝑀 + 1 ) ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ( 𝐾 ∈ ℤ ∧ 1 ∈ ℤ ) ) → ( 𝐾 ∈ ( ( 𝑀 + 1 ) ... 𝑁 ) ↔ ( 𝐾 − 1 ) ∈ ( ( ( 𝑀 + 1 ) − 1 ) ... ( 𝑁 − 1 ) ) ) )
8	7	biimp3a	⊢ ( ( ( ( 𝑀 + 1 ) ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ( 𝐾 ∈ ℤ ∧ 1 ∈ ℤ ) ∧ 𝐾 ∈ ( ( 𝑀 + 1 ) ... 𝑁 ) ) → ( 𝐾 − 1 ) ∈ ( ( ( 𝑀 + 1 ) − 1 ) ... ( 𝑁 − 1 ) ) )
9	2 3 4 5 6 8	syl221anc	⊢ ( 𝐾 ∈ ( ( 𝑀 + 1 ) ... 𝑁 ) → ( 𝐾 − 1 ) ∈ ( ( ( 𝑀 + 1 ) − 1 ) ... ( 𝑁 − 1 ) ) )
10	1 9	syl	⊢ ( ( 𝐾 ∈ ( 𝑀 ... 𝑁 ) ∧ 𝐾 ≠ 𝑀 ) → ( 𝐾 − 1 ) ∈ ( ( ( 𝑀 + 1 ) − 1 ) ... ( 𝑁 − 1 ) ) )
11		elfzel1	⊢ ( 𝐾 ∈ ( 𝑀 ... 𝑁 ) → 𝑀 ∈ ℤ )
12	11	adantr	⊢ ( ( 𝐾 ∈ ( 𝑀 ... 𝑁 ) ∧ 𝐾 ≠ 𝑀 ) → 𝑀 ∈ ℤ )
13	12	zcnd	⊢ ( ( 𝐾 ∈ ( 𝑀 ... 𝑁 ) ∧ 𝐾 ≠ 𝑀 ) → 𝑀 ∈ ℂ )
14		1cnd	⊢ ( ( 𝐾 ∈ ( 𝑀 ... 𝑁 ) ∧ 𝐾 ≠ 𝑀 ) → 1 ∈ ℂ )
15	13 14	pncand	⊢ ( ( 𝐾 ∈ ( 𝑀 ... 𝑁 ) ∧ 𝐾 ≠ 𝑀 ) → ( ( 𝑀 + 1 ) − 1 ) = 𝑀 )
16	15	oveq1d	⊢ ( ( 𝐾 ∈ ( 𝑀 ... 𝑁 ) ∧ 𝐾 ≠ 𝑀 ) → ( ( ( 𝑀 + 1 ) − 1 ) ... ( 𝑁 − 1 ) ) = ( 𝑀 ... ( 𝑁 − 1 ) ) )
17	10 16	eleqtrd	⊢ ( ( 𝐾 ∈ ( 𝑀 ... 𝑁 ) ∧ 𝐾 ≠ 𝑀 ) → ( 𝐾 − 1 ) ∈ ( 𝑀 ... ( 𝑁 − 1 ) ) )