This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ( 𝐴 ∈ R → ( 𝐴 +R ( 𝐴 ·R -1R ) ) = 0R )

Proof

Step Hyp Ref Expression
1 1idsr ⊢ ( 𝐴 ∈ R → ( 𝐴 ·R 1R ) = 𝐴 )
2 1 oveq1d ⊢ ( 𝐴 ∈ R → ( ( 𝐴 ·R 1R ) +R ( 𝐴 ·R -1R ) ) = ( 𝐴 +R ( 𝐴 ·R -1R ) ) )
3 distrsr ⊢ ( 𝐴 ·R ( -1R +R 1R ) ) = ( ( 𝐴 ·R -1R ) +R ( 𝐴 ·R 1R ) )
4 m1p1sr ⊢ ( -1R +R 1R ) = 0R
5 4 oveq2i ⊢ ( 𝐴 ·R ( -1R +R 1R ) ) = ( 𝐴 ·R 0R )
6 addcomsr ⊢ ( ( 𝐴 ·R -1R ) +R ( 𝐴 ·R 1R ) ) = ( ( 𝐴 ·R 1R ) +R ( 𝐴 ·R -1R ) )
7 3 5 6 3eqtr3i ⊢ ( 𝐴 ·R 0R ) = ( ( 𝐴 ·R 1R ) +R ( 𝐴 ·R -1R ) )
8 00sr ⊢ ( 𝐴 ∈ R → ( 𝐴 ·R 0R ) = 0R )
9 7 8 eqtr3id ⊢ ( 𝐴 ∈ R → ( ( 𝐴 ·R 1R ) +R ( 𝐴 ·R -1R ) ) = 0R )
10 2 9 eqtr3d ⊢ ( 𝐴 ∈ R → ( 𝐴 +R ( 𝐴 ·R -1R ) ) = 0R )