Metamath Proof Explorer

Theorem prodgt0

Description: Infer that a multiplicand is positive from a nonnegative multiplier and positive product. (Contributed by NM, 24-Apr-2005) (Revised by Mario Carneiro, 27-May-2016)

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

Proof

Step Hyp Ref Expression
1 0red 
 |-  ( ( A e. RR /\ B e. RR ) -> 0 e. RR )
2 simpl 
 |-  ( ( A e. RR /\ B e. RR ) -> A e. RR )
3 1 2 leloed 
 |-  ( ( A e. RR /\ B e. RR ) -> ( 0 <_ A <-> ( 0 < A \/ 0 = A ) ) )
4 simpll 
 |-  ( ( ( A e. RR /\ B e. RR ) /\ ( 0 < A /\ 0 < ( A x. B ) ) ) -> A e. RR )
5 simplr 
 |-  ( ( ( A e. RR /\ B e. RR ) /\ ( 0 < A /\ 0 < ( A x. B ) ) ) -> B e. RR )
6 4 5 remulcld 
 |-  ( ( ( A e. RR /\ B e. RR ) /\ ( 0 < A /\ 0 < ( A x. B ) ) ) -> ( A x. B ) e. RR )
7 simprl 
 |-  ( ( ( A e. RR /\ B e. RR ) /\ ( 0 < A /\ 0 < ( A x. B ) ) ) -> 0 < A )
8 7 gt0ne0d 
 |-  ( ( ( A e. RR /\ B e. RR ) /\ ( 0 < A /\ 0 < ( A x. B ) ) ) -> A =/= 0 )
9 4 8 rereccld 
 |-  ( ( ( A e. RR /\ B e. RR ) /\ ( 0 < A /\ 0 < ( A x. B ) ) ) -> ( 1 / A ) e. RR )
10 simprr 
 |-  ( ( ( A e. RR /\ B e. RR ) /\ ( 0 < A /\ 0 < ( A x. B ) ) ) -> 0 < ( A x. B ) )
11 recgt0 
 |-  ( ( A e. RR /\ 0 < A ) -> 0 < ( 1 / A ) )
12 11 ad2ant2r 
 |-  ( ( ( A e. RR /\ B e. RR ) /\ ( 0 < A /\ 0 < ( A x. B ) ) ) -> 0 < ( 1 / A ) )
13 6 9 10 12 mulgt0d 
 |-  ( ( ( A e. RR /\ B e. RR ) /\ ( 0 < A /\ 0 < ( A x. B ) ) ) -> 0 < ( ( A x. B ) x. ( 1 / A ) ) )
14 6 recnd 
 |-  ( ( ( A e. RR /\ B e. RR ) /\ ( 0 < A /\ 0 < ( A x. B ) ) ) -> ( A x. B ) e. CC )
15 4 recnd 
 |-  ( ( ( A e. RR /\ B e. RR ) /\ ( 0 < A /\ 0 < ( A x. B ) ) ) -> A e. CC )
16 14 15 8 divrecd 
 |-  ( ( ( A e. RR /\ B e. RR ) /\ ( 0 < A /\ 0 < ( A x. B ) ) ) -> ( ( A x. B ) / A ) = ( ( A x. B ) x. ( 1 / A ) ) )
17 simpr 
 |-  ( ( A e. RR /\ B e. RR ) -> B e. RR )
18 17 recnd 
 |-  ( ( A e. RR /\ B e. RR ) -> B e. CC )
19 18 adantr 
 |-  ( ( ( A e. RR /\ B e. RR ) /\ ( 0 < A /\ 0 < ( A x. B ) ) ) -> B e. CC )
20 19 15 8 divcan3d 
 |-  ( ( ( A e. RR /\ B e. RR ) /\ ( 0 < A /\ 0 < ( A x. B ) ) ) -> ( ( A x. B ) / A ) = B )
21 16 20 eqtr3d 
 |-  ( ( ( A e. RR /\ B e. RR ) /\ ( 0 < A /\ 0 < ( A x. B ) ) ) -> ( ( A x. B ) x. ( 1 / A ) ) = B )
22 13 21 breqtrd 
 |-  ( ( ( A e. RR /\ B e. RR ) /\ ( 0 < A /\ 0 < ( A x. B ) ) ) -> 0 < B )
23 22 exp32 
 |-  ( ( A e. RR /\ B e. RR ) -> ( 0 < A -> ( 0 < ( A x. B ) -> 0 < B ) ) )
24 0re 
 |-  0 e. RR
25 24 ltnri 
 |-  -. 0 < 0
26 18 mul02d 
 |-  ( ( A e. RR /\ B e. RR ) -> ( 0 x. B ) = 0 )
27 26 breq2d 
 |-  ( ( A e. RR /\ B e. RR ) -> ( 0 < ( 0 x. B ) <-> 0 < 0 ) )
28 25 27 mtbiri 
 |-  ( ( A e. RR /\ B e. RR ) -> -. 0 < ( 0 x. B ) )
29 28 pm2.21d 
 |-  ( ( A e. RR /\ B e. RR ) -> ( 0 < ( 0 x. B ) -> 0 < B ) )
30 oveq1 
 |-  ( 0 = A -> ( 0 x. B ) = ( A x. B ) )
31 30 breq2d 
 |-  ( 0 = A -> ( 0 < ( 0 x. B ) <-> 0 < ( A x. B ) ) )
32 31 imbi1d 
 |-  ( 0 = A -> ( ( 0 < ( 0 x. B ) -> 0 < B ) <-> ( 0 < ( A x. B ) -> 0 < B ) ) )
33 29 32 syl5ibcom 
 |-  ( ( A e. RR /\ B e. RR ) -> ( 0 = A -> ( 0 < ( A x. B ) -> 0 < B ) ) )
34 23 33 jaod 
 |-  ( ( A e. RR /\ B e. RR ) -> ( ( 0 < A \/ 0 = A ) -> ( 0 < ( A x. B ) -> 0 < B ) ) )
35 3 34 sylbid 
 |-  ( ( A e. RR /\ B e. RR ) -> ( 0 <_ A -> ( 0 < ( A x. B ) -> 0 < B ) ) )
36 35 imp32 
 |-  ( ( ( A e. RR /\ B e. RR ) /\ ( 0 <_ A /\ 0 < ( A x. B ) ) ) -> 0 < B )