Theorem lemuldiv4d

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

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

Proof

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