[STATEMENT]
lemma Ln_inverse: assumes "z \<notin> \<real>\<^sub>\<le>\<^sub>0" shows "Ln(inverse z) = -(Ln z)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Ln (inverse z) = - Ln z
[PROOF STEP]
proof (cases "z=0")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. z = 0 \<Longrightarrow> Ln (inverse z) = - Ln z
 2. z \<noteq> 0 \<Longrightarrow> Ln (inverse z) = - Ln z
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
z \<noteq> 0

goal (2 subgoals):
 1. z = 0 \<Longrightarrow> Ln (inverse z) = - Ln z
 2. z \<noteq> 0 \<Longrightarrow> Ln (inverse z) = - Ln z
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Ln (inverse z) = - Ln z
[PROOF STEP]
proof (rule exp_complex_eqI)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<bar>Im (Ln (inverse z)) - Im (- Ln z)\<bar> < 2 * pi
 2. exp (Ln (inverse z)) = exp (- Ln z)
[PROOF STEP]
have "\<bar>Im (Ln (inverse z)) - Im (- Ln z)\<bar> \<le> \<bar>Im (Ln (inverse z))\<bar> + \<bar>Im (- Ln z)\<bar>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<bar>Im (Ln (inverse z)) - Im (- Ln z)\<bar> \<le> \<bar>Im (Ln (inverse z))\<bar> + \<bar>Im (- Ln z)\<bar>
[PROOF STEP]
by (rule abs_triangle_ineq4)
[PROOF STATE]
proof (state)
this:
\<bar>Im (Ln (inverse z)) - Im (- Ln z)\<bar> \<le> \<bar>Im (Ln (inverse z))\<bar> + \<bar>Im (- Ln z)\<bar>

goal (2 subgoals):
 1. \<bar>Im (Ln (inverse z)) - Im (- Ln z)\<bar> < 2 * pi
 2. exp (Ln (inverse z)) = exp (- Ln z)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
\<bar>Im (Ln (inverse z)) - Im (- Ln z)\<bar> \<le> \<bar>Im (Ln (inverse z))\<bar> + \<bar>Im (- Ln z)\<bar>

goal (2 subgoals):
 1. \<bar>Im (Ln (inverse z)) - Im (- Ln z)\<bar> < 2 * pi
 2. exp (Ln (inverse z)) = exp (- Ln z)
[PROOF STEP]
have "\<dots> < pi + pi"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<bar>Im (Ln (inverse z))\<bar> + \<bar>Im (- Ln z)\<bar> < pi + pi
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<bar>Im (Ln (inverse z))\<bar> + \<bar>Im (- Ln z)\<bar> < pi + pi
[PROOF STEP]
have "\<bar>Im (Ln (inverse z))\<bar> < pi"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<bar>Im (Ln (inverse z))\<bar> < pi
[PROOF STEP]
by (simp add: False Im_Ln_less_pi abs_if assms minus_less_iff mpi_less_Im_Ln)
[PROOF STATE]
proof (state)
this:
\<bar>Im (Ln (inverse z))\<bar> < pi

goal (1 subgoal):
 1. \<bar>Im (Ln (inverse z))\<bar> + \<bar>Im (- Ln z)\<bar> < pi + pi
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
\<bar>Im (Ln (inverse z))\<bar> < pi

goal (1 subgoal):
 1. \<bar>Im (Ln (inverse z))\<bar> + \<bar>Im (- Ln z)\<bar> < pi + pi
[PROOF STEP]
have "\<bar>Im (- Ln z)\<bar> \<le> pi"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<bar>Im (- Ln z)\<bar> \<le> pi
[PROOF STEP]
using False Im_Ln_le_pi mpi_less_Im_Ln
[PROOF STATE]
proof (prove)
using this:
z \<noteq> 0
?z \<noteq> 0 \<Longrightarrow> Im (Ln ?z) \<le> pi
?z \<noteq> 0 \<Longrightarrow> - pi < Im (Ln ?z)

goal (1 subgoal):
 1. \<bar>Im (- Ln z)\<bar> \<le> pi
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
\<bar>Im (- Ln z)\<bar> \<le> pi

goal (1 subgoal):
 1. \<bar>Im (Ln (inverse z))\<bar> + \<bar>Im (- Ln z)\<bar> < pi + pi
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
\<bar>Im (Ln (inverse z))\<bar> < pi
\<bar>Im (- Ln z)\<bar> \<le> pi
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<bar>Im (Ln (inverse z))\<bar> < pi
\<bar>Im (- Ln z)\<bar> \<le> pi

goal (1 subgoal):
 1. \<bar>Im (Ln (inverse z))\<bar> + \<bar>Im (- Ln z)\<bar> < pi + pi
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<bar>Im (Ln (inverse z))\<bar> + \<bar>Im (- Ln z)\<bar> < pi + pi

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<bar>Im (Ln (inverse z))\<bar> + \<bar>Im (- Ln z)\<bar> < pi + pi

goal (2 subgoals):
 1. \<bar>Im (Ln (inverse z)) - Im (- Ln z)\<bar> < 2 * pi
 2. exp (Ln (inverse z)) = exp (- Ln z)
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
\<bar>Im (Ln (inverse z)) - Im (- Ln z)\<bar> < pi + pi
[PROOF STEP]
show "\<bar>Im (Ln (inverse z)) - Im (- Ln z)\<bar> < 2 * pi"
[PROOF STATE]
proof (prove)
using this:
\<bar>Im (Ln (inverse z)) - Im (- Ln z)\<bar> < pi + pi

goal (1 subgoal):
 1. \<bar>Im (Ln (inverse z)) - Im (- Ln z)\<bar> < 2 * pi
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<bar>Im (Ln (inverse z)) - Im (- Ln z)\<bar> < 2 * pi

goal (1 subgoal):
 1. exp (Ln (inverse z)) = exp (- Ln z)
[PROOF STEP]
show "exp (Ln (inverse z)) = exp (- Ln z)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. exp (Ln (inverse z)) = exp (- Ln z)
[PROOF STEP]
by (simp add: False exp_minus)
[PROOF STATE]
proof (state)
this:
exp (Ln (inverse z)) = exp (- Ln z)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
Ln (inverse z) = - Ln z

goal (1 subgoal):
 1. z = 0 \<Longrightarrow> Ln (inverse z) = - Ln z
[PROOF STEP]
qed (use assms in auto)