Theorem xmulm1

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

	Ref	Expression
Assertion	xmulm1	⊢ ( 𝐴 ∈ ℝ* → ( - 1 ·e 𝐴 ) = -𝑒 𝐴 )

Proof

Step	Hyp	Ref	Expression
1		1re	⊢ 1 ∈ ℝ
2		rexneg	⊢ ( 1 ∈ ℝ → -𝑒 1 = - 1 )
3	1 2	ax-mp	⊢ -𝑒 1 = - 1
4	3	oveq1i	⊢ ( -𝑒 1 ·e 𝐴 ) = ( - 1 ·e 𝐴 )
5		1xr	⊢ 1 ∈ ℝ*
6		xmulneg1	⊢ ( ( 1 ∈ ℝ* ∧ 𝐴 ∈ ℝ* ) → ( -𝑒 1 ·e 𝐴 ) = -𝑒 ( 1 ·e 𝐴 ) )
7	5 6	mpan	⊢ ( 𝐴 ∈ ℝ* → ( -𝑒 1 ·e 𝐴 ) = -𝑒 ( 1 ·e 𝐴 ) )
8	4 7	eqtr3id	⊢ ( 𝐴 ∈ ℝ* → ( - 1 ·e 𝐴 ) = -𝑒 ( 1 ·e 𝐴 ) )
9		xmullid	⊢ ( 𝐴 ∈ ℝ* → ( 1 ·e 𝐴 ) = 𝐴 )
10		xnegeq	⊢ ( ( 1 ·e 𝐴 ) = 𝐴 → -𝑒 ( 1 ·e 𝐴 ) = -𝑒 𝐴 )
11	9 10	syl	⊢ ( 𝐴 ∈ ℝ* → -𝑒 ( 1 ·e 𝐴 ) = -𝑒 𝐴 )
12	8 11	eqtrd	⊢ ( 𝐴 ∈ ℝ* → ( - 1 ·e 𝐴 ) = -𝑒 𝐴 )