Metamath Proof Explorer

Theorem ledivmul2

Description: 'Less than or equal to' relationship between division and multiplication. (Contributed by NM, 9-Dec-2005)

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

Proof

Step Hyp Ref Expression
1 ledivmul ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ C ∈ ℝ ∧ 0 < C → A C ≤ B ↔ A ≤ C ⁢ B
2 recn ⊢ B ∈ ℝ → B ∈ ℂ
3 recn ⊢ C ∈ ℝ → C ∈ ℂ
4 mulcom ⊢ B ∈ ℂ ∧ C ∈ ℂ → B ⁢ C = C ⁢ B
5 2 3 4 syl2an ⊢ B ∈ ℝ ∧ C ∈ ℝ → B ⁢ C = C ⁢ B
6 5 adantrr ⊢ B ∈ ℝ ∧ C ∈ ℝ ∧ 0 < C → B ⁢ C = C ⁢ B
7 6 3adant1 ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ C ∈ ℝ ∧ 0 < C → B ⁢ C = C ⁢ B
8 7 breq2d ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ C ∈ ℝ ∧ 0 < C → A ≤ B ⁢ C ↔ A ≤ C ⁢ B
9 1 8 bitr4d ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ C ∈ ℝ ∧ 0 < C → A C ≤ B ↔ A ≤ B ⁢ C