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

Proof

Step	Hyp	Ref	Expression
1		prodge0ld.1	|- ( ph -> A e. RR )
2		prodge0ld.2	|- ( ph -> B e. RR+ )
3		prodge0ld.3	|- ( ph -> 0 <_ ( A x. B ) )
4	2	rpcnd	|- ( ph -> B e. CC )
5	1	recnd	|- ( ph -> A e. CC )
6	4 5	mulcomd	|- ( ph -> ( B x. A ) = ( A x. B ) )
7	3 6	breqtrrd	|- ( ph -> 0 <_ ( B x. A ) )
8	2 1 7	prodge0rd	|- ( ph -> 0 <_ A )