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 ⊢ A ∈ ℝ ∧ B ∈ ℝ → A + 𝑒 − B = A − B

Proof

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