fzodisj

Description: Abutting half-open integer ranges are disjoint. (Contributed by Stefan O'Rear, 14-Aug-2015)

		Ref	Expression
	Assertion	fzodisj	$⊢ (A ..^B) \cap (B ..^C) = \emptyset$

Step	Hyp	Ref	Expression
1		disj1	$⊢ (A ..^B) \cap (B ..^C) = \emptyset \leftrightarrow \forall x (x \in (A ..^B) \to \neg x \in (B ..^C))$
2		elfzolt2	$⊢ x \in (A ..^B) \to x < B$
3		elfzoelz	$⊢ x \in (A ..^B) \to x \in ℤ$
4	3	zred	$⊢ x \in (A ..^B) \to x \in ℝ$
5		elfzoel2	$⊢ x \in (A ..^B) \to B \in ℤ$
6	5	zred	$⊢ x \in (A ..^B) \to B \in ℝ$
7	4 6	ltnled	$⊢ x \in (A ..^B) \to (x < B \leftrightarrow \neg B \leq x)$
8	2 7	mpbid	$⊢ x \in (A ..^B) \to \neg B \leq x$
9		elfzole1	$⊢ x \in (B ..^C) \to B \leq x$
10	8 9	nsyl	$⊢ x \in (A ..^B) \to \neg x \in (B ..^C)$
11	1 10	mpgbir	$⊢ (A ..^B) \cap (B ..^C) = \emptyset$

Metamath Proof Explorer