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 ∈ ℝ
5		0re	⊢ 0 ∈ ℝ
6	4 5	ltnegcon1i	⊢ ( - 1 < 0 ↔ - 0 < 1 )
7	3 6	mpbir	⊢ - 1 < 0