Metamath Proof Explorer

Theorem resub

Description: Real part distributes over subtraction. (Contributed by NM, 17-Mar-2005)

Ref Expression
Assertion resub ⊢ A ∈ ℂ ∧ B ∈ ℂ → ℜ ⁡ A − B = ℜ ⁡ A − ℜ ⁡ B

Proof

Step Hyp Ref Expression
1 negcl ⊢ B ∈ ℂ → − B ∈ ℂ
2 readd ⊢ A ∈ ℂ ∧ − B ∈ ℂ → ℜ ⁡ A + − B = ℜ ⁡ A + ℜ ⁡ − B
3 1 2 sylan2 ⊢ A ∈ ℂ ∧ B ∈ ℂ → ℜ ⁡ A + − B = ℜ ⁡ A + ℜ ⁡ − B
4 reneg ⊢ B ∈ ℂ → ℜ ⁡ − B = − ℜ ⁡ B
5 4 adantl ⊢ A ∈ ℂ ∧ B ∈ ℂ → ℜ ⁡ − B = − ℜ ⁡ B
6 5 oveq2d ⊢ A ∈ ℂ ∧ B ∈ ℂ → ℜ ⁡ A + ℜ ⁡ − B = ℜ ⁡ A + − ℜ ⁡ B
7 3 6 eqtrd ⊢ A ∈ ℂ ∧ B ∈ ℂ → ℜ ⁡ A + − B = ℜ ⁡ A + − ℜ ⁡ B
8 negsub ⊢ A ∈ ℂ ∧ B ∈ ℂ → A + − B = A − B
9 8 fveq2d ⊢ A ∈ ℂ ∧ B ∈ ℂ → ℜ ⁡ A + − B = ℜ ⁡ A − B
10 recl ⊢ A ∈ ℂ → ℜ ⁡ A ∈ ℝ
11 10 recnd ⊢ A ∈ ℂ → ℜ ⁡ A ∈ ℂ
12 recl ⊢ B ∈ ℂ → ℜ ⁡ B ∈ ℝ
13 12 recnd ⊢ B ∈ ℂ → ℜ ⁡ B ∈ ℂ
14 negsub ⊢ ℜ ⁡ A ∈ ℂ ∧ ℜ ⁡ B ∈ ℂ → ℜ ⁡ A + − ℜ ⁡ B = ℜ ⁡ A − ℜ ⁡ B
15 11 13 14 syl2an ⊢ A ∈ ℂ ∧ B ∈ ℂ → ℜ ⁡ A + − ℜ ⁡ B = ℜ ⁡ A − ℜ ⁡ B
16 7 9 15 3eqtr3d ⊢ A ∈ ℂ ∧ B ∈ ℂ → ℜ ⁡ A − B = ℜ ⁡ A − ℜ ⁡ B