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 e. RR /\ 0 < A ) /\ ( B e. RR /\ 0 < B ) ) -> 0 < ( A x. B ) )

Step	Hyp	Ref	Expression
1		axmulgt0	\|- ( ( A e. RR /\ B e. RR ) -> ( ( 0 < A /\ 0 < B ) -> 0 < ( A x. B ) ) )
2	1	imp	\|- ( ( ( A e. RR /\ B e. RR ) /\ ( 0 < A /\ 0 < B ) ) -> 0 < ( A x. B ) )
3	2	an4s	\|- ( ( ( A e. RR /\ 0 < A ) /\ ( B e. RR /\ 0 < B ) ) -> 0 < ( A x. B ) )

Step

Hyp

Ref

Expression

 |-  ( ( A e. RR /\ B e. RR ) -> ( ( 0 < A /\ 0 < B ) -> 0 < ( A x. B ) ) )

 |-  ( ( ( A e. RR /\ B e. RR ) /\ ( 0 < A /\ 0 < B ) ) -> 0 < ( A x. B ) )

 |-  ( ( ( A e. RR /\ 0 < A ) /\ ( B e. RR /\ 0 < B ) ) -> 0 < ( A x. B ) )