Theorem lt2mul2div

Description: 'Less than' relationship between division and multiplication. (Contributed by NM, 8-Jan-2006)

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

Proof

Step	Hyp	Ref	Expression
1		recn	⊢ ( 𝐶 ∈ ℝ → 𝐶 ∈ ℂ )
2		recn	⊢ ( 𝐷 ∈ ℝ → 𝐷 ∈ ℂ )
3		mulcom	⊢ ( ( 𝐶 ∈ ℂ ∧ 𝐷 ∈ ℂ ) → ( 𝐶 · 𝐷 ) = ( 𝐷 · 𝐶 ) )
4	1 2 3	syl2an	⊢ ( ( 𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ ) → ( 𝐶 · 𝐷 ) = ( 𝐷 · 𝐶 ) )
5	4	oveq1d	⊢ ( ( 𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ ) → ( ( 𝐶 · 𝐷 ) / 𝐵 ) = ( ( 𝐷 · 𝐶 ) / 𝐵 ) )
6	5	adantl	⊢ ( ( ( 𝐵 ∈ ℝ ∧ 0 < 𝐵 ) ∧ ( 𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ ) ) → ( ( 𝐶 · 𝐷 ) / 𝐵 ) = ( ( 𝐷 · 𝐶 ) / 𝐵 ) )
7	2	ad2antll	⊢ ( ( ( 𝐵 ∈ ℝ ∧ 0 < 𝐵 ) ∧ ( 𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ ) ) → 𝐷 ∈ ℂ )
8	1	ad2antrl	⊢ ( ( ( 𝐵 ∈ ℝ ∧ 0 < 𝐵 ) ∧ ( 𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ ) ) → 𝐶 ∈ ℂ )
9		recn	⊢ ( 𝐵 ∈ ℝ → 𝐵 ∈ ℂ )
10	9	adantr	⊢ ( ( 𝐵 ∈ ℝ ∧ 0 < 𝐵 ) → 𝐵 ∈ ℂ )
11		gt0ne0	⊢ ( ( 𝐵 ∈ ℝ ∧ 0 < 𝐵 ) → 𝐵 ≠ 0 )
12	10 11	jca	⊢ ( ( 𝐵 ∈ ℝ ∧ 0 < 𝐵 ) → ( 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0 ) )
13	12	adantr	⊢ ( ( ( 𝐵 ∈ ℝ ∧ 0 < 𝐵 ) ∧ ( 𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ ) ) → ( 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0 ) )
14		divass	⊢ ( ( 𝐷 ∈ ℂ ∧ 𝐶 ∈ ℂ ∧ ( 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0 ) ) → ( ( 𝐷 · 𝐶 ) / 𝐵 ) = ( 𝐷 · ( 𝐶 / 𝐵 ) ) )
15	7 8 13 14	syl3anc	⊢ ( ( ( 𝐵 ∈ ℝ ∧ 0 < 𝐵 ) ∧ ( 𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ ) ) → ( ( 𝐷 · 𝐶 ) / 𝐵 ) = ( 𝐷 · ( 𝐶 / 𝐵 ) ) )
16	6 15	eqtrd	⊢ ( ( ( 𝐵 ∈ ℝ ∧ 0 < 𝐵 ) ∧ ( 𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ ) ) → ( ( 𝐶 · 𝐷 ) / 𝐵 ) = ( 𝐷 · ( 𝐶 / 𝐵 ) ) )
17	16	adantrrr	⊢ ( ( ( 𝐵 ∈ ℝ ∧ 0 < 𝐵 ) ∧ ( 𝐶 ∈ ℝ ∧ ( 𝐷 ∈ ℝ ∧ 0 < 𝐷 ) ) ) → ( ( 𝐶 · 𝐷 ) / 𝐵 ) = ( 𝐷 · ( 𝐶 / 𝐵 ) ) )
18	17	adantll	⊢ ( ( ( 𝐴 ∈ ℝ ∧ ( 𝐵 ∈ ℝ ∧ 0 < 𝐵 ) ) ∧ ( 𝐶 ∈ ℝ ∧ ( 𝐷 ∈ ℝ ∧ 0 < 𝐷 ) ) ) → ( ( 𝐶 · 𝐷 ) / 𝐵 ) = ( 𝐷 · ( 𝐶 / 𝐵 ) ) )
19	18	breq2d	⊢ ( ( ( 𝐴 ∈ ℝ ∧ ( 𝐵 ∈ ℝ ∧ 0 < 𝐵 ) ) ∧ ( 𝐶 ∈ ℝ ∧ ( 𝐷 ∈ ℝ ∧ 0 < 𝐷 ) ) ) → ( 𝐴 < ( ( 𝐶 · 𝐷 ) / 𝐵 ) ↔ 𝐴 < ( 𝐷 · ( 𝐶 / 𝐵 ) ) ) )
20		simpll	⊢ ( ( ( 𝐴 ∈ ℝ ∧ ( 𝐵 ∈ ℝ ∧ 0 < 𝐵 ) ) ∧ ( 𝐶 ∈ ℝ ∧ ( 𝐷 ∈ ℝ ∧ 0 < 𝐷 ) ) ) → 𝐴 ∈ ℝ )
21		remulcl	⊢ ( ( 𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ ) → ( 𝐶 · 𝐷 ) ∈ ℝ )
22	21	adantrr	⊢ ( ( 𝐶 ∈ ℝ ∧ ( 𝐷 ∈ ℝ ∧ 0 < 𝐷 ) ) → ( 𝐶 · 𝐷 ) ∈ ℝ )
23	22	adantl	⊢ ( ( ( 𝐴 ∈ ℝ ∧ ( 𝐵 ∈ ℝ ∧ 0 < 𝐵 ) ) ∧ ( 𝐶 ∈ ℝ ∧ ( 𝐷 ∈ ℝ ∧ 0 < 𝐷 ) ) ) → ( 𝐶 · 𝐷 ) ∈ ℝ )
24		simplr	⊢ ( ( ( 𝐴 ∈ ℝ ∧ ( 𝐵 ∈ ℝ ∧ 0 < 𝐵 ) ) ∧ ( 𝐶 ∈ ℝ ∧ ( 𝐷 ∈ ℝ ∧ 0 < 𝐷 ) ) ) → ( 𝐵 ∈ ℝ ∧ 0 < 𝐵 ) )
25		ltmuldiv	⊢ ( ( 𝐴 ∈ ℝ ∧ ( 𝐶 · 𝐷 ) ∈ ℝ ∧ ( 𝐵 ∈ ℝ ∧ 0 < 𝐵 ) ) → ( ( 𝐴 · 𝐵 ) < ( 𝐶 · 𝐷 ) ↔ 𝐴 < ( ( 𝐶 · 𝐷 ) / 𝐵 ) ) )
26	20 23 24 25	syl3anc	⊢ ( ( ( 𝐴 ∈ ℝ ∧ ( 𝐵 ∈ ℝ ∧ 0 < 𝐵 ) ) ∧ ( 𝐶 ∈ ℝ ∧ ( 𝐷 ∈ ℝ ∧ 0 < 𝐷 ) ) ) → ( ( 𝐴 · 𝐵 ) < ( 𝐶 · 𝐷 ) ↔ 𝐴 < ( ( 𝐶 · 𝐷 ) / 𝐵 ) ) )
27		simpl	⊢ ( ( 𝐵 ∈ ℝ ∧ 0 < 𝐵 ) → 𝐵 ∈ ℝ )
28	27 11	jca	⊢ ( ( 𝐵 ∈ ℝ ∧ 0 < 𝐵 ) → ( 𝐵 ∈ ℝ ∧ 𝐵 ≠ 0 ) )
29		redivcl	⊢ ( ( 𝐶 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐵 ≠ 0 ) → ( 𝐶 / 𝐵 ) ∈ ℝ )
30	29	3expb	⊢ ( ( 𝐶 ∈ ℝ ∧ ( 𝐵 ∈ ℝ ∧ 𝐵 ≠ 0 ) ) → ( 𝐶 / 𝐵 ) ∈ ℝ )
31	28 30	sylan2	⊢ ( ( 𝐶 ∈ ℝ ∧ ( 𝐵 ∈ ℝ ∧ 0 < 𝐵 ) ) → ( 𝐶 / 𝐵 ) ∈ ℝ )
32	31	ancoms	⊢ ( ( ( 𝐵 ∈ ℝ ∧ 0 < 𝐵 ) ∧ 𝐶 ∈ ℝ ) → ( 𝐶 / 𝐵 ) ∈ ℝ )
33	32	ad2ant2lr	⊢ ( ( ( 𝐴 ∈ ℝ ∧ ( 𝐵 ∈ ℝ ∧ 0 < 𝐵 ) ) ∧ ( 𝐶 ∈ ℝ ∧ ( 𝐷 ∈ ℝ ∧ 0 < 𝐷 ) ) ) → ( 𝐶 / 𝐵 ) ∈ ℝ )
34		simprr	⊢ ( ( ( 𝐴 ∈ ℝ ∧ ( 𝐵 ∈ ℝ ∧ 0 < 𝐵 ) ) ∧ ( 𝐶 ∈ ℝ ∧ ( 𝐷 ∈ ℝ ∧ 0 < 𝐷 ) ) ) → ( 𝐷 ∈ ℝ ∧ 0 < 𝐷 ) )
35		ltdivmul	⊢ ( ( 𝐴 ∈ ℝ ∧ ( 𝐶 / 𝐵 ) ∈ ℝ ∧ ( 𝐷 ∈ ℝ ∧ 0 < 𝐷 ) ) → ( ( 𝐴 / 𝐷 ) < ( 𝐶 / 𝐵 ) ↔ 𝐴 < ( 𝐷 · ( 𝐶 / 𝐵 ) ) ) )
36	20 33 34 35	syl3anc	⊢ ( ( ( 𝐴 ∈ ℝ ∧ ( 𝐵 ∈ ℝ ∧ 0 < 𝐵 ) ) ∧ ( 𝐶 ∈ ℝ ∧ ( 𝐷 ∈ ℝ ∧ 0 < 𝐷 ) ) ) → ( ( 𝐴 / 𝐷 ) < ( 𝐶 / 𝐵 ) ↔ 𝐴 < ( 𝐷 · ( 𝐶 / 𝐵 ) ) ) )
37	19 26 36	3bitr4d	⊢ ( ( ( 𝐴 ∈ ℝ ∧ ( 𝐵 ∈ ℝ ∧ 0 < 𝐵 ) ) ∧ ( 𝐶 ∈ ℝ ∧ ( 𝐷 ∈ ℝ ∧ 0 < 𝐷 ) ) ) → ( ( 𝐴 · 𝐵 ) < ( 𝐶 · 𝐷 ) ↔ ( 𝐴 / 𝐷 ) < ( 𝐶 / 𝐵 ) ) )