Theorem rexsub

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

	Ref	Expression
Assertion	rexsub	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( 𝐴 +𝑒 -𝑒 𝐵 ) = ( 𝐴 − 𝐵 ) )

Proof

Step	Hyp	Ref	Expression
1		rexneg	⊢ ( 𝐵 ∈ ℝ → -𝑒 𝐵 = - 𝐵 )
2	1	adantl	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → -𝑒 𝐵 = - 𝐵 )
3	2	oveq2d	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( 𝐴 +𝑒 -𝑒 𝐵 ) = ( 𝐴 +𝑒 - 𝐵 ) )
4		renegcl	⊢ ( 𝐵 ∈ ℝ → - 𝐵 ∈ ℝ )
5		rexadd	⊢ ( ( 𝐴 ∈ ℝ ∧ - 𝐵 ∈ ℝ ) → ( 𝐴 +𝑒 - 𝐵 ) = ( 𝐴 + - 𝐵 ) )
6	4 5	sylan2	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( 𝐴 +𝑒 - 𝐵 ) = ( 𝐴 + - 𝐵 ) )
7		recn	⊢ ( 𝐴 ∈ ℝ → 𝐴 ∈ ℂ )
8		recn	⊢ ( 𝐵 ∈ ℝ → 𝐵 ∈ ℂ )
9		negsub	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( 𝐴 + - 𝐵 ) = ( 𝐴 − 𝐵 ) )
10	7 8 9	syl2an	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( 𝐴 + - 𝐵 ) = ( 𝐴 − 𝐵 ) )
11	3 6 10	3eqtrd	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( 𝐴 +𝑒 -𝑒 𝐵 ) = ( 𝐴 − 𝐵 ) )