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→CB≤CA

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→CB≤CA
17 8 15 16 syl2anc ⊢A∈ℝ∧0<A∧B∈ℝ∧0<B∧C∈ℝ∧0≤C∧A≤B→CB≤CA