[STATEMENT]
lemma (in Ring) ideal_prod_ideal:"\<lbrakk>ideal R I; ideal R J \<rbrakk> \<Longrightarrow>
                                        ideal R (I \<diamondsuit>\<^sub>r J)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ideal R I; ideal R J\<rbrakk> \<Longrightarrow> ideal R (I \<diamondsuit>\<^sub>r J)
[PROOF STEP]
apply (rule ideal_condition1)
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<lbrakk>ideal R I; ideal R J\<rbrakk> \<Longrightarrow> I \<diamondsuit>\<^sub>r J \<subseteq> carrier R
 2. \<lbrakk>ideal R I; ideal R J\<rbrakk> \<Longrightarrow> I \<diamondsuit>\<^sub>r J \<noteq> {}
 3. \<lbrakk>ideal R I; ideal R J\<rbrakk> \<Longrightarrow> \<forall>x\<in>I \<diamondsuit>\<^sub>r J. \<forall>y\<in>I \<diamondsuit>\<^sub>r J. x \<plusminus> y \<in> I \<diamondsuit>\<^sub>r J
 4. \<lbrakk>ideal R I; ideal R J\<rbrakk> \<Longrightarrow> \<forall>r\<in>carrier R. \<forall>x\<in>I \<diamondsuit>\<^sub>r J. r \<cdot>\<^sub>r x \<in> I \<diamondsuit>\<^sub>r J
[PROOF STEP]
apply (simp add:ideal_prod_def)
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<lbrakk>ideal R I; ideal R J\<rbrakk> \<Longrightarrow> \<Inter> {L. ideal R L \<and> {x. \<exists>i\<in>I. \<exists>j\<in>J. x = i \<cdot>\<^sub>r j} \<subseteq> L} \<subseteq> carrier R
 2. \<lbrakk>ideal R I; ideal R J\<rbrakk> \<Longrightarrow> I \<diamondsuit>\<^sub>r J \<noteq> {}
 3. \<lbrakk>ideal R I; ideal R J\<rbrakk> \<Longrightarrow> \<forall>x\<in>I \<diamondsuit>\<^sub>r J. \<forall>y\<in>I \<diamondsuit>\<^sub>r J. x \<plusminus> y \<in> I \<diamondsuit>\<^sub>r J
 4. \<lbrakk>ideal R I; ideal R J\<rbrakk> \<Longrightarrow> \<forall>r\<in>carrier R. \<forall>x\<in>I \<diamondsuit>\<^sub>r J. r \<cdot>\<^sub>r x \<in> I \<diamondsuit>\<^sub>r J
[PROOF STEP]
apply (rule subsetI, simp)
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<And>x. \<lbrakk>ideal R I; ideal R J; \<forall>xa. ideal R xa \<and> {x. \<exists>i\<in>I. \<exists>j\<in>J. x = i \<cdot>\<^sub>r j} \<subseteq> xa \<longrightarrow> x \<in> xa\<rbrakk> \<Longrightarrow> x \<in> carrier R
 2. \<lbrakk>ideal R I; ideal R J\<rbrakk> \<Longrightarrow> I \<diamondsuit>\<^sub>r J \<noteq> {}
 3. \<lbrakk>ideal R I; ideal R J\<rbrakk> \<Longrightarrow> \<forall>x\<in>I \<diamondsuit>\<^sub>r J. \<forall>y\<in>I \<diamondsuit>\<^sub>r J. x \<plusminus> y \<in> I \<diamondsuit>\<^sub>r J
 4. \<lbrakk>ideal R I; ideal R J\<rbrakk> \<Longrightarrow> \<forall>r\<in>carrier R. \<forall>x\<in>I \<diamondsuit>\<^sub>r J. r \<cdot>\<^sub>r x \<in> I \<diamondsuit>\<^sub>r J
[PROOF STEP]
apply (cut_tac whole_ideal)
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<And>x. \<lbrakk>ideal R I; ideal R J; \<forall>xa. ideal R xa \<and> {x. \<exists>i\<in>I. \<exists>j\<in>J. x = i \<cdot>\<^sub>r j} \<subseteq> xa \<longrightarrow> x \<in> xa; ideal R (carrier R)\<rbrakk> \<Longrightarrow> x \<in> carrier R
 2. \<lbrakk>ideal R I; ideal R J\<rbrakk> \<Longrightarrow> I \<diamondsuit>\<^sub>r J \<noteq> {}
 3. \<lbrakk>ideal R I; ideal R J\<rbrakk> \<Longrightarrow> \<forall>x\<in>I \<diamondsuit>\<^sub>r J. \<forall>y\<in>I \<diamondsuit>\<^sub>r J. x \<plusminus> y \<in> I \<diamondsuit>\<^sub>r J
 4. \<lbrakk>ideal R I; ideal R J\<rbrakk> \<Longrightarrow> \<forall>r\<in>carrier R. \<forall>x\<in>I \<diamondsuit>\<^sub>r J. r \<cdot>\<^sub>r x \<in> I \<diamondsuit>\<^sub>r J
