Metamath Proof Explorer

Theorem lemulge11

Description: Multiplication by a number greater than or equal to 1. (Contributed by NM, 17-Dec-2005)

Ref Expression
Assertion lemulge11 ⊢A∈ℝ∧B∈ℝ∧0≤A∧1≤B→A≤A⁢B

Proof

Step Hyp Ref Expression
1 ax-1rid ⊢A∈ℝ→A⋅1=A
2 1 ad2antrr ⊢A∈ℝ∧B∈ℝ∧0≤A∧1≤B→A⋅1=A
3 simpll ⊢A∈ℝ∧B∈ℝ∧0≤A∧1≤B→A∈ℝ
4 simprl ⊢A∈ℝ∧B∈ℝ∧0≤A∧1≤B→0≤A
5 3 4 jca ⊢A∈ℝ∧B∈ℝ∧0≤A∧1≤B→A∈ℝ∧0≤A
6 simplr ⊢A∈ℝ∧B∈ℝ∧0≤A∧1≤B→B∈ℝ
7 1re ⊢1∈ℝ
8 0le1 ⊢0≤1
9 7 8 pm3.2i ⊢1∈ℝ∧0≤1
10 6 9 jctil ⊢A∈ℝ∧B∈ℝ∧0≤A∧1≤B→1∈ℝ∧0≤1∧B∈ℝ
11 5 3 10 jca31 ⊢A∈ℝ∧B∈ℝ∧0≤A∧1≤B→A∈ℝ∧0≤A∧A∈ℝ∧1∈ℝ∧0≤1∧B∈ℝ
12 leid ⊢A∈ℝ→A≤A
13 12 ad2antrr ⊢A∈ℝ∧B∈ℝ∧0≤A∧1≤B→A≤A
14 simprr ⊢A∈ℝ∧B∈ℝ∧0≤A∧1≤B→1≤B
15 13 14 jca ⊢A∈ℝ∧B∈ℝ∧0≤A∧1≤B→A≤A∧1≤B
16 lemul12a ⊢A∈ℝ∧0≤A∧A∈ℝ∧1∈ℝ∧0≤1∧B∈ℝ→A≤A∧1≤B→A⋅1≤A⁢B
17 11 15 16 sylc ⊢A∈ℝ∧B∈ℝ∧0≤A∧1≤B→A⋅1≤A⁢B
18 2 17 eqbrtrrd ⊢A∈ℝ∧B∈ℝ∧0≤A∧1≤B→A≤A⁢B