Theorem fzodisjsn

Description: A half-open integer range and the singleton of its upper bound are disjoint. (Contributed by AV, 7-Mar-2021)

	Ref	Expression
Assertion	fzodisjsn	$$⊢\left(A..^B\right)\cap \left\{B\right\}=\varnothing$$

Proof

Step	Hyp	Ref	Expression
1		disj1	$$⊢\left(A..^B\right)\cap \left\{B\right\}=\varnothing \leftrightarrow \forall x\left(x\in \left(A..^B\right)\to \neg x\in \left\{B\right\}\right)$$
2		elfzoelz	$$⊢x\in \left(A..^B\right)\to x\in \mathbb{Z}$$
3	2	zred	$$⊢x\in \left(A..^B\right)\to x\in ℝ$$
4		elfzolt2	$$⊢x\in \left(A..^B\right)\to x<B$$
5	3 4	ltned	$$⊢x\in \left(A..^B\right)\to x\ne B$$
6	5	neneqd	$$⊢x\in \left(A..^B\right)\to \neg x=B$$
7		elsni	$$⊢x\in \left\{B\right\}\to x=B$$
8	6 7	nsyl	$$⊢x\in \left(A..^B\right)\to \neg x\in \left\{B\right\}$$
9	1 8	mpgbir	$$⊢\left(A..^B\right)\cap \left\{B\right\}=\varnothing$$