fzopred

Description: Join a predecessor to the beginning of an open integer interval. Generalization of fzo0sn0fzo1 . (Contributed by AV, 14-Jul-2020)

		Ref	Expression
	Assertion	fzopred	$⊢ (M \in ℤ \land N \in ℤ \land M < N) \to (M ..^N) = \{M\} \cup (M + 1 ..^N)$

Step	Hyp	Ref	Expression
1		fzolb	$⊢ M \in (M ..^N) \leftrightarrow (M \in ℤ \land N \in ℤ \land M < N)$
2		fzofzp1	$⊢ M \in (M ..^N) \to M + 1 \in (M \dots N)$
3	1 2	sylbir	$⊢ (M \in ℤ \land N \in ℤ \land M < N) \to M + 1 \in (M \dots N)$
4		fzosplit	$⊢ M + 1 \in (M \dots N) \to (M ..^N) = (M ..^M + 1) \cup (M + 1 ..^N)$
5	3 4	syl	$⊢ (M \in ℤ \land N \in ℤ \land M < N) \to (M ..^N) = (M ..^M + 1) \cup (M + 1 ..^N)$
6		fzosn	$⊢ M \in ℤ \to (M ..^M + 1) = \{M\}$
7	6	3ad2ant1	$⊢ (M \in ℤ \land N \in ℤ \land M < N) \to (M ..^M + 1) = \{M\}$
8	7	uneq1d	$⊢ (M \in ℤ \land N \in ℤ \land M < N) \to (M ..^M + 1) \cup (M + 1 ..^N) = \{M\} \cup (M + 1 ..^N)$
9	5 8	eqtrd	$⊢ (M \in ℤ \land N \in ℤ \land M < N) \to (M ..^N) = \{M\} \cup (M + 1 ..^N)$

Metamath Proof Explorer