This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem fzonel

Description: A half-open range does not contain its right endpoint. (Contributed by Stefan O'Rear, 25-Aug-2015)

		Ref	Expression
	Assertion	fzonel	$⊢ \neg B \in (A ..^B)$

Step	Hyp	Ref	Expression
1		elfzolt2	$⊢ B \in (A ..^B) \to B < B$
2		elfzoel2	$⊢ B \in (A ..^B) \to B \in ℤ$
3	2	zred	$⊢ B \in (A ..^B) \to B \in ℝ$
4	3	ltnrd	$⊢ B \in (A ..^B) \to \neg B < B$
5	1 4	pm2.65i	$⊢ \neg B \in (A ..^B)$