[STATEMENT]
lemma Arg_exp: "-pi < Im z \<Longrightarrow> Im z \<le> pi \<Longrightarrow> Arg(exp z) = Im z"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>- pi < Im z; Im z \<le> pi\<rbrakk> \<Longrightarrow> Arg (exp z) = Im z
[PROOF STEP]
by (rule Arg_unique [of "exp(Re z)"]) (auto simp: exp_eq_polar)