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

Proof

Step	Hyp	Ref	Expression
1		prodge0rd.1	$$⊢\phi \to A\in {ℝ}^{+}$$
2		prodge0rd.2	$$⊢\phi \to B\in ℝ$$
3		prodge0rd.3	$$⊢\phi \to 0\le AB$$
4		0red	$$⊢\phi \to 0\in ℝ$$
5	1	rpred	$$⊢\phi \to A\in ℝ$$
6	5 2	remulcld	$$⊢\phi \to AB\in ℝ$$
7	4 6 3	lensymd	$$⊢\phi \to \neg AB<0$$
8	5	adantr	$$⊢\left(\phi \wedge 0<-B\right)\to A\in ℝ$$
9	2	renegcld	$$⊢\phi \to -B\in ℝ$$
10	9	adantr	$$⊢\left(\phi \wedge 0<-B\right)\to -B\in ℝ$$
11	1	rpgt0d	$$⊢\phi \to 0<A$$
12	11	adantr	$$⊢\left(\phi \wedge 0<-B\right)\to 0<A$$
13		simpr	$$⊢\left(\phi \wedge 0<-B\right)\to 0<-B$$
14	8 10 12 13	mulgt0d	$$⊢\left(\phi \wedge 0<-B\right)\to 0<A\left(-B\right)$$
15	5	recnd	$$⊢\phi \to A\in ℂ$$
16	15	adantr	$$⊢\left(\phi \wedge 0<-B\right)\to A\in ℂ$$
17	2	recnd	$$⊢\phi \to B\in ℂ$$
18	17	adantr	$$⊢\left(\phi \wedge 0<-B\right)\to B\in ℂ$$
19	16 18	mulneg2d	$$⊢\left(\phi \wedge 0<-B\right)\to A\left(-B\right)=-AB$$
20	14 19	breqtrd	$$⊢\left(\phi \wedge 0<-B\right)\to 0<-AB$$
21	20	ex	$$⊢\phi \to \left(0<-B\to 0<-AB\right)$$
22	2	lt0neg1d	$$⊢\phi \to \left(B<0\leftrightarrow 0<-B\right)$$
23	6	lt0neg1d	$$⊢\phi \to \left(AB<0\leftrightarrow 0<-AB\right)$$
24	21 22 23	3imtr4d	$$⊢\phi \to \left(B<0\to AB<0\right)$$
25	7 24	mtod	$$⊢\phi \to \neg B<0$$
26	4 2 25	nltled	$$⊢\phi \to 0\le B$$