Theorem ltmuldiv

Description: 'Less than' relationship between division and multiplication. (Contributed by NM, 12-Oct-1999) (Proof shortened by Mario Carneiro, 27-May-2016)

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

Proof

Step	Hyp	Ref	Expression
1		simp1	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ ( 𝐶 ∈ ℝ ∧ 0 < 𝐶 ) ) → 𝐴 ∈ ℝ )
2		simp3l	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ ( 𝐶 ∈ ℝ ∧ 0 < 𝐶 ) ) → 𝐶 ∈ ℝ )
3	1 2	remulcld	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ ( 𝐶 ∈ ℝ ∧ 0 < 𝐶 ) ) → ( 𝐴 · 𝐶 ) ∈ ℝ )
4		ltdiv1	⊢ ( ( ( 𝐴 · 𝐶 ) ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ ( 𝐶 ∈ ℝ ∧ 0 < 𝐶 ) ) → ( ( 𝐴 · 𝐶 ) < 𝐵 ↔ ( ( 𝐴 · 𝐶 ) / 𝐶 ) < ( 𝐵 / 𝐶 ) ) )
5	3 4	syld3an1	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ ( 𝐶 ∈ ℝ ∧ 0 < 𝐶 ) ) → ( ( 𝐴 · 𝐶 ) < 𝐵 ↔ ( ( 𝐴 · 𝐶 ) / 𝐶 ) < ( 𝐵 / 𝐶 ) ) )
6	1	recnd	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ ( 𝐶 ∈ ℝ ∧ 0 < 𝐶 ) ) → 𝐴 ∈ ℂ )
7	2	recnd	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ ( 𝐶 ∈ ℝ ∧ 0 < 𝐶 ) ) → 𝐶 ∈ ℂ )
8		simp3r	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ ( 𝐶 ∈ ℝ ∧ 0 < 𝐶 ) ) → 0 < 𝐶 )
9	8	gt0ne0d	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ ( 𝐶 ∈ ℝ ∧ 0 < 𝐶 ) ) → 𝐶 ≠ 0 )
10	6 7 9	divcan4d	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ ( 𝐶 ∈ ℝ ∧ 0 < 𝐶 ) ) → ( ( 𝐴 · 𝐶 ) / 𝐶 ) = 𝐴 )
11	10	breq1d	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ ( 𝐶 ∈ ℝ ∧ 0 < 𝐶 ) ) → ( ( ( 𝐴 · 𝐶 ) / 𝐶 ) < ( 𝐵 / 𝐶 ) ↔ 𝐴 < ( 𝐵 / 𝐶 ) ) )
12	5 11	bitrd	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ ( 𝐶 ∈ ℝ ∧ 0 < 𝐶 ) ) → ( ( 𝐴 · 𝐶 ) < 𝐵 ↔ 𝐴 < ( 𝐵 / 𝐶 ) ) )