This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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