Metamath Proof Explorer

Theorem mulgt0b2d

Description: Biconditional, deductive form of mulgt0 . The first factor is positive iff the product is. (Contributed by SN, 24-Nov-2025)

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 simpr ⊢ ( ( 𝜑 ∧ 0 < 𝐴 ) → 0 < 𝐴 )
7 3 adantr ⊢ ( ( 𝜑 ∧ 0 < 𝐴 ) → 0 < 𝐵 )
8 4 5 6 7 mulgt0d ⊢ ( ( 𝜑 ∧ 0 < 𝐴 ) → 0 < ( 𝐴 · 𝐵 ) )
9 1 2 remulcld ⊢ ( 𝜑 → ( 𝐴 · 𝐵 ) ∈ ℝ )
10 9 adantr ⊢ ( ( 𝜑 ∧ 0 < ( 𝐴 · 𝐵 ) ) → ( 𝐴 · 𝐵 ) ∈ ℝ )
11 2 adantr ⊢ ( ( 𝜑 ∧ 0 < ( 𝐴 · 𝐵 ) ) → 𝐵 ∈ ℝ )
12 simpr ⊢ ( ( 𝜑 ∧ 0 < ( 𝐴 · 𝐵 ) ) → 0 < ( 𝐴 · 𝐵 ) )
13 12 gt0ne0d ⊢ ( ( 𝜑 ∧ 0 < ( 𝐴 · 𝐵 ) ) → ( 𝐴 · 𝐵 ) ≠ 0 )
14 oveq2 ⊢ ( 𝐵 = 0 → ( 𝐴 · 𝐵 ) = ( 𝐴 · 0 ) )
15 1 adantr ⊢ ( ( 𝜑 ∧ 0 < ( 𝐴 · 𝐵 ) ) → 𝐴 ∈ ℝ )
16 remul01 ⊢ ( 𝐴 ∈ ℝ → ( 𝐴 · 0 ) = 0 )
17 15 16 syl ⊢ ( ( 𝜑 ∧ 0 < ( 𝐴 · 𝐵 ) ) → ( 𝐴 · 0 ) = 0 )
18 14 17 sylan9eqr ⊢ ( ( ( 𝜑 ∧ 0 < ( 𝐴 · 𝐵 ) ) ∧ 𝐵 = 0 ) → ( 𝐴 · 𝐵 ) = 0 )
19 13 18 mteqand ⊢ ( ( 𝜑 ∧ 0 < ( 𝐴 · 𝐵 ) ) → 𝐵 ≠ 0 )
20 11 19 sn-rereccld ⊢ ( ( 𝜑 ∧ 0 < ( 𝐴 · 𝐵 ) ) → ( 1 /ℝ 𝐵 ) ∈ ℝ )
21 2 3 sn-recgt0d ⊢ ( 𝜑 → 0 < ( 1 /ℝ 𝐵 ) )
22 21 adantr ⊢ ( ( 𝜑 ∧ 0 < ( 𝐴 · 𝐵 ) ) → 0 < ( 1 /ℝ 𝐵 ) )
23 10 20 12 22 mulgt0d ⊢ ( ( 𝜑 ∧ 0 < ( 𝐴 · 𝐵 ) ) → 0 < ( ( 𝐴 · 𝐵 ) · ( 1 /ℝ 𝐵 ) ) )
24 15 recnd ⊢ ( ( 𝜑 ∧ 0 < ( 𝐴 · 𝐵 ) ) → 𝐴 ∈ ℂ )
25 11 recnd ⊢ ( ( 𝜑 ∧ 0 < ( 𝐴 · 𝐵 ) ) → 𝐵 ∈ ℂ )
26 20 recnd ⊢ ( ( 𝜑 ∧ 0 < ( 𝐴 · 𝐵 ) ) → ( 1 /ℝ 𝐵 ) ∈ ℂ )
27 24 25 26 mulassd ⊢ ( ( 𝜑 ∧ 0 < ( 𝐴 · 𝐵 ) ) → ( ( 𝐴 · 𝐵 ) · ( 1 /ℝ 𝐵 ) ) = ( 𝐴 · ( 𝐵 · ( 1 /ℝ 𝐵 ) ) ) )
28 3 gt0ne0d ⊢ ( 𝜑 → 𝐵 ≠ 0 )
29 2 28 rerecidd ⊢ ( 𝜑 → ( 𝐵 · ( 1 /ℝ 𝐵 ) ) = 1 )
30 29 oveq2d ⊢ ( 𝜑 → ( 𝐴 · ( 𝐵 · ( 1 /ℝ 𝐵 ) ) ) = ( 𝐴 · 1 ) )
31 30 adantr ⊢ ( ( 𝜑 ∧ 0 < ( 𝐴 · 𝐵 ) ) → ( 𝐴 · ( 𝐵 · ( 1 /ℝ 𝐵 ) ) ) = ( 𝐴 · 1 ) )
32 ax-1rid ⊢ ( 𝐴 ∈ ℝ → ( 𝐴 · 1 ) = 𝐴 )
33 15 32 syl ⊢ ( ( 𝜑 ∧ 0 < ( 𝐴 · 𝐵 ) ) → ( 𝐴 · 1 ) = 𝐴 )
34 27 31 33 3eqtrd ⊢ ( ( 𝜑 ∧ 0 < ( 𝐴 · 𝐵 ) ) → ( ( 𝐴 · 𝐵 ) · ( 1 /ℝ 𝐵 ) ) = 𝐴 )
35 23 34 breqtrd ⊢ ( ( 𝜑 ∧ 0 < ( 𝐴 · 𝐵 ) ) → 0 < 𝐴 )
36 8 35 impbida ⊢ ( 𝜑 → ( 0 < 𝐴 ↔ 0 < ( 𝐴 · 𝐵 ) ) )