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 ⊢ A ∈ ℝ ∧ B ∈ ℝ → 0 < ℝ A ∧ 0 < ℝ B → 0 < ℝ A B
Detailed syntax breakdown
Step
Hyp
Ref
Expression
0
cA class A
1
cr class ℝ
2
0 1
wcel wff A ∈ ℝ
3
cB class B
4
3 1
wcel wff B ∈ ℝ
5
2 4
wa wff A ∈ ℝ ∧ B ∈ ℝ
6
cc0 class 0
7
cltrr class < ℝ
8
6 0 7
wbr wff 0 < ℝ A
9
6 3 7
wbr wff 0 < ℝ B
10
8 9
wa wff 0 < ℝ A ∧ 0 < ℝ B
11
cmul class ×
12
0 3 11
co class A B
13
6 12 7
wbr wff 0 < ℝ A B
14
10 13
wi wff 0 < ℝ A ∧ 0 < ℝ B → 0 < ℝ A B
15
5 14
wi wff A ∈ ℝ ∧ B ∈ ℝ → 0 < ℝ A ∧ 0 < ℝ B → 0 < ℝ A B