Metamath Proof Explorer

Theorem lediv2a

Description: Division of both sides of 'less than or equal to' into a nonnegative number. (Contributed by Paul Chapman, 7-Sep-2007)

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

Proof

Step Hyp Ref Expression
1 pm3.2 ⊢ C ∈ ℝ → C ∈ ℝ → C ∈ ℝ ∧ C ∈ ℝ
2 1 pm2.43i ⊢ C ∈ ℝ → C ∈ ℝ ∧ C ∈ ℝ
3 2 adantr ⊢ C ∈ ℝ ∧ 0 ≤ C → C ∈ ℝ ∧ C ∈ ℝ
4 leid ⊢ C ∈ ℝ → C ≤ C
5 4 anim1ci ⊢ C ∈ ℝ ∧ 0 ≤ C → 0 ≤ C ∧ C ≤ C
6 3 5 jca ⊢ C ∈ ℝ ∧ 0 ≤ C → C ∈ ℝ ∧ C ∈ ℝ ∧ 0 ≤ C ∧ C ≤ C
7 6 ad2antlr ⊢ A ∈ ℝ ∧ 0 < A ∧ C ∈ ℝ ∧ 0 ≤ C ∧ A ≤ B → C ∈ ℝ ∧ C ∈ ℝ ∧ 0 ≤ C ∧ C ≤ C
8 7 3adantl2 ⊢ A ∈ ℝ ∧ 0 < A ∧ B ∈ ℝ ∧ 0 < B ∧ C ∈ ℝ ∧ 0 ≤ C ∧ A ≤ B → C ∈ ℝ ∧ C ∈ ℝ ∧ 0 ≤ C ∧ C ≤ C
9 id ⊢ A ∈ ℝ ∧ B ∈ ℝ → A ∈ ℝ ∧ B ∈ ℝ
10 9 ad2ant2r ⊢ A ∈ ℝ ∧ 0 < A ∧ B ∈ ℝ ∧ 0 < B → A ∈ ℝ ∧ B ∈ ℝ
11 10 adantr ⊢ A ∈ ℝ ∧ 0 < A ∧ B ∈ ℝ ∧ 0 < B ∧ A ≤ B → A ∈ ℝ ∧ B ∈ ℝ
12 simplr ⊢ A ∈ ℝ ∧ 0 < A ∧ B ∈ ℝ ∧ 0 < B → 0 < A
13 12 anim1i ⊢ A ∈ ℝ ∧ 0 < A ∧ B ∈ ℝ ∧ 0 < B ∧ A ≤ B → 0 < A ∧ A ≤ B
14 11 13 jca ⊢ A ∈ ℝ ∧ 0 < A ∧ B ∈ ℝ ∧ 0 < B ∧ A ≤ B → A ∈ ℝ ∧ B ∈ ℝ ∧ 0 < A ∧ A ≤ B
15 14 3adantl3 ⊢ A ∈ ℝ ∧ 0 < A ∧ B ∈ ℝ ∧ 0 < B ∧ C ∈ ℝ ∧ 0 ≤ C ∧ A ≤ B → A ∈ ℝ ∧ B ∈ ℝ ∧ 0 < A ∧ A ≤ B
16 lediv12a ⊢ C ∈ ℝ ∧ C ∈ ℝ ∧ 0 ≤ C ∧ C ≤ C ∧ A ∈ ℝ ∧ B ∈ ℝ ∧ 0 < A ∧ A ≤ B → C B ≤ C A
17 8 15 16 syl2anc ⊢ A ∈ ℝ ∧ 0 < A ∧ B ∈ ℝ ∧ 0 < B ∧ C ∈ ℝ ∧ 0 ≤ C ∧ A ≤ B → C B ≤ C A