Metamath Proof Explorer

Theorem prodgt02

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

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

Proof

Step Hyp Ref Expression
1 recn 
 |-  ( A e. RR -> A e. CC )
2 recn 
 |-  ( B e. RR -> B e. CC )
3 mulcom 
 |-  ( ( A e. CC /\ B e. CC ) -> ( A x. B ) = ( B x. A ) )
4 1 2 3 syl2an 
 |-  ( ( A e. RR /\ B e. RR ) -> ( A x. B ) = ( B x. A ) )
5 4 breq2d 
 |-  ( ( A e. RR /\ B e. RR ) -> ( 0 < ( A x. B ) <-> 0 < ( B x. A ) ) )
6 5 biimpd 
 |-  ( ( A e. RR /\ B e. RR ) -> ( 0 < ( A x. B ) -> 0 < ( B x. A ) ) )
7 prodgt0 
 |-  ( ( ( B e. RR /\ A e. RR ) /\ ( 0 <_ B /\ 0 < ( B x. A ) ) ) -> 0 < A )
8 7 ex 
 |-  ( ( B e. RR /\ A e. RR ) -> ( ( 0 <_ B /\ 0 < ( B x. A ) ) -> 0 < A ) )
9 8 ancoms 
 |-  ( ( A e. RR /\ B e. RR ) -> ( ( 0 <_ B /\ 0 < ( B x. A ) ) -> 0 < A ) )
10 6 9 sylan2d 
 |-  ( ( A e. RR /\ B e. RR ) -> ( ( 0 <_ B /\ 0 < ( A x. B ) ) -> 0 < A ) )
11 10 imp 
 |-  ( ( ( A e. RR /\ B e. RR ) /\ ( 0 <_ B /\ 0 < ( A x. B ) ) ) -> 0 < A )