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 ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( ℑ ‘ ( 𝐴 + 𝐵 ) ) = ( ( ℑ ‘ 𝐴 ) + ( ℑ ‘ 𝐵 ) ) )

Proof

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