This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem axmulgt0

Description: The product of two positive reals is positive. Axiom 21 of 22 for real and complex numbers, derived from ZF set theory. (This restates ax-pre-mulgt0 with ordering on the extended reals.) (Contributed by NM, 13-Oct-2005)

Ref Expression
Assertion axmulgt0 ⊢ A ∈ ℝ ∧ B ∈ ℝ → 0 < A ∧ 0 < B → 0 < A ⁢ B

Proof

Step Hyp Ref Expression
1 ax-pre-mulgt0 ⊢ A ∈ ℝ ∧ B ∈ ℝ → 0 < ℝ A ∧ 0 < ℝ B → 0 < ℝ A ⁢ B
2 0re ⊢ 0 ∈ ℝ
3 ltxrlt ⊢ 0 ∈ ℝ ∧ A ∈ ℝ → 0 < A ↔ 0 < ℝ A
4 2 3 mpan ⊢ A ∈ ℝ → 0 < A ↔ 0 < ℝ A
5 ltxrlt ⊢ 0 ∈ ℝ ∧ B ∈ ℝ → 0 < B ↔ 0 < ℝ B
6 2 5 mpan ⊢ B ∈ ℝ → 0 < B ↔ 0 < ℝ B
7 4 6 bi2anan9 ⊢ A ∈ ℝ ∧ B ∈ ℝ → 0 < A ∧ 0 < B ↔ 0 < ℝ A ∧ 0 < ℝ B
8 remulcl ⊢ A ∈ ℝ ∧ B ∈ ℝ → A ⁢ B ∈ ℝ
9 ltxrlt ⊢ 0 ∈ ℝ ∧ A ⁢ B ∈ ℝ → 0 < A ⁢ B ↔ 0 < ℝ A ⁢ B
10 2 8 9 sylancr ⊢ A ∈ ℝ ∧ B ∈ ℝ → 0 < A ⁢ B ↔ 0 < ℝ A ⁢ B
11 1 7 10 3imtr4d ⊢ A ∈ ℝ ∧ B ∈ ℝ → 0 < A ∧ 0 < B → 0 < A ⁢ B