This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ) ) )