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

Metamath Proof Explorer

Theorem resubeqsub

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

Ref Expression
Assertion resubeqsub ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( 𝐴 −ℝ 𝐵 ) = ( 𝐴 − 𝐵 ) )

Proof

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