[STATEMENT]
lemma (in Ring) nprod_mem:"\<lbrakk>\<forall>i \<le> n. f i \<in> carrier R; l \<le> n\<rbrakk> \<Longrightarrow>
                              nprod R f l \<in> carrier R"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<forall>i\<le>n. f i \<in> carrier R; l \<le> n\<rbrakk> \<Longrightarrow> e\<Pi>\<^bsub>R,l\<^esub> f \<in> carrier R
[PROOF STEP]
by (simp add:nprod_memTr)


[STATEMENT]
lemma (in Ring) ideal_nprod_incTr:"ideal R A \<Longrightarrow>
                (\<forall>i \<le> n. f i \<in> carrier R) \<and>
                             (\<exists>l \<le> n. f l \<in> A) \<longrightarrow> nprod R f n \<in> A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ideal R A \<Longrightarrow> (\<forall>i\<le>n. f i \<in> carrier R) \<and> (\<exists>l\<le>n. f l \<in> A) \<longrightarrow> e\<Pi>\<^bsub>R,n\<^esub> f \<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> carrier R) \<and> (\<exists>l\<le>0. f l \<in> A) \<longrightarrow> e\<Pi>\<^bsub>R,0\<^esub> f \<in> A
 2. \<And>n. \<lbrakk>ideal R A; (\<forall>i\<le>n. f i \<in> carrier R) \<and> (\<exists>l\<le>n. f l \<in> A) \<longrightarrow> e\<Pi>\<^bsub>R,n\<^esub> f \<in> A\<rbrakk> \<Longrightarrow> (\<forall>i\<le>Suc n. f i \<in> carrier R) \<and> (\<exists>l\<le>Suc n. f l \<in> A) \<longrightarrow> e\<Pi>\<^bsub>R,Suc n\<^esub> f \<in> 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>l\<le>0. f l \<in> A) \<longrightarrow> e\<Pi>\<^bsub>R,0\<^esub> f \<in> A
 2. \<And>n. \<lbrakk>ideal R A; (\<forall>i\<le>n. f i \<in> carrier R) \<and> (\<exists>l\<le>n. f l \<in> A) \<longrightarrow> e\<Pi>\<^bsub>R,n\<^esub> f \<in> A\<rbrakk> \<Longrightarrow> (\<forall>i\<le>Suc n. f i \<in> carrier R) \<and> (\<exists>l\<le>Suc n. f l \<in> A) \<longrightarrow> e\<Pi>\<^bsub>R,Suc n\<^esub> f \<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> carrier R) \<and> (\<exists>l\<le>n. f l \<in> A) \<longrightarrow> e\<Pi>\<^bsub>R,n\<^esub> f \<in> A\<rbrakk> \<Longrightarrow> (\<forall>i\<le>Suc n. f i \<in> carrier R) \<and> (\<exists>l\<le>Suc n. f l \<in> A) \<longrightarrow> e\<Pi>\<^bsub>R,Suc n\<^esub> f \<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> carrier R) \<and> (\<exists>l\<le>n. f l \<in> A) \<longrightarrow> e\<Pi>\<^bsub>R,n\<^esub> f \<in> A\<rbrakk> \<Longrightarrow> (\<forall>i\<le>Suc n. f i \<in> carrier R) \<and> (\<exists>l\<le>Suc n. f l \<in> A) \<longrightarrow> e\<Pi>\<^bsub>R,Suc n\<^esub> f \<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> carrier R) \<and> (\<exists>l\<le>n. f l \<in> A) \<longrightarrow> e\<Pi>\<^bsub>R,n\<^esub> f \<in> A; (\<forall>i\<le>Suc n. f i \<in> carrier R) \<and> (\<exists>l\<le>Suc n. f l \<in> A)\<rbrakk> \<Longrightarrow> e\<Pi>\<^bsub>R,Suc n\<^esub> f \<in> 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>l\<le>n. f l \<in> A) \<longrightarrow> e\<Pi>\<^bsub>R,n\<^esub> f \<in> A; \<forall>i\<le>Suc n. f i \<in> carrier R; \<exists>l\<le>Suc n. f l \<in> A\<rbrakk> \<Longrightarrow> e\<Pi>\<^bsub>R,Suc n\<^esub> f \<in> A
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>n. \<lbrakk>ideal R A; (\<exists>l\<le>n. f l \<in> A) \<longrightarrow> e\<Pi>\<^bsub>R,n\<^esub> f \<in> A; \<forall>i\<le>Suc n. f i \<in> carrier R; \<exists>l\<le>Suc n. f l \<in> A\<rbrakk> \<Longrightarrow> e\<Pi>\<^bsub>R,n\<^esub> f \<cdot>\<^sub>r f (Suc n) \<in> A
[PROOF STEP]
apply (erule exE)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>n l. \<lbrakk>ideal R A; (\<exists>l\<le>n. f l \<in> A) \<longrightarrow> e\<Pi>\<^bsub>R,n\<^esub> f \<in> A; \<forall>i\<le>Suc n. f i \<in> carrier R; l \<le> Suc n \<and> f l \<in> A\<rbrakk> \<Longrightarrow> e\<Pi>\<^bsub>R,n\<^esub> f \<cdot>\<^sub>r f (Suc n) \<in> A
[PROOF STEP]
apply (case_tac "l = Suc n", simp)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>n l. \<lbrakk>ideal R A; (\<exists>l\<le>n. f l \<in> A) \<longrightarrow> e\<Pi>\<^bsub>R,n\<^esub> f \<in> A; \<forall>i\<le>Suc n. f i \<in> carrier R; f (Suc n) \<in> A; l = Suc n\<rbrakk> \<Longrightarrow> e\<Pi>\<^bsub>R,n\<^esub> f \<cdot>\<^sub>r f (Suc n) \<in> A
 2. \<And>n l. \<lbrakk>ideal R A; (\<exists>l\<le>n. f l \<in> A) \<longrightarrow> e\<Pi>\<^bsub>R,n\<^esub> f \<in> A; \<forall>i\<le>Suc n. f i \<in> carrier R; l \<le> Suc n \<and> f l \<in> A; l \<noteq> Suc n\<rbrakk> \<Longrightarrow> e\<Pi>\<^bsub>R,n\<^esub> f \<cdot>\<^sub>r f (Suc n) \<in> A
[PROOF STEP]
apply (rule_tac x = "f (Suc n)" and r = "nprod R f n" in
                 ideal_ring_multiple[of "A"], assumption+)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>n l. \<lbrakk>ideal R A; (\<exists>l\<le>n. f l \<in> A) \<longrightarrow> e\<Pi>\<^bsub>R,n\<^esub> f \<in> A; \<forall>i\<le>Suc n. f i \<in> carrier R; f (Suc n) \<in> A; l = Suc n\<rbrakk> \<Longrightarrow> e\<Pi>\<^bsub>R,n\<^esub> f \<in> carrier R
 2. \<And>n l. \<lbrakk>ideal R A; (\<exists>l\<le>n. f l \<in> A) \<longrightarrow> e\<Pi>\<^bsub>R,n\<^esub> f \<in> A; \<forall>i\<le>Suc n. f i \<in> carrier R; l \<le> Suc n \<and> f l \<in> A; l \<noteq> Suc n\<rbrakk> \<Longrightarrow> e\<Pi>\<^bsub>R,n\<^esub> f \<cdot>\<^sub>r f (Suc n) \<in> A
[PROOF STEP]
apply (rule_tac n = "Suc n" and f = f and l = n in nprod_mem,
                 assumption+, simp)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>n l. \<lbrakk>ideal R A; (\<exists>l\<le>n. f l \<in> A) \<longrightarrow> e\<Pi>\<^bsub>R,n\<^esub> f \<in> A; \<forall>i\<le>Suc n. f i \<in> carrier R; l \<le> Suc n \<and> f l \<in> A; l \<noteq> Suc n\<rbrakk> \<Longrightarrow> e\<Pi>\<^bsub>R,n\<^esub> f \<cdot>\<^sub>r f (Suc n) \<in> A
[PROOF STEP]
apply (erule conjE)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>n l. \<lbrakk>ideal R A; (\<exists>l\<le>n. f l \<in> A) \<longrightarrow> e\<Pi>\<^bsub>R,n\<^esub> f \<in> A; \<forall>i\<le>Suc n. f i \<in> carrier R; l \<noteq> Suc n; l \<le> Suc n; f l \<in> A\<rbrakk> \<Longrightarrow> e\<Pi>\<^bsub>R,n\<^esub> f \<cdot>\<^sub>r f (Suc n) \<in> A
[PROOF STEP]
apply (frule_tac m = l and n = "Suc n" in noteq_le_less, assumption,
       frule_tac x = l and n = "Suc n" in less_le_diff,
       thin_tac "l \<le> Suc n", thin_tac "l < Suc n", simp)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>n l. \<lbrakk>ideal R A; (\<exists>l\<le>n. f l \<in> A) \<longrightarrow> e\<Pi>\<^bsub>R,n\<^esub> f \<in> A; \<forall>i\<le>Suc n. f i \<in> carrier R; f l \<in> A; l \<le> n\<rbrakk> \<Longrightarrow> e\<Pi>\<^bsub>R,n\<^esub> f \<cdot>\<^sub>r f (Suc n) \<in> A
[PROOF STEP]
apply (rule_tac x = "nprod R f n" and r = "f (Suc n)" in
                      ideal_ring_multiple1[of "A"], assumption+)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>n l. \<lbrakk>ideal R A; (\<exists>l\<le>n. f l \<in> A) \<longrightarrow> e\<Pi>\<^bsub>R,n\<^esub> f \<in> A; \<forall>i\<le>Suc n. f i \<in> carrier R; f l \<in> A; l \<le> n\<rbrakk> \<Longrightarrow> e\<Pi>\<^bsub>R,n\<^esub> f \<in> A
 2. \<And>n l. \<lbrakk>ideal R A; (\<exists>l\<le>n. f l \<in> A) \<longrightarrow> e\<Pi>\<^bsub>R,n\<^esub> f \<in> A; \<forall>i\<le>Suc n. f i \<in> carrier R; f l \<in> A; l \<le> n\<rbrakk> \<Longrightarrow> f (Suc n) \<in> carrier R
[PROOF STEP]
apply blast
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>n l. \<lbrakk>ideal R A; (\<exists>l\<le>n. f l \<in> A) \<longrightarrow> e\<Pi>\<^bsub>R,n\<^esub> f \<in> A; \<forall>i\<le>Suc n. f i \<in> carrier R; f l \<in> A; l \<le> n\<rbrakk> \<Longrightarrow> f (Suc n) \<in> carrier R
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma (in Ring) ideal_nprod_inc:"\<lbrakk>ideal R A; \<forall>i \<le> n. f i \<in> carrier R;
                \<exists>l \<le> n. f l \<in> A\<rbrakk> \<Longrightarrow> nprod R f n \<in> A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ideal R A; \<forall>i\<le>n. f i \<in> carrier R; \<exists>l\<le>n. f l \<in> A\<rbrakk> \<Longrightarrow> e\<Pi>\<^bsub>R,n\<^esub> f \<in> A
[PROOF STEP]
by (simp add:ideal_nprod_incTr)


[STATEMENT]
lemma (in Ring) nprod_excTr:"prime_ideal R P \<Longrightarrow>
          (\<forall>i \<le> n. f i \<in> carrier R) \<and> (\<forall>l \<le> n. f l \<notin> P) \<longrightarrow>
                                                     nprod R f n \<notin> P"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. prime_ideal R P \<Longrightarrow> (\<forall>i\<le>n. f i \<in> carrier R) \<and> (\<forall>l\<le>n. f l \<notin> P) \<longrightarrow> e\<Pi>\<^bsub>R,n\<^esub> f \<notin> P
[PROOF STEP]
apply (induct_tac n)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. prime_ideal R P \<Longrightarrow> (\<forall>i\<le>0. f i \<in> carrier R) \<and> (\<forall>l\<le>0. f l \<notin> P) \<longrightarrow> e\<Pi>\<^bsub>R,0\<^esub> f \<notin> P
 2. \<And>n. \<lbrakk>prime_ideal R P; (\<forall>i\<le>n. f i \<in> carrier R) \<and> (\<forall>l\<le>n. f l \<notin> P) \<longrightarrow> e\<Pi>\<^bsub>R,n\<^esub> f \<notin> P\<rbrakk> \<Longrightarrow> (\<forall>i\<le>Suc n. f i \<in> carrier R) \<and> (\<forall>l\<le>Suc n. f l \<notin> P) \<longrightarrow> e\<Pi>\<^bsub>R,Suc n\<^esub> f \<notin> P
