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

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

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