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