This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ ( 𝐶 ∈ ℝ ∧ 0 < 𝐶 ) ) → ( 𝐴 ≤ 𝐵 ↔ ( 𝐴 / 𝐶 ) ≤ ( 𝐵 / 𝐶 ) ) )

Proof

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