Metamath Proof Explorer

Theorem prodgt0

Description: Infer that a multiplicand is positive from a nonnegative multiplier and positive product. (Contributed by NM, 24-Apr-2005) (Revised by Mario Carneiro, 27-May-2016)

Ref Expression
Assertion prodgt0 ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( 0 ≤ 𝐴 ∧ 0 < ( 𝐴 · 𝐵 ) ) ) → 0 < 𝐵 )

Proof

Step Hyp Ref Expression
1 0red ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → 0 ∈ ℝ )
2 simpl ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → 𝐴 ∈ ℝ )
3 1 2 leloed ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( 0 ≤ 𝐴 ↔ ( 0 < 𝐴 ∨ 0 = 𝐴 ) ) )
4 simpll ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( 0 < 𝐴 ∧ 0 < ( 𝐴 · 𝐵 ) ) ) → 𝐴 ∈ ℝ )
5 simplr ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( 0 < 𝐴 ∧ 0 < ( 𝐴 · 𝐵 ) ) ) → 𝐵 ∈ ℝ )
6 4 5 remulcld ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( 0 < 𝐴 ∧ 0 < ( 𝐴 · 𝐵 ) ) ) → ( 𝐴 · 𝐵 ) ∈ ℝ )
7 simprl ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( 0 < 𝐴 ∧ 0 < ( 𝐴 · 𝐵 ) ) ) → 0 < 𝐴 )
8 7 gt0ne0d ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( 0 < 𝐴 ∧ 0 < ( 𝐴 · 𝐵 ) ) ) → 𝐴 ≠ 0 )
9 4 8 rereccld ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( 0 < 𝐴 ∧ 0 < ( 𝐴 · 𝐵 ) ) ) → ( 1 / 𝐴 ) ∈ ℝ )
10 simprr ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( 0 < 𝐴 ∧ 0 < ( 𝐴 · 𝐵 ) ) ) → 0 < ( 𝐴 · 𝐵 ) )
11 recgt0 ⊢ ( ( 𝐴 ∈ ℝ ∧ 0 < 𝐴 ) → 0 < ( 1 / 𝐴 ) )
12 11 ad2ant2r ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( 0 < 𝐴 ∧ 0 < ( 𝐴 · 𝐵 ) ) ) → 0 < ( 1 / 𝐴 ) )
13 6 9 10 12 mulgt0d ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( 0 < 𝐴 ∧ 0 < ( 𝐴 · 𝐵 ) ) ) → 0 < ( ( 𝐴 · 𝐵 ) · ( 1 / 𝐴 ) ) )
14 6 recnd ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( 0 < 𝐴 ∧ 0 < ( 𝐴 · 𝐵 ) ) ) → ( 𝐴 · 𝐵 ) ∈ ℂ )
15 4 recnd ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( 0 < 𝐴 ∧ 0 < ( 𝐴 · 𝐵 ) ) ) → 𝐴 ∈ ℂ )
16 14 15 8 divrecd ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( 0 < 𝐴 ∧ 0 < ( 𝐴 · 𝐵 ) ) ) → ( ( 𝐴 · 𝐵 ) / 𝐴 ) = ( ( 𝐴 · 𝐵 ) · ( 1 / 𝐴 ) ) )
17 simpr ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → 𝐵 ∈ ℝ )
18 17 recnd ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → 𝐵 ∈ ℂ )
19 18 adantr ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( 0 < 𝐴 ∧ 0 < ( 𝐴 · 𝐵 ) ) ) → 𝐵 ∈ ℂ )
20 19 15 8 divcan3d ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( 0 < 𝐴 ∧ 0 < ( 𝐴 · 𝐵 ) ) ) → ( ( 𝐴 · 𝐵 ) / 𝐴 ) = 𝐵 )
21 16 20 eqtr3d ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( 0 < 𝐴 ∧ 0 < ( 𝐴 · 𝐵 ) ) ) → ( ( 𝐴 · 𝐵 ) · ( 1 / 𝐴 ) ) = 𝐵 )
22 13 21 breqtrd ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( 0 < 𝐴 ∧ 0 < ( 𝐴 · 𝐵 ) ) ) → 0 < 𝐵 )
23 22 exp32 ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( 0 < 𝐴 → ( 0 < ( 𝐴 · 𝐵 ) → 0 < 𝐵 ) ) )
24 0re ⊢ 0 ∈ ℝ
25 24 ltnri ⊢ ¬ 0 < 0
26 18 mul02d ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( 0 · 𝐵 ) = 0 )
27 26 breq2d ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( 0 < ( 0 · 𝐵 ) ↔ 0 < 0 ) )
28 25 27 mtbiri ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ¬ 0 < ( 0 · 𝐵 ) )
29 28 pm2.21d ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( 0 < ( 0 · 𝐵 ) → 0 < 𝐵 ) )
30 oveq1 ⊢ ( 0 = 𝐴 → ( 0 · 𝐵 ) = ( 𝐴 · 𝐵 ) )
31 30 breq2d ⊢ ( 0 = 𝐴 → ( 0 < ( 0 · 𝐵 ) ↔ 0 < ( 𝐴 · 𝐵 ) ) )
32 31 imbi1d ⊢ ( 0 = 𝐴 → ( ( 0 < ( 0 · 𝐵 ) → 0 < 𝐵 ) ↔ ( 0 < ( 𝐴 · 𝐵 ) → 0 < 𝐵 ) ) )
33 29 32 syl5ibcom ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( 0 = 𝐴 → ( 0 < ( 𝐴 · 𝐵 ) → 0 < 𝐵 ) ) )
34 23 33 jaod ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( ( 0 < 𝐴 ∨ 0 = 𝐴 ) → ( 0 < ( 𝐴 · 𝐵 ) → 0 < 𝐵 ) ) )
35 3 34 sylbid ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( 0 ≤ 𝐴 → ( 0 < ( 𝐴 · 𝐵 ) → 0 < 𝐵 ) ) )
36 35 imp32 ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( 0 ≤ 𝐴 ∧ 0 < ( 𝐴 · 𝐵 ) ) ) → 0 < 𝐵 )