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 ⊢A∈ℝ∧B∈ℝ∧C∈ℝ∧0≤C∧A≤B→A⁢C≤B⁢C

Proof

Step Hyp Ref Expression
1 0re ⊢0∈ℝ
2 leloe ⊢0∈ℝ∧C∈ℝ→0≤C↔0<C∨0=C
3 1 2 mpan ⊢C∈ℝ→0≤C↔0<C∨0=C
4 3 pm5.32i ⊢C∈ℝ∧0≤C↔C∈ℝ∧0<C∨0=C
5 lemul1 ⊢A∈ℝ∧B∈ℝ∧C∈ℝ∧0<C→A≤B↔A⁢C≤B⁢C
6 5 biimpd ⊢A∈ℝ∧B∈ℝ∧C∈ℝ∧0<C→A≤B→A⁢C≤B⁢C
7 6 3expia ⊢A∈ℝ∧B∈ℝ→C∈ℝ∧0<C→A≤B→A⁢C≤B⁢C
8 7 com12 ⊢C∈ℝ∧0<C→A∈ℝ∧B∈ℝ→A≤B→A⁢C≤B⁢C
9 1 leidi ⊢0≤0
10 recn ⊢A∈ℝ→A∈ℂ
11 10 mul01d ⊢A∈ℝ→A⋅0=0
12 recn ⊢B∈ℝ→B∈ℂ
13 12 mul01d ⊢B∈ℝ→B⋅0=0
14 11 13 breqan12d ⊢A∈ℝ∧B∈ℝ→A⋅0≤B⋅0↔0≤0
15 9 14 mpbiri ⊢A∈ℝ∧B∈ℝ→A⋅0≤B⋅0
16 oveq2 ⊢0=C→A⋅0=A⁢C
17 oveq2 ⊢0=C→B⋅0=B⁢C
18 16 17 breq12d ⊢0=C→A⋅0≤B⋅0↔A⁢C≤B⁢C
19 15 18 imbitrid ⊢0=C→A∈ℝ∧B∈ℝ→A⁢C≤B⁢C
20 19 a1dd ⊢0=C→A∈ℝ∧B∈ℝ→A≤B→A⁢C≤B⁢C
21 20 adantl ⊢C∈ℝ∧0=C→A∈ℝ∧B∈ℝ→A≤B→A⁢C≤B⁢C
22 8 21 jaodan ⊢C∈ℝ∧0<C∨0=C→A∈ℝ∧B∈ℝ→A≤B→A⁢C≤B⁢C
23 4 22 sylbi ⊢C∈ℝ∧0≤C→A∈ℝ∧B∈ℝ→A≤B→A⁢C≤B⁢C
24 23 com12 ⊢A∈ℝ∧B∈ℝ→C∈ℝ∧0≤C→A≤B→A⁢C≤B⁢C
25 24 3impia ⊢A∈ℝ∧B∈ℝ∧C∈ℝ∧0≤C→A≤B→A⁢C≤B⁢C
26 25 imp ⊢A∈ℝ∧B∈ℝ∧C∈ℝ∧0≤C∧A≤B→A⁢C≤B⁢C