Metamath Proof Explorer


Axiom ax-pre-mulgt0

Description: The product of two positive reals is positive. Axiom 21 of 22 for real and complex numbers, justified by Theorem axpre-mulgt0 . Normally new proofs would use axmulgt0 . (New usage is discouraged.) (Contributed by NM, 13-Oct-2005)

Ref Expression
Assertion ax-pre-mulgt0
|- ( ( A e. RR /\ B e. RR ) -> ( ( 0  0 

Detailed syntax breakdown

Step Hyp Ref Expression
0 cA
 |-  A
1 cr
 |-  RR
2 0 1 wcel
 |-  A e. RR
3 cB
 |-  B
4 3 1 wcel
 |-  B e. RR
5 2 4 wa
 |-  ( A e. RR /\ B e. RR )
6 cc0
 |-  0
7 cltrr
 |-  
8 6 0 7 wbr
 |-  0 
9 6 3 7 wbr
 |-  0 
10 8 9 wa
 |-  ( 0 
11 cmul
 |-  x.
12 0 3 11 co
 |-  ( A x. B )
13 6 12 7 wbr
 |-  0 
14 10 13 wi
 |-  ( ( 0  0 
15 5 14 wi
 |-  ( ( A e. RR /\ B e. RR ) -> ( ( 0  0