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