# Metamath Proof Explorer

## Theorem lemul1a

Description: Multiplication of both sides of 'less than or equal to' by a nonnegative number. (Contributed by NM, 21-Feb-2005)

Ref Expression
Assertion lemul1a ${⊢}\left(\left({A}\in ℝ\wedge {B}\in ℝ\wedge \left({C}\in ℝ\wedge 0\le {C}\right)\right)\wedge {A}\le {B}\right)\to {A}{C}\le {B}{C}$

### Proof

Step Hyp Ref Expression
1 0re ${⊢}0\in ℝ$
2 leloe ${⊢}\left(0\in ℝ\wedge {C}\in ℝ\right)\to \left(0\le {C}↔\left(0<{C}\vee 0={C}\right)\right)$
3 1 2 mpan ${⊢}{C}\in ℝ\to \left(0\le {C}↔\left(0<{C}\vee 0={C}\right)\right)$
4 3 pm5.32i ${⊢}\left({C}\in ℝ\wedge 0\le {C}\right)↔\left({C}\in ℝ\wedge \left(0<{C}\vee 0={C}\right)\right)$
5 lemul1 ${⊢}\left({A}\in ℝ\wedge {B}\in ℝ\wedge \left({C}\in ℝ\wedge 0<{C}\right)\right)\to \left({A}\le {B}↔{A}{C}\le {B}{C}\right)$
6 5 biimpd ${⊢}\left({A}\in ℝ\wedge {B}\in ℝ\wedge \left({C}\in ℝ\wedge 0<{C}\right)\right)\to \left({A}\le {B}\to {A}{C}\le {B}{C}\right)$
7 6 3expia ${⊢}\left({A}\in ℝ\wedge {B}\in ℝ\right)\to \left(\left({C}\in ℝ\wedge 0<{C}\right)\to \left({A}\le {B}\to {A}{C}\le {B}{C}\right)\right)$
8 7 com12 ${⊢}\left({C}\in ℝ\wedge 0<{C}\right)\to \left(\left({A}\in ℝ\wedge {B}\in ℝ\right)\to \left({A}\le {B}\to {A}{C}\le {B}{C}\right)\right)$
9 1 leidi ${⊢}0\le 0$
10 recn ${⊢}{A}\in ℝ\to {A}\in ℂ$
11 10 mul01d ${⊢}{A}\in ℝ\to {A}\cdot 0=0$
12 recn ${⊢}{B}\in ℝ\to {B}\in ℂ$
13 12 mul01d ${⊢}{B}\in ℝ\to {B}\cdot 0=0$
14 11 13 breqan12d ${⊢}\left({A}\in ℝ\wedge {B}\in ℝ\right)\to \left({A}\cdot 0\le {B}\cdot 0↔0\le 0\right)$
15 9 14 mpbiri ${⊢}\left({A}\in ℝ\wedge {B}\in ℝ\right)\to {A}\cdot 0\le {B}\cdot 0$
16 oveq2 ${⊢}0={C}\to {A}\cdot 0={A}{C}$
17 oveq2 ${⊢}0={C}\to {B}\cdot 0={B}{C}$
18 16 17 breq12d ${⊢}0={C}\to \left({A}\cdot 0\le {B}\cdot 0↔{A}{C}\le {B}{C}\right)$
19 15 18 syl5ib ${⊢}0={C}\to \left(\left({A}\in ℝ\wedge {B}\in ℝ\right)\to {A}{C}\le {B}{C}\right)$
20 19 a1dd ${⊢}0={C}\to \left(\left({A}\in ℝ\wedge {B}\in ℝ\right)\to \left({A}\le {B}\to {A}{C}\le {B}{C}\right)\right)$
21 20 adantl ${⊢}\left({C}\in ℝ\wedge 0={C}\right)\to \left(\left({A}\in ℝ\wedge {B}\in ℝ\right)\to \left({A}\le {B}\to {A}{C}\le {B}{C}\right)\right)$
22 8 21 jaodan ${⊢}\left({C}\in ℝ\wedge \left(0<{C}\vee 0={C}\right)\right)\to \left(\left({A}\in ℝ\wedge {B}\in ℝ\right)\to \left({A}\le {B}\to {A}{C}\le {B}{C}\right)\right)$
23 4 22 sylbi ${⊢}\left({C}\in ℝ\wedge 0\le {C}\right)\to \left(\left({A}\in ℝ\wedge {B}\in ℝ\right)\to \left({A}\le {B}\to {A}{C}\le {B}{C}\right)\right)$
24 23 com12 ${⊢}\left({A}\in ℝ\wedge {B}\in ℝ\right)\to \left(\left({C}\in ℝ\wedge 0\le {C}\right)\to \left({A}\le {B}\to {A}{C}\le {B}{C}\right)\right)$
25 24 3impia ${⊢}\left({A}\in ℝ\wedge {B}\in ℝ\wedge \left({C}\in ℝ\wedge 0\le {C}\right)\right)\to \left({A}\le {B}\to {A}{C}\le {B}{C}\right)$
26 25 imp ${⊢}\left(\left({A}\in ℝ\wedge {B}\in ℝ\wedge \left({C}\in ℝ\wedge 0\le {C}\right)\right)\wedge {A}\le {B}\right)\to {A}{C}\le {B}{C}$