Metamath Proof Explorer


Theorem mulgt0con1d

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

Ref Expression
Hypotheses mulgt0con1d.a φ A
mulgt0con1d.b φ B
mulgt0con1d.1 φ 0 < B
mulgt0con1d.2 φ A B < 0
Assertion mulgt0con1d φ A < 0

Proof

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