Metamath Proof Explorer


Theorem mulgt0b2d

Description: Biconditional, deductive form of mulgt0 . The second factor is positive iff the product is. Note that the commuted form cannot be proven since resubdi does not have a commuted form. (Contributed by SN, 26-Jun-2024)

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

Proof

Step Hyp Ref Expression
1 mulgt0b2d.a φ A
2 mulgt0b2d.b φ B
3 mulgt0b2d.1 φ 0 < A
4 1 adantr φ 0 < B A
5 2 adantr φ 0 < B B
6 3 adantr φ 0 < B 0 < A
7 simpr φ 0 < B 0 < B
8 4 5 6 7 mulgt0d φ 0 < B 0 < A B
9 8 ex φ 0 < B 0 < A B
10 1 adantr φ A B 0 - 1 < 0 A
11 1re 1
12 rernegcl 1 0 - 1
13 11 12 mp1i φ 0 - 1
14 2 13 remulcld φ B 0 - 1
15 14 adantr φ A B 0 - 1 < 0 B 0 - 1
16 3 adantr φ A B 0 - 1 < 0 0 < A
17 1 recnd φ A
18 2 recnd φ B
19 13 recnd φ 0 - 1
20 17 18 19 mulassd φ A B 0 - 1 = A B 0 - 1
21 20 breq1d φ A B 0 - 1 < 0 A B 0 - 1 < 0
22 21 biimpa φ A B 0 - 1 < 0 A B 0 - 1 < 0
23 10 15 16 22 mulgt0con2d φ A B 0 - 1 < 0 B 0 - 1 < 0
24 23 ex φ A B 0 - 1 < 0 B 0 - 1 < 0
25 1 2 remulcld φ A B
26 relt0neg2 A B 0 < A B 0 - A B < 0
27 25 26 syl φ 0 < A B 0 - A B < 0
28 1red φ 1
29 25 28 remulneg2d φ A B 0 - 1 = 0 - A B 1
30 ax-1rid A B A B 1 = A B
31 25 30 syl φ A B 1 = A B
32 31 oveq2d φ 0 - A B 1 = 0 - A B
33 29 32 eqtrd φ A B 0 - 1 = 0 - A B
34 33 breq1d φ A B 0 - 1 < 0 0 - A B < 0
35 27 34 bitr4d φ 0 < A B A B 0 - 1 < 0
36 relt0neg2 B 0 < B 0 - B < 0
37 2 36 syl φ 0 < B 0 - B < 0
38 2 28 remulneg2d φ B 0 - 1 = 0 - B 1
39 ax-1rid B B 1 = B
40 2 39 syl φ B 1 = B
41 40 oveq2d φ 0 - B 1 = 0 - B
42 38 41 eqtrd φ B 0 - 1 = 0 - B
43 42 breq1d φ B 0 - 1 < 0 0 - B < 0
44 37 43 bitr4d φ 0 < B B 0 - 1 < 0
45 24 35 44 3imtr4d φ 0 < A B 0 < B
46 9 45 impbid φ 0 < B 0 < A B