Metamath Proof Explorer


Theorem xmullid

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

Ref Expression
Assertion xmullid
|- ( A e. RR* -> ( 1 *e A ) = A )

Proof

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