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 ≤ ( 𝐴 · 𝐵 ) ) |
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 ≤ ( 𝐴 · 𝐵 ) ) |