# Metamath Proof Explorer

## Theorem lemulge12

Description: Multiplication by a number greater than or equal to 1. (Contributed by Paul Chapman, 21-Mar-2011)

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

### Proof

Step Hyp Ref Expression
1 lemulge11 ${⊢}\left(\left({A}\in ℝ\wedge {B}\in ℝ\right)\wedge \left(0\le {A}\wedge 1\le {B}\right)\right)\to {A}\le {A}{B}$
2 recn ${⊢}{A}\in ℝ\to {A}\in ℂ$
3 recn ${⊢}{B}\in ℝ\to {B}\in ℂ$
4 mulcom ${⊢}\left({A}\in ℂ\wedge {B}\in ℂ\right)\to {A}{B}={B}{A}$
5 2 3 4 syl2an ${⊢}\left({A}\in ℝ\wedge {B}\in ℝ\right)\to {A}{B}={B}{A}$
6 5 breq2d ${⊢}\left({A}\in ℝ\wedge {B}\in ℝ\right)\to \left({A}\le {A}{B}↔{A}\le {B}{A}\right)$
7 6 adantr ${⊢}\left(\left({A}\in ℝ\wedge {B}\in ℝ\right)\wedge \left(0\le {A}\wedge 1\le {B}\right)\right)\to \left({A}\le {A}{B}↔{A}\le {B}{A}\right)$
8 1 7 mpbid ${⊢}\left(\left({A}\in ℝ\wedge {B}\in ℝ\right)\wedge \left(0\le {A}\wedge 1\le {B}\right)\right)\to {A}\le {B}{A}$