[STATEMENT]
lemma (in Corps) app_LB:"\<lbrakk>vals_nonequiv K (Suc n) vv;
      \<forall>l\<le> (Suc n). x l \<in> carrier K; j \<le> (Suc n)\<rbrakk> \<Longrightarrow>
        \<forall>N. (\<Psi>\<^bsub>K (Suc n) vv x m\<^esub>) j < N \<longrightarrow> (an m) \<le>
  (vv j (\<Sigma>\<^sub>e K (\<lambda>j\<in>{h. h \<le> (Suc n)}. (x j) \<cdot>\<^sub>r (1\<^sub>r \<plusminus> -\<^sub>a (1\<^sub>r \<plusminus>
  -\<^sub>a ((\<Omega>\<^bsub>K vv (Suc n)\<^esub>) j)^\<^bsup>K N\<^esup>)^\<^bsup>K N\<^esup>)) (Suc n) \<plusminus> -\<^sub>a (x j)))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>vals_nonequiv K (Suc n) vv; \<forall>l\<le>Suc n. x l \<in> carrier K; j \<le> Suc n\<rbrakk> \<Longrightarrow> \<forall>N>(\<Psi>\<^bsub>K Suc n vv x m\<^esub>) j. an m \<le> vv j (\<Sigma>\<^sub>e K (\<lambda>j\<in>{h. h \<le> Suc n}. x j \<cdot>\<^sub>r (1\<^sub>r \<plusminus> -\<^sub>a (1\<^sub>r \<plusminus> -\<^sub>a (\<Omega>\<^bsub>K vv Suc n\<^esub>) j^\<^bsup>K N\<^esup>)^\<^bsup>K N\<^esup>)) Suc n \<plusminus> -\<^sub>a x j)
[PROOF STEP]
apply (frule ApproximationTr3[of "n" "vv" "x" "j" "m"],
                               assumption+)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>vals_nonequiv K (Suc n) vv; \<forall>l\<le>Suc n. x l \<in> carrier K; j \<le> Suc n; \<exists>L. \<forall>N>L. an m \<le> vv j (\<Sigma>\<^sub>e K (\<lambda>k\<in>{h. h \<le> Suc n}. x k \<cdot>\<^sub>r (1\<^sub>r \<plusminus> -\<^sub>a (1\<^sub>r \<plusminus> -\<^sub>a (\<Omega>\<^bsub>K vv Suc n\<^esub>) k^\<^bsup>K N\<^esup>)^\<^bsup>K N\<^esup>)) Suc n \<plusminus> -\<^sub>a x j)\<rbrakk> \<Longrightarrow> \<forall>N>(\<Psi>\<^bsub>K Suc n vv x m\<^esub>) j. an m \<le> vv j (\<Sigma>\<^sub>e K (\<lambda>j\<in>{h. h \<le> Suc n}. x j \<cdot>\<^sub>r (1\<^sub>r \<plusminus> -\<^sub>a (1\<^sub>r \<plusminus> -\<^sub>a (\<Omega>\<^bsub>K vv Suc n\<^esub>) j^\<^bsup>K N\<^esup>)^\<^bsup>K N\<^esup>)) Suc n \<plusminus> -\<^sub>a x j)
