Metamath Proof Explorer


Theorem pn0sr

Description: A signed real plus its negative is zero. (Contributed by NM, 14-May-1996) (New usage is discouraged.)

Ref Expression
Assertion pn0sr
|- ( A e. R. -> ( A +R ( A .R -1R ) ) = 0R )

Proof

Step Hyp Ref Expression
1 1idsr
 |-  ( A e. R. -> ( A .R 1R ) = A )
2 1 oveq1d
 |-  ( A e. R. -> ( ( A .R 1R ) +R ( A .R -1R ) ) = ( A +R ( A .R -1R ) ) )
3 distrsr
 |-  ( A .R ( -1R +R 1R ) ) = ( ( A .R -1R ) +R ( A .R 1R ) )
4 m1p1sr
 |-  ( -1R +R 1R ) = 0R
5 4 oveq2i
 |-  ( A .R ( -1R +R 1R ) ) = ( A .R 0R )
6 addcomsr
 |-  ( ( A .R -1R ) +R ( A .R 1R ) ) = ( ( A .R 1R ) +R ( A .R -1R ) )
7 3 5 6 3eqtr3i
 |-  ( A .R 0R ) = ( ( A .R 1R ) +R ( A .R -1R ) )
8 00sr
 |-  ( A e. R. -> ( A .R 0R ) = 0R )
9 7 8 eqtr3id
 |-  ( A e. R. -> ( ( A .R 1R ) +R ( A .R -1R ) ) = 0R )
10 2 9 eqtr3d
 |-  ( A e. R. -> ( A +R ( A .R -1R ) ) = 0R )