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 e. CC /\ B e. CC ) -> ( Re ` ( A + B ) ) = ( ( Re ` A ) + ( Re ` B ) ) )

Proof

Step	Hyp	Ref	Expression
1		recl	|- ( A e. CC -> ( Re ` A ) e. RR )
2	1	adantr	|- ( ( A e. CC /\ B e. CC ) -> ( Re ` A ) e. RR )
3	2	recnd	|- ( ( A e. CC /\ B e. CC ) -> ( Re ` A ) e. CC )
4		ax-icn	|- _i e. CC
5		imcl	|- ( A e. CC -> ( Im ` A ) e. RR )
6	5	adantr	|- ( ( A e. CC /\ B e. CC ) -> ( Im ` A ) e. RR )
7	6	recnd	|- ( ( A e. CC /\ B e. CC ) -> ( Im ` A ) e. CC )
8		mulcl	|- ( ( _i e. CC /\ ( Im ` A ) e. CC ) -> ( _i x. ( Im ` A ) ) e. CC )
9	4 7 8	sylancr	|- ( ( A e. CC /\ B e. CC ) -> ( _i x. ( Im ` A ) ) e. CC )
10		recl	|- ( B e. CC -> ( Re ` B ) e. RR )
11	10	adantl	|- ( ( A e. CC /\ B e. CC ) -> ( Re ` B ) e. RR )
12	11	recnd	|- ( ( A e. CC /\ B e. CC ) -> ( Re ` B ) e. CC )
13		imcl	|- ( B e. CC -> ( Im ` B ) e. RR )
14	13	adantl	|- ( ( A e. CC /\ B e. CC ) -> ( Im ` B ) e. RR )
15	14	recnd	|- ( ( A e. CC /\ B e. CC ) -> ( Im ` B ) e. CC )
16		mulcl	|- ( ( _i e. CC /\ ( Im ` B ) e. CC ) -> ( _i x. ( Im ` B ) ) e. CC )
17	4 15 16	sylancr	|- ( ( A e. CC /\ B e. CC ) -> ( _i x. ( Im ` B ) ) e. CC )
18	3 9 12 17	add4d	|- ( ( A e. CC /\ B e. CC ) -> ( ( ( Re ` A ) + ( _i x. ( Im ` A ) ) ) + ( ( Re ` B ) + ( _i x. ( Im ` B ) ) ) ) = ( ( ( Re ` A ) + ( Re ` B ) ) + ( ( _i x. ( Im ` A ) ) + ( _i x. ( Im ` B ) ) ) ) )
19		replim	|- ( A e. CC -> A = ( ( Re ` A ) + ( _i x. ( Im ` A ) ) ) )
20		replim	|- ( B e. CC -> B = ( ( Re ` B ) + ( _i x. ( Im ` B ) ) ) )
21	19 20	oveqan12d	|- ( ( A e. CC /\ B e. CC ) -> ( A + B ) = ( ( ( Re ` A ) + ( _i x. ( Im ` A ) ) ) + ( ( Re ` B ) + ( _i x. ( Im ` B ) ) ) ) )
22	4	a1i	|- ( ( A e. CC /\ B e. CC ) -> _i e. CC )
23	22 7 15	adddid	|- ( ( A e. CC /\ B e. CC ) -> ( _i x. ( ( Im ` A ) + ( Im ` B ) ) ) = ( ( _i x. ( Im ` A ) ) + ( _i x. ( Im ` B ) ) ) )
24	23	oveq2d	|- ( ( A e. CC /\ B e. CC ) -> ( ( ( Re ` A ) + ( Re ` B ) ) + ( _i x. ( ( Im ` A ) + ( Im ` B ) ) ) ) = ( ( ( Re ` A ) + ( Re ` B ) ) + ( ( _i x. ( Im ` A ) ) + ( _i x. ( Im ` B ) ) ) ) )
25	18 21 24	3eqtr4d	|- ( ( A e. CC /\ B e. CC ) -> ( A + B ) = ( ( ( Re ` A ) + ( Re ` B ) ) + ( _i x. ( ( Im ` A ) + ( Im ` B ) ) ) ) )
26	25	fveq2d	|- ( ( A e. CC /\ B e. CC ) -> ( Re ` ( A + B ) ) = ( Re ` ( ( ( Re ` A ) + ( Re ` B ) ) + ( _i x. ( ( Im ` A ) + ( Im ` B ) ) ) ) ) )
27		readdcl	|- ( ( ( Re ` A ) e. RR /\ ( Re ` B ) e. RR ) -> ( ( Re ` A ) + ( Re ` B ) ) e. RR )
28	1 10 27	syl2an	|- ( ( A e. CC /\ B e. CC ) -> ( ( Re ` A ) + ( Re ` B ) ) e. RR )
29		readdcl	|- ( ( ( Im ` A ) e. RR /\ ( Im ` B ) e. RR ) -> ( ( Im ` A ) + ( Im ` B ) ) e. RR )
30	5 13 29	syl2an	|- ( ( A e. CC /\ B e. CC ) -> ( ( Im ` A ) + ( Im ` B ) ) e. RR )
31		crre	|- ( ( ( ( Re ` A ) + ( Re ` B ) ) e. RR /\ ( ( Im ` A ) + ( Im ` B ) ) e. RR ) -> ( Re ` ( ( ( Re ` A ) + ( Re ` B ) ) + ( _i x. ( ( Im ` A ) + ( Im ` B ) ) ) ) ) = ( ( Re ` A ) + ( Re ` B ) ) )
32	28 30 31	syl2anc	|- ( ( A e. CC /\ B e. CC ) -> ( Re ` ( ( ( Re ` A ) + ( Re ` B ) ) + ( _i x. ( ( Im ` A ) + ( Im ` B ) ) ) ) ) = ( ( Re ` A ) + ( Re ` B ) ) )
33	26 32	eqtrd	|- ( ( A e. CC /\ B e. CC ) -> ( Re ` ( A + B ) ) = ( ( Re ` A ) + ( Re ` B ) ) )