Metamath Proof Explorer

Theorem xlemul1

Description: Extended real version of lemul1 . (Contributed by Mario Carneiro, 20-Aug-2015)

Ref Expression
Assertion xlemul1 
|- ( ( A e. RR* /\ B e. RR* /\ C e. RR+ ) -> ( A <_ B <-> ( A *e C ) <_ ( B *e C ) ) )

Proof

Step Hyp Ref Expression
1 rpxr 
 |-  ( C e. RR+ -> C e. RR* )
2 rpge0 
 |-  ( C e. RR+ -> 0 <_ C )
3 1 2 jca 
 |-  ( C e. RR+ -> ( C e. RR* /\ 0 <_ C ) )
4 xlemul1a 
 |-  ( ( ( A e. RR* /\ B e. RR* /\ ( C e. RR* /\ 0 <_ C ) ) /\ A <_ B ) -> ( A *e C ) <_ ( B *e C ) )
5 4 ex 
 |-  ( ( A e. RR* /\ B e. RR* /\ ( C e. RR* /\ 0 <_ C ) ) -> ( A <_ B -> ( A *e C ) <_ ( B *e C ) ) )
6 3 5 syl3an3 
 |-  ( ( A e. RR* /\ B e. RR* /\ C e. RR+ ) -> ( A <_ B -> ( A *e C ) <_ ( B *e C ) ) )
7 simp1 
 |-  ( ( A e. RR* /\ B e. RR* /\ C e. RR+ ) -> A e. RR* )
8 1 3ad2ant3 
 |-  ( ( A e. RR* /\ B e. RR* /\ C e. RR+ ) -> C e. RR* )
9 xmulcl 
 |-  ( ( A e. RR* /\ C e. RR* ) -> ( A *e C ) e. RR* )
10 7 8 9 syl2anc 
 |-  ( ( A e. RR* /\ B e. RR* /\ C e. RR+ ) -> ( A *e C ) e. RR* )
11 simp2 
 |-  ( ( A e. RR* /\ B e. RR* /\ C e. RR+ ) -> B e. RR* )
12 xmulcl 
 |-  ( ( B e. RR* /\ C e. RR* ) -> ( B *e C ) e. RR* )
13 11 8 12 syl2anc 
 |-  ( ( A e. RR* /\ B e. RR* /\ C e. RR+ ) -> ( B *e C ) e. RR* )
14 rpreccl 
 |-  ( C e. RR+ -> ( 1 / C ) e. RR+ )
15 14 3ad2ant3 
 |-  ( ( A e. RR* /\ B e. RR* /\ C e. RR+ ) -> ( 1 / C ) e. RR+ )
16 rpxr 
 |-  ( ( 1 / C ) e. RR+ -> ( 1 / C ) e. RR* )
17 15 16 syl 
 |-  ( ( A e. RR* /\ B e. RR* /\ C e. RR+ ) -> ( 1 / C ) e. RR* )
18 rpge0 
 |-  ( ( 1 / C ) e. RR+ -> 0 <_ ( 1 / C ) )
19 15 18 syl 
 |-  ( ( A e. RR* /\ B e. RR* /\ C e. RR+ ) -> 0 <_ ( 1 / C ) )
20 xlemul1a 
 |-  ( ( ( ( A *e C ) e. RR* /\ ( B *e C ) e. RR* /\ ( ( 1 / C ) e. RR* /\ 0 <_ ( 1 / C ) ) ) /\ ( A *e C ) <_ ( B *e C ) ) -> ( ( A *e C ) *e ( 1 / C ) ) <_ ( ( B *e C ) *e ( 1 / C ) ) )
21 20 ex 
 |-  ( ( ( A *e C ) e. RR* /\ ( B *e C ) e. RR* /\ ( ( 1 / C ) e. RR* /\ 0 <_ ( 1 / C ) ) ) -> ( ( A *e C ) <_ ( B *e C ) -> ( ( A *e C ) *e ( 1 / C ) ) <_ ( ( B *e C ) *e ( 1 / C ) ) ) )
22 10 13 17 19 21 syl112anc 
 |-  ( ( A e. RR* /\ B e. RR* /\ C e. RR+ ) -> ( ( A *e C ) <_ ( B *e C ) -> ( ( A *e C ) *e ( 1 / C ) ) <_ ( ( B *e C ) *e ( 1 / C ) ) ) )
