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	⊢ ( 𝜑 → 𝐴 ∈ ℝ )
	prodge0ld.2	⊢ ( 𝜑 → 𝐵 ∈ ℝ+ )
	prodge0ld.3	⊢ ( 𝜑 → 0 ≤ ( 𝐴 · 𝐵 ) )
Assertion	prodge0ld	⊢ ( 𝜑 → 0 ≤ 𝐴 )

Proof

Step	Hyp	Ref	Expression
1		prodge0ld.1	⊢ ( 𝜑 → 𝐴 ∈ ℝ )
2		prodge0ld.2	⊢ ( 𝜑 → 𝐵 ∈ ℝ+ )
3		prodge0ld.3	⊢ ( 𝜑 → 0 ≤ ( 𝐴 · 𝐵 ) )
4	2	rpcnd	⊢ ( 𝜑 → 𝐵 ∈ ℂ )
5	1	recnd	⊢ ( 𝜑 → 𝐴 ∈ ℂ )
6	4 5	mulcomd	⊢ ( 𝜑 → ( 𝐵 · 𝐴 ) = ( 𝐴 · 𝐵 ) )
7	3 6	breqtrrd	⊢ ( 𝜑 → 0 ≤ ( 𝐵 · 𝐴 ) )
8	2 1 7	prodge0rd	⊢ ( 𝜑 → 0 ≤ 𝐴 )