[PROOF STEP]
(** n = 0 **)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. prime_ideal R P \<Longrightarrow> (\<forall>i\<le>0. f i \<in> carrier R) \<and> (\<forall>l\<le>0. f l \<notin> P) \<longrightarrow> e\<Pi>\<^bsub>R,0\<^esub> f \<notin> P
 2. \<And>n. \<lbrakk>prime_ideal R P; (\<forall>i\<le>n. f i \<in> carrier R) \<and> (\<forall>l\<le>n. f l \<notin> P) \<longrightarrow> e\<Pi>\<^bsub>R,n\<^esub> f \<notin> P\<rbrakk> \<Longrightarrow> (\<forall>i\<le>Suc n. f i \<in> carrier R) \<and> (\<forall>l\<le>Suc n. f l \<notin> P) \<longrightarrow> e\<Pi>\<^bsub>R,Suc n\<^esub> f \<notin> P
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>n. \<lbrakk>prime_ideal R P; (\<forall>i\<le>n. f i \<in> carrier R) \<and> (\<forall>l\<le>n. f l \<notin> P) \<longrightarrow> e\<Pi>\<^bsub>R,n\<^esub> f \<notin> P\<rbrakk> \<Longrightarrow> (\<forall>i\<le>Suc n. f i \<in> carrier R) \<and> (\<forall>l\<le>Suc n. f l \<notin> P) \<longrightarrow> e\<Pi>\<^bsub>R,Suc n\<^esub> f \<notin> P
[PROOF STEP]
(* n = 0 done *)
(** n **)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>n. \<lbrakk>prime_ideal R P; (\<forall>i\<le>n. f i \<in> carrier R) \<and> (\<forall>l\<le>n. f l \<notin> P) \<longrightarrow> e\<Pi>\<^bsub>R,n\<^esub> f \<notin> P\<rbrakk> \<Longrightarrow> (\<forall>i\<le>Suc n. f i \<in> carrier R) \<and> (\<forall>l\<le>Suc n. f l \<notin> P) \<longrightarrow> e\<Pi>\<^bsub>R,Suc n\<^esub> f \<notin> P
[PROOF STEP]
apply (rule impI)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>n. \<lbrakk>prime_ideal R P; (\<forall>i\<le>n. f i \<in> carrier R) \<and> (\<forall>l\<le>n. f l \<notin> P) \<longrightarrow> e\<Pi>\<^bsub>R,n\<^esub> f \<notin> P; (\<forall>i\<le>Suc n. f i \<in> carrier R) \<and> (\<forall>l\<le>Suc n. f l \<notin> P)\<rbrakk> \<Longrightarrow> e\<Pi>\<^bsub>R,Suc n\<^esub> f \<notin> P
[PROOF STEP]
apply (erule conjE)+
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>n. \<lbrakk>prime_ideal R P; (\<forall>i\<le>n. f i \<in> carrier R) \<and> (\<forall>l\<le>n. f l \<notin> P) \<longrightarrow> e\<Pi>\<^bsub>R,n\<^esub> f \<notin> P; \<forall>i\<le>Suc n. f i \<in> carrier R; \<forall>l\<le>Suc n. f l \<notin> P\<rbrakk> \<Longrightarrow> e\<Pi>\<^bsub>R,Suc n\<^esub> f \<notin> P
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>n. \<lbrakk>prime_ideal R P; e\<Pi>\<^bsub>R,n\<^esub> f \<notin> P; \<forall>i\<le>Suc n. f i \<in> carrier R; \<forall>l\<le>Suc n. f l \<notin> P\<rbrakk> \<Longrightarrow> e\<Pi>\<^bsub>R,n\<^esub> f \<cdot>\<^sub>r f (Suc n) \<notin> P
[PROOF STEP]
apply (rule_tac y = "f (Suc n)" and x = "nprod R f n" in
          prime_elems_mult_not[of "P"], assumption,
         rule_tac n = n in  nprod_mem, rule allI, simp+)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma (in Ring) prime_nprod_exc:"\<lbrakk>prime_ideal R P; \<forall>i \<le> n. f i \<in> carrier R;
                \<forall>l \<le> n. f l \<notin> P\<rbrakk> \<Longrightarrow> nprod R f n \<notin> P"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>prime_ideal R P; \<forall>i\<le>n. f i \<in> carrier R; \<forall>l\<le>n. f l \<notin> P\<rbrakk> \<Longrightarrow> e\<Pi>\<^bsub>R,n\<^esub> f \<notin> P
[PROOF STEP]
by (simp add:nprod_excTr)


[STATEMENT]
lemma (in Ring) id_nilrad_ideal:"ideal R (nilrad R)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ideal R (nilrad R)
[PROOF STEP]
apply (cut_tac ring_is_ag)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. aGroup R \<Longrightarrow> ideal R (nilrad R)
[PROOF STEP]
apply (rule ideal_condition1[of "nilrad R"])
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. aGroup R \<Longrightarrow> nilrad R \<subseteq> carrier R
 2. aGroup R \<Longrightarrow> nilrad R \<noteq> {}
 3. aGroup R \<Longrightarrow> \<forall>x\<in>nilrad R. \<forall>y\<in>nilrad R. x \<plusminus> y \<in> nilrad R
 4. aGroup R \<Longrightarrow> \<forall>r\<in>carrier R. \<forall>x\<in>nilrad R. r \<cdot>\<^sub>r x \<in> nilrad R
[PROOF STEP]
apply (rule subsetI)
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<And>x. \<lbrakk>aGroup R; x \<in> nilrad R\<rbrakk> \<Longrightarrow> x \<in> carrier R
 2. aGroup R \<Longrightarrow> nilrad R \<noteq> {}
 3. aGroup R \<Longrightarrow> \<forall>x\<in>nilrad R. \<forall>y\<in>nilrad R. x \<plusminus> y \<in> nilrad R
 4. aGroup R \<Longrightarrow> \<forall>r\<in>carrier R. \<forall>x\<in>nilrad R. r \<cdot>\<^sub>r x \<in> nilrad R
[PROOF STEP]
apply (simp add:nilrad_def CollectI)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. aGroup R \<Longrightarrow> nilrad R \<noteq> {}
 2. aGroup R \<Longrightarrow> \<forall>x\<in>nilrad R. \<forall>y\<in>nilrad R. x \<plusminus> y \<in> nilrad R
 3. aGroup R \<Longrightarrow> \<forall>r\<in>carrier R. \<forall>x\<in>nilrad R. r \<cdot>\<^sub>r x \<in> nilrad R
[PROOF STEP]
apply (simp add:nilrad_def)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. aGroup R \<Longrightarrow> \<exists>x. x \<in> carrier R \<and> nilpotent R x
 2. aGroup R \<Longrightarrow> \<forall>x\<in>nilrad R. \<forall>y\<in>nilrad R. x \<plusminus> y \<in> nilrad R
 3. aGroup R \<Longrightarrow> \<forall>r\<in>carrier R. \<forall>x\<in>nilrad R. r \<cdot>\<^sub>r x \<in> nilrad R
[PROOF STEP]
apply (cut_tac ring_zero)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<lbrakk>aGroup R; \<zero> \<in> carrier R\<rbrakk> \<Longrightarrow> \<exists>x. x \<in> carrier R \<and> nilpotent R x
 2. aGroup R \<Longrightarrow> \<forall>x\<in>nilrad R. \<forall>y\<in>nilrad R. x \<plusminus> y \<in> nilrad R
 3. aGroup R \<Longrightarrow> \<forall>r\<in>carrier R. \<forall>x\<in>nilrad R. r \<cdot>\<^sub>r x \<in> nilrad R
[PROOF STEP]
apply (subgoal_tac "nilpotent R \<zero>")
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<lbrakk>aGroup R; \<zero> \<in> carrier R; nilpotent R \<zero>\<rbrakk> \<Longrightarrow> \<exists>x. x \<in> carrier R \<and> nilpotent R x
 2. \<lbrakk>aGroup R; \<zero> \<in> carrier R\<rbrakk> \<Longrightarrow> nilpotent R \<zero>
 3. aGroup R \<Longrightarrow> \<forall>x\<in>nilrad R. \<forall>y\<in>nilrad R. x \<plusminus> y \<in> nilrad R
 4. aGroup R \<Longrightarrow> \<forall>r\<in>carrier R. \<forall>x\<in>nilrad R. r \<cdot>\<^sub>r x \<in> nilrad R
[PROOF STEP]
apply blast
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<lbrakk>aGroup R; \<zero> \<in> carrier R\<rbrakk> \<Longrightarrow> nilpotent R \<zero>
 2. aGroup R \<Longrightarrow> \<forall>x\<in>nilrad R. \<forall>y\<in>nilrad R. x \<plusminus> y \<in> nilrad R
 3. aGroup R \<Longrightarrow> \<forall>r\<in>carrier R. \<forall>x\<in>nilrad R. r \<cdot>\<^sub>r x \<in> nilrad R
[PROOF STEP]
apply (simp add:nilpotent_def)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<lbrakk>aGroup R; \<zero> \<in> carrier R\<rbrakk> \<Longrightarrow> \<exists>n. \<zero>^\<^bsup>R n\<^esup> = \<zero>
 2. aGroup R \<Longrightarrow> \<forall>x\<in>nilrad R. \<forall>y\<in>nilrad R. x \<plusminus> y \<in> nilrad R
 3. aGroup R \<Longrightarrow> \<forall>r\<in>carrier R. \<forall>x\<in>nilrad R. r \<cdot>\<^sub>r x \<in> nilrad R
[PROOF STEP]
apply (frule np_1[of "\<zero>"], blast)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. aGroup R \<Longrightarrow> \<forall>x\<in>nilrad R. \<forall>y\<in>nilrad R. x \<plusminus> y \<in> nilrad R
 2. aGroup R \<Longrightarrow> \<forall>r\<in>carrier R. \<forall>x\<in>nilrad R. r \<cdot>\<^sub>r x \<in> nilrad R
[PROOF STEP]
apply (rule ballI)+
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x y. \<lbrakk>aGroup R; x \<in> nilrad R; y \<in> nilrad R\<rbrakk> \<Longrightarrow> x \<plusminus> y \<in> nilrad R
 2. aGroup R \<Longrightarrow> \<forall>r\<in>carrier R. \<forall>x\<in>nilrad R. r \<cdot>\<^sub>r x \<in> nilrad R
[PROOF STEP]
apply (simp add:nilrad_def nilpotent_def, (erule conjE)+)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x y. \<lbrakk>aGroup R; x \<in> carrier R; \<exists>n. x^\<^bsup>R n\<^esup> = \<zero>; y \<in> carrier R; \<exists>n. y^\<^bsup>R n\<^esup> = \<zero>\<rbrakk> \<Longrightarrow> x \<plusminus> y \<in> carrier R \<and> (\<exists>n. (x \<plusminus> y)^\<^bsup>R n\<^esup> = \<zero>)
 2. aGroup R \<Longrightarrow> \<forall>r\<in>carrier R. \<forall>x\<in>nilrad R. r \<cdot>\<^sub>r x \<in> nilrad R
[PROOF STEP]
apply (erule exE)+
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x y n na. \<lbrakk>aGroup R; x \<in> carrier R; y \<in> carrier R; x^\<^bsup>R n\<^esup> = \<zero>; y^\<^bsup>R na\<^esup> = \<zero>\<rbrakk> \<Longrightarrow> x \<plusminus> y \<in> carrier R \<and> (\<exists>n. (x \<plusminus> y)^\<^bsup>R n\<^esup> = \<zero>)
 2. aGroup R \<Longrightarrow> \<forall>r\<in>carrier R. \<forall>x\<in>nilrad R. r \<cdot>\<^sub>r x \<in> nilrad R
[PROOF STEP]
apply (simp add:aGroup.ag_pOp_closed[of "R"])
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x y n na. \<lbrakk>aGroup R; x \<in> carrier R; y \<in> carrier R; x^\<^bsup>R n\<^esup> = \<zero>; y^\<^bsup>R na\<^esup> = \<zero>\<rbrakk> \<Longrightarrow> \<exists>n. (x \<plusminus> y)^\<^bsup>R n\<^esup> = \<zero>
 2. aGroup R \<Longrightarrow> \<forall>r\<in>carrier R. \<forall>x\<in>nilrad R. r \<cdot>\<^sub>r x \<in> nilrad R
[PROOF STEP]
apply (frule_tac x = x and y = y and m = n and n = na in npAdd,
        assumption+, blast)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. aGroup R \<Longrightarrow> \<forall>r\<in>carrier R. \<forall>x\<in>nilrad R. r \<cdot>\<^sub>r x \<in> nilrad R
[PROOF STEP]
apply (rule ballI)+
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>r x. \<lbrakk>aGroup R; r \<in> carrier R; x \<in> nilrad R\<rbrakk> \<Longrightarrow> r \<cdot>\<^sub>r x \<in> nilrad R
[PROOF STEP]
apply (simp add:nilrad_def nilpotent_def, erule conjE, erule exE)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>r x n. \<lbrakk>aGroup R; r \<in> carrier R; x \<in> carrier R; x^\<^bsup>R n\<^esup> = \<zero>\<rbrakk> \<Longrightarrow> r \<cdot>\<^sub>r x \<in> carrier R \<and> (\<exists>n. (r \<cdot>\<^sub>r x)^\<^bsup>R n\<^esup> = \<zero>)
[PROOF STEP]
apply (simp add:ring_tOp_closed,
        frule_tac x = r and y = x and n = n in npMul, assumption+,
           simp,
        frule_tac x = r and n = n in npClose)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>r x n. \<lbrakk>aGroup R; r \<in> carrier R; x \<in> carrier R; x^\<^bsup>R n\<^esup> = \<zero>; (r \<cdot>\<^sub>r x)^\<^bsup>R n\<^esup> = r^\<^bsup>R n\<^esup> \<cdot>\<^sub>r \<zero>; r^\<^bsup>R n\<^esup> \<in> carrier R\<rbrakk> \<Longrightarrow> \<exists>n. (r \<cdot>\<^sub>r x)^\<^bsup>R n\<^esup> = \<zero>
