ltdiv23

Description: Swap denominator with other side of 'less than'. (Contributed by NM, 3-Oct-1999)

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

Proof

Step	Hyp	Ref	Expression
1		simpl	$⊢ (B \in ℝ \land 0 < B) \to B \in ℝ$
2		gt0ne0	$⊢ (B \in ℝ \land 0 < B) \to B \neq 0$
3	1 2	jca	$⊢ (B \in ℝ \land 0 < B) \to (B \in ℝ \land B \neq 0)$
4		redivcl	$⊢ (A \in ℝ \land B \in ℝ \land B \neq 0) \to \frac{A}{B} \in ℝ$
5	4	3expb	$⊢ (A \in ℝ \land (B \in ℝ \land B \neq 0)) \to \frac{A}{B} \in ℝ$
6	3 5	sylan2	$⊢ (A \in ℝ \land (B \in ℝ \land 0 < B)) \to \frac{A}{B} \in ℝ$
7	6	3adant3	$⊢ (A \in ℝ \land (B \in ℝ \land 0 < B) \land C \in ℝ) \to \frac{A}{B} \in ℝ$
8		simp3	$⊢ (A \in ℝ \land (B \in ℝ \land 0 < B) \land C \in ℝ) \to C \in ℝ$
9		simp2	$⊢ (A \in ℝ \land (B \in ℝ \land 0 < B) \land C \in ℝ) \to (B \in ℝ \land 0 < B)$
10		ltmul1	$⊢ (\frac{A}{B} \in ℝ \land C \in ℝ \land (B \in ℝ \land 0 < B)) \to (\frac{A}{B} < C \leftrightarrow (\frac{A}{B}) B < C B)$
11	7 8 9 10	syl3anc	$⊢ (A \in ℝ \land (B \in ℝ \land 0 < B) \land C \in ℝ) \to (\frac{A}{B} < C \leftrightarrow (\frac{A}{B}) B < C B)$
12	11	3adant3r	$⊢ (A \in ℝ \land (B \in ℝ \land 0 < B) \land (C \in ℝ \land 0 < C)) \to (\frac{A}{B} < C \leftrightarrow (\frac{A}{B}) B < C B)$
13		recn	$⊢ A \in ℝ \to A \in ℂ$
14	13	adantr	$⊢ (A \in ℝ \land (B \in ℝ \land 0 < B)) \to A \in ℂ$
15		recn	$⊢ B \in ℝ \to B \in ℂ$
16	15	ad2antrl	$⊢ (A \in ℝ \land (B \in ℝ \land 0 < B)) \to B \in ℂ$
17	2	adantl	$⊢ (A \in ℝ \land (B \in ℝ \land 0 < B)) \to B \neq 0$
18	14 16 17	divcan1d	$⊢ (A \in ℝ \land (B \in ℝ \land 0 < B)) \to (\frac{A}{B}) B = A$
19	18	3adant3	$⊢ (A \in ℝ \land (B \in ℝ \land 0 < B) \land (C \in ℝ \land 0 < C)) \to (\frac{A}{B}) B = A$
20	19	breq1d	$⊢ (A \in ℝ \land (B \in ℝ \land 0 < B) \land (C \in ℝ \land 0 < C)) \to ((\frac{A}{B}) B < C B \leftrightarrow A < C B)$
21		remulcl	$⊢ (C \in ℝ \land B \in ℝ) \to C B \in ℝ$
22	21	ancoms	$⊢ (B \in ℝ \land C \in ℝ) \to C B \in ℝ$
23	22	adantrr	$⊢ (B \in ℝ \land (C \in ℝ \land 0 < C)) \to C B \in ℝ$
24	23	3adant1	$⊢ (A \in ℝ \land B \in ℝ \land (C \in ℝ \land 0 < C)) \to C B \in ℝ$
25		ltdiv1	$⊢ (A \in ℝ \land C B \in ℝ \land (C \in ℝ \land 0 < C)) \to (A < C B \leftrightarrow \frac{A}{C} < \frac{C B}{C})$
26	24 25	syld3an2	$⊢ (A \in ℝ \land B \in ℝ \land (C \in ℝ \land 0 < C)) \to (A < C B \leftrightarrow \frac{A}{C} < \frac{C B}{C})$
27		recn	$⊢ C \in ℝ \to C \in ℂ$
28	27	adantr	$⊢ (C \in ℝ \land 0 < C) \to C \in ℂ$
29		gt0ne0	$⊢ (C \in ℝ \land 0 < C) \to C \neq 0$
30	28 29	jca	$⊢ (C \in ℝ \land 0 < C) \to (C \in ℂ \land C \neq 0)$
31		divcan3	$⊢ (B \in ℂ \land C \in ℂ \land C \neq 0) \to \frac{C B}{C} = B$
32	31	3expb	$⊢ (B \in ℂ \land (C \in ℂ \land C \neq 0)) \to \frac{C B}{C} = B$
33	15 30 32	syl2an	$⊢ (B \in ℝ \land (C \in ℝ \land 0 < C)) \to \frac{C B}{C} = B$
34	33	3adant1	$⊢ (A \in ℝ \land B \in ℝ \land (C \in ℝ \land 0 < C)) \to \frac{C B}{C} = B$
35	34	breq2d	$⊢ (A \in ℝ \land B \in ℝ \land (C \in ℝ \land 0 < C)) \to (\frac{A}{C} < \frac{C B}{C} \leftrightarrow \frac{A}{C} < B)$
36	26 35	bitrd	$⊢ (A \in ℝ \land B \in ℝ \land (C \in ℝ \land 0 < C)) \to (A < C B \leftrightarrow \frac{A}{C} < B)$
37	36	3adant2r	$⊢ (A \in ℝ \land (B \in ℝ \land 0 < B) \land (C \in ℝ \land 0 < C)) \to (A < C B \leftrightarrow \frac{A}{C} < B)$
38	12 20 37	3bitrd	$⊢ (A \in ℝ \land (B \in ℝ \land 0 < B) \land (C \in ℝ \land 0 < C)) \to (\frac{A}{B} < C \leftrightarrow \frac{A}{C} < B)$

Metamath Proof Explorer

Theorem ltdiv23

Proof