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 ( 𝐴 ∈ ℝ* → ( - 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 𝐴 ) = -𝑒 𝐴 )