range of cos

Stream: maths

[Johan Commelin]

Do we know that complex.cos has infinite range? (That's all I need.)

[Floris van Doorn]

It's shouldn't be too hard with docs#real.range_cos, docs#cardinal.mk_Icc_real and definition of docs#real.cos. But presumably you want something shorter.

[Kevin Buzzard]

Presumably any function on the reals or complexes which is differentiable at some point with nonzero derivative has infinite image

[Johan Commelin]

@Floris van Doorn Thanks, I'll try.

[Johan Commelin]

@Floris van Doorn would you mind taking a look at #4241? It seems convenient (-;

[Mario Carneiro]

Isn't there an arccos function?

[Mario Carneiro]

that should prove pretty directly that the range of complex.cos is C

[Johan Commelin]

It seems that it's only there for real.cos

[Mario Carneiro]

Is complex.log there? It should just be some arithmetic of logs

[Mario Carneiro]

See http://us.metamath.org/mpeuni/df-acos.html and http://us.metamath.org/mpeuni/df-asin.html