Metamath Proof Explorer

Theorem resubeqsub

Description: Equivalence between real subtraction and subtraction. (Contributed by SN, 5-May-2024)

Ref Expression
Assertion resubeqsub ⊢ A ∈ ℝ ∧ B ∈ ℝ → A - ℝ B = A − B

Proof

Step Hyp Ref Expression
1 ax-resscn ⊢ ℝ ⊆ ℂ
2 resubeu ⊢ B ∈ ℝ ∧ A ∈ ℝ → ∃! x ∈ ℝ B + x = A
3 reurex ⊢ ∃! x ∈ ℝ B + x = A → ∃ x ∈ ℝ B + x = A
4 2 3 syl ⊢ B ∈ ℝ ∧ A ∈ ℝ → ∃ x ∈ ℝ B + x = A
5 recn ⊢ B ∈ ℝ → B ∈ ℂ
6 recn ⊢ A ∈ ℝ → A ∈ ℂ
7 sn-subeu ⊢ B ∈ ℂ ∧ A ∈ ℂ → ∃! x ∈ ℂ B + x = A
8 5 6 7 syl2an ⊢ B ∈ ℝ ∧ A ∈ ℝ → ∃! x ∈ ℂ B + x = A
9 riotass ⊢ ℝ ⊆ ℂ ∧ ∃ x ∈ ℝ B + x = A ∧ ∃! x ∈ ℂ B + x = A → ι x ∈ ℝ | B + x = A = ι x ∈ ℂ | B + x = A
10 1 4 8 9 mp3an2i ⊢ B ∈ ℝ ∧ A ∈ ℝ → ι x ∈ ℝ | B + x = A = ι x ∈ ℂ | B + x = A
11 10 ancoms ⊢ A ∈ ℝ ∧ B ∈ ℝ → ι x ∈ ℝ | B + x = A = ι x ∈ ℂ | B + x = A
12 resubval ⊢ A ∈ ℝ ∧ B ∈ ℝ → A - ℝ B = ι x ∈ ℝ | B + x = A
13 subval ⊢ A ∈ ℂ ∧ B ∈ ℂ → A − B = ι x ∈ ℂ | B + x = A
14 6 5 13 syl2an ⊢ A ∈ ℝ ∧ B ∈ ℝ → A − B = ι x ∈ ℂ | B + x = A
15 11 12 14 3eqtr4d ⊢ A ∈ ℝ ∧ B ∈ ℝ → A - ℝ B = A − B