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	$$⊢\phi \to A\in ℝ$$
	prodge0ld.2	$$⊢\phi \to B\in {ℝ}^{+}$$
	prodge0ld.3	$$⊢\phi \to 0\le AB$$
Assertion	prodge0ld	$$⊢\phi \to 0\le A$$

Proof

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