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	$⊢ (K \in (M ..^N) \land K \neq M) \to K - 1 \in (M ..^N - 1)$

Step	Hyp	Ref	Expression
1		fzone1	$⊢ (K \in (M ..^N) \land K \neq M) \to K \in (M + 1 ..^N)$
2		1z	$⊢ 1 \in ℤ$
3		fzosubel	$⊢ (K \in (M + 1 ..^N) \land 1 \in ℤ) \to K - 1 \in (M + 1 - 1 ..^N - 1)$
4	1 2 3	sylancl	$⊢ (K \in (M ..^N) \land K \neq M) \to K - 1 \in (M + 1 - 1 ..^N - 1)$
5		elfzoel1	$⊢ K \in (M ..^N) \to M \in ℤ$
6	5	adantr	$⊢ (K \in (M ..^N) \land K \neq M) \to M \in ℤ$
7	6	zcnd	$⊢ (K \in (M ..^N) \land K \neq M) \to M \in ℂ$
8		1cnd	$⊢ (K \in (M ..^N) \land K \neq M) \to 1 \in ℂ$
9	7 8	pncand	$⊢ (K \in (M ..^N) \land K \neq M) \to M + 1 - 1 = M$
10	9	oveq1d	$⊢ (K \in (M ..^N) \land K \neq M) \to (M + 1 - 1 ..^N - 1) = (M ..^N - 1)$
11	4 10	eleqtrd	$⊢ (K \in (M ..^N) \land K \neq M) \to K - 1 \in (M ..^N - 1)$

Metamath Proof Explorer