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	$$⊢\left(A\in ℝ\wedge B\in ℝ\right)\to \left(\left(0{<}_{ℝ}A\wedge 0{<}_{ℝ}B\right)\to 0{<}_{ℝ}AB\right)$$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cA	$$classA$$
1		cr	$$classℝ$$
2	0 1	wcel	$$wffA\in ℝ$$
3		cB	$$classB$$
4	3 1	wcel	$$wffB\in ℝ$$
5	2 4	wa	$$wff\left(A\in ℝ\wedge B\in ℝ\right)$$
6		cc0	$$class0$$
7		cltrr	$$class{<}_{ℝ}$$
8	6 0 7	wbr	$$wff0{<}_{ℝ}A$$
9	6 3 7	wbr	$$wff0{<}_{ℝ}B$$
10	8 9	wa	$$wff\left(0{<}_{ℝ}A\wedge 0{<}_{ℝ}B\right)$$
11		cmul	$$class\times$$
12	0 3 11	co	$$classAB$$
13	6 12 7	wbr	$$wff0{<}_{ℝ}AB$$
14	10 13	wi	$$wff\left(\left(0{<}_{ℝ}A\wedge 0{<}_{ℝ}B\right)\to 0{<}_{ℝ}AB\right)$$
15	5 14	wi	$$wff\left(\left(A\in ℝ\wedge B\in ℝ\right)\to \left(\left(0{<}_{ℝ}A\wedge 0{<}_{ℝ}B\right)\to 0{<}_{ℝ}AB\right)\right)$$