Theorem resubeu

Description: Existential uniqueness of real differences. (Contributed by Steven Nguyen, 7-Jan-2023)

	Ref	Expression
Assertion	resubeu	$$⊢\left(A\in ℝ\wedge B\in ℝ\right)\to \exists !x\in ℝA+x=B$$

Proof

Step	Hyp	Ref	Expression
1		simpl	$$⊢\left(A\in ℝ\wedge B\in ℝ\right)\to A\in ℝ$$
2		rernegcl	$$⊢A\in ℝ\to 0{-}_{ℝ}A\in ℝ$$
3	2	adantr	$$⊢\left(A\in ℝ\wedge B\in ℝ\right)\to 0{-}_{ℝ}A\in ℝ$$
4		elre0re	$$⊢A\in ℝ\to 0\in ℝ$$
5	4 4	readdcld	$$⊢A\in ℝ\to 0+0\in ℝ$$
6		rernegcl	$$⊢0+0\in ℝ\to 0{-}_{ℝ}\left(0+0\right)\in ℝ$$
7	5 6	syl	$$⊢A\in ℝ\to 0{-}_{ℝ}\left(0+0\right)\in ℝ$$
8	7	adantr	$$⊢\left(A\in ℝ\wedge B\in ℝ\right)\to 0{-}_{ℝ}\left(0+0\right)\in ℝ$$
9		simpr	$$⊢\left(A\in ℝ\wedge B\in ℝ\right)\to B\in ℝ$$
10	8 9	readdcld	$$⊢\left(A\in ℝ\wedge B\in ℝ\right)\to \left(0{-}_{ℝ}\left(0+0\right)\right)+B\in ℝ$$
11	3 10	readdcld	$$⊢\left(A\in ℝ\wedge B\in ℝ\right)\to \left(0{-}_{ℝ}A\right)+\left(0{-}_{ℝ}\left(0+0\right)\right)+B\in ℝ$$
12		resubeulem2	$$⊢\left(A\in ℝ\wedge B\in ℝ\right)\to A+\left(0{-}_{ℝ}A\right)+\left(\left(0{-}_{ℝ}\left(0+0\right)\right)+B\right)=B$$
13		oveq2	$$⊢x=\left(0{-}_{ℝ}A\right)+\left(0{-}_{ℝ}\left(0+0\right)\right)+B\to A+x=A+\left(0{-}_{ℝ}A\right)+\left(\left(0{-}_{ℝ}\left(0+0\right)\right)+B\right)$$
14	13	eqeq1d	$$⊢x=\left(0{-}_{ℝ}A\right)+\left(0{-}_{ℝ}\left(0+0\right)\right)+B\to \left(A+x=B\leftrightarrow A+\left(0{-}_{ℝ}A\right)+\left(\left(0{-}_{ℝ}\left(0+0\right)\right)+B\right)=B\right)$$
15	14	rspcev	$$⊢\left(\left(0{-}_{ℝ}A\right)+\left(0{-}_{ℝ}\left(0+0\right)\right)+B\in ℝ\wedge A+\left(0{-}_{ℝ}A\right)+\left(\left(0{-}_{ℝ}\left(0+0\right)\right)+B\right)=B\right)\to \exists x\in ℝA+x=B$$
16	11 12 15	syl2anc	$$⊢\left(A\in ℝ\wedge B\in ℝ\right)\to \exists x\in ℝA+x=B$$
17	1 16	renegeulem	$$⊢\left(A\in ℝ\wedge B\in ℝ\right)\to \exists !x\in ℝA+x=B$$