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 ⊢ φ → A ∈ ℝ +
prodge0rd.2 ⊢ φ → B ∈ ℝ
prodge0rd.3 ⊢ φ → 0 ≤ A ⁢ B
Assertion prodge0rd ⊢ φ → 0 ≤ B

Proof

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