Metamath Proof Explorer

Theorem prodgt02

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

Ref Expression
Assertion prodgt02 ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ 0 ≤ B ∧ 0 < A ⁢ B → 0 < A

Proof

Step Hyp Ref Expression
1 recn ⊢ A ∈ ℝ → A ∈ ℂ
2 recn ⊢ B ∈ ℝ → B ∈ ℂ
3 mulcom ⊢ A ∈ ℂ ∧ B ∈ ℂ → A ⁢ B = B ⁢ A
4 1 2 3 syl2an ⊢ A ∈ ℝ ∧ B ∈ ℝ → A ⁢ B = B ⁢ A
5 4 breq2d ⊢ A ∈ ℝ ∧ B ∈ ℝ → 0 < A ⁢ B ↔ 0 < B ⁢ A
6 5 biimpd ⊢ A ∈ ℝ ∧ B ∈ ℝ → 0 < A ⁢ B → 0 < B ⁢ A
7 prodgt0 ⊢ B ∈ ℝ ∧ A ∈ ℝ ∧ 0 ≤ B ∧ 0 < B ⁢ A → 0 < A
8 7 ex ⊢ B ∈ ℝ ∧ A ∈ ℝ → 0 ≤ B ∧ 0 < B ⁢ A → 0 < A
9 8 ancoms ⊢ A ∈ ℝ ∧ B ∈ ℝ → 0 ≤ B ∧ 0 < B ⁢ A → 0 < A
10 6 9 sylan2d ⊢ A ∈ ℝ ∧ B ∈ ℝ → 0 ≤ B ∧ 0 < A ⁢ B → 0 < A
11 10 imp ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ 0 ≤ B ∧ 0 < A ⁢ B → 0 < A