[STATEMENT]
lemma (in Corps) Approximation1_5Tr7:"\<lbrakk>a \<in> carrier K; vv 0 a = 1;
      x \<in> carrier K\<rbrakk> \<Longrightarrow>
      vals_nonequiv K (Suc n) vv  \<and> Ostrowski_elem K (Suc n) vv x \<longrightarrow>
      (\<exists>l. \<forall>m. l < m \<longrightarrow> (\<forall>j\<in>nset (Suc 0) (Suc n).
                (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>a \<in> carrier K; vv 0 a = 1; x \<in> carrier K\<rbrakk> \<Longrightarrow> vals_nonequiv K (Suc n) vv \<and> Ostrowski_elem K (Suc n) vv x \<longrightarrow> (\<exists>l. \<forall>m>l. \<forall>j\<in>nset (Suc 0) (Suc n). 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 (induct_tac n,
       rule impI, erule conjE, simp add:nset_m_m[of "Suc 0"],
       frule vals_nonequiv_valuation[of "Suc 0" "vv" "Suc 0"], simp,
       frule Approximation1_5Tr6[of "0" "vv" "a" "x" "Suc 0"], assumption+)
[PROOF STATE]
proof (prove)
goal (6 subgoals):
 1. \<lbrakk>a \<in> carrier K; vv 0 a = 1; x \<in> carrier K; vals_nonequiv K (Suc 0) vv; Ostrowski_elem K (Suc 0) vv x; valuation K (vv (Suc 0))\<rbrakk> \<Longrightarrow> a \<noteq> \<zero>
 2. \<lbrakk>a \<in> carrier K; vv 0 a = 1; x \<in> carrier K; vals_nonequiv K (Suc 0) vv; Ostrowski_elem K (Suc 0) vv x; valuation K (vv (Suc 0))\<rbrakk> \<Longrightarrow> x \<in> carrier K
 3. \<lbrakk>a \<in> carrier K; vv 0 a = 1; x \<in> carrier K; vals_nonequiv K (Suc 0) vv; Ostrowski_elem K (Suc 0) vv x; valuation K (vv (Suc 0))\<rbrakk> \<Longrightarrow> Ostrowski_elem K (Suc 0) vv x
 4. \<lbrakk>a \<in> carrier K; vv 0 a = 1; x \<in> carrier K; vals_nonequiv K (Suc 0) vv; Ostrowski_elem K (Suc 0) vv x; valuation K (vv (Suc 0))\<rbrakk> \<Longrightarrow> Suc 0 \<in> nset (Suc 0) (Suc 0)
 5. \<lbrakk>a \<in> carrier K; vv 0 a = 1; x \<in> carrier K; vals_nonequiv K (Suc 0) vv; Ostrowski_elem K (Suc 0) vv x; valuation K (vv (Suc 0)); \<exists>l. \<forall>m>l. vv (Suc 0) ((1\<^sub>r \<plusminus> -\<^sub>a x)^\<^bsup>K m\<^esup> \<plusminus> a \<cdot>\<^sub>r x^\<^bsup>K m\<^esup>) = 0\<rbrakk> \<Longrightarrow> \<exists>l. \<forall>m>l. vv (Suc 0) ((1\<^sub>r \<plusminus> -\<^sub>a x)^\<^bsup>K m\<^esup> \<plusminus> a \<cdot>\<^sub>r x^\<^bsup>K m\<^esup>) = 0
 6. \<And>n. \<lbrakk>a \<in> carrier K; vv 0 a = 1; x \<in> carrier K; vals_nonequiv K (Suc n) vv \<and> Ostrowski_elem K (Suc n) vv x \<longrightarrow> (\<exists>l. \<forall>m>l. \<forall>j\<in>nset (Suc 0) (Suc n). vv j ((1\<^sub>r \<plusminus> -\<^sub>a x)^\<^bsup>K m\<^esup> \<plusminus> a \<cdot>\<^sub>r x^\<^bsup>K m\<^esup>) = 0)\<rbrakk> \<Longrightarrow> vals_nonequiv K (Suc (Suc n)) vv \<and> Ostrowski_elem K (Suc (Suc n)) vv x \<longrightarrow> (\<exists>l. \<forall>m>l. \<forall>j\<in>nset (Suc 0) (Suc (Suc n)). 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 0" "vv" "0"], simp,
       frule val_1_nonzero[of "vv 0" "a"], assumption+, simp add:nset_def,
       assumption)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>n. \<lbrakk>a \<in> carrier K; vv 0 a = 1; x \<in> carrier K; vals_nonequiv K (Suc n) vv \<and> Ostrowski_elem K (Suc n) vv x \<longrightarrow> (\<exists>l. \<forall>m>l. \<forall>j\<in>nset (Suc 0) (Suc n). vv j ((1\<^sub>r \<plusminus> -\<^sub>a x)^\<^bsup>K m\<^esup> \<plusminus> a \<cdot>\<^sub>r x^\<^bsup>K m\<^esup>) = 0)\<rbrakk> \<Longrightarrow> vals_nonequiv K (Suc (Suc n)) vv \<and> Ostrowski_elem K (Suc (Suc n)) vv x \<longrightarrow> (\<exists>l. \<forall>m>l. \<forall>j\<in>nset (Suc 0) (Suc (Suc n)). 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]
(** case n **)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>n. \<lbrakk>a \<in> carrier K; vv 0 a = 1; x \<in> carrier K; vals_nonequiv K (Suc n) vv \<and> Ostrowski_elem K (Suc n) vv x \<longrightarrow> (\<exists>l. \<forall>m>l. \<forall>j\<in>nset (Suc 0) (Suc n). vv j ((1\<^sub>r \<plusminus> -\<^sub>a x)^\<^bsup>K m\<^esup> \<plusminus> a \<cdot>\<^sub>r x^\<^bsup>K m\<^esup>) = 0)\<rbrakk> \<Longrightarrow> vals_nonequiv K (Suc (Suc n)) vv \<and> Ostrowski_elem K (Suc (Suc n)) vv x \<longrightarrow> (\<exists>l. \<forall>m>l. \<forall>j\<in>nset (Suc 0) (Suc (Suc n)). 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 (rule impI, erule conjE,
       frule_tac n = n in  restrict_vals_nonequiv[of _ "vv"],
       frule_tac n = n in restrict_Ostrowski_elem[of "x"  _ "vv"],
          assumption, simp,
       erule exE,
       frule_tac n = "Suc n" and j = "Suc (Suc n)" in Approximation1_5Tr6
        [of _ "vv" "a" "x"], assumption+,
       frule_tac n = "Suc (Suc n)" in vals_nonequiv_valuation[of _ "vv"
        "0"],simp,
       rule val_1_nonzero[of "vv 0" "a"], assumption+,
       simp add:nset_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>n l. \<lbrakk>a \<in> carrier K; vv 0 a = 1; x \<in> carrier K; vals_nonequiv K (Suc (Suc n)) vv; Ostrowski_elem K (Suc (Suc n)) vv x; vals_nonequiv K (Suc n) vv; Ostrowski_elem K (Suc n) vv x; \<forall>m>l. \<forall>j\<in>nset (Suc 0) (Suc n). vv j ((1\<^sub>r \<plusminus> -\<^sub>a x)^\<^bsup>K m\<^esup> \<plusminus> a \<cdot>\<^sub>r x^\<^bsup>K m\<^esup>) = 0; \<exists>l. \<forall>m>l. vv (Suc (Suc n)) ((1\<^sub>r \<plusminus> -\<^sub>a x)^\<^bsup>K m\<^esup> \<plusminus> a \<cdot>\<^sub>r x^\<^bsup>K m\<^esup>) = 0\<rbrakk> \<Longrightarrow> \<exists>l. \<forall>m>l. \<forall>j\<in>nset (Suc 0) (Suc (Suc n)). 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 (erule exE,
       subgoal_tac "\<forall>m. (max l la) < m \<longrightarrow> (\<forall>j\<in>nset (Suc 0) (Suc (Suc n)).
         vv j ((1\<^sub>r \<plusminus> -\<^sub>a x)^\<^bsup>K m\<^esup> \<plusminus> a \<cdot>\<^sub>r (x^\<^bsup>K m\<^esup>)) = 0)",
       blast,
      simp add:nset_Suc)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma (in Corps) Approximation1_5P:"\<lbrakk>vals_nonequiv K (Suc n) vv;
    n_val K (vv 0) = vv 0\<rbrakk> \<Longrightarrow>
    \<exists>x\<in>carrier K. ((vv 0 x = 1) \<and> (\<forall>j\<in>nset (Suc 0) (Suc n). (vv j x) = 0))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>vals_nonequiv K (Suc n) vv; n_val K (vv 0) = vv 0\<rbrakk> \<Longrightarrow> \<exists>x\<in>carrier K. vv 0 x = 1 \<and> (\<forall>j\<in>nset (Suc 0) (Suc n). vv j x = 0)
[PROOF STEP]
apply (frule vals_nonequiv_valuation[of "Suc n" "vv" "0"], simp)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>vals_nonequiv K (Suc n) vv; n_val K (vv 0) = vv 0; valuation K (vv 0)\<rbrakk> \<Longrightarrow> \<exists>x\<in>carrier K. vv 0 x = 1 \<and> (\<forall>j\<in>nset (Suc 0) (Suc n). vv j x = 0)
[PROOF STEP]
apply (
       frule n_val_surj[of "vv 0"], erule bexE)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>vals_nonequiv K (Suc n) vv; n_val K (vv 0) = vv 0; valuation K (vv 0); x \<in> carrier K; n_val K (vv 0) x = 1\<rbrakk> \<Longrightarrow> \<exists>x\<in>carrier K. vv 0 x = 1 \<and> (\<forall>j\<in>nset (Suc 0) (Suc n). vv j x = 0)
[PROOF STEP]
apply (
       rename_tac aa)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>aa. \<lbrakk>vals_nonequiv K (Suc n) vv; n_val K (vv 0) = vv 0; valuation K (vv 0); aa \<in> carrier K; n_val K (vv 0) aa = 1\<rbrakk> \<Longrightarrow> \<exists>x\<in>carrier K. vv 0 x = 1 \<and> (\<forall>j\<in>nset (Suc 0) (Suc n). vv j x = 0)
[PROOF STEP]
apply (
       cut_tac n = n in Ostrowski)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>aa. \<lbrakk>vals_nonequiv K (Suc n) vv; n_val K (vv 0) = vv 0; valuation K (vv 0); aa \<in> carrier K; n_val K (vv 0) aa = 1; \<forall>vv. vals_nonequiv K (Suc n) vv \<longrightarrow> (\<exists>x\<in>carrier K. Ostrowski_elem K (Suc n) vv x)\<rbrakk> \<Longrightarrow> \<exists>x\<in>carrier K. vv 0 x = 1 \<and> (\<forall>j\<in>nset (Suc 0) (Suc n). vv j x = 0)
[PROOF STEP]
apply (
       drule_tac a = vv in forall_spec[of "vals_nonequiv K (Suc n)"], simp)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>aa. \<lbrakk>vals_nonequiv K (Suc n) vv; n_val K (vv 0) = vv 0; valuation K (vv 0); aa \<in> carrier K; n_val K (vv 0) aa = 1; \<exists>x\<in>carrier K. Ostrowski_elem K (Suc n) vv x\<rbrakk> \<Longrightarrow> \<exists>x\<in>carrier K. vv 0 x = 1 \<and> (\<forall>j\<in>nset (Suc 0) (Suc n). vv j x = 0)
[PROOF STEP]
apply (
       erule bexE,
       frule_tac a = aa and x = x in Approximation1_5Tr1[of "n" "vv"],
       assumption+,
       simp, assumption+)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>aa x. \<lbrakk>vals_nonequiv K (Suc n) vv; n_val K (vv 0) = vv 0; valuation K (vv 0); aa \<in> carrier K; n_val K (vv 0) aa = 1; x \<in> carrier K; Ostrowski_elem K (Suc n) vv x; \<forall>m\<ge>2. vv 0 ((1\<^sub>r \<plusminus> -\<^sub>a x)^\<^bsup>K m\<^esup> \<plusminus> aa \<cdot>\<^sub>r x^\<^bsup>K m\<^esup>) = 1\<rbrakk> \<Longrightarrow> \<exists>x\<in>carrier K. vv 0 x = 1 \<and> (\<forall>j\<in>nset (Suc 0) (Suc n). vv j x = 0)
[PROOF STEP]
apply (frule_tac a = aa and x = x in Approximation1_5Tr7[of _ "vv" _ "n"],
       simp, assumption,
       simp, erule exE,
       cut_tac b = "Suc l" in max.cobounded1[of "2"],
       cut_tac b = "Suc l" in max.cobounded2[of _ "2"],
       cut_tac n = l in lessI,
       frule_tac x = l and y = "Suc l" and z = "max 2 (Suc l)" in
         less_le_trans, assumption+,
       thin_tac "Suc l \<le> max 2 (Suc l)", thin_tac "l < Suc l",
       drule_tac a = "max 2 (Suc l)" in forall_spec, simp,
       drule_tac a = "max 2 (Suc l)" in forall_spec, assumption)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>aa x l. \<lbrakk>vals_nonequiv K (Suc n) vv; n_val K (vv 0) = vv 0; valuation K (vv 0); aa \<in> carrier K; vv 0 aa = 1; x \<in> carrier K; Ostrowski_elem K (Suc n) vv x; 2 \<le> max 2 (Suc l); l < max 2 (Suc l); vv 0 ((1\<^sub>r \<plusminus> -\<^sub>a x)^\<^bsup>K max 2 (Suc l)\<^esup> \<plusminus> aa \<cdot>\<^sub>r x^\<^bsup>K max 2 (Suc l)\<^esup>) = 1; \<forall>j\<in>nset (Suc 0) (Suc n). vv j ((1\<^sub>r \<plusminus> -\<^sub>a x)^\<^bsup>K max 2 (Suc l)\<^esup> \<plusminus> aa \<cdot>\<^sub>r x^\<^bsup>K max 2 (Suc l)\<^esup>) = 0\<rbrakk> \<Longrightarrow> \<exists>x\<in>carrier K. vv 0 x = 1 \<and> (\<forall>j\<in>nset (Suc 0) (Suc n). vv j x = 0)
[PROOF STEP]
apply (subgoal_tac "(1\<^sub>r \<plusminus> -\<^sub>a x)^\<^bsup>K (max 2 (Suc l))\<^esup> \<plusminus> aa \<cdot>\<^sub>r (x^\<^bsup>K (max 2 (Suc l))\<^esup>) \<in>
       carrier K",
       blast,
       cut_tac field_is_ring, frule Ring.ring_is_ag[of "K"],
       rule aGroup.ag_pOp_closed, assumption+, rule Ring.npClose, assumption+,
       rule aGroup.ag_pOp_closed, assumption+, simp add:Ring.ring_one,
       simp add:aGroup.ag_mOp_closed, rule Ring.ring_tOp_closed, assumption+,
       rule Ring.npClose, assumption+)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma K_gamma_hom:"k \<le> n \<Longrightarrow> \<forall>j \<le> n. (\<lambda>l. \<gamma>\<^bsub>k l\<^esub>) j \<in> Zset"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. k \<le> n \<Longrightarrow> \<forall>j\<le>n. \<gamma>\<^bsub>k j\<^esub> \<in> Zset
[PROOF STEP]
apply (simp add:Zset_def)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma transpos_eq:"(\<tau>\<^bsub>0 0\<^esub>) k = k"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<tau>\<^bsub>0 0\<^esub>) k = k
[PROOF STEP]
by (simp add:transpos_def)


[STATEMENT]
lemma (in Corps) transpos_vals_nonequiv:"\<lbrakk>vals_nonequiv K (Suc n) vv;
      j \<le> (Suc n)\<rbrakk> \<Longrightarrow> vals_nonequiv K (Suc n) (vv \<circ> (\<tau>\<^bsub>0 j\<^esub>))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>vals_nonequiv K (Suc n) vv; j \<le> Suc n\<rbrakk> \<Longrightarrow> vals_nonequiv K (Suc n) (vv \<circ> \<tau>\<^bsub>0 j\<^esub>)
[PROOF STEP]
apply (simp add:vals_nonequiv_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>valuations K (Suc n) vv \<and> (\<forall>j\<le>Suc n. \<forall>l\<le>Suc n. j \<noteq> l \<longrightarrow> \<not> v_equiv K (vv j) (vv l)); j \<le> Suc n\<rbrakk> \<Longrightarrow> valuations K (Suc n) (vv \<circ> \<tau>\<^bsub>0 j\<^esub>) \<and> (\<forall>ja\<le>Suc n. \<forall>l\<le>Suc n. ja \<noteq> l \<longrightarrow> \<not> v_equiv K (vv ((\<tau>\<^bsub>0 j\<^esub>) ja)) (vv ((\<tau>\<^bsub>0 j\<^esub>) l)))
[PROOF STEP]
apply (frule conjunct1, fold vals_nonequiv_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>vals_nonequiv K (Suc n) vv; j \<le> Suc n; valuations K (Suc n) vv\<rbrakk> \<Longrightarrow> valuations K (Suc n) (vv \<circ> \<tau>\<^bsub>0 j\<^esub>) \<and> (\<forall>ja\<le>Suc n. \<forall>l\<le>Suc n. ja \<noteq> l \<longrightarrow> \<not> v_equiv K (vv ((\<tau>\<^bsub>0 j\<^esub>) ja)) (vv ((\<tau>\<^bsub>0 j\<^esub>) l)))
[PROOF STEP]
apply (simp add:valuations_def, rule conjI)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>vals_nonequiv K (Suc n) vv; j \<le> Suc n; \<forall>j\<le>Suc n. valuation K (vv j)\<rbrakk> \<Longrightarrow> \<forall>ja\<le>Suc n. valuation K (vv ((\<tau>\<^bsub>0 j\<^esub>) ja))
 2. \<lbrakk>vals_nonequiv K (Suc n) vv; j \<le> Suc n; \<forall>j\<le>Suc n. valuation K (vv j)\<rbrakk> \<Longrightarrow> \<forall>ja\<le>Suc n. \<forall>l\<le>Suc n. ja \<noteq> l \<longrightarrow> \<not> v_equiv K (vv ((\<tau>\<^bsub>0 j\<^esub>) ja)) (vv ((\<tau>\<^bsub>0 j\<^esub>) l))
[PROOF STEP]
apply (rule allI, rule impI)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>ja. \<lbrakk>vals_nonequiv K (Suc n) vv; j \<le> Suc n; \<forall>j\<le>Suc n. valuation K (vv j); ja \<le> Suc n\<rbrakk> \<Longrightarrow> valuation K (vv ((\<tau>\<^bsub>0 j\<^esub>) ja))
 2. \<lbrakk>vals_nonequiv K (Suc n) vv; j \<le> Suc n; \<forall>j\<le>Suc n. valuation K (vv j)\<rbrakk> \<Longrightarrow> \<forall>ja\<le>Suc n. \<forall>l\<le>Suc n. ja \<noteq> l \<longrightarrow> \<not> v_equiv K (vv ((\<tau>\<^bsub>0 j\<^esub>) ja)) (vv ((\<tau>\<^bsub>0 j\<^esub>) l))
[PROOF STEP]
apply (case_tac "ja = 0", simp,
        case_tac "j = 0", simp add:transpos_eq)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>ja. \<lbrakk>vals_nonequiv K (Suc n) vv; j \<le> Suc n; \<forall>j\<le>Suc n. valuation K (vv j); ja = 0; j \<noteq> 0\<rbrakk> \<Longrightarrow> valuation K (vv ((\<tau>\<^bsub>0 j\<^esub>) 0))
 2. \<And>ja. \<lbrakk>vals_nonequiv K (Suc n) vv; j \<le> Suc n; \<forall>j\<le>Suc n. valuation K (vv j); ja \<le> Suc n; ja \<noteq> 0\<rbrakk> \<Longrightarrow> valuation K (vv ((\<tau>\<^bsub>0 j\<^esub>) ja))
 3. \<lbrakk>vals_nonequiv K (Suc n) vv; j \<le> Suc n; \<forall>j\<le>Suc n. valuation K (vv j)\<rbrakk> \<Longrightarrow> \<forall>ja\<le>Suc n. \<forall>l\<le>Suc n. ja \<noteq> l \<longrightarrow> \<not> v_equiv K (vv ((\<tau>\<^bsub>0 j\<^esub>) ja)) (vv ((\<tau>\<^bsub>0 j\<^esub>) l))
[PROOF STEP]
apply (subst transpos_ij_1[of "0" "Suc n" "j"], simp, assumption+,
        rule not_sym, assumption, simp)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>ja. \<lbrakk>vals_nonequiv K (Suc n) vv; j \<le> Suc n; \<forall>j\<le>Suc n. valuation K (vv j); ja \<le> Suc n; ja \<noteq> 0\<rbrakk> \<Longrightarrow> valuation K (vv ((\<tau>\<^bsub>0 j\<^esub>) ja))
 2. \<lbrakk>vals_nonequiv K (Suc n) vv; j \<le> Suc n; \<forall>j\<le>Suc n. valuation K (vv j)\<rbrakk> \<Longrightarrow> \<forall>ja\<le>Suc n. \<forall>l\<le>Suc n. ja \<noteq> l \<longrightarrow> \<not> v_equiv K (vv ((\<tau>\<^bsub>0 j\<^esub>) ja)) (vv ((\<tau>\<^bsub>0 j\<^esub>) l))
[PROOF STEP]
apply (case_tac "ja = j", simp)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>ja. \<lbrakk>vals_nonequiv K (Suc n) vv; \<forall>j\<le>Suc n. valuation K (vv j); j \<le> Suc n; 0 < j; ja = j\<rbrakk> \<Longrightarrow> valuation K (vv ((\<tau>\<^bsub>0 j\<^esub>) j))
 2. \<And>ja. \<lbrakk>vals_nonequiv K (Suc n) vv; j \<le> Suc n; \<forall>j\<le>Suc n. valuation K (vv j); ja \<le> Suc n; ja \<noteq> 0; ja \<noteq> j\<rbrakk> \<Longrightarrow> valuation K (vv ((\<tau>\<^bsub>0 j\<^esub>) ja))
 3. \<lbrakk>vals_nonequiv K (Suc n) vv; j \<le> Suc n; \<forall>j\<le>Suc n. valuation K (vv j)\<rbrakk> \<Longrightarrow> \<forall>ja\<le>Suc n. \<forall>l\<le>Suc n. ja \<noteq> l \<longrightarrow> \<not> v_equiv K (vv ((\<tau>\<^bsub>0 j\<^esub>) ja)) (vv ((\<tau>\<^bsub>0 j\<^esub>) l))
[PROOF STEP]
apply (subst transpos_ij_2[of "0" "Suc n" "j"], simp, assumption, simp,
        simp add:vals_nonequiv_valuation)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>ja. \<lbrakk>vals_nonequiv K (Suc n) vv; j \<le> Suc n; \<forall>j\<le>Suc n. valuation K (vv j); ja \<le> Suc n; ja \<noteq> 0; ja \<noteq> j\<rbrakk> \<Longrightarrow> valuation K (vv ((\<tau>\<^bsub>0 j\<^esub>) ja))
 2. \<lbrakk>vals_nonequiv K (Suc n) vv; j \<le> Suc n; \<forall>j\<le>Suc n. valuation K (vv j)\<rbrakk> \<Longrightarrow> \<forall>ja\<le>Suc n. \<forall>l\<le>Suc n. ja \<noteq> l \<longrightarrow> \<not> v_equiv K (vv ((\<tau>\<^bsub>0 j\<^esub>) ja)) (vv ((\<tau>\<^bsub>0 j\<^esub>) l))
[PROOF STEP]
apply (case_tac "j = 0", simp add:transpos_eq)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>ja. \<lbrakk>vals_nonequiv K (Suc n) vv; j \<le> Suc n; \<forall>j\<le>Suc n. valuation K (vv j); ja \<le> Suc n; ja \<noteq> 0; ja \<noteq> j; j \<noteq> 0\<rbrakk> \<Longrightarrow> valuation K (vv ((\<tau>\<^bsub>0 j\<^esub>) ja))
 2. \<lbrakk>vals_nonequiv K (Suc n) vv; j \<le> Suc n; \<forall>j\<le>Suc n. valuation K (vv j)\<rbrakk> \<Longrightarrow> \<forall>ja\<le>Suc n. \<forall>l\<le>Suc n. ja \<noteq> l \<longrightarrow> \<not> v_equiv K (vv ((\<tau>\<^bsub>0 j\<^esub>) ja)) (vv ((\<tau>\<^bsub>0 j\<^esub>) l))
[PROOF STEP]
apply (cut_tac x = ja in transpos_id_1[of 0 "Suc n" j], simp, assumption+,
        rule not_sym, assumption+)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>ja. \<lbrakk>vals_nonequiv K (Suc n) vv; j \<le> Suc n; \<forall>j\<le>Suc n. valuation K (vv j); ja \<le> Suc n; ja \<noteq> 0; ja \<noteq> j; j \<noteq> 0; (\<tau>\<^bsub>0 j\<^esub>) ja = ja\<rbrakk> \<Longrightarrow> valuation K (vv ((\<tau>\<^bsub>0 j\<^esub>) ja))
 2. \<lbrakk>vals_nonequiv K (Suc n) vv; j \<le> Suc n; \<forall>j\<le>Suc n. valuation K (vv j)\<rbrakk> \<Longrightarrow> \<forall>ja\<le>Suc n. \<forall>l\<le>Suc n. ja \<noteq> l \<longrightarrow> \<not> v_equiv K (vv ((\<tau>\<^bsub>0 j\<^esub>) ja)) (vv ((\<tau>\<^bsub>0 j\<^esub>) l))
[PROOF STEP]
apply (simp add:vals_nonequiv_valuation,
        (rule allI, rule impI)+, rule impI)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>ja l. \<lbrakk>vals_nonequiv K (Suc n) vv; j \<le> Suc n; \<forall>j\<le>Suc n. valuation K (vv j); ja \<le> Suc n; l \<le> Suc n; ja \<noteq> l\<rbrakk> \<Longrightarrow> \<not> v_equiv K (vv ((\<tau>\<^bsub>0 j\<^esub>) ja)) (vv ((\<tau>\<^bsub>0 j\<^esub>) l))
[PROOF STEP]
apply (case_tac "j = 0", simp add:transpos_eq,
        simp add:vals_nonequiv_def,
        cut_tac transpos_inj[of "0" "Suc n" "j"], simp)
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<And>ja l. \<lbrakk>vals_nonequiv K (Suc n) vv; j \<le> Suc n; \<forall>j\<le>Suc n. valuation K (vv j); ja \<le> Suc n; l \<le> Suc n; ja \<noteq> l; 0 < j; inj_on (\<tau>\<^bsub>0 j\<^esub>) {i. i \<le> Suc n}\<rbrakk> \<Longrightarrow> \<not> v_equiv K (vv ((\<tau>\<^bsub>0 j\<^esub>) ja)) (vv ((\<tau>\<^bsub>0 j\<^esub>) l))
 2. \<And>ja l. \<lbrakk>vals_nonequiv K (Suc n) vv; j \<le> Suc n; \<forall>j\<le>Suc n. valuation K (vv j); ja \<le> Suc n; l \<le> Suc n; ja \<noteq> l; j \<noteq> 0\<rbrakk> \<Longrightarrow> 0 \<le> Suc n
 3. \<And>ja l. \<lbrakk>vals_nonequiv K (Suc n) vv; j \<le> Suc n; \<forall>j\<le>Suc n. valuation K (vv j); ja \<le> Suc n; l \<le> Suc n; ja \<noteq> l; j \<noteq> 0\<rbrakk> \<Longrightarrow> j \<le> Suc n
 4. \<And>ja l. \<lbrakk>vals_nonequiv K (Suc n) vv; j \<le> Suc n; \<forall>j\<le>Suc n. valuation K (vv j); ja \<le> Suc n; l \<le> Suc n; ja \<noteq> l; j \<noteq> 0\<rbrakk> \<Longrightarrow> 0 \<noteq> j
[PROOF STEP]
apply (frule_tac x = ja and y = l in injective[of "transpos 0 j"
                       "{j. j \<le> (Suc n)}"], simp, simp, assumption+)
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<And>ja l. \<lbrakk>vals_nonequiv K (Suc n) vv; j \<le> Suc n; \<forall>j\<le>Suc n. valuation K (vv j); ja \<le> Suc n; l \<le> Suc n; ja \<noteq> l; 0 < j; inj_on (\<tau>\<^bsub>0 j\<^esub>) {i. i \<le> Suc n}; (\<tau>\<^bsub>0 j\<^esub>) ja \<noteq> (\<tau>\<^bsub>0 j\<^esub>) l\<rbrakk> \<Longrightarrow> \<not> v_equiv K (vv ((\<tau>\<^bsub>0 j\<^esub>) ja)) (vv ((\<tau>\<^bsub>0 j\<^esub>) l))
 2. \<And>ja l. \<lbrakk>vals_nonequiv K (Suc n) vv; j \<le> Suc n; \<forall>j\<le>Suc n. valuation K (vv j); ja \<le> Suc n; l \<le> Suc n; ja \<noteq> l; j \<noteq> 0\<rbrakk> \<Longrightarrow> 0 \<le> Suc n
 3. \<And>ja l. \<lbrakk>vals_nonequiv K (Suc n) vv; j \<le> Suc n; \<forall>j\<le>Suc n. valuation K (vv j); ja \<le> Suc n; l \<le> Suc n; ja \<noteq> l; j \<noteq> 0\<rbrakk> \<Longrightarrow> j \<le> Suc n
 4. \<And>ja l. \<lbrakk>vals_nonequiv K (Suc n) vv; j \<le> Suc n; \<forall>j\<le>Suc n. valuation K (vv j); ja \<le> Suc n; l \<le> Suc n; ja \<noteq> l; j \<noteq> 0\<rbrakk> \<Longrightarrow> 0 \<noteq> j
[PROOF STEP]
apply (cut_tac l = ja in transpos_mem[of "0" "Suc n" "j"], simp, assumption+,
        simp, assumption,
       cut_tac l = l in transpos_mem[of "0" "Suc n" "j"], simp, assumption+,
        simp, assumption)
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<And>ja l. \<lbrakk>vals_nonequiv K (Suc n) vv; j \<le> Suc n; \<forall>j\<le>Suc n. valuation K (vv j); ja \<le> Suc n; l \<le> Suc n; ja \<noteq> l; 0 < j; inj_on (\<tau>\<^bsub>0 j\<^esub>) {i. i \<le> Suc n}; (\<tau>\<^bsub>0 j\<^esub>) ja \<noteq> (\<tau>\<^bsub>0 j\<^esub>) l; (\<tau>\<^bsub>0 j\<^esub>) ja \<le> Suc n; (\<tau>\<^bsub>0 j\<^esub>) l \<le> Suc n\<rbrakk> \<Longrightarrow> \<not> v_equiv K (vv ((\<tau>\<^bsub>0 j\<^esub>) ja)) (vv ((\<tau>\<^bsub>0 j\<^esub>) l))
 2. \<And>ja l. \<lbrakk>vals_nonequiv K (Suc n) vv; j \<le> Suc n; \<forall>j\<le>Suc n. valuation K (vv j); ja \<le> Suc n; l \<le> Suc n; ja \<noteq> l; j \<noteq> 0\<rbrakk> \<Longrightarrow> 0 \<le> Suc n
 3. \<And>ja l. \<lbrakk>vals_nonequiv K (Suc n) vv; j \<le> Suc n; \<forall>j\<le>Suc n. valuation K (vv j); ja \<le> Suc n; l \<le> Suc n; ja \<noteq> l; j \<noteq> 0\<rbrakk> \<Longrightarrow> j \<le> Suc n
 4. \<And>ja l. \<lbrakk>vals_nonequiv K (Suc n) vv; j \<le> Suc n; \<forall>j\<le>Suc n. valuation K (vv j); ja \<le> Suc n; l \<le> Suc n; ja \<noteq> l; j \<noteq> 0\<rbrakk> \<Longrightarrow> 0 \<noteq> j
[PROOF STEP]
apply (simp add:vals_nonequiv_def,
        simp, assumption, rule not_sym, assumption)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma (in Corps) Ostrowski_base_hom:"vals_nonequiv K (Suc n) vv \<Longrightarrow>
      Ostrowski_base K vv (Suc n) \<in> {h. h \<le> (Suc n)} \<rightarrow> carrier K"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vals_nonequiv K (Suc n) vv \<Longrightarrow> \<Omega>\<^bsub>K vv Suc n\<^esub> \<in> {h. h \<le> Suc n} \<rightarrow> carrier K
[PROOF STEP]
apply (rule Pi_I, rename_tac l,
       simp add:Ostrowski_base_def,
       frule_tac j = l in transpos_vals_nonequiv[of n vv], simp,
       cut_tac Ostrowski[of n])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>l. \<lbrakk>vals_nonequiv K (Suc n) vv; l \<le> Suc n; vals_nonequiv K (Suc n) (vv \<circ> \<tau>\<^bsub>0 l\<^esub>); \<forall>vv. vals_nonequiv K (Suc n) vv \<longrightarrow> (\<exists>x\<in>carrier K. Ostrowski_elem K (Suc n) vv x)\<rbrakk> \<Longrightarrow> (SOME x. x \<in> carrier K \<and> Ostrowski_elem K (Suc n) (vv \<circ> \<tau>\<^bsub>0 l\<^esub>) x) \<in> carrier K
[PROOF STEP]
apply (drule_tac a = "vv \<circ> \<tau>\<^bsub>0 l\<^esub>" in forall_spec, simp,
       rule someI2_ex, blast, simp)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma (in Corps) Ostrowski_base_mem:"vals_nonequiv K (Suc n) vv \<Longrightarrow>
         \<forall>j \<le> (Suc n). Ostrowski_base K vv (Suc n) j \<in> carrier K"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vals_nonequiv K (Suc n) vv \<Longrightarrow> \<forall>j\<le>Suc n. (\<Omega>\<^bsub>K vv Suc n\<^esub>) j \<in> carrier K
[PROOF STEP]
by (rule allI, rule impI,
       frule Ostrowski_base_hom[of "n" "vv"],
       simp add:funcset_mem del:Pi_I')


[STATEMENT]
lemma (in Corps)  Ostrowski_base_mem_1:"\<lbrakk>vals_nonequiv K (Suc n) vv;
       j \<le> (Suc n)\<rbrakk> \<Longrightarrow> Ostrowski_base K vv (Suc n) j \<in> carrier K"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>vals_nonequiv K (Suc n) vv; j \<le> Suc n\<rbrakk> \<Longrightarrow> (\<Omega>\<^bsub>K vv Suc n\<^esub>) j \<in> carrier K
[PROOF STEP]
by (simp add:Ostrowski_base_mem)


[STATEMENT]
lemma (in Corps) Ostrowski_base_nonzero:"\<lbrakk>vals_nonequiv K (Suc n) vv;
       j \<le> Suc n\<rbrakk>  \<Longrightarrow> (\<Omega>\<^bsub>K vv (Suc n)\<^esub>) j \<noteq> \<zero>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>vals_nonequiv K (Suc n) vv; j \<le> Suc n\<rbrakk> \<Longrightarrow> (\<Omega>\<^bsub>K vv Suc n\<^esub>) j \<noteq> \<zero>
[PROOF STEP]
apply (simp add:Ostrowski_base_def,
       frule_tac j = j in transpos_vals_nonequiv[of "n" "vv"],
                      assumption+,
       cut_tac Ostrowski[of "n"],
       drule_tac a = "vv \<circ> \<tau>\<^bsub>0 j\<^esub>" in forall_spec, assumption,
       rule someI2_ex, blast)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>vals_nonequiv K (Suc n) vv; j \<le> Suc n; vals_nonequiv K (Suc n) (vv \<circ> \<tau>\<^bsub>0 j\<^esub>); \<exists>x\<in>carrier K. Ostrowski_elem K (Suc n) (vv \<circ> \<tau>\<^bsub>0 j\<^esub>) x; x \<in> carrier K \<and> Ostrowski_elem K (Suc n) (vv \<circ> \<tau>\<^bsub>0 j\<^esub>) x\<rbrakk> \<Longrightarrow> x \<noteq> \<zero>
[PROOF STEP]
apply (thin_tac "\<exists>x\<in>carrier K. Ostrowski_elem K (Suc n) (vv \<circ> \<tau>\<^bsub>0 j\<^esub>) x",
       erule conjE)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>vals_nonequiv K (Suc n) vv; j \<le> Suc n; vals_nonequiv K (Suc n) (vv \<circ> \<tau>\<^bsub>0 j\<^esub>); x \<in> carrier K; Ostrowski_elem K (Suc n) (vv \<circ> \<tau>\<^bsub>0 j\<^esub>) x\<rbrakk> \<Longrightarrow> x \<noteq> \<zero>
[PROOF STEP]
apply (rule_tac vv = "vv \<circ> \<tau>\<^bsub>0 j\<^esub>" and x = x in Ostrowski_elem_nonzero[of "n"],
       assumption+)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma (in Corps) Ostrowski_base_pos:"\<lbrakk>vals_nonequiv K (Suc n) vv;
      j \<le> Suc n; ja \<le> Suc n; ja \<noteq> j\<rbrakk> \<Longrightarrow> 0 < ((vv j) ((\<Omega>\<^bsub>K vv (Suc n)\<^esub>) ja))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>vals_nonequiv K (Suc n) vv; j \<le> Suc n; ja \<le> Suc n; ja \<noteq> j\<rbrakk> \<Longrightarrow> 0 < vv j ((\<Omega>\<^bsub>K vv Suc n\<^esub>) ja)
[PROOF STEP]
apply (simp add:Ostrowski_base_def,
       frule_tac j = ja in transpos_vals_nonequiv[of "n" "vv"],
       assumption+,
       cut_tac Ostrowski[of "n"],
       drule_tac a = "vv \<circ> \<tau>\<^bsub>0 ja\<^esub>" in forall_spec, assumption+)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>vals_nonequiv K (Suc n) vv; j \<le> Suc n; ja \<le> Suc n; ja \<noteq> j; vals_nonequiv K (Suc n) (vv \<circ> \<tau>\<^bsub>0 ja\<^esub>); \<exists>x\<in>carrier K. Ostrowski_elem K (Suc n) (vv \<circ> \<tau>\<^bsub>0 ja\<^esub>) x\<rbrakk> \<Longrightarrow> 0 < vv j (SOME x. x \<in> carrier K \<and> Ostrowski_elem K (Suc n) (vv \<circ> \<tau>\<^bsub>0 ja\<^esub>) x)
[PROOF STEP]
apply (rule someI2_ex, blast,
       thin_tac "\<exists>x\<in>carrier K. Ostrowski_elem K (Suc n) (vv \<circ> \<tau>\<^bsub>0 ja\<^esub>) x",
       simp add:Ostrowski_elem_def, (erule conjE)+)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>vals_nonequiv K (Suc n) vv; j \<le> Suc n; ja \<le> Suc n; ja \<noteq> j; vals_nonequiv K (Suc n) (vv \<circ> \<tau>\<^bsub>0 ja\<^esub>); x \<in> carrier K; 0 < vv ((\<tau>\<^bsub>0 ja\<^esub>) 0) (1\<^sub>r \<plusminus> -\<^sub>a x); \<forall>j\<in>nset (Suc 0) (Suc n). 0 < vv ((\<tau>\<^bsub>0 ja\<^esub>) j) x\<rbrakk> \<Longrightarrow> 0 < vv j x
[PROOF STEP]
apply (case_tac "ja = 0", simp, cut_tac transpos_eq[of "j"],
       simp add:nset_def, frule Suc_leI[of "0" "j"],
       frule_tac a = j in forall_spec, simp, simp)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>vals_nonequiv K (Suc n) vv; j \<le> Suc n; ja \<le> Suc n; ja \<noteq> j; vals_nonequiv K (Suc n) (vv \<circ> \<tau>\<^bsub>0 ja\<^esub>); x \<in> carrier K; 0 < vv ((\<tau>\<^bsub>0 ja\<^esub>) 0) (1\<^sub>r \<plusminus> -\<^sub>a x); \<forall>j\<in>nset (Suc 0) (Suc n). 0 < vv ((\<tau>\<^bsub>0 ja\<^esub>) j) x; ja \<noteq> 0\<rbrakk> \<Longrightarrow> 0 < vv j x
[PROOF STEP]
apply (case_tac "j = 0", simp,
       frule_tac x = ja in bspec, simp add:nset_def,
       cut_tac  transpos_ij_2[of "0" "Suc n" "ja"], simp, simp+)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>vals_nonequiv K (Suc n) vv; j \<le> Suc n; ja \<le> Suc n; ja \<noteq> j; vals_nonequiv K (Suc n) (vv \<circ> \<tau>\<^bsub>0 ja\<^esub>); x \<in> carrier K; 0 < vv ((\<tau>\<^bsub>0 ja\<^esub>) 0) (1\<^sub>r \<plusminus> -\<^sub>a x); \<forall>j\<in>nset (Suc 0) (Suc n). 0 < vv ((\<tau>\<^bsub>0 ja\<^esub>) j) x; 0 < ja; 0 < j\<rbrakk> \<Longrightarrow> 0 < vv j x
[PROOF STEP]
apply (frule_tac x = j in bspec, simp add:nset_def,
       cut_tac transpos_id[of "0" "Suc n" "ja" "j"], simp+)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma (in Corps) App_base_hom:"\<lbrakk>vals_nonequiv K (Suc n) vv;
      \<forall>j \<le> (Suc n). n_val K (vv j) = vv j\<rbrakk> \<Longrightarrow>
        \<forall>j \<le> (Suc n). App_base K vv (Suc n) j \<in> carrier K"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>vals_nonequiv K (Suc n) vv; \<forall>j\<le>Suc n. n_val K (vv j) = vv j\<rbrakk> \<Longrightarrow> \<forall>j\<le>Suc n. App_base K vv (Suc n) j \<in> carrier K
[PROOF STEP]
apply (rule allI, rule impI,
       rename_tac k,
       subst App_base_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>k. \<lbrakk>vals_nonequiv K (Suc n) vv; \<forall>j\<le>Suc n. n_val K (vv j) = vv j; k \<le> Suc n\<rbrakk> \<Longrightarrow> (\<lambda>j\<in>{h. h \<le> Suc n}. SOME x. x \<in> carrier K \<and> (vv \<circ> \<tau>\<^bsub>0 j\<^esub>) 0 x = 1 \<and> (\<forall>k\<in>nset (Suc 0) (Suc n). (vv \<circ> \<tau>\<^bsub>0 j\<^esub>) k x = 0)) k \<in> carrier K
[PROOF STEP]
apply (case_tac "k = 0", simp, simp add:transpos_eq,
        frule Approximation1_5P[of "n" "vv"], simp,
        rule someI2_ex, blast, simp)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>k. \<lbrakk>vals_nonequiv K (Suc n) vv; \<forall>j\<le>Suc n. n_val K (vv j) = vv j; k \<le> Suc n; k \<noteq> 0\<rbrakk> \<Longrightarrow> (\<lambda>j\<in>{h. h \<le> Suc n}. SOME x. x \<in> carrier K \<and> (vv \<circ> \<tau>\<^bsub>0 j\<^esub>) 0 x = 1 \<and> (\<forall>k\<in>nset (Suc 0) (Suc n). (vv \<circ> \<tau>\<^bsub>0 j\<^esub>) k x = 0)) k \<in> carrier K
[PROOF STEP]
apply (frule_tac j = k in transpos_vals_nonequiv[of "n" "vv"],
                 simp add:nset_def,
        frule_tac vv = "vv \<circ> \<tau>\<^bsub>0 k\<^esub>" in Approximation1_5P[of "n"])
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>k. \<lbrakk>vals_nonequiv K (Suc n) vv; \<forall>j\<le>Suc n. n_val K (vv j) = vv j; k \<le> Suc n; k \<noteq> 0; vals_nonequiv K (Suc n) (vv \<circ> \<tau>\<^bsub>0 k\<^esub>)\<rbrakk> \<Longrightarrow> n_val K ((vv \<circ> \<tau>\<^bsub>0 k\<^esub>) 0) = (vv \<circ> \<tau>\<^bsub>0 k\<^esub>) 0
 2. \<And>k. \<lbrakk>vals_nonequiv K (Suc n) vv; \<forall>j\<le>Suc n. n_val K (vv j) = vv j; k \<le> Suc n; k \<noteq> 0; vals_nonequiv K (Suc n) (vv \<circ> \<tau>\<^bsub>0 k\<^esub>); \<exists>x\<in>carrier K. (vv \<circ> \<tau>\<^bsub>0 k\<^esub>) 0 x = 1 \<and> (\<forall>j\<in>nset (Suc 0) (Suc n). (vv \<circ> \<tau>\<^bsub>0 k\<^esub>) j x = 0)\<rbrakk> \<Longrightarrow> (\<lambda>j\<in>{h. h \<le> Suc n}. SOME x. x \<in> carrier K \<and> (vv \<circ> \<tau>\<^bsub>0 j\<^esub>) 0 x = 1 \<and> (\<forall>k\<in>nset (Suc 0) (Suc n). (vv \<circ> \<tau>\<^bsub>0 j\<^esub>) k x = 0)) k \<in> carrier K
[PROOF STEP]
apply (simp add:cmp_def, subst transpos_ij_1[of "0" "Suc n"], simp+,
        subst transpos_ij_1[of 0 "Suc n" k], simp+)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>k. \<lbrakk>vals_nonequiv K (Suc n) vv; \<forall>j\<le>Suc n. n_val K (vv j) = vv j; k \<le> Suc n; 0 < k; vals_nonequiv K (Suc n) (vv \<circ> \<tau>\<^bsub>0 k\<^esub>); \<exists>x\<in>carrier K. vv ((\<tau>\<^bsub>0 k\<^esub>) 0) x = 1 \<and> (\<forall>j\<in>nset (Suc 0) (Suc n). vv ((\<tau>\<^bsub>0 k\<^esub>) j) x = 0)\<rbrakk> \<Longrightarrow> (SOME x. x \<in> carrier K \<and> vv ((\<tau>\<^bsub>0 k\<^esub>) 0) x = 1 \<and> (\<forall>ka\<in>nset (Suc 0) (Suc n). vv ((\<tau>\<^bsub>0 k\<^esub>) ka) x = 0)) \<in> carrier K
[PROOF STEP]
apply (rule someI2_ex, blast, simp)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma (in Corps) Approzimation1_5P2:"\<lbrakk>vals_nonequiv K (Suc n) vv;
           \<forall>l\<in>{h. h \<le> Suc n}. n_val K (vv l) = vv l; i \<le> Suc n; j \<le> Suc n\<rbrakk>
          \<Longrightarrow> vv i (App_base K vv (Suc n) j) = \<delta>\<^bsub>i j\<^esub> "
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>vals_nonequiv K (Suc n) vv; \<forall>l\<in>{h. h \<le> Suc n}. n_val K (vv l) = vv l; i \<le> Suc n; j \<le> Suc n\<rbrakk> \<Longrightarrow> vv i (App_base K vv (Suc n) j) = \<delta>\<^bsub>i j\<^esub>
[PROOF STEP]
apply (simp add:App_base_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>vals_nonequiv K (Suc n) vv; \<forall>l\<le>Suc n. n_val K (vv l) = vv l; i \<le> Suc n; j \<le> Suc n\<rbrakk> \<Longrightarrow> vv i (SOME x. x \<in> carrier K \<and> vv ((\<tau>\<^bsub>0 j\<^esub>) 0) x = 1 \<and> (\<forall>k\<in>nset (Suc 0) (Suc n). vv ((\<tau>\<^bsub>0 j\<^esub>) k) x = 0)) = \<delta>\<^bsub>i j\<^esub>
[PROOF STEP]
apply (case_tac "j = 0", simp add:transpos_eq,
       rule someI2_ex,
       frule Approximation1_5P[of "n" "vv"], simp , blast,
       simp add:Kronecker_delta_def, rule impI, (erule conjE)+,
       frule_tac x = i in bspec, simp add:nset_def, assumption)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>vals_nonequiv K (Suc n) vv; \<forall>l\<le>Suc n. n_val K (vv l) = vv l; i \<le> Suc n; j \<le> Suc n; j \<noteq> 0\<rbrakk> \<Longrightarrow> vv i (SOME x. x \<in> carrier K \<and> vv ((\<tau>\<^bsub>0 j\<^esub>) 0) x = 1 \<and> (\<forall>k\<in>nset (Suc 0) (Suc n). vv ((\<tau>\<^bsub>0 j\<^esub>) k) x = 0)) = \<delta>\<^bsub>i j\<^esub>
[PROOF STEP]
apply (frule_tac j = j in transpos_vals_nonequiv[of "n" "vv"], simp,
       frule Approximation1_5P[of "n" "vv \<circ> \<tau>\<^bsub>0 j\<^esub>"],
       simp add:cmp_def, simp add:transpos_ij_1[of 0 "Suc n" j])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>vals_nonequiv K (Suc n) vv; \<forall>l\<le>Suc n. n_val K (vv l) = vv l; i \<le> Suc n; j \<le> Suc n; j \<noteq> 0; vals_nonequiv K (Suc n) (vv \<circ> \<tau>\<^bsub>0 j\<^esub>); \<exists>x\<in>carrier K. (vv \<circ> \<tau>\<^bsub>0 j\<^esub>) 0 x = 1 \<and> (\<forall>ja\<in>nset (Suc 0) (Suc n). (vv \<circ> \<tau>\<^bsub>0 j\<^esub>) ja x = 0)\<rbrakk> \<Longrightarrow> vv i (SOME x. x \<in> carrier K \<and> vv ((\<tau>\<^bsub>0 j\<^esub>) 0) x = 1 \<and> (\<forall>k\<in>nset (Suc 0) (Suc n). vv ((\<tau>\<^bsub>0 j\<^esub>) k) x = 0)) = \<delta>\<^bsub>i j\<^esub>
[PROOF STEP]
apply (simp add:cmp_def,
         case_tac "i = 0", simp add:transpos_eq,
         simp add:transpos_ij_1, simp add:Kronecker_delta_def,
         rule someI2_ex, blast,
         thin_tac "\<exists>x\<in>carrier K.
            vv j x = 1 \<and> (\<forall>ja\<in>nset (Suc 0) (Suc n). vv ((\<tau>\<^bsub>0 j\<^esub>) ja) x = 0)",
        (erule conjE)+,
         drule_tac x = j in bspec, simp add:nset_def,
         simp add:transpos_ij_2)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>vals_nonequiv K (Suc n) vv; \<forall>l\<le>Suc n. n_val K (vv l) = vv l; i \<le> Suc n; j \<le> Suc n; 0 < j; vals_nonequiv K (Suc n) (vv \<circ> \<tau>\<^bsub>0 j\<^esub>); \<exists>x\<in>carrier K. vv ((\<tau>\<^bsub>0 j\<^esub>) 0) x = 1 \<and> (\<forall>ja\<in>nset (Suc 0) (Suc n). vv ((\<tau>\<^bsub>0 j\<^esub>) ja) x = 0); i \<noteq> 0\<rbrakk> \<Longrightarrow> vv i (SOME x. x \<in> carrier K \<and> vv ((\<tau>\<^bsub>0 j\<^esub>) 0) x = 1 \<and> (\<forall>k\<in>nset (Suc 0) (Suc n). vv ((\<tau>\<^bsub>0 j\<^esub>) k) x = 0)) = \<delta>\<^bsub>i j\<^esub>
[PROOF STEP]
apply (simp add:Kronecker_delta_def,
       case_tac "i = j", simp add:transpos_ij_1, rule someI2_ex, blast, simp)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>vals_nonequiv K (Suc n) vv; \<forall>l\<le>Suc n. n_val K (vv l) = vv l; i \<le> Suc n; j \<le> Suc n; 0 < j; vals_nonequiv K (Suc n) (vv \<circ> \<tau>\<^bsub>0 j\<^esub>); \<exists>x\<in>carrier K. vv ((\<tau>\<^bsub>0 j\<^esub>) 0) x = 1 \<and> (\<forall>ja\<in>nset (Suc 0) (Suc n). vv ((\<tau>\<^bsub>0 j\<^esub>) ja) x = 0); 0 < i; i \<noteq> j\<rbrakk> \<Longrightarrow> (i = j \<longrightarrow> vv j (SOME x. x \<in> carrier K \<and> vv ((\<tau>\<^bsub>0 j\<^esub>) 0) x = 1 \<and> (\<forall>k\<in>nset (Suc 0) (Suc n). vv ((\<tau>\<^bsub>0 j\<^esub>) k) x = 0)) = 1) \<and> (i \<noteq> j \<longrightarrow> vv i (SOME x. x \<in> carrier K \<and> vv ((\<tau>\<^bsub>0 j\<^esub>) 0) x = 1 \<and> (\<forall>k\<in>nset (Suc 0) (Suc n). vv ((\<tau>\<^bsub>0 j\<^esub>) k) x = 0)) = 0)
[PROOF STEP]
apply (simp, rule someI2_ex, blast,
       thin_tac "\<exists>x\<in>carrier K. vv ((\<tau>\<^bsub>0 j\<^esub>) 0) x = 1 \<and>
                     (\<forall>ja\<in>nset (Suc 0) (Suc n). vv ((\<tau>\<^bsub>0 j\<^esub>) ja) x = 0)",
       (erule conjE)+,
       drule_tac x = i in bspec, simp add:nset_def,
       cut_tac transpos_id[of 0 "Suc n" j i], simp+)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma (in Corps) Approximation1_5:"\<lbrakk>vals_nonequiv K (Suc n) vv;
  \<forall>j \<le> (Suc n). n_val K (vv j) = vv j\<rbrakk> \<Longrightarrow>
  \<exists>x. (\<forall>j \<le> (Suc n). x j \<in> carrier K) \<and> (\<forall>i \<le> (Suc n). \<forall>j \<le> (Suc n).
                              ((vv i)  (x j) = \<delta>\<^bsub>i j\<^esub>))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>vals_nonequiv K (Suc n) vv; \<forall>j\<le>Suc n. n_val K (vv j) = vv j\<rbrakk> \<Longrightarrow> \<exists>x. (\<forall>j\<le>Suc n. x j \<in> carrier K) \<and> (\<forall>i\<le>Suc n. \<forall>j\<le>Suc n. vv i (x j) = \<delta>\<^bsub>i j\<^esub>)
[PROOF STEP]
apply (frule App_base_hom[of n vv], rule allI, simp)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>vals_nonequiv K (Suc n) vv; \<forall>j\<le>Suc n. n_val K (vv j) = vv j; \<forall>j\<le>Suc n. App_base K vv (Suc n) j \<in> carrier K\<rbrakk> \<Longrightarrow> \<exists>x. (\<forall>j\<le>Suc n. x j \<in> carrier K) \<and> (\<forall>i\<le>Suc n. \<forall>j\<le>Suc n. vv i (x j) = \<delta>\<^bsub>i j\<^esub>)
[PROOF STEP]
apply (subgoal_tac "(\<forall>i \<le> (Suc n). \<forall>j \<le> (Suc n).
                 (vv i) ((App_base K vv (Suc n)) j)  = (\<delta>\<^bsub>i j\<^esub>))",
        blast)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>vals_nonequiv K (Suc n) vv; \<forall>j\<le>Suc n. n_val K (vv j) = vv j; \<forall>j\<le>Suc n. App_base K vv (Suc n) j \<in> carrier K\<rbrakk> \<Longrightarrow> \<forall>i\<le>Suc n. \<forall>j\<le>Suc n. vv i (App_base K vv (Suc n) j) = \<delta>\<^bsub>i j\<^esub>
[PROOF STEP]
apply (rule allI, rule impI)+
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>i j. \<lbrakk>vals_nonequiv K (Suc n) vv; \<forall>j\<le>Suc n. n_val K (vv j) = vv j; \<forall>j\<le>Suc n. App_base K vv (Suc n) j \<in> carrier K; i \<le> Suc n; j \<le> Suc n\<rbrakk> \<Longrightarrow> vv i (App_base K vv (Suc n) j) = \<delta>\<^bsub>i j\<^esub>
[PROOF STEP]
apply (rule Approzimation1_5P2, assumption+, simp+)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma (in Corps) Ostrowski_baseTr0:"\<lbrakk>vals_nonequiv K (Suc n) vv; l \<le> (Suc n) \<rbrakk>
   \<Longrightarrow>   0 < ((vv l) (1\<^sub>r \<plusminus> -\<^sub>a (Ostrowski_base K vv (Suc n) l))) \<and>
  (\<forall>m\<in>{h. h \<le> (Suc n)} - {l}. 0 < ((vv m) (Ostrowski_base K vv (Suc n) l)))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>vals_nonequiv K (Suc n) vv; l \<le> Suc n\<rbrakk> \<Longrightarrow> 0 < vv l (1\<^sub>r \<plusminus> -\<^sub>a (\<Omega>\<^bsub>K vv Suc n\<^esub>) l) \<and> (\<forall>m\<in>{h. h \<le> Suc n} - {l}. 0 < vv m ((\<Omega>\<^bsub>K vv Suc n\<^esub>) l))
[PROOF STEP]
apply (simp add:Ostrowski_base_def,
       frule_tac j = l in transpos_vals_nonequiv[of "n" "vv"], assumption,
       cut_tac Ostrowski[of "n"],
       drule_tac a = "vv \<circ> \<tau>\<^bsub>0 l\<^esub>" in forall_spec, assumption)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>vals_nonequiv K (Suc n) vv; l \<le> Suc n; vals_nonequiv K (Suc n) (vv \<circ> \<tau>\<^bsub>0 l\<^esub>); \<exists>x\<in>carrier K. Ostrowski_elem K (Suc n) (vv \<circ> \<tau>\<^bsub>0 l\<^esub>) x\<rbrakk> \<Longrightarrow> 0 < vv l (1\<^sub>r \<plusminus> -\<^sub>a (SOME x. x \<in> carrier K \<and> Ostrowski_elem K (Suc n) (vv \<circ> \<tau>\<^bsub>0 l\<^esub>) x)) \<and> (\<forall>m\<in>{h. h \<le> Suc n} - {l}. 0 < vv m (SOME x. x \<in> carrier K \<and> Ostrowski_elem K (Suc n) (vv \<circ> \<tau>\<^bsub>0 l\<^esub>) x))
[PROOF STEP]
apply (erule bexE,
       unfold Ostrowski_elem_def, frule conjunct1,
       fold Ostrowski_elem_def,
       rule conjI, simp add:Ostrowski_elem_def)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x. \<lbrakk>vals_nonequiv K (Suc n) vv; l \<le> Suc n; vals_nonequiv K (Suc n) (vv \<circ> \<tau>\<^bsub>0 l\<^esub>); x \<in> carrier K; 0 < vv ((\<tau>\<^bsub>0 l\<^esub>) 0) (1\<^sub>r \<plusminus> -\<^sub>a x) \<and> (\<forall>j\<in>nset (Suc 0) (Suc n). 0 < vv ((\<tau>\<^bsub>0 l\<^esub>) j) x)\<rbrakk> \<Longrightarrow> 0 < vv l (1\<^sub>r \<plusminus> -\<^sub>a (SOME x. x \<in> carrier K \<and> 0 < vv ((\<tau>\<^bsub>0 l\<^esub>) 0) (1\<^sub>r \<plusminus> -\<^sub>a x) \<and> (\<forall>j\<in>nset (Suc 0) (Suc n). 0 < vv ((\<tau>\<^bsub>0 l\<^esub>) j) x)))
 2. \<And>x. \<lbrakk>vals_nonequiv K (Suc n) vv; l \<le> Suc n; vals_nonequiv K (Suc n) (vv \<circ> \<tau>\<^bsub>0 l\<^esub>); x \<in> carrier K; Ostrowski_elem K (Suc n) (vv \<circ> \<tau>\<^bsub>0 l\<^esub>) x; 0 < (vv \<circ> \<tau>\<^bsub>0 l\<^esub>) 0 (1\<^sub>r \<plusminus> -\<^sub>a x)\<rbrakk> \<Longrightarrow> \<forall>m\<in>{h. h \<le> Suc n} - {l}. 0 < vv m (SOME x. x \<in> carrier K \<and> Ostrowski_elem K (Suc n) (vv \<circ> \<tau>\<^bsub>0 l\<^esub>) x)
[PROOF STEP]
apply (case_tac "l = 0", simp, simp add:transpos_eq,
       rule someI2_ex, blast, simp,
       simp add:transpos_ij_1,
       rule someI2_ex, blast, simp)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>vals_nonequiv K (Suc n) vv; l \<le> Suc n; vals_nonequiv K (Suc n) (vv \<circ> \<tau>\<^bsub>0 l\<^esub>); x \<in> carrier K; Ostrowski_elem K (Suc n) (vv \<circ> \<tau>\<^bsub>0 l\<^esub>) x; 0 < (vv \<circ> \<tau>\<^bsub>0 l\<^esub>) 0 (1\<^sub>r \<plusminus> -\<^sub>a x)\<rbrakk> \<Longrightarrow> \<forall>m\<in>{h. h \<le> Suc n} - {l}. 0 < vv m (SOME x. x \<in> carrier K \<and> Ostrowski_elem K (Suc n) (vv \<circ> \<tau>\<^bsub>0 l\<^esub>) x)
[PROOF STEP]
apply (simp add:Ostrowski_elem_def,
       case_tac "l = 0", simp, simp add:transpos_eq,
       rule someI2_ex, blast,
       thin_tac "0 < vv 0 (1\<^sub>r \<plusminus> -\<^sub>a x) \<and>
                      (\<forall>j\<in>nset (Suc 0) (Suc n). 0 < vv j x)",
       rule ballI, simp add:nset_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>vals_nonequiv K (Suc n) vv; l \<le> Suc n; vals_nonequiv K (Suc n) (vv \<circ> \<tau>\<^bsub>0 l\<^esub>); x \<in> carrier K; 0 < vv ((\<tau>\<^bsub>0 l\<^esub>) 0) (1\<^sub>r \<plusminus> -\<^sub>a x) \<and> (\<forall>j\<in>nset (Suc 0) (Suc n). 0 < vv ((\<tau>\<^bsub>0 l\<^esub>) j) x); l \<noteq> 0\<rbrakk> \<Longrightarrow> \<forall>m\<in>{h. h \<le> Suc n} - {l}. 0 < vv m (SOME x. x \<in> carrier K \<and> 0 < vv ((\<tau>\<^bsub>0 l\<^esub>) 0) (1\<^sub>r \<plusminus> -\<^sub>a x) \<and> (\<forall>j\<in>nset (Suc 0) (Suc n). 0 < vv ((\<tau>\<^bsub>0 l\<^esub>) j) x))
[PROOF STEP]
apply (rule ballI, erule conjE,
       rule someI2_ex, blast,
       thin_tac "\<forall>j\<in>nset (Suc 0) (Suc n). 0 < vv ((\<tau>\<^bsub>0 l\<^esub>) j) x",
       (erule conjE)+)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x m xa. \<lbrakk>vals_nonequiv K (Suc n) vv; l \<le> Suc n; vals_nonequiv K (Suc n) (vv \<circ> \<tau>\<^bsub>0 l\<^esub>); x \<in> carrier K; l \<noteq> 0; m \<in> {h. h \<le> Suc n} - {l}; 0 < vv ((\<tau>\<^bsub>0 l\<^esub>) 0) (1\<^sub>r \<plusminus> -\<^sub>a x); xa \<in> carrier K; 0 < vv ((\<tau>\<^bsub>0 l\<^esub>) 0) (1\<^sub>r \<plusminus> -\<^sub>a xa); \<forall>j\<in>nset (Suc 0) (Suc n). 0 < vv ((\<tau>\<^bsub>0 l\<^esub>) j) xa\<rbrakk> \<Longrightarrow> 0 < vv m xa
[PROOF STEP]
apply (case_tac "m = 0", simp,
       drule_tac x = l in bspec, simp add:nset_def,
       simp add:transpos_ij_2,
       drule_tac x = m in bspec, simp add:nset_def,
       simp add:transpos_id)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma (in Corps) Ostrowski_baseTr1:"\<lbrakk>vals_nonequiv K (Suc n) vv; l \<le> (Suc n)\<rbrakk>
     \<Longrightarrow> 0 < ((vv l) (1\<^sub>r \<plusminus> -\<^sub>a (Ostrowski_base K vv (Suc n) l)))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>vals_nonequiv K (Suc n) vv; l \<le> Suc n\<rbrakk> \<Longrightarrow> 0 < vv l (1\<^sub>r \<plusminus> -\<^sub>a (\<Omega>\<^bsub>K vv Suc n\<^esub>) l)
[PROOF STEP]
by (simp add:Ostrowski_baseTr0)


[STATEMENT]
lemma (in Corps) Ostrowski_baseTr2:"\<lbrakk>vals_nonequiv K (Suc n) vv;
        l \<le> (Suc n); m \<le> (Suc n); l \<noteq> m\<rbrakk> \<Longrightarrow>
        0 < ((vv m) (Ostrowski_base K vv (Suc n) l))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>vals_nonequiv K (Suc n) vv; l \<le> Suc n; m \<le> Suc n; l \<noteq> m\<rbrakk> \<Longrightarrow> 0 < vv m ((\<Omega>\<^bsub>K vv Suc n\<^esub>) l)
[PROOF STEP]
apply (frule Ostrowski_baseTr0[of "n" "vv" "l"], assumption+)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>vals_nonequiv K (Suc n) vv; l \<le> Suc n; m \<le> Suc n; l \<noteq> m; 0 < vv l (1\<^sub>r \<plusminus> -\<^sub>a (\<Omega>\<^bsub>K vv Suc n\<^esub>) l) \<and> (\<forall>m\<in>{h. h \<le> Suc n} - {l}. 0 < vv m ((\<Omega>\<^bsub>K vv Suc n\<^esub>) l))\<rbrakk> \<Longrightarrow> 0 < vv m ((\<Omega>\<^bsub>K vv Suc n\<^esub>) l)
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma Nset_have_two:"j \<in>{h. h \<le> (Suc n)} \<Longrightarrow> \<exists>m \<in> {h. h \<le> (Suc n)}. j \<noteq> m"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. j \<in> {h. h \<le> Suc n} \<Longrightarrow> \<exists>m\<in>{h. h \<le> Suc n}. j \<noteq> m
[PROOF STEP]
apply (rule contrapos_pp, simp+,
       case_tac "j = Suc n", simp,
       drule_tac a = 0 in forall_spec, simp, arith)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>j \<le> Suc n; \<forall>m\<le>Suc n. j = m; j \<noteq> Suc n\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
apply (drule_tac a = "Suc n" in forall_spec, simp, simp)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma (in Corps) Ostrowski_base_npow_not_one:"\<lbrakk>0 < N; j \<le> Suc n;
       vals_nonequiv K (Suc n) vv\<rbrakk>  \<Longrightarrow>
                              1\<^sub>r \<plusminus> -\<^sub>a ((\<Omega>\<^bsub>K vv (Suc n)\<^esub>) j^\<^bsup>K N\<^esup>) \<noteq> \<zero>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>0 < N; j \<le> Suc n; vals_nonequiv K (Suc n) vv\<rbrakk> \<Longrightarrow> 1\<^sub>r \<plusminus> -\<^sub>a (\<Omega>\<^bsub>K vv Suc n\<^esub>) j^\<^bsup>K N\<^esup> \<noteq> \<zero>
[PROOF STEP]
apply (cut_tac field_is_ring, frule Ring.ring_is_ag[of "K"],
       rule contrapos_pp, simp+,
       frule Ostrowski_base_mem_1[of "n" "vv" "j"], assumption,
       frule Ring.npClose[of "K" "(\<Omega>\<^bsub>K vv (Suc n)\<^esub>) j" "N"], assumption+,
       frule Ring.ring_one[of "K"],
       frule aGroup.ag_mOp_closed[of K "(\<Omega>\<^bsub>K vv (Suc n)\<^esub>) j^\<^bsup>K N\<^esup>"], assumption+,
       frule aGroup.ag_pOp_closed[of "K" "1\<^sub>r" "-\<^sub>a ((\<Omega>\<^bsub>K  vv (Suc n)\<^esub>) j^\<^bsup>K N\<^esup>)"],
       assumption+)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>0 < N; j \<le> Suc n; vals_nonequiv K (Suc n) vv; Ring K; aGroup K; 1\<^sub>r \<plusminus> -\<^sub>a (\<Omega>\<^bsub>K vv Suc n\<^esub>) j^\<^bsup>K N\<^esup> = \<zero>; (\<Omega>\<^bsub>K vv Suc n\<^esub>) j \<in> carrier K; (\<Omega>\<^bsub>K vv Suc n\<^esub>) j^\<^bsup>K N\<^esup> \<in> carrier K; 1\<^sub>r \<in> carrier K; -\<^sub>a (\<Omega>\<^bsub>K vv Suc n\<^esub>) j^\<^bsup>K N\<^esup> \<in> carrier K; 1\<^sub>r \<plusminus> -\<^sub>a (\<Omega>\<^bsub>K vv Suc n\<^esub>) j^\<^bsup>K N\<^esup> \<in> carrier K\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
apply (frule  aGroup.ag_pOp_add_r[of "K" "1\<^sub>r \<plusminus> -\<^sub>a ((\<Omega>\<^bsub>K vv (Suc n)\<^esub>) j^\<^bsup>K N\<^esup>)" "\<zero>"
           "(\<Omega>\<^bsub>K  vv  (Suc n)\<^esub>) j^\<^bsup>K N\<^esup>"], assumption+,
        simp add:aGroup.ag_inc_zero, assumption+,
        thin_tac "1\<^sub>r \<plusminus> -\<^sub>a ((\<Omega>\<^bsub>K vv (Suc n)\<^esub>) j^\<^bsup>K N\<^esup>) = \<zero>")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>0 < N; j \<le> Suc n; vals_nonequiv K (Suc n) vv; Ring K; aGroup K; (\<Omega>\<^bsub>K vv Suc n\<^esub>) j \<in> carrier K; (\<Omega>\<^bsub>K vv Suc n\<^esub>) j^\<^bsup>K N\<^esup> \<in> carrier K; 1\<^sub>r \<in> carrier K; -\<^sub>a (\<Omega>\<^bsub>K vv Suc n\<^esub>) j^\<^bsup>K N\<^esup> \<in> carrier K; 1\<^sub>r \<plusminus> -\<^sub>a (\<Omega>\<^bsub>K vv Suc n\<^esub>) j^\<^bsup>K N\<^esup> \<in> carrier K; 1\<^sub>r \<plusminus> -\<^sub>a (\<Omega>\<^bsub>K vv Suc n\<^esub>) j^\<^bsup>K N\<^esup> \<plusminus> (\<Omega>\<^bsub>K vv Suc n\<^esub>) j^\<^bsup>K N\<^esup> = \<zero> \<plusminus> (\<Omega>\<^bsub>K vv Suc n\<^esub>) j^\<^bsup>K N\<^esup>\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
apply (simp add:aGroup.ag_pOp_assoc[of "K" "1\<^sub>r" "-\<^sub>a ((\<Omega>\<^bsub>K vv (Suc n)\<^esub>) j^\<^bsup>K N\<^esup>)"])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>0 < N; j \<le> Suc n; vals_nonequiv K (Suc n) vv; Ring K; aGroup K; (\<Omega>\<^bsub>K vv Suc n\<^esub>) j \<in> carrier K; (\<Omega>\<^bsub>K vv Suc n\<^esub>) j^\<^bsup>K N\<^esup> \<in> carrier K; 1\<^sub>r \<in> carrier K; -\<^sub>a (\<Omega>\<^bsub>K vv Suc n\<^esub>) j^\<^bsup>K N\<^esup> \<in> carrier K; 1\<^sub>r \<plusminus> -\<^sub>a (\<Omega>\<^bsub>K vv Suc n\<^esub>) j^\<^bsup>K N\<^esup> \<in> carrier K; 1\<^sub>r \<plusminus> (-\<^sub>a (\<Omega>\<^bsub>K vv Suc n\<^esub>) j^\<^bsup>K N\<^esup> \<plusminus> (\<Omega>\<^bsub>K vv Suc n\<^esub>) j^\<^bsup>K N\<^esup>) = \<zero> \<plusminus> (\<Omega>\<^bsub>K vv Suc n\<^esub>) j^\<^bsup>K N\<^esup>\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
apply (simp add:aGroup.ag_l_inv1, simp add:aGroup.ag_r_zero aGroup.ag_l_zero)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>0 < N; j \<le> Suc n; vals_nonequiv K (Suc n) vv; Ring K; aGroup K; (\<Omega>\<^bsub>K vv Suc n\<^esub>) j \<in> carrier K; (\<Omega>\<^bsub>K vv Suc n\<^esub>) j^\<^bsup>K N\<^esup> \<in> carrier K; -\<^sub>a (\<Omega>\<^bsub>K vv Suc n\<^esub>) j^\<^bsup>K N\<^esup> \<in> carrier K; (\<Omega>\<^bsub>K vv Suc n\<^esub>) j^\<^bsup>K N\<^esup> \<plusminus> -\<^sub>a (\<Omega>\<^bsub>K vv Suc n\<^esub>) j^\<^bsup>K N\<^esup> \<in> carrier K; 1\<^sub>r = (\<Omega>\<^bsub>K vv Suc n\<^esub>) j^\<^bsup>K N\<^esup>\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
apply (subgoal_tac "\<forall>m \<le> (Suc n). (j \<noteq> m \<longrightarrow>
                                 0 < (vv m ((\<Omega>\<^bsub>K vv (Suc n)\<^esub>) j)))")
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>0 < N; j \<le> Suc n; vals_nonequiv K (Suc n) vv; Ring K; aGroup K; (\<Omega>\<^bsub>K vv Suc n\<^esub>) j \<in> carrier K; (\<Omega>\<^bsub>K vv Suc n\<^esub>) j^\<^bsup>K N\<^esup> \<in> carrier K; -\<^sub>a (\<Omega>\<^bsub>K vv Suc n\<^esub>) j^\<^bsup>K N\<^esup> \<in> carrier K; (\<Omega>\<^bsub>K vv Suc n\<^esub>) j^\<^bsup>K N\<^esup> \<plusminus> -\<^sub>a (\<Omega>\<^bsub>K vv Suc n\<^esub>) j^\<^bsup>K N\<^esup> \<in> carrier K; 1\<^sub>r = (\<Omega>\<^bsub>K vv Suc n\<^esub>) j^\<^bsup>K N\<^esup>; \<forall>m\<le>Suc n. j \<noteq> m \<longrightarrow> 0 < vv m ((\<Omega>\<^bsub>K vv Suc n\<^esub>) j)\<rbrakk> \<Longrightarrow> False
 2. \<lbrakk>0 < N; j \<le> Suc n; vals_nonequiv K (Suc n) vv; Ring K; aGroup K; (\<Omega>\<^bsub>K vv Suc n\<^esub>) j \<in> carrier K; (\<Omega>\<^bsub>K vv Suc n\<^esub>) j^\<^bsup>K N\<^esup> \<in> carrier K; -\<^sub>a (\<Omega>\<^bsub>K vv Suc n\<^esub>) j^\<^bsup>K N\<^esup> \<in> carrier K; (\<Omega>\<^bsub>K vv Suc n\<^esub>) j^\<^bsup>K N\<^esup> \<plusminus> -\<^sub>a (\<Omega>\<^bsub>K vv Suc n\<^esub>) j^\<^bsup>K N\<^esup> \<in> carrier K; 1\<^sub>r = (\<Omega>\<^bsub>K vv Suc n\<^esub>) j^\<^bsup>K N\<^esup>\<rbrakk> \<Longrightarrow> \<forall>m\<le>Suc n. j \<noteq> m \<longrightarrow> 0 < vv m ((\<Omega>\<^bsub>K vv Suc n\<^esub>) j)
[PROOF STEP]
apply (cut_tac Nset_have_two[of "j" "n"],
        erule bexE, drule_tac a = m in forall_spec, simp,
       thin_tac "(\<Omega>\<^bsub>K vv (Suc n)\<^esub>) j^\<^bsup>K N\<^esup> \<plusminus> -\<^sub>a ((\<Omega>\<^bsub>K vv (Suc n)\<^esub>) j^\<^bsup>K N\<^esup>) \<in> carrier K",
       frule_tac f = "vv m" in eq_elems_eq_val[of "1\<^sub>r" "(\<Omega>\<^bsub>K vv (Suc n)\<^esub>) j^\<^bsup>K N\<^esup>"],
       thin_tac "1\<^sub>r = (\<Omega>\<^bsub>K vv (Suc n)\<^esub>) j^\<^bsup>K N\<^esup>", simp)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>m. \<lbrakk>0 < N; j \<le> Suc n; vals_nonequiv K (Suc n) vv; Ring K; aGroup K; (\<Omega>\<^bsub>K vv Suc n\<^esub>) j \<in> carrier K; (\<Omega>\<^bsub>K vv Suc n\<^esub>) j^\<^bsup>K N\<^esup> \<in> carrier K; -\<^sub>a (\<Omega>\<^bsub>K vv Suc n\<^esub>) j^\<^bsup>K N\<^esup> \<in> carrier K; m \<le> Suc n; j \<noteq> m; 0 < vv m ((\<Omega>\<^bsub>K vv Suc n\<^esub>) j); vv m 1\<^sub>r = vv m ((\<Omega>\<^bsub>K vv Suc n\<^esub>) j^\<^bsup>K N\<^esup>)\<rbrakk> \<Longrightarrow> False
 2. \<lbrakk>0 < N; j \<le> Suc n; vals_nonequiv K (Suc n) vv; Ring K; aGroup K; (\<Omega>\<^bsub>K vv Suc n\<^esub>) j \<in> carrier K; (\<Omega>\<^bsub>K vv Suc n\<^esub>) j^\<^bsup>K N\<^esup> \<in> carrier K; -\<^sub>a (\<Omega>\<^bsub>K vv Suc n\<^esub>) j^\<^bsup>K N\<^esup> \<in> carrier K; (\<Omega>\<^bsub>K vv Suc n\<^esub>) j^\<^bsup>K N\<^esup> \<plusminus> -\<^sub>a (\<Omega>\<^bsub>K vv Suc n\<^esub>) j^\<^bsup>K N\<^esup> \<in> carrier K; 1\<^sub>r = (\<Omega>\<^bsub>K vv Suc n\<^esub>) j^\<^bsup>K N\<^esup>; \<forall>m\<le>Suc n. j \<noteq> m \<longrightarrow> 0 < vv m ((\<Omega>\<^bsub>K vv Suc n\<^esub>) j)\<rbrakk> \<Longrightarrow> j \<in> {h. h \<le> Suc n}
 3. \<lbrakk>0 < N; j \<le> Suc n; vals_nonequiv K (Suc n) vv; Ring K; aGroup K; (\<Omega>\<^bsub>K vv Suc n\<^esub>) j \<in> carrier K; (\<Omega>\<^bsub>K vv Suc n\<^esub>) j^\<^bsup>K N\<^esup> \<in> carrier K; -\<^sub>a (\<Omega>\<^bsub>K vv Suc n\<^esub>) j^\<^bsup>K N\<^esup> \<in> carrier K; (\<Omega>\<^bsub>K vv Suc n\<^esub>) j^\<^bsup>K N\<^esup> \<plusminus> -\<^sub>a (\<Omega>\<^bsub>K vv Suc n\<^esub>) j^\<^bsup>K N\<^esup> \<in> carrier K; 1\<^sub>r = (\<Omega>\<^bsub>K vv Suc n\<^esub>) j^\<^bsup>K N\<^esup>\<rbrakk> \<Longrightarrow> \<forall>m\<le>Suc n. j \<noteq> m \<longrightarrow> 0 < vv m ((\<Omega>\<^bsub>K vv Suc n\<^esub>) j)
[PROOF STEP]
apply (frule_tac m = m in vals_nonequiv_valuation[of "Suc n" "vv"],
        assumption+,
        frule_tac v1 = "vv m" and n1 = N in val_exp_ring[THEN sym,
         of  _ "(\<Omega>\<^bsub>K vv (Suc n)\<^esub>) j"], assumption+,
        simp add:Ostrowski_base_nonzero, simp, simp add:value_of_one)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>m. \<lbrakk>0 < N; j \<le> Suc n; vals_nonequiv K (Suc n) vv; Ring K; aGroup K; (\<Omega>\<^bsub>K vv Suc n\<^esub>) j \<in> carrier K; (\<Omega>\<^bsub>K vv Suc n\<^esub>) j^\<^bsup>K N\<^esup> \<in> carrier K; -\<^sub>a (\<Omega>\<^bsub>K vv Suc n\<^esub>) j^\<^bsup>K N\<^esup> \<in> carrier K; m \<le> Suc n; j \<noteq> m; 0 < vv m ((\<Omega>\<^bsub>K vv Suc n\<^esub>) j); int N *\<^sub>a vv m ((\<Omega>\<^bsub>K vv Suc n\<^esub>) j) = 0; valuation K (vv m); vv m ((\<Omega>\<^bsub>K vv Suc n\<^esub>) j^\<^bsup>K N\<^esup>) = 0\<rbrakk> \<Longrightarrow> False
 2. \<lbrakk>0 < N; j \<le> Suc n; vals_nonequiv K (Suc n) vv; Ring K; aGroup K; (\<Omega>\<^bsub>K vv Suc n\<^esub>) j \<in> carrier K; (\<Omega>\<^bsub>K vv Suc n\<^esub>) j^\<^bsup>K N\<^esup> \<in> carrier K; -\<^sub>a (\<Omega>\<^bsub>K vv Suc n\<^esub>) j^\<^bsup>K N\<^esup> \<in> carrier K; (\<Omega>\<^bsub>K vv Suc n\<^esub>) j^\<^bsup>K N\<^esup> \<plusminus> -\<^sub>a (\<Omega>\<^bsub>K vv Suc n\<^esub>) j^\<^bsup>K N\<^esup> \<in> carrier K; 1\<^sub>r = (\<Omega>\<^bsub>K vv Suc n\<^esub>) j^\<^bsup>K N\<^esup>; \<forall>m\<le>Suc n. j \<noteq> m \<longrightarrow> 0 < vv m ((\<Omega>\<^bsub>K vv Suc n\<^esub>) j)\<rbrakk> \<Longrightarrow> j \<in> {h. h \<le> Suc n}
 3. \<lbrakk>0 < N; j \<le> Suc n; vals_nonequiv K (Suc n) vv; Ring K; aGroup K; (\<Omega>\<^bsub>K vv Suc n\<^esub>) j \<in> carrier K; (\<Omega>\<^bsub>K vv Suc n\<^esub>) j^\<^bsup>K N\<^esup> \<in> carrier K; -\<^sub>a (\<Omega>\<^bsub>K vv Suc n\<^esub>) j^\<^bsup>K N\<^esup> \<in> carrier K; (\<Omega>\<^bsub>K vv Suc n\<^esub>) j^\<^bsup>K N\<^esup> \<plusminus> -\<^sub>a (\<Omega>\<^bsub>K vv Suc n\<^esub>) j^\<^bsup>K N\<^esup> \<in> carrier K; 1\<^sub>r = (\<Omega>\<^bsub>K vv Suc n\<^esub>) j^\<^bsup>K N\<^esup>\<rbrakk> \<Longrightarrow> \<forall>m\<le>Suc n. j \<noteq> m \<longrightarrow> 0 < vv m ((\<Omega>\<^bsub>K vv Suc n\<^esub>) j)
[PROOF STEP]
apply (subgoal_tac "int N \<noteq> 0",
        frule_tac x = "vv m ((\<Omega>\<^bsub>K vv (Suc n)\<^esub>) j)" in asprod_0[of "int N"],
        assumption, simp add:less_ant_def, simp, simp,
        rule allI, rule impI, rule impI,
        rule Ostrowski_baseTr2, assumption+)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma (in Ring) expansion_of_sum1:"x \<in> carrier R \<Longrightarrow>
                (1\<^sub>r \<plusminus> x)^\<^bsup>R n\<^esup> = nsum R (\<lambda>i. \<^bsub>n\<^esub>C\<^bsub>i\<^esub> \<times>\<^bsub>R\<^esub> x^\<^bsup>R i\<^esup>) n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x \<in> carrier R \<Longrightarrow> (1\<^sub>r \<plusminus> x)^\<^bsup>R n\<^esup> = \<Sigma>\<^sub>e R (\<lambda>i.  \<^bsub>n\<^esub>C\<^bsub>i\<^esub> \<times>\<^bsub>R\<^esub> x^\<^bsup>R i\<^esup>) n
[PROOF STEP]
apply (cut_tac ring_one, frule npeSum2[of "1\<^sub>r" "x" "n"], assumption+,
       simp add:npOne, subgoal_tac "\<forall>(j::nat). (x^\<^bsup>R j\<^esup>) \<in> carrier R")
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>x \<in> carrier R; 1\<^sub>r \<in> carrier R; (1\<^sub>r \<plusminus> x)^\<^bsup>R n\<^esup> = \<Sigma>\<^sub>e R (\<lambda>i.  \<^bsub>n\<^esub>C\<^bsub>i\<^esub> \<times>\<^bsub>R\<^esub> (1\<^sub>r \<cdot>\<^sub>r x^\<^bsup>R i\<^esup>)) n; \<forall>j. x^\<^bsup>R j\<^esup> \<in> carrier R\<rbrakk> \<Longrightarrow> \<Sigma>\<^sub>e R (\<lambda>i.  \<^bsub>n\<^esub>C\<^bsub>i\<^esub> \<times>\<^bsub>R\<^esub> (1\<^sub>r \<cdot>\<^sub>r x^\<^bsup>R i\<^esup>)) n = \<Sigma>\<^sub>e R (\<lambda>i.  \<^bsub>n\<^esub>C\<^bsub>i\<^esub> \<times>\<^bsub>R\<^esub> x^\<^bsup>R i\<^esup>) n
 2. \<lbrakk>x \<in> carrier R; 1\<^sub>r \<in> carrier R; (1\<^sub>r \<plusminus> x)^\<^bsup>R n\<^esup> = \<Sigma>\<^sub>e R (\<lambda>i.  \<^bsub>n\<^esub>C\<^bsub>i\<^esub> \<times>\<^bsub>R\<^esub> (1\<^sub>r \<cdot>\<^sub>r x^\<^bsup>R i\<^esup>)) n\<rbrakk> \<Longrightarrow> \<forall>j. x^\<^bsup>R j\<^esup> \<in> carrier R
[PROOF STEP]
apply (simp add:ring_l_one, rule allI, simp add:npClose)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma (in Ring) tail_of_expansion:"x \<in> carrier R \<Longrightarrow> (1\<^sub>r \<plusminus> x)^\<^bsup>R (Suc n)\<^esup> =
             (nsum R (\<lambda> i. (\<^bsub>(Suc n)\<^esub>C\<^bsub>(Suc i)\<^esub> \<times>\<^bsub>R\<^esub> x^\<^bsup>R (Suc i)\<^esup>)) n) \<plusminus> 1\<^sub>r"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x \<in> carrier R \<Longrightarrow> (1\<^sub>r \<plusminus> x)^\<^bsup>R Suc n\<^esup> = \<Sigma>\<^sub>e R (\<lambda>i.  \<^bsub>Suc n\<^esub>C\<^bsub>Suc i\<^esub> \<times>\<^bsub>R\<^esub> x^\<^bsup>R Suc i\<^esup>) n \<plusminus> 1\<^sub>r
[PROOF STEP]
apply (cut_tac ring_is_ag)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>x \<in> carrier R; aGroup R\<rbrakk> \<Longrightarrow> (1\<^sub>r \<plusminus> x)^\<^bsup>R Suc n\<^esup> = \<Sigma>\<^sub>e R (\<lambda>i.  \<^bsub>Suc n\<^esub>C\<^bsub>Suc i\<^esub> \<times>\<^bsub>R\<^esub> x^\<^bsup>R Suc i\<^esup>) n \<plusminus> 1\<^sub>r
[PROOF STEP]
apply (frule expansion_of_sum1[of "x" "Suc n"],
       simp del:nsum_suc binomial_Suc_Suc npow_suc,
       thin_tac "(1\<^sub>r \<plusminus> x)^\<^bsup>R (Suc n)\<^esup> = \<Sigma>\<^sub>e R (\<lambda>i. \<^bsub>(Suc n)\<^esub>C\<^bsub>i\<^esub> \<times>\<^bsub>R\<^esub> x^\<^bsup>R i\<^esup>) (Suc n)")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>x \<in> carrier R; aGroup R\<rbrakk> \<Longrightarrow> \<Sigma>\<^sub>e R (\<lambda>i.  \<^bsub>Suc n\<^esub>C\<^bsub>i\<^esub> \<times>\<^bsub>R\<^esub> x^\<^bsup>R i\<^esup>) Suc n = \<Sigma>\<^sub>e R (\<lambda>i.  \<^bsub>Suc n\<^esub>C\<^bsub>Suc i\<^esub> \<times>\<^bsub>R\<^esub> x^\<^bsup>R Suc i\<^esup>) n \<plusminus> 1\<^sub>r
[PROOF STEP]
apply (subst aGroup.nsumTail[of R n "\<lambda>i. \<^bsub>(Suc n)\<^esub>C\<^bsub>i\<^esub> \<times>\<^bsub>R\<^esub> x^\<^bsup>R i\<^esup>"], assumption,
       rule allI, rule impI, rule nsClose, rule npClose, assumption)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>x \<in> carrier R; aGroup R\<rbrakk> \<Longrightarrow> \<Sigma>\<^sub>e R (\<lambda>i.  \<^bsub>Suc n\<^esub>C\<^bsub>Suc i\<^esub> \<times>\<^bsub>R\<^esub> x^\<^bsup>R Suc i\<^esup>) n \<plusminus>  \<^bsub>Suc n\<^esub>C\<^bsub>0\<^esub> \<times>\<^bsub>R\<^esub> x^\<^bsup>R 0\<^esup> = \<Sigma>\<^sub>e R (\<lambda>i.  \<^bsub>Suc n\<^esub>C\<^bsub>Suc i\<^esub> \<times>\<^bsub>R\<^esub> x^\<^bsup>R Suc i\<^esup>) n \<plusminus> 1\<^sub>r
[PROOF STEP]
apply (cut_tac ring_one,
       simp del:nsum_suc binomial_Suc_Suc npow_suc add:aGroup.ag_l_zero)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma (in Ring) tail_of_expansion1:"x \<in> carrier R \<Longrightarrow>
  (1\<^sub>r \<plusminus> x)^\<^bsup>R (Suc n)\<^esup>  = x \<cdot>\<^sub>r (nsum R (\<lambda> i. (\<^bsub>(Suc n)\<^esub>C\<^bsub>(Suc i)\<^esub> \<times>\<^bsub>R\<^esub> x^\<^bsup>R i\<^esup>)) n) \<plusminus> 1\<^sub>r"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x \<in> carrier R \<Longrightarrow> (1\<^sub>r \<plusminus> x)^\<^bsup>R Suc n\<^esup> = x \<cdot>\<^sub>r \<Sigma>\<^sub>e R (\<lambda>i.  \<^bsub>Suc n\<^esub>C\<^bsub>Suc i\<^esub> \<times>\<^bsub>R\<^esub> x^\<^bsup>R i\<^esup>) n \<plusminus> 1\<^sub>r
[PROOF STEP]
apply (frule tail_of_expansion[of "x" "n"],
       simp del:nsum_suc binomial_Suc_Suc npow_suc,
       subgoal_tac "\<forall>i.  \<^bsub>Suc n\<^esub>C\<^bsub>Suc i\<^esub> \<times>\<^bsub>R\<^esub> x^\<^bsup>R i\<^esup> \<in> carrier R",
       cut_tac ring_one, cut_tac ring_is_ag)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>x \<in> carrier R; (1\<^sub>r \<plusminus> x)^\<^bsup>R Suc n\<^esup> = \<Sigma>\<^sub>e R (\<lambda>i.  \<^bsub>Suc n\<^esub>C\<^bsub>Suc i\<^esub> \<times>\<^bsub>R\<^esub> x^\<^bsup>R Suc i\<^esup>) n \<plusminus> 1\<^sub>r; \<forall>i.  \<^bsub>Suc n\<^esub>C\<^bsub>Suc i\<^esub> \<times>\<^bsub>R\<^esub> x^\<^bsup>R i\<^esup> \<in> carrier R; 1\<^sub>r \<in> carrier R; aGroup R\<rbrakk> \<Longrightarrow> \<Sigma>\<^sub>e R (\<lambda>i.  \<^bsub>Suc n\<^esub>C\<^bsub>Suc i\<^esub> \<times>\<^bsub>R\<^esub> x^\<^bsup>R Suc i\<^esup>) n \<plusminus> 1\<^sub>r = x \<cdot>\<^sub>r \<Sigma>\<^sub>e R (\<lambda>i.  \<^bsub>Suc n\<^esub>C\<^bsub>Suc i\<^esub> \<times>\<^bsub>R\<^esub> x^\<^bsup>R i\<^esup>) n \<plusminus> 1\<^sub>r
 2. \<lbrakk>x \<in> carrier R; (1\<^sub>r \<plusminus> x)^\<^bsup>R Suc n\<^esup> = \<Sigma>\<^sub>e R (\<lambda>i.  \<^bsub>Suc n\<^esub>C\<^bsub>Suc i\<^esub> \<times>\<^bsub>R\<^esub> x^\<^bsup>R Suc i\<^esup>) n \<plusminus> 1\<^sub>r\<rbrakk> \<Longrightarrow> \<forall>i.  \<^bsub>Suc n\<^esub>C\<^bsub>Suc i\<^esub> \<times>\<^bsub>R\<^esub> x^\<^bsup>R i\<^esup> \<in> carrier R
[PROOF STEP]
prefer 2
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>x \<in> carrier R; (1\<^sub>r \<plusminus> x)^\<^bsup>R Suc n\<^esup> = \<Sigma>\<^sub>e R (\<lambda>i.  \<^bsub>Suc n\<^esub>C\<^bsub>Suc i\<^esub> \<times>\<^bsub>R\<^esub> x^\<^bsup>R Suc i\<^esup>) n \<plusminus> 1\<^sub>r\<rbrakk> \<Longrightarrow> \<forall>i.  \<^bsub>Suc n\<^esub>C\<^bsub>Suc i\<^esub> \<times>\<^bsub>R\<^esub> x^\<^bsup>R i\<^esup> \<in> carrier R
 2. \<lbrakk>x \<in> carrier R; (1\<^sub>r \<plusminus> x)^\<^bsup>R Suc n\<^esup> = \<Sigma>\<^sub>e R (\<lambda>i.  \<^bsub>Suc n\<^esub>C\<^bsub>Suc i\<^esub> \<times>\<^bsub>R\<^esub> x^\<^bsup>R Suc i\<^esup>) n \<plusminus> 1\<^sub>r; \<forall>i.  \<^bsub>Suc n\<^esub>C\<^bsub>Suc i\<^esub> \<times>\<^bsub>R\<^esub> x^\<^bsup>R i\<^esup> \<in> carrier R; 1\<^sub>r \<in> carrier R; aGroup R\<rbrakk> \<Longrightarrow> \<Sigma>\<^sub>e R (\<lambda>i.  \<^bsub>Suc n\<^esub>C\<^bsub>Suc i\<^esub> \<times>\<^bsub>R\<^esub> x^\<^bsup>R Suc i\<^esup>) n \<plusminus> 1\<^sub>r = x \<cdot>\<^sub>r \<Sigma>\<^sub>e R (\<lambda>i.  \<^bsub>Suc n\<^esub>C\<^bsub>Suc i\<^esub> \<times>\<^bsub>R\<^esub> x^\<^bsup>R i\<^esup>) n \<plusminus> 1\<^sub>r
[PROOF STEP]
apply(simp add: nsClose npClose)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>x \<in> carrier R; (1\<^sub>r \<plusminus> x)^\<^bsup>R Suc n\<^esup> = \<Sigma>\<^sub>e R (\<lambda>i.  \<^bsub>Suc n\<^esub>C\<^bsub>Suc i\<^esub> \<times>\<^bsub>R\<^esub> x^\<^bsup>R Suc i\<^esup>) n \<plusminus> 1\<^sub>r; \<forall>i.  \<^bsub>Suc n\<^esub>C\<^bsub>Suc i\<^esub> \<times>\<^bsub>R\<^esub> x^\<^bsup>R i\<^esup> \<in> carrier R; 1\<^sub>r \<in> carrier R; aGroup R\<rbrakk> \<Longrightarrow> \<Sigma>\<^sub>e R (\<lambda>i.  \<^bsub>Suc n\<^esub>C\<^bsub>Suc i\<^esub> \<times>\<^bsub>R\<^esub> x^\<^bsup>R Suc i\<^esup>) n \<plusminus> 1\<^sub>r = x \<cdot>\<^sub>r \<Sigma>\<^sub>e R (\<lambda>i.  \<^bsub>Suc n\<^esub>C\<^bsub>Suc i\<^esub> \<times>\<^bsub>R\<^esub> x^\<^bsup>R i\<^esup>) n \<plusminus> 1\<^sub>r
[PROOF STEP]
apply (rule aGroup.ag_pOp_add_r[of "R" _ _ "1\<^sub>r"], assumption+,
       rule aGroup.nsum_mem, assumption+, rule allI, rule impI,
       rule nsClose, rule npClose, assumption)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<lbrakk>x \<in> carrier R; (1\<^sub>r \<plusminus> x)^\<^bsup>R Suc n\<^esup> = \<Sigma>\<^sub>e R (\<lambda>i.  \<^bsub>Suc n\<^esub>C\<^bsub>Suc i\<^esub> \<times>\<^bsub>R\<^esub> x^\<^bsup>R Suc i\<^esup>) n \<plusminus> 1\<^sub>r; \<forall>i.  \<^bsub>Suc n\<^esub>C\<^bsub>Suc i\<^esub> \<times>\<^bsub>R\<^esub> x^\<^bsup>R i\<^esup> \<in> carrier R; 1\<^sub>r \<in> carrier R; aGroup R\<rbrakk> \<Longrightarrow> x \<cdot>\<^sub>r \<Sigma>\<^sub>e R (\<lambda>i.  \<^bsub>Suc n\<^esub>C\<^bsub>Suc i\<^esub> \<times>\<^bsub>R\<^esub> x^\<^bsup>R i\<^esup>) n \<in> carrier R
 2. \<lbrakk>x \<in> carrier R; (1\<^sub>r \<plusminus> x)^\<^bsup>R Suc n\<^esup> = \<Sigma>\<^sub>e R (\<lambda>i.  \<^bsub>Suc n\<^esub>C\<^bsub>Suc i\<^esub> \<times>\<^bsub>R\<^esub> x^\<^bsup>R Suc i\<^esup>) n \<plusminus> 1\<^sub>r; \<forall>i.  \<^bsub>Suc n\<^esub>C\<^bsub>Suc i\<^esub> \<times>\<^bsub>R\<^esub> x^\<^bsup>R i\<^esup> \<in> carrier R; 1\<^sub>r \<in> carrier R; aGroup R\<rbrakk> \<Longrightarrow> 1\<^sub>r \<in> carrier R
 3. \<lbrakk>x \<in> carrier R; (1\<^sub>r \<plusminus> x)^\<^bsup>R Suc n\<^esup> = \<Sigma>\<^sub>e R (\<lambda>i.  \<^bsub>Suc n\<^esub>C\<^bsub>Suc i\<^esub> \<times>\<^bsub>R\<^esub> x^\<^bsup>R Suc i\<^esup>) n \<plusminus> 1\<^sub>r; \<forall>i.  \<^bsub>Suc n\<^esub>C\<^bsub>Suc i\<^esub> \<times>\<^bsub>R\<^esub> x^\<^bsup>R i\<^esup> \<in> carrier R; 1\<^sub>r \<in> carrier R; aGroup R\<rbrakk> \<Longrightarrow> \<Sigma>\<^sub>e R (\<lambda>i.  \<^bsub>Suc n\<^esub>C\<^bsub>Suc i\<^esub> \<times>\<^bsub>R\<^esub> x^\<^bsup>R Suc i\<^esup>) n = x \<cdot>\<^sub>r \<Sigma>\<^sub>e R (\<lambda>i.  \<^bsub>Suc n\<^esub>C\<^bsub>Suc i\<^esub> \<times>\<^bsub>R\<^esub> x^\<^bsup>R i\<^esup>) n
[PROOF STEP]
apply (rule ring_tOp_closed, assumption+,
       rule aGroup.nsum_mem, assumption+, blast, simp add:ring_one)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>x \<in> carrier R; (1\<^sub>r \<plusminus> x)^\<^bsup>R Suc n\<^esup> = \<Sigma>\<^sub>e R (\<lambda>i.  \<^bsub>Suc n\<^esub>C\<^bsub>Suc i\<^esub> \<times>\<^bsub>R\<^esub> x^\<^bsup>R Suc i\<^esup>) n \<plusminus> 1\<^sub>r; \<forall>i.  \<^bsub>Suc n\<^esub>C\<^bsub>Suc i\<^esub> \<times>\<^bsub>R\<^esub> x^\<^bsup>R i\<^esup> \<in> carrier R; 1\<^sub>r \<in> carrier R; aGroup R\<rbrakk> \<Longrightarrow> \<Sigma>\<^sub>e R (\<lambda>i.  \<^bsub>Suc n\<^esub>C\<^bsub>Suc i\<^esub> \<times>\<^bsub>R\<^esub> x^\<^bsup>R Suc i\<^esup>) n = x \<cdot>\<^sub>r \<Sigma>\<^sub>e R (\<lambda>i.  \<^bsub>Suc n\<^esub>C\<^bsub>Suc i\<^esub> \<times>\<^bsub>R\<^esub> x^\<^bsup>R i\<^esup>) n
[PROOF STEP]
apply (subst nsumMulEleL[of "\<lambda>i. \<^bsub>Suc n\<^esub>C\<^bsub>Suc i\<^esub> \<times>\<^bsub>R\<^esub> x^\<^bsup>R i\<^esup>" "x"], assumption+)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>x \<in> carrier R; (1\<^sub>r \<plusminus> x)^\<^bsup>R Suc n\<^esup> = \<Sigma>\<^sub>e R (\<lambda>i.  \<^bsub>Suc n\<^esub>C\<^bsub>Suc i\<^esub> \<times>\<^bsub>R\<^esub> x^\<^bsup>R Suc i\<^esup>) n \<plusminus> 1\<^sub>r; \<forall>i.  \<^bsub>Suc n\<^esub>C\<^bsub>Suc i\<^esub> \<times>\<^bsub>R\<^esub> x^\<^bsup>R i\<^esup> \<in> carrier R; 1\<^sub>r \<in> carrier R; aGroup R\<rbrakk> \<Longrightarrow> \<Sigma>\<^sub>e R (\<lambda>i.  \<^bsub>Suc n\<^esub>C\<^bsub>Suc i\<^esub> \<times>\<^bsub>R\<^esub> x^\<^bsup>R Suc i\<^esup>) n = \<Sigma>\<^sub>e R (\<lambda>i. x \<cdot>\<^sub>r  \<^bsub>Suc n\<^esub>C\<^bsub>Suc i\<^esub> \<times>\<^bsub>R\<^esub> x^\<^bsup>R i\<^esup>) n
[PROOF STEP]
apply (rule aGroup.nsum_eq, assumption, rule allI, rule impI, rule nsClose,
       rule npClose, assumption, rule allI, rule impI,
       rule ring_tOp_closed, assumption+, rule nsClose, rule npClose,
       assumption)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>x \<in> carrier R; (1\<^sub>r \<plusminus> x)^\<^bsup>R Suc n\<^esup> = \<Sigma>\<^sub>e R (\<lambda>i.  \<^bsub>Suc n\<^esub>C\<^bsub>Suc i\<^esub> \<times>\<^bsub>R\<^esub> x^\<^bsup>R Suc i\<^esup>) n \<plusminus> 1\<^sub>r; \<forall>i.  \<^bsub>Suc n\<^esub>C\<^bsub>Suc i\<^esub> \<times>\<^bsub>R\<^esub> x^\<^bsup>R i\<^esup> \<in> carrier R; 1\<^sub>r \<in> carrier R; aGroup R\<rbrakk> \<Longrightarrow> \<forall>j\<le>n.  \<^bsub>Suc n\<^esub>C\<^bsub>Suc j\<^esub> \<times>\<^bsub>R\<^esub> x^\<^bsup>R Suc j\<^esup> = x \<cdot>\<^sub>r  \<^bsub>Suc n\<^esub>C\<^bsub>Suc j\<^esub> \<times>\<^bsub>R\<^esub> x^\<^bsup>R j\<^esup>
[PROOF STEP]
apply (rule allI, rule impI)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>j. \<lbrakk>x \<in> carrier R; (1\<^sub>r \<plusminus> x)^\<^bsup>R Suc n\<^esup> = \<Sigma>\<^sub>e R (\<lambda>i.  \<^bsub>Suc n\<^esub>C\<^bsub>Suc i\<^esub> \<times>\<^bsub>R\<^esub> x^\<^bsup>R Suc i\<^esup>) n \<plusminus> 1\<^sub>r; \<forall>i.  \<^bsub>Suc n\<^esub>C\<^bsub>Suc i\<^esub> \<times>\<^bsub>R\<^esub> x^\<^bsup>R i\<^esup> \<in> carrier R; 1\<^sub>r \<in> carrier R; aGroup R; j \<le> n\<rbrakk> \<Longrightarrow>  \<^bsub>Suc n\<^esub>C\<^bsub>Suc j\<^esub> \<times>\<^bsub>R\<^esub> x^\<^bsup>R Suc j\<^esup> = x \<cdot>\<^sub>r  \<^bsub>Suc n\<^esub>C\<^bsub>Suc j\<^esub> \<times>\<^bsub>R\<^esub> x^\<^bsup>R j\<^esup>
[PROOF STEP]
apply (subst nsMulDistrL, assumption, simp add:npClose,
       frule_tac n = j in npClose[of x], simp add:ring_tOp_commute[of x])
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma (in Corps) nsum_in_VrTr:"valuation K v \<Longrightarrow>
       (\<forall>j \<le> n. f j \<in> carrier K) \<and> (\<forall>j \<le> n.
       0 \<le> (v (f j))) \<longrightarrow> (nsum K f n) \<in> carrier (Vr K v)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. valuation K v \<Longrightarrow> (\<forall>j\<le>n. f j \<in> carrier K) \<and> (\<forall>j\<le>n. 0 \<le> v (f j)) \<longrightarrow> \<Sigma>\<^sub>e K f n \<in> carrier (Vr K v)
[PROOF STEP]
apply (induct_tac n)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. valuation K v \<Longrightarrow> (\<forall>j\<le>0. f j \<in> carrier K) \<and> (\<forall>j\<le>0. 0 \<le> v (f j)) \<longrightarrow> \<Sigma>\<^sub>e K f 0 \<in> carrier (Vr K v)
 2. \<And>n. \<lbrakk>valuation K v; (\<forall>j\<le>n. f j \<in> carrier K) \<and> (\<forall>j\<le>n. 0 \<le> v (f j)) \<longrightarrow> \<Sigma>\<^sub>e K f n \<in> carrier (Vr K v)\<rbrakk> \<Longrightarrow> (\<forall>j\<le>Suc n. f j \<in> carrier K) \<and> (\<forall>j\<le>Suc n. 0 \<le> v (f j)) \<longrightarrow> \<Sigma>\<^sub>e K f Suc n \<in> carrier (Vr K v)
[PROOF STEP]
apply (rule impI, erule conjE, simp add:val_pos_mem_Vr)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>n. \<lbrakk>valuation K v; (\<forall>j\<le>n. f j \<in> carrier K) \<and> (\<forall>j\<le>n. 0 \<le> v (f j)) \<longrightarrow> \<Sigma>\<^sub>e K f n \<in> carrier (Vr K v)\<rbrakk> \<Longrightarrow> (\<forall>j\<le>Suc n. f j \<in> carrier K) \<and> (\<forall>j\<le>Suc n. 0 \<le> v (f j)) \<longrightarrow> \<Sigma>\<^sub>e K f Suc n \<in> carrier (Vr K v)
[PROOF STEP]
apply (rule impI, erule conjE)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>n. \<lbrakk>valuation K v; (\<forall>j\<le>n. f j \<in> carrier K) \<and> (\<forall>j\<le>n. 0 \<le> v (f j)) \<longrightarrow> \<Sigma>\<^sub>e K f n \<in> carrier (Vr K v); \<forall>j\<le>Suc n. f j \<in> carrier K; \<forall>j\<le>Suc n. 0 \<le> v (f j)\<rbrakk> \<Longrightarrow> \<Sigma>\<^sub>e K f Suc n \<in> carrier (Vr K v)
[PROOF STEP]
apply (frule Vr_ring[of v], frule Ring.ring_is_ag[of "Vr K v"],
       frule_tac  x = "f (Suc n)" and y = "nsum K f n" in
         aGroup.ag_pOp_closed[of "Vr K v"],
       subst val_pos_mem_Vr[THEN sym, of  "v"], assumption+,
       simp, simp, simp)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>n. \<lbrakk>valuation K v; (\<forall>j\<le>n. f j \<in> carrier K) \<and> (\<forall>j\<le>n. 0 \<le> v (f j)) \<longrightarrow> \<Sigma>\<^sub>e K f n \<in> carrier (Vr K v); \<forall>j\<le>Suc n. f j \<in> carrier K; \<forall>j\<le>Suc n. 0 \<le> v (f j); Ring (Vr K v); aGroup (Vr K v); f (Suc n) \<plusminus>\<^bsub>Vr K v\<^esub> \<Sigma>\<^sub>e K f n \<in> carrier (Vr K v)\<rbrakk> \<Longrightarrow> \<Sigma>\<^sub>e K f Suc n \<in> carrier (Vr K v)
[PROOF STEP]
apply (simp, subst Vr_pOp_f_pOp[of "v", THEN sym], assumption+,
       subst val_pos_mem_Vr[THEN sym, of v], assumption+,
       simp+)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>n. \<lbrakk>valuation K v; \<Sigma>\<^sub>e K f n \<in> carrier (Vr K v); \<forall>j\<le>Suc n. f j \<in> carrier K; \<forall>j\<le>Suc n. 0 \<le> v (f j); Ring (Vr K v); aGroup (Vr K v); f (Suc n) \<plusminus>\<^bsub>Vr K v\<^esub> \<Sigma>\<^sub>e K f n \<in> carrier (Vr K v)\<rbrakk> \<Longrightarrow> \<Sigma>\<^sub>e K f n \<plusminus>\<^bsub>Vr K v\<^esub> f (Suc n) \<in> carrier (Vr K v)
[PROOF STEP]
apply (subst aGroup.ag_pOp_commute, assumption+, simp add:val_pos_mem_Vr,
       assumption)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma (in Corps) nsum_in_Vr:"\<lbrakk>valuation K v; \<forall>j \<le> n. f j \<in> carrier K;
       \<forall>j \<le> n.  0 \<le> (v (f j))\<rbrakk> \<Longrightarrow> (nsum K f n) \<in> carrier (Vr K v)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>valuation K v; \<forall>j\<le>n. f j \<in> carrier K; \<forall>j\<le>n. 0 \<le> v (f j)\<rbrakk> \<Longrightarrow> \<Sigma>\<^sub>e K f n \<in> carrier (Vr K v)
[PROOF STEP]
apply (simp add:nsum_in_VrTr)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma (in Corps) nsum_mem_in_Vr:"\<lbrakk>valuation K v;
       \<forall>j \<le> n. (f j) \<in> carrier K; \<forall>j \<le> n. 0 \<le> (v (f j))\<rbrakk> \<Longrightarrow>
         (nsum K f n) \<in> carrier (Vr K v)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>valuation K v; \<forall>j\<le>n. f j \<in> carrier K; \<forall>j\<le>n. 0 \<le> v (f j)\<rbrakk> \<Longrightarrow> \<Sigma>\<^sub>e K f n \<in> carrier (Vr K v)
[PROOF STEP]
by (rule nsum_in_Vr)


[STATEMENT]
lemma (in Corps) val_nscal_ge_selfTr:"\<lbrakk>valuation K v; x \<in> carrier K; 0 \<le> v x\<rbrakk>
       \<Longrightarrow>  v x \<le>  v (n \<times>\<^bsub>K\<^esub> x)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>valuation K v; x \<in> carrier K; 0 \<le> v x\<rbrakk> \<Longrightarrow> v x \<le> v ( n \<times>\<^bsub>K\<^esub> x)
[PROOF STEP]
apply (cut_tac field_is_ring, induct_tac n, simp)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>valuation K v; x \<in> carrier K; 0 \<le> v x; Ring K\<rbrakk> \<Longrightarrow> v x \<le> v \<zero>
 2. \<And>n. \<lbrakk>valuation K v; x \<in> carrier K; 0 \<le> v x; Ring K; v x \<le> v ( n \<times>\<^bsub>K\<^esub> x)\<rbrakk> \<Longrightarrow> v x \<le> v ( Suc n \<times>\<^bsub>K\<^esub> x)
[PROOF STEP]
apply (simp add:value_of_zero,
       simp,
       frule_tac y = "n \<times>\<^bsub>K\<^esub> x" in amin_le_plus[of "v" "x"], assumption+,
       rule Ring.nsClose, assumption+)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>n. \<lbrakk>valuation K v; x \<in> carrier K; 0 \<le> v x; Ring K; v x \<le> v ( n \<times>\<^bsub>K\<^esub> x); amin (v x) (v ( n \<times>\<^bsub>K\<^esub> x)) \<le> v (x \<plusminus>  n \<times>\<^bsub>K\<^esub> x)\<rbrakk> \<Longrightarrow> v x \<le> v ( n \<times>\<^bsub>K\<^esub> x \<plusminus> x)
[PROOF STEP]
apply (simp add:amin_def,
       frule Ring.ring_is_ag[of K],
       frule_tac n = n in Ring.nsClose[of K x], assumption+,
       simp add:aGroup.ag_pOp_commute)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma (in Corps) ApproximationTr:"\<lbrakk>valuation K v; x \<in> carrier K; 0 \<le> (v x)\<rbrakk> \<Longrightarrow>
             v x \<le> (v (1\<^sub>r \<plusminus> -\<^sub>a ((1\<^sub>r \<plusminus> x)^\<^bsup>K (Suc n)\<^esup>)))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>valuation K v; x \<in> carrier K; 0 \<le> v x\<rbrakk> \<Longrightarrow> v x \<le> v (1\<^sub>r \<plusminus> -\<^sub>a (1\<^sub>r \<plusminus> x)^\<^bsup>K Suc n\<^esup>)
[PROOF STEP]
apply (cut_tac field_is_ring, frule Ring.ring_is_ag[of "K"],
       case_tac "x = \<zero>\<^bsub>K\<^esub>",
       simp, frule Ring.ring_one[of "K"], simp add:aGroup.ag_r_zero,
       simp add:Ring.npOne, simp add:Ring.ring_l_one,simp add:aGroup.ag_r_inv1,
       subst Ring.tail_of_expansion1[of "K" "x"], assumption+,
       frule Ring.ring_one[of "K"])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>valuation K v; x \<in> carrier K; 0 \<le> v x; Ring K; aGroup K; x \<noteq> \<zero>; 1\<^sub>r \<in> carrier K\<rbrakk> \<Longrightarrow> v x \<le> v (1\<^sub>r \<plusminus> -\<^sub>a (x \<cdot>\<^sub>r \<Sigma>\<^sub>e K (\<lambda>i.  \<^bsub>Suc n\<^esub>C\<^bsub>Suc i\<^esub> \<times>\<^bsub>K\<^esub> x^\<^bsup>K i\<^esup>) n \<plusminus> 1\<^sub>r))
[PROOF STEP]
apply (subgoal_tac "(nsum K (\<lambda>i. \<^bsub>Suc n\<^esub>C\<^bsub>Suc i\<^esub> \<times>\<^bsub>K\<^esub> x^\<^bsup>K i\<^esup>) n)\<in>carrier (Vr K v)",
       frule Vr_mem_f_mem[of "v" "(nsum K (\<lambda>i. \<^bsub>Suc n\<^esub>C\<^bsub>Suc i\<^esub> \<times>\<^bsub>K\<^esub> x^\<^bsup>K i\<^esup>) n)"],
       assumption+,
       frule_tac x = x and y = "nsum K (\<lambda>i. \<^bsub>Suc n\<^esub>C\<^bsub>Suc i\<^esub> \<times>\<^bsub>K\<^esub> x^\<^bsup>K i\<^esup>) n" in
       Ring.ring_tOp_closed[of "K"], assumption+,
       subst aGroup.ag_pOp_commute[of "K" _ "1\<^sub>r"], assumption+,
       subst aGroup.ag_p_inv[of "K" "1\<^sub>r"], assumption+,
       subst aGroup.ag_pOp_assoc[THEN sym], assumption+,
       simp add:aGroup.ag_mOp_closed, rule aGroup.ag_mOp_closed, assumption+,
       simp del:binomial_Suc_Suc add:aGroup.ag_r_inv1, subst aGroup.ag_l_zero,
       assumption+,
       rule aGroup.ag_mOp_closed, assumption+, simp add:val_minus_eq)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>valuation K v; x \<in> carrier K; 0 \<le> v x; Ring K; aGroup K; x \<noteq> \<zero>; 1\<^sub>r \<in> carrier K; \<Sigma>\<^sub>e K (\<lambda>i.  (\<^bsub>n\<^esub>C\<^bsub>i\<^esub> + \<^bsub>n\<^esub>C\<^bsub>Suc i\<^esub>) \<times>\<^bsub>K\<^esub> x^\<^bsup>K i\<^esup>) n \<in> carrier (Vr K v); \<Sigma>\<^sub>e K (\<lambda>i.  (\<^bsub>n\<^esub>C\<^bsub>i\<^esub> + \<^bsub>n\<^esub>C\<^bsub>Suc i\<^esub>) \<times>\<^bsub>K\<^esub> x^\<^bsup>K i\<^esup>) n \<in> carrier K; x \<cdot>\<^sub>r \<Sigma>\<^sub>e K (\<lambda>i.  (\<^bsub>n\<^esub>C\<^bsub>i\<^esub> + \<^bsub>n\<^esub>C\<^bsub>Suc i\<^esub>) \<times>\<^bsub>K\<^esub> x^\<^bsup>K i\<^esup>) n \<in> carrier K\<rbrakk> \<Longrightarrow> v x \<le> v (x \<cdot>\<^sub>r \<Sigma>\<^sub>e K (\<lambda>i.  (\<^bsub>n\<^esub>C\<^bsub>i\<^esub> + \<^bsub>n\<^esub>C\<^bsub>Suc i\<^esub>) \<times>\<^bsub>K\<^esub> x^\<^bsup>K i\<^esup>) n)
 2. \<lbrakk>valuation K v; x \<in> carrier K; 0 \<le> v x; Ring K; aGroup K; x \<noteq> \<zero>; 1\<^sub>r \<in> carrier K\<rbrakk> \<Longrightarrow> \<Sigma>\<^sub>e K (\<lambda>i.  \<^bsub>Suc n\<^esub>C\<^bsub>Suc i\<^esub> \<times>\<^bsub>K\<^esub> x^\<^bsup>K i\<^esup>) n \<in> carrier (Vr K v)
[PROOF STEP]
apply (subst val_t2p[of v], assumption+)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>valuation K v; x \<in> carrier K; 0 \<le> v x; Ring K; aGroup K; x \<noteq> \<zero>; 1\<^sub>r \<in> carrier K; \<Sigma>\<^sub>e K (\<lambda>i.  (\<^bsub>n\<^esub>C\<^bsub>i\<^esub> + \<^bsub>n\<^esub>C\<^bsub>Suc i\<^esub>) \<times>\<^bsub>K\<^esub> x^\<^bsup>K i\<^esup>) n \<in> carrier (Vr K v); \<Sigma>\<^sub>e K (\<lambda>i.  (\<^bsub>n\<^esub>C\<^bsub>i\<^esub> + \<^bsub>n\<^esub>C\<^bsub>Suc i\<^esub>) \<times>\<^bsub>K\<^esub> x^\<^bsup>K i\<^esup>) n \<in> carrier K; x \<cdot>\<^sub>r \<Sigma>\<^sub>e K (\<lambda>i.  (\<^bsub>n\<^esub>C\<^bsub>i\<^esub> + \<^bsub>n\<^esub>C\<^bsub>Suc i\<^esub>) \<times>\<^bsub>K\<^esub> x^\<^bsup>K i\<^esup>) n \<in> carrier K\<rbrakk> \<Longrightarrow> v x \<le> v x + v (\<Sigma>\<^sub>e K (\<lambda>i.  (\<^bsub>n\<^esub>C\<^bsub>i\<^esub> + \<^bsub>n\<^esub>C\<^bsub>Suc i\<^esub>) \<times>\<^bsub>K\<^esub> x^\<^bsup>K i\<^esup>) n)
 2. \<lbrakk>valuation K v; x \<in> carrier K; 0 \<le> v x; Ring K; aGroup K; x \<noteq> \<zero>; 1\<^sub>r \<in> carrier K\<rbrakk> \<Longrightarrow> \<Sigma>\<^sub>e K (\<lambda>i.  \<^bsub>Suc n\<^esub>C\<^bsub>Suc i\<^esub> \<times>\<^bsub>K\<^esub> x^\<^bsup>K i\<^esup>) n \<in> carrier (Vr K v)
[PROOF STEP]
apply (
       simp add:val_pos_mem_Vr[THEN sym, of v
                  "nsum K (\<lambda>i.(\<^bsub>n\<^esub>C\<^bsub>i\<^esub> + \<^bsub>n\<^esub>C\<^bsub>Suc i\<^esub>) \<times>\<^bsub>K\<^esub> x^\<^bsup>K i\<^esup>) n"],
       frule aadd_le_mono[of "0" "v (nsum K (\<lambda>i.(\<^bsub>n\<^esub>C\<^bsub>i\<^esub> + \<^bsub>n\<^esub>C\<^bsub>Suc i\<^esub>) \<times>\<^bsub>K\<^esub> x^\<^bsup>K i\<^esup>) n)"
         "v x"], simp add:aadd_0_l, simp add:aadd_commute[of "v x"])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>valuation K v; x \<in> carrier K; 0 \<le> v x; Ring K; aGroup K; x \<noteq> \<zero>; 1\<^sub>r \<in> carrier K\<rbrakk> \<Longrightarrow> \<Sigma>\<^sub>e K (\<lambda>i.  \<^bsub>Suc n\<^esub>C\<^bsub>Suc i\<^esub> \<times>\<^bsub>K\<^esub> x^\<^bsup>K i\<^esup>) n \<in> carrier (Vr K v)
[PROOF STEP]
apply (rule nsum_mem_in_Vr[of v n "\<lambda>i.\<^bsub>Suc n\<^esub>C\<^bsub>Suc i\<^esub> \<times>\<^bsub>K\<^esub> x^\<^bsup>K i\<^esup>"], assumption,
       rule allI, rule impI)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>j. \<lbrakk>valuation K v; x \<in> carrier K; 0 \<le> v x; Ring K; aGroup K; x \<noteq> \<zero>; 1\<^sub>r \<in> carrier K; j \<le> n\<rbrakk> \<Longrightarrow>  \<^bsub>Suc n\<^esub>C\<^bsub>Suc j\<^esub> \<times>\<^bsub>K\<^esub> x^\<^bsup>K j\<^esup> \<in> carrier K
 2. \<lbrakk>valuation K v; x \<in> carrier K; 0 \<le> v x; Ring K; aGroup K; x \<noteq> \<zero>; 1\<^sub>r \<in> carrier K\<rbrakk> \<Longrightarrow> \<forall>j\<le>n. 0 \<le> v ( \<^bsub>Suc n\<^esub>C\<^bsub>Suc j\<^esub> \<times>\<^bsub>K\<^esub> x^\<^bsup>K j\<^esup>)
[PROOF STEP]
apply (rule Ring.nsClose, assumption+)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>j. \<lbrakk>valuation K v; x \<in> carrier K; 0 \<le> v x; Ring K; aGroup K; x \<noteq> \<zero>; 1\<^sub>r \<in> carrier K; j \<le> n\<rbrakk> \<Longrightarrow> x^\<^bsup>K j\<^esup> \<in> carrier K
 2. \<lbrakk>valuation K v; x \<in> carrier K; 0 \<le> v x; Ring K; aGroup K; x \<noteq> \<zero>; 1\<^sub>r \<in> carrier K\<rbrakk> \<Longrightarrow> \<forall>j\<le>n. 0 \<le> v ( \<^bsub>Suc n\<^esub>C\<^bsub>Suc j\<^esub> \<times>\<^bsub>K\<^esub> x^\<^bsup>K j\<^esup>)
[PROOF STEP]
apply (simp add:Ring.npClose)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>valuation K v; x \<in> carrier K; 0 \<le> v x; Ring K; aGroup K; x \<noteq> \<zero>; 1\<^sub>r \<in> carrier K\<rbrakk> \<Longrightarrow> \<forall>j\<le>n. 0 \<le> v ( \<^bsub>Suc n\<^esub>C\<^bsub>Suc j\<^esub> \<times>\<^bsub>K\<^esub> x^\<^bsup>K j\<^esup>)
[PROOF STEP]
apply (rule allI, rule impI)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>j. \<lbrakk>valuation K v; x \<in> carrier K; 0 \<le> v x; Ring K; aGroup K; x \<noteq> \<zero>; 1\<^sub>r \<in> carrier K; j \<le> n\<rbrakk> \<Longrightarrow> 0 \<le> v ( \<^bsub>Suc n\<^esub>C\<^bsub>Suc j\<^esub> \<times>\<^bsub>K\<^esub> x^\<^bsup>K j\<^esup>)
[PROOF STEP]
apply (cut_tac i = 0 and j = "v (x^\<^bsup>K j\<^esup>)" and k = "v (\<^bsub>Suc n\<^esub>C\<^bsub>Suc j\<^esub> \<times>\<^bsub>K\<^esub> x^\<^bsup>K j\<^esup>)"
       in ale_trans)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>j. \<lbrakk>valuation K v; x \<in> carrier K; 0 \<le> v x; Ring K; aGroup K; x \<noteq> \<zero>; 1\<^sub>r \<in> carrier K; j \<le> n\<rbrakk> \<Longrightarrow> 0 \<le> v (x^\<^bsup>K j\<^esup>)
 2. \<And>j. \<lbrakk>valuation K v; x \<in> carrier K; 0 \<le> v x; Ring K; aGroup K; x \<noteq> \<zero>; 1\<^sub>r \<in> carrier K; j \<le> n\<rbrakk> \<Longrightarrow> v (x^\<^bsup>K j\<^esup>) \<le> v ( \<^bsub>Suc n\<^esub>C\<^bsub>Suc j\<^esub> \<times>\<^bsub>K\<^esub> x^\<^bsup>K j\<^esup>)
 3. \<And>j. \<lbrakk>valuation K v; x \<in> carrier K; 0 \<le> v x; Ring K; aGroup K; x \<noteq> \<zero>; 1\<^sub>r \<in> carrier K; j \<le> n; 0 \<le> v ( \<^bsub>Suc n\<^esub>C\<^bsub>Suc j\<^esub> \<times>\<^bsub>K\<^esub> x^\<^bsup>K j\<^esup>)\<rbrakk> \<Longrightarrow> 0 \<le> v ( \<^bsub>Suc n\<^esub>C\<^bsub>Suc j\<^esub> \<times>\<^bsub>K\<^esub> x^\<^bsup>K j\<^esup>)
[PROOF STEP]
apply (case_tac "j = 0", simp add:value_of_one)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>j. \<lbrakk>valuation K v; x \<in> carrier K; 0 \<le> v x; Ring K; aGroup K; x \<noteq> \<zero>; 1\<^sub>r \<in> carrier K; j \<le> n; j \<noteq> 0\<rbrakk> \<Longrightarrow> 0 \<le> v (x^\<^bsup>K j\<^esup>)
 2. \<And>j. \<lbrakk>valuation K v; x \<in> carrier K; 0 \<le> v x; Ring K; aGroup K; x \<noteq> \<zero>; 1\<^sub>r \<in> carrier K; j \<le> n\<rbrakk> \<Longrightarrow> v (x^\<^bsup>K j\<^esup>) \<le> v ( \<^bsub>Suc n\<^esub>C\<^bsub>Suc j\<^esub> \<times>\<^bsub>K\<^esub> x^\<^bsup>K j\<^esup>)
 3. \<And>j. \<lbrakk>valuation K v; x \<in> carrier K; 0 \<le> v x; Ring K; aGroup K; x \<noteq> \<zero>; 1\<^sub>r \<in> carrier K; j \<le> n; 0 \<le> v ( \<^bsub>Suc n\<^esub>C\<^bsub>Suc j\<^esub> \<times>\<^bsub>K\<^esub> x^\<^bsup>K j\<^esup>)\<rbrakk> \<Longrightarrow> 0 \<le> v ( \<^bsub>Suc n\<^esub>C\<^bsub>Suc j\<^esub> \<times>\<^bsub>K\<^esub> x^\<^bsup>K j\<^esup>)
[PROOF STEP]
apply (simp add: val_exp_ring[THEN sym],
        frule val_nonzero_z[of v x], assumption+,
        erule exE,
        cut_tac m1 = 0 and n1 = j in of_nat_less_iff[THEN sym],
        frule_tac a = "0 < j" and b = "int 0 < int j" in a_b_exchange,
        assumption, thin_tac "0 < j", thin_tac "(0 < j) = (int 0 < int j)")
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>j z. \<lbrakk>valuation K v; x \<in> carrier K; 0 \<le> v x; Ring K; aGroup K; x \<noteq> \<zero>; 1\<^sub>r \<in> carrier K; j \<le> n; v x = ant z; int 0 < int j\<rbrakk> \<Longrightarrow> 0 \<le> int j *\<^sub>a v x
 2. \<And>j. \<lbrakk>valuation K v; x \<in> carrier K; 0 \<le> v x; Ring K; aGroup K; x \<noteq> \<zero>; 1\<^sub>r \<in> carrier K; j \<le> n\<rbrakk> \<Longrightarrow> v (x^\<^bsup>K j\<^esup>) \<le> v ( \<^bsub>Suc n\<^esub>C\<^bsub>Suc j\<^esub> \<times>\<^bsub>K\<^esub> x^\<^bsup>K j\<^esup>)
 3. \<And>j. \<lbrakk>valuation K v; x \<in> carrier K; 0 \<le> v x; Ring K; aGroup K; x \<noteq> \<zero>; 1\<^sub>r \<in> carrier K; j \<le> n; 0 \<le> v ( \<^bsub>Suc n\<^esub>C\<^bsub>Suc j\<^esub> \<times>\<^bsub>K\<^esub> x^\<^bsup>K j\<^esup>)\<rbrakk> \<Longrightarrow> 0 \<le> v ( \<^bsub>Suc n\<^esub>C\<^bsub>Suc j\<^esub> \<times>\<^bsub>K\<^esub> x^\<^bsup>K j\<^esup>)
[PROOF STEP]
apply (simp del: of_nat_0_less_iff)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>j z. \<lbrakk>valuation K v; x \<in> carrier K; 0 \<le> ant z; Ring K; aGroup K; x \<noteq> \<zero>; 1\<^sub>r \<in> carrier K; j \<le> n; v x = ant z; 0 < int j\<rbrakk> \<Longrightarrow> 0 \<le> int j *\<^sub>a ant z
 2. \<And>j. \<lbrakk>valuation K v; x \<in> carrier K; 0 \<le> v x; Ring K; aGroup K; x \<noteq> \<zero>; 1\<^sub>r \<in> carrier K; j \<le> n\<rbrakk> \<Longrightarrow> v (x^\<^bsup>K j\<^esup>) \<le> v ( \<^bsub>Suc n\<^esub>C\<^bsub>Suc j\<^esub> \<times>\<^bsub>K\<^esub> x^\<^bsup>K j\<^esup>)
 3. \<And>j. \<lbrakk>valuation K v; x \<in> carrier K; 0 \<le> v x; Ring K; aGroup K; x \<noteq> \<zero>; 1\<^sub>r \<in> carrier K; j \<le> n; 0 \<le> v ( \<^bsub>Suc n\<^esub>C\<^bsub>Suc j\<^esub> \<times>\<^bsub>K\<^esub> x^\<^bsup>K j\<^esup>)\<rbrakk> \<Longrightarrow> 0 \<le> v ( \<^bsub>Suc n\<^esub>C\<^bsub>Suc j\<^esub> \<times>\<^bsub>K\<^esub> x^\<^bsup>K j\<^esup>)
[PROOF STEP]
apply (frule_tac w1 = "int j" and x1 = 0 and y1 = "ant z" in
         asprod_pos_mono[THEN sym],
        simp only:asprod_n_0)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>j. \<lbrakk>valuation K v; x \<in> carrier K; 0 \<le> v x; Ring K; aGroup K; x \<noteq> \<zero>; 1\<^sub>r \<in> carrier K; j \<le> n\<rbrakk> \<Longrightarrow> v (x^\<^bsup>K j\<^esup>) \<le> v ( \<^bsub>Suc n\<^esub>C\<^bsub>Suc j\<^esub> \<times>\<^bsub>K\<^esub> x^\<^bsup>K j\<^esup>)
 2. \<And>j. \<lbrakk>valuation K v; x \<in> carrier K; 0 \<le> v x; Ring K; aGroup K; x \<noteq> \<zero>; 1\<^sub>r \<in> carrier K; j \<le> n; 0 \<le> v ( \<^bsub>Suc n\<^esub>C\<^bsub>Suc j\<^esub> \<times>\<^bsub>K\<^esub> x^\<^bsup>K j\<^esup>)\<rbrakk> \<Longrightarrow> 0 \<le> v ( \<^bsub>Suc n\<^esub>C\<^bsub>Suc j\<^esub> \<times>\<^bsub>K\<^esub> x^\<^bsup>K j\<^esup>)
[PROOF STEP]
apply(rule_tac x = "x^\<^bsup>K j\<^esup>" and n = "\<^bsub>Suc n\<^esub>C\<^bsub>Suc j\<^esub>" in
       val_nscal_ge_selfTr[of v], assumption+,
       simp add:Ring.npClose, simp add:val_exp_ring[THEN sym],
       frule val_nonzero_z[of "v" "x"], assumption+, erule exE, simp)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>j z. \<lbrakk>valuation K v; x \<in> carrier K; 0 \<le> ant z; Ring K; aGroup K; x \<noteq> \<zero>; 1\<^sub>r \<in> carrier K; j \<le> n; v x = ant z\<rbrakk> \<Longrightarrow> 0 \<le> int j *\<^sub>a ant z
 2. \<And>j. \<lbrakk>valuation K v; x \<in> carrier K; 0 \<le> v x; Ring K; aGroup K; x \<noteq> \<zero>; 1\<^sub>r \<in> carrier K; j \<le> n; 0 \<le> v ( \<^bsub>Suc n\<^esub>C\<^bsub>Suc j\<^esub> \<times>\<^bsub>K\<^esub> x^\<^bsup>K j\<^esup>)\<rbrakk> \<Longrightarrow> 0 \<le> v ( \<^bsub>Suc n\<^esub>C\<^bsub>Suc j\<^esub> \<times>\<^bsub>K\<^esub> x^\<^bsup>K j\<^esup>)
[PROOF STEP]
apply (case_tac "j = 0", simp)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>j z. \<lbrakk>valuation K v; x \<in> carrier K; 0 \<le> ant z; Ring K; aGroup K; x \<noteq> \<zero>; 1\<^sub>r \<in> carrier K; j \<le> n; v x = ant z; j \<noteq> 0\<rbrakk> \<Longrightarrow> 0 \<le> int j *\<^sub>a ant z
 2. \<And>j. \<lbrakk>valuation K v; x \<in> carrier K; 0 \<le> v x; Ring K; aGroup K; x \<noteq> \<zero>; 1\<^sub>r \<in> carrier K; j \<le> n; 0 \<le> v ( \<^bsub>Suc n\<^esub>C\<^bsub>Suc j\<^esub> \<times>\<^bsub>K\<^esub> x^\<^bsup>K j\<^esup>)\<rbrakk> \<Longrightarrow> 0 \<le> v ( \<^bsub>Suc n\<^esub>C\<^bsub>Suc j\<^esub> \<times>\<^bsub>K\<^esub> x^\<^bsup>K j\<^esup>)
[PROOF STEP]
apply (subst asprod_amult, simp, simp add:a_z_z)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>j z. \<lbrakk>valuation K v; x \<in> carrier K; 0 \<le> ant z; Ring K; aGroup K; x \<noteq> \<zero>; 1\<^sub>r \<in> carrier K; j \<le> n; v x = ant z; 0 < j\<rbrakk> \<Longrightarrow> 0 \<le> ant (int j * z)
 2. \<And>j. \<lbrakk>valuation K v; x \<in> carrier K; 0 \<le> v x; Ring K; aGroup K; x \<noteq> \<zero>; 1\<^sub>r \<in> carrier K; j \<le> n; 0 \<le> v ( \<^bsub>Suc n\<^esub>C\<^bsub>Suc j\<^esub> \<times>\<^bsub>K\<^esub> x^\<^bsup>K j\<^esup>)\<rbrakk> \<Longrightarrow> 0 \<le> v ( \<^bsub>Suc n\<^esub>C\<^bsub>Suc j\<^esub> \<times>\<^bsub>K\<^esub> x^\<^bsup>K j\<^esup>)
[PROOF STEP]
apply(
        simp only:ant_0[THEN sym], simp only:ale_zle,
        cut_tac m1 = 0 and n1 = j in of_nat_less_iff[THEN sym])
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>j z. \<lbrakk>valuation K v; x \<in> carrier K; 0 \<le> z; Ring K; aGroup K; x \<noteq> \<zero>; 1\<^sub>r \<in> carrier K; j \<le> n; v x = ant z; 0 < j; (0 < j) = (of_nat 0 < of_nat j)\<rbrakk> \<Longrightarrow> 0 \<le> int j * z
 2. \<And>j. \<lbrakk>valuation K v; x \<in> carrier K; 0 \<le> v x; Ring K; aGroup K; x \<noteq> \<zero>; 1\<^sub>r \<in> carrier K; j \<le> n; 0 \<le> v ( \<^bsub>Suc n\<^esub>C\<^bsub>Suc j\<^esub> \<times>\<^bsub>K\<^esub> x^\<^bsup>K j\<^esup>)\<rbrakk> \<Longrightarrow> 0 \<le> v ( \<^bsub>Suc n\<^esub>C\<^bsub>Suc j\<^esub> \<times>\<^bsub>K\<^esub> x^\<^bsup>K j\<^esup>)
[PROOF STEP]
apply (        frule_tac a = "0 < j" and b = "int 0 < int j" in a_b_exchange,
        assumption+, thin_tac "0 < j", thin_tac "(0 < j) = (int 0 < int j)",
        frule_tac z = "int 0" and z' = "int j" in zless_imp_zle,
        frule_tac i = "int 0" and j = "int j" and k = z in int_mult_le,
         assumption+, simp add:mult.commute )
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>j. \<lbrakk>valuation K v; x \<in> carrier K; 0 \<le> v x; Ring K; aGroup K; x \<noteq> \<zero>; 1\<^sub>r \<in> carrier K; j \<le> n; 0 \<le> v ( \<^bsub>Suc n\<^esub>C\<^bsub>Suc j\<^esub> \<times>\<^bsub>K\<^esub> x^\<^bsup>K j\<^esup>)\<rbrakk> \<Longrightarrow> 0 \<le> v ( \<^bsub>Suc n\<^esub>C\<^bsub>Suc j\<^esub> \<times>\<^bsub>K\<^esub> x^\<^bsup>K j\<^esup>)
[PROOF STEP]
apply assumption
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma (in Corps) ApproximationTr0:"aa \<in> carrier K \<Longrightarrow>
            (1\<^sub>r \<plusminus> -\<^sub>a (aa^\<^bsup>K N\<^esup>))^\<^bsup>K N\<^esup> \<in> carrier K"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. aa \<in> carrier K \<Longrightarrow> (1\<^sub>r \<plusminus> -\<^sub>a aa^\<^bsup>K N\<^esup>)^\<^bsup>K N\<^esup> \<in> carrier K
[PROOF STEP]
apply (cut_tac field_is_ring, frule Ring.ring_is_ag[of "K"],
       rule Ring.npClose, assumption+,
       rule aGroup.ag_pOp_closed, assumption+, simp add:Ring.ring_one,
       rule aGroup.ag_mOp_closed, assumption+, rule Ring.npClose, assumption+)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma (in Corps) ApproximationTr1:"aa \<in> carrier K \<Longrightarrow>
            1\<^sub>r \<plusminus> -\<^sub>a ((1\<^sub>r \<plusminus> -\<^sub>a (aa^\<^bsup>K N\<^esup>))^\<^bsup>K N\<^esup>) \<in> carrier K"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. aa \<in> carrier K \<Longrightarrow> 1\<^sub>r \<plusminus> -\<^sub>a (1\<^sub>r \<plusminus> -\<^sub>a aa^\<^bsup>K N\<^esup>)^\<^bsup>K N\<^esup> \<in> carrier K
[PROOF STEP]
apply (cut_tac field_is_ring, frule Ring.ring_is_ag[of "K"],
       frule ApproximationTr0[of aa N],
       frule Ring.ring_one[of "K"], rule aGroup.ag_pOp_closed, assumption+,
       rule aGroup.ag_mOp_closed, assumption+)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done