# Metamath Proof Explorer

## Theorem rexsub

Description: Extended real subtraction when both arguments are real. (Contributed by Mario Carneiro, 23-Aug-2015)

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

### Proof

Step Hyp Ref Expression
1 rexneg ${⊢}{B}\in ℝ\to -{B}=-{B}$
2 1 adantl ${⊢}\left({A}\in ℝ\wedge {B}\in ℝ\right)\to -{B}=-{B}$
3 2 oveq2d ${⊢}\left({A}\in ℝ\wedge {B}\in ℝ\right)\to {A}{+}_{𝑒}\left(-{B}\right)={A}{+}_{𝑒}\left(-{B}\right)$
4 renegcl ${⊢}{B}\in ℝ\to -{B}\in ℝ$
5 rexadd ${⊢}\left({A}\in ℝ\wedge -{B}\in ℝ\right)\to {A}{+}_{𝑒}\left(-{B}\right)={A}+\left(-{B}\right)$
6 4 5 sylan2 ${⊢}\left({A}\in ℝ\wedge {B}\in ℝ\right)\to {A}{+}_{𝑒}\left(-{B}\right)={A}+\left(-{B}\right)$
7 recn ${⊢}{A}\in ℝ\to {A}\in ℂ$
8 recn ${⊢}{B}\in ℝ\to {B}\in ℂ$
9 negsub ${⊢}\left({A}\in ℂ\wedge {B}\in ℂ\right)\to {A}+\left(-{B}\right)={A}-{B}$
10 7 8 9 syl2an ${⊢}\left({A}\in ℝ\wedge {B}\in ℝ\right)\to {A}+\left(-{B}\right)={A}-{B}$
11 3 6 10 3eqtrd ${⊢}\left({A}\in ℝ\wedge {B}\in ℝ\right)\to {A}{+}_{𝑒}\left(-{B}\right)={A}-{B}$