Metamath Proof Explorer

Theorem lemul2a

Description: Multiplication of both sides of 'less than or equal to' by a nonnegative number. (Contributed by Paul Chapman, 7-Sep-2007)

Ref Expression
Assertion lemul2a ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ C ∈ ℝ ∧ 0 ≤ C ∧ A ≤ B → C ⁢ A ≤ C ⁢ B

Proof

Step Hyp Ref Expression
1 lemul1a ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ C ∈ ℝ ∧ 0 ≤ C ∧ A ≤ B → A ⁢ C ≤ B ⁢ C
2 recn ⊢ A ∈ ℝ → A ∈ ℂ
3 recn ⊢ C ∈ ℝ → C ∈ ℂ
4 mulcom ⊢ A ∈ ℂ ∧ C ∈ ℂ → A ⁢ C = C ⁢ A
5 2 3 4 syl2an ⊢ A ∈ ℝ ∧ C ∈ ℝ → A ⁢ C = C ⁢ A
6 5 adantrr ⊢ A ∈ ℝ ∧ C ∈ ℝ ∧ 0 ≤ C → A ⁢ C = C ⁢ A
7 6 3adant2 ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ C ∈ ℝ ∧ 0 ≤ C → A ⁢ C = C ⁢ A
8 7 adantr ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ C ∈ ℝ ∧ 0 ≤ C ∧ A ≤ B → A ⁢ C = C ⁢ A
9 recn ⊢ B ∈ ℝ → B ∈ ℂ
10 mulcom ⊢ B ∈ ℂ ∧ C ∈ ℂ → B ⁢ C = C ⁢ B
11 9 3 10 syl2an ⊢ B ∈ ℝ ∧ C ∈ ℝ → B ⁢ C = C ⁢ B
12 11 adantrr ⊢ B ∈ ℝ ∧ C ∈ ℝ ∧ 0 ≤ C → B ⁢ C = C ⁢ B
13 12 3adant1 ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ C ∈ ℝ ∧ 0 ≤ C → B ⁢ C = C ⁢ B
14 13 adantr ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ C ∈ ℝ ∧ 0 ≤ C ∧ A ≤ B → B ⁢ C = C ⁢ B
15 1 8 14 3brtr3d ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ C ∈ ℝ ∧ 0 ≤ C ∧ A ≤ B → C ⁢ A ≤ C ⁢ B