fzdif1

Description: Split the first element of a finite set of sequential integers. More generic than fzpred . Analogous to fzdif2 . (Contributed by AV, 12-Sep-2025)

		Ref	Expression
	Assertion	fzdif1	$⊢ N \in ℤ_{\geq M} \to (M \dots N) ∖ \{M\} = (M + 1 \dots N)$

Proof

Step	Hyp	Ref	Expression
1		eldif	$⊢ x \in ((M \dots N) ∖ \{M\}) \leftrightarrow (x \in (M \dots N) \land \neg x \in \{M\})$
2		elsng	$⊢ x \in (M \dots N) \to (x \in \{M\} \leftrightarrow x = M)$
3	2	necon3bbid	$⊢ x \in (M \dots N) \to (\neg x \in \{M\} \leftrightarrow x \neq M)$
4		fzne1	$⊢ (x \in (M \dots N) \land x \neq M) \to x \in (M + 1 \dots N)$
5	3 4	sylbida	$⊢ (x \in (M \dots N) \land \neg x \in \{M\}) \to x \in (M + 1 \dots N)$
6		eluzel2	$⊢ N \in ℤ_{\geq M} \to M \in ℤ$
7	6	uzidd	$⊢ N \in ℤ_{\geq M} \to M \in ℤ_{\geq M}$
8		peano2uz	$⊢ M \in ℤ_{\geq M} \to M + 1 \in ℤ_{\geq M}$
9		fzss1	$⊢ M + 1 \in ℤ_{\geq M} \to (M + 1 \dots N) \subseteq (M \dots N)$
10	7 8 9	3syl	$⊢ N \in ℤ_{\geq M} \to (M + 1 \dots N) \subseteq (M \dots N)$
11	10	sselda	$⊢ (N \in ℤ_{\geq M} \land x \in (M + 1 \dots N)) \to x \in (M \dots N)$
12		elfz2	$⊢ x \in (M + 1 \dots N) \leftrightarrow ((M + 1 \in ℤ \land N \in ℤ \land x \in ℤ) \land (M + 1 \leq x \land x \leq N))$
13	6	zred	$⊢ N \in ℤ_{\geq M} \to M \in ℝ$
14	13	adantl	$⊢ (((M + 1 \in ℤ \land N \in ℤ \land x \in ℤ) \land (M + 1 \leq x \land x \leq N)) \land N \in ℤ_{\geq M}) \to M \in ℝ$
15		simp3	$⊢ (M + 1 \in ℤ \land N \in ℤ \land x \in ℤ) \to x \in ℤ$
16		zltp1le	$⊢ (M \in ℤ \land x \in ℤ) \to (M < x \leftrightarrow M + 1 \leq x)$
17	6 15 16	syl2anr	$⊢ ((M + 1 \in ℤ \land N \in ℤ \land x \in ℤ) \land N \in ℤ_{\geq M}) \to (M < x \leftrightarrow M + 1 \leq x)$
18	17	biimprd	$⊢ ((M + 1 \in ℤ \land N \in ℤ \land x \in ℤ) \land N \in ℤ_{\geq M}) \to (M + 1 \leq x \to M < x)$
19	18	a1d	$⊢ ((M + 1 \in ℤ \land N \in ℤ \land x \in ℤ) \land N \in ℤ_{\geq M}) \to (x \leq N \to (M + 1 \leq x \to M < x))$
20	19	ex	$⊢ (M + 1 \in ℤ \land N \in ℤ \land x \in ℤ) \to (N \in ℤ_{\geq M} \to (x \leq N \to (M + 1 \leq x \to M < x)))$
21	20	com24	$⊢ (M + 1 \in ℤ \land N \in ℤ \land x \in ℤ) \to (M + 1 \leq x \to (x \leq N \to (N \in ℤ_{\geq M} \to M < x)))$
22	21	imp42	$⊢ (((M + 1 \in ℤ \land N \in ℤ \land x \in ℤ) \land (M + 1 \leq x \land x \leq N)) \land N \in ℤ_{\geq M}) \to M < x$
23	14 22	gtned	$⊢ (((M + 1 \in ℤ \land N \in ℤ \land x \in ℤ) \land (M + 1 \leq x \land x \leq N)) \land N \in ℤ_{\geq M}) \to x \neq M$
24	23	ex	$⊢ ((M + 1 \in ℤ \land N \in ℤ \land x \in ℤ) \land (M + 1 \leq x \land x \leq N)) \to (N \in ℤ_{\geq M} \to x \neq M)$
25	12 24	sylbi	$⊢ x \in (M + 1 \dots N) \to (N \in ℤ_{\geq M} \to x \neq M)$
26	25	impcom	$⊢ (N \in ℤ_{\geq M} \land x \in (M + 1 \dots N)) \to x \neq M$
27		nelsn	$⊢ x \neq M \to \neg x \in \{M\}$
28	26 27	syl	$⊢ (N \in ℤ_{\geq M} \land x \in (M + 1 \dots N)) \to \neg x \in \{M\}$
29	11 28	jca	$⊢ (N \in ℤ_{\geq M} \land x \in (M + 1 \dots N)) \to (x \in (M \dots N) \land \neg x \in \{M\})$
30	29	ex	$⊢ N \in ℤ_{\geq M} \to (x \in (M + 1 \dots N) \to (x \in (M \dots N) \land \neg x \in \{M\}))$
31	5 30	impbid2	$⊢ N \in ℤ_{\geq M} \to ((x \in (M \dots N) \land \neg x \in \{M\}) \leftrightarrow x \in (M + 1 \dots N))$
32	1 31	bitrid	$⊢ N \in ℤ_{\geq M} \to (x \in ((M \dots N) ∖ \{M\}) \leftrightarrow x \in (M + 1 \dots N))$
33	32	eqrdv	$⊢ N \in ℤ_{\geq M} \to (M \dots N) ∖ \{M\} = (M + 1 \dots N)$

Metamath Proof Explorer

Theorem fzdif1

Proof