Metamath Proof Explorer


Theorem lediv2ad

Description: Division of both sides of 'less than or equal to' into a nonnegative number. (Contributed by Mario Carneiro, 28-May-2016)

Ref Expression
Hypotheses rpred.1 ( 𝜑𝐴 ∈ ℝ+ )
rpaddcld.1 ( 𝜑𝐵 ∈ ℝ+ )
lediv2ad.3 ( 𝜑𝐶 ∈ ℝ )
lediv2ad.4 ( 𝜑 → 0 ≤ 𝐶 )
lediv2ad.5 ( 𝜑𝐴𝐵 )
Assertion lediv2ad ( 𝜑 → ( 𝐶 / 𝐵 ) ≤ ( 𝐶 / 𝐴 ) )

Proof

Step Hyp Ref Expression
1 rpred.1 ( 𝜑𝐴 ∈ ℝ+ )
2 rpaddcld.1 ( 𝜑𝐵 ∈ ℝ+ )
3 lediv2ad.3 ( 𝜑𝐶 ∈ ℝ )
4 lediv2ad.4 ( 𝜑 → 0 ≤ 𝐶 )
5 lediv2ad.5 ( 𝜑𝐴𝐵 )
6 1 rpregt0d ( 𝜑 → ( 𝐴 ∈ ℝ ∧ 0 < 𝐴 ) )
7 2 rpregt0d ( 𝜑 → ( 𝐵 ∈ ℝ ∧ 0 < 𝐵 ) )
8 3 4 jca ( 𝜑 → ( 𝐶 ∈ ℝ ∧ 0 ≤ 𝐶 ) )
9 lediv2a ( ( ( ( 𝐴 ∈ ℝ ∧ 0 < 𝐴 ) ∧ ( 𝐵 ∈ ℝ ∧ 0 < 𝐵 ) ∧ ( 𝐶 ∈ ℝ ∧ 0 ≤ 𝐶 ) ) ∧ 𝐴𝐵 ) → ( 𝐶 / 𝐵 ) ≤ ( 𝐶 / 𝐴 ) )
10 6 7 8 5 9 syl31anc ( 𝜑 → ( 𝐶 / 𝐵 ) ≤ ( 𝐶 / 𝐴 ) )