Metamath Proof Explorer

Theorem fzouzdisj

Description: A half-open integer range does not overlap the upper integer range starting at the endpoint of the first range. (Contributed by Mario Carneiro, 21-Sep-2016)

		Ref	Expression
	Assertion	fzouzdisj	$⊢ (A ..^B) \cap ℤ_{\geq B} = \emptyset$

Proof

Step	Hyp	Ref	Expression
1		elfzolt2	$⊢ x \in (A ..^B) \to x < B$
2	1	adantr	$⊢ (x \in (A ..^B) \land x \in ℤ_{\geq B}) \to x < B$
3		eluzel2	$⊢ x \in ℤ_{\geq B} \to B \in ℤ$
4	3	adantl	$⊢ (x \in (A ..^B) \land x \in ℤ_{\geq B}) \to B \in ℤ$
5	4	zred	$⊢ (x \in (A ..^B) \land x \in ℤ_{\geq B}) \to B \in ℝ$
6		eluzelre	$⊢ x \in ℤ_{\geq B} \to x \in ℝ$
7	6	adantl	$⊢ (x \in (A ..^B) \land x \in ℤ_{\geq B}) \to x \in ℝ$
8		eluzle	$⊢ x \in ℤ_{\geq B} \to B \leq x$
9	8	adantl	$⊢ (x \in (A ..^B) \land x \in ℤ_{\geq B}) \to B \leq x$
10	5 7 9	lensymd	$⊢ (x \in (A ..^B) \land x \in ℤ_{\geq B}) \to \neg x < B$
11	2 10	pm2.65i	$⊢ \neg (x \in (A ..^B) \land x \in ℤ_{\geq B})$
12		elin	$⊢ x \in ((A ..^B) \cap ℤ_{\geq B}) \leftrightarrow (x \in (A ..^B) \land x \in ℤ_{\geq B})$
13	11 12	mtbir	$⊢ \neg x \in ((A ..^B) \cap ℤ_{\geq B})$
14	13	nel0	$⊢ (A ..^B) \cap ℤ_{\geq B} = \emptyset$