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 syl5eqr 
 |-  ( A e. R. -> ( ( A .R 1R ) +R ( A .R -1R ) ) = 0R )
10 2 9 eqtr3d 
 |-  ( A e. R. -> ( A +R ( A .R -1R ) ) = 0R )