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 )