Description: The complex conjugate of a sum. (Contributed by Paul Chapman, 9-Nov-2007) (Revised by Mario Carneiro, 25-Jul-2014)
Ref | Expression | ||
---|---|---|---|
Hypotheses | fsumre.1 | ||
fsumre.2 | |||
Assertion | fsumcj |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | fsumre.1 | ||
2 | fsumre.2 | ||
3 | cjf | ||
4 | cjadd | ||
5 | 1 2 3 4 | fsumrelem |