[PROOF STEP]
apply (simp del:nsum_suc add:app_lb_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>vals_nonequiv K (Suc n) vv; \<forall>l\<le>Suc n. x l \<in> carrier K; j \<le> Suc n; \<exists>L. \<forall>N>L. an m \<le> vv j (\<Sigma>\<^sub>e K (\<lambda>k\<in>{h. h \<le> Suc n}. x k \<cdot>\<^sub>r (1\<^sub>r \<plusminus> -\<^sub>a (1\<^sub>r \<plusminus> -\<^sub>a (\<Omega>\<^bsub>K vv Suc n\<^esub>) k^\<^bsup>K N\<^esup>)^\<^bsup>K N\<^esup>)) Suc n \<plusminus> -\<^sub>a x j)\<rbrakk> \<Longrightarrow> \<forall>N>SOME L. \<forall>N>L. an m \<le> vv j (\<Sigma>\<^sub>e K (\<lambda>j\<in>{h. h \<le> Suc n}. x j \<cdot>\<^sub>r (1\<^sub>r \<plusminus> -\<^sub>a (1\<^sub>r \<plusminus> -\<^sub>a (\<Omega>\<^bsub>K vv Suc n\<^esub>) j^\<^bsup>K N\<^esup>)^\<^bsup>K N\<^esup>)) Suc n \<plusminus> -\<^sub>a x j). an m \<le> vv j (\<Sigma>\<^sub>e K (\<lambda>j\<in>{h. h \<le> Suc n}. x j \<cdot>\<^sub>r (1\<^sub>r \<plusminus> -\<^sub>a (1\<^sub>r \<plusminus> -\<^sub>a (\<Omega>\<^bsub>K vv Suc n\<^esub>) j^\<^bsup>K N\<^esup>)^\<^bsup>K N\<^esup>)) Suc n \<plusminus> -\<^sub>a x j)
[PROOF STEP]
apply (rule allI)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>N. \<lbrakk>vals_nonequiv K (Suc n) vv; \<forall>l\<le>Suc n. x l \<in> carrier K; j \<le> Suc n; \<exists>L. \<forall>N>L. an m \<le> vv j (\<Sigma>\<^sub>e K (\<lambda>k\<in>{h. h \<le> Suc n}. x k \<cdot>\<^sub>r (1\<^sub>r \<plusminus> -\<^sub>a (1\<^sub>r \<plusminus> -\<^sub>a (\<Omega>\<^bsub>K vv Suc n\<^esub>) k^\<^bsup>K N\<^esup>)^\<^bsup>K N\<^esup>)) Suc n \<plusminus> -\<^sub>a x j)\<rbrakk> \<Longrightarrow> (SOME L. \<forall>N>L. an m \<le> vv j (\<Sigma>\<^sub>e K (\<lambda>j\<in>{h. h \<le> Suc n}. x j \<cdot>\<^sub>r (1\<^sub>r \<plusminus> -\<^sub>a (1\<^sub>r \<plusminus> -\<^sub>a (\<Omega>\<^bsub>K vv Suc n\<^esub>) j^\<^bsup>K N\<^esup>)^\<^bsup>K N\<^esup>)) Suc n \<plusminus> -\<^sub>a x j)) < N \<longrightarrow> an m \<le> vv j (\<Sigma>\<^sub>e K (\<lambda>j\<in>{h. h \<le> Suc n}. x j \<cdot>\<^sub>r (1\<^sub>r \<plusminus> -\<^sub>a (1\<^sub>r \<plusminus> -\<^sub>a (\<Omega>\<^bsub>K vv Suc n\<^esub>) j^\<^bsup>K N\<^esup>)^\<^bsup>K N\<^esup>)) Suc n \<plusminus> -\<^sub>a x j)
[PROOF STEP]
apply (rule someI2_ex)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>N. \<lbrakk>vals_nonequiv K (Suc n) vv; \<forall>l\<le>Suc n. x l \<in> carrier K; j \<le> Suc n; \<exists>L. \<forall>N>L. an m \<le> vv j (\<Sigma>\<^sub>e K (\<lambda>k\<in>{h. h \<le> Suc n}. x k \<cdot>\<^sub>r (1\<^sub>r \<plusminus> -\<^sub>a (1\<^sub>r \<plusminus> -\<^sub>a (\<Omega>\<^bsub>K vv Suc n\<^esub>) k^\<^bsup>K N\<^esup>)^\<^bsup>K N\<^esup>)) Suc n \<plusminus> -\<^sub>a x j)\<rbrakk> \<Longrightarrow> \<exists>a. \<forall>N>a. an m \<le> vv j (\<Sigma>\<^sub>e K (\<lambda>j\<in>{h. h \<le> Suc n}. x j \<cdot>\<^sub>r (1\<^sub>r \<plusminus> -\<^sub>a (1\<^sub>r \<plusminus> -\<^sub>a (\<Omega>\<^bsub>K vv Suc n\<^esub>) j^\<^bsup>K N\<^esup>)^\<^bsup>K N\<^esup>)) Suc n \<plusminus> -\<^sub>a x j)
 2. \<And>N xa. \<lbrakk>vals_nonequiv K (Suc n) vv; \<forall>l\<le>Suc n. x l \<in> carrier K; j \<le> Suc n; \<exists>L. \<forall>N>L. an m \<le> vv j (\<Sigma>\<^sub>e K (\<lambda>k\<in>{h. h \<le> Suc n}. x k \<cdot>\<^sub>r (1\<^sub>r \<plusminus> -\<^sub>a (1\<^sub>r \<plusminus> -\<^sub>a (\<Omega>\<^bsub>K vv Suc n\<^esub>) k^\<^bsup>K N\<^esup>)^\<^bsup>K N\<^esup>)) Suc n \<plusminus> -\<^sub>a x j); \<forall>N>xa. an m \<le> vv j (\<Sigma>\<^sub>e K (\<lambda>j\<in>{h. h \<le> Suc n}. x j \<cdot>\<^sub>r (1\<^sub>r \<plusminus> -\<^sub>a (1\<^sub>r \<plusminus> -\<^sub>a (\<Omega>\<^bsub>K vv Suc n\<^esub>) j^\<^bsup>K N\<^esup>)^\<^bsup>K N\<^esup>)) Suc n \<plusminus> -\<^sub>a x j)\<rbrakk> \<Longrightarrow> xa < N \<longrightarrow> an m \<le> vv j (\<Sigma>\<^sub>e K (\<lambda>j\<in>{h. h \<le> Suc n}. x j \<cdot>\<^sub>r (1\<^sub>r \<plusminus> -\<^sub>a (1\<^sub>r \<plusminus> -\<^sub>a (\<Omega>\<^bsub>K vv Suc n\<^esub>) j^\<^bsup>K N\<^esup>)^\<^bsup>K N\<^esup>)) Suc n \<plusminus> -\<^sub>a x j)
[PROOF STEP]
apply assumption+
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>N xa. \<lbrakk>vals_nonequiv K (Suc n) vv; \<forall>l\<le>Suc n. x l \<in> carrier K; j \<le> Suc n; \<exists>L. \<forall>N>L. an m \<le> vv j (\<Sigma>\<^sub>e K (\<lambda>k\<in>{h. h \<le> Suc n}. x k \<cdot>\<^sub>r (1\<^sub>r \<plusminus> -\<^sub>a (1\<^sub>r \<plusminus> -\<^sub>a (\<Omega>\<^bsub>K vv Suc n\<^esub>) k^\<^bsup>K N\<^esup>)^\<^bsup>K N\<^esup>)) Suc n \<plusminus> -\<^sub>a x j); \<forall>N>xa. an m \<le> vv j (\<Sigma>\<^sub>e K (\<lambda>j\<in>{h. h \<le> Suc n}. x j \<cdot>\<^sub>r (1\<^sub>r \<plusminus> -\<^sub>a (1\<^sub>r \<plusminus> -\<^sub>a (\<Omega>\<^bsub>K vv Suc n\<^esub>) j^\<^bsup>K N\<^esup>)^\<^bsup>K N\<^esup>)) Suc n \<plusminus> -\<^sub>a x j)\<rbrakk> \<Longrightarrow> xa < N \<longrightarrow> an m \<le> vv j (\<Sigma>\<^sub>e K (\<lambda>j\<in>{h. h \<le> Suc n}. x j \<cdot>\<^sub>r (1\<^sub>r \<plusminus> -\<^sub>a (1\<^sub>r \<plusminus> -\<^sub>a (\<Omega>\<^bsub>K vv Suc n\<^esub>) j^\<^bsup>K N\<^esup>)^\<^bsup>K N\<^esup>)) Suc n \<plusminus> -\<^sub>a x j)
[PROOF STEP]
apply (rule impI)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>N xa. \<lbrakk>vals_nonequiv K (Suc n) vv; \<forall>l\<le>Suc n. x l \<in> carrier K; j \<le> Suc n; \<exists>L. \<forall>N>L. an m \<le> vv j (\<Sigma>\<^sub>e K (\<lambda>k\<in>{h. h \<le> Suc n}. x k \<cdot>\<^sub>r (1\<^sub>r \<plusminus> -\<^sub>a (1\<^sub>r \<plusminus> -\<^sub>a (\<Omega>\<^bsub>K vv Suc n\<^esub>) k^\<^bsup>K N\<^esup>)^\<^bsup>K N\<^esup>)) Suc n \<plusminus> -\<^sub>a x j); \<forall>N>xa. an m \<le> vv j (\<Sigma>\<^sub>e K (\<lambda>j\<in>{h. h \<le> Suc n}. x j \<cdot>\<^sub>r (1\<^sub>r \<plusminus> -\<^sub>a (1\<^sub>r \<plusminus> -\<^sub>a (\<Omega>\<^bsub>K vv Suc n\<^esub>) j^\<^bsup>K N\<^esup>)^\<^bsup>K N\<^esup>)) Suc n \<plusminus> -\<^sub>a x j); xa < N\<rbrakk> \<Longrightarrow> an m \<le> vv j (\<Sigma>\<^sub>e K (\<lambda>j\<in>{h. h \<le> Suc n}. x j \<cdot>\<^sub>r (1\<^sub>r \<plusminus> -\<^sub>a (1\<^sub>r \<plusminus> -\<^sub>a (\<Omega>\<^bsub>K vv Suc n\<^esub>) j^\<^bsup>K N\<^esup>)^\<^bsup>K N\<^esup>)) Suc n \<plusminus> -\<^sub>a x j)
[PROOF STEP]
apply blast
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma (in Corps) ApplicationTr4:"\<lbrakk>vals_nonequiv K (Suc n) vv;
 \<forall>j\<in>{h. h \<le> (Suc n)}. x j \<in> carrier K\<rbrakk> \<Longrightarrow>
 \<exists>l. \<forall>N. l < N \<longrightarrow> (\<forall>j \<le> (Suc n).  (an m) \<le>
  (vv j (\<Sigma>\<^sub>e K (\<lambda>j\<in>{h. h \<le> (Suc n)}. (x j) \<cdot>\<^sub>r (1\<^sub>r \<plusminus> -\<^sub>a (1\<^sub>r \<plusminus>
  -\<^sub>a ((\<Omega>\<^bsub>K vv (Suc n)\<^esub>) j)^\<^bsup>K N\<^esup>)^\<^bsup>K N\<^esup>)) (Suc n) \<plusminus> -\<^sub>a (x j))))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>vals_nonequiv K (Suc n) vv; \<forall>j\<in>{h. h \<le> Suc n}. x j \<in> carrier K\<rbrakk> \<Longrightarrow> \<exists>l. \<forall>N>l. \<forall>j\<le>Suc n. an m \<le> vv j (\<Sigma>\<^sub>e K (\<lambda>j\<in>{h. h \<le> Suc n}. x j \<cdot>\<^sub>r (1\<^sub>r \<plusminus> -\<^sub>a (1\<^sub>r \<plusminus> -\<^sub>a (\<Omega>\<^bsub>K vv Suc n\<^esub>) j^\<^bsup>K N\<^esup>)^\<^bsup>K N\<^esup>)) Suc n \<plusminus> -\<^sub>a x j)
[PROOF STEP]
apply (subgoal_tac "\<forall>N. (m_max (Suc n) (\<Psi>\<^bsub>K (Suc n) vv x m\<^esub>)) < N \<longrightarrow>
  (\<forall>j\<le> (Suc n).  (an m) \<le>
  (vv j (\<Sigma>\<^sub>e K (\<lambda>j\<in>{h. h \<le> (Suc n)}. (x j) \<cdot>\<^sub>r (1\<^sub>r \<plusminus> -\<^sub>a (1\<^sub>r \<plusminus>
  -\<^sub>a ((\<Omega>\<^bsub>K vv (Suc n)\<^esub>) j)^\<^bsup>K N\<^esup>)^\<^bsup>K N\<^esup>)) (Suc n) \<plusminus> -\<^sub>a (x j))))")
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>vals_nonequiv K (Suc n) vv; \<forall>j\<in>{h. h \<le> Suc n}. x j \<in> carrier K; \<forall>N>m_max (Suc n) (\<Psi>\<^bsub>K Suc n vv x m\<^esub>). \<forall>j\<le>Suc n. an m \<le> vv j (\<Sigma>\<^sub>e K (\<lambda>j\<in>{h. h \<le> Suc n}. x j \<cdot>\<^sub>r (1\<^sub>r \<plusminus> -\<^sub>a (1\<^sub>r \<plusminus> -\<^sub>a (\<Omega>\<^bsub>K vv Suc n\<^esub>) j^\<^bsup>K N\<^esup>)^\<^bsup>K N\<^esup>)) Suc n \<plusminus> -\<^sub>a x j)\<rbrakk> \<Longrightarrow> \<exists>l. \<forall>N>l. \<forall>j\<le>Suc n. an m \<le> vv j (\<Sigma>\<^sub>e K (\<lambda>j\<in>{h. h \<le> Suc n}. x j \<cdot>\<^sub>r (1\<^sub>r \<plusminus> -\<^sub>a (1\<^sub>r \<plusminus> -\<^sub>a (\<Omega>\<^bsub>K vv Suc n\<^esub>) j^\<^bsup>K N\<^esup>)^\<^bsup>K N\<^esup>)) Suc n \<plusminus> -\<^sub>a x j)
 2. \<lbrakk>vals_nonequiv K (Suc n) vv; \<forall>j\<in>{h. h \<le> Suc n}. x j \<in> carrier K\<rbrakk> \<Longrightarrow> \<forall>N>m_max (Suc n) (\<Psi>\<^bsub>K Suc n vv x m\<^esub>). \<forall>j\<le>Suc n. an m \<le> vv j (\<Sigma>\<^sub>e K (\<lambda>j\<in>{h. h \<le> Suc n}. x j \<cdot>\<^sub>r (1\<^sub>r \<plusminus> -\<^sub>a (1\<^sub>r \<plusminus> -\<^sub>a (\<Omega>\<^bsub>K vv Suc n\<^esub>) j^\<^bsup>K N\<^esup>)^\<^bsup>K N\<^esup>)) Suc n \<plusminus> -\<^sub>a x j)
[PROOF STEP]
apply blast
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>vals_nonequiv K (Suc n) vv; \<forall>j\<in>{h. h \<le> Suc n}. x j \<in> carrier K\<rbrakk> \<Longrightarrow> \<forall>N>m_max (Suc n) (\<Psi>\<^bsub>K Suc n vv x m\<^esub>). \<forall>j\<le>Suc n. an m \<le> vv j (\<Sigma>\<^sub>e K (\<lambda>j\<in>{h. h \<le> Suc n}. x j \<cdot>\<^sub>r (1\<^sub>r \<plusminus> -\<^sub>a (1\<^sub>r \<plusminus> -\<^sub>a (\<Omega>\<^bsub>K vv Suc n\<^esub>) j^\<^bsup>K N\<^esup>)^\<^bsup>K N\<^esup>)) Suc n \<plusminus> -\<^sub>a x j)
[PROOF STEP]
apply (rule allI, rule impI)+
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>N j. \<lbrakk>vals_nonequiv K (Suc n) vv; \<forall>j\<in>{h. h \<le> Suc n}. x j \<in> carrier K; m_max (Suc n) (\<Psi>\<^bsub>K Suc n vv x m\<^esub>) < N; j \<le> Suc n\<rbrakk> \<Longrightarrow> an m \<le> vv j (\<Sigma>\<^sub>e K (\<lambda>j\<in>{h. h \<le> Suc n}. x j \<cdot>\<^sub>r (1\<^sub>r \<plusminus> -\<^sub>a (1\<^sub>r \<plusminus> -\<^sub>a (\<Omega>\<^bsub>K vv Suc n\<^esub>) j^\<^bsup>K N\<^esup>)^\<^bsup>K N\<^esup>)) Suc n \<plusminus> -\<^sub>a x j)
[PROOF STEP]
apply (frule_tac j = j in  app_LB[of  "n" "vv" "x" _ "m"],
       simp, assumption,
       subgoal_tac "(\<Psi>\<^bsub>K (Suc n) vv x m\<^esub>) j < N", blast)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>N j. \<lbrakk>vals_nonequiv K (Suc n) vv; \<forall>j\<in>{h. h \<le> Suc n}. x j \<in> carrier K; m_max (Suc n) (\<Psi>\<^bsub>K Suc n vv x m\<^esub>) < N; j \<le> Suc n; \<forall>N>(\<Psi>\<^bsub>K Suc n vv x m\<^esub>) j. an m \<le> vv j (\<Sigma>\<^sub>e K (\<lambda>j\<in>{h. h \<le> Suc n}. x j \<cdot>\<^sub>r (1\<^sub>r \<plusminus> -\<^sub>a (1\<^sub>r \<plusminus> -\<^sub>a (\<Omega>\<^bsub>K vv Suc n\<^esub>) j^\<^bsup>K N\<^esup>)^\<^bsup>K N\<^esup>)) Suc n \<plusminus> -\<^sub>a x j)\<rbrakk> \<Longrightarrow> (\<Psi>\<^bsub>K Suc n vv x m\<^esub>) j < N
[PROOF STEP]
apply (frule_tac l = j and n = "Suc n" and f = "\<Psi>\<^bsub>K (Suc n) vv x m\<^esub>" in m_max_gt,
       frule_tac x = "(\<Psi>\<^bsub>K (Suc n) vv x m\<^esub>) j" and
       y = "m_max (Suc n) (\<Psi>\<^bsub>K (Suc n) vv x m\<^esub>)" and z = N in le_less_trans,
       assumption+)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
theorem (in Corps) Approximation_thm:"\<lbrakk>vals_nonequiv K (Suc n) vv;
\<forall>j\<le> (Suc n). (x j) \<in> carrier K\<rbrakk>  \<Longrightarrow>
\<exists>y\<in>carrier K. \<forall>j\<le> (Suc n). (an m) \<le> (vv j (y \<plusminus> -\<^sub>a (x j)))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>vals_nonequiv K (Suc n) vv; \<forall>j\<le>Suc n. x j \<in> carrier K\<rbrakk> \<Longrightarrow> \<exists>y\<in>carrier K. \<forall>j\<le>Suc n. an m \<le> vv j (y \<plusminus> -\<^sub>a x j)
[PROOF STEP]
apply (cut_tac field_is_ring, frule Ring.ring_is_ag[of "K"])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>vals_nonequiv K (Suc n) vv; \<forall>j\<le>Suc n. x j \<in> carrier K; Ring K; aGroup K\<rbrakk> \<Longrightarrow> \<exists>y\<in>carrier K. \<forall>j\<le>Suc n. an m \<le> vv j (y \<plusminus> -\<^sub>a x j)
[PROOF STEP]
apply (subgoal_tac "\<exists>l. (\<forall>N. l < N \<longrightarrow> (\<forall>j \<le> (Suc n). (an m) \<le> ((vv j) ((nsum K (\<lambda>j\<in>{h. h \<le> (Suc n)}. (x j) \<cdot>\<^sub>r (1\<^sub>r \<plusminus> -\<^sub>a (1\<^sub>r \<plusminus> -\<^sub>a ((\<Omega>\<^bsub>K vv (Suc n)\<^esub>) j)^\<^bsup>K N\<^esup>)^\<^bsup>K N\<^esup>)) (Suc n)) \<plusminus> -\<^sub>a (x j)))))")
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>vals_nonequiv K (Suc n) vv; \<forall>j\<le>Suc n. x j \<in> carrier K; Ring K; aGroup K; \<exists>l. \<forall>N>l. \<forall>j\<le>Suc n. an m \<le> vv j (\<Sigma>\<^sub>e K (\<lambda>j\<in>{h. h \<le> Suc n}. x j \<cdot>\<^sub>r (1\<^sub>r \<plusminus> -\<^sub>a (1\<^sub>r \<plusminus> -\<^sub>a (\<Omega>\<^bsub>K vv Suc n\<^esub>) j^\<^bsup>K N\<^esup>)^\<^bsup>K N\<^esup>)) Suc n \<plusminus> -\<^sub>a x j)\<rbrakk> \<Longrightarrow> \<exists>y\<in>carrier K. \<forall>j\<le>Suc n. an m \<le> vv j (y \<plusminus> -\<^sub>a x j)
 2. \<lbrakk>vals_nonequiv K (Suc n) vv; \<forall>j\<le>Suc n. x j \<in> carrier K; Ring K; aGroup K\<rbrakk> \<Longrightarrow> \<exists>l. \<forall>N>l. \<forall>j\<le>Suc n. an m \<le> vv j (\<Sigma>\<^sub>e K (\<lambda>j\<in>{h. h \<le> Suc n}. x j \<cdot>\<^sub>r (1\<^sub>r \<plusminus> -\<^sub>a (1\<^sub>r \<plusminus> -\<^sub>a (\<Omega>\<^bsub>K vv Suc n\<^esub>) j^\<^bsup>K N\<^esup>)^\<^bsup>K N\<^esup>)) Suc n \<plusminus> -\<^sub>a x j)
[PROOF STEP]
apply (erule exE)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>l. \<lbrakk>vals_nonequiv K (Suc n) vv; \<forall>j\<le>Suc n. x j \<in> carrier K; Ring K; aGroup K; \<forall>N>l. \<forall>j\<le>Suc n. an m \<le> vv j (\<Sigma>\<^sub>e K (\<lambda>j\<in>{h. h \<le> Suc n}. x j \<cdot>\<^sub>r (1\<^sub>r \<plusminus> -\<^sub>a (1\<^sub>r \<plusminus> -\<^sub>a (\<Omega>\<^bsub>K vv Suc n\<^esub>) j^\<^bsup>K N\<^esup>)^\<^bsup>K N\<^esup>)) Suc n \<plusminus> -\<^sub>a x j)\<rbrakk> \<Longrightarrow> \<exists>y\<in>carrier K. \<forall>j\<le>Suc n. an m \<le> vv j (y \<plusminus> -\<^sub>a x j)
 2. \<lbrakk>vals_nonequiv K (Suc n) vv; \<forall>j\<le>Suc n. x j \<in> carrier K; Ring K; aGroup K\<rbrakk> \<Longrightarrow> \<exists>l. \<forall>N>l. \<forall>j\<le>Suc n. an m \<le> vv j (\<Sigma>\<^sub>e K (\<lambda>j\<in>{h. h \<le> Suc n}. x j \<cdot>\<^sub>r (1\<^sub>r \<plusminus> -\<^sub>a (1\<^sub>r \<plusminus> -\<^sub>a (\<Omega>\<^bsub>K vv Suc n\<^esub>) j^\<^bsup>K N\<^esup>)^\<^bsup>K N\<^esup>)) Suc n \<plusminus> -\<^sub>a x j)
[PROOF STEP]
apply (rename_tac M)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>M. \<lbrakk>vals_nonequiv K (Suc n) vv; \<forall>j\<le>Suc n. x j \<in> carrier K; Ring K; aGroup K; \<forall>N>M. \<forall>j\<le>Suc n. an m \<le> vv j (\<Sigma>\<^sub>e K (\<lambda>j\<in>{h. h \<le> Suc n}. x j \<cdot>\<^sub>r (1\<^sub>r \<plusminus> -\<^sub>a (1\<^sub>r \<plusminus> -\<^sub>a (\<Omega>\<^bsub>K vv Suc n\<^esub>) j^\<^bsup>K N\<^esup>)^\<^bsup>K N\<^esup>)) Suc n \<plusminus> -\<^sub>a x j)\<rbrakk> \<Longrightarrow> \<exists>y\<in>carrier K. \<forall>j\<le>Suc n. an m \<le> vv j (y \<plusminus> -\<^sub>a x j)
 2. \<lbrakk>vals_nonequiv K (Suc n) vv; \<forall>j\<le>Suc n. x j \<in> carrier K; Ring K; aGroup K\<rbrakk> \<Longrightarrow> \<exists>l. \<forall>N>l. \<forall>j\<le>Suc n. an m \<le> vv j (\<Sigma>\<^sub>e K (\<lambda>j\<in>{h. h \<le> Suc n}. x j \<cdot>\<^sub>r (1\<^sub>r \<plusminus> -\<^sub>a (1\<^sub>r \<plusminus> -\<^sub>a (\<Omega>\<^bsub>K vv Suc n\<^esub>) j^\<^bsup>K N\<^esup>)^\<^bsup>K N\<^esup>)) Suc n \<plusminus> -\<^sub>a x j)
[PROOF STEP]
apply (subgoal_tac "\<forall>j\<le> (Suc n). (an m) \<le>
 (vv j ( (\<Sigma>\<^sub>e K (\<lambda>j\<in>{h. h \<le> (Suc n)}. (x j) \<cdot>\<^sub>r (1\<^sub>r \<plusminus> -\<^sub>a (1\<^sub>r \<plusminus>
  -\<^sub>a ((\<Omega>\<^bsub>K vv (Suc n)\<^esub>) j)^\<^bsup>K (Suc M)\<^esup>)^\<^bsup>K (Suc M)\<^esup>)) (Suc n)) \<plusminus> -\<^sub>a (x j)))")
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>M. \<lbrakk>vals_nonequiv K (Suc n) vv; \<forall>j\<le>Suc n. x j \<in> carrier K; Ring K; aGroup K; \<forall>N>M. \<forall>j\<le>Suc n. an m \<le> vv j (\<Sigma>\<^sub>e K (\<lambda>j\<in>{h. h \<le> Suc n}. x j \<cdot>\<^sub>r (1\<^sub>r \<plusminus> -\<^sub>a (1\<^sub>r \<plusminus> -\<^sub>a (\<Omega>\<^bsub>K vv Suc n\<^esub>) j^\<^bsup>K N\<^esup>)^\<^bsup>K N\<^esup>)) Suc n \<plusminus> -\<^sub>a x j); \<forall>j\<le>Suc n. an m \<le> vv j (\<Sigma>\<^sub>e K (\<lambda>j\<in>{h. h \<le> Suc n}. x j \<cdot>\<^sub>r (1\<^sub>r \<plusminus> -\<^sub>a (1\<^sub>r \<plusminus> -\<^sub>a (\<Omega>\<^bsub>K vv Suc n\<^esub>) j^\<^bsup>K Suc M\<^esup>)^\<^bsup>K Suc M\<^esup>)) Suc n \<plusminus> -\<^sub>a x j)\<rbrakk> \<Longrightarrow> \<exists>y\<in>carrier K. \<forall>j\<le>Suc n. an m \<le> vv j (y \<plusminus> -\<^sub>a x j)
 2. \<And>M. \<lbrakk>vals_nonequiv K (Suc n) vv; \<forall>j\<le>Suc n. x j \<in> carrier K; Ring K; aGroup K; \<forall>N>M. \<forall>j\<le>Suc n. an m \<le> vv j (\<Sigma>\<^sub>e K (\<lambda>j\<in>{h. h \<le> Suc n}. x j \<cdot>\<^sub>r (1\<^sub>r \<plusminus> -\<^sub>a (1\<^sub>r \<plusminus> -\<^sub>a (\<Omega>\<^bsub>K vv Suc n\<^esub>) j^\<^bsup>K N\<^esup>)^\<^bsup>K N\<^esup>)) Suc n \<plusminus> -\<^sub>a x j)\<rbrakk> \<Longrightarrow> \<forall>j\<le>Suc n. an m \<le> vv j (\<Sigma>\<^sub>e K (\<lambda>j\<in>{h. h \<le> Suc n}. x j \<cdot>\<^sub>r (1\<^sub>r \<plusminus> -\<^sub>a (1\<^sub>r \<plusminus> -\<^sub>a (\<Omega>\<^bsub>K vv Suc n\<^esub>) j^\<^bsup>K Suc M\<^esup>)^\<^bsup>K Suc M\<^esup>)) Suc n \<plusminus> -\<^sub>a x j)
 3. \<lbrakk>vals_nonequiv K (Suc n) vv; \<forall>j\<le>Suc n. x j \<in> carrier K; Ring K; aGroup K\<rbrakk> \<Longrightarrow> \<exists>l. \<forall>N>l. \<forall>j\<le>Suc n. an m \<le> vv j (\<Sigma>\<^sub>e K (\<lambda>j\<in>{h. h \<le> Suc n}. x j \<cdot>\<^sub>r (1\<^sub>r \<plusminus> -\<^sub>a (1\<^sub>r \<plusminus> -\<^sub>a (\<Omega>\<^bsub>K vv Suc n\<^esub>) j^\<^bsup>K N\<^esup>)^\<^bsup>K N\<^esup>)) Suc n \<plusminus> -\<^sub>a x j)
[PROOF STEP]
apply (subgoal_tac "\<Sigma>\<^sub>e K (\<lambda>j\<in>{h. h \<le> (Suc n)}. (x j) \<cdot>\<^sub>r (1\<^sub>r \<plusminus>
 -\<^sub>a (1\<^sub>r \<plusminus> -\<^sub>a ((\<Omega>\<^bsub>K vv (Suc n)\<^esub>) j)^\<^bsup>K (Suc M)\<^esup>)^\<^bsup>K (Suc M)\<^esup>)) (Suc n) \<in> carrier K")
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<And>M. \<lbrakk>vals_nonequiv K (Suc n) vv; \<forall>j\<le>Suc n. x j \<in> carrier K; Ring K; aGroup K; \<forall>N>M. \<forall>j\<le>Suc n. an m \<le> vv j (\<Sigma>\<^sub>e K (\<lambda>j\<in>{h. h \<le> Suc n}. x j \<cdot>\<^sub>r (1\<^sub>r \<plusminus> -\<^sub>a (1\<^sub>r \<plusminus> -\<^sub>a (\<Omega>\<^bsub>K vv Suc n\<^esub>) j^\<^bsup>K N\<^esup>)^\<^bsup>K N\<^esup>)) Suc n \<plusminus> -\<^sub>a x j); \<forall>j\<le>Suc n. an m \<le> vv j (\<Sigma>\<^sub>e K (\<lambda>j\<in>{h. h \<le> Suc n}. x j \<cdot>\<^sub>r (1\<^sub>r \<plusminus> -\<^sub>a (1\<^sub>r \<plusminus> -\<^sub>a (\<Omega>\<^bsub>K vv Suc n\<^esub>) j^\<^bsup>K Suc M\<^esup>)^\<^bsup>K Suc M\<^esup>)) Suc n \<plusminus> -\<^sub>a x j); \<Sigma>\<^sub>e K (\<lambda>j\<in>{h. h \<le> Suc n}. x j \<cdot>\<^sub>r (1\<^sub>r \<plusminus> -\<^sub>a (1\<^sub>r \<plusminus> -\<^sub>a (\<Omega>\<^bsub>K vv Suc n\<^esub>) j^\<^bsup>K Suc M\<^esup>)^\<^bsup>K Suc M\<^esup>)) Suc n \<in> carrier K\<rbrakk> \<Longrightarrow> \<exists>y\<in>carrier K. \<forall>j\<le>Suc n. an m \<le> vv j (y \<plusminus> -\<^sub>a x j)
 2. \<And>M. \<lbrakk>vals_nonequiv K (Suc n) vv; \<forall>j\<le>Suc n. x j \<in> carrier K; Ring K; aGroup K; \<forall>N>M. \<forall>j\<le>Suc n. an m \<le> vv j (\<Sigma>\<^sub>e K (\<lambda>j\<in>{h. h \<le> Suc n}. x j \<cdot>\<^sub>r (1\<^sub>r \<plusminus> -\<^sub>a (1\<^sub>r \<plusminus> -\<^sub>a (\<Omega>\<^bsub>K vv Suc n\<^esub>) j^\<^bsup>K N\<^esup>)^\<^bsup>K N\<^esup>)) Suc n \<plusminus> -\<^sub>a x j); \<forall>j\<le>Suc n. an m \<le> vv j (\<Sigma>\<^sub>e K (\<lambda>j\<in>{h. h \<le> Suc n}. x j \<cdot>\<^sub>r (1\<^sub>r \<plusminus> -\<^sub>a (1\<^sub>r \<plusminus> -\<^sub>a (\<Omega>\<^bsub>K vv Suc n\<^esub>) j^\<^bsup>K Suc M\<^esup>)^\<^bsup>K Suc M\<^esup>)) Suc n \<plusminus> -\<^sub>a x j)\<rbrakk> \<Longrightarrow> \<Sigma>\<^sub>e K (\<lambda>j\<in>{h. h \<le> Suc n}. x j \<cdot>\<^sub>r (1\<^sub>r \<plusminus> -\<^sub>a (1\<^sub>r \<plusminus> -\<^sub>a (\<Omega>\<^bsub>K vv Suc n\<^esub>) j^\<^bsup>K Suc M\<^esup>)^\<^bsup>K Suc M\<^esup>)) Suc n \<in> carrier K
 3. \<And>M. \<lbrakk>vals_nonequiv K (Suc n) vv; \<forall>j\<le>Suc n. x j \<in> carrier K; Ring K; aGroup K; \<forall>N>M. \<forall>j\<le>Suc n. an m \<le> vv j (\<Sigma>\<^sub>e K (\<lambda>j\<in>{h. h \<le> Suc n}. x j \<cdot>\<^sub>r (1\<^sub>r \<plusminus> -\<^sub>a (1\<^sub>r \<plusminus> -\<^sub>a (\<Omega>\<^bsub>K vv Suc n\<^esub>) j^\<^bsup>K N\<^esup>)^\<^bsup>K N\<^esup>)) Suc n \<plusminus> -\<^sub>a x j)\<rbrakk> \<Longrightarrow> \<forall>j\<le>Suc n. an m \<le> vv j (\<Sigma>\<^sub>e K (\<lambda>j\<in>{h. h \<le> Suc n}. x j \<cdot>\<^sub>r (1\<^sub>r \<plusminus> -\<^sub>a (1\<^sub>r \<plusminus> -\<^sub>a (\<Omega>\<^bsub>K vv Suc n\<^esub>) j^\<^bsup>K Suc M\<^esup>)^\<^bsup>K Suc M\<^esup>)) Suc n \<plusminus> -\<^sub>a x j)
 4. \<lbrakk>vals_nonequiv K (Suc n) vv; \<forall>j\<le>Suc n. x j \<in> carrier K; Ring K; aGroup K\<rbrakk> \<Longrightarrow> \<exists>l. \<forall>N>l. \<forall>j\<le>Suc n. an m \<le> vv j (\<Sigma>\<^sub>e K (\<lambda>j\<in>{h. h \<le> Suc n}. x j \<cdot>\<^sub>r (1\<^sub>r \<plusminus> -\<^sub>a (1\<^sub>r \<plusminus> -\<^sub>a (\<Omega>\<^bsub>K vv Suc n\<^esub>) j^\<^bsup>K N\<^esup>)^\<^bsup>K N\<^esup>)) Suc n \<plusminus> -\<^sub>a x j)
[PROOF STEP]
apply blast
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>M. \<lbrakk>vals_nonequiv K (Suc n) vv; \<forall>j\<le>Suc n. x j \<in> carrier K; Ring K; aGroup K; \<forall>N>M. \<forall>j\<le>Suc n. an m \<le> vv j (\<Sigma>\<^sub>e K (\<lambda>j\<in>{h. h \<le> Suc n}. x j \<cdot>\<^sub>r (1\<^sub>r \<plusminus> -\<^sub>a (1\<^sub>r \<plusminus> -\<^sub>a (\<Omega>\<^bsub>K vv Suc n\<^esub>) j^\<^bsup>K N\<^esup>)^\<^bsup>K N\<^esup>)) Suc n \<plusminus> -\<^sub>a x j); \<forall>j\<le>Suc n. an m \<le> vv j (\<Sigma>\<^sub>e K (\<lambda>j\<in>{h. h \<le> Suc n}. x j \<cdot>\<^sub>r (1\<^sub>r \<plusminus> -\<^sub>a (1\<^sub>r \<plusminus> -\<^sub>a (\<Omega>\<^bsub>K vv Suc n\<^esub>) j^\<^bsup>K Suc M\<^esup>)^\<^bsup>K Suc M\<^esup>)) Suc n \<plusminus> -\<^sub>a x j)\<rbrakk> \<Longrightarrow> \<Sigma>\<^sub>e K (\<lambda>j\<in>{h. h \<le> Suc n}. x j \<cdot>\<^sub>r (1\<^sub>r \<plusminus> -\<^sub>a (1\<^sub>r \<plusminus> -\<^sub>a (\<Omega>\<^bsub>K vv Suc n\<^esub>) j^\<^bsup>K Suc M\<^esup>)^\<^bsup>K Suc M\<^esup>)) Suc n \<in> carrier K
 2. \<And>M. \<lbrakk>vals_nonequiv K (Suc n) vv; \<forall>j\<le>Suc n. x j \<in> carrier K; Ring K; aGroup K; \<forall>N>M. \<forall>j\<le>Suc n. an m \<le> vv j (\<Sigma>\<^sub>e K (\<lambda>j\<in>{h. h \<le> Suc n}. x j \<cdot>\<^sub>r (1\<^sub>r \<plusminus> -\<^sub>a (1\<^sub>r \<plusminus> -\<^sub>a (\<Omega>\<^bsub>K vv Suc n\<^esub>) j^\<^bsup>K N\<^esup>)^\<^bsup>K N\<^esup>)) Suc n \<plusminus> -\<^sub>a x j)\<rbrakk> \<Longrightarrow> \<forall>j\<le>Suc n. an m \<le> vv j (\<Sigma>\<^sub>e K (\<lambda>j\<in>{h. h \<le> Suc n}. x j \<cdot>\<^sub>r (1\<^sub>r \<plusminus> -\<^sub>a (1\<^sub>r \<plusminus> -\<^sub>a (\<Omega>\<^bsub>K vv Suc n\<^esub>) j^\<^bsup>K Suc M\<^esup>)^\<^bsup>K Suc M\<^esup>)) Suc n \<plusminus> -\<^sub>a x j)
 3. \<lbrakk>vals_nonequiv K (Suc n) vv; \<forall>j\<le>Suc n. x j \<in> carrier K; Ring K; aGroup K\<rbrakk> \<Longrightarrow> \<exists>l. \<forall>N>l. \<forall>j\<le>Suc n. an m \<le> vv j (\<Sigma>\<^sub>e K (\<lambda>j\<in>{h. h \<le> Suc n}. x j \<cdot>\<^sub>r (1\<^sub>r \<plusminus> -\<^sub>a (1\<^sub>r \<plusminus> -\<^sub>a (\<Omega>\<^bsub>K vv Suc n\<^esub>) j^\<^bsup>K N\<^esup>)^\<^bsup>K N\<^esup>)) Suc n \<plusminus> -\<^sub>a x j)
[PROOF STEP]
apply (rule aGroup.nsum_mem[of "K" "Suc n"], assumption+)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>M. \<lbrakk>vals_nonequiv K (Suc n) vv; \<forall>j\<le>Suc n. x j \<in> carrier K; Ring K; aGroup K; \<forall>N>M. \<forall>j\<le>Suc n. an m \<le> vv j (\<Sigma>\<^sub>e K (\<lambda>j\<in>{h. h \<le> Suc n}. x j \<cdot>\<^sub>r (1\<^sub>r \<plusminus> -\<^sub>a (1\<^sub>r \<plusminus> -\<^sub>a (\<Omega>\<^bsub>K vv Suc n\<^esub>) j^\<^bsup>K N\<^esup>)^\<^bsup>K N\<^esup>)) Suc n \<plusminus> -\<^sub>a x j); \<forall>j\<le>Suc n. an m \<le> vv j (\<Sigma>\<^sub>e K (\<lambda>j\<in>{h. h \<le> Suc n}. x j \<cdot>\<^sub>r (1\<^sub>r \<plusminus> -\<^sub>a (1\<^sub>r \<plusminus> -\<^sub>a (\<Omega>\<^bsub>K vv Suc n\<^esub>) j^\<^bsup>K Suc M\<^esup>)^\<^bsup>K Suc M\<^esup>)) Suc n \<plusminus> -\<^sub>a x j)\<rbrakk> \<Longrightarrow> \<forall>j\<le>Suc n. (\<lambda>j\<in>{h. h \<le> Suc n}. x j \<cdot>\<^sub>r (1\<^sub>r \<plusminus> -\<^sub>a (1\<^sub>r \<plusminus> -\<^sub>a (\<Omega>\<^bsub>K vv Suc n\<^esub>) j^\<^bsup>K Suc M\<^esup>)^\<^bsup>K Suc M\<^esup>)) j \<in> carrier K
 2. \<And>M. \<lbrakk>vals_nonequiv K (Suc n) vv; \<forall>j\<le>Suc n. x j \<in> carrier K; Ring K; aGroup K; \<forall>N>M. \<forall>j\<le>Suc n. an m \<le> vv j (\<Sigma>\<^sub>e K (\<lambda>j\<in>{h. h \<le> Suc n}. x j \<cdot>\<^sub>r (1\<^sub>r \<plusminus> -\<^sub>a (1\<^sub>r \<plusminus> -\<^sub>a (\<Omega>\<^bsub>K vv Suc n\<^esub>) j^\<^bsup>K N\<^esup>)^\<^bsup>K N\<^esup>)) Suc n \<plusminus> -\<^sub>a x j)\<rbrakk> \<Longrightarrow> \<forall>j\<le>Suc n. an m \<le> vv j (\<Sigma>\<^sub>e K (\<lambda>j\<in>{h. h \<le> Suc n}. x j \<cdot>\<^sub>r (1\<^sub>r \<plusminus> -\<^sub>a (1\<^sub>r \<plusminus> -\<^sub>a (\<Omega>\<^bsub>K vv Suc n\<^esub>) j^\<^bsup>K Suc M\<^esup>)^\<^bsup>K Suc M\<^esup>)) Suc n \<plusminus> -\<^sub>a x j)
 3. \<lbrakk>vals_nonequiv K (Suc n) vv; \<forall>j\<le>Suc n. x j \<in> carrier K; Ring K; aGroup K\<rbrakk> \<Longrightarrow> \<exists>l. \<forall>N>l. \<forall>j\<le>Suc n. an m \<le> vv j (\<Sigma>\<^sub>e K (\<lambda>j\<in>{h. h \<le> Suc n}. x j \<cdot>\<^sub>r (1\<^sub>r \<plusminus> -\<^sub>a (1\<^sub>r \<plusminus> -\<^sub>a (\<Omega>\<^bsub>K vv Suc n\<^esub>) j^\<^bsup>K N\<^esup>)^\<^bsup>K N\<^esup>)) Suc n \<plusminus> -\<^sub>a x j)
[PROOF STEP]
apply (rule allI, rule impI, simp del:nsum_suc npow_suc)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>M j. \<lbrakk>vals_nonequiv K (Suc n) vv; \<forall>j\<le>Suc n. x j \<in> carrier K; Ring K; aGroup K; \<forall>N>M. \<forall>j\<le>Suc n. an m \<le> vv j (\<Sigma>\<^sub>e K (\<lambda>j\<in>{h. h \<le> Suc n}. x j \<cdot>\<^sub>r (1\<^sub>r \<plusminus> -\<^sub>a (1\<^sub>r \<plusminus> -\<^sub>a (\<Omega>\<^bsub>K vv Suc n\<^esub>) j^\<^bsup>K N\<^esup>)^\<^bsup>K N\<^esup>)) Suc n \<plusminus> -\<^sub>a x j); j \<le> Suc n\<rbrakk> \<Longrightarrow> x j \<cdot>\<^sub>r (1\<^sub>r \<plusminus> -\<^sub>a (1\<^sub>r \<plusminus> -\<^sub>a (\<Omega>\<^bsub>K vv Suc n\<^esub>) j^\<^bsup>K Suc M\<^esup>)^\<^bsup>K Suc M\<^esup>) \<in> carrier K
 2. \<And>M. \<lbrakk>vals_nonequiv K (Suc n) vv; \<forall>j\<le>Suc n. x j \<in> carrier K; Ring K; aGroup K; \<forall>N>M. \<forall>j\<le>Suc n. an m \<le> vv j (\<Sigma>\<^sub>e K (\<lambda>j\<in>{h. h \<le> Suc n}. x j \<cdot>\<^sub>r (1\<^sub>r \<plusminus> -\<^sub>a (1\<^sub>r \<plusminus> -\<^sub>a (\<Omega>\<^bsub>K vv Suc n\<^esub>) j^\<^bsup>K N\<^esup>)^\<^bsup>K N\<^esup>)) Suc n \<plusminus> -\<^sub>a x j)\<rbrakk> \<Longrightarrow> \<forall>j\<le>Suc n. an m \<le> vv j (\<Sigma>\<^sub>e K (\<lambda>j\<in>{h. h \<le> Suc n}. x j \<cdot>\<^sub>r (1\<^sub>r \<plusminus> -\<^sub>a (1\<^sub>r \<plusminus> -\<^sub>a (\<Omega>\<^bsub>K vv Suc n\<^esub>) j^\<^bsup>K Suc M\<^esup>)^\<^bsup>K Suc M\<^esup>)) Suc n \<plusminus> -\<^sub>a x j)
 3. \<lbrakk>vals_nonequiv K (Suc n) vv; \<forall>j\<le>Suc n. x j \<in> carrier K; Ring K; aGroup K\<rbrakk> \<Longrightarrow> \<exists>l. \<forall>N>l. \<forall>j\<le>Suc n. an m \<le> vv j (\<Sigma>\<^sub>e K (\<lambda>j\<in>{h. h \<le> Suc n}. x j \<cdot>\<^sub>r (1\<^sub>r \<plusminus> -\<^sub>a (1\<^sub>r \<plusminus> -\<^sub>a (\<Omega>\<^bsub>K vv Suc n\<^esub>) j^\<^bsup>K N\<^esup>)^\<^bsup>K N\<^esup>)) Suc n \<plusminus> -\<^sub>a x j)
[PROOF STEP]
apply (rule Ring.ring_tOp_closed, assumption+, simp,
        rule ApproximationTr1, simp add:Ostrowski_base_mem)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>M. \<lbrakk>vals_nonequiv K (Suc n) vv; \<forall>j\<le>Suc n. x j \<in> carrier K; Ring K; aGroup K; \<forall>N>M. \<forall>j\<le>Suc n. an m \<le> vv j (\<Sigma>\<^sub>e K (\<lambda>j\<in>{h. h \<le> Suc n}. x j \<cdot>\<^sub>r (1\<^sub>r \<plusminus> -\<^sub>a (1\<^sub>r \<plusminus> -\<^sub>a (\<Omega>\<^bsub>K vv Suc n\<^esub>) j^\<^bsup>K N\<^esup>)^\<^bsup>K N\<^esup>)) Suc n \<plusminus> -\<^sub>a x j)\<rbrakk> \<Longrightarrow> \<forall>j\<le>Suc n. an m \<le> vv j (\<Sigma>\<^sub>e K (\<lambda>j\<in>{h. h \<le> Suc n}. x j \<cdot>\<^sub>r (1\<^sub>r \<plusminus> -\<^sub>a (1\<^sub>r \<plusminus> -\<^sub>a (\<Omega>\<^bsub>K vv Suc n\<^esub>) j^\<^bsup>K Suc M\<^esup>)^\<^bsup>K Suc M\<^esup>)) Suc n \<plusminus> -\<^sub>a x j)
 2. \<lbrakk>vals_nonequiv K (Suc n) vv; \<forall>j\<le>Suc n. x j \<in> carrier K; Ring K; aGroup K\<rbrakk> \<Longrightarrow> \<exists>l. \<forall>N>l. \<forall>j\<le>Suc n. an m \<le> vv j (\<Sigma>\<^sub>e K (\<lambda>j\<in>{h. h \<le> Suc n}. x j \<cdot>\<^sub>r (1\<^sub>r \<plusminus> -\<^sub>a (1\<^sub>r \<plusminus> -\<^sub>a (\<Omega>\<^bsub>K vv Suc n\<^esub>) j^\<^bsup>K N\<^esup>)^\<^bsup>K N\<^esup>)) Suc n \<plusminus> -\<^sub>a x j)
[PROOF STEP]
apply (subgoal_tac "M < Suc M")
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>M. \<lbrakk>vals_nonequiv K (Suc n) vv; \<forall>j\<le>Suc n. x j \<in> carrier K; Ring K; aGroup K; \<forall>N>M. \<forall>j\<le>Suc n. an m \<le> vv j (\<Sigma>\<^sub>e K (\<lambda>j\<in>{h. h \<le> Suc n}. x j \<cdot>\<^sub>r (1\<^sub>r \<plusminus> -\<^sub>a (1\<^sub>r \<plusminus> -\<^sub>a (\<Omega>\<^bsub>K vv Suc n\<^esub>) j^\<^bsup>K N\<^esup>)^\<^bsup>K N\<^esup>)) Suc n \<plusminus> -\<^sub>a x j); M < Suc M\<rbrakk> \<Longrightarrow> \<forall>j\<le>Suc n. an m \<le> vv j (\<Sigma>\<^sub>e K (\<lambda>j\<in>{h. h \<le> Suc n}. x j \<cdot>\<^sub>r (1\<^sub>r \<plusminus> -\<^sub>a (1\<^sub>r \<plusminus> -\<^sub>a (\<Omega>\<^bsub>K vv Suc n\<^esub>) j^\<^bsup>K Suc M\<^esup>)^\<^bsup>K Suc M\<^esup>)) Suc n \<plusminus> -\<^sub>a x j)
 2. \<And>M. \<lbrakk>vals_nonequiv K (Suc n) vv; \<forall>j\<le>Suc n. x j \<in> carrier K; Ring K; aGroup K; \<forall>N>M. \<forall>j\<le>Suc n. an m \<le> vv j (\<Sigma>\<^sub>e K (\<lambda>j\<in>{h. h \<le> Suc n}. x j \<cdot>\<^sub>r (1\<^sub>r \<plusminus> -\<^sub>a (1\<^sub>r \<plusminus> -\<^sub>a (\<Omega>\<^bsub>K vv Suc n\<^esub>) j^\<^bsup>K N\<^esup>)^\<^bsup>K N\<^esup>)) Suc n \<plusminus> -\<^sub>a x j)\<rbrakk> \<Longrightarrow> M < Suc M
 3. \<lbrakk>vals_nonequiv K (Suc n) vv; \<forall>j\<le>Suc n. x j \<in> carrier K; Ring K; aGroup K\<rbrakk> \<Longrightarrow> \<exists>l. \<forall>N>l. \<forall>j\<le>Suc n. an m \<le> vv j (\<Sigma>\<^sub>e K (\<lambda>j\<in>{h. h \<le> Suc n}. x j \<cdot>\<^sub>r (1\<^sub>r \<plusminus> -\<^sub>a (1\<^sub>r \<plusminus> -\<^sub>a (\<Omega>\<^bsub>K vv Suc n\<^esub>) j^\<^bsup>K N\<^esup>)^\<^bsup>K N\<^esup>)) Suc n \<plusminus> -\<^sub>a x j)
[PROOF STEP]
apply blast
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>M. \<lbrakk>vals_nonequiv K (Suc n) vv; \<forall>j\<le>Suc n. x j \<in> carrier K; Ring K; aGroup K; \<forall>N>M. \<forall>j\<le>Suc n. an m \<le> vv j (\<Sigma>\<^sub>e K (\<lambda>j\<in>{h. h \<le> Suc n}. x j \<cdot>\<^sub>r (1\<^sub>r \<plusminus> -\<^sub>a (1\<^sub>r \<plusminus> -\<^sub>a (\<Omega>\<^bsub>K vv Suc n\<^esub>) j^\<^bsup>K N\<^esup>)^\<^bsup>K N\<^esup>)) Suc n \<plusminus> -\<^sub>a x j)\<rbrakk> \<Longrightarrow> M < Suc M
 2. \<lbrakk>vals_nonequiv K (Suc n) vv; \<forall>j\<le>Suc n. x j \<in> carrier K; Ring K; aGroup K\<rbrakk> \<Longrightarrow> \<exists>l. \<forall>N>l. \<forall>j\<le>Suc n. an m \<le> vv j (\<Sigma>\<^sub>e K (\<lambda>j\<in>{h. h \<le> Suc n}. x j \<cdot>\<^sub>r (1\<^sub>r \<plusminus> -\<^sub>a (1\<^sub>r \<plusminus> -\<^sub>a (\<Omega>\<^bsub>K vv Suc n\<^esub>) j^\<^bsup>K N\<^esup>)^\<^bsup>K N\<^esup>)) Suc n \<plusminus> -\<^sub>a x j)
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>vals_nonequiv K (Suc n) vv; \<forall>j\<le>Suc n. x j \<in> carrier K; Ring K; aGroup K\<rbrakk> \<Longrightarrow> \<exists>l. \<forall>N>l. \<forall>j\<le>Suc n. an m \<le> vv j (\<Sigma>\<^sub>e K (\<lambda>j\<in>{h. h \<le> Suc n}. x j \<cdot>\<^sub>r (1\<^sub>r \<plusminus> -\<^sub>a (1\<^sub>r \<plusminus> -\<^sub>a (\<Omega>\<^bsub>K vv Suc n\<^esub>) j^\<^bsup>K N\<^esup>)^\<^bsup>K N\<^esup>)) Suc n \<plusminus> -\<^sub>a x j)
[PROOF STEP]
apply (rule ApplicationTr4[of n vv x], assumption+)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>vals_nonequiv K (Suc n) vv; \<forall>j\<le>Suc n. x j \<in> carrier K; Ring K; aGroup K\<rbrakk> \<Longrightarrow> \<forall>j\<in>{h. h \<le> Suc n}. x j \<in> carrier K
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma (in Corps) distinct_pds_restriction:"\<lbrakk>distinct_pds K (Suc n) P\<rbrakk> \<Longrightarrow>
       distinct_pds K n P"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. distinct_pds K (Suc n) P \<Longrightarrow> distinct_pds K n P
[PROOF STEP]
apply (simp add:distinct_pds_def)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma (in Corps) distinct_pds_valuation:"\<lbrakk>j \<le> (Suc n);
       distinct_pds K (Suc n) P\<rbrakk> \<Longrightarrow>  valuation K (\<nu>\<^bsub>K (P j)\<^esub>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>j \<le> Suc n; distinct_pds K (Suc n) P\<rbrakk> \<Longrightarrow> valuation K (\<nu>\<^bsub>K P j\<^esub>)
[PROOF STEP]
apply (rule_tac P = "P j" in representative_of_pd_valuation)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>j \<le> Suc n; distinct_pds K (Suc n) P\<rbrakk> \<Longrightarrow> P j \<in> Pds
[PROOF STEP]
apply (simp add:distinct_pds_def)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma (in Corps) distinct_pds_valuation1:"\<lbrakk>0 < n; j \<le> n; distinct_pds K n P\<rbrakk>
 \<Longrightarrow>  valuation K (\<nu>\<^bsub>K (P j)\<^esub>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>0 < n; j \<le> n; distinct_pds K n P\<rbrakk> \<Longrightarrow> valuation K (\<nu>\<^bsub>K P j\<^esub>)
[PROOF STEP]
apply (rule distinct_pds_valuation[of "j" "n - Suc 0" "P"])
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>0 < n; j \<le> n; distinct_pds K n P\<rbrakk> \<Longrightarrow> j \<le> Suc (n - Suc 0)
 2. \<lbrakk>0 < n; j \<le> n; distinct_pds K n P\<rbrakk> \<Longrightarrow> distinct_pds K (Suc (n - Suc 0)) P
[PROOF STEP]
apply simp+
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma (in Corps) distinct_pds_valuation2:"\<lbrakk>j \<le> n; distinct_pds K n P\<rbrakk> \<Longrightarrow>
          valuation K (\<nu>\<^bsub>K (P j)\<^esub>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>j \<le> n; distinct_pds K n P\<rbrakk> \<Longrightarrow> valuation K (\<nu>\<^bsub>K P j\<^esub>)
[PROOF STEP]
apply (case_tac "n = 0",
       simp add:distinct_pds_def,
       subgoal_tac "0 \<in> {0::nat}",
       simp add:representative_of_pd_valuation[of "P 0"],
       simp)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>j \<le> n; distinct_pds K n P; n \<noteq> 0\<rbrakk> \<Longrightarrow> valuation K (\<nu>\<^bsub>K P j\<^esub>)
[PROOF STEP]
apply (simp add:distinct_pds_valuation1[of "n"])
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma (in Corps) ring_n_pd:"distinct_pds K n P \<Longrightarrow> Ring (O\<^bsub>K P n\<^esub>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. distinct_pds K n P \<Longrightarrow> Ring (O\<^bsub>K P n\<^esub>)
[PROOF STEP]
by (simp add:ring_n_pd_def, simp add:ring_n_distinct_prime_divisors)


[STATEMENT]
lemma (in Corps) ring_n_pd_Suc:"distinct_pds K (Suc n) P \<Longrightarrow>
          carrier (O\<^bsub> K P (Suc n)\<^esub>) \<subseteq> carrier (O\<^bsub>K P n\<^esub>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. distinct_pds K (Suc n) P \<Longrightarrow> carrier (O\<^bsub>K P Suc n\<^esub>) \<subseteq> carrier (O\<^bsub>K P n\<^esub>)
[PROOF STEP]
apply (rule subsetI)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>distinct_pds K (Suc n) P; x \<in> carrier (O\<^bsub>K P Suc n\<^esub>)\<rbrakk> \<Longrightarrow> x \<in> carrier (O\<^bsub>K P n\<^esub>)
[PROOF STEP]
apply (simp add:ring_n_pd_def Sr_def)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma (in Corps) ring_n_pd_pOp_K_pOp:"\<lbrakk>distinct_pds K n P; x\<in>carrier (O\<^bsub>K P n\<^esub>);
 y \<in> carrier (O\<^bsub>K P n\<^esub>)\<rbrakk>  \<Longrightarrow> x \<plusminus>\<^bsub>(O\<^bsub>K P n\<^esub>)\<^esub> y = x \<plusminus> y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>distinct_pds K n P; x \<in> carrier (O\<^bsub>K P n\<^esub>); y \<in> carrier (O\<^bsub>K P n\<^esub>)\<rbrakk> \<Longrightarrow> x \<plusminus>\<^bsub>O\<^bsub>K P n\<^esub>\<^esub> y = x \<plusminus> y
[PROOF STEP]
apply (simp add:ring_n_pd_def Sr_def)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma (in Corps) ring_n_pd_tOp_K_tOp:"\<lbrakk>distinct_pds K n P; x \<in>carrier (O\<^bsub>K P n\<^esub>);
      y \<in> carrier (O\<^bsub>K P n\<^esub>)\<rbrakk> \<Longrightarrow>  x \<cdot>\<^sub>r\<^bsub>(O\<^bsub>K P n\<^esub>)\<^esub> y = x \<cdot>\<^sub>r y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>distinct_pds K n P; x \<in> carrier (O\<^bsub>K P n\<^esub>); y \<in> carrier (O\<^bsub>K P n\<^esub>)\<rbrakk> \<Longrightarrow> x \<cdot>\<^sub>r\<^bsub>O\<^bsub>K P n\<^esub>\<^esub> y = x \<cdot>\<^sub>r y
[PROOF STEP]
apply (simp add:ring_n_pd_def Sr_def)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma (in Corps) ring_n_eSum_K_eSumTr:"distinct_pds K n P \<Longrightarrow>
  (\<forall>j\<le>m. f j \<in> carrier (O\<^bsub>K P n\<^esub>)) \<longrightarrow> nsum (O\<^bsub>K P n\<^esub>) f m = nsum K f m"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. distinct_pds K n P \<Longrightarrow> (\<forall>j\<le>m. f j \<in> carrier (O\<^bsub>K P n\<^esub>)) \<longrightarrow> \<Sigma>\<^sub>e O\<^bsub>K P n\<^esub> f m = \<Sigma>\<^sub>e K f m
[PROOF STEP]
apply (induct_tac m)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. distinct_pds K n P \<Longrightarrow> (\<forall>j\<le>0. f j \<in> carrier (O\<^bsub>K P n\<^esub>)) \<longrightarrow> \<Sigma>\<^sub>e O\<^bsub>K P n\<^esub> f 0 = \<Sigma>\<^sub>e K f 0
 2. \<And>na. \<lbrakk>distinct_pds K n P; (\<forall>j\<le>na. f j \<in> carrier (O\<^bsub>K P n\<^esub>)) \<longrightarrow> \<Sigma>\<^sub>e O\<^bsub>K P n\<^esub> f na = \<Sigma>\<^sub>e K f na\<rbrakk> \<Longrightarrow> (\<forall>j\<le>Suc na. f j \<in> carrier (O\<^bsub>K P n\<^esub>)) \<longrightarrow> \<Sigma>\<^sub>e O\<^bsub>K P n\<^esub> f Suc na = \<Sigma>\<^sub>e K f Suc na
[PROOF STEP]
apply (rule impI, simp)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>na. \<lbrakk>distinct_pds K n P; (\<forall>j\<le>na. f j \<in> carrier (O\<^bsub>K P n\<^esub>)) \<longrightarrow> \<Sigma>\<^sub>e O\<^bsub>K P n\<^esub> f na = \<Sigma>\<^sub>e K f na\<rbrakk> \<Longrightarrow> (\<forall>j\<le>Suc na. f j \<in> carrier (O\<^bsub>K P n\<^esub>)) \<longrightarrow> \<Sigma>\<^sub>e O\<^bsub>K P n\<^esub> f Suc na = \<Sigma>\<^sub>e K f Suc na
[PROOF STEP]
apply (rule impI, simp,
        subst ring_n_pd_pOp_K_pOp, assumption+,
        frule_tac n = n in ring_n_pd[of _ "P"],
        frule_tac Ring.ring_is_ag, drule sym, simp)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>na. \<lbrakk>distinct_pds K n P; \<forall>j\<le>Suc na. f j \<in> carrier (O\<^bsub>K P n\<^esub>); Ring (O\<^bsub>K P n\<^esub>); aGroup (O\<^bsub>K P n\<^esub>); \<Sigma>\<^sub>e K f na = \<Sigma>\<^sub>e O\<^bsub>K P n\<^esub> f na\<rbrakk> \<Longrightarrow> \<Sigma>\<^sub>e O\<^bsub>K P n\<^esub> f na \<in> carrier (O\<^bsub>K P n\<^esub>)
 2. \<And>na. \<lbrakk>distinct_pds K n P; \<Sigma>\<^sub>e O\<^bsub>K P n\<^esub> f na = \<Sigma>\<^sub>e K f na; \<forall>j\<le>Suc na. f j \<in> carrier (O\<^bsub>K P n\<^esub>)\<rbrakk> \<Longrightarrow> f (Suc na) \<in> carrier (O\<^bsub>K P n\<^esub>)
 3. \<And>na. \<lbrakk>distinct_pds K n P; \<Sigma>\<^sub>e O\<^bsub>K P n\<^esub> f na = \<Sigma>\<^sub>e K f na; \<forall>j\<le>Suc na. f j \<in> carrier (O\<^bsub>K P n\<^esub>)\<rbrakk> \<Longrightarrow> \<Sigma>\<^sub>e K f na \<plusminus> f (Suc na) = \<Sigma>\<^sub>e K f na \<plusminus> f (Suc na)
[PROOF STEP]
apply (rule aGroup.nsum_mem, assumption+, simp+)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma (in Corps) ring_n_eSum_K_eSum:"\<lbrakk>distinct_pds K n P;
      \<forall>j \<le> m. f j \<in> carrier (O\<^bsub>K P n\<^esub>)\<rbrakk> \<Longrightarrow> nsum (O\<^bsub>K P n\<^esub>) f m = nsum K f m"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>distinct_pds K n P; \<forall>j\<le>m. f j \<in> carrier (O\<^bsub>K P n\<^esub>)\<rbrakk> \<Longrightarrow> \<Sigma>\<^sub>e O\<^bsub>K P n\<^esub> f m = \<Sigma>\<^sub>e K f m
[PROOF STEP]
apply (simp add:ring_n_eSum_K_eSumTr)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma (in Corps) ideal_eSum_closed:"\<lbrakk>distinct_pds K n P; ideal (O\<^bsub>K P n\<^esub>) I;
      \<forall>j \<le> m. f j \<in> I\<rbrakk> \<Longrightarrow>  nsum K f m \<in> I"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>distinct_pds K n P; ideal (O\<^bsub>K P n\<^esub>) I; \<forall>j\<le>m. f j \<in> I\<rbrakk> \<Longrightarrow> \<Sigma>\<^sub>e K f m \<in> I
[PROOF STEP]
apply (frule ring_n_pd[of "n" "P"])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>distinct_pds K n P; ideal (O\<^bsub>K P n\<^esub>) I; \<forall>j\<le>m. f j \<in> I; Ring (O\<^bsub>K P n\<^esub>)\<rbrakk> \<Longrightarrow> \<Sigma>\<^sub>e K f m \<in> I
[PROOF STEP]
thm Ring.ideal_nsum_closed
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>distinct_pds K n P; ideal (O\<^bsub>K P n\<^esub>) I; \<forall>j\<le>m. f j \<in> I; Ring (O\<^bsub>K P n\<^esub>)\<rbrakk> \<Longrightarrow> \<Sigma>\<^sub>e K f m \<in> I
[PROOF STEP]
apply (frule_tac n = m in
       Ring.ideal_nsum_closed[of "(O\<^bsub>K P n\<^esub>)" "I" _ "f"], assumption+)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>distinct_pds K n P; ideal (O\<^bsub>K P n\<^esub>) I; \<forall>j\<le>m. f j \<in> I; Ring (O\<^bsub>K P n\<^esub>); \<Sigma>\<^sub>e O\<^bsub>K P n\<^esub> f m \<in> I\<rbrakk> \<Longrightarrow> \<Sigma>\<^sub>e K f m \<in> I
[PROOF STEP]
apply (subst ring_n_eSum_K_eSum [THEN sym, of n P m f], assumption+,
        rule allI, simp add:Ring.ideal_subset)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>distinct_pds K n P; ideal (O\<^bsub>K P n\<^esub>) I; \<forall>j\<le>m. f j \<in> I; Ring (O\<^bsub>K P n\<^esub>); \<Sigma>\<^sub>e O\<^bsub>K P n\<^esub> f m \<in> I\<rbrakk> \<Longrightarrow> \<Sigma>\<^sub>e O\<^bsub>K P n\<^esub> f m \<in> I
[PROOF STEP]
apply assumption
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma (in Corps) zero_in_ring_n_pd_zero_K:"distinct_pds K n P \<Longrightarrow>
                               \<zero>\<^bsub>(O\<^bsub>K P n\<^esub>)\<^esub> = \<zero>\<^bsub>K\<^esub>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. distinct_pds K n P \<Longrightarrow> \<zero>\<^bsub>O\<^bsub>K P n\<^esub>\<^esub> = \<zero>
[PROOF STEP]
apply (simp add:ring_n_pd_def Sr_def)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma (in Corps) one_in_ring_n_pd_one_K:"distinct_pds K n P \<Longrightarrow>
                                      1\<^sub>r\<^bsub>(O\<^bsub>K P n\<^esub>)\<^esub> = 1\<^sub>r"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. distinct_pds K n P \<Longrightarrow> 1\<^sub>r\<^bsub>O\<^bsub>K P n\<^esub>\<^esub> = 1\<^sub>r
[PROOF STEP]
apply (simp add:ring_n_pd_def Sr_def)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma (in Corps) mem_ring_n_pd_mem_K:"\<lbrakk>distinct_pds K n P; x \<in>carrier (O\<^bsub>K P n\<^esub>)\<rbrakk>
 \<Longrightarrow> x \<in> carrier K"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>distinct_pds K n P; x \<in> carrier (O\<^bsub>K P n\<^esub>)\<rbrakk> \<Longrightarrow> x \<in> carrier K
[PROOF STEP]
apply (simp add:ring_n_pd_def Sr_def)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma (in Corps) ring_n_tOp_K_tOp:"\<lbrakk>distinct_pds K n P; x \<in> carrier (O\<^bsub>K P n\<^esub>);
      y \<in> carrier (O\<^bsub>K P n\<^esub>)\<rbrakk>  \<Longrightarrow> x \<cdot>\<^sub>r\<^bsub>(O\<^bsub>K P n\<^esub>)\<^esub> y = x \<cdot>\<^sub>r y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>distinct_pds K n P; x \<in> carrier (O\<^bsub>K P n\<^esub>); y \<in> carrier (O\<^bsub>K P n\<^esub>)\<rbrakk> \<Longrightarrow> x \<cdot>\<^sub>r\<^bsub>O\<^bsub>K P n\<^esub>\<^esub> y = x \<cdot>\<^sub>r y
[PROOF STEP]
apply (simp add:ring_n_pd_def Sr_def)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma (in Corps) ring_n_exp_K_exp:"\<lbrakk>distinct_pds K n P; x \<in> carrier (O\<^bsub>K P n\<^esub>)\<rbrakk>
        \<Longrightarrow> x^\<^bsup>K m\<^esup> = x^\<^bsup>(O\<^bsub>K P n\<^esub>) m\<^esup>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>distinct_pds K n P; x \<in> carrier (O\<^bsub>K P n\<^esub>)\<rbrakk> \<Longrightarrow> x^\<^bsup>K m\<^esup> = x^\<^bsup>O\<^bsub>K P n\<^esub> m\<^esup>
[PROOF STEP]
apply (frule ring_n_pd[of "n" "P"])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>distinct_pds K n P; x \<in> carrier (O\<^bsub>K P n\<^esub>); Ring (O\<^bsub>K P n\<^esub>)\<rbrakk> \<Longrightarrow> x^\<^bsup>K m\<^esup> = x^\<^bsup>O\<^bsub>K P n\<^esub> m\<^esup>
[PROOF STEP]
apply (induct_tac m)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>distinct_pds K n P; x \<in> carrier (O\<^bsub>K P n\<^esub>); Ring (O\<^bsub>K P n\<^esub>)\<rbrakk> \<Longrightarrow> x^\<^bsup>K 0\<^esup> = x^\<^bsup>O\<^bsub>K P n\<^esub> 0\<^esup>
 2. \<And>na. \<lbrakk>distinct_pds K n P; x \<in> carrier (O\<^bsub>K P n\<^esub>); Ring (O\<^bsub>K P n\<^esub>); x^\<^bsup>K na\<^esup> = x^\<^bsup>O\<^bsub>K P n\<^esub> na\<^esup>\<rbrakk> \<Longrightarrow> x^\<^bsup>K Suc na\<^esup> = x^\<^bsup>O\<^bsub>K P n\<^esub> Suc na\<^esup>
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>distinct_pds K n P; x \<in> carrier (O\<^bsub>K P n\<^esub>); Ring (O\<^bsub>K P n\<^esub>)\<rbrakk> \<Longrightarrow> 1\<^sub>r = 1\<^sub>r\<^bsub>O\<^bsub>K P n\<^esub>\<^esub>
 2. \<And>na. \<lbrakk>distinct_pds K n P; x \<in> carrier (O\<^bsub>K P n\<^esub>); Ring (O\<^bsub>K P n\<^esub>); x^\<^bsup>K na\<^esup> = x^\<^bsup>O\<^bsub>K P n\<^esub> na\<^esup>\<rbrakk> \<Longrightarrow> x^\<^bsup>K Suc na\<^esup> = x^\<^bsup>O\<^bsub>K P n\<^esub> Suc na\<^esup>
[PROOF STEP]
apply (simp add:one_in_ring_n_pd_one_K)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>na. \<lbrakk>distinct_pds K n P; x \<in> carrier (O\<^bsub>K P n\<^esub>); Ring (O\<^bsub>K P n\<^esub>); x^\<^bsup>K na\<^esup> = x^\<^bsup>O\<^bsub>K P n\<^esub> na\<^esup>\<rbrakk> \<Longrightarrow> x^\<^bsup>K Suc na\<^esup> = x^\<^bsup>O\<^bsub>K P n\<^esub> Suc na\<^esup>
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>na. \<lbrakk>distinct_pds K n P; x \<in> carrier (O\<^bsub>K P n\<^esub>); Ring (O\<^bsub>K P n\<^esub>); x^\<^bsup>K na\<^esup> = x^\<^bsup>O\<^bsub>K P n\<^esub> na\<^esup>\<rbrakk> \<Longrightarrow> x^\<^bsup>O\<^bsub>K P n\<^esub> na\<^esup> \<cdot>\<^sub>r x = x^\<^bsup>O\<^bsub>K P n\<^esub> na\<^esup> \<cdot>\<^sub>r\<^bsub>O\<^bsub>K P n\<^esub>\<^esub> x
[PROOF STEP]
apply (frule_tac n = na in Ring.npClose[of "O\<^bsub>K P n\<^esub>" "x"], assumption+)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>na. \<lbrakk>distinct_pds K n P; x \<in> carrier (O\<^bsub>K P n\<^esub>); Ring (O\<^bsub>K P n\<^esub>); x^\<^bsup>K na\<^esup> = x^\<^bsup>O\<^bsub>K P n\<^esub> na\<^esup>; x^\<^bsup>O\<^bsub>K P n\<^esub> na\<^esup> \<in> carrier (O\<^bsub>K P n\<^esub>)\<rbrakk> \<Longrightarrow> x^\<^bsup>O\<^bsub>K P n\<^esub> na\<^esup> \<cdot>\<^sub>r x = x^\<^bsup>O\<^bsub>K P n\<^esub> na\<^esup> \<cdot>\<^sub>r\<^bsub>O\<^bsub>K P n\<^esub>\<^esub> x
[PROOF STEP]
apply (simp add:ring_n_tOp_K_tOp)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done