Theorem lemuldiv3d

Description: 'Less than or equal to' relationship between division and multiplication. (Contributed by Stanislas Polu, 9-Mar-2020)

	Ref	Expression
Hypotheses	lemuldiv3d.1	⊢ ( 𝜑 → ( 𝐵 · 𝐴 ) ≤ 𝐶 )
	lemuldiv3d.2	⊢ ( 𝜑 → 0 < 𝐴 )
	lemuldiv3d.3	⊢ ( 𝜑 → 𝐴 ∈ ℝ )
	lemuldiv3d.4	⊢ ( 𝜑 → 𝐵 ∈ ℝ )
	lemuldiv3d.5	⊢ ( 𝜑 → 𝐶 ∈ ℝ )
Assertion	lemuldiv3d	⊢ ( 𝜑 → 𝐵 ≤ ( 𝐶 / 𝐴 ) )

Proof

Step	Hyp	Ref	Expression
1		lemuldiv3d.1	⊢ ( 𝜑 → ( 𝐵 · 𝐴 ) ≤ 𝐶 )
2		lemuldiv3d.2	⊢ ( 𝜑 → 0 < 𝐴 )
3		lemuldiv3d.3	⊢ ( 𝜑 → 𝐴 ∈ ℝ )
4		lemuldiv3d.4	⊢ ( 𝜑 → 𝐵 ∈ ℝ )
5		lemuldiv3d.5	⊢ ( 𝜑 → 𝐶 ∈ ℝ )
6		lemuldiv	⊢ ( ( 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ∧ ( 𝐴 ∈ ℝ ∧ 0 < 𝐴 ) ) → ( ( 𝐵 · 𝐴 ) ≤ 𝐶 ↔ 𝐵 ≤ ( 𝐶 / 𝐴 ) ) )
7	4 5 3 2 6	syl112anc	⊢ ( 𝜑 → ( ( 𝐵 · 𝐴 ) ≤ 𝐶 ↔ 𝐵 ≤ ( 𝐶 / 𝐴 ) ) )
8	1 7	mpbid	⊢ ( 𝜑 → 𝐵 ≤ ( 𝐶 / 𝐴 ) )