Can mathematica display or verify trig identities?

Questions
1

I was trying to prove |cosh\:z|^2 = sinh^2\:x + cos^2\:x , ended up with a different answer and wanted to see how Mathematica did it - so is there a way to ask mathematica to either display or verify this - and other trig identities?

2

The equality looks false:

Plot[{Abs[Cosh[x]]^2, Sinh[x]^2 + Cos[x]^2}, {x, -1, 1}]
3

Sorry, typo - | { cosh(z)}|^2 = sinh^2 x + cos^2y

4

Because of \overline{\cosh(z)}=\cosh(\bar{z}) it can be produced by

In[23]:= Simplify[TrigExpand[TrigReduce[Cosh[x + I y] Cosh[x - I y]]] /. {Sin[y]^2 -> (1 - Cos[y]^2),
                                                                          Cosh[x]^2 -> (1 + Sinh[x]^2)}]
Out[23]= Cos[y]^2 + Sinh[x]^2

and then checked again by

In[37]:= FullSimplify[Cosh[x + I y] Cosh[x - I y] - (Cos[y]^2 + Sinh[x]^2)]
Out[37]= 0

B.t.w. there are equivalent answers, e.g. if one takes the other side of the basic identies in replacement

In[39]:= Simplify[TrigExpand[TrigReduce[Cosh[x + I y] Cosh[x - I y]]] /. {Cos[y]^2 -> (1 - Sin[y]^2), 
                                                                          Sinh[x]^2 -> (Cosh[x]^2 - 1)}]
Out[39]= Cosh[x]^2 - Sin[y]^2

In[41]:= FullSimplify[Cosh[x + I y] Cosh[x - I y] - Cosh[x]^2 + Sin[y]^2]
Out[41]= 0
5

That’s cool thanks - and I will especially remember the simple but clever check - but it seems I would need to know the correct intermediate identities first, so my question is now - what if I had no idea of how to approach this? I was hoping for something like a ‘complex_identity_expand’ command, which would list all the possibilities … ?

6

what if I had no idea of how to approach this?

Then one gains some insight with the help of the functions site, reads around in mathworld, experiments with the trig functions family trigonometric expressions, and tries putting expressions into different forms.

Usually there is no canonical form for a trigonometric expression: Sometimes you prefer the exponential form, then you need arguments as functions of many variables, then you need possibly to separate variables and want to express it as a bundle of functions of a single variable each.

Last but not least, there are sources like wikipedia, all giving hints what can be done next.

I was hoping for something like a ‘complexidentityexpand’ command

Of course you do. Me too. But instead we got only (!) tools like Mathematica, which implement lots of GetTheJobDone-facilities, if only one is able to specify the job …