Metamath Proof Explorer

Theorem xmulgt0

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

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

Proof

Step Hyp Ref Expression
1 simpr 
 |-  ( ( A e. RR* /\ 0 < A ) -> 0 < A )
2 simpr 
 |-  ( ( B e. RR* /\ 0 < B ) -> 0 < B )
3 1 2 anim12i 
 |-  ( ( ( A e. RR* /\ 0 < A ) /\ ( B e. RR* /\ 0 < B ) ) -> ( 0 < A /\ 0 < B ) )
4 mulgt0 
 |-  ( ( ( A e. RR /\ 0 < A ) /\ ( B e. RR /\ 0 < B ) ) -> 0 < ( A x. B ) )
5 4 an4s 
 |-  ( ( ( A e. RR /\ B e. RR ) /\ ( 0 < A /\ 0 < B ) ) -> 0 < ( A x. B ) )
6 5 ancoms 
 |-  ( ( ( 0 < A /\ 0 < B ) /\ ( A e. RR /\ B e. RR ) ) -> 0 < ( A x. B ) )
7 rexmul 
 |-  ( ( A e. RR /\ B e. RR ) -> ( A *e B ) = ( A x. B ) )
8 7 adantl 
 |-  ( ( ( 0 < A /\ 0 < B ) /\ ( A e. RR /\ B e. RR ) ) -> ( A *e B ) = ( A x. B ) )
9 6 8 breqtrrd 
 |-  ( ( ( 0 < A /\ 0 < B ) /\ ( A e. RR /\ B e. RR ) ) -> 0 < ( A *e B ) )
10 3 9 sylan 
 |-  ( ( ( ( A e. RR* /\ 0 < A ) /\ ( B e. RR* /\ 0 < B ) ) /\ ( A e. RR /\ B e. RR ) ) -> 0 < ( A *e B ) )
11 10 anassrs 
 |-  ( ( ( ( ( A e. RR* /\ 0 < A ) /\ ( B e. RR* /\ 0 < B ) ) /\ A e. RR ) /\ B e. RR ) -> 0 < ( A *e B ) )
12 0ltpnf 
 |-  0 < +oo
13 oveq2 
 |-  ( B = +oo -> ( A *e B ) = ( A *e +oo ) )
14 xmulpnf1 
 |-  ( ( A e. RR* /\ 0 < A ) -> ( A *e +oo ) = +oo )
15 14 adantr 
 |-  ( ( ( A e. RR* /\ 0 < A ) /\ ( B e. RR* /\ 0 < B ) ) -> ( A *e +oo ) = +oo )
16 13 15 sylan9eqr 
 |-  ( ( ( ( A e. RR* /\ 0 < A ) /\ ( B e. RR* /\ 0 < B ) ) /\ B = +oo ) -> ( A *e B ) = +oo )
17 12 16 breqtrrid 
 |-  ( ( ( ( A e. RR* /\ 0 < A ) /\ ( B e. RR* /\ 0 < B ) ) /\ B = +oo ) -> 0 < ( A *e B ) )
18 17 adantlr 
 |-  ( ( ( ( ( A e. RR* /\ 0 < A ) /\ ( B e. RR* /\ 0 < B ) ) /\ A e. RR ) /\ B = +oo ) -> 0 < ( A *e B ) )
19 simplrr 
 |-  ( ( ( ( A e. RR* /\ 0 < A ) /\ ( B e. RR* /\ 0 < B ) ) /\ A e. RR ) -> 0 < B )
20 xmulasslem2 
 |-  ( ( 0 < B /\ B = -oo ) -> 0 < ( A *e B ) )
21 19 20 sylan 
 |-  ( ( ( ( ( A e. RR* /\ 0 < A ) /\ ( B e. RR* /\ 0 < B ) ) /\ A e. RR ) /\ B = -oo ) -> 0 < ( A *e B ) )
22 simprl 
 |-  ( ( ( A e. RR* /\ 0 < A ) /\ ( B e. RR* /\ 0 < B ) ) -> B e. RR* )
23 elxr 
 |-  ( B e. RR* <-> ( B e. RR \/ B = +oo \/ B = -oo ) )
24 22 23 sylib 
 |-  ( ( ( A e. RR* /\ 0 < A ) /\ ( B e. RR* /\ 0 < B ) ) -> ( B e. RR \/ B = +oo \/ B = -oo ) )
25 24 adantr 
 |-  ( ( ( ( A e. RR* /\ 0 < A ) /\ ( B e. RR* /\ 0 < B ) ) /\ A e. RR ) -> ( B e. RR \/ B = +oo \/ B = -oo ) )
26 11 18 21 25 mpjao3dan 
 |-  ( ( ( ( A e. RR* /\ 0 < A ) /\ ( B e. RR* /\ 0 < B ) ) /\ A e. RR ) -> 0 < ( A *e B ) )
27 oveq1 
 |-  ( A = +oo -> ( A *e B ) = ( +oo *e B ) )
28 xmulpnf2 
 |-  ( ( B e. RR* /\ 0 < B ) -> ( +oo *e B ) = +oo )
29 28 adantl 
 |-  ( ( ( A e. RR* /\ 0 < A ) /\ ( B e. RR* /\ 0 < B ) ) -> ( +oo *e B ) = +oo )
30 27 29 sylan9eqr 
 |-  ( ( ( ( A e. RR* /\ 0 < A ) /\ ( B e. RR* /\ 0 < B ) ) /\ A = +oo ) -> ( A *e B ) = +oo )
31 12 30 breqtrrid 
 |-  ( ( ( ( A e. RR* /\ 0 < A ) /\ ( B e. RR* /\ 0 < B ) ) /\ A = +oo ) -> 0 < ( A *e B ) )
32 xmulasslem2 
 |-  ( ( 0 < A /\ A = -oo ) -> 0 < ( A *e B ) )
33 32 ad4ant24 
 |-  ( ( ( ( A e. RR* /\ 0 < A ) /\ ( B e. RR* /\ 0 < B ) ) /\ A = -oo ) -> 0 < ( A *e B ) )
34 simpll 
 |-  ( ( ( A e. RR* /\ 0 < A ) /\ ( B e. RR* /\ 0 < B ) ) -> A e. RR* )
35 elxr 
 |-  ( A e. RR* <-> ( A e. RR \/ A = +oo \/ A = -oo ) )
36 34 35 sylib 
 |-  ( ( ( A e. RR* /\ 0 < A ) /\ ( B e. RR* /\ 0 < B ) ) -> ( A e. RR \/ A = +oo \/ A = -oo ) )
37 26 31 33 36 mpjao3dan 
 |-  ( ( ( A e. RR* /\ 0 < A ) /\ ( B e. RR* /\ 0 < B ) ) -> 0 < ( A *e B ) )