23 xmulass 
 |-  ( ( A e. RR* /\ C e. RR* /\ ( 1 / C ) e. RR* ) -> ( ( A *e C ) *e ( 1 / C ) ) = ( A *e ( C *e ( 1 / C ) ) ) )
24 7 8 17 23 syl3anc 
 |-  ( ( A e. RR* /\ B e. RR* /\ C e. RR+ ) -> ( ( A *e C ) *e ( 1 / C ) ) = ( A *e ( C *e ( 1 / C ) ) ) )
25 rpre 
 |-  ( C e. RR+ -> C e. RR )
26 25 3ad2ant3 
 |-  ( ( A e. RR* /\ B e. RR* /\ C e. RR+ ) -> C e. RR )
27 15 rpred 
 |-  ( ( A e. RR* /\ B e. RR* /\ C e. RR+ ) -> ( 1 / C ) e. RR )
28 rexmul 
 |-  ( ( C e. RR /\ ( 1 / C ) e. RR ) -> ( C *e ( 1 / C ) ) = ( C x. ( 1 / C ) ) )
29 26 27 28 syl2anc 
 |-  ( ( A e. RR* /\ B e. RR* /\ C e. RR+ ) -> ( C *e ( 1 / C ) ) = ( C x. ( 1 / C ) ) )
30 26 recnd 
 |-  ( ( A e. RR* /\ B e. RR* /\ C e. RR+ ) -> C e. CC )
31 rpne0 
 |-  ( C e. RR+ -> C =/= 0 )
32 31 3ad2ant3 
 |-  ( ( A e. RR* /\ B e. RR* /\ C e. RR+ ) -> C =/= 0 )
33 30 32 recidd 
 |-  ( ( A e. RR* /\ B e. RR* /\ C e. RR+ ) -> ( C x. ( 1 / C ) ) = 1 )
34 29 33 eqtrd 
 |-  ( ( A e. RR* /\ B e. RR* /\ C e. RR+ ) -> ( C *e ( 1 / C ) ) = 1 )
35 34 oveq2d 
 |-  ( ( A e. RR* /\ B e. RR* /\ C e. RR+ ) -> ( A *e ( C *e ( 1 / C ) ) ) = ( A *e 1 ) )
36 xmulid1 
 |-  ( A e. RR* -> ( A *e 1 ) = A )
37 7 36 syl 
 |-  ( ( A e. RR* /\ B e. RR* /\ C e. RR+ ) -> ( A *e 1 ) = A )
38 24 35 37 3eqtrd 
 |-  ( ( A e. RR* /\ B e. RR* /\ C e. RR+ ) -> ( ( A *e C ) *e ( 1 / C ) ) = A )
39 xmulass 
 |-  ( ( B e. RR* /\ C e. RR* /\ ( 1 / C ) e. RR* ) -> ( ( B *e C ) *e ( 1 / C ) ) = ( B *e ( C *e ( 1 / C ) ) ) )
40 11 8 17 39 syl3anc 
 |-  ( ( A e. RR* /\ B e. RR* /\ C e. RR+ ) -> ( ( B *e C ) *e ( 1 / C ) ) = ( B *e ( C *e ( 1 / C ) ) ) )
41 34 oveq2d 
 |-  ( ( A e. RR* /\ B e. RR* /\ C e. RR+ ) -> ( B *e ( C *e ( 1 / C ) ) ) = ( B *e 1 ) )
42 xmulid1 
 |-  ( B e. RR* -> ( B *e 1 ) = B )
43 11 42 syl 
 |-  ( ( A e. RR* /\ B e. RR* /\ C e. RR+ ) -> ( B *e 1 ) = B )
44 40 41 43 3eqtrd 
 |-  ( ( A e. RR* /\ B e. RR* /\ C e. RR+ ) -> ( ( B *e C ) *e ( 1 / C ) ) = B )
45 38 44 breq12d 
 |-  ( ( A e. RR* /\ B e. RR* /\ C e. RR+ ) -> ( ( ( A *e C ) *e ( 1 / C ) ) <_ ( ( B *e C ) *e ( 1 / C ) ) <-> A <_ B ) )
46 22 45 sylibd 
 |-  ( ( A e. RR* /\ B e. RR* /\ C e. RR+ ) -> ( ( A *e C ) <_ ( B *e C ) -> A <_ B ) )
47 6 46 impbid 
 |-  ( ( A e. RR* /\ B e. RR* /\ C e. RR+ ) -> ( A <_ B <-> ( A *e C ) <_ ( B *e C ) ) )