Theorem renegadd

Description: Relationship between real negation and addition. (Contributed by Steven Nguyen, 7-Jan-2023)

	Ref	Expression
Assertion	renegadd	$$⊢\left(A\in ℝ\wedge B\in ℝ\right)\to \left(0{-}_{ℝ}A=B\leftrightarrow A+B=0\right)$$

Proof

Step	Hyp	Ref	Expression
1		elre0re	$$⊢A\in ℝ\to 0\in ℝ$$
2		resubval	$$⊢\left(0\in ℝ\wedge A\in ℝ\right)\to 0{-}_{ℝ}A=\left(\iota x\in ℝ|A+x=0\right)$$
3	1 2	mpancom	$$⊢A\in ℝ\to 0{-}_{ℝ}A=\left(\iota x\in ℝ|A+x=0\right)$$
4	3	eqeq1d	$$⊢A\in ℝ\to \left(0{-}_{ℝ}A=B\leftrightarrow \left(\iota x\in ℝ|A+x=0\right)=B\right)$$
5	4	adantr	$$⊢\left(A\in ℝ\wedge B\in ℝ\right)\to \left(0{-}_{ℝ}A=B\leftrightarrow \left(\iota x\in ℝ|A+x=0\right)=B\right)$$
6		renegeu	$$⊢A\in ℝ\to \exists !x\in ℝA+x=0$$
7		oveq2	$$⊢x=B\to A+x=A+B$$
8	7	eqeq1d	$$⊢x=B\to \left(A+x=0\leftrightarrow A+B=0\right)$$
9	8	riota2	$$⊢\left(B\in ℝ\wedge \exists !x\in ℝA+x=0\right)\to \left(A+B=0\leftrightarrow \left(\iota x\in ℝ|A+x=0\right)=B\right)$$
10	6 9	sylan2	$$⊢\left(B\in ℝ\wedge A\in ℝ\right)\to \left(A+B=0\leftrightarrow \left(\iota x\in ℝ|A+x=0\right)=B\right)$$
11	10	ancoms	$$⊢\left(A\in ℝ\wedge B\in ℝ\right)\to \left(A+B=0\leftrightarrow \left(\iota x\in ℝ|A+x=0\right)=B\right)$$
12	5 11	bitr4d	$$⊢\left(A\in ℝ\wedge B\in ℝ\right)\to \left(0{-}_{ℝ}A=B\leftrightarrow A+B=0\right)$$