Metamath Proof Explorer


Theorem mulgt0

Description: The product of two positive numbers is positive. (Contributed by NM, 10-Mar-2008)

Ref Expression
Assertion mulgt0 A 0 < A B 0 < B 0 < A B

Proof

Step Hyp Ref Expression
1 axmulgt0 A B 0 < A 0 < B 0 < A B
2 1 imp A B 0 < A 0 < B 0 < A B
3 2 an4s A 0 < A B 0 < B 0 < A B