lt2mul2div

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

		Ref	Expression
	Assertion	lt2mul2div	$⊢ ((A \in ℝ \land (B \in ℝ \land 0 < B)) \land (C \in ℝ \land (D \in ℝ \land 0 < D))) \to (A B < C D \leftrightarrow \frac{A}{D} < \frac{C}{B})$

Proof

Step	Hyp	Ref	Expression
1		recn	$⊢ C \in ℝ \to C \in ℂ$
2		recn	$⊢ D \in ℝ \to D \in ℂ$
3		mulcom	$⊢ (C \in ℂ \land D \in ℂ) \to C D = D C$
4	1 2 3	syl2an	$⊢ (C \in ℝ \land D \in ℝ) \to C D = D C$
5	4	oveq1d	$⊢ (C \in ℝ \land D \in ℝ) \to \frac{C D}{B} = \frac{D C}{B}$
6	5	adantl	$⊢ ((B \in ℝ \land 0 < B) \land (C \in ℝ \land D \in ℝ)) \to \frac{C D}{B} = \frac{D C}{B}$
7	2	ad2antll	$⊢ ((B \in ℝ \land 0 < B) \land (C \in ℝ \land D \in ℝ)) \to D \in ℂ$
8	1	ad2antrl	$⊢ ((B \in ℝ \land 0 < B) \land (C \in ℝ \land D \in ℝ)) \to C \in ℂ$
9		recn	$⊢ B \in ℝ \to B \in ℂ$
10	9	adantr	$⊢ (B \in ℝ \land 0 < B) \to B \in ℂ$
11		gt0ne0	$⊢ (B \in ℝ \land 0 < B) \to B \neq 0$
12	10 11	jca	$⊢ (B \in ℝ \land 0 < B) \to (B \in ℂ \land B \neq 0)$
13	12	adantr	$⊢ ((B \in ℝ \land 0 < B) \land (C \in ℝ \land D \in ℝ)) \to (B \in ℂ \land B \neq 0)$
14		divass	$⊢ (D \in ℂ \land C \in ℂ \land (B \in ℂ \land B \neq 0)) \to \frac{D C}{B} = D (\frac{C}{B})$
15	7 8 13 14	syl3anc	$⊢ ((B \in ℝ \land 0 < B) \land (C \in ℝ \land D \in ℝ)) \to \frac{D C}{B} = D (\frac{C}{B})$
16	6 15	eqtrd	$⊢ ((B \in ℝ \land 0 < B) \land (C \in ℝ \land D \in ℝ)) \to \frac{C D}{B} = D (\frac{C}{B})$
17	16	adantrrr	$⊢ ((B \in ℝ \land 0 < B) \land (C \in ℝ \land (D \in ℝ \land 0 < D))) \to \frac{C D}{B} = D (\frac{C}{B})$
18	17	adantll	$⊢ ((A \in ℝ \land (B \in ℝ \land 0 < B)) \land (C \in ℝ \land (D \in ℝ \land 0 < D))) \to \frac{C D}{B} = D (\frac{C}{B})$
19	18	breq2d	$⊢ ((A \in ℝ \land (B \in ℝ \land 0 < B)) \land (C \in ℝ \land (D \in ℝ \land 0 < D))) \to (A < \frac{C D}{B} \leftrightarrow A < D (\frac{C}{B}))$
20		simpll	$⊢ ((A \in ℝ \land (B \in ℝ \land 0 < B)) \land (C \in ℝ \land (D \in ℝ \land 0 < D))) \to A \in ℝ$
21		remulcl	$⊢ (C \in ℝ \land D \in ℝ) \to C D \in ℝ$
22	21	adantrr	$⊢ (C \in ℝ \land (D \in ℝ \land 0 < D)) \to C D \in ℝ$
23	22	adantl	$⊢ ((A \in ℝ \land (B \in ℝ \land 0 < B)) \land (C \in ℝ \land (D \in ℝ \land 0 < D))) \to C D \in ℝ$
24		simplr	$⊢ ((A \in ℝ \land (B \in ℝ \land 0 < B)) \land (C \in ℝ \land (D \in ℝ \land 0 < D))) \to (B \in ℝ \land 0 < B)$
25		ltmuldiv	$⊢ (A \in ℝ \land C D \in ℝ \land (B \in ℝ \land 0 < B)) \to (A B < C D \leftrightarrow A < \frac{C D}{B})$
26	20 23 24 25	syl3anc	$⊢ ((A \in ℝ \land (B \in ℝ \land 0 < B)) \land (C \in ℝ \land (D \in ℝ \land 0 < D))) \to (A B < C D \leftrightarrow A < \frac{C D}{B})$
27		simpl	$⊢ (B \in ℝ \land 0 < B) \to B \in ℝ$
28	27 11	jca	$⊢ (B \in ℝ \land 0 < B) \to (B \in ℝ \land B \neq 0)$
29		redivcl	$⊢ (C \in ℝ \land B \in ℝ \land B \neq 0) \to \frac{C}{B} \in ℝ$
30	29	3expb	$⊢ (C \in ℝ \land (B \in ℝ \land B \neq 0)) \to \frac{C}{B} \in ℝ$
31	28 30	sylan2	$⊢ (C \in ℝ \land (B \in ℝ \land 0 < B)) \to \frac{C}{B} \in ℝ$
32	31	ancoms	$⊢ ((B \in ℝ \land 0 < B) \land C \in ℝ) \to \frac{C}{B} \in ℝ$
33	32	ad2ant2lr	$⊢ ((A \in ℝ \land (B \in ℝ \land 0 < B)) \land (C \in ℝ \land (D \in ℝ \land 0 < D))) \to \frac{C}{B} \in ℝ$
34		simprr	$⊢ ((A \in ℝ \land (B \in ℝ \land 0 < B)) \land (C \in ℝ \land (D \in ℝ \land 0 < D))) \to (D \in ℝ \land 0 < D)$
35		ltdivmul	$⊢ (A \in ℝ \land \frac{C}{B} \in ℝ \land (D \in ℝ \land 0 < D)) \to (\frac{A}{D} < \frac{C}{B} \leftrightarrow A < D (\frac{C}{B}))$
36	20 33 34 35	syl3anc	$⊢ ((A \in ℝ \land (B \in ℝ \land 0 < B)) \land (C \in ℝ \land (D \in ℝ \land 0 < D))) \to (\frac{A}{D} < \frac{C}{B} \leftrightarrow A < D (\frac{C}{B}))$
37	19 26 36	3bitr4d	$⊢ ((A \in ℝ \land (B \in ℝ \land 0 < B)) \land (C \in ℝ \land (D \in ℝ \land 0 < D))) \to (A B < C D \leftrightarrow \frac{A}{D} < \frac{C}{B})$

Metamath Proof Explorer

Theorem lt2mul2div

Proof