Metamath Proof Explorer

Theorem readd

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

Ref Expression
Assertion readd ⊢ 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 crre ⊢ ℜ ⁡ 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