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

Metamath Proof Explorer

Theorem mulgt0con1d

Description: Counterpart to mulgt0con2d , though not a lemma. This is the first use of ax-pre-mulgt0 . One direction of mulgt0b2d . (Contributed by SN, 26-Jun-2024)

		Ref	Expression
	Hypotheses	mulgt0con1d.a	$⊢ φ \to A \in ℝ$
		mulgt0con1d.b	$⊢ φ \to B \in ℝ$
		mulgt0con1d.1	$⊢ φ \to 0 < B$
		mulgt0con1d.2	$⊢ φ \to A B < 0$
	Assertion	mulgt0con1d	$⊢ φ \to A < 0$

Proof

Step	Hyp	Ref	Expression
1		mulgt0con1d.a	$⊢ φ \to A \in ℝ$
2		mulgt0con1d.b	$⊢ φ \to B \in ℝ$
3		mulgt0con1d.1	$⊢ φ \to 0 < B$
4		mulgt0con1d.2	$⊢ φ \to A B < 0$
5	1 2	remulcld	$⊢ φ \to A B \in ℝ$
6	1	adantr	$⊢ (φ \land 0 < A) \to A \in ℝ$
7	2	adantr	$⊢ (φ \land 0 < A) \to B \in ℝ$
8		simpr	$⊢ (φ \land 0 < A) \to 0 < A$
9	3	adantr	$⊢ (φ \land 0 < A) \to 0 < B$
10	6 7 8 9	mulgt0d	$⊢ (φ \land 0 < A) \to 0 < A B$
11	10	ex	$⊢ φ \to (0 < A \to 0 < A B)$
12		remul02	$⊢ B \in ℝ \to 0 \cdot B = 0$
13	2 12	syl	$⊢ φ \to 0 \cdot B = 0$
14		oveq1	$⊢ A = 0 \to A B = 0 \cdot B$
15	14	eqeq1d	$⊢ A = 0 \to (A B = 0 \leftrightarrow 0 \cdot B = 0)$
16	13 15	syl5ibrcom	$⊢ φ \to (A = 0 \to A B = 0)$
17	1 5 11 16	mulgt0con1dlem	$⊢ φ \to (A B < 0 \to A < 0)$
18	4 17	mpd	$⊢ φ \to A < 0$