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 \in ℝ \land B \in ℝ) \land (0 \leq B \land 0 < A B)) \to 0 < A$

Step	Hyp	Ref	Expression
1		recn	$⊢ A \in ℝ \to A \in ℂ$
2		recn	$⊢ B \in ℝ \to B \in ℂ$
3		mulcom	$⊢ (A \in ℂ \land B \in ℂ) \to A B = B A$
4	1 2 3	syl2an	$⊢ (A \in ℝ \land B \in ℝ) \to A B = B A$
5	4	breq2d	$⊢ (A \in ℝ \land B \in ℝ) \to (0 < A B \leftrightarrow 0 < B A)$
6	5	biimpd	$⊢ (A \in ℝ \land B \in ℝ) \to (0 < A B \to 0 < B A)$
7		prodgt0	$⊢ ((B \in ℝ \land A \in ℝ) \land (0 \leq B \land 0 < B A)) \to 0 < A$
8	7	ex	$⊢ (B \in ℝ \land A \in ℝ) \to ((0 \leq B \land 0 < B A) \to 0 < A)$
9	8	ancoms	$⊢ (A \in ℝ \land B \in ℝ) \to ((0 \leq B \land 0 < B A) \to 0 < A)$
10	6 9	sylan2d	$⊢ (A \in ℝ \land B \in ℝ) \to ((0 \leq B \land 0 < A B) \to 0 < A)$
11	10	imp	$⊢ ((A \in ℝ \land B \in ℝ) \land (0 \leq B \land 0 < A B)) \to 0 < A$

Metamath Proof Explorer