Theorem ledivmul

Description: 'Less than or equal to' relationship between division and multiplication. (Contributed by NM, 9-Dec-2005)

	Ref	Expression
Assertion	ledivmul	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ ( 𝐶 ∈ ℝ ∧ 0 < 𝐶 ) ) → ( ( 𝐴 / 𝐶 ) ≤ 𝐵 ↔ 𝐴 ≤ ( 𝐶 · 𝐵 ) ) )

Proof

Step	Hyp	Ref	Expression
1		remulcl	⊢ ( ( 𝐶 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( 𝐶 · 𝐵 ) ∈ ℝ )
2	1	ancoms	⊢ ( ( 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) → ( 𝐶 · 𝐵 ) ∈ ℝ )
3	2	adantrr	⊢ ( ( 𝐵 ∈ ℝ ∧ ( 𝐶 ∈ ℝ ∧ 0 < 𝐶 ) ) → ( 𝐶 · 𝐵 ) ∈ ℝ )
4	3	3adant1	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ ( 𝐶 ∈ ℝ ∧ 0 < 𝐶 ) ) → ( 𝐶 · 𝐵 ) ∈ ℝ )
5		lediv1	⊢ ( ( 𝐴 ∈ ℝ ∧ ( 𝐶 · 𝐵 ) ∈ ℝ ∧ ( 𝐶 ∈ ℝ ∧ 0 < 𝐶 ) ) → ( 𝐴 ≤ ( 𝐶 · 𝐵 ) ↔ ( 𝐴 / 𝐶 ) ≤ ( ( 𝐶 · 𝐵 ) / 𝐶 ) ) )
6	4 5	syld3an2	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ ( 𝐶 ∈ ℝ ∧ 0 < 𝐶 ) ) → ( 𝐴 ≤ ( 𝐶 · 𝐵 ) ↔ ( 𝐴 / 𝐶 ) ≤ ( ( 𝐶 · 𝐵 ) / 𝐶 ) ) )
7		recn	⊢ ( 𝐵 ∈ ℝ → 𝐵 ∈ ℂ )
8	7	adantr	⊢ ( ( 𝐵 ∈ ℝ ∧ ( 𝐶 ∈ ℝ ∧ 0 < 𝐶 ) ) → 𝐵 ∈ ℂ )
9		recn	⊢ ( 𝐶 ∈ ℝ → 𝐶 ∈ ℂ )
10	9	ad2antrl	⊢ ( ( 𝐵 ∈ ℝ ∧ ( 𝐶 ∈ ℝ ∧ 0 < 𝐶 ) ) → 𝐶 ∈ ℂ )
11		gt0ne0	⊢ ( ( 𝐶 ∈ ℝ ∧ 0 < 𝐶 ) → 𝐶 ≠ 0 )
12	11	adantl	⊢ ( ( 𝐵 ∈ ℝ ∧ ( 𝐶 ∈ ℝ ∧ 0 < 𝐶 ) ) → 𝐶 ≠ 0 )
13	8 10 12	divcan3d	⊢ ( ( 𝐵 ∈ ℝ ∧ ( 𝐶 ∈ ℝ ∧ 0 < 𝐶 ) ) → ( ( 𝐶 · 𝐵 ) / 𝐶 ) = 𝐵 )
14	13	3adant1	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ ( 𝐶 ∈ ℝ ∧ 0 < 𝐶 ) ) → ( ( 𝐶 · 𝐵 ) / 𝐶 ) = 𝐵 )
15	14	breq2d	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ ( 𝐶 ∈ ℝ ∧ 0 < 𝐶 ) ) → ( ( 𝐴 / 𝐶 ) ≤ ( ( 𝐶 · 𝐵 ) / 𝐶 ) ↔ ( 𝐴 / 𝐶 ) ≤ 𝐵 ) )
16	6 15	bitr2d	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ ( 𝐶 ∈ ℝ ∧ 0 < 𝐶 ) ) → ( ( 𝐴 / 𝐶 ) ≤ 𝐵 ↔ 𝐴 ≤ ( 𝐶 · 𝐵 ) ) )