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

Metamath Proof Explorer

Theorem lt0ne0d

Description: Something less than zero is not zero. Deduction form. (Contributed by David Moews, 28-Feb-2017)

		Ref	Expression
	Hypothesis	lt0ne0d.1	$⊢ φ \to A < 0$
	Assertion	lt0ne0d	$⊢ φ \to A \neq 0$

Step	Hyp	Ref	Expression
1		lt0ne0d.1	$⊢ φ \to A < 0$
2		0re	$⊢ 0 \in ℝ$
3	2	ltnri	$⊢ \neg 0 < 0$
4		breq1	$⊢ A = 0 \to (A < 0 \leftrightarrow 0 < 0)$
5	3 4	mtbiri	$⊢ A = 0 \to \neg A < 0$
6	5	necon2ai	$⊢ A < 0 \to A \neq 0$
7	1 6	syl	$⊢ φ \to A \neq 0$