[STATEMENT]
lemma Ln_minus_ii [simp]: "Ln(-\<i>) = - (\<i> * pi/2)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Ln (- \<i>) = - (\<i> * complex_of_real pi / 2)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. Ln (- \<i>) = - (\<i> * complex_of_real pi / 2)
[PROOF STEP]
have  "Ln(-\<i>) = Ln(inverse \<i>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Ln (- \<i>) = Ln (inverse \<i>)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
Ln (- \<i>) = Ln (inverse \<i>)

goal (1 subgoal):
 1. Ln (- \<i>) = - (\<i> * complex_of_real pi / 2)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
Ln (- \<i>) = Ln (inverse \<i>)

goal (1 subgoal):
 1. Ln (- \<i>) = - (\<i> * complex_of_real pi / 2)
[PROOF STEP]
have "\<dots> = - (Ln \<i>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Ln (inverse \<i>) = - Ln \<i>
[PROOF STEP]
using Ln_inverse
[PROOF STATE]
proof (prove)
using this:
?z \<notin> \<real>\<^sub>\<le>\<^sub>0 \<Longrightarrow> Ln (inverse ?z) = - Ln ?z

goal (1 subgoal):
 1. Ln (inverse \<i>) = - Ln \<i>
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
Ln (inverse \<i>) = - Ln \<i>

goal (1 subgoal):
 1. Ln (- \<i>) = - (\<i> * complex_of_real pi / 2)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
Ln (inverse \<i>) = - Ln \<i>

goal (1 subgoal):
 1. Ln (- \<i>) = - (\<i> * complex_of_real pi / 2)
[PROOF STEP]
have "\<dots> = - (\<i> * pi/2)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. - Ln \<i> = - (\<i> * complex_of_real pi / 2)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
- Ln \<i> = - (\<i> * complex_of_real pi / 2)

goal (1 subgoal):
 1. Ln (- \<i>) = - (\<i> * complex_of_real pi / 2)
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
Ln (- \<i>) = - (\<i> * complex_of_real pi / 2)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
Ln (- \<i>) = - (\<i> * complex_of_real pi / 2)

goal (1 subgoal):
 1. Ln (- \<i>) = - (\<i> * complex_of_real pi / 2)
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
Ln (- \<i>) = - (\<i> * complex_of_real pi / 2)

goal:
No subgoals!
[PROOF STEP]
qed