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