Theorem resubeqsub

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

	Ref	Expression
Assertion	resubeqsub	$$⊢\left(A\in ℝ\wedge B\in ℝ\right)\to A{-}_{ℝ}B=A-B$$

Proof

Step	Hyp	Ref	Expression
1		ax-resscn	$$⊢ℝ\subseteq ℂ$$
2		resubeu	$$⊢\left(B\in ℝ\wedge A\in ℝ\right)\to \exists !x\in ℝB+x=A$$
3		reurex	$$⊢\exists !x\in ℝB+x=A\to \exists x\in ℝB+x=A$$
4	2 3	syl	$$⊢\left(B\in ℝ\wedge A\in ℝ\right)\to \exists x\in ℝB+x=A$$
5		recn	$$⊢B\in ℝ\to B\in ℂ$$
6		recn	$$⊢A\in ℝ\to A\in ℂ$$
7		sn-subeu	$$⊢\left(B\in ℂ\wedge A\in ℂ\right)\to \exists !x\in ℂB+x=A$$
8	5 6 7	syl2an	$$⊢\left(B\in ℝ\wedge A\in ℝ\right)\to \exists !x\in ℂB+x=A$$
9		riotass	$$⊢\left(ℝ\subseteq ℂ\wedge \exists x\in ℝB+x=A\wedge \exists !x\in ℂB+x=A\right)\to \left(\iota x\in ℝ|B+x=A\right)=\left(\iota x\in ℂ|B+x=A\right)$$
10	1 4 8 9	mp3an2i	$$⊢\left(B\in ℝ\wedge A\in ℝ\right)\to \left(\iota x\in ℝ|B+x=A\right)=\left(\iota x\in ℂ|B+x=A\right)$$
11	10	ancoms	$$⊢\left(A\in ℝ\wedge B\in ℝ\right)\to \left(\iota x\in ℝ|B+x=A\right)=\left(\iota x\in ℂ|B+x=A\right)$$
12		resubval	$$⊢\left(A\in ℝ\wedge B\in ℝ\right)\to A{-}_{ℝ}B=\left(\iota x\in ℝ|B+x=A\right)$$
13		subval	$$⊢\left(A\in ℂ\wedge B\in ℂ\right)\to A-B=\left(\iota x\in ℂ|B+x=A\right)$$
14	6 5 13	syl2an	$$⊢\left(A\in ℝ\wedge B\in ℝ\right)\to A-B=\left(\iota x\in ℂ|B+x=A\right)$$
15	11 12 14	3eqtr4d	$$⊢\left(A\in ℝ\wedge B\in ℝ\right)\to A{-}_{ℝ}B=A-B$$