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

Metamath Proof Explorer

Theorem remulcli

Description: Closure law for multiplication of reals. (Contributed by NM, 17-Jan-1997)

Ref Expression
Hypotheses recni.1 ⊢ A ∈ ℝ
axri.2 ⊢ B ∈ ℝ
Assertion remulcli ⊢ A ⁢ B ∈ ℝ

Proof

Step Hyp Ref Expression
1 recni.1 ⊢ A ∈ ℝ
2 axri.2 ⊢ B ∈ ℝ
3 remulcl ⊢ A ∈ ℝ ∧ B ∈ ℝ → A ⁢ B ∈ ℝ
4 1 2 3 mp2an ⊢ A ⁢ B ∈ ℝ