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

Metamath Proof Explorer

Theorem xmulm1

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

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

Proof

Step Hyp Ref Expression
1 1re 
 |-  1 e. RR
2 rexneg 
 |-  ( 1 e. RR -> -e 1 = -u 1 )
3 1 2 ax-mp 
 |-  -e 1 = -u 1
4 3 oveq1i 
 |-  ( -e 1 *e A ) = ( -u 1 *e A )
5 1xr 
 |-  1 e. RR*
6 xmulneg1 
 |-  ( ( 1 e. RR* /\ A e. RR* ) -> ( -e 1 *e A ) = -e ( 1 *e A ) )
7 5 6 mpan 
 |-  ( A e. RR* -> ( -e 1 *e A ) = -e ( 1 *e A ) )
8 4 7 eqtr3id 
 |-  ( A e. RR* -> ( -u 1 *e A ) = -e ( 1 *e A ) )
9 xmullid 
 |-  ( A e. RR* -> ( 1 *e A ) = A )
10 xnegeq 
 |-  ( ( 1 *e A ) = A -> -e ( 1 *e A ) = -e A )
11 9 10 syl 
 |-  ( A e. RR* -> -e ( 1 *e A ) = -e A )
12 8 11 eqtrd 
 |-  ( A e. RR* -> ( -u 1 *e A ) = -e A )