This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem prodge0rd

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

Ref Expression
Hypotheses prodge0rd.1 ⊢ ( 𝜑 → 𝐴 ∈ ℝ+ )
prodge0rd.2 ⊢ ( 𝜑 → 𝐵 ∈ ℝ )
prodge0rd.3 ⊢ ( 𝜑 → 0 ≤ ( 𝐴 · 𝐵 ) )
Assertion prodge0rd ( 𝜑 → 0 ≤ 𝐵 )

Proof

Step Hyp Ref Expression
1 prodge0rd.1 ⊢ ( 𝜑 → 𝐴 ∈ ℝ+ )
2 prodge0rd.2 ⊢ ( 𝜑 → 𝐵 ∈ ℝ )
3 prodge0rd.3 ⊢ ( 𝜑 → 0 ≤ ( 𝐴 · 𝐵 ) )
4 0red ⊢ ( 𝜑 → 0 ∈ ℝ )
5 1 rpred ⊢ ( 𝜑 → 𝐴 ∈ ℝ )
6 5 2 remulcld ⊢ ( 𝜑 → ( 𝐴 · 𝐵 ) ∈ ℝ )
7 4 6 3 lensymd ⊢ ( 𝜑 → ¬ ( 𝐴 · 𝐵 ) < 0 )
8 5 adantr ⊢ ( ( 𝜑 ∧ 0 < - 𝐵 ) → 𝐴 ∈ ℝ )
9 2 renegcld ⊢ ( 𝜑 → - 𝐵 ∈ ℝ )
10 9 adantr ⊢ ( ( 𝜑 ∧ 0 < - 𝐵 ) → - 𝐵 ∈ ℝ )
11 1 rpgt0d ⊢ ( 𝜑 → 0 < 𝐴 )
12 11 adantr ⊢ ( ( 𝜑 ∧ 0 < - 𝐵 ) → 0 < 𝐴 )
13 simpr ⊢ ( ( 𝜑 ∧ 0 < - 𝐵 ) → 0 < - 𝐵 )
14 8 10 12 13 mulgt0d ⊢ ( ( 𝜑 ∧ 0 < - 𝐵 ) → 0 < ( 𝐴 · - 𝐵 ) )
15 5 recnd ⊢ ( 𝜑 → 𝐴 ∈ ℂ )
16 15 adantr ⊢ ( ( 𝜑 ∧ 0 < - 𝐵 ) → 𝐴 ∈ ℂ )
17 2 recnd ⊢ ( 𝜑 → 𝐵 ∈ ℂ )
18 17 adantr ⊢ ( ( 𝜑 ∧ 0 < - 𝐵 ) → 𝐵 ∈ ℂ )
19 16 18 mulneg2d ⊢ ( ( 𝜑 ∧ 0 < - 𝐵 ) → ( 𝐴 · - 𝐵 ) = - ( 𝐴 · 𝐵 ) )
20 14 19 breqtrd ⊢ ( ( 𝜑 ∧ 0 < - 𝐵 ) → 0 < - ( 𝐴 · 𝐵 ) )
21 20 ex ⊢ ( 𝜑 → ( 0 < - 𝐵 → 0 < - ( 𝐴 · 𝐵 ) ) )
22 2 lt0neg1d ⊢ ( 𝜑 → ( 𝐵 < 0 ↔ 0 < - 𝐵 ) )
23 6 lt0neg1d ⊢ ( 𝜑 → ( ( 𝐴 · 𝐵 ) < 0 ↔ 0 < - ( 𝐴 · 𝐵 ) ) )
24 21 22 23 3imtr4d ⊢ ( 𝜑 → ( 𝐵 < 0 → ( 𝐴 · 𝐵 ) < 0 ) )
25 7 24 mtod ⊢ ( 𝜑 → ¬ 𝐵 < 0 )
26 4 2 25 nltled ⊢ ( 𝜑 → 0 ≤ 𝐵 )