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

Metamath Proof Explorer

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