[STATEMENT]
lemma twice_field_differentiable_at_power [simp, intro]:
  "(\<lambda>x. x ^ n) twice_field_differentiable_at x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>x. x ^ n) twice_field_differentiable_at x
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (\<lambda>x. x ^ n) twice_field_differentiable_at x
[PROOF STEP]
have "\<forall>x\<in>UNIV. (\<lambda>x. x ^ n) field_differentiable at x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>x\<in>UNIV. (\<lambda>x. x ^ n) field_differentiable at x
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<forall>x\<in>UNIV. (\<lambda>x. x ^ n) field_differentiable at x

goal (1 subgoal):
 1. (\<lambda>x. x ^ n) twice_field_differentiable_at x
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
\<forall>x\<in>UNIV. (\<lambda>x. x ^ n) field_differentiable at x

goal (1 subgoal):
 1. (\<lambda>x. x ^ n) twice_field_differentiable_at x
[PROOF STEP]
have "deriv ((\<lambda>x. x ^ n)) field_differentiable at x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. deriv (\<lambda>x. x ^ n) field_differentiable at x
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. deriv (\<lambda>x. x ^ n) field_differentiable at x
[PROOF STEP]
have "deriv ((\<lambda>x. x ^ n)) = (\<lambda>x. of_nat n * x ^ (n - 1))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. deriv (\<lambda>x. x ^ n) = (\<lambda>x. of_nat n * x ^ (n - 1))
[PROOF STEP]
by (simp add: ext)
[PROOF STATE]
proof (state)
this:
deriv (\<lambda>x. x ^ n) = (\<lambda>x. of_nat n * x ^ (n - 1))

goal (1 subgoal):
 1. deriv (\<lambda>x. x ^ n) field_differentiable at x
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
deriv (\<lambda>x. x ^ n) = (\<lambda>x. of_nat n * x ^ (n - 1))
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
deriv (\<lambda>x. x ^ n) = (\<lambda>x. of_nat n * x ^ (n - 1))

goal (1 subgoal):
 1. deriv (\<lambda>x. x ^ n) field_differentiable at x
[PROOF STEP]
using field_differentiable_mult[of "\<lambda>x. of_nat n" x UNIV "\<lambda>x. x ^ (n - 1)"]
[PROOF STATE]
proof (prove)
using this:
deriv (\<lambda>x. x ^ n) = (\<lambda>x. of_nat n * x ^ (n - 1))
\<lbrakk>(\<lambda>x. of_nat n) field_differentiable at x; (\<lambda>x. x ^ (n - 1)) field_differentiable at x\<rbrakk> \<Longrightarrow> (\<lambda>z. of_nat n * z ^ (n - 1)) field_differentiable at x

goal (1 subgoal):
 1. deriv (\<lambda>x. x ^ n) field_differentiable at x
[PROOF STEP]
by (simp add: field_differentiable_caratheodory_at)
[PROOF STATE]
proof (state)
this:
deriv (\<lambda>x. x ^ n) field_differentiable at x

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
deriv (\<lambda>x. x ^ n) field_differentiable at x

goal (1 subgoal):
 1. (\<lambda>x. x ^ n) twice_field_differentiable_at x
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
\<forall>x\<in>UNIV. (\<lambda>x. x ^ n) field_differentiable at x
deriv (\<lambda>x. x ^ n) field_differentiable at x
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<forall>x\<in>UNIV. (\<lambda>x. x ^ n) field_differentiable at x
deriv (\<lambda>x. x ^ n) field_differentiable at x

goal (1 subgoal):
 1. (\<lambda>x. x ^ n) twice_field_differentiable_at x
[PROOF STEP]
unfolding twice_field_differentiable_at_def field_differentiable_on_def
[PROOF STATE]
proof (prove)
using this:
\<forall>x\<in>UNIV. (\<lambda>x. x ^ n) field_differentiable at x
deriv (\<lambda>x. x ^ n) field_differentiable at x

goal (1 subgoal):
 1. \<exists>S. (\<forall>x\<in>S. (\<lambda>x. x ^ n) field_differentiable at x within S) \<and> x \<in> interior S \<and> deriv (\<lambda>x. x ^ n) field_differentiable at x
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
(\<lambda>x. x ^ n) twice_field_differentiable_at x

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma twice_field_differentiable_at_power_fun [intro]:
  assumes "f twice_field_differentiable_at x"
    shows "(\<lambda>x. f x ^ n) twice_field_differentiable_at x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>x. f x ^ n) twice_field_differentiable_at x
[PROOF STEP]
by (blast intro: assms twice_field_differentiable_at_compose [OF _ twice_field_differentiable_at_power])


