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		xmulid2	|- ( 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 )