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