[STATEMENT]
lemma eventually_deriv_inverse:
  assumes "x \<noteq> 0"
    shows "\<forall>\<^sub>F x in nhds x. deriv inverse x = - 1 / (x ^ 2)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>\<^sub>F x in nhds x. deriv inverse x = - (1::'a) / x\<^sup>2
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<forall>\<^sub>F x in nhds x. deriv inverse x = - (1::'a) / x\<^sup>2
[PROOF STEP]
obtain T where open_T: "open T" and "\<forall>z\<in>T. z \<noteq> 0" and x_in_T: "x \<in> T"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>T. \<lbrakk>open T; \<forall>z\<in>T. z \<noteq> (0::'a); x \<in> T\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using assms t1_space
[PROOF STATE]
proof (prove)
using this:
x \<noteq> (0::'a)
?x \<noteq> ?y \<Longrightarrow> \<exists>U. open U \<and> ?x \<in> U \<and> ?y \<notin> U

goal (1 subgoal):
 1. (\<And>T. \<lbrakk>open T; \<forall>z\<in>T. z \<noteq> (0::'a); x \<in> T\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
open T
\<forall>z\<in>T. z \<noteq> (0::'a)
x \<in> T

goal (1 subgoal):
 1. \<forall>\<^sub>F x in nhds x. deriv inverse x = - (1::'a) / x\<^sup>2
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
open T
\<forall>z\<in>T. z \<noteq> (0::'a)
x \<in> T
[PROOF STEP]
have "\<forall>x \<in> T. deriv inverse x = - 1 / (x ^ 2)"
[PROOF STATE]
proof (prove)
using this:
open T
\<forall>z\<in>T. z \<noteq> (0::'a)
x \<in> T

goal (1 subgoal):
 1. \<forall>x\<in>T. deriv inverse x = - (1::'a) / x\<^sup>2
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<forall>x\<in>T. deriv inverse x = - (1::'a) / x\<^sup>2

goal (1 subgoal):
 1. \<forall>\<^sub>F x in nhds x. deriv inverse x = - (1::'a) / x\<^sup>2
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<forall>x\<in>T. deriv inverse x = - (1::'a) / x\<^sup>2
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<forall>x\<in>T. deriv inverse x = - (1::'a) / x\<^sup>2

goal (1 subgoal):
 1. \<forall>\<^sub>F x in nhds x. deriv inverse x = - (1::'a) / x\<^sup>2
[PROOF STEP]
using eventually_nhds open_T x_in_T
[PROOF STATE]
proof (prove)
using this:
\<forall>x\<in>T. deriv inverse x = - (1::'a) / x\<^sup>2
eventually ?P (nhds ?a) = (\<exists>S. open S \<and> ?a \<in> S \<and> (\<forall>x\<in>S. ?P x))
open T
x \<in> T

goal (1 subgoal):
 1. \<forall>\<^sub>F x in nhds x. deriv inverse x = - (1::'a) / x\<^sup>2
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<forall>\<^sub>F x in nhds x. deriv inverse x = - (1::'a) / x\<^sup>2

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma deriv_deriv_inverse [simp]:
  assumes "x \<noteq> 0"
  shows "deriv (deriv inverse) x = 2 * inverse (x ^ 3)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. deriv (deriv inverse) x = (2::'a) * inverse (x ^ 3)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. deriv (deriv inverse) x = (2::'a) * inverse (x ^ 3)
[PROOF STEP]
have "deriv (\<lambda>x. inverse (x ^ 2)) x = - (of_nat 2 * x) / ((x ^ 2) ^ 2)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. deriv (\<lambda>x. inverse (x\<^sup>2)) x = - (of_nat 2 * x) / (x\<^sup>2)\<^sup>2
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
x \<noteq> (0::'a)

goal (1 subgoal):
 1. deriv (\<lambda>x. inverse (x\<^sup>2)) x = - (of_nat 2 * x) / (x\<^sup>2)\<^sup>2
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
deriv (\<lambda>x. inverse (x\<^sup>2)) x = - (of_nat 2 * x) / (x\<^sup>2)\<^sup>2

goal (1 subgoal):
 1. deriv (deriv inverse) x = (2::'a) * inverse (x ^ 3)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
deriv (\<lambda>x. inverse (x\<^sup>2)) x = - (of_nat 2 * x) / (x\<^sup>2)\<^sup>2

goal (1 subgoal):
 1. deriv (deriv inverse) x = (2::'a) * inverse (x ^ 3)
[PROOF STEP]
have "(\<lambda>x. inverse (x ^ 2)) field_differentiable at x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>x. inverse (x\<^sup>2)) field_differentiable at x
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
x \<noteq> (0::'a)

goal (1 subgoal):
 1. (\<lambda>x. inverse (x\<^sup>2)) field_differentiable at x
[PROOF STEP]
by (simp add: field_differentiable_inverse)
[PROOF STATE]
proof (state)
this:
(\<lambda>x. inverse (x\<^sup>2)) field_differentiable at x

goal (1 subgoal):
 1. deriv (deriv inverse) x = (2::'a) * inverse (x ^ 3)
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
deriv (\<lambda>x. inverse (x\<^sup>2)) x = - (of_nat 2 * x) / (x\<^sup>2)\<^sup>2
(\<lambda>x. inverse (x\<^sup>2)) field_differentiable at x
[PROOF STEP]
have "deriv (\<lambda>x. - (inverse (x ^ 2))) x = of_nat 2 * x / (x ^ 4)"
[PROOF STATE]
proof (prove)
using this:
deriv (\<lambda>x. inverse (x\<^sup>2)) x = - (of_nat 2 * x) / (x\<^sup>2)\<^sup>2
(\<lambda>x. inverse (x\<^sup>2)) field_differentiable at x

goal (1 subgoal):
 1. deriv (\<lambda>x. - inverse (x\<^sup>2)) x = of_nat 2 * x / x ^ 4
[PROOF STEP]
using deriv_chain[of "\<lambda>x. inverse (x ^ 2)" x]
[PROOF STATE]
proof (prove)
using this:
deriv (\<lambda>x. inverse (x\<^sup>2)) x = - (of_nat 2 * x) / (x\<^sup>2)\<^sup>2
(\<lambda>x. inverse (x\<^sup>2)) field_differentiable at x
\<lbrakk>(\<lambda>x. inverse (x\<^sup>2)) field_differentiable at x; ?g field_differentiable at (inverse (x\<^sup>2))\<rbrakk> \<Longrightarrow> deriv (?g \<circ> (\<lambda>x. inverse (x\<^sup>2))) x = deriv ?g (inverse (x\<^sup>2)) * deriv (\<lambda>x. inverse (x\<^sup>2)) x

goal (1 subgoal):
 1. deriv (\<lambda>x. - inverse (x\<^sup>2)) x = of_nat 2 * x / x ^ 4
[PROOF STEP]
by (simp add: comp_def field_differentiable_minus field_simps)
[PROOF STATE]
proof (state)
this:
deriv (\<lambda>x. - inverse (x\<^sup>2)) x = of_nat 2 * x / x ^ 4

goal (1 subgoal):
 1. deriv (deriv inverse) x = (2::'a) * inverse (x ^ 3)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
deriv (\<lambda>x. - inverse (x\<^sup>2)) x = of_nat 2 * x / x ^ 4
[PROOF STEP]
have "deriv (\<lambda>x. - 1 / (x ^ 2)) x = 2 * inverse (x ^ 3)"
[PROOF STATE]
proof (prove)
using this:
deriv (\<lambda>x. - inverse (x\<^sup>2)) x = of_nat 2 * x / x ^ 4

goal (1 subgoal):
 1. deriv (\<lambda>x. - (1::'a) / x\<^sup>2) x = (2::'a) * inverse (x ^ 3)
[PROOF STEP]
by (simp add: power4_eq_xxxx power3_eq_cube field_simps)
[PROOF STATE]
proof (state)
this:
deriv (\<lambda>x. - (1::'a) / x\<^sup>2) x = (2::'a) * inverse (x ^ 3)

goal (1 subgoal):
 1. deriv (deriv inverse) x = (2::'a) * inverse (x ^ 3)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
deriv (\<lambda>x. - (1::'a) / x\<^sup>2) x = (2::'a) * inverse (x ^ 3)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
deriv (\<lambda>x. - (1::'a) / x\<^sup>2) x = (2::'a) * inverse (x ^ 3)

goal (1 subgoal):
 1. deriv (deriv inverse) x = (2::'a) * inverse (x ^ 3)
[PROOF STEP]
using assms eventually_deriv_inverse deriv_cong_ev
[PROOF STATE]
proof (prove)
using this:
deriv (\<lambda>x. - (1::'a) / x\<^sup>2) x = (2::'a) * inverse (x ^ 3)
x \<noteq> (0::'a)
?x \<noteq> (0::?'a) \<Longrightarrow> \<forall>\<^sub>F x in nhds ?x. deriv inverse x = - (1::?'a) / x\<^sup>2
\<lbrakk>\<forall>\<^sub>F x in nhds ?x. ?f x = ?g x; ?x = ?y\<rbrakk> \<Longrightarrow> deriv ?f ?x = deriv ?g ?y

goal (1 subgoal):
 1. deriv (deriv inverse) x = (2::'a) * inverse (x ^ 3)
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
deriv (deriv inverse) x = (2::'a) * inverse (x ^ 3)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma twice_field_differentiable_at_inverse [simp, intro]:
  assumes "x \<noteq> 0"
  shows "inverse twice_field_differentiable_at x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. inverse twice_field_differentiable_at x
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. inverse twice_field_differentiable_at x
[PROOF STEP]
obtain T where zero_T: "0 \<notin> T" and x_in_T: "x \<in> T" and open_T: "open T"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>T. \<lbrakk>(0::'a) \<notin> T; x \<in> T; open T\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using assms t1_space
[PROOF STATE]
proof (prove)
using this:
x \<noteq> (0::'a)
?x \<noteq> ?y \<Longrightarrow> \<exists>U. open U \<and> ?x \<in> U \<and> ?y \<notin> U

goal (1 subgoal):
 1. (\<And>T. \<lbrakk>(0::'a) \<notin> T; x \<in> T; open T\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
(0::'a) \<notin> T
x \<in> T
open T

goal (1 subgoal):
 1. inverse twice_field_differentiable_at x
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
(0::'a) \<notin> T
x \<in> T
open T
[PROOF STEP]
have "T \<subseteq> {z. z \<noteq> 0}"
[PROOF STATE]
proof (prove)
using this:
(0::'a) \<notin> T
x \<in> T
open T

goal (1 subgoal):
 1. T \<subseteq> {z. z \<noteq> (0::'a)}
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
T \<subseteq> {z. z \<noteq> (0::'a)}

goal (1 subgoal):
 1. inverse twice_field_differentiable_at x
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
T \<subseteq> {z. z \<noteq> (0::'a)}
[PROOF STEP]
have "\<forall>x\<in>T. inverse field_differentiable at x within T"
[PROOF STATE]
proof (prove)
using this:
T \<subseteq> {z. z \<noteq> (0::'a)}

goal (1 subgoal):
 1. \<forall>x\<in>T. inverse field_differentiable at x within T
[PROOF STEP]
using DERIV_inverse field_differentiable_def
[PROOF STATE]
proof (prove)
using this:
T \<subseteq> {z. z \<noteq> (0::'a)}
?x \<noteq> (0::?'a) \<Longrightarrow> (inverse has_field_derivative - (inverse ?x ^ Suc (Suc 0))) (at ?x within ?s)
?f field_differentiable ?F \<equiv> \<exists>f'. (?f has_field_derivative f') ?F

goal (1 subgoal):
 1. \<forall>x\<in>T. inverse field_differentiable at x within T
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<forall>x\<in>T. inverse field_differentiable at x within T

goal (1 subgoal):
 1. inverse twice_field_differentiable_at x
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
\<forall>x\<in>T. inverse field_differentiable at x within T

goal (1 subgoal):
 1. inverse twice_field_differentiable_at x
[PROOF STEP]
have "deriv inverse field_differentiable at x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. deriv inverse field_differentiable at x
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. deriv inverse field_differentiable at x
[PROOF STEP]
have "(\<lambda>x. - inverse (x ^ 2)) field_differentiable at x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>x. - inverse (x\<^sup>2)) field_differentiable at x
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
x \<noteq> (0::'a)

goal (1 subgoal):
 1. (\<lambda>x. - inverse (x\<^sup>2)) field_differentiable at x
[PROOF STEP]
by (simp add: field_differentiable_inverse field_differentiable_minus)
[PROOF STATE]
proof (state)
this:
(\<lambda>x. - inverse (x\<^sup>2)) field_differentiable at x

goal (1 subgoal):
 1. deriv inverse field_differentiable at x
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
(\<lambda>x. - inverse (x\<^sup>2)) field_differentiable at x
[PROOF STEP]
have "(\<lambda>x. - 1 / (x ^ 2)) field_differentiable at x"
[PROOF STATE]
proof (prove)
using this:
(\<lambda>x. - inverse (x\<^sup>2)) field_differentiable at x

goal (1 subgoal):
 1. (\<lambda>x. - (1::'a) / x\<^sup>2) field_differentiable at x
[PROOF STEP]
by (simp add: inverse_eq_divide)
[PROOF STATE]
proof (state)
this:
(\<lambda>x. - (1::'a) / x\<^sup>2) field_differentiable at x

goal (1 subgoal):
 1. deriv inverse field_differentiable at x
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
(\<lambda>x. - (1::'a) / x\<^sup>2) field_differentiable at x
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
(\<lambda>x. - (1::'a) / x\<^sup>2) field_differentiable at x

goal (1 subgoal):
 1. deriv inverse field_differentiable at x
[PROOF STEP]
using eventually_deriv_inverse[OF assms]
[PROOF STATE]
proof (prove)
using this:
(\<lambda>x. - (1::'a) / x\<^sup>2) field_differentiable at x
\<forall>\<^sub>F x in nhds x. deriv inverse x = - (1::'a) / x\<^sup>2

goal (1 subgoal):
 1. deriv inverse field_differentiable at x
[PROOF STEP]
by (simp add: DERIV_cong_ev field_differentiable_def)
[PROOF STATE]
proof (state)
this:
deriv inverse field_differentiable at x

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
deriv inverse field_differentiable at x

goal (1 subgoal):
 1. inverse twice_field_differentiable_at x
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
deriv inverse field_differentiable at x

goal (1 subgoal):
 1. inverse twice_field_differentiable_at x
[PROOF STEP]
have "x \<in> interior T"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x \<in> interior T
[PROOF STEP]
by (simp add: x_in_T open_T interior_open)
[PROOF STATE]
proof (state)
this:
x \<in> interior T

goal (1 subgoal):
 1. inverse twice_field_differentiable_at x
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
\<forall>x\<in>T. inverse field_differentiable at x within T
deriv inverse field_differentiable at x
x \<in> interior T
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<forall>x\<in>T. inverse field_differentiable at x within T
deriv inverse field_differentiable at x
x \<in> interior T

goal (1 subgoal):
 1. inverse twice_field_differentiable_at x
[PROOF STEP]
unfolding twice_field_differentiable_at_def field_differentiable_on_def
[PROOF STATE]
proof (prove)
using this:
\<forall>x\<in>T. inverse field_differentiable at x within T
deriv inverse field_differentiable at x
x \<in> interior T

goal (1 subgoal):
 1. \<exists>S. (\<forall>x\<in>S. inverse field_differentiable at x within S) \<and> x \<in> interior S \<and> deriv inverse field_differentiable at x
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
inverse twice_field_differentiable_at x

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma twice_field_differentiable_at_inverse_fun [simp, intro]:
  assumes "f twice_field_differentiable_at x"
          "f x \<noteq> 0"
  shows "(\<lambda>x. inverse (f x)) twice_field_differentiable_at x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>x. inverse (f x)) twice_field_differentiable_at x
[PROOF STEP]
by (simp add: assms twice_field_differentiable_at_compose)


[STATEMENT]
lemma twice_field_differentiable_at_divide [intro]:
  assumes "f twice_field_differentiable_at x"
      and "g twice_field_differentiable_at x"
      and "g x \<noteq> 0"
    shows "(\<lambda>x. f x / g x) twice_field_differentiable_at x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>x. f x / g x) twice_field_differentiable_at x
[PROOF STEP]
by (simp add: assms divide_inverse twice_field_differentiable_at_mult)


[STATEMENT]
lemma twice_field_differentiable_at_polyn [simp, intro]:
  fixes coef :: "nat \<Rightarrow> 'a :: {real_normed_field}"
    and n :: nat
  shows "(\<lambda>x. \<Sum>i<n. coef i * x ^ i) twice_field_differentiable_at x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>x. \<Sum>i<n. coef i * x ^ i) twice_field_differentiable_at x
[PROOF STEP]
proof (induction n)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. (\<lambda>x. \<Sum>i<0. coef i * x ^ i) twice_field_differentiable_at x
 2. \<And>n. (\<lambda>x. \<Sum>i<n. coef i * x ^ i) twice_field_differentiable_at x \<Longrightarrow> (\<lambda>x. \<Sum>i<Suc n. coef i * x ^ i) twice_field_differentiable_at x
[PROOF STEP]
case 0
[PROOF STATE]
proof (state)
this:

goal (2 subgoals):
 1. (\<lambda>x. \<Sum>i<0. coef i * x ^ i) twice_field_differentiable_at x
 2. \<And>n. (\<lambda>x. \<Sum>i<n. coef i * x ^ i) twice_field_differentiable_at x \<Longrightarrow> (\<lambda>x. \<Sum>i<Suc n. coef i * x ^ i) twice_field_differentiable_at x
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>x. \<Sum>i<0. coef i * x ^ i) twice_field_differentiable_at x
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
(\<lambda>x. \<Sum>i<0. coef i * x ^ i) twice_field_differentiable_at x

goal (1 subgoal):
 1. \<And>n. (\<lambda>x. \<Sum>i<n. coef i * x ^ i) twice_field_differentiable_at x \<Longrightarrow> (\<lambda>x. \<Sum>i<Suc n. coef i * x ^ i) twice_field_differentiable_at x
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>n. (\<lambda>x. \<Sum>i<n. coef i * x ^ i) twice_field_differentiable_at x \<Longrightarrow> (\<lambda>x. \<Sum>i<Suc n. coef i * x ^ i) twice_field_differentiable_at x
[PROOF STEP]
case hyp: (Suc n)
[PROOF STATE]
proof (state)
this:
(\<lambda>x. \<Sum>i<n. coef i * x ^ i) twice_field_differentiable_at x

goal (1 subgoal):
 1. \<And>n. (\<lambda>x. \<Sum>i<n. coef i * x ^ i) twice_field_differentiable_at x \<Longrightarrow> (\<lambda>x. \<Sum>i<Suc n. coef i * x ^ i) twice_field_differentiable_at x
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>x. \<Sum>i<Suc n. coef i * x ^ i) twice_field_differentiable_at x
[PROOF STEP]
proof (simp, rule twice_field_differentiable_at_add)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. (\<lambda>x. \<Sum>i<n. coef i * x ^ i) twice_field_differentiable_at x
 2. (\<lambda>x. coef n * x ^ n) twice_field_differentiable_at x
[PROOF STEP]
show "(\<lambda>x. \<Sum>i<n. coef i * x ^ i) twice_field_differentiable_at x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>x. \<Sum>i<n. coef i * x ^ i) twice_field_differentiable_at x
[PROOF STEP]
by (rule hyp)
[PROOF STATE]
proof (state)
this:
(\<lambda>x. \<Sum>i<n. coef i * x ^ i) twice_field_differentiable_at x

goal (1 subgoal):
 1. (\<lambda>x. coef n * x ^ n) twice_field_differentiable_at x
[PROOF STEP]
show "(\<lambda>x. coef n * x ^ n) twice_field_differentiable_at x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>x. coef n * x ^ n) twice_field_differentiable_at x
[PROOF STEP]
using twice_field_differentiable_at_compose[of "\<lambda>x. x ^ n" x "(*) (coef n)"]
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>(\<lambda>x. x ^ n) twice_field_differentiable_at x; (*) (coef n) twice_field_differentiable_at x ^ n\<rbrakk> \<Longrightarrow> (\<lambda>x. coef n * x ^ n) twice_field_differentiable_at x

goal (1 subgoal):
 1. (\<lambda>x. coef n * x ^ n) twice_field_differentiable_at x
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
(\<lambda>x. coef n * x ^ n) twice_field_differentiable_at x

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
(\<lambda>x. \<Sum>i<Suc n. coef i * x ^ i) twice_field_differentiable_at x

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma twice_field_differentiable_at_polyn_fun [simp]:
  fixes coef :: "nat \<Rightarrow> 'a :: {real_normed_field}"
    and n :: nat
  assumes "f twice_field_differentiable_at x"
  shows "(\<lambda>x. \<Sum>i<n. coef i * f x ^ i) twice_field_differentiable_at x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>x. \<Sum>i<n. coef i * f x ^ i) twice_field_differentiable_at x
[PROOF STEP]
by (blast intro: assms twice_field_differentiable_at_compose [OF _ twice_field_differentiable_at_polyn])


[STATEMENT]
lemma  (in interval) trans2:"\<lbrakk>p\<parallel>t; t\<parallel>r; r\<parallel>q\<rbrakk> \<Longrightarrow> \<not>p\<parallel>q"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>p \<parallel> t; t \<parallel> r; r \<parallel> q\<rbrakk> \<Longrightarrow> \<not> p \<parallel> q
[PROOF STEP]
using M1 meets_asym
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?p \<parallel> ?q; ?p \<parallel> ?s; ?r \<parallel> ?q\<rbrakk> \<Longrightarrow> ?r \<parallel> ?s
?p \<parallel> ?q \<Longrightarrow> \<not> ?q \<parallel> ?p

goal (1 subgoal):
 1. \<lbrakk>p \<parallel> t; t \<parallel> r; r \<parallel> q\<rbrakk> \<Longrightarrow> \<not> p \<parallel> q
[PROOF STEP]
by blast


[STATEMENT]
lemma (in interval) nontrans2:"u\<parallel>r \<Longrightarrow> \<not> (\<exists>t. r\<parallel>t \<and> t\<parallel>u)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. u \<parallel> r \<Longrightarrow> \<nexists>t. r \<parallel> t \<and> t \<parallel> u
[PROOF STEP]
using M1 M5exist trans2
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?p \<parallel> ?q; ?p \<parallel> ?s; ?r \<parallel> ?q\<rbrakk> \<Longrightarrow> ?r \<parallel> ?s
?p \<parallel> ?q \<Longrightarrow> \<exists>r s t. r \<parallel> ?p \<and> ?p \<parallel> ?q \<and> ?q \<parallel> s \<and> r \<parallel> t \<and> t \<parallel> s
\<lbrakk>?p \<parallel> ?t; ?t \<parallel> ?r; ?r \<parallel> ?q\<rbrakk> \<Longrightarrow> \<not> ?p \<parallel> ?q

goal (1 subgoal):
 1. u \<parallel> r \<Longrightarrow> \<nexists>t. r \<parallel> t \<and> t \<parallel> u
[PROOF STEP]
by blast


[STATEMENT]
lemma (in interval) nonmeets1:"\<not> (u\<parallel>r \<and> r\<parallel>u)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<not> (u \<parallel> r \<and> r \<parallel> u)
[PROOF STEP]
using meets_asym
[PROOF STATE]
proof (prove)
using this:
?p \<parallel> ?q \<Longrightarrow> \<not> ?q \<parallel> ?p

goal (1 subgoal):
 1. \<not> (u \<parallel> r \<and> r \<parallel> u)
[PROOF STEP]
by blast


[STATEMENT]
lemma (in interval)  nonmeets2: "\<lbrakk>\<I> u ; \<I> r \<rbrakk> \<Longrightarrow> \<not> (u\<parallel>r \<and> u = r)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<I> u; \<I> r\<rbrakk> \<Longrightarrow> \<not> (u \<parallel> r \<and> u = r)
[PROOF STEP]
using meets_irrefl
[PROOF STATE]
proof (prove)
using this:
\<I> ?p \<Longrightarrow> \<not> ?p \<parallel> ?p

goal (1 subgoal):
 1. \<lbrakk>\<I> u; \<I> r\<rbrakk> \<Longrightarrow> \<not> (u \<parallel> r \<and> u = r)
[PROOF STEP]
by blast


[STATEMENT]
lemma (in interval) nonmeets3: "\<not> (u\<parallel>r \<and> (\<exists>p. u\<parallel>p \<and> p\<parallel>r))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<not> (u \<parallel> r \<and> (\<exists>p. u \<parallel> p \<and> p \<parallel> r))
[PROOF STEP]
using nontrans1
[PROOF STATE]
proof (prove)
using this:
?u \<parallel> ?r \<Longrightarrow> \<nexists>t. ?u \<parallel> t \<and> t \<parallel> ?r

goal (1 subgoal):
 1. \<not> (u \<parallel> r \<and> (\<exists>p. u \<parallel> p \<and> p \<parallel> r))
[PROOF STEP]
by blast


[STATEMENT]
lemma (in interval) nonmeets4: "\<not>(u\<parallel>r \<and> (\<exists>p. r\<parallel>p \<and> p\<parallel>u))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<not> (u \<parallel> r \<and> (\<exists>p. r \<parallel> p \<and> p \<parallel> u))
[PROOF STEP]
using nontrans2
[PROOF STATE]
proof (prove)
using this:
?u \<parallel> ?r \<Longrightarrow> \<nexists>t. ?r \<parallel> t \<and> t \<parallel> ?u

goal (1 subgoal):
 1. \<not> (u \<parallel> r \<and> (\<exists>p. r \<parallel> p \<and> p \<parallel> u))
[PROOF STEP]
by blast


[STATEMENT]
lemma (in interval) elimmeets: "(p \<parallel> s \<and> (\<exists>t. p \<parallel> t \<and> t \<parallel> s) \<and> (\<exists>t. r \<parallel> t \<and> t \<parallel> q)) = False"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (p \<parallel> s \<and> (\<exists>t. p \<parallel> t \<and> t \<parallel> s) \<and> (\<exists>t. r \<parallel> t \<and> t \<parallel> q)) = False
[PROOF STEP]
using meets_atrans
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?p \<parallel> ?q; ?q \<parallel> ?r\<rbrakk> \<Longrightarrow> \<not> ?p \<parallel> ?r

goal (1 subgoal):
 1. (p \<parallel> s \<and> (\<exists>t. p \<parallel> t \<and> t \<parallel> s) \<and> (\<exists>t. r \<parallel> t \<and> t \<parallel> q)) = False
[PROOF STEP]
by blast


[STATEMENT]
lemma (in interval) M5exist_var:
assumes "x\<parallel>y" "y\<parallel>z" "z\<parallel>w"
shows "\<exists>t. x\<parallel>t \<and> t\<parallel>w"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>t. x \<parallel> t \<and> t \<parallel> w
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>t. x \<parallel> t \<and> t \<parallel> w
[PROOF STEP]
from assms(1,3)
[PROOF STATE]
proof (chain)
picking this:
x \<parallel> y
z \<parallel> w
[PROOF STEP]
have a:"x\<parallel>w \<oplus> (\<exists>t. x\<parallel>t \<and> t\<parallel>w) \<oplus> (\<exists>t. z\<parallel>t \<and> t\<parallel>y)"
[PROOF STATE]
proof (prove)
using this:
x \<parallel> y
z \<parallel> w

goal (1 subgoal):
 1. x \<parallel> w \<oplus> (\<exists>t. x \<parallel> t \<and> t \<parallel> w) \<oplus> (\<exists>t. z \<parallel> t \<and> t \<parallel> y)
[PROOF STEP]
using M2[of x y z w]
[PROOF STATE]
proof (prove)
using this:
x \<parallel> y
z \<parallel> w
\<lbrakk>x \<parallel> y; z \<parallel> w\<rbrakk> \<Longrightarrow> x \<parallel> w \<oplus> ((\<exists>t. x \<parallel> t \<and> t \<parallel> w) \<oplus> (\<exists>t. z \<parallel> t \<and> t \<parallel> y))

goal (1 subgoal):
 1. x \<parallel> w \<oplus> (\<exists>t. x \<parallel> t \<and> t \<parallel> w) \<oplus> (\<exists>t. z \<parallel> t \<and> t \<parallel> y)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
x \<parallel> w \<oplus> (\<exists>t. x \<parallel> t \<and> t \<parallel> w) \<oplus> (\<exists>t. z \<parallel> t \<and> t \<parallel> y)

goal (1 subgoal):
 1. \<exists>t. x \<parallel> t \<and> t \<parallel> w
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
x \<parallel> y
y \<parallel> z
z \<parallel> w
[PROOF STEP]
have b1:"\<not>x\<parallel>w"
[PROOF STATE]
proof (prove)
using this:
x \<parallel> y
y \<parallel> z
z \<parallel> w

goal (1 subgoal):
 1. \<not> x \<parallel> w
[PROOF STEP]
using trans2
[PROOF STATE]
proof (prove)
using this:
x \<parallel> y
y \<parallel> z
z \<parallel> w
\<lbrakk>?p \<parallel> ?t; ?t \<parallel> ?r; ?r \<parallel> ?q\<rbrakk> \<Longrightarrow> \<not> ?p \<parallel> ?q

goal (1 subgoal):
 1. \<not> x \<parallel> w
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<not> x \<parallel> w

goal (1 subgoal):
 1. \<exists>t. x \<parallel> t \<and> t \<parallel> w
[PROOF STEP]
from assms(2)
[PROOF STATE]
proof (chain)
picking this:
y \<parallel> z
[PROOF STEP]
have "\<not> (\<exists>t. z\<parallel>t \<and> t\<parallel>y)"
[PROOF STATE]
proof (prove)
using this:
y \<parallel> z

goal (1 subgoal):
 1. \<nexists>t. z \<parallel> t \<and> t \<parallel> y
[PROOF STEP]
by (simp add: nontrans2)
[PROOF STATE]
proof (state)
this:
\<nexists>t. z \<parallel> t \<and> t \<parallel> y

goal (1 subgoal):
 1. \<exists>t. x \<parallel> t \<and> t \<parallel> w
[PROOF STEP]
with b1 a
[PROOF STATE]
proof (chain)
picking this:
\<not> x \<parallel> w
x \<parallel> w \<oplus> (\<exists>t. x \<parallel> t \<and> t \<parallel> w) \<oplus> (\<exists>t. z \<parallel> t \<and> t \<parallel> y)
\<nexists>t. z \<parallel> t \<and> t \<parallel> y
[PROOF STEP]
have " (\<exists>t. x\<parallel>t \<and> t\<parallel>w)"
[PROOF STATE]
proof (prove)
using this:
\<not> x \<parallel> w
x \<parallel> w \<oplus> (\<exists>t. x \<parallel> t \<and> t \<parallel> w) \<oplus> (\<exists>t. z \<parallel> t \<and> t \<parallel> y)
\<nexists>t. z \<parallel> t \<and> t \<parallel> y

goal (1 subgoal):
 1. \<exists>t. x \<parallel> t \<and> t \<parallel> w
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<exists>t. x \<parallel> t \<and> t \<parallel> w

goal (1 subgoal):
 1. \<exists>t. x \<parallel> t \<and> t \<parallel> w
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
\<exists>t. x \<parallel> t \<and> t \<parallel> w

goal (1 subgoal):
 1. \<exists>t. x \<parallel> t \<and> t \<parallel> w
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<exists>t. x \<parallel> t \<and> t \<parallel> w

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma (in interval) M5exist_var2:
assumes "p\<parallel>q"
shows "\<exists>r1 r2 r3 s t. r1\<parallel>r2 \<and> r2\<parallel>r3 \<and> r3\<parallel>p \<and> p\<parallel>q \<and> q\<parallel>s \<and> r1\<parallel>t \<and> t\<parallel>s"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>r1 r2 r3 s t. r1 \<parallel> r2 \<and> r2 \<parallel> r3 \<and> r3 \<parallel> p \<and> p \<parallel> q \<and> q \<parallel> s \<and> r1 \<parallel> t \<and> t \<parallel> s
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>r1 r2 r3 s t. r1 \<parallel> r2 \<and> r2 \<parallel> r3 \<and> r3 \<parallel> p \<and> p \<parallel> q \<and> q \<parallel> s \<and> r1 \<parallel> t \<and> t \<parallel> s
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
p \<parallel> q
[PROOF STEP]
obtain r3 k1 s  where r3p:"r3\<parallel>p" and  qs:"q\<parallel>s"  and  r3k1:"r3 \<parallel>k1"  and  k1s:"k1\<parallel>s"
[PROOF STATE]
proof (prove)
using this:
p \<parallel> q

goal (1 subgoal):
 1. (\<And>r3 s k1. \<lbrakk>r3 \<parallel> p; q \<parallel> s; r3 \<parallel> k1; k1 \<parallel> s\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using M5exist
[PROOF STATE]
proof (prove)
using this:
p \<parallel> q
?p \<parallel> ?q \<Longrightarrow> \<exists>r s t. r \<parallel> ?p \<and> ?p \<parallel> ?q \<and> ?q \<parallel> s \<and> r \<parallel> t \<and> t \<parallel> s

goal (1 subgoal):
 1. (\<And>r3 s k1. \<lbrakk>r3 \<parallel> p; q \<parallel> s; r3 \<parallel> k1; k1 \<parallel> s\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
r3 \<parallel> p
q \<parallel> s
r3 \<parallel> k1
k1 \<parallel> s

goal (1 subgoal):
 1. \<exists>r1 r2 r3 s t. r1 \<parallel> r2 \<and> r2 \<parallel> r3 \<and> r3 \<parallel> p \<and> p \<parallel> q \<and> q \<parallel> s \<and> r1 \<parallel> t \<and> t \<parallel> s
[PROOF STEP]
from r3p
[PROOF STATE]
proof (chain)
picking this:
r3 \<parallel> p
[PROOF STEP]
obtain r2 where r2r3:"r2\<parallel>r3"
[PROOF STATE]
proof (prove)
using this:
r3 \<parallel> p

goal (1 subgoal):
 1. (\<And>r2. r2 \<parallel> r3 \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using M3[of r3] meets_wd
[PROOF STATE]
proof (prove)
using this:
r3 \<parallel> p
\<I> r3 \<Longrightarrow> \<exists>q r. q \<parallel> r3 \<and> r3 \<parallel> r
?p \<parallel> ?q \<Longrightarrow> \<I> ?p \<and> \<I> ?q

goal (1 subgoal):
 1. (\<And>r2. r2 \<parallel> r3 \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
r2 \<parallel> r3

goal (1 subgoal):
 1. \<exists>r1 r2 r3 s t. r1 \<parallel> r2 \<and> r2 \<parallel> r3 \<and> r3 \<parallel> p \<and> p \<parallel> q \<and> q \<parallel> s \<and> r1 \<parallel> t \<and> t \<parallel> s
[PROOF STEP]
from r2r3
[PROOF STATE]
proof (chain)
picking this:
r2 \<parallel> r3
[PROOF STEP]
obtain r1 where r1r2:"r1\<parallel>r2"
[PROOF STATE]
proof (prove)
using this:
r2 \<parallel> r3

goal (1 subgoal):
 1. (\<And>r1. r1 \<parallel> r2 \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using M3[of r2] meets_wd
[PROOF STATE]
proof (prove)
using this:
r2 \<parallel> r3
\<I> r2 \<Longrightarrow> \<exists>q r. q \<parallel> r2 \<and> r2 \<parallel> r
?p \<parallel> ?q \<Longrightarrow> \<I> ?p \<and> \<I> ?q

goal (1 subgoal):
 1. (\<And>r1. r1 \<parallel> r2 \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
r1 \<parallel> r2

goal (1 subgoal):
 1. \<exists>r1 r2 r3 s t. r1 \<parallel> r2 \<and> r2 \<parallel> r3 \<and> r3 \<parallel> p \<and> p \<parallel> q \<and> q \<parallel> s \<and> r1 \<parallel> t \<and> t \<parallel> s
[PROOF STEP]
with  assms  r2r3 r3p qs
[PROOF STATE]
proof (chain)
picking this:
p \<parallel> q
r2 \<parallel> r3
r3 \<parallel> p
q \<parallel> s
r1 \<parallel> r2
[PROOF STEP]
obtain t where r1t1:"r1\<parallel>t" and t1q:"t\<parallel>s"
[PROOF STATE]
proof (prove)
using this:
p \<parallel> q
r2 \<parallel> r3
r3 \<parallel> p
q \<parallel> s
r1 \<parallel> r2

goal (1 subgoal):
 1. (\<And>t. \<lbrakk>r1 \<parallel> t; t \<parallel> s\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using M5exist_var
[PROOF STATE]
proof (prove)
using this:
p \<parallel> q
r2 \<parallel> r3
r3 \<parallel> p
q \<parallel> s
r1 \<parallel> r2
\<lbrakk>?x \<parallel> ?y; ?y \<parallel> ?z; ?z \<parallel> ?w\<rbrakk> \<Longrightarrow> \<exists>t. ?x \<parallel> t \<and> t \<parallel> ?w

goal (1 subgoal):
 1. (\<And>t. \<lbrakk>r1 \<parallel> t; t \<parallel> s\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
r1 \<parallel> t
t \<parallel> s

goal (1 subgoal):
 1. \<exists>r1 r2 r3 s t. r1 \<parallel> r2 \<and> r2 \<parallel> r3 \<and> r3 \<parallel> p \<and> p \<parallel> q \<and> q \<parallel> s \<and> r1 \<parallel> t \<and> t \<parallel> s
[PROOF STEP]
with assms r1r2 r2r3 r3p qs
[PROOF STATE]
proof (chain)
picking this:
p \<parallel> q
r1 \<parallel> r2
r2 \<parallel> r3
r3 \<parallel> p
q \<parallel> s
r1 \<parallel> t
t \<parallel> s
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
p \<parallel> q
r1 \<parallel> r2
r2 \<parallel> r3
r3 \<parallel> p
q \<parallel> s
r1 \<parallel> t
t \<parallel> s

goal (1 subgoal):
 1. \<exists>r1 r2 r3 s t. r1 \<parallel> r2 \<and> r2 \<parallel> r3 \<and> r3 \<parallel> p \<and> p \<parallel> q \<and> q \<parallel> s \<and> r1 \<parallel> t \<and> t \<parallel> s
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<exists>r1 r2 r3 s t. r1 \<parallel> r2 \<and> r2 \<parallel> r3 \<and> r3 \<parallel> p \<and> p \<parallel> q \<and> q \<parallel> s \<and> r1 \<parallel> t \<and> t \<parallel> s

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma (in interval) M5exist_var3:
assumes "k\<parallel>l" and "l\<parallel>q" and "q\<parallel>t" and "t\<parallel>r"
shows  "\<exists>lqt. k\<parallel>lqt \<and> lqt\<parallel>r"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>lqt. k \<parallel> lqt \<and> lqt \<parallel> r
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>lqt. k \<parallel> lqt \<and> lqt \<parallel> r
[PROOF STEP]
from assms(1-3)
[PROOF STATE]
proof (chain)
picking this:
k \<parallel> l
l \<parallel> q
q \<parallel> t
[PROOF STEP]
obtain lq where "k\<parallel>lq" and "lq\<parallel>t"
[PROOF STATE]
proof (prove)
using this:
k \<parallel> l
l \<parallel> q
q \<parallel> t

goal (1 subgoal):
 1. (\<And>lq. \<lbrakk>k \<parallel> lq; lq \<parallel> t\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using M5exist_var
[PROOF STATE]
proof (prove)
using this:
k \<parallel> l
l \<parallel> q
q \<parallel> t
\<lbrakk>?x \<parallel> ?y; ?y \<parallel> ?z; ?z \<parallel> ?w\<rbrakk> \<Longrightarrow> \<exists>t. ?x \<parallel> t \<and> t \<parallel> ?w

goal (1 subgoal):
 1. (\<And>lq. \<lbrakk>k \<parallel> lq; lq \<parallel> t\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
k \<parallel> lq
lq \<parallel> t

goal (1 subgoal):
 1. \<exists>lqt. k \<parallel> lqt \<and> lqt \<parallel> r
[PROOF STEP]
with assms(4)
[PROOF STATE]
proof (chain)
picking this:
t \<parallel> r
k \<parallel> lq
lq \<parallel> t
[PROOF STEP]
obtain lqt where "k\<parallel>lqt" and "lqt\<parallel>r"
[PROOF STATE]
proof (prove)
using this:
t \<parallel> r
k \<parallel> lq
lq \<parallel> t

goal (1 subgoal):
 1. (\<And>lqt. \<lbrakk>k \<parallel> lqt; lqt \<parallel> r\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using M5exist_var
[PROOF STATE]
proof (prove)
using this:
t \<parallel> r
k \<parallel> lq
lq \<parallel> t
\<lbrakk>?x \<parallel> ?y; ?y \<parallel> ?z; ?z \<parallel> ?w\<rbrakk> \<Longrightarrow> \<exists>t. ?x \<parallel> t \<and> t \<parallel> ?w

goal (1 subgoal):
 1. (\<And>lqt. \<lbrakk>k \<parallel> lqt; lqt \<parallel> r\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
k \<parallel> lqt
lqt \<parallel> r

goal (1 subgoal):
 1. \<exists>lqt. k \<parallel> lqt \<and> lqt \<parallel> r
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
k \<parallel> lqt
lqt \<parallel> r

goal (1 subgoal):
 1. \<exists>lqt. k \<parallel> lqt \<and> lqt \<parallel> r
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<exists>lqt. k \<parallel> lqt \<and> lqt \<parallel> r

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma (in Corps) OstrowskiTr8:"\<lbrakk>valuation K v; x \<in> carrier K;
      0 < v (1\<^sub>r \<plusminus> -\<^sub>a x)\<rbrakk> \<Longrightarrow>
      0 < (v (1\<^sub>r \<plusminus> -\<^sub>a (x \<cdot>\<^sub>r ((1\<^sub>r \<plusminus> x \<cdot>\<^sub>r (1\<^sub>r \<plusminus> -\<^sub>a x))\<^bsup>\<hyphen>K\<^esup>))))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>valuation K v; x \<in> carrier K; 0 < v (1\<^sub>r \<plusminus> -\<^sub>a x)\<rbrakk> \<Longrightarrow> 0 < v (1\<^sub>r \<plusminus> -\<^sub>a x \<cdot>\<^sub>r (1\<^sub>r \<plusminus> x \<cdot>\<^sub>r (1\<^sub>r \<plusminus> -\<^sub>a x))\<^bsup>\<hyphen> K\<^esup>)
[PROOF STEP]
apply (cut_tac field_is_ring, frule Ring.ring_is_ag[of "K"])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>valuation K v; x \<in> carrier K; 0 < v (1\<^sub>r \<plusminus> -\<^sub>a x); Ring K; aGroup K\<rbrakk> \<Longrightarrow> 0 < v (1\<^sub>r \<plusminus> -\<^sub>a x \<cdot>\<^sub>r (1\<^sub>r \<plusminus> x \<cdot>\<^sub>r (1\<^sub>r \<plusminus> -\<^sub>a x))\<^bsup>\<hyphen> K\<^esup>)
[PROOF STEP]
apply (frule aGroup.ag_mOp_closed[of "K" "x"], assumption+,
       frule Ring.ring_one[of "K"],
       frule aGroup.ag_pOp_closed[of "K" "1\<^sub>r" " -\<^sub>a x"], assumption+,
       frule OstrowskiTr32[of v x], assumption+)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>valuation K v; x \<in> carrier K; 0 < v (1\<^sub>r \<plusminus> -\<^sub>a x); Ring K; aGroup K; -\<^sub>a x \<in> carrier K; 1\<^sub>r \<in> carrier K; 1\<^sub>r \<plusminus> -\<^sub>a x \<in> carrier K; 0 \<le> v x\<rbrakk> \<Longrightarrow> 0 < v (1\<^sub>r \<plusminus> -\<^sub>a x \<cdot>\<^sub>r (1\<^sub>r \<plusminus> x \<cdot>\<^sub>r (1\<^sub>r \<plusminus> -\<^sub>a x))\<^bsup>\<hyphen> K\<^esup>)
[PROOF STEP]
apply (case_tac "x = 1\<^sub>r\<^bsub>K\<^esub>", simp,
       simp add:aGroup.ag_r_inv1, simp add:Ring.ring_times_x_0,
       simp add:aGroup.ag_r_zero, cut_tac val_field_1_neq_0,
       cut_tac invf_one, simp, simp add:Ring.ring_r_one,
       simp add:aGroup.ag_r_inv1, assumption+)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>valuation K v; x \<in> carrier K; 0 < v (1\<^sub>r \<plusminus> -\<^sub>a x); Ring K; aGroup K; -\<^sub>a x \<in> carrier K; 1\<^sub>r \<in> carrier K; 1\<^sub>r \<plusminus> -\<^sub>a x \<in> carrier K; 0 \<le> v x; x \<noteq> 1\<^sub>r\<rbrakk> \<Longrightarrow> 0 < v (1\<^sub>r \<plusminus> -\<^sub>a x \<cdot>\<^sub>r (1\<^sub>r \<plusminus> x \<cdot>\<^sub>r (1\<^sub>r \<plusminus> -\<^sub>a x))\<^bsup>\<hyphen> K\<^esup>)
[PROOF STEP]
apply (frule aGroup.ag_pOp_closed[of K "1\<^sub>r" "x \<cdot>\<^sub>r (1\<^sub>r \<plusminus> -\<^sub>a x)"], assumption+,
       rule Ring.ring_tOp_closed, assumption+)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>valuation K v; x \<in> carrier K; 0 < v (1\<^sub>r \<plusminus> -\<^sub>a x); Ring K; aGroup K; -\<^sub>a x \<in> carrier K; 1\<^sub>r \<in> carrier K; 1\<^sub>r \<plusminus> -\<^sub>a x \<in> carrier K; 0 \<le> v x; x \<noteq> 1\<^sub>r; 1\<^sub>r \<plusminus> x \<cdot>\<^sub>r (1\<^sub>r \<plusminus> -\<^sub>a x) \<in> carrier K\<rbrakk> \<Longrightarrow> 0 < v (1\<^sub>r \<plusminus> -\<^sub>a x \<cdot>\<^sub>r (1\<^sub>r \<plusminus> x \<cdot>\<^sub>r (1\<^sub>r \<plusminus> -\<^sub>a x))\<^bsup>\<hyphen> K\<^esup>)
[PROOF STEP]
apply (cut_tac invf_closed[of "1\<^sub>r \<plusminus> x \<cdot>\<^sub>r (1\<^sub>r \<plusminus> -\<^sub>a x)"])
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>valuation K v; x \<in> carrier K; 0 < v (1\<^sub>r \<plusminus> -\<^sub>a x); Ring K; aGroup K; -\<^sub>a x \<in> carrier K; 1\<^sub>r \<in> carrier K; 1\<^sub>r \<plusminus> -\<^sub>a x \<in> carrier K; 0 \<le> v x; x \<noteq> 1\<^sub>r; 1\<^sub>r \<plusminus> x \<cdot>\<^sub>r (1\<^sub>r \<plusminus> -\<^sub>a x) \<in> carrier K; (1\<^sub>r \<plusminus> x \<cdot>\<^sub>r (1\<^sub>r \<plusminus> -\<^sub>a x))\<^bsup>\<hyphen> K\<^esup> \<in> carrier K\<rbrakk> \<Longrightarrow> 0 < v (1\<^sub>r \<plusminus> -\<^sub>a x \<cdot>\<^sub>r (1\<^sub>r \<plusminus> x \<cdot>\<^sub>r (1\<^sub>r \<plusminus> -\<^sub>a x))\<^bsup>\<hyphen> K\<^esup>)
 2. \<lbrakk>valuation K v; x \<in> carrier K; 0 < v (1\<^sub>r \<plusminus> -\<^sub>a x); Ring K; aGroup K; -\<^sub>a x \<in> carrier K; 1\<^sub>r \<in> carrier K; 1\<^sub>r \<plusminus> -\<^sub>a x \<in> carrier K; 0 \<le> v x; x \<noteq> 1\<^sub>r; 1\<^sub>r \<plusminus> x \<cdot>\<^sub>r (1\<^sub>r \<plusminus> -\<^sub>a x) \<in> carrier K\<rbrakk> \<Longrightarrow> 1\<^sub>r \<plusminus> x \<cdot>\<^sub>r (1\<^sub>r \<plusminus> -\<^sub>a x) \<in> carrier K - {\<zero>}
[PROOF STEP]
apply (cut_tac field_one_plus_frac3[of x], simp del:npow_suc,
        subst val_t2p[of v], assumption+)
[PROOF STATE]
proof (prove)
goal (7 subgoals):
 1. \<lbrakk>valuation K v; x \<in> carrier K; 0 < v (1\<^sub>r \<plusminus> -\<^sub>a x); Ring K; aGroup K; -\<^sub>a x \<in> carrier K; 1\<^sub>r \<in> carrier K; 1\<^sub>r \<plusminus> -\<^sub>a x \<in> carrier K; 0 \<le> v x; x \<noteq> 1\<^sub>r; 1\<^sub>r \<plusminus> x \<cdot>\<^sub>r (1\<^sub>r \<plusminus> -\<^sub>a x) \<in> carrier K; (1\<^sub>r \<plusminus> x \<cdot>\<^sub>r (1\<^sub>r \<plusminus> -\<^sub>a x))\<^bsup>\<hyphen> K\<^esup> \<in> carrier K; 1\<^sub>r \<plusminus> -\<^sub>a x \<cdot>\<^sub>r (1\<^sub>r \<plusminus> x \<cdot>\<^sub>r (1\<^sub>r \<plusminus> -\<^sub>a x))\<^bsup>\<hyphen> K\<^esup> = (1\<^sub>r \<plusminus> -\<^sub>a x^\<^bsup>K Suc (Suc 0)\<^esup>) \<cdot>\<^sub>r (1\<^sub>r \<plusminus> x \<cdot>\<^sub>r (1\<^sub>r \<plusminus> -\<^sub>a x))\<^bsup>\<hyphen> K\<^esup>\<rbrakk> \<Longrightarrow> 1\<^sub>r \<plusminus> -\<^sub>a x^\<^bsup>K Suc (Suc 0)\<^esup> \<in> carrier K
 2. \<lbrakk>valuation K v; x \<in> carrier K; 0 < v (1\<^sub>r \<plusminus> -\<^sub>a x); Ring K; aGroup K; -\<^sub>a x \<in> carrier K; 1\<^sub>r \<in> carrier K; 1\<^sub>r \<plusminus> -\<^sub>a x \<in> carrier K; 0 \<le> v x; x \<noteq> 1\<^sub>r; 1\<^sub>r \<plusminus> x \<cdot>\<^sub>r (1\<^sub>r \<plusminus> -\<^sub>a x) \<in> carrier K; (1\<^sub>r \<plusminus> x \<cdot>\<^sub>r (1\<^sub>r \<plusminus> -\<^sub>a x))\<^bsup>\<hyphen> K\<^esup> \<in> carrier K; 1\<^sub>r \<plusminus> -\<^sub>a x \<cdot>\<^sub>r (1\<^sub>r \<plusminus> x \<cdot>\<^sub>r (1\<^sub>r \<plusminus> -\<^sub>a x))\<^bsup>\<hyphen> K\<^esup> = (1\<^sub>r \<plusminus> -\<^sub>a x^\<^bsup>K Suc (Suc 0)\<^esup>) \<cdot>\<^sub>r (1\<^sub>r \<plusminus> x \<cdot>\<^sub>r (1\<^sub>r \<plusminus> -\<^sub>a x))\<^bsup>\<hyphen> K\<^esup>\<rbrakk> \<Longrightarrow> (1\<^sub>r \<plusminus> x \<cdot>\<^sub>r (1\<^sub>r \<plusminus> -\<^sub>a x))\<^bsup>\<hyphen> K\<^esup> \<in> carrier K
 3. \<lbrakk>valuation K v; x \<in> carrier K; 0 < v (1\<^sub>r \<plusminus> -\<^sub>a x); Ring K; aGroup K; -\<^sub>a x \<in> carrier K; 1\<^sub>r \<in> carrier K; 1\<^sub>r \<plusminus> -\<^sub>a x \<in> carrier K; 0 \<le> v x; x \<noteq> 1\<^sub>r; 1\<^sub>r \<plusminus> x \<cdot>\<^sub>r (1\<^sub>r \<plusminus> -\<^sub>a x) \<in> carrier K; (1\<^sub>r \<plusminus> x \<cdot>\<^sub>r (1\<^sub>r \<plusminus> -\<^sub>a x))\<^bsup>\<hyphen> K\<^esup> \<in> carrier K; 1\<^sub>r \<plusminus> -\<^sub>a x \<cdot>\<^sub>r (1\<^sub>r \<plusminus> x \<cdot>\<^sub>r (1\<^sub>r \<plusminus> -\<^sub>a x))\<^bsup>\<hyphen> K\<^esup> = (1\<^sub>r \<plusminus> -\<^sub>a x^\<^bsup>K Suc (Suc 0)\<^esup>) \<cdot>\<^sub>r (1\<^sub>r \<plusminus> x \<cdot>\<^sub>r (1\<^sub>r \<plusminus> -\<^sub>a x))\<^bsup>\<hyphen> K\<^esup>\<rbrakk> \<Longrightarrow> 0 < v (1\<^sub>r \<plusminus> -\<^sub>a x^\<^bsup>K Suc (Suc 0)\<^esup>) + v ((1\<^sub>r \<plusminus> x \<cdot>\<^sub>r (1\<^sub>r \<plusminus> -\<^sub>a x))\<^bsup>\<hyphen> K\<^esup>)
 4. \<lbrakk>valuation K v; x \<in> carrier K; 0 < v (1\<^sub>r \<plusminus> -\<^sub>a x); Ring K; aGroup K; -\<^sub>a x \<in> carrier K; 1\<^sub>r \<in> carrier K; 1\<^sub>r \<plusminus> -\<^sub>a x \<in> carrier K; 0 \<le> v x; x \<noteq> 1\<^sub>r; 1\<^sub>r \<plusminus> x \<cdot>\<^sub>r (1\<^sub>r \<plusminus> -\<^sub>a x) \<in> carrier K; (1\<^sub>r \<plusminus> x \<cdot>\<^sub>r (1\<^sub>r \<plusminus> -\<^sub>a x))\<^bsup>\<hyphen> K\<^esup> \<in> carrier K\<rbrakk> \<Longrightarrow> x \<in> carrier K
 5. \<lbrakk>valuation K v; x \<in> carrier K; 0 < v (1\<^sub>r \<plusminus> -\<^sub>a x); Ring K; aGroup K; -\<^sub>a x \<in> carrier K; 1\<^sub>r \<in> carrier K; 1\<^sub>r \<plusminus> -\<^sub>a x \<in> carrier K; 0 \<le> v x; x \<noteq> 1\<^sub>r; 1\<^sub>r \<plusminus> x \<cdot>\<^sub>r (1\<^sub>r \<plusminus> -\<^sub>a x) \<in> carrier K; (1\<^sub>r \<plusminus> x \<cdot>\<^sub>r (1\<^sub>r \<plusminus> -\<^sub>a x))\<^bsup>\<hyphen> K\<^esup> \<in> carrier K\<rbrakk> \<Longrightarrow> x \<noteq> 1\<^sub>r
 6. \<lbrakk>valuation K v; x \<in> carrier K; 0 < v (1\<^sub>r \<plusminus> -\<^sub>a x); Ring K; aGroup K; -\<^sub>a x \<in> carrier K; 1\<^sub>r \<in> carrier K; 1\<^sub>r \<plusminus> -\<^sub>a x \<in> carrier K; 0 \<le> v x; x \<noteq> 1\<^sub>r; 1\<^sub>r \<plusminus> x \<cdot>\<^sub>r (1\<^sub>r \<plusminus> -\<^sub>a x) \<in> carrier K; (1\<^sub>r \<plusminus> x \<cdot>\<^sub>r (1\<^sub>r \<plusminus> -\<^sub>a x))\<^bsup>\<hyphen> K\<^esup> \<in> carrier K\<rbrakk> \<Longrightarrow> 1\<^sub>r \<plusminus> x \<cdot>\<^sub>r (1\<^sub>r \<plusminus> -\<^sub>a x) \<noteq> \<zero>
 7. \<lbrakk>valuation K v; x \<in> carrier K; 0 < v (1\<^sub>r \<plusminus> -\<^sub>a x); Ring K; aGroup K; -\<^sub>a x \<in> carrier K; 1\<^sub>r \<in> carrier K; 1\<^sub>r \<plusminus> -\<^sub>a x \<in> carrier K; 0 \<le> v x; x \<noteq> 1\<^sub>r; 1\<^sub>r \<plusminus> x \<cdot>\<^sub>r (1\<^sub>r \<plusminus> -\<^sub>a x) \<in> carrier K\<rbrakk> \<Longrightarrow> 1\<^sub>r \<plusminus> x \<cdot>\<^sub>r (1\<^sub>r \<plusminus> -\<^sub>a x) \<in> carrier K - {\<zero>}
[PROOF STEP]
apply (rule aGroup.ag_pOp_closed, assumption+,
        rule aGroup.ag_mOp_closed, assumption+, rule Ring.npClose,
        assumption+,
        thin_tac "1\<^sub>r \<plusminus> -\<^sub>a x \<cdot>\<^sub>r (1\<^sub>r \<plusminus> x \<cdot>\<^sub>r (1\<^sub>r \<plusminus> -\<^sub>a x))\<^bsup>\<hyphen> K\<^esup> =
        (1\<^sub>r \<plusminus> -\<^sub>a x^\<^bsup>K (Suc (Suc 0))\<^esup>) \<cdot>\<^sub>r (1\<^sub>r \<plusminus> x \<cdot>\<^sub>r (1\<^sub>r \<plusminus> -\<^sub>a x))\<^bsup>\<hyphen> K\<^esup>",
        subgoal_tac "1\<^sub>r \<plusminus> -\<^sub>a x^\<^bsup>K (Suc (Suc 0))\<^esup> = (1\<^sub>r \<plusminus> x) \<cdot>\<^sub>r (1\<^sub>r \<plusminus> -\<^sub>a x)",
        simp del:npow_suc,
        thin_tac "1\<^sub>r \<plusminus> -\<^sub>a x^\<^bsup>K (Suc (Suc 0))\<^esup> = (1\<^sub>r \<plusminus> x) \<cdot>\<^sub>r (1\<^sub>r \<plusminus> -\<^sub>a x)")
[PROOF STATE]
proof (prove)
goal (6 subgoals):
 1. \<lbrakk>valuation K v; x \<in> carrier K; 0 < v (1\<^sub>r \<plusminus> -\<^sub>a x); Ring K; aGroup K; -\<^sub>a x \<in> carrier K; 1\<^sub>r \<in> carrier K; 1\<^sub>r \<plusminus> -\<^sub>a x \<in> carrier K; 0 \<le> v x; x \<noteq> 1\<^sub>r; 1\<^sub>r \<plusminus> x \<cdot>\<^sub>r (1\<^sub>r \<plusminus> -\<^sub>a x) \<in> carrier K; (1\<^sub>r \<plusminus> x \<cdot>\<^sub>r (1\<^sub>r \<plusminus> -\<^sub>a x))\<^bsup>\<hyphen> K\<^esup> \<in> carrier K\<rbrakk> \<Longrightarrow> 0 < v ((1\<^sub>r \<plusminus> x) \<cdot>\<^sub>r (1\<^sub>r \<plusminus> -\<^sub>a x)) + v ((1\<^sub>r \<plusminus> x \<cdot>\<^sub>r (1\<^sub>r \<plusminus> -\<^sub>a x))\<^bsup>\<hyphen> K\<^esup>)
 2. \<lbrakk>valuation K v; x \<in> carrier K; 0 < v (1\<^sub>r \<plusminus> -\<^sub>a x); Ring K; aGroup K; -\<^sub>a x \<in> carrier K; 1\<^sub>r \<in> carrier K; 1\<^sub>r \<plusminus> -\<^sub>a x \<in> carrier K; 0 \<le> v x; x \<noteq> 1\<^sub>r; 1\<^sub>r \<plusminus> x \<cdot>\<^sub>r (1\<^sub>r \<plusminus> -\<^sub>a x) \<in> carrier K; (1\<^sub>r \<plusminus> x \<cdot>\<^sub>r (1\<^sub>r \<plusminus> -\<^sub>a x))\<^bsup>\<hyphen> K\<^esup> \<in> carrier K\<rbrakk> \<Longrightarrow> 1\<^sub>r \<plusminus> -\<^sub>a x^\<^bsup>K Suc (Suc 0)\<^esup> = (1\<^sub>r \<plusminus> x) \<cdot>\<^sub>r (1\<^sub>r \<plusminus> -\<^sub>a x)
 3. \<lbrakk>valuation K v; x \<in> carrier K; 0 < v (1\<^sub>r \<plusminus> -\<^sub>a x); Ring K; aGroup K; -\<^sub>a x \<in> carrier K; 1\<^sub>r \<in> carrier K; 1\<^sub>r \<plusminus> -\<^sub>a x \<in> carrier K; 0 \<le> v x; x \<noteq> 1\<^sub>r; 1\<^sub>r \<plusminus> x \<cdot>\<^sub>r (1\<^sub>r \<plusminus> -\<^sub>a x) \<in> carrier K; (1\<^sub>r \<plusminus> x \<cdot>\<^sub>r (1\<^sub>r \<plusminus> -\<^sub>a x))\<^bsup>\<hyphen> K\<^esup> \<in> carrier K\<rbrakk> \<Longrightarrow> x \<in> carrier K
 4. \<lbrakk>valuation K v; x \<in> carrier K; 0 < v (1\<^sub>r \<plusminus> -\<^sub>a x); Ring K; aGroup K; -\<^sub>a x \<in> carrier K; 1\<^sub>r \<in> carrier K; 1\<^sub>r \<plusminus> -\<^sub>a x \<in> carrier K; 0 \<le> v x; x \<noteq> 1\<^sub>r; 1\<^sub>r \<plusminus> x \<cdot>\<^sub>r (1\<^sub>r \<plusminus> -\<^sub>a x) \<in> carrier K; (1\<^sub>r \<plusminus> x \<cdot>\<^sub>r (1\<^sub>r \<plusminus> -\<^sub>a x))\<^bsup>\<hyphen> K\<^esup> \<in> carrier K\<rbrakk> \<Longrightarrow> x \<noteq> 1\<^sub>r
 5. \<lbrakk>valuation K v; x \<in> carrier K; 0 < v (1\<^sub>r \<plusminus> -\<^sub>a x); Ring K; aGroup K; -\<^sub>a x \<in> carrier K; 1\<^sub>r \<in> carrier K; 1\<^sub>r \<plusminus> -\<^sub>a x \<in> carrier K; 0 \<le> v x; x \<noteq> 1\<^sub>r; 1\<^sub>r \<plusminus> x \<cdot>\<^sub>r (1\<^sub>r \<plusminus> -\<^sub>a x) \<in> carrier K; (1\<^sub>r \<plusminus> x \<cdot>\<^sub>r (1\<^sub>r \<plusminus> -\<^sub>a x))\<^bsup>\<hyphen> K\<^esup> \<in> carrier K\<rbrakk> \<Longrightarrow> 1\<^sub>r \<plusminus> x \<cdot>\<^sub>r (1\<^sub>r \<plusminus> -\<^sub>a x) \<noteq> \<zero>
 6. \<lbrakk>valuation K v; x \<in> carrier K; 0 < v (1\<^sub>r \<plusminus> -\<^sub>a x); Ring K; aGroup K; -\<^sub>a x \<in> carrier K; 1\<^sub>r \<in> carrier K; 1\<^sub>r \<plusminus> -\<^sub>a x \<in> carrier K; 0 \<le> v x; x \<noteq> 1\<^sub>r; 1\<^sub>r \<plusminus> x \<cdot>\<^sub>r (1\<^sub>r \<plusminus> -\<^sub>a x) \<in> carrier K\<rbrakk> \<Longrightarrow> 1\<^sub>r \<plusminus> x \<cdot>\<^sub>r (1\<^sub>r \<plusminus> -\<^sub>a x) \<in> carrier K - {\<zero>}
[PROOF STEP]
apply (subst val_t2p[of v], assumption+,
        rule aGroup.ag_pOp_closed, assumption+,
        subst value_of_inv[of v "1\<^sub>r \<plusminus> x \<cdot>\<^sub>r (1\<^sub>r \<plusminus> -\<^sub>a x)"], tactic \<open>CHANGED distinct_subgoals_tac\<close>, assumption+)
[PROOF STATE]
proof (prove)
goal (6 subgoals):
 1. \<lbrakk>valuation K v; x \<in> carrier K; 0 < v (1\<^sub>r \<plusminus> -\<^sub>a x); Ring K; aGroup K; -\<^sub>a x \<in> carrier K; 1\<^sub>r \<in> carrier K; 1\<^sub>r \<plusminus> -\<^sub>a x \<in> carrier K; 0 \<le> v x; x \<noteq> 1\<^sub>r; 1\<^sub>r \<plusminus> x \<cdot>\<^sub>r (1\<^sub>r \<plusminus> -\<^sub>a x) \<in> carrier K; (1\<^sub>r \<plusminus> x \<cdot>\<^sub>r (1\<^sub>r \<plusminus> -\<^sub>a x))\<^bsup>\<hyphen> K\<^esup> \<in> carrier K\<rbrakk> \<Longrightarrow> 1\<^sub>r \<plusminus> x \<cdot>\<^sub>r (1\<^sub>r \<plusminus> -\<^sub>a x) \<noteq> \<zero>
 2. \<lbrakk>valuation K v; x \<in> carrier K; 0 < v (1\<^sub>r \<plusminus> -\<^sub>a x); Ring K; aGroup K; -\<^sub>a x \<in> carrier K; 1\<^sub>r \<in> carrier K; 1\<^sub>r \<plusminus> -\<^sub>a x \<in> carrier K; 0 \<le> v x; x \<noteq> 1\<^sub>r; 1\<^sub>r \<plusminus> x \<cdot>\<^sub>r (1\<^sub>r \<plusminus> -\<^sub>a x) \<in> carrier K; (1\<^sub>r \<plusminus> x \<cdot>\<^sub>r (1\<^sub>r \<plusminus> -\<^sub>a x))\<^bsup>\<hyphen> K\<^esup> \<in> carrier K\<rbrakk> \<Longrightarrow> 0 < v (1\<^sub>r \<plusminus> x) + v (1\<^sub>r \<plusminus> -\<^sub>a x) + - v (1\<^sub>r \<plusminus> x \<cdot>\<^sub>r (1\<^sub>r \<plusminus> -\<^sub>a x))
 3. \<lbrakk>valuation K v; x \<in> carrier K; 0 < v (1\<^sub>r \<plusminus> -\<^sub>a x); Ring K; aGroup K; -\<^sub>a x \<in> carrier K; 1\<^sub>r \<in> carrier K; 1\<^sub>r \<plusminus> -\<^sub>a x \<in> carrier K; 0 \<le> v x; x \<noteq> 1\<^sub>r; 1\<^sub>r \<plusminus> x \<cdot>\<^sub>r (1\<^sub>r \<plusminus> -\<^sub>a x) \<in> carrier K; (1\<^sub>r \<plusminus> x \<cdot>\<^sub>r (1\<^sub>r \<plusminus> -\<^sub>a x))\<^bsup>\<hyphen> K\<^esup> \<in> carrier K\<rbrakk> \<Longrightarrow> 1\<^sub>r \<plusminus> -\<^sub>a x^\<^bsup>K Suc (Suc 0)\<^esup> = (1\<^sub>r \<plusminus> x) \<cdot>\<^sub>r (1\<^sub>r \<plusminus> -\<^sub>a x)
 4. \<lbrakk>valuation K v; x \<in> carrier K; 0 < v (1\<^sub>r \<plusminus> -\<^sub>a x); Ring K; aGroup K; -\<^sub>a x \<in> carrier K; 1\<^sub>r \<in> carrier K; 1\<^sub>r \<plusminus> -\<^sub>a x \<in> carrier K; 0 \<le> v x; x \<noteq> 1\<^sub>r; 1\<^sub>r \<plusminus> x \<cdot>\<^sub>r (1\<^sub>r \<plusminus> -\<^sub>a x) \<in> carrier K; (1\<^sub>r \<plusminus> x \<cdot>\<^sub>r (1\<^sub>r \<plusminus> -\<^sub>a x))\<^bsup>\<hyphen> K\<^esup> \<in> carrier K\<rbrakk> \<Longrightarrow> x \<in> carrier K
 5. \<lbrakk>valuation K v; x \<in> carrier K; 0 < v (1\<^sub>r \<plusminus> -\<^sub>a x); Ring K; aGroup K; -\<^sub>a x \<in> carrier K; 1\<^sub>r \<in> carrier K; 1\<^sub>r \<plusminus> -\<^sub>a x \<in> carrier K; 0 \<le> v x; x \<noteq> 1\<^sub>r; 1\<^sub>r \<plusminus> x \<cdot>\<^sub>r (1\<^sub>r \<plusminus> -\<^sub>a x) \<in> carrier K; (1\<^sub>r \<plusminus> x \<cdot>\<^sub>r (1\<^sub>r \<plusminus> -\<^sub>a x))\<^bsup>\<hyphen> K\<^esup> \<in> carrier K\<rbrakk> \<Longrightarrow> x \<noteq> 1\<^sub>r
 6. \<lbrakk>valuation K v; x \<in> carrier K; 0 < v (1\<^sub>r \<plusminus> -\<^sub>a x); Ring K; aGroup K; -\<^sub>a x \<in> carrier K; 1\<^sub>r \<in> carrier K; 1\<^sub>r \<plusminus> -\<^sub>a x \<in> carrier K; 0 \<le> v x; x \<noteq> 1\<^sub>r; 1\<^sub>r \<plusminus> x \<cdot>\<^sub>r (1\<^sub>r \<plusminus> -\<^sub>a x) \<in> carrier K\<rbrakk> \<Longrightarrow> 1\<^sub>r \<plusminus> x \<cdot>\<^sub>r (1\<^sub>r \<plusminus> -\<^sub>a x) \<in> carrier K - {\<zero>}
[PROOF STEP]
apply (rule contrapos_pp, simp+,
        frule Ring.ring_tOp_closed[of K x "(1\<^sub>r \<plusminus> -\<^sub>a x)"], assumption+,
        simp add:aGroup.ag_pOp_commute[of K "1\<^sub>r"],
        frule aGroup.ag_eq_diffzero[THEN sym, of K "x \<cdot>\<^sub>r (-\<^sub>a x \<plusminus> 1\<^sub>r)" "-\<^sub>a 1\<^sub>r"],
        assumption+, rule aGroup.ag_mOp_closed, assumption+)
[PROOF STATE]
proof (prove)
goal (6 subgoals):
 1. \<lbrakk>valuation K v; x \<in> carrier K; 0 < v (-\<^sub>a x \<plusminus> 1\<^sub>r); Ring K; aGroup K; -\<^sub>a x \<in> carrier K; 1\<^sub>r \<in> carrier K; -\<^sub>a x \<plusminus> 1\<^sub>r \<in> carrier K; 0 \<le> v x; x \<noteq> 1\<^sub>r; \<zero> \<in> carrier K; \<zero>\<^bsup>\<hyphen> K\<^esup> \<in> carrier K; x \<cdot>\<^sub>r (-\<^sub>a x \<plusminus> 1\<^sub>r) \<plusminus> 1\<^sub>r = \<zero>; x \<cdot>\<^sub>r (-\<^sub>a x \<plusminus> 1\<^sub>r) \<in> carrier K; (x \<cdot>\<^sub>r (-\<^sub>a x \<plusminus> 1\<^sub>r) \<plusminus> -\<^sub>a (-\<^sub>a 1\<^sub>r) = \<zero>) = (x \<cdot>\<^sub>r (-\<^sub>a x \<plusminus> 1\<^sub>r) = -\<^sub>a 1\<^sub>r)\<rbrakk> \<Longrightarrow> False
 2. \<lbrakk>valuation K v; x \<in> carrier K; 0 < v (1\<^sub>r \<plusminus> -\<^sub>a x); Ring K; aGroup K; -\<^sub>a x \<in> carrier K; 1\<^sub>r \<in> carrier K; 1\<^sub>r \<plusminus> -\<^sub>a x \<in> carrier K; 0 \<le> v x; x \<noteq> 1\<^sub>r; 1\<^sub>r \<plusminus> x \<cdot>\<^sub>r (1\<^sub>r \<plusminus> -\<^sub>a x) \<in> carrier K; (1\<^sub>r \<plusminus> x \<cdot>\<^sub>r (1\<^sub>r \<plusminus> -\<^sub>a x))\<^bsup>\<hyphen> K\<^esup> \<in> carrier K\<rbrakk> \<Longrightarrow> 0 < v (1\<^sub>r \<plusminus> x) + v (1\<^sub>r \<plusminus> -\<^sub>a x) + - v (1\<^sub>r \<plusminus> x \<cdot>\<^sub>r (1\<^sub>r \<plusminus> -\<^sub>a x))
 3. \<lbrakk>valuation K v; x \<in> carrier K; 0 < v (1\<^sub>r \<plusminus> -\<^sub>a x); Ring K; aGroup K; -\<^sub>a x \<in> carrier K; 1\<^sub>r \<in> carrier K; 1\<^sub>r \<plusminus> -\<^sub>a x \<in> carrier K; 0 \<le> v x; x \<noteq> 1\<^sub>r; 1\<^sub>r \<plusminus> x \<cdot>\<^sub>r (1\<^sub>r \<plusminus> -\<^sub>a x) \<in> carrier K; (1\<^sub>r \<plusminus> x \<cdot>\<^sub>r (1\<^sub>r \<plusminus> -\<^sub>a x))\<^bsup>\<hyphen> K\<^esup> \<in> carrier K\<rbrakk> \<Longrightarrow> 1\<^sub>r \<plusminus> -\<^sub>a x^\<^bsup>K Suc (Suc 0)\<^esup> = (1\<^sub>r \<plusminus> x) \<cdot>\<^sub>r (1\<^sub>r \<plusminus> -\<^sub>a x)
 4. \<lbrakk>valuation K v; x \<in> carrier K; 0 < v (1\<^sub>r \<plusminus> -\<^sub>a x); Ring K; aGroup K; -\<^sub>a x \<in> carrier K; 1\<^sub>r \<in> carrier K; 1\<^sub>r \<plusminus> -\<^sub>a x \<in> carrier K; 0 \<le> v x; x \<noteq> 1\<^sub>r; 1\<^sub>r \<plusminus> x \<cdot>\<^sub>r (1\<^sub>r \<plusminus> -\<^sub>a x) \<in> carrier K; (1\<^sub>r \<plusminus> x \<cdot>\<^sub>r (1\<^sub>r \<plusminus> -\<^sub>a x))\<^bsup>\<hyphen> K\<^esup> \<in> carrier K\<rbrakk> \<Longrightarrow> x \<in> carrier K
 5. \<lbrakk>valuation K v; x \<in> carrier K; 0 < v (1\<^sub>r \<plusminus> -\<^sub>a x); Ring K; aGroup K; -\<^sub>a x \<in> carrier K; 1\<^sub>r \<in> carrier K; 1\<^sub>r \<plusminus> -\<^sub>a x \<in> carrier K; 0 \<le> v x; x \<noteq> 1\<^sub>r; 1\<^sub>r \<plusminus> x \<cdot>\<^sub>r (1\<^sub>r \<plusminus> -\<^sub>a x) \<in> carrier K; (1\<^sub>r \<plusminus> x \<cdot>\<^sub>r (1\<^sub>r \<plusminus> -\<^sub>a x))\<^bsup>\<hyphen> K\<^esup> \<in> carrier K\<rbrakk> \<Longrightarrow> x \<noteq> 1\<^sub>r
 6. \<lbrakk>valuation K v; x \<in> carrier K; 0 < v (1\<^sub>r \<plusminus> -\<^sub>a x); Ring K; aGroup K; -\<^sub>a x \<in> carrier K; 1\<^sub>r \<in> carrier K; 1\<^sub>r \<plusminus> -\<^sub>a x \<in> carrier K; 0 \<le> v x; x \<noteq> 1\<^sub>r; 1\<^sub>r \<plusminus> x \<cdot>\<^sub>r (1\<^sub>r \<plusminus> -\<^sub>a x) \<in> carrier K\<rbrakk> \<Longrightarrow> 1\<^sub>r \<plusminus> x \<cdot>\<^sub>r (1\<^sub>r \<plusminus> -\<^sub>a x) \<in> carrier K - {\<zero>}
[PROOF STEP]
apply (simp add:aGroup.ag_inv_inv[of K "1\<^sub>r"],
        frule eq_elems_eq_val[of "x \<cdot>\<^sub>r (-\<^sub>a x \<plusminus> 1\<^sub>r)" "-\<^sub>a 1\<^sub>r" v],
        thin_tac "x \<cdot>\<^sub>r (-\<^sub>a x \<plusminus> 1\<^sub>r) = -\<^sub>a 1\<^sub>r",
        simp add:val_minus_eq value_of_one)
[PROOF STATE]
proof (prove)
goal (6 subgoals):
 1. \<lbrakk>valuation K v; x \<in> carrier K; 0 < v (-\<^sub>a x \<plusminus> 1\<^sub>r); Ring K; aGroup K; -\<^sub>a x \<in> carrier K; 1\<^sub>r \<in> carrier K; -\<^sub>a x \<plusminus> 1\<^sub>r \<in> carrier K; 0 \<le> v x; x \<noteq> 1\<^sub>r; \<zero> \<in> carrier K; \<zero>\<^bsup>\<hyphen> K\<^esup> \<in> carrier K; -\<^sub>a 1\<^sub>r \<plusminus> 1\<^sub>r = \<zero>; -\<^sub>a 1\<^sub>r \<in> carrier K; v (x \<cdot>\<^sub>r (-\<^sub>a x \<plusminus> 1\<^sub>r)) = 0\<rbrakk> \<Longrightarrow> False
 2. \<lbrakk>valuation K v; x \<in> carrier K; 0 < v (1\<^sub>r \<plusminus> -\<^sub>a x); Ring K; aGroup K; -\<^sub>a x \<in> carrier K; 1\<^sub>r \<in> carrier K; 1\<^sub>r \<plusminus> -\<^sub>a x \<in> carrier K; 0 \<le> v x; x \<noteq> 1\<^sub>r; 1\<^sub>r \<plusminus> x \<cdot>\<^sub>r (1\<^sub>r \<plusminus> -\<^sub>a x) \<in> carrier K; (1\<^sub>r \<plusminus> x \<cdot>\<^sub>r (1\<^sub>r \<plusminus> -\<^sub>a x))\<^bsup>\<hyphen> K\<^esup> \<in> carrier K\<rbrakk> \<Longrightarrow> 0 < v (1\<^sub>r \<plusminus> x) + v (1\<^sub>r \<plusminus> -\<^sub>a x) + - v (1\<^sub>r \<plusminus> x \<cdot>\<^sub>r (1\<^sub>r \<plusminus> -\<^sub>a x))
 3. \<lbrakk>valuation K v; x \<in> carrier K; 0 < v (1\<^sub>r \<plusminus> -\<^sub>a x); Ring K; aGroup K; -\<^sub>a x \<in> carrier K; 1\<^sub>r \<in> carrier K; 1\<^sub>r \<plusminus> -\<^sub>a x \<in> carrier K; 0 \<le> v x; x \<noteq> 1\<^sub>r; 1\<^sub>r \<plusminus> x \<cdot>\<^sub>r (1\<^sub>r \<plusminus> -\<^sub>a x) \<in> carrier K; (1\<^sub>r \<plusminus> x \<cdot>\<^sub>r (1\<^sub>r \<plusminus> -\<^sub>a x))\<^bsup>\<hyphen> K\<^esup> \<in> carrier K\<rbrakk> \<Longrightarrow> 1\<^sub>r \<plusminus> -\<^sub>a x^\<^bsup>K Suc (Suc 0)\<^esup> = (1\<^sub>r \<plusminus> x) \<cdot>\<^sub>r (1\<^sub>r \<plusminus> -\<^sub>a x)
 4. \<lbrakk>valuation K v; x \<in> carrier K; 0 < v (1\<^sub>r \<plusminus> -\<^sub>a x); Ring K; aGroup K; -\<^sub>a x \<in> carrier K; 1\<^sub>r \<in> carrier K; 1\<^sub>r \<plusminus> -\<^sub>a x \<in> carrier K; 0 \<le> v x; x \<noteq> 1\<^sub>r; 1\<^sub>r \<plusminus> x \<cdot>\<^sub>r (1\<^sub>r \<plusminus> -\<^sub>a x) \<in> carrier K; (1\<^sub>r \<plusminus> x \<cdot>\<^sub>r (1\<^sub>r \<plusminus> -\<^sub>a x))\<^bsup>\<hyphen> K\<^esup> \<in> carrier K\<rbrakk> \<Longrightarrow> x \<in> carrier K
 5. \<lbrakk>valuation K v; x \<in> carrier K; 0 < v (1\<^sub>r \<plusminus> -\<^sub>a x); Ring K; aGroup K; -\<^sub>a x \<in> carrier K; 1\<^sub>r \<in> carrier K; 1\<^sub>r \<plusminus> -\<^sub>a x \<in> carrier K; 0 \<le> v x; x \<noteq> 1\<^sub>r; 1\<^sub>r \<plusminus> x \<cdot>\<^sub>r (1\<^sub>r \<plusminus> -\<^sub>a x) \<in> carrier K; (1\<^sub>r \<plusminus> x \<cdot>\<^sub>r (1\<^sub>r \<plusminus> -\<^sub>a x))\<^bsup>\<hyphen> K\<^esup> \<in> carrier K\<rbrakk> \<Longrightarrow> x \<noteq> 1\<^sub>r
 6. \<lbrakk>valuation K v; x \<in> carrier K; 0 < v (1\<^sub>r \<plusminus> -\<^sub>a x); Ring K; aGroup K; -\<^sub>a x \<in> carrier K; 1\<^sub>r \<in> carrier K; 1\<^sub>r \<plusminus> -\<^sub>a x \<in> carrier K; 0 \<le> v x; x \<noteq> 1\<^sub>r; 1\<^sub>r \<plusminus> x \<cdot>\<^sub>r (1\<^sub>r \<plusminus> -\<^sub>a x) \<in> carrier K\<rbrakk> \<Longrightarrow> 1\<^sub>r \<plusminus> x \<cdot>\<^sub>r (1\<^sub>r \<plusminus> -\<^sub>a x) \<in> carrier K - {\<zero>}
[PROOF STEP]
apply (simp add:val_t2p,
               frule aadd_pos_poss[of "v x" "v (-\<^sub>a x \<plusminus> 1\<^sub>r)"], assumption+,
               simp,
               subst value_less_eq[THEN sym, of v "1\<^sub>r" "x \<cdot>\<^sub>r (1\<^sub>r \<plusminus> -\<^sub>a x)"],
               assumption+,
               rule Ring.ring_tOp_closed, assumption+,
               simp add:value_of_one, subst val_t2p[of v], assumption+,
               rule aadd_pos_poss[of "v x" "v (1\<^sub>r \<plusminus> -\<^sub>a x)"], assumption+,
               simp add:value_of_one,
               cut_tac aadd_pos_poss[of "v (1\<^sub>r \<plusminus> x)" "v (1\<^sub>r \<plusminus> -\<^sub>a x)"],
               simp add:aadd_0_r, rule val_axiom4, assumption+)
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<lbrakk>valuation K v; x \<in> carrier K; 0 < v (1\<^sub>r \<plusminus> -\<^sub>a x); Ring K; aGroup K; -\<^sub>a x \<in> carrier K; 1\<^sub>r \<in> carrier K; 1\<^sub>r \<plusminus> -\<^sub>a x \<in> carrier K; 0 \<le> v x; x \<noteq> 1\<^sub>r; 1\<^sub>r \<plusminus> x \<cdot>\<^sub>r (1\<^sub>r \<plusminus> -\<^sub>a x) \<in> carrier K; (1\<^sub>r \<plusminus> x \<cdot>\<^sub>r (1\<^sub>r \<plusminus> -\<^sub>a x))\<^bsup>\<hyphen> K\<^esup> \<in> carrier K\<rbrakk> \<Longrightarrow> 1\<^sub>r \<plusminus> -\<^sub>a x^\<^bsup>K Suc (Suc 0)\<^esup> = (1\<^sub>r \<plusminus> x) \<cdot>\<^sub>r (1\<^sub>r \<plusminus> -\<^sub>a x)
 2. \<lbrakk>valuation K v; x \<in> carrier K; 0 < v (1\<^sub>r \<plusminus> -\<^sub>a x); Ring K; aGroup K; -\<^sub>a x \<in> carrier K; 1\<^sub>r \<in> carrier K; 1\<^sub>r \<plusminus> -\<^sub>a x \<in> carrier K; 0 \<le> v x; x \<noteq> 1\<^sub>r; 1\<^sub>r \<plusminus> x \<cdot>\<^sub>r (1\<^sub>r \<plusminus> -\<^sub>a x) \<in> carrier K; (1\<^sub>r \<plusminus> x \<cdot>\<^sub>r (1\<^sub>r \<plusminus> -\<^sub>a x))\<^bsup>\<hyphen> K\<^esup> \<in> carrier K\<rbrakk> \<Longrightarrow> x \<in> carrier K
 3. \<lbrakk>valuation K v; x \<in> carrier K; 0 < v (1\<^sub>r \<plusminus> -\<^sub>a x); Ring K; aGroup K; -\<^sub>a x \<in> carrier K; 1\<^sub>r \<in> carrier K; 1\<^sub>r \<plusminus> -\<^sub>a x \<in> carrier K; 0 \<le> v x; x \<noteq> 1\<^sub>r; 1\<^sub>r \<plusminus> x \<cdot>\<^sub>r (1\<^sub>r \<plusminus> -\<^sub>a x) \<in> carrier K; (1\<^sub>r \<plusminus> x \<cdot>\<^sub>r (1\<^sub>r \<plusminus> -\<^sub>a x))\<^bsup>\<hyphen> K\<^esup> \<in> carrier K\<rbrakk> \<Longrightarrow> x \<noteq> 1\<^sub>r
 4. \<lbrakk>valuation K v; x \<in> carrier K; 0 < v (1\<^sub>r \<plusminus> -\<^sub>a x); Ring K; aGroup K; -\<^sub>a x \<in> carrier K; 1\<^sub>r \<in> carrier K; 1\<^sub>r \<plusminus> -\<^sub>a x \<in> carrier K; 0 \<le> v x; x \<noteq> 1\<^sub>r; 1\<^sub>r \<plusminus> x \<cdot>\<^sub>r (1\<^sub>r \<plusminus> -\<^sub>a x) \<in> carrier K\<rbrakk> \<Longrightarrow> 1\<^sub>r \<plusminus> x \<cdot>\<^sub>r (1\<^sub>r \<plusminus> -\<^sub>a x) \<in> carrier K - {\<zero>}
[PROOF STEP]
apply (subst Ring.ring_distrib2, assumption+, simp add:Ring.ring_l_one,
         subst Ring.ring_distrib1, assumption+, simp add:Ring.ring_r_one,
         subst aGroup.pOp_assocTr43, assumption+,
         rule Ring.ring_tOp_closed, assumption+,
         simp add:aGroup.ag_l_inv1 aGroup.ag_r_zero,
        subst Ring.ring_inv1_2, assumption+, simp, assumption+)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>valuation K v; x \<in> carrier K; 0 < v (1\<^sub>r \<plusminus> -\<^sub>a x); Ring K; aGroup K; -\<^sub>a x \<in> carrier K; 1\<^sub>r \<in> carrier K; 1\<^sub>r \<plusminus> -\<^sub>a x \<in> carrier K; 0 \<le> v x; x \<noteq> 1\<^sub>r; 1\<^sub>r \<plusminus> x \<cdot>\<^sub>r (1\<^sub>r \<plusminus> -\<^sub>a x) \<in> carrier K\<rbrakk> \<Longrightarrow> 1\<^sub>r \<plusminus> x \<cdot>\<^sub>r (1\<^sub>r \<plusminus> -\<^sub>a x) \<in> carrier K - {\<zero>}
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>valuation K v; x \<in> carrier K; 0 < v (1\<^sub>r \<plusminus> -\<^sub>a x); Ring K; aGroup K; -\<^sub>a x \<in> carrier K; 1\<^sub>r \<in> carrier K; 1\<^sub>r \<plusminus> -\<^sub>a x \<in> carrier K; 0 \<le> v x; x \<noteq> 1\<^sub>r; 1\<^sub>r \<plusminus> x \<cdot>\<^sub>r (1\<^sub>r \<plusminus> -\<^sub>a x) \<in> carrier K\<rbrakk> \<Longrightarrow> 1\<^sub>r \<plusminus> x \<cdot>\<^sub>r (1\<^sub>r \<plusminus> -\<^sub>a x) \<noteq> \<zero>
[PROOF STEP]
apply (rule contrapos_pp, simp+,
       frule Ring.ring_tOp_closed[of K x "(1\<^sub>r \<plusminus> -\<^sub>a x)"], assumption+,
       simp add:aGroup.ag_pOp_commute[of K "1\<^sub>r"],
       frule aGroup.ag_eq_diffzero[THEN sym, of K "x \<cdot>\<^sub>r (-\<^sub>a x \<plusminus> 1\<^sub>r)" "-\<^sub>a 1\<^sub>r"],
       assumption+, rule aGroup.ag_mOp_closed, assumption+)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>valuation K v; x \<in> carrier K; 0 < v (-\<^sub>a x \<plusminus> 1\<^sub>r); Ring K; aGroup K; -\<^sub>a x \<in> carrier K; 1\<^sub>r \<in> carrier K; -\<^sub>a x \<plusminus> 1\<^sub>r \<in> carrier K; 0 \<le> v x; x \<noteq> 1\<^sub>r; \<zero> \<in> carrier K; x \<cdot>\<^sub>r (-\<^sub>a x \<plusminus> 1\<^sub>r) \<plusminus> 1\<^sub>r = \<zero>; x \<cdot>\<^sub>r (-\<^sub>a x \<plusminus> 1\<^sub>r) \<in> carrier K; (x \<cdot>\<^sub>r (-\<^sub>a x \<plusminus> 1\<^sub>r) \<plusminus> -\<^sub>a (-\<^sub>a 1\<^sub>r) = \<zero>) = (x \<cdot>\<^sub>r (-\<^sub>a x \<plusminus> 1\<^sub>r) = -\<^sub>a 1\<^sub>r)\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
apply (simp add:aGroup.ag_inv_inv[of K "1\<^sub>r"],
        frule eq_elems_eq_val[of "x \<cdot>\<^sub>r (-\<^sub>a x \<plusminus> 1\<^sub>r)" "-\<^sub>a 1\<^sub>r" v],
        thin_tac "x \<cdot>\<^sub>r (-\<^sub>a x \<plusminus> 1\<^sub>r) = -\<^sub>a 1\<^sub>r",
        simp add:val_minus_eq value_of_one,
        simp add:val_t2p,
        frule aadd_pos_poss[of "v x" "v (-\<^sub>a x \<plusminus> 1\<^sub>r)"], assumption+,
        simp)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma (in Corps) OstrowskiTr9:"\<lbrakk>valuation K v; x \<in> carrier K; 0 < (v x)\<rbrakk> \<Longrightarrow>
                 0 < (v (x \<cdot>\<^sub>r ((1\<^sub>r \<plusminus> x \<cdot>\<^sub>r (1\<^sub>r \<plusminus> -\<^sub>a x))\<^bsup>\<hyphen>K\<^esup>)))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>valuation K v; x \<in> carrier K; 0 < v x\<rbrakk> \<Longrightarrow> 0 < v (x \<cdot>\<^sub>r (1\<^sub>r \<plusminus> x \<cdot>\<^sub>r (1\<^sub>r \<plusminus> -\<^sub>a x))\<^bsup>\<hyphen> K\<^esup>)
[PROOF STEP]
apply (subgoal_tac "1\<^sub>r \<plusminus> x \<cdot>\<^sub>r (1\<^sub>r \<plusminus> -\<^sub>a x) \<noteq> \<zero>")
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>valuation K v; x \<in> carrier K; 0 < v x; 1\<^sub>r \<plusminus> x \<cdot>\<^sub>r (1\<^sub>r \<plusminus> -\<^sub>a x) \<noteq> \<zero>\<rbrakk> \<Longrightarrow> 0 < v (x \<cdot>\<^sub>r (1\<^sub>r \<plusminus> x \<cdot>\<^sub>r (1\<^sub>r \<plusminus> -\<^sub>a x))\<^bsup>\<hyphen> K\<^esup>)
 2. \<lbrakk>valuation K v; x \<in> carrier K; 0 < v x\<rbrakk> \<Longrightarrow> 1\<^sub>r \<plusminus> x \<cdot>\<^sub>r (1\<^sub>r \<plusminus> -\<^sub>a x) \<noteq> \<zero>
[PROOF STEP]
apply (cut_tac field_is_ring, frule Ring.ring_is_ag[of "K"],
       frule aGroup.ag_mOp_closed[of "K" "x"], assumption+,
       frule Ring.ring_one[of "K"],
       frule aGroup.ag_pOp_closed[of "K" "1\<^sub>r" "-\<^sub>a x"], assumption+,
       subst val_t2p, assumption+,
       cut_tac invf_closed1[of "1\<^sub>r \<plusminus> x \<cdot>\<^sub>r (1\<^sub>r \<plusminus> -\<^sub>a x)"], simp)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<lbrakk>valuation K v; x \<in> carrier K; 0 < v x; 1\<^sub>r \<plusminus> x \<cdot>\<^sub>r (1\<^sub>r \<plusminus> -\<^sub>a x) \<noteq> \<zero>; Ring K; aGroup K; -\<^sub>a x \<in> carrier K; 1\<^sub>r \<in> carrier K; 1\<^sub>r \<plusminus> -\<^sub>a x \<in> carrier K\<rbrakk> \<Longrightarrow> 1\<^sub>r \<plusminus> x \<cdot>\<^sub>r (1\<^sub>r \<plusminus> -\<^sub>a x) \<in> carrier K - {\<zero>}
 2. \<lbrakk>valuation K v; x \<in> carrier K; 0 < v x; 1\<^sub>r \<plusminus> x \<cdot>\<^sub>r (1\<^sub>r \<plusminus> -\<^sub>a x) \<noteq> \<zero>; Ring K; aGroup K; -\<^sub>a x \<in> carrier K; 1\<^sub>r \<in> carrier K; 1\<^sub>r \<plusminus> -\<^sub>a x \<in> carrier K\<rbrakk> \<Longrightarrow> 0 < v x + v ((1\<^sub>r \<plusminus> x \<cdot>\<^sub>r (1\<^sub>r \<plusminus> -\<^sub>a x))\<^bsup>\<hyphen> K\<^esup>)
 3. \<lbrakk>valuation K v; x \<in> carrier K; 0 < v x\<rbrakk> \<Longrightarrow> 1\<^sub>r \<plusminus> x \<cdot>\<^sub>r (1\<^sub>r \<plusminus> -\<^sub>a x) \<noteq> \<zero>
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<lbrakk>valuation K v; x \<in> carrier K; 0 < v x; 1\<^sub>r \<plusminus> x \<cdot>\<^sub>r (1\<^sub>r \<plusminus> -\<^sub>a x) \<noteq> \<zero>; Ring K; aGroup K; -\<^sub>a x \<in> carrier K; 1\<^sub>r \<in> carrier K; 1\<^sub>r \<plusminus> -\<^sub>a x \<in> carrier K\<rbrakk> \<Longrightarrow> 1\<^sub>r \<plusminus> x \<cdot>\<^sub>r (1\<^sub>r \<plusminus> -\<^sub>a x) \<in> carrier K
 2. \<lbrakk>valuation K v; x \<in> carrier K; 0 < v x; 1\<^sub>r \<plusminus> x \<cdot>\<^sub>r (1\<^sub>r \<plusminus> -\<^sub>a x) \<noteq> \<zero>; Ring K; aGroup K; -\<^sub>a x \<in> carrier K; 1\<^sub>r \<in> carrier K; 1\<^sub>r \<plusminus> -\<^sub>a x \<in> carrier K\<rbrakk> \<Longrightarrow> 0 < v x + v ((1\<^sub>r \<plusminus> x \<cdot>\<^sub>r (1\<^sub>r \<plusminus> -\<^sub>a x))\<^bsup>\<hyphen> K\<^esup>)
 3. \<lbrakk>valuation K v; x \<in> carrier K; 0 < v x\<rbrakk> \<Longrightarrow> 1\<^sub>r \<plusminus> x \<cdot>\<^sub>r (1\<^sub>r \<plusminus> -\<^sub>a x) \<noteq> \<zero>
[PROOF STEP]
apply (rule aGroup.ag_pOp_closed, assumption+,
        rule Ring.ring_tOp_closed, assumption+)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>valuation K v; x \<in> carrier K; 0 < v x; 1\<^sub>r \<plusminus> x \<cdot>\<^sub>r (1\<^sub>r \<plusminus> -\<^sub>a x) \<noteq> \<zero>; Ring K; aGroup K; -\<^sub>a x \<in> carrier K; 1\<^sub>r \<in> carrier K; 1\<^sub>r \<plusminus> -\<^sub>a x \<in> carrier K\<rbrakk> \<Longrightarrow> 0 < v x + v ((1\<^sub>r \<plusminus> x \<cdot>\<^sub>r (1\<^sub>r \<plusminus> -\<^sub>a x))\<^bsup>\<hyphen> K\<^esup>)
 2. \<lbrakk>valuation K v; x \<in> carrier K; 0 < v x\<rbrakk> \<Longrightarrow> 1\<^sub>r \<plusminus> x \<cdot>\<^sub>r (1\<^sub>r \<plusminus> -\<^sub>a x) \<noteq> \<zero>
[PROOF STEP]
(*
 apply (rule contrapos_pp, simp+,
       frule Ring.ring_tOp_closed[of K x "(1\<^sub>r \<plusminus> -\<^sub>a x)"], assumption+) apply (
       simp add:aGroup.ag_pOp_commute[of K "1\<^sub>r"],
       frule aGroup.ag_eq_diffzero[THEN sym, of K "x \<cdot>\<^sub>r (-\<^sub>a x \<plusminus> 1\<^sub>r)" "-\<^sub>a 1\<^sub>r"])
       apply (rule Ring.ring_tOp_closed, assumption+,
              rule aGroup.ag_mOp_closed, assumption+)
       apply (simp add:aGroup.ag_inv_inv)
       apply (frule eq_elems_eq_val[of "x \<cdot>\<^sub>r (-\<^sub>a x \<plusminus> 1\<^sub>r)" "-\<^sub>a 1\<^sub>r" v],
        thin_tac "x \<cdot>\<^sub>r (-\<^sub>a x \<plusminus> 1\<^sub>r) = -\<^sub>a 1\<^sub>r",
        simp add:val_minus_eq value_of_one,
        simp add:val_t2p)
        apply (simp add:aadd_commute[of "v x" "v (-\<^sub>a x \<plusminus> 1\<^sub>r)"])
       apply (cut_tac aadd_pos_poss[of "v (-\<^sub>a x \<plusminus> 1\<^sub>r)" "v x"], simp)
       apply (simp add:val_minus_eq[THEN sym, of v x])
       apply (subst aGroup.ag_pOp_commute, assumption+)
       apply (rule val_axiom4[of v "-\<^sub>a x"], assumption+)
       apply (simp add:aless_imp_le, assumption) *)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>valuation K v; x \<in> carrier K; 0 < v x; 1\<^sub>r \<plusminus> x \<cdot>\<^sub>r (1\<^sub>r \<plusminus> -\<^sub>a x) \<noteq> \<zero>; Ring K; aGroup K; -\<^sub>a x \<in> carrier K; 1\<^sub>r \<in> carrier K; 1\<^sub>r \<plusminus> -\<^sub>a x \<in> carrier K\<rbrakk> \<Longrightarrow> 0 < v x + v ((1\<^sub>r \<plusminus> x \<cdot>\<^sub>r (1\<^sub>r \<plusminus> -\<^sub>a x))\<^bsup>\<hyphen> K\<^esup>)
 2. \<lbrakk>valuation K v; x \<in> carrier K; 0 < v x\<rbrakk> \<Longrightarrow> 1\<^sub>r \<plusminus> x \<cdot>\<^sub>r (1\<^sub>r \<plusminus> -\<^sub>a x) \<noteq> \<zero>
[PROOF STEP]
apply (subst value_of_inv[of v "1\<^sub>r \<plusminus> x \<cdot>\<^sub>r (1\<^sub>r \<plusminus> -\<^sub>a x)"], assumption+,
        rule aGroup.ag_pOp_closed, assumption+,
               rule Ring.ring_tOp_closed, assumption+,
        frule value_less_eq[THEN sym, of v "1\<^sub>r" "-\<^sub>a x"], assumption+,
        simp add:value_of_one, simp add:val_minus_eq,
        subst value_less_eq[THEN sym, of v "1\<^sub>r" "x \<cdot>\<^sub>r (1\<^sub>r \<plusminus> -\<^sub>a x)"],
           assumption+, rule Ring.ring_tOp_closed, assumption+,
           simp add:value_of_one, subst val_t2p, assumption+,
           subst aadd_commute,
       rule aadd_pos_poss[of "v (1\<^sub>r \<plusminus> -\<^sub>a x)" "v x"],
       simp, assumption, simp add:value_of_one,
       simp add:aadd_0_r)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>valuation K v; x \<in> carrier K; 0 < v x\<rbrakk> \<Longrightarrow> 1\<^sub>r \<plusminus> x \<cdot>\<^sub>r (1\<^sub>r \<plusminus> -\<^sub>a x) \<noteq> \<zero>
[PROOF STEP]
apply (cut_tac field_is_ring, frule Ring.ring_is_ag[of K],
       frule Ring.ring_one,
       rule contrapos_pp, simp+,
       frule Ring.ring_tOp_closed[of K x "(1\<^sub>r \<plusminus> -\<^sub>a x)"], assumption+,
       rule aGroup.ag_pOp_closed, assumption+,
       rule aGroup.ag_mOp_closed, assumption+,
       frule aGroup.ag_mOp_closed[of K x], assumption+)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>valuation K v; x \<in> carrier K; 0 < v x; Ring K; aGroup K; 1\<^sub>r \<in> carrier K; 1\<^sub>r \<plusminus> x \<cdot>\<^sub>r (1\<^sub>r \<plusminus> -\<^sub>a x) = \<zero>; x \<cdot>\<^sub>r (1\<^sub>r \<plusminus> -\<^sub>a x) \<in> carrier K; -\<^sub>a x \<in> carrier K\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
apply (simp add:aGroup.ag_pOp_commute[of K "1\<^sub>r"],
       frule aGroup.ag_eq_diffzero[THEN sym, of K "x \<cdot>\<^sub>r (-\<^sub>a x \<plusminus> 1\<^sub>r)" "-\<^sub>a 1\<^sub>r"],
       simp add:aGroup.ag_pOp_commute,
       rule aGroup.ag_mOp_closed, assumption+,
       simp add:aGroup.ag_inv_inv,
       frule eq_elems_eq_val[of "x \<cdot>\<^sub>r (-\<^sub>a x \<plusminus> 1\<^sub>r)" "-\<^sub>a 1\<^sub>r" v],
        thin_tac "x \<cdot>\<^sub>r (-\<^sub>a x \<plusminus> 1\<^sub>r) = -\<^sub>a 1\<^sub>r",
        simp add:val_minus_eq value_of_one,
        frule_tac aGroup.ag_pOp_closed[of K "-\<^sub>a x" "1\<^sub>r"], assumption+,
        simp add:val_t2p)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>valuation K v; x \<in> carrier K; 0 < v x; Ring K; aGroup K; 1\<^sub>r \<in> carrier K; -\<^sub>a 1\<^sub>r \<plusminus> 1\<^sub>r = \<zero>; -\<^sub>a 1\<^sub>r \<in> carrier K; -\<^sub>a x \<in> carrier K; v x + v (-\<^sub>a x \<plusminus> 1\<^sub>r) = 0; -\<^sub>a x \<plusminus> 1\<^sub>r \<in> carrier K\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
apply (simp add:aadd_commute[of "v x"],
         cut_tac aadd_pos_poss[of "v (-\<^sub>a x \<plusminus> 1\<^sub>r)" "v x"], simp,
         subst aGroup.ag_pOp_commute, assumption+,
         subst value_less_eq[THEN sym, of v "1\<^sub>r" "-\<^sub>a x"], assumption+,
         simp add:value_of_one val_minus_eq, simp add:value_of_one)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>valuation K v; x \<in> carrier K; 0 < v x; Ring K; aGroup K; 1\<^sub>r \<in> carrier K; -\<^sub>a 1\<^sub>r \<plusminus> 1\<^sub>r = \<zero>; -\<^sub>a 1\<^sub>r \<in> carrier K; -\<^sub>a x \<in> carrier K; v (-\<^sub>a x \<plusminus> 1\<^sub>r) + v x = 0; -\<^sub>a x \<plusminus> 1\<^sub>r \<in> carrier K\<rbrakk> \<Longrightarrow> 0 < v x
[PROOF STEP]
apply assumption
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma (in Corps) OstrowskiTr10:"\<lbrakk>valuation K v; x \<in> carrier K;
       \<not> 0 \<le> v x\<rbrakk> \<Longrightarrow> 0 < (v (x \<cdot>\<^sub>r ((1\<^sub>r \<plusminus> x \<cdot>\<^sub>r (1\<^sub>r \<plusminus> -\<^sub>a x))\<^bsup>\<hyphen>K\<^esup>)))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>valuation K v; x \<in> carrier K; \<not> 0 \<le> v x\<rbrakk> \<Longrightarrow> 0 < v (x \<cdot>\<^sub>r (1\<^sub>r \<plusminus> x \<cdot>\<^sub>r (1\<^sub>r \<plusminus> -\<^sub>a x))\<^bsup>\<hyphen> K\<^esup>)
[PROOF STEP]
apply (frule OstrowskiTr6[of "v" "x"], assumption+,
       cut_tac invf_closed1[of "1\<^sub>r \<plusminus> x \<cdot>\<^sub>r (1\<^sub>r \<plusminus> -\<^sub>a x)"], simp,
       erule conjE, simp add:aneg_le, frule val_neg_nonzero[of "v" "x"],
       (erule conjE)+, assumption+, erule conjE)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>valuation K v; x \<in> carrier K; v x < 0; 1\<^sub>r \<plusminus> x \<cdot>\<^sub>r (1\<^sub>r \<plusminus> -\<^sub>a x) \<in> carrier K; 1\<^sub>r \<plusminus> x \<cdot>\<^sub>r (1\<^sub>r \<plusminus> -\<^sub>a x) \<noteq> \<zero>; x \<noteq> \<zero>; (1\<^sub>r \<plusminus> x \<cdot>\<^sub>r (1\<^sub>r \<plusminus> -\<^sub>a x))\<^bsup>\<hyphen> K\<^esup> \<in> carrier K; (1\<^sub>r \<plusminus> x \<cdot>\<^sub>r (1\<^sub>r \<plusminus> -\<^sub>a x))\<^bsup>\<hyphen> K\<^esup> \<noteq> \<zero>\<rbrakk> \<Longrightarrow> 0 < v (x \<cdot>\<^sub>r (1\<^sub>r \<plusminus> x \<cdot>\<^sub>r (1\<^sub>r \<plusminus> -\<^sub>a x))\<^bsup>\<hyphen> K\<^esup>)
 2. \<lbrakk>valuation K v; x \<in> carrier K; \<not> 0 \<le> v x; 1\<^sub>r \<plusminus> x \<cdot>\<^sub>r (1\<^sub>r \<plusminus> -\<^sub>a x) \<in> carrier K - {\<zero>}\<rbrakk> \<Longrightarrow> 1\<^sub>r \<plusminus> x \<cdot>\<^sub>r (1\<^sub>r \<plusminus> -\<^sub>a x) \<in> carrier K - {\<zero>}
[PROOF STEP]
apply (cut_tac field_is_ring, frule Ring.ring_is_ag[of "K"],
       frule aGroup.ag_mOp_closed[of "K" "x"], assumption+,
       frule Ring.ring_one[of "K"],
       frule aGroup.ag_pOp_closed[of "K" "1\<^sub>r" "-\<^sub>a x"], assumption+,
       subst val_t2p, assumption+)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>valuation K v; x \<in> carrier K; v x < 0; 1\<^sub>r \<plusminus> x \<cdot>\<^sub>r (1\<^sub>r \<plusminus> -\<^sub>a x) \<in> carrier K; 1\<^sub>r \<plusminus> x \<cdot>\<^sub>r (1\<^sub>r \<plusminus> -\<^sub>a x) \<noteq> \<zero>; x \<noteq> \<zero>; (1\<^sub>r \<plusminus> x \<cdot>\<^sub>r (1\<^sub>r \<plusminus> -\<^sub>a x))\<^bsup>\<hyphen> K\<^esup> \<in> carrier K; (1\<^sub>r \<plusminus> x \<cdot>\<^sub>r (1\<^sub>r \<plusminus> -\<^sub>a x))\<^bsup>\<hyphen> K\<^esup> \<noteq> \<zero>; Ring K; aGroup K; -\<^sub>a x \<in> carrier K; 1\<^sub>r \<in> carrier K; 1\<^sub>r \<plusminus> -\<^sub>a x \<in> carrier K\<rbrakk> \<Longrightarrow> 0 < v x + v ((1\<^sub>r \<plusminus> x \<cdot>\<^sub>r (1\<^sub>r \<plusminus> -\<^sub>a x))\<^bsup>\<hyphen> K\<^esup>)
 2. \<lbrakk>valuation K v; x \<in> carrier K; \<not> 0 \<le> v x; 1\<^sub>r \<plusminus> x \<cdot>\<^sub>r (1\<^sub>r \<plusminus> -\<^sub>a x) \<in> carrier K - {\<zero>}\<rbrakk> \<Longrightarrow> 1\<^sub>r \<plusminus> x \<cdot>\<^sub>r (1\<^sub>r \<plusminus> -\<^sub>a x) \<in> carrier K - {\<zero>}
[PROOF STEP]
apply (subst value_of_inv[of "v" "1\<^sub>r \<plusminus> x \<cdot>\<^sub>r (1\<^sub>r \<plusminus> -\<^sub>a x)"],
       assumption+, subst aGroup.ag_pOp_commute[of "K" "1\<^sub>r"], assumption+,
       rule Ring.ring_tOp_closed, assumption+,
       subst value_less_eq[THEN sym, of v
                                      "x \<cdot>\<^sub>r (1\<^sub>r \<plusminus> -\<^sub>a x)" "1\<^sub>r"], assumption+)
[PROOF STATE]
proof (prove)
goal (5 subgoals):
 1. \<lbrakk>valuation K v; x \<in> carrier K; v x < 0; 1\<^sub>r \<plusminus> x \<cdot>\<^sub>r (1\<^sub>r \<plusminus> -\<^sub>a x) \<in> carrier K; 1\<^sub>r \<plusminus> x \<cdot>\<^sub>r (1\<^sub>r \<plusminus> -\<^sub>a x) \<noteq> \<zero>; x \<noteq> \<zero>; (1\<^sub>r \<plusminus> x \<cdot>\<^sub>r (1\<^sub>r \<plusminus> -\<^sub>a x))\<^bsup>\<hyphen> K\<^esup> \<in> carrier K; (1\<^sub>r \<plusminus> x \<cdot>\<^sub>r (1\<^sub>r \<plusminus> -\<^sub>a x))\<^bsup>\<hyphen> K\<^esup> \<noteq> \<zero>; Ring K; aGroup K; -\<^sub>a x \<in> carrier K; 1\<^sub>r \<in> carrier K; 1\<^sub>r \<plusminus> -\<^sub>a x \<in> carrier K\<rbrakk> \<Longrightarrow> x \<cdot>\<^sub>r (1\<^sub>r \<plusminus> -\<^sub>a x) \<in> carrier K
 2. \<lbrakk>valuation K v; x \<in> carrier K; v x < 0; 1\<^sub>r \<plusminus> x \<cdot>\<^sub>r (1\<^sub>r \<plusminus> -\<^sub>a x) \<in> carrier K; 1\<^sub>r \<plusminus> x \<cdot>\<^sub>r (1\<^sub>r \<plusminus> -\<^sub>a x) \<noteq> \<zero>; x \<noteq> \<zero>; (1\<^sub>r \<plusminus> x \<cdot>\<^sub>r (1\<^sub>r \<plusminus> -\<^sub>a x))\<^bsup>\<hyphen> K\<^esup> \<in> carrier K; (1\<^sub>r \<plusminus> x \<cdot>\<^sub>r (1\<^sub>r \<plusminus> -\<^sub>a x))\<^bsup>\<hyphen> K\<^esup> \<noteq> \<zero>; Ring K; aGroup K; -\<^sub>a x \<in> carrier K; 1\<^sub>r \<in> carrier K; 1\<^sub>r \<plusminus> -\<^sub>a x \<in> carrier K\<rbrakk> \<Longrightarrow> 1\<^sub>r \<in> carrier K
 3. \<lbrakk>valuation K v; x \<in> carrier K; v x < 0; 1\<^sub>r \<plusminus> x \<cdot>\<^sub>r (1\<^sub>r \<plusminus> -\<^sub>a x) \<in> carrier K; 1\<^sub>r \<plusminus> x \<cdot>\<^sub>r (1\<^sub>r \<plusminus> -\<^sub>a x) \<noteq> \<zero>; x \<noteq> \<zero>; (1\<^sub>r \<plusminus> x \<cdot>\<^sub>r (1\<^sub>r \<plusminus> -\<^sub>a x))\<^bsup>\<hyphen> K\<^esup> \<in> carrier K; (1\<^sub>r \<plusminus> x \<cdot>\<^sub>r (1\<^sub>r \<plusminus> -\<^sub>a x))\<^bsup>\<hyphen> K\<^esup> \<noteq> \<zero>; Ring K; aGroup K; -\<^sub>a x \<in> carrier K; 1\<^sub>r \<in> carrier K; 1\<^sub>r \<plusminus> -\<^sub>a x \<in> carrier K\<rbrakk> \<Longrightarrow> v (x \<cdot>\<^sub>r (1\<^sub>r \<plusminus> -\<^sub>a x)) < v 1\<^sub>r
 4. \<lbrakk>valuation K v; x \<in> carrier K; v x < 0; 1\<^sub>r \<plusminus> x \<cdot>\<^sub>r (1\<^sub>r \<plusminus> -\<^sub>a x) \<in> carrier K; 1\<^sub>r \<plusminus> x \<cdot>\<^sub>r (1\<^sub>r \<plusminus> -\<^sub>a x) \<noteq> \<zero>; x \<noteq> \<zero>; (1\<^sub>r \<plusminus> x \<cdot>\<^sub>r (1\<^sub>r \<plusminus> -\<^sub>a x))\<^bsup>\<hyphen> K\<^esup> \<in> carrier K; (1\<^sub>r \<plusminus> x \<cdot>\<^sub>r (1\<^sub>r \<plusminus> -\<^sub>a x))\<^bsup>\<hyphen> K\<^esup> \<noteq> \<zero>; Ring K; aGroup K; -\<^sub>a x \<in> carrier K; 1\<^sub>r \<in> carrier K; 1\<^sub>r \<plusminus> -\<^sub>a x \<in> carrier K\<rbrakk> \<Longrightarrow> 0 < v x + - v (x \<cdot>\<^sub>r (1\<^sub>r \<plusminus> -\<^sub>a x))
 5. \<lbrakk>valuation K v; x \<in> carrier K; \<not> 0 \<le> v x; 1\<^sub>r \<plusminus> x \<cdot>\<^sub>r (1\<^sub>r \<plusminus> -\<^sub>a x) \<in> carrier K - {\<zero>}\<rbrakk> \<Longrightarrow> 1\<^sub>r \<plusminus> x \<cdot>\<^sub>r (1\<^sub>r \<plusminus> -\<^sub>a x) \<in> carrier K - {\<zero>}
[PROOF STEP]
apply (rule Ring.ring_tOp_closed, assumption+, simp add:value_of_one,
       frule one_plus_x_nonzero[of "v" "-\<^sub>a x"], assumption,
       simp add:val_minus_eq, erule conjE, simp,
       subst val_t2p[of "v"], assumption+, simp add:aadd_two_negg)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>valuation K v; x \<in> carrier K; v x < 0; 1\<^sub>r \<plusminus> x \<cdot>\<^sub>r (1\<^sub>r \<plusminus> -\<^sub>a x) \<in> carrier K; 1\<^sub>r \<plusminus> x \<cdot>\<^sub>r (1\<^sub>r \<plusminus> -\<^sub>a x) \<noteq> \<zero>; x \<noteq> \<zero>; (1\<^sub>r \<plusminus> x \<cdot>\<^sub>r (1\<^sub>r \<plusminus> -\<^sub>a x))\<^bsup>\<hyphen> K\<^esup> \<in> carrier K; (1\<^sub>r \<plusminus> x \<cdot>\<^sub>r (1\<^sub>r \<plusminus> -\<^sub>a x))\<^bsup>\<hyphen> K\<^esup> \<noteq> \<zero>; Ring K; aGroup K; -\<^sub>a x \<in> carrier K; 1\<^sub>r \<in> carrier K; 1\<^sub>r \<plusminus> -\<^sub>a x \<in> carrier K\<rbrakk> \<Longrightarrow> 0 < v x + - v (x \<cdot>\<^sub>r (1\<^sub>r \<plusminus> -\<^sub>a x))
 2. \<lbrakk>valuation K v; x \<in> carrier K; \<not> 0 \<le> v x; 1\<^sub>r \<plusminus> x \<cdot>\<^sub>r (1\<^sub>r \<plusminus> -\<^sub>a x) \<in> carrier K - {\<zero>}\<rbrakk> \<Longrightarrow> 1\<^sub>r \<plusminus> x \<cdot>\<^sub>r (1\<^sub>r \<plusminus> -\<^sub>a x) \<in> carrier K - {\<zero>}
[PROOF STEP]
apply (simp add:val_t2p,
       frule value_less_eq[THEN sym, of "v" "-\<^sub>a x" "1\<^sub>r"], assumption+,
       simp add:value_of_one, simp add:val_minus_eq,
       simp add:val_minus_eq, simp add:aGroup.ag_pOp_commute[of "K" "-\<^sub>a x"],
       frule val_nonzero_z[of "v" "x"], assumption+, erule exE,
       simp add:a_zpz aminus, simp add:ant_0[THEN sym] aless_zless,
       assumption)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done