# Metamath Proof Explorer

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

Ref Expression
Assertion readd ${⊢}\left({A}\in ℂ\wedge {B}\in ℂ\right)\to \Re \left({A}+{B}\right)=\Re \left({A}\right)+\Re \left({B}\right)$

### Proof

Step Hyp Ref Expression
1 recl ${⊢}{A}\in ℂ\to \Re \left({A}\right)\in ℝ$
2 1 adantr ${⊢}\left({A}\in ℂ\wedge {B}\in ℂ\right)\to \Re \left({A}\right)\in ℝ$
3 2 recnd ${⊢}\left({A}\in ℂ\wedge {B}\in ℂ\right)\to \Re \left({A}\right)\in ℂ$
4 ax-icn ${⊢}\mathrm{i}\in ℂ$
5 imcl ${⊢}{A}\in ℂ\to \Im \left({A}\right)\in ℝ$
6 5 adantr ${⊢}\left({A}\in ℂ\wedge {B}\in ℂ\right)\to \Im \left({A}\right)\in ℝ$
7 6 recnd ${⊢}\left({A}\in ℂ\wedge {B}\in ℂ\right)\to \Im \left({A}\right)\in ℂ$
8 mulcl ${⊢}\left(\mathrm{i}\in ℂ\wedge \Im \left({A}\right)\in ℂ\right)\to \mathrm{i}\Im \left({A}\right)\in ℂ$
9 4 7 8 sylancr ${⊢}\left({A}\in ℂ\wedge {B}\in ℂ\right)\to \mathrm{i}\Im \left({A}\right)\in ℂ$
10 recl ${⊢}{B}\in ℂ\to \Re \left({B}\right)\in ℝ$
11 10 adantl ${⊢}\left({A}\in ℂ\wedge {B}\in ℂ\right)\to \Re \left({B}\right)\in ℝ$
12 11 recnd ${⊢}\left({A}\in ℂ\wedge {B}\in ℂ\right)\to \Re \left({B}\right)\in ℂ$
13 imcl ${⊢}{B}\in ℂ\to \Im \left({B}\right)\in ℝ$
14 13 adantl ${⊢}\left({A}\in ℂ\wedge {B}\in ℂ\right)\to \Im \left({B}\right)\in ℝ$
15 14 recnd ${⊢}\left({A}\in ℂ\wedge {B}\in ℂ\right)\to \Im \left({B}\right)\in ℂ$
16 mulcl ${⊢}\left(\mathrm{i}\in ℂ\wedge \Im \left({B}\right)\in ℂ\right)\to \mathrm{i}\Im \left({B}\right)\in ℂ$
17 4 15 16 sylancr ${⊢}\left({A}\in ℂ\wedge {B}\in ℂ\right)\to \mathrm{i}\Im \left({B}\right)\in ℂ$
18 3 9 12 17 add4d ${⊢}\left({A}\in ℂ\wedge {B}\in ℂ\right)\to \Re \left({A}\right)+\mathrm{i}\Im \left({A}\right)+\Re \left({B}\right)+\mathrm{i}\Im \left({B}\right)=\Re \left({A}\right)+\Re \left({B}\right)+\mathrm{i}\Im \left({A}\right)+\mathrm{i}\Im \left({B}\right)$
19 replim ${⊢}{A}\in ℂ\to {A}=\Re \left({A}\right)+\mathrm{i}\Im \left({A}\right)$
20 replim ${⊢}{B}\in ℂ\to {B}=\Re \left({B}\right)+\mathrm{i}\Im \left({B}\right)$
21 19 20 oveqan12d ${⊢}\left({A}\in ℂ\wedge {B}\in ℂ\right)\to {A}+{B}=\Re \left({A}\right)+\mathrm{i}\Im \left({A}\right)+\Re \left({B}\right)+\mathrm{i}\Im \left({B}\right)$
22 4 a1i ${⊢}\left({A}\in ℂ\wedge {B}\in ℂ\right)\to \mathrm{i}\in ℂ$
23 22 7 15 adddid ${⊢}\left({A}\in ℂ\wedge {B}\in ℂ\right)\to \mathrm{i}\left(\Im \left({A}\right)+\Im \left({B}\right)\right)=\mathrm{i}\Im \left({A}\right)+\mathrm{i}\Im \left({B}\right)$
24 23 oveq2d ${⊢}\left({A}\in ℂ\wedge {B}\in ℂ\right)\to \Re \left({A}\right)+\Re \left({B}\right)+\mathrm{i}\left(\Im \left({A}\right)+\Im \left({B}\right)\right)=\Re \left({A}\right)+\Re \left({B}\right)+\mathrm{i}\Im \left({A}\right)+\mathrm{i}\Im \left({B}\right)$
25 18 21 24 3eqtr4d ${⊢}\left({A}\in ℂ\wedge {B}\in ℂ\right)\to {A}+{B}=\Re \left({A}\right)+\Re \left({B}\right)+\mathrm{i}\left(\Im \left({A}\right)+\Im \left({B}\right)\right)$
26 25 fveq2d ${⊢}\left({A}\in ℂ\wedge {B}\in ℂ\right)\to \Re \left({A}+{B}\right)=\Re \left(\Re \left({A}\right)+\Re \left({B}\right)+\mathrm{i}\left(\Im \left({A}\right)+\Im \left({B}\right)\right)\right)$
27 readdcl ${⊢}\left(\Re \left({A}\right)\in ℝ\wedge \Re \left({B}\right)\in ℝ\right)\to \Re \left({A}\right)+\Re \left({B}\right)\in ℝ$
28 1 10 27 syl2an ${⊢}\left({A}\in ℂ\wedge {B}\in ℂ\right)\to \Re \left({A}\right)+\Re \left({B}\right)\in ℝ$
29 readdcl ${⊢}\left(\Im \left({A}\right)\in ℝ\wedge \Im \left({B}\right)\in ℝ\right)\to \Im \left({A}\right)+\Im \left({B}\right)\in ℝ$
30 5 13 29 syl2an ${⊢}\left({A}\in ℂ\wedge {B}\in ℂ\right)\to \Im \left({A}\right)+\Im \left({B}\right)\in ℝ$
31 crre ${⊢}\left(\Re \left({A}\right)+\Re \left({B}\right)\in ℝ\wedge \Im \left({A}\right)+\Im \left({B}\right)\in ℝ\right)\to \Re \left(\Re \left({A}\right)+\Re \left({B}\right)+\mathrm{i}\left(\Im \left({A}\right)+\Im \left({B}\right)\right)\right)=\Re \left({A}\right)+\Re \left({B}\right)$
32 28 30 31 syl2anc ${⊢}\left({A}\in ℂ\wedge {B}\in ℂ\right)\to \Re \left(\Re \left({A}\right)+\Re \left({B}\right)+\mathrm{i}\left(\Im \left({A}\right)+\Im \left({B}\right)\right)\right)=\Re \left({A}\right)+\Re \left({B}\right)$
33 26 32 eqtrd ${⊢}\left({A}\in ℂ\wedge {B}\in ℂ\right)\to \Re \left({A}+{B}\right)=\Re \left({A}\right)+\Re \left({B}\right)$