[PROOF STEP]
apply (simp add:ring_times_x_0, blast)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma (in Ring) id_rad_invim:"ideal R I \<Longrightarrow>
       rad_ideal R I = (rInvim R (qring R I) (pj R I ) (nilrad (qring R I)))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ideal R I \<Longrightarrow> rad_ideal R I = rInvim R (R /\<^sub>r I) (pj R I) (nilrad (R /\<^sub>r I))
[PROOF STEP]
apply (cut_tac ring_is_ag)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ideal R I; aGroup R\<rbrakk> \<Longrightarrow> rad_ideal R I = rInvim R (R /\<^sub>r I) (pj R I) (nilrad (R /\<^sub>r I))
[PROOF STEP]
apply (rule equalityI)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>ideal R I; aGroup R\<rbrakk> \<Longrightarrow> rad_ideal R I \<subseteq> rInvim R (R /\<^sub>r I) (pj R I) (nilrad (R /\<^sub>r I))
 2. \<lbrakk>ideal R I; aGroup R\<rbrakk> \<Longrightarrow> rInvim R (R /\<^sub>r I) (pj R I) (nilrad (R /\<^sub>r I)) \<subseteq> rad_ideal R I
[PROOF STEP]
apply (rule subsetI)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x. \<lbrakk>ideal R I; aGroup R; x \<in> rad_ideal R I\<rbrakk> \<Longrightarrow> x \<in> rInvim R (R /\<^sub>r I) (pj R I) (nilrad (R /\<^sub>r I))
 2. \<lbrakk>ideal R I; aGroup R\<rbrakk> \<Longrightarrow> rInvim R (R /\<^sub>r I) (pj R I) (nilrad (R /\<^sub>r I)) \<subseteq> rad_ideal R I
[PROOF STEP]
apply (simp add:rad_ideal_def)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x. \<lbrakk>ideal R I; aGroup R; x \<in> carrier R \<and> nilpotent (R /\<^sub>r I) (pj R I x)\<rbrakk> \<Longrightarrow> x \<in> rInvim R (R /\<^sub>r I) (pj R I) (nilrad (R /\<^sub>r I))
 2. \<lbrakk>ideal R I; aGroup R\<rbrakk> \<Longrightarrow> rInvim R (R /\<^sub>r I) (pj R I) (nilrad (R /\<^sub>r I)) \<subseteq> rad_ideal R I
[PROOF STEP]
apply (erule conjE)+
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x. \<lbrakk>ideal R I; aGroup R; x \<in> carrier R; nilpotent (R /\<^sub>r I) (pj R I x)\<rbrakk> \<Longrightarrow> x \<in> rInvim R (R /\<^sub>r I) (pj R I) (nilrad (R /\<^sub>r I))
 2. \<lbrakk>ideal R I; aGroup R\<rbrakk> \<Longrightarrow> rInvim R (R /\<^sub>r I) (pj R I) (nilrad (R /\<^sub>r I)) \<subseteq> rad_ideal R I
[PROOF STEP]
apply (simp add:rInvim_def)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x. \<lbrakk>ideal R I; aGroup R; x \<in> carrier R; nilpotent (R /\<^sub>r I) (pj R I x)\<rbrakk> \<Longrightarrow> pj R I x \<in> nilrad (R /\<^sub>r I)
 2. \<lbrakk>ideal R I; aGroup R\<rbrakk> \<Longrightarrow> rInvim R (R /\<^sub>r I) (pj R I) (nilrad (R /\<^sub>r I)) \<subseteq> rad_ideal R I
[PROOF STEP]
apply (simp add:nilrad_def)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x. \<lbrakk>ideal R I; aGroup R; x \<in> carrier R; nilpotent (R /\<^sub>r I) (pj R I x)\<rbrakk> \<Longrightarrow> pj R I x \<in> carrier (R /\<^sub>r I)
 2. \<lbrakk>ideal R I; aGroup R\<rbrakk> \<Longrightarrow> rInvim R (R /\<^sub>r I) (pj R I) (nilrad (R /\<^sub>r I)) \<subseteq> rad_ideal R I
[PROOF STEP]
apply (subst pj_mem, rule Ring_axioms)
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<And>x. \<lbrakk>ideal R I; aGroup R; x \<in> carrier R; nilpotent (R /\<^sub>r I) (pj R I x)\<rbrakk> \<Longrightarrow> ideal R I
 2. \<And>x. \<lbrakk>ideal R I; aGroup R; x \<in> carrier R; nilpotent (R /\<^sub>r I) (pj R I x)\<rbrakk> \<Longrightarrow> x \<in> carrier R
 3. \<And>x. \<lbrakk>ideal R I; aGroup R; x \<in> carrier R; nilpotent (R /\<^sub>r I) (pj R I x)\<rbrakk> \<Longrightarrow> x \<uplus>\<^bsub>R\<^esub> I \<in> carrier (R /\<^sub>r I)
 4. \<lbrakk>ideal R I; aGroup R\<rbrakk> \<Longrightarrow> rInvim R (R /\<^sub>r I) (pj R I) (nilrad (R /\<^sub>r I)) \<subseteq> rad_ideal R I
[PROOF STEP]
apply assumption+
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x. \<lbrakk>ideal R I; aGroup R; x \<in> carrier R; nilpotent (R /\<^sub>r I) (pj R I x)\<rbrakk> \<Longrightarrow> x \<uplus>\<^bsub>R\<^esub> I \<in> carrier (R /\<^sub>r I)
 2. \<lbrakk>ideal R I; aGroup R\<rbrakk> \<Longrightarrow> rInvim R (R /\<^sub>r I) (pj R I) (nilrad (R /\<^sub>r I)) \<subseteq> rad_ideal R I
[PROOF STEP]
apply (simp add:qring_def ar_coset_def set_rcs_def)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x. \<lbrakk>ideal R I; aGroup R; x \<in> carrier R; nilpotent \<lparr>carrier = {C. \<exists>a\<in>carrier (b_ag R). C = I \<bullet>\<^bsub>b_ag R\<^esub> a}, pop = c_top (b_ag R) I, mop = c_iop (b_ag R) I, zero = I, tp = rcostOp R I, un = I \<bullet>\<^bsub>b_ag R\<^esub> 1\<^sub>r\<rparr> (pj R I x)\<rbrakk> \<Longrightarrow> \<exists>a\<in>carrier (b_ag R). I \<bullet>\<^bsub>b_ag R\<^esub> x = I \<bullet>\<^bsub>b_ag R\<^esub> a
 2. \<lbrakk>ideal R I; aGroup R\<rbrakk> \<Longrightarrow> rInvim R (R /\<^sub>r I) (pj R I) (nilrad (R /\<^sub>r I)) \<subseteq> rad_ideal R I
[PROOF STEP]
apply (simp add:aGroup.ag_carrier_carrier)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x. \<lbrakk>ideal R I; aGroup R; x \<in> carrier R; nilpotent \<lparr>carrier = {C. \<exists>a\<in>carrier R. C = I \<bullet>\<^bsub>b_ag R\<^esub> a}, pop = c_top (b_ag R) I, mop = c_iop (b_ag R) I, zero = I, tp = rcostOp R I, un = I \<bullet>\<^bsub>b_ag R\<^esub> 1\<^sub>r\<rparr> (pj R I x)\<rbrakk> \<Longrightarrow> \<exists>a\<in>carrier R. I \<bullet>\<^bsub>b_ag R\<^esub> x = I \<bullet>\<^bsub>b_ag R\<^esub> a
 2. \<lbrakk>ideal R I; aGroup R\<rbrakk> \<Longrightarrow> rInvim R (R /\<^sub>r I) (pj R I) (nilrad (R /\<^sub>r I)) \<subseteq> rad_ideal R I
[PROOF STEP]
apply blast
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ideal R I; aGroup R\<rbrakk> \<Longrightarrow> rInvim R (R /\<^sub>r I) (pj R I) (nilrad (R /\<^sub>r I)) \<subseteq> rad_ideal R I
[PROOF STEP]
apply (rule subsetI)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>ideal R I; aGroup R; x \<in> rInvim R (R /\<^sub>r I) (pj R I) (nilrad (R /\<^sub>r I))\<rbrakk> \<Longrightarrow> x \<in> rad_ideal R I
[PROOF STEP]
apply (simp add:rInvim_def nilrad_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>ideal R I; aGroup R; x \<in> carrier R \<and> pj R I x \<in> carrier (R /\<^sub>r I) \<and> nilpotent (R /\<^sub>r I) (pj R I x)\<rbrakk> \<Longrightarrow> x \<in> rad_ideal R I
[PROOF STEP]
apply (simp add: rad_ideal_def)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma (in Ring) id_rad_ideal:"ideal R I \<Longrightarrow> ideal R (rad_ideal R I)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ideal R I \<Longrightarrow> ideal R (rad_ideal R I)
[PROOF STEP]
(* thm invim_of_ideal *)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ideal R I \<Longrightarrow> ideal R (rad_ideal R I)
[PROOF STEP]
apply (subst id_rad_invim [of "I"], assumption)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ideal R I \<Longrightarrow> ideal R (rInvim R (R /\<^sub>r I) (pj R I) (nilrad (R /\<^sub>r I)))
[PROOF STEP]
apply (rule invim_of_ideal, rule Ring_axioms, assumption)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ideal R I \<Longrightarrow> ideal (R /\<^sub>r I) (nilrad (R /\<^sub>r I))
[PROOF STEP]
apply (rule Ring.id_nilrad_ideal)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ideal R I \<Longrightarrow> Ring (R /\<^sub>r I)
[PROOF STEP]
apply (simp add:qring_ring)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma (in Ring) id_rad_cont_I:"ideal R I \<Longrightarrow> I \<subseteq> (rad_ideal R I)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ideal R I \<Longrightarrow> I \<subseteq> rad_ideal R I
[PROOF STEP]
apply (simp add:rad_ideal_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ideal R I \<Longrightarrow> I \<subseteq> {a \<in> carrier R. nilpotent (R /\<^sub>r I) (pj R I a)}
[PROOF STEP]
apply (rule subsetI, simp,
       simp add:ideal_subset)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>ideal R I; x \<in> I\<rbrakk> \<Longrightarrow> nilpotent (R /\<^sub>r I) (pj R I x)
[PROOF STEP]
apply (simp add:nilpotent_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>ideal R I; x \<in> I\<rbrakk> \<Longrightarrow> \<exists>n. pj R I x^\<^bsup>R /\<^sub>r I n\<^esup> = \<zero>\<^bsub>R /\<^sub>r I\<^esub>
[PROOF STEP]
apply (subst pj_mem, rule Ring_axioms, assumption+,
       simp add:ideal_subset)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>ideal R I; x \<in> I\<rbrakk> \<Longrightarrow> \<exists>n. (x \<uplus>\<^bsub>R\<^esub> I)^\<^bsup>R /\<^sub>r I n\<^esup> = \<zero>\<^bsub>R /\<^sub>r I\<^esub>
[PROOF STEP]
(* thm npQring *)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>ideal R I; x \<in> I\<rbrakk> \<Longrightarrow> \<exists>n. (x \<uplus>\<^bsub>R\<^esub> I)^\<^bsup>R /\<^sub>r I n\<^esup> = \<zero>\<^bsub>R /\<^sub>r I\<^esub>
[PROOF STEP]
apply (frule_tac h = x in ideal_subset[of "I"], assumption,
        frule_tac a = x in npQring[OF Ring, of "I" _ "Suc 0"], assumption,
        simp only:np_1, simp only:Qring_fix1,
        subst qring_zero[of "I"], assumption)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>ideal R I; x \<in> I; x \<in> carrier R; I^\<^bsup>R /\<^sub>r I Suc 0\<^esup> = I\<rbrakk> \<Longrightarrow> \<exists>n. I^\<^bsup>R /\<^sub>r I n\<^esup> = I
[PROOF STEP]
apply blast
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma (in Ring) id_rad_set:"ideal R I \<Longrightarrow>
       rad_ideal R I = {x. x \<in> carrier R \<and> (\<exists>n. npow R x n \<in> I)}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ideal R I \<Longrightarrow> rad_ideal R I = {x \<in> carrier R. \<exists>n. x^\<^bsup>R n\<^esup> \<in> I}
[PROOF STEP]
apply (simp add:rad_ideal_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ideal R I \<Longrightarrow> {a \<in> carrier R. nilpotent (R /\<^sub>r I) (pj R I a)} = {x \<in> carrier R. \<exists>n. x^\<^bsup>R n\<^esup> \<in> I}
[PROOF STEP]
apply (rule equalityI)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. ideal R I \<Longrightarrow> {a \<in> carrier R. nilpotent (R /\<^sub>r I) (pj R I a)} \<subseteq> {x \<in> carrier R. \<exists>n. x^\<^bsup>R n\<^esup> \<in> I}
 2. ideal R I \<Longrightarrow> {x \<in> carrier R. \<exists>n. x^\<^bsup>R n\<^esup> \<in> I} \<subseteq> {a \<in> carrier R. nilpotent (R /\<^sub>r I) (pj R I a)}
[PROOF STEP]
apply (rule subsetI)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x. \<lbrakk>ideal R I; x \<in> {a \<in> carrier R. nilpotent (R /\<^sub>r I) (pj R I a)}\<rbrakk> \<Longrightarrow> x \<in> {x \<in> carrier R. \<exists>n. x^\<^bsup>R n\<^esup> \<in> I}
 2. ideal R I \<Longrightarrow> {x \<in> carrier R. \<exists>n. x^\<^bsup>R n\<^esup> \<in> I} \<subseteq> {a \<in> carrier R. nilpotent (R /\<^sub>r I) (pj R I a)}
[PROOF STEP]
apply (simp add:nilpotent_def, erule conjE, erule exE)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x n. \<lbrakk>ideal R I; x \<in> carrier R; pj R I x^\<^bsup>R /\<^sub>r I n\<^esup> = \<zero>\<^bsub>R /\<^sub>r I\<^esub>\<rbrakk> \<Longrightarrow> \<exists>n. x^\<^bsup>R n\<^esup> \<in> I
 2. ideal R I \<Longrightarrow> {x \<in> carrier R. \<exists>n. x^\<^bsup>R n\<^esup> \<in> I} \<subseteq> {a \<in> carrier R. nilpotent (R /\<^sub>r I) (pj R I a)}
[PROOF STEP]
apply (simp add: pj_mem[OF Ring], simp add:npQring[OF Ring])
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x n. \<lbrakk>ideal R I; x \<in> carrier R; x^\<^bsup>R n\<^esup> \<uplus>\<^bsub>R\<^esub> I = \<zero>\<^bsub>R /\<^sub>r I\<^esub>\<rbrakk> \<Longrightarrow> \<exists>n. x^\<^bsup>R n\<^esup> \<in> I
 2. ideal R I \<Longrightarrow> {x \<in> carrier R. \<exists>n. x^\<^bsup>R n\<^esup> \<in> I} \<subseteq> {a \<in> carrier R. nilpotent (R /\<^sub>r I) (pj R I a)}
[PROOF STEP]
apply ( simp add:qring_zero)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x n. \<lbrakk>ideal R I; x \<in> carrier R; x^\<^bsup>R n\<^esup> \<uplus>\<^bsub>R\<^esub> I = I\<rbrakk> \<Longrightarrow> \<exists>n. x^\<^bsup>R n\<^esup> \<in> I
 2. ideal R I \<Longrightarrow> {x \<in> carrier R. \<exists>n. x^\<^bsup>R n\<^esup> \<in> I} \<subseteq> {a \<in> carrier R. nilpotent (R /\<^sub>r I) (pj R I a)}
[PROOF STEP]
apply (frule_tac x = x and n = n in npClose)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x n. \<lbrakk>ideal R I; x \<in> carrier R; x^\<^bsup>R n\<^esup> \<uplus>\<^bsub>R\<^esub> I = I; x^\<^bsup>R n\<^esup> \<in> carrier R\<rbrakk> \<Longrightarrow> \<exists>n. x^\<^bsup>R n\<^esup> \<in> I
 2. ideal R I \<Longrightarrow> {x \<in> carrier R. \<exists>n. x^\<^bsup>R n\<^esup> \<in> I} \<subseteq> {a \<in> carrier R. nilpotent (R /\<^sub>r I) (pj R I a)}
[PROOF STEP]
apply (frule_tac a = "x^\<^bsup>R n\<^esup>" in ar_coset_same3[of "I"], assumption+,
        blast)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ideal R I \<Longrightarrow> {x \<in> carrier R. \<exists>n. x^\<^bsup>R n\<^esup> \<in> I} \<subseteq> {a \<in> carrier R. nilpotent (R /\<^sub>r I) (pj R I a)}
[PROOF STEP]
apply (rule subsetI, simp, erule conjE, erule exE)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x n. \<lbrakk>ideal R I; x \<in> carrier R; x^\<^bsup>R n\<^esup> \<in> I\<rbrakk> \<Longrightarrow> nilpotent (R /\<^sub>r I) (pj R I x)
[PROOF STEP]
apply (simp add:nilpotent_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x n. \<lbrakk>ideal R I; x \<in> carrier R; x^\<^bsup>R n\<^esup> \<in> I\<rbrakk> \<Longrightarrow> \<exists>n. pj R I x^\<^bsup>R /\<^sub>r I n\<^esup> = \<zero>\<^bsub>R /\<^sub>r I\<^esub>
[PROOF STEP]
apply (simp add: pj_mem[OF Ring], simp add:npQring[OF Ring],
                                            simp add:qring_zero)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x n. \<lbrakk>ideal R I; x \<in> carrier R; x^\<^bsup>R n\<^esup> \<in> I\<rbrakk> \<Longrightarrow> \<exists>n. x^\<^bsup>R n\<^esup> \<uplus>\<^bsub>R\<^esub> I = I
[PROOF STEP]
apply (frule_tac a = "x^\<^bsup>R n\<^esup>" in ar_coset_same4[of "I"], assumption+)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x n. \<lbrakk>ideal R I; x \<in> carrier R; x^\<^bsup>R n\<^esup> \<in> I; x^\<^bsup>R n\<^esup> \<uplus>\<^bsub>R\<^esub> I = I\<rbrakk> \<Longrightarrow> \<exists>n. x^\<^bsup>R n\<^esup> \<uplus>\<^bsub>R\<^esub> I = I
[PROOF STEP]
apply blast
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma (in Ring) rad_primary_prime:"primary_ideal R q \<Longrightarrow>
                                    prime_ideal R (rad_ideal R q)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. primary_ideal R q \<Longrightarrow> prime_ideal R (rad_ideal R q)
[PROOF STEP]
apply (simp add:prime_ideal_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. primary_ideal R q \<Longrightarrow> ideal R (rad_ideal R q) \<and> 1\<^sub>r \<notin> rad_ideal R q \<and> (\<forall>x\<in>carrier R. \<forall>y\<in>carrier R. x \<cdot>\<^sub>r y \<in> rad_ideal R q \<longrightarrow> x \<in> rad_ideal R q \<or> y \<in> rad_ideal R q)
[PROOF STEP]
apply (frule primary_ideal_ideal[of "q"])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>primary_ideal R q; ideal R q\<rbrakk> \<Longrightarrow> ideal R (rad_ideal R q) \<and> 1\<^sub>r \<notin> rad_ideal R q \<and> (\<forall>x\<in>carrier R. \<forall>y\<in>carrier R. x \<cdot>\<^sub>r y \<in> rad_ideal R q \<longrightarrow> x \<in> rad_ideal R q \<or> y \<in> rad_ideal R q)
[PROOF STEP]
apply (simp add:id_rad_ideal)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>primary_ideal R q; ideal R q\<rbrakk> \<Longrightarrow> 1\<^sub>r \<notin> rad_ideal R q \<and> (\<forall>x\<in>carrier R. \<forall>y\<in>carrier R. x \<cdot>\<^sub>r y \<in> rad_ideal R q \<longrightarrow> x \<in> rad_ideal R q \<or> y \<in> rad_ideal R q)
[PROOF STEP]
apply (rule conjI)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>primary_ideal R q; ideal R q\<rbrakk> \<Longrightarrow> 1\<^sub>r \<notin> rad_ideal R q
 2. \<lbrakk>primary_ideal R q; ideal R q\<rbrakk> \<Longrightarrow> \<forall>x\<in>carrier R. \<forall>y\<in>carrier R. x \<cdot>\<^sub>r y \<in> rad_ideal R q \<longrightarrow> x \<in> rad_ideal R q \<or> y \<in> rad_ideal R q
[PROOF STEP]
apply (rule contrapos_pp, simp+)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>primary_ideal R q; ideal R q; 1\<^sub>r \<in> rad_ideal R q\<rbrakk> \<Longrightarrow> False
 2. \<lbrakk>primary_ideal R q; ideal R q\<rbrakk> \<Longrightarrow> \<forall>x\<in>carrier R. \<forall>y\<in>carrier R. x \<cdot>\<^sub>r y \<in> rad_ideal R q \<longrightarrow> x \<in> rad_ideal R q \<or> y \<in> rad_ideal R q
[PROOF STEP]
apply (simp add:id_rad_set, erule conjE, erule exE)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>n. \<lbrakk>primary_ideal R q; ideal R q; 1\<^sub>r \<in> carrier R; 1\<^sub>r^\<^bsup>R n\<^esup> \<in> q\<rbrakk> \<Longrightarrow> False
 2. \<lbrakk>primary_ideal R q; ideal R q\<rbrakk> \<Longrightarrow> \<forall>x\<in>carrier R. \<forall>y\<in>carrier R. x \<cdot>\<^sub>r y \<in> rad_ideal R q \<longrightarrow> x \<in> rad_ideal R q \<or> y \<in> rad_ideal R q
[PROOF STEP]
apply (simp add:npOne)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>primary_ideal R q; ideal R q; 1\<^sub>r \<in> carrier R; 1\<^sub>r \<in> q\<rbrakk> \<Longrightarrow> False
 2. \<lbrakk>primary_ideal R q; ideal R q\<rbrakk> \<Longrightarrow> \<forall>x\<in>carrier R. \<forall>y\<in>carrier R. x \<cdot>\<^sub>r y \<in> rad_ideal R q \<longrightarrow> x \<in> rad_ideal R q \<or> y \<in> rad_ideal R q
[PROOF STEP]
apply (simp add:primary_ideal_proper1[of "q"])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>primary_ideal R q; ideal R q\<rbrakk> \<Longrightarrow> \<forall>x\<in>carrier R. \<forall>y\<in>carrier R. x \<cdot>\<^sub>r y \<in> rad_ideal R q \<longrightarrow> x \<in> rad_ideal R q \<or> y \<in> rad_ideal R q
[PROOF STEP]
apply ((rule ballI)+, rule impI)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x y. \<lbrakk>primary_ideal R q; ideal R q; x \<in> carrier R; y \<in> carrier R; x \<cdot>\<^sub>r y \<in> rad_ideal R q\<rbrakk> \<Longrightarrow> x \<in> rad_ideal R q \<or> y \<in> rad_ideal R q
[PROOF STEP]
apply (rule contrapos_pp, simp+, erule conjE)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x y. \<lbrakk>primary_ideal R q; ideal R q; x \<in> carrier R; y \<in> carrier R; x \<cdot>\<^sub>r y \<in> rad_ideal R q; x \<notin> rad_ideal R q; y \<notin> rad_ideal R q\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
apply (simp add:id_rad_set, erule conjE, erule exE)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x y n. \<lbrakk>primary_ideal R q; ideal R q; x \<in> carrier R; y \<in> carrier R; \<forall>n. x^\<^bsup>R n\<^esup> \<notin> q; \<forall>n. y^\<^bsup>R n\<^esup> \<notin> q; x \<cdot>\<^sub>r y \<in> carrier R; (x \<cdot>\<^sub>r y)^\<^bsup>R n\<^esup> \<in> q\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
apply (simp add:npMul)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x y n. \<lbrakk>primary_ideal R q; ideal R q; x \<in> carrier R; y \<in> carrier R; \<forall>n. x^\<^bsup>R n\<^esup> \<notin> q; \<forall>n. y^\<^bsup>R n\<^esup> \<notin> q; x \<cdot>\<^sub>r y \<in> carrier R; x^\<^bsup>R n\<^esup> \<cdot>\<^sub>r y^\<^bsup>R n\<^esup> \<in> q\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
apply (simp add:primary_ideal_def, (erule conjE)+)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x y n. \<lbrakk>ideal R q; x \<in> carrier R; y \<in> carrier R; \<forall>n. x^\<^bsup>R n\<^esup> \<notin> q; \<forall>n. y^\<^bsup>R n\<^esup> \<notin> q; x \<cdot>\<^sub>r y \<in> carrier R; x^\<^bsup>R n\<^esup> \<cdot>\<^sub>r y^\<^bsup>R n\<^esup> \<in> q; 1\<^sub>r \<notin> q; \<forall>x\<in>carrier R. \<forall>y\<in>carrier R. x \<cdot>\<^sub>r y \<in> q \<longrightarrow> (\<exists>n. x^\<^bsup>R n\<^esup> \<in> q) \<or> y \<in> q\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
apply (frule_tac x = x and n = n in npClose,
        frule_tac x = y and n = n in npClose)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x y n. \<lbrakk>ideal R q; x \<in> carrier R; y \<in> carrier R; \<forall>n. x^\<^bsup>R n\<^esup> \<notin> q; \<forall>n. y^\<^bsup>R n\<^esup> \<notin> q; x \<cdot>\<^sub>r y \<in> carrier R; x^\<^bsup>R n\<^esup> \<cdot>\<^sub>r y^\<^bsup>R n\<^esup> \<in> q; 1\<^sub>r \<notin> q; \<forall>x\<in>carrier R. \<forall>y\<in>carrier R. x \<cdot>\<^sub>r y \<in> q \<longrightarrow> (\<exists>n. x^\<^bsup>R n\<^esup> \<in> q) \<or> y \<in> q; x^\<^bsup>R n\<^esup> \<in> carrier R; y^\<^bsup>R n\<^esup> \<in> carrier R\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
apply (frule_tac x = "x^\<^bsup>R n\<^esup>" in bspec, assumption,
        thin_tac "\<forall>x\<in>carrier R. \<forall>y\<in>carrier R. x \<cdot>\<^sub>r y \<in> q \<longrightarrow>
                                    (\<exists>n. x^\<^bsup>R n\<^esup> \<in> q) \<or> y \<in> q",
        frule_tac x = "y^\<^bsup>R n\<^esup>" in bspec, assumption,
        thin_tac "\<forall>y\<in>carrier R. x^\<^bsup>R n\<^esup> \<cdot>\<^sub>r y \<in> q \<longrightarrow>
                             (\<exists>na. x^\<^bsup>R n\<^esup>^\<^bsup>R na\<^esup> \<in> q) \<or> y \<in> q", simp)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x y n. \<lbrakk>ideal R q; x \<in> carrier R; y \<in> carrier R; \<forall>n. x^\<^bsup>R n\<^esup> \<notin> q; \<forall>n. y^\<^bsup>R n\<^esup> \<notin> q; x \<cdot>\<^sub>r y \<in> carrier R; x^\<^bsup>R n\<^esup> \<cdot>\<^sub>r y^\<^bsup>R n\<^esup> \<in> q; 1\<^sub>r \<notin> q; x^\<^bsup>R n\<^esup> \<in> carrier R; y^\<^bsup>R n\<^esup> \<in> carrier R; \<exists>na. x^\<^bsup>R n\<^esup>^\<^bsup>R na\<^esup> \<in> q\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
apply (simp add:npMulExp)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma (in Ring) npow_notin_prime:"\<lbrakk>prime_ideal R P; x \<in> carrier R; x \<notin> P\<rbrakk>
                                \<Longrightarrow> \<forall>n. npow R x n \<notin> P"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>prime_ideal R P; x \<in> carrier R; x \<notin> P\<rbrakk> \<Longrightarrow> \<forall>n. x^\<^bsup>R n\<^esup> \<notin> P
[PROOF STEP]
apply (rule allI)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>n. \<lbrakk>prime_ideal R P; x \<in> carrier R; x \<notin> P\<rbrakk> \<Longrightarrow> x^\<^bsup>R n\<^esup> \<notin> P
[PROOF STEP]
apply (induct_tac n)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>n. \<lbrakk>prime_ideal R P; x \<in> carrier R; x \<notin> P\<rbrakk> \<Longrightarrow> x^\<^bsup>R 0\<^esup> \<notin> P
 2. \<And>n na. \<lbrakk>prime_ideal R P; x \<in> carrier R; x \<notin> P; x^\<^bsup>R na\<^esup> \<notin> P\<rbrakk> \<Longrightarrow> x^\<^bsup>R Suc na\<^esup> \<notin> P
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>prime_ideal R P; x \<in> carrier R; x \<notin> P\<rbrakk> \<Longrightarrow> 1\<^sub>r \<notin> P
 2. \<And>n na. \<lbrakk>prime_ideal R P; x \<in> carrier R; x \<notin> P; x^\<^bsup>R na\<^esup> \<notin> P\<rbrakk> \<Longrightarrow> x^\<^bsup>R Suc na\<^esup> \<notin> P
[PROOF STEP]
apply (simp add:prime_ideal_proper1)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>n na. \<lbrakk>prime_ideal R P; x \<in> carrier R; x \<notin> P; x^\<^bsup>R na\<^esup> \<notin> P\<rbrakk> \<Longrightarrow> x^\<^bsup>R Suc na\<^esup> \<notin> P
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>na. \<lbrakk>prime_ideal R P; x \<in> carrier R; x \<notin> P; x^\<^bsup>R na\<^esup> \<notin> P\<rbrakk> \<Longrightarrow> x^\<^bsup>R na\<^esup> \<cdot>\<^sub>r x \<notin> P
[PROOF STEP]
apply (frule_tac x = x and n = na in npClose)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>na. \<lbrakk>prime_ideal R P; x \<in> carrier R; x \<notin> P; x^\<^bsup>R na\<^esup> \<notin> P; x^\<^bsup>R na\<^esup> \<in> carrier R\<rbrakk> \<Longrightarrow> x^\<^bsup>R na\<^esup> \<cdot>\<^sub>r x \<notin> P
[PROOF STEP]
apply (simp add:prime_elems_mult_not)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma (in Ring) npow_in_prime:"\<lbrakk>prime_ideal R P; x \<in> carrier R;
                               \<exists>n. npow R x n \<in> P \<rbrakk> \<Longrightarrow> x \<in> P"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>prime_ideal R P; x \<in> carrier R; \<exists>n. x^\<^bsup>R n\<^esup> \<in> P\<rbrakk> \<Longrightarrow> x \<in> P
[PROOF STEP]
apply (rule contrapos_pp, simp+)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>prime_ideal R P; x \<in> carrier R; \<exists>n. x^\<^bsup>R n\<^esup> \<in> P; x \<notin> P\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
apply (frule npow_notin_prime, assumption+)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>prime_ideal R P; x \<in> carrier R; \<exists>n. x^\<^bsup>R n\<^esup> \<in> P; x \<notin> P; \<forall>n. x^\<^bsup>R n\<^esup> \<notin> P\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
apply blast
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma (in Ring) mul_closed_set_sub:"mul_closed_set R S \<Longrightarrow> S \<subseteq> carrier R"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. mul_closed_set R S \<Longrightarrow> S \<subseteq> carrier R
[PROOF STEP]
by (simp add:mul_closed_set_def)


[STATEMENT]
lemma (in Ring) mul_closed_set_tOp_closed:"\<lbrakk>mul_closed_set R S; s \<in> S;
                            t \<in> S\<rbrakk> \<Longrightarrow> s \<cdot>\<^sub>r t \<in> S"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>mul_closed_set R S; s \<in> S; t \<in> S\<rbrakk> \<Longrightarrow> s \<cdot>\<^sub>r t \<in> S
[PROOF STEP]
by (simp add:mul_closed_set_def)


[STATEMENT]
lemma (in Corps) f_inv_unique:"\<lbrakk> x \<in> carrier K - {\<zero>}; x' \<in> carrier K;
      x'' \<in> carrier K; x' \<cdot>\<^sub>r  x = 1\<^sub>r; x'' \<cdot>\<^sub>r x = 1\<^sub>r \<rbrakk> \<Longrightarrow> x' = x''"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>x \<in> carrier K - {\<zero>}; x' \<in> carrier K; x'' \<in> carrier K; x' \<cdot>\<^sub>r x = 1\<^sub>r; x'' \<cdot>\<^sub>r x = 1\<^sub>r\<rbrakk> \<Longrightarrow> x' = x''
[PROOF STEP]
apply (cut_tac  f_is_ring)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>x \<in> carrier K - {\<zero>}; x' \<in> carrier K; x'' \<in> carrier K; x' \<cdot>\<^sub>r x = 1\<^sub>r; x'' \<cdot>\<^sub>r x = 1\<^sub>r; Ring K\<rbrakk> \<Longrightarrow> x' = x''
[PROOF STEP]
apply (cut_tac x = x' and y = x and z = x'' in Ring.ring_tOp_assoc[of K],
        assumption+, simp, assumption, simp)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>x \<in> carrier K \<and> x \<noteq> \<zero>; x' \<in> carrier K; x'' \<in> carrier K; x' \<cdot>\<^sub>r x = 1\<^sub>r; x'' \<cdot>\<^sub>r x = 1\<^sub>r; Ring K; 1\<^sub>r \<cdot>\<^sub>r x'' = x' \<cdot>\<^sub>r (x \<cdot>\<^sub>r x'')\<rbrakk> \<Longrightarrow> x' = x''
[PROOF STEP]
apply (simp add:Ring.ring_l_one[of K],
        simp add:Ring.ring_tOp_commute[of K x x''] Ring.ring_r_one[of K])
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma (in Corps) invf_inv:"x \<in> carrier K - {\<zero>} \<Longrightarrow>
                (invf K x) \<in> carrier K \<and> (invf K x) \<cdot>\<^sub>r x = 1\<^sub>r "
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x \<in> carrier K - {\<zero>} \<Longrightarrow> invf K x \<in> carrier K \<and> invf K x \<cdot>\<^sub>r x = 1\<^sub>r
[PROOF STEP]
apply (simp add:invf_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x \<in> carrier K \<and> x \<noteq> \<zero> \<Longrightarrow> (THE y. y \<in> carrier K \<and> y \<cdot>\<^sub>r x = 1\<^sub>r) \<in> carrier K \<and> (THE y. y \<in> carrier K \<and> y \<cdot>\<^sub>r x = 1\<^sub>r) \<cdot>\<^sub>r x = 1\<^sub>r
[PROOF STEP]
apply (rule theI')
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x \<in> carrier K \<and> x \<noteq> \<zero> \<Longrightarrow> \<exists>!xa. xa \<in> carrier K \<and> xa \<cdot>\<^sub>r x = 1\<^sub>r
[PROOF STEP]
apply (rule ex_ex1I)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. x \<in> carrier K \<and> x \<noteq> \<zero> \<Longrightarrow> \<exists>xa. xa \<in> carrier K \<and> xa \<cdot>\<^sub>r x = 1\<^sub>r
 2. \<And>xa y. \<lbrakk>x \<in> carrier K \<and> x \<noteq> \<zero>; xa \<in> carrier K \<and> xa \<cdot>\<^sub>r x = 1\<^sub>r; y \<in> carrier K \<and> y \<cdot>\<^sub>r x = 1\<^sub>r\<rbrakk> \<Longrightarrow> xa = y
[PROOF STEP]
apply (cut_tac f_inv, blast)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>xa y. \<lbrakk>x \<in> carrier K \<and> x \<noteq> \<zero>; xa \<in> carrier K \<and> xa \<cdot>\<^sub>r x = 1\<^sub>r; y \<in> carrier K \<and> y \<cdot>\<^sub>r x = 1\<^sub>r\<rbrakk> \<Longrightarrow> xa = y
[PROOF STEP]
apply (rule_tac x' = xa and x'' = y in f_inv_unique[of x])
[PROOF STATE]
proof (prove)
goal (5 subgoals):
 1. \<And>xa y. \<lbrakk>x \<in> carrier K \<and> x \<noteq> \<zero>; xa \<in> carrier K \<and> xa \<cdot>\<^sub>r x = 1\<^sub>r; y \<in> carrier K \<and> y \<cdot>\<^sub>r x = 1\<^sub>r\<rbrakk> \<Longrightarrow> x \<in> carrier K - {\<zero>}
 2. \<And>xa y. \<lbrakk>x \<in> carrier K \<and> x \<noteq> \<zero>; xa \<in> carrier K \<and> xa \<cdot>\<^sub>r x = 1\<^sub>r; y \<in> carrier K \<and> y \<cdot>\<^sub>r x = 1\<^sub>r\<rbrakk> \<Longrightarrow> xa \<in> carrier K
 3. \<And>xa y. \<lbrakk>x \<in> carrier K \<and> x \<noteq> \<zero>; xa \<in> carrier K \<and> xa \<cdot>\<^sub>r x = 1\<^sub>r; y \<in> carrier K \<and> y \<cdot>\<^sub>r x = 1\<^sub>r\<rbrakk> \<Longrightarrow> y \<in> carrier K
 4. \<And>xa y. \<lbrakk>x \<in> carrier K \<and> x \<noteq> \<zero>; xa \<in> carrier K \<and> xa \<cdot>\<^sub>r x = 1\<^sub>r; y \<in> carrier K \<and> y \<cdot>\<^sub>r x = 1\<^sub>r\<rbrakk> \<Longrightarrow> xa \<cdot>\<^sub>r x = 1\<^sub>r
 5. \<And>xa y. \<lbrakk>x \<in> carrier K \<and> x \<noteq> \<zero>; xa \<in> carrier K \<and> xa \<cdot>\<^sub>r x = 1\<^sub>r; y \<in> carrier K \<and> y \<cdot>\<^sub>r x = 1\<^sub>r\<rbrakk> \<Longrightarrow> y \<cdot>\<^sub>r x = 1\<^sub>r
[PROOF STEP]
apply simp+
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma (in Idomain) idom_is_ring: "Ring R"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Ring R
[PROOF STEP]
..


[STATEMENT]
lemma (in Idomain) idom_tOp_nonzeros:"\<lbrakk>x \<in> carrier R;
       y \<in> carrier R; x \<noteq> \<zero>;  y \<noteq> \<zero>\<rbrakk> \<Longrightarrow> x \<cdot>\<^sub>r y \<noteq> \<zero>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>x \<in> carrier R; y \<in> carrier R; x \<noteq> \<zero>; y \<noteq> \<zero>\<rbrakk> \<Longrightarrow> x \<cdot>\<^sub>r y \<noteq> \<zero>
[PROOF STEP]
apply (rule contrapos_pp, simp+)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>x \<in> carrier R; y \<in> carrier R; x \<noteq> \<zero>; y \<noteq> \<zero>; x \<cdot>\<^sub>r y = \<zero>\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
apply (cut_tac idom[of x y])
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<lbrakk>x \<in> carrier R; y \<in> carrier R; x \<noteq> \<zero>; y \<noteq> \<zero>; x \<cdot>\<^sub>r y = \<zero>; x = \<zero> \<or> y = \<zero>\<rbrakk> \<Longrightarrow> False
 2. \<lbrakk>x \<in> carrier R; y \<in> carrier R; x \<noteq> \<zero>; y \<noteq> \<zero>; x \<cdot>\<^sub>r y = \<zero>\<rbrakk> \<Longrightarrow> x \<in> carrier R
 3. \<lbrakk>x \<in> carrier R; y \<in> carrier R; x \<noteq> \<zero>; y \<noteq> \<zero>; x \<cdot>\<^sub>r y = \<zero>\<rbrakk> \<Longrightarrow> y \<in> carrier R
 4. \<lbrakk>x \<in> carrier R; y \<in> carrier R; x \<noteq> \<zero>; y \<noteq> \<zero>; x \<cdot>\<^sub>r y = \<zero>\<rbrakk> \<Longrightarrow> x \<cdot>\<^sub>r y = \<zero>
[PROOF STEP]
apply (erule disjE, simp+)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma (in Idomain) idom_potent_nonzero:
       "\<lbrakk>x \<in> carrier R; x \<noteq> \<zero>\<rbrakk>  \<Longrightarrow> npow R x n \<noteq> \<zero> "
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>x \<in> carrier R; x \<noteq> \<zero>\<rbrakk> \<Longrightarrow> x^\<^bsup>R n\<^esup> \<noteq> \<zero>
[PROOF STEP]
apply (induct_tac n)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>x \<in> carrier R; x \<noteq> \<zero>\<rbrakk> \<Longrightarrow> x^\<^bsup>R 0\<^esup> \<noteq> \<zero>
 2. \<And>n. \<lbrakk>x \<in> carrier R; x \<noteq> \<zero>; x^\<^bsup>R n\<^esup> \<noteq> \<zero>\<rbrakk> \<Longrightarrow> x^\<^bsup>R Suc n\<^esup> \<noteq> \<zero>
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>x \<in> carrier R; x \<noteq> \<zero>\<rbrakk> \<Longrightarrow> 1\<^sub>r \<noteq> \<zero>
 2. \<And>n. \<lbrakk>x \<in> carrier R; x \<noteq> \<zero>; x^\<^bsup>R n\<^esup> \<noteq> \<zero>\<rbrakk> \<Longrightarrow> x^\<^bsup>R Suc n\<^esup> \<noteq> \<zero>
[PROOF STEP]
(* case 0 *)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>x \<in> carrier R; x \<noteq> \<zero>\<rbrakk> \<Longrightarrow> 1\<^sub>r \<noteq> \<zero>
 2. \<And>n. \<lbrakk>x \<in> carrier R; x \<noteq> \<zero>; x^\<^bsup>R n\<^esup> \<noteq> \<zero>\<rbrakk> \<Longrightarrow> x^\<^bsup>R Suc n\<^esup> \<noteq> \<zero>
[PROOF STEP]
apply (rule contrapos_pp, simp+)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>x \<in> carrier R; x \<noteq> \<zero>; 1\<^sub>r = \<zero>\<rbrakk> \<Longrightarrow> False
 2. \<And>n. \<lbrakk>x \<in> carrier R; x \<noteq> \<zero>; x^\<^bsup>R n\<^esup> \<noteq> \<zero>\<rbrakk> \<Longrightarrow> x^\<^bsup>R Suc n\<^esup> \<noteq> \<zero>
[PROOF STEP]
apply (frule ring_l_one[of "x", THEN sym])
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>x \<in> carrier R; x \<noteq> \<zero>; 1\<^sub>r = \<zero>; x = 1\<^sub>r \<cdot>\<^sub>r x\<rbrakk> \<Longrightarrow> False
 2. \<And>n. \<lbrakk>x \<in> carrier R; x \<noteq> \<zero>; x^\<^bsup>R n\<^esup> \<noteq> \<zero>\<rbrakk> \<Longrightarrow> x^\<^bsup>R Suc n\<^esup> \<noteq> \<zero>
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>x \<in> carrier R; x \<noteq> \<zero>; 1\<^sub>r = \<zero>; x = \<zero> \<cdot>\<^sub>r x\<rbrakk> \<Longrightarrow> False
 2. \<And>n. \<lbrakk>x \<in> carrier R; x \<noteq> \<zero>; x^\<^bsup>R n\<^esup> \<noteq> \<zero>\<rbrakk> \<Longrightarrow> x^\<^bsup>R Suc n\<^esup> \<noteq> \<zero>
[PROOF STEP]
apply (simp add:ring_times_0_x)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>n. \<lbrakk>x \<in> carrier R; x \<noteq> \<zero>; x^\<^bsup>R n\<^esup> \<noteq> \<zero>\<rbrakk> \<Longrightarrow> x^\<^bsup>R Suc n\<^esup> \<noteq> \<zero>
[PROOF STEP]
(* case (Suc n) *)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>n. \<lbrakk>x \<in> carrier R; x \<noteq> \<zero>; x^\<^bsup>R n\<^esup> \<noteq> \<zero>\<rbrakk> \<Longrightarrow> x^\<^bsup>R Suc n\<^esup> \<noteq> \<zero>
[PROOF STEP]
apply (rule contrapos_pp, simp+)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>n. \<lbrakk>x \<in> carrier R; x \<noteq> \<zero>; x^\<^bsup>R n\<^esup> \<noteq> \<zero>; x^\<^bsup>R n\<^esup> \<cdot>\<^sub>r x = \<zero>\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
apply (frule_tac n = n in npClose[of x],
        cut_tac a = "x^\<^bsup>R n\<^esup>" and b = x in idom, assumption+)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>n. \<lbrakk>x \<in> carrier R; x \<noteq> \<zero>; x^\<^bsup>R n\<^esup> \<noteq> \<zero>; x^\<^bsup>R n\<^esup> \<cdot>\<^sub>r x = \<zero>; x^\<^bsup>R n\<^esup> \<in> carrier R; x^\<^bsup>R n\<^esup> = \<zero> \<or> x = \<zero>\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
apply (erule disjE, simp+)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma (in Idomain) idom_potent_unit:"\<lbrakk>a \<in> carrier R; 0 < n\<rbrakk>
                 \<Longrightarrow> (Unit R a) = (Unit R (npow R a n))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>a \<in> carrier R; 0 < n\<rbrakk> \<Longrightarrow> Unit R a = Unit R (a^\<^bsup>R n\<^esup>)
[PROOF STEP]
apply (rule iffI)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>a \<in> carrier R; 0 < n; Unit R a\<rbrakk> \<Longrightarrow> Unit R (a^\<^bsup>R n\<^esup>)
 2. \<lbrakk>a \<in> carrier R; 0 < n; Unit R (a^\<^bsup>R n\<^esup>)\<rbrakk> \<Longrightarrow> Unit R a
[PROOF STEP]
apply (simp add:Unit_def, erule bexE)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>b. \<lbrakk>a \<in> carrier R; 0 < n; b \<in> carrier R; a \<cdot>\<^sub>r b = 1\<^sub>r\<rbrakk> \<Longrightarrow> a^\<^bsup>R n\<^esup> \<in> carrier R \<and> (\<exists>b\<in>carrier R. a^\<^bsup>R n\<^esup> \<cdot>\<^sub>r b = 1\<^sub>r)
 2. \<lbrakk>a \<in> carrier R; 0 < n; Unit R (a^\<^bsup>R n\<^esup>)\<rbrakk> \<Longrightarrow> Unit R a
[PROOF STEP]
apply (simp add:npClose)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>b. \<lbrakk>a \<in> carrier R; 0 < n; b \<in> carrier R; a \<cdot>\<^sub>r b = 1\<^sub>r\<rbrakk> \<Longrightarrow> \<exists>b\<in>carrier R. a^\<^bsup>R n\<^esup> \<cdot>\<^sub>r b = 1\<^sub>r
 2. \<lbrakk>a \<in> carrier R; 0 < n; Unit R (a^\<^bsup>R n\<^esup>)\<rbrakk> \<Longrightarrow> Unit R a
[PROOF STEP]
apply (frule_tac x1 = a and y1 = b and n1 = n in npMul[THEN sym], assumption,
        simp add:npOne)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>b. \<lbrakk>a \<in> carrier R; 0 < n; b \<in> carrier R; a \<cdot>\<^sub>r b = 1\<^sub>r; a^\<^bsup>R n\<^esup> \<cdot>\<^sub>r b^\<^bsup>R n\<^esup> = 1\<^sub>r\<rbrakk> \<Longrightarrow> \<exists>b\<in>carrier R. a^\<^bsup>R n\<^esup> \<cdot>\<^sub>r b = 1\<^sub>r
 2. \<lbrakk>a \<in> carrier R; 0 < n; Unit R (a^\<^bsup>R n\<^esup>)\<rbrakk> \<Longrightarrow> Unit R a
[PROOF STEP]
apply (frule_tac x = b and n = n in npClose, blast)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>a \<in> carrier R; 0 < n; Unit R (a^\<^bsup>R n\<^esup>)\<rbrakk> \<Longrightarrow> Unit R a
[PROOF STEP]
apply (case_tac "n = Suc 0", simp only: np_1)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>a \<in> carrier R; 0 < n; Unit R (a^\<^bsup>R n\<^esup>); n \<noteq> Suc 0\<rbrakk> \<Longrightarrow> Unit R a
[PROOF STEP]
apply (simp add:Unit_def, erule conjE, erule bexE)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>b. \<lbrakk>a \<in> carrier R; 0 < n; n \<noteq> Suc 0; a^\<^bsup>R n\<^esup> \<in> carrier R; b \<in> carrier R; a^\<^bsup>R n\<^esup> \<cdot>\<^sub>r b = 1\<^sub>r\<rbrakk> \<Longrightarrow> \<exists>b\<in>carrier R. a \<cdot>\<^sub>r b = 1\<^sub>r
[PROOF STEP]
apply (cut_tac x = a and n = "n - Suc 0" in npow_suc[of R], simp del:npow_suc,
      thin_tac "a^\<^bsup>R n\<^esup> = a^\<^bsup>R (n - Suc 0)\<^esup> \<cdot>\<^sub>r a",
      frule_tac x = a and n = "n - Suc 0" in npClose,
      frule_tac x = "a^\<^bsup>R (n - Suc 0)\<^esup>" and y = a in ring_tOp_commute, assumption+,
      simp add:ring_tOp_assoc,
      frule_tac x = "a^\<^bsup>R (n - Suc 0)\<^esup>" and y = b in ring_tOp_closed, assumption+)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>b. \<lbrakk>a \<in> carrier R; 0 < n; n \<noteq> Suc 0; a \<cdot>\<^sub>r a^\<^bsup>R (n - Suc 0)\<^esup> \<in> carrier R; b \<in> carrier R; a \<cdot>\<^sub>r (a^\<^bsup>R (n - Suc 0)\<^esup> \<cdot>\<^sub>r b) = 1\<^sub>r; a^\<^bsup>R (n - Suc 0)\<^esup> \<in> carrier R; a^\<^bsup>R (n - Suc 0)\<^esup> \<cdot>\<^sub>r a = a \<cdot>\<^sub>r a^\<^bsup>R (n - Suc 0)\<^esup>; a^\<^bsup>R (n - Suc 0)\<^esup> \<cdot>\<^sub>r b \<in> carrier R\<rbrakk> \<Longrightarrow> \<exists>b\<in>carrier R. a \<cdot>\<^sub>r b = 1\<^sub>r
[PROOF STEP]
apply blast
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma (in Idomain) idom_mult_cancel_r:"\<lbrakk>a \<in> carrier R;
       b \<in> carrier R; c \<in> carrier R; c \<noteq> \<zero>; a \<cdot>\<^sub>r c = b \<cdot>\<^sub>r c\<rbrakk> \<Longrightarrow> a = b"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>a \<in> carrier R; b \<in> carrier R; c \<in> carrier R; c \<noteq> \<zero>; a \<cdot>\<^sub>r c = b \<cdot>\<^sub>r c\<rbrakk> \<Longrightarrow> a = b
[PROOF STEP]
apply (cut_tac ring_is_ag)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>a \<in> carrier R; b \<in> carrier R; c \<in> carrier R; c \<noteq> \<zero>; a \<cdot>\<^sub>r c = b \<cdot>\<^sub>r c; aGroup R\<rbrakk> \<Longrightarrow> a = b
[PROOF STEP]
apply (frule ring_tOp_closed[of "a" "c"], assumption+,
        frule ring_tOp_closed[of "b" "c"], assumption+)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>a \<in> carrier R; b \<in> carrier R; c \<in> carrier R; c \<noteq> \<zero>; a \<cdot>\<^sub>r c = b \<cdot>\<^sub>r c; aGroup R; a \<cdot>\<^sub>r c \<in> carrier R; b \<cdot>\<^sub>r c \<in> carrier R\<rbrakk> \<Longrightarrow> a = b
[PROOF STEP]
apply (simp add:aGroup.ag_eq_diffzero[of "R" "a \<cdot>\<^sub>r c" "b \<cdot>\<^sub>r c"],
        simp add:ring_inv1_1,
        frule aGroup.ag_mOp_closed[of "R" "b"], assumption,
        simp add:ring_distrib2[THEN sym, of "c" "a" "-\<^sub>a b"])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>a \<in> carrier R; b \<in> carrier R; c \<in> carrier R; c \<noteq> \<zero>; (a \<plusminus> -\<^sub>a b) \<cdot>\<^sub>r c = \<zero>; aGroup R; a \<cdot>\<^sub>r c \<in> carrier R; b \<cdot>\<^sub>r c \<in> carrier R; -\<^sub>a b \<in> carrier R\<rbrakk> \<Longrightarrow> a = b
[PROOF STEP]
apply (frule aGroup.ag_pOp_closed[of "R" "a" "-\<^sub>a b"], assumption+)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>a \<in> carrier R; b \<in> carrier R; c \<in> carrier R; c \<noteq> \<zero>; (a \<plusminus> -\<^sub>a b) \<cdot>\<^sub>r c = \<zero>; aGroup R; a \<cdot>\<^sub>r c \<in> carrier R; b \<cdot>\<^sub>r c \<in> carrier R; -\<^sub>a b \<in> carrier R; a \<plusminus> -\<^sub>a b \<in> carrier R\<rbrakk> \<Longrightarrow> a = b
[PROOF STEP]
apply (subst aGroup.ag_eq_diffzero[of R a b], assumption+)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>a \<in> carrier R; b \<in> carrier R; c \<in> carrier R; c \<noteq> \<zero>; (a \<plusminus> -\<^sub>a b) \<cdot>\<^sub>r c = \<zero>; aGroup R; a \<cdot>\<^sub>r c \<in> carrier R; b \<cdot>\<^sub>r c \<in> carrier R; -\<^sub>a b \<in> carrier R; a \<plusminus> -\<^sub>a b \<in> carrier R\<rbrakk> \<Longrightarrow> a \<plusminus> -\<^sub>a b = \<zero>
[PROOF STEP]
apply (rule contrapos_pp, simp+)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>a \<in> carrier R; b \<in> carrier R; c \<in> carrier R; c \<noteq> \<zero>; (a \<plusminus> -\<^sub>a b) \<cdot>\<^sub>r c = \<zero>; aGroup R; a \<cdot>\<^sub>r c \<in> carrier R; b \<cdot>\<^sub>r c \<in> carrier R; -\<^sub>a b \<in> carrier R; a \<plusminus> -\<^sub>a b \<in> carrier R; a \<plusminus> -\<^sub>a b \<noteq> \<zero>\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
apply (frule idom_tOp_nonzeros[of "a \<plusminus> -\<^sub>a b" c], assumption+, simp)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma (in Idomain) idom_mult_cancel_l:"\<lbrakk>a \<in> carrier R;
      b \<in> carrier R; c \<in> carrier R; c \<noteq> \<zero>; c \<cdot>\<^sub>r a = c \<cdot>\<^sub>r b\<rbrakk> \<Longrightarrow> a = b"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>a \<in> carrier R; b \<in> carrier R; c \<in> carrier R; c \<noteq> \<zero>; c \<cdot>\<^sub>r a = c \<cdot>\<^sub>r b\<rbrakk> \<Longrightarrow> a = b
[PROOF STEP]
apply (simp add:ring_tOp_commute)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>a \<in> carrier R; b \<in> carrier R; c \<in> carrier R; c \<noteq> \<zero>; a \<cdot>\<^sub>r c = b \<cdot>\<^sub>r c\<rbrakk> \<Longrightarrow> a = b
[PROOF STEP]
apply (simp add:idom_mult_cancel_r)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma (in Corps) invf_closed1:"x \<in> carrier K - {\<zero>} \<Longrightarrow>
                               invf K x \<in> (carrier K) - {\<zero>}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x \<in> carrier K - {\<zero>} \<Longrightarrow> x\<^bsup>\<hyphen> K\<^esup> \<in> carrier K - {\<zero>}
[PROOF STEP]
apply (frule  invf_inv[of x], erule conjE)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>x \<in> carrier K - {\<zero>}; x\<^bsup>\<hyphen> K\<^esup> \<in> carrier K; x\<^bsup>\<hyphen> K\<^esup> \<cdot>\<^sub>r x = 1\<^sub>r\<rbrakk> \<Longrightarrow> x\<^bsup>\<hyphen> K\<^esup> \<in> carrier K - {\<zero>}
[PROOF STEP]
apply (rule contrapos_pp, simp+)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>x \<in> carrier K \<and> x \<noteq> \<zero>; \<zero> \<in> carrier K; \<zero> \<cdot>\<^sub>r x = 1\<^sub>r; x\<^bsup>\<hyphen> K\<^esup> = \<zero>\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
apply (cut_tac f_is_ring)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>x \<in> carrier K \<and> x \<noteq> \<zero>; \<zero> \<in> carrier K; \<zero> \<cdot>\<^sub>r x = 1\<^sub>r; x\<^bsup>\<hyphen> K\<^esup> = \<zero>; Ring K\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
apply (
        simp add:Ring.ring_times_0_x[of K])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>x \<in> carrier K \<and> x \<noteq> 1\<^sub>r; 1\<^sub>r \<in> carrier K; \<zero> = 1\<^sub>r; x\<^bsup>\<hyphen> K\<^esup> = 1\<^sub>r; Ring K\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
apply (frule sym, thin_tac "\<zero> = 1\<^sub>r", simp, erule conjE)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<zero> \<in> carrier K; x\<^bsup>\<hyphen> K\<^esup> = \<zero>; Ring K; 1\<^sub>r = \<zero>; x \<in> carrier K; x \<noteq> \<zero>\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
apply (frule Ring.ring_l_one[of K x], assumption)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<zero> \<in> carrier K; x\<^bsup>\<hyphen> K\<^esup> = \<zero>; Ring K; 1\<^sub>r = \<zero>; x \<in> carrier K; x \<noteq> \<zero>; 1\<^sub>r \<cdot>\<^sub>r x = x\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
apply (rotate_tac -1, frule sym, thin_tac "1\<^sub>r \<cdot>\<^sub>r x = x",
        simp add:Ring.ring_times_0_x)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma (in Corps) linvf:"x \<in> carrier K - {\<zero>} \<Longrightarrow> (invf K x) \<cdot>\<^sub>r x = 1\<^sub>r"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x \<in> carrier K - {\<zero>} \<Longrightarrow> x\<^bsup>\<hyphen> K\<^esup> \<cdot>\<^sub>r x = 1\<^sub>r
[PROOF STEP]
by (simp add:invf_inv)


[STATEMENT]
lemma (in Corps) field_is_ring:"Ring K"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Ring K
[PROOF STEP]
by (simp add:f_is_ring)


[STATEMENT]
lemma (in Corps) invf_one:"1\<^sub>r \<noteq> \<zero>  \<Longrightarrow> invf K (1\<^sub>r) = 1\<^sub>r"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 1\<^sub>r \<noteq> \<zero> \<Longrightarrow> 1\<^sub>r\<^bsup>\<hyphen> K\<^esup> = 1\<^sub>r
[PROOF STEP]
apply (cut_tac field_is_ring)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>1\<^sub>r \<noteq> \<zero>; Ring K\<rbrakk> \<Longrightarrow> 1\<^sub>r\<^bsup>\<hyphen> K\<^esup> = 1\<^sub>r
[PROOF STEP]
apply (frule_tac Ring.ring_one)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>1\<^sub>r \<noteq> \<zero>; Ring K; 1\<^sub>r \<in> carrier K\<rbrakk> \<Longrightarrow> 1\<^sub>r\<^bsup>\<hyphen> K\<^esup> = 1\<^sub>r
[PROOF STEP]
apply (cut_tac invf_closed1 [of "1\<^sub>r"])
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>1\<^sub>r \<noteq> \<zero>; Ring K; 1\<^sub>r \<in> carrier K; 1\<^sub>r\<^bsup>\<hyphen> K\<^esup> \<in> carrier K - {\<zero>}\<rbrakk> \<Longrightarrow> 1\<^sub>r\<^bsup>\<hyphen> K\<^esup> = 1\<^sub>r
 2. \<lbrakk>1\<^sub>r \<noteq> \<zero>; Ring K; 1\<^sub>r \<in> carrier K\<rbrakk> \<Longrightarrow> 1\<^sub>r \<in> carrier K - {\<zero>}
[PROOF STEP]
apply (cut_tac linvf[of "1\<^sub>r"])
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<lbrakk>1\<^sub>r \<noteq> \<zero>; Ring K; 1\<^sub>r \<in> carrier K; 1\<^sub>r\<^bsup>\<hyphen> K\<^esup> \<in> carrier K - {\<zero>}; 1\<^sub>r\<^bsup>\<hyphen> K\<^esup> \<cdot>\<^sub>r 1\<^sub>r = 1\<^sub>r\<rbrakk> \<Longrightarrow> 1\<^sub>r\<^bsup>\<hyphen> K\<^esup> = 1\<^sub>r
 2. \<lbrakk>1\<^sub>r \<noteq> \<zero>; Ring K; 1\<^sub>r \<in> carrier K; 1\<^sub>r\<^bsup>\<hyphen> K\<^esup> \<in> carrier K - {\<zero>}\<rbrakk> \<Longrightarrow> 1\<^sub>r \<in> carrier K - {\<zero>}
 3. \<lbrakk>1\<^sub>r \<noteq> \<zero>; Ring K; 1\<^sub>r \<in> carrier K\<rbrakk> \<Longrightarrow> 1\<^sub>r \<in> carrier K - {\<zero>}
[PROOF STEP]
apply (simp add:Ring.ring_r_one[of "K"])
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>1\<^sub>r \<noteq> \<zero>; Ring K; 1\<^sub>r \<in> carrier K; 1\<^sub>r\<^bsup>\<hyphen> K\<^esup> \<in> carrier K - {\<zero>}\<rbrakk> \<Longrightarrow> 1\<^sub>r \<in> carrier K - {\<zero>}
 2. \<lbrakk>1\<^sub>r \<noteq> \<zero>; Ring K; 1\<^sub>r \<in> carrier K\<rbrakk> \<Longrightarrow> 1\<^sub>r \<in> carrier K - {\<zero>}
[PROOF STEP]
apply simp+
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma (in Corps) field_tOp_assoc:"\<lbrakk>x \<in> carrier K; y \<in> carrier K; z \<in> carrier K\<rbrakk>
                                \<Longrightarrow> x \<cdot>\<^sub>r y \<cdot>\<^sub>r z =  x \<cdot>\<^sub>r (y \<cdot>\<^sub>r z)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>x \<in> carrier K; y \<in> carrier K; z \<in> carrier K\<rbrakk> \<Longrightarrow> x \<cdot>\<^sub>r y \<cdot>\<^sub>r z = x \<cdot>\<^sub>r (y \<cdot>\<^sub>r z)
[PROOF STEP]
apply (cut_tac field_is_ring)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>x \<in> carrier K; y \<in> carrier K; z \<in> carrier K; Ring K\<rbrakk> \<Longrightarrow> x \<cdot>\<^sub>r y \<cdot>\<^sub>r z = x \<cdot>\<^sub>r (y \<cdot>\<^sub>r z)
[PROOF STEP]
apply (simp add:Ring.ring_tOp_assoc)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma (in Corps) field_tOp_commute:"\<lbrakk>x \<in> carrier K; y \<in> carrier K\<rbrakk>
                                \<Longrightarrow> x \<cdot>\<^sub>r y  =  y \<cdot>\<^sub>r x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>x \<in> carrier K; y \<in> carrier K\<rbrakk> \<Longrightarrow> x \<cdot>\<^sub>r y = y \<cdot>\<^sub>r x
[PROOF STEP]
apply (cut_tac field_is_ring)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>x \<in> carrier K; y \<in> carrier K; Ring K\<rbrakk> \<Longrightarrow> x \<cdot>\<^sub>r y = y \<cdot>\<^sub>r x
[PROOF STEP]
apply (simp add:Ring.ring_tOp_commute)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma (in Corps) field_inv_inv:"\<lbrakk>x \<in> carrier K; x \<noteq> \<zero>\<rbrakk> \<Longrightarrow> (x\<^bsup>\<hyphen>K\<^esup>)\<^bsup>\<hyphen>K\<^esup> = x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>x \<in> carrier K; x \<noteq> \<zero>\<rbrakk> \<Longrightarrow> x\<^bsup>\<hyphen> K\<^esup>\<^bsup>\<hyphen> K\<^esup> = x
[PROOF STEP]
apply (cut_tac invf_closed1[of "x"])
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>x \<in> carrier K; x \<noteq> \<zero>; x\<^bsup>\<hyphen> K\<^esup> \<in> carrier K - {\<zero>}\<rbrakk> \<Longrightarrow> x\<^bsup>\<hyphen> K\<^esup>\<^bsup>\<hyphen> K\<^esup> = x
 2. \<lbrakk>x \<in> carrier K; x \<noteq> \<zero>\<rbrakk> \<Longrightarrow> x \<in> carrier K - {\<zero>}
[PROOF STEP]
apply (cut_tac invf_inv[of "x\<^bsup>\<hyphen>K\<^esup>"], erule conjE)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<lbrakk>x \<in> carrier K; x \<noteq> \<zero>; x\<^bsup>\<hyphen> K\<^esup> \<in> carrier K - {\<zero>}; x\<^bsup>\<hyphen> K\<^esup>\<^bsup>\<hyphen> K\<^esup> \<in> carrier K; x\<^bsup>\<hyphen> K\<^esup>\<^bsup>\<hyphen> K\<^esup> \<cdot>\<^sub>r x\<^bsup>\<hyphen> K\<^esup> = 1\<^sub>r\<rbrakk> \<Longrightarrow> x\<^bsup>\<hyphen> K\<^esup>\<^bsup>\<hyphen> K\<^esup> = x
 2. \<lbrakk>x \<in> carrier K; x \<noteq> \<zero>; x\<^bsup>\<hyphen> K\<^esup> \<in> carrier K - {\<zero>}\<rbrakk> \<Longrightarrow> x\<^bsup>\<hyphen> K\<^esup> \<in> carrier K - {\<zero>}
 3. \<lbrakk>x \<in> carrier K; x \<noteq> \<zero>\<rbrakk> \<Longrightarrow> x \<in> carrier K - {\<zero>}
[PROOF STEP]
apply (frule field_tOp_assoc[THEN sym, of "x\<^bsup>\<hyphen> K\<^esup>\<^bsup>\<hyphen> K\<^esup>" "x\<^bsup>\<hyphen> K\<^esup>" "x"],
        simp, assumption, simp)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<lbrakk>x \<in> carrier K; x \<noteq> \<zero>; x\<^bsup>\<hyphen> K\<^esup> \<in> carrier K \<and> x\<^bsup>\<hyphen> K\<^esup> \<noteq> \<zero>; x\<^bsup>\<hyphen> K\<^esup>\<^bsup>\<hyphen> K\<^esup> \<in> carrier K; x\<^bsup>\<hyphen> K\<^esup>\<^bsup>\<hyphen> K\<^esup> \<cdot>\<^sub>r x\<^bsup>\<hyphen> K\<^esup> = 1\<^sub>r; x\<^bsup>\<hyphen> K\<^esup>\<^bsup>\<hyphen> K\<^esup> \<cdot>\<^sub>r (x\<^bsup>\<hyphen> K\<^esup> \<cdot>\<^sub>r x) = 1\<^sub>r \<cdot>\<^sub>r x\<rbrakk> \<Longrightarrow> x\<^bsup>\<hyphen> K\<^esup>\<^bsup>\<hyphen> K\<^esup> = x
 2. \<lbrakk>x \<in> carrier K; x \<noteq> \<zero>; x\<^bsup>\<hyphen> K\<^esup> \<in> carrier K - {\<zero>}\<rbrakk> \<Longrightarrow> x\<^bsup>\<hyphen> K\<^esup> \<in> carrier K - {\<zero>}
 3. \<lbrakk>x \<in> carrier K; x \<noteq> \<zero>\<rbrakk> \<Longrightarrow> x \<in> carrier K - {\<zero>}
[PROOF STEP]
apply (cut_tac field_is_ring,
        simp add:Ring.ring_l_one Ring.ring_r_one, erule conjE,
        cut_tac invf_inv[of x], erule conjE, simp add:Ring.ring_r_one)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<lbrakk>x \<in> carrier K; x \<noteq> \<zero>; x\<^bsup>\<hyphen> K\<^esup>\<^bsup>\<hyphen> K\<^esup> \<in> carrier K; x\<^bsup>\<hyphen> K\<^esup>\<^bsup>\<hyphen> K\<^esup> \<cdot>\<^sub>r x\<^bsup>\<hyphen> K\<^esup> = 1\<^sub>r; x\<^bsup>\<hyphen> K\<^esup>\<^bsup>\<hyphen> K\<^esup> \<cdot>\<^sub>r (x\<^bsup>\<hyphen> K\<^esup> \<cdot>\<^sub>r x) = x; Ring K; x\<^bsup>\<hyphen> K\<^esup> \<in> carrier K; x\<^bsup>\<hyphen> K\<^esup> \<noteq> \<zero>\<rbrakk> \<Longrightarrow> x \<in> carrier K - {\<zero>}
 2. \<lbrakk>x \<in> carrier K; x \<noteq> \<zero>; x\<^bsup>\<hyphen> K\<^esup> \<in> carrier K - {\<zero>}\<rbrakk> \<Longrightarrow> x\<^bsup>\<hyphen> K\<^esup> \<in> carrier K - {\<zero>}
 3. \<lbrakk>x \<in> carrier K; x \<noteq> \<zero>\<rbrakk> \<Longrightarrow> x \<in> carrier K - {\<zero>}
[PROOF STEP]
apply simp+
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma (in Corps) field_is_idom:"Idomain K"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Idomain K
[PROOF STEP]
apply (rule Idomain.intro)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. Ring K
 2. Idomain_axioms K
[PROOF STEP]
apply (simp add:field_is_ring)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Idomain_axioms K
[PROOF STEP]
apply (cut_tac field_is_ring)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Ring K \<Longrightarrow> Idomain_axioms K
[PROOF STEP]
apply (rule Idomain_axioms.intro)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a b. \<lbrakk>Ring K; a \<in> carrier K; b \<in> carrier K; a \<cdot>\<^sub>r b = \<zero>\<rbrakk> \<Longrightarrow> a = \<zero> \<or> b = \<zero>
[PROOF STEP]
apply (rule contrapos_pp, simp+, erule conjE)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a b. \<lbrakk>Ring K; a \<in> carrier K; b \<in> carrier K; a \<cdot>\<^sub>r b = \<zero>; a \<noteq> \<zero>; b \<noteq> \<zero>\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
apply (cut_tac x = a in invf_closed1, simp, simp, erule conjE)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a b. \<lbrakk>Ring K; a \<in> carrier K; b \<in> carrier K; a \<cdot>\<^sub>r b = \<zero>; a \<noteq> \<zero>; b \<noteq> \<zero>; a\<^bsup>\<hyphen> K\<^esup> \<in> carrier K; a\<^bsup>\<hyphen> K\<^esup> \<noteq> \<zero>\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
apply (frule_tac x = "a\<^bsup>\<hyphen> K\<^esup>" and y = a and z = b in field_tOp_assoc,
         assumption+)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a b. \<lbrakk>Ring K; a \<in> carrier K; b \<in> carrier K; a \<cdot>\<^sub>r b = \<zero>; a \<noteq> \<zero>; b \<noteq> \<zero>; a\<^bsup>\<hyphen> K\<^esup> \<in> carrier K; a\<^bsup>\<hyphen> K\<^esup> \<noteq> \<zero>; a\<^bsup>\<hyphen> K\<^esup> \<cdot>\<^sub>r a \<cdot>\<^sub>r b = a\<^bsup>\<hyphen> K\<^esup> \<cdot>\<^sub>r (a \<cdot>\<^sub>r b)\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
apply (simp add:linvf Ring.ring_times_x_0 Ring.ring_l_one)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma (in Corps) field_potent_nonzero:"\<lbrakk>x \<in> carrier K; x \<noteq> \<zero>\<rbrakk> \<Longrightarrow>
                                       x^\<^bsup>K n\<^esup> \<noteq> \<zero>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>x \<in> carrier K; x \<noteq> \<zero>\<rbrakk> \<Longrightarrow> x^\<^bsup>K n\<^esup> \<noteq> \<zero>
[PROOF STEP]
apply (cut_tac field_is_idom)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>x \<in> carrier K; x \<noteq> \<zero>; Idomain K\<rbrakk> \<Longrightarrow> x^\<^bsup>K n\<^esup> \<noteq> \<zero>
[PROOF STEP]
apply (cut_tac field_is_ring,
       simp add:Idomain.idom_potent_nonzero)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma (in Corps) field_potent_nonzero1:"\<lbrakk>x \<in> carrier K; x \<noteq> \<zero>\<rbrakk> \<Longrightarrow> x\<^bsub>K\<^esub>\<^bsup>n\<^esup>  \<noteq> \<zero>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>x \<in> carrier K; x \<noteq> \<zero>\<rbrakk> \<Longrightarrow> x\<^bsub>K\<^esub>\<^bsup>n\<^esup> \<noteq> \<zero>
[PROOF STEP]
apply (simp add:npowf_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>x \<in> carrier K; x \<noteq> \<zero>\<rbrakk> \<Longrightarrow> (0 \<le> n \<longrightarrow> x^\<^bsup>K nat n\<^esup> \<noteq> \<zero>) \<and> (\<not> 0 \<le> n \<longrightarrow> x\<^bsup>\<hyphen> K\<^esup>^\<^bsup>K nat (- n)\<^esup> \<noteq> \<zero>)
[PROOF STEP]
apply (case_tac "0 \<le> n")
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>x \<in> carrier K; x \<noteq> \<zero>; 0 \<le> n\<rbrakk> \<Longrightarrow> (0 \<le> n \<longrightarrow> x^\<^bsup>K nat n\<^esup> \<noteq> \<zero>) \<and> (\<not> 0 \<le> n \<longrightarrow> x\<^bsup>\<hyphen> K\<^esup>^\<^bsup>K nat (- n)\<^esup> \<noteq> \<zero>)
 2. \<lbrakk>x \<in> carrier K; x \<noteq> \<zero>; \<not> 0 \<le> n\<rbrakk> \<Longrightarrow> (0 \<le> n \<longrightarrow> x^\<^bsup>K nat n\<^esup> \<noteq> \<zero>) \<and> (\<not> 0 \<le> n \<longrightarrow> x\<^bsup>\<hyphen> K\<^esup>^\<^bsup>K nat (- n)\<^esup> \<noteq> \<zero>)
[PROOF STEP]
apply (simp add:field_potent_nonzero)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>x \<in> carrier K; x \<noteq> \<zero>; \<not> 0 \<le> n\<rbrakk> \<Longrightarrow> (0 \<le> n \<longrightarrow> x^\<^bsup>K nat n\<^esup> \<noteq> \<zero>) \<and> (\<not> 0 \<le> n \<longrightarrow> x\<^bsup>\<hyphen> K\<^esup>^\<^bsup>K nat (- n)\<^esup> \<noteq> \<zero>)
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>x \<in> carrier K; x \<noteq> \<zero>; \<not> 0 \<le> n\<rbrakk> \<Longrightarrow> x\<^bsup>\<hyphen> K\<^esup>^\<^bsup>K nat (- n)\<^esup> \<noteq> \<zero>
[PROOF STEP]
apply (cut_tac invf_closed1[of "x"], simp+, (erule conjE)+)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>x \<in> carrier K; x \<noteq> \<zero>; \<not> 0 \<le> n; x\<^bsup>\<hyphen> K\<^esup> \<in> carrier K; x\<^bsup>\<hyphen> K\<^esup> \<noteq> \<zero>\<rbrakk> \<Longrightarrow> x\<^bsup>\<hyphen> K\<^esup>^\<^bsup>K nat (- n)\<^esup> \<noteq> \<zero>
 2. \<lbrakk>x \<in> carrier K; x \<noteq> \<zero>; \<not> 0 \<le> n\<rbrakk> \<Longrightarrow> x \<in> carrier K - {\<zero>}
[PROOF STEP]
apply (simp add:field_potent_nonzero)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>x \<in> carrier K; x \<noteq> \<zero>; \<not> 0 \<le> n\<rbrakk> \<Longrightarrow> x \<in> carrier K - {\<zero>}
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma (in Corps) field_nilp_zero:"\<lbrakk>x \<in> carrier K; x^\<^bsup>K n\<^esup> = \<zero>\<rbrakk> \<Longrightarrow> x = \<zero>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>x \<in> carrier K; x^\<^bsup>K n\<^esup> = \<zero>\<rbrakk> \<Longrightarrow> x = \<zero>
[PROOF STEP]
by (rule contrapos_pp, simp+, simp add:field_potent_nonzero)


[STATEMENT]
lemma (in Corps) npowf_mem:"\<lbrakk>a \<in> carrier K; a \<noteq> \<zero>\<rbrakk> \<Longrightarrow>
                                    npowf K a n \<in> carrier K"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>a \<in> carrier K; a \<noteq> \<zero>\<rbrakk> \<Longrightarrow> a\<^bsub>K\<^esub>\<^bsup>n\<^esup> \<in> carrier K
[PROOF STEP]
apply (simp add:npowf_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>a \<in> carrier K; a \<noteq> \<zero>\<rbrakk> \<Longrightarrow> (0 \<le> n \<longrightarrow> a^\<^bsup>K nat n\<^esup> \<in> carrier K) \<and> (\<not> 0 \<le> n \<longrightarrow> a\<^bsup>\<hyphen> K\<^esup>^\<^bsup>K nat (- n)\<^esup> \<in> carrier K)
[PROOF STEP]
apply (cut_tac field_is_ring)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>a \<in> carrier K; a \<noteq> \<zero>; Ring K\<rbrakk> \<Longrightarrow> (0 \<le> n \<longrightarrow> a^\<^bsup>K nat n\<^esup> \<in> carrier K) \<and> (\<not> 0 \<le> n \<longrightarrow> a\<^bsup>\<hyphen> K\<^esup>^\<^bsup>K nat (- n)\<^esup> \<in> carrier K)
[PROOF STEP]
apply (case_tac "0 \<le> n", simp,
       simp add:Ring.npClose, simp)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>a \<in> carrier K; a \<noteq> \<zero>; Ring K; \<not> 0 \<le> n\<rbrakk> \<Longrightarrow> a\<^bsup>\<hyphen> K\<^esup>^\<^bsup>K nat (- n)\<^esup> \<in> carrier K
[PROOF STEP]
apply (cut_tac invf_closed1[of "a"], simp, erule conjE,
       simp add:Ring.npClose, simp)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma (in Corps) field_npowf_exp_zero:"\<lbrakk>a \<in> carrier K; a \<noteq> \<zero>\<rbrakk> \<Longrightarrow>
                                    npowf K a 0 = 1\<^sub>r"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>a \<in> carrier K; a \<noteq> \<zero>\<rbrakk> \<Longrightarrow> a\<^bsub>K\<^esub>\<^bsup>0\<^esup> = 1\<^sub>r
[PROOF STEP]
by (cut_tac field_is_ring, simp add:npowf_def)