[PROOF STEP]
apply (frule_tac x = "carrier R" in spec,
        thin_tac "\<forall>xa. ideal R xa \<and> {x. \<exists>i\<in>I. \<exists>j\<in>J. x = i \<cdot>\<^sub>r j} \<subseteq> xa \<longrightarrow>
                                                                   x \<in> xa")
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<And>x. \<lbrakk>ideal R I; ideal R J; ideal R (carrier R); ideal R (carrier R) \<and> {x. \<exists>i\<in>I. \<exists>j\<in>J. x = i \<cdot>\<^sub>r j} \<subseteq> carrier R \<longrightarrow> x \<in> carrier R\<rbrakk> \<Longrightarrow> x \<in> carrier R
 2. \<lbrakk>ideal R I; ideal R J\<rbrakk> \<Longrightarrow> I \<diamondsuit>\<^sub>r J \<noteq> {}
 3. \<lbrakk>ideal R I; ideal R J\<rbrakk> \<Longrightarrow> \<forall>x\<in>I \<diamondsuit>\<^sub>r J. \<forall>y\<in>I \<diamondsuit>\<^sub>r J. x \<plusminus> y \<in> I \<diamondsuit>\<^sub>r J
 4. \<lbrakk>ideal R I; ideal R J\<rbrakk> \<Longrightarrow> \<forall>r\<in>carrier R. \<forall>x\<in>I \<diamondsuit>\<^sub>r J. r \<cdot>\<^sub>r x \<in> I \<diamondsuit>\<^sub>r J
[PROOF STEP]
apply (subgoal_tac "{x. \<exists>i\<in>I. \<exists>j\<in>J. x = i \<cdot>\<^sub>r j} \<subseteq> carrier R", simp)
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<And>x. \<lbrakk>ideal R I; ideal R J; ideal R (carrier R); ideal R (carrier R) \<and> {x. \<exists>i\<in>I. \<exists>j\<in>J. x = i \<cdot>\<^sub>r j} \<subseteq> carrier R \<longrightarrow> x \<in> carrier R\<rbrakk> \<Longrightarrow> {x. \<exists>i\<in>I. \<exists>j\<in>J. x = i \<cdot>\<^sub>r j} \<subseteq> carrier R
 2. \<lbrakk>ideal R I; ideal R J\<rbrakk> \<Longrightarrow> I \<diamondsuit>\<^sub>r J \<noteq> {}
 3. \<lbrakk>ideal R I; ideal R J\<rbrakk> \<Longrightarrow> \<forall>x\<in>I \<diamondsuit>\<^sub>r J. \<forall>y\<in>I \<diamondsuit>\<^sub>r J. x \<plusminus> y \<in> I \<diamondsuit>\<^sub>r J
 4. \<lbrakk>ideal R I; ideal R J\<rbrakk> \<Longrightarrow> \<forall>r\<in>carrier R. \<forall>x\<in>I \<diamondsuit>\<^sub>r J. r \<cdot>\<^sub>r x \<in> I \<diamondsuit>\<^sub>r J
[PROOF STEP]
apply (thin_tac "ideal R (carrier R) \<and>
            {x. \<exists>i\<in>I. \<exists>j\<in>J. x = i \<cdot>\<^sub>r j} \<subseteq> carrier R \<longrightarrow> x \<in> carrier R")
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<And>x. \<lbrakk>ideal R I; ideal R J; ideal R (carrier R)\<rbrakk> \<Longrightarrow> {x. \<exists>i\<in>I. \<exists>j\<in>J. x = i \<cdot>\<^sub>r j} \<subseteq> carrier R
 2. \<lbrakk>ideal R I; ideal R J\<rbrakk> \<Longrightarrow> I \<diamondsuit>\<^sub>r J \<noteq> {}
 3. \<lbrakk>ideal R I; ideal R J\<rbrakk> \<Longrightarrow> \<forall>x\<in>I \<diamondsuit>\<^sub>r J. \<forall>y\<in>I \<diamondsuit>\<^sub>r J. x \<plusminus> y \<in> I \<diamondsuit>\<^sub>r J
 4. \<lbrakk>ideal R I; ideal R J\<rbrakk> \<Longrightarrow> \<forall>r\<in>carrier R. \<forall>x\<in>I \<diamondsuit>\<^sub>r J. r \<cdot>\<^sub>r x \<in> I \<diamondsuit>\<^sub>r J
[PROOF STEP]
apply (rule subsetI, simp, (erule bexE)+, simp)
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<And>xa i j. \<lbrakk>ideal R I; ideal R J; ideal R (carrier R); i \<in> I; j \<in> J; xa = i \<cdot>\<^sub>r j\<rbrakk> \<Longrightarrow> i \<cdot>\<^sub>r j \<in> carrier R
 2. \<lbrakk>ideal R I; ideal R J\<rbrakk> \<Longrightarrow> I \<diamondsuit>\<^sub>r J \<noteq> {}
 3. \<lbrakk>ideal R I; ideal R J\<rbrakk> \<Longrightarrow> \<forall>x\<in>I \<diamondsuit>\<^sub>r J. \<forall>y\<in>I \<diamondsuit>\<^sub>r J. x \<plusminus> y \<in> I \<diamondsuit>\<^sub>r J
 4. \<lbrakk>ideal R I; ideal R J\<rbrakk> \<Longrightarrow> \<forall>r\<in>carrier R. \<forall>x\<in>I \<diamondsuit>\<^sub>r J. r \<cdot>\<^sub>r x \<in> I \<diamondsuit>\<^sub>r J
[PROOF STEP]
apply (frule_tac h = i in ideal_subset[of "I"], assumption+,
        frule_tac h = j in ideal_subset[of "J"], assumption+)
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<And>xa i j. \<lbrakk>ideal R I; ideal R J; ideal R (carrier R); i \<in> I; j \<in> J; xa = i \<cdot>\<^sub>r j; i \<in> carrier R; j \<in> carrier R\<rbrakk> \<Longrightarrow> i \<cdot>\<^sub>r j \<in> carrier R
 2. \<lbrakk>ideal R I; ideal R J\<rbrakk> \<Longrightarrow> I \<diamondsuit>\<^sub>r J \<noteq> {}
 3. \<lbrakk>ideal R I; ideal R J\<rbrakk> \<Longrightarrow> \<forall>x\<in>I \<diamondsuit>\<^sub>r J. \<forall>y\<in>I \<diamondsuit>\<^sub>r J. x \<plusminus> y \<in> I \<diamondsuit>\<^sub>r J
 4. \<lbrakk>ideal R I; ideal R J\<rbrakk> \<Longrightarrow> \<forall>r\<in>carrier R. \<forall>x\<in>I \<diamondsuit>\<^sub>r J. r \<cdot>\<^sub>r x \<in> I \<diamondsuit>\<^sub>r J
[PROOF STEP]
apply (rule_tac x = i and y = j in ring_tOp_closed, assumption+)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<lbrakk>ideal R I; ideal R J\<rbrakk> \<Longrightarrow> I \<diamondsuit>\<^sub>r J \<noteq> {}
 2. \<lbrakk>ideal R I; ideal R J\<rbrakk> \<Longrightarrow> \<forall>x\<in>I \<diamondsuit>\<^sub>r J. \<forall>y\<in>I \<diamondsuit>\<^sub>r J. x \<plusminus> y \<in> I \<diamondsuit>\<^sub>r J
 3. \<lbrakk>ideal R I; ideal R J\<rbrakk> \<Longrightarrow> \<forall>r\<in>carrier R. \<forall>x\<in>I \<diamondsuit>\<^sub>r J. r \<cdot>\<^sub>r x \<in> I \<diamondsuit>\<^sub>r J
[PROOF STEP]
apply (frule ideal_zero[of "I"],
        frule ideal_zero[of "J"],
        subgoal_tac "\<zero> \<in> I \<diamondsuit>\<^sub>r\<^bsub> R\<^esub> J", blast)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<lbrakk>ideal R I; ideal R J; \<zero> \<in> I; \<zero> \<in> J\<rbrakk> \<Longrightarrow> \<zero> \<in> I \<diamondsuit>\<^sub>r J
 2. \<lbrakk>ideal R I; ideal R J\<rbrakk> \<Longrightarrow> \<forall>x\<in>I \<diamondsuit>\<^sub>r J. \<forall>y\<in>I \<diamondsuit>\<^sub>r J. x \<plusminus> y \<in> I \<diamondsuit>\<^sub>r J
 3. \<lbrakk>ideal R I; ideal R J\<rbrakk> \<Longrightarrow> \<forall>r\<in>carrier R. \<forall>x\<in>I \<diamondsuit>\<^sub>r J. r \<cdot>\<^sub>r x \<in> I \<diamondsuit>\<^sub>r J
[PROOF STEP]
apply (simp add:ideal_prod_def)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<lbrakk>ideal R I; ideal R J; \<zero> \<in> I; \<zero> \<in> J\<rbrakk> \<Longrightarrow> \<forall>x. ideal R x \<and> {x. \<exists>i\<in>I. \<exists>j\<in>J. x = i \<cdot>\<^sub>r j} \<subseteq> x \<longrightarrow> \<zero> \<in> x
 2. \<lbrakk>ideal R I; ideal R J\<rbrakk> \<Longrightarrow> \<forall>x\<in>I \<diamondsuit>\<^sub>r J. \<forall>y\<in>I \<diamondsuit>\<^sub>r J. x \<plusminus> y \<in> I \<diamondsuit>\<^sub>r J
 3. \<lbrakk>ideal R I; ideal R J\<rbrakk> \<Longrightarrow> \<forall>r\<in>carrier R. \<forall>x\<in>I \<diamondsuit>\<^sub>r J. r \<cdot>\<^sub>r x \<in> I \<diamondsuit>\<^sub>r J
[PROOF STEP]
apply (rule allI, rule impI, erule conjE)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>x. \<lbrakk>ideal R I; ideal R J; \<zero> \<in> I; \<zero> \<in> J; ideal R x; {x. \<exists>i\<in>I. \<exists>j\<in>J. x = i \<cdot>\<^sub>r j} \<subseteq> x\<rbrakk> \<Longrightarrow> \<zero> \<in> x
 2. \<lbrakk>ideal R I; ideal R J\<rbrakk> \<Longrightarrow> \<forall>x\<in>I \<diamondsuit>\<^sub>r J. \<forall>y\<in>I \<diamondsuit>\<^sub>r J. x \<plusminus> y \<in> I \<diamondsuit>\<^sub>r J
 3. \<lbrakk>ideal R I; ideal R J\<rbrakk> \<Longrightarrow> \<forall>r\<in>carrier R. \<forall>x\<in>I \<diamondsuit>\<^sub>r J. r \<cdot>\<^sub>r x \<in> I \<diamondsuit>\<^sub>r J
[PROOF STEP]
apply (rule ideal_zero, assumption)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>ideal R I; ideal R J\<rbrakk> \<Longrightarrow> \<forall>x\<in>I \<diamondsuit>\<^sub>r J. \<forall>y\<in>I \<diamondsuit>\<^sub>r J. x \<plusminus> y \<in> I \<diamondsuit>\<^sub>r J
 2. \<lbrakk>ideal R I; ideal R J\<rbrakk> \<Longrightarrow> \<forall>r\<in>carrier R. \<forall>x\<in>I \<diamondsuit>\<^sub>r J. r \<cdot>\<^sub>r x \<in> I \<diamondsuit>\<^sub>r J
[PROOF STEP]
apply (rule ballI)+
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x y. \<lbrakk>ideal R I; ideal R J; x \<in> I \<diamondsuit>\<^sub>r J; y \<in> I \<diamondsuit>\<^sub>r J\<rbrakk> \<Longrightarrow> x \<plusminus> y \<in> I \<diamondsuit>\<^sub>r J
 2. \<lbrakk>ideal R I; ideal R J\<rbrakk> \<Longrightarrow> \<forall>r\<in>carrier R. \<forall>x\<in>I \<diamondsuit>\<^sub>r J. r \<cdot>\<^sub>r x \<in> I \<diamondsuit>\<^sub>r J
[PROOF STEP]
apply (simp add:ideal_prod_def)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x y. \<lbrakk>ideal R I; ideal R J; \<forall>xa. ideal R xa \<and> {x. \<exists>i\<in>I. \<exists>j\<in>J. x = i \<cdot>\<^sub>r j} \<subseteq> xa \<longrightarrow> x \<in> xa; \<forall>x. ideal R x \<and> {x. \<exists>i\<in>I. \<exists>j\<in>J. x = i \<cdot>\<^sub>r j} \<subseteq> x \<longrightarrow> y \<in> x\<rbrakk> \<Longrightarrow> \<forall>xa. ideal R xa \<and> {x. \<exists>i\<in>I. \<exists>j\<in>J. x = i \<cdot>\<^sub>r j} \<subseteq> xa \<longrightarrow> x \<plusminus> y \<in> xa
 2. \<lbrakk>ideal R I; ideal R J\<rbrakk> \<Longrightarrow> \<forall>r\<in>carrier R. \<forall>x\<in>I \<diamondsuit>\<^sub>r J. r \<cdot>\<^sub>r x \<in> I \<diamondsuit>\<^sub>r J
[PROOF STEP]
apply (rule allI, rule impI)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x y xa. \<lbrakk>ideal R I; ideal R J; \<forall>xa. ideal R xa \<and> {x. \<exists>i\<in>I. \<exists>j\<in>J. x = i \<cdot>\<^sub>r j} \<subseteq> xa \<longrightarrow> x \<in> xa; \<forall>x. ideal R x \<and> {x. \<exists>i\<in>I. \<exists>j\<in>J. x = i \<cdot>\<^sub>r j} \<subseteq> x \<longrightarrow> y \<in> x; ideal R xa \<and> {x. \<exists>i\<in>I. \<exists>j\<in>J. x = i \<cdot>\<^sub>r j} \<subseteq> xa\<rbrakk> \<Longrightarrow> x \<plusminus> y \<in> xa
 2. \<lbrakk>ideal R I; ideal R J\<rbrakk> \<Longrightarrow> \<forall>r\<in>carrier R. \<forall>x\<in>I \<diamondsuit>\<^sub>r J. r \<cdot>\<^sub>r x \<in> I \<diamondsuit>\<^sub>r J
[PROOF STEP]
apply (frule_tac x = xa in spec,
        thin_tac "\<forall>xa. ideal R xa \<and> {x. \<exists>i\<in>I. \<exists>j\<in>J. x = i \<cdot>\<^sub>r j} \<subseteq> xa
                                            \<longrightarrow> x \<in> xa",
        frule_tac x = xa in spec,
        thin_tac "\<forall>x. ideal R x \<and> {x. \<exists>i\<in>I. \<exists>j\<in>J. x = i \<cdot>\<^sub>r j} \<subseteq> x \<longrightarrow> y \<in> x",
        erule conjE, simp,
        rule_tac x = x and y = y in ideal_pOp_closed, assumption+)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ideal R I; ideal R J\<rbrakk> \<Longrightarrow> \<forall>r\<in>carrier R. \<forall>x\<in>I \<diamondsuit>\<^sub>r J. r \<cdot>\<^sub>r x \<in> I \<diamondsuit>\<^sub>r J
[PROOF STEP]
apply (rule ballI)+
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>r x. \<lbrakk>ideal R I; ideal R J; r \<in> carrier R; x \<in> I \<diamondsuit>\<^sub>r J\<rbrakk> \<Longrightarrow> r \<cdot>\<^sub>r x \<in> I \<diamondsuit>\<^sub>r J
[PROOF STEP]
apply (simp add:ideal_prod_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>r x. \<lbrakk>ideal R I; ideal R J; r \<in> carrier R; \<forall>xa. ideal R xa \<and> {x. \<exists>i\<in>I. \<exists>j\<in>J. x = i \<cdot>\<^sub>r j} \<subseteq> xa \<longrightarrow> x \<in> xa\<rbrakk> \<Longrightarrow> \<forall>xa. ideal R xa \<and> {x. \<exists>i\<in>I. \<exists>j\<in>J. x = i \<cdot>\<^sub>r j} \<subseteq> xa \<longrightarrow> r \<cdot>\<^sub>r x \<in> xa
[PROOF STEP]
apply (rule allI, rule impI, erule conjE)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>r x xa. \<lbrakk>ideal R I; ideal R J; r \<in> carrier R; \<forall>xa. ideal R xa \<and> {x. \<exists>i\<in>I. \<exists>j\<in>J. x = i \<cdot>\<^sub>r j} \<subseteq> xa \<longrightarrow> x \<in> xa; ideal R xa; {x. \<exists>i\<in>I. \<exists>j\<in>J. x = i \<cdot>\<^sub>r j} \<subseteq> xa\<rbrakk> \<Longrightarrow> r \<cdot>\<^sub>r x \<in> xa
[PROOF STEP]
apply (frule_tac x = xa in spec,
               thin_tac "\<forall>xa. ideal R xa \<and> {x. \<exists>i\<in>I. \<exists>j\<in>J. x = i \<cdot>\<^sub>r j}
                            \<subseteq> xa \<longrightarrow> x \<in> xa", simp)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>r x xa. \<lbrakk>ideal R I; ideal R J; r \<in> carrier R; ideal R xa; {x. \<exists>i\<in>I. \<exists>j\<in>J. x = i \<cdot>\<^sub>r j} \<subseteq> xa; x \<in> xa\<rbrakk> \<Longrightarrow> r \<cdot>\<^sub>r x \<in> xa
[PROOF STEP]
apply (simp add:ideal_ring_multiple)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma (in Ring) ideal_prod_commute:"\<lbrakk>ideal R I; ideal R J\<rbrakk> \<Longrightarrow>
                                              I \<diamondsuit>\<^sub>r J = J \<diamondsuit>\<^sub>r I"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ideal R I; ideal R J\<rbrakk> \<Longrightarrow> I \<diamondsuit>\<^sub>r J = J \<diamondsuit>\<^sub>r I
[PROOF STEP]
apply (simp add:ideal_prod_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ideal R I; ideal R J\<rbrakk> \<Longrightarrow> \<Inter> {L. ideal R L \<and> {x. \<exists>i\<in>I. \<exists>j\<in>J. x = i \<cdot>\<^sub>r j} \<subseteq> L} = \<Inter> {L. ideal R L \<and> {x. \<exists>i\<in>J. \<exists>j\<in>I. x = i \<cdot>\<^sub>r j} \<subseteq> L}
[PROOF STEP]
apply (subgoal_tac "{K. ideal R K \<and> {x. \<exists>i\<in>I. \<exists>j\<in>J. x = i \<cdot>\<^sub>r j}
       \<subseteq> K}  = {K. ideal R K \<and> {x. \<exists>i\<in>J. \<exists>j\<in>I. x = i \<cdot>\<^sub>r j} \<subseteq> K}")
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>ideal R I; ideal R J; {K. ideal R K \<and> {x. \<exists>i\<in>I. \<exists>j\<in>J. x = i \<cdot>\<^sub>r j} \<subseteq> K} = {K. ideal R K \<and> {x. \<exists>i\<in>J. \<exists>j\<in>I. x = i \<cdot>\<^sub>r j} \<subseteq> K}\<rbrakk> \<Longrightarrow> \<Inter> {L. ideal R L \<and> {x. \<exists>i\<in>I. \<exists>j\<in>J. x = i \<cdot>\<^sub>r j} \<subseteq> L} = \<Inter> {L. ideal R L \<and> {x. \<exists>i\<in>J. \<exists>j\<in>I. x = i \<cdot>\<^sub>r j} \<subseteq> L}
 2. \<lbrakk>ideal R I; ideal R J\<rbrakk> \<Longrightarrow> {K. ideal R K \<and> {x. \<exists>i\<in>I. \<exists>j\<in>J. x = i \<cdot>\<^sub>r j} \<subseteq> K} = {K. ideal R K \<and> {x. \<exists>i\<in>J. \<exists>j\<in>I. x = i \<cdot>\<^sub>r j} \<subseteq> K}
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ideal R I; ideal R J\<rbrakk> \<Longrightarrow> {K. ideal R K \<and> {x. \<exists>i\<in>I. \<exists>j\<in>J. x = i \<cdot>\<^sub>r j} \<subseteq> K} = {K. ideal R K \<and> {x. \<exists>i\<in>J. \<exists>j\<in>I. x = i \<cdot>\<^sub>r j} \<subseteq> K}
[PROOF STEP]
apply (rule equalityI)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>ideal R I; ideal R J\<rbrakk> \<Longrightarrow> {K. ideal R K \<and> {x. \<exists>i\<in>I. \<exists>j\<in>J. x = i \<cdot>\<^sub>r j} \<subseteq> K} \<subseteq> {K. ideal R K \<and> {x. \<exists>i\<in>J. \<exists>j\<in>I. x = i \<cdot>\<^sub>r j} \<subseteq> K}
 2. \<lbrakk>ideal R I; ideal R J\<rbrakk> \<Longrightarrow> {K. ideal R K \<and> {x. \<exists>i\<in>J. \<exists>j\<in>I. x = i \<cdot>\<^sub>r j} \<subseteq> K} \<subseteq> {K. ideal R K \<and> {x. \<exists>i\<in>I. \<exists>j\<in>J. x = i \<cdot>\<^sub>r j} \<subseteq> K}
[PROOF STEP]
apply (rule subsetI, rename_tac X, simp, erule conjE)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>X. \<lbrakk>ideal R I; ideal R J; ideal R X; {x. \<exists>i\<in>I. \<exists>j\<in>J. x = i \<cdot>\<^sub>r j} \<subseteq> X\<rbrakk> \<Longrightarrow> {x. \<exists>i\<in>J. \<exists>j\<in>I. x = i \<cdot>\<^sub>r j} \<subseteq> X
 2. \<lbrakk>ideal R I; ideal R J\<rbrakk> \<Longrightarrow> {K. ideal R K \<and> {x. \<exists>i\<in>J. \<exists>j\<in>I. x = i \<cdot>\<^sub>r j} \<subseteq> K} \<subseteq> {K. ideal R K \<and> {x. \<exists>i\<in>I. \<exists>j\<in>J. x = i \<cdot>\<^sub>r j} \<subseteq> K}
[PROOF STEP]
apply (rule subsetI, simp)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>X x. \<lbrakk>ideal R I; ideal R J; ideal R X; {x. \<exists>i\<in>I. \<exists>j\<in>J. x = i \<cdot>\<^sub>r j} \<subseteq> X; \<exists>i\<in>J. \<exists>j\<in>I. x = i \<cdot>\<^sub>r j\<rbrakk> \<Longrightarrow> x \<in> X
 2. \<lbrakk>ideal R I; ideal R J\<rbrakk> \<Longrightarrow> {K. ideal R K \<and> {x. \<exists>i\<in>J. \<exists>j\<in>I. x = i \<cdot>\<^sub>r j} \<subseteq> K} \<subseteq> {K. ideal R K \<and> {x. \<exists>i\<in>I. \<exists>j\<in>J. x = i \<cdot>\<^sub>r j} \<subseteq> K}
[PROOF STEP]
apply ((erule bexE)+)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>X x i j. \<lbrakk>ideal R I; ideal R J; ideal R X; {x. \<exists>i\<in>I. \<exists>j\<in>J. x = i \<cdot>\<^sub>r j} \<subseteq> X; i \<in> J; j \<in> I; x = i \<cdot>\<^sub>r j\<rbrakk> \<Longrightarrow> x \<in> X
 2. \<lbrakk>ideal R I; ideal R J\<rbrakk> \<Longrightarrow> {K. ideal R K \<and> {x. \<exists>i\<in>J. \<exists>j\<in>I. x = i \<cdot>\<^sub>r j} \<subseteq> K} \<subseteq> {K. ideal R K \<and> {x. \<exists>i\<in>I. \<exists>j\<in>J. x = i \<cdot>\<^sub>r j} \<subseteq> K}
[PROOF STEP]
apply (subgoal_tac "x \<in> {x. \<exists>i\<in>I. \<exists>j\<in>J. x = i \<cdot>\<^sub>r j}",
        rule_tac c = x and A = "{x. \<exists>i\<in>I. \<exists>j\<in>J. x = i \<cdot>\<^sub>r j}" and B = X in
        subsetD, assumption+,
        frule_tac h = i in ideal_subset[of "J"], assumption,
        frule_tac h = j in ideal_subset[of "I"], assumption,
        frule_tac x = i and y = j in ring_tOp_commute, assumption+, simp,
        blast)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ideal R I; ideal R J\<rbrakk> \<Longrightarrow> {K. ideal R K \<and> {x. \<exists>i\<in>J. \<exists>j\<in>I. x = i \<cdot>\<^sub>r j} \<subseteq> K} \<subseteq> {K. ideal R K \<and> {x. \<exists>i\<in>I. \<exists>j\<in>J. x = i \<cdot>\<^sub>r j} \<subseteq> K}
[PROOF STEP]
apply (rule subsetI, simp, erule conjE,
        rule subsetI, simp,
        (erule bexE)+,
        subgoal_tac "xa \<in> {x. \<exists>i\<in>J. \<exists>j\<in>I. x = i \<cdot>\<^sub>r j}",
        rule_tac c = xa and A = "{x. \<exists>i\<in>J. \<exists>j\<in>I. x = i \<cdot>\<^sub>r j}" and B = x in
                 subsetD, assumption+,
        frule_tac h = i in ideal_subset[of "I"], assumption,
        frule_tac h = j in ideal_subset[of "J"], assumption,
        frule_tac x = i and y = j in ring_tOp_commute, assumption+, simp,
        blast)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma (in Ring) ideal_prod_subTr:"\<lbrakk>ideal R I; ideal R J; ideal R C;
                        \<forall>i\<in>I. \<forall>j\<in>J. i \<cdot>\<^sub>r j \<in> C\<rbrakk> \<Longrightarrow> I \<diamondsuit>\<^sub>r J \<subseteq> C"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ideal R I; ideal R J; ideal R C; \<forall>i\<in>I. \<forall>j\<in>J. i \<cdot>\<^sub>r j \<in> C\<rbrakk> \<Longrightarrow> I \<diamondsuit>\<^sub>r J \<subseteq> C
[PROOF STEP]
apply (simp add:ideal_prod_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ideal R I; ideal R J; ideal R C; \<forall>i\<in>I. \<forall>j\<in>J. i \<cdot>\<^sub>r j \<in> C\<rbrakk> \<Longrightarrow> \<Inter> {L. ideal R L \<and> {x. \<exists>i\<in>I. \<exists>j\<in>J. x = i \<cdot>\<^sub>r j} \<subseteq> L} \<subseteq> C
[PROOF STEP]
apply (rule_tac B = C and
        A = "{L. ideal R L \<and> {x. \<exists>i\<in>I. \<exists>j\<in>J. x = i \<cdot>\<^sub>r j} \<subseteq> L}" in
        Inter_lower)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ideal R I; ideal R J; ideal R C; \<forall>i\<in>I. \<forall>j\<in>J. i \<cdot>\<^sub>r j \<in> C\<rbrakk> \<Longrightarrow> C \<in> {L. ideal R L \<and> {x. \<exists>i\<in>I. \<exists>j\<in>J. x = i \<cdot>\<^sub>r j} \<subseteq> L}
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ideal R I; ideal R J; ideal R C; \<forall>i\<in>I. \<forall>j\<in>J. i \<cdot>\<^sub>r j \<in> C\<rbrakk> \<Longrightarrow> {x. \<exists>i\<in>I. \<exists>j\<in>J. x = i \<cdot>\<^sub>r j} \<subseteq> C
[PROOF STEP]
apply (rule subsetI, simp, (erule bexE)+, simp)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma (in Ring) n_prod_idealTr:
     "(\<forall>k \<le> n. ideal R (J k)) \<longrightarrow> ideal R (ideal_n_prod R n J)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<forall>k\<le>n. ideal R (J k)) \<longrightarrow> ideal R (i\<Pi>\<^bsub>R,n\<^esub> J)
[PROOF STEP]
apply (induct_tac n)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. (\<forall>k\<le>0. ideal R (J k)) \<longrightarrow> ideal R (i\<Pi>\<^bsub>R,0\<^esub> J)
 2. \<And>n. (\<forall>k\<le>n. ideal R (J k)) \<longrightarrow> ideal R (i\<Pi>\<^bsub>R,n\<^esub> J) \<Longrightarrow> (\<forall>k\<le>Suc n. ideal R (J k)) \<longrightarrow> ideal R (i\<Pi>\<^bsub>R,Suc n\<^esub> J)
[PROOF STEP]
apply (rule impI)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<forall>k\<le>0. ideal R (J k) \<Longrightarrow> ideal R (i\<Pi>\<^bsub>R,0\<^esub> J)
 2. \<And>n. (\<forall>k\<le>n. ideal R (J k)) \<longrightarrow> ideal R (i\<Pi>\<^bsub>R,n\<^esub> J) \<Longrightarrow> (\<forall>k\<le>Suc n. ideal R (J k)) \<longrightarrow> ideal R (i\<Pi>\<^bsub>R,Suc n\<^esub> J)
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>n. (\<forall>k\<le>n. ideal R (J k)) \<longrightarrow> ideal R (i\<Pi>\<^bsub>R,n\<^esub> J) \<Longrightarrow> (\<forall>k\<le>Suc n. ideal R (J k)) \<longrightarrow> ideal R (i\<Pi>\<^bsub>R,Suc n\<^esub> J)
[PROOF STEP]
apply (rule impI)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>n. \<lbrakk>(\<forall>k\<le>n. ideal R (J k)) \<longrightarrow> ideal R (i\<Pi>\<^bsub>R,n\<^esub> J); \<forall>k\<le>Suc n. ideal R (J k)\<rbrakk> \<Longrightarrow> ideal R (i\<Pi>\<^bsub>R,Suc n\<^esub> J)
[PROOF STEP]
apply (simp only:ideal_n_prodSn)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>n. \<lbrakk>(\<forall>k\<le>n. ideal R (J k)) \<longrightarrow> ideal R (i\<Pi>\<^bsub>R,n\<^esub> J); \<forall>k\<le>Suc n. ideal R (J k)\<rbrakk> \<Longrightarrow> ideal R (i\<Pi>\<^bsub>R,n\<^esub> J \<diamondsuit>\<^sub>r J (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>ideal R (i\<Pi>\<^bsub>R,n\<^esub> J); \<forall>k\<le>Suc n. ideal R (J k)\<rbrakk> \<Longrightarrow> ideal R (i\<Pi>\<^bsub>R,n\<^esub> J \<diamondsuit>\<^sub>r J (Suc n))
[PROOF STEP]
apply (rule ideal_prod_ideal, assumption)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>n. \<lbrakk>ideal R (i\<Pi>\<^bsub>R,n\<^esub> J); \<forall>k\<le>Suc n. ideal R (J k)\<rbrakk> \<Longrightarrow> ideal R (J (Suc n))
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma (in Ring) n_prod_ideal:"\<lbrakk>\<forall>k \<le> n. ideal R (J k)\<rbrakk>
                               \<Longrightarrow>  ideal R (ideal_n_prod R n J)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>k\<le>n. ideal R (J k) \<Longrightarrow> ideal R (i\<Pi>\<^bsub>R,n\<^esub> J)
[PROOF STEP]
apply (simp add:n_prod_idealTr)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma (in Ring) ideal_prod_el1:"\<lbrakk>ideal R I; ideal R J; a \<in> (I \<diamondsuit>\<^sub>r J)\<rbrakk> \<Longrightarrow>
                           a \<in> I"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ideal R I; ideal R J; a \<in> I \<diamondsuit>\<^sub>r J\<rbrakk> \<Longrightarrow> a \<in> I
[PROOF STEP]
apply (frule ideal_prod_la1 [of "I" "J"], assumption+)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ideal R I; ideal R J; a \<in> I \<diamondsuit>\<^sub>r J; I \<diamondsuit>\<^sub>r J \<subseteq> I\<rbrakk> \<Longrightarrow> a \<in> I
[PROOF STEP]
apply (rule subsetD, assumption+)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma (in Ring) ideal_prod_la2:"\<lbrakk>ideal R I; ideal R J \<rbrakk> \<Longrightarrow> (I \<diamondsuit>\<^sub>r J) \<subseteq> J"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ideal R I; ideal R J\<rbrakk> \<Longrightarrow> I \<diamondsuit>\<^sub>r J \<subseteq> J
[PROOF STEP]
apply (subst ideal_prod_commute, assumption+,
        rule ideal_prod_la1[of "J" "I"], assumption+)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma (in Ring) ideal_prod_sub_Int:"\<lbrakk>ideal R I; ideal R J \<rbrakk> \<Longrightarrow>
                     (I \<diamondsuit>\<^sub>r J) \<subseteq> I \<inter> J"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ideal R I; ideal R J\<rbrakk> \<Longrightarrow> I \<diamondsuit>\<^sub>r J \<subseteq> I \<inter> J
[PROOF STEP]
by (simp add:ideal_prod_la1 ideal_prod_la2)


[STATEMENT]
lemma (in Ring) ideal_prod_el2:"\<lbrakk>ideal R I; ideal R J; a \<in> (I \<diamondsuit>\<^sub>r J)\<rbrakk> \<Longrightarrow>
                                 a \<in> J"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ideal R I; ideal R J; a \<in> I \<diamondsuit>\<^sub>r J\<rbrakk> \<Longrightarrow> a \<in> J
[PROOF STEP]
by (frule ideal_prod_la2 [of "I" "J"], assumption+,
       rule subsetD, assumption+)


[STATEMENT]
lemma (in Ring) ele_n_prodTr0:"\<lbrakk>\<forall>k \<le> (Suc n). ideal R (J k);
             a \<in> i\<Pi>\<^bsub>R,(Suc n)\<^esub> J \<rbrakk> \<Longrightarrow> a \<in> (i\<Pi>\<^bsub>R,n\<^esub> J) \<and> a \<in> (J (Suc n))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<forall>k\<le>Suc n. ideal R (J k); a \<in> i\<Pi>\<^bsub>R,Suc n\<^esub> J\<rbrakk> \<Longrightarrow> a \<in> i\<Pi>\<^bsub>R,n\<^esub> J \<and> a \<in> J (Suc n)
[PROOF STEP]
apply (simp add:Nset_Suc[of n])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<forall>k\<le>Suc n. ideal R (J k); a \<in> i\<Pi>\<^bsub>R,n\<^esub> J \<diamondsuit>\<^sub>r J (Suc n)\<rbrakk> \<Longrightarrow> a \<in> i\<Pi>\<^bsub>R,n\<^esub> J \<and> a \<in> J (Suc n)
[PROOF STEP]
apply (cut_tac n_prod_ideal[of n J])
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>\<forall>k\<le>Suc n. ideal R (J k); a \<in> i\<Pi>\<^bsub>R,n\<^esub> J \<diamondsuit>\<^sub>r J (Suc n); ideal R (i\<Pi>\<^bsub>R,n\<^esub> J)\<rbrakk> \<Longrightarrow> a \<in> i\<Pi>\<^bsub>R,n\<^esub> J \<and> a \<in> J (Suc n)
 2. \<lbrakk>\<forall>k\<le>Suc n. ideal R (J k); a \<in> i\<Pi>\<^bsub>R,n\<^esub> J \<diamondsuit>\<^sub>r J (Suc n)\<rbrakk> \<Longrightarrow> \<forall>k\<le>n. ideal R (J k)
[PROOF STEP]
apply (rule conjI)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<lbrakk>\<forall>k\<le>Suc n. ideal R (J k); a \<in> i\<Pi>\<^bsub>R,n\<^esub> J \<diamondsuit>\<^sub>r J (Suc n); ideal R (i\<Pi>\<^bsub>R,n\<^esub> J)\<rbrakk> \<Longrightarrow> a \<in> i\<Pi>\<^bsub>R,n\<^esub> J
 2. \<lbrakk>\<forall>k\<le>Suc n. ideal R (J k); a \<in> i\<Pi>\<^bsub>R,n\<^esub> J \<diamondsuit>\<^sub>r J (Suc n); ideal R (i\<Pi>\<^bsub>R,n\<^esub> J)\<rbrakk> \<Longrightarrow> a \<in> J (Suc n)
 3. \<lbrakk>\<forall>k\<le>Suc n. ideal R (J k); a \<in> i\<Pi>\<^bsub>R,n\<^esub> J \<diamondsuit>\<^sub>r J (Suc n)\<rbrakk> \<Longrightarrow> \<forall>k\<le>n. ideal R (J k)
[PROOF STEP]
apply (rule ideal_prod_el1 [of "i\<Pi>\<^bsub>R,n\<^esub> J" "J (Suc n)"], assumption, simp+)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>\<forall>k\<le>Suc n. ideal R (J k); a \<in> i\<Pi>\<^bsub>R,n\<^esub> J \<diamondsuit>\<^sub>r J (Suc n); ideal R (i\<Pi>\<^bsub>R,n\<^esub> J)\<rbrakk> \<Longrightarrow> a \<in> J (Suc n)
 2. \<lbrakk>\<forall>k\<le>Suc n. ideal R (J k); a \<in> i\<Pi>\<^bsub>R,n\<^esub> J \<diamondsuit>\<^sub>r J (Suc n)\<rbrakk> \<Longrightarrow> \<forall>k\<le>n. ideal R (J k)
[PROOF STEP]
apply (rule ideal_prod_el2[of "i\<Pi>\<^bsub>R,n\<^esub> J" "J (Suc n)"], assumption+, simp+)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma (in Ring) ele_n_prodTr1:
      "(\<forall>k \<le> n. ideal R (J k)) \<and> a \<in> ideal_n_prod R n J \<longrightarrow>
                                             (\<forall>k \<le> n. a \<in> (J k))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<forall>k\<le>n. ideal R (J k)) \<and> a \<in> i\<Pi>\<^bsub>R,n\<^esub> J \<longrightarrow> (\<forall>k\<le>n. a \<in> J k)
[PROOF STEP]
apply (induct_tac n)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. (\<forall>k\<le>0. ideal R (J k)) \<and> a \<in> i\<Pi>\<^bsub>R,0\<^esub> J \<longrightarrow> (\<forall>k\<le>0. a \<in> J k)
 2. \<And>n. (\<forall>k\<le>n. ideal R (J k)) \<and> a \<in> i\<Pi>\<^bsub>R,n\<^esub> J \<longrightarrow> (\<forall>k\<le>n. a \<in> J k) \<Longrightarrow> (\<forall>k\<le>Suc n. ideal R (J k)) \<and> a \<in> i\<Pi>\<^bsub>R,Suc n\<^esub> J \<longrightarrow> (\<forall>k\<le>Suc n. a \<in> J k)
[PROOF STEP]
(** n = 0 **)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. (\<forall>k\<le>0. ideal R (J k)) \<and> a \<in> i\<Pi>\<^bsub>R,0\<^esub> J \<longrightarrow> (\<forall>k\<le>0. a \<in> J k)
 2. \<And>n. (\<forall>k\<le>n. ideal R (J k)) \<and> a \<in> i\<Pi>\<^bsub>R,n\<^esub> J \<longrightarrow> (\<forall>k\<le>n. a \<in> J k) \<Longrightarrow> (\<forall>k\<le>Suc n. ideal R (J k)) \<and> a \<in> i\<Pi>\<^bsub>R,Suc n\<^esub> J \<longrightarrow> (\<forall>k\<le>Suc n. a \<in> J k)
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>n. (\<forall>k\<le>n. ideal R (J k)) \<and> a \<in> i\<Pi>\<^bsub>R,n\<^esub> J \<longrightarrow> (\<forall>k\<le>n. a \<in> J k) \<Longrightarrow> (\<forall>k\<le>Suc n. ideal R (J k)) \<and> a \<in> i\<Pi>\<^bsub>R,Suc n\<^esub> J \<longrightarrow> (\<forall>k\<le>Suc n. a \<in> J k)
[PROOF STEP]
(** n **)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>n. (\<forall>k\<le>n. ideal R (J k)) \<and> a \<in> i\<Pi>\<^bsub>R,n\<^esub> J \<longrightarrow> (\<forall>k\<le>n. a \<in> J k) \<Longrightarrow> (\<forall>k\<le>Suc n. ideal R (J k)) \<and> a \<in> i\<Pi>\<^bsub>R,Suc n\<^esub> J \<longrightarrow> (\<forall>k\<le>Suc n. a \<in> J k)
[PROOF STEP]
apply (rule impI)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>n. \<lbrakk>(\<forall>k\<le>n. ideal R (J k)) \<and> a \<in> i\<Pi>\<^bsub>R,n\<^esub> J \<longrightarrow> (\<forall>k\<le>n. a \<in> J k); (\<forall>k\<le>Suc n. ideal R (J k)) \<and> a \<in> i\<Pi>\<^bsub>R,Suc n\<^esub> J\<rbrakk> \<Longrightarrow> \<forall>k\<le>Suc n. a \<in> J k
[PROOF STEP]
apply (rule allI, rule impI)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>n k. \<lbrakk>(\<forall>k\<le>n. ideal R (J k)) \<and> a \<in> i\<Pi>\<^bsub>R,n\<^esub> J \<longrightarrow> (\<forall>k\<le>n. a \<in> J k); (\<forall>k\<le>Suc n. ideal R (J k)) \<and> a \<in> i\<Pi>\<^bsub>R,Suc n\<^esub> J; k \<le> Suc n\<rbrakk> \<Longrightarrow> a \<in> J k
[PROOF STEP]
apply (cut_tac n = n in Nsetn_sub_mem1, simp)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>n k. \<lbrakk>a \<in> i\<Pi>\<^bsub>R,n\<^esub> J \<longrightarrow> (\<forall>k\<le>n. a \<in> J k); (\<forall>k\<le>Suc n. ideal R (J k)) \<and> a \<in> i\<Pi>\<^bsub>R,n\<^esub> J \<diamondsuit>\<^sub>r J (Suc n); k \<le> Suc n\<rbrakk> \<Longrightarrow> a \<in> J k
[PROOF STEP]
apply (erule conjE)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>n k. \<lbrakk>a \<in> i\<Pi>\<^bsub>R,n\<^esub> J \<longrightarrow> (\<forall>k\<le>n. a \<in> J k); k \<le> Suc n; \<forall>k\<le>Suc n. ideal R (J k); a \<in> i\<Pi>\<^bsub>R,n\<^esub> J \<diamondsuit>\<^sub>r J (Suc n)\<rbrakk> \<Longrightarrow> a \<in> J k
[PROOF STEP]
apply (frule_tac n = n in ele_n_prodTr0[of _ J a])
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>n k. \<lbrakk>a \<in> i\<Pi>\<^bsub>R,n\<^esub> J \<longrightarrow> (\<forall>k\<le>n. a \<in> J k); k \<le> Suc n; \<forall>k\<le>Suc n. ideal R (J k); a \<in> i\<Pi>\<^bsub>R,n\<^esub> J \<diamondsuit>\<^sub>r J (Suc n)\<rbrakk> \<Longrightarrow> a \<in> i\<Pi>\<^bsub>R,Suc n\<^esub> J
 2. \<And>n k. \<lbrakk>a \<in> i\<Pi>\<^bsub>R,n\<^esub> J \<longrightarrow> (\<forall>k\<le>n. a \<in> J k); k \<le> Suc n; \<forall>k\<le>Suc n. ideal R (J k); a \<in> i\<Pi>\<^bsub>R,n\<^esub> J \<diamondsuit>\<^sub>r J (Suc n); a \<in> i\<Pi>\<^bsub>R,n\<^esub> J \<and> a \<in> J (Suc n)\<rbrakk> \<Longrightarrow> a \<in> J k
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>n k. \<lbrakk>a \<in> i\<Pi>\<^bsub>R,n\<^esub> J \<longrightarrow> (\<forall>k\<le>n. a \<in> J k); k \<le> Suc n; \<forall>k\<le>Suc n. ideal R (J k); a \<in> i\<Pi>\<^bsub>R,n\<^esub> J \<diamondsuit>\<^sub>r J (Suc n); a \<in> i\<Pi>\<^bsub>R,n\<^esub> J \<and> a \<in> J (Suc n)\<rbrakk> \<Longrightarrow> a \<in> J k
[PROOF STEP]
apply (erule conjE,
        thin_tac "\<forall>k\<le>Suc n. ideal R (J k)")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>n k. \<lbrakk>a \<in> i\<Pi>\<^bsub>R,n\<^esub> J \<longrightarrow> (\<forall>k\<le>n. a \<in> J k); k \<le> Suc n; a \<in> i\<Pi>\<^bsub>R,n\<^esub> J \<diamondsuit>\<^sub>r J (Suc n); a \<in> i\<Pi>\<^bsub>R,n\<^esub> J; a \<in> J (Suc n)\<rbrakk> \<Longrightarrow> a \<in> J k
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>n k. \<lbrakk>\<forall>k\<le>n. a \<in> J k; k \<le> Suc n; a \<in> i\<Pi>\<^bsub>R,n\<^esub> J \<diamondsuit>\<^sub>r J (Suc n); a \<in> i\<Pi>\<^bsub>R,n\<^esub> J; a \<in> J (Suc n)\<rbrakk> \<Longrightarrow> a \<in> J k
[PROOF STEP]
apply (case_tac "k = Suc n", simp)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>n k. \<lbrakk>\<forall>k\<le>n. a \<in> J k; k \<le> Suc n; a \<in> i\<Pi>\<^bsub>R,n\<^esub> J \<diamondsuit>\<^sub>r J (Suc n); a \<in> i\<Pi>\<^bsub>R,n\<^esub> J; a \<in> J (Suc n); k \<noteq> Suc n\<rbrakk> \<Longrightarrow> a \<in> J k
[PROOF STEP]
apply (frule_tac m = k and n = "Suc n" in noteq_le_less, assumption+,
        thin_tac "k \<le> Suc n")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>n k. \<lbrakk>\<forall>k\<le>n. a \<in> J k; a \<in> i\<Pi>\<^bsub>R,n\<^esub> J \<diamondsuit>\<^sub>r J (Suc n); a \<in> i\<Pi>\<^bsub>R,n\<^esub> J; a \<in> J (Suc n); k \<noteq> Suc n; k < Suc n\<rbrakk> \<Longrightarrow> a \<in> J k
[PROOF STEP]
apply (frule_tac x = k and n = "Suc n" in less_le_diff, simp)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma (in Ring) ele_n_prod:"\<lbrakk>\<forall>k \<le> n. ideal R (J k);
                       a \<in> ideal_n_prod R n J \<rbrakk> \<Longrightarrow>  \<forall>k \<le> n. a \<in> (J k)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<forall>k\<le>n. ideal R (J k); a \<in> i\<Pi>\<^bsub>R,n\<^esub> J\<rbrakk> \<Longrightarrow> \<forall>k\<le>n. a \<in> J k
[PROOF STEP]
by (simp add: ele_n_prodTr1 [of "n" "J" "a"])


[STATEMENT]
lemma (in Ring) idealprod_whole_l:"ideal R I \<Longrightarrow> (carrier R) \<diamondsuit>\<^sub>r\<^bsub>R\<^esub> I = I"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ideal R I \<Longrightarrow> carrier R \<diamondsuit>\<^sub>r I = I
[PROOF STEP]
apply (rule equalityI)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. ideal R I \<Longrightarrow> carrier R \<diamondsuit>\<^sub>r I \<subseteq> I
 2. ideal R I \<Longrightarrow> I \<subseteq> carrier R \<diamondsuit>\<^sub>r I
[PROOF STEP]
apply (rule subsetI)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x. \<lbrakk>ideal R I; x \<in> carrier R \<diamondsuit>\<^sub>r I\<rbrakk> \<Longrightarrow> x \<in> I
 2. ideal R I \<Longrightarrow> I \<subseteq> carrier R \<diamondsuit>\<^sub>r I
[PROOF STEP]
apply (simp add:ideal_prod_def)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x. \<lbrakk>ideal R I; \<forall>xa. ideal R xa \<and> {x. \<exists>i\<in>carrier R. \<exists>j\<in>I. x = i \<cdot>\<^sub>r j} \<subseteq> xa \<longrightarrow> x \<in> xa\<rbrakk> \<Longrightarrow> x \<in> I
 2. ideal R I \<Longrightarrow> I \<subseteq> carrier R \<diamondsuit>\<^sub>r I
[PROOF STEP]
apply (subgoal_tac "{x. \<exists>i\<in>carrier R. \<exists>j\<in>I. x = i \<cdot>\<^sub>r j} \<subseteq> I")
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>x. \<lbrakk>ideal R I; \<forall>xa. ideal R xa \<and> {x. \<exists>i\<in>carrier R. \<exists>j\<in>I. x = i \<cdot>\<^sub>r j} \<subseteq> xa \<longrightarrow> x \<in> xa; {x. \<exists>i\<in>carrier R. \<exists>j\<in>I. x = i \<cdot>\<^sub>r j} \<subseteq> I\<rbrakk> \<Longrightarrow> x \<in> I
 2. \<And>x. \<lbrakk>ideal R I; \<forall>xa. ideal R xa \<and> {x. \<exists>i\<in>carrier R. \<exists>j\<in>I. x = i \<cdot>\<^sub>r j} \<subseteq> xa \<longrightarrow> x \<in> xa\<rbrakk> \<Longrightarrow> {x. \<exists>i\<in>carrier R. \<exists>j\<in>I. x = i \<cdot>\<^sub>r j} \<subseteq> I
 3. ideal R I \<Longrightarrow> I \<subseteq> carrier R \<diamondsuit>\<^sub>r I
[PROOF STEP]
apply blast
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x. \<lbrakk>ideal R I; \<forall>xa. ideal R xa \<and> {x. \<exists>i\<in>carrier R. \<exists>j\<in>I. x = i \<cdot>\<^sub>r j} \<subseteq> xa \<longrightarrow> x \<in> xa\<rbrakk> \<Longrightarrow> {x. \<exists>i\<in>carrier R. \<exists>j\<in>I. x = i \<cdot>\<^sub>r j} \<subseteq> I
 2. ideal R I \<Longrightarrow> I \<subseteq> carrier R \<diamondsuit>\<^sub>r I
[PROOF STEP]
apply (thin_tac "\<forall>xa. ideal R xa \<and> {x. \<exists>i\<in>carrier R. \<exists>j\<in>I.
                       x = i \<cdot>\<^sub>r j} \<subseteq> xa \<longrightarrow> x \<in> xa")
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x. ideal R I \<Longrightarrow> {x. \<exists>i\<in>carrier R. \<exists>j\<in>I. x = i \<cdot>\<^sub>r j} \<subseteq> I
 2. ideal R I \<Longrightarrow> I \<subseteq> carrier R \<diamondsuit>\<^sub>r I
[PROOF STEP]
apply (rule subsetI)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x xa. \<lbrakk>ideal R I; xa \<in> {x. \<exists>i\<in>carrier R. \<exists>j\<in>I. x = i \<cdot>\<^sub>r j}\<rbrakk> \<Longrightarrow> xa \<in> I
 2. ideal R I \<Longrightarrow> I \<subseteq> carrier R \<diamondsuit>\<^sub>r I
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>xa. \<lbrakk>ideal R I; \<exists>i\<in>carrier R. \<exists>j\<in>I. xa = i \<cdot>\<^sub>r j\<rbrakk> \<Longrightarrow> xa \<in> I
 2. ideal R I \<Longrightarrow> I \<subseteq> carrier R \<diamondsuit>\<^sub>r I
[PROOF STEP]
apply ((erule bexE)+, simp)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>xa i j. \<lbrakk>ideal R I; i \<in> carrier R; j \<in> I; xa = i \<cdot>\<^sub>r j\<rbrakk> \<Longrightarrow> i \<cdot>\<^sub>r j \<in> I
 2. ideal R I \<Longrightarrow> I \<subseteq> carrier R \<diamondsuit>\<^sub>r I
[PROOF STEP]
apply (thin_tac "xa = i \<cdot>\<^sub>r j", simp add:ideal_ring_multiple)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ideal R I \<Longrightarrow> I \<subseteq> carrier R \<diamondsuit>\<^sub>r I
[PROOF STEP]
apply (rule subsetI)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>ideal R I; x \<in> I\<rbrakk> \<Longrightarrow> x \<in> carrier R \<diamondsuit>\<^sub>r I
[PROOF STEP]
apply (simp add:ideal_prod_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>ideal R I; x \<in> I\<rbrakk> \<Longrightarrow> \<forall>xa. ideal R xa \<and> {x. \<exists>i\<in>carrier R. \<exists>j\<in>I. x = i \<cdot>\<^sub>r j} \<subseteq> xa \<longrightarrow> x \<in> xa
[PROOF STEP]
apply (rule allI, rule impI)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x xa. \<lbrakk>ideal R I; x \<in> I; ideal R xa \<and> {x. \<exists>i\<in>carrier R. \<exists>j\<in>I. x = i \<cdot>\<^sub>r j} \<subseteq> xa\<rbrakk> \<Longrightarrow> x \<in> xa
[PROOF STEP]
apply (erule conjE)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x xa. \<lbrakk>ideal R I; x \<in> I; ideal R xa; {x. \<exists>i\<in>carrier R. \<exists>j\<in>I. x = i \<cdot>\<^sub>r j} \<subseteq> xa\<rbrakk> \<Longrightarrow> x \<in> xa
[PROOF STEP]
apply (rename_tac xa X)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>xa X. \<lbrakk>ideal R I; xa \<in> I; ideal R X; {x. \<exists>i\<in>carrier R. \<exists>j\<in>I. x = i \<cdot>\<^sub>r j} \<subseteq> X\<rbrakk> \<Longrightarrow> xa \<in> X
[PROOF STEP]
apply (cut_tac ring_one)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>xa X. \<lbrakk>ideal R I; xa \<in> I; ideal R X; {x. \<exists>i\<in>carrier R. \<exists>j\<in>I. x = i \<cdot>\<^sub>r j} \<subseteq> X; 1\<^sub>r \<in> carrier R\<rbrakk> \<Longrightarrow> xa \<in> X
[PROOF STEP]
apply (frule_tac h = xa in ideal_subset[of "I"], assumption,
        frule_tac x = xa in ring_l_one)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>xa X. \<lbrakk>ideal R I; xa \<in> I; ideal R X; {x. \<exists>i\<in>carrier R. \<exists>j\<in>I. x = i \<cdot>\<^sub>r j} \<subseteq> X; 1\<^sub>r \<in> carrier R; xa \<in> carrier R; 1\<^sub>r \<cdot>\<^sub>r xa = xa\<rbrakk> \<Longrightarrow> xa \<in> X
[PROOF STEP]
apply (subgoal_tac "1\<^sub>r \<cdot>\<^sub>r xa \<in> {x. \<exists>i\<in>carrier R. \<exists>j\<in>I. x = i \<cdot>\<^sub>r j}")
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>xa X. \<lbrakk>ideal R I; xa \<in> I; ideal R X; {x. \<exists>i\<in>carrier R. \<exists>j\<in>I. x = i \<cdot>\<^sub>r j} \<subseteq> X; 1\<^sub>r \<in> carrier R; xa \<in> carrier R; 1\<^sub>r \<cdot>\<^sub>r xa = xa; 1\<^sub>r \<cdot>\<^sub>r xa \<in> {x. \<exists>i\<in>carrier R. \<exists>j\<in>I. x = i \<cdot>\<^sub>r j}\<rbrakk> \<Longrightarrow> xa \<in> X
 2. \<And>xa X. \<lbrakk>ideal R I; xa \<in> I; ideal R X; {x. \<exists>i\<in>carrier R. \<exists>j\<in>I. x = i \<cdot>\<^sub>r j} \<subseteq> X; 1\<^sub>r \<in> carrier R; xa \<in> carrier R; 1\<^sub>r \<cdot>\<^sub>r xa = xa\<rbrakk> \<Longrightarrow> 1\<^sub>r \<cdot>\<^sub>r xa \<in> {x. \<exists>i\<in>carrier R. \<exists>j\<in>I. x = i \<cdot>\<^sub>r j}
[PROOF STEP]
apply (rule_tac c = xa and A = "{x. \<exists>i\<in>carrier R. \<exists>j\<in>I. x = i \<cdot>\<^sub>r j}" and
         B = X in subsetD, assumption+)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>xa X. \<lbrakk>ideal R I; xa \<in> I; ideal R X; {x. \<exists>i\<in>carrier R. \<exists>j\<in>I. x = i \<cdot>\<^sub>r j} \<subseteq> X; 1\<^sub>r \<in> carrier R; xa \<in> carrier R; 1\<^sub>r \<cdot>\<^sub>r xa = xa; 1\<^sub>r \<cdot>\<^sub>r xa \<in> {x. \<exists>i\<in>carrier R. \<exists>j\<in>I. x = i \<cdot>\<^sub>r j}\<rbrakk> \<Longrightarrow> xa \<in> {x. \<exists>i\<in>carrier R. \<exists>j\<in>I. x = i \<cdot>\<^sub>r j}
 2. \<And>xa X. \<lbrakk>ideal R I; xa \<in> I; ideal R X; {x. \<exists>i\<in>carrier R. \<exists>j\<in>I. x = i \<cdot>\<^sub>r j} \<subseteq> X; 1\<^sub>r \<in> carrier R; xa \<in> carrier R; 1\<^sub>r \<cdot>\<^sub>r xa = xa\<rbrakk> \<Longrightarrow> 1\<^sub>r \<cdot>\<^sub>r xa \<in> {x. \<exists>i\<in>carrier R. \<exists>j\<in>I. x = i \<cdot>\<^sub>r j}
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>xa X. \<lbrakk>ideal R I; xa \<in> I; ideal R X; {x. \<exists>i\<in>carrier R. \<exists>j\<in>I. x = i \<cdot>\<^sub>r j} \<subseteq> X; 1\<^sub>r \<in> carrier R; xa \<in> carrier R; 1\<^sub>r \<cdot>\<^sub>r xa = xa\<rbrakk> \<Longrightarrow> 1\<^sub>r \<cdot>\<^sub>r xa \<in> {x. \<exists>i\<in>carrier R. \<exists>j\<in>I. x = i \<cdot>\<^sub>r j}
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>xa X. \<lbrakk>ideal R I; xa \<in> I; ideal R X; {x. \<exists>i\<in>carrier R. \<exists>j\<in>I. x = i \<cdot>\<^sub>r j} \<subseteq> X; 1\<^sub>r \<in> carrier R; xa \<in> carrier R; 1\<^sub>r \<cdot>\<^sub>r xa = xa\<rbrakk> \<Longrightarrow> \<exists>i\<in>carrier R. \<exists>j\<in>I. xa = i \<cdot>\<^sub>r j
[PROOF STEP]
apply (frule sym, thin_tac "1\<^sub>r \<cdot>\<^sub>r xa = xa", blast)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma (in Ring) idealprod_whole_r:"ideal R I \<Longrightarrow> I \<diamondsuit>\<^sub>r (carrier R) = I"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ideal R I \<Longrightarrow> I \<diamondsuit>\<^sub>r carrier R = I
[PROOF STEP]
by (cut_tac whole_ideal,
       simp add:ideal_prod_commute[of "I" "carrier R"],
       simp add:idealprod_whole_l)


[STATEMENT]
lemma (in Ring) idealpow_1_self:"ideal R I \<Longrightarrow> I \<^bsup>\<diamondsuit>R (Suc 0)\<^esup> = I"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ideal R I \<Longrightarrow> I \<^bsup>\<diamondsuit>R Suc 0\<^esup> = I
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ideal R I \<Longrightarrow> I \<diamondsuit>\<^sub>r carrier R = I
[PROOF STEP]
apply (simp add:idealprod_whole_r)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma (in Ring) ideal_pow_ideal:"ideal R I \<Longrightarrow> ideal R (I \<^bsup>\<diamondsuit>R n\<^esup>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ideal R I \<Longrightarrow> ideal R (I \<^bsup>\<diamondsuit>R n\<^esup>)
[PROOF STEP]
apply (induct_tac n)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. ideal R I \<Longrightarrow> ideal R (I \<^bsup>\<diamondsuit>R 0\<^esup>)
 2. \<And>n. \<lbrakk>ideal R I; ideal R (I \<^bsup>\<diamondsuit>R n\<^esup>)\<rbrakk> \<Longrightarrow> ideal R (I \<^bsup>\<diamondsuit>R Suc n\<^esup>)
[PROOF STEP]
apply (simp add:whole_ideal)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>n. \<lbrakk>ideal R I; ideal R (I \<^bsup>\<diamondsuit>R n\<^esup>)\<rbrakk> \<Longrightarrow> ideal R (I \<^bsup>\<diamondsuit>R Suc n\<^esup>)
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>n. \<lbrakk>ideal R I; ideal R (I \<^bsup>\<diamondsuit>R n\<^esup>)\<rbrakk> \<Longrightarrow> ideal R (I \<diamondsuit>\<^sub>r I \<^bsup>\<diamondsuit>R n\<^esup>)
[PROOF STEP]
apply (simp add:ideal_prod_ideal)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma (in Ring) ideal_prod_prime:"\<lbrakk>ideal R I; ideal R J; prime_ideal R P;
                          I \<diamondsuit>\<^sub>r J \<subseteq> P \<rbrakk> \<Longrightarrow> I \<subseteq> P \<or> J \<subseteq> P"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ideal R I; ideal R J; prime_ideal R P; I \<diamondsuit>\<^sub>r J \<subseteq> P\<rbrakk> \<Longrightarrow> I \<subseteq> P \<or> J \<subseteq> P
[PROOF STEP]
apply (rule contrapos_pp, simp+)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ideal R I; ideal R J; prime_ideal R P; I \<diamondsuit>\<^sub>r J \<subseteq> P; \<not> I \<subseteq> P \<and> \<not> J \<subseteq> P\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
apply (erule conjE, simp add:subset_eq, (erule bexE)+)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x xa. \<lbrakk>ideal R I; ideal R J; prime_ideal R P; \<forall>x\<in>I \<diamondsuit>\<^sub>r J. x \<in> P; x \<in> I; x \<notin> P; xa \<in> J; xa \<notin> P\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
apply (frule_tac i = x and j = xa in prod_mem_prod_ideals[of "I" "J"],
          assumption+)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x xa. \<lbrakk>ideal R I; ideal R J; prime_ideal R P; \<forall>x\<in>I \<diamondsuit>\<^sub>r J. x \<in> P; x \<in> I; x \<notin> P; xa \<in> J; xa \<notin> P; x \<cdot>\<^sub>r xa \<in> I \<diamondsuit>\<^sub>r J\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
apply (frule_tac x = "x \<cdot>\<^sub>r xa" in bspec, assumption,
        thin_tac "\<forall>x\<in>I \<diamondsuit>\<^sub>r\<^bsub> R\<^esub> J. x \<in> P")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x xa. \<lbrakk>ideal R I; ideal R J; prime_ideal R P; x \<in> I; x \<notin> P; xa \<in> J; xa \<notin> P; x \<cdot>\<^sub>r xa \<in> I \<diamondsuit>\<^sub>r J; x \<cdot>\<^sub>r xa \<in> P\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
apply (simp add: prime_ideal_def, (erule conjE)+)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x xa. \<lbrakk>ideal R I; ideal R J; x \<in> I; x \<notin> P; xa \<in> J; xa \<notin> P; x \<cdot>\<^sub>r xa \<in> I \<diamondsuit>\<^sub>r J; x \<cdot>\<^sub>r xa \<in> P; ideal R P; 1\<^sub>r \<notin> P; \<forall>x\<in>carrier R. \<forall>y\<in>carrier R. x \<cdot>\<^sub>r y \<in> P \<longrightarrow> x \<in> P \<or> y \<in> P\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
apply (frule_tac h = x in ideal_subset, assumption,
        frule_tac x = x in bspec, assumption,
        thin_tac "\<forall>x\<in>carrier R. \<forall>y\<in>carrier R. x \<cdot>\<^sub>r y \<in> P \<longrightarrow> x \<in> P \<or> y \<in> P",
        frule_tac h = xa in ideal_subset, assumption,
        frule_tac x = xa in bspec, assumption,
        thin_tac "\<forall>y\<in>carrier R. x \<cdot>\<^sub>r y \<in> P \<longrightarrow> x \<in> P \<or> y \<in> P",
        simp)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma (in Ring) ideal_n_prod_primeTr:"prime_ideal R P \<Longrightarrow>
       (\<forall>k \<le> n. ideal R (J k)) \<longrightarrow> (ideal_n_prod R n J \<subseteq> P) \<longrightarrow>
                                               (\<exists>i \<le> n. (J i) \<subseteq> P)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. prime_ideal R P \<Longrightarrow> (\<forall>k\<le>n. ideal R (J k)) \<longrightarrow> i\<Pi>\<^bsub>R,n\<^esub> J \<subseteq> P \<longrightarrow> (\<exists>i\<le>n. J i \<subseteq> P)
[PROOF STEP]
apply (induct_tac n)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. prime_ideal R P \<Longrightarrow> (\<forall>k\<le>0. ideal R (J k)) \<longrightarrow> i\<Pi>\<^bsub>R,0\<^esub> J \<subseteq> P \<longrightarrow> (\<exists>i\<le>0. J i \<subseteq> P)
 2. \<And>n. \<lbrakk>prime_ideal R P; (\<forall>k\<le>n. ideal R (J k)) \<longrightarrow> i\<Pi>\<^bsub>R,n\<^esub> J \<subseteq> P \<longrightarrow> (\<exists>i\<le>n. J i \<subseteq> P)\<rbrakk> \<Longrightarrow> (\<forall>k\<le>Suc n. ideal R (J k)) \<longrightarrow> i\<Pi>\<^bsub>R,Suc n\<^esub> J \<subseteq> P \<longrightarrow> (\<exists>i\<le>Suc n. J i \<subseteq> P)
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>n. \<lbrakk>prime_ideal R P; (\<forall>k\<le>n. ideal R (J k)) \<longrightarrow> i\<Pi>\<^bsub>R,n\<^esub> J \<subseteq> P \<longrightarrow> (\<exists>i\<le>n. J i \<subseteq> P)\<rbrakk> \<Longrightarrow> (\<forall>k\<le>Suc n. ideal R (J k)) \<longrightarrow> i\<Pi>\<^bsub>R,Suc n\<^esub> J \<subseteq> P \<longrightarrow> (\<exists>i\<le>Suc n. J i \<subseteq> P)
[PROOF STEP]
apply (rule impI)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>n. \<lbrakk>prime_ideal R P; (\<forall>k\<le>n. ideal R (J k)) \<longrightarrow> i\<Pi>\<^bsub>R,n\<^esub> J \<subseteq> P \<longrightarrow> (\<exists>i\<le>n. J i \<subseteq> P); \<forall>k\<le>Suc n. ideal R (J k)\<rbrakk> \<Longrightarrow> i\<Pi>\<^bsub>R,Suc n\<^esub> J \<subseteq> P \<longrightarrow> (\<exists>i\<le>Suc n. J i \<subseteq> P)
[PROOF STEP]
apply (rule impI, simp)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>n. \<lbrakk>prime_ideal R P; i\<Pi>\<^bsub>R,n\<^esub> J \<subseteq> P \<longrightarrow> (\<exists>i\<le>n. J i \<subseteq> P); \<forall>k\<le>Suc n. ideal R (J k); i\<Pi>\<^bsub>R,n\<^esub> J \<diamondsuit>\<^sub>r J (Suc n) \<subseteq> P\<rbrakk> \<Longrightarrow> \<exists>i\<le>Suc n. J i \<subseteq> P
[PROOF STEP]
apply (cut_tac I = "i\<Pi>\<^bsub>R,n\<^esub> J" and J = "J (Suc n)" in
                      ideal_prod_prime[of _ _ "P"],
        rule_tac n = n and J = J in n_prod_ideal,
         rule allI, simp+)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>n. \<lbrakk>prime_ideal R P; i\<Pi>\<^bsub>R,n\<^esub> J \<subseteq> P \<longrightarrow> (\<exists>i\<le>n. J i \<subseteq> P); \<forall>k\<le>Suc n. ideal R (J k); i\<Pi>\<^bsub>R,n\<^esub> J \<diamondsuit>\<^sub>r J (Suc n) \<subseteq> P; i\<Pi>\<^bsub>R,n\<^esub> J \<subseteq> P \<or> J (Suc n) \<subseteq> P\<rbrakk> \<Longrightarrow> \<exists>i\<le>Suc n. J i \<subseteq> P
[PROOF STEP]
apply (erule disjE, simp)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>n. \<lbrakk>prime_ideal R P; \<exists>i\<le>n. J i \<subseteq> P; \<forall>k\<le>Suc n. ideal R (J k); i\<Pi>\<^bsub>R,n\<^esub> J \<diamondsuit>\<^sub>r J (Suc n) \<subseteq> P; i\<Pi>\<^bsub>R,n\<^esub> J \<subseteq> P\<rbrakk> \<Longrightarrow> \<exists>i\<le>Suc n. J i \<subseteq> P
 2. \<And>n. \<lbrakk>prime_ideal R P; i\<Pi>\<^bsub>R,n\<^esub> J \<subseteq> P \<longrightarrow> (\<exists>i\<le>n. J i \<subseteq> P); \<forall>k\<le>Suc n. ideal R (J k); i\<Pi>\<^bsub>R,n\<^esub> J \<diamondsuit>\<^sub>r J (Suc n) \<subseteq> P; J (Suc n) \<subseteq> P\<rbrakk> \<Longrightarrow> \<exists>i\<le>Suc n. J i \<subseteq> P
[PROOF STEP]
apply (cut_tac n = n in Nsetn_sub_mem1,
        blast)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>n. \<lbrakk>prime_ideal R P; i\<Pi>\<^bsub>R,n\<^esub> J \<subseteq> P \<longrightarrow> (\<exists>i\<le>n. J i \<subseteq> P); \<forall>k\<le>Suc n. ideal R (J k); i\<Pi>\<^bsub>R,n\<^esub> J \<diamondsuit>\<^sub>r J (Suc n) \<subseteq> P; J (Suc n) \<subseteq> P\<rbrakk> \<Longrightarrow> \<exists>i\<le>Suc n. J i \<subseteq> P
[PROOF STEP]
apply blast
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma (in Ring) ideal_n_prod_prime:"\<lbrakk>prime_ideal R P;
            \<forall>k \<le> n. ideal R (J k); ideal_n_prod R n J \<subseteq> P\<rbrakk> \<Longrightarrow>
                                            \<exists>i \<le> n. (J i) \<subseteq> P"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>prime_ideal R P; \<forall>k\<le>n. ideal R (J k); i\<Pi>\<^bsub>R,n\<^esub> J \<subseteq> P\<rbrakk> \<Longrightarrow> \<exists>i\<le>n. J i \<subseteq> P
[PROOF STEP]
apply (simp add:ideal_n_prod_primeTr)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma (in Ring) prod_primeTr:"\<lbrakk>prime_ideal R P; ideal R A; \<not> A \<subseteq> P;
                ideal R B; \<not> B \<subseteq> P \<rbrakk> \<Longrightarrow> \<exists>x. x \<in> A \<and> x \<in> B \<and> x \<notin> P"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>prime_ideal R P; ideal R A; \<not> A \<subseteq> P; ideal R B; \<not> B \<subseteq> P\<rbrakk> \<Longrightarrow> \<exists>x. x \<in> A \<and> x \<in> B \<and> x \<notin> P
[PROOF STEP]
apply (simp add:subset_eq)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>prime_ideal R P; ideal R A; \<exists>x\<in>A. x \<notin> P; ideal R B; \<exists>x\<in>B. x \<notin> P\<rbrakk> \<Longrightarrow> \<exists>x. x \<in> A \<and> x \<in> B \<and> x \<notin> P
[PROOF STEP]
apply (erule bexE)+
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x xa. \<lbrakk>prime_ideal R P; ideal R A; ideal R B; x \<in> A; x \<notin> P; xa \<in> B; xa \<notin> P\<rbrakk> \<Longrightarrow> \<exists>x. x \<in> A \<and> x \<in> B \<and> x \<notin> P
[PROOF STEP]
apply (subgoal_tac "x \<cdot>\<^sub>r xa \<in> A \<and> x \<cdot>\<^sub>r xa \<in> B \<and> x \<cdot>\<^sub>r xa \<notin> P")
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x xa. \<lbrakk>prime_ideal R P; ideal R A; ideal R B; x \<in> A; x \<notin> P; xa \<in> B; xa \<notin> P; x \<cdot>\<^sub>r xa \<in> A \<and> x \<cdot>\<^sub>r xa \<in> B \<and> x \<cdot>\<^sub>r xa \<notin> P\<rbrakk> \<Longrightarrow> \<exists>x. x \<in> A \<and> x \<in> B \<and> x \<notin> P
 2. \<And>x xa. \<lbrakk>prime_ideal R P; ideal R A; ideal R B; x \<in> A; x \<notin> P; xa \<in> B; xa \<notin> P\<rbrakk> \<Longrightarrow> x \<cdot>\<^sub>r xa \<in> A \<and> x \<cdot>\<^sub>r xa \<in> B \<and> x \<cdot>\<^sub>r xa \<notin> P
[PROOF STEP]
apply blast
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x xa. \<lbrakk>prime_ideal R P; ideal R A; ideal R B; x \<in> A; x \<notin> P; xa \<in> B; xa \<notin> P\<rbrakk> \<Longrightarrow> x \<cdot>\<^sub>r xa \<in> A \<and> x \<cdot>\<^sub>r xa \<in> B \<and> x \<cdot>\<^sub>r xa \<notin> P
[PROOF STEP]
apply (rule conjI)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x xa. \<lbrakk>prime_ideal R P; ideal R A; ideal R B; x \<in> A; x \<notin> P; xa \<in> B; xa \<notin> P\<rbrakk> \<Longrightarrow> x \<cdot>\<^sub>r xa \<in> A
 2. \<And>x xa. \<lbrakk>prime_ideal R P; ideal R A; ideal R B; x \<in> A; x \<notin> P; xa \<in> B; xa \<notin> P\<rbrakk> \<Longrightarrow> x \<cdot>\<^sub>r xa \<in> B \<and> x \<cdot>\<^sub>r xa \<notin> P
[PROOF STEP]
apply (rule ideal_ring_multiple1, assumption+)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x xa. \<lbrakk>prime_ideal R P; ideal R A; ideal R B; x \<in> A; x \<notin> P; xa \<in> B; xa \<notin> P\<rbrakk> \<Longrightarrow> xa \<in> carrier R
 2. \<And>x xa. \<lbrakk>prime_ideal R P; ideal R A; ideal R B; x \<in> A; x \<notin> P; xa \<in> B; xa \<notin> P\<rbrakk> \<Longrightarrow> x \<cdot>\<^sub>r xa \<in> B \<and> x \<cdot>\<^sub>r xa \<notin> P
[PROOF STEP]
apply (simp add:ideal_subset)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x xa. \<lbrakk>prime_ideal R P; ideal R A; ideal R B; x \<in> A; x \<notin> P; xa \<in> B; xa \<notin> P\<rbrakk> \<Longrightarrow> x \<cdot>\<^sub>r xa \<in> B \<and> x \<cdot>\<^sub>r xa \<notin> P
[PROOF STEP]
apply (rule conjI)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x xa. \<lbrakk>prime_ideal R P; ideal R A; ideal R B; x \<in> A; x \<notin> P; xa \<in> B; xa \<notin> P\<rbrakk> \<Longrightarrow> x \<cdot>\<^sub>r xa \<in> B
 2. \<And>x xa. \<lbrakk>prime_ideal R P; ideal R A; ideal R B; x \<in> A; x \<notin> P; xa \<in> B; xa \<notin> P\<rbrakk> \<Longrightarrow> x \<cdot>\<^sub>r xa \<notin> P
[PROOF STEP]
apply (rule ideal_ring_multiple, assumption+)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x xa. \<lbrakk>prime_ideal R P; ideal R A; ideal R B; x \<in> A; x \<notin> P; xa \<in> B; xa \<notin> P\<rbrakk> \<Longrightarrow> x \<in> carrier R
 2. \<And>x xa. \<lbrakk>prime_ideal R P; ideal R A; ideal R B; x \<in> A; x \<notin> P; xa \<in> B; xa \<notin> P\<rbrakk> \<Longrightarrow> x \<cdot>\<^sub>r xa \<notin> P
[PROOF STEP]
apply (simp add:ideal_subset)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x xa. \<lbrakk>prime_ideal R P; ideal R A; ideal R B; x \<in> A; x \<notin> P; xa \<in> B; xa \<notin> P\<rbrakk> \<Longrightarrow> x \<cdot>\<^sub>r xa \<notin> P
[PROOF STEP]
apply (rule contrapos_pp, simp+)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x xa. \<lbrakk>prime_ideal R P; ideal R A; ideal R B; x \<in> A; x \<notin> P; xa \<in> B; xa \<notin> P; x \<cdot>\<^sub>r xa \<in> P\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
apply (simp add:prime_ideal_def, (erule conjE)+)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x xa. \<lbrakk>ideal R A; ideal R B; x \<in> A; x \<notin> P; xa \<in> B; xa \<notin> P; x \<cdot>\<^sub>r xa \<in> P; ideal R P; 1\<^sub>r \<notin> P; \<forall>x\<in>carrier R. \<forall>y\<in>carrier R. x \<cdot>\<^sub>r y \<in> P \<longrightarrow> x \<in> P \<or> y \<in> P\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
apply (frule_tac h = x in ideal_subset[of "A"], assumption+,
        frule_tac h = xa in ideal_subset[of "B"], assumption+,
        frule_tac x = x in bspec, assumption,
        thin_tac "\<forall>x\<in>carrier R. \<forall>y\<in>carrier R. x \<cdot>\<^sub>r y \<in> P \<longrightarrow> x \<in> P \<or> y \<in> P",
        frule_tac x = xa in bspec, assumption,
        thin_tac "\<forall>y\<in>carrier R. x \<cdot>\<^sub>r y \<in> P \<longrightarrow> x \<in> P \<or> y \<in> P")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x xa. \<lbrakk>ideal R A; ideal R B; x \<in> A; x \<notin> P; xa \<in> B; xa \<notin> P; x \<cdot>\<^sub>r xa \<in> P; ideal R P; 1\<^sub>r \<notin> P; x \<in> carrier R; xa \<in> carrier R; x \<cdot>\<^sub>r xa \<in> P \<longrightarrow> x \<in> P \<or> xa \<in> P\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma (in Ring) prod_primeTr1:"\<lbrakk>\<forall>k \<le> (Suc n). prime_ideal R (P k);
       ideal R A; \<forall>l \<le> (Suc n). \<not> (A \<subseteq> P l);
       \<forall>k \<le> (Suc n). \<forall>l \<le> (Suc n). k = l \<or> \<not> (P k) \<subseteq> (P l); i \<le> (Suc n)\<rbrakk> \<Longrightarrow>
       \<forall>l \<le> n. ppa R P A i l \<in> A \<and>
                  ppa R P A i l \<in> (P (skip i l)) \<and> ppa R P A i l \<notin> (P i)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<forall>k\<le>Suc n. prime_ideal R (P k); ideal R A; \<forall>l\<le>Suc n. \<not> A \<subseteq> P l; \<forall>k\<le>Suc n. \<forall>l\<le>Suc n. k = l \<or> \<not> P k \<subseteq> P l; i \<le> Suc n\<rbrakk> \<Longrightarrow> \<forall>l\<le>n. ppa R P A i l \<in> A \<and> ppa R P A i l \<in> P (skip i l) \<and> ppa R P A i l \<notin> P i
[PROOF STEP]
apply (rule allI, rule impI)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>l. \<lbrakk>\<forall>k\<le>Suc n. prime_ideal R (P k); ideal R A; \<forall>l\<le>Suc n. \<not> A \<subseteq> P l; \<forall>k\<le>Suc n. \<forall>l\<le>Suc n. k = l \<or> \<not> P k \<subseteq> P l; i \<le> Suc n; l \<le> n\<rbrakk> \<Longrightarrow> ppa R P A i l \<in> A \<and> ppa R P A i l \<in> P (skip i l) \<and> ppa R P A i l \<notin> P i
[PROOF STEP]
apply (cut_tac i = i and l = l in skip_il_neq_i)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>l. \<lbrakk>\<forall>k\<le>Suc n. prime_ideal R (P k); ideal R A; \<forall>l\<le>Suc n. \<not> A \<subseteq> P l; \<forall>k\<le>Suc n. \<forall>l\<le>Suc n. k = l \<or> \<not> P k \<subseteq> P l; i \<le> Suc n; l \<le> n; skip i l \<noteq> i\<rbrakk> \<Longrightarrow> ppa R P A i l \<in> A \<and> ppa R P A i l \<in> P (skip i l) \<and> ppa R P A i l \<notin> P i
[PROOF STEP]
apply (rotate_tac 2)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>l. \<lbrakk>\<forall>l\<le>Suc n. \<not> A \<subseteq> P l; \<forall>k\<le>Suc n. \<forall>l\<le>Suc n. k = l \<or> \<not> P k \<subseteq> P l; i \<le> Suc n; l \<le> n; skip i l \<noteq> i; \<forall>k\<le>Suc n. prime_ideal R (P k); ideal R A\<rbrakk> \<Longrightarrow> ppa R P A i l \<in> A \<and> ppa R P A i l \<in> P (skip i l) \<and> ppa R P A i l \<notin> P i
[PROOF STEP]
apply (frule_tac x = i in spec,
             thin_tac "\<forall>l \<le> (Suc n). \<not> A \<subseteq> P l", simp)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>l. \<lbrakk>\<forall>k\<le>Suc n. \<forall>l\<le>Suc n. k = l \<or> \<not> P k \<subseteq> P l; i \<le> Suc n; l \<le> n; skip i l \<noteq> i; \<forall>k\<le>Suc n. prime_ideal R (P k); ideal R A; \<not> A \<subseteq> P i\<rbrakk> \<Longrightarrow> ppa R P A i l \<in> A \<and> ppa R P A i l \<in> P (skip i l) \<and> ppa R P A i l \<notin> P i
[PROOF STEP]
apply (cut_tac l = l in skip_mem[of _ "n" "i"], simp,
             frule_tac x = "skip i l" in spec,
             thin_tac "\<forall>k \<le> (Suc n). \<forall>l \<le> (Suc n). k = l \<or> \<not> P k \<subseteq> P l",
             simp)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>l. \<lbrakk>i \<le> Suc n; l \<le> n; skip i l \<noteq> i; \<forall>k\<le>Suc n. prime_ideal R (P k); ideal R A; \<not> A \<subseteq> P i; skip i l \<le> Suc n; \<forall>la\<le>Suc n. skip i l = la \<or> \<not> P (skip i l) \<subseteq> P la\<rbrakk> \<Longrightarrow> ppa R P A i l \<in> A \<and> ppa R P A i l \<in> P (skip i l) \<and> ppa R P A i l \<notin> P i
[PROOF STEP]
apply (rotate_tac -1,
            frule_tac x = i in spec,
            thin_tac "\<forall>la \<le> (Suc n). skip i l = la \<or> \<not> P (skip i l) \<subseteq> P la",
            simp)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>l. \<lbrakk>i \<le> Suc n; l \<le> n; skip i l \<noteq> i; \<forall>k\<le>Suc n. prime_ideal R (P k); ideal R A; \<not> A \<subseteq> P i; skip i l \<le> Suc n; \<not> P (skip i l) \<subseteq> P i\<rbrakk> \<Longrightarrow> ppa R P A i l \<in> A \<and> ppa R P A i l \<in> P (skip i l) \<and> ppa R P A i l \<notin> P i
[PROOF STEP]
apply (cut_tac P = "P i" and A = A and B = "P (skip i l)" in prod_primeTr,
       simp, assumption+)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>l. \<lbrakk>i \<le> Suc n; l \<le> n; skip i l \<noteq> i; \<forall>k\<le>Suc n. prime_ideal R (P k); ideal R A; \<not> A \<subseteq> P i; skip i l \<le> Suc n; \<not> P (skip i l) \<subseteq> P i\<rbrakk> \<Longrightarrow> ideal R (P (skip i l))
 2. \<And>l. \<lbrakk>i \<le> Suc n; l \<le> n; skip i l \<noteq> i; \<forall>k\<le>Suc n. prime_ideal R (P k); ideal R A; \<not> A \<subseteq> P i; skip i l \<le> Suc n; \<not> P (skip i l) \<subseteq> P i\<rbrakk> \<Longrightarrow> \<not> P (skip i l) \<subseteq> P i
 3. \<And>l. \<lbrakk>i \<le> Suc n; l \<le> n; skip i l \<noteq> i; \<forall>k\<le>Suc n. prime_ideal R (P k); ideal R A; \<not> A \<subseteq> P i; skip i l \<le> Suc n; \<not> P (skip i l) \<subseteq> P i; \<exists>x. x \<in> A \<and> x \<in> P (skip i l) \<and> x \<notin> P i\<rbrakk> \<Longrightarrow> ppa R P A i l \<in> A \<and> ppa R P A i l \<in> P (skip i l) \<and> ppa R P A i l \<notin> P i
[PROOF STEP]
apply (frule_tac x = "skip i l" in spec,
        thin_tac "\<forall>k\<le>Suc n. prime_ideal R (P k)", simp,
        rule prime_ideal_ideal, assumption+)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>l. \<lbrakk>i \<le> Suc n; l \<le> n; skip i l \<noteq> i; \<forall>k\<le>Suc n. prime_ideal R (P k); ideal R A; \<not> A \<subseteq> P i; skip i l \<le> Suc n; \<not> P (skip i l) \<subseteq> P i; \<exists>x. x \<in> A \<and> x \<in> P (skip i l) \<and> x \<notin> P i\<rbrakk> \<Longrightarrow> ppa R P A i l \<in> A \<and> ppa R P A i l \<in> P (skip i l) \<and> ppa R P A i l \<notin> P i
[PROOF STEP]
apply (simp add:ppa_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>l. \<lbrakk>i \<le> Suc n; l \<le> n; skip i l \<noteq> i; \<forall>k\<le>Suc n. prime_ideal R (P k); ideal R A; \<not> A \<subseteq> P i; skip i l \<le> Suc n; \<not> P (skip i l) \<subseteq> P i; \<exists>x. x \<in> A \<and> x \<in> P (skip i l) \<and> x \<notin> P i\<rbrakk> \<Longrightarrow> (SOME x. x \<in> A \<and> x \<in> P (skip i l) \<and> x \<notin> P i) \<in> A \<and> (SOME x. x \<in> A \<and> x \<in> P (skip i l) \<and> x \<notin> P i) \<in> P (skip i l) \<and> (SOME x. x \<in> A \<and> x \<in> P (skip i l) \<and> x \<notin> P i) \<notin> P i
[PROOF STEP]
apply (rule someI2_ex, assumption+)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma (in Ring) ppa_mem:"\<lbrakk>\<forall>k \<le> (Suc n). prime_ideal R (P k); ideal R A;
      \<forall>l \<le> (Suc n). \<not> (A \<subseteq> P l);
      \<forall>k \<le> (Suc n). \<forall>l \<le> (Suc n). k = l \<or> \<not> (P k) \<subseteq> (P l);
      i  \<le> (Suc n); l \<le> n\<rbrakk> \<Longrightarrow> ppa R P A i l \<in> carrier R"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<forall>k\<le>Suc n. prime_ideal R (P k); ideal R A; \<forall>l\<le>Suc n. \<not> A \<subseteq> P l; \<forall>k\<le>Suc n. \<forall>l\<le>Suc n. k = l \<or> \<not> P k \<subseteq> P l; i \<le> Suc n; l \<le> n\<rbrakk> \<Longrightarrow> ppa R P A i l \<in> carrier R
[PROOF STEP]
apply (frule_tac prod_primeTr1[of n P A], assumption+)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<forall>k\<le>Suc n. prime_ideal R (P k); ideal R A; \<forall>l\<le>Suc n. \<not> A \<subseteq> P l; \<forall>k\<le>Suc n. \<forall>l\<le>Suc n. k = l \<or> \<not> P k \<subseteq> P l; i \<le> Suc n; l \<le> n; \<forall>l\<le>n. ppa R P A i l \<in> A \<and> ppa R P A i l \<in> P (skip i l) \<and> ppa R P A i l \<notin> P i\<rbrakk> \<Longrightarrow> ppa R P A i l \<in> carrier R
[PROOF STEP]
apply (rotate_tac -1, frule_tac x = l in spec,
        thin_tac "\<forall>l\<le>n. ppa R P A i l \<in> A \<and>
           ppa R P A i l \<in> P (skip i l) \<and> ppa R P A i l \<notin> P i", simp)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<forall>k\<le>Suc n. prime_ideal R (P k); ideal R A; \<forall>l\<le>Suc n. \<not> A \<subseteq> P l; \<forall>k\<le>Suc n. \<forall>l\<le>Suc n. k = l \<or> \<not> P k \<subseteq> P l; i \<le> Suc n; l \<le> n; ppa R P A i l \<in> A \<and> ppa R P A i l \<in> P (skip i l) \<and> ppa R P A i l \<notin> P i\<rbrakk> \<Longrightarrow> ppa R P A i l \<in> carrier R
[PROOF STEP]
apply (simp add:ideal_subset)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma (in Ring) nsum_memrTr:"(\<forall>i \<le> n. f i \<in> carrier R) \<longrightarrow>
                             (\<forall>l \<le> n. nsum R f l \<in> carrier R)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<forall>i\<le>n. f i \<in> carrier R) \<longrightarrow> (\<forall>l\<le>n. \<Sigma>\<^sub>e R f l \<in> carrier R)
[PROOF STEP]
apply (cut_tac ring_is_ag)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. aGroup R \<Longrightarrow> (\<forall>i\<le>n. f i \<in> carrier R) \<longrightarrow> (\<forall>l\<le>n. \<Sigma>\<^sub>e R f l \<in> carrier R)
[PROOF STEP]
apply (induct_tac n)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. aGroup R \<Longrightarrow> (\<forall>i\<le>0. f i \<in> carrier R) \<longrightarrow> (\<forall>l\<le>0. \<Sigma>\<^sub>e R f l \<in> carrier R)
 2. \<And>n. \<lbrakk>aGroup R; (\<forall>i\<le>n. f i \<in> carrier R) \<longrightarrow> (\<forall>l\<le>n. \<Sigma>\<^sub>e R f l \<in> carrier R)\<rbrakk> \<Longrightarrow> (\<forall>i\<le>Suc n. f i \<in> carrier R) \<longrightarrow> (\<forall>l\<le>Suc n. \<Sigma>\<^sub>e R f l \<in> carrier R)
[PROOF STEP]
(** n = 0 **)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. aGroup R \<Longrightarrow> (\<forall>i\<le>0. f i \<in> carrier R) \<longrightarrow> (\<forall>l\<le>0. \<Sigma>\<^sub>e R f l \<in> carrier R)
 2. \<And>n. \<lbrakk>aGroup R; (\<forall>i\<le>n. f i \<in> carrier R) \<longrightarrow> (\<forall>l\<le>n. \<Sigma>\<^sub>e R f l \<in> carrier R)\<rbrakk> \<Longrightarrow> (\<forall>i\<le>Suc n. f i \<in> carrier R) \<longrightarrow> (\<forall>l\<le>Suc n. \<Sigma>\<^sub>e R f l \<in> carrier R)
[PROOF STEP]
apply (rule impI, rule allI, rule impI)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>l. \<lbrakk>aGroup R; \<forall>i\<le>0. f i \<in> carrier R; l \<le> 0\<rbrakk> \<Longrightarrow> \<Sigma>\<^sub>e R f l \<in> carrier R
 2. \<And>n. \<lbrakk>aGroup R; (\<forall>i\<le>n. f i \<in> carrier R) \<longrightarrow> (\<forall>l\<le>n. \<Sigma>\<^sub>e R f l \<in> carrier R)\<rbrakk> \<Longrightarrow> (\<forall>i\<le>Suc n. f i \<in> carrier R) \<longrightarrow> (\<forall>l\<le>Suc n. \<Sigma>\<^sub>e R f l \<in> carrier R)
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>n. \<lbrakk>aGroup R; (\<forall>i\<le>n. f i \<in> carrier R) \<longrightarrow> (\<forall>l\<le>n. \<Sigma>\<^sub>e R f l \<in> carrier R)\<rbrakk> \<Longrightarrow> (\<forall>i\<le>Suc n. f i \<in> carrier R) \<longrightarrow> (\<forall>l\<le>Suc n. \<Sigma>\<^sub>e R f l \<in> carrier R)
[PROOF STEP]
(** n **)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>n. \<lbrakk>aGroup R; (\<forall>i\<le>n. f i \<in> carrier R) \<longrightarrow> (\<forall>l\<le>n. \<Sigma>\<^sub>e R f l \<in> carrier R)\<rbrakk> \<Longrightarrow> (\<forall>i\<le>Suc n. f i \<in> carrier R) \<longrightarrow> (\<forall>l\<le>Suc n. \<Sigma>\<^sub>e R f l \<in> carrier R)
[PROOF STEP]
apply (rule impI)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>n. \<lbrakk>aGroup R; (\<forall>i\<le>n. f i \<in> carrier R) \<longrightarrow> (\<forall>l\<le>n. \<Sigma>\<^sub>e R f l \<in> carrier R); \<forall>i\<le>Suc n. f i \<in> carrier R\<rbrakk> \<Longrightarrow> \<forall>l\<le>Suc n. \<Sigma>\<^sub>e R f l \<in> carrier R
[PROOF STEP]
apply (rule allI, rule impI)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>n l. \<lbrakk>aGroup R; (\<forall>i\<le>n. f i \<in> carrier R) \<longrightarrow> (\<forall>l\<le>n. \<Sigma>\<^sub>e R f l \<in> carrier R); \<forall>i\<le>Suc n. f i \<in> carrier R; l \<le> Suc n\<rbrakk> \<Longrightarrow> \<Sigma>\<^sub>e R f l \<in> carrier R
[PROOF STEP]
apply (rule aGroup.nsum_mem, assumption)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>n l. \<lbrakk>aGroup R; (\<forall>i\<le>n. f i \<in> carrier R) \<longrightarrow> (\<forall>l\<le>n. \<Sigma>\<^sub>e R f l \<in> carrier R); \<forall>i\<le>Suc n. f i \<in> carrier R; l \<le> Suc n\<rbrakk> \<Longrightarrow> \<forall>j\<le>l. f j \<in> carrier R
[PROOF STEP]
apply (rule allI, simp)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma (in Ring) nsum_memr:"\<forall>i \<le> n. f i \<in> carrier R \<Longrightarrow>
                          \<forall>l \<le> n. nsum R f l \<in> carrier R"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>i\<le>n. f i \<in> carrier R \<Longrightarrow> \<forall>l\<le>n. \<Sigma>\<^sub>e R f l \<in> carrier R
[PROOF STEP]
by (simp add:nsum_memrTr)


[STATEMENT]
lemma (in Ring) nsum_ideal_incTr:"ideal R A \<Longrightarrow>
               (\<forall>i \<le> n. f i \<in> A) \<longrightarrow>  nsum R f n \<in> A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ideal R A \<Longrightarrow> (\<forall>i\<le>n. f i \<in> A) \<longrightarrow> \<Sigma>\<^sub>e R f n \<in> A
[PROOF STEP]
apply (induct_tac n)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. ideal R A \<Longrightarrow> (\<forall>i\<le>0. f i \<in> A) \<longrightarrow> \<Sigma>\<^sub>e R f 0 \<in> A
 2. \<And>n. \<lbrakk>ideal R A; (\<forall>i\<le>n. f i \<in> A) \<longrightarrow> \<Sigma>\<^sub>e R f n \<in> A\<rbrakk> \<Longrightarrow> (\<forall>i\<le>Suc n. f i \<in> A) \<longrightarrow> \<Sigma>\<^sub>e R f Suc n \<in> A
[PROOF STEP]
apply (rule impI)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>ideal R A; \<forall>i\<le>0. f i \<in> A\<rbrakk> \<Longrightarrow> \<Sigma>\<^sub>e R f 0 \<in> A
 2. \<And>n. \<lbrakk>ideal R A; (\<forall>i\<le>n. f i \<in> A) \<longrightarrow> \<Sigma>\<^sub>e R f n \<in> A\<rbrakk> \<Longrightarrow> (\<forall>i\<le>Suc n. f i \<in> A) \<longrightarrow> \<Sigma>\<^sub>e R f Suc n \<in> A
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>n. \<lbrakk>ideal R A; (\<forall>i\<le>n. f i \<in> A) \<longrightarrow> \<Sigma>\<^sub>e R f n \<in> A\<rbrakk> \<Longrightarrow> (\<forall>i\<le>Suc n. f i \<in> A) \<longrightarrow> \<Sigma>\<^sub>e R f Suc n \<in> A
[PROOF STEP]
(** n **)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>n. \<lbrakk>ideal R A; (\<forall>i\<le>n. f i \<in> A) \<longrightarrow> \<Sigma>\<^sub>e R f n \<in> A\<rbrakk> \<Longrightarrow> (\<forall>i\<le>Suc n. f i \<in> A) \<longrightarrow> \<Sigma>\<^sub>e R f Suc n \<in> A
[PROOF STEP]
apply (rule impI)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>n. \<lbrakk>ideal R A; (\<forall>i\<le>n. f i \<in> A) \<longrightarrow> \<Sigma>\<^sub>e R f n \<in> A; \<forall>i\<le>Suc n. f i \<in> A\<rbrakk> \<Longrightarrow> \<Sigma>\<^sub>e R f Suc n \<in> A
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>n. \<lbrakk>ideal R A; \<Sigma>\<^sub>e R f n \<in> A; \<forall>i\<le>Suc n. f i \<in> A\<rbrakk> \<Longrightarrow> \<Sigma>\<^sub>e R f n \<plusminus> f (Suc n) \<in> A
[PROOF STEP]
apply (rule ideal_pOp_closed, assumption+)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>n. \<lbrakk>ideal R A; \<Sigma>\<^sub>e R f n \<in> A; \<forall>i\<le>Suc n. f i \<in> A\<rbrakk> \<Longrightarrow> f (Suc n) \<in> A
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma (in Ring) nsum_ideal_inc:"\<lbrakk>ideal R A; \<forall>i \<le> n. f i \<in> A\<rbrakk> \<Longrightarrow>
                    nsum R f n \<in> A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ideal R A; \<forall>i\<le>n. f i \<in> A\<rbrakk> \<Longrightarrow> \<Sigma>\<^sub>e R f n \<in> A
[PROOF STEP]
by (simp add:nsum_ideal_incTr)


[STATEMENT]
lemma (in Ring) nsum_ideal_excTr:"ideal R A \<Longrightarrow>
      (\<forall>i \<le> n. f i \<in> carrier R) \<and> (\<exists>j \<le> n. (\<forall>l \<in> {i. i \<le> n} -{j}. f l \<in> A)
       \<and> (f j \<notin> A)) \<longrightarrow> nsum R f n \<notin> A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ideal R A \<Longrightarrow> (\<forall>i\<le>n. f i \<in> carrier R) \<and> (\<exists>j\<le>n. (\<forall>l\<in>{i. i \<le> n} - {j}. f l \<in> A) \<and> f j \<notin> A) \<longrightarrow> \<Sigma>\<^sub>e R f n \<notin> A
[PROOF STEP]
apply (induct_tac n)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. ideal R A \<Longrightarrow> (\<forall>i\<le>0. f i \<in> carrier R) \<and> (\<exists>j\<le>0. (\<forall>l\<in>{i. i \<le> 0} - {j}. f l \<in> A) \<and> f j \<notin> A) \<longrightarrow> \<Sigma>\<^sub>e R f 0 \<notin> A
 2. \<And>n. \<lbrakk>ideal R A; (\<forall>i\<le>n. f i \<in> carrier R) \<and> (\<exists>j\<le>n. (\<forall>l\<in>{i. i \<le> n} - {j}. f l \<in> A) \<and> f j \<notin> A) \<longrightarrow> \<Sigma>\<^sub>e R f n \<notin> A\<rbrakk> \<Longrightarrow> (\<forall>i\<le>Suc n. f i \<in> carrier R) \<and> (\<exists>j\<le>Suc n. (\<forall>l\<in>{i. i \<le> Suc n} - {j}. f l \<in> A) \<and> f j \<notin> A) \<longrightarrow> \<Sigma>\<^sub>e R f Suc n \<notin> A
[PROOF STEP]
(** n = 0 **)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. ideal R A \<Longrightarrow> (\<forall>i\<le>0. f i \<in> carrier R) \<and> (\<exists>j\<le>0. (\<forall>l\<in>{i. i \<le> 0} - {j}. f l \<in> A) \<and> f j \<notin> A) \<longrightarrow> \<Sigma>\<^sub>e R f 0 \<notin> A
 2. \<And>n. \<lbrakk>ideal R A; (\<forall>i\<le>n. f i \<in> carrier R) \<and> (\<exists>j\<le>n. (\<forall>l\<in>{i. i \<le> n} - {j}. f l \<in> A) \<and> f j \<notin> A) \<longrightarrow> \<Sigma>\<^sub>e R f n \<notin> A\<rbrakk> \<Longrightarrow> (\<forall>i\<le>Suc n. f i \<in> carrier R) \<and> (\<exists>j\<le>Suc n. (\<forall>l\<in>{i. i \<le> Suc n} - {j}. f l \<in> A) \<and> f j \<notin> A) \<longrightarrow> \<Sigma>\<^sub>e R f Suc n \<notin> A
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>n. \<lbrakk>ideal R A; (\<forall>i\<le>n. f i \<in> carrier R) \<and> (\<exists>j\<le>n. (\<forall>l\<in>{i. i \<le> n} - {j}. f l \<in> A) \<and> f j \<notin> A) \<longrightarrow> \<Sigma>\<^sub>e R f n \<notin> A\<rbrakk> \<Longrightarrow> (\<forall>i\<le>Suc n. f i \<in> carrier R) \<and> (\<exists>j\<le>Suc n. (\<forall>l\<in>{i. i \<le> Suc n} - {j}. f l \<in> A) \<and> f j \<notin> A) \<longrightarrow> \<Sigma>\<^sub>e R f Suc n \<notin> A
[PROOF STEP]
(** n **)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>n. \<lbrakk>ideal R A; (\<forall>i\<le>n. f i \<in> carrier R) \<and> (\<exists>j\<le>n. (\<forall>l\<in>{i. i \<le> n} - {j}. f l \<in> A) \<and> f j \<notin> A) \<longrightarrow> \<Sigma>\<^sub>e R f n \<notin> A\<rbrakk> \<Longrightarrow> (\<forall>i\<le>Suc n. f i \<in> carrier R) \<and> (\<exists>j\<le>Suc n. (\<forall>l\<in>{i. i \<le> Suc n} - {j}. f l \<in> A) \<and> f j \<notin> A) \<longrightarrow> \<Sigma>\<^sub>e R f Suc n \<notin> A
[PROOF STEP]
apply (rule impI)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>n. \<lbrakk>ideal R A; (\<forall>i\<le>n. f i \<in> carrier R) \<and> (\<exists>j\<le>n. (\<forall>l\<in>{i. i \<le> n} - {j}. f l \<in> A) \<and> f j \<notin> A) \<longrightarrow> \<Sigma>\<^sub>e R f n \<notin> A; (\<forall>i\<le>Suc n. f i \<in> carrier R) \<and> (\<exists>j\<le>Suc n. (\<forall>l\<in>{i. i \<le> Suc n} - {j}. f l \<in> A) \<and> f j \<notin> A)\<rbrakk> \<Longrightarrow> \<Sigma>\<^sub>e R f Suc n \<notin> A
[PROOF STEP]
apply (erule conjE)+
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>n. \<lbrakk>ideal R A; (\<forall>i\<le>n. f i \<in> carrier R) \<and> (\<exists>j\<le>n. (\<forall>l\<in>{i. i \<le> n} - {j}. f l \<in> A) \<and> f j \<notin> A) \<longrightarrow> \<Sigma>\<^sub>e R f n \<notin> A; \<forall>i\<le>Suc n. f i \<in> carrier R; \<exists>j\<le>Suc n. (\<forall>l\<in>{i. i \<le> Suc n} - {j}. f l \<in> A) \<and> f j \<notin> A\<rbrakk> \<Longrightarrow> \<Sigma>\<^sub>e R f Suc n \<notin> A
[PROOF STEP]
apply (erule exE)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>n j. \<lbrakk>ideal R A; (\<forall>i\<le>n. f i \<in> carrier R) \<and> (\<exists>j\<le>n. (\<forall>l\<in>{i. i \<le> n} - {j}. f l \<in> A) \<and> f j \<notin> A) \<longrightarrow> \<Sigma>\<^sub>e R f n \<notin> A; \<forall>i\<le>Suc n. f i \<in> carrier R; j \<le> Suc n \<and> (\<forall>l\<in>{i. i \<le> Suc n} - {j}. f l \<in> A) \<and> f j \<notin> A\<rbrakk> \<Longrightarrow> \<Sigma>\<^sub>e R f Suc n \<notin> A
[PROOF STEP]
apply (case_tac "j = Suc n", simp)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>n j. \<lbrakk>ideal R A; (\<exists>j\<le>n. f j \<notin> A) \<longrightarrow> \<Sigma>\<^sub>e R f n \<notin> A; \<forall>i\<le>Suc n. f i \<in> carrier R; (\<forall>l\<in>{i. i \<le> Suc n} - {Suc n}. f l \<in> A) \<and> f (Suc n) \<notin> A; j = Suc n\<rbrakk> \<Longrightarrow> \<Sigma>\<^sub>e R f n \<plusminus> f (Suc n) \<notin> A
 2. \<And>n j. \<lbrakk>ideal R A; (\<forall>i\<le>n. f i \<in> carrier R) \<and> (\<exists>j\<le>n. (\<forall>l\<in>{i. i \<le> n} - {j}. f l \<in> A) \<and> f j \<notin> A) \<longrightarrow> \<Sigma>\<^sub>e R f n \<notin> A; \<forall>i\<le>Suc n. f i \<in> carrier R; j \<le> Suc n \<and> (\<forall>l\<in>{i. i \<le> Suc n} - {j}. f l \<in> A) \<and> f j \<notin> A; j \<noteq> Suc n\<rbrakk> \<Longrightarrow> \<Sigma>\<^sub>e R f Suc n \<notin> A
[PROOF STEP]
apply (
       thin_tac "(\<exists>j\<le>n. f j \<notin> A) \<longrightarrow> \<Sigma>\<^sub>e R f n \<notin> A")
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>n j. \<lbrakk>ideal R A; \<forall>i\<le>Suc n. f i \<in> carrier R; (\<forall>l\<in>{i. i \<le> Suc n} - {Suc n}. f l \<in> A) \<and> f (Suc n) \<notin> A; j = Suc n\<rbrakk> \<Longrightarrow> \<Sigma>\<^sub>e R f n \<plusminus> f (Suc n) \<notin> A
 2. \<And>n j. \<lbrakk>ideal R A; (\<forall>i\<le>n. f i \<in> carrier R) \<and> (\<exists>j\<le>n. (\<forall>l\<in>{i. i \<le> n} - {j}. f l \<in> A) \<and> f j \<notin> A) \<longrightarrow> \<Sigma>\<^sub>e R f n \<notin> A; \<forall>i\<le>Suc n. f i \<in> carrier R; j \<le> Suc n \<and> (\<forall>l\<in>{i. i \<le> Suc n} - {j}. f l \<in> A) \<and> f j \<notin> A; j \<noteq> Suc n\<rbrakk> \<Longrightarrow> \<Sigma>\<^sub>e R f Suc n \<notin> A
[PROOF STEP]
apply (erule conjE)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>n j. \<lbrakk>ideal R A; \<forall>i\<le>Suc n. f i \<in> carrier R; j = Suc n; \<forall>l\<in>{i. i \<le> Suc n} - {Suc n}. f l \<in> A; f (Suc n) \<notin> A\<rbrakk> \<Longrightarrow> \<Sigma>\<^sub>e R f n \<plusminus> f (Suc n) \<notin> A
 2. \<And>n j. \<lbrakk>ideal R A; (\<forall>i\<le>n. f i \<in> carrier R) \<and> (\<exists>j\<le>n. (\<forall>l\<in>{i. i \<le> n} - {j}. f l \<in> A) \<and> f j \<notin> A) \<longrightarrow> \<Sigma>\<^sub>e R f n \<notin> A; \<forall>i\<le>Suc n. f i \<in> carrier R; j \<le> Suc n \<and> (\<forall>l\<in>{i. i \<le> Suc n} - {j}. f l \<in> A) \<and> f j \<notin> A; j \<noteq> Suc n\<rbrakk> \<Longrightarrow> \<Sigma>\<^sub>e R f Suc n \<notin> A
[PROOF STEP]
apply (cut_tac n = n and f = f in nsum_ideal_inc[of A], assumption,
        rule allI, simp)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>n j. \<lbrakk>ideal R A; \<forall>i\<le>Suc n. f i \<in> carrier R; j = Suc n; \<forall>l\<in>{i. i \<le> Suc n} - {Suc n}. f l \<in> A; f (Suc n) \<notin> A; \<Sigma>\<^sub>e R f n \<in> A\<rbrakk> \<Longrightarrow> \<Sigma>\<^sub>e R f n \<plusminus> f (Suc n) \<notin> A
 2. \<And>n j. \<lbrakk>ideal R A; (\<forall>i\<le>n. f i \<in> carrier R) \<and> (\<exists>j\<le>n. (\<forall>l\<in>{i. i \<le> n} - {j}. f l \<in> A) \<and> f j \<notin> A) \<longrightarrow> \<Sigma>\<^sub>e R f n \<notin> A; \<forall>i\<le>Suc n. f i \<in> carrier R; j \<le> Suc n \<and> (\<forall>l\<in>{i. i \<le> Suc n} - {j}. f l \<in> A) \<and> f j \<notin> A; j \<noteq> Suc n\<rbrakk> \<Longrightarrow> \<Sigma>\<^sub>e R f Suc n \<notin> A
[PROOF STEP]
apply (rule contrapos_pp, simp+)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>n j. \<lbrakk>ideal R A; \<forall>i\<le>Suc n. f i \<in> carrier R; j = Suc n; \<forall>l\<in>{i. i \<le> Suc n} - {Suc n}. f l \<in> A; f (Suc n) \<notin> A; \<Sigma>\<^sub>e R f n \<in> A; \<Sigma>\<^sub>e R f n \<plusminus> f (Suc n) \<in> A\<rbrakk> \<Longrightarrow> False
 2. \<And>n j. \<lbrakk>ideal R A; (\<forall>i\<le>n. f i \<in> carrier R) \<and> (\<exists>j\<le>n. (\<forall>l\<in>{i. i \<le> n} - {j}. f l \<in> A) \<and> f j \<notin> A) \<longrightarrow> \<Sigma>\<^sub>e R f n \<notin> A; \<forall>i\<le>Suc n. f i \<in> carrier R; j \<le> Suc n \<and> (\<forall>l\<in>{i. i \<le> Suc n} - {j}. f l \<in> A) \<and> f j \<notin> A; j \<noteq> Suc n\<rbrakk> \<Longrightarrow> \<Sigma>\<^sub>e R f Suc n \<notin> A
[PROOF STEP]
apply (frule_tac a = "\<Sigma>\<^sub>e R f n" and b = "f (Suc n)" in
                   ideal_ele_sumTr1[of A],
        simp add:ideal_subset, simp, assumption+, simp)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>n j. \<lbrakk>ideal R A; (\<forall>i\<le>n. f i \<in> carrier R) \<and> (\<exists>j\<le>n. (\<forall>l\<in>{i. i \<le> n} - {j}. f l \<in> A) \<and> f j \<notin> A) \<longrightarrow> \<Sigma>\<^sub>e R f n \<notin> A; \<forall>i\<le>Suc n. f i \<in> carrier R; j \<le> Suc n \<and> (\<forall>l\<in>{i. i \<le> Suc n} - {j}. f l \<in> A) \<and> f j \<notin> A; j \<noteq> Suc n\<rbrakk> \<Longrightarrow> \<Sigma>\<^sub>e R f Suc n \<notin> A
[PROOF STEP]
apply (erule conjE,
       frule_tac m = j and n = "Suc n" in noteq_le_less, assumption,
       frule_tac x = j and n = "Suc n" in less_le_diff,
       thin_tac "j \<le> Suc n", thin_tac "j < Suc n", simp,
       cut_tac n = n in Nsetn_sub_mem1, simp)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>n j. \<lbrakk>ideal R A; (\<exists>j\<le>n. (\<forall>l\<in>{i. i \<le> n} - {j}. f l \<in> A) \<and> f j \<notin> A) \<longrightarrow> \<Sigma>\<^sub>e R f n \<notin> A; \<forall>i\<le>Suc n. f i \<in> carrier R; (\<forall>l\<in>{i. i \<le> Suc n} - {j}. f l \<in> A) \<and> f j \<notin> A; j \<le> n\<rbrakk> \<Longrightarrow> \<Sigma>\<^sub>e R f n \<plusminus> f (Suc n) \<notin> A
[PROOF STEP]
apply (erule conjE,
       frule_tac x = "Suc n" in bspec, simp)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>n j. \<lbrakk>ideal R A; (\<exists>j\<le>n. (\<forall>l\<in>{i. i \<le> n} - {j}. f l \<in> A) \<and> f j \<notin> A) \<longrightarrow> \<Sigma>\<^sub>e R f n \<notin> A; \<forall>i\<le>Suc n. f i \<in> carrier R; j \<le> n; \<forall>l\<in>{i. i \<le> Suc n} - {j}. f l \<in> A; f j \<notin> A; f (Suc n) \<in> A\<rbrakk> \<Longrightarrow> \<Sigma>\<^sub>e R f n \<plusminus> f (Suc n) \<notin> A
[PROOF STEP]
apply (rule contrapos_pp, simp+)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>n j. \<lbrakk>ideal R A; (\<exists>j\<le>n. (\<forall>l\<in>{i. i \<le> n} - {j}. f l \<in> A) \<and> f j \<notin> A) \<longrightarrow> \<Sigma>\<^sub>e R f n \<notin> A; \<forall>i\<le>Suc n. f i \<in> carrier R; j \<le> n; \<forall>l\<in>{i. i \<le> Suc n} - {j}. f l \<in> A; f j \<notin> A; \<Sigma>\<^sub>e R f n \<plusminus> f (Suc n) \<in> A\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
apply (frule_tac a = "\<Sigma>\<^sub>e R f n" and b = "f (Suc n)" in
                   ideal_ele_sumTr2[of A])
[PROOF STATE]
proof (prove)
goal (5 subgoals):
 1. \<And>n j. \<lbrakk>ideal R A; (\<exists>j\<le>n. (\<forall>l\<in>{i. i \<le> n} - {j}. f l \<in> A) \<and> f j \<notin> A) \<longrightarrow> \<Sigma>\<^sub>e R f n \<notin> A; \<forall>i\<le>Suc n. f i \<in> carrier R; j \<le> n; \<forall>l\<in>{i. i \<le> Suc n} - {j}. f l \<in> A; f j \<notin> A; \<Sigma>\<^sub>e R f n \<plusminus> f (Suc n) \<in> A\<rbrakk> \<Longrightarrow> \<Sigma>\<^sub>e R f n \<in> carrier R
 2. \<And>n j. \<lbrakk>ideal R A; (\<exists>j\<le>n. (\<forall>l\<in>{i. i \<le> n} - {j}. f l \<in> A) \<and> f j \<notin> A) \<longrightarrow> \<Sigma>\<^sub>e R f n \<notin> A; \<forall>i\<le>Suc n. f i \<in> carrier R; j \<le> n; \<forall>l\<in>{i. i \<le> Suc n} - {j}. f l \<in> A; f j \<notin> A; \<Sigma>\<^sub>e R f n \<plusminus> f (Suc n) \<in> A\<rbrakk> \<Longrightarrow> f (Suc n) \<in> carrier R
 3. \<And>n j. \<lbrakk>ideal R A; (\<exists>j\<le>n. (\<forall>l\<in>{i. i \<le> n} - {j}. f l \<in> A) \<and> f j \<notin> A) \<longrightarrow> \<Sigma>\<^sub>e R f n \<notin> A; \<forall>i\<le>Suc n. f i \<in> carrier R; j \<le> n; \<forall>l\<in>{i. i \<le> Suc n} - {j}. f l \<in> A; f j \<notin> A; \<Sigma>\<^sub>e R f n \<plusminus> f (Suc n) \<in> A\<rbrakk> \<Longrightarrow> \<Sigma>\<^sub>e R f n \<plusminus> f (Suc n) \<in> A
 4. \<And>n j. \<lbrakk>ideal R A; (\<exists>j\<le>n. (\<forall>l\<in>{i. i \<le> n} - {j}. f l \<in> A) \<and> f j \<notin> A) \<longrightarrow> \<Sigma>\<^sub>e R f n \<notin> A; \<forall>i\<le>Suc n. f i \<in> carrier R; j \<le> n; \<forall>l\<in>{i. i \<le> Suc n} - {j}. f l \<in> A; f j \<notin> A; \<Sigma>\<^sub>e R f n \<plusminus> f (Suc n) \<in> A\<rbrakk> \<Longrightarrow> f (Suc n) \<in> A
 5. \<And>n j. \<lbrakk>ideal R A; (\<exists>j\<le>n. (\<forall>l\<in>{i. i \<le> n} - {j}. f l \<in> A) \<and> f j \<notin> A) \<longrightarrow> \<Sigma>\<^sub>e R f n \<notin> A; \<forall>i\<le>Suc n. f i \<in> carrier R; j \<le> n; \<forall>l\<in>{i. i \<le> Suc n} - {j}. f l \<in> A; f j \<notin> A; \<Sigma>\<^sub>e R f n \<plusminus> f (Suc n) \<in> A; \<Sigma>\<^sub>e R f n \<in> A\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
apply (cut_tac ring_is_ag,
        rule_tac n = n in aGroup.nsum_mem[of R _ f], assumption+,
        rule allI, simp, simp, assumption+, simp)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>n j. \<lbrakk>ideal R A; (\<exists>j\<le>n. (\<forall>l\<in>{i. i \<le> n} - {j}. f l \<in> A) \<and> f j \<notin> A) \<longrightarrow> \<Sigma>\<^sub>e R f n \<notin> A; \<forall>i\<le>Suc n. f i \<in> carrier R; j \<le> n; \<forall>l\<in>{i. i \<le> Suc n} - {j}. f l \<in> A; f j \<notin> A; \<Sigma>\<^sub>e R f n \<plusminus> f (Suc n) \<in> A; \<Sigma>\<^sub>e R f n \<in> A\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
apply (subgoal_tac "\<exists>j\<le>n. (\<forall>l\<in>{i. i \<le> n} - {j}. f l \<in> A) \<and> f j \<notin> A",
        simp,
        thin_tac "(\<exists>j\<le>n. (\<forall>l\<in>{i. i \<le> n} - {j}. f l \<in> A) \<and> f j \<notin> A)
                     \<longrightarrow> \<Sigma>\<^sub>e R f n \<notin> A")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>n j. \<lbrakk>ideal R A; \<forall>i\<le>Suc n. f i \<in> carrier R; j \<le> n; \<forall>l\<in>{i. i \<le> Suc n} - {j}. f l \<in> A; f j \<notin> A; \<Sigma>\<^sub>e R f n \<plusminus> f (Suc n) \<in> A; \<Sigma>\<^sub>e R f n \<in> A\<rbrakk> \<Longrightarrow> \<exists>j\<le>n. (\<forall>l\<in>{i. i \<le> n} - {j}. f l \<in> A) \<and> f j \<notin> A
[PROOF STEP]
apply (subgoal_tac "\<forall>l\<in>{i. i \<le> n} - {j}. f l \<in> A", blast,
        thin_tac "\<Sigma>\<^sub>e R f n \<plusminus> f (Suc n) \<in> A",
        thin_tac "\<Sigma>\<^sub>e R f n \<in> A")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>n j. \<lbrakk>ideal R A; \<forall>i\<le>Suc n. f i \<in> carrier R; j \<le> n; \<forall>l\<in>{i. i \<le> Suc n} - {j}. f l \<in> A; f j \<notin> A\<rbrakk> \<Longrightarrow> \<forall>l\<in>{i. i \<le> n} - {j}. f l \<in> A
[PROOF STEP]
apply (rule ballI)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>n j l. \<lbrakk>ideal R A; \<forall>i\<le>Suc n. f i \<in> carrier R; j \<le> n; \<forall>l\<in>{i. i \<le> Suc n} - {j}. f l \<in> A; f j \<notin> A; l \<in> {i. i \<le> n} - {j}\<rbrakk> \<Longrightarrow> f l \<in> A
[PROOF STEP]
apply (frule_tac x = l in bspec, simp, assumption)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma (in Ring) nsum_ideal_exc:"\<lbrakk>ideal R A; \<forall>i \<le> n. f i \<in> carrier R;
      \<exists>j \<le> n. (\<forall>l\<in>{i. i \<le> n} -{j}. f l \<in> A) \<and> (f j \<notin> A) \<rbrakk> \<Longrightarrow> nsum R f n \<notin> A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ideal R A; \<forall>i\<le>n. f i \<in> carrier R; \<exists>j\<le>n. (\<forall>l\<in>{i. i \<le> n} - {j}. f l \<in> A) \<and> f j \<notin> A\<rbrakk> \<Longrightarrow> \<Sigma>\<^sub>e R f n \<notin> A
[PROOF STEP]
by (simp add:nsum_ideal_excTr)


[STATEMENT]
lemma (in Ring) nprod_memTr:"(\<forall>i \<le> n. f i \<in> carrier R) \<longrightarrow>
                             (\<forall>l. l \<le> n \<longrightarrow>  nprod R f l \<in> carrier R)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<forall>i\<le>n. f i \<in> carrier R) \<longrightarrow> (\<forall>l\<le>n. e\<Pi>\<^bsub>R,l\<^esub> f \<in> carrier R)
[PROOF STEP]
apply (induct_tac n)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. (\<forall>i\<le>0. f i \<in> carrier R) \<longrightarrow> (\<forall>l\<le>0. e\<Pi>\<^bsub>R,l\<^esub> f \<in> carrier R)
 2. \<And>n. (\<forall>i\<le>n. f i \<in> carrier R) \<longrightarrow> (\<forall>l\<le>n. e\<Pi>\<^bsub>R,l\<^esub> f \<in> carrier R) \<Longrightarrow> (\<forall>i\<le>Suc n. f i \<in> carrier R) \<longrightarrow> (\<forall>l\<le>Suc n. e\<Pi>\<^bsub>R,l\<^esub> f \<in> carrier R)
[PROOF STEP]
apply (rule impI, rule allI, rule impI, simp)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>n. (\<forall>i\<le>n. f i \<in> carrier R) \<longrightarrow> (\<forall>l\<le>n. e\<Pi>\<^bsub>R,l\<^esub> f \<in> carrier R) \<Longrightarrow> (\<forall>i\<le>Suc n. f i \<in> carrier R) \<longrightarrow> (\<forall>l\<le>Suc n. e\<Pi>\<^bsub>R,l\<^esub> f \<in> carrier R)
[PROOF STEP]
apply (rule impI, rule allI, rule impI)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>n l. \<lbrakk>(\<forall>i\<le>n. f i \<in> carrier R) \<longrightarrow> (\<forall>l\<le>n. e\<Pi>\<^bsub>R,l\<^esub> f \<in> carrier R); \<forall>i\<le>Suc n. f i \<in> carrier R; l \<le> Suc n\<rbrakk> \<Longrightarrow> e\<Pi>\<^bsub>R,l\<^esub> f \<in> carrier R
[PROOF STEP]
apply (case_tac "l \<le> n")
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>n l. \<lbrakk>(\<forall>i\<le>n. f i \<in> carrier R) \<longrightarrow> (\<forall>l\<le>n. e\<Pi>\<^bsub>R,l\<^esub> f \<in> carrier R); \<forall>i\<le>Suc n. f i \<in> carrier R; l \<le> Suc n; l \<le> n\<rbrakk> \<Longrightarrow> e\<Pi>\<^bsub>R,l\<^esub> f \<in> carrier R
 2. \<And>n l. \<lbrakk>(\<forall>i\<le>n. f i \<in> carrier R) \<longrightarrow> (\<forall>l\<le>n. e\<Pi>\<^bsub>R,l\<^esub> f \<in> carrier R); \<forall>i\<le>Suc n. f i \<in> carrier R; l \<le> Suc n; \<not> l \<le> n\<rbrakk> \<Longrightarrow> e\<Pi>\<^bsub>R,l\<^esub> f \<in> carrier R
[PROOF STEP]
apply (cut_tac n = n in Nset_Suc, blast)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>n l. \<lbrakk>(\<forall>i\<le>n. f i \<in> carrier R) \<longrightarrow> (\<forall>l\<le>n. e\<Pi>\<^bsub>R,l\<^esub> f \<in> carrier R); \<forall>i\<le>Suc n. f i \<in> carrier R; l \<le> Suc n; \<not> l \<le> n\<rbrakk> \<Longrightarrow> e\<Pi>\<^bsub>R,l\<^esub> f \<in> carrier R
[PROOF STEP]
apply (cut_tac m = l and n = "Suc n" in Nat.le_antisym, assumption)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>n l. \<lbrakk>(\<forall>i\<le>n. f i \<in> carrier R) \<longrightarrow> (\<forall>l\<le>n. e\<Pi>\<^bsub>R,l\<^esub> f \<in> carrier R); \<forall>i\<le>Suc n. f i \<in> carrier R; l \<le> Suc n; \<not> l \<le> n\<rbrakk> \<Longrightarrow> Suc n \<le> l
 2. \<And>n l. \<lbrakk>(\<forall>i\<le>n. f i \<in> carrier R) \<longrightarrow> (\<forall>l\<le>n. e\<Pi>\<^bsub>R,l\<^esub> f \<in> carrier R); \<forall>i\<le>Suc n. f i \<in> carrier R; l \<le> Suc n; \<not> l \<le> n; l = Suc n\<rbrakk> \<Longrightarrow> e\<Pi>\<^bsub>R,l\<^esub> f \<in> carrier R
[PROOF STEP]
apply (simp add: not_less)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>n l. \<lbrakk>(\<forall>i\<le>n. f i \<in> carrier R) \<longrightarrow> (\<forall>l\<le>n. e\<Pi>\<^bsub>R,l\<^esub> f \<in> carrier R); \<forall>i\<le>Suc n. f i \<in> carrier R; l \<le> Suc n; \<not> l \<le> n; l = Suc n\<rbrakk> \<Longrightarrow> e\<Pi>\<^bsub>R,l\<^esub> f \<in> carrier R
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>n l. \<lbrakk>\<forall>l\<le>n. e\<Pi>\<^bsub>R,l\<^esub> f \<in> carrier R; \<forall>i\<le>Suc n. f i \<in> carrier R; l = Suc n\<rbrakk> \<Longrightarrow> e\<Pi>\<^bsub>R,n\<^esub> f \<cdot>\<^sub>r f (Suc n) \<in> carrier R
[PROOF STEP]
apply (rule ring_tOp_closed, simp)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>n l. \<lbrakk>\<forall>l\<le>n. e\<Pi>\<^bsub>R,l\<^esub> f \<in> carrier R; \<forall>i\<le>Suc n. f i \<in> carrier R; l = Suc n\<rbrakk> \<Longrightarrow> f (Suc n) \<in> carrier R
[PROOF STEP]
apply (cut_tac n = n in Nset_Suc, blast)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done