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 )