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	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( 𝐴 −ℝ 𝐵 ) = ( 𝐴 − 𝐵 ) )