This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ) )