Metamath Proof Explorer

Theorem ledivmul

Description: 'Less than or equal to' relationship between division and multiplication. (Contributed by NM, 9-Dec-2005)

Ref Expression
Assertion ledivmul ⊢ 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 lediv1 ⊢ 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