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