Metamath Proof Explorer


Theorem lemul1i

Description: Multiplication of both sides of 'less than or equal to' by a positive number. (Contributed by NM, 2-Aug-1999)

Ref Expression
Hypotheses ltplus1.1 𝐴 ∈ ℝ
prodgt0.2 𝐵 ∈ ℝ
ltmul1.3 𝐶 ∈ ℝ
Assertion lemul1i ( 0 < 𝐶 → ( 𝐴𝐵 ↔ ( 𝐴 · 𝐶 ) ≤ ( 𝐵 · 𝐶 ) ) )

Proof

Step Hyp Ref Expression
1 ltplus1.1 𝐴 ∈ ℝ
2 prodgt0.2 𝐵 ∈ ℝ
3 ltmul1.3 𝐶 ∈ ℝ
4 lemul1 ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ ( 𝐶 ∈ ℝ ∧ 0 < 𝐶 ) ) → ( 𝐴𝐵 ↔ ( 𝐴 · 𝐶 ) ≤ ( 𝐵 · 𝐶 ) ) )
5 1 2 4 mp3an12 ( ( 𝐶 ∈ ℝ ∧ 0 < 𝐶 ) → ( 𝐴𝐵 ↔ ( 𝐴 · 𝐶 ) ≤ ( 𝐵 · 𝐶 ) ) )
6 3 5 mpan ( 0 < 𝐶 → ( 𝐴𝐵 ↔ ( 𝐴 · 𝐶 ) ≤ ( 𝐵 · 𝐶 ) ) )