Metamath Proof Explorer

Theorem imsub

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

Ref Expression
Assertion imsub ⊢ A ∈ ℂ ∧ B ∈ ℂ → ℑ ⁡ A − B = ℑ ⁡ A − ℑ ⁡ B

Proof

Step Hyp Ref Expression
1 negcl ⊢ B ∈ ℂ → − B ∈ ℂ
2 imadd ⊢ A ∈ ℂ ∧ − B ∈ ℂ → ℑ ⁡ A + − B = ℑ ⁡ A + ℑ ⁡ − B
3 1 2 sylan2 ⊢ A ∈ ℂ ∧ B ∈ ℂ → ℑ ⁡ A + − B = ℑ ⁡ A + ℑ ⁡ − B
4 imneg ⊢ 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 imcl ⊢ A ∈ ℂ → ℑ ⁡ A ∈ ℝ
11 10 recnd ⊢ A ∈ ℂ → ℑ ⁡ A ∈ ℂ
12 imcl ⊢ 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