Metamath Proof Explorer


Theorem mulge0i

Description: The product of two nonnegative numbers is nonnegative. (Contributed by NM, 30-Jul-1999)

Ref Expression
Hypotheses lt2.1 𝐴 ∈ ℝ
lt2.2 𝐵 ∈ ℝ
Assertion mulge0i ( ( 0 ≤ 𝐴 ∧ 0 ≤ 𝐵 ) → 0 ≤ ( 𝐴 · 𝐵 ) )

Proof

Step Hyp Ref Expression
1 lt2.1 𝐴 ∈ ℝ
2 lt2.2 𝐵 ∈ ℝ
3 mulge0 ( ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) ∧ ( 𝐵 ∈ ℝ ∧ 0 ≤ 𝐵 ) ) → 0 ≤ ( 𝐴 · 𝐵 ) )
4 3 an4s ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( 0 ≤ 𝐴 ∧ 0 ≤ 𝐵 ) ) → 0 ≤ ( 𝐴 · 𝐵 ) )
5 1 2 4 mpanl12 ( ( 0 ≤ 𝐴 ∧ 0 ≤ 𝐵 ) → 0 ≤ ( 𝐴 · 𝐵 ) )