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

Metamath Proof Explorer

Theorem fzom1ne1

Description: Elementhood in a half-open interval, except the lower bound, shifted by one. (Contributed by Thierry Arnoux, 1-Jan-2024)

Ref Expression
Assertion fzom1ne1 ( ( 𝐾 ∈ ( 𝑀 ..^ 𝑁 ) ∧ 𝐾 ≠ 𝑀 ) → ( 𝐾 − 1 ) ∈ ( 𝑀 ..^ ( 𝑁 − 1 ) ) )

Proof

Step Hyp Ref Expression
1 fzone1 ⊢ ( ( 𝐾 ∈ ( 𝑀 ..^ 𝑁 ) ∧ 𝐾 ≠ 𝑀 ) → 𝐾 ∈ ( ( 𝑀 + 1 ) ..^ 𝑁 ) )
2 1z ⊢ 1 ∈ ℤ
3 fzosubel ⊢ ( ( 𝐾 ∈ ( ( 𝑀 + 1 ) ..^ 𝑁 ) ∧ 1 ∈ ℤ ) → ( 𝐾 − 1 ) ∈ ( ( ( 𝑀 + 1 ) − 1 ) ..^ ( 𝑁 − 1 ) ) )
4 1 2 3 sylancl ⊢ ( ( 𝐾 ∈ ( 𝑀 ..^ 𝑁 ) ∧ 𝐾 ≠ 𝑀 ) → ( 𝐾 − 1 ) ∈ ( ( ( 𝑀 + 1 ) − 1 ) ..^ ( 𝑁 − 1 ) ) )
5 elfzoel1 ⊢ ( 𝐾 ∈ ( 𝑀 ..^ 𝑁 ) → 𝑀 ∈ ℤ )
6 5 adantr ⊢ ( ( 𝐾 ∈ ( 𝑀 ..^ 𝑁 ) ∧ 𝐾 ≠ 𝑀 ) → 𝑀 ∈ ℤ )
7 6 zcnd ⊢ ( ( 𝐾 ∈ ( 𝑀 ..^ 𝑁 ) ∧ 𝐾 ≠ 𝑀 ) → 𝑀 ∈ ℂ )
8 1cnd ⊢ ( ( 𝐾 ∈ ( 𝑀 ..^ 𝑁 ) ∧ 𝐾 ≠ 𝑀 ) → 1 ∈ ℂ )
9 7 8 pncand ⊢ ( ( 𝐾 ∈ ( 𝑀 ..^ 𝑁 ) ∧ 𝐾 ≠ 𝑀 ) → ( ( 𝑀 + 1 ) − 1 ) = 𝑀 )
10 9 oveq1d ⊢ ( ( 𝐾 ∈ ( 𝑀 ..^ 𝑁 ) ∧ 𝐾 ≠ 𝑀 ) → ( ( ( 𝑀 + 1 ) − 1 ) ..^ ( 𝑁 − 1 ) ) = ( 𝑀 ..^ ( 𝑁 − 1 ) ) )
11 4 10 eleqtrd ⊢ ( ( 𝐾 ∈ ( 𝑀 ..^ 𝑁 ) ∧ 𝐾 ≠ 𝑀 ) → ( 𝐾 − 1 ) ∈ ( 𝑀 ..^ ( 𝑁 − 1 ) ) )