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

Proof

Step Hyp Ref Expression
1 lemulge11 ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ 0 ≤ A ∧ 1 ≤ B → A ≤ A ⁢ B
2 recn ⊢ A ∈ ℝ → A ∈ ℂ
3 recn ⊢ B ∈ ℝ → B ∈ ℂ
4 mulcom ⊢ A ∈ ℂ ∧ B ∈ ℂ → A ⁢ B = B ⁢ A
5 2 3 4 syl2an ⊢ A ∈ ℝ ∧ B ∈ ℝ → A ⁢ B = B ⁢ A
6 5 breq2d ⊢ A ∈ ℝ ∧ B ∈ ℝ → A ≤ A ⁢ B ↔ A ≤ B ⁢ A
7 6 adantr ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ 0 ≤ A ∧ 1 ≤ B → A ≤ A ⁢ B ↔ A ≤ B ⁢ A
8 1 7 mpbid ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ 0 ≤ A ∧ 1 ≤ B → A ≤ B ⁢ A