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 ⊢ ( 𝜑 → 𝐴 ∈ ℝ )
mulgt0b2d.b ⊢ ( 𝜑 → 𝐵 ∈ ℝ )
mulgt0b2d.1 ⊢ ( 𝜑 → 0 < 𝐴 )
Assertion mulgt0b2d ( 𝜑 → ( 0 < 𝐵 ↔ 0 < ( 𝐴 · 𝐵 ) ) )

Proof

Step Hyp Ref Expression
1 mulgt0b2d.a ⊢ ( 𝜑 → 𝐴 ∈ ℝ )
2 mulgt0b2d.b ⊢ ( 𝜑 → 𝐵 ∈ ℝ )
3 mulgt0b2d.1 ⊢ ( 𝜑 → 0 < 𝐴 )
4 1 adantr ⊢ ( ( 𝜑 ∧ 0 < 𝐵 ) → 𝐴 ∈ ℝ )
5 2 adantr ⊢ ( ( 𝜑 ∧ 0 < 𝐵 ) → 𝐵 ∈ ℝ )
6 3 adantr ⊢ ( ( 𝜑 ∧ 0 < 𝐵 ) → 0 < 𝐴 )
7 simpr ⊢ ( ( 𝜑 ∧ 0 < 𝐵 ) → 0 < 𝐵 )
8 4 5 6 7 mulgt0d ⊢ ( ( 𝜑 ∧ 0 < 𝐵 ) → 0 < ( 𝐴 · 𝐵 ) )
9 8 ex ⊢ ( 𝜑 → ( 0 < 𝐵 → 0 < ( 𝐴 · 𝐵 ) ) )
10 1 adantr ⊢ ( ( 𝜑 ∧ ( ( 𝐴 · 𝐵 ) · ( 0 −ℝ 1 ) ) < 0 ) → 𝐴 ∈ ℝ )
11 1re ⊢ 1 ∈ ℝ
12 rernegcl ⊢ ( 1 ∈ ℝ → ( 0 −ℝ 1 ) ∈ ℝ )
13 11 12 mp1i ⊢ ( 𝜑 → ( 0 −ℝ 1 ) ∈ ℝ )
14 2 13 remulcld ⊢ ( 𝜑 → ( 𝐵 · ( 0 −ℝ 1 ) ) ∈ ℝ )
15 14 adantr ⊢ ( ( 𝜑 ∧ ( ( 𝐴 · 𝐵 ) · ( 0 −ℝ 1 ) ) < 0 ) → ( 𝐵 · ( 0 −ℝ 1 ) ) ∈ ℝ )
16 3 adantr ⊢ ( ( 𝜑 ∧ ( ( 𝐴 · 𝐵 ) · ( 0 −ℝ 1 ) ) < 0 ) → 0 < 𝐴 )
17 1 recnd ⊢ ( 𝜑 → 𝐴 ∈ ℂ )
18 2 recnd ⊢ ( 𝜑 → 𝐵 ∈ ℂ )
19 13 recnd ⊢ ( 𝜑 → ( 0 −ℝ 1 ) ∈ ℂ )
20 17 18 19 mulassd ⊢ ( 𝜑 → ( ( 𝐴 · 𝐵 ) · ( 0 −ℝ 1 ) ) = ( 𝐴 · ( 𝐵 · ( 0 −ℝ 1 ) ) ) )
21 20 breq1d ⊢ ( 𝜑 → ( ( ( 𝐴 · 𝐵 ) · ( 0 −ℝ 1 ) ) < 0 ↔ ( 𝐴 · ( 𝐵 · ( 0 −ℝ 1 ) ) ) < 0 ) )
22 21 biimpa ⊢ ( ( 𝜑 ∧ ( ( 𝐴 · 𝐵 ) · ( 0 −ℝ 1 ) ) < 0 ) → ( 𝐴 · ( 𝐵 · ( 0 −ℝ 1 ) ) ) < 0 )
23 10 15 16 22 mulgt0con2d ⊢ ( ( 𝜑 ∧ ( ( 𝐴 · 𝐵 ) · ( 0 −ℝ 1 ) ) < 0 ) → ( 𝐵 · ( 0 −ℝ 1 ) ) < 0 )
24 23 ex ⊢ ( 𝜑 → ( ( ( 𝐴 · 𝐵 ) · ( 0 −ℝ 1 ) ) < 0 → ( 𝐵 · ( 0 −ℝ 1 ) ) < 0 ) )
25 1 2 remulcld ⊢ ( 𝜑 → ( 𝐴 · 𝐵 ) ∈ ℝ )
26 relt0neg2 ⊢ ( ( 𝐴 · 𝐵 ) ∈ ℝ → ( 0 < ( 𝐴 · 𝐵 ) ↔ ( 0 −ℝ ( 𝐴 · 𝐵 ) ) < 0 ) )
27 25 26 syl ⊢ ( 𝜑 → ( 0 < ( 𝐴 · 𝐵 ) ↔ ( 0 −ℝ ( 𝐴 · 𝐵 ) ) < 0 ) )
28 0red ⊢ ( 𝜑 → 0 ∈ ℝ )
29 1red ⊢ ( 𝜑 → 1 ∈ ℝ )
30 resubdi ⊢ ( ( ( 𝐴 · 𝐵 ) ∈ ℝ ∧ 0 ∈ ℝ ∧ 1 ∈ ℝ ) → ( ( 𝐴 · 𝐵 ) · ( 0 −ℝ 1 ) ) = ( ( ( 𝐴 · 𝐵 ) · 0 ) −ℝ ( ( 𝐴 · 𝐵 ) · 1 ) ) )
31 25 28 29 30 syl3anc ⊢ ( 𝜑 → ( ( 𝐴 · 𝐵 ) · ( 0 −ℝ 1 ) ) = ( ( ( 𝐴 · 𝐵 ) · 0 ) −ℝ ( ( 𝐴 · 𝐵 ) · 1 ) ) )
32 remul01 ⊢ ( ( 𝐴 · 𝐵 ) ∈ ℝ → ( ( 𝐴 · 𝐵 ) · 0 ) = 0 )
33 ax-1rid ⊢ ( ( 𝐴 · 𝐵 ) ∈ ℝ → ( ( 𝐴 · 𝐵 ) · 1 ) = ( 𝐴 · 𝐵 ) )
34 32 33 oveq12d ⊢ ( ( 𝐴 · 𝐵 ) ∈ ℝ → ( ( ( 𝐴 · 𝐵 ) · 0 ) −ℝ ( ( 𝐴 · 𝐵 ) · 1 ) ) = ( 0 −ℝ ( 𝐴 · 𝐵 ) ) )
35 25 34 syl ⊢ ( 𝜑 → ( ( ( 𝐴 · 𝐵 ) · 0 ) −ℝ ( ( 𝐴 · 𝐵 ) · 1 ) ) = ( 0 −ℝ ( 𝐴 · 𝐵 ) ) )
36 31 35 eqtrd ⊢ ( 𝜑 → ( ( 𝐴 · 𝐵 ) · ( 0 −ℝ 1 ) ) = ( 0 −ℝ ( 𝐴 · 𝐵 ) ) )
37 36 breq1d ⊢ ( 𝜑 → ( ( ( 𝐴 · 𝐵 ) · ( 0 −ℝ 1 ) ) < 0 ↔ ( 0 −ℝ ( 𝐴 · 𝐵 ) ) < 0 ) )
38 27 37 bitr4d ⊢ ( 𝜑 → ( 0 < ( 𝐴 · 𝐵 ) ↔ ( ( 𝐴 · 𝐵 ) · ( 0 −ℝ 1 ) ) < 0 ) )
39 relt0neg2 ⊢ ( 𝐵 ∈ ℝ → ( 0 < 𝐵 ↔ ( 0 −ℝ 𝐵 ) < 0 ) )
40 2 39 syl ⊢ ( 𝜑 → ( 0 < 𝐵 ↔ ( 0 −ℝ 𝐵 ) < 0 ) )
41 resubdi ⊢ ( ( 𝐵 ∈ ℝ ∧ 0 ∈ ℝ ∧ 1 ∈ ℝ ) → ( 𝐵 · ( 0 −ℝ 1 ) ) = ( ( 𝐵 · 0 ) −ℝ ( 𝐵 · 1 ) ) )
42 2 28 29 41 syl3anc ⊢ ( 𝜑 → ( 𝐵 · ( 0 −ℝ 1 ) ) = ( ( 𝐵 · 0 ) −ℝ ( 𝐵 · 1 ) ) )
43 remul01 ⊢ ( 𝐵 ∈ ℝ → ( 𝐵 · 0 ) = 0 )
44 ax-1rid ⊢ ( 𝐵 ∈ ℝ → ( 𝐵 · 1 ) = 𝐵 )
45 43 44 oveq12d ⊢ ( 𝐵 ∈ ℝ → ( ( 𝐵 · 0 ) −ℝ ( 𝐵 · 1 ) ) = ( 0 −ℝ 𝐵 ) )
46 2 45 syl ⊢ ( 𝜑 → ( ( 𝐵 · 0 ) −ℝ ( 𝐵 · 1 ) ) = ( 0 −ℝ 𝐵 ) )
47 42 46 eqtrd ⊢ ( 𝜑 → ( 𝐵 · ( 0 −ℝ 1 ) ) = ( 0 −ℝ 𝐵 ) )
48 47 breq1d ⊢ ( 𝜑 → ( ( 𝐵 · ( 0 −ℝ 1 ) ) < 0 ↔ ( 0 −ℝ 𝐵 ) < 0 ) )
49 40 48 bitr4d ⊢ ( 𝜑 → ( 0 < 𝐵 ↔ ( 𝐵 · ( 0 −ℝ 1 ) ) < 0 ) )
50 24 38 49 3imtr4d ⊢ ( 𝜑 → ( 0 < ( 𝐴 · 𝐵 ) → 0 < 𝐵 ) )
51 9 50 impbid ⊢ ( 𝜑 → ( 0 < 𝐵 ↔ 0 < ( 𝐴 · 𝐵 ) ) )