Metamath Proof Explorer

Theorem lemuldiv2

Description: 'Less than or equal' relationship between division and multiplication. (Contributed by NM, 10-Mar-2006)

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

Proof

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