Metamath Proof Explorer

Theorem xmulge0

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

Ref Expression
Assertion xmulge0 
|- ( ( ( A e. RR* /\ 0 <_ A ) /\ ( B e. RR* /\ 0 <_ B ) ) -> 0 <_ ( A *e B ) )

Proof

Step Hyp Ref Expression
1 xmulgt0 
 |-  ( ( ( A e. RR* /\ 0 < A ) /\ ( B e. RR* /\ 0 < B ) ) -> 0 < ( A *e B ) )
2 1 an4s 
 |-  ( ( ( A e. RR* /\ B e. RR* ) /\ ( 0 < A /\ 0 < B ) ) -> 0 < ( A *e B ) )
3 0xr 
 |-  0 e. RR*
4 xmulcl 
 |-  ( ( A e. RR* /\ B e. RR* ) -> ( A *e B ) e. RR* )
5 4 adantr 
 |-  ( ( ( A e. RR* /\ B e. RR* ) /\ ( 0 < A /\ 0 < B ) ) -> ( A *e B ) e. RR* )
6 xrltle 
 |-  ( ( 0 e. RR* /\ ( A *e B ) e. RR* ) -> ( 0 < ( A *e B ) -> 0 <_ ( A *e B ) ) )
7 3 5 6 sylancr 
 |-  ( ( ( A e. RR* /\ B e. RR* ) /\ ( 0 < A /\ 0 < B ) ) -> ( 0 < ( A *e B ) -> 0 <_ ( A *e B ) ) )
8 2 7 mpd 
 |-  ( ( ( A e. RR* /\ B e. RR* ) /\ ( 0 < A /\ 0 < B ) ) -> 0 <_ ( A *e B ) )
9 8 ex 
 |-  ( ( A e. RR* /\ B e. RR* ) -> ( ( 0 < A /\ 0 < B ) -> 0 <_ ( A *e B ) ) )
10 9 ad2ant2r 
 |-  ( ( ( A e. RR* /\ 0 <_ A ) /\ ( B e. RR* /\ 0 <_ B ) ) -> ( ( 0 < A /\ 0 < B ) -> 0 <_ ( A *e B ) ) )
11 10 impl 
 |-  ( ( ( ( ( A e. RR* /\ 0 <_ A ) /\ ( B e. RR* /\ 0 <_ B ) ) /\ 0 < A ) /\ 0 < B ) -> 0 <_ ( A *e B ) )
12 0le0 
 |-  0 <_ 0
13 oveq2 
 |-  ( 0 = B -> ( A *e 0 ) = ( A *e B ) )
14 13 eqcomd 
 |-  ( 0 = B -> ( A *e B ) = ( A *e 0 ) )
15 xmul01 
 |-  ( A e. RR* -> ( A *e 0 ) = 0 )
16 15 ad2antrr 
 |-  ( ( ( A e. RR* /\ 0 <_ A ) /\ ( B e. RR* /\ 0 <_ B ) ) -> ( A *e 0 ) = 0 )
17 14 16 sylan9eqr 
 |-  ( ( ( ( A e. RR* /\ 0 <_ A ) /\ ( B e. RR* /\ 0 <_ B ) ) /\ 0 = B ) -> ( A *e B ) = 0 )
18 12 17 breqtrrid 
 |-  ( ( ( ( A e. RR* /\ 0 <_ A ) /\ ( B e. RR* /\ 0 <_ B ) ) /\ 0 = B ) -> 0 <_ ( A *e B ) )
19 18 adantlr 
 |-  ( ( ( ( ( A e. RR* /\ 0 <_ A ) /\ ( B e. RR* /\ 0 <_ B ) ) /\ 0 < A ) /\ 0 = B ) -> 0 <_ ( A *e B ) )
20 xrleloe 
 |-  ( ( 0 e. RR* /\ B e. RR* ) -> ( 0 <_ B <-> ( 0 < B \/ 0 = B ) ) )
21 3 20 mpan 
 |-  ( B e. RR* -> ( 0 <_ B <-> ( 0 < B \/ 0 = B ) ) )
22 21 biimpa 
 |-  ( ( B e. RR* /\ 0 <_ B ) -> ( 0 < B \/ 0 = B ) )
23 22 ad2antlr 
 |-  ( ( ( ( A e. RR* /\ 0 <_ A ) /\ ( B e. RR* /\ 0 <_ B ) ) /\ 0 < A ) -> ( 0 < B \/ 0 = B ) )
24 11 19 23 mpjaodan 
 |-  ( ( ( ( A e. RR* /\ 0 <_ A ) /\ ( B e. RR* /\ 0 <_ B ) ) /\ 0 < A ) -> 0 <_ ( A *e B ) )
25 oveq1 
 |-  ( 0 = A -> ( 0 *e B ) = ( A *e B ) )
26 25 eqcomd 
 |-  ( 0 = A -> ( A *e B ) = ( 0 *e B ) )
27 xmul02 
 |-  ( B e. RR* -> ( 0 *e B ) = 0 )
28 27 ad2antrl 
 |-  ( ( ( A e. RR* /\ 0 <_ A ) /\ ( B e. RR* /\ 0 <_ B ) ) -> ( 0 *e B ) = 0 )
29 26 28 sylan9eqr 
 |-  ( ( ( ( A e. RR* /\ 0 <_ A ) /\ ( B e. RR* /\ 0 <_ B ) ) /\ 0 = A ) -> ( A *e B ) = 0 )
30 12 29 breqtrrid 
 |-  ( ( ( ( A e. RR* /\ 0 <_ A ) /\ ( B e. RR* /\ 0 <_ B ) ) /\ 0 = A ) -> 0 <_ ( A *e B ) )
31 xrleloe 
 |-  ( ( 0 e. RR* /\ A e. RR* ) -> ( 0 <_ A <-> ( 0 < A \/ 0 = A ) ) )
32 3 31 mpan 
 |-  ( A e. RR* -> ( 0 <_ A <-> ( 0 < A \/ 0 = A ) ) )
33 32 biimpa 
 |-  ( ( A e. RR* /\ 0 <_ A ) -> ( 0 < A \/ 0 = A ) )
34 33 adantr 
 |-  ( ( ( A e. RR* /\ 0 <_ A ) /\ ( B e. RR* /\ 0 <_ B ) ) -> ( 0 < A \/ 0 = A ) )
35 24 30 34 mpjaodan 
 |-  ( ( ( A e. RR* /\ 0 <_ A ) /\ ( B e. RR* /\ 0 <_ B ) ) -> 0 <_ ( A *e B ) )