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

Step	Hyp	Ref	Expression
1		fzne1	$⊢ (K \in (M \dots N) \land K \neq M) \to K \in (M + 1 \dots N)$
2		elfzel1	$⊢ K \in (M + 1 \dots N) \to M + 1 \in ℤ$
3		elfzel2	$⊢ K \in (M + 1 \dots N) \to N \in ℤ$
4		elfzelz	$⊢ K \in (M + 1 \dots N) \to K \in ℤ$
5		1zzd	$⊢ K \in (M + 1 \dots N) \to 1 \in ℤ$
6		id	$⊢ K \in (M + 1 \dots N) \to K \in (M + 1 \dots N)$
7		fzsubel	$⊢ ((M + 1 \in ℤ \land N \in ℤ) \land (K \in ℤ \land 1 \in ℤ)) \to (K \in (M + 1 \dots N) \leftrightarrow K - 1 \in (M + 1 - 1 \dots N - 1))$
8	7	biimp3a	$⊢ ((M + 1 \in ℤ \land N \in ℤ) \land (K \in ℤ \land 1 \in ℤ) \land K \in (M + 1 \dots N)) \to K - 1 \in (M + 1 - 1 \dots N - 1)$
9	2 3 4 5 6 8	syl221anc	$⊢ K \in (M + 1 \dots N) \to K - 1 \in (M + 1 - 1 \dots N - 1)$
10	1 9	syl	$⊢ (K \in (M \dots N) \land K \neq M) \to K - 1 \in (M + 1 - 1 \dots N - 1)$
11		elfzel1	$⊢ K \in (M \dots N) \to M \in ℤ$
12	11	adantr	$⊢ (K \in (M \dots N) \land K \neq M) \to M \in ℤ$
13	12	zcnd	$⊢ (K \in (M \dots N) \land K \neq M) \to M \in ℂ$
14		1cnd	$⊢ (K \in (M \dots N) \land K \neq M) \to 1 \in ℂ$
15	13 14	pncand	$⊢ (K \in (M \dots N) \land K \neq M) \to M + 1 - 1 = M$
16	15	oveq1d	$⊢ (K \in (M \dots N) \land K \neq M) \to (M + 1 - 1 \dots N - 1) = (M \dots N - 1)$
17	10 16	eleqtrd	$⊢ (K \in (M \dots N) \land K \neq M) \to K - 1 \in (M \dots N - 1)$

Metamath Proof Explorer