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

Metamath Proof Explorer

Theorem fzdif2

Description: Split the last element of a finite set of sequential integers. More generic than fzsuc . (Contributed by Thierry Arnoux, 22-Aug-2020)

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

Proof

Step	Hyp	Ref	Expression
1		fzspl	$⊢ N \in ℤ_{\geq M} \to (M \dots N) = (M \dots N - 1) \cup \{N\}$
2	1	difeq1d	$⊢ N \in ℤ_{\geq M} \to (M \dots N) ∖ \{N\} = ((M \dots N - 1) \cup \{N\}) ∖ \{N\}$
3		difun2	$⊢ ((M \dots N - 1) \cup \{N\}) ∖ \{N\} = (M \dots N - 1) ∖ \{N\}$
4	2 3	eqtrdi	$⊢ N \in ℤ_{\geq M} \to (M \dots N) ∖ \{N\} = (M \dots N - 1) ∖ \{N\}$
5		eluzelz	$⊢ N \in ℤ_{\geq M} \to N \in ℤ$
6		uzid	$⊢ N \in ℤ \to N \in ℤ_{\geq N}$
7		uznfz	$⊢ N \in ℤ_{\geq N} \to \neg N \in (M \dots N - 1)$
8	5 6 7	3syl	$⊢ N \in ℤ_{\geq M} \to \neg N \in (M \dots N - 1)$
9		disjsn	$⊢ (M \dots N - 1) \cap \{N\} = \emptyset \leftrightarrow \neg N \in (M \dots N - 1)$
10	8 9	sylibr	$⊢ N \in ℤ_{\geq M} \to (M \dots N - 1) \cap \{N\} = \emptyset$
11		disjdif2	$⊢ (M \dots N - 1) \cap \{N\} = \emptyset \to (M \dots N - 1) ∖ \{N\} = (M \dots N - 1)$
12	10 11	syl	$⊢ N \in ℤ_{\geq M} \to (M \dots N - 1) ∖ \{N\} = (M \dots N - 1)$
13	4 12	eqtrd	$⊢ N \in ℤ_{\geq M} \to (M \dots N) ∖ \{N\} = (M \dots N - 1)$