Theorem lediv12a

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

	Ref	Expression
Assertion	lediv12a	|- ( ( ( ( A e. RR /\ B e. RR ) /\ ( 0 <_ A /\ A <_ B ) ) /\ ( ( C e. RR /\ D e. RR ) /\ ( 0 < C /\ C <_ D ) ) ) -> ( A / D ) <_ ( B / C ) )

Proof

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