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