[STATEMENT]
lemma (in Ring) np_1:"a \<in> carrier R \<Longrightarrow> npow R a (Suc 0) = a"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. a \<in> carrier R \<Longrightarrow> a^\<^bsup>R Suc 0\<^esup> = a
[PROOF STEP]
(* Y. Santo*)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. a \<in> carrier R \<Longrightarrow> a^\<^bsup>R Suc 0\<^esup> = a
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. a \<in> carrier R \<Longrightarrow> 1\<^sub>r \<cdot>\<^sub>r a = a
[PROOF STEP]
apply (simp add:ring_l_one)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma (in aGroup) nsum_memTr: "(\<forall>j \<le> n. f j \<in> carrier A) \<longrightarrow>
                                 nsum A f n \<in> carrier A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<forall>j\<le>n. f j \<in> carrier A) \<longrightarrow> \<Sigma>\<^sub>e A f n \<in> carrier A
[PROOF STEP]
apply (induct_tac "n")
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. (\<forall>j\<le>0. f j \<in> carrier A) \<longrightarrow> \<Sigma>\<^sub>e A f 0 \<in> carrier A
 2. \<And>n. (\<forall>j\<le>n. f j \<in> carrier A) \<longrightarrow> \<Sigma>\<^sub>e A f n \<in> carrier A \<Longrightarrow> (\<forall>j\<le>Suc n. f j \<in> carrier A) \<longrightarrow> \<Sigma>\<^sub>e A f Suc n \<in> carrier A
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>n. (\<forall>j\<le>n. f j \<in> carrier A) \<longrightarrow> \<Sigma>\<^sub>e A f n \<in> carrier A \<Longrightarrow> (\<forall>j\<le>Suc n. f j \<in> carrier A) \<longrightarrow> \<Sigma>\<^sub>e A f Suc n \<in> carrier A
[PROOF STEP]
apply (rule impI)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>n. \<lbrakk>(\<forall>j\<le>n. f j \<in> carrier A) \<longrightarrow> \<Sigma>\<^sub>e A f n \<in> carrier A; \<forall>j\<le>Suc n. f j \<in> carrier A\<rbrakk> \<Longrightarrow> \<Sigma>\<^sub>e A f Suc n \<in> carrier A
[PROOF STEP]
apply (cut_tac n = n in Nsetn_sub_mem1, simp)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>n. \<lbrakk>\<Sigma>\<^sub>e A f n \<in> carrier A; \<forall>j\<le>Suc n. f j \<in> carrier A\<rbrakk> \<Longrightarrow> \<Sigma>\<^sub>e A f n \<plusminus> f (Suc n) \<in> carrier A
[PROOF STEP]
apply (frule_tac a = "Suc n" in forall_spec, simp,
         thin_tac "\<forall>j\<le>Suc n. f j \<in> carrier A")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>n. \<lbrakk>\<Sigma>\<^sub>e A f n \<in> carrier A; f (Suc n) \<in> carrier A\<rbrakk> \<Longrightarrow> \<Sigma>\<^sub>e A f n \<plusminus> f (Suc n) \<in> carrier A
[PROOF STEP]
apply (rule ag_pOp_closed, assumption+)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma (in aGroup) nsum_mem:"\<forall>j \<le> n. f j \<in> carrier A \<Longrightarrow>
                                 nsum A f n \<in> carrier A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>j\<le>n. f j \<in> carrier A \<Longrightarrow> \<Sigma>\<^sub>e A f n \<in> carrier A
[PROOF STEP]
apply (simp add:nsum_memTr)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma (in aGroup) nsum_eqTr:"(\<forall>j \<le> n. f j \<in> carrier A \<and>
                                      g j \<in> carrier A \<and>
                                      f j = g j)
                           \<longrightarrow>  nsum A f n = nsum A g n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<forall>j\<le>n. f j \<in> carrier A \<and> g j \<in> carrier A \<and> f j = g j) \<longrightarrow> \<Sigma>\<^sub>e A f n = \<Sigma>\<^sub>e A g n
[PROOF STEP]
apply (induct_tac n)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. (\<forall>j\<le>0. f j \<in> carrier A \<and> g j \<in> carrier A \<and> f j = g j) \<longrightarrow> \<Sigma>\<^sub>e A f 0 = \<Sigma>\<^sub>e A g 0
 2. \<And>n. (\<forall>j\<le>n. f j \<in> carrier A \<and> g j \<in> carrier A \<and> f j = g j) \<longrightarrow> \<Sigma>\<^sub>e A f n = \<Sigma>\<^sub>e A g n \<Longrightarrow> (\<forall>j\<le>Suc n. f j \<in> carrier A \<and> g j \<in> carrier A \<and> f j = g j) \<longrightarrow> \<Sigma>\<^sub>e A f Suc n = \<Sigma>\<^sub>e A g Suc n
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>n. (\<forall>j\<le>n. f j \<in> carrier A \<and> g j \<in> carrier A \<and> f j = g j) \<longrightarrow> \<Sigma>\<^sub>e A f n = \<Sigma>\<^sub>e A g n \<Longrightarrow> (\<forall>j\<le>Suc n. f j \<in> carrier A \<and> g j \<in> carrier A \<and> f j = g j) \<longrightarrow> \<Sigma>\<^sub>e A f Suc n = \<Sigma>\<^sub>e A g Suc n
[PROOF STEP]
apply (rule impI)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>n. \<lbrakk>(\<forall>j\<le>n. f j \<in> carrier A \<and> g j \<in> carrier A \<and> f j = g j) \<longrightarrow> \<Sigma>\<^sub>e A f n = \<Sigma>\<^sub>e A g n; \<forall>j\<le>Suc n. f j \<in> carrier A \<and> g j \<in> carrier A \<and> f j = g j\<rbrakk> \<Longrightarrow> \<Sigma>\<^sub>e A f Suc n = \<Sigma>\<^sub>e A g Suc n
[PROOF STEP]
apply (cut_tac n = n in Nsetn_sub_mem1, simp)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma (in aGroup) nsum_eq:"\<lbrakk>\<forall>j \<le> n. f j \<in> carrier A; \<forall>j \<le> n. g j \<in> carrier A;
                           \<forall>j \<le> n. f j = g j\<rbrakk> \<Longrightarrow>  nsum A f n = nsum A g n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<forall>j\<le>n. f j \<in> carrier A; \<forall>j\<le>n. g j \<in> carrier A; \<forall>j\<le>n. f j = g j\<rbrakk> \<Longrightarrow> \<Sigma>\<^sub>e A f n = \<Sigma>\<^sub>e A g n
[PROOF STEP]
by (simp add:nsum_eqTr)


[STATEMENT]
lemma (in aGroup) nsum_cmp_assoc:"\<lbrakk>\<forall>j \<le> n. f j \<in> carrier A;
       g \<in> {j. j \<le> n} \<rightarrow> {j. j \<le> n}; h \<in> {j. j \<le> n} \<rightarrow> {j. j \<le> n}\<rbrakk> \<Longrightarrow>
       nsum A (cmp (cmp f h) g) n = nsum A (cmp f (cmp h g)) n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<forall>j\<le>n. f j \<in> carrier A; g \<in> {j. j \<le> n} \<rightarrow> {j. j \<le> n}; h \<in> {j. j \<le> n} \<rightarrow> {j. j \<le> n}\<rbrakk> \<Longrightarrow> \<Sigma>\<^sub>e A cmp (cmp f h) g n = \<Sigma>\<^sub>e A cmp f (cmp h g) n
[PROOF STEP]
apply (rule nsum_eq)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<lbrakk>\<forall>j\<le>n. f j \<in> carrier A; g \<in> {j. j \<le> n} \<rightarrow> {j. j \<le> n}; h \<in> {j. j \<le> n} \<rightarrow> {j. j \<le> n}\<rbrakk> \<Longrightarrow> \<forall>j\<le>n. cmp (cmp f h) g j \<in> carrier A
 2. \<lbrakk>\<forall>j\<le>n. f j \<in> carrier A; g \<in> {j. j \<le> n} \<rightarrow> {j. j \<le> n}; h \<in> {j. j \<le> n} \<rightarrow> {j. j \<le> n}\<rbrakk> \<Longrightarrow> \<forall>j\<le>n. cmp f (cmp h g) j \<in> carrier A
 3. \<lbrakk>\<forall>j\<le>n. f j \<in> carrier A; g \<in> {j. j \<le> n} \<rightarrow> {j. j \<le> n}; h \<in> {j. j \<le> n} \<rightarrow> {j. j \<le> n}\<rbrakk> \<Longrightarrow> \<forall>j\<le>n. cmp (cmp f h) g j = cmp f (cmp h g) j
[PROOF STEP]
apply (rule allI, rule impI, simp add:cmp_def)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>j. \<lbrakk>\<forall>j\<le>n. f j \<in> carrier A; g \<in> {j. j \<le> n} \<rightarrow> {j. j \<le> n}; h \<in> {j. j \<le> n} \<rightarrow> {j. j \<le> n}; j \<le> n\<rbrakk> \<Longrightarrow> f (h (g j)) \<in> carrier A
 2. \<lbrakk>\<forall>j\<le>n. f j \<in> carrier A; g \<in> {j. j \<le> n} \<rightarrow> {j. j \<le> n}; h \<in> {j. j \<le> n} \<rightarrow> {j. j \<le> n}\<rbrakk> \<Longrightarrow> \<forall>j\<le>n. cmp f (cmp h g) j \<in> carrier A
 3. \<lbrakk>\<forall>j\<le>n. f j \<in> carrier A; g \<in> {j. j \<le> n} \<rightarrow> {j. j \<le> n}; h \<in> {j. j \<le> n} \<rightarrow> {j. j \<le> n}\<rbrakk> \<Longrightarrow> \<forall>j\<le>n. cmp (cmp f h) g j = cmp f (cmp h g) j
[PROOF STEP]
apply (frule_tac x = j in funcset_mem[of g "{j. j \<le> n}" "{j. j \<le> n}"], simp,
       frule_tac x = "g j" in funcset_mem[of h "{j. j \<le> n}" "{j. j \<le> n}"],
       assumption, simp)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>\<forall>j\<le>n. f j \<in> carrier A; g \<in> {j. j \<le> n} \<rightarrow> {j. j \<le> n}; h \<in> {j. j \<le> n} \<rightarrow> {j. j \<le> n}\<rbrakk> \<Longrightarrow> \<forall>j\<le>n. cmp f (cmp h g) j \<in> carrier A
 2. \<lbrakk>\<forall>j\<le>n. f j \<in> carrier A; g \<in> {j. j \<le> n} \<rightarrow> {j. j \<le> n}; h \<in> {j. j \<le> n} \<rightarrow> {j. j \<le> n}\<rbrakk> \<Longrightarrow> \<forall>j\<le>n. cmp (cmp f h) g j = cmp f (cmp h g) j
[PROOF STEP]
apply (rule allI, rule impI, simp add:cmp_def,
       frule_tac x = j in funcset_mem[of g "{j. j \<le> n}" "{j. j \<le> n}"], simp,
       frule_tac x = "g j" in funcset_mem[of h "{j. j \<le> n}" "{j. j \<le> n}"],
       assumption, simp)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<forall>j\<le>n. f j \<in> carrier A; g \<in> {j. j \<le> n} \<rightarrow> {j. j \<le> n}; h \<in> {j. j \<le> n} \<rightarrow> {j. j \<le> n}\<rbrakk> \<Longrightarrow> \<forall>j\<le>n. cmp (cmp f h) g j = cmp f (cmp h g) j
[PROOF STEP]
apply (rule allI, simp add:cmp_def)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma (in aGroup) fSum_Suc:"\<forall>j \<in> nset n (n + Suc m). f j \<in> carrier A \<Longrightarrow>
              fSum A f n (n + Suc m) = fSum A f n (n + m) \<plusminus> f (n + Suc m)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>j\<in>nset n (n + Suc m). f j \<in> carrier A \<Longrightarrow> \<Sigma>\<^sub>f A f n (n + Suc m) = \<Sigma>\<^sub>f A f n (n + m) \<plusminus> f (n + Suc m)
[PROOF STEP]
by (simp add:fSum_def, simp add:cmp_def slide_def)


[STATEMENT]
lemma (in aGroup) fSum_eqTr:"(\<forall>j \<in> nset n (n + m). f j \<in> carrier A \<and>
         g j \<in> carrier A \<and>  f j = g j)  \<longrightarrow>
                       fSum A f  n (n + m) = fSum A g n (n + m)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<forall>j\<in>nset n (n + m). f j \<in> carrier A \<and> g j \<in> carrier A \<and> f j = g j) \<longrightarrow> \<Sigma>\<^sub>f A f n (n + m) = \<Sigma>\<^sub>f A g n (n + m)
[PROOF STEP]
apply (induct_tac m)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. (\<forall>j\<in>nset n (n + 0). f j \<in> carrier A \<and> g j \<in> carrier A \<and> f j = g j) \<longrightarrow> \<Sigma>\<^sub>f A f n (n + 0) = \<Sigma>\<^sub>f A g n (n + 0)
 2. \<And>na. (\<forall>j\<in>nset n (n + na). f j \<in> carrier A \<and> g j \<in> carrier A \<and> f j = g j) \<longrightarrow> \<Sigma>\<^sub>f A f n (n + na) = \<Sigma>\<^sub>f A g n (n + na) \<Longrightarrow> (\<forall>j\<in>nset n (n + Suc na). f j \<in> carrier A \<and> g j \<in> carrier A \<and> f j = g j) \<longrightarrow> \<Sigma>\<^sub>f A f n (n + Suc na) = \<Sigma>\<^sub>f A g n (n + Suc na)
[PROOF STEP]
apply (simp add:fSum_def,
        simp add:cmp_def slide_def,
        simp add:nset_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>na. (\<forall>j\<in>nset n (n + na). f j \<in> carrier A \<and> g j \<in> carrier A \<and> f j = g j) \<longrightarrow> \<Sigma>\<^sub>f A f n (n + na) = \<Sigma>\<^sub>f A g n (n + na) \<Longrightarrow> (\<forall>j\<in>nset n (n + Suc na). f j \<in> carrier A \<and> g j \<in> carrier A \<and> f j = g j) \<longrightarrow> \<Sigma>\<^sub>f A f n (n + Suc na) = \<Sigma>\<^sub>f A g n (n + Suc na)
[PROOF STEP]
apply (rule impI)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>na. \<lbrakk>(\<forall>j\<in>nset n (n + na). f j \<in> carrier A \<and> g j \<in> carrier A \<and> f j = g j) \<longrightarrow> \<Sigma>\<^sub>f A f n (n + na) = \<Sigma>\<^sub>f A g n (n + na); \<forall>j\<in>nset n (n + Suc na). f j \<in> carrier A \<and> g j \<in> carrier A \<and> f j = g j\<rbrakk> \<Longrightarrow> \<Sigma>\<^sub>f A f n (n + Suc na) = \<Sigma>\<^sub>f A g n (n + Suc na)
[PROOF STEP]
apply (subst fSum_Suc,
        rule ballI, simp, simp)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>na. \<lbrakk>(\<forall>j\<in>nset n (n + na). f j \<in> carrier A \<and> g j \<in> carrier A \<and> f j = g j) \<longrightarrow> \<Sigma>\<^sub>f A f n (n + na) = \<Sigma>\<^sub>f A g n (n + na); \<forall>j\<in>nset n (Suc (n + na)). f j \<in> carrier A \<and> g j \<in> carrier A \<and> f j = g j\<rbrakk> \<Longrightarrow> \<Sigma>\<^sub>f A f n (n + na) \<plusminus> f (Suc (n + na)) = \<Sigma>\<^sub>f A g n Suc (n + na)
[PROOF STEP]
apply (cut_tac n = n and m = na and f = g in fSum_Suc,
        rule ballI, simp, simp,
        thin_tac "\<Sigma>\<^sub>f A g n (Suc (n + na)) =
                                   \<Sigma>\<^sub>f A g n (n + na) \<plusminus> g (Suc (n + na))")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>na. \<lbrakk>(\<forall>j\<in>nset n (n + na). f j \<in> carrier A \<and> g j \<in> carrier A \<and> f j = g j) \<longrightarrow> \<Sigma>\<^sub>f A f n (n + na) = \<Sigma>\<^sub>f A g n (n + na); \<forall>j\<in>nset n (Suc (n + na)). f j \<in> carrier A \<and> g j \<in> carrier A \<and> f j = g j\<rbrakk> \<Longrightarrow> \<Sigma>\<^sub>f A f n (n + na) \<plusminus> f (Suc (n + na)) = \<Sigma>\<^sub>f A g n (n + na) \<plusminus> g (Suc (n + na))
[PROOF STEP]
apply (cut_tac n = n and m = na in nsetnm_sub_mem, simp,
        thin_tac "\<forall>j. j \<in> nset n (n + na) \<longrightarrow> j \<in> nset n (Suc (n + na))")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>na. \<lbrakk>\<Sigma>\<^sub>f A f n (n + na) = \<Sigma>\<^sub>f A g n (n + na); \<forall>j\<in>nset n (Suc (n + na)). f j \<in> carrier A \<and> g j \<in> carrier A \<and> f j = g j\<rbrakk> \<Longrightarrow> \<Sigma>\<^sub>f A g n (n + na) \<plusminus> f (Suc (n + na)) = \<Sigma>\<^sub>f A g n (n + na) \<plusminus> g (Suc (n + na))
[PROOF STEP]
apply (frule_tac x = "Suc (n + na)" in bspec,
       simp add:nset_def, simp)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma (in aGroup) fSum_eq:"\<lbrakk> \<forall>j \<in> nset n (n + m). f j \<in> carrier A;
      \<forall>j \<in> nset n (n + m). g j \<in> carrier A; (\<forall>j\<in> nset n (n + m). f j = g j)\<rbrakk>
       \<Longrightarrow>
         fSum A f n (n + m) = fSum A g n (n + m)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<forall>j\<in>nset n (n + m). f j \<in> carrier A; \<forall>j\<in>nset n (n + m). g j \<in> carrier A; \<forall>j\<in>nset n (n + m). f j = g j\<rbrakk> \<Longrightarrow> \<Sigma>\<^sub>f A f n (n + m) = \<Sigma>\<^sub>f A g n (n + m)
[PROOF STEP]
by (simp add:fSum_eqTr)


[STATEMENT]
lemma (in aGroup) fSum_eq1:"\<lbrakk>n \<le> m; \<forall>j\<in>nset n m. f j \<in> carrier A;
       \<forall>j\<in>nset n m. g j \<in> carrier A;  \<forall>j\<in>nset n m. f j = g j\<rbrakk> \<Longrightarrow>
         fSum A f n m = fSum A g n m"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>n \<le> m; \<forall>j\<in>nset n m. f j \<in> carrier A; \<forall>j\<in>nset n m. g j \<in> carrier A; \<forall>j\<in>nset n m. f j = g j\<rbrakk> \<Longrightarrow> \<Sigma>\<^sub>f A f n m = \<Sigma>\<^sub>f A g n m
[PROOF STEP]
apply (cut_tac fSum_eq[of n "m - n" f g])
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<lbrakk>n \<le> m; \<forall>j\<in>nset n m. f j \<in> carrier A; \<forall>j\<in>nset n m. g j \<in> carrier A; \<forall>j\<in>nset n m. f j = g j; \<Sigma>\<^sub>f A f n (n + (m - n)) = \<Sigma>\<^sub>f A g n (n + (m - n))\<rbrakk> \<Longrightarrow> \<Sigma>\<^sub>f A f n m = \<Sigma>\<^sub>f A g n m
 2. \<lbrakk>n \<le> m; \<forall>j\<in>nset n m. f j \<in> carrier A; \<forall>j\<in>nset n m. g j \<in> carrier A; \<forall>j\<in>nset n m. f j = g j\<rbrakk> \<Longrightarrow> \<forall>j\<in>nset n (n + (m - n)). f j \<in> carrier A
 3. \<lbrakk>n \<le> m; \<forall>j\<in>nset n m. f j \<in> carrier A; \<forall>j\<in>nset n m. g j \<in> carrier A; \<forall>j\<in>nset n m. f j = g j\<rbrakk> \<Longrightarrow> \<forall>j\<in>nset n (n + (m - n)). g j \<in> carrier A
 4. \<lbrakk>n \<le> m; \<forall>j\<in>nset n m. f j \<in> carrier A; \<forall>j\<in>nset n m. g j \<in> carrier A; \<forall>j\<in>nset n m. f j = g j\<rbrakk> \<Longrightarrow> \<forall>j\<in>nset n (n + (m - n)). f j = g j
[PROOF STEP]
apply simp+
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma (in aGroup) fSum_zeroTr:"(\<forall>j \<in> nset n (n + m). f j = \<zero>)  \<longrightarrow>
                       fSum A f  n (n + m) = \<zero>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<forall>j\<in>nset n (n + m). f j = \<zero>) \<longrightarrow> \<Sigma>\<^sub>f A f n (n + m) = \<zero>
[PROOF STEP]
apply (induct_tac m)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. (\<forall>j\<in>nset n (n + 0). f j = \<zero>) \<longrightarrow> \<Sigma>\<^sub>f A f n (n + 0) = \<zero>
 2. \<And>na. (\<forall>j\<in>nset n (n + na). f j = \<zero>) \<longrightarrow> \<Sigma>\<^sub>f A f n (n + na) = \<zero> \<Longrightarrow> (\<forall>j\<in>nset n (n + Suc na). f j = \<zero>) \<longrightarrow> \<Sigma>\<^sub>f A f n (n + Suc na) = \<zero>
[PROOF STEP]
apply (simp add:fSum_def cmp_def slide_def nset_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>na. (\<forall>j\<in>nset n (n + na). f j = \<zero>) \<longrightarrow> \<Sigma>\<^sub>f A f n (n + na) = \<zero> \<Longrightarrow> (\<forall>j\<in>nset n (n + Suc na). f j = \<zero>) \<longrightarrow> \<Sigma>\<^sub>f A f n (n + Suc na) = \<zero>
[PROOF STEP]
apply (rule impI)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>na. \<lbrakk>(\<forall>j\<in>nset n (n + na). f j = \<zero>) \<longrightarrow> \<Sigma>\<^sub>f A f n (n + na) = \<zero>; \<forall>j\<in>nset n (n + Suc na). f j = \<zero>\<rbrakk> \<Longrightarrow> \<Sigma>\<^sub>f A f n (n + Suc na) = \<zero>
[PROOF STEP]
apply (subst fSum_Suc)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>na. \<lbrakk>(\<forall>j\<in>nset n (n + na). f j = \<zero>) \<longrightarrow> \<Sigma>\<^sub>f A f n (n + na) = \<zero>; \<forall>j\<in>nset n (n + Suc na). f j = \<zero>\<rbrakk> \<Longrightarrow> \<forall>j\<in>nset n (n + Suc na). f j \<in> carrier A
 2. \<And>na. \<lbrakk>(\<forall>j\<in>nset n (n + na). f j = \<zero>) \<longrightarrow> \<Sigma>\<^sub>f A f n (n + na) = \<zero>; \<forall>j\<in>nset n (n + Suc na). f j = \<zero>\<rbrakk> \<Longrightarrow> \<Sigma>\<^sub>f A f n (n + na) \<plusminus> f (n + Suc na) = \<zero>
[PROOF STEP]
apply (rule ballI, simp add:ag_inc_zero)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>na. \<lbrakk>(\<forall>j\<in>nset n (n + na). f j = \<zero>) \<longrightarrow> \<Sigma>\<^sub>f A f n (n + na) = \<zero>; \<forall>j\<in>nset n (n + Suc na). f j = \<zero>\<rbrakk> \<Longrightarrow> \<Sigma>\<^sub>f A f n (n + na) \<plusminus> f (n + Suc na) = \<zero>
[PROOF STEP]
apply (frule_tac x = "n + Suc na" in bspec, simp add:nset_def,
       simp)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>na. \<lbrakk>(\<forall>j\<in>nset n (n + na). f j = \<zero>) \<longrightarrow> \<Sigma>\<^sub>f A f n (n + na) = \<zero>; \<forall>j\<in>nset n (Suc (n + na)). f j = \<zero>; f (Suc (n + na)) = \<zero>\<rbrakk> \<Longrightarrow> \<Sigma>\<^sub>f A f n (n + na) \<plusminus> \<zero> = \<zero>
[PROOF STEP]
apply (simp add:nset_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>na. \<lbrakk>\<Sigma>\<^sub>f A f n (n + na) = \<zero>; \<forall>j. n \<le> j \<and> j \<le> Suc (n + na) \<longrightarrow> f j = \<zero>\<rbrakk> \<Longrightarrow> \<zero> \<plusminus> \<zero> = \<zero>
[PROOF STEP]
apply (cut_tac ag_inc_zero, simp add:ag_l_zero)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma (in aGroup) fSum_zero:"\<forall>j \<in> nset n (n + m). f j = \<zero>  \<Longrightarrow>
                       fSum A f  n (n + m) = \<zero>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>j\<in>nset n (n + m). f j = \<zero> \<Longrightarrow> \<Sigma>\<^sub>f A f n (n + m) = \<zero>
[PROOF STEP]
by (simp add:fSum_zeroTr)


[STATEMENT]
lemma (in aGroup) fSum_zero1:"\<lbrakk>n < m; \<forall>j \<in> nset (Suc n) m. f j = \<zero>\<rbrakk>  \<Longrightarrow>
                       fSum A f  (Suc n) m = \<zero>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>n < m; \<forall>j\<in>nset (Suc n) m. f j = \<zero>\<rbrakk> \<Longrightarrow> \<Sigma>\<^sub>f A f Suc n m = \<zero>
[PROOF STEP]
apply (cut_tac fSum_zero[of "Suc n" "m - Suc n" f])
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>n < m; \<forall>j\<in>nset (Suc n) m. f j = \<zero>; \<Sigma>\<^sub>f A f Suc n (Suc n + (m - Suc n)) = \<zero>\<rbrakk> \<Longrightarrow> \<Sigma>\<^sub>f A f Suc n m = \<zero>
 2. \<lbrakk>n < m; \<forall>j\<in>nset (Suc n) m. f j = \<zero>\<rbrakk> \<Longrightarrow> \<forall>j\<in>nset (Suc n) (Suc n + (m - Suc n)). f j = \<zero>
[PROOF STEP]
apply simp+
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma (in Ring) nsumMulEleL: "\<And> n. \<lbrakk> \<forall> i. f i \<in> carrier R; x \<in> carrier R \<rbrakk>
        \<Longrightarrow> x \<cdot>\<^sub>r (nsum R f n) = nsum R (\<lambda> i. x \<cdot>\<^sub>r (f i)) n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>n. \<lbrakk>\<forall>i. f i \<in> carrier R; x \<in> carrier R\<rbrakk> \<Longrightarrow> x \<cdot>\<^sub>r \<Sigma>\<^sub>e R f n = \<Sigma>\<^sub>e R (\<lambda>i. x \<cdot>\<^sub>r f i) n
[PROOF STEP]
apply (cut_tac ring_is_ag)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>n. \<lbrakk>\<forall>i. f i \<in> carrier R; x \<in> carrier R; aGroup R\<rbrakk> \<Longrightarrow> x \<cdot>\<^sub>r \<Sigma>\<^sub>e R f n = \<Sigma>\<^sub>e R (\<lambda>i. x \<cdot>\<^sub>r f i) n
[PROOF STEP]
apply (induct_tac "n")
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>n. \<lbrakk>\<forall>i. f i \<in> carrier R; x \<in> carrier R; aGroup R\<rbrakk> \<Longrightarrow> x \<cdot>\<^sub>r \<Sigma>\<^sub>e R f 0 = \<Sigma>\<^sub>e R (\<lambda>i. x \<cdot>\<^sub>r f i) 0
 2. \<And>n na. \<lbrakk>\<forall>i. f i \<in> carrier R; x \<in> carrier R; aGroup R; x \<cdot>\<^sub>r \<Sigma>\<^sub>e R f na = \<Sigma>\<^sub>e R (\<lambda>i. x \<cdot>\<^sub>r f i) na\<rbrakk> \<Longrightarrow> x \<cdot>\<^sub>r \<Sigma>\<^sub>e R f Suc na = \<Sigma>\<^sub>e R (\<lambda>i. x \<cdot>\<^sub>r f i) Suc na
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>n na. \<lbrakk>\<forall>i. f i \<in> carrier R; x \<in> carrier R; aGroup R; x \<cdot>\<^sub>r \<Sigma>\<^sub>e R f na = \<Sigma>\<^sub>e R (\<lambda>i. x \<cdot>\<^sub>r f i) na\<rbrakk> \<Longrightarrow> x \<cdot>\<^sub>r \<Sigma>\<^sub>e R f Suc na = \<Sigma>\<^sub>e R (\<lambda>i. x \<cdot>\<^sub>r f i) Suc na
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>na. \<lbrakk>\<forall>i. f i \<in> carrier R; x \<in> carrier R; aGroup R; x \<cdot>\<^sub>r \<Sigma>\<^sub>e R f na = \<Sigma>\<^sub>e R (\<lambda>i. x \<cdot>\<^sub>r f i) na\<rbrakk> \<Longrightarrow> x \<cdot>\<^sub>r (\<Sigma>\<^sub>e R f na \<plusminus> f (Suc na)) = \<Sigma>\<^sub>e R (\<lambda>i. x \<cdot>\<^sub>r f i) na \<plusminus> x \<cdot>\<^sub>r f (Suc na)
[PROOF STEP]
apply (subst ring_distrib1, assumption)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>na. \<lbrakk>\<forall>i. f i \<in> carrier R; x \<in> carrier R; aGroup R; x \<cdot>\<^sub>r \<Sigma>\<^sub>e R f na = \<Sigma>\<^sub>e R (\<lambda>i. x \<cdot>\<^sub>r f i) na\<rbrakk> \<Longrightarrow> \<Sigma>\<^sub>e R f na \<in> carrier R
 2. \<And>na. \<lbrakk>\<forall>i. f i \<in> carrier R; x \<in> carrier R; aGroup R; x \<cdot>\<^sub>r \<Sigma>\<^sub>e R f na = \<Sigma>\<^sub>e R (\<lambda>i. x \<cdot>\<^sub>r f i) na\<rbrakk> \<Longrightarrow> f (Suc na) \<in> carrier R
 3. \<And>na. \<lbrakk>\<forall>i. f i \<in> carrier R; x \<in> carrier R; aGroup R; x \<cdot>\<^sub>r \<Sigma>\<^sub>e R f na = \<Sigma>\<^sub>e R (\<lambda>i. x \<cdot>\<^sub>r f i) na\<rbrakk> \<Longrightarrow> x \<cdot>\<^sub>r \<Sigma>\<^sub>e R f na \<plusminus> x \<cdot>\<^sub>r f (Suc na) = \<Sigma>\<^sub>e R (\<lambda>i. x \<cdot>\<^sub>r f i) na \<plusminus> x \<cdot>\<^sub>r f (Suc na)
[PROOF STEP]
apply (rule aGroup.nsum_mem, assumption)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>na. \<lbrakk>\<forall>i. f i \<in> carrier R; x \<in> carrier R; aGroup R; x \<cdot>\<^sub>r \<Sigma>\<^sub>e R f na = \<Sigma>\<^sub>e R (\<lambda>i. x \<cdot>\<^sub>r f i) na\<rbrakk> \<Longrightarrow> \<forall>j\<le>na. f j \<in> carrier R
 2. \<And>na. \<lbrakk>\<forall>i. f i \<in> carrier R; x \<in> carrier R; aGroup R; x \<cdot>\<^sub>r \<Sigma>\<^sub>e R f na = \<Sigma>\<^sub>e R (\<lambda>i. x \<cdot>\<^sub>r f i) na\<rbrakk> \<Longrightarrow> f (Suc na) \<in> carrier R
 3. \<And>na. \<lbrakk>\<forall>i. f i \<in> carrier R; x \<in> carrier R; aGroup R; x \<cdot>\<^sub>r \<Sigma>\<^sub>e R f na = \<Sigma>\<^sub>e R (\<lambda>i. x \<cdot>\<^sub>r f i) na\<rbrakk> \<Longrightarrow> x \<cdot>\<^sub>r \<Sigma>\<^sub>e R f na \<plusminus> x \<cdot>\<^sub>r f (Suc na) = \<Sigma>\<^sub>e R (\<lambda>i. x \<cdot>\<^sub>r f i) na \<plusminus> x \<cdot>\<^sub>r f (Suc na)
[PROOF STEP]
apply (rule allI, simp+)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma (in Ring) nsumMulElmL:
  "\<And> n. \<lbrakk> \<forall> i. f i \<in> carrier R; x \<in> carrier R \<rbrakk>
        \<Longrightarrow> x \<cdot>\<^sub>r (nsum R f n) = nsum R (\<lambda> i. x \<cdot>\<^sub>r (f i)) n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>n. \<lbrakk>\<forall>i. f i \<in> carrier R; x \<in> carrier R\<rbrakk> \<Longrightarrow> x \<cdot>\<^sub>r \<Sigma>\<^sub>e R f n = \<Sigma>\<^sub>e R (\<lambda>i. x \<cdot>\<^sub>r f i) n
[PROOF STEP]
apply (cut_tac ring_is_ag)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>n. \<lbrakk>\<forall>i. f i \<in> carrier R; x \<in> carrier R; aGroup R\<rbrakk> \<Longrightarrow> x \<cdot>\<^sub>r \<Sigma>\<^sub>e R f n = \<Sigma>\<^sub>e R (\<lambda>i. x \<cdot>\<^sub>r f i) n
[PROOF STEP]
apply (induct_tac "n")
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>n. \<lbrakk>\<forall>i. f i \<in> carrier R; x \<in> carrier R; aGroup R\<rbrakk> \<Longrightarrow> x \<cdot>\<^sub>r \<Sigma>\<^sub>e R f 0 = \<Sigma>\<^sub>e R (\<lambda>i. x \<cdot>\<^sub>r f i) 0
 2. \<And>n na. \<lbrakk>\<forall>i. f i \<in> carrier R; x \<in> carrier R; aGroup R; x \<cdot>\<^sub>r \<Sigma>\<^sub>e R f na = \<Sigma>\<^sub>e R (\<lambda>i. x \<cdot>\<^sub>r f i) na\<rbrakk> \<Longrightarrow> x \<cdot>\<^sub>r \<Sigma>\<^sub>e R f Suc na = \<Sigma>\<^sub>e R (\<lambda>i. x \<cdot>\<^sub>r f i) Suc na
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>n na. \<lbrakk>\<forall>i. f i \<in> carrier R; x \<in> carrier R; aGroup R; x \<cdot>\<^sub>r \<Sigma>\<^sub>e R f na = \<Sigma>\<^sub>e R (\<lambda>i. x \<cdot>\<^sub>r f i) na\<rbrakk> \<Longrightarrow> x \<cdot>\<^sub>r \<Sigma>\<^sub>e R f Suc na = \<Sigma>\<^sub>e R (\<lambda>i. x \<cdot>\<^sub>r f i) Suc na
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>na. \<lbrakk>\<forall>i. f i \<in> carrier R; x \<in> carrier R; aGroup R; x \<cdot>\<^sub>r \<Sigma>\<^sub>e R f na = \<Sigma>\<^sub>e R (\<lambda>i. x \<cdot>\<^sub>r f i) na\<rbrakk> \<Longrightarrow> x \<cdot>\<^sub>r (\<Sigma>\<^sub>e R f na \<plusminus> f (Suc na)) = \<Sigma>\<^sub>e R (\<lambda>i. x \<cdot>\<^sub>r f i) na \<plusminus> x \<cdot>\<^sub>r f (Suc na)
[PROOF STEP]
apply (subst ring_distrib1, assumption+)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>na. \<lbrakk>\<forall>i. f i \<in> carrier R; x \<in> carrier R; aGroup R; x \<cdot>\<^sub>r \<Sigma>\<^sub>e R f na = \<Sigma>\<^sub>e R (\<lambda>i. x \<cdot>\<^sub>r f i) na\<rbrakk> \<Longrightarrow> \<Sigma>\<^sub>e R f na \<in> carrier R
 2. \<And>na. \<lbrakk>\<forall>i. f i \<in> carrier R; x \<in> carrier R; aGroup R; x \<cdot>\<^sub>r \<Sigma>\<^sub>e R f na = \<Sigma>\<^sub>e R (\<lambda>i. x \<cdot>\<^sub>r f i) na\<rbrakk> \<Longrightarrow> f (Suc na) \<in> carrier R
 3. \<And>na. \<lbrakk>\<forall>i. f i \<in> carrier R; x \<in> carrier R; aGroup R; x \<cdot>\<^sub>r \<Sigma>\<^sub>e R f na = \<Sigma>\<^sub>e R (\<lambda>i. x \<cdot>\<^sub>r f i) na\<rbrakk> \<Longrightarrow> x \<cdot>\<^sub>r \<Sigma>\<^sub>e R f na \<plusminus> x \<cdot>\<^sub>r f (Suc na) = \<Sigma>\<^sub>e R (\<lambda>i. x \<cdot>\<^sub>r f i) na \<plusminus> x \<cdot>\<^sub>r f (Suc na)
[PROOF STEP]
apply (simp add:aGroup.nsum_mem)+
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma (in aGroup) nsumTailTr:
         "(\<forall>j\<le>(Suc n). f j \<in> carrier A) \<longrightarrow>
          nsum A f (Suc n) = (nsum A (\<lambda> i. (f (Suc i))) n) \<plusminus> (f 0)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<forall>j\<le>Suc n. f j \<in> carrier A) \<longrightarrow> \<Sigma>\<^sub>e A f Suc n = \<Sigma>\<^sub>e A (\<lambda>i. f (Suc i)) n \<plusminus> f 0
[PROOF STEP]
apply (induct_tac "n")
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. (\<forall>j\<le>Suc 0. f j \<in> carrier A) \<longrightarrow> \<Sigma>\<^sub>e A f Suc 0 = \<Sigma>\<^sub>e A (\<lambda>i. f (Suc i)) 0 \<plusminus> f 0
 2. \<And>n. (\<forall>j\<le>Suc n. f j \<in> carrier A) \<longrightarrow> \<Sigma>\<^sub>e A f Suc n = \<Sigma>\<^sub>e A (\<lambda>i. f (Suc i)) n \<plusminus> f 0 \<Longrightarrow> (\<forall>j\<le>Suc (Suc n). f j \<in> carrier A) \<longrightarrow> \<Sigma>\<^sub>e A f Suc (Suc n) = \<Sigma>\<^sub>e A (\<lambda>i. f (Suc i)) Suc n \<plusminus> f 0
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. (\<forall>j\<le>Suc 0. f j \<in> carrier A) \<longrightarrow> f 0 \<plusminus> f (Suc 0) = f (Suc 0) \<plusminus> f 0
 2. \<And>n. (\<forall>j\<le>Suc n. f j \<in> carrier A) \<longrightarrow> \<Sigma>\<^sub>e A f Suc n = \<Sigma>\<^sub>e A (\<lambda>i. f (Suc i)) n \<plusminus> f 0 \<Longrightarrow> (\<forall>j\<le>Suc (Suc n). f j \<in> carrier A) \<longrightarrow> \<Sigma>\<^sub>e A f Suc (Suc n) = \<Sigma>\<^sub>e A (\<lambda>i. f (Suc i)) Suc n \<plusminus> f 0
[PROOF STEP]
apply (rule impI,
         rule ag_pOp_commute)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<forall>j\<le>Suc 0. f j \<in> carrier A \<Longrightarrow> f 0 \<in> carrier A
 2. \<forall>j\<le>Suc 0. f j \<in> carrier A \<Longrightarrow> f (Suc 0) \<in> carrier A
 3. \<And>n. (\<forall>j\<le>Suc n. f j \<in> carrier A) \<longrightarrow> \<Sigma>\<^sub>e A f Suc n = \<Sigma>\<^sub>e A (\<lambda>i. f (Suc i)) n \<plusminus> f 0 \<Longrightarrow> (\<forall>j\<le>Suc (Suc n). f j \<in> carrier A) \<longrightarrow> \<Sigma>\<^sub>e A f Suc (Suc n) = \<Sigma>\<^sub>e A (\<lambda>i. f (Suc i)) Suc n \<plusminus> f 0
[PROOF STEP]
apply (cut_tac Nset_inc_0[of "Suc 0"],
         simp add:Pi_def,
         cut_tac n_in_Nsetn[of "Suc 0"],
         simp add:Pi_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>n. (\<forall>j\<le>Suc n. f j \<in> carrier A) \<longrightarrow> \<Sigma>\<^sub>e A f Suc n = \<Sigma>\<^sub>e A (\<lambda>i. f (Suc i)) n \<plusminus> f 0 \<Longrightarrow> (\<forall>j\<le>Suc (Suc n). f j \<in> carrier A) \<longrightarrow> \<Sigma>\<^sub>e A f Suc (Suc n) = \<Sigma>\<^sub>e A (\<lambda>i. f (Suc i)) Suc n \<plusminus> f 0
[PROOF STEP]
apply (rule impI)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>n. \<lbrakk>(\<forall>j\<le>Suc n. f j \<in> carrier A) \<longrightarrow> \<Sigma>\<^sub>e A f Suc n = \<Sigma>\<^sub>e A (\<lambda>i. f (Suc i)) n \<plusminus> f 0; \<forall>j\<le>Suc (Suc n). f j \<in> carrier A\<rbrakk> \<Longrightarrow> \<Sigma>\<^sub>e A f Suc (Suc n) = \<Sigma>\<^sub>e A (\<lambda>i. f (Suc i)) Suc n \<plusminus> f 0
[PROOF STEP]
apply (cut_tac n = "Suc n" in Nsetn_sub_mem1, simp)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>n. \<lbrakk>\<Sigma>\<^sub>e A f n \<plusminus> f (Suc n) = \<Sigma>\<^sub>e A (\<lambda>i. f (Suc i)) n \<plusminus> f 0; \<forall>j\<le>Suc (Suc n). f j \<in> carrier A\<rbrakk> \<Longrightarrow> \<Sigma>\<^sub>e A (\<lambda>i. f (Suc i)) n \<plusminus> f 0 \<plusminus> f (Suc (Suc n)) = \<Sigma>\<^sub>e A (\<lambda>i. f (Suc i)) n \<plusminus> f (Suc (Suc n)) \<plusminus> f 0
[PROOF STEP]
apply (frule_tac a = 0 in forall_spec, simp,
          frule_tac a = "Suc (Suc n)" in forall_spec, simp)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>n. \<lbrakk>\<Sigma>\<^sub>e A f n \<plusminus> f (Suc n) = \<Sigma>\<^sub>e A (\<lambda>i. f (Suc i)) n \<plusminus> f 0; \<forall>j\<le>Suc (Suc n). f j \<in> carrier A; f 0 \<in> carrier A; f (Suc (Suc n)) \<in> carrier A\<rbrakk> \<Longrightarrow> \<Sigma>\<^sub>e A (\<lambda>i. f (Suc i)) n \<plusminus> f 0 \<plusminus> f (Suc (Suc n)) = \<Sigma>\<^sub>e A (\<lambda>i. f (Suc i)) n \<plusminus> f (Suc (Suc n)) \<plusminus> f 0
[PROOF STEP]
apply (cut_tac n = n in nsum_mem[of  _  "\<lambda>i. f (Suc i)"],
          rule allI, rule impI,
          frule_tac a = "Suc j" in forall_spec, simp, simp,
          thin_tac "\<forall>j\<le>Suc (Suc n). f j \<in> carrier A")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>n. \<lbrakk>\<Sigma>\<^sub>e A f n \<plusminus> f (Suc n) = \<Sigma>\<^sub>e A (\<lambda>i. f (Suc i)) n \<plusminus> f 0; f 0 \<in> carrier A; f (Suc (Suc n)) \<in> carrier A; \<Sigma>\<^sub>e A (\<lambda>i. f (Suc i)) n \<in> carrier A\<rbrakk> \<Longrightarrow> \<Sigma>\<^sub>e A (\<lambda>i. f (Suc i)) n \<plusminus> f 0 \<plusminus> f (Suc (Suc n)) = \<Sigma>\<^sub>e A (\<lambda>i. f (Suc i)) n \<plusminus> f (Suc (Suc n)) \<plusminus> f 0
[PROOF STEP]
apply (subst ag_pOp_assoc, assumption+)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>n. \<lbrakk>\<Sigma>\<^sub>e A f n \<plusminus> f (Suc n) = \<Sigma>\<^sub>e A (\<lambda>i. f (Suc i)) n \<plusminus> f 0; f 0 \<in> carrier A; f (Suc (Suc n)) \<in> carrier A; \<Sigma>\<^sub>e A (\<lambda>i. f (Suc i)) n \<in> carrier A\<rbrakk> \<Longrightarrow> \<Sigma>\<^sub>e A (\<lambda>i. f (Suc i)) n \<plusminus> (f 0 \<plusminus> f (Suc (Suc n))) = \<Sigma>\<^sub>e A (\<lambda>i. f (Suc i)) n \<plusminus> f (Suc (Suc n)) \<plusminus> f 0
[PROOF STEP]
apply (simp add:ag_pOp_commute[of  "f 0"])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>n. \<lbrakk>\<Sigma>\<^sub>e A f n \<plusminus> f (Suc n) = \<Sigma>\<^sub>e A (\<lambda>i. f (Suc i)) n \<plusminus> f 0; f 0 \<in> carrier A; f (Suc (Suc n)) \<in> carrier A; \<Sigma>\<^sub>e A (\<lambda>i. f (Suc i)) n \<in> carrier A\<rbrakk> \<Longrightarrow> \<Sigma>\<^sub>e A (\<lambda>i. f (Suc i)) n \<plusminus> (f (Suc (Suc n)) \<plusminus> f 0) = \<Sigma>\<^sub>e A (\<lambda>i. f (Suc i)) n \<plusminus> f (Suc (Suc n)) \<plusminus> f 0
[PROOF STEP]
apply (subst ag_pOp_assoc[THEN sym], assumption+)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>n. \<lbrakk>\<Sigma>\<^sub>e A f n \<plusminus> f (Suc n) = \<Sigma>\<^sub>e A (\<lambda>i. f (Suc i)) n \<plusminus> f 0; f 0 \<in> carrier A; f (Suc (Suc n)) \<in> carrier A; \<Sigma>\<^sub>e A (\<lambda>i. f (Suc i)) n \<in> carrier A\<rbrakk> \<Longrightarrow> \<Sigma>\<^sub>e A (\<lambda>i. f (Suc i)) n \<plusminus> f (Suc (Suc n)) \<plusminus> f 0 = \<Sigma>\<^sub>e A (\<lambda>i. f (Suc i)) n \<plusminus> f (Suc (Suc n)) \<plusminus> f 0
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma (in aGroup) nsumTail:
      "\<forall>j \<le> (Suc n). f j \<in> carrier A \<Longrightarrow>
            nsum A f (Suc n) = (nsum A (\<lambda> i. (f (Suc i))) n) \<plusminus> (f 0)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>j\<le>Suc n. f j \<in> carrier A \<Longrightarrow> \<Sigma>\<^sub>e A f Suc n = \<Sigma>\<^sub>e A (\<lambda>i. f (Suc i)) n \<plusminus> f 0
[PROOF STEP]
by (cut_tac nsumTailTr[of n f], simp)


[STATEMENT]
lemma (in aGroup) nsumElmTail:
  "\<forall>i. f i \<in> carrier A
        \<Longrightarrow> nsum A f (Suc n) = (nsum A (\<lambda> i. (f (Suc i))) n) \<plusminus> (f 0)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>i. f i \<in> carrier A \<Longrightarrow> \<Sigma>\<^sub>e A f Suc n = \<Sigma>\<^sub>e A (\<lambda>i. f (Suc i)) n \<plusminus> f 0
[PROOF STEP]
apply (cut_tac n = n and f = f in nsumTail,
         rule allI, simp, simp)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma (in aGroup) nsum_addTr:
  "(\<forall>j \<le> n. f j \<in> carrier A \<and> g j \<in> carrier A) \<longrightarrow>
   nsum A (\<lambda> i. (f i) \<plusminus> (g i)) n = (nsum A f n) \<plusminus> (nsum A g n)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<forall>j\<le>n. f j \<in> carrier A \<and> g j \<in> carrier A) \<longrightarrow> \<Sigma>\<^sub>e A (\<lambda>i. f i \<plusminus> g i) n = \<Sigma>\<^sub>e A f n \<plusminus> \<Sigma>\<^sub>e A g n
[PROOF STEP]
apply (induct_tac "n")
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. (\<forall>j\<le>0. f j \<in> carrier A \<and> g j \<in> carrier A) \<longrightarrow> \<Sigma>\<^sub>e A (\<lambda>i. f i \<plusminus> g i) 0 = \<Sigma>\<^sub>e A f 0 \<plusminus> \<Sigma>\<^sub>e A g 0
 2. \<And>n. (\<forall>j\<le>n. f j \<in> carrier A \<and> g j \<in> carrier A) \<longrightarrow> \<Sigma>\<^sub>e A (\<lambda>i. f i \<plusminus> g i) n = \<Sigma>\<^sub>e A f n \<plusminus> \<Sigma>\<^sub>e A g n \<Longrightarrow> (\<forall>j\<le>Suc n. f j \<in> carrier A \<and> g j \<in> carrier A) \<longrightarrow> \<Sigma>\<^sub>e A (\<lambda>i. f i \<plusminus> g i) Suc n = \<Sigma>\<^sub>e A f Suc n \<plusminus> \<Sigma>\<^sub>e A g Suc n
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>n. (\<forall>j\<le>n. f j \<in> carrier A \<and> g j \<in> carrier A) \<longrightarrow> \<Sigma>\<^sub>e A (\<lambda>i. f i \<plusminus> g i) n = \<Sigma>\<^sub>e A f n \<plusminus> \<Sigma>\<^sub>e A g n \<Longrightarrow> (\<forall>j\<le>Suc n. f j \<in> carrier A \<and> g j \<in> carrier A) \<longrightarrow> \<Sigma>\<^sub>e A (\<lambda>i. f i \<plusminus> g i) Suc n = \<Sigma>\<^sub>e A f Suc n \<plusminus> \<Sigma>\<^sub>e A g Suc n
[PROOF STEP]
apply (simp, rule impI)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>n. \<lbrakk>(\<forall>j\<le>n. f j \<in> carrier A \<and> g j \<in> carrier A) \<longrightarrow> \<Sigma>\<^sub>e A (\<lambda>i. f i \<plusminus> g i) n = \<Sigma>\<^sub>e A f n \<plusminus> \<Sigma>\<^sub>e A g n; \<forall>j\<le>Suc n. f j \<in> carrier A \<and> g j \<in> carrier A\<rbrakk> \<Longrightarrow> \<Sigma>\<^sub>e A f n \<plusminus> \<Sigma>\<^sub>e A g n \<plusminus> (f (Suc n) \<plusminus> g (Suc n)) = \<Sigma>\<^sub>e A f n \<plusminus> f (Suc n) \<plusminus> (\<Sigma>\<^sub>e A g n \<plusminus> g (Suc n))
[PROOF STEP]
apply (cut_tac n = n in Nsetn_sub_mem1, simp)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>n. \<lbrakk>\<Sigma>\<^sub>e A (\<lambda>i. f i \<plusminus> g i) n = \<Sigma>\<^sub>e A f n \<plusminus> \<Sigma>\<^sub>e A g n; \<forall>j\<le>Suc n. f j \<in> carrier A \<and> g j \<in> carrier A\<rbrakk> \<Longrightarrow> \<Sigma>\<^sub>e A f n \<plusminus> \<Sigma>\<^sub>e A g n \<plusminus> (f (Suc n) \<plusminus> g (Suc n)) = \<Sigma>\<^sub>e A f n \<plusminus> f (Suc n) \<plusminus> (\<Sigma>\<^sub>e A g n \<plusminus> g (Suc n))
[PROOF STEP]
apply (thin_tac "\<Sigma>\<^sub>e A (\<lambda>i. f i \<plusminus> g i) n = \<Sigma>\<^sub>e A f n \<plusminus> \<Sigma>\<^sub>e A g n")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>n. \<forall>j\<le>Suc n. f j \<in> carrier A \<and> g j \<in> carrier A \<Longrightarrow> \<Sigma>\<^sub>e A f n \<plusminus> \<Sigma>\<^sub>e A g n \<plusminus> (f (Suc n) \<plusminus> g (Suc n)) = \<Sigma>\<^sub>e A f n \<plusminus> f (Suc n) \<plusminus> (\<Sigma>\<^sub>e A g n \<plusminus> g (Suc n))
[PROOF STEP]
apply (rule aGroup.ag_add4_rel, rule aGroup_axioms)
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<And>n. \<forall>j\<le>Suc n. f j \<in> carrier A \<and> g j \<in> carrier A \<Longrightarrow> \<Sigma>\<^sub>e A f n \<in> carrier A
 2. \<And>n. \<forall>j\<le>Suc n. f j \<in> carrier A \<and> g j \<in> carrier A \<Longrightarrow> \<Sigma>\<^sub>e A g n \<in> carrier A
 3. \<And>n. \<forall>j\<le>Suc n. f j \<in> carrier A \<and> g j \<in> carrier A \<Longrightarrow> f (Suc n) \<in> carrier A
 4. \<And>n. \<forall>j\<le>Suc n. f j \<in> carrier A \<and> g j \<in> carrier A \<Longrightarrow> g (Suc n) \<in> carrier A
[PROOF STEP]
apply (rule aGroup.nsum_mem, rule aGroup_axioms, rule allI, simp)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>n. \<forall>j\<le>Suc n. f j \<in> carrier A \<and> g j \<in> carrier A \<Longrightarrow> \<Sigma>\<^sub>e A g n \<in> carrier A
 2. \<And>n. \<forall>j\<le>Suc n. f j \<in> carrier A \<and> g j \<in> carrier A \<Longrightarrow> f (Suc n) \<in> carrier A
 3. \<And>n. \<forall>j\<le>Suc n. f j \<in> carrier A \<and> g j \<in> carrier A \<Longrightarrow> g (Suc n) \<in> carrier A
[PROOF STEP]
apply (rule aGroup.nsum_mem, rule aGroup_axioms, rule allI, simp)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>n. \<forall>j\<le>Suc n. f j \<in> carrier A \<and> g j \<in> carrier A \<Longrightarrow> f (Suc n) \<in> carrier A
 2. \<And>n. \<forall>j\<le>Suc n. f j \<in> carrier A \<and> g j \<in> carrier A \<Longrightarrow> g (Suc n) \<in> carrier A
[PROOF STEP]
apply simp+
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma (in aGroup) nsum_add:
  "\<lbrakk> \<forall>j \<le> n. f j \<in> carrier A; \<forall>j \<le> n. g j \<in> carrier A\<rbrakk>  \<Longrightarrow>
   nsum A (\<lambda> i. (f i) \<plusminus> (g i)) n = (nsum A f n) \<plusminus> (nsum A g n)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<forall>j\<le>n. f j \<in> carrier A; \<forall>j\<le>n. g j \<in> carrier A\<rbrakk> \<Longrightarrow> \<Sigma>\<^sub>e A (\<lambda>i. f i \<plusminus> g i) n = \<Sigma>\<^sub>e A f n \<plusminus> \<Sigma>\<^sub>e A g n
[PROOF STEP]
by (cut_tac nsum_addTr[of n f g], simp)


[STATEMENT]
lemma (in aGroup) nsumElmAdd:
  "\<lbrakk> \<forall> i. f i \<in> carrier A; \<forall> i. g i \<in> carrier A\<rbrakk>
        \<Longrightarrow> nsum A (\<lambda> i. (f i) \<plusminus> (g i)) n = (nsum A f n) \<plusminus> (nsum A g n)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<forall>i. f i \<in> carrier A; \<forall>i. g i \<in> carrier A\<rbrakk> \<Longrightarrow> \<Sigma>\<^sub>e A (\<lambda>i. f i \<plusminus> g i) n = \<Sigma>\<^sub>e A f n \<plusminus> \<Sigma>\<^sub>e A g n
[PROOF STEP]
apply (cut_tac nsum_add[of n f g])
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<lbrakk>\<forall>i. f i \<in> carrier A; \<forall>i. g i \<in> carrier A; \<Sigma>\<^sub>e A (\<lambda>i. f i \<plusminus> g i) n = \<Sigma>\<^sub>e A f n \<plusminus> \<Sigma>\<^sub>e A g n\<rbrakk> \<Longrightarrow> \<Sigma>\<^sub>e A (\<lambda>i. f i \<plusminus> g i) n = \<Sigma>\<^sub>e A f n \<plusminus> \<Sigma>\<^sub>e A g n
 2. \<lbrakk>\<forall>i. f i \<in> carrier A; \<forall>i. g i \<in> carrier A\<rbrakk> \<Longrightarrow> \<forall>j\<le>n. f j \<in> carrier A
 3. \<lbrakk>\<forall>i. f i \<in> carrier A; \<forall>i. g i \<in> carrier A\<rbrakk> \<Longrightarrow> \<forall>j\<le>n. g j \<in> carrier A
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>\<forall>i. f i \<in> carrier A; \<forall>i. g i \<in> carrier A\<rbrakk> \<Longrightarrow> \<forall>j\<le>n. f j \<in> carrier A
 2. \<lbrakk>\<forall>i. f i \<in> carrier A; \<forall>i. g i \<in> carrier A\<rbrakk> \<Longrightarrow> \<forall>j\<le>n. g j \<in> carrier A
[PROOF STEP]
apply (rule allI, simp)+
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma (in aGroup) nsum_add_nmTr:
  "(\<forall>j \<le> n. f j \<in> carrier A) \<and> (\<forall>j \<le> m. g j \<in> carrier A) \<longrightarrow>
   nsum A (jointfun n f m g) (Suc (n + m)) = (nsum A f n) \<plusminus> (nsum A g m)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<forall>j\<le>n. f j \<in> carrier A) \<and> (\<forall>j\<le>m. g j \<in> carrier A) \<longrightarrow> \<Sigma>\<^sub>e A jointfun n f m g Suc (n + m) = \<Sigma>\<^sub>e A f n \<plusminus> \<Sigma>\<^sub>e A g m
[PROOF STEP]
apply (induct_tac m)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. (\<forall>j\<le>n. f j \<in> carrier A) \<and> (\<forall>j\<le>0. g j \<in> carrier A) \<longrightarrow> \<Sigma>\<^sub>e A jointfun n f 0 g Suc (n + 0) = \<Sigma>\<^sub>e A f n \<plusminus> \<Sigma>\<^sub>e A g 0
 2. \<And>na. (\<forall>j\<le>n. f j \<in> carrier A) \<and> (\<forall>j\<le>na. g j \<in> carrier A) \<longrightarrow> \<Sigma>\<^sub>e A jointfun n f na g Suc (n + na) = \<Sigma>\<^sub>e A f n \<plusminus> \<Sigma>\<^sub>e A g na \<Longrightarrow> (\<forall>j\<le>n. f j \<in> carrier A) \<and> (\<forall>j\<le>Suc na. g j \<in> carrier A) \<longrightarrow> \<Sigma>\<^sub>e A jointfun n f (Suc na) g Suc (n + Suc na) = \<Sigma>\<^sub>e A f n \<plusminus> \<Sigma>\<^sub>e A g Suc na
[PROOF STEP]
apply (simp add:jointfun_def sliden_def)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. (\<forall>j\<le>n. f j \<in> carrier A) \<and> g 0 \<in> carrier A \<longrightarrow> \<Sigma>\<^sub>e A (\<lambda>a. if a \<le> n then f a else g (sliden (Suc n) a)) n \<plusminus> g 0 = \<Sigma>\<^sub>e A f n \<plusminus> g 0
 2. \<And>na. (\<forall>j\<le>n. f j \<in> carrier A) \<and> (\<forall>j\<le>na. g j \<in> carrier A) \<longrightarrow> \<Sigma>\<^sub>e A jointfun n f na g Suc (n + na) = \<Sigma>\<^sub>e A f n \<plusminus> \<Sigma>\<^sub>e A g na \<Longrightarrow> (\<forall>j\<le>n. f j \<in> carrier A) \<and> (\<forall>j\<le>Suc na. g j \<in> carrier A) \<longrightarrow> \<Sigma>\<^sub>e A jointfun n f (Suc na) g Suc (n + Suc na) = \<Sigma>\<^sub>e A f n \<plusminus> \<Sigma>\<^sub>e A g Suc na
[PROOF STEP]
apply (rule impI)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. (\<forall>j\<le>n. f j \<in> carrier A) \<and> g 0 \<in> carrier A \<Longrightarrow> \<Sigma>\<^sub>e A (\<lambda>a. if a \<le> n then f a else g (sliden (Suc n) a)) n \<plusminus> g 0 = \<Sigma>\<^sub>e A f n \<plusminus> g 0
 2. \<And>na. (\<forall>j\<le>n. f j \<in> carrier A) \<and> (\<forall>j\<le>na. g j \<in> carrier A) \<longrightarrow> \<Sigma>\<^sub>e A jointfun n f na g Suc (n + na) = \<Sigma>\<^sub>e A f n \<plusminus> \<Sigma>\<^sub>e A g na \<Longrightarrow> (\<forall>j\<le>n. f j \<in> carrier A) \<and> (\<forall>j\<le>Suc na. g j \<in> carrier A) \<longrightarrow> \<Sigma>\<^sub>e A jointfun n f (Suc na) g Suc (n + Suc na) = \<Sigma>\<^sub>e A f n \<plusminus> \<Sigma>\<^sub>e A g Suc na
[PROOF STEP]
apply (rule ag_pOp_add_r)
[PROOF STATE]
proof (prove)
goal (5 subgoals):
 1. (\<forall>j\<le>n. f j \<in> carrier A) \<and> g 0 \<in> carrier A \<Longrightarrow> \<Sigma>\<^sub>e A (\<lambda>a. if a \<le> n then f a else g (sliden (Suc n) a)) n \<in> carrier A
 2. (\<forall>j\<le>n. f j \<in> carrier A) \<and> g 0 \<in> carrier A \<Longrightarrow> \<Sigma>\<^sub>e A f n \<in> carrier A
 3. (\<forall>j\<le>n. f j \<in> carrier A) \<and> g 0 \<in> carrier A \<Longrightarrow> g 0 \<in> carrier A
 4. (\<forall>j\<le>n. f j \<in> carrier A) \<and> g 0 \<in> carrier A \<Longrightarrow> \<Sigma>\<^sub>e A (\<lambda>a. if a \<le> n then f a else g (sliden (Suc n) a)) n = \<Sigma>\<^sub>e A f n
 5. \<And>na. (\<forall>j\<le>n. f j \<in> carrier A) \<and> (\<forall>j\<le>na. g j \<in> carrier A) \<longrightarrow> \<Sigma>\<^sub>e A jointfun n f na g Suc (n + na) = \<Sigma>\<^sub>e A f n \<plusminus> \<Sigma>\<^sub>e A g na \<Longrightarrow> (\<forall>j\<le>n. f j \<in> carrier A) \<and> (\<forall>j\<le>Suc na. g j \<in> carrier A) \<longrightarrow> \<Sigma>\<^sub>e A jointfun n f (Suc na) g Suc (n + Suc na) = \<Sigma>\<^sub>e A f n \<plusminus> \<Sigma>\<^sub>e A g Suc na
[PROOF STEP]
apply (rule nsum_mem, rule allI, erule conjE, rule impI, simp)
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. (\<forall>j\<le>n. f j \<in> carrier A) \<and> g 0 \<in> carrier A \<Longrightarrow> \<Sigma>\<^sub>e A f n \<in> carrier A
 2. (\<forall>j\<le>n. f j \<in> carrier A) \<and> g 0 \<in> carrier A \<Longrightarrow> g 0 \<in> carrier A
 3. (\<forall>j\<le>n. f j \<in> carrier A) \<and> g 0 \<in> carrier A \<Longrightarrow> \<Sigma>\<^sub>e A (\<lambda>a. if a \<le> n then f a else g (sliden (Suc n) a)) n = \<Sigma>\<^sub>e A f n
 4. \<And>na. (\<forall>j\<le>n. f j \<in> carrier A) \<and> (\<forall>j\<le>na. g j \<in> carrier A) \<longrightarrow> \<Sigma>\<^sub>e A jointfun n f na g Suc (n + na) = \<Sigma>\<^sub>e A f n \<plusminus> \<Sigma>\<^sub>e A g na \<Longrightarrow> (\<forall>j\<le>n. f j \<in> carrier A) \<and> (\<forall>j\<le>Suc na. g j \<in> carrier A) \<longrightarrow> \<Sigma>\<^sub>e A jointfun n f (Suc na) g Suc (n + Suc na) = \<Sigma>\<^sub>e A f n \<plusminus> \<Sigma>\<^sub>e A g Suc na
[PROOF STEP]
apply (erule conjE, simp add:nsum_mem, simp)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. (\<forall>j\<le>n. f j \<in> carrier A) \<and> g 0 \<in> carrier A \<Longrightarrow> \<Sigma>\<^sub>e A (\<lambda>a. if a \<le> n then f a else g (sliden (Suc n) a)) n = \<Sigma>\<^sub>e A f n
 2. \<And>na. (\<forall>j\<le>n. f j \<in> carrier A) \<and> (\<forall>j\<le>na. g j \<in> carrier A) \<longrightarrow> \<Sigma>\<^sub>e A jointfun n f na g Suc (n + na) = \<Sigma>\<^sub>e A f n \<plusminus> \<Sigma>\<^sub>e A g na \<Longrightarrow> (\<forall>j\<le>n. f j \<in> carrier A) \<and> (\<forall>j\<le>Suc na. g j \<in> carrier A) \<longrightarrow> \<Sigma>\<^sub>e A jointfun n f (Suc na) g Suc (n + Suc na) = \<Sigma>\<^sub>e A f n \<plusminus> \<Sigma>\<^sub>e A g Suc na
[PROOF STEP]
apply (rule nsum_eq[of n], simp+)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>na. (\<forall>j\<le>n. f j \<in> carrier A) \<and> (\<forall>j\<le>na. g j \<in> carrier A) \<longrightarrow> \<Sigma>\<^sub>e A jointfun n f na g (n + na) \<plusminus> jointfun n f na g (Suc (n + na)) = \<Sigma>\<^sub>e A f n \<plusminus> \<Sigma>\<^sub>e A g na \<Longrightarrow> (\<forall>j\<le>n. f j \<in> carrier A) \<and> (\<forall>j\<le>Suc na. g j \<in> carrier A) \<longrightarrow> \<Sigma>\<^sub>e A jointfun n f (Suc na) g (n + na) \<plusminus> jointfun n f (Suc na) g (Suc (n + na)) \<plusminus> jointfun n f (Suc na) g (Suc (Suc (n + na))) = \<Sigma>\<^sub>e A f n \<plusminus> (\<Sigma>\<^sub>e A g na \<plusminus> g (Suc na))
[PROOF STEP]
apply (simp add:jointfun_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>na. (\<forall>j\<le>n. f j \<in> carrier A) \<and> (\<forall>j\<le>na. g j \<in> carrier A) \<longrightarrow> \<Sigma>\<^sub>e A (\<lambda>i. if i \<le> n then f i else g (sliden (Suc n) i)) (n + na) \<plusminus> g (sliden (Suc n) (Suc (n + na))) = \<Sigma>\<^sub>e A f n \<plusminus> \<Sigma>\<^sub>e A g na \<Longrightarrow> (\<forall>j\<le>n. f j \<in> carrier A) \<and> (\<forall>j\<le>Suc na. g j \<in> carrier A) \<longrightarrow> \<Sigma>\<^sub>e A f n \<plusminus> \<Sigma>\<^sub>e A g na \<plusminus> g (sliden (Suc n) (Suc (Suc (n + na)))) = \<Sigma>\<^sub>e A f n \<plusminus> (\<Sigma>\<^sub>e A g na \<plusminus> g (Suc na))
[PROOF STEP]
apply (rule impI, simp)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>na. \<lbrakk>\<Sigma>\<^sub>e A (\<lambda>i. if i \<le> n then f i else g (sliden (Suc n) i)) (n + na) \<plusminus> g (sliden (Suc n) (Suc (n + na))) = \<Sigma>\<^sub>e A f n \<plusminus> \<Sigma>\<^sub>e A g na; (\<forall>j\<le>n. f j \<in> carrier A) \<and> (\<forall>j\<le>Suc na. g j \<in> carrier A)\<rbrakk> \<Longrightarrow> \<Sigma>\<^sub>e A f n \<plusminus> \<Sigma>\<^sub>e A g na \<plusminus> g (sliden (Suc n) (Suc (Suc (n + na)))) = \<Sigma>\<^sub>e A f n \<plusminus> (\<Sigma>\<^sub>e A g na \<plusminus> g (Suc na))
[PROOF STEP]
apply (erule conjE, simp add:sliden_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>na. \<lbrakk>\<Sigma>\<^sub>e A (\<lambda>i. if i \<le> n then f i else g (sliden (Suc n) i)) (n + na) \<plusminus> g na = \<Sigma>\<^sub>e A f n \<plusminus> \<Sigma>\<^sub>e A g na; \<forall>j\<le>n. f j \<in> carrier A; \<forall>j\<le>Suc na. g j \<in> carrier A\<rbrakk> \<Longrightarrow> \<Sigma>\<^sub>e A f n \<plusminus> \<Sigma>\<^sub>e A g na \<plusminus> g (Suc na) = \<Sigma>\<^sub>e A f n \<plusminus> (\<Sigma>\<^sub>e A g na \<plusminus> g (Suc na))
[PROOF STEP]
apply (thin_tac "\<Sigma>\<^sub>e A (\<lambda>i. if i \<le> n then f i else g (sliden (Suc n) i))
        (n + na) \<plusminus> g na = \<Sigma>\<^sub>e A f n \<plusminus> \<Sigma>\<^sub>e A g na")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>na. \<lbrakk>\<forall>j\<le>n. f j \<in> carrier A; \<forall>j\<le>Suc na. g j \<in> carrier A\<rbrakk> \<Longrightarrow> \<Sigma>\<^sub>e A f n \<plusminus> \<Sigma>\<^sub>e A g na \<plusminus> g (Suc na) = \<Sigma>\<^sub>e A f n \<plusminus> (\<Sigma>\<^sub>e A g na \<plusminus> g (Suc na))
[PROOF STEP]
apply (subst ag_pOp_assoc)
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<And>na. \<lbrakk>\<forall>j\<le>n. f j \<in> carrier A; \<forall>j\<le>Suc na. g j \<in> carrier A\<rbrakk> \<Longrightarrow> \<Sigma>\<^sub>e A f n \<in> carrier A
 2. \<And>na. \<lbrakk>\<forall>j\<le>n. f j \<in> carrier A; \<forall>j\<le>Suc na. g j \<in> carrier A\<rbrakk> \<Longrightarrow> \<Sigma>\<^sub>e A g na \<in> carrier A
 3. \<And>na. \<lbrakk>\<forall>j\<le>n. f j \<in> carrier A; \<forall>j\<le>Suc na. g j \<in> carrier A\<rbrakk> \<Longrightarrow> g (Suc na) \<in> carrier A
 4. \<And>na. \<lbrakk>\<forall>j\<le>n. f j \<in> carrier A; \<forall>j\<le>Suc na. g j \<in> carrier A\<rbrakk> \<Longrightarrow> \<Sigma>\<^sub>e A f n \<plusminus> (\<Sigma>\<^sub>e A g na \<plusminus> g (Suc na)) = \<Sigma>\<^sub>e A f n \<plusminus> (\<Sigma>\<^sub>e A g na \<plusminus> g (Suc na))
[PROOF STEP]
apply (simp add:nsum_mem)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>na. \<lbrakk>\<forall>j\<le>n. f j \<in> carrier A; \<forall>j\<le>Suc na. g j \<in> carrier A\<rbrakk> \<Longrightarrow> \<Sigma>\<^sub>e A g na \<in> carrier A
 2. \<And>na. \<lbrakk>\<forall>j\<le>n. f j \<in> carrier A; \<forall>j\<le>Suc na. g j \<in> carrier A\<rbrakk> \<Longrightarrow> g (Suc na) \<in> carrier A
 3. \<And>na. \<lbrakk>\<forall>j\<le>n. f j \<in> carrier A; \<forall>j\<le>Suc na. g j \<in> carrier A\<rbrakk> \<Longrightarrow> \<Sigma>\<^sub>e A f n \<plusminus> (\<Sigma>\<^sub>e A g na \<plusminus> g (Suc na)) = \<Sigma>\<^sub>e A f n \<plusminus> (\<Sigma>\<^sub>e A g na \<plusminus> g (Suc na))
[PROOF STEP]
apply (simp add:nsum_mem, simp)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>na. \<lbrakk>\<forall>j\<le>n. f j \<in> carrier A; \<forall>j\<le>Suc na. g j \<in> carrier A\<rbrakk> \<Longrightarrow> \<Sigma>\<^sub>e A f n \<plusminus> (\<Sigma>\<^sub>e A g na \<plusminus> g (Suc na)) = \<Sigma>\<^sub>e A f n \<plusminus> (\<Sigma>\<^sub>e A g na \<plusminus> g (Suc na))
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma (in aGroup) nsum_add_nm:
"\<lbrakk>\<forall>j \<le> n. f j \<in> carrier A; \<forall>j \<le> m. g j \<in> carrier A\<rbrakk> \<Longrightarrow>
   nsum A (jointfun n f m g) (Suc (n + m)) = (nsum A f n) \<plusminus> (nsum A g m)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<forall>j\<le>n. f j \<in> carrier A; \<forall>j\<le>m. g j \<in> carrier A\<rbrakk> \<Longrightarrow> \<Sigma>\<^sub>e A jointfun n f m g Suc (n + m) = \<Sigma>\<^sub>e A f n \<plusminus> \<Sigma>\<^sub>e A g m
[PROOF STEP]
apply (cut_tac nsum_add_nmTr[of n f m g])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<forall>j\<le>n. f j \<in> carrier A; \<forall>j\<le>m. g j \<in> carrier A; (\<forall>j\<le>n. f j \<in> carrier A) \<and> (\<forall>j\<le>m. g j \<in> carrier A) \<longrightarrow> \<Sigma>\<^sub>e A jointfun n f m g Suc (n + m) = \<Sigma>\<^sub>e A f n \<plusminus> \<Sigma>\<^sub>e A g m\<rbrakk> \<Longrightarrow> \<Sigma>\<^sub>e A jointfun n f m g Suc (n + m) = \<Sigma>\<^sub>e A f n \<plusminus> \<Sigma>\<^sub>e A g m
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma (in Ring) npeSum2_sub_muly:
  "\<lbrakk> x \<in> carrier R; y \<in> carrier R \<rbrakk> \<Longrightarrow>
        y \<cdot>\<^sub>r(nsum R (\<lambda>i. nscal R ((npow R x (n-i)) \<cdot>\<^sub>r (npow R y i))
                                (n choose i)) n)
        = nsum R (\<lambda>i. nscal R ((npow R x (n-i)) \<cdot>\<^sub>r (npow R y (i+1)))
                                (n choose i)) n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>x \<in> carrier R; y \<in> carrier R\<rbrakk> \<Longrightarrow> y \<cdot>\<^sub>r \<Sigma>\<^sub>e R (\<lambda>i.  (n choose i) \<times>\<^bsub>R\<^esub> (x^\<^bsup>R (n - i)\<^esup> \<cdot>\<^sub>r y^\<^bsup>R i\<^esup>)) n = \<Sigma>\<^sub>e R (\<lambda>i.  (n choose i) \<times>\<^bsub>R\<^esub> (x^\<^bsup>R (n - i)\<^esup> \<cdot>\<^sub>r y^\<^bsup>R (i + 1)\<^esup>)) n
[PROOF STEP]
apply (cut_tac ring_is_ag)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>x \<in> carrier R; y \<in> carrier R; aGroup R\<rbrakk> \<Longrightarrow> y \<cdot>\<^sub>r \<Sigma>\<^sub>e R (\<lambda>i.  (n choose i) \<times>\<^bsub>R\<^esub> (x^\<^bsup>R (n - i)\<^esup> \<cdot>\<^sub>r y^\<^bsup>R i\<^esup>)) n = \<Sigma>\<^sub>e R (\<lambda>i.  (n choose i) \<times>\<^bsub>R\<^esub> (x^\<^bsup>R (n - i)\<^esup> \<cdot>\<^sub>r y^\<^bsup>R (i + 1)\<^esup>)) n
[PROOF STEP]
apply (subst nsumMulElmL)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<lbrakk>x \<in> carrier R; y \<in> carrier R; aGroup R\<rbrakk> \<Longrightarrow> \<forall>i.  (n choose i) \<times>\<^bsub>R\<^esub> (x^\<^bsup>R (n - i)\<^esup> \<cdot>\<^sub>r y^\<^bsup>R i\<^esup>) \<in> carrier R
 2. \<lbrakk>x \<in> carrier R; y \<in> carrier R; aGroup R\<rbrakk> \<Longrightarrow> y \<in> carrier R
 3. \<lbrakk>x \<in> carrier R; y \<in> carrier R; aGroup R\<rbrakk> \<Longrightarrow> \<Sigma>\<^sub>e R (\<lambda>i. y \<cdot>\<^sub>r  (n choose i) \<times>\<^bsub>R\<^esub> (x^\<^bsup>R (n - i)\<^esup> \<cdot>\<^sub>r y^\<^bsup>R i\<^esup>)) n = \<Sigma>\<^sub>e R (\<lambda>i.  (n choose i) \<times>\<^bsub>R\<^esub> (x^\<^bsup>R (n - i)\<^esup> \<cdot>\<^sub>r y^\<^bsup>R (i + 1)\<^esup>)) n
[PROOF STEP]
apply (rule allI)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>i. \<lbrakk>x \<in> carrier R; y \<in> carrier R; aGroup R\<rbrakk> \<Longrightarrow>  (n choose i) \<times>\<^bsub>R\<^esub> (x^\<^bsup>R (n - i)\<^esup> \<cdot>\<^sub>r y^\<^bsup>R i\<^esup>) \<in> carrier R
 2. \<lbrakk>x \<in> carrier R; y \<in> carrier R; aGroup R\<rbrakk> \<Longrightarrow> y \<in> carrier R
 3. \<lbrakk>x \<in> carrier R; y \<in> carrier R; aGroup R\<rbrakk> \<Longrightarrow> \<Sigma>\<^sub>e R (\<lambda>i. y \<cdot>\<^sub>r  (n choose i) \<times>\<^bsub>R\<^esub> (x^\<^bsup>R (n - i)\<^esup> \<cdot>\<^sub>r y^\<^bsup>R i\<^esup>)) n = \<Sigma>\<^sub>e R (\<lambda>i.  (n choose i) \<times>\<^bsub>R\<^esub> (x^\<^bsup>R (n - i)\<^esup> \<cdot>\<^sub>r y^\<^bsup>R (i + 1)\<^esup>)) n
[PROOF STEP]
apply (simp only:nsClose add:ring_tOp_closed
             add:npClose)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>x \<in> carrier R; y \<in> carrier R; aGroup R\<rbrakk> \<Longrightarrow> y \<in> carrier R
 2. \<lbrakk>x \<in> carrier R; y \<in> carrier R; aGroup R\<rbrakk> \<Longrightarrow> \<Sigma>\<^sub>e R (\<lambda>i. y \<cdot>\<^sub>r  (n choose i) \<times>\<^bsub>R\<^esub> (x^\<^bsup>R (n - i)\<^esup> \<cdot>\<^sub>r y^\<^bsup>R i\<^esup>)) n = \<Sigma>\<^sub>e R (\<lambda>i.  (n choose i) \<times>\<^bsub>R\<^esub> (x^\<^bsup>R (n - i)\<^esup> \<cdot>\<^sub>r y^\<^bsup>R (i + 1)\<^esup>)) n
[PROOF STEP]
apply assumption
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>x \<in> carrier R; y \<in> carrier R; aGroup R\<rbrakk> \<Longrightarrow> \<Sigma>\<^sub>e R (\<lambda>i. y \<cdot>\<^sub>r  (n choose i) \<times>\<^bsub>R\<^esub> (x^\<^bsup>R (n - i)\<^esup> \<cdot>\<^sub>r y^\<^bsup>R i\<^esup>)) n = \<Sigma>\<^sub>e R (\<lambda>i.  (n choose i) \<times>\<^bsub>R\<^esub> (x^\<^bsup>R (n - i)\<^esup> \<cdot>\<^sub>r y^\<^bsup>R (i + 1)\<^esup>)) n
[PROOF STEP]
apply (simp only:nsMulDistrL add:nsClose add:ring_tOp_closed
         add:npClose)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>x \<in> carrier R; y \<in> carrier R; aGroup R\<rbrakk> \<Longrightarrow> \<Sigma>\<^sub>e R (\<lambda>i.  (n choose i) \<times>\<^bsub>R\<^esub> (y \<cdot>\<^sub>r (x^\<^bsup>R (n - i)\<^esup> \<cdot>\<^sub>r y^\<^bsup>R i\<^esup>))) n = \<Sigma>\<^sub>e R (\<lambda>i.  (n choose i) \<times>\<^bsub>R\<^esub> (x^\<^bsup>R (n - i)\<^esup> \<cdot>\<^sub>r y^\<^bsup>R (i + 1)\<^esup>)) n
[PROOF STEP]
apply (simp only: rMulLC [of "y"] add:npClose)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>x \<in> carrier R; y \<in> carrier R; aGroup R\<rbrakk> \<Longrightarrow> \<Sigma>\<^sub>e R (\<lambda>i.  (n choose i) \<times>\<^bsub>R\<^esub> (x^\<^bsup>R (n - i)\<^esup> \<cdot>\<^sub>r (y \<cdot>\<^sub>r y^\<^bsup>R i\<^esup>))) n = \<Sigma>\<^sub>e R (\<lambda>i.  (n choose i) \<times>\<^bsub>R\<^esub> (x^\<^bsup>R (n - i)\<^esup> \<cdot>\<^sub>r y^\<^bsup>R (i + 1)\<^esup>)) n
[PROOF STEP]
apply (simp del:npow_suc add:ring_tOp_commute[of y])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>x \<in> carrier R; y \<in> carrier R; aGroup R\<rbrakk> \<Longrightarrow> \<Sigma>\<^sub>e R (\<lambda>i.  (n choose i) \<times>\<^bsub>R\<^esub> (x^\<^bsup>R (n - i)\<^esup> \<cdot>\<^sub>r (y \<cdot>\<^sub>r y^\<^bsup>R i\<^esup>))) n = \<Sigma>\<^sub>e R (\<lambda>i.  (n choose i) \<times>\<^bsub>R\<^esub> (x^\<^bsup>R (n - i)\<^esup> \<cdot>\<^sub>r y^\<^bsup>R Suc i\<^esup>)) n
[PROOF STEP]
apply (rule aGroup.nsum_eq, assumption)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<lbrakk>x \<in> carrier R; y \<in> carrier R; aGroup R\<rbrakk> \<Longrightarrow> \<forall>j\<le>n.  (n choose j) \<times>\<^bsub>R\<^esub> (x^\<^bsup>R (n - j)\<^esup> \<cdot>\<^sub>r (y \<cdot>\<^sub>r y^\<^bsup>R j\<^esup>)) \<in> carrier R
 2. \<lbrakk>x \<in> carrier R; y \<in> carrier R; aGroup R\<rbrakk> \<Longrightarrow> \<forall>j\<le>n.  (n choose j) \<times>\<^bsub>R\<^esub> (x^\<^bsup>R (n - j)\<^esup> \<cdot>\<^sub>r y^\<^bsup>R Suc j\<^esup>) \<in> carrier R
 3. \<lbrakk>x \<in> carrier R; y \<in> carrier R; aGroup R\<rbrakk> \<Longrightarrow> \<forall>j\<le>n.  (n choose j) \<times>\<^bsub>R\<^esub> (x^\<^bsup>R (n - j)\<^esup> \<cdot>\<^sub>r (y \<cdot>\<^sub>r y^\<^bsup>R j\<^esup>)) =  (n choose j) \<times>\<^bsub>R\<^esub> (x^\<^bsup>R (n - j)\<^esup> \<cdot>\<^sub>r y^\<^bsup>R Suc j\<^esup>)
[PROOF STEP]
apply (rule allI, rule impI, rule nsClose,
         rule ring_tOp_closed, simp add:npClose,
         rule ring_tOp_closed, assumption, simp add:npClose)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>x \<in> carrier R; y \<in> carrier R; aGroup R\<rbrakk> \<Longrightarrow> \<forall>j\<le>n.  (n choose j) \<times>\<^bsub>R\<^esub> (x^\<^bsup>R (n - j)\<^esup> \<cdot>\<^sub>r y^\<^bsup>R Suc j\<^esup>) \<in> carrier R
 2. \<lbrakk>x \<in> carrier R; y \<in> carrier R; aGroup R\<rbrakk> \<Longrightarrow> \<forall>j\<le>n.  (n choose j) \<times>\<^bsub>R\<^esub> (x^\<^bsup>R (n - j)\<^esup> \<cdot>\<^sub>r (y \<cdot>\<^sub>r y^\<^bsup>R j\<^esup>)) =  (n choose j) \<times>\<^bsub>R\<^esub> (x^\<^bsup>R (n - j)\<^esup> \<cdot>\<^sub>r y^\<^bsup>R Suc j\<^esup>)
[PROOF STEP]
apply (rule allI, rule impI, rule nsClose,
         rule ring_tOp_closed, simp add:npClose,
         rule npClose, assumption)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>x \<in> carrier R; y \<in> carrier R; aGroup R\<rbrakk> \<Longrightarrow> \<forall>j\<le>n.  (n choose j) \<times>\<^bsub>R\<^esub> (x^\<^bsup>R (n - j)\<^esup> \<cdot>\<^sub>r (y \<cdot>\<^sub>r y^\<^bsup>R j\<^esup>)) =  (n choose j) \<times>\<^bsub>R\<^esub> (x^\<^bsup>R (n - j)\<^esup> \<cdot>\<^sub>r y^\<^bsup>R Suc j\<^esup>)
[PROOF STEP]
apply (rule allI, rule impI)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>j. \<lbrakk>x \<in> carrier R; y \<in> carrier R; aGroup R; j \<le> n\<rbrakk> \<Longrightarrow>  (n choose j) \<times>\<^bsub>R\<^esub> (x^\<^bsup>R (n - j)\<^esup> \<cdot>\<^sub>r (y \<cdot>\<^sub>r y^\<^bsup>R j\<^esup>)) =  (n choose j) \<times>\<^bsub>R\<^esub> (x^\<^bsup>R (n - j)\<^esup> \<cdot>\<^sub>r y^\<^bsup>R Suc j\<^esup>)
[PROOF STEP]
apply (frule_tac n = j in npClose[of y])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>j. \<lbrakk>x \<in> carrier R; y \<in> carrier R; aGroup R; j \<le> n; y^\<^bsup>R j\<^esup> \<in> carrier R\<rbrakk> \<Longrightarrow>  (n choose j) \<times>\<^bsub>R\<^esub> (x^\<^bsup>R (n - j)\<^esup> \<cdot>\<^sub>r (y \<cdot>\<^sub>r y^\<^bsup>R j\<^esup>)) =  (n choose j) \<times>\<^bsub>R\<^esub> (x^\<^bsup>R (n - j)\<^esup> \<cdot>\<^sub>r y^\<^bsup>R Suc j\<^esup>)
[PROOF STEP]
apply (simp add:ring_tOp_commute[of y])
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma binomial_n0: "(Suc n choose 0) = (n choose 0)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Suc n choose 0 = n choose 0
[PROOF STEP]
by simp


[STATEMENT]
lemma binomial_ngt_diff:
  "(n choose Suc n) = (Suc n choose Suc n) - (n choose n)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. n choose Suc n = Suc n choose Suc n - (n choose n)
[PROOF STEP]
by (subst binomial_Suc_Suc, arith)


[STATEMENT]
lemma binomial_ngt_0: "(n choose Suc n) = 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. n choose Suc n = 0
[PROOF STEP]
apply (subst binomial_ngt_diff,
         (subst binomial_n_n)+)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 1 - 1 = 0
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma diffLessSuc: "m \<le> n \<Longrightarrow> Suc (n-m) = Suc n - m"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. m \<le> n \<Longrightarrow> Suc (n - m) = Suc n - m
[PROOF STEP]
by arith


[STATEMENT]
lemma (in Ring) npow_suc_i:
  "\<lbrakk> x \<in> carrier R; i \<le> n \<rbrakk>
        \<Longrightarrow> npow R x (Suc n - i) =  x \<cdot>\<^sub>r (npow R x (n-i))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>x \<in> carrier R; i \<le> n\<rbrakk> \<Longrightarrow> x^\<^bsup>R (Suc n - i)\<^esup> = x \<cdot>\<^sub>r x^\<^bsup>R (n - i)\<^esup>
[PROOF STEP]
apply (subst diffLessSuc [THEN sym, of "i" "n"], assumption)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>x \<in> carrier R; i \<le> n\<rbrakk> \<Longrightarrow> x^\<^bsup>R Suc (n - i)\<^esup> = x \<cdot>\<^sub>r x^\<^bsup>R (n - i)\<^esup>
[PROOF STEP]
apply (frule_tac n = "n - i" in npClose,
         simp add:ring_tOp_commute[of x])
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma (in Ring) npeSum2_sub_mulx: "\<lbrakk> x \<in> carrier R; y \<in> carrier R \<rbrakk> \<Longrightarrow>
  x \<cdot>\<^sub>r (nsum R (\<lambda> i. nscal R ((npow R x (n-i)) \<cdot>\<^sub>r (npow R y i))
                                                        (n choose i)) n)
   = (nsum R (\<lambda>i. nscal R
                          ((npow R x (Suc n - Suc i)) \<cdot>\<^sub>r (npow R y (Suc i)))
                          (n choose Suc i)) n) \<plusminus>
                (nscal R ((npow R x (Suc n - 0)) \<cdot>\<^sub>r (npow R y 0))
                        (Suc n choose 0))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>x \<in> carrier R; y \<in> carrier R\<rbrakk> \<Longrightarrow> x \<cdot>\<^sub>r \<Sigma>\<^sub>e R (\<lambda>i.  (n choose i) \<times>\<^bsub>R\<^esub> (x^\<^bsup>R (n - i)\<^esup> \<cdot>\<^sub>r y^\<^bsup>R i\<^esup>)) n = \<Sigma>\<^sub>e R (\<lambda>i.  (n choose Suc i) \<times>\<^bsub>R\<^esub> (x^\<^bsup>R (Suc n - Suc i)\<^esup> \<cdot>\<^sub>r y^\<^bsup>R Suc i\<^esup>)) n \<plusminus>  (Suc n choose 0) \<times>\<^bsub>R\<^esub> (x^\<^bsup>R (Suc n - 0)\<^esup> \<cdot>\<^sub>r y^\<^bsup>R 0\<^esup>)
[PROOF STEP]
apply (cut_tac ring_is_ag)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>x \<in> carrier R; y \<in> carrier R; aGroup R\<rbrakk> \<Longrightarrow> x \<cdot>\<^sub>r \<Sigma>\<^sub>e R (\<lambda>i.  (n choose i) \<times>\<^bsub>R\<^esub> (x^\<^bsup>R (n - i)\<^esup> \<cdot>\<^sub>r y^\<^bsup>R i\<^esup>)) n = \<Sigma>\<^sub>e R (\<lambda>i.  (n choose Suc i) \<times>\<^bsub>R\<^esub> (x^\<^bsup>R (Suc n - Suc i)\<^esup> \<cdot>\<^sub>r y^\<^bsup>R Suc i\<^esup>)) n \<plusminus>  (Suc n choose 0) \<times>\<^bsub>R\<^esub> (x^\<^bsup>R (Suc n - 0)\<^esup> \<cdot>\<^sub>r y^\<^bsup>R 0\<^esup>)
[PROOF STEP]
apply (simp only: binomial_n0)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>x \<in> carrier R; y \<in> carrier R; aGroup R\<rbrakk> \<Longrightarrow> x \<cdot>\<^sub>r \<Sigma>\<^sub>e R (\<lambda>i.  (n choose i) \<times>\<^bsub>R\<^esub> (x^\<^bsup>R (n - i)\<^esup> \<cdot>\<^sub>r y^\<^bsup>R i\<^esup>)) n = \<Sigma>\<^sub>e R (\<lambda>i.  (n choose Suc i) \<times>\<^bsub>R\<^esub> (x^\<^bsup>R (Suc n - Suc i)\<^esup> \<cdot>\<^sub>r y^\<^bsup>R Suc i\<^esup>)) n \<plusminus>  (n choose 0) \<times>\<^bsub>R\<^esub> (x^\<^bsup>R (Suc n - 0)\<^esup> \<cdot>\<^sub>r y^\<^bsup>R 0\<^esup>)
[PROOF STEP]
apply (subst aGroup.nsumElmTail [THEN sym, of R "\<lambda> i. nscal R ((npow R x (Suc n - i)) \<cdot>\<^sub>r (npow R y i)) (n choose i)"], assumption+)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>x \<in> carrier R; y \<in> carrier R; aGroup R\<rbrakk> \<Longrightarrow> \<forall>i.  (n choose i) \<times>\<^bsub>R\<^esub> (x^\<^bsup>R (Suc n - i)\<^esup> \<cdot>\<^sub>r y^\<^bsup>R i\<^esup>) \<in> carrier R
 2. \<lbrakk>x \<in> carrier R; y \<in> carrier R; aGroup R\<rbrakk> \<Longrightarrow> x \<cdot>\<^sub>r \<Sigma>\<^sub>e R (\<lambda>i.  (n choose i) \<times>\<^bsub>R\<^esub> (x^\<^bsup>R (n - i)\<^esup> \<cdot>\<^sub>r y^\<^bsup>R i\<^esup>)) n = \<Sigma>\<^sub>e R (\<lambda>i.  (n choose i) \<times>\<^bsub>R\<^esub> (x^\<^bsup>R (Suc n - i)\<^esup> \<cdot>\<^sub>r y^\<^bsup>R i\<^esup>)) Suc n
[PROOF STEP]
apply (rule allI)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>i. \<lbrakk>x \<in> carrier R; y \<in> carrier R; aGroup R\<rbrakk> \<Longrightarrow>  (n choose i) \<times>\<^bsub>R\<^esub> (x^\<^bsup>R (Suc n - i)\<^esup> \<cdot>\<^sub>r y^\<^bsup>R i\<^esup>) \<in> carrier R
 2. \<lbrakk>x \<in> carrier R; y \<in> carrier R; aGroup R\<rbrakk> \<Longrightarrow> x \<cdot>\<^sub>r \<Sigma>\<^sub>e R (\<lambda>i.  (n choose i) \<times>\<^bsub>R\<^esub> (x^\<^bsup>R (n - i)\<^esup> \<cdot>\<^sub>r y^\<^bsup>R i\<^esup>)) n = \<Sigma>\<^sub>e R (\<lambda>i.  (n choose i) \<times>\<^bsub>R\<^esub> (x^\<^bsup>R (Suc n - i)\<^esup> \<cdot>\<^sub>r y^\<^bsup>R i\<^esup>)) Suc n
[PROOF STEP]
apply (simp only:nsClose add:ring_tOp_closed add:npClose)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>x \<in> carrier R; y \<in> carrier R; aGroup R\<rbrakk> \<Longrightarrow> x \<cdot>\<^sub>r \<Sigma>\<^sub>e R (\<lambda>i.  (n choose i) \<times>\<^bsub>R\<^esub> (x^\<^bsup>R (n - i)\<^esup> \<cdot>\<^sub>r y^\<^bsup>R i\<^esup>)) n = \<Sigma>\<^sub>e R (\<lambda>i.  (n choose i) \<times>\<^bsub>R\<^esub> (x^\<^bsup>R (Suc n - i)\<^esup> \<cdot>\<^sub>r y^\<^bsup>R i\<^esup>)) Suc n
[PROOF STEP]
apply (simp only:nsum_suc)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>x \<in> carrier R; y \<in> carrier R; aGroup R\<rbrakk> \<Longrightarrow> x \<cdot>\<^sub>r \<Sigma>\<^sub>e R (\<lambda>i.  (n choose i) \<times>\<^bsub>R\<^esub> (x^\<^bsup>R (n - i)\<^esup> \<cdot>\<^sub>r y^\<^bsup>R i\<^esup>)) n = \<Sigma>\<^sub>e R (\<lambda>i.  (n choose i) \<times>\<^bsub>R\<^esub> (x^\<^bsup>R (Suc n - i)\<^esup> \<cdot>\<^sub>r y^\<^bsup>R i\<^esup>)) n \<plusminus>  (n choose Suc n) \<times>\<^bsub>R\<^esub> (x^\<^bsup>R (Suc n - Suc n)\<^esup> \<cdot>\<^sub>r y^\<^bsup>R Suc n\<^esup>)
[PROOF STEP]
apply (subst binomial_ngt_0)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>x \<in> carrier R; y \<in> carrier R; aGroup R\<rbrakk> \<Longrightarrow> x \<cdot>\<^sub>r \<Sigma>\<^sub>e R (\<lambda>i.  (n choose i) \<times>\<^bsub>R\<^esub> (x^\<^bsup>R (n - i)\<^esup> \<cdot>\<^sub>r y^\<^bsup>R i\<^esup>)) n = \<Sigma>\<^sub>e R (\<lambda>i.  (n choose i) \<times>\<^bsub>R\<^esub> (x^\<^bsup>R (Suc n - i)\<^esup> \<cdot>\<^sub>r y^\<^bsup>R i\<^esup>)) n \<plusminus>  0 \<times>\<^bsub>R\<^esub> (x^\<^bsup>R (Suc n - Suc n)\<^esup> \<cdot>\<^sub>r y^\<^bsup>R Suc n\<^esup>)
[PROOF STEP]
apply (simp only:nscal_0)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>x \<in> carrier R; y \<in> carrier R; aGroup R\<rbrakk> \<Longrightarrow> x \<cdot>\<^sub>r \<Sigma>\<^sub>e R (\<lambda>i.  (n choose i) \<times>\<^bsub>R\<^esub> (x^\<^bsup>R (n - i)\<^esup> \<cdot>\<^sub>r y^\<^bsup>R i\<^esup>)) n = \<Sigma>\<^sub>e R (\<lambda>i.  (n choose i) \<times>\<^bsub>R\<^esub> (x^\<^bsup>R (Suc n - i)\<^esup> \<cdot>\<^sub>r y^\<^bsup>R i\<^esup>)) n \<plusminus> \<zero>
[PROOF STEP]
apply (subst aGroup.ag_r_zero, assumption)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>x \<in> carrier R; y \<in> carrier R; aGroup R\<rbrakk> \<Longrightarrow> \<Sigma>\<^sub>e R (\<lambda>i.  (n choose i) \<times>\<^bsub>R\<^esub> (x^\<^bsup>R (Suc n - i)\<^esup> \<cdot>\<^sub>r y^\<^bsup>R i\<^esup>)) n \<in> carrier R
 2. \<lbrakk>x \<in> carrier R; y \<in> carrier R; aGroup R\<rbrakk> \<Longrightarrow> x \<cdot>\<^sub>r \<Sigma>\<^sub>e R (\<lambda>i.  (n choose i) \<times>\<^bsub>R\<^esub> (x^\<^bsup>R (n - i)\<^esup> \<cdot>\<^sub>r y^\<^bsup>R i\<^esup>)) n = \<Sigma>\<^sub>e R (\<lambda>i.  (n choose i) \<times>\<^bsub>R\<^esub> (x^\<^bsup>R (Suc n - i)\<^esup> \<cdot>\<^sub>r y^\<^bsup>R i\<^esup>)) n
[PROOF STEP]
apply (simp add:aGroup.nsum_mem nsClose ring_tOp_closed npClose)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>x \<in> carrier R; y \<in> carrier R; aGroup R\<rbrakk> \<Longrightarrow> x \<cdot>\<^sub>r \<Sigma>\<^sub>e R (\<lambda>i.  (n choose i) \<times>\<^bsub>R\<^esub> (x^\<^bsup>R (n - i)\<^esup> \<cdot>\<^sub>r y^\<^bsup>R i\<^esup>)) n = \<Sigma>\<^sub>e R (\<lambda>i.  (n choose i) \<times>\<^bsub>R\<^esub> (x^\<^bsup>R (Suc n - i)\<^esup> \<cdot>\<^sub>r y^\<^bsup>R i\<^esup>)) n
[PROOF STEP]
apply (subst nsumMulElmL [of  _ "x"])
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<lbrakk>x \<in> carrier R; y \<in> carrier R; aGroup R\<rbrakk> \<Longrightarrow> \<forall>i.  (n choose i) \<times>\<^bsub>R\<^esub> (x^\<^bsup>R (n - i)\<^esup> \<cdot>\<^sub>r y^\<^bsup>R i\<^esup>) \<in> carrier R
 2. \<lbrakk>x \<in> carrier R; y \<in> carrier R; aGroup R\<rbrakk> \<Longrightarrow> x \<in> carrier R
 3. \<lbrakk>x \<in> carrier R; y \<in> carrier R; aGroup R\<rbrakk> \<Longrightarrow> \<Sigma>\<^sub>e R (\<lambda>i. x \<cdot>\<^sub>r  (n choose i) \<times>\<^bsub>R\<^esub> (x^\<^bsup>R (n - i)\<^esup> \<cdot>\<^sub>r y^\<^bsup>R i\<^esup>)) n = \<Sigma>\<^sub>e R (\<lambda>i.  (n choose i) \<times>\<^bsub>R\<^esub> (x^\<^bsup>R (Suc n - i)\<^esup> \<cdot>\<^sub>r y^\<^bsup>R i\<^esup>)) n
[PROOF STEP]
apply (rule allI, rule nsClose, rule ring_tOp_closed, simp add:npClose,
           simp add:npClose, assumption)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>x \<in> carrier R; y \<in> carrier R; aGroup R\<rbrakk> \<Longrightarrow> \<Sigma>\<^sub>e R (\<lambda>i. x \<cdot>\<^sub>r  (n choose i) \<times>\<^bsub>R\<^esub> (x^\<^bsup>R (n - i)\<^esup> \<cdot>\<^sub>r y^\<^bsup>R i\<^esup>)) n = \<Sigma>\<^sub>e R (\<lambda>i.  (n choose i) \<times>\<^bsub>R\<^esub> (x^\<^bsup>R (Suc n - i)\<^esup> \<cdot>\<^sub>r y^\<^bsup>R i\<^esup>)) n
[PROOF STEP]
apply (simp add: nsMulDistrL [of "x"] ring_tOp_closed npClose)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>x \<in> carrier R; y \<in> carrier R; aGroup R\<rbrakk> \<Longrightarrow> \<Sigma>\<^sub>e R (\<lambda>i.  (n choose i) \<times>\<^bsub>R\<^esub> (x \<cdot>\<^sub>r (x^\<^bsup>R (n - i)\<^esup> \<cdot>\<^sub>r y^\<^bsup>R i\<^esup>))) n = \<Sigma>\<^sub>e R (\<lambda>i.  (n choose i) \<times>\<^bsub>R\<^esub> (x^\<^bsup>R (Suc n - i)\<^esup> \<cdot>\<^sub>r y^\<^bsup>R i\<^esup>)) n
[PROOF STEP]
apply (simp add:ring_tOp_assoc [THEN sym, of "x"] npClose)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>x \<in> carrier R; y \<in> carrier R; aGroup R\<rbrakk> \<Longrightarrow> \<Sigma>\<^sub>e R (\<lambda>i.  (n choose i) \<times>\<^bsub>R\<^esub> (x \<cdot>\<^sub>r x^\<^bsup>R (n - i)\<^esup> \<cdot>\<^sub>r y^\<^bsup>R i\<^esup>)) n = \<Sigma>\<^sub>e R (\<lambda>i.  (n choose i) \<times>\<^bsub>R\<^esub> (x^\<^bsup>R (Suc n - i)\<^esup> \<cdot>\<^sub>r y^\<^bsup>R i\<^esup>)) n
[PROOF STEP]
apply (rule aGroup.nsum_eq, assumption)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<lbrakk>x \<in> carrier R; y \<in> carrier R; aGroup R\<rbrakk> \<Longrightarrow> \<forall>j\<le>n.  (n choose j) \<times>\<^bsub>R\<^esub> (x \<cdot>\<^sub>r x^\<^bsup>R (n - j)\<^esup> \<cdot>\<^sub>r y^\<^bsup>R j\<^esup>) \<in> carrier R
 2. \<lbrakk>x \<in> carrier R; y \<in> carrier R; aGroup R\<rbrakk> \<Longrightarrow> \<forall>j\<le>n.  (n choose j) \<times>\<^bsub>R\<^esub> (x^\<^bsup>R (Suc n - j)\<^esup> \<cdot>\<^sub>r y^\<^bsup>R j\<^esup>) \<in> carrier R
 3. \<lbrakk>x \<in> carrier R; y \<in> carrier R; aGroup R\<rbrakk> \<Longrightarrow> \<forall>j\<le>n.  (n choose j) \<times>\<^bsub>R\<^esub> (x \<cdot>\<^sub>r x^\<^bsup>R (n - j)\<^esup> \<cdot>\<^sub>r y^\<^bsup>R j\<^esup>) =  (n choose j) \<times>\<^bsub>R\<^esub> (x^\<^bsup>R (Suc n - j)\<^esup> \<cdot>\<^sub>r y^\<^bsup>R j\<^esup>)
[PROOF STEP]
apply (rule allI, rule impI,
          rule nsClose, (rule ring_tOp_closed)+, assumption,
          simp add:npClose, simp add:npClose)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>x \<in> carrier R; y \<in> carrier R; aGroup R\<rbrakk> \<Longrightarrow> \<forall>j\<le>n.  (n choose j) \<times>\<^bsub>R\<^esub> (x^\<^bsup>R (Suc n - j)\<^esup> \<cdot>\<^sub>r y^\<^bsup>R j\<^esup>) \<in> carrier R
 2. \<lbrakk>x \<in> carrier R; y \<in> carrier R; aGroup R\<rbrakk> \<Longrightarrow> \<forall>j\<le>n.  (n choose j) \<times>\<^bsub>R\<^esub> (x \<cdot>\<^sub>r x^\<^bsup>R (n - j)\<^esup> \<cdot>\<^sub>r y^\<^bsup>R j\<^esup>) =  (n choose j) \<times>\<^bsub>R\<^esub> (x^\<^bsup>R (Suc n - j)\<^esup> \<cdot>\<^sub>r y^\<^bsup>R j\<^esup>)
[PROOF STEP]
apply (rule allI, rule impI,
          rule nsClose, rule ring_tOp_closed,
          simp add:npClose, simp add:npClose)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>x \<in> carrier R; y \<in> carrier R; aGroup R\<rbrakk> \<Longrightarrow> \<forall>j\<le>n.  (n choose j) \<times>\<^bsub>R\<^esub> (x \<cdot>\<^sub>r x^\<^bsup>R (n - j)\<^esup> \<cdot>\<^sub>r y^\<^bsup>R j\<^esup>) =  (n choose j) \<times>\<^bsub>R\<^esub> (x^\<^bsup>R (Suc n - j)\<^esup> \<cdot>\<^sub>r y^\<^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; y \<in> carrier R; aGroup R; j \<le> n\<rbrakk> \<Longrightarrow>  (n choose j) \<times>\<^bsub>R\<^esub> (x \<cdot>\<^sub>r x^\<^bsup>R (n - j)\<^esup> \<cdot>\<^sub>r y^\<^bsup>R j\<^esup>) =  (n choose j) \<times>\<^bsub>R\<^esub> (x^\<^bsup>R (Suc n - j)\<^esup> \<cdot>\<^sub>r y^\<^bsup>R j\<^esup>)
[PROOF STEP]
apply (frule_tac n = "n - j" in npClose[of x],
        simp add:ring_tOp_commute[of x],
        subst npow_suc[THEN sym])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>j. \<lbrakk>x \<in> carrier R; y \<in> carrier R; aGroup R; j \<le> n; x^\<^bsup>R (n - j)\<^esup> \<in> carrier R\<rbrakk> \<Longrightarrow>  (n choose j) \<times>\<^bsub>R\<^esub> (x^\<^bsup>R Suc (n - j)\<^esup> \<cdot>\<^sub>r y^\<^bsup>R j\<^esup>) =  (n choose j) \<times>\<^bsub>R\<^esub> (x^\<^bsup>R (Suc n - j)\<^esup> \<cdot>\<^sub>r y^\<^bsup>R j\<^esup>)
[PROOF STEP]
apply (simp add:Suc_diff_le)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma (in Ring) npeSum2_sub_mulx2:
  "\<lbrakk> x \<in> carrier R; y \<in> carrier R \<rbrakk> \<Longrightarrow>
        x \<cdot>\<^sub>r (nsum R (\<lambda> i. nscal R ((npow R x (n-i)) \<cdot>\<^sub>r (npow R y i))
                                (n choose i)) n)
        = (nsum R  (\<lambda>i. nscal R
                          ((npow R x (n - i)) \<cdot>\<^sub>r ((npow R y i) \<cdot>\<^sub>r y ))
                          (n choose Suc i)) n) \<plusminus>
                (\<zero> \<plusminus> ((x \<cdot>\<^sub>r (npow R x n)) \<cdot>\<^sub>r (1\<^sub>r)))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>x \<in> carrier R; y \<in> carrier R\<rbrakk> \<Longrightarrow> x \<cdot>\<^sub>r \<Sigma>\<^sub>e R (\<lambda>i.  (n choose i) \<times>\<^bsub>R\<^esub> (x^\<^bsup>R (n - i)\<^esup> \<cdot>\<^sub>r y^\<^bsup>R i\<^esup>)) n = \<Sigma>\<^sub>e R (\<lambda>i.  (n choose Suc i) \<times>\<^bsub>R\<^esub> (x^\<^bsup>R (n - i)\<^esup> \<cdot>\<^sub>r (y^\<^bsup>R i\<^esup> \<cdot>\<^sub>r y))) n \<plusminus> (\<zero> \<plusminus> x \<cdot>\<^sub>r x^\<^bsup>R n\<^esup> \<cdot>\<^sub>r 1\<^sub>r)
[PROOF STEP]
apply (subst  npeSum2_sub_mulx, assumption+, simp)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>x \<in> carrier R; y \<in> carrier R\<rbrakk> \<Longrightarrow> \<Sigma>\<^sub>e R (\<lambda>i.  (n choose Suc i) \<times>\<^bsub>R\<^esub> (x^\<^bsup>R (n - i)\<^esup> \<cdot>\<^sub>r (y^\<^bsup>R i\<^esup> \<cdot>\<^sub>r y))) n \<plusminus> (\<zero> \<plusminus> x^\<^bsup>R n\<^esup> \<cdot>\<^sub>r x \<cdot>\<^sub>r 1\<^sub>r) = \<Sigma>\<^sub>e R (\<lambda>i.  (n choose Suc i) \<times>\<^bsub>R\<^esub> (x^\<^bsup>R (n - i)\<^esup> \<cdot>\<^sub>r (y^\<^bsup>R i\<^esup> \<cdot>\<^sub>r y))) n \<plusminus> (\<zero> \<plusminus> x \<cdot>\<^sub>r x^\<^bsup>R n\<^esup> \<cdot>\<^sub>r 1\<^sub>r)
[PROOF STEP]
apply (frule npClose[of x n])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>x \<in> carrier R; y \<in> carrier R; x^\<^bsup>R n\<^esup> \<in> carrier R\<rbrakk> \<Longrightarrow> \<Sigma>\<^sub>e R (\<lambda>i.  (n choose Suc i) \<times>\<^bsub>R\<^esub> (x^\<^bsup>R (n - i)\<^esup> \<cdot>\<^sub>r (y^\<^bsup>R i\<^esup> \<cdot>\<^sub>r y))) n \<plusminus> (\<zero> \<plusminus> x^\<^bsup>R n\<^esup> \<cdot>\<^sub>r x \<cdot>\<^sub>r 1\<^sub>r) = \<Sigma>\<^sub>e R (\<lambda>i.  (n choose Suc i) \<times>\<^bsub>R\<^esub> (x^\<^bsup>R (n - i)\<^esup> \<cdot>\<^sub>r (y^\<^bsup>R i\<^esup> \<cdot>\<^sub>r y))) n \<plusminus> (\<zero> \<plusminus> x \<cdot>\<^sub>r x^\<^bsup>R n\<^esup> \<cdot>\<^sub>r 1\<^sub>r)
[PROOF STEP]
apply (subst ring_tOp_commute[of x], assumption+)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>x \<in> carrier R; y \<in> carrier R; x^\<^bsup>R n\<^esup> \<in> carrier R\<rbrakk> \<Longrightarrow> \<Sigma>\<^sub>e R (\<lambda>i.  (n choose Suc i) \<times>\<^bsub>R\<^esub> (x^\<^bsup>R (n - i)\<^esup> \<cdot>\<^sub>r (y^\<^bsup>R i\<^esup> \<cdot>\<^sub>r y))) n \<plusminus> (\<zero> \<plusminus> x^\<^bsup>R n\<^esup> \<cdot>\<^sub>r x \<cdot>\<^sub>r 1\<^sub>r) = \<Sigma>\<^sub>e R (\<lambda>i.  (n choose Suc i) \<times>\<^bsub>R\<^esub> (x^\<^bsup>R (n - i)\<^esup> \<cdot>\<^sub>r (y^\<^bsup>R i\<^esup> \<cdot>\<^sub>r y))) n \<plusminus> (\<zero> \<plusminus> x^\<^bsup>R n\<^esup> \<cdot>\<^sub>r x \<cdot>\<^sub>r 1\<^sub>r)
[PROOF STEP]
apply (cut_tac ring_is_ag)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>x \<in> carrier R; y \<in> carrier R; x^\<^bsup>R n\<^esup> \<in> carrier R; aGroup R\<rbrakk> \<Longrightarrow> \<Sigma>\<^sub>e R (\<lambda>i.  (n choose Suc i) \<times>\<^bsub>R\<^esub> (x^\<^bsup>R (n - i)\<^esup> \<cdot>\<^sub>r (y^\<^bsup>R i\<^esup> \<cdot>\<^sub>r y))) n \<plusminus> (\<zero> \<plusminus> x^\<^bsup>R n\<^esup> \<cdot>\<^sub>r x \<cdot>\<^sub>r 1\<^sub>r) = \<Sigma>\<^sub>e R (\<lambda>i.  (n choose Suc i) \<times>\<^bsub>R\<^esub> (x^\<^bsup>R (n - i)\<^esup> \<cdot>\<^sub>r (y^\<^bsup>R i\<^esup> \<cdot>\<^sub>r y))) n \<plusminus> (\<zero> \<plusminus> x^\<^bsup>R n\<^esup> \<cdot>\<^sub>r x \<cdot>\<^sub>r 1\<^sub>r)
[PROOF STEP]
apply (cut_tac aGroup.nsum_eq[of R n
        "\<lambda>i.  (n choose Suc i) \<times>\<^bsub>R\<^esub> (x^\<^bsup>R (n - i)\<^esup> \<cdot>\<^sub>r y^\<^bsup>R (Suc i)\<^esup>)"
        "\<lambda>i.  (n choose Suc i) \<times>\<^bsub>R\<^esub> (x^\<^bsup>R (n - i)\<^esup> \<cdot>\<^sub>r (y^\<^bsup>R i\<^esup> \<cdot>\<^sub>r y))"])
[PROOF STATE]
proof (prove)
goal (5 subgoals):
 1. \<lbrakk>x \<in> carrier R; y \<in> carrier R; x^\<^bsup>R n\<^esup> \<in> carrier R; aGroup R; \<Sigma>\<^sub>e R (\<lambda>i.  (n choose Suc i) \<times>\<^bsub>R\<^esub> (x^\<^bsup>R (n - i)\<^esup> \<cdot>\<^sub>r y^\<^bsup>R Suc i\<^esup>)) n = \<Sigma>\<^sub>e R (\<lambda>i.  (n choose Suc i) \<times>\<^bsub>R\<^esub> (x^\<^bsup>R (n - i)\<^esup> \<cdot>\<^sub>r (y^\<^bsup>R i\<^esup> \<cdot>\<^sub>r y))) n\<rbrakk> \<Longrightarrow> \<Sigma>\<^sub>e R (\<lambda>i.  (n choose Suc i) \<times>\<^bsub>R\<^esub> (x^\<^bsup>R (n - i)\<^esup> \<cdot>\<^sub>r (y^\<^bsup>R i\<^esup> \<cdot>\<^sub>r y))) n \<plusminus> (\<zero> \<plusminus> x^\<^bsup>R n\<^esup> \<cdot>\<^sub>r x \<cdot>\<^sub>r 1\<^sub>r) = \<Sigma>\<^sub>e R (\<lambda>i.  (n choose Suc i) \<times>\<^bsub>R\<^esub> (x^\<^bsup>R (n - i)\<^esup> \<cdot>\<^sub>r (y^\<^bsup>R i\<^esup> \<cdot>\<^sub>r y))) n \<plusminus> (\<zero> \<plusminus> x^\<^bsup>R n\<^esup> \<cdot>\<^sub>r x \<cdot>\<^sub>r 1\<^sub>r)
 2. \<lbrakk>x \<in> carrier R; y \<in> carrier R; x^\<^bsup>R n\<^esup> \<in> carrier R; aGroup R\<rbrakk> \<Longrightarrow> aGroup R
 3. \<lbrakk>x \<in> carrier R; y \<in> carrier R; x^\<^bsup>R n\<^esup> \<in> carrier R; aGroup R\<rbrakk> \<Longrightarrow> \<forall>j\<le>n.  (n choose Suc j) \<times>\<^bsub>R\<^esub> (x^\<^bsup>R (n - j)\<^esup> \<cdot>\<^sub>r y^\<^bsup>R Suc j\<^esup>) \<in> carrier R
 4. \<lbrakk>x \<in> carrier R; y \<in> carrier R; x^\<^bsup>R n\<^esup> \<in> carrier R; aGroup R\<rbrakk> \<Longrightarrow> \<forall>j\<le>n.  (n choose Suc j) \<times>\<^bsub>R\<^esub> (x^\<^bsup>R (n - j)\<^esup> \<cdot>\<^sub>r (y^\<^bsup>R j\<^esup> \<cdot>\<^sub>r y)) \<in> carrier R
 5. \<lbrakk>x \<in> carrier R; y \<in> carrier R; x^\<^bsup>R n\<^esup> \<in> carrier R; aGroup R\<rbrakk> \<Longrightarrow> \<forall>j\<le>n.  (n choose Suc j) \<times>\<^bsub>R\<^esub> (x^\<^bsup>R (n - j)\<^esup> \<cdot>\<^sub>r y^\<^bsup>R Suc j\<^esup>) =  (n choose Suc j) \<times>\<^bsub>R\<^esub> (x^\<^bsup>R (n - j)\<^esup> \<cdot>\<^sub>r (y^\<^bsup>R j\<^esup> \<cdot>\<^sub>r y))
[PROOF STEP]
apply (simp del:npow_suc)+
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<lbrakk>x \<in> carrier R; y \<in> carrier R; x^\<^bsup>R n\<^esup> \<in> carrier R; aGroup R\<rbrakk> \<Longrightarrow> \<forall>j\<le>n.  (n choose Suc j) \<times>\<^bsub>R\<^esub> (x^\<^bsup>R (n - j)\<^esup> \<cdot>\<^sub>r y^\<^bsup>R Suc j\<^esup>) \<in> carrier R
 2. \<lbrakk>x \<in> carrier R; y \<in> carrier R; x^\<^bsup>R n\<^esup> \<in> carrier R; aGroup R\<rbrakk> \<Longrightarrow> \<forall>j\<le>n.  (n choose Suc j) \<times>\<^bsub>R\<^esub> (x^\<^bsup>R (n - j)\<^esup> \<cdot>\<^sub>r (y^\<^bsup>R j\<^esup> \<cdot>\<^sub>r y)) \<in> carrier R
 3. \<lbrakk>x \<in> carrier R; y \<in> carrier R; x^\<^bsup>R n\<^esup> \<in> carrier R; aGroup R\<rbrakk> \<Longrightarrow> \<forall>j\<le>n.  (n choose Suc j) \<times>\<^bsub>R\<^esub> (x^\<^bsup>R (n - j)\<^esup> \<cdot>\<^sub>r y^\<^bsup>R Suc j\<^esup>) =  (n choose Suc j) \<times>\<^bsub>R\<^esub> (x^\<^bsup>R (n - j)\<^esup> \<cdot>\<^sub>r (y^\<^bsup>R j\<^esup> \<cdot>\<^sub>r y))
[PROOF STEP]
apply (rule allI, rule impI,
         rule nsClose, rule ring_tOp_closed, simp add:npClose,
         simp only:npClose)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>x \<in> carrier R; y \<in> carrier R; x^\<^bsup>R n\<^esup> \<in> carrier R; aGroup R\<rbrakk> \<Longrightarrow> \<forall>j\<le>n.  (n choose Suc j) \<times>\<^bsub>R\<^esub> (x^\<^bsup>R (n - j)\<^esup> \<cdot>\<^sub>r (y^\<^bsup>R j\<^esup> \<cdot>\<^sub>r y)) \<in> carrier R
 2. \<lbrakk>x \<in> carrier R; y \<in> carrier R; x^\<^bsup>R n\<^esup> \<in> carrier R; aGroup R\<rbrakk> \<Longrightarrow> \<forall>j\<le>n.  (n choose Suc j) \<times>\<^bsub>R\<^esub> (x^\<^bsup>R (n - j)\<^esup> \<cdot>\<^sub>r y^\<^bsup>R Suc j\<^esup>) =  (n choose Suc j) \<times>\<^bsub>R\<^esub> (x^\<^bsup>R (n - j)\<^esup> \<cdot>\<^sub>r (y^\<^bsup>R j\<^esup> \<cdot>\<^sub>r y))
[PROOF STEP]
apply (rule allI, rule impI,
         rule nsClose, rule ring_tOp_closed, simp add:npClose,
         rule ring_tOp_closed, simp add:npClose, assumption)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>x \<in> carrier R; y \<in> carrier R; x^\<^bsup>R n\<^esup> \<in> carrier R; aGroup R\<rbrakk> \<Longrightarrow> \<forall>j\<le>n.  (n choose Suc j) \<times>\<^bsub>R\<^esub> (x^\<^bsup>R (n - j)\<^esup> \<cdot>\<^sub>r y^\<^bsup>R Suc j\<^esup>) =  (n choose Suc j) \<times>\<^bsub>R\<^esub> (x^\<^bsup>R (n - j)\<^esup> \<cdot>\<^sub>r (y^\<^bsup>R j\<^esup> \<cdot>\<^sub>r y))
[PROOF STEP]
apply (rule allI, rule impI)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>j. \<lbrakk>x \<in> carrier R; y \<in> carrier R; x^\<^bsup>R n\<^esup> \<in> carrier R; aGroup R; j \<le> n\<rbrakk> \<Longrightarrow>  (n choose Suc j) \<times>\<^bsub>R\<^esub> (x^\<^bsup>R (n - j)\<^esup> \<cdot>\<^sub>r y^\<^bsup>R Suc j\<^esup>) =  (n choose Suc j) \<times>\<^bsub>R\<^esub> (x^\<^bsup>R (n - j)\<^esup> \<cdot>\<^sub>r (y^\<^bsup>R j\<^esup> \<cdot>\<^sub>r y))
[PROOF STEP]
apply (frule_tac n = j in npClose[of y])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>j. \<lbrakk>x \<in> carrier R; y \<in> carrier R; x^\<^bsup>R n\<^esup> \<in> carrier R; aGroup R; j \<le> n; y^\<^bsup>R j\<^esup> \<in> carrier R\<rbrakk> \<Longrightarrow>  (n choose Suc j) \<times>\<^bsub>R\<^esub> (x^\<^bsup>R (n - j)\<^esup> \<cdot>\<^sub>r y^\<^bsup>R Suc j\<^esup>) =  (n choose Suc j) \<times>\<^bsub>R\<^esub> (x^\<^bsup>R (n - j)\<^esup> \<cdot>\<^sub>r (y^\<^bsup>R j\<^esup> \<cdot>\<^sub>r y))
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done