Metamath Proof Explorer

Theorem ltmuldiv2

Description: 'Less than' relationship between division and multiplication. (Contributed by NM, 18-Nov-2004)

Ref Expression
Assertion ltmuldiv2 ⊢ 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 ltmuldiv ⊢ 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