Theorem lt2mul2divd

Description: The ratio of nonnegative and positive numbers is nonnegative. (Contributed by Mario Carneiro, 28-May-2016)

	Ref	Expression
Hypotheses	lt2mul2divd.1	⊢ ( 𝜑 → 𝐴 ∈ ℝ )
	lt2mul2divd.2	⊢ ( 𝜑 → 𝐵 ∈ ℝ+ )
	lt2mul2divd.3	⊢ ( 𝜑 → 𝐶 ∈ ℝ )
	lt2mul2divd.4	⊢ ( 𝜑 → 𝐷 ∈ ℝ+ )
Assertion	lt2mul2divd	⊢ ( 𝜑 → ( ( 𝐴 · 𝐵 ) < ( 𝐶 · 𝐷 ) ↔ ( 𝐴 / 𝐷 ) < ( 𝐶 / 𝐵 ) ) )

Proof

Step	Hyp	Ref	Expression
1		lt2mul2divd.1	⊢ ( 𝜑 → 𝐴 ∈ ℝ )
2		lt2mul2divd.2	⊢ ( 𝜑 → 𝐵 ∈ ℝ+ )
3		lt2mul2divd.3	⊢ ( 𝜑 → 𝐶 ∈ ℝ )
4		lt2mul2divd.4	⊢ ( 𝜑 → 𝐷 ∈ ℝ+ )
5	2	rpregt0d	⊢ ( 𝜑 → ( 𝐵 ∈ ℝ ∧ 0 < 𝐵 ) )
6	4	rpregt0d	⊢ ( 𝜑 → ( 𝐷 ∈ ℝ ∧ 0 < 𝐷 ) )
7		lt2mul2div	⊢ ( ( ( 𝐴 ∈ ℝ ∧ ( 𝐵 ∈ ℝ ∧ 0 < 𝐵 ) ) ∧ ( 𝐶 ∈ ℝ ∧ ( 𝐷 ∈ ℝ ∧ 0 < 𝐷 ) ) ) → ( ( 𝐴 · 𝐵 ) < ( 𝐶 · 𝐷 ) ↔ ( 𝐴 / 𝐷 ) < ( 𝐶 / 𝐵 ) ) )
8	1 5 3 6 7	syl22anc	⊢ ( 𝜑 → ( ( 𝐴 · 𝐵 ) < ( 𝐶 · 𝐷 ) ↔ ( 𝐴 / 𝐷 ) < ( 𝐶 / 𝐵 ) ) )