This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.
Database REAL AND COMPLEX NUMBERS Construction and axiomatization of real and complex numbers Real and complex number postulates restated as axioms 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 <ℝ ( 𝐴 · 𝐵 ) ) )