Theorem resubeu

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

	Ref	Expression
Assertion	resubeu	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ∃! 𝑥 ∈ ℝ ( 𝐴 + 𝑥 ) = 𝐵 )

Proof

Step	Hyp	Ref	Expression
1		simpl	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → 𝐴 ∈ ℝ )
2		rernegcl	⊢ ( 𝐴 ∈ ℝ → ( 0 −ℝ 𝐴 ) ∈ ℝ )
3	2	adantr	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( 0 −ℝ 𝐴 ) ∈ ℝ )
4		elre0re	⊢ ( 𝐴 ∈ ℝ → 0 ∈ ℝ )
5	4 4	readdcld	⊢ ( 𝐴 ∈ ℝ → ( 0 + 0 ) ∈ ℝ )
6		rernegcl	⊢ ( ( 0 + 0 ) ∈ ℝ → ( 0 −ℝ ( 0 + 0 ) ) ∈ ℝ )
7	5 6	syl	⊢ ( 𝐴 ∈ ℝ → ( 0 −ℝ ( 0 + 0 ) ) ∈ ℝ )
8	7	adantr	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( 0 −ℝ ( 0 + 0 ) ) ∈ ℝ )
9		simpr	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → 𝐵 ∈ ℝ )
10	8 9	readdcld	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( ( 0 −ℝ ( 0 + 0 ) ) + 𝐵 ) ∈ ℝ )
11	3 10	readdcld	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( ( 0 −ℝ 𝐴 ) + ( ( 0 −ℝ ( 0 + 0 ) ) + 𝐵 ) ) ∈ ℝ )
12		resubeulem2	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( 𝐴 + ( ( 0 −ℝ 𝐴 ) + ( ( 0 −ℝ ( 0 + 0 ) ) + 𝐵 ) ) ) = 𝐵 )
13		oveq2	⊢ ( 𝑥 = ( ( 0 −ℝ 𝐴 ) + ( ( 0 −ℝ ( 0 + 0 ) ) + 𝐵 ) ) → ( 𝐴 + 𝑥 ) = ( 𝐴 + ( ( 0 −ℝ 𝐴 ) + ( ( 0 −ℝ ( 0 + 0 ) ) + 𝐵 ) ) ) )
14	13	eqeq1d	⊢ ( 𝑥 = ( ( 0 −ℝ 𝐴 ) + ( ( 0 −ℝ ( 0 + 0 ) ) + 𝐵 ) ) → ( ( 𝐴 + 𝑥 ) = 𝐵 ↔ ( 𝐴 + ( ( 0 −ℝ 𝐴 ) + ( ( 0 −ℝ ( 0 + 0 ) ) + 𝐵 ) ) ) = 𝐵 ) )
15	14	rspcev	⊢ ( ( ( ( 0 −ℝ 𝐴 ) + ( ( 0 −ℝ ( 0 + 0 ) ) + 𝐵 ) ) ∈ ℝ ∧ ( 𝐴 + ( ( 0 −ℝ 𝐴 ) + ( ( 0 −ℝ ( 0 + 0 ) ) + 𝐵 ) ) ) = 𝐵 ) → ∃ 𝑥 ∈ ℝ ( 𝐴 + 𝑥 ) = 𝐵 )
16	11 12 15	syl2anc	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ∃ 𝑥 ∈ ℝ ( 𝐴 + 𝑥 ) = 𝐵 )
17	1 16	renegeulem	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ∃! 𝑥 ∈ ℝ ( 𝐴 + 𝑥 ) = 𝐵 )