Metamath Proof Explorer

Theorem lediv1

Description: Division of both sides of a less than or equal to relation by a positive number. (Contributed by NM, 18-Nov-2004)

Ref Expression
Assertion lediv1 ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ C ∈ ℝ ∧ 0 < C → A ≤ B ↔ A C ≤ B C

Proof

Step Hyp Ref Expression
1 ltdiv1 ⊢ B ∈ ℝ ∧ A ∈ ℝ ∧ C ∈ ℝ ∧ 0 < C → B < A ↔ B C < A C
2 1 3com12 ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ C ∈ ℝ ∧ 0 < C → B < A ↔ B C < A C
3 2 notbid ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ C ∈ ℝ ∧ 0 < C → ¬ B < A ↔ ¬ B C < A C
4 lenlt ⊢ A ∈ ℝ ∧ B ∈ ℝ → A ≤ B ↔ ¬ B < A
5 4 3adant3 ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ C ∈ ℝ ∧ 0 < C → A ≤ B ↔ ¬ B < A
6 gt0ne0 ⊢ C ∈ ℝ ∧ 0 < C → C ≠ 0
7 6 3adant1 ⊢ A ∈ ℝ ∧ C ∈ ℝ ∧ 0 < C → C ≠ 0
8 redivcl ⊢ A ∈ ℝ ∧ C ∈ ℝ ∧ C ≠ 0 → A C ∈ ℝ
9 7 8 syld3an3 ⊢ A ∈ ℝ ∧ C ∈ ℝ ∧ 0 < C → A C ∈ ℝ
10 9 3expb ⊢ A ∈ ℝ ∧ C ∈ ℝ ∧ 0 < C → A C ∈ ℝ
11 10 3adant2 ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ C ∈ ℝ ∧ 0 < C → A C ∈ ℝ
12 6 3adant1 ⊢ B ∈ ℝ ∧ C ∈ ℝ ∧ 0 < C → C ≠ 0
13 redivcl ⊢ B ∈ ℝ ∧ C ∈ ℝ ∧ C ≠ 0 → B C ∈ ℝ
14 12 13 syld3an3 ⊢ B ∈ ℝ ∧ C ∈ ℝ ∧ 0 < C → B C ∈ ℝ
15 14 3expb ⊢ B ∈ ℝ ∧ C ∈ ℝ ∧ 0 < C → B C ∈ ℝ
16 15 3adant1 ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ C ∈ ℝ ∧ 0 < C → B C ∈ ℝ
17 11 16 lenltd ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ C ∈ ℝ ∧ 0 < C → A C ≤ B C ↔ ¬ B C < A C
18 3 5 17 3bitr4d ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ C ∈ ℝ ∧ 0 < C → A ≤ B ↔ A C ≤ B C