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