lediv12a

Description: Comparison of ratio of two nonnegative numbers. (Contributed by NM, 31-Dec-2005)

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

Proof

Step	Hyp	Ref	Expression
1		simplr	$⊢ ((C \in ℝ \land D \in ℝ) \land (0 < C \land C \leq D)) \to D \in ℝ$
2		0re	$⊢ 0 \in ℝ$
3		ltletr	$⊢ (0 \in ℝ \land C \in ℝ \land D \in ℝ) \to ((0 < C \land C \leq D) \to 0 < D)$
4	2 3	mp3an1	$⊢ (C \in ℝ \land D \in ℝ) \to ((0 < C \land C \leq D) \to 0 < D)$
5	4	imp	$⊢ ((C \in ℝ \land D \in ℝ) \land (0 < C \land C \leq D)) \to 0 < D$
6	5	gt0ne0d	$⊢ ((C \in ℝ \land D \in ℝ) \land (0 < C \land C \leq D)) \to D \neq 0$
7	1 6	rereccld	$⊢ ((C \in ℝ \land D \in ℝ) \land (0 < C \land C \leq D)) \to \frac{1}{D} \in ℝ$
8		gt0ne0	$⊢ (C \in ℝ \land 0 < C) \to C \neq 0$
9		rereccl	$⊢ (C \in ℝ \land C \neq 0) \to \frac{1}{C} \in ℝ$
10	8 9	syldan	$⊢ (C \in ℝ \land 0 < C) \to \frac{1}{C} \in ℝ$
11	10	ad2ant2r	$⊢ ((C \in ℝ \land D \in ℝ) \land (0 < C \land C \leq D)) \to \frac{1}{C} \in ℝ$
12		recgt0	$⊢ (D \in ℝ \land 0 < D) \to 0 < \frac{1}{D}$
13	1 5 12	syl2anc	$⊢ ((C \in ℝ \land D \in ℝ) \land (0 < C \land C \leq D)) \to 0 < \frac{1}{D}$
14		ltle	$⊢ (0 \in ℝ \land \frac{1}{D} \in ℝ) \to (0 < \frac{1}{D} \to 0 \leq \frac{1}{D})$
15	2 7 14	sylancr	$⊢ ((C \in ℝ \land D \in ℝ) \land (0 < C \land C \leq D)) \to (0 < \frac{1}{D} \to 0 \leq \frac{1}{D})$
16	13 15	mpd	$⊢ ((C \in ℝ \land D \in ℝ) \land (0 < C \land C \leq D)) \to 0 \leq \frac{1}{D}$
17		simprr	$⊢ ((C \in ℝ \land D \in ℝ) \land (0 < C \land C \leq D)) \to C \leq D$
18		id	$⊢ (C \in ℝ \land 0 < C) \to (C \in ℝ \land 0 < C)$
19	18	ad2ant2r	$⊢ ((C \in ℝ \land D \in ℝ) \land (0 < C \land C \leq D)) \to (C \in ℝ \land 0 < C)$
20		lerec	$⊢ ((C \in ℝ \land 0 < C) \land (D \in ℝ \land 0 < D)) \to (C \leq D \leftrightarrow \frac{1}{D} \leq \frac{1}{C})$
21	19 1 5 20	syl12anc	$⊢ ((C \in ℝ \land D \in ℝ) \land (0 < C \land C \leq D)) \to (C \leq D \leftrightarrow \frac{1}{D} \leq \frac{1}{C})$
22	17 21	mpbid	$⊢ ((C \in ℝ \land D \in ℝ) \land (0 < C \land C \leq D)) \to \frac{1}{D} \leq \frac{1}{C}$
23	16 22	jca	$⊢ ((C \in ℝ \land D \in ℝ) \land (0 < C \land C \leq D)) \to (0 \leq \frac{1}{D} \land \frac{1}{D} \leq \frac{1}{C})$
24	7 11 23	jca31	$⊢ ((C \in ℝ \land D \in ℝ) \land (0 < C \land C \leq D)) \to ((\frac{1}{D} \in ℝ \land \frac{1}{C} \in ℝ) \land (0 \leq \frac{1}{D} \land \frac{1}{D} \leq \frac{1}{C}))$
25		simplll	$⊢ (((A \in ℝ \land B \in ℝ) \land (0 \leq A \land A \leq B)) \land ((\frac{1}{D} \in ℝ \land \frac{1}{C} \in ℝ) \land (0 \leq \frac{1}{D} \land \frac{1}{D} \leq \frac{1}{C}))) \to A \in ℝ$
26		simplrl	$⊢ (((A \in ℝ \land B \in ℝ) \land (0 \leq A \land A \leq B)) \land ((\frac{1}{D} \in ℝ \land \frac{1}{C} \in ℝ) \land (0 \leq \frac{1}{D} \land \frac{1}{D} \leq \frac{1}{C}))) \to 0 \leq A$
27		simpllr	$⊢ (((A \in ℝ \land B \in ℝ) \land (0 \leq A \land A \leq B)) \land ((\frac{1}{D} \in ℝ \land \frac{1}{C} \in ℝ) \land (0 \leq \frac{1}{D} \land \frac{1}{D} \leq \frac{1}{C}))) \to B \in ℝ$
28	25 26 27	jca31	$⊢ (((A \in ℝ \land B \in ℝ) \land (0 \leq A \land A \leq B)) \land ((\frac{1}{D} \in ℝ \land \frac{1}{C} \in ℝ) \land (0 \leq \frac{1}{D} \land \frac{1}{D} \leq \frac{1}{C}))) \to ((A \in ℝ \land 0 \leq A) \land B \in ℝ)$
29		simprll	$⊢ (((A \in ℝ \land B \in ℝ) \land (0 \leq A \land A \leq B)) \land ((\frac{1}{D} \in ℝ \land \frac{1}{C} \in ℝ) \land (0 \leq \frac{1}{D} \land \frac{1}{D} \leq \frac{1}{C}))) \to \frac{1}{D} \in ℝ$
30		simprrl	$⊢ (((A \in ℝ \land B \in ℝ) \land (0 \leq A \land A \leq B)) \land ((\frac{1}{D} \in ℝ \land \frac{1}{C} \in ℝ) \land (0 \leq \frac{1}{D} \land \frac{1}{D} \leq \frac{1}{C}))) \to 0 \leq \frac{1}{D}$
31	29 30	jca	$⊢ (((A \in ℝ \land B \in ℝ) \land (0 \leq A \land A \leq B)) \land ((\frac{1}{D} \in ℝ \land \frac{1}{C} \in ℝ) \land (0 \leq \frac{1}{D} \land \frac{1}{D} \leq \frac{1}{C}))) \to (\frac{1}{D} \in ℝ \land 0 \leq \frac{1}{D})$
32		simprlr	$⊢ (((A \in ℝ \land B \in ℝ) \land (0 \leq A \land A \leq B)) \land ((\frac{1}{D} \in ℝ \land \frac{1}{C} \in ℝ) \land (0 \leq \frac{1}{D} \land \frac{1}{D} \leq \frac{1}{C}))) \to \frac{1}{C} \in ℝ$
33	28 31 32	jca32	$⊢ (((A \in ℝ \land B \in ℝ) \land (0 \leq A \land A \leq B)) \land ((\frac{1}{D} \in ℝ \land \frac{1}{C} \in ℝ) \land (0 \leq \frac{1}{D} \land \frac{1}{D} \leq \frac{1}{C}))) \to (((A \in ℝ \land 0 \leq A) \land B \in ℝ) \land ((\frac{1}{D} \in ℝ \land 0 \leq \frac{1}{D}) \land \frac{1}{C} \in ℝ))$
34		simplrr	$⊢ (((A \in ℝ \land B \in ℝ) \land (0 \leq A \land A \leq B)) \land ((\frac{1}{D} \in ℝ \land \frac{1}{C} \in ℝ) \land (0 \leq \frac{1}{D} \land \frac{1}{D} \leq \frac{1}{C}))) \to A \leq B$
35		simprrr	$⊢ (((A \in ℝ \land B \in ℝ) \land (0 \leq A \land A \leq B)) \land ((\frac{1}{D} \in ℝ \land \frac{1}{C} \in ℝ) \land (0 \leq \frac{1}{D} \land \frac{1}{D} \leq \frac{1}{C}))) \to \frac{1}{D} \leq \frac{1}{C}$
36	34 35	jca	$⊢ (((A \in ℝ \land B \in ℝ) \land (0 \leq A \land A \leq B)) \land ((\frac{1}{D} \in ℝ \land \frac{1}{C} \in ℝ) \land (0 \leq \frac{1}{D} \land \frac{1}{D} \leq \frac{1}{C}))) \to (A \leq B \land \frac{1}{D} \leq \frac{1}{C})$
37		lemul12a	$⊢ (((A \in ℝ \land 0 \leq A) \land B \in ℝ) \land ((\frac{1}{D} \in ℝ \land 0 \leq \frac{1}{D}) \land \frac{1}{C} \in ℝ)) \to ((A \leq B \land \frac{1}{D} \leq \frac{1}{C}) \to A (\frac{1}{D}) \leq B (\frac{1}{C}))$
38	33 36 37	sylc	$⊢ (((A \in ℝ \land B \in ℝ) \land (0 \leq A \land A \leq B)) \land ((\frac{1}{D} \in ℝ \land \frac{1}{C} \in ℝ) \land (0 \leq \frac{1}{D} \land \frac{1}{D} \leq \frac{1}{C}))) \to A (\frac{1}{D}) \leq B (\frac{1}{C})$
39	24 38	sylan2	$⊢ (((A \in ℝ \land B \in ℝ) \land (0 \leq A \land A \leq B)) \land ((C \in ℝ \land D \in ℝ) \land (0 < C \land C \leq D))) \to A (\frac{1}{D}) \leq B (\frac{1}{C})$
40		recn	$⊢ A \in ℝ \to A \in ℂ$
41	40	adantr	$⊢ (A \in ℝ \land ((C \in ℝ \land D \in ℝ) \land (0 < C \land C \leq D))) \to A \in ℂ$
42		recn	$⊢ D \in ℝ \to D \in ℂ$
43	42	ad2antlr	$⊢ ((C \in ℝ \land D \in ℝ) \land (0 < C \land C \leq D)) \to D \in ℂ$
44	43	adantl	$⊢ (A \in ℝ \land ((C \in ℝ \land D \in ℝ) \land (0 < C \land C \leq D))) \to D \in ℂ$
45	6	adantl	$⊢ (A \in ℝ \land ((C \in ℝ \land D \in ℝ) \land (0 < C \land C \leq D))) \to D \neq 0$
46	41 44 45	divrecd	$⊢ (A \in ℝ \land ((C \in ℝ \land D \in ℝ) \land (0 < C \land C \leq D))) \to \frac{A}{D} = A (\frac{1}{D})$
47	46	ad4ant14	$⊢ (((A \in ℝ \land B \in ℝ) \land (0 \leq A \land A \leq B)) \land ((C \in ℝ \land D \in ℝ) \land (0 < C \land C \leq D))) \to \frac{A}{D} = A (\frac{1}{D})$
48		recn	$⊢ B \in ℝ \to B \in ℂ$
49	48	adantr	$⊢ (B \in ℝ \land (C \in ℝ \land 0 < C)) \to B \in ℂ$
50		recn	$⊢ C \in ℝ \to C \in ℂ$
51	50	ad2antrl	$⊢ (B \in ℝ \land (C \in ℝ \land 0 < C)) \to C \in ℂ$
52	8	adantl	$⊢ (B \in ℝ \land (C \in ℝ \land 0 < C)) \to C \neq 0$
53	49 51 52	divrecd	$⊢ (B \in ℝ \land (C \in ℝ \land 0 < C)) \to \frac{B}{C} = B (\frac{1}{C})$
54	53	adantrrr	$⊢ (B \in ℝ \land (C \in ℝ \land (0 < C \land C \leq D))) \to \frac{B}{C} = B (\frac{1}{C})$
55	54	adantrlr	$⊢ (B \in ℝ \land ((C \in ℝ \land D \in ℝ) \land (0 < C \land C \leq D))) \to \frac{B}{C} = B (\frac{1}{C})$
56	55	ad4ant24	$⊢ (((A \in ℝ \land B \in ℝ) \land (0 \leq A \land A \leq B)) \land ((C \in ℝ \land D \in ℝ) \land (0 < C \land C \leq D))) \to \frac{B}{C} = B (\frac{1}{C})$
57	39 47 56	3brtr4d	$⊢ (((A \in ℝ \land B \in ℝ) \land (0 \leq A \land A \leq B)) \land ((C \in ℝ \land D \in ℝ) \land (0 < C \land C \leq D))) \to \frac{A}{D} \leq \frac{B}{C}$

Metamath Proof Explorer

Theorem lediv12a

Proof