Metamath Proof Explorer

Theorem imadd

Description: Imaginary part distributes over addition. (Contributed by NM, 18-Mar-2005) (Revised by Mario Carneiro, 14-Jul-2014)

Ref Expression
Assertion imadd ⊢A∈ℂ∧B∈ℂ→ℑ⁡A+B=ℑ⁡A+ℑ⁡B

Proof

Step Hyp Ref Expression
1 recl ⊢A∈ℂ→ℜ⁡A∈ℝ
2 1 adantr ⊢A∈ℂ∧B∈ℂ→ℜ⁡A∈ℝ
3 2 recnd ⊢A∈ℂ∧B∈ℂ→ℜ⁡A∈ℂ
4 ax-icn ⊢i∈ℂ
5 imcl ⊢A∈ℂ→ℑ⁡A∈ℝ
6 5 adantr ⊢A∈ℂ∧B∈ℂ→ℑ⁡A∈ℝ
7 6 recnd ⊢A∈ℂ∧B∈ℂ→ℑ⁡A∈ℂ
8 mulcl ⊢i∈ℂ∧ℑ⁡A∈ℂ→i⁢ℑ⁡A∈ℂ
9 4 7 8 sylancr ⊢A∈ℂ∧B∈ℂ→i⁢ℑ⁡A∈ℂ
10 recl ⊢B∈ℂ→ℜ⁡B∈ℝ
11 10 adantl ⊢A∈ℂ∧B∈ℂ→ℜ⁡B∈ℝ
12 11 recnd ⊢A∈ℂ∧B∈ℂ→ℜ⁡B∈ℂ
13 imcl ⊢B∈ℂ→ℑ⁡B∈ℝ
14 13 adantl ⊢A∈ℂ∧B∈ℂ→ℑ⁡B∈ℝ
15 14 recnd ⊢A∈ℂ∧B∈ℂ→ℑ⁡B∈ℂ
16 mulcl ⊢i∈ℂ∧ℑ⁡B∈ℂ→i⁢ℑ⁡B∈ℂ
17 4 15 16 sylancr ⊢A∈ℂ∧B∈ℂ→i⁢ℑ⁡B∈ℂ
18 3 9 12 17 add4d ⊢A∈ℂ∧B∈ℂ→ℜ⁡A+i⁢ℑ⁡A+ℜ⁡B+i⁢ℑ⁡B=ℜ⁡A+ℜ⁡B+i⁢ℑ⁡A+i⁢ℑ⁡B
19 replim ⊢A∈ℂ→A=ℜ⁡A+i⁢ℑ⁡A
20 replim ⊢B∈ℂ→B=ℜ⁡B+i⁢ℑ⁡B
21 19 20 oveqan12d ⊢A∈ℂ∧B∈ℂ→A+B=ℜ⁡A+i⁢ℑ⁡A+ℜ⁡B+i⁢ℑ⁡B
22 4 a1i ⊢A∈ℂ∧B∈ℂ→i∈ℂ
23 22 7 15 adddid ⊢A∈ℂ∧B∈ℂ→i⁢ℑ⁡A+ℑ⁡B=i⁢ℑ⁡A+i⁢ℑ⁡B
24 23 oveq2d ⊢A∈ℂ∧B∈ℂ→ℜ⁡A+ℜ⁡B+i⁢ℑ⁡A+ℑ⁡B=ℜ⁡A+ℜ⁡B+i⁢ℑ⁡A+i⁢ℑ⁡B
25 18 21 24 3eqtr4d ⊢A∈ℂ∧B∈ℂ→A+B=ℜ⁡A+ℜ⁡B+i⁢ℑ⁡A+ℑ⁡B
26 25 fveq2d ⊢A∈ℂ∧B∈ℂ→ℑ⁡A+B=ℑ⁡ℜ⁡A+ℜ⁡B+i⁢ℑ⁡A+ℑ⁡B
27 readdcl ⊢ℜ⁡A∈ℝ∧ℜ⁡B∈ℝ→ℜ⁡A+ℜ⁡B∈ℝ
28 1 10 27 syl2an ⊢A∈ℂ∧B∈ℂ→ℜ⁡A+ℜ⁡B∈ℝ
29 readdcl ⊢ℑ⁡A∈ℝ∧ℑ⁡B∈ℝ→ℑ⁡A+ℑ⁡B∈ℝ
30 5 13 29 syl2an ⊢A∈ℂ∧B∈ℂ→ℑ⁡A+ℑ⁡B∈ℝ
31 crim ⊢ℜ⁡A+ℜ⁡B∈ℝ∧ℑ⁡A+ℑ⁡B∈ℝ→ℑ⁡ℜ⁡A+ℜ⁡B+i⁢ℑ⁡A+ℑ⁡B=ℑ⁡A+ℑ⁡B
32 28 30 31 syl2anc ⊢A∈ℂ∧B∈ℂ→ℑ⁡ℜ⁡A+ℜ⁡B+i⁢ℑ⁡A+ℑ⁡B=ℑ⁡A+ℑ⁡B
33 26 32 eqtrd ⊢A∈ℂ∧B∈ℂ→ℑ⁡A+B=ℑ⁡A+ℑ⁡B