Theorem neg1lt0

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

	Ref	Expression
Assertion	neg1lt0	$$⊢-1<0$$

Proof

Step	Hyp	Ref	Expression
1		neg0	$$⊢-0=0$$
2		0lt1	$$⊢0<1$$
3	1 2	eqbrtri	$$⊢-0<1$$
4		1re	$$⊢1\in ℝ$$
5		0re	$$⊢0\in ℝ$$
6	4 5	ltnegcon1i	$$⊢-1<0\leftrightarrow -0<1$$
7	3 6	mpbir	$$⊢-1<0$$