[STATEMENT]
lemma (in Corps) Ostrowski_first:"vals_nonequiv K (Suc 0) vv
         \<Longrightarrow> \<exists>x\<in>carrier K. Ostrowski_elem K (Suc 0) vv x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vals_nonequiv K (Suc 0) vv \<Longrightarrow> \<exists>x\<in>carrier K. Ostrowski_elem K (Suc 0) vv x
[PROOF STEP]
apply (simp add:vals_nonequiv_def,
        cut_tac Nset_Suc0, (erule conjE)+,
        simp add:valuations_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>{i. i \<le> Suc 0} = {0, Suc 0}; \<forall>j\<le>Suc 0. valuation K (vv j); \<forall>j\<le>Suc 0. \<forall>l\<le>Suc 0. j \<noteq> l \<longrightarrow> \<not> v_equiv K (vv j) (vv l)\<rbrakk> \<Longrightarrow> \<exists>x\<in>carrier K. Ostrowski_elem K (Suc 0) vv x
[PROOF STEP]
apply (rotate_tac -1,
        frule_tac a = 0 in forall_spec, simp,
        rotate_tac -1,
        drule_tac a = "Suc 0" in forall_spec, simp)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<forall>j\<le>Suc 0. \<forall>l\<le>Suc 0. j \<noteq> l \<longrightarrow> \<not> v_equiv K (vv j) (vv l); {i. i \<le> Suc 0} = {0, Suc 0}; \<forall>j\<le>Suc 0. valuation K (vv j); 0 \<noteq> Suc 0 \<longrightarrow> \<not> v_equiv K (vv 0) (vv (Suc 0))\<rbrakk> \<Longrightarrow> \<exists>x\<in>carrier K. Ostrowski_elem K (Suc 0) vv x
[PROOF STEP]
apply (drule_tac a = "Suc 0" in forall_spec, simp,
        rotate_tac -1,
        drule_tac a = 0 in forall_spec, simp, simp)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>{i. i \<le> Suc 0} = {0, Suc 0}; \<forall>j\<le>Suc 0. valuation K (vv j); \<not> v_equiv K (vv 0) (vv (Suc 0)); \<not> v_equiv K (vv (Suc 0)) (vv 0)\<rbrakk> \<Longrightarrow> \<exists>x\<in>carrier K. Ostrowski_elem K (Suc 0) vv x
[PROOF STEP]
apply (frule_tac a = 0 in forall_spec, simp,
        drule_tac a = "Suc 0" in forall_spec, simp,
        frule_tac v = "vv 0" and v' = "vv (Suc 0)" in
         nonequiv_ex_Ostrowski_elem, assumption+,
         erule bexE)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>{i. i \<le> Suc 0} = {0, Suc 0}; \<not> v_equiv K (vv 0) (vv (Suc 0)); \<not> v_equiv K (vv (Suc 0)) (vv 0); valuation K (vv 0); valuation K (vv (Suc 0)); x \<in> carrier K; 0 \<le> vv 0 x \<and> vv (Suc 0) x < 0\<rbrakk> \<Longrightarrow> \<exists>x\<in>carrier K. Ostrowski_elem K (Suc 0) vv x
[PROOF STEP]
apply (erule conjE,
        frule_tac v = "vv (Suc 0)" and v' = "vv 0" in
        nonequiv_ex_Ostrowski_elem, assumption+,
        erule bexE,
        thin_tac "\<not> v_equiv K (vv (Suc 0)) (vv 0)",
        thin_tac "\<not> v_equiv K (vv 0) (vv (Suc 0))")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x xa. \<lbrakk>{i. i \<le> Suc 0} = {0, Suc 0}; valuation K (vv 0); valuation K (vv (Suc 0)); x \<in> carrier K; 0 \<le> vv 0 x; vv (Suc 0) x < 0; xa \<in> carrier K; 0 \<le> vv (Suc 0) xa \<and> vv 0 xa < 0\<rbrakk> \<Longrightarrow> \<exists>x\<in>carrier K. Ostrowski_elem K (Suc 0) vv x
[PROOF STEP]
apply (rename_tac s t)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>s t. \<lbrakk>{i. i \<le> Suc 0} = {0, Suc 0}; valuation K (vv 0); valuation K (vv (Suc 0)); s \<in> carrier K; 0 \<le> vv 0 s; vv (Suc 0) s < 0; t \<in> carrier K; 0 \<le> vv (Suc 0) t \<and> vv 0 t < 0\<rbrakk> \<Longrightarrow> \<exists>x\<in>carrier K. Ostrowski_elem K (Suc 0) vv x
[PROOF STEP]
(* we show s and t are non-zero in the following 4
                          lines *)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>s t. \<lbrakk>{i. i \<le> Suc 0} = {0, Suc 0}; valuation K (vv 0); valuation K (vv (Suc 0)); s \<in> carrier K; 0 \<le> vv 0 s; vv (Suc 0) s < 0; t \<in> carrier K; 0 \<le> vv (Suc 0) t \<and> vv 0 t < 0\<rbrakk> \<Longrightarrow> \<exists>x\<in>carrier K. Ostrowski_elem K (Suc 0) vv x
[PROOF STEP]
apply (erule conjE,
        frule_tac x = t and v = "vv 0" in val_neg_nonzero, assumption+)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>s t. \<lbrakk>{i. i \<le> Suc 0} = {0, Suc 0}; valuation K (vv 0); valuation K (vv (Suc 0)); s \<in> carrier K; 0 \<le> vv 0 s; vv (Suc 0) s < 0; t \<in> carrier K; 0 \<le> vv (Suc 0) t; vv 0 t < 0; t \<noteq> \<zero>\<rbrakk> \<Longrightarrow> \<exists>x\<in>carrier K. Ostrowski_elem K (Suc 0) vv x
[PROOF STEP]
apply (simp add:less_ant_def, (erule conjE)+,
       frule_tac x = s and v = "vv (Suc 0)" in val_neg_nonzero,
       assumption+, unfold less_ant_def)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>s t. \<lbrakk>{i. i \<le> Suc 0} = {0, Suc 0}; valuation K (vv 0); valuation K (vv (Suc 0)); s \<in> carrier K; 0 \<le> vv 0 s; t \<in> carrier K; 0 \<le> vv (Suc 0) t; t \<noteq> \<zero>; vv (Suc 0) s \<le> 0; vv (Suc 0) s \<noteq> 0; vv 0 t \<le> 0; vv 0 t \<noteq> 0\<rbrakk> \<Longrightarrow> vv (Suc 0) s \<le> 0 \<and> vv (Suc 0) s \<noteq> 0
 2. \<And>s t. \<lbrakk>{i. i \<le> Suc 0} = {0, Suc 0}; valuation K (vv 0); valuation K (vv (Suc 0)); s \<in> carrier K; 0 \<le> vv 0 s; t \<in> carrier K; 0 \<le> vv (Suc 0) t; t \<noteq> \<zero>; vv (Suc 0) s \<le> 0; vv (Suc 0) s \<noteq> 0; vv 0 t \<le> 0; vv 0 t \<noteq> 0; s \<noteq> \<zero>\<rbrakk> \<Longrightarrow> \<exists>x\<in>carrier K. Ostrowski_elem K (Suc 0) vv x
[PROOF STEP]
apply (rule conjI, assumption+)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>s t. \<lbrakk>{i. i \<le> Suc 0} = {0, Suc 0}; valuation K (vv 0); valuation K (vv (Suc 0)); s \<in> carrier K; 0 \<le> vv 0 s; t \<in> carrier K; 0 \<le> vv (Suc 0) t; t \<noteq> \<zero>; vv (Suc 0) s \<le> 0; vv (Suc 0) s \<noteq> 0; vv 0 t \<le> 0; vv 0 t \<noteq> 0; s \<noteq> \<zero>\<rbrakk> \<Longrightarrow> \<exists>x\<in>carrier K. Ostrowski_elem K (Suc 0) vv x
[PROOF STEP]
apply (frule_tac s = s and t = t and v = "vv 0" in OstrowskiTr2,
        assumption+, rule ale_neq_less, assumption+)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>s t. \<lbrakk>{i. i \<le> Suc 0} = {0, Suc 0}; valuation K (vv 0); valuation K (vv (Suc 0)); s \<in> carrier K; 0 \<le> vv 0 s; t \<in> carrier K; 0 \<le> vv (Suc 0) t; t \<noteq> \<zero>; vv (Suc 0) s \<le> 0; vv (Suc 0) s \<noteq> 0; vv 0 t \<le> 0; vv 0 t \<noteq> 0; s \<noteq> \<zero>; 0 < vv 0 (1\<^sub>r \<plusminus> -\<^sub>a t \<cdot>\<^sub>r (s \<plusminus> t)\<^bsup>\<hyphen> K\<^esup>)\<rbrakk> \<Longrightarrow> \<exists>x\<in>carrier K. Ostrowski_elem K (Suc 0) vv x
[PROOF STEP]
apply (frule_tac s = s and t = t and v = "vv (Suc 0)" in OstrowskiTr3,
         assumption+, rule ale_neq_less, assumption+)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>s t. \<lbrakk>{i. i \<le> Suc 0} = {0, Suc 0}; valuation K (vv 0); valuation K (vv (Suc 0)); s \<in> carrier K; 0 \<le> vv 0 s; t \<in> carrier K; 0 \<le> vv (Suc 0) t; t \<noteq> \<zero>; vv (Suc 0) s \<le> 0; vv (Suc 0) s \<noteq> 0; vv 0 t \<le> 0; vv 0 t \<noteq> 0; s \<noteq> \<zero>; 0 < vv 0 (1\<^sub>r \<plusminus> -\<^sub>a t \<cdot>\<^sub>r (s \<plusminus> t)\<^bsup>\<hyphen> K\<^esup>); 0 < vv (Suc 0) (t \<cdot>\<^sub>r (s \<plusminus> t)\<^bsup>\<hyphen> K\<^esup>)\<rbrakk> \<Longrightarrow> \<exists>x\<in>carrier K. Ostrowski_elem K (Suc 0) vv x
[PROOF STEP]
apply (subgoal_tac "t \<cdot>\<^sub>r (( s \<plusminus> t)\<^bsup>\<hyphen>K\<^esup>) \<in> carrier K",
        simp only:Ostrowski_elem_def,
        simp only: nset_m_m[of "Suc 0"], blast)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>s t. \<lbrakk>{i. i \<le> Suc 0} = {0, Suc 0}; valuation K (vv 0); valuation K (vv (Suc 0)); s \<in> carrier K; 0 \<le> vv 0 s; t \<in> carrier K; 0 \<le> vv (Suc 0) t; t \<noteq> \<zero>; vv (Suc 0) s \<le> 0; vv (Suc 0) s \<noteq> 0; vv 0 t \<le> 0; vv 0 t \<noteq> 0; s \<noteq> \<zero>; 0 < vv 0 (1\<^sub>r \<plusminus> -\<^sub>a t \<cdot>\<^sub>r (s \<plusminus> t)\<^bsup>\<hyphen> K\<^esup>); 0 < vv (Suc 0) (t \<cdot>\<^sub>r (s \<plusminus> t)\<^bsup>\<hyphen> K\<^esup>)\<rbrakk> \<Longrightarrow> t \<cdot>\<^sub>r (s \<plusminus> t)\<^bsup>\<hyphen> K\<^esup> \<in> carrier K
[PROOF STEP]
(* Here simp add:nset_m_m[of "Suc 0"] wouldn't work *)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>s t. \<lbrakk>{i. i \<le> Suc 0} = {0, Suc 0}; valuation K (vv 0); valuation K (vv (Suc 0)); s \<in> carrier K; 0 \<le> vv 0 s; t \<in> carrier K; 0 \<le> vv (Suc 0) t; t \<noteq> \<zero>; vv (Suc 0) s \<le> 0; vv (Suc 0) s \<noteq> 0; vv 0 t \<le> 0; vv 0 t \<noteq> 0; s \<noteq> \<zero>; 0 < vv 0 (1\<^sub>r \<plusminus> -\<^sub>a t \<cdot>\<^sub>r (s \<plusminus> t)\<^bsup>\<hyphen> K\<^esup>); 0 < vv (Suc 0) (t \<cdot>\<^sub>r (s \<plusminus> t)\<^bsup>\<hyphen> K\<^esup>)\<rbrakk> \<Longrightarrow> t \<cdot>\<^sub>r (s \<plusminus> t)\<^bsup>\<hyphen> K\<^esup> \<in> carrier K
[PROOF STEP]
apply (cut_tac field_is_ring, frule Ring.ring_is_ag[of "K"],
        rule Ring.ring_tOp_closed, assumption+,
        frule_tac s = s and t = t and v = "vv 0" in OstrowskiTr1,
        assumption+, rule ale_neq_less, assumption+,
        frule_tac x = s and y = t in aGroup.ag_pOp_closed[of "K"], assumption+)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>s t. \<lbrakk>{i. i \<le> Suc 0} = {0, Suc 0}; valuation K (vv 0); valuation K (vv (Suc 0)); s \<in> carrier K; 0 \<le> vv 0 s; t \<in> carrier K; 0 \<le> vv (Suc 0) t; t \<noteq> \<zero>; vv (Suc 0) s \<le> 0; vv (Suc 0) s \<noteq> 0; vv 0 t \<le> 0; vv 0 t \<noteq> 0; s \<noteq> \<zero>; 0 < vv 0 (1\<^sub>r \<plusminus> -\<^sub>a t \<cdot>\<^sub>r (s \<plusminus> t)\<^bsup>\<hyphen> K\<^esup>); 0 < vv (Suc 0) (t \<cdot>\<^sub>r (s \<plusminus> t)\<^bsup>\<hyphen> K\<^esup>); Ring K; aGroup K; s \<plusminus> t \<noteq> \<zero>; s \<plusminus> t \<in> carrier K\<rbrakk> \<Longrightarrow> (s \<plusminus> t)\<^bsup>\<hyphen> K\<^esup> \<in> carrier K
[PROOF STEP]
apply (cut_tac x = "s \<plusminus> t" in invf_closed, blast)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>s t. \<lbrakk>{i. i \<le> Suc 0} = {0, Suc 0}; valuation K (vv 0); valuation K (vv (Suc 0)); s \<in> carrier K; 0 \<le> vv 0 s; t \<in> carrier K; 0 \<le> vv (Suc 0) t; t \<noteq> \<zero>; vv (Suc 0) s \<le> 0; vv (Suc 0) s \<noteq> 0; vv 0 t \<le> 0; vv 0 t \<noteq> 0; s \<noteq> \<zero>; 0 < vv 0 (1\<^sub>r \<plusminus> -\<^sub>a t \<cdot>\<^sub>r (s \<plusminus> t)\<^bsup>\<hyphen> K\<^esup>); 0 < vv (Suc 0) (t \<cdot>\<^sub>r (s \<plusminus> t)\<^bsup>\<hyphen> K\<^esup>); Ring K; aGroup K; s \<plusminus> t \<noteq> \<zero>; s \<plusminus> t \<in> carrier K; (s \<plusminus> t)\<^bsup>\<hyphen> K\<^esup> \<in> carrier K\<rbrakk> \<Longrightarrow> (s \<plusminus> t)\<^bsup>\<hyphen> K\<^esup> \<in> carrier K
[PROOF STEP]
apply assumption
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
(* in the above two lines, simp wouldn't work *)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma (in Corps) Ostrowski:"\<forall>vv. vals_nonequiv K (Suc n) vv \<longrightarrow>
                        (\<exists>x\<in>carrier K. Ostrowski_elem K (Suc n) vv x)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>vv. vals_nonequiv K (Suc n) vv \<longrightarrow> (\<exists>x\<in>carrier K. Ostrowski_elem K (Suc n) vv x)
[PROOF STEP]
apply (induct_tac n,
 rule allI, rule impI, simp add:Ostrowski_first)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>n. \<forall>vv. vals_nonequiv K (Suc n) vv \<longrightarrow> (\<exists>x\<in>carrier K. Ostrowski_elem K (Suc n) vv x) \<Longrightarrow> \<forall>vv. vals_nonequiv K (Suc (Suc n)) vv \<longrightarrow> (\<exists>x\<in>carrier K. Ostrowski_elem K (Suc (Suc n)) vv x)
[PROOF STEP]
(** case (Suc n) **)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>n. \<forall>vv. vals_nonequiv K (Suc n) vv \<longrightarrow> (\<exists>x\<in>carrier K. Ostrowski_elem K (Suc n) vv x) \<Longrightarrow> \<forall>vv. vals_nonequiv K (Suc (Suc n)) vv \<longrightarrow> (\<exists>x\<in>carrier K. Ostrowski_elem K (Suc (Suc n)) vv x)
[PROOF STEP]
apply (rule allI, rule impI,
       frule_tac n = n and vv = vv in restrict_vals_nonequiv1,
       frule_tac n = n and vv = vv in restrict_vals_nonequiv2,
       frule_tac a = "compose {h. h \<le> Suc n} vv (skip 1)" in forall_spec,
        assumption,
       drule_tac a = "compose {h. h \<le> Suc n} vv (skip 2)" in forall_spec,
         assumption+, (erule bexE)+)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>n vv x xa. \<lbrakk>vals_nonequiv K (Suc (Suc n)) vv; vals_nonequiv K (Suc n) (compose {h. h \<le> Suc n} vv (skip 1)); vals_nonequiv K (Suc n) (compose {j. j \<le> Suc n} vv (skip 2)); x \<in> carrier K; Ostrowski_elem K (Suc n) (compose {h. h \<le> Suc n} vv (skip 1)) x; xa \<in> carrier K; Ostrowski_elem K (Suc n) (compose {h. h \<le> Suc n} vv (skip 2)) xa\<rbrakk> \<Longrightarrow> \<exists>x\<in>carrier K. Ostrowski_elem K (Suc (Suc n)) vv x
[PROOF STEP]
apply (rename_tac n vv s t,
       cut_tac field_is_ring, frule Ring.ring_is_ag[of "K"])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>n vv s t. \<lbrakk>vals_nonequiv K (Suc (Suc n)) vv; vals_nonequiv K (Suc n) (compose {h. h \<le> Suc n} vv (skip 1)); vals_nonequiv K (Suc n) (compose {j. j \<le> Suc n} vv (skip 2)); s \<in> carrier K; Ostrowski_elem K (Suc n) (compose {h. h \<le> Suc n} vv (skip 1)) s; t \<in> carrier K; Ostrowski_elem K (Suc n) (compose {h. h \<le> Suc n} vv (skip 2)) t; Ring K; aGroup K\<rbrakk> \<Longrightarrow> \<exists>x\<in>carrier K. Ostrowski_elem K (Suc (Suc n)) vv x
[PROOF STEP]
(**  case * * *  **)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>n vv s t. \<lbrakk>vals_nonequiv K (Suc (Suc n)) vv; vals_nonequiv K (Suc n) (compose {h. h \<le> Suc n} vv (skip 1)); vals_nonequiv K (Suc n) (compose {j. j \<le> Suc n} vv (skip 2)); s \<in> carrier K; Ostrowski_elem K (Suc n) (compose {h. h \<le> Suc n} vv (skip 1)) s; t \<in> carrier K; Ostrowski_elem K (Suc n) (compose {h. h \<le> Suc n} vv (skip 2)) t; Ring K; aGroup K\<rbrakk> \<Longrightarrow> \<exists>x\<in>carrier K. Ostrowski_elem K (Suc (Suc n)) vv x
[PROOF STEP]
apply (frule_tac x = s and y = t in Ring.ring_tOp_closed[of "K"], assumption+,
        case_tac "0 \<le> vv (Suc 0) s \<and> 0 \<le> vv (Suc (Suc 0)) t",
        frule_tac vv = vv and s = s and t = t in OstrowskiTr5, assumption+)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>n vv s t. \<lbrakk>vals_nonequiv K (Suc (Suc n)) vv; vals_nonequiv K (Suc n) (compose {h. h \<le> Suc n} vv (skip 1)); vals_nonequiv K (Suc n) (compose {j. j \<le> Suc n} vv (skip 2)); s \<in> carrier K; Ostrowski_elem K (Suc n) (compose {h. h \<le> Suc n} vv (skip 1)) s; t \<in> carrier K; Ostrowski_elem K (Suc n) (compose {h. h \<le> Suc n} vv (skip 2)) t; Ring K; aGroup K; s \<cdot>\<^sub>r t \<in> carrier K; 0 \<le> vv (Suc 0) s \<and> 0 \<le> vv (Suc (Suc 0)) t; Ostrowski_elem K (Suc (Suc n)) vv (s \<cdot>\<^sub>r t)\<rbrakk> \<Longrightarrow> \<exists>x\<in>carrier K. Ostrowski_elem K (Suc (Suc n)) vv x
 2. \<And>n vv s t. \<lbrakk>vals_nonequiv K (Suc (Suc n)) vv; vals_nonequiv K (Suc n) (compose {h. h \<le> Suc n} vv (skip 1)); vals_nonequiv K (Suc n) (compose {j. j \<le> Suc n} vv (skip 2)); s \<in> carrier K; Ostrowski_elem K (Suc n) (compose {h. h \<le> Suc n} vv (skip 1)) s; t \<in> carrier K; Ostrowski_elem K (Suc n) (compose {h. h \<le> Suc n} vv (skip 2)) t; Ring K; aGroup K; s \<cdot>\<^sub>r t \<in> carrier K; \<not> (0 \<le> vv (Suc 0) s \<and> 0 \<le> vv (Suc (Suc 0)) t)\<rbrakk> \<Longrightarrow> \<exists>x\<in>carrier K. Ostrowski_elem K (Suc (Suc n)) vv x
[PROOF STEP]
apply blast
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>n vv s t. \<lbrakk>vals_nonequiv K (Suc (Suc n)) vv; vals_nonequiv K (Suc n) (compose {h. h \<le> Suc n} vv (skip 1)); vals_nonequiv K (Suc n) (compose {j. j \<le> Suc n} vv (skip 2)); s \<in> carrier K; Ostrowski_elem K (Suc n) (compose {h. h \<le> Suc n} vv (skip 1)) s; t \<in> carrier K; Ostrowski_elem K (Suc n) (compose {h. h \<le> Suc n} vv (skip 2)) t; Ring K; aGroup K; s \<cdot>\<^sub>r t \<in> carrier K; \<not> (0 \<le> vv (Suc 0) s \<and> 0 \<le> vv (Suc (Suc 0)) t)\<rbrakk> \<Longrightarrow> \<exists>x\<in>carrier K. Ostrowski_elem K (Suc (Suc n)) vv x
[PROOF STEP]
(** case * * * **)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>n vv s t. \<lbrakk>vals_nonequiv K (Suc (Suc n)) vv; vals_nonequiv K (Suc n) (compose {h. h \<le> Suc n} vv (skip 1)); vals_nonequiv K (Suc n) (compose {j. j \<le> Suc n} vv (skip 2)); s \<in> carrier K; Ostrowski_elem K (Suc n) (compose {h. h \<le> Suc n} vv (skip 1)) s; t \<in> carrier K; Ostrowski_elem K (Suc n) (compose {h. h \<le> Suc n} vv (skip 2)) t; Ring K; aGroup K; s \<cdot>\<^sub>r t \<in> carrier K; \<not> (0 \<le> vv (Suc 0) s \<and> 0 \<le> vv (Suc (Suc 0)) t)\<rbrakk> \<Longrightarrow> \<exists>x\<in>carrier K. Ostrowski_elem K (Suc (Suc n)) vv x
[PROOF STEP]
apply (simp,
       case_tac "0 \<le> (vv (Suc 0) s)", simp,
       frule_tac n = "Suc (Suc n)" and m = "Suc (Suc 0)" and vv = vv in
         vals_nonequiv_valuation,
       simp,
       frule_tac v = "vv (Suc (Suc 0))" and x = t in OstrowskiTr6,
         assumption+,
       frule_tac x = "1\<^sub>r \<plusminus> t \<cdot>\<^sub>r (1\<^sub>r \<plusminus> -\<^sub>a t)" in invf_closed1,
       frule_tac x = t and y = "(1\<^sub>r \<plusminus> t \<cdot>\<^sub>r (1\<^sub>r \<plusminus> -\<^sub>a t))\<^bsup>\<hyphen>K\<^esup>" in
               Ring.ring_tOp_closed, assumption+, simp)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>n vv s t. \<lbrakk>vals_nonequiv K (Suc (Suc n)) vv; vals_nonequiv K (Suc n) (compose {h. h \<le> Suc n} vv (skip (Suc 0))); vals_nonequiv K (Suc n) (compose {j. j \<le> Suc n} vv (skip 2)); s \<in> carrier K; Ostrowski_elem K (Suc n) (compose {h. h \<le> Suc n} vv (skip (Suc 0))) s; t \<in> carrier K; Ostrowski_elem K (Suc n) (compose {h. h \<le> Suc n} vv (skip 2)) t; Ring K; aGroup K; s \<cdot>\<^sub>r t \<in> carrier K; \<not> 0 \<le> vv (Suc (Suc 0)) t; 0 \<le> vv (Suc 0) s; valuation K (vv (Suc (Suc 0))); 1\<^sub>r \<plusminus> t \<cdot>\<^sub>r (1\<^sub>r \<plusminus> -\<^sub>a t) \<in> carrier K - {\<zero>}; (1\<^sub>r \<plusminus> t \<cdot>\<^sub>r (1\<^sub>r \<plusminus> -\<^sub>a t))\<^bsup>\<hyphen> K\<^esup> \<in> carrier K - {\<zero>}; t \<cdot>\<^sub>r (1\<^sub>r \<plusminus> t \<cdot>\<^sub>r (1\<^sub>r \<plusminus> -\<^sub>a t))\<^bsup>\<hyphen> K\<^esup> \<in> carrier K\<rbrakk> \<Longrightarrow> \<exists>x\<in>carrier K. Ostrowski_elem K (Suc (Suc n)) vv x
 2. \<And>n vv s t. \<lbrakk>vals_nonequiv K (Suc (Suc n)) vv; vals_nonequiv K (Suc n) (compose {h. h \<le> Suc n} vv (skip (Suc 0))); vals_nonequiv K (Suc n) (compose {j. j \<le> Suc n} vv (skip 2)); s \<in> carrier K; Ostrowski_elem K (Suc n) (compose {h. h \<le> Suc n} vv (skip (Suc 0))) s; t \<in> carrier K; Ostrowski_elem K (Suc n) (compose {h. h \<le> Suc n} vv (skip 2)) t; Ring K; aGroup K; s \<cdot>\<^sub>r t \<in> carrier K; 0 \<le> vv (Suc 0) s \<longrightarrow> \<not> 0 \<le> vv (Suc (Suc 0)) t; \<not> 0 \<le> vv (Suc 0) s\<rbrakk> \<Longrightarrow> \<exists>x\<in>carrier K. Ostrowski_elem K (Suc (Suc n)) vv x
[PROOF STEP]
apply (subgoal_tac "Ostrowski_elem K (Suc (Suc n)) vv
                       (t \<cdot>\<^sub>r ((1\<^sub>r \<plusminus> t \<cdot>\<^sub>r (1\<^sub>r \<plusminus> (-\<^sub>a t)))\<^bsup>\<hyphen>K\<^esup>))",
       blast)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>n vv s t. \<lbrakk>vals_nonequiv K (Suc (Suc n)) vv; vals_nonequiv K (Suc n) (compose {h. h \<le> Suc n} vv (skip (Suc 0))); vals_nonequiv K (Suc n) (compose {j. j \<le> Suc n} vv (skip 2)); s \<in> carrier K; Ostrowski_elem K (Suc n) (compose {h. h \<le> Suc n} vv (skip (Suc 0))) s; t \<in> carrier K; Ostrowski_elem K (Suc n) (compose {h. h \<le> Suc n} vv (skip 2)) t; Ring K; aGroup K; s \<cdot>\<^sub>r t \<in> carrier K; \<not> 0 \<le> vv (Suc (Suc 0)) t; 0 \<le> vv (Suc 0) s; valuation K (vv (Suc (Suc 0))); 1\<^sub>r \<plusminus> t \<cdot>\<^sub>r (1\<^sub>r \<plusminus> -\<^sub>a t) \<in> carrier K - {\<zero>}; (1\<^sub>r \<plusminus> t \<cdot>\<^sub>r (1\<^sub>r \<plusminus> -\<^sub>a t))\<^bsup>\<hyphen> K\<^esup> \<in> carrier K - {\<zero>}; t \<cdot>\<^sub>r (1\<^sub>r \<plusminus> t \<cdot>\<^sub>r (1\<^sub>r \<plusminus> -\<^sub>a t))\<^bsup>\<hyphen> K\<^esup> \<in> carrier K\<rbrakk> \<Longrightarrow> Ostrowski_elem K (Suc (Suc n)) vv (t \<cdot>\<^sub>r (1\<^sub>r \<plusminus> t \<cdot>\<^sub>r (1\<^sub>r \<plusminus> -\<^sub>a t))\<^bsup>\<hyphen> K\<^esup>)
 2. \<And>n vv s t. \<lbrakk>vals_nonequiv K (Suc (Suc n)) vv; vals_nonequiv K (Suc n) (compose {h. h \<le> Suc n} vv (skip (Suc 0))); vals_nonequiv K (Suc n) (compose {j. j \<le> Suc n} vv (skip 2)); s \<in> carrier K; Ostrowski_elem K (Suc n) (compose {h. h \<le> Suc n} vv (skip (Suc 0))) s; t \<in> carrier K; Ostrowski_elem K (Suc n) (compose {h. h \<le> Suc n} vv (skip 2)) t; Ring K; aGroup K; s \<cdot>\<^sub>r t \<in> carrier K; 0 \<le> vv (Suc 0) s \<longrightarrow> \<not> 0 \<le> vv (Suc (Suc 0)) t; \<not> 0 \<le> vv (Suc 0) s\<rbrakk> \<Longrightarrow> \<exists>x\<in>carrier K. Ostrowski_elem K (Suc (Suc n)) vv x
[PROOF STEP]
apply (subst Ostrowski_elem_def,
       rule conjI,
       thin_tac "Ostrowski_elem K (Suc n)
         (compose {h. h \<le> Suc n} vv (skip (Suc 0))) s",
       thin_tac "vals_nonequiv K (Suc n)
         (compose {h. h \<le> Suc n} vv (skip (Suc 0)))",
       thin_tac "vals_nonequiv K (Suc n) (compose {h. h\<le> Suc n} vv (skip 2))",
       thin_tac "0 \<le> (vv (Suc 0) s)",
       frule_tac n = "Suc (Suc n)" and vv = vv and m = 0 in
                      vals_nonequiv_valuation, simp,
       rule_tac v = "vv 0" and x = t in
          OstrowskiTr8, assumption+)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>n vv s t. \<lbrakk>vals_nonequiv K (Suc (Suc n)) vv; s \<in> carrier K; t \<in> carrier K; Ostrowski_elem K (Suc n) (compose {h. h \<le> Suc n} vv (skip 2)) t; Ring K; aGroup K; s \<cdot>\<^sub>r t \<in> carrier K; \<not> 0 \<le> vv (Suc (Suc 0)) t; valuation K (vv (Suc (Suc 0))); 1\<^sub>r \<plusminus> t \<cdot>\<^sub>r (1\<^sub>r \<plusminus> -\<^sub>a t) \<in> carrier K - {\<zero>}; (1\<^sub>r \<plusminus> t \<cdot>\<^sub>r (1\<^sub>r \<plusminus> -\<^sub>a t))\<^bsup>\<hyphen> K\<^esup> \<in> carrier K - {\<zero>}; t \<cdot>\<^sub>r (1\<^sub>r \<plusminus> t \<cdot>\<^sub>r (1\<^sub>r \<plusminus> -\<^sub>a t))\<^bsup>\<hyphen> K\<^esup> \<in> carrier K; valuation K (vv 0)\<rbrakk> \<Longrightarrow> 0 < vv 0 (1\<^sub>r \<plusminus> -\<^sub>a t)
 2. \<And>n vv s t. \<lbrakk>vals_nonequiv K (Suc (Suc n)) vv; vals_nonequiv K (Suc n) (compose {h. h \<le> Suc n} vv (skip (Suc 0))); vals_nonequiv K (Suc n) (compose {j. j \<le> Suc n} vv (skip 2)); s \<in> carrier K; Ostrowski_elem K (Suc n) (compose {h. h \<le> Suc n} vv (skip (Suc 0))) s; t \<in> carrier K; Ostrowski_elem K (Suc n) (compose {h. h \<le> Suc n} vv (skip 2)) t; Ring K; aGroup K; s \<cdot>\<^sub>r t \<in> carrier K; \<not> 0 \<le> vv (Suc (Suc 0)) t; 0 \<le> vv (Suc 0) s; valuation K (vv (Suc (Suc 0))); 1\<^sub>r \<plusminus> t \<cdot>\<^sub>r (1\<^sub>r \<plusminus> -\<^sub>a t) \<in> carrier K - {\<zero>}; (1\<^sub>r \<plusminus> t \<cdot>\<^sub>r (1\<^sub>r \<plusminus> -\<^sub>a t))\<^bsup>\<hyphen> K\<^esup> \<in> carrier K - {\<zero>}; t \<cdot>\<^sub>r (1\<^sub>r \<plusminus> t \<cdot>\<^sub>r (1\<^sub>r \<plusminus> -\<^sub>a t))\<^bsup>\<hyphen> K\<^esup> \<in> carrier K\<rbrakk> \<Longrightarrow> \<forall>j\<in>nset (Suc 0) (Suc (Suc n)). 0 < vv j (t \<cdot>\<^sub>r (1\<^sub>r \<plusminus> t \<cdot>\<^sub>r (1\<^sub>r \<plusminus> -\<^sub>a t))\<^bsup>\<hyphen> K\<^esup>)
 3. \<And>n vv s t. \<lbrakk>vals_nonequiv K (Suc (Suc n)) vv; vals_nonequiv K (Suc n) (compose {h. h \<le> Suc n} vv (skip (Suc 0))); vals_nonequiv K (Suc n) (compose {j. j \<le> Suc n} vv (skip 2)); s \<in> carrier K; Ostrowski_elem K (Suc n) (compose {h. h \<le> Suc n} vv (skip (Suc 0))) s; t \<in> carrier K; Ostrowski_elem K (Suc n) (compose {h. h \<le> Suc n} vv (skip 2)) t; Ring K; aGroup K; s \<cdot>\<^sub>r t \<in> carrier K; 0 \<le> vv (Suc 0) s \<longrightarrow> \<not> 0 \<le> vv (Suc (Suc 0)) t; \<not> 0 \<le> vv (Suc 0) s\<rbrakk> \<Longrightarrow> \<exists>x\<in>carrier K. Ostrowski_elem K (Suc (Suc n)) vv x
[PROOF STEP]
apply (simp add:Ostrowski_elem_def, (erule conjE)+,
       thin_tac "\<forall>j\<in>nset (Suc 0) (Suc n).
            0 < (compose {h. h \<le> (Suc n)} vv (skip 2) j t)",
       simp add:compose_def skip_def,
       rule ballI,
       thin_tac "0 \<le> (vv (Suc 0) s)",
       thin_tac "Ostrowski_elem K (Suc n)
                    (compose {h. h \<le> (Suc n)} vv (skip (Suc 0))) s",
       frule_tac n = "Suc (Suc n)" and vv = vv and m = j in
                     vals_nonequiv_valuation,
       simp add:nset_def, simp add:Ostrowski_elem_def, (erule conjE)+)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>n vv s t j. \<lbrakk>vals_nonequiv K (Suc (Suc n)) vv; vals_nonequiv K (Suc n) (compose {h. h \<le> Suc n} vv (skip (Suc 0))); vals_nonequiv K (Suc n) (compose {j. j \<le> Suc n} vv (skip 2)); s \<in> carrier K; t \<in> carrier K; Ring K; aGroup K; s \<cdot>\<^sub>r t \<in> carrier K; \<not> 0 \<le> vv (Suc (Suc 0)) t; valuation K (vv (Suc (Suc 0))); t \<cdot>\<^sub>r (1\<^sub>r \<plusminus> t \<cdot>\<^sub>r (1\<^sub>r \<plusminus> -\<^sub>a t))\<^bsup>\<hyphen> K\<^esup> \<in> carrier K; j \<in> nset (Suc 0) (Suc (Suc n)); valuation K (vv j); 0 < compose {h. h \<le> Suc n} vv (skip 2) 0 (1\<^sub>r \<plusminus> -\<^sub>a t); \<forall>j\<in>nset (Suc 0) (Suc n). 0 < compose {h. h \<le> Suc n} vv (skip 2) j t; 1\<^sub>r \<plusminus> t \<cdot>\<^sub>r (1\<^sub>r \<plusminus> -\<^sub>a t) \<in> carrier K; 1\<^sub>r \<plusminus> t \<cdot>\<^sub>r (1\<^sub>r \<plusminus> -\<^sub>a t) \<noteq> \<zero>; (1\<^sub>r \<plusminus> t \<cdot>\<^sub>r (1\<^sub>r \<plusminus> -\<^sub>a t))\<^bsup>\<hyphen> K\<^esup> \<in> carrier K; (1\<^sub>r \<plusminus> t \<cdot>\<^sub>r (1\<^sub>r \<plusminus> -\<^sub>a t))\<^bsup>\<hyphen> K\<^esup> \<noteq> \<zero>\<rbrakk> \<Longrightarrow> 0 < vv j (t \<cdot>\<^sub>r (1\<^sub>r \<plusminus> t \<cdot>\<^sub>r (1\<^sub>r \<plusminus> -\<^sub>a t))\<^bsup>\<hyphen> K\<^esup>)
 2. \<And>n vv s t. \<lbrakk>vals_nonequiv K (Suc (Suc n)) vv; vals_nonequiv K (Suc n) (compose {h. h \<le> Suc n} vv (skip (Suc 0))); vals_nonequiv K (Suc n) (compose {j. j \<le> Suc n} vv (skip 2)); s \<in> carrier K; Ostrowski_elem K (Suc n) (compose {h. h \<le> Suc n} vv (skip (Suc 0))) s; t \<in> carrier K; Ostrowski_elem K (Suc n) (compose {h. h \<le> Suc n} vv (skip 2)) t; Ring K; aGroup K; s \<cdot>\<^sub>r t \<in> carrier K; 0 \<le> vv (Suc 0) s \<longrightarrow> \<not> 0 \<le> vv (Suc (Suc 0)) t; \<not> 0 \<le> vv (Suc 0) s\<rbrakk> \<Longrightarrow> \<exists>x\<in>carrier K. Ostrowski_elem K (Suc (Suc n)) vv x
[PROOF STEP]
(** case * * * **)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>n vv s t j. \<lbrakk>vals_nonequiv K (Suc (Suc n)) vv; vals_nonequiv K (Suc n) (compose {h. h \<le> Suc n} vv (skip (Suc 0))); vals_nonequiv K (Suc n) (compose {j. j \<le> Suc n} vv (skip 2)); s \<in> carrier K; t \<in> carrier K; Ring K; aGroup K; s \<cdot>\<^sub>r t \<in> carrier K; \<not> 0 \<le> vv (Suc (Suc 0)) t; valuation K (vv (Suc (Suc 0))); t \<cdot>\<^sub>r (1\<^sub>r \<plusminus> t \<cdot>\<^sub>r (1\<^sub>r \<plusminus> -\<^sub>a t))\<^bsup>\<hyphen> K\<^esup> \<in> carrier K; j \<in> nset (Suc 0) (Suc (Suc n)); valuation K (vv j); 0 < compose {h. h \<le> Suc n} vv (skip 2) 0 (1\<^sub>r \<plusminus> -\<^sub>a t); \<forall>j\<in>nset (Suc 0) (Suc n). 0 < compose {h. h \<le> Suc n} vv (skip 2) j t; 1\<^sub>r \<plusminus> t \<cdot>\<^sub>r (1\<^sub>r \<plusminus> -\<^sub>a t) \<in> carrier K; 1\<^sub>r \<plusminus> t \<cdot>\<^sub>r (1\<^sub>r \<plusminus> -\<^sub>a t) \<noteq> \<zero>; (1\<^sub>r \<plusminus> t \<cdot>\<^sub>r (1\<^sub>r \<plusminus> -\<^sub>a t))\<^bsup>\<hyphen> K\<^esup> \<in> carrier K; (1\<^sub>r \<plusminus> t \<cdot>\<^sub>r (1\<^sub>r \<plusminus> -\<^sub>a t))\<^bsup>\<hyphen> K\<^esup> \<noteq> \<zero>\<rbrakk> \<Longrightarrow> 0 < vv j (t \<cdot>\<^sub>r (1\<^sub>r \<plusminus> t \<cdot>\<^sub>r (1\<^sub>r \<plusminus> -\<^sub>a t))\<^bsup>\<hyphen> K\<^esup>)
 2. \<And>n vv s t. \<lbrakk>vals_nonequiv K (Suc (Suc n)) vv; vals_nonequiv K (Suc n) (compose {h. h \<le> Suc n} vv (skip (Suc 0))); vals_nonequiv K (Suc n) (compose {j. j \<le> Suc n} vv (skip 2)); s \<in> carrier K; Ostrowski_elem K (Suc n) (compose {h. h \<le> Suc n} vv (skip (Suc 0))) s; t \<in> carrier K; Ostrowski_elem K (Suc n) (compose {h. h \<le> Suc n} vv (skip 2)) t; Ring K; aGroup K; s \<cdot>\<^sub>r t \<in> carrier K; 0 \<le> vv (Suc 0) s \<longrightarrow> \<not> 0 \<le> vv (Suc (Suc 0)) t; \<not> 0 \<le> vv (Suc 0) s\<rbrakk> \<Longrightarrow> \<exists>x\<in>carrier K. Ostrowski_elem K (Suc (Suc n)) vv x
[PROOF STEP]
apply (case_tac "j = Suc 0", simp,
        drule_tac x = "Suc 0" in bspec,
        simp add:nset_def,
        simp add:compose_def skip_def,
        rule_tac v = "vv (Suc 0)" and x = t in
         OstrowskiTr9, assumption+,
        frule_tac j = j and n = n in nset_Tr51, assumption+,
        drule_tac x = "j - Suc 0" in bspec, assumption+,
        simp add:compose_def skip_def)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>n vv s t j. \<lbrakk>vals_nonequiv K (Suc (Suc n)) vv; vals_nonequiv K (Suc n) (\<lambda>x\<in>{h. h \<le> Suc n}. vv (if x = 0 then x else Suc x)); vals_nonequiv K (Suc n) (\<lambda>x\<in>{j. j \<le> Suc n}. vv (if x \<le> Suc 0 then x else Suc x)); s \<in> carrier K; t \<in> carrier K; Ring K; aGroup K; s \<cdot>\<^sub>r t \<in> carrier K; \<not> 0 \<le> vv (Suc (Suc 0)) t; valuation K (vv (Suc (Suc 0))); t \<cdot>\<^sub>r (1\<^sub>r \<plusminus> t \<cdot>\<^sub>r (1\<^sub>r \<plusminus> -\<^sub>a t))\<^bsup>\<hyphen> K\<^esup> \<in> carrier K; j \<in> nset (Suc 0) (Suc (Suc n)); valuation K (vv j); 0 < vv 0 (1\<^sub>r \<plusminus> -\<^sub>a t); 1\<^sub>r \<plusminus> t \<cdot>\<^sub>r (1\<^sub>r \<plusminus> -\<^sub>a t) \<in> carrier K; 1\<^sub>r \<plusminus> t \<cdot>\<^sub>r (1\<^sub>r \<plusminus> -\<^sub>a t) \<noteq> \<zero>; (1\<^sub>r \<plusminus> t \<cdot>\<^sub>r (1\<^sub>r \<plusminus> -\<^sub>a t))\<^bsup>\<hyphen> K\<^esup> \<in> carrier K; (1\<^sub>r \<plusminus> t \<cdot>\<^sub>r (1\<^sub>r \<plusminus> -\<^sub>a t))\<^bsup>\<hyphen> K\<^esup> \<noteq> \<zero>; j \<noteq> Suc 0; j - Suc 0 \<in> nset (Suc 0) (Suc n); 0 < (if j - Suc 0 \<le> Suc n then vv (if j - Suc 0 \<le> Suc 0 then j - Suc 0 else Suc (j - Suc 0)) else undefined) t\<rbrakk> \<Longrightarrow> 0 < vv j (t \<cdot>\<^sub>r (1\<^sub>r \<plusminus> t \<cdot>\<^sub>r (1\<^sub>r \<plusminus> -\<^sub>a t))\<^bsup>\<hyphen> K\<^esup>)
 2. \<And>n vv s t. \<lbrakk>vals_nonequiv K (Suc (Suc n)) vv; vals_nonequiv K (Suc n) (compose {h. h \<le> Suc n} vv (skip (Suc 0))); vals_nonequiv K (Suc n) (compose {j. j \<le> Suc n} vv (skip 2)); s \<in> carrier K; Ostrowski_elem K (Suc n) (compose {h. h \<le> Suc n} vv (skip (Suc 0))) s; t \<in> carrier K; Ostrowski_elem K (Suc n) (compose {h. h \<le> Suc n} vv (skip 2)) t; Ring K; aGroup K; s \<cdot>\<^sub>r t \<in> carrier K; 0 \<le> vv (Suc 0) s \<longrightarrow> \<not> 0 \<le> vv (Suc (Suc 0)) t; \<not> 0 \<le> vv (Suc 0) s\<rbrakk> \<Longrightarrow> \<exists>x\<in>carrier K. Ostrowski_elem K (Suc (Suc n)) vv x
[PROOF STEP]
(** case * * * **)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>n vv s t j. \<lbrakk>vals_nonequiv K (Suc (Suc n)) vv; vals_nonequiv K (Suc n) (\<lambda>x\<in>{h. h \<le> Suc n}. vv (if x = 0 then x else Suc x)); vals_nonequiv K (Suc n) (\<lambda>x\<in>{j. j \<le> Suc n}. vv (if x \<le> Suc 0 then x else Suc x)); s \<in> carrier K; t \<in> carrier K; Ring K; aGroup K; s \<cdot>\<^sub>r t \<in> carrier K; \<not> 0 \<le> vv (Suc (Suc 0)) t; valuation K (vv (Suc (Suc 0))); t \<cdot>\<^sub>r (1\<^sub>r \<plusminus> t \<cdot>\<^sub>r (1\<^sub>r \<plusminus> -\<^sub>a t))\<^bsup>\<hyphen> K\<^esup> \<in> carrier K; j \<in> nset (Suc 0) (Suc (Suc n)); valuation K (vv j); 0 < vv 0 (1\<^sub>r \<plusminus> -\<^sub>a t); 1\<^sub>r \<plusminus> t \<cdot>\<^sub>r (1\<^sub>r \<plusminus> -\<^sub>a t) \<in> carrier K; 1\<^sub>r \<plusminus> t \<cdot>\<^sub>r (1\<^sub>r \<plusminus> -\<^sub>a t) \<noteq> \<zero>; (1\<^sub>r \<plusminus> t \<cdot>\<^sub>r (1\<^sub>r \<plusminus> -\<^sub>a t))\<^bsup>\<hyphen> K\<^esup> \<in> carrier K; (1\<^sub>r \<plusminus> t \<cdot>\<^sub>r (1\<^sub>r \<plusminus> -\<^sub>a t))\<^bsup>\<hyphen> K\<^esup> \<noteq> \<zero>; j \<noteq> Suc 0; j - Suc 0 \<in> nset (Suc 0) (Suc n); 0 < (if j - Suc 0 \<le> Suc n then vv (if j - Suc 0 \<le> Suc 0 then j - Suc 0 else Suc (j - Suc 0)) else undefined) t\<rbrakk> \<Longrightarrow> 0 < vv j (t \<cdot>\<^sub>r (1\<^sub>r \<plusminus> t \<cdot>\<^sub>r (1\<^sub>r \<plusminus> -\<^sub>a t))\<^bsup>\<hyphen> K\<^esup>)
 2. \<And>n vv s t. \<lbrakk>vals_nonequiv K (Suc (Suc n)) vv; vals_nonequiv K (Suc n) (compose {h. h \<le> Suc n} vv (skip (Suc 0))); vals_nonequiv K (Suc n) (compose {j. j \<le> Suc n} vv (skip 2)); s \<in> carrier K; Ostrowski_elem K (Suc n) (compose {h. h \<le> Suc n} vv (skip (Suc 0))) s; t \<in> carrier K; Ostrowski_elem K (Suc n) (compose {h. h \<le> Suc n} vv (skip 2)) t; Ring K; aGroup K; s \<cdot>\<^sub>r t \<in> carrier K; 0 \<le> vv (Suc 0) s \<longrightarrow> \<not> 0 \<le> vv (Suc (Suc 0)) t; \<not> 0 \<le> vv (Suc 0) s\<rbrakk> \<Longrightarrow> \<exists>x\<in>carrier K. Ostrowski_elem K (Suc (Suc n)) vv x
[PROOF STEP]
apply (case_tac "j = Suc (Suc 0)", simp)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>n vv s t j. \<lbrakk>vals_nonequiv K (Suc (Suc n)) vv; vals_nonequiv K (Suc n) (\<lambda>x\<in>{h. h \<le> Suc n}. vv (if x = 0 then x else Suc x)); vals_nonequiv K (Suc n) (\<lambda>x\<in>{j. j \<le> Suc n}. vv (if x \<le> Suc 0 then x else Suc x)); s \<in> carrier K; t \<in> carrier K; Ring K; aGroup K; s \<cdot>\<^sub>r t \<in> carrier K; \<not> 0 \<le> vv (Suc (Suc 0)) t; valuation K (vv (Suc (Suc 0))); t \<cdot>\<^sub>r (1\<^sub>r \<plusminus> t \<cdot>\<^sub>r (1\<^sub>r \<plusminus> -\<^sub>a t))\<^bsup>\<hyphen> K\<^esup> \<in> carrier K; Suc (Suc 0) \<in> nset (Suc 0) (Suc (Suc n)); 0 < vv 0 (1\<^sub>r \<plusminus> -\<^sub>a t); 1\<^sub>r \<plusminus> t \<cdot>\<^sub>r (1\<^sub>r \<plusminus> -\<^sub>a t) \<in> carrier K; 1\<^sub>r \<plusminus> t \<cdot>\<^sub>r (1\<^sub>r \<plusminus> -\<^sub>a t) \<noteq> \<zero>; (1\<^sub>r \<plusminus> t \<cdot>\<^sub>r (1\<^sub>r \<plusminus> -\<^sub>a t))\<^bsup>\<hyphen> K\<^esup> \<in> carrier K; (1\<^sub>r \<plusminus> t \<cdot>\<^sub>r (1\<^sub>r \<plusminus> -\<^sub>a t))\<^bsup>\<hyphen> K\<^esup> \<noteq> \<zero>; Suc 0 \<in> nset (Suc 0) (Suc n); 0 < vv (Suc 0) t; j = Suc (Suc 0)\<rbrakk> \<Longrightarrow> 0 < vv (Suc (Suc 0)) (t \<cdot>\<^sub>r (1\<^sub>r \<plusminus> t \<cdot>\<^sub>r (1\<^sub>r \<plusminus> -\<^sub>a t))\<^bsup>\<hyphen> K\<^esup>)
 2. \<And>n vv s t j. \<lbrakk>vals_nonequiv K (Suc (Suc n)) vv; vals_nonequiv K (Suc n) (\<lambda>x\<in>{h. h \<le> Suc n}. vv (if x = 0 then x else Suc x)); vals_nonequiv K (Suc n) (\<lambda>x\<in>{j. j \<le> Suc n}. vv (if x \<le> Suc 0 then x else Suc x)); s \<in> carrier K; t \<in> carrier K; Ring K; aGroup K; s \<cdot>\<^sub>r t \<in> carrier K; \<not> 0 \<le> vv (Suc (Suc 0)) t; valuation K (vv (Suc (Suc 0))); t \<cdot>\<^sub>r (1\<^sub>r \<plusminus> t \<cdot>\<^sub>r (1\<^sub>r \<plusminus> -\<^sub>a t))\<^bsup>\<hyphen> K\<^esup> \<in> carrier K; j \<in> nset (Suc 0) (Suc (Suc n)); valuation K (vv j); 0 < vv 0 (1\<^sub>r \<plusminus> -\<^sub>a t); 1\<^sub>r \<plusminus> t \<cdot>\<^sub>r (1\<^sub>r \<plusminus> -\<^sub>a t) \<in> carrier K; 1\<^sub>r \<plusminus> t \<cdot>\<^sub>r (1\<^sub>r \<plusminus> -\<^sub>a t) \<noteq> \<zero>; (1\<^sub>r \<plusminus> t \<cdot>\<^sub>r (1\<^sub>r \<plusminus> -\<^sub>a t))\<^bsup>\<hyphen> K\<^esup> \<in> carrier K; (1\<^sub>r \<plusminus> t \<cdot>\<^sub>r (1\<^sub>r \<plusminus> -\<^sub>a t))\<^bsup>\<hyphen> K\<^esup> \<noteq> \<zero>; j \<noteq> Suc 0; j - Suc 0 \<in> nset (Suc 0) (Suc n); 0 < (if j - Suc 0 \<le> Suc n then vv (if j - Suc 0 \<le> Suc 0 then j - Suc 0 else Suc (j - Suc 0)) else undefined) t; j \<noteq> Suc (Suc 0)\<rbrakk> \<Longrightarrow> 0 < vv j (t \<cdot>\<^sub>r (1\<^sub>r \<plusminus> t \<cdot>\<^sub>r (1\<^sub>r \<plusminus> -\<^sub>a t))\<^bsup>\<hyphen> K\<^esup>)
 3. \<And>n vv s t. \<lbrakk>vals_nonequiv K (Suc (Suc n)) vv; vals_nonequiv K (Suc n) (compose {h. h \<le> Suc n} vv (skip (Suc 0))); vals_nonequiv K (Suc n) (compose {j. j \<le> Suc n} vv (skip 2)); s \<in> carrier K; Ostrowski_elem K (Suc n) (compose {h. h \<le> Suc n} vv (skip (Suc 0))) s; t \<in> carrier K; Ostrowski_elem K (Suc n) (compose {h. h \<le> Suc n} vv (skip 2)) t; Ring K; aGroup K; s \<cdot>\<^sub>r t \<in> carrier K; 0 \<le> vv (Suc 0) s \<longrightarrow> \<not> 0 \<le> vv (Suc (Suc 0)) t; \<not> 0 \<le> vv (Suc 0) s\<rbrakk> \<Longrightarrow> \<exists>x\<in>carrier K. Ostrowski_elem K (Suc (Suc n)) vv x
[PROOF STEP]
apply (
       rule_tac v = "vv (Suc (Suc 0))" and x = t in OstrowskiTr10,
       assumption+)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>n vv s t j. \<lbrakk>vals_nonequiv K (Suc (Suc n)) vv; vals_nonequiv K (Suc n) (\<lambda>x\<in>{h. h \<le> Suc n}. vv (if x = 0 then x else Suc x)); vals_nonequiv K (Suc n) (\<lambda>x\<in>{j. j \<le> Suc n}. vv (if x \<le> Suc 0 then x else Suc x)); s \<in> carrier K; t \<in> carrier K; Ring K; aGroup K; s \<cdot>\<^sub>r t \<in> carrier K; \<not> 0 \<le> vv (Suc (Suc 0)) t; valuation K (vv (Suc (Suc 0))); t \<cdot>\<^sub>r (1\<^sub>r \<plusminus> t \<cdot>\<^sub>r (1\<^sub>r \<plusminus> -\<^sub>a t))\<^bsup>\<hyphen> K\<^esup> \<in> carrier K; j \<in> nset (Suc 0) (Suc (Suc n)); valuation K (vv j); 0 < vv 0 (1\<^sub>r \<plusminus> -\<^sub>a t); 1\<^sub>r \<plusminus> t \<cdot>\<^sub>r (1\<^sub>r \<plusminus> -\<^sub>a t) \<in> carrier K; 1\<^sub>r \<plusminus> t \<cdot>\<^sub>r (1\<^sub>r \<plusminus> -\<^sub>a t) \<noteq> \<zero>; (1\<^sub>r \<plusminus> t \<cdot>\<^sub>r (1\<^sub>r \<plusminus> -\<^sub>a t))\<^bsup>\<hyphen> K\<^esup> \<in> carrier K; (1\<^sub>r \<plusminus> t \<cdot>\<^sub>r (1\<^sub>r \<plusminus> -\<^sub>a t))\<^bsup>\<hyphen> K\<^esup> \<noteq> \<zero>; j \<noteq> Suc 0; j - Suc 0 \<in> nset (Suc 0) (Suc n); 0 < (if j - Suc 0 \<le> Suc n then vv (if j - Suc 0 \<le> Suc 0 then j - Suc 0 else Suc (j - Suc 0)) else undefined) t; j \<noteq> Suc (Suc 0)\<rbrakk> \<Longrightarrow> 0 < vv j (t \<cdot>\<^sub>r (1\<^sub>r \<plusminus> t \<cdot>\<^sub>r (1\<^sub>r \<plusminus> -\<^sub>a t))\<^bsup>\<hyphen> K\<^esup>)
 2. \<And>n vv s t. \<lbrakk>vals_nonequiv K (Suc (Suc n)) vv; vals_nonequiv K (Suc n) (compose {h. h \<le> Suc n} vv (skip (Suc 0))); vals_nonequiv K (Suc n) (compose {j. j \<le> Suc n} vv (skip 2)); s \<in> carrier K; Ostrowski_elem K (Suc n) (compose {h. h \<le> Suc n} vv (skip (Suc 0))) s; t \<in> carrier K; Ostrowski_elem K (Suc n) (compose {h. h \<le> Suc n} vv (skip 2)) t; Ring K; aGroup K; s \<cdot>\<^sub>r t \<in> carrier K; 0 \<le> vv (Suc 0) s \<longrightarrow> \<not> 0 \<le> vv (Suc (Suc 0)) t; \<not> 0 \<le> vv (Suc 0) s\<rbrakk> \<Longrightarrow> \<exists>x\<in>carrier K. Ostrowski_elem K (Suc (Suc n)) vv x
[PROOF STEP]
apply (
       subgoal_tac "\<not> j - Suc 0 \<le> Suc 0", simp add:nset_def)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>n vv s t j. \<lbrakk>vals_nonequiv K (Suc (Suc n)) vv; vals_nonequiv K (Suc n) (\<lambda>x\<in>{h. h \<le> Suc n}. vv (if x = 0 then x else Suc x)); vals_nonequiv K (Suc n) (\<lambda>x\<in>{j. j \<le> Suc n}. vv (if x \<le> Suc 0 then x else Suc x)); s \<in> carrier K; t \<in> carrier K; Ring K; aGroup K; s \<cdot>\<^sub>r t \<in> carrier K; \<not> 0 \<le> vv (Suc (Suc 0)) t; valuation K (vv (Suc (Suc 0))); t \<cdot>\<^sub>r (1\<^sub>r \<plusminus> t \<cdot>\<^sub>r (1\<^sub>r \<plusminus> -\<^sub>a t))\<^bsup>\<hyphen> K\<^esup> \<in> carrier K; Suc 0 \<le> j \<and> j \<le> Suc (Suc n); valuation K (vv j); 0 < vv 0 (1\<^sub>r \<plusminus> -\<^sub>a t); 1\<^sub>r \<plusminus> t \<cdot>\<^sub>r (1\<^sub>r \<plusminus> -\<^sub>a t) \<in> carrier K; 1\<^sub>r \<plusminus> t \<cdot>\<^sub>r (1\<^sub>r \<plusminus> -\<^sub>a t) \<noteq> \<zero>; (1\<^sub>r \<plusminus> t \<cdot>\<^sub>r (1\<^sub>r \<plusminus> -\<^sub>a t))\<^bsup>\<hyphen> K\<^esup> \<in> carrier K; (1\<^sub>r \<plusminus> t \<cdot>\<^sub>r (1\<^sub>r \<plusminus> -\<^sub>a t))\<^bsup>\<hyphen> K\<^esup> \<noteq> \<zero>; j \<noteq> Suc 0; j - Suc 0 \<le> Suc n; 0 < vv j t; j \<noteq> Suc (Suc 0); \<not> j - Suc 0 \<le> Suc 0\<rbrakk> \<Longrightarrow> 0 < vv j (t \<cdot>\<^sub>r (1\<^sub>r \<plusminus> t \<cdot>\<^sub>r (1\<^sub>r \<plusminus> -\<^sub>a t))\<^bsup>\<hyphen> K\<^esup>)
 2. \<And>n vv s t j. \<lbrakk>vals_nonequiv K (Suc (Suc n)) vv; vals_nonequiv K (Suc n) (\<lambda>x\<in>{h. h \<le> Suc n}. vv (if x = 0 then x else Suc x)); vals_nonequiv K (Suc n) (\<lambda>x\<in>{j. j \<le> Suc n}. vv (if x \<le> Suc 0 then x else Suc x)); s \<in> carrier K; t \<in> carrier K; Ring K; aGroup K; s \<cdot>\<^sub>r t \<in> carrier K; \<not> 0 \<le> vv (Suc (Suc 0)) t; valuation K (vv (Suc (Suc 0))); t \<cdot>\<^sub>r (1\<^sub>r \<plusminus> t \<cdot>\<^sub>r (1\<^sub>r \<plusminus> -\<^sub>a t))\<^bsup>\<hyphen> K\<^esup> \<in> carrier K; j \<in> nset (Suc 0) (Suc (Suc n)); valuation K (vv j); 0 < vv 0 (1\<^sub>r \<plusminus> -\<^sub>a t); 1\<^sub>r \<plusminus> t \<cdot>\<^sub>r (1\<^sub>r \<plusminus> -\<^sub>a t) \<in> carrier K; 1\<^sub>r \<plusminus> t \<cdot>\<^sub>r (1\<^sub>r \<plusminus> -\<^sub>a t) \<noteq> \<zero>; (1\<^sub>r \<plusminus> t \<cdot>\<^sub>r (1\<^sub>r \<plusminus> -\<^sub>a t))\<^bsup>\<hyphen> K\<^esup> \<in> carrier K; (1\<^sub>r \<plusminus> t \<cdot>\<^sub>r (1\<^sub>r \<plusminus> -\<^sub>a t))\<^bsup>\<hyphen> K\<^esup> \<noteq> \<zero>; j \<noteq> Suc 0; j - Suc 0 \<in> nset (Suc 0) (Suc n); 0 < (if j - Suc 0 \<le> Suc n then vv (if j - Suc 0 \<le> Suc 0 then j - Suc 0 else Suc (j - Suc 0)) else undefined) t; j \<noteq> Suc (Suc 0)\<rbrakk> \<Longrightarrow> \<not> j - Suc 0 \<le> Suc 0
 3. \<And>n vv s t. \<lbrakk>vals_nonequiv K (Suc (Suc n)) vv; vals_nonequiv K (Suc n) (compose {h. h \<le> Suc n} vv (skip (Suc 0))); vals_nonequiv K (Suc n) (compose {j. j \<le> Suc n} vv (skip 2)); s \<in> carrier K; Ostrowski_elem K (Suc n) (compose {h. h \<le> Suc n} vv (skip (Suc 0))) s; t \<in> carrier K; Ostrowski_elem K (Suc n) (compose {h. h \<le> Suc n} vv (skip 2)) t; Ring K; aGroup K; s \<cdot>\<^sub>r t \<in> carrier K; 0 \<le> vv (Suc 0) s \<longrightarrow> \<not> 0 \<le> vv (Suc (Suc 0)) t; \<not> 0 \<le> vv (Suc 0) s\<rbrakk> \<Longrightarrow> \<exists>x\<in>carrier K. Ostrowski_elem K (Suc (Suc n)) vv x
[PROOF STEP]
apply(
       rule_tac v = "vv j" and x = t in
                    OstrowskiTr9)
[PROOF STATE]
proof (prove)
goal (5 subgoals):
 1. \<And>n vv s t j. \<lbrakk>vals_nonequiv K (Suc (Suc n)) vv; vals_nonequiv K (Suc n) (\<lambda>x\<in>{h. h \<le> Suc n}. vv (if x = 0 then x else Suc x)); vals_nonequiv K (Suc n) (\<lambda>x\<in>{j. j \<le> Suc n}. vv (if x \<le> Suc 0 then x else Suc x)); s \<in> carrier K; t \<in> carrier K; Ring K; aGroup K; s \<cdot>\<^sub>r t \<in> carrier K; \<not> 0 \<le> vv (Suc (Suc 0)) t; valuation K (vv (Suc (Suc 0))); t \<cdot>\<^sub>r (1\<^sub>r \<plusminus> t \<cdot>\<^sub>r (1\<^sub>r \<plusminus> -\<^sub>a t))\<^bsup>\<hyphen> K\<^esup> \<in> carrier K; Suc 0 \<le> j \<and> j \<le> Suc (Suc n); valuation K (vv j); 0 < vv 0 (1\<^sub>r \<plusminus> -\<^sub>a t); 1\<^sub>r \<plusminus> t \<cdot>\<^sub>r (1\<^sub>r \<plusminus> -\<^sub>a t) \<in> carrier K; 1\<^sub>r \<plusminus> t \<cdot>\<^sub>r (1\<^sub>r \<plusminus> -\<^sub>a t) \<noteq> \<zero>; (1\<^sub>r \<plusminus> t \<cdot>\<^sub>r (1\<^sub>r \<plusminus> -\<^sub>a t))\<^bsup>\<hyphen> K\<^esup> \<in> carrier K; (1\<^sub>r \<plusminus> t \<cdot>\<^sub>r (1\<^sub>r \<plusminus> -\<^sub>a t))\<^bsup>\<hyphen> K\<^esup> \<noteq> \<zero>; j \<noteq> Suc 0; j - Suc 0 \<le> Suc n; 0 < vv j t; j \<noteq> Suc (Suc 0); \<not> j - Suc 0 \<le> Suc 0\<rbrakk> \<Longrightarrow> valuation K (vv j)
 2. \<And>n vv s t j. \<lbrakk>vals_nonequiv K (Suc (Suc n)) vv; vals_nonequiv K (Suc n) (\<lambda>x\<in>{h. h \<le> Suc n}. vv (if x = 0 then x else Suc x)); vals_nonequiv K (Suc n) (\<lambda>x\<in>{j. j \<le> Suc n}. vv (if x \<le> Suc 0 then x else Suc x)); s \<in> carrier K; t \<in> carrier K; Ring K; aGroup K; s \<cdot>\<^sub>r t \<in> carrier K; \<not> 0 \<le> vv (Suc (Suc 0)) t; valuation K (vv (Suc (Suc 0))); t \<cdot>\<^sub>r (1\<^sub>r \<plusminus> t \<cdot>\<^sub>r (1\<^sub>r \<plusminus> -\<^sub>a t))\<^bsup>\<hyphen> K\<^esup> \<in> carrier K; Suc 0 \<le> j \<and> j \<le> Suc (Suc n); valuation K (vv j); 0 < vv 0 (1\<^sub>r \<plusminus> -\<^sub>a t); 1\<^sub>r \<plusminus> t \<cdot>\<^sub>r (1\<^sub>r \<plusminus> -\<^sub>a t) \<in> carrier K; 1\<^sub>r \<plusminus> t \<cdot>\<^sub>r (1\<^sub>r \<plusminus> -\<^sub>a t) \<noteq> \<zero>; (1\<^sub>r \<plusminus> t \<cdot>\<^sub>r (1\<^sub>r \<plusminus> -\<^sub>a t))\<^bsup>\<hyphen> K\<^esup> \<in> carrier K; (1\<^sub>r \<plusminus> t \<cdot>\<^sub>r (1\<^sub>r \<plusminus> -\<^sub>a t))\<^bsup>\<hyphen> K\<^esup> \<noteq> \<zero>; j \<noteq> Suc 0; j - Suc 0 \<le> Suc n; 0 < vv j t; j \<noteq> Suc (Suc 0); \<not> j - Suc 0 \<le> Suc 0\<rbrakk> \<Longrightarrow> t \<in> carrier K
 3. \<And>n vv s t j. \<lbrakk>vals_nonequiv K (Suc (Suc n)) vv; vals_nonequiv K (Suc n) (\<lambda>x\<in>{h. h \<le> Suc n}. vv (if x = 0 then x else Suc x)); vals_nonequiv K (Suc n) (\<lambda>x\<in>{j. j \<le> Suc n}. vv (if x \<le> Suc 0 then x else Suc x)); s \<in> carrier K; t \<in> carrier K; Ring K; aGroup K; s \<cdot>\<^sub>r t \<in> carrier K; \<not> 0 \<le> vv (Suc (Suc 0)) t; valuation K (vv (Suc (Suc 0))); t \<cdot>\<^sub>r (1\<^sub>r \<plusminus> t \<cdot>\<^sub>r (1\<^sub>r \<plusminus> -\<^sub>a t))\<^bsup>\<hyphen> K\<^esup> \<in> carrier K; Suc 0 \<le> j \<and> j \<le> Suc (Suc n); valuation K (vv j); 0 < vv 0 (1\<^sub>r \<plusminus> -\<^sub>a t); 1\<^sub>r \<plusminus> t \<cdot>\<^sub>r (1\<^sub>r \<plusminus> -\<^sub>a t) \<in> carrier K; 1\<^sub>r \<plusminus> t \<cdot>\<^sub>r (1\<^sub>r \<plusminus> -\<^sub>a t) \<noteq> \<zero>; (1\<^sub>r \<plusminus> t \<cdot>\<^sub>r (1\<^sub>r \<plusminus> -\<^sub>a t))\<^bsup>\<hyphen> K\<^esup> \<in> carrier K; (1\<^sub>r \<plusminus> t \<cdot>\<^sub>r (1\<^sub>r \<plusminus> -\<^sub>a t))\<^bsup>\<hyphen> K\<^esup> \<noteq> \<zero>; j \<noteq> Suc 0; j - Suc 0 \<le> Suc n; 0 < vv j t; j \<noteq> Suc (Suc 0); \<not> j - Suc 0 \<le> Suc 0\<rbrakk> \<Longrightarrow> 0 < vv j t
 4. \<And>n vv s t j. \<lbrakk>vals_nonequiv K (Suc (Suc n)) vv; vals_nonequiv K (Suc n) (\<lambda>x\<in>{h. h \<le> Suc n}. vv (if x = 0 then x else Suc x)); vals_nonequiv K (Suc n) (\<lambda>x\<in>{j. j \<le> Suc n}. vv (if x \<le> Suc 0 then x else Suc x)); s \<in> carrier K; t \<in> carrier K; Ring K; aGroup K; s \<cdot>\<^sub>r t \<in> carrier K; \<not> 0 \<le> vv (Suc (Suc 0)) t; valuation K (vv (Suc (Suc 0))); t \<cdot>\<^sub>r (1\<^sub>r \<plusminus> t \<cdot>\<^sub>r (1\<^sub>r \<plusminus> -\<^sub>a t))\<^bsup>\<hyphen> K\<^esup> \<in> carrier K; j \<in> nset (Suc 0) (Suc (Suc n)); valuation K (vv j); 0 < vv 0 (1\<^sub>r \<plusminus> -\<^sub>a t); 1\<^sub>r \<plusminus> t \<cdot>\<^sub>r (1\<^sub>r \<plusminus> -\<^sub>a t) \<in> carrier K; 1\<^sub>r \<plusminus> t \<cdot>\<^sub>r (1\<^sub>r \<plusminus> -\<^sub>a t) \<noteq> \<zero>; (1\<^sub>r \<plusminus> t \<cdot>\<^sub>r (1\<^sub>r \<plusminus> -\<^sub>a t))\<^bsup>\<hyphen> K\<^esup> \<in> carrier K; (1\<^sub>r \<plusminus> t \<cdot>\<^sub>r (1\<^sub>r \<plusminus> -\<^sub>a t))\<^bsup>\<hyphen> K\<^esup> \<noteq> \<zero>; j \<noteq> Suc 0; j - Suc 0 \<in> nset (Suc 0) (Suc n); 0 < (if j - Suc 0 \<le> Suc n then vv (if j - Suc 0 \<le> Suc 0 then j - Suc 0 else Suc (j - Suc 0)) else undefined) t; j \<noteq> Suc (Suc 0)\<rbrakk> \<Longrightarrow> \<not> j - Suc 0 \<le> Suc 0
 5. \<And>n vv s t. \<lbrakk>vals_nonequiv K (Suc (Suc n)) vv; vals_nonequiv K (Suc n) (compose {h. h \<le> Suc n} vv (skip (Suc 0))); vals_nonequiv K (Suc n) (compose {j. j \<le> Suc n} vv (skip 2)); s \<in> carrier K; Ostrowski_elem K (Suc n) (compose {h. h \<le> Suc n} vv (skip (Suc 0))) s; t \<in> carrier K; Ostrowski_elem K (Suc n) (compose {h. h \<le> Suc n} vv (skip 2)) t; Ring K; aGroup K; s \<cdot>\<^sub>r t \<in> carrier K; 0 \<le> vv (Suc 0) s \<longrightarrow> \<not> 0 \<le> vv (Suc (Suc 0)) t; \<not> 0 \<le> vv (Suc 0) s\<rbrakk> \<Longrightarrow> \<exists>x\<in>carrier K. Ostrowski_elem K (Suc (Suc n)) vv x
[PROOF STEP]
apply (simp add:nset_def, assumption+)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>n vv s t j. \<lbrakk>vals_nonequiv K (Suc (Suc n)) vv; vals_nonequiv K (Suc n) (\<lambda>x\<in>{h. h \<le> Suc n}. vv (if x = 0 then x else Suc x)); vals_nonequiv K (Suc n) (\<lambda>x\<in>{j. j \<le> Suc n}. vv (if x \<le> Suc 0 then x else Suc x)); s \<in> carrier K; t \<in> carrier K; Ring K; aGroup K; s \<cdot>\<^sub>r t \<in> carrier K; \<not> 0 \<le> vv (Suc (Suc 0)) t; valuation K (vv (Suc (Suc 0))); t \<cdot>\<^sub>r (1\<^sub>r \<plusminus> t \<cdot>\<^sub>r (1\<^sub>r \<plusminus> -\<^sub>a t))\<^bsup>\<hyphen> K\<^esup> \<in> carrier K; j \<in> nset (Suc 0) (Suc (Suc n)); valuation K (vv j); 0 < vv 0 (1\<^sub>r \<plusminus> -\<^sub>a t); 1\<^sub>r \<plusminus> t \<cdot>\<^sub>r (1\<^sub>r \<plusminus> -\<^sub>a t) \<in> carrier K; 1\<^sub>r \<plusminus> t \<cdot>\<^sub>r (1\<^sub>r \<plusminus> -\<^sub>a t) \<noteq> \<zero>; (1\<^sub>r \<plusminus> t \<cdot>\<^sub>r (1\<^sub>r \<plusminus> -\<^sub>a t))\<^bsup>\<hyphen> K\<^esup> \<in> carrier K; (1\<^sub>r \<plusminus> t \<cdot>\<^sub>r (1\<^sub>r \<plusminus> -\<^sub>a t))\<^bsup>\<hyphen> K\<^esup> \<noteq> \<zero>; j \<noteq> Suc 0; j - Suc 0 \<in> nset (Suc 0) (Suc n); 0 < (if j - Suc 0 \<le> Suc n then vv (if j - Suc 0 \<le> Suc 0 then j - Suc 0 else Suc (j - Suc 0)) else undefined) t; j \<noteq> Suc (Suc 0)\<rbrakk> \<Longrightarrow> \<not> j - Suc 0 \<le> Suc 0
 2. \<And>n vv s t. \<lbrakk>vals_nonequiv K (Suc (Suc n)) vv; vals_nonequiv K (Suc n) (compose {h. h \<le> Suc n} vv (skip (Suc 0))); vals_nonequiv K (Suc n) (compose {j. j \<le> Suc n} vv (skip 2)); s \<in> carrier K; Ostrowski_elem K (Suc n) (compose {h. h \<le> Suc n} vv (skip (Suc 0))) s; t \<in> carrier K; Ostrowski_elem K (Suc n) (compose {h. h \<le> Suc n} vv (skip 2)) t; Ring K; aGroup K; s \<cdot>\<^sub>r t \<in> carrier K; 0 \<le> vv (Suc 0) s \<longrightarrow> \<not> 0 \<le> vv (Suc (Suc 0)) t; \<not> 0 \<le> vv (Suc 0) s\<rbrakk> \<Longrightarrow> \<exists>x\<in>carrier K. Ostrowski_elem K (Suc (Suc n)) vv x
[PROOF STEP]
apply (simp add:nset_def, (erule conjE)+, rule nset_Tr52, assumption+,
       thin_tac "vals_nonequiv K (Suc n)
         (compose {h. h \<le> (Suc n)} vv (skip (Suc 0)))",
       thin_tac "vals_nonequiv K (Suc n)
                   (compose {h. h \<le> (Suc n)} vv (skip 2))",
       thin_tac "Ostrowski_elem K (Suc n)
                   (compose {h. h \<le>(Suc n)} vv (skip 2)) t")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>n vv s t. \<lbrakk>vals_nonequiv K (Suc (Suc n)) vv; s \<in> carrier K; Ostrowski_elem K (Suc n) (compose {h. h \<le> Suc n} vv (skip (Suc 0))) s; t \<in> carrier K; Ring K; aGroup K; s \<cdot>\<^sub>r t \<in> carrier K; 0 \<le> vv (Suc 0) s \<longrightarrow> \<not> 0 \<le> vv (Suc (Suc 0)) t; \<not> 0 \<le> vv (Suc 0) s\<rbrakk> \<Longrightarrow> \<exists>x\<in>carrier K. Ostrowski_elem K (Suc (Suc n)) vv x
[PROOF STEP]
apply (subgoal_tac "s \<cdot>\<^sub>r ((1\<^sub>r \<plusminus> s \<cdot>\<^sub>r (1\<^sub>r \<plusminus> -\<^sub>a s))\<^bsup>\<hyphen>K\<^esup>) \<in> carrier K",
        subgoal_tac "Ostrowski_elem K (Suc (Suc n)) vv
                            (s \<cdot>\<^sub>r ((1\<^sub>r \<plusminus> s \<cdot>\<^sub>r (1\<^sub>r \<plusminus> -\<^sub>a s))\<^bsup>\<hyphen>K\<^esup>))", blast)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>n vv s t. \<lbrakk>vals_nonequiv K (Suc (Suc n)) vv; s \<in> carrier K; Ostrowski_elem K (Suc n) (compose {h. h \<le> Suc n} vv (skip (Suc 0))) s; t \<in> carrier K; Ring K; aGroup K; s \<cdot>\<^sub>r t \<in> carrier K; 0 \<le> vv (Suc 0) s \<longrightarrow> \<not> 0 \<le> vv (Suc (Suc 0)) t; \<not> 0 \<le> vv (Suc 0) s; s \<cdot>\<^sub>r (1\<^sub>r \<plusminus> s \<cdot>\<^sub>r (1\<^sub>r \<plusminus> -\<^sub>a s))\<^bsup>\<hyphen> K\<^esup> \<in> carrier K\<rbrakk> \<Longrightarrow> Ostrowski_elem K (Suc (Suc n)) vv (s \<cdot>\<^sub>r (1\<^sub>r \<plusminus> s \<cdot>\<^sub>r (1\<^sub>r \<plusminus> -\<^sub>a s))\<^bsup>\<hyphen> K\<^esup>)
 2. \<And>n vv s t. \<lbrakk>vals_nonequiv K (Suc (Suc n)) vv; s \<in> carrier K; Ostrowski_elem K (Suc n) (compose {h. h \<le> Suc n} vv (skip (Suc 0))) s; t \<in> carrier K; Ring K; aGroup K; s \<cdot>\<^sub>r t \<in> carrier K; 0 \<le> vv (Suc 0) s \<longrightarrow> \<not> 0 \<le> vv (Suc (Suc 0)) t; \<not> 0 \<le> vv (Suc 0) s\<rbrakk> \<Longrightarrow> s \<cdot>\<^sub>r (1\<^sub>r \<plusminus> s \<cdot>\<^sub>r (1\<^sub>r \<plusminus> -\<^sub>a s))\<^bsup>\<hyphen> K\<^esup> \<in> carrier K
[PROOF STEP]
prefer 2
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>n vv s t. \<lbrakk>vals_nonequiv K (Suc (Suc n)) vv; s \<in> carrier K; Ostrowski_elem K (Suc n) (compose {h. h \<le> Suc n} vv (skip (Suc 0))) s; t \<in> carrier K; Ring K; aGroup K; s \<cdot>\<^sub>r t \<in> carrier K; 0 \<le> vv (Suc 0) s \<longrightarrow> \<not> 0 \<le> vv (Suc (Suc 0)) t; \<not> 0 \<le> vv (Suc 0) s\<rbrakk> \<Longrightarrow> s \<cdot>\<^sub>r (1\<^sub>r \<plusminus> s \<cdot>\<^sub>r (1\<^sub>r \<plusminus> -\<^sub>a s))\<^bsup>\<hyphen> K\<^esup> \<in> carrier K
 2. \<And>n vv s t. \<lbrakk>vals_nonequiv K (Suc (Suc n)) vv; s \<in> carrier K; Ostrowski_elem K (Suc n) (compose {h. h \<le> Suc n} vv (skip (Suc 0))) s; t \<in> carrier K; Ring K; aGroup K; s \<cdot>\<^sub>r t \<in> carrier K; 0 \<le> vv (Suc 0) s \<longrightarrow> \<not> 0 \<le> vv (Suc (Suc 0)) t; \<not> 0 \<le> vv (Suc 0) s; s \<cdot>\<^sub>r (1\<^sub>r \<plusminus> s \<cdot>\<^sub>r (1\<^sub>r \<plusminus> -\<^sub>a s))\<^bsup>\<hyphen> K\<^esup> \<in> carrier K\<rbrakk> \<Longrightarrow> Ostrowski_elem K (Suc (Suc n)) vv (s \<cdot>\<^sub>r (1\<^sub>r \<plusminus> s \<cdot>\<^sub>r (1\<^sub>r \<plusminus> -\<^sub>a s))\<^bsup>\<hyphen> K\<^esup>)
[PROOF STEP]
apply (frule_tac n = "Suc (Suc n)" and m = "Suc 0" and vv = vv in
        vals_nonequiv_valuation, simp,
     frule_tac v = "vv (Suc 0)" and x = s in OstrowskiTr6, assumption+,
     rule Ring.ring_tOp_closed, assumption+,
     frule_tac x = "1\<^sub>r \<plusminus> s \<cdot>\<^sub>r (1\<^sub>r \<plusminus> -\<^sub>a s)" in invf_closed1, simp,
     simp add:Ostrowski_elem_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>n vv s t. \<lbrakk>vals_nonequiv K (Suc (Suc n)) vv; s \<in> carrier K; 0 < compose {h. h \<le> Suc n} vv (skip (Suc 0)) 0 (1\<^sub>r \<plusminus> -\<^sub>a s) \<and> (\<forall>j\<in>nset (Suc 0) (Suc n). 0 < compose {h. h \<le> Suc n} vv (skip (Suc 0)) j s); t \<in> carrier K; Ring K; aGroup K; s \<cdot>\<^sub>r t \<in> carrier K; \<not> 0 \<le> vv (Suc 0) s; s \<cdot>\<^sub>r (1\<^sub>r \<plusminus> s \<cdot>\<^sub>r (1\<^sub>r \<plusminus> -\<^sub>a s))\<^bsup>\<hyphen> K\<^esup> \<in> carrier K\<rbrakk> \<Longrightarrow> 0 < vv 0 (1\<^sub>r \<plusminus> -\<^sub>a s \<cdot>\<^sub>r (1\<^sub>r \<plusminus> s \<cdot>\<^sub>r (1\<^sub>r \<plusminus> -\<^sub>a s))\<^bsup>\<hyphen> K\<^esup>) \<and> (\<forall>j\<in>nset (Suc 0) (Suc (Suc n)). 0 < vv j (s \<cdot>\<^sub>r (1\<^sub>r \<plusminus> s \<cdot>\<^sub>r (1\<^sub>r \<plusminus> -\<^sub>a s))\<^bsup>\<hyphen> K\<^esup>))
[PROOF STEP]
apply (rule conjI)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>n vv s t. \<lbrakk>vals_nonequiv K (Suc (Suc n)) vv; s \<in> carrier K; 0 < compose {h. h \<le> Suc n} vv (skip (Suc 0)) 0 (1\<^sub>r \<plusminus> -\<^sub>a s) \<and> (\<forall>j\<in>nset (Suc 0) (Suc n). 0 < compose {h. h \<le> Suc n} vv (skip (Suc 0)) j s); t \<in> carrier K; Ring K; aGroup K; s \<cdot>\<^sub>r t \<in> carrier K; \<not> 0 \<le> vv (Suc 0) s; s \<cdot>\<^sub>r (1\<^sub>r \<plusminus> s \<cdot>\<^sub>r (1\<^sub>r \<plusminus> -\<^sub>a s))\<^bsup>\<hyphen> K\<^esup> \<in> carrier K\<rbrakk> \<Longrightarrow> 0 < vv 0 (1\<^sub>r \<plusminus> -\<^sub>a s \<cdot>\<^sub>r (1\<^sub>r \<plusminus> s \<cdot>\<^sub>r (1\<^sub>r \<plusminus> -\<^sub>a s))\<^bsup>\<hyphen> K\<^esup>)
 2. \<And>n vv s t. \<lbrakk>vals_nonequiv K (Suc (Suc n)) vv; s \<in> carrier K; 0 < compose {h. h \<le> Suc n} vv (skip (Suc 0)) 0 (1\<^sub>r \<plusminus> -\<^sub>a s) \<and> (\<forall>j\<in>nset (Suc 0) (Suc n). 0 < compose {h. h \<le> Suc n} vv (skip (Suc 0)) j s); t \<in> carrier K; Ring K; aGroup K; s \<cdot>\<^sub>r t \<in> carrier K; \<not> 0 \<le> vv (Suc 0) s; s \<cdot>\<^sub>r (1\<^sub>r \<plusminus> s \<cdot>\<^sub>r (1\<^sub>r \<plusminus> -\<^sub>a s))\<^bsup>\<hyphen> K\<^esup> \<in> carrier K\<rbrakk> \<Longrightarrow> \<forall>j\<in>nset (Suc 0) (Suc (Suc n)). 0 < vv j (s \<cdot>\<^sub>r (1\<^sub>r \<plusminus> s \<cdot>\<^sub>r (1\<^sub>r \<plusminus> -\<^sub>a s))\<^bsup>\<hyphen> K\<^esup>)
[PROOF STEP]
apply (rule_tac v = "vv 0" and x = s in OstrowskiTr8,
       simp add:vals_nonequiv_valuation, assumption+)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>n vv s t. \<lbrakk>vals_nonequiv K (Suc (Suc n)) vv; s \<in> carrier K; 0 < compose {h. h \<le> Suc n} vv (skip (Suc 0)) 0 (1\<^sub>r \<plusminus> -\<^sub>a s) \<and> (\<forall>j\<in>nset (Suc 0) (Suc n). 0 < compose {h. h \<le> Suc n} vv (skip (Suc 0)) j s); t \<in> carrier K; Ring K; aGroup K; s \<cdot>\<^sub>r t \<in> carrier K; \<not> 0 \<le> vv (Suc 0) s; s \<cdot>\<^sub>r (1\<^sub>r \<plusminus> s \<cdot>\<^sub>r (1\<^sub>r \<plusminus> -\<^sub>a s))\<^bsup>\<hyphen> K\<^esup> \<in> carrier K\<rbrakk> \<Longrightarrow> 0 < vv 0 (1\<^sub>r \<plusminus> -\<^sub>a s)
 2. \<And>n vv s t. \<lbrakk>vals_nonequiv K (Suc (Suc n)) vv; s \<in> carrier K; 0 < compose {h. h \<le> Suc n} vv (skip (Suc 0)) 0 (1\<^sub>r \<plusminus> -\<^sub>a s) \<and> (\<forall>j\<in>nset (Suc 0) (Suc n). 0 < compose {h. h \<le> Suc n} vv (skip (Suc 0)) j s); t \<in> carrier K; Ring K; aGroup K; s \<cdot>\<^sub>r t \<in> carrier K; \<not> 0 \<le> vv (Suc 0) s; s \<cdot>\<^sub>r (1\<^sub>r \<plusminus> s \<cdot>\<^sub>r (1\<^sub>r \<plusminus> -\<^sub>a s))\<^bsup>\<hyphen> K\<^esup> \<in> carrier K\<rbrakk> \<Longrightarrow> \<forall>j\<in>nset (Suc 0) (Suc (Suc n)). 0 < vv j (s \<cdot>\<^sub>r (1\<^sub>r \<plusminus> s \<cdot>\<^sub>r (1\<^sub>r \<plusminus> -\<^sub>a s))\<^bsup>\<hyphen> K\<^esup>)
[PROOF STEP]
apply (
       thin_tac "vals_nonequiv K (Suc (Suc n)) vv",
       (erule conjE)+,
       thin_tac "\<forall>j\<in>nset (Suc 0) (Suc n).
            0 < (compose {h. h \<le> (Suc n)} vv (skip (Suc 0)) j s)",
       simp add:compose_def skip_def,  rule ballI)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>n vv s t j. \<lbrakk>vals_nonequiv K (Suc (Suc n)) vv; s \<in> carrier K; 0 < compose {h. h \<le> Suc n} vv (skip (Suc 0)) 0 (1\<^sub>r \<plusminus> -\<^sub>a s) \<and> (\<forall>j\<in>nset (Suc 0) (Suc n). 0 < compose {h. h \<le> Suc n} vv (skip (Suc 0)) j s); t \<in> carrier K; Ring K; aGroup K; s \<cdot>\<^sub>r t \<in> carrier K; \<not> 0 \<le> vv (Suc 0) s; s \<cdot>\<^sub>r (1\<^sub>r \<plusminus> s \<cdot>\<^sub>r (1\<^sub>r \<plusminus> -\<^sub>a s))\<^bsup>\<hyphen> K\<^esup> \<in> carrier K; j \<in> nset (Suc 0) (Suc (Suc n))\<rbrakk> \<Longrightarrow> 0 < vv j (s \<cdot>\<^sub>r (1\<^sub>r \<plusminus> s \<cdot>\<^sub>r (1\<^sub>r \<plusminus> -\<^sub>a s))\<^bsup>\<hyphen> K\<^esup>)
[PROOF STEP]
(** case *** *** **)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>n vv s t j. \<lbrakk>vals_nonequiv K (Suc (Suc n)) vv; s \<in> carrier K; 0 < compose {h. h \<le> Suc n} vv (skip (Suc 0)) 0 (1\<^sub>r \<plusminus> -\<^sub>a s) \<and> (\<forall>j\<in>nset (Suc 0) (Suc n). 0 < compose {h. h \<le> Suc n} vv (skip (Suc 0)) j s); t \<in> carrier K; Ring K; aGroup K; s \<cdot>\<^sub>r t \<in> carrier K; \<not> 0 \<le> vv (Suc 0) s; s \<cdot>\<^sub>r (1\<^sub>r \<plusminus> s \<cdot>\<^sub>r (1\<^sub>r \<plusminus> -\<^sub>a s))\<^bsup>\<hyphen> K\<^esup> \<in> carrier K; j \<in> nset (Suc 0) (Suc (Suc n))\<rbrakk> \<Longrightarrow> 0 < vv j (s \<cdot>\<^sub>r (1\<^sub>r \<plusminus> s \<cdot>\<^sub>r (1\<^sub>r \<plusminus> -\<^sub>a s))\<^bsup>\<hyphen> K\<^esup>)
[PROOF STEP]
apply (case_tac "j = Suc 0", simp,
     rule_tac v = "vv (Suc 0)" and x = s in OstrowskiTr10,
     simp add:vals_nonequiv_valuation, assumption+,
     rule_tac v = "vv j" and x = s in OstrowskiTr9,
     simp add:vals_nonequiv_valuation nset_def, assumption,
     (erule conjE)+, simp add:compose_def skip_def,
     frule_tac j = j in nset_Tr51, assumption+,
     drule_tac x = "j - Suc 0" in bspec, assumption+)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>n vv s t j. \<lbrakk>vals_nonequiv K (Suc (Suc n)) vv; s \<in> carrier K; t \<in> carrier K; Ring K; aGroup K; s \<cdot>\<^sub>r t \<in> carrier K; \<not> 0 \<le> vv (Suc 0) s; s \<cdot>\<^sub>r (1\<^sub>r \<plusminus> s \<cdot>\<^sub>r (1\<^sub>r \<plusminus> -\<^sub>a s))\<^bsup>\<hyphen> K\<^esup> \<in> carrier K; j \<in> nset (Suc 0) (Suc (Suc n)); j \<noteq> Suc 0; 0 < vv 0 (1\<^sub>r \<plusminus> -\<^sub>a s); j - Suc 0 \<in> nset (Suc 0) (Suc n); 0 < (if j - Suc 0 \<le> Suc n then vv (if j - Suc 0 = 0 then j - Suc 0 else Suc (j - Suc 0)) else undefined) s\<rbrakk> \<Longrightarrow> 0 < vv j s
[PROOF STEP]
apply (simp add:nset_def)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma (in Corps) val_1_nonzero:"\<lbrakk>valuation K v; x \<in> carrier K; v x = 1\<rbrakk> \<Longrightarrow>
                               x \<noteq> \<zero>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>valuation K v; x \<in> carrier K; v x = 1\<rbrakk> \<Longrightarrow> x \<noteq> \<zero>
[PROOF STEP]
apply (rule contrapos_pp, simp+,
       simp add:value_of_zero,
       rotate_tac 3, drule sym, simp only:ant_1[THEN sym],
       simp del:ant_1)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma (in Corps) Approximation1_5Tr1:"\<lbrakk>vals_nonequiv K (Suc n) vv;
 n_val K (vv 0) = vv 0; a \<in> carrier K; vv 0 a = 1; x \<in> carrier K;
 Ostrowski_elem K (Suc n) vv x\<rbrakk>  \<Longrightarrow>
        \<forall>m. 2 \<le> m \<longrightarrow> vv 0 ((1\<^sub>r \<plusminus> -\<^sub>a x)^\<^bsup>K m\<^esup> \<plusminus> a \<cdot>\<^sub>r (x^\<^bsup>K m\<^esup>)) = 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>vals_nonequiv K (Suc n) vv; n_val K (vv 0) = vv 0; a \<in> carrier K; vv 0 a = 1; x \<in> carrier K; Ostrowski_elem K (Suc n) vv x\<rbrakk> \<Longrightarrow> \<forall>m\<ge>2. vv 0 ((1\<^sub>r \<plusminus> -\<^sub>a x)^\<^bsup>K m\<^esup> \<plusminus> a \<cdot>\<^sub>r x^\<^bsup>K m\<^esup>) = 1
[PROOF STEP]
apply (cut_tac field_is_ring, frule Ring.ring_is_ag[of "K"],
       frule Ring.ring_one[of "K"],
       rule allI, rule impI,
       frule vals_nonequiv_valuation[of "Suc n" "vv" "0"],
       simp,
       simp add:Ostrowski_elem_def, frule conjunct1, fold Ostrowski_elem_def,
       frule val_1_nonzero[of "vv 0" "a"], assumption+)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>m. \<lbrakk>vals_nonequiv K (Suc n) vv; n_val K (vv 0) = vv 0; a \<in> carrier K; vv 0 a = 1; x \<in> carrier K; Ostrowski_elem K (Suc n) vv x; Ring K; aGroup K; 1\<^sub>r \<in> carrier K; 2 \<le> m; valuation K (vv 0); 0 < vv 0 (1\<^sub>r \<plusminus> -\<^sub>a x); a \<noteq> \<zero>\<rbrakk> \<Longrightarrow> vv 0 ((1\<^sub>r \<plusminus> -\<^sub>a x)^\<^bsup>K m\<^esup> \<plusminus> a \<cdot>\<^sub>r x^\<^bsup>K m\<^esup>) = 1
[PROOF STEP]
apply (frule vals_nonequiv_valuation[of "Suc n" "vv" "0"], simp,
       frule val_nonzero_noninf[of "vv 0" "a"], assumption+,
       frule val_unit_cond[of "vv 0" "x"], assumption+,
       frule_tac n = m in Ring.npClose[of "K" "x"], assumption+,
       frule aGroup.ag_mOp_closed[of "K" "x"], assumption+,
       frule aGroup.ag_pOp_closed[of "K" "1\<^sub>r" "-\<^sub>a x"], assumption+)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>m. \<lbrakk>vals_nonequiv K (Suc n) vv; n_val K (vv 0) = vv 0; a \<in> carrier K; vv 0 a = 1; x \<in> carrier K; Ostrowski_elem K (Suc n) vv x; Ring K; aGroup K; 1\<^sub>r \<in> carrier K; 2 \<le> m; valuation K (vv 0); 0 < vv 0 (1\<^sub>r \<plusminus> -\<^sub>a x); a \<noteq> \<zero>; valuation K (vv 0); vv 0 a \<noteq> \<infinity>; vv 0 x = 0; x^\<^bsup>K m\<^esup> \<in> carrier K; -\<^sub>a x \<in> carrier K; 1\<^sub>r \<plusminus> -\<^sub>a x \<in> carrier K\<rbrakk> \<Longrightarrow> vv 0 ((1\<^sub>r \<plusminus> -\<^sub>a x)^\<^bsup>K m\<^esup> \<plusminus> a \<cdot>\<^sub>r x^\<^bsup>K m\<^esup>) = 1
[PROOF STEP]
apply (subgoal_tac "0 < m",
       frule_tac x = "a \<cdot>\<^sub>r (x^\<^bsup>K m\<^esup>)" and y = "(1\<^sub>r \<plusminus> -\<^sub>a x)^\<^bsup>K m\<^esup>" in
       value_less_eq[of "vv 0"],
       rule Ring.ring_tOp_closed, assumption+,
       rule Ring.npClose, assumption+, simp add: val_t2p,
       frule value_zero_nonzero[of "vv 0" "x"], assumption+,
       simp add:val_exp_ring[THEN sym], simp add:asprod_n_0 aadd_0_r)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>m. \<lbrakk>vals_nonequiv K (Suc n) vv; n_val K (vv 0) = vv 0; a \<in> carrier K; vv 0 a = 1; x \<in> carrier K; Ostrowski_elem K (Suc n) vv x; Ring K; aGroup K; 1\<^sub>r \<in> carrier K; 2 \<le> m; 0 < vv 0 (1\<^sub>r \<plusminus> -\<^sub>a x); a \<noteq> \<zero>; valuation K (vv 0); \<infinity> \<noteq> 1; vv 0 x = 0; x^\<^bsup>K m\<^esup> \<in> carrier K; -\<^sub>a x \<in> carrier K; 1\<^sub>r \<plusminus> -\<^sub>a x \<in> carrier K; x \<noteq> \<zero>\<rbrakk> \<Longrightarrow> 1 < vv 0 ((1\<^sub>r \<plusminus> -\<^sub>a x)^\<^bsup>K m\<^esup>)
 2. \<And>m. \<lbrakk>vals_nonequiv K (Suc n) vv; n_val K (vv 0) = vv 0; a \<in> carrier K; vv 0 a = 1; x \<in> carrier K; Ostrowski_elem K (Suc n) vv x; Ring K; aGroup K; 1\<^sub>r \<in> carrier K; 2 \<le> m; valuation K (vv 0); 0 < vv 0 (1\<^sub>r \<plusminus> -\<^sub>a x); a \<noteq> \<zero>; valuation K (vv 0); vv 0 a \<noteq> \<infinity>; vv 0 x = 0; x^\<^bsup>K m\<^esup> \<in> carrier K; -\<^sub>a x \<in> carrier K; 1\<^sub>r \<plusminus> -\<^sub>a x \<in> carrier K; 0 < m; vv 0 (a \<cdot>\<^sub>r x^\<^bsup>K m\<^esup>) = vv 0 (a \<cdot>\<^sub>r x^\<^bsup>K m\<^esup> \<plusminus> (1\<^sub>r \<plusminus> -\<^sub>a x)^\<^bsup>K m\<^esup>)\<rbrakk> \<Longrightarrow> vv 0 ((1\<^sub>r \<plusminus> -\<^sub>a x)^\<^bsup>K m\<^esup> \<plusminus> a \<cdot>\<^sub>r x^\<^bsup>K m\<^esup>) = 1
 3. \<And>m. \<lbrakk>vals_nonequiv K (Suc n) vv; n_val K (vv 0) = vv 0; a \<in> carrier K; vv 0 a = 1; x \<in> carrier K; Ostrowski_elem K (Suc n) vv x; Ring K; aGroup K; 1\<^sub>r \<in> carrier K; 2 \<le> m; valuation K (vv 0); 0 < vv 0 (1\<^sub>r \<plusminus> -\<^sub>a x); a \<noteq> \<zero>; valuation K (vv 0); vv 0 a \<noteq> \<infinity>; vv 0 x = 0; x^\<^bsup>K m\<^esup> \<in> carrier K; -\<^sub>a x \<in> carrier K; 1\<^sub>r \<plusminus> -\<^sub>a x \<in> carrier K\<rbrakk> \<Longrightarrow> 0 < m
[PROOF STEP]
apply (case_tac "x = 1\<^sub>r\<^bsub>K\<^esub>", simp add:aGroup.ag_r_inv1,
       frule_tac n = m in Ring.npZero_sub[of "K"], simp,
       simp add:value_of_zero)
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<And>m. \<lbrakk>vals_nonequiv K (Suc n) vv; n_val K (vv 0) = vv 0; a \<in> carrier K; vv 0 a = 1; Ostrowski_elem K (Suc n) vv 1\<^sub>r; Ring K; aGroup K; 1\<^sub>r \<in> carrier K; 2 \<le> m; 0 < \<infinity>; a \<noteq> \<zero>; valuation K (vv 0); \<infinity> \<noteq> 1; vv 0 1\<^sub>r = 0; 1\<^sub>r^\<^bsup>K m\<^esup> \<in> carrier K; -\<^sub>a 1\<^sub>r \<in> carrier K; \<zero> \<in> carrier K; 1\<^sub>r \<noteq> \<zero>; x = 1\<^sub>r; \<zero>^\<^bsup>K m\<^esup> = \<zero>\<rbrakk> \<Longrightarrow> 1 < \<infinity>
 2. \<And>m. \<lbrakk>vals_nonequiv K (Suc n) vv; n_val K (vv 0) = vv 0; a \<in> carrier K; vv 0 a = 1; x \<in> carrier K; Ostrowski_elem K (Suc n) vv x; Ring K; aGroup K; 1\<^sub>r \<in> carrier K; 2 \<le> m; 0 < vv 0 (1\<^sub>r \<plusminus> -\<^sub>a x); a \<noteq> \<zero>; valuation K (vv 0); \<infinity> \<noteq> 1; vv 0 x = 0; x^\<^bsup>K m\<^esup> \<in> carrier K; -\<^sub>a x \<in> carrier K; 1\<^sub>r \<plusminus> -\<^sub>a x \<in> carrier K; x \<noteq> \<zero>; x \<noteq> 1\<^sub>r\<rbrakk> \<Longrightarrow> 1 < vv 0 ((1\<^sub>r \<plusminus> -\<^sub>a x)^\<^bsup>K m\<^esup>)
 3. \<And>m. \<lbrakk>vals_nonequiv K (Suc n) vv; n_val K (vv 0) = vv 0; a \<in> carrier K; vv 0 a = 1; x \<in> carrier K; Ostrowski_elem K (Suc n) vv x; Ring K; aGroup K; 1\<^sub>r \<in> carrier K; 2 \<le> m; valuation K (vv 0); 0 < vv 0 (1\<^sub>r \<plusminus> -\<^sub>a x); a \<noteq> \<zero>; valuation K (vv 0); vv 0 a \<noteq> \<infinity>; vv 0 x = 0; x^\<^bsup>K m\<^esup> \<in> carrier K; -\<^sub>a x \<in> carrier K; 1\<^sub>r \<plusminus> -\<^sub>a x \<in> carrier K; 0 < m; vv 0 (a \<cdot>\<^sub>r x^\<^bsup>K m\<^esup>) = vv 0 (a \<cdot>\<^sub>r x^\<^bsup>K m\<^esup> \<plusminus> (1\<^sub>r \<plusminus> -\<^sub>a x)^\<^bsup>K m\<^esup>)\<rbrakk> \<Longrightarrow> vv 0 ((1\<^sub>r \<plusminus> -\<^sub>a x)^\<^bsup>K m\<^esup> \<plusminus> a \<cdot>\<^sub>r x^\<^bsup>K m\<^esup>) = 1
 4. \<And>m. \<lbrakk>vals_nonequiv K (Suc n) vv; n_val K (vv 0) = vv 0; a \<in> carrier K; vv 0 a = 1; x \<in> carrier K; Ostrowski_elem K (Suc n) vv x; Ring K; aGroup K; 1\<^sub>r \<in> carrier K; 2 \<le> m; valuation K (vv 0); 0 < vv 0 (1\<^sub>r \<plusminus> -\<^sub>a x); a \<noteq> \<zero>; valuation K (vv 0); vv 0 a \<noteq> \<infinity>; vv 0 x = 0; x^\<^bsup>K m\<^esup> \<in> carrier K; -\<^sub>a x \<in> carrier K; 1\<^sub>r \<plusminus> -\<^sub>a x \<in> carrier K\<rbrakk> \<Longrightarrow> 0 < m
[PROOF STEP]
apply (cut_tac inf_ge_any[of "1"], simp add: less_le)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>m. \<lbrakk>vals_nonequiv K (Suc n) vv; n_val K (vv 0) = vv 0; a \<in> carrier K; vv 0 a = 1; x \<in> carrier K; Ostrowski_elem K (Suc n) vv x; Ring K; aGroup K; 1\<^sub>r \<in> carrier K; 2 \<le> m; 0 < vv 0 (1\<^sub>r \<plusminus> -\<^sub>a x); a \<noteq> \<zero>; valuation K (vv 0); \<infinity> \<noteq> 1; vv 0 x = 0; x^\<^bsup>K m\<^esup> \<in> carrier K; -\<^sub>a x \<in> carrier K; 1\<^sub>r \<plusminus> -\<^sub>a x \<in> carrier K; x \<noteq> \<zero>; x \<noteq> 1\<^sub>r\<rbrakk> \<Longrightarrow> 1 < vv 0 ((1\<^sub>r \<plusminus> -\<^sub>a x)^\<^bsup>K m\<^esup>)
 2. \<And>m. \<lbrakk>vals_nonequiv K (Suc n) vv; n_val K (vv 0) = vv 0; a \<in> carrier K; vv 0 a = 1; x \<in> carrier K; Ostrowski_elem K (Suc n) vv x; Ring K; aGroup K; 1\<^sub>r \<in> carrier K; 2 \<le> m; valuation K (vv 0); 0 < vv 0 (1\<^sub>r \<plusminus> -\<^sub>a x); a \<noteq> \<zero>; valuation K (vv 0); vv 0 a \<noteq> \<infinity>; vv 0 x = 0; x^\<^bsup>K m\<^esup> \<in> carrier K; -\<^sub>a x \<in> carrier K; 1\<^sub>r \<plusminus> -\<^sub>a x \<in> carrier K; 0 < m; vv 0 (a \<cdot>\<^sub>r x^\<^bsup>K m\<^esup>) = vv 0 (a \<cdot>\<^sub>r x^\<^bsup>K m\<^esup> \<plusminus> (1\<^sub>r \<plusminus> -\<^sub>a x)^\<^bsup>K m\<^esup>)\<rbrakk> \<Longrightarrow> vv 0 ((1\<^sub>r \<plusminus> -\<^sub>a x)^\<^bsup>K m\<^esup> \<plusminus> a \<cdot>\<^sub>r x^\<^bsup>K m\<^esup>) = 1
 3. \<And>m. \<lbrakk>vals_nonequiv K (Suc n) vv; n_val K (vv 0) = vv 0; a \<in> carrier K; vv 0 a = 1; x \<in> carrier K; Ostrowski_elem K (Suc n) vv x; Ring K; aGroup K; 1\<^sub>r \<in> carrier K; 2 \<le> m; valuation K (vv 0); 0 < vv 0 (1\<^sub>r \<plusminus> -\<^sub>a x); a \<noteq> \<zero>; valuation K (vv 0); vv 0 a \<noteq> \<infinity>; vv 0 x = 0; x^\<^bsup>K m\<^esup> \<in> carrier K; -\<^sub>a x \<in> carrier K; 1\<^sub>r \<plusminus> -\<^sub>a x \<in> carrier K\<rbrakk> \<Longrightarrow> 0 < m
[PROOF STEP]
apply (rotate_tac -1, drule not_sym,
      frule aGroup.ag_neq_diffnonzero[of "K" "1\<^sub>r" "x"],
      simp add:Ring.ring_one[of "K"], assumption+, simp,
      simp add:val_exp_ring[THEN sym],
      cut_tac n1 = m in of_nat_0_less_iff[THEN sym])
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>m. \<lbrakk>vals_nonequiv K (Suc n) vv; n_val K (vv 0) = vv 0; a \<in> carrier K; vv 0 a = 1; x \<in> carrier K; Ostrowski_elem K (Suc n) vv x; Ring K; aGroup K; 1\<^sub>r \<in> carrier K; 2 \<le> m; 0 < vv 0 (1\<^sub>r \<plusminus> -\<^sub>a x); a \<noteq> \<zero>; valuation K (vv 0); \<infinity> \<noteq> 1; vv 0 x = 0; x^\<^bsup>K m\<^esup> \<in> carrier K; -\<^sub>a x \<in> carrier K; 1\<^sub>r \<plusminus> -\<^sub>a x \<in> carrier K; x \<noteq> \<zero>; 1\<^sub>r \<plusminus> -\<^sub>a x \<noteq> \<zero>; 1\<^sub>r \<noteq> x; (0 < m) = ((0::?'a63) < of_nat m)\<rbrakk> \<Longrightarrow> 1 < int m *\<^sub>a vv 0 (1\<^sub>r \<plusminus> -\<^sub>a x)
 2. \<And>m. \<lbrakk>vals_nonequiv K (Suc n) vv; n_val K (vv 0) = vv 0; a \<in> carrier K; vv 0 a = 1; x \<in> carrier K; Ostrowski_elem K (Suc n) vv x; Ring K; aGroup K; 1\<^sub>r \<in> carrier K; 2 \<le> m; valuation K (vv 0); 0 < vv 0 (1\<^sub>r \<plusminus> -\<^sub>a x); a \<noteq> \<zero>; valuation K (vv 0); vv 0 a \<noteq> \<infinity>; vv 0 x = 0; x^\<^bsup>K m\<^esup> \<in> carrier K; -\<^sub>a x \<in> carrier K; 1\<^sub>r \<plusminus> -\<^sub>a x \<in> carrier K; 0 < m; vv 0 (a \<cdot>\<^sub>r x^\<^bsup>K m\<^esup>) = vv 0 (a \<cdot>\<^sub>r x^\<^bsup>K m\<^esup> \<plusminus> (1\<^sub>r \<plusminus> -\<^sub>a x)^\<^bsup>K m\<^esup>)\<rbrakk> \<Longrightarrow> vv 0 ((1\<^sub>r \<plusminus> -\<^sub>a x)^\<^bsup>K m\<^esup> \<plusminus> a \<cdot>\<^sub>r x^\<^bsup>K m\<^esup>) = 1
 3. \<And>m. \<lbrakk>vals_nonequiv K (Suc n) vv; n_val K (vv 0) = vv 0; a \<in> carrier K; vv 0 a = 1; x \<in> carrier K; Ostrowski_elem K (Suc n) vv x; Ring K; aGroup K; 1\<^sub>r \<in> carrier K; 2 \<le> m; valuation K (vv 0); 0 < vv 0 (1\<^sub>r \<plusminus> -\<^sub>a x); a \<noteq> \<zero>; valuation K (vv 0); vv 0 a \<noteq> \<infinity>; vv 0 x = 0; x^\<^bsup>K m\<^esup> \<in> carrier K; -\<^sub>a x \<in> carrier K; 1\<^sub>r \<plusminus> -\<^sub>a x \<in> carrier K\<rbrakk> \<Longrightarrow> 0 < m
[PROOF STEP]
apply (cut_tac a = "0 < m" and b = "0 < int m" in a_b_exchange, simp,
       assumption)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>m. \<lbrakk>vals_nonequiv K (Suc n) vv; n_val K (vv 0) = vv 0; a \<in> carrier K; vv 0 a = 1; x \<in> carrier K; Ostrowski_elem K (Suc n) vv x; Ring K; aGroup K; 1\<^sub>r \<in> carrier K; 2 \<le> m; 0 < vv 0 (1\<^sub>r \<plusminus> -\<^sub>a x); a \<noteq> \<zero>; valuation K (vv 0); \<infinity> \<noteq> 1; vv 0 x = 0; x^\<^bsup>K m\<^esup> \<in> carrier K; -\<^sub>a x \<in> carrier K; 1\<^sub>r \<plusminus> -\<^sub>a x \<in> carrier K; x \<noteq> \<zero>; 1\<^sub>r \<plusminus> -\<^sub>a x \<noteq> \<zero>; 1\<^sub>r \<noteq> x; (0 < m) = (0 < int m); 0 < int m\<rbrakk> \<Longrightarrow> 1 < int m *\<^sub>a vv 0 (1\<^sub>r \<plusminus> -\<^sub>a x)
 2. \<And>m. \<lbrakk>vals_nonequiv K (Suc n) vv; n_val K (vv 0) = vv 0; a \<in> carrier K; vv 0 a = 1; x \<in> carrier K; Ostrowski_elem K (Suc n) vv x; Ring K; aGroup K; 1\<^sub>r \<in> carrier K; 2 \<le> m; valuation K (vv 0); 0 < vv 0 (1\<^sub>r \<plusminus> -\<^sub>a x); a \<noteq> \<zero>; valuation K (vv 0); vv 0 a \<noteq> \<infinity>; vv 0 x = 0; x^\<^bsup>K m\<^esup> \<in> carrier K; -\<^sub>a x \<in> carrier K; 1\<^sub>r \<plusminus> -\<^sub>a x \<in> carrier K; 0 < m; vv 0 (a \<cdot>\<^sub>r x^\<^bsup>K m\<^esup>) = vv 0 (a \<cdot>\<^sub>r x^\<^bsup>K m\<^esup> \<plusminus> (1\<^sub>r \<plusminus> -\<^sub>a x)^\<^bsup>K m\<^esup>)\<rbrakk> \<Longrightarrow> vv 0 ((1\<^sub>r \<plusminus> -\<^sub>a x)^\<^bsup>K m\<^esup> \<plusminus> a \<cdot>\<^sub>r x^\<^bsup>K m\<^esup>) = 1
 3. \<And>m. \<lbrakk>vals_nonequiv K (Suc n) vv; n_val K (vv 0) = vv 0; a \<in> carrier K; vv 0 a = 1; x \<in> carrier K; Ostrowski_elem K (Suc n) vv x; Ring K; aGroup K; 1\<^sub>r \<in> carrier K; 2 \<le> m; valuation K (vv 0); 0 < vv 0 (1\<^sub>r \<plusminus> -\<^sub>a x); a \<noteq> \<zero>; valuation K (vv 0); vv 0 a \<noteq> \<infinity>; vv 0 x = 0; x^\<^bsup>K m\<^esup> \<in> carrier K; -\<^sub>a x \<in> carrier K; 1\<^sub>r \<plusminus> -\<^sub>a x \<in> carrier K\<rbrakk> \<Longrightarrow> 0 < m
[PROOF STEP]
apply (thin_tac "(0 < m) = (0 < int m)",
      frule val_nonzero_z[of "vv 0" "1\<^sub>r \<plusminus> -\<^sub>a x"], assumption+,
      erule exE, simp, simp add:asprod_amult a_z_z,
      simp only:ant_1[THEN sym], simp only:aless_zless, simp add:ge2_zmult_pos)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>m. \<lbrakk>vals_nonequiv K (Suc n) vv; n_val K (vv 0) = vv 0; a \<in> carrier K; vv 0 a = 1; x \<in> carrier K; Ostrowski_elem K (Suc n) vv x; Ring K; aGroup K; 1\<^sub>r \<in> carrier K; 2 \<le> m; valuation K (vv 0); 0 < vv 0 (1\<^sub>r \<plusminus> -\<^sub>a x); a \<noteq> \<zero>; valuation K (vv 0); vv 0 a \<noteq> \<infinity>; vv 0 x = 0; x^\<^bsup>K m\<^esup> \<in> carrier K; -\<^sub>a x \<in> carrier K; 1\<^sub>r \<plusminus> -\<^sub>a x \<in> carrier K; 0 < m; vv 0 (a \<cdot>\<^sub>r x^\<^bsup>K m\<^esup>) = vv 0 (a \<cdot>\<^sub>r x^\<^bsup>K m\<^esup> \<plusminus> (1\<^sub>r \<plusminus> -\<^sub>a x)^\<^bsup>K m\<^esup>)\<rbrakk> \<Longrightarrow> vv 0 ((1\<^sub>r \<plusminus> -\<^sub>a x)^\<^bsup>K m\<^esup> \<plusminus> a \<cdot>\<^sub>r x^\<^bsup>K m\<^esup>) = 1
 2. \<And>m. \<lbrakk>vals_nonequiv K (Suc n) vv; n_val K (vv 0) = vv 0; a \<in> carrier K; vv 0 a = 1; x \<in> carrier K; Ostrowski_elem K (Suc n) vv x; Ring K; aGroup K; 1\<^sub>r \<in> carrier K; 2 \<le> m; valuation K (vv 0); 0 < vv 0 (1\<^sub>r \<plusminus> -\<^sub>a x); a \<noteq> \<zero>; valuation K (vv 0); vv 0 a \<noteq> \<infinity>; vv 0 x = 0; x^\<^bsup>K m\<^esup> \<in> carrier K; -\<^sub>a x \<in> carrier K; 1\<^sub>r \<plusminus> -\<^sub>a x \<in> carrier K\<rbrakk> \<Longrightarrow> 0 < m
[PROOF STEP]
apply (subst aGroup.ag_pOp_commute[of "K"], assumption+,
       rule Ring.npClose, assumption+, rule Ring.ring_tOp_closed[of "K"],
       assumption+,
       rotate_tac -1, drule sym, simp,
       thin_tac "vv 0 (a \<cdot>\<^sub>r x^\<^bsup>K m\<^esup> \<plusminus> (1\<^sub>r \<plusminus> -\<^sub>a x)^\<^bsup>K m\<^esup>) = vv 0 (a \<cdot>\<^sub>r x^\<^bsup>K m\<^esup>)")
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>m. \<lbrakk>vals_nonequiv K (Suc n) vv; n_val K (vv 0) = vv 0; a \<in> carrier K; vv 0 a = 1; x \<in> carrier K; Ostrowski_elem K (Suc n) vv x; Ring K; aGroup K; 1\<^sub>r \<in> carrier K; 2 \<le> m; 0 < vv 0 (1\<^sub>r \<plusminus> -\<^sub>a x); a \<noteq> \<zero>; valuation K (vv 0); \<infinity> \<noteq> 1; vv 0 x = 0; x^\<^bsup>K m\<^esup> \<in> carrier K; -\<^sub>a x \<in> carrier K; 1\<^sub>r \<plusminus> -\<^sub>a x \<in> carrier K\<rbrakk> \<Longrightarrow> vv 0 (a \<cdot>\<^sub>r x^\<^bsup>K m\<^esup>) = 1
 2. \<And>m. \<lbrakk>vals_nonequiv K (Suc n) vv; n_val K (vv 0) = vv 0; a \<in> carrier K; vv 0 a = 1; x \<in> carrier K; Ostrowski_elem K (Suc n) vv x; Ring K; aGroup K; 1\<^sub>r \<in> carrier K; 2 \<le> m; valuation K (vv 0); 0 < vv 0 (1\<^sub>r \<plusminus> -\<^sub>a x); a \<noteq> \<zero>; valuation K (vv 0); vv 0 a \<noteq> \<infinity>; vv 0 x = 0; x^\<^bsup>K m\<^esup> \<in> carrier K; -\<^sub>a x \<in> carrier K; 1\<^sub>r \<plusminus> -\<^sub>a x \<in> carrier K\<rbrakk> \<Longrightarrow> 0 < m
[PROOF STEP]
apply (simp add:val_t2p,
       frule value_zero_nonzero[of "vv 0" "x"], assumption+,
       simp add:val_exp_ring[THEN sym], simp add:asprod_n_0,
       simp add:aadd_0_r,
       cut_tac z = m in less_le_trans[of "0" "2"], simp, assumption+)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma (in Corps) Approximation1_5Tr3:"\<lbrakk>vals_nonequiv K (Suc n) vv;
      x \<in> carrier K; Ostrowski_elem K (Suc n) vv x; j \<in> nset (Suc 0) (Suc n)\<rbrakk>
        \<Longrightarrow>  vv j ((1\<^sub>r \<plusminus> -\<^sub>a x)^\<^bsup>K m\<^esup>) = 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>vals_nonequiv K (Suc n) vv; x \<in> carrier K; Ostrowski_elem K (Suc n) vv x; j \<in> nset (Suc 0) (Suc n)\<rbrakk> \<Longrightarrow> vv j ((1\<^sub>r \<plusminus> -\<^sub>a x)^\<^bsup>K m\<^esup>) = 0
[PROOF STEP]
apply (frule Ostrowski_elem_not_one[of "n" "vv" "x"], assumption+,
       cut_tac field_is_ring, frule Ring.ring_is_ag[of "K"],
       frule Ring.ring_one[of "K"],
       frule aGroup.ag_pOp_closed[of "K" "1\<^sub>r" "-\<^sub>a x"], assumption+)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>vals_nonequiv K (Suc n) vv; x \<in> carrier K; Ostrowski_elem K (Suc n) vv x; j \<in> nset (Suc 0) (Suc n); 1\<^sub>r \<plusminus> -\<^sub>a x \<noteq> \<zero>; Ring K; aGroup K; 1\<^sub>r \<in> carrier K\<rbrakk> \<Longrightarrow> -\<^sub>a x \<in> carrier K
 2. \<lbrakk>vals_nonequiv K (Suc n) vv; x \<in> carrier K; Ostrowski_elem K (Suc n) vv x; j \<in> nset (Suc 0) (Suc n); 1\<^sub>r \<plusminus> -\<^sub>a x \<noteq> \<zero>; Ring K; aGroup K; 1\<^sub>r \<in> carrier K; 1\<^sub>r \<plusminus> -\<^sub>a x \<in> carrier K\<rbrakk> \<Longrightarrow> vv j ((1\<^sub>r \<plusminus> -\<^sub>a x)^\<^bsup>K m\<^esup>) = 0
[PROOF STEP]
apply (simp add:aGroup.ag_mOp_closed, simp add:nset_def,
       frule_tac m = j in vals_nonequiv_valuation[of "Suc n" "vv"],
       simp,
       frule_tac v1 = "vv j" and x1 = "1\<^sub>r \<plusminus> -\<^sub>a x" and n1 = m in
        val_exp_ring[THEN sym], assumption+)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>vals_nonequiv K (Suc n) vv; x \<in> carrier K; Ostrowski_elem K (Suc n) vv x; Suc 0 \<le> j \<and> j \<le> Suc n; 1\<^sub>r \<plusminus> -\<^sub>a x \<noteq> \<zero>; Ring K; aGroup K; 1\<^sub>r \<in> carrier K; 1\<^sub>r \<plusminus> -\<^sub>a x \<in> carrier K; valuation K (vv j); vv j ((1\<^sub>r \<plusminus> -\<^sub>a x)^\<^bsup>K m\<^esup>) = int m *\<^sub>a vv j (1\<^sub>r \<plusminus> -\<^sub>a x)\<rbrakk> \<Longrightarrow> vv j ((1\<^sub>r \<plusminus> -\<^sub>a x)^\<^bsup>K m\<^esup>) = 0
[PROOF STEP]
apply (frule_tac v = "vv j" and x = "1\<^sub>r" and  y = "-\<^sub>a x" in
       value_less_eq, assumption+, simp add:aGroup.ag_mOp_closed)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>vals_nonequiv K (Suc n) vv; x \<in> carrier K; Ostrowski_elem K (Suc n) vv x; Suc 0 \<le> j \<and> j \<le> Suc n; 1\<^sub>r \<plusminus> -\<^sub>a x \<noteq> \<zero>; Ring K; aGroup K; 1\<^sub>r \<in> carrier K; 1\<^sub>r \<plusminus> -\<^sub>a x \<in> carrier K; valuation K (vv j); vv j ((1\<^sub>r \<plusminus> -\<^sub>a x)^\<^bsup>K m\<^esup>) = int m *\<^sub>a vv j (1\<^sub>r \<plusminus> -\<^sub>a x)\<rbrakk> \<Longrightarrow> vv j 1\<^sub>r < vv j (-\<^sub>a x)
 2. \<lbrakk>vals_nonequiv K (Suc n) vv; x \<in> carrier K; Ostrowski_elem K (Suc n) vv x; Suc 0 \<le> j \<and> j \<le> Suc n; 1\<^sub>r \<plusminus> -\<^sub>a x \<noteq> \<zero>; Ring K; aGroup K; 1\<^sub>r \<in> carrier K; 1\<^sub>r \<plusminus> -\<^sub>a x \<in> carrier K; valuation K (vv j); vv j ((1\<^sub>r \<plusminus> -\<^sub>a x)^\<^bsup>K m\<^esup>) = int m *\<^sub>a vv j (1\<^sub>r \<plusminus> -\<^sub>a x); vv j 1\<^sub>r = vv j (1\<^sub>r \<plusminus> -\<^sub>a x)\<rbrakk> \<Longrightarrow> vv j ((1\<^sub>r \<plusminus> -\<^sub>a x)^\<^bsup>K m\<^esup>) = 0
[PROOF STEP]
apply(simp add:value_of_one, simp add:val_minus_eq,
       simp add:Ostrowski_elem_def nset_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>vals_nonequiv K (Suc n) vv; x \<in> carrier K; Ostrowski_elem K (Suc n) vv x; Suc 0 \<le> j \<and> j \<le> Suc n; 1\<^sub>r \<plusminus> -\<^sub>a x \<noteq> \<zero>; Ring K; aGroup K; 1\<^sub>r \<in> carrier K; 1\<^sub>r \<plusminus> -\<^sub>a x \<in> carrier K; valuation K (vv j); vv j ((1\<^sub>r \<plusminus> -\<^sub>a x)^\<^bsup>K m\<^esup>) = int m *\<^sub>a vv j (1\<^sub>r \<plusminus> -\<^sub>a x); vv j 1\<^sub>r = vv j (1\<^sub>r \<plusminus> -\<^sub>a x)\<rbrakk> \<Longrightarrow> vv j ((1\<^sub>r \<plusminus> -\<^sub>a x)^\<^bsup>K m\<^esup>) = 0
[PROOF STEP]
apply (simp add:value_of_one, rotate_tac -1, drule sym,
       simp add:asprod_n_0)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma (in Corps) Approximation1_5Tr4:"\<lbrakk>vals_nonequiv K (Suc n) vv;
     aa \<in> carrier K; x \<in> carrier K;
     Ostrowski_elem K (Suc n) vv x; j \<le> (Suc n)\<rbrakk> \<Longrightarrow>
     vv j (aa \<cdot>\<^sub>r (x^\<^bsup>K m\<^esup>)) = vv j aa + (int m) *\<^sub>a (vv j  x)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>vals_nonequiv K (Suc n) vv; aa \<in> carrier K; x \<in> carrier K; Ostrowski_elem K (Suc n) vv x; j \<le> Suc n\<rbrakk> \<Longrightarrow> vv j (aa \<cdot>\<^sub>r x^\<^bsup>K m\<^esup>) = vv j aa + int m *\<^sub>a vv j x
[PROOF STEP]
apply (frule Ostrowski_elem_nonzero[of "n" "vv" "x"],
                                          assumption+,
       cut_tac field_is_ring, frule Ring.ring_is_ag[of "K"])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>vals_nonequiv K (Suc n) vv; aa \<in> carrier K; x \<in> carrier K; Ostrowski_elem K (Suc n) vv x; j \<le> Suc n; x \<noteq> \<zero>; Ring K; aGroup K\<rbrakk> \<Longrightarrow> vv j (aa \<cdot>\<^sub>r x^\<^bsup>K m\<^esup>) = vv j aa + int m *\<^sub>a vv j x
[PROOF STEP]
apply (frule_tac m = j in vals_nonequiv_valuation[of "Suc n" "vv"], assumption)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>vals_nonequiv K (Suc n) vv; aa \<in> carrier K; x \<in> carrier K; Ostrowski_elem K (Suc n) vv x; j \<le> Suc n; x \<noteq> \<zero>; Ring K; aGroup K; valuation K (vv j)\<rbrakk> \<Longrightarrow> vv j (aa \<cdot>\<^sub>r x^\<^bsup>K m\<^esup>) = vv j aa + int m *\<^sub>a vv j x
[PROOF STEP]
apply (subst val_t2p[of "vv j"], assumption+,
       rule Ring.npClose, assumption+,
       cut_tac field_is_idom,
       frule_tac v1 = "vv j" and x1 = x and n1 = m in
       val_exp_ring[THEN sym], assumption+, simp)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma (in Corps) Approximation1_5Tr5:"\<lbrakk>vals_nonequiv K (Suc n) vv;
     a \<in> carrier K; a \<noteq> \<zero>; x \<in> carrier K;
     Ostrowski_elem K (Suc n) vv x; j \<in> nset (Suc 0) (Suc n)\<rbrakk> \<Longrightarrow>
               \<exists>l. \<forall>m. l < m \<longrightarrow> 0 < (vv j (a \<cdot>\<^sub>r (x^\<^bsup>K m\<^esup>)))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>vals_nonequiv K (Suc n) vv; a \<in> carrier K; a \<noteq> \<zero>; x \<in> carrier K; Ostrowski_elem K (Suc n) vv x; j \<in> nset (Suc 0) (Suc n)\<rbrakk> \<Longrightarrow> \<exists>l. \<forall>m>l. 0 < vv j (a \<cdot>\<^sub>r x^\<^bsup>K m\<^esup>)
[PROOF STEP]
apply (frule Ostrowski_elem_nonzero[of "n" "vv" "x"], assumption+,
      subgoal_tac "\<forall>n. vv j (a \<cdot>\<^sub>r (x^\<^bsup>K n\<^esup>)) = vv j a + (int n) *\<^sub>a (vv j  x)",
      simp,
      thin_tac "\<forall>n. vv j (a \<cdot>\<^sub>r x^\<^bsup>K n\<^esup>) = vv j a + int n *\<^sub>a vv j x")
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>vals_nonequiv K (Suc n) vv; a \<in> carrier K; a \<noteq> \<zero>; x \<in> carrier K; Ostrowski_elem K (Suc n) vv x; j \<in> nset (Suc 0) (Suc n); x \<noteq> \<zero>\<rbrakk> \<Longrightarrow> \<exists>l. \<forall>m>l. 0 < vv j a + int m *\<^sub>a vv j x
 2. \<lbrakk>vals_nonequiv K (Suc n) vv; a \<in> carrier K; a \<noteq> \<zero>; x \<in> carrier K; Ostrowski_elem K (Suc n) vv x; j \<in> nset (Suc 0) (Suc n); x \<noteq> \<zero>\<rbrakk> \<Longrightarrow> \<forall>n. vv j (a \<cdot>\<^sub>r x^\<^bsup>K n\<^esup>) = vv j a + int n *\<^sub>a vv j x
[PROOF STEP]
prefer 2
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>vals_nonequiv K (Suc n) vv; a \<in> carrier K; a \<noteq> \<zero>; x \<in> carrier K; Ostrowski_elem K (Suc n) vv x; j \<in> nset (Suc 0) (Suc n); x \<noteq> \<zero>\<rbrakk> \<Longrightarrow> \<forall>n. vv j (a \<cdot>\<^sub>r x^\<^bsup>K n\<^esup>) = vv j a + int n *\<^sub>a vv j x
 2. \<lbrakk>vals_nonequiv K (Suc n) vv; a \<in> carrier K; a \<noteq> \<zero>; x \<in> carrier K; Ostrowski_elem K (Suc n) vv x; j \<in> nset (Suc 0) (Suc n); x \<noteq> \<zero>\<rbrakk> \<Longrightarrow> \<exists>l. \<forall>m>l. 0 < vv j a + int m *\<^sub>a vv j x
[PROOF STEP]
apply (rule allI, rule Approximation1_5Tr4[of _ vv a x j],
         assumption+, simp add:nset_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>vals_nonequiv K (Suc n) vv; a \<in> carrier K; a \<noteq> \<zero>; x \<in> carrier K; Ostrowski_elem K (Suc n) vv x; j \<in> nset (Suc 0) (Suc n); x \<noteq> \<zero>\<rbrakk> \<Longrightarrow> \<exists>l. \<forall>m>l. 0 < vv j a + int m *\<^sub>a vv j x
[PROOF STEP]
apply (frule_tac m = j in vals_nonequiv_valuation[of "Suc n" "vv"],
       simp add:nset_def,
       frule val_nonzero_z[of "vv j" "a"], assumption+, erule exE,
       simp add:Ostrowski_elem_def,
       frule conjunct2, fold Ostrowski_elem_def,
       drule_tac x = j in bspec, assumption)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>z. \<lbrakk>vals_nonequiv K (Suc n) vv; a \<in> carrier K; a \<noteq> \<zero>; x \<in> carrier K; Ostrowski_elem K (Suc n) vv x; j \<in> nset (Suc 0) (Suc n); x \<noteq> \<zero>; valuation K (vv j); vv j a = ant z; 0 < vv j x\<rbrakk> \<Longrightarrow> \<exists>l. \<forall>m>l. 0 < ant z + int m *\<^sub>a vv j x
[PROOF STEP]
apply (frule Ostrowski_elem_nonzero[of "n" "vv" "x"], assumption+,
       frule val_nonzero_z[of "vv j" "x"], assumption+, erule exE, simp,
       frule_tac a = za and x = z in zmult_pos_bignumTr,
       simp add:asprod_amult a_z_z a_zpz)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma (in Corps) Approximation1_5Tr6:"\<lbrakk>vals_nonequiv K (Suc n) vv;
      a \<in> carrier K; a \<noteq> \<zero>; x \<in> carrier K;
      Ostrowski_elem K (Suc n) vv x; j \<in> nset (Suc 0) (Suc n)\<rbrakk> \<Longrightarrow>
        \<exists>l. \<forall>m. l < m \<longrightarrow> vv j ((1\<^sub>r \<plusminus> -\<^sub>a x)^\<^bsup>K m\<^esup> \<plusminus> a \<cdot>\<^sub>r (x^\<^bsup>K m\<^esup>)) = 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>vals_nonequiv K (Suc n) vv; a \<in> carrier K; a \<noteq> \<zero>; x \<in> carrier K; Ostrowski_elem K (Suc n) vv x; j \<in> nset (Suc 0) (Suc n)\<rbrakk> \<Longrightarrow> \<exists>l. \<forall>m>l. vv j ((1\<^sub>r \<plusminus> -\<^sub>a x)^\<^bsup>K m\<^esup> \<plusminus> a \<cdot>\<^sub>r x^\<^bsup>K m\<^esup>) = 0
[PROOF STEP]
apply (frule vals_nonequiv_valuation[of "Suc n" "vv" "j"],
       simp add:nset_def,
       frule Approximation1_5Tr5[of "n" "vv" "a" "x" "j"],
               assumption+, erule exE,
       cut_tac field_is_ring, frule Ring.ring_is_ag[of "K"],
       subgoal_tac "\<forall>m. l < m \<longrightarrow> vv j ((1\<^sub>r \<plusminus> -\<^sub>a x)^\<^bsup>K m\<^esup> \<plusminus> a \<cdot>\<^sub>r (x^\<^bsup>K m\<^esup>)) =
       vv j ((1\<^sub>r \<plusminus> -\<^sub>a x)^\<^bsup>K m\<^esup>)")
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>l. \<lbrakk>vals_nonequiv K (Suc n) vv; a \<in> carrier K; a \<noteq> \<zero>; x \<in> carrier K; Ostrowski_elem K (Suc n) vv x; j \<in> nset (Suc 0) (Suc n); valuation K (vv j); \<forall>m>l. 0 < vv j (a \<cdot>\<^sub>r x^\<^bsup>K m\<^esup>); Ring K; aGroup K; \<forall>m>l. vv j ((1\<^sub>r \<plusminus> -\<^sub>a x)^\<^bsup>K m\<^esup> \<plusminus> a \<cdot>\<^sub>r x^\<^bsup>K m\<^esup>) = vv j ((1\<^sub>r \<plusminus> -\<^sub>a x)^\<^bsup>K m\<^esup>)\<rbrakk> \<Longrightarrow> \<exists>l. \<forall>m>l. vv j ((1\<^sub>r \<plusminus> -\<^sub>a x)^\<^bsup>K m\<^esup> \<plusminus> a \<cdot>\<^sub>r x^\<^bsup>K m\<^esup>) = 0
 2. \<And>l. \<lbrakk>vals_nonequiv K (Suc n) vv; a \<in> carrier K; a \<noteq> \<zero>; x \<in> carrier K; Ostrowski_elem K (Suc n) vv x; j \<in> nset (Suc 0) (Suc n); valuation K (vv j); \<forall>m>l. 0 < vv j (a \<cdot>\<^sub>r x^\<^bsup>K m\<^esup>); Ring K; aGroup K\<rbrakk> \<Longrightarrow> \<forall>m>l. vv j ((1\<^sub>r \<plusminus> -\<^sub>a x)^\<^bsup>K m\<^esup> \<plusminus> a \<cdot>\<^sub>r x^\<^bsup>K m\<^esup>) = vv j ((1\<^sub>r \<plusminus> -\<^sub>a x)^\<^bsup>K m\<^esup>)
[PROOF STEP]
apply (simp add:Approximation1_5Tr3, blast)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>l. \<lbrakk>vals_nonequiv K (Suc n) vv; a \<in> carrier K; a \<noteq> \<zero>; x \<in> carrier K; Ostrowski_elem K (Suc n) vv x; j \<in> nset (Suc 0) (Suc n); valuation K (vv j); \<forall>m>l. 0 < vv j (a \<cdot>\<^sub>r x^\<^bsup>K m\<^esup>); Ring K; aGroup K\<rbrakk> \<Longrightarrow> \<forall>m>l. vv j ((1\<^sub>r \<plusminus> -\<^sub>a x)^\<^bsup>K m\<^esup> \<plusminus> a \<cdot>\<^sub>r x^\<^bsup>K m\<^esup>) = vv j ((1\<^sub>r \<plusminus> -\<^sub>a x)^\<^bsup>K m\<^esup>)
[PROOF STEP]
apply (rule allI, rule impI,
        drule_tac a = m in forall_spec, assumption,
        frule_tac x = "(1\<^sub>r \<plusminus> -\<^sub>a x)^\<^bsup>K m\<^esup>" and y = "a \<cdot>\<^sub>r (x^\<^bsup>K m\<^esup>)" in
           value_less_eq[of "vv j"],
        rule Ring.npClose, assumption+,
        rule aGroup.ag_pOp_closed, assumption+, simp add:Ring.ring_one,
        simp add:aGroup.ag_mOp_closed)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>l m. \<lbrakk>vals_nonequiv K (Suc n) vv; a \<in> carrier K; a \<noteq> \<zero>; x \<in> carrier K; Ostrowski_elem K (Suc n) vv x; j \<in> nset (Suc 0) (Suc n); valuation K (vv j); Ring K; aGroup K; l < m; 0 < vv j (a \<cdot>\<^sub>r x^\<^bsup>K m\<^esup>)\<rbrakk> \<Longrightarrow> a \<cdot>\<^sub>r x^\<^bsup>K m\<^esup> \<in> carrier K
 2. \<And>l m. \<lbrakk>vals_nonequiv K (Suc n) vv; a \<in> carrier K; a \<noteq> \<zero>; x \<in> carrier K; Ostrowski_elem K (Suc n) vv x; j \<in> nset (Suc 0) (Suc n); valuation K (vv j); Ring K; aGroup K; l < m; 0 < vv j (a \<cdot>\<^sub>r x^\<^bsup>K m\<^esup>)\<rbrakk> \<Longrightarrow> vv j ((1\<^sub>r \<plusminus> -\<^sub>a x)^\<^bsup>K m\<^esup>) < vv j (a \<cdot>\<^sub>r x^\<^bsup>K m\<^esup>)
 3. \<And>l m. \<lbrakk>vals_nonequiv K (Suc n) vv; a \<in> carrier K; a \<noteq> \<zero>; x \<in> carrier K; Ostrowski_elem K (Suc n) vv x; j \<in> nset (Suc 0) (Suc n); valuation K (vv j); Ring K; aGroup K; l < m; 0 < vv j (a \<cdot>\<^sub>r x^\<^bsup>K m\<^esup>); vv j ((1\<^sub>r \<plusminus> -\<^sub>a x)^\<^bsup>K m\<^esup>) = vv j ((1\<^sub>r \<plusminus> -\<^sub>a x)^\<^bsup>K m\<^esup> \<plusminus> a \<cdot>\<^sub>r x^\<^bsup>K m\<^esup>)\<rbrakk> \<Longrightarrow> vv j ((1\<^sub>r \<plusminus> -\<^sub>a x)^\<^bsup>K m\<^esup> \<plusminus> a \<cdot>\<^sub>r x^\<^bsup>K m\<^esup>) = vv j ((1\<^sub>r \<plusminus> -\<^sub>a x)^\<^bsup>K m\<^esup>)
[PROOF STEP]
apply (rule Ring.ring_tOp_closed, assumption+,
        rule Ring.npClose, assumption+,
        simp add:Approximation1_5Tr3,
        frule sym, assumption)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done