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 ∈ ℝ * → -1 ⋅ 𝑒 A = − A

Proof

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