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 | ⊢ ( 𝜑 → ( 𝐶 / 𝐵 ) ≤ ( 𝐶 / 𝐴 ) ) |
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 | ⊢ ( 𝜑 → ( 𝐶 / 𝐵 ) ≤ ( 𝐶 / 𝐴 ) ) |