[STATEMENT]
lemma (in Ring) mulDisj:"\<lbrakk>mul_closed_set R S; 1\<^sub>r \<in> S; \<zero> \<notin> S;
    T = {I. ideal R I \<and> S \<inter> I = {}}; maximal_set T mx \<rbrakk> \<Longrightarrow> prime_ideal R mx"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>mul_closed_set R S; 1\<^sub>r \<in> S; \<zero> \<notin> S; T = {I. ideal R I \<and> S \<inter> I = {}}; maximal_set T mx\<rbrakk> \<Longrightarrow> prime_ideal R mx
[PROOF STEP]
apply (simp add:prime_ideal_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>mul_closed_set R S; 1\<^sub>r \<in> S; \<zero> \<notin> S; T = {I. ideal R I \<and> S \<inter> I = {}}; maximal_set {I. ideal R I \<and> S \<inter> I = {}} mx\<rbrakk> \<Longrightarrow> ideal R mx \<and> 1\<^sub>r \<notin> mx \<and> (\<forall>x\<in>carrier R. \<forall>y\<in>carrier R. x \<cdot>\<^sub>r y \<in> mx \<longrightarrow> x \<in> mx \<or> y \<in> mx)
[PROOF STEP]
apply (rule conjI, simp add:maximal_set_def,
       rule conjI, simp add:maximal_set_def)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>mul_closed_set R S; 1\<^sub>r \<in> S; \<zero> \<notin> S; T = {I. ideal R I \<and> S \<inter> I = {}}; ideal R mx \<and> S \<inter> mx = {} \<and> (\<forall>s. ideal R s \<and> S \<inter> s = {} \<longrightarrow> mx \<subseteq> s \<longrightarrow> s = mx)\<rbrakk> \<Longrightarrow> 1\<^sub>r \<notin> mx
 2. \<lbrakk>mul_closed_set R S; 1\<^sub>r \<in> S; \<zero> \<notin> S; T = {I. ideal R I \<and> S \<inter> I = {}}; maximal_set {I. ideal R I \<and> S \<inter> I = {}} mx\<rbrakk> \<Longrightarrow> \<forall>x\<in>carrier R. \<forall>y\<in>carrier R. x \<cdot>\<^sub>r y \<in> mx \<longrightarrow> x \<in> mx \<or> y \<in> mx
[PROOF STEP]
apply (rule contrapos_pp, simp+)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>mul_closed_set R S; 1\<^sub>r \<in> S; \<zero> \<notin> S; T = {I. ideal R I \<and> S \<inter> I = {}}; ideal R mx \<and> S \<inter> mx = {} \<and> (\<forall>s. ideal R s \<and> S \<inter> s = {} \<longrightarrow> mx \<subseteq> s \<longrightarrow> s = mx); 1\<^sub>r \<in> mx\<rbrakk> \<Longrightarrow> False
 2. \<lbrakk>mul_closed_set R S; 1\<^sub>r \<in> S; \<zero> \<notin> S; T = {I. ideal R I \<and> S \<inter> I = {}}; maximal_set {I. ideal R I \<and> S \<inter> I = {}} mx\<rbrakk> \<Longrightarrow> \<forall>x\<in>carrier R. \<forall>y\<in>carrier R. x \<cdot>\<^sub>r y \<in> mx \<longrightarrow> x \<in> mx \<or> y \<in> mx
[PROOF STEP]
apply ((erule conjE)+, blast)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>mul_closed_set R S; 1\<^sub>r \<in> S; \<zero> \<notin> S; T = {I. ideal R I \<and> S \<inter> I = {}}; maximal_set {I. ideal R I \<and> S \<inter> I = {}} mx\<rbrakk> \<Longrightarrow> \<forall>x\<in>carrier R. \<forall>y\<in>carrier R. x \<cdot>\<^sub>r y \<in> mx \<longrightarrow> x \<in> mx \<or> y \<in> mx
[PROOF STEP]
apply ((rule ballI)+, rule impI)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x y. \<lbrakk>mul_closed_set R S; 1\<^sub>r \<in> S; \<zero> \<notin> S; T = {I. ideal R I \<and> S \<inter> I = {}}; maximal_set {I. ideal R I \<and> S \<inter> I = {}} mx; x \<in> carrier R; y \<in> carrier R; x \<cdot>\<^sub>r y \<in> mx\<rbrakk> \<Longrightarrow> x \<in> mx \<or> y \<in> mx
[PROOF STEP]
apply (rule contrapos_pp, simp+, (erule conjE)+)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x y. \<lbrakk>mul_closed_set R S; 1\<^sub>r \<in> S; \<zero> \<notin> S; T = {I. ideal R I \<and> S \<inter> I = {}}; maximal_set {I. ideal R I \<and> S \<inter> I = {}} mx; x \<in> carrier R; y \<in> carrier R; x \<cdot>\<^sub>r y \<in> mx; x \<notin> mx; y \<notin> mx\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
apply (cut_tac a = x in id_ideal_psub_sum[of "mx"],
               simp add:maximal_set_def, assumption+,
       cut_tac a = y in id_ideal_psub_sum[of "mx"],
               simp add:maximal_set_def, assumption+)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x y. \<lbrakk>mul_closed_set R S; 1\<^sub>r \<in> S; \<zero> \<notin> S; T = {I. ideal R I \<and> S \<inter> I = {}}; maximal_set {I. ideal R I \<and> S \<inter> I = {}} mx; x \<in> carrier R; y \<in> carrier R; x \<cdot>\<^sub>r y \<in> mx; x \<notin> mx; y \<notin> mx; mx \<subset> mx \<minusplus> R \<diamondsuit>\<^sub>p x; mx \<subset> mx \<minusplus> R \<diamondsuit>\<^sub>p y\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
apply (frule_tac J = "mx \<minusplus> R \<diamondsuit>\<^sub>p x" in maximal_setTr[of "S" "mx"],
       rule sum_ideals, simp add:maximal_set_def,
       simp add:principal_ideal, assumption,
       thin_tac "mx \<subset> mx \<minusplus> R \<diamondsuit>\<^sub>p x")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x y. \<lbrakk>mul_closed_set R S; 1\<^sub>r \<in> S; \<zero> \<notin> S; T = {I. ideal R I \<and> S \<inter> I = {}}; maximal_set {I. ideal R I \<and> S \<inter> I = {}} mx; x \<in> carrier R; y \<in> carrier R; x \<cdot>\<^sub>r y \<in> mx; x \<notin> mx; y \<notin> mx; mx \<subset> mx \<minusplus> R \<diamondsuit>\<^sub>p y; S \<inter> (mx \<minusplus> R \<diamondsuit>\<^sub>p x) \<noteq> {}\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
apply (frule_tac J = "mx \<minusplus> R \<diamondsuit>\<^sub>p y" in maximal_setTr[of "S" "mx"],
       rule sum_ideals, simp add:maximal_set_def,
       simp add:principal_ideal, assumption,
       thin_tac "mx \<subset> mx \<minusplus> R \<diamondsuit>\<^sub>p y")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x y. \<lbrakk>mul_closed_set R S; 1\<^sub>r \<in> S; \<zero> \<notin> S; T = {I. ideal R I \<and> S \<inter> I = {}}; maximal_set {I. ideal R I \<and> S \<inter> I = {}} mx; x \<in> carrier R; y \<in> carrier R; x \<cdot>\<^sub>r y \<in> mx; x \<notin> mx; y \<notin> mx; S \<inter> (mx \<minusplus> R \<diamondsuit>\<^sub>p x) \<noteq> {}; S \<inter> (mx \<minusplus> R \<diamondsuit>\<^sub>p y) \<noteq> {}\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
apply (frule_tac A = "S \<inter> (mx \<minusplus> R \<diamondsuit>\<^sub>p x)" in nonempty_ex,
       frule_tac A = "S \<inter> (mx \<minusplus> R \<diamondsuit>\<^sub>p y)" in nonempty_ex,
       (erule exE)+, simp, (erule conjE)+)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x y xa xb. \<lbrakk>mul_closed_set R S; 1\<^sub>r \<in> S; \<zero> \<notin> S; T = {I. ideal R I \<and> S \<inter> I = {}}; maximal_set {I. ideal R I \<and> S \<inter> I = {}} mx; x \<in> carrier R; y \<in> carrier R; x \<cdot>\<^sub>r y \<in> mx; x \<notin> mx; y \<notin> mx; S \<inter> (mx \<minusplus> R \<diamondsuit>\<^sub>p x) \<noteq> {}; S \<inter> (mx \<minusplus> R \<diamondsuit>\<^sub>p y) \<noteq> {}; xa \<in> S; xa \<in> mx \<minusplus> R \<diamondsuit>\<^sub>p x; xb \<in> S; xb \<in> mx \<minusplus> R \<diamondsuit>\<^sub>p y\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
apply (rename_tac x y s1 s2,
       thin_tac "S \<inter> (mx \<minusplus> R \<diamondsuit>\<^sub>p x) \<noteq> {}",
       thin_tac "S \<inter> (mx \<minusplus> R \<diamondsuit>\<^sub>p y) \<noteq> {}")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x y s1 s2. \<lbrakk>mul_closed_set R S; 1\<^sub>r \<in> S; \<zero> \<notin> S; T = {I. ideal R I \<and> S \<inter> I = {}}; maximal_set {I. ideal R I \<and> S \<inter> I = {}} mx; x \<in> carrier R; y \<in> carrier R; x \<cdot>\<^sub>r y \<in> mx; x \<notin> mx; y \<notin> mx; s1 \<in> S; s1 \<in> mx \<minusplus> R \<diamondsuit>\<^sub>p x; s2 \<in> S; s2 \<in> mx \<minusplus> R \<diamondsuit>\<^sub>p y\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
apply (frule maximal_set_idealTr,
       frule_tac a = x in principal_ideal,
       frule_tac a = y in principal_ideal,
       frule ideal_subset1[of mx],
       frule_tac I = "R \<diamondsuit>\<^sub>p x" in ideal_subset1,
       frule_tac I = "R \<diamondsuit>\<^sub>p y" in ideal_subset1)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x y s1 s2. \<lbrakk>mul_closed_set R S; 1\<^sub>r \<in> S; \<zero> \<notin> S; T = {I. ideal R I \<and> S \<inter> I = {}}; maximal_set {I. ideal R I \<and> S \<inter> I = {}} mx; x \<in> carrier R; y \<in> carrier R; x \<cdot>\<^sub>r y \<in> mx; x \<notin> mx; y \<notin> mx; s1 \<in> S; s1 \<in> mx \<minusplus> R \<diamondsuit>\<^sub>p x; s2 \<in> S; s2 \<in> mx \<minusplus> R \<diamondsuit>\<^sub>p y; ideal R mx; ideal R (R \<diamondsuit>\<^sub>p x); ideal R (R \<diamondsuit>\<^sub>p y); mx \<subseteq> carrier R; R \<diamondsuit>\<^sub>p x \<subseteq> carrier R; R \<diamondsuit>\<^sub>p y \<subseteq> carrier R\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
apply (cut_tac ring_is_ag,
       simp add:aGroup.set_sum[of R mx],
       erule bexE, erule bexE, simp)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x y s1 s2 h k. \<lbrakk>mul_closed_set R S; 1\<^sub>r \<in> S; \<zero> \<notin> S; T = {I. ideal R I \<and> S \<inter> I = {}}; maximal_set {I. ideal R I \<and> S \<inter> I = {}} mx; x \<in> carrier R; y \<in> carrier R; x \<cdot>\<^sub>r y \<in> mx; x \<notin> mx; y \<notin> mx; h \<plusminus> k \<in> S; s2 \<in> S; \<exists>h\<in>mx. \<exists>k\<in>R \<diamondsuit>\<^sub>p y. s2 = h \<plusminus> k; ideal R mx; ideal R (R \<diamondsuit>\<^sub>p x); ideal R (R \<diamondsuit>\<^sub>p y); mx \<subseteq> carrier R; R \<diamondsuit>\<^sub>p x \<subseteq> carrier R; R \<diamondsuit>\<^sub>p y \<subseteq> carrier R; aGroup R; h \<in> mx; k \<in> R \<diamondsuit>\<^sub>p x; s1 = h \<plusminus> k\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
apply (frule_tac s = s1 and t = s2 in mul_closed_set_tOp_closed, simp,
       assumption, simp,
       frule_tac c = h in subsetD[of mx "carrier R"], assumption+,
       frule_tac c = k and A = "R \<diamondsuit>\<^sub>p x" in subsetD[of _ "carrier R"],
       assumption+)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x y s1 s2 h k. \<lbrakk>mul_closed_set R S; 1\<^sub>r \<in> S; \<zero> \<notin> S; T = {I. ideal R I \<and> S \<inter> I = {}}; maximal_set {I. ideal R I \<and> S \<inter> I = {}} mx; x \<in> carrier R; y \<in> carrier R; x \<cdot>\<^sub>r y \<in> mx; x \<notin> mx; y \<notin> mx; h \<plusminus> k \<in> S; s2 \<in> S; \<exists>h\<in>mx. \<exists>k\<in>R \<diamondsuit>\<^sub>p y. s2 = h \<plusminus> k; ideal R mx; ideal R (R \<diamondsuit>\<^sub>p x); ideal R (R \<diamondsuit>\<^sub>p y); mx \<subseteq> carrier R; R \<diamondsuit>\<^sub>p x \<subseteq> carrier R; R \<diamondsuit>\<^sub>p y \<subseteq> carrier R; aGroup R; h \<in> mx; k \<in> R \<diamondsuit>\<^sub>p x; s1 = h \<plusminus> k; (h \<plusminus> k) \<cdot>\<^sub>r s2 \<in> S; h \<in> carrier R; k \<in> carrier R\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
apply (
       cut_tac mul_closed_set_sub,
       frule_tac c = s2 in subsetD[of S "carrier R"], assumption+,
       simp add:ring_distrib2)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x y s1 s2 h k. \<lbrakk>mul_closed_set R S; 1\<^sub>r \<in> S; \<zero> \<notin> S; T = {I. ideal R I \<and> S \<inter> I = {}}; maximal_set {I. ideal R I \<and> S \<inter> I = {}} mx; x \<in> carrier R; y \<in> carrier R; x \<cdot>\<^sub>r y \<in> mx; x \<notin> mx; y \<notin> mx; h \<plusminus> k \<in> S; s2 \<in> S; \<exists>h\<in>mx. \<exists>k\<in>R \<diamondsuit>\<^sub>p y. s2 = h \<plusminus> k; ideal R mx; ideal R (R \<diamondsuit>\<^sub>p x); ideal R (R \<diamondsuit>\<^sub>p y); mx \<subseteq> carrier R; R \<diamondsuit>\<^sub>p x \<subseteq> carrier R; R \<diamondsuit>\<^sub>p y \<subseteq> carrier R; aGroup R; h \<in> mx; k \<in> R \<diamondsuit>\<^sub>p x; s1 = h \<plusminus> k; h \<cdot>\<^sub>r s2 \<plusminus> k \<cdot>\<^sub>r s2 \<in> S; h \<in> carrier R; k \<in> carrier R; S \<subseteq> carrier R; s2 \<in> carrier R\<rbrakk> \<Longrightarrow> False
 2. \<And>x y s1 s2 h k. \<lbrakk>mul_closed_set R S; 1\<^sub>r \<in> S; \<zero> \<notin> S; T = {I. ideal R I \<and> S \<inter> I = {}}; maximal_set {I. ideal R I \<and> S \<inter> I = {}} mx; x \<in> carrier R; y \<in> carrier R; x \<cdot>\<^sub>r y \<in> mx; x \<notin> mx; y \<notin> mx; h \<plusminus> k \<in> S; s2 \<in> S; \<exists>h\<in>mx. \<exists>k\<in>R \<diamondsuit>\<^sub>p y. s2 = h \<plusminus> k; ideal R mx; ideal R (R \<diamondsuit>\<^sub>p x); ideal R (R \<diamondsuit>\<^sub>p y); mx \<subseteq> carrier R; R \<diamondsuit>\<^sub>p x \<subseteq> carrier R; R \<diamondsuit>\<^sub>p y \<subseteq> carrier R; aGroup R; h \<in> mx; k \<in> R \<diamondsuit>\<^sub>p x; s1 = h \<plusminus> k; (h \<plusminus> k) \<cdot>\<^sub>r s2 \<in> S; h \<in> carrier R; k \<in> carrier R\<rbrakk> \<Longrightarrow> mul_closed_set R S
[PROOF STEP]
apply ((erule bexE)+, simp,
       frule_tac c = ha in subsetD[of mx "carrier R"], assumption+,
       frule_tac c = ka and A = "R \<diamondsuit>\<^sub>p y" in subsetD[of _ "carrier R"],
       assumption+,
       simp add:ring_distrib1)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x y s1 s2 h k ha ka. \<lbrakk>mul_closed_set R S; 1\<^sub>r \<in> S; \<zero> \<notin> S; T = {I. ideal R I \<and> S \<inter> I = {}}; maximal_set {I. ideal R I \<and> S \<inter> I = {}} mx; x \<in> carrier R; y \<in> carrier R; x \<cdot>\<^sub>r y \<in> mx; x \<notin> mx; y \<notin> mx; h \<plusminus> k \<in> S; ha \<plusminus> ka \<in> S; ideal R mx; ideal R (R \<diamondsuit>\<^sub>p x); ideal R (R \<diamondsuit>\<^sub>p y); mx \<subseteq> carrier R; R \<diamondsuit>\<^sub>p x \<subseteq> carrier R; R \<diamondsuit>\<^sub>p y \<subseteq> carrier R; aGroup R; h \<in> mx; k \<in> R \<diamondsuit>\<^sub>p x; s1 = h \<plusminus> k; h \<cdot>\<^sub>r ha \<plusminus> h \<cdot>\<^sub>r ka \<plusminus> (k \<cdot>\<^sub>r ha \<plusminus> k \<cdot>\<^sub>r ka) \<in> S; h \<in> carrier R; k \<in> carrier R; S \<subseteq> carrier R; ha \<plusminus> ka \<in> carrier R; ha \<in> mx; ka \<in> R \<diamondsuit>\<^sub>p y; s2 = ha \<plusminus> ka; ha \<in> carrier R; ka \<in> carrier R\<rbrakk> \<Longrightarrow> False
 2. \<And>x y s1 s2 h k. \<lbrakk>mul_closed_set R S; 1\<^sub>r \<in> S; \<zero> \<notin> S; T = {I. ideal R I \<and> S \<inter> I = {}}; maximal_set {I. ideal R I \<and> S \<inter> I = {}} mx; x \<in> carrier R; y \<in> carrier R; x \<cdot>\<^sub>r y \<in> mx; x \<notin> mx; y \<notin> mx; h \<plusminus> k \<in> S; s2 \<in> S; \<exists>h\<in>mx. \<exists>k\<in>R \<diamondsuit>\<^sub>p y. s2 = h \<plusminus> k; ideal R mx; ideal R (R \<diamondsuit>\<^sub>p x); ideal R (R \<diamondsuit>\<^sub>p y); mx \<subseteq> carrier R; R \<diamondsuit>\<^sub>p x \<subseteq> carrier R; R \<diamondsuit>\<^sub>p y \<subseteq> carrier R; aGroup R; h \<in> mx; k \<in> R \<diamondsuit>\<^sub>p x; s1 = h \<plusminus> k; (h \<plusminus> k) \<cdot>\<^sub>r s2 \<in> S; h \<in> carrier R; k \<in> carrier R\<rbrakk> \<Longrightarrow> mul_closed_set R S
[PROOF STEP]
apply (frule_tac x = h and r = ha in ideal_ring_multiple1[of mx], assumption+)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x y s1 s2 h k ha ka. \<lbrakk>mul_closed_set R S; 1\<^sub>r \<in> S; \<zero> \<notin> S; T = {I. ideal R I \<and> S \<inter> I = {}}; maximal_set {I. ideal R I \<and> S \<inter> I = {}} mx; x \<in> carrier R; y \<in> carrier R; x \<cdot>\<^sub>r y \<in> mx; x \<notin> mx; y \<notin> mx; h \<plusminus> k \<in> S; ha \<plusminus> ka \<in> S; ideal R mx; ideal R (R \<diamondsuit>\<^sub>p x); ideal R (R \<diamondsuit>\<^sub>p y); mx \<subseteq> carrier R; R \<diamondsuit>\<^sub>p x \<subseteq> carrier R; R \<diamondsuit>\<^sub>p y \<subseteq> carrier R; aGroup R; h \<in> mx; k \<in> R \<diamondsuit>\<^sub>p x; s1 = h \<plusminus> k; h \<cdot>\<^sub>r ha \<plusminus> h \<cdot>\<^sub>r ka \<plusminus> (k \<cdot>\<^sub>r ha \<plusminus> k \<cdot>\<^sub>r ka) \<in> S; h \<in> carrier R; k \<in> carrier R; S \<subseteq> carrier R; ha \<plusminus> ka \<in> carrier R; ha \<in> mx; ka \<in> R \<diamondsuit>\<^sub>p y; s2 = ha \<plusminus> ka; ha \<in> carrier R; ka \<in> carrier R; h \<cdot>\<^sub>r ha \<in> mx\<rbrakk> \<Longrightarrow> False
 2. \<And>x y s1 s2 h k. \<lbrakk>mul_closed_set R S; 1\<^sub>r \<in> S; \<zero> \<notin> S; T = {I. ideal R I \<and> S \<inter> I = {}}; maximal_set {I. ideal R I \<and> S \<inter> I = {}} mx; x \<in> carrier R; y \<in> carrier R; x \<cdot>\<^sub>r y \<in> mx; x \<notin> mx; y \<notin> mx; h \<plusminus> k \<in> S; s2 \<in> S; \<exists>h\<in>mx. \<exists>k\<in>R \<diamondsuit>\<^sub>p y. s2 = h \<plusminus> k; ideal R mx; ideal R (R \<diamondsuit>\<^sub>p x); ideal R (R \<diamondsuit>\<^sub>p y); mx \<subseteq> carrier R; R \<diamondsuit>\<^sub>p x \<subseteq> carrier R; R \<diamondsuit>\<^sub>p y \<subseteq> carrier R; aGroup R; h \<in> mx; k \<in> R \<diamondsuit>\<^sub>p x; s1 = h \<plusminus> k; (h \<plusminus> k) \<cdot>\<^sub>r s2 \<in> S; h \<in> carrier R; k \<in> carrier R\<rbrakk> \<Longrightarrow> mul_closed_set R S
[PROOF STEP]
apply (frule_tac x = h and r = ka in ideal_ring_multiple1[of mx], assumption+,
       frule_tac x = ha and r = k in ideal_ring_multiple[of mx], assumption+)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x y s1 s2 h k ha ka. \<lbrakk>mul_closed_set R S; 1\<^sub>r \<in> S; \<zero> \<notin> S; T = {I. ideal R I \<and> S \<inter> I = {}}; maximal_set {I. ideal R I \<and> S \<inter> I = {}} mx; x \<in> carrier R; y \<in> carrier R; x \<cdot>\<^sub>r y \<in> mx; x \<notin> mx; y \<notin> mx; h \<plusminus> k \<in> S; ha \<plusminus> ka \<in> S; ideal R mx; ideal R (R \<diamondsuit>\<^sub>p x); ideal R (R \<diamondsuit>\<^sub>p y); mx \<subseteq> carrier R; R \<diamondsuit>\<^sub>p x \<subseteq> carrier R; R \<diamondsuit>\<^sub>p y \<subseteq> carrier R; aGroup R; h \<in> mx; k \<in> R \<diamondsuit>\<^sub>p x; s1 = h \<plusminus> k; h \<cdot>\<^sub>r ha \<plusminus> h \<cdot>\<^sub>r ka \<plusminus> (k \<cdot>\<^sub>r ha \<plusminus> k \<cdot>\<^sub>r ka) \<in> S; h \<in> carrier R; k \<in> carrier R; S \<subseteq> carrier R; ha \<plusminus> ka \<in> carrier R; ha \<in> mx; ka \<in> R \<diamondsuit>\<^sub>p y; s2 = ha \<plusminus> ka; ha \<in> carrier R; ka \<in> carrier R; h \<cdot>\<^sub>r ha \<in> mx; h \<cdot>\<^sub>r ka \<in> mx; k \<cdot>\<^sub>r ha \<in> mx\<rbrakk> \<Longrightarrow> False
 2. \<And>x y s1 s2 h k. \<lbrakk>mul_closed_set R S; 1\<^sub>r \<in> S; \<zero> \<notin> S; T = {I. ideal R I \<and> S \<inter> I = {}}; maximal_set {I. ideal R I \<and> S \<inter> I = {}} mx; x \<in> carrier R; y \<in> carrier R; x \<cdot>\<^sub>r y \<in> mx; x \<notin> mx; y \<notin> mx; h \<plusminus> k \<in> S; s2 \<in> S; \<exists>h\<in>mx. \<exists>k\<in>R \<diamondsuit>\<^sub>p y. s2 = h \<plusminus> k; ideal R mx; ideal R (R \<diamondsuit>\<^sub>p x); ideal R (R \<diamondsuit>\<^sub>p y); mx \<subseteq> carrier R; R \<diamondsuit>\<^sub>p x \<subseteq> carrier R; R \<diamondsuit>\<^sub>p y \<subseteq> carrier R; aGroup R; h \<in> mx; k \<in> R \<diamondsuit>\<^sub>p x; s1 = h \<plusminus> k; (h \<plusminus> k) \<cdot>\<^sub>r s2 \<in> S; h \<in> carrier R; k \<in> carrier R\<rbrakk> \<Longrightarrow> mul_closed_set R S
[PROOF STEP]
apply (frule_tac a = x and b = y and x = k and y = ka in
                  mul_two_principal_idealsTr, assumption+,
       erule bexE,
       frule_tac x = "x \<cdot>\<^sub>r y" and r = r in ideal_ring_multiple[of mx],
       assumption+,
       rotate_tac -2, frule sym, thin_tac "k \<cdot>\<^sub>r ka = r \<cdot>\<^sub>r (x \<cdot>\<^sub>r y)", simp)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x y s1 s2 h k ha ka r. \<lbrakk>k \<cdot>\<^sub>r ka \<in> mx; mul_closed_set R S; 1\<^sub>r \<in> S; \<zero> \<notin> S; T = {I. ideal R I \<and> S \<inter> I = {}}; maximal_set {I. ideal R I \<and> S \<inter> I = {}} mx; x \<in> carrier R; y \<in> carrier R; x \<cdot>\<^sub>r y \<in> mx; x \<notin> mx; y \<notin> mx; h \<plusminus> k \<in> S; ha \<plusminus> ka \<in> S; ideal R mx; ideal R (R \<diamondsuit>\<^sub>p x); ideal R (R \<diamondsuit>\<^sub>p y); mx \<subseteq> carrier R; R \<diamondsuit>\<^sub>p x \<subseteq> carrier R; R \<diamondsuit>\<^sub>p y \<subseteq> carrier R; aGroup R; h \<in> mx; k \<in> R \<diamondsuit>\<^sub>p x; s1 = h \<plusminus> k; h \<cdot>\<^sub>r ha \<plusminus> h \<cdot>\<^sub>r ka \<plusminus> (k \<cdot>\<^sub>r ha \<plusminus> k \<cdot>\<^sub>r ka) \<in> S; h \<in> carrier R; k \<in> carrier R; S \<subseteq> carrier R; ha \<plusminus> ka \<in> carrier R; ha \<in> mx; ka \<in> R \<diamondsuit>\<^sub>p y; s2 = ha \<plusminus> ka; ha \<in> carrier R; ka \<in> carrier R; h \<cdot>\<^sub>r ha \<in> mx; h \<cdot>\<^sub>r ka \<in> mx; k \<cdot>\<^sub>r ha \<in> mx; r \<in> carrier R; r \<cdot>\<^sub>r (x \<cdot>\<^sub>r y) = k \<cdot>\<^sub>r ka\<rbrakk> \<Longrightarrow> False
 2. \<And>x y s1 s2 h k. \<lbrakk>mul_closed_set R S; 1\<^sub>r \<in> S; \<zero> \<notin> S; T = {I. ideal R I \<and> S \<inter> I = {}}; maximal_set {I. ideal R I \<and> S \<inter> I = {}} mx; x \<in> carrier R; y \<in> carrier R; x \<cdot>\<^sub>r y \<in> mx; x \<notin> mx; y \<notin> mx; h \<plusminus> k \<in> S; s2 \<in> S; \<exists>h\<in>mx. \<exists>k\<in>R \<diamondsuit>\<^sub>p y. s2 = h \<plusminus> k; ideal R mx; ideal R (R \<diamondsuit>\<^sub>p x); ideal R (R \<diamondsuit>\<^sub>p y); mx \<subseteq> carrier R; R \<diamondsuit>\<^sub>p x \<subseteq> carrier R; R \<diamondsuit>\<^sub>p y \<subseteq> carrier R; aGroup R; h \<in> mx; k \<in> R \<diamondsuit>\<^sub>p x; s1 = h \<plusminus> k; (h \<plusminus> k) \<cdot>\<^sub>r s2 \<in> S; h \<in> carrier R; k \<in> carrier R\<rbrakk> \<Longrightarrow> mul_closed_set R S
[PROOF STEP]
apply (frule_tac x = "h \<cdot>\<^sub>r ha \<plusminus> h \<cdot>\<^sub>r ka" and y = "k \<cdot>\<^sub>r ha \<plusminus> k \<cdot>\<^sub>r ka" in
        ideal_pOp_closed[of mx])
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<And>x y s1 s2 h k ha ka r. \<lbrakk>k \<cdot>\<^sub>r ka \<in> mx; mul_closed_set R S; 1\<^sub>r \<in> S; \<zero> \<notin> S; T = {I. ideal R I \<and> S \<inter> I = {}}; maximal_set {I. ideal R I \<and> S \<inter> I = {}} mx; x \<in> carrier R; y \<in> carrier R; x \<cdot>\<^sub>r y \<in> mx; x \<notin> mx; y \<notin> mx; h \<plusminus> k \<in> S; ha \<plusminus> ka \<in> S; ideal R mx; ideal R (R \<diamondsuit>\<^sub>p x); ideal R (R \<diamondsuit>\<^sub>p y); mx \<subseteq> carrier R; R \<diamondsuit>\<^sub>p x \<subseteq> carrier R; R \<diamondsuit>\<^sub>p y \<subseteq> carrier R; aGroup R; h \<in> mx; k \<in> R \<diamondsuit>\<^sub>p x; s1 = h \<plusminus> k; h \<cdot>\<^sub>r ha \<plusminus> h \<cdot>\<^sub>r ka \<plusminus> (k \<cdot>\<^sub>r ha \<plusminus> k \<cdot>\<^sub>r ka) \<in> S; h \<in> carrier R; k \<in> carrier R; S \<subseteq> carrier R; ha \<plusminus> ka \<in> carrier R; ha \<in> mx; ka \<in> R \<diamondsuit>\<^sub>p y; s2 = ha \<plusminus> ka; ha \<in> carrier R; ka \<in> carrier R; h \<cdot>\<^sub>r ha \<in> mx; h \<cdot>\<^sub>r ka \<in> mx; k \<cdot>\<^sub>r ha \<in> mx; r \<in> carrier R; r \<cdot>\<^sub>r (x \<cdot>\<^sub>r y) = k \<cdot>\<^sub>r ka\<rbrakk> \<Longrightarrow> h \<cdot>\<^sub>r ha \<plusminus> h \<cdot>\<^sub>r ka \<in> mx
 2. \<And>x y s1 s2 h k ha ka r. \<lbrakk>k \<cdot>\<^sub>r ka \<in> mx; mul_closed_set R S; 1\<^sub>r \<in> S; \<zero> \<notin> S; T = {I. ideal R I \<and> S \<inter> I = {}}; maximal_set {I. ideal R I \<and> S \<inter> I = {}} mx; x \<in> carrier R; y \<in> carrier R; x \<cdot>\<^sub>r y \<in> mx; x \<notin> mx; y \<notin> mx; h \<plusminus> k \<in> S; ha \<plusminus> ka \<in> S; ideal R mx; ideal R (R \<diamondsuit>\<^sub>p x); ideal R (R \<diamondsuit>\<^sub>p y); mx \<subseteq> carrier R; R \<diamondsuit>\<^sub>p x \<subseteq> carrier R; R \<diamondsuit>\<^sub>p y \<subseteq> carrier R; aGroup R; h \<in> mx; k \<in> R \<diamondsuit>\<^sub>p x; s1 = h \<plusminus> k; h \<cdot>\<^sub>r ha \<plusminus> h \<cdot>\<^sub>r ka \<plusminus> (k \<cdot>\<^sub>r ha \<plusminus> k \<cdot>\<^sub>r ka) \<in> S; h \<in> carrier R; k \<in> carrier R; S \<subseteq> carrier R; ha \<plusminus> ka \<in> carrier R; ha \<in> mx; ka \<in> R \<diamondsuit>\<^sub>p y; s2 = ha \<plusminus> ka; ha \<in> carrier R; ka \<in> carrier R; h \<cdot>\<^sub>r ha \<in> mx; h \<cdot>\<^sub>r ka \<in> mx; k \<cdot>\<^sub>r ha \<in> mx; r \<in> carrier R; r \<cdot>\<^sub>r (x \<cdot>\<^sub>r y) = k \<cdot>\<^sub>r ka\<rbrakk> \<Longrightarrow> k \<cdot>\<^sub>r ha \<plusminus> k \<cdot>\<^sub>r ka \<in> mx
 3. \<And>x y s1 s2 h k ha ka r. \<lbrakk>k \<cdot>\<^sub>r ka \<in> mx; mul_closed_set R S; 1\<^sub>r \<in> S; \<zero> \<notin> S; T = {I. ideal R I \<and> S \<inter> I = {}}; maximal_set {I. ideal R I \<and> S \<inter> I = {}} mx; x \<in> carrier R; y \<in> carrier R; x \<cdot>\<^sub>r y \<in> mx; x \<notin> mx; y \<notin> mx; h \<plusminus> k \<in> S; ha \<plusminus> ka \<in> S; ideal R mx; ideal R (R \<diamondsuit>\<^sub>p x); ideal R (R \<diamondsuit>\<^sub>p y); mx \<subseteq> carrier R; R \<diamondsuit>\<^sub>p x \<subseteq> carrier R; R \<diamondsuit>\<^sub>p y \<subseteq> carrier R; aGroup R; h \<in> mx; k \<in> R \<diamondsuit>\<^sub>p x; s1 = h \<plusminus> k; h \<cdot>\<^sub>r ha \<plusminus> h \<cdot>\<^sub>r ka \<plusminus> (k \<cdot>\<^sub>r ha \<plusminus> k \<cdot>\<^sub>r ka) \<in> S; h \<in> carrier R; k \<in> carrier R; S \<subseteq> carrier R; ha \<plusminus> ka \<in> carrier R; ha \<in> mx; ka \<in> R \<diamondsuit>\<^sub>p y; s2 = ha \<plusminus> ka; ha \<in> carrier R; ka \<in> carrier R; h \<cdot>\<^sub>r ha \<in> mx; h \<cdot>\<^sub>r ka \<in> mx; k \<cdot>\<^sub>r ha \<in> mx; r \<in> carrier R; r \<cdot>\<^sub>r (x \<cdot>\<^sub>r y) = k \<cdot>\<^sub>r ka; h \<cdot>\<^sub>r ha \<plusminus> h \<cdot>\<^sub>r ka \<plusminus> (k \<cdot>\<^sub>r ha \<plusminus> k \<cdot>\<^sub>r ka) \<in> mx\<rbrakk> \<Longrightarrow> False
 4. \<And>x y s1 s2 h k. \<lbrakk>mul_closed_set R S; 1\<^sub>r \<in> S; \<zero> \<notin> S; T = {I. ideal R I \<and> S \<inter> I = {}}; maximal_set {I. ideal R I \<and> S \<inter> I = {}} mx; x \<in> carrier R; y \<in> carrier R; x \<cdot>\<^sub>r y \<in> mx; x \<notin> mx; y \<notin> mx; h \<plusminus> k \<in> S; s2 \<in> S; \<exists>h\<in>mx. \<exists>k\<in>R \<diamondsuit>\<^sub>p y. s2 = h \<plusminus> k; ideal R mx; ideal R (R \<diamondsuit>\<^sub>p x); ideal R (R \<diamondsuit>\<^sub>p y); mx \<subseteq> carrier R; R \<diamondsuit>\<^sub>p x \<subseteq> carrier R; R \<diamondsuit>\<^sub>p y \<subseteq> carrier R; aGroup R; h \<in> mx; k \<in> R \<diamondsuit>\<^sub>p x; s1 = h \<plusminus> k; (h \<plusminus> k) \<cdot>\<^sub>r s2 \<in> S; h \<in> carrier R; k \<in> carrier R\<rbrakk> \<Longrightarrow> mul_closed_set R S
[PROOF STEP]
apply (rule ideal_pOp_closed, assumption+)+
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x y s1 s2 h k ha ka r. \<lbrakk>k \<cdot>\<^sub>r ka \<in> mx; mul_closed_set R S; 1\<^sub>r \<in> S; \<zero> \<notin> S; T = {I. ideal R I \<and> S \<inter> I = {}}; maximal_set {I. ideal R I \<and> S \<inter> I = {}} mx; x \<in> carrier R; y \<in> carrier R; x \<cdot>\<^sub>r y \<in> mx; x \<notin> mx; y \<notin> mx; h \<plusminus> k \<in> S; ha \<plusminus> ka \<in> S; ideal R mx; ideal R (R \<diamondsuit>\<^sub>p x); ideal R (R \<diamondsuit>\<^sub>p y); mx \<subseteq> carrier R; R \<diamondsuit>\<^sub>p x \<subseteq> carrier R; R \<diamondsuit>\<^sub>p y \<subseteq> carrier R; aGroup R; h \<in> mx; k \<in> R \<diamondsuit>\<^sub>p x; s1 = h \<plusminus> k; h \<cdot>\<^sub>r ha \<plusminus> h \<cdot>\<^sub>r ka \<plusminus> (k \<cdot>\<^sub>r ha \<plusminus> k \<cdot>\<^sub>r ka) \<in> S; h \<in> carrier R; k \<in> carrier R; S \<subseteq> carrier R; ha \<plusminus> ka \<in> carrier R; ha \<in> mx; ka \<in> R \<diamondsuit>\<^sub>p y; s2 = ha \<plusminus> ka; ha \<in> carrier R; ka \<in> carrier R; h \<cdot>\<^sub>r ha \<in> mx; h \<cdot>\<^sub>r ka \<in> mx; k \<cdot>\<^sub>r ha \<in> mx; r \<in> carrier R; r \<cdot>\<^sub>r (x \<cdot>\<^sub>r y) = k \<cdot>\<^sub>r ka; h \<cdot>\<^sub>r ha \<plusminus> h \<cdot>\<^sub>r ka \<plusminus> (k \<cdot>\<^sub>r ha \<plusminus> k \<cdot>\<^sub>r ka) \<in> mx\<rbrakk> \<Longrightarrow> False
 2. \<And>x y s1 s2 h k. \<lbrakk>mul_closed_set R S; 1\<^sub>r \<in> S; \<zero> \<notin> S; T = {I. ideal R I \<and> S \<inter> I = {}}; maximal_set {I. ideal R I \<and> S \<inter> I = {}} mx; x \<in> carrier R; y \<in> carrier R; x \<cdot>\<^sub>r y \<in> mx; x \<notin> mx; y \<notin> mx; h \<plusminus> k \<in> S; s2 \<in> S; \<exists>h\<in>mx. \<exists>k\<in>R \<diamondsuit>\<^sub>p y. s2 = h \<plusminus> k; ideal R mx; ideal R (R \<diamondsuit>\<^sub>p x); ideal R (R \<diamondsuit>\<^sub>p y); mx \<subseteq> carrier R; R \<diamondsuit>\<^sub>p x \<subseteq> carrier R; R \<diamondsuit>\<^sub>p y \<subseteq> carrier R; aGroup R; h \<in> mx; k \<in> R \<diamondsuit>\<^sub>p x; s1 = h \<plusminus> k; (h \<plusminus> k) \<cdot>\<^sub>r s2 \<in> S; h \<in> carrier R; k \<in> carrier R\<rbrakk> \<Longrightarrow> mul_closed_set R S
[PROOF STEP]
apply (simp add:maximal_set_def)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x y s1 s2 h k ha ka r. \<lbrakk>k \<cdot>\<^sub>r ka \<in> mx; mul_closed_set R S; 1\<^sub>r \<in> S; \<zero> \<notin> S; T = {I. ideal R I \<and> S \<inter> I = {}}; S \<inter> mx = {} \<and> (\<forall>s. ideal R s \<and> S \<inter> s = {} \<longrightarrow> mx \<subseteq> s \<longrightarrow> s = mx); x \<in> carrier R; y \<in> carrier R; x \<cdot>\<^sub>r y \<in> mx; x \<notin> mx; y \<notin> mx; h \<plusminus> k \<in> S; ha \<plusminus> ka \<in> S; ideal R mx; ideal R (R \<diamondsuit>\<^sub>p x); ideal R (R \<diamondsuit>\<^sub>p y); mx \<subseteq> carrier R; R \<diamondsuit>\<^sub>p x \<subseteq> carrier R; R \<diamondsuit>\<^sub>p y \<subseteq> carrier R; aGroup R; h \<in> mx; k \<in> R \<diamondsuit>\<^sub>p x; s1 = h \<plusminus> k; h \<cdot>\<^sub>r ha \<plusminus> h \<cdot>\<^sub>r ka \<plusminus> (k \<cdot>\<^sub>r ha \<plusminus> k \<cdot>\<^sub>r ka) \<in> S; h \<in> carrier R; k \<in> carrier R; S \<subseteq> carrier R; ha \<plusminus> ka \<in> carrier R; ha \<in> mx; ka \<in> R \<diamondsuit>\<^sub>p y; s2 = ha \<plusminus> ka; ha \<in> carrier R; ka \<in> carrier R; h \<cdot>\<^sub>r ha \<in> mx; h \<cdot>\<^sub>r ka \<in> mx; k \<cdot>\<^sub>r ha \<in> mx; r \<in> carrier R; r \<cdot>\<^sub>r (x \<cdot>\<^sub>r y) = k \<cdot>\<^sub>r ka; h \<cdot>\<^sub>r ha \<plusminus> h \<cdot>\<^sub>r ka \<plusminus> (k \<cdot>\<^sub>r ha \<plusminus> k \<cdot>\<^sub>r ka) \<in> mx\<rbrakk> \<Longrightarrow> False
 2. \<And>x y s1 s2 h k. \<lbrakk>mul_closed_set R S; 1\<^sub>r \<in> S; \<zero> \<notin> S; T = {I. ideal R I \<and> S \<inter> I = {}}; maximal_set {I. ideal R I \<and> S \<inter> I = {}} mx; x \<in> carrier R; y \<in> carrier R; x \<cdot>\<^sub>r y \<in> mx; x \<notin> mx; y \<notin> mx; h \<plusminus> k \<in> S; s2 \<in> S; \<exists>h\<in>mx. \<exists>k\<in>R \<diamondsuit>\<^sub>p y. s2 = h \<plusminus> k; ideal R mx; ideal R (R \<diamondsuit>\<^sub>p x); ideal R (R \<diamondsuit>\<^sub>p y); mx \<subseteq> carrier R; R \<diamondsuit>\<^sub>p x \<subseteq> carrier R; R \<diamondsuit>\<^sub>p y \<subseteq> carrier R; aGroup R; h \<in> mx; k \<in> R \<diamondsuit>\<^sub>p x; s1 = h \<plusminus> k; (h \<plusminus> k) \<cdot>\<^sub>r s2 \<in> S; h \<in> carrier R; k \<in> carrier R\<rbrakk> \<Longrightarrow> mul_closed_set R S
[PROOF STEP]
apply blast
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x y s1 s2 h k. \<lbrakk>mul_closed_set R S; 1\<^sub>r \<in> S; \<zero> \<notin> S; T = {I. ideal R I \<and> S \<inter> I = {}}; maximal_set {I. ideal R I \<and> S \<inter> I = {}} mx; x \<in> carrier R; y \<in> carrier R; x \<cdot>\<^sub>r y \<in> mx; x \<notin> mx; y \<notin> mx; h \<plusminus> k \<in> S; s2 \<in> S; \<exists>h\<in>mx. \<exists>k\<in>R \<diamondsuit>\<^sub>p y. s2 = h \<plusminus> k; ideal R mx; ideal R (R \<diamondsuit>\<^sub>p x); ideal R (R \<diamondsuit>\<^sub>p y); mx \<subseteq> carrier R; R \<diamondsuit>\<^sub>p x \<subseteq> carrier R; R \<diamondsuit>\<^sub>p y \<subseteq> carrier R; aGroup R; h \<in> mx; k \<in> R \<diamondsuit>\<^sub>p x; s1 = h \<plusminus> k; (h \<plusminus> k) \<cdot>\<^sub>r s2 \<in> S; h \<in> carrier R; k \<in> carrier R\<rbrakk> \<Longrightarrow> mul_closed_set R S
[PROOF STEP]
apply assumption
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma (in Ring) ex_mulDisj_maximal:"\<lbrakk>mul_closed_set R S; \<zero> \<notin> S; 1\<^sub>r \<in> S;
       T = {I. ideal R I \<and> S \<inter> I = {}}\<rbrakk> \<Longrightarrow>  \<exists>mx. maximal_set T mx"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>mul_closed_set R S; \<zero> \<notin> S; 1\<^sub>r \<in> S; T = {I. ideal R I \<and> S \<inter> I = {}}\<rbrakk> \<Longrightarrow> \<exists>mx. maximal_set T mx
[PROOF STEP]
apply (cut_tac A="{ I. ideal R I \<and> S \<inter> I = {}}" in Zorn_Lemma2)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>mul_closed_set R S; \<zero> \<notin> S; 1\<^sub>r \<in> S; T = {I. ideal R I \<and> S \<inter> I = {}}\<rbrakk> \<Longrightarrow> \<forall>C\<in>chains {I. ideal R I \<and> S \<inter> I = {}}. \<exists>U\<in>{I. ideal R I \<and> S \<inter> I = {}}. \<forall>X\<in>C. X \<subseteq> U
 2. \<lbrakk>mul_closed_set R S; \<zero> \<notin> S; 1\<^sub>r \<in> S; T = {I. ideal R I \<and> S \<inter> I = {}}; \<exists>M\<in>{I. ideal R I \<and> S \<inter> I = {}}. \<forall>X\<in>{I. ideal R I \<and> S \<inter> I = {}}. M \<subseteq> X \<longrightarrow> X = M\<rbrakk> \<Longrightarrow> \<exists>mx. maximal_set T mx
[PROOF STEP]
prefer 2
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>mul_closed_set R S; \<zero> \<notin> S; 1\<^sub>r \<in> S; T = {I. ideal R I \<and> S \<inter> I = {}}; \<exists>M\<in>{I. ideal R I \<and> S \<inter> I = {}}. \<forall>X\<in>{I. ideal R I \<and> S \<inter> I = {}}. M \<subseteq> X \<longrightarrow> X = M\<rbrakk> \<Longrightarrow> \<exists>mx. maximal_set T mx
 2. \<lbrakk>mul_closed_set R S; \<zero> \<notin> S; 1\<^sub>r \<in> S; T = {I. ideal R I \<and> S \<inter> I = {}}\<rbrakk> \<Longrightarrow> \<forall>C\<in>chains {I. ideal R I \<and> S \<inter> I = {}}. \<exists>U\<in>{I. ideal R I \<and> S \<inter> I = {}}. \<forall>X\<in>C. X \<subseteq> U
[PROOF STEP]
apply (simp add:maximal_set_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>mul_closed_set R S; \<zero> \<notin> S; 1\<^sub>r \<in> S; T = {I. ideal R I \<and> S \<inter> I = {}}\<rbrakk> \<Longrightarrow> \<forall>C\<in>chains {I. ideal R I \<and> S \<inter> I = {}}. \<exists>U\<in>{I. ideal R I \<and> S \<inter> I = {}}. \<forall>X\<in>C. X \<subseteq> U
[PROOF STEP]
apply (rule ballI)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>C. \<lbrakk>mul_closed_set R S; \<zero> \<notin> S; 1\<^sub>r \<in> S; T = {I. ideal R I \<and> S \<inter> I = {}}; C \<in> chains {I. ideal R I \<and> S \<inter> I = {}}\<rbrakk> \<Longrightarrow> \<exists>U\<in>{I. ideal R I \<and> S \<inter> I = {}}. \<forall>X\<in>C. X \<subseteq> U
[PROOF STEP]
apply (case_tac "C = {}")
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>C. \<lbrakk>mul_closed_set R S; \<zero> \<notin> S; 1\<^sub>r \<in> S; T = {I. ideal R I \<and> S \<inter> I = {}}; C \<in> chains {I. ideal R I \<and> S \<inter> I = {}}; C = {}\<rbrakk> \<Longrightarrow> \<exists>U\<in>{I. ideal R I \<and> S \<inter> I = {}}. \<forall>X\<in>C. X \<subseteq> U
 2. \<And>C. \<lbrakk>mul_closed_set R S; \<zero> \<notin> S; 1\<^sub>r \<in> S; T = {I. ideal R I \<and> S \<inter> I = {}}; C \<in> chains {I. ideal R I \<and> S \<inter> I = {}}; C \<noteq> {}\<rbrakk> \<Longrightarrow> \<exists>U\<in>{I. ideal R I \<and> S \<inter> I = {}}. \<forall>X\<in>C. X \<subseteq> U
[PROOF STEP]
apply (cut_tac zero_ideal, blast)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>C. \<lbrakk>mul_closed_set R S; \<zero> \<notin> S; 1\<^sub>r \<in> S; T = {I. ideal R I \<and> S \<inter> I = {}}; C \<in> chains {I. ideal R I \<and> S \<inter> I = {}}; C \<noteq> {}\<rbrakk> \<Longrightarrow> \<exists>U\<in>{I. ideal R I \<and> S \<inter> I = {}}. \<forall>X\<in>C. X \<subseteq> U
[PROOF STEP]
apply (subgoal_tac "C \<in> chains {I. ideal R I \<and> I \<subset> carrier R}")
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>C. \<lbrakk>mul_closed_set R S; \<zero> \<notin> S; 1\<^sub>r \<in> S; T = {I. ideal R I \<and> S \<inter> I = {}}; C \<in> chains {I. ideal R I \<and> S \<inter> I = {}}; C \<noteq> {}; C \<in> chains {I. ideal R I \<and> I \<subset> carrier R}\<rbrakk> \<Longrightarrow> \<exists>U\<in>{I. ideal R I \<and> S \<inter> I = {}}. \<forall>X\<in>C. X \<subseteq> U
 2. \<And>C. \<lbrakk>mul_closed_set R S; \<zero> \<notin> S; 1\<^sub>r \<in> S; T = {I. ideal R I \<and> S \<inter> I = {}}; C \<in> chains {I. ideal R I \<and> S \<inter> I = {}}; C \<noteq> {}\<rbrakk> \<Longrightarrow> C \<in> chains {I. ideal R I \<and> I \<subset> carrier R}
[PROOF STEP]
apply (frule chains_un, assumption)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>C. \<lbrakk>mul_closed_set R S; \<zero> \<notin> S; 1\<^sub>r \<in> S; T = {I. ideal R I \<and> S \<inter> I = {}}; C \<in> chains {I. ideal R I \<and> S \<inter> I = {}}; C \<noteq> {}; C \<in> chains {I. ideal R I \<and> I \<subset> carrier R}; ideal R (\<Union> C)\<rbrakk> \<Longrightarrow> \<exists>U\<in>{I. ideal R I \<and> S \<inter> I = {}}. \<forall>X\<in>C. X \<subseteq> U
 2. \<And>C. \<lbrakk>mul_closed_set R S; \<zero> \<notin> S; 1\<^sub>r \<in> S; T = {I. ideal R I \<and> S \<inter> I = {}}; C \<in> chains {I. ideal R I \<and> S \<inter> I = {}}; C \<noteq> {}\<rbrakk> \<Longrightarrow> C \<in> chains {I. ideal R I \<and> I \<subset> carrier R}
[PROOF STEP]
apply (subgoal_tac "S \<inter> (\<Union> C) = {}")
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>C. \<lbrakk>mul_closed_set R S; \<zero> \<notin> S; 1\<^sub>r \<in> S; T = {I. ideal R I \<and> S \<inter> I = {}}; C \<in> chains {I. ideal R I \<and> S \<inter> I = {}}; C \<noteq> {}; C \<in> chains {I. ideal R I \<and> I \<subset> carrier R}; ideal R (\<Union> C); S \<inter> \<Union> C = {}\<rbrakk> \<Longrightarrow> \<exists>U\<in>{I. ideal R I \<and> S \<inter> I = {}}. \<forall>X\<in>C. X \<subseteq> U
 2. \<And>C. \<lbrakk>mul_closed_set R S; \<zero> \<notin> S; 1\<^sub>r \<in> S; T = {I. ideal R I \<and> S \<inter> I = {}}; C \<in> chains {I. ideal R I \<and> S \<inter> I = {}}; C \<noteq> {}; C \<in> chains {I. ideal R I \<and> I \<subset> carrier R}; ideal R (\<Union> C)\<rbrakk> \<Longrightarrow> S \<inter> \<Union> C = {}
 3. \<And>C. \<lbrakk>mul_closed_set R S; \<zero> \<notin> S; 1\<^sub>r \<in> S; T = {I. ideal R I \<and> S \<inter> I = {}}; C \<in> chains {I. ideal R I \<and> S \<inter> I = {}}; C \<noteq> {}\<rbrakk> \<Longrightarrow> C \<in> chains {I. ideal R I \<and> I \<subset> carrier R}
[PROOF STEP]
apply (subgoal_tac "\<forall>x\<in>C. x \<subseteq> \<Union> C",  blast)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>C. \<lbrakk>mul_closed_set R S; \<zero> \<notin> S; 1\<^sub>r \<in> S; T = {I. ideal R I \<and> S \<inter> I = {}}; C \<in> chains {I. ideal R I \<and> S \<inter> I = {}}; C \<noteq> {}; C \<in> chains {I. ideal R I \<and> I \<subset> carrier R}; ideal R (\<Union> C); S \<inter> \<Union> C = {}\<rbrakk> \<Longrightarrow> \<forall>x\<in>C. x \<subseteq> \<Union> C
 2. \<And>C. \<lbrakk>mul_closed_set R S; \<zero> \<notin> S; 1\<^sub>r \<in> S; T = {I. ideal R I \<and> S \<inter> I = {}}; C \<in> chains {I. ideal R I \<and> S \<inter> I = {}}; C \<noteq> {}; C \<in> chains {I. ideal R I \<and> I \<subset> carrier R}; ideal R (\<Union> C)\<rbrakk> \<Longrightarrow> S \<inter> \<Union> C = {}
 3. \<And>C. \<lbrakk>mul_closed_set R S; \<zero> \<notin> S; 1\<^sub>r \<in> S; T = {I. ideal R I \<and> S \<inter> I = {}}; C \<in> chains {I. ideal R I \<and> S \<inter> I = {}}; C \<noteq> {}\<rbrakk> \<Longrightarrow> C \<in> chains {I. ideal R I \<and> I \<subset> carrier R}
[PROOF STEP]
apply (rule ballI, rule subsetI, simp add:CollectI)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>C x xa. \<lbrakk>mul_closed_set R S; \<zero> \<notin> S; 1\<^sub>r \<in> S; T = {I. ideal R I \<and> S \<inter> I = {}}; C \<in> chains {I. ideal R I \<and> S \<inter> I = {}}; C \<noteq> {}; C \<in> chains {I. ideal R I \<and> I \<subset> carrier R}; ideal R (\<Union> C); S \<inter> \<Union> C = {}; x \<in> C; xa \<in> x\<rbrakk> \<Longrightarrow> \<exists>X\<in>C. xa \<in> X
 2. \<And>C. \<lbrakk>mul_closed_set R S; \<zero> \<notin> S; 1\<^sub>r \<in> S; T = {I. ideal R I \<and> S \<inter> I = {}}; C \<in> chains {I. ideal R I \<and> S \<inter> I = {}}; C \<noteq> {}; C \<in> chains {I. ideal R I \<and> I \<subset> carrier R}; ideal R (\<Union> C)\<rbrakk> \<Longrightarrow> S \<inter> \<Union> C = {}
 3. \<And>C. \<lbrakk>mul_closed_set R S; \<zero> \<notin> S; 1\<^sub>r \<in> S; T = {I. ideal R I \<and> S \<inter> I = {}}; C \<in> chains {I. ideal R I \<and> S \<inter> I = {}}; C \<noteq> {}\<rbrakk> \<Longrightarrow> C \<in> chains {I. ideal R I \<and> I \<subset> carrier R}
[PROOF STEP]
apply blast
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>C. \<lbrakk>mul_closed_set R S; \<zero> \<notin> S; 1\<^sub>r \<in> S; T = {I. ideal R I \<and> S \<inter> I = {}}; C \<in> chains {I. ideal R I \<and> S \<inter> I = {}}; C \<noteq> {}; C \<in> chains {I. ideal R I \<and> I \<subset> carrier R}; ideal R (\<Union> C)\<rbrakk> \<Longrightarrow> S \<inter> \<Union> C = {}
 2. \<And>C. \<lbrakk>mul_closed_set R S; \<zero> \<notin> S; 1\<^sub>r \<in> S; T = {I. ideal R I \<and> S \<inter> I = {}}; C \<in> chains {I. ideal R I \<and> S \<inter> I = {}}; C \<noteq> {}\<rbrakk> \<Longrightarrow> C \<in> chains {I. ideal R I \<and> I \<subset> carrier R}
[PROOF STEP]
apply (rule contrapos_pp, simp+)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>C. \<lbrakk>mul_closed_set R S; \<zero> \<notin> S; 1\<^sub>r \<in> S; T = {I. ideal R I \<and> S \<inter> I = {}}; C \<in> chains {I. ideal R I \<and> S \<inter> I = {}}; C \<noteq> {}; C \<in> chains {I. ideal R I \<and> I \<subset> carrier R}; ideal R (\<Union> C); S \<inter> \<Union> C \<noteq> {}\<rbrakk> \<Longrightarrow> False
 2. \<And>C. \<lbrakk>mul_closed_set R S; \<zero> \<notin> S; 1\<^sub>r \<in> S; T = {I. ideal R I \<and> S \<inter> I = {}}; C \<in> chains {I. ideal R I \<and> S \<inter> I = {}}; C \<noteq> {}\<rbrakk> \<Longrightarrow> C \<in> chains {I. ideal R I \<and> I \<subset> carrier R}
[PROOF STEP]
apply (frule_tac A = S and B = "\<Union> C" in nonempty_int)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>C. \<lbrakk>mul_closed_set R S; \<zero> \<notin> S; 1\<^sub>r \<in> S; T = {I. ideal R I \<and> S \<inter> I = {}}; C \<in> chains {I. ideal R I \<and> S \<inter> I = {}}; C \<noteq> {}; C \<in> chains {I. ideal R I \<and> I \<subset> carrier R}; ideal R (\<Union> C); S \<inter> \<Union> C \<noteq> {}; \<exists>x. x \<in> S \<inter> \<Union> C\<rbrakk> \<Longrightarrow> False
 2. \<And>C. \<lbrakk>mul_closed_set R S; \<zero> \<notin> S; 1\<^sub>r \<in> S; T = {I. ideal R I \<and> S \<inter> I = {}}; C \<in> chains {I. ideal R I \<and> S \<inter> I = {}}; C \<noteq> {}\<rbrakk> \<Longrightarrow> C \<in> chains {I. ideal R I \<and> I \<subset> carrier R}
[PROOF STEP]
apply (erule exE)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>C x. \<lbrakk>mul_closed_set R S; \<zero> \<notin> S; 1\<^sub>r \<in> S; T = {I. ideal R I \<and> S \<inter> I = {}}; C \<in> chains {I. ideal R I \<and> S \<inter> I = {}}; C \<noteq> {}; C \<in> chains {I. ideal R I \<and> I \<subset> carrier R}; ideal R (\<Union> C); S \<inter> \<Union> C \<noteq> {}; x \<in> S \<inter> \<Union> C\<rbrakk> \<Longrightarrow> False
 2. \<And>C. \<lbrakk>mul_closed_set R S; \<zero> \<notin> S; 1\<^sub>r \<in> S; T = {I. ideal R I \<and> S \<inter> I = {}}; C \<in> chains {I. ideal R I \<and> S \<inter> I = {}}; C \<noteq> {}\<rbrakk> \<Longrightarrow> C \<in> chains {I. ideal R I \<and> I \<subset> carrier R}
[PROOF STEP]
apply (simp, erule conjE, erule bexE)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>C x X. \<lbrakk>mul_closed_set R S; \<zero> \<notin> S; 1\<^sub>r \<in> S; T = {I. ideal R I \<and> S \<inter> I = {}}; C \<in> chains {I. ideal R I \<and> S \<inter> I = {}}; C \<noteq> {}; C \<in> chains {I. ideal R I \<and> I \<subset> carrier R}; ideal R (\<Union> C); S \<inter> \<Union> C \<noteq> {}; x \<in> S; X \<in> C; x \<in> X\<rbrakk> \<Longrightarrow> False
 2. \<And>C. \<lbrakk>mul_closed_set R S; \<zero> \<notin> S; 1\<^sub>r \<in> S; T = {I. ideal R I \<and> S \<inter> I = {}}; C \<in> chains {I. ideal R I \<and> S \<inter> I = {}}; C \<noteq> {}\<rbrakk> \<Longrightarrow> C \<in> chains {I. ideal R I \<and> I \<subset> carrier R}
[PROOF STEP]
apply (simp add:chains_def, erule conjE)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>C x X. \<lbrakk>mul_closed_set R S; \<zero> \<notin> S; 1\<^sub>r \<in> S; T = {I. ideal R I \<and> S \<inter> I = {}}; C \<noteq> {}; C \<subseteq> {I. ideal R I \<and> I \<subset> carrier R}; ideal R (\<Union> C); S \<inter> \<Union> C \<noteq> {}; x \<in> S; X \<in> C; x \<in> X; C \<subseteq> {I. ideal R I \<and> S \<inter> I = {}}; chain\<^sub>\<subseteq> C\<rbrakk> \<Longrightarrow> False
 2. \<And>C. \<lbrakk>mul_closed_set R S; \<zero> \<notin> S; 1\<^sub>r \<in> S; T = {I. ideal R I \<and> S \<inter> I = {}}; C \<in> chains {I. ideal R I \<and> S \<inter> I = {}}; C \<noteq> {}\<rbrakk> \<Longrightarrow> C \<in> chains {I. ideal R I \<and> I \<subset> carrier R}
[PROOF STEP]
apply (frule_tac c = X and A = C and B = "{I. ideal R I \<and> S \<inter> I = {}}" in
        subsetD, assumption+,
        thin_tac "C \<subseteq> {I. ideal R I \<and> I \<subset> carrier R}",
        thin_tac "C \<subseteq> {I. ideal R I \<and> S \<inter> I = {}}")
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>C x X. \<lbrakk>mul_closed_set R S; \<zero> \<notin> S; 1\<^sub>r \<in> S; T = {I. ideal R I \<and> S \<inter> I = {}}; C \<noteq> {}; ideal R (\<Union> C); S \<inter> \<Union> C \<noteq> {}; x \<in> S; X \<in> C; x \<in> X; chain\<^sub>\<subseteq> C; X \<in> {I. ideal R I \<and> S \<inter> I = {}}\<rbrakk> \<Longrightarrow> False
 2. \<And>C. \<lbrakk>mul_closed_set R S; \<zero> \<notin> S; 1\<^sub>r \<in> S; T = {I. ideal R I \<and> S \<inter> I = {}}; C \<in> chains {I. ideal R I \<and> S \<inter> I = {}}; C \<noteq> {}\<rbrakk> \<Longrightarrow> C \<in> chains {I. ideal R I \<and> I \<subset> carrier R}
[PROOF STEP]
apply (simp, blast)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>C. \<lbrakk>mul_closed_set R S; \<zero> \<notin> S; 1\<^sub>r \<in> S; T = {I. ideal R I \<and> S \<inter> I = {}}; C \<in> chains {I. ideal R I \<and> S \<inter> I = {}}; C \<noteq> {}\<rbrakk> \<Longrightarrow> C \<in> chains {I. ideal R I \<and> I \<subset> carrier R}
[PROOF STEP]
apply (simp add:chains_def chain_subset_def, erule conjE)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>C. \<lbrakk>mul_closed_set R S; \<zero> \<notin> S; 1\<^sub>r \<in> S; T = {I. ideal R I \<and> S \<inter> I = {}}; C \<noteq> {}; C \<subseteq> {I. ideal R I \<and> S \<inter> I = {}}; \<forall>A\<in>C. \<forall>B\<in>C. A \<subseteq> B \<or> B \<subseteq> A\<rbrakk> \<Longrightarrow> C \<subseteq> {I. ideal R I \<and> I \<subset> carrier R}
[PROOF STEP]
apply (rule subsetI)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>C x. \<lbrakk>mul_closed_set R S; \<zero> \<notin> S; 1\<^sub>r \<in> S; T = {I. ideal R I \<and> S \<inter> I = {}}; C \<noteq> {}; C \<subseteq> {I. ideal R I \<and> S \<inter> I = {}}; \<forall>A\<in>C. \<forall>B\<in>C. A \<subseteq> B \<or> B \<subseteq> A; x \<in> C\<rbrakk> \<Longrightarrow> x \<in> {I. ideal R I \<and> I \<subset> carrier R}
[PROOF STEP]
apply (frule_tac c = x and A = C and B = "{I. ideal R I \<and> S \<inter> I = {}}" in
                  subsetD, assumption+,
        thin_tac "C \<subseteq> {I. ideal R I \<and> S \<inter> I = {}}",
        thin_tac "T = {I. ideal R I \<and> S \<inter> I = {}}")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>C x. \<lbrakk>mul_closed_set R S; \<zero> \<notin> S; 1\<^sub>r \<in> S; C \<noteq> {}; \<forall>A\<in>C. \<forall>B\<in>C. A \<subseteq> B \<or> B \<subseteq> A; x \<in> C; x \<in> {I. ideal R I \<and> S \<inter> I = {}}\<rbrakk> \<Longrightarrow> x \<in> {I. ideal R I \<and> I \<subset> carrier R}
[PROOF STEP]
apply (simp, thin_tac "\<forall>x\<in>C. \<forall>y\<in>C. x \<subseteq> y \<or> y \<subseteq> x", erule conjE)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>C x. \<lbrakk>mul_closed_set R S; \<zero> \<notin> S; 1\<^sub>r \<in> S; C \<noteq> {}; x \<in> C; ideal R x; S \<inter> x = {}\<rbrakk> \<Longrightarrow> x \<subset> carrier R
[PROOF STEP]
apply (simp add:psubset_eq ideal_subset1)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>C x. \<lbrakk>mul_closed_set R S; \<zero> \<notin> S; 1\<^sub>r \<in> S; C \<noteq> {}; x \<in> C; ideal R x; S \<inter> x = {}\<rbrakk> \<Longrightarrow> x \<noteq> carrier R
[PROOF STEP]
apply (rule contrapos_pp, simp+)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>C x. \<lbrakk>mul_closed_set R S; \<zero> \<notin> S; 1\<^sub>r \<in> S; C \<noteq> {}; carrier R \<in> C; ideal R (carrier R); S \<inter> carrier R = {}; x = carrier R\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
apply (rotate_tac -1, frule sym, thin_tac "x = carrier R",
        thin_tac "carrier R = x")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>C x. \<lbrakk>mul_closed_set R S; \<zero> \<notin> S; 1\<^sub>r \<in> S; C \<noteq> {}; carrier R \<in> C; ideal R (carrier R); S \<inter> carrier R = {}\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
apply (cut_tac ring_one, blast)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma (in Ring) ex_mulDisj_prime:"\<lbrakk>mul_closed_set R S; \<zero> \<notin> S; 1\<^sub>r \<in> S\<rbrakk> \<Longrightarrow>
                            \<exists>mx. prime_ideal R mx \<and> S \<inter> mx = {}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>mul_closed_set R S; \<zero> \<notin> S; 1\<^sub>r \<in> S\<rbrakk> \<Longrightarrow> \<exists>mx. prime_ideal R mx \<and> S \<inter> mx = {}
[PROOF STEP]
apply (frule ex_mulDisj_maximal[of "S" "{I. ideal R I \<and> S \<inter> I = {}}"],
               assumption+, simp, erule exE)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>mx. \<lbrakk>mul_closed_set R S; \<zero> \<notin> S; 1\<^sub>r \<in> S; maximal_set {I. ideal R I \<and> S \<inter> I = {}} mx\<rbrakk> \<Longrightarrow> \<exists>mx. prime_ideal R mx \<and> S \<inter> mx = {}
[PROOF STEP]
apply (frule_tac mx = mx in mulDisj [of "S" "{I. ideal R I \<and> S \<inter> I = {}}"],
                  assumption+, simp, assumption)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>mx. \<lbrakk>mul_closed_set R S; \<zero> \<notin> S; 1\<^sub>r \<in> S; maximal_set {I. ideal R I \<and> S \<inter> I = {}} mx; prime_ideal R mx\<rbrakk> \<Longrightarrow> \<exists>mx. prime_ideal R mx \<and> S \<inter> mx = {}
[PROOF STEP]
apply (simp add:maximal_set_def, (erule conjE)+, blast)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma (in Ring) nilradTr1:"\<not> zeroring R \<Longrightarrow> nilrad R = \<Inter> {p. prime_ideal R p}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<not> zeroring R \<Longrightarrow> nilrad R = \<Inter> {p. prime_ideal R p}
[PROOF STEP]
apply (rule equalityI)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<not> zeroring R \<Longrightarrow> nilrad R \<subseteq> \<Inter> {p. prime_ideal R p}
 2. \<not> zeroring R \<Longrightarrow> \<Inter> {p. prime_ideal R p} \<subseteq> nilrad R
[PROOF STEP]
(* nilrad R \<subseteq> \<Inter>Collect (prime_ideal R) *)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<not> zeroring R \<Longrightarrow> nilrad R \<subseteq> \<Inter> {p. prime_ideal R p}
 2. \<not> zeroring R \<Longrightarrow> \<Inter> {p. prime_ideal R p} \<subseteq> nilrad R
[PROOF STEP]
apply (rule subsetI)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x. \<lbrakk>\<not> zeroring R; x \<in> nilrad R\<rbrakk> \<Longrightarrow> x \<in> \<Inter> {p. prime_ideal R p}
 2. \<not> zeroring R \<Longrightarrow> \<Inter> {p. prime_ideal R p} \<subseteq> nilrad R
[PROOF STEP]
apply (simp add:nilrad_def CollectI nilpotent_def)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x. \<lbrakk>\<not> zeroring R; x \<in> carrier R \<and> (\<exists>n. x^\<^bsup>R n\<^esup> = \<zero>)\<rbrakk> \<Longrightarrow> \<forall>xa. prime_ideal R xa \<longrightarrow> x \<in> xa
 2. \<not> zeroring R \<Longrightarrow> \<Inter> {p. prime_ideal R p} \<subseteq> nilrad R
[PROOF STEP]
apply (erule conjE, erule exE)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x n. \<lbrakk>\<not> zeroring R; x \<in> carrier R; x^\<^bsup>R n\<^esup> = \<zero>\<rbrakk> \<Longrightarrow> \<forall>xa. prime_ideal R xa \<longrightarrow> x \<in> xa
 2. \<not> zeroring R \<Longrightarrow> \<Inter> {p. prime_ideal R p} \<subseteq> nilrad R
[PROOF STEP]
apply (rule allI, rule impI)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x n xa. \<lbrakk>\<not> zeroring R; x \<in> carrier R; x^\<^bsup>R n\<^esup> = \<zero>; prime_ideal R xa\<rbrakk> \<Longrightarrow> x \<in> xa
 2. \<not> zeroring R \<Longrightarrow> \<Inter> {p. prime_ideal R p} \<subseteq> nilrad R
[PROOF STEP]
apply (frule_tac prime_ideal_ideal)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x n xa. \<lbrakk>\<not> zeroring R; x \<in> carrier R; x^\<^bsup>R n\<^esup> = \<zero>; prime_ideal R xa; ideal R xa\<rbrakk> \<Longrightarrow> x \<in> xa
 2. \<not> zeroring R \<Longrightarrow> \<Inter> {p. prime_ideal R p} \<subseteq> nilrad R
[PROOF STEP]
apply (frule sym, thin_tac "x^\<^bsup>R n\<^esup> = \<zero>", frule ideal_zero, simp)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x n xa. \<lbrakk>\<not> zeroring R; x \<in> carrier R; prime_ideal R xa; ideal R xa; \<zero> = x^\<^bsup>R n\<^esup>; x^\<^bsup>R n\<^esup> \<in> xa\<rbrakk> \<Longrightarrow> x \<in> xa
 2. \<not> zeroring R \<Longrightarrow> \<Inter> {p. prime_ideal R p} \<subseteq> nilrad R
[PROOF STEP]
apply (case_tac "n = 0", simp)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>x n xa. \<lbrakk>\<not> zeroring R; x \<in> carrier R; prime_ideal R xa; ideal R xa; \<zero> = 1\<^sub>r; 1\<^sub>r \<in> xa; n = 0\<rbrakk> \<Longrightarrow> x \<in> xa
 2. \<And>x n xa. \<lbrakk>\<not> zeroring R; x \<in> carrier R; prime_ideal R xa; ideal R xa; \<zero> = x^\<^bsup>R n\<^esup>; x^\<^bsup>R n\<^esup> \<in> xa; n \<noteq> 0\<rbrakk> \<Longrightarrow> x \<in> xa
 3. \<not> zeroring R \<Longrightarrow> \<Inter> {p. prime_ideal R p} \<subseteq> nilrad R
[PROOF STEP]
apply (frule Zero_ring1[THEN not_sym], simp)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x n xa. \<lbrakk>\<not> zeroring R; x \<in> carrier R; prime_ideal R xa; ideal R xa; \<zero> = x^\<^bsup>R n\<^esup>; x^\<^bsup>R n\<^esup> \<in> xa; n \<noteq> 0\<rbrakk> \<Longrightarrow> x \<in> xa
 2. \<not> zeroring R \<Longrightarrow> \<Inter> {p. prime_ideal R p} \<subseteq> nilrad R
[PROOF STEP]
apply (rule_tac P = xa and x = x in npow_in_prime,assumption+, blast)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<not> zeroring R \<Longrightarrow> \<Inter> {p. prime_ideal R p} \<subseteq> nilrad R
[PROOF STEP]
apply (rule subsetI)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>\<not> zeroring R; x \<in> \<Inter> {p. prime_ideal R p}\<rbrakk> \<Longrightarrow> x \<in> nilrad R
[PROOF STEP]
apply (rule contrapos_pp, simp+)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>\<not> zeroring R; \<forall>xa. prime_ideal R xa \<longrightarrow> x \<in> xa; x \<notin> nilrad R\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
apply (frule id_maximal_Exist, erule exE,
        frule maximal_prime)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x I. \<lbrakk>\<not> zeroring R; \<forall>xa. prime_ideal R xa \<longrightarrow> x \<in> xa; x \<notin> nilrad R; maximal_ideal R I; prime_ideal R I\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
apply (frule_tac a = I in forall_spec, assumption,
        frule_tac I = I in prime_ideal_ideal,
        frule_tac h = x and I = I in ideal_subset, assumption)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x I. \<lbrakk>\<not> zeroring R; \<forall>xa. prime_ideal R xa \<longrightarrow> x \<in> xa; x \<notin> nilrad R; maximal_ideal R I; prime_ideal R I; x \<in> I; ideal R I; x \<in> carrier R\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
apply (subgoal_tac "\<zero> \<notin> {s. \<exists>n. s = npow R x n} \<and>
                                  1\<^sub>r \<in> {s. \<exists>n. s = npow R x n}")
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x I. \<lbrakk>\<not> zeroring R; \<forall>xa. prime_ideal R xa \<longrightarrow> x \<in> xa; x \<notin> nilrad R; maximal_ideal R I; prime_ideal R I; x \<in> I; ideal R I; x \<in> carrier R; \<zero> \<notin> {s. \<exists>n. s = x^\<^bsup>R n\<^esup>} \<and> 1\<^sub>r \<in> {s. \<exists>n. s = x^\<^bsup>R n\<^esup>}\<rbrakk> \<Longrightarrow> False
 2. \<And>x I. \<lbrakk>\<not> zeroring R; \<forall>xa. prime_ideal R xa \<longrightarrow> x \<in> xa; x \<notin> nilrad R; maximal_ideal R I; prime_ideal R I; x \<in> I; ideal R I; x \<in> carrier R\<rbrakk> \<Longrightarrow> \<zero> \<notin> {s. \<exists>n. s = x^\<^bsup>R n\<^esup>} \<and> 1\<^sub>r \<in> {s. \<exists>n. s = x^\<^bsup>R n\<^esup>}
[PROOF STEP]
apply (subgoal_tac "mul_closed_set R {s. \<exists>n. s = npow R x n}")
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>x I. \<lbrakk>\<not> zeroring R; \<forall>xa. prime_ideal R xa \<longrightarrow> x \<in> xa; x \<notin> nilrad R; maximal_ideal R I; prime_ideal R I; x \<in> I; ideal R I; x \<in> carrier R; \<zero> \<notin> {s. \<exists>n. s = x^\<^bsup>R n\<^esup>} \<and> 1\<^sub>r \<in> {s. \<exists>n. s = x^\<^bsup>R n\<^esup>}; mul_closed_set R {s. \<exists>n. s = x^\<^bsup>R n\<^esup>}\<rbrakk> \<Longrightarrow> False
 2. \<And>x I. \<lbrakk>\<not> zeroring R; \<forall>xa. prime_ideal R xa \<longrightarrow> x \<in> xa; x \<notin> nilrad R; maximal_ideal R I; prime_ideal R I; x \<in> I; ideal R I; x \<in> carrier R; \<zero> \<notin> {s. \<exists>n. s = x^\<^bsup>R n\<^esup>} \<and> 1\<^sub>r \<in> {s. \<exists>n. s = x^\<^bsup>R n\<^esup>}\<rbrakk> \<Longrightarrow> mul_closed_set R {s. \<exists>n. s = x^\<^bsup>R n\<^esup>}
 3. \<And>x I. \<lbrakk>\<not> zeroring R; \<forall>xa. prime_ideal R xa \<longrightarrow> x \<in> xa; x \<notin> nilrad R; maximal_ideal R I; prime_ideal R I; x \<in> I; ideal R I; x \<in> carrier R\<rbrakk> \<Longrightarrow> \<zero> \<notin> {s. \<exists>n. s = x^\<^bsup>R n\<^esup>} \<and> 1\<^sub>r \<in> {s. \<exists>n. s = x^\<^bsup>R n\<^esup>}
[PROOF STEP]
apply (erule conjE)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>x I. \<lbrakk>\<not> zeroring R; \<forall>xa. prime_ideal R xa \<longrightarrow> x \<in> xa; x \<notin> nilrad R; maximal_ideal R I; prime_ideal R I; x \<in> I; ideal R I; x \<in> carrier R; mul_closed_set R {s. \<exists>n. s = x^\<^bsup>R n\<^esup>}; \<zero> \<notin> {s. \<exists>n. s = x^\<^bsup>R n\<^esup>}; 1\<^sub>r \<in> {s. \<exists>n. s = x^\<^bsup>R n\<^esup>}\<rbrakk> \<Longrightarrow> False
 2. \<And>x I. \<lbrakk>\<not> zeroring R; \<forall>xa. prime_ideal R xa \<longrightarrow> x \<in> xa; x \<notin> nilrad R; maximal_ideal R I; prime_ideal R I; x \<in> I; ideal R I; x \<in> carrier R; \<zero> \<notin> {s. \<exists>n. s = x^\<^bsup>R n\<^esup>} \<and> 1\<^sub>r \<in> {s. \<exists>n. s = x^\<^bsup>R n\<^esup>}\<rbrakk> \<Longrightarrow> mul_closed_set R {s. \<exists>n. s = x^\<^bsup>R n\<^esup>}
 3. \<And>x I. \<lbrakk>\<not> zeroring R; \<forall>xa. prime_ideal R xa \<longrightarrow> x \<in> xa; x \<notin> nilrad R; maximal_ideal R I; prime_ideal R I; x \<in> I; ideal R I; x \<in> carrier R\<rbrakk> \<Longrightarrow> \<zero> \<notin> {s. \<exists>n. s = x^\<^bsup>R n\<^esup>} \<and> 1\<^sub>r \<in> {s. \<exists>n. s = x^\<^bsup>R n\<^esup>}
[PROOF STEP]
apply (frule_tac S = "{s. \<exists>n. s = npow R x n}" in ex_mulDisj_prime,
       assumption+, erule exE, erule conjE)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>x I mx. \<lbrakk>\<not> zeroring R; \<forall>xa. prime_ideal R xa \<longrightarrow> x \<in> xa; x \<notin> nilrad R; maximal_ideal R I; prime_ideal R I; x \<in> I; ideal R I; x \<in> carrier R; mul_closed_set R {s. \<exists>n. s = x^\<^bsup>R n\<^esup>}; \<zero> \<notin> {s. \<exists>n. s = x^\<^bsup>R n\<^esup>}; 1\<^sub>r \<in> {s. \<exists>n. s = x^\<^bsup>R n\<^esup>}; prime_ideal R mx; {s. \<exists>n. s = x^\<^bsup>R n\<^esup>} \<inter> mx = {}\<rbrakk> \<Longrightarrow> False
 2. \<And>x I. \<lbrakk>\<not> zeroring R; \<forall>xa. prime_ideal R xa \<longrightarrow> x \<in> xa; x \<notin> nilrad R; maximal_ideal R I; prime_ideal R I; x \<in> I; ideal R I; x \<in> carrier R; \<zero> \<notin> {s. \<exists>n. s = x^\<^bsup>R n\<^esup>} \<and> 1\<^sub>r \<in> {s. \<exists>n. s = x^\<^bsup>R n\<^esup>}\<rbrakk> \<Longrightarrow> mul_closed_set R {s. \<exists>n. s = x^\<^bsup>R n\<^esup>}
 3. \<And>x I. \<lbrakk>\<not> zeroring R; \<forall>xa. prime_ideal R xa \<longrightarrow> x \<in> xa; x \<notin> nilrad R; maximal_ideal R I; prime_ideal R I; x \<in> I; ideal R I; x \<in> carrier R\<rbrakk> \<Longrightarrow> \<zero> \<notin> {s. \<exists>n. s = x^\<^bsup>R n\<^esup>} \<and> 1\<^sub>r \<in> {s. \<exists>n. s = x^\<^bsup>R n\<^esup>}
[PROOF STEP]
apply (subgoal_tac "x \<in> {s. \<exists>n. s = x^\<^bsup>R n\<^esup>}", blast)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>x I mx. \<lbrakk>\<not> zeroring R; \<forall>xa. prime_ideal R xa \<longrightarrow> x \<in> xa; x \<notin> nilrad R; maximal_ideal R I; prime_ideal R I; x \<in> I; ideal R I; x \<in> carrier R; mul_closed_set R {s. \<exists>n. s = x^\<^bsup>R n\<^esup>}; \<zero> \<notin> {s. \<exists>n. s = x^\<^bsup>R n\<^esup>}; 1\<^sub>r \<in> {s. \<exists>n. s = x^\<^bsup>R n\<^esup>}; prime_ideal R mx; {s. \<exists>n. s = x^\<^bsup>R n\<^esup>} \<inter> mx = {}\<rbrakk> \<Longrightarrow> x \<in> {s. \<exists>n. s = x^\<^bsup>R n\<^esup>}
 2. \<And>x I. \<lbrakk>\<not> zeroring R; \<forall>xa. prime_ideal R xa \<longrightarrow> x \<in> xa; x \<notin> nilrad R; maximal_ideal R I; prime_ideal R I; x \<in> I; ideal R I; x \<in> carrier R; \<zero> \<notin> {s. \<exists>n. s = x^\<^bsup>R n\<^esup>} \<and> 1\<^sub>r \<in> {s. \<exists>n. s = x^\<^bsup>R n\<^esup>}\<rbrakk> \<Longrightarrow> mul_closed_set R {s. \<exists>n. s = x^\<^bsup>R n\<^esup>}
 3. \<And>x I. \<lbrakk>\<not> zeroring R; \<forall>xa. prime_ideal R xa \<longrightarrow> x \<in> xa; x \<notin> nilrad R; maximal_ideal R I; prime_ideal R I; x \<in> I; ideal R I; x \<in> carrier R\<rbrakk> \<Longrightarrow> \<zero> \<notin> {s. \<exists>n. s = x^\<^bsup>R n\<^esup>} \<and> 1\<^sub>r \<in> {s. \<exists>n. s = x^\<^bsup>R n\<^esup>}
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>x I mx. \<lbrakk>\<not> zeroring R; \<forall>xa. prime_ideal R xa \<longrightarrow> x \<in> xa; x \<notin> nilrad R; maximal_ideal R I; prime_ideal R I; ideal R I; x \<in> carrier R; mul_closed_set R {s. \<exists>n. s = x^\<^bsup>R n\<^esup>}; \<forall>n. \<zero> \<noteq> x^\<^bsup>R n\<^esup>; \<exists>n. 1\<^sub>r = x^\<^bsup>R n\<^esup>; prime_ideal R mx; {s. \<exists>n. s = x^\<^bsup>R n\<^esup>} \<inter> mx = {}\<rbrakk> \<Longrightarrow> \<exists>n. x = x^\<^bsup>R n\<^esup>
 2. \<And>x I. \<lbrakk>\<not> zeroring R; \<forall>xa. prime_ideal R xa \<longrightarrow> x \<in> xa; x \<notin> nilrad R; maximal_ideal R I; prime_ideal R I; x \<in> I; ideal R I; x \<in> carrier R; \<zero> \<notin> {s. \<exists>n. s = x^\<^bsup>R n\<^esup>} \<and> 1\<^sub>r \<in> {s. \<exists>n. s = x^\<^bsup>R n\<^esup>}\<rbrakk> \<Longrightarrow> mul_closed_set R {s. \<exists>n. s = x^\<^bsup>R n\<^esup>}
 3. \<And>x I. \<lbrakk>\<not> zeroring R; \<forall>xa. prime_ideal R xa \<longrightarrow> x \<in> xa; x \<notin> nilrad R; maximal_ideal R I; prime_ideal R I; x \<in> I; ideal R I; x \<in> carrier R\<rbrakk> \<Longrightarrow> \<zero> \<notin> {s. \<exists>n. s = x^\<^bsup>R n\<^esup>} \<and> 1\<^sub>r \<in> {s. \<exists>n. s = x^\<^bsup>R n\<^esup>}
[PROOF STEP]
apply (cut_tac t = x in np_1[THEN sym], assumption, blast)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x I. \<lbrakk>\<not> zeroring R; \<forall>xa. prime_ideal R xa \<longrightarrow> x \<in> xa; x \<notin> nilrad R; maximal_ideal R I; prime_ideal R I; x \<in> I; ideal R I; x \<in> carrier R; \<zero> \<notin> {s. \<exists>n. s = x^\<^bsup>R n\<^esup>} \<and> 1\<^sub>r \<in> {s. \<exists>n. s = x^\<^bsup>R n\<^esup>}\<rbrakk> \<Longrightarrow> mul_closed_set R {s. \<exists>n. s = x^\<^bsup>R n\<^esup>}
 2. \<And>x I. \<lbrakk>\<not> zeroring R; \<forall>xa. prime_ideal R xa \<longrightarrow> x \<in> xa; x \<notin> nilrad R; maximal_ideal R I; prime_ideal R I; x \<in> I; ideal R I; x \<in> carrier R\<rbrakk> \<Longrightarrow> \<zero> \<notin> {s. \<exists>n. s = x^\<^bsup>R n\<^esup>} \<and> 1\<^sub>r \<in> {s. \<exists>n. s = x^\<^bsup>R n\<^esup>}
[PROOF STEP]
apply (thin_tac "\<zero> \<notin> {s. \<exists>n. s = x^\<^bsup>R n\<^esup>} \<and> 1\<^sub>r \<in> {s. \<exists>n. s = x^\<^bsup>R n\<^esup>}",
       thin_tac "\<forall>xa. prime_ideal R xa \<longrightarrow> x \<in> xa")
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x I. \<lbrakk>\<not> zeroring R; x \<notin> nilrad R; maximal_ideal R I; prime_ideal R I; x \<in> I; ideal R I; x \<in> carrier R\<rbrakk> \<Longrightarrow> mul_closed_set R {s. \<exists>n. s = x^\<^bsup>R n\<^esup>}
 2. \<And>x I. \<lbrakk>\<not> zeroring R; \<forall>xa. prime_ideal R xa \<longrightarrow> x \<in> xa; x \<notin> nilrad R; maximal_ideal R I; prime_ideal R I; x \<in> I; ideal R I; x \<in> carrier R\<rbrakk> \<Longrightarrow> \<zero> \<notin> {s. \<exists>n. s = x^\<^bsup>R n\<^esup>} \<and> 1\<^sub>r \<in> {s. \<exists>n. s = x^\<^bsup>R n\<^esup>}
[PROOF STEP]
apply (subst mul_closed_set_def)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x I. \<lbrakk>\<not> zeroring R; x \<notin> nilrad R; maximal_ideal R I; prime_ideal R I; x \<in> I; ideal R I; x \<in> carrier R\<rbrakk> \<Longrightarrow> {s. \<exists>n. s = x^\<^bsup>R n\<^esup>} \<subseteq> carrier R \<and> (\<forall>s\<in>{s. \<exists>n. s = x^\<^bsup>R n\<^esup>}. \<forall>t\<in>{s. \<exists>n. s = x^\<^bsup>R n\<^esup>}. s \<cdot>\<^sub>r t \<in> {s. \<exists>n. s = x^\<^bsup>R n\<^esup>})
 2. \<And>x I. \<lbrakk>\<not> zeroring R; \<forall>xa. prime_ideal R xa \<longrightarrow> x \<in> xa; x \<notin> nilrad R; maximal_ideal R I; prime_ideal R I; x \<in> I; ideal R I; x \<in> carrier R\<rbrakk> \<Longrightarrow> \<zero> \<notin> {s. \<exists>n. s = x^\<^bsup>R n\<^esup>} \<and> 1\<^sub>r \<in> {s. \<exists>n. s = x^\<^bsup>R n\<^esup>}
[PROOF STEP]
apply (rule conjI)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>x I. \<lbrakk>\<not> zeroring R; x \<notin> nilrad R; maximal_ideal R I; prime_ideal R I; x \<in> I; ideal R I; x \<in> carrier R\<rbrakk> \<Longrightarrow> {s. \<exists>n. s = x^\<^bsup>R n\<^esup>} \<subseteq> carrier R
 2. \<And>x I. \<lbrakk>\<not> zeroring R; x \<notin> nilrad R; maximal_ideal R I; prime_ideal R I; x \<in> I; ideal R I; x \<in> carrier R\<rbrakk> \<Longrightarrow> \<forall>s\<in>{s. \<exists>n. s = x^\<^bsup>R n\<^esup>}. \<forall>t\<in>{s. \<exists>n. s = x^\<^bsup>R n\<^esup>}. s \<cdot>\<^sub>r t \<in> {s. \<exists>n. s = x^\<^bsup>R n\<^esup>}
 3. \<And>x I. \<lbrakk>\<not> zeroring R; \<forall>xa. prime_ideal R xa \<longrightarrow> x \<in> xa; x \<notin> nilrad R; maximal_ideal R I; prime_ideal R I; x \<in> I; ideal R I; x \<in> carrier R\<rbrakk> \<Longrightarrow> \<zero> \<notin> {s. \<exists>n. s = x^\<^bsup>R n\<^esup>} \<and> 1\<^sub>r \<in> {s. \<exists>n. s = x^\<^bsup>R n\<^esup>}
[PROOF STEP]
apply (rule subsetI, simp, erule exE)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>x I xa n. \<lbrakk>\<not> zeroring R; x \<notin> nilrad R; maximal_ideal R I; prime_ideal R I; x \<in> I; ideal R I; x \<in> carrier R; xa = x^\<^bsup>R n\<^esup>\<rbrakk> \<Longrightarrow> xa \<in> carrier R
 2. \<And>x I. \<lbrakk>\<not> zeroring R; x \<notin> nilrad R; maximal_ideal R I; prime_ideal R I; x \<in> I; ideal R I; x \<in> carrier R\<rbrakk> \<Longrightarrow> \<forall>s\<in>{s. \<exists>n. s = x^\<^bsup>R n\<^esup>}. \<forall>t\<in>{s. \<exists>n. s = x^\<^bsup>R n\<^esup>}. s \<cdot>\<^sub>r t \<in> {s. \<exists>n. s = x^\<^bsup>R n\<^esup>}
 3. \<And>x I. \<lbrakk>\<not> zeroring R; \<forall>xa. prime_ideal R xa \<longrightarrow> x \<in> xa; x \<notin> nilrad R; maximal_ideal R I; prime_ideal R I; x \<in> I; ideal R I; x \<in> carrier R\<rbrakk> \<Longrightarrow> \<zero> \<notin> {s. \<exists>n. s = x^\<^bsup>R n\<^esup>} \<and> 1\<^sub>r \<in> {s. \<exists>n. s = x^\<^bsup>R n\<^esup>}
[PROOF STEP]
apply (simp add:npClose)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x I. \<lbrakk>\<not> zeroring R; x \<notin> nilrad R; maximal_ideal R I; prime_ideal R I; x \<in> I; ideal R I; x \<in> carrier R\<rbrakk> \<Longrightarrow> \<forall>s\<in>{s. \<exists>n. s = x^\<^bsup>R n\<^esup>}. \<forall>t\<in>{s. \<exists>n. s = x^\<^bsup>R n\<^esup>}. s \<cdot>\<^sub>r t \<in> {s. \<exists>n. s = x^\<^bsup>R n\<^esup>}
 2. \<And>x I. \<lbrakk>\<not> zeroring R; \<forall>xa. prime_ideal R xa \<longrightarrow> x \<in> xa; x \<notin> nilrad R; maximal_ideal R I; prime_ideal R I; x \<in> I; ideal R I; x \<in> carrier R\<rbrakk> \<Longrightarrow> \<zero> \<notin> {s. \<exists>n. s = x^\<^bsup>R n\<^esup>} \<and> 1\<^sub>r \<in> {s. \<exists>n. s = x^\<^bsup>R n\<^esup>}
[PROOF STEP]
apply ((rule ballI)+, simp, (erule exE)+, simp)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x I s t n na. \<lbrakk>\<not> zeroring R; x \<notin> nilrad R; maximal_ideal R I; prime_ideal R I; x \<in> I; ideal R I; x \<in> carrier R; s = x^\<^bsup>R n\<^esup>; t = x^\<^bsup>R na\<^esup>\<rbrakk> \<Longrightarrow> \<exists>nb. x^\<^bsup>R n\<^esup> \<cdot>\<^sub>r x^\<^bsup>R na\<^esup> = x^\<^bsup>R nb\<^esup>
 2. \<And>x I. \<lbrakk>\<not> zeroring R; \<forall>xa. prime_ideal R xa \<longrightarrow> x \<in> xa; x \<notin> nilrad R; maximal_ideal R I; prime_ideal R I; x \<in> I; ideal R I; x \<in> carrier R\<rbrakk> \<Longrightarrow> \<zero> \<notin> {s. \<exists>n. s = x^\<^bsup>R n\<^esup>} \<and> 1\<^sub>r \<in> {s. \<exists>n. s = x^\<^bsup>R n\<^esup>}
[PROOF STEP]
apply (simp add:npMulDistr, blast)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x I. \<lbrakk>\<not> zeroring R; \<forall>xa. prime_ideal R xa \<longrightarrow> x \<in> xa; x \<notin> nilrad R; maximal_ideal R I; prime_ideal R I; x \<in> I; ideal R I; x \<in> carrier R\<rbrakk> \<Longrightarrow> \<zero> \<notin> {s. \<exists>n. s = x^\<^bsup>R n\<^esup>} \<and> 1\<^sub>r \<in> {s. \<exists>n. s = x^\<^bsup>R n\<^esup>}
[PROOF STEP]
apply (rule conjI)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x I. \<lbrakk>\<not> zeroring R; \<forall>xa. prime_ideal R xa \<longrightarrow> x \<in> xa; x \<notin> nilrad R; maximal_ideal R I; prime_ideal R I; x \<in> I; ideal R I; x \<in> carrier R\<rbrakk> \<Longrightarrow> \<zero> \<notin> {s. \<exists>n. s = x^\<^bsup>R n\<^esup>}
 2. \<And>x I. \<lbrakk>\<not> zeroring R; \<forall>xa. prime_ideal R xa \<longrightarrow> x \<in> xa; x \<notin> nilrad R; maximal_ideal R I; prime_ideal R I; x \<in> I; ideal R I; x \<in> carrier R\<rbrakk> \<Longrightarrow> 1\<^sub>r \<in> {s. \<exists>n. s = x^\<^bsup>R n\<^esup>}
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x I. \<lbrakk>\<not> zeroring R; \<forall>xa. prime_ideal R xa \<longrightarrow> x \<in> xa; x \<notin> nilrad R; maximal_ideal R I; prime_ideal R I; ideal R I; x \<in> carrier R\<rbrakk> \<Longrightarrow> \<forall>n. \<zero> \<noteq> x^\<^bsup>R n\<^esup>
 2. \<And>x I. \<lbrakk>\<not> zeroring R; \<forall>xa. prime_ideal R xa \<longrightarrow> x \<in> xa; x \<notin> nilrad R; maximal_ideal R I; prime_ideal R I; x \<in> I; ideal R I; x \<in> carrier R\<rbrakk> \<Longrightarrow> 1\<^sub>r \<in> {s. \<exists>n. s = x^\<^bsup>R n\<^esup>}
[PROOF STEP]
apply (rule contrapos_pp, simp+, erule exE)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x I n. \<lbrakk>\<not> zeroring R; \<forall>xa. prime_ideal R xa \<longrightarrow> x \<in> xa; x \<notin> nilrad R; maximal_ideal R I; prime_ideal R I; ideal R I; x \<in> carrier R; \<zero> = x^\<^bsup>R n\<^esup>\<rbrakk> \<Longrightarrow> False
 2. \<And>x I. \<lbrakk>\<not> zeroring R; \<forall>xa. prime_ideal R xa \<longrightarrow> x \<in> xa; x \<notin> nilrad R; maximal_ideal R I; prime_ideal R I; x \<in> I; ideal R I; x \<in> carrier R\<rbrakk> \<Longrightarrow> 1\<^sub>r \<in> {s. \<exists>n. s = x^\<^bsup>R n\<^esup>}
[PROOF STEP]
apply (frule sym, thin_tac "\<zero> = x^\<^bsup>R n\<^esup>")
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x I n. \<lbrakk>\<not> zeroring R; \<forall>xa. prime_ideal R xa \<longrightarrow> x \<in> xa; x \<notin> nilrad R; maximal_ideal R I; prime_ideal R I; ideal R I; x \<in> carrier R; x^\<^bsup>R n\<^esup> = \<zero>\<rbrakk> \<Longrightarrow> False
 2. \<And>x I. \<lbrakk>\<not> zeroring R; \<forall>xa. prime_ideal R xa \<longrightarrow> x \<in> xa; x \<notin> nilrad R; maximal_ideal R I; prime_ideal R I; x \<in> I; ideal R I; x \<in> carrier R\<rbrakk> \<Longrightarrow> 1\<^sub>r \<in> {s. \<exists>n. s = x^\<^bsup>R n\<^esup>}
[PROOF STEP]
apply (simp add:nilrad_def nilpotent_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x I. \<lbrakk>\<not> zeroring R; \<forall>xa. prime_ideal R xa \<longrightarrow> x \<in> xa; x \<notin> nilrad R; maximal_ideal R I; prime_ideal R I; x \<in> I; ideal R I; x \<in> carrier R\<rbrakk> \<Longrightarrow> 1\<^sub>r \<in> {s. \<exists>n. s = x^\<^bsup>R n\<^esup>}
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x I. \<lbrakk>\<not> zeroring R; \<forall>xa. prime_ideal R xa \<longrightarrow> x \<in> xa; x \<notin> nilrad R; maximal_ideal R I; prime_ideal R I; ideal R I; x \<in> carrier R\<rbrakk> \<Longrightarrow> \<exists>n. 1\<^sub>r = x^\<^bsup>R n\<^esup>
[PROOF STEP]
apply (cut_tac x1 = x in npow_0[THEN sym, of "R"], blast)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma (in Ring) nonilp_residue_nilrad:"\<lbrakk>\<not> zeroring R; x \<in> carrier R;
        nilpotent (qring R (nilrad R)) (x \<uplus>\<^bsub>R\<^esub> (nilrad R))\<rbrakk> \<Longrightarrow>
                   x \<uplus>\<^bsub>R\<^esub> (nilrad R) = \<zero>\<^bsub>(qring R (nilrad R))\<^esub>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<not> zeroring R; x \<in> carrier R; nilpotent (R /\<^sub>r nilrad R) (x \<uplus>\<^bsub>R\<^esub> nilrad R)\<rbrakk> \<Longrightarrow> x \<uplus>\<^bsub>R\<^esub> nilrad R = \<zero>\<^bsub>R /\<^sub>r nilrad R\<^esub>
[PROOF STEP]
apply (simp add:nilpotent_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<not> zeroring R; x \<in> carrier R; \<exists>n. (x \<uplus>\<^bsub>R\<^esub> nilrad R)^\<^bsup>R /\<^sub>r nilrad R n\<^esup> = \<zero>\<^bsub>R /\<^sub>r nilrad R\<^esub>\<rbrakk> \<Longrightarrow> x \<uplus>\<^bsub>R\<^esub> nilrad R = \<zero>\<^bsub>R /\<^sub>r nilrad R\<^esub>
[PROOF STEP]
apply (erule exE)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>n. \<lbrakk>\<not> zeroring R; x \<in> carrier R; (x \<uplus>\<^bsub>R\<^esub> nilrad R)^\<^bsup>R /\<^sub>r nilrad R n\<^esup> = \<zero>\<^bsub>R /\<^sub>r nilrad R\<^esub>\<rbrakk> \<Longrightarrow> x \<uplus>\<^bsub>R\<^esub> nilrad R = \<zero>\<^bsub>R /\<^sub>r nilrad R\<^esub>
[PROOF STEP]
apply (cut_tac id_nilrad_ideal)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>n. \<lbrakk>\<not> zeroring R; x \<in> carrier R; (x \<uplus>\<^bsub>R\<^esub> nilrad R)^\<^bsup>R /\<^sub>r nilrad R n\<^esup> = \<zero>\<^bsub>R /\<^sub>r nilrad R\<^esub>; ideal R (nilrad R)\<rbrakk> \<Longrightarrow> x \<uplus>\<^bsub>R\<^esub> nilrad R = \<zero>\<^bsub>R /\<^sub>r nilrad R\<^esub>
[PROOF STEP]
apply (simp add:qring_zero)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>n. \<lbrakk>\<not> zeroring R; x \<in> carrier R; (x \<uplus>\<^bsub>R\<^esub> nilrad R)^\<^bsup>R /\<^sub>r nilrad R n\<^esup> = nilrad R; ideal R (nilrad R)\<rbrakk> \<Longrightarrow> x \<uplus>\<^bsub>R\<^esub> nilrad R = nilrad R
[PROOF STEP]
apply (cut_tac "Ring")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>n. \<lbrakk>\<not> zeroring R; x \<in> carrier R; (x \<uplus>\<^bsub>R\<^esub> nilrad R)^\<^bsup>R /\<^sub>r nilrad R n\<^esup> = nilrad R; ideal R (nilrad R); Ring R\<rbrakk> \<Longrightarrow> x \<uplus>\<^bsub>R\<^esub> nilrad R = nilrad R
[PROOF STEP]
apply (simp add:npQring)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>n. \<lbrakk>\<not> zeroring R; x \<in> carrier R; x^\<^bsup>R n\<^esup> \<uplus>\<^bsub>R\<^esub> nilrad R = nilrad R; ideal R (nilrad R); Ring R\<rbrakk> \<Longrightarrow> x \<uplus>\<^bsub>R\<^esub> nilrad R = nilrad R
[PROOF STEP]
apply (frule_tac x = x and n = n in npClose)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>n. \<lbrakk>\<not> zeroring R; x \<in> carrier R; x^\<^bsup>R n\<^esup> \<uplus>\<^bsub>R\<^esub> nilrad R = nilrad R; ideal R (nilrad R); Ring R; x^\<^bsup>R n\<^esup> \<in> carrier R\<rbrakk> \<Longrightarrow> x \<uplus>\<^bsub>R\<^esub> nilrad R = nilrad R
[PROOF STEP]
apply (frule_tac I = "nilrad R" and a = "x^\<^bsup>R n\<^esup>" in ar_coset_same3,
             assumption+)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>n. \<lbrakk>\<not> zeroring R; x \<in> carrier R; x^\<^bsup>R n\<^esup> \<uplus>\<^bsub>R\<^esub> nilrad R = nilrad R; ideal R (nilrad R); Ring R; x^\<^bsup>R n\<^esup> \<in> carrier R; x^\<^bsup>R n\<^esup> \<in> nilrad R\<rbrakk> \<Longrightarrow> x \<uplus>\<^bsub>R\<^esub> nilrad R = nilrad R
[PROOF STEP]
apply (rule_tac I = "nilrad R" and a = x in ar_coset_same4, assumption)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>n. \<lbrakk>\<not> zeroring R; x \<in> carrier R; x^\<^bsup>R n\<^esup> \<uplus>\<^bsub>R\<^esub> nilrad R = nilrad R; ideal R (nilrad R); Ring R; x^\<^bsup>R n\<^esup> \<in> carrier R; x^\<^bsup>R n\<^esup> \<in> nilrad R\<rbrakk> \<Longrightarrow> x \<in> nilrad R
[PROOF STEP]
apply (thin_tac "x^\<^bsup>R n\<^esup> \<uplus>\<^bsub>R\<^esub> nilrad R = nilrad R",
        simp add:nilrad_def nilpotent_def, erule exE)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>n na. \<lbrakk>\<not> zeroring R; x \<in> carrier R; ideal R {x \<in> carrier R. \<exists>n. x^\<^bsup>R n\<^esup> = \<zero>}; Ring R; x^\<^bsup>R n\<^esup> \<in> carrier R; x^\<^bsup>R n\<^esup>^\<^bsup>R na\<^esup> = \<zero>\<rbrakk> \<Longrightarrow> \<exists>n. x^\<^bsup>R n\<^esup> = \<zero>
[PROOF STEP]
apply (simp add:npMulExp, blast)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done