fzdifsuc

Description: Remove a successor from the end of a finite set of sequential integers. (Contributed by AV, 4-Sep-2019)

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

Step	Hyp	Ref	Expression
1		fzsuc	$⊢ N \in ℤ_{\geq M} \to (M \dots N + 1) = (M \dots N) \cup \{N + 1\}$
2	1	difeq1d	$⊢ N \in ℤ_{\geq M} \to (M \dots N + 1) ∖ \{N + 1\} = ((M \dots N) \cup \{N + 1\}) ∖ \{N + 1\}$
3		uncom	$⊢ \{N + 1\} \cup (M \dots N) = (M \dots N) \cup \{N + 1\}$
4		ssun2	$⊢ \{N + 1\} \subseteq (M \dots N) \cup \{N + 1\}$
5		incom	$⊢ \{N + 1\} \cap (M \dots N) = (M \dots N) \cap \{N + 1\}$
6		fzp1disj	$⊢ (M \dots N) \cap \{N + 1\} = \emptyset$
7	5 6	eqtri	$⊢ \{N + 1\} \cap (M \dots N) = \emptyset$
8	7	a1i	$⊢ N \in ℤ_{\geq M} \to \{N + 1\} \cap (M \dots N) = \emptyset$
9		uneqdifeq	$⊢ (\{N + 1\} \subseteq (M \dots N) \cup \{N + 1\} \land \{N + 1\} \cap (M \dots N) = \emptyset) \to (\{N + 1\} \cup (M \dots N) = (M \dots N) \cup \{N + 1\} \leftrightarrow ((M \dots N) \cup \{N + 1\}) ∖ \{N + 1\} = (M \dots N))$
10	4 8 9	sylancr	$⊢ N \in ℤ_{\geq M} \to (\{N + 1\} \cup (M \dots N) = (M \dots N) \cup \{N + 1\} \leftrightarrow ((M \dots N) \cup \{N + 1\}) ∖ \{N + 1\} = (M \dots N))$
11	3 10	mpbii	$⊢ N \in ℤ_{\geq M} \to ((M \dots N) \cup \{N + 1\}) ∖ \{N + 1\} = (M \dots N)$
12	2 11	eqtr2d	$⊢ N \in ℤ_{\geq M} \to (M \dots N) = (M \dots N + 1) ∖ \{N + 1\}$

Metamath Proof Explorer