Metamath Proof Explorer

Theorem ltdivmul2

Description: 'Less than' relationship between division and multiplication. (Contributed by NM, 24-Feb-2005)

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

Proof

Step Hyp Ref Expression
1 ltdivmul ⊢ 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