This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem lemul2

Description: Multiplication of both sides of 'less than or equal to' by a positive number. (Contributed by NM, 16-Mar-2005)

Ref Expression
Assertion lemul2 ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ C ∈ ℝ ∧ 0 < C → A ≤ B ↔ C ⁢ A ≤ C ⁢ B

Proof

Step Hyp Ref Expression
1 lemul1 ⊢ 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 3adant2 ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ C ∈ ℝ → A ⁢ C = C ⁢ A
7 recn ⊢ B ∈ ℝ → B ∈ ℂ
8 mulcom ⊢ B ∈ ℂ ∧ C ∈ ℂ → B ⁢ C = C ⁢ B
9 7 3 8 syl2an ⊢ B ∈ ℝ ∧ C ∈ ℝ → B ⁢ C = C ⁢ B
10 9 3adant1 ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ C ∈ ℝ → B ⁢ C = C ⁢ B
11 6 10 breq12d ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ C ∈ ℝ → A ⁢ C ≤ B ⁢ C ↔ C ⁢ A ≤ C ⁢ B
12 11 3adant3r ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ C ∈ ℝ ∧ 0 < C → A ⁢ C ≤ B ⁢ C ↔ C ⁢ A ≤ C ⁢ B
13 1 12 bitrd ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ C ∈ ℝ ∧ 0 < C → A ≤ B ↔ C ⁢ A ≤ C ⁢ B