Theorem renegid

Description: Addition of a real number and its negative. (Contributed by Steven Nguyen, 7-Jan-2023)

	Ref	Expression
Assertion	renegid	|- ( A e. RR -> ( A + ( 0 -R A ) ) = 0 )

Proof

Step	Hyp	Ref	Expression
1		eqid	|- ( 0 -R A ) = ( 0 -R A )
2		rernegcl	|- ( A e. RR -> ( 0 -R A ) e. RR )
3		renegadd	|- ( ( A e. RR /\ ( 0 -R A ) e. RR ) -> ( ( 0 -R A ) = ( 0 -R A ) <-> ( A + ( 0 -R A ) ) = 0 ) )
4	2 3	mpdan	|- ( A e. RR -> ( ( 0 -R A ) = ( 0 -R A ) <-> ( A + ( 0 -R A ) ) = 0 ) )
5	1 4	mpbii	|- ( A e. RR -> ( A + ( 0 -R A ) ) = 0 )