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

Metamath Proof Explorer

Theorem prodge0ld

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

	Ref	Expression
Hypotheses	prodge0ld.1	$⊢ φ \to A \in ℝ$
	prodge0ld.2	$⊢ φ \to B \in ℝ^{+}$
	prodge0ld.3	$⊢ φ \to 0 \leq A B$
Assertion	prodge0ld	$⊢ φ \to 0 \leq A$

Proof

Step	Hyp	Ref	Expression
1		prodge0ld.1	$⊢ φ \to A \in ℝ$
2		prodge0ld.2	$⊢ φ \to B \in ℝ^{+}$
3		prodge0ld.3	$⊢ φ \to 0 \leq A B$
4	2	rpcnd	$⊢ φ \to B \in ℂ$
5	1	recnd	$⊢ φ \to A \in ℂ$
6	4 5	mulcomd	$⊢ φ \to B A = A B$
7	3 6	breqtrrd	$⊢ φ \to 0 \leq B A$
8	2 1 7	prodge0rd	$⊢ φ \to 0 \leq A$