Metamath Proof Explorer


Theorem mulgt0ii

Description: The product of two positive numbers is positive. (Contributed by NM, 18-May-1999)

Ref Expression
Hypotheses lt.1
|- A e. RR
lt.2
|- B e. RR
mulgt0i.3
|- 0 < A
mulgt0i.4
|- 0 < B
Assertion mulgt0ii
|- 0 < ( A x. B )

Proof

Step Hyp Ref Expression
1 lt.1
 |-  A e. RR
2 lt.2
 |-  B e. RR
3 mulgt0i.3
 |-  0 < A
4 mulgt0i.4
 |-  0 < B
5 1 2 mulgt0i
 |-  ( ( 0 < A /\ 0 < B ) -> 0 < ( A x. B ) )
6 3 4 5 mp2an
 |-  0 < ( A x. B )