Metamath Proof Explorer

Theorem xmul02

Description: Extended real version of mul02 . (Contributed by Mario Carneiro, 20-Aug-2015)

Ref Expression
Assertion xmul02 
|- ( A e. RR* -> ( 0 *e A ) = 0 )

Proof

Step Hyp Ref Expression
1 0xr 
 |-  0 e. RR*
2 xmulcom 
 |-  ( ( 0 e. RR* /\ A e. RR* ) -> ( 0 *e A ) = ( A *e 0 ) )
3 1 2 mpan 
 |-  ( A e. RR* -> ( 0 *e A ) = ( A *e 0 ) )
4 xmul01 
 |-  ( A e. RR* -> ( A *e 0 ) = 0 )
5 3 4 eqtrd 
 |-  ( A e. RR* -> ( 0 *e A ) = 0 )