Theorem axmulgt0

Description: The product of two positive reals is positive. Axiom 21 of 22 for real and complex numbers, derived from ZF set theory. (This restates ax-pre-mulgt0 with ordering on the extended reals.) (Contributed by NM, 13-Oct-2005)

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

Proof

Step	Hyp	Ref	Expression
1		ax-pre-mulgt0	|- ( ( A e. RR /\ B e. RR ) -> ( ( 0 0
2		0re	|- 0 e. RR
3		ltxrlt	|- ( ( 0 e. RR /\ A e. RR ) -> ( 0 < A <-> 0
4	2 3	mpan	|- ( A e. RR -> ( 0 < A <-> 0
5		ltxrlt	|- ( ( 0 e. RR /\ B e. RR ) -> ( 0 < B <-> 0
6	2 5	mpan	|- ( B e. RR -> ( 0 < B <-> 0
7	4 6	bi2anan9	|- ( ( A e. RR /\ B e. RR ) -> ( ( 0 < A /\ 0 < B ) <-> ( 0
8		remulcl	|- ( ( A e. RR /\ B e. RR ) -> ( A x. B ) e. RR )
9		ltxrlt	|- ( ( 0 e. RR /\ ( A x. B ) e. RR ) -> ( 0 < ( A x. B ) <-> 0
10	2 8 9	sylancr	|- ( ( A e. RR /\ B e. RR ) -> ( 0 < ( A x. B ) <-> 0
11	1 7 10	3imtr4d	|- ( ( A e. RR /\ B e. RR ) -> ( ( 0 < A /\ 0 < B ) -> 0 < ( A x. B ) ) )