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

Metamath Proof Explorer

Theorem neg1lt0

Description: -1 is less than 0. (Contributed by David A. Wheeler, 8-Dec-2018)

		Ref	Expression
	Assertion	neg1lt0	$⊢ - 1 < 0$

Step	Hyp	Ref	Expression
1		0lt1	$⊢ 0 < 1$
2		1re	$⊢ 1 \in ℝ$
3		lt0neg2	$⊢ 1 \in ℝ \to (0 < 1 \leftrightarrow - 1 < 0)$
4	2 3	ax-mp	$⊢ 0 < 1 \leftrightarrow - 1 < 0$
5	1 4	mpbi	$⊢ - 1 < 0$