Metamath Proof Explorer


Theorem mulgt0con1dlem

Description: Lemma for mulgt0con1d . Contraposes a positive deduction to a negative deduction. (Contributed by SN, 26-Jun-2024)

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

Proof

Step Hyp Ref Expression
1 mulgt0con1dlem.a φ A
2 mulgt0con1dlem.b φ B
3 mulgt0con1dlem.1 φ 0 < A 0 < B
4 mulgt0con1dlem.2 φ A = 0 B = 0
5 0red φ 0
6 2 5 lttrid φ B < 0 ¬ B = 0 0 < B
7 4 3 orim12d φ A = 0 0 < A B = 0 0 < B
8 7 con3d φ ¬ B = 0 0 < B ¬ A = 0 0 < A
9 1 5 lttrid φ A < 0 ¬ A = 0 0 < A
10 8 9 sylibrd φ ¬ B = 0 0 < B A < 0
11 6 10 sylbid φ B < 0 A < 0