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