Metamath Proof Explorer


Theorem ltmul12a

Description: Comparison of product of two positive numbers. (Contributed by NM, 30-Dec-2005)

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

Proof

Step Hyp Ref Expression
1 simplll
 |-  ( ( ( ( A e. RR /\ B e. RR ) /\ ( C e. RR /\ D e. RR ) ) /\ ( ( 0 <_ A /\ A < B ) /\ ( 0 <_ C /\ C < D ) ) ) -> A e. RR )
2 simpllr
 |-  ( ( ( ( A e. RR /\ B e. RR ) /\ ( C e. RR /\ D e. RR ) ) /\ ( ( 0 <_ A /\ A < B ) /\ ( 0 <_ C /\ C < D ) ) ) -> B e. RR )
3 simpll
 |-  ( ( ( C e. RR /\ D e. RR ) /\ ( 0 <_ C /\ C < D ) ) -> C e. RR )
4 simprl
 |-  ( ( ( C e. RR /\ D e. RR ) /\ ( 0 <_ C /\ C < D ) ) -> 0 <_ C )
5 3 4 jca
 |-  ( ( ( C e. RR /\ D e. RR ) /\ ( 0 <_ C /\ C < D ) ) -> ( C e. RR /\ 0 <_ C ) )
6 5 ad2ant2l
 |-  ( ( ( ( A e. RR /\ B e. RR ) /\ ( C e. RR /\ D e. RR ) ) /\ ( ( 0 <_ A /\ A < B ) /\ ( 0 <_ C /\ C < D ) ) ) -> ( C e. RR /\ 0 <_ C ) )
7 ltle
 |-  ( ( A e. RR /\ B e. RR ) -> ( A < B -> A <_ B ) )
8 7 imp
 |-  ( ( ( A e. RR /\ B e. RR ) /\ A < B ) -> A <_ B )
9 8 adantrl
 |-  ( ( ( A e. RR /\ B e. RR ) /\ ( 0 <_ A /\ A < B ) ) -> A <_ B )
10 9 ad2ant2r
 |-  ( ( ( ( A e. RR /\ B e. RR ) /\ ( C e. RR /\ D e. RR ) ) /\ ( ( 0 <_ A /\ A < B ) /\ ( 0 <_ C /\ C < D ) ) ) -> A <_ B )
11 lemul1a
 |-  ( ( ( A e. RR /\ B e. RR /\ ( C e. RR /\ 0 <_ C ) ) /\ A <_ B ) -> ( A x. C ) <_ ( B x. C ) )
12 1 2 6 10 11 syl31anc
 |-  ( ( ( ( A e. RR /\ B e. RR ) /\ ( C e. RR /\ D e. RR ) ) /\ ( ( 0 <_ A /\ A < B ) /\ ( 0 <_ C /\ C < D ) ) ) -> ( A x. C ) <_ ( B x. C ) )
13 simplrl
 |-  ( ( ( ( A e. RR /\ B e. RR ) /\ ( C e. RR /\ D e. RR ) ) /\ ( 0 <_ A /\ A < B ) ) -> C e. RR )
14 simplrr
 |-  ( ( ( ( A e. RR /\ B e. RR ) /\ ( C e. RR /\ D e. RR ) ) /\ ( 0 <_ A /\ A < B ) ) -> D e. RR )
15 simpllr
 |-  ( ( ( ( A e. RR /\ B e. RR ) /\ ( C e. RR /\ D e. RR ) ) /\ ( 0 <_ A /\ A < B ) ) -> B e. RR )
16 0re
 |-  0 e. RR
17 lelttr
 |-  ( ( 0 e. RR /\ A e. RR /\ B e. RR ) -> ( ( 0 <_ A /\ A < B ) -> 0 < B ) )
18 16 17 mp3an1
 |-  ( ( A e. RR /\ B e. RR ) -> ( ( 0 <_ A /\ A < B ) -> 0 < B ) )
19 18 imp
 |-  ( ( ( A e. RR /\ B e. RR ) /\ ( 0 <_ A /\ A < B ) ) -> 0 < B )
20 19 adantlr
 |-  ( ( ( ( A e. RR /\ B e. RR ) /\ ( C e. RR /\ D e. RR ) ) /\ ( 0 <_ A /\ A < B ) ) -> 0 < B )
21 ltmul2
 |-  ( ( C e. RR /\ D e. RR /\ ( B e. RR /\ 0 < B ) ) -> ( C < D <-> ( B x. C ) < ( B x. D ) ) )
22 13 14 15 20 21 syl112anc
 |-  ( ( ( ( A e. RR /\ B e. RR ) /\ ( C e. RR /\ D e. RR ) ) /\ ( 0 <_ A /\ A < B ) ) -> ( C < D <-> ( B x. C ) < ( B x. D ) ) )
23 22 biimpa
 |-  ( ( ( ( ( A e. RR /\ B e. RR ) /\ ( C e. RR /\ D e. RR ) ) /\ ( 0 <_ A /\ A < B ) ) /\ C < D ) -> ( B x. C ) < ( B x. D ) )
24 23 anasss
 |-  ( ( ( ( A e. RR /\ B e. RR ) /\ ( C e. RR /\ D e. RR ) ) /\ ( ( 0 <_ A /\ A < B ) /\ C < D ) ) -> ( B x. C ) < ( B x. D ) )
25 24 adantrrl
 |-  ( ( ( ( A e. RR /\ B e. RR ) /\ ( C e. RR /\ D e. RR ) ) /\ ( ( 0 <_ A /\ A < B ) /\ ( 0 <_ C /\ C < D ) ) ) -> ( B x. C ) < ( B x. D ) )
26 remulcl
 |-  ( ( A e. RR /\ C e. RR ) -> ( A x. C ) e. RR )
27 26 ad2ant2r
 |-  ( ( ( A e. RR /\ B e. RR ) /\ ( C e. RR /\ D e. RR ) ) -> ( A x. C ) e. RR )
28 remulcl
 |-  ( ( B e. RR /\ C e. RR ) -> ( B x. C ) e. RR )
29 28 ad2ant2lr
 |-  ( ( ( A e. RR /\ B e. RR ) /\ ( C e. RR /\ D e. RR ) ) -> ( B x. C ) e. RR )
30 remulcl
 |-  ( ( B e. RR /\ D e. RR ) -> ( B x. D ) e. RR )
31 30 ad2ant2l
 |-  ( ( ( A e. RR /\ B e. RR ) /\ ( C e. RR /\ D e. RR ) ) -> ( B x. D ) e. RR )
32 lelttr
 |-  ( ( ( A x. C ) e. RR /\ ( B x. C ) e. RR /\ ( B x. D ) e. RR ) -> ( ( ( A x. C ) <_ ( B x. C ) /\ ( B x. C ) < ( B x. D ) ) -> ( A x. C ) < ( B x. D ) ) )
33 27 29 31 32 syl3anc
 |-  ( ( ( A e. RR /\ B e. RR ) /\ ( C e. RR /\ D e. RR ) ) -> ( ( ( A x. C ) <_ ( B x. C ) /\ ( B x. C ) < ( B x. D ) ) -> ( A x. C ) < ( B x. D ) ) )
34 33 adantr
 |-  ( ( ( ( A e. RR /\ B e. RR ) /\ ( C e. RR /\ D e. RR ) ) /\ ( ( 0 <_ A /\ A < B ) /\ ( 0 <_ C /\ C < D ) ) ) -> ( ( ( A x. C ) <_ ( B x. C ) /\ ( B x. C ) < ( B x. D ) ) -> ( A x. C ) < ( B x. D ) ) )
35 12 25 34 mp2and
 |-  ( ( ( ( A e. RR /\ B e. RR ) /\ ( C e. RR /\ D e. RR ) ) /\ ( ( 0 <_ A /\ A < B ) /\ ( 0 <_ C /\ C < D ) ) ) -> ( A x. C ) < ( B x. D ) )
36 35 an4s
 |-  ( ( ( ( A e. RR /\ B e. RR ) /\ ( 0 <_ A /\ A < B ) ) /\ ( ( C e. RR /\ D e. RR ) /\ ( 0 <_ C /\ C < D ) ) ) -> ( A x. C ) < ( B x. D ) )