# Metamath Proof Explorer

## Theorem ltdivmul

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

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

### Proof

Step Hyp Ref Expression
1 remulcl $⊢ C ∈ ℝ ∧ B ∈ ℝ → C ⁢ B ∈ ℝ$
2 1 ancoms $⊢ B ∈ ℝ ∧ C ∈ ℝ → C ⁢ B ∈ ℝ$
3 2 adantrr $⊢ B ∈ ℝ ∧ C ∈ ℝ ∧ 0 < C → C ⁢ B ∈ ℝ$
4 3 3adant1 $⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ C ∈ ℝ ∧ 0 < C → C ⁢ B ∈ ℝ$
5 ltdiv1 $⊢ A ∈ ℝ ∧ C ⁢ B ∈ ℝ ∧ C ∈ ℝ ∧ 0 < C → A < C ⁢ B ↔ A C < C ⁢ B C$
6 4 5 syld3an2 $⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ C ∈ ℝ ∧ 0 < C → A < C ⁢ B ↔ A C < C ⁢ B C$
7 recn $⊢ B ∈ ℝ → B ∈ ℂ$
8 7 adantr $⊢ B ∈ ℝ ∧ C ∈ ℝ ∧ 0 < C → B ∈ ℂ$
9 recn $⊢ C ∈ ℝ → C ∈ ℂ$
10 9 ad2antrl $⊢ B ∈ ℝ ∧ C ∈ ℝ ∧ 0 < C → C ∈ ℂ$
11 gt0ne0 $⊢ C ∈ ℝ ∧ 0 < C → C ≠ 0$
12 11 adantl $⊢ B ∈ ℝ ∧ C ∈ ℝ ∧ 0 < C → C ≠ 0$
13 8 10 12 divcan3d $⊢ B ∈ ℝ ∧ C ∈ ℝ ∧ 0 < C → C ⁢ B C = B$
14 13 3adant1 $⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ C ∈ ℝ ∧ 0 < C → C ⁢ B C = B$
15 14 breq2d $⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ C ∈ ℝ ∧ 0 < C → A C < C ⁢ B C ↔ A C < B$
16 6 15 bitr2d $⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ C ∈ ℝ ∧ 0 < C → A C < B ↔ A < C ⁢ B$