# 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 ${⊢}\left({A}\in ℝ\wedge {B}\in ℝ\right)\to \left(\left(0<{A}\wedge 0<{B}\right)\to 0<{A}{B}\right)$

### Proof

Step Hyp Ref Expression
1 ax-pre-mulgt0 ${⊢}\left({A}\in ℝ\wedge {B}\in ℝ\right)\to \left(\left(0{<}_{ℝ}{A}\wedge 0{<}_{ℝ}{B}\right)\to 0{<}_{ℝ}{A}{B}\right)$
2 0re ${⊢}0\in ℝ$
3 ltxrlt ${⊢}\left(0\in ℝ\wedge {A}\in ℝ\right)\to \left(0<{A}↔0{<}_{ℝ}{A}\right)$
4 2 3 mpan ${⊢}{A}\in ℝ\to \left(0<{A}↔0{<}_{ℝ}{A}\right)$
5 ltxrlt ${⊢}\left(0\in ℝ\wedge {B}\in ℝ\right)\to \left(0<{B}↔0{<}_{ℝ}{B}\right)$
6 2 5 mpan ${⊢}{B}\in ℝ\to \left(0<{B}↔0{<}_{ℝ}{B}\right)$
7 4 6 bi2anan9 ${⊢}\left({A}\in ℝ\wedge {B}\in ℝ\right)\to \left(\left(0<{A}\wedge 0<{B}\right)↔\left(0{<}_{ℝ}{A}\wedge 0{<}_{ℝ}{B}\right)\right)$
8 remulcl ${⊢}\left({A}\in ℝ\wedge {B}\in ℝ\right)\to {A}{B}\in ℝ$
9 ltxrlt ${⊢}\left(0\in ℝ\wedge {A}{B}\in ℝ\right)\to \left(0<{A}{B}↔0{<}_{ℝ}{A}{B}\right)$
10 2 8 9 sylancr ${⊢}\left({A}\in ℝ\wedge {B}\in ℝ\right)\to \left(0<{A}{B}↔0{<}_{ℝ}{A}{B}\right)$
11 1 7 10 3imtr4d ${⊢}\left({A}\in ℝ\wedge {B}\in ℝ\right)\to \left(\left(0<{A}\wedge 0<{B}\right)\to 0<{A}{B}\right)$