Metamath Proof Explorer


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 ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ∃! 𝑥 ∈ ℝ ( 𝐴 + 𝑥 ) = 𝐵 )