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

Metamath Proof Explorer

Theorem xmulcl

Description: Closure of extended real multiplication. (Contributed by Mario Carneiro, 20-Aug-2015)

Ref Expression
Assertion xmulcl 
|- ( ( A e. RR* /\ B e. RR* ) -> ( A *e B ) e. RR* )

Proof

Step Hyp Ref Expression
1 xmulf 
 |-  *e : ( RR* X. RR* ) --> RR*
2 1 fovcl 
 |-  ( ( A e. RR* /\ B e. RR* ) -> ( A *e B ) e. RR* )