ledivdiv

Description: Invert ratios of positive numbers and swap their ordering. (Contributed by NM, 9-Jan-2006)

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

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	adantlr	$⊢ ((A \in ℝ \land 0 < A) \land (B \in ℝ \land 0 < B)) \to \frac{A}{B} \in ℝ$
8		divgt0	$⊢ ((A \in ℝ \land 0 < A) \land (B \in ℝ \land 0 < B)) \to 0 < \frac{A}{B}$
9	7 8	jca	$⊢ ((A \in ℝ \land 0 < A) \land (B \in ℝ \land 0 < B)) \to (\frac{A}{B} \in ℝ \land 0 < \frac{A}{B})$
10		simpl	$⊢ (D \in ℝ \land 0 < D) \to D \in ℝ$
11		gt0ne0	$⊢ (D \in ℝ \land 0 < D) \to D \neq 0$
12	10 11	jca	$⊢ (D \in ℝ \land 0 < D) \to (D \in ℝ \land D \neq 0)$
13		redivcl	$⊢ (C \in ℝ \land D \in ℝ \land D \neq 0) \to \frac{C}{D} \in ℝ$
14	13	3expb	$⊢ (C \in ℝ \land (D \in ℝ \land D \neq 0)) \to \frac{C}{D} \in ℝ$
15	12 14	sylan2	$⊢ (C \in ℝ \land (D \in ℝ \land 0 < D)) \to \frac{C}{D} \in ℝ$
16	15	adantlr	$⊢ ((C \in ℝ \land 0 < C) \land (D \in ℝ \land 0 < D)) \to \frac{C}{D} \in ℝ$
17		divgt0	$⊢ ((C \in ℝ \land 0 < C) \land (D \in ℝ \land 0 < D)) \to 0 < \frac{C}{D}$
18	16 17	jca	$⊢ ((C \in ℝ \land 0 < C) \land (D \in ℝ \land 0 < D)) \to (\frac{C}{D} \in ℝ \land 0 < \frac{C}{D})$
19		lerec	$⊢ ((\frac{A}{B} \in ℝ \land 0 < \frac{A}{B}) \land (\frac{C}{D} \in ℝ \land 0 < \frac{C}{D})) \to (\frac{A}{B} \leq \frac{C}{D} \leftrightarrow \frac{1}{\frac{C}{D}} \leq \frac{1}{\frac{A}{B}})$
20	9 18 19	syl2an	$⊢ (((A \in ℝ \land 0 < A) \land (B \in ℝ \land 0 < B)) \land ((C \in ℝ \land 0 < C) \land (D \in ℝ \land 0 < D))) \to (\frac{A}{B} \leq \frac{C}{D} \leftrightarrow \frac{1}{\frac{C}{D}} \leq \frac{1}{\frac{A}{B}})$
21		recn	$⊢ C \in ℝ \to C \in ℂ$
22	21	adantr	$⊢ (C \in ℝ \land 0 < C) \to C \in ℂ$
23		gt0ne0	$⊢ (C \in ℝ \land 0 < C) \to C \neq 0$
24	22 23	jca	$⊢ (C \in ℝ \land 0 < C) \to (C \in ℂ \land C \neq 0)$
25		recn	$⊢ D \in ℝ \to D \in ℂ$
26	25	adantr	$⊢ (D \in ℝ \land 0 < D) \to D \in ℂ$
27	26 11	jca	$⊢ (D \in ℝ \land 0 < D) \to (D \in ℂ \land D \neq 0)$
28		recdiv	$⊢ ((C \in ℂ \land C \neq 0) \land (D \in ℂ \land D \neq 0)) \to \frac{1}{\frac{C}{D}} = \frac{D}{C}$
29	24 27 28	syl2an	$⊢ ((C \in ℝ \land 0 < C) \land (D \in ℝ \land 0 < D)) \to \frac{1}{\frac{C}{D}} = \frac{D}{C}$
30		recn	$⊢ A \in ℝ \to A \in ℂ$
31	30	adantr	$⊢ (A \in ℝ \land 0 < A) \to A \in ℂ$
32		gt0ne0	$⊢ (A \in ℝ \land 0 < A) \to A \neq 0$
33	31 32	jca	$⊢ (A \in ℝ \land 0 < A) \to (A \in ℂ \land A \neq 0)$
34		recn	$⊢ B \in ℝ \to B \in ℂ$
35	34	adantr	$⊢ (B \in ℝ \land 0 < B) \to B \in ℂ$
36	35 2	jca	$⊢ (B \in ℝ \land 0 < B) \to (B \in ℂ \land B \neq 0)$
37		recdiv	$⊢ ((A \in ℂ \land A \neq 0) \land (B \in ℂ \land B \neq 0)) \to \frac{1}{\frac{A}{B}} = \frac{B}{A}$
38	33 36 37	syl2an	$⊢ ((A \in ℝ \land 0 < A) \land (B \in ℝ \land 0 < B)) \to \frac{1}{\frac{A}{B}} = \frac{B}{A}$
39	29 38	breqan12rd	$⊢ (((A \in ℝ \land 0 < A) \land (B \in ℝ \land 0 < B)) \land ((C \in ℝ \land 0 < C) \land (D \in ℝ \land 0 < D))) \to (\frac{1}{\frac{C}{D}} \leq \frac{1}{\frac{A}{B}} \leftrightarrow \frac{D}{C} \leq \frac{B}{A})$
40	20 39	bitrd	$⊢ (((A \in ℝ \land 0 < A) \land (B \in ℝ \land 0 < B)) \land ((C \in ℝ \land 0 < C) \land (D \in ℝ \land 0 < D))) \to (\frac{A}{B} \leq \frac{C}{D} \leftrightarrow \frac{D}{C} \leq \frac{B}{A})$

Metamath Proof Explorer

Theorem ledivdiv

Proof