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	|- ( ph -> A e. RR+ )
	prodge0rd.2	|- ( ph -> B e. RR )
	prodge0rd.3	|- ( ph -> 0 <_ ( A x. B ) )
Assertion	prodge0rd	|- ( ph -> 0 <_ B )

Proof

Step	Hyp	Ref	Expression
1		prodge0rd.1	|- ( ph -> A e. RR+ )
2		prodge0rd.2	|- ( ph -> B e. RR )
3		prodge0rd.3	|- ( ph -> 0 <_ ( A x. B ) )
4		0red	|- ( ph -> 0 e. RR )
5	1	rpred	|- ( ph -> A e. RR )
6	5 2	remulcld	|- ( ph -> ( A x. B ) e. RR )
7	4 6 3	lensymd	|- ( ph -> -. ( A x. B ) < 0 )
8	5	adantr	|- ( ( ph /\ 0 < -u B ) -> A e. RR )
9	2	renegcld	|- ( ph -> -u B e. RR )
10	9	adantr	|- ( ( ph /\ 0 < -u B ) -> -u B e. RR )
11	1	rpgt0d	|- ( ph -> 0 < A )
12	11	adantr	|- ( ( ph /\ 0 < -u B ) -> 0 < A )
13		simpr	|- ( ( ph /\ 0 < -u B ) -> 0 < -u B )
14	8 10 12 13	mulgt0d	|- ( ( ph /\ 0 < -u B ) -> 0 < ( A x. -u B ) )
15	5	recnd	|- ( ph -> A e. CC )
16	15	adantr	|- ( ( ph /\ 0 < -u B ) -> A e. CC )
17	2	recnd	|- ( ph -> B e. CC )
18	17	adantr	|- ( ( ph /\ 0 < -u B ) -> B e. CC )
19	16 18	mulneg2d	|- ( ( ph /\ 0 < -u B ) -> ( A x. -u B ) = -u ( A x. B ) )
20	14 19	breqtrd	|- ( ( ph /\ 0 < -u B ) -> 0 < -u ( A x. B ) )
21	20	ex	|- ( ph -> ( 0 < -u B -> 0 < -u ( A x. B ) ) )
22	2	lt0neg1d	|- ( ph -> ( B < 0 <-> 0 < -u B ) )
23	6	lt0neg1d	|- ( ph -> ( ( A x. B ) < 0 <-> 0 < -u ( A x. B ) ) )
24	21 22 23	3imtr4d	|- ( ph -> ( B < 0 -> ( A x. B ) < 0 ) )
25	7 24	mtod	|- ( ph -> -. B < 0 )
26	4 2 25	nltled	|- ( ph -> 0 <_ B )