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