This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ( ( ( ( 𝐴 ∈ ℝ ∧ 0 < 𝐴 ) ∧ ( 𝐵 ∈ ℝ ∧ 0 < 𝐵 ) ∧ ( 𝐶 ∈ ℝ ∧ 0 ≤ 𝐶 ) ) ∧ 𝐴 ≤ 𝐵 ) → ( 𝐶 / 𝐵 ) ≤ ( 𝐶 / 𝐴 ) )

Proof

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