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	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( ( 0 <ℝ 𝐴 ∧ 0 <ℝ 𝐵 ) → 0 <ℝ ( 𝐴 · 𝐵 ) ) )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cA	⊢ 𝐴
1		cr	⊢ ℝ
2	0 1	wcel	⊢ 𝐴 ∈ ℝ
3		cB	⊢ 𝐵
4	3 1	wcel	⊢ 𝐵 ∈ ℝ
5	2 4	wa	⊢ ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ )
6		cc0	⊢ 0
7		cltrr	⊢ <ℝ
8	6 0 7	wbr	⊢ 0 <ℝ 𝐴
9	6 3 7	wbr	⊢ 0 <ℝ 𝐵
10	8 9	wa	⊢ ( 0 <ℝ 𝐴 ∧ 0 <ℝ 𝐵 )
11		cmul	⊢ ·
12	0 3 11	co	⊢ ( 𝐴 · 𝐵 )
13	6 12 7	wbr	⊢ 0 <ℝ ( 𝐴 · 𝐵 )
14	10 13	wi	⊢ ( ( 0 <ℝ 𝐴 ∧ 0 <ℝ 𝐵 ) → 0 <ℝ ( 𝐴 · 𝐵 ) )
15	5 14	wi	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( ( 0 <ℝ 𝐴 ∧ 0 <ℝ 𝐵 ) → 0 <ℝ ( 𝐴 · 𝐵 ) ) )