prinfzo0

Description: The intersection of a half-open integer range and the pair of its outer left borders is empty. (Contributed by AV, 9-Jan-2021)

		Ref	Expression
	Assertion	prinfzo0	$⊢ M \in ℤ \to \{M, N\} \cap (M + 1 ..^N) = \emptyset$

Proof

Step	Hyp	Ref	Expression
1		elfz3	$⊢ M \in ℤ \to M \in (M \dots M)$
2		fznuz	$⊢ M \in (M \dots M) \to \neg M \in ℤ_{\geq (M + 1)}$
3	1 2	syl	$⊢ M \in ℤ \to \neg M \in ℤ_{\geq (M + 1)}$
4	3	3mix1d	$⊢ M \in ℤ \to (\neg M \in ℤ_{\geq (M + 1)} \lor \neg N \in ℤ \lor \neg M < N)$
5		3ianor	$⊢ \neg (M \in ℤ_{\geq (M + 1)} \land N \in ℤ \land M < N) \leftrightarrow (\neg M \in ℤ_{\geq (M + 1)} \lor \neg N \in ℤ \lor \neg M < N)$
6		elfzo2	$⊢ M \in (M + 1 ..^N) \leftrightarrow (M \in ℤ_{\geq (M + 1)} \land N \in ℤ \land M < N)$
7	5 6	xchnxbir	$⊢ \neg M \in (M + 1 ..^N) \leftrightarrow (\neg M \in ℤ_{\geq (M + 1)} \lor \neg N \in ℤ \lor \neg M < N)$
8	4 7	sylibr	$⊢ M \in ℤ \to \neg M \in (M + 1 ..^N)$
9		incom	$⊢ \{M\} \cap (M + 1 ..^N) = (M + 1 ..^N) \cap \{M\}$
10	9	eqeq1i	$⊢ \{M\} \cap (M + 1 ..^N) = \emptyset \leftrightarrow (M + 1 ..^N) \cap \{M\} = \emptyset$
11		disjsn	$⊢ (M + 1 ..^N) \cap \{M\} = \emptyset \leftrightarrow \neg M \in (M + 1 ..^N)$
12	10 11	bitri	$⊢ \{M\} \cap (M + 1 ..^N) = \emptyset \leftrightarrow \neg M \in (M + 1 ..^N)$
13	8 12	sylibr	$⊢ M \in ℤ \to \{M\} \cap (M + 1 ..^N) = \emptyset$
14		fzonel	$⊢ \neg N \in (M + 1 ..^N)$
15	14	a1i	$⊢ M \in ℤ \to \neg N \in (M + 1 ..^N)$
16		incom	$⊢ \{N\} \cap (M + 1 ..^N) = (M + 1 ..^N) \cap \{N\}$
17	16	eqeq1i	$⊢ \{N\} \cap (M + 1 ..^N) = \emptyset \leftrightarrow (M + 1 ..^N) \cap \{N\} = \emptyset$
18		disjsn	$⊢ (M + 1 ..^N) \cap \{N\} = \emptyset \leftrightarrow \neg N \in (M + 1 ..^N)$
19	17 18	bitri	$⊢ \{N\} \cap (M + 1 ..^N) = \emptyset \leftrightarrow \neg N \in (M + 1 ..^N)$
20	15 19	sylibr	$⊢ M \in ℤ \to \{N\} \cap (M + 1 ..^N) = \emptyset$
21		df-pr	$⊢ \{M, N\} = \{M\} \cup \{N\}$
22	21	ineq1i	$⊢ \{M, N\} \cap (M + 1 ..^N) = (\{M\} \cup \{N\}) \cap (M + 1 ..^N)$
23	22	eqeq1i	$⊢ \{M, N\} \cap (M + 1 ..^N) = \emptyset \leftrightarrow (\{M\} \cup \{N\}) \cap (M + 1 ..^N) = \emptyset$
24		undisj1	$⊢ (\{M\} \cap (M + 1 ..^N) = \emptyset \land \{N\} \cap (M + 1 ..^N) = \emptyset) \leftrightarrow (\{M\} \cup \{N\}) \cap (M + 1 ..^N) = \emptyset$
25	23 24	bitr4i	$⊢ \{M, N\} \cap (M + 1 ..^N) = \emptyset \leftrightarrow (\{M\} \cap (M + 1 ..^N) = \emptyset \land \{N\} \cap (M + 1 ..^N) = \emptyset)$
26	13 20 25	sylanbrc	$⊢ M \in ℤ \to \{M, N\} \cap (M + 1 ..^N) = \emptyset$

Metamath Proof Explorer

Theorem prinfzo0

Proof