Theorem fsumre

Description: The real part of a sum. (Contributed by Paul Chapman, 9-Nov-2007) (Revised by Mario Carneiro, 25-Jul-2014)

	Ref	Expression
Hypotheses	fsumre.1	|- ( ph -> A e. Fin )
	fsumre.2	|- ( ( ph /\ k e. A ) -> B e. CC )
Assertion	fsumre	|- ( ph -> ( Re ` sum_ k e. A B ) = sum_ k e. A ( Re ` B ) )

Proof

Step	Hyp	Ref	Expression
1		fsumre.1	|- ( ph -> A e. Fin )
2		fsumre.2	|- ( ( ph /\ k e. A ) -> B e. CC )
3		ref	|- Re : CC --> RR
4		ax-resscn	|- RR C_ CC
5		fss	|- ( ( Re : CC --> RR /\ RR C_ CC ) -> Re : CC --> CC )
6	3 4 5	mp2an	|- Re : CC --> CC
7		readd	|- ( ( x e. CC /\ y e. CC ) -> ( Re ` ( x + y ) ) = ( ( Re ` x ) + ( Re ` y ) ) )
8	1 2 6 7	fsumrelem	|- ( ph -> ( Re ` sum_ k e. A B ) = sum_ k e. A ( Re ` B ) )