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