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

Proof

Step	Hyp	Ref	Expression
1		prodge0rd.1	⊢ ( 𝜑 → 𝐴 ∈ ℝ+ )
2		prodge0rd.2	⊢ ( 𝜑 → 𝐵 ∈ ℝ )
3		prodge0rd.3	⊢ ( 𝜑 → 0 ≤ ( 𝐴 · 𝐵 ) )
4		0red	⊢ ( 𝜑 → 0 ∈ ℝ )
5	1	rpred	⊢ ( 𝜑 → 𝐴 ∈ ℝ )
6	5 2	remulcld	⊢ ( 𝜑 → ( 𝐴 · 𝐵 ) ∈ ℝ )
7	4 6 3	lensymd	⊢ ( 𝜑 → ¬ ( 𝐴 · 𝐵 ) < 0 )
8	5	adantr	⊢ ( ( 𝜑 ∧ 0 < - 𝐵 ) → 𝐴 ∈ ℝ )
9	2	renegcld	⊢ ( 𝜑 → - 𝐵 ∈ ℝ )
10	9	adantr	⊢ ( ( 𝜑 ∧ 0 < - 𝐵 ) → - 𝐵 ∈ ℝ )
11	1	rpgt0d	⊢ ( 𝜑 → 0 < 𝐴 )
12	11	adantr	⊢ ( ( 𝜑 ∧ 0 < - 𝐵 ) → 0 < 𝐴 )
13		simpr	⊢ ( ( 𝜑 ∧ 0 < - 𝐵 ) → 0 < - 𝐵 )
14	8 10 12 13	mulgt0d	⊢ ( ( 𝜑 ∧ 0 < - 𝐵 ) → 0 < ( 𝐴 · - 𝐵 ) )
15	5	recnd	⊢ ( 𝜑 → 𝐴 ∈ ℂ )
16	15	adantr	⊢ ( ( 𝜑 ∧ 0 < - 𝐵 ) → 𝐴 ∈ ℂ )
17	2	recnd	⊢ ( 𝜑 → 𝐵 ∈ ℂ )
18	17	adantr	⊢ ( ( 𝜑 ∧ 0 < - 𝐵 ) → 𝐵 ∈ ℂ )
19	16 18	mulneg2d	⊢ ( ( 𝜑 ∧ 0 < - 𝐵 ) → ( 𝐴 · - 𝐵 ) = - ( 𝐴 · 𝐵 ) )
20	14 19	breqtrd	⊢ ( ( 𝜑 ∧ 0 < - 𝐵 ) → 0 < - ( 𝐴 · 𝐵 ) )
21	20	ex	⊢ ( 𝜑 → ( 0 < - 𝐵 → 0 < - ( 𝐴 · 𝐵 ) ) )
22	2	lt0neg1d	⊢ ( 𝜑 → ( 𝐵 < 0 ↔ 0 < - 𝐵 ) )
23	6	lt0neg1d	⊢ ( 𝜑 → ( ( 𝐴 · 𝐵 ) < 0 ↔ 0 < - ( 𝐴 · 𝐵 ) ) )
24	21 22 23	3imtr4d	⊢ ( 𝜑 → ( 𝐵 < 0 → ( 𝐴 · 𝐵 ) < 0 ) )
25	7 24	mtod	⊢ ( 𝜑 → ¬ 𝐵 < 0 )
26	4 2 25	nltled	⊢ ( 𝜑 → 0 ≤ 𝐵 )