[STATEMENT]
lemma (in Corps) npow_exp_minusTr1:"\<lbrakk>x \<in> carrier K; x \<noteq> \<zero>; 0 \<le> i\<rbrakk>  \<Longrightarrow>
       0 \<le> i - (int j) \<longrightarrow>  x\<^bsub>K\<^esub>\<^bsup>(i - (int j))\<^esup> = x^\<^bsup>K (nat i)\<^esup> \<cdot>\<^sub>r (x\<^bsup>\<hyphen>K\<^esup>)^\<^bsup>K j\<^esup>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>x \<in> carrier K; x \<noteq> \<zero>; 0 \<le> i\<rbrakk> \<Longrightarrow> 0 \<le> i - int j \<longrightarrow> x\<^bsub>K\<^esub>\<^bsup>(i - int j)\<^esup> = x^\<^bsup>K nat i\<^esup> \<cdot>\<^sub>r x\<^bsup>\<hyphen> K\<^esup>^\<^bsup>K j\<^esup>
[PROOF STEP]
apply (cut_tac field_is_ring,
       cut_tac invf_closed1[of "x"], simp,
       simp add:npowf_def, erule conjE)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>x \<in> carrier K; x \<noteq> \<zero>; 0 \<le> i; Ring K; x\<^bsup>\<hyphen> K\<^esup> \<in> carrier K; x\<^bsup>\<hyphen> K\<^esup> \<noteq> \<zero>\<rbrakk> \<Longrightarrow> int j \<le> i \<longrightarrow> x^\<^bsup>K nat (i - int j)\<^esup> = x^\<^bsup>K nat i\<^esup> \<cdot>\<^sub>r x\<^bsup>\<hyphen> K\<^esup>^\<^bsup>K j\<^esup>
 2. \<lbrakk>x \<in> carrier K; x \<noteq> \<zero>; 0 \<le> i; Ring K\<rbrakk> \<Longrightarrow> x \<in> carrier K - {\<zero>}
[PROOF STEP]
apply (induct_tac "j", simp)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<lbrakk>x \<in> carrier K; x \<noteq> \<zero>; 0 \<le> i; Ring K; x\<^bsup>\<hyphen> K\<^esup> \<in> carrier K; x\<^bsup>\<hyphen> K\<^esup> \<noteq> \<zero>\<rbrakk> \<Longrightarrow> x^\<^bsup>K nat i\<^esup> = x^\<^bsup>K nat i\<^esup> \<cdot>\<^sub>r 1\<^sub>r
 2. \<And>n. \<lbrakk>x \<in> carrier K; x \<noteq> \<zero>; 0 \<le> i; Ring K; x\<^bsup>\<hyphen> K\<^esup> \<in> carrier K; x\<^bsup>\<hyphen> K\<^esup> \<noteq> \<zero>; int n \<le> i \<longrightarrow> x^\<^bsup>K nat (i - int n)\<^esup> = x^\<^bsup>K nat i\<^esup> \<cdot>\<^sub>r x\<^bsup>\<hyphen> K\<^esup>^\<^bsup>K n\<^esup>\<rbrakk> \<Longrightarrow> int (Suc n) \<le> i \<longrightarrow> x^\<^bsup>K nat (i - int (Suc n))\<^esup> = x^\<^bsup>K nat i\<^esup> \<cdot>\<^sub>r x\<^bsup>\<hyphen> K\<^esup>^\<^bsup>K Suc n\<^esup>
 3. \<lbrakk>x \<in> carrier K; x \<noteq> \<zero>; 0 \<le> i; Ring K\<rbrakk> \<Longrightarrow> x \<in> carrier K - {\<zero>}
[PROOF STEP]
apply (frule Ring.npClose[of "K" "x" "nat i"], assumption+,
        simp add:Ring.ring_r_one)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>n. \<lbrakk>x \<in> carrier K; x \<noteq> \<zero>; 0 \<le> i; Ring K; x\<^bsup>\<hyphen> K\<^esup> \<in> carrier K; x\<^bsup>\<hyphen> K\<^esup> \<noteq> \<zero>; int n \<le> i \<longrightarrow> x^\<^bsup>K nat (i - int n)\<^esup> = x^\<^bsup>K nat i\<^esup> \<cdot>\<^sub>r x\<^bsup>\<hyphen> K\<^esup>^\<^bsup>K n\<^esup>\<rbrakk> \<Longrightarrow> int (Suc n) \<le> i \<longrightarrow> x^\<^bsup>K nat (i - int (Suc n))\<^esup> = x^\<^bsup>K nat i\<^esup> \<cdot>\<^sub>r x\<^bsup>\<hyphen> K\<^esup>^\<^bsup>K Suc n\<^esup>
 2. \<lbrakk>x \<in> carrier K; x \<noteq> \<zero>; 0 \<le> i; Ring K\<rbrakk> \<Longrightarrow> x \<in> carrier K - {\<zero>}
[PROOF STEP]
apply (rule impI, simp)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>n. \<lbrakk>x \<in> carrier K; x \<noteq> \<zero>; Ring K; x\<^bsup>\<hyphen> K\<^esup> \<in> carrier K; x\<^bsup>\<hyphen> K\<^esup> \<noteq> \<zero>; x^\<^bsup>K nat (i - int n)\<^esup> = x^\<^bsup>K nat i\<^esup> \<cdot>\<^sub>r x\<^bsup>\<hyphen> K\<^esup>^\<^bsup>K n\<^esup>; 1 + int n \<le> i\<rbrakk> \<Longrightarrow> x^\<^bsup>K nat (i - (1 + int n))\<^esup> = x^\<^bsup>K nat i\<^esup> \<cdot>\<^sub>r (x\<^bsup>\<hyphen> K\<^esup>^\<^bsup>K n\<^esup> \<cdot>\<^sub>r x\<^bsup>\<hyphen> K\<^esup>)
 2. \<lbrakk>x \<in> carrier K; x \<noteq> \<zero>; 0 \<le> i; Ring K\<rbrakk> \<Longrightarrow> x \<in> carrier K - {\<zero>}
[PROOF STEP]
apply (subst zdiff)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>n. \<lbrakk>x \<in> carrier K; x \<noteq> \<zero>; Ring K; x\<^bsup>\<hyphen> K\<^esup> \<in> carrier K; x\<^bsup>\<hyphen> K\<^esup> \<noteq> \<zero>; x^\<^bsup>K nat (i - int n)\<^esup> = x^\<^bsup>K nat i\<^esup> \<cdot>\<^sub>r x\<^bsup>\<hyphen> K\<^esup>^\<^bsup>K n\<^esup>; 1 + int n \<le> i\<rbrakk> \<Longrightarrow> x^\<^bsup>K nat (i + - (1 + int n))\<^esup> = x^\<^bsup>K nat i\<^esup> \<cdot>\<^sub>r (x\<^bsup>\<hyphen> K\<^esup>^\<^bsup>K n\<^esup> \<cdot>\<^sub>r x\<^bsup>\<hyphen> K\<^esup>)
 2. \<lbrakk>x \<in> carrier K; x \<noteq> \<zero>; 0 \<le> i; Ring K\<rbrakk> \<Longrightarrow> x \<in> carrier K - {\<zero>}
[PROOF STEP]
apply (simp add:add.commute[of "1"])
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>n. \<lbrakk>x \<in> carrier K; x \<noteq> \<zero>; Ring K; x\<^bsup>\<hyphen> K\<^esup> \<in> carrier K; x\<^bsup>\<hyphen> K\<^esup> \<noteq> \<zero>; x^\<^bsup>K nat (i - int n)\<^esup> = x^\<^bsup>K nat i\<^esup> \<cdot>\<^sub>r x\<^bsup>\<hyphen> K\<^esup>^\<^bsup>K n\<^esup>; int n + 1 \<le> i\<rbrakk> \<Longrightarrow> x^\<^bsup>K nat (i + (- int n - 1))\<^esup> = x^\<^bsup>K nat i\<^esup> \<cdot>\<^sub>r (x\<^bsup>\<hyphen> K\<^esup>^\<^bsup>K n\<^esup> \<cdot>\<^sub>r x\<^bsup>\<hyphen> K\<^esup>)
 2. \<lbrakk>x \<in> carrier K; x \<noteq> \<zero>; 0 \<le> i; Ring K\<rbrakk> \<Longrightarrow> x \<in> carrier K - {\<zero>}
[PROOF STEP]
apply (cut_tac z = i and w = "int n + 1" in zdiff,
       simp only:minus_add_distrib,
       thin_tac "i - (int n + 1) = i + (- int n + - 1)")
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>n. \<lbrakk>x \<in> carrier K; x \<noteq> \<zero>; Ring K; x\<^bsup>\<hyphen> K\<^esup> \<in> carrier K; x\<^bsup>\<hyphen> K\<^esup> \<noteq> \<zero>; x^\<^bsup>K nat (i - int n)\<^esup> = x^\<^bsup>K nat i\<^esup> \<cdot>\<^sub>r x\<^bsup>\<hyphen> K\<^esup>^\<^bsup>K n\<^esup>; int n + 1 \<le> i\<rbrakk> \<Longrightarrow> x^\<^bsup>K nat (i + (- int n - 1))\<^esup> = x^\<^bsup>K nat i\<^esup> \<cdot>\<^sub>r (x\<^bsup>\<hyphen> K\<^esup>^\<^bsup>K n\<^esup> \<cdot>\<^sub>r x\<^bsup>\<hyphen> K\<^esup>)
 2. \<lbrakk>x \<in> carrier K; x \<noteq> \<zero>; 0 \<le> i; Ring K\<rbrakk> \<Longrightarrow> x \<in> carrier K - {\<zero>}
[PROOF STEP]
apply (cut_tac z = "i + - int n" in nat_diff_distrib[of "1"],
         simp, simp)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>n. \<lbrakk>x \<in> carrier K; x \<noteq> \<zero>; Ring K; x\<^bsup>\<hyphen> K\<^esup> \<in> carrier K; x\<^bsup>\<hyphen> K\<^esup> \<noteq> \<zero>; x^\<^bsup>K nat (i - int n)\<^esup> = x^\<^bsup>K nat i\<^esup> \<cdot>\<^sub>r x\<^bsup>\<hyphen> K\<^esup>^\<^bsup>K n\<^esup>; int n + 1 \<le> i; nat (i + - int n - 1) = nat (i + - int n) - nat 1\<rbrakk> \<Longrightarrow> x^\<^bsup>K nat (i + (- int n - 1))\<^esup> = x^\<^bsup>K nat i\<^esup> \<cdot>\<^sub>r (x\<^bsup>\<hyphen> K\<^esup>^\<^bsup>K n\<^esup> \<cdot>\<^sub>r x\<^bsup>\<hyphen> K\<^esup>)
 2. \<lbrakk>x \<in> carrier K; x \<noteq> \<zero>; 0 \<le> i; Ring K\<rbrakk> \<Longrightarrow> x \<in> carrier K - {\<zero>}
[PROOF STEP]
apply (simp only:zdiff[of _ "1"], simp)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>n. \<lbrakk>x \<in> carrier K; x \<noteq> \<zero>; Ring K; x\<^bsup>\<hyphen> K\<^esup> \<in> carrier K; x\<^bsup>\<hyphen> K\<^esup> \<noteq> \<zero>; x^\<^bsup>K nat (i - int n)\<^esup> = x^\<^bsup>K nat i\<^esup> \<cdot>\<^sub>r x\<^bsup>\<hyphen> K\<^esup>^\<^bsup>K n\<^esup>; int n + 1 \<le> i; nat (i - int n - 1) = nat (i - int n) - Suc 0\<rbrakk> \<Longrightarrow> x^\<^bsup>K nat (i + (- int n - 1))\<^esup> = x^\<^bsup>K nat i\<^esup> \<cdot>\<^sub>r (x\<^bsup>\<hyphen> K\<^esup>^\<^bsup>K n\<^esup> \<cdot>\<^sub>r x\<^bsup>\<hyphen> K\<^esup>)
 2. \<lbrakk>x \<in> carrier K; x \<noteq> \<zero>; 0 \<le> i; Ring K\<rbrakk> \<Longrightarrow> x \<in> carrier K - {\<zero>}
[PROOF STEP]
apply (cut_tac field_is_idom)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>n. \<lbrakk>x \<in> carrier K; x \<noteq> \<zero>; Ring K; x\<^bsup>\<hyphen> K\<^esup> \<in> carrier K; x\<^bsup>\<hyphen> K\<^esup> \<noteq> \<zero>; x^\<^bsup>K nat (i - int n)\<^esup> = x^\<^bsup>K nat i\<^esup> \<cdot>\<^sub>r x\<^bsup>\<hyphen> K\<^esup>^\<^bsup>K n\<^esup>; int n + 1 \<le> i; nat (i - int n - 1) = nat (i - int n) - Suc 0; Idomain K\<rbrakk> \<Longrightarrow> x^\<^bsup>K nat (i + (- int n - 1))\<^esup> = x^\<^bsup>K nat i\<^esup> \<cdot>\<^sub>r (x\<^bsup>\<hyphen> K\<^esup>^\<^bsup>K n\<^esup> \<cdot>\<^sub>r x\<^bsup>\<hyphen> K\<^esup>)
 2. \<lbrakk>x \<in> carrier K; x \<noteq> \<zero>; 0 \<le> i; Ring K\<rbrakk> \<Longrightarrow> x \<in> carrier K - {\<zero>}
[PROOF STEP]
apply (frule_tac n = "nat i" in Ring.npClose[of "K" "x"], assumption+,
       frule_tac n = "nat i" in Ring.npClose[of "K" "x\<^bsup>\<hyphen> K\<^esup>"], assumption+,
       frule_tac n = n in Ring.npClose[of "K" "x\<^bsup>\<hyphen> K\<^esup>"], assumption+ )
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>n. \<lbrakk>x \<in> carrier K; x \<noteq> \<zero>; Ring K; x\<^bsup>\<hyphen> K\<^esup> \<in> carrier K; x\<^bsup>\<hyphen> K\<^esup> \<noteq> \<zero>; x^\<^bsup>K nat (i - int n)\<^esup> = x^\<^bsup>K nat i\<^esup> \<cdot>\<^sub>r x\<^bsup>\<hyphen> K\<^esup>^\<^bsup>K n\<^esup>; int n + 1 \<le> i; nat (i - int n - 1) = nat (i - int n) - Suc 0; Idomain K; x^\<^bsup>K nat i\<^esup> \<in> carrier K; x\<^bsup>\<hyphen> K\<^esup>^\<^bsup>K nat i\<^esup> \<in> carrier K; x\<^bsup>\<hyphen> K\<^esup>^\<^bsup>K n\<^esup> \<in> carrier K\<rbrakk> \<Longrightarrow> x^\<^bsup>K nat (i + (- int n - 1))\<^esup> = x^\<^bsup>K nat i\<^esup> \<cdot>\<^sub>r (x\<^bsup>\<hyphen> K\<^esup>^\<^bsup>K n\<^esup> \<cdot>\<^sub>r x\<^bsup>\<hyphen> K\<^esup>)
 2. \<lbrakk>x \<in> carrier K; x \<noteq> \<zero>; 0 \<le> i; Ring K\<rbrakk> \<Longrightarrow> x \<in> carrier K - {\<zero>}
[PROOF STEP]
apply (rule_tac a = "x^\<^bsup>K (nat (i + (- int n - 1)))\<^esup>" and
       b = "x^\<^bsup>K (nat i)\<^esup> \<cdot>\<^sub>r (x\<^bsup>\<hyphen> K\<^esup>^\<^bsup>K n\<^esup> \<cdot>\<^sub>r x\<^bsup>\<hyphen> K\<^esup>)" and c = x in
       Idomain.idom_mult_cancel_r[of "K"], assumption+)
[PROOF STATE]
proof (prove)
goal (6 subgoals):
 1. \<And>n. \<lbrakk>x \<in> carrier K; x \<noteq> \<zero>; Ring K; x\<^bsup>\<hyphen> K\<^esup> \<in> carrier K; x\<^bsup>\<hyphen> K\<^esup> \<noteq> \<zero>; x^\<^bsup>K nat (i - int n)\<^esup> = x^\<^bsup>K nat i\<^esup> \<cdot>\<^sub>r x\<^bsup>\<hyphen> K\<^esup>^\<^bsup>K n\<^esup>; int n + 1 \<le> i; nat (i - int n - 1) = nat (i - int n) - Suc 0; Idomain K; x^\<^bsup>K nat i\<^esup> \<in> carrier K; x\<^bsup>\<hyphen> K\<^esup>^\<^bsup>K nat i\<^esup> \<in> carrier K; x\<^bsup>\<hyphen> K\<^esup>^\<^bsup>K n\<^esup> \<in> carrier K\<rbrakk> \<Longrightarrow> x^\<^bsup>K nat (i + (- int n - 1))\<^esup> \<in> carrier K
 2. \<And>n. \<lbrakk>x \<in> carrier K; x \<noteq> \<zero>; Ring K; x\<^bsup>\<hyphen> K\<^esup> \<in> carrier K; x\<^bsup>\<hyphen> K\<^esup> \<noteq> \<zero>; x^\<^bsup>K nat (i - int n)\<^esup> = x^\<^bsup>K nat i\<^esup> \<cdot>\<^sub>r x\<^bsup>\<hyphen> K\<^esup>^\<^bsup>K n\<^esup>; int n + 1 \<le> i; nat (i - int n - 1) = nat (i - int n) - Suc 0; Idomain K; x^\<^bsup>K nat i\<^esup> \<in> carrier K; x\<^bsup>\<hyphen> K\<^esup>^\<^bsup>K nat i\<^esup> \<in> carrier K; x\<^bsup>\<hyphen> K\<^esup>^\<^bsup>K n\<^esup> \<in> carrier K\<rbrakk> \<Longrightarrow> x^\<^bsup>K nat i\<^esup> \<cdot>\<^sub>r (x\<^bsup>\<hyphen> K\<^esup>^\<^bsup>K n\<^esup> \<cdot>\<^sub>r x\<^bsup>\<hyphen> K\<^esup>) \<in> carrier K
 3. \<And>n. \<lbrakk>x \<in> carrier K; x \<noteq> \<zero>; Ring K; x\<^bsup>\<hyphen> K\<^esup> \<in> carrier K; x\<^bsup>\<hyphen> K\<^esup> \<noteq> \<zero>; x^\<^bsup>K nat (i - int n)\<^esup> = x^\<^bsup>K nat i\<^esup> \<cdot>\<^sub>r x\<^bsup>\<hyphen> K\<^esup>^\<^bsup>K n\<^esup>; int n + 1 \<le> i; nat (i - int n - 1) = nat (i - int n) - Suc 0; Idomain K; x^\<^bsup>K nat i\<^esup> \<in> carrier K; x\<^bsup>\<hyphen> K\<^esup>^\<^bsup>K nat i\<^esup> \<in> carrier K; x\<^bsup>\<hyphen> K\<^esup>^\<^bsup>K n\<^esup> \<in> carrier K\<rbrakk> \<Longrightarrow> x \<in> carrier K
 4. \<And>n. \<lbrakk>x \<in> carrier K; x \<noteq> \<zero>; Ring K; x\<^bsup>\<hyphen> K\<^esup> \<in> carrier K; x\<^bsup>\<hyphen> K\<^esup> \<noteq> \<zero>; x^\<^bsup>K nat (i - int n)\<^esup> = x^\<^bsup>K nat i\<^esup> \<cdot>\<^sub>r x\<^bsup>\<hyphen> K\<^esup>^\<^bsup>K n\<^esup>; int n + 1 \<le> i; nat (i - int n - 1) = nat (i - int n) - Suc 0; Idomain K; x^\<^bsup>K nat i\<^esup> \<in> carrier K; x\<^bsup>\<hyphen> K\<^esup>^\<^bsup>K nat i\<^esup> \<in> carrier K; x\<^bsup>\<hyphen> K\<^esup>^\<^bsup>K n\<^esup> \<in> carrier K\<rbrakk> \<Longrightarrow> x \<noteq> \<zero>
 5. \<And>n. \<lbrakk>x \<in> carrier K; x \<noteq> \<zero>; Ring K; x\<^bsup>\<hyphen> K\<^esup> \<in> carrier K; x\<^bsup>\<hyphen> K\<^esup> \<noteq> \<zero>; x^\<^bsup>K nat (i - int n)\<^esup> = x^\<^bsup>K nat i\<^esup> \<cdot>\<^sub>r x\<^bsup>\<hyphen> K\<^esup>^\<^bsup>K n\<^esup>; int n + 1 \<le> i; nat (i - int n - 1) = nat (i - int n) - Suc 0; Idomain K; x^\<^bsup>K nat i\<^esup> \<in> carrier K; x\<^bsup>\<hyphen> K\<^esup>^\<^bsup>K nat i\<^esup> \<in> carrier K; x\<^bsup>\<hyphen> K\<^esup>^\<^bsup>K n\<^esup> \<in> carrier K\<rbrakk> \<Longrightarrow> x^\<^bsup>K nat (i + (- int n - 1))\<^esup> \<cdot>\<^sub>r x = x^\<^bsup>K nat i\<^esup> \<cdot>\<^sub>r (x\<^bsup>\<hyphen> K\<^esup>^\<^bsup>K n\<^esup> \<cdot>\<^sub>r x\<^bsup>\<hyphen> K\<^esup>) \<cdot>\<^sub>r x
 6. \<lbrakk>x \<in> carrier K; x \<noteq> \<zero>; 0 \<le> i; Ring K\<rbrakk> \<Longrightarrow> x \<in> carrier K - {\<zero>}
[PROOF STEP]
apply (simp add:Ring.npClose, rule Ring.ring_tOp_closed, assumption+,
        rule Ring.ring_tOp_closed, assumption+)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>n. \<lbrakk>x \<in> carrier K; x \<noteq> \<zero>; Ring K; x\<^bsup>\<hyphen> K\<^esup> \<in> carrier K; x\<^bsup>\<hyphen> K\<^esup> \<noteq> \<zero>; x^\<^bsup>K nat (i - int n)\<^esup> = x^\<^bsup>K nat i\<^esup> \<cdot>\<^sub>r x\<^bsup>\<hyphen> K\<^esup>^\<^bsup>K n\<^esup>; int n + 1 \<le> i; nat (i - int n - 1) = nat (i - int n) - Suc 0; Idomain K; x^\<^bsup>K nat i\<^esup> \<in> carrier K; x\<^bsup>\<hyphen> K\<^esup>^\<^bsup>K nat i\<^esup> \<in> carrier K; x\<^bsup>\<hyphen> K\<^esup>^\<^bsup>K n\<^esup> \<in> carrier K\<rbrakk> \<Longrightarrow> x^\<^bsup>K nat (i + (- int n - 1))\<^esup> \<cdot>\<^sub>r x = x^\<^bsup>K nat i\<^esup> \<cdot>\<^sub>r (x\<^bsup>\<hyphen> K\<^esup>^\<^bsup>K n\<^esup> \<cdot>\<^sub>r x\<^bsup>\<hyphen> K\<^esup>) \<cdot>\<^sub>r x
 2. \<lbrakk>x \<in> carrier K; x \<noteq> \<zero>; 0 \<le> i; Ring K\<rbrakk> \<Longrightarrow> x \<in> carrier K - {\<zero>}
[PROOF STEP]
apply (subgoal_tac "0 < nat (i - int n)")
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>n. \<lbrakk>x \<in> carrier K; x \<noteq> \<zero>; Ring K; x\<^bsup>\<hyphen> K\<^esup> \<in> carrier K; x\<^bsup>\<hyphen> K\<^esup> \<noteq> \<zero>; x^\<^bsup>K nat (i - int n)\<^esup> = x^\<^bsup>K nat i\<^esup> \<cdot>\<^sub>r x\<^bsup>\<hyphen> K\<^esup>^\<^bsup>K n\<^esup>; int n + 1 \<le> i; nat (i - int n - 1) = nat (i - int n) - Suc 0; Idomain K; x^\<^bsup>K nat i\<^esup> \<in> carrier K; x\<^bsup>\<hyphen> K\<^esup>^\<^bsup>K nat i\<^esup> \<in> carrier K; x\<^bsup>\<hyphen> K\<^esup>^\<^bsup>K n\<^esup> \<in> carrier K; 0 < nat (i - int n)\<rbrakk> \<Longrightarrow> x^\<^bsup>K nat (i + (- int n - 1))\<^esup> \<cdot>\<^sub>r x = x^\<^bsup>K nat i\<^esup> \<cdot>\<^sub>r (x\<^bsup>\<hyphen> K\<^esup>^\<^bsup>K n\<^esup> \<cdot>\<^sub>r x\<^bsup>\<hyphen> K\<^esup>) \<cdot>\<^sub>r x
 2. \<And>n. \<lbrakk>x \<in> carrier K; x \<noteq> \<zero>; Ring K; x\<^bsup>\<hyphen> K\<^esup> \<in> carrier K; x\<^bsup>\<hyphen> K\<^esup> \<noteq> \<zero>; x^\<^bsup>K nat (i - int n)\<^esup> = x^\<^bsup>K nat i\<^esup> \<cdot>\<^sub>r x\<^bsup>\<hyphen> K\<^esup>^\<^bsup>K n\<^esup>; int n + 1 \<le> i; nat (i - int n - 1) = nat (i - int n) - Suc 0; Idomain K; x^\<^bsup>K nat i\<^esup> \<in> carrier K; x\<^bsup>\<hyphen> K\<^esup>^\<^bsup>K nat i\<^esup> \<in> carrier K; x\<^bsup>\<hyphen> K\<^esup>^\<^bsup>K n\<^esup> \<in> carrier K\<rbrakk> \<Longrightarrow> 0 < nat (i - int n)
 3. \<lbrakk>x \<in> carrier K; x \<noteq> \<zero>; 0 \<le> i; Ring K\<rbrakk> \<Longrightarrow> x \<in> carrier K - {\<zero>}
[PROOF STEP]
apply (subst Ring.npMulElmR, assumption+, simp,
        simp add:field_tOp_assoc[THEN sym, of "x^\<^bsup>K (nat i)\<^esup>" _ "x\<^bsup>\<hyphen> K\<^esup>"])
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>n. \<lbrakk>x \<in> carrier K; x \<noteq> \<zero>; Ring K; x\<^bsup>\<hyphen> K\<^esup> \<in> carrier K; x\<^bsup>\<hyphen> K\<^esup> \<noteq> \<zero>; x^\<^bsup>K nat (i - int n)\<^esup> = x^\<^bsup>K nat i\<^esup> \<cdot>\<^sub>r x\<^bsup>\<hyphen> K\<^esup>^\<^bsup>K n\<^esup>; int n + 1 \<le> i; nat (i - int n - 1) = nat (i - int n) - Suc 0; Idomain K; x^\<^bsup>K nat i\<^esup> \<in> carrier K; x\<^bsup>\<hyphen> K\<^esup>^\<^bsup>K nat i\<^esup> \<in> carrier K; x\<^bsup>\<hyphen> K\<^esup>^\<^bsup>K n\<^esup> \<in> carrier K\<rbrakk> \<Longrightarrow> x^\<^bsup>K nat (i + (- int n - 1))\<^esup> \<cdot>\<^sub>r x = x^\<^bsup>K nat i\<^esup> \<cdot>\<^sub>r x\<^bsup>\<hyphen> K\<^esup>^\<^bsup>K n\<^esup> \<cdot>\<^sub>r x\<^bsup>\<hyphen> K\<^esup> \<cdot>\<^sub>r x
 2. \<And>n. \<lbrakk>x \<in> carrier K; x \<noteq> \<zero>; Ring K; x\<^bsup>\<hyphen> K\<^esup> \<in> carrier K; x\<^bsup>\<hyphen> K\<^esup> \<noteq> \<zero>; x^\<^bsup>K nat (i - int n)\<^esup> = x^\<^bsup>K nat i\<^esup> \<cdot>\<^sub>r x\<^bsup>\<hyphen> K\<^esup>^\<^bsup>K n\<^esup>; int n + 1 \<le> i; nat (i - int n - 1) = nat (i - int n) - Suc 0; Idomain K; x^\<^bsup>K nat i\<^esup> \<in> carrier K; x\<^bsup>\<hyphen> K\<^esup>^\<^bsup>K nat i\<^esup> \<in> carrier K; x\<^bsup>\<hyphen> K\<^esup>^\<^bsup>K n\<^esup> \<in> carrier K\<rbrakk> \<Longrightarrow> 0 < nat (i - int n)
 3. \<lbrakk>x \<in> carrier K; x \<noteq> \<zero>; 0 \<le> i; Ring K\<rbrakk> \<Longrightarrow> x \<in> carrier K - {\<zero>}
[PROOF STEP]
apply (subst field_tOp_assoc[of _ _ x])
[PROOF STATE]
proof (prove)
goal (6 subgoals):
 1. \<And>n. \<lbrakk>x \<in> carrier K; x \<noteq> \<zero>; Ring K; x\<^bsup>\<hyphen> K\<^esup> \<in> carrier K; x\<^bsup>\<hyphen> K\<^esup> \<noteq> \<zero>; x^\<^bsup>K nat (i - int n)\<^esup> = x^\<^bsup>K nat i\<^esup> \<cdot>\<^sub>r x\<^bsup>\<hyphen> K\<^esup>^\<^bsup>K n\<^esup>; int n + 1 \<le> i; nat (i - int n - 1) = nat (i - int n) - Suc 0; Idomain K; x^\<^bsup>K nat i\<^esup> \<in> carrier K; x\<^bsup>\<hyphen> K\<^esup>^\<^bsup>K nat i\<^esup> \<in> carrier K; x\<^bsup>\<hyphen> K\<^esup>^\<^bsup>K n\<^esup> \<in> carrier K\<rbrakk> \<Longrightarrow> x^\<^bsup>K nat i\<^esup> \<cdot>\<^sub>r x\<^bsup>\<hyphen> K\<^esup>^\<^bsup>K n\<^esup> \<in> carrier K
 2. \<And>n. \<lbrakk>x \<in> carrier K; x \<noteq> \<zero>; Ring K; x\<^bsup>\<hyphen> K\<^esup> \<in> carrier K; x\<^bsup>\<hyphen> K\<^esup> \<noteq> \<zero>; x^\<^bsup>K nat (i - int n)\<^esup> = x^\<^bsup>K nat i\<^esup> \<cdot>\<^sub>r x\<^bsup>\<hyphen> K\<^esup>^\<^bsup>K n\<^esup>; int n + 1 \<le> i; nat (i - int n - 1) = nat (i - int n) - Suc 0; Idomain K; x^\<^bsup>K nat i\<^esup> \<in> carrier K; x\<^bsup>\<hyphen> K\<^esup>^\<^bsup>K nat i\<^esup> \<in> carrier K; x\<^bsup>\<hyphen> K\<^esup>^\<^bsup>K n\<^esup> \<in> carrier K\<rbrakk> \<Longrightarrow> x\<^bsup>\<hyphen> K\<^esup> \<in> carrier K
 3. \<And>n. \<lbrakk>x \<in> carrier K; x \<noteq> \<zero>; Ring K; x\<^bsup>\<hyphen> K\<^esup> \<in> carrier K; x\<^bsup>\<hyphen> K\<^esup> \<noteq> \<zero>; x^\<^bsup>K nat (i - int n)\<^esup> = x^\<^bsup>K nat i\<^esup> \<cdot>\<^sub>r x\<^bsup>\<hyphen> K\<^esup>^\<^bsup>K n\<^esup>; int n + 1 \<le> i; nat (i - int n - 1) = nat (i - int n) - Suc 0; Idomain K; x^\<^bsup>K nat i\<^esup> \<in> carrier K; x\<^bsup>\<hyphen> K\<^esup>^\<^bsup>K nat i\<^esup> \<in> carrier K; x\<^bsup>\<hyphen> K\<^esup>^\<^bsup>K n\<^esup> \<in> carrier K\<rbrakk> \<Longrightarrow> x \<in> carrier K
 4. \<And>n. \<lbrakk>x \<in> carrier K; x \<noteq> \<zero>; Ring K; x\<^bsup>\<hyphen> K\<^esup> \<in> carrier K; x\<^bsup>\<hyphen> K\<^esup> \<noteq> \<zero>; x^\<^bsup>K nat (i - int n)\<^esup> = x^\<^bsup>K nat i\<^esup> \<cdot>\<^sub>r x\<^bsup>\<hyphen> K\<^esup>^\<^bsup>K n\<^esup>; int n + 1 \<le> i; nat (i - int n - 1) = nat (i - int n) - Suc 0; Idomain K; x^\<^bsup>K nat i\<^esup> \<in> carrier K; x\<^bsup>\<hyphen> K\<^esup>^\<^bsup>K nat i\<^esup> \<in> carrier K; x\<^bsup>\<hyphen> K\<^esup>^\<^bsup>K n\<^esup> \<in> carrier K\<rbrakk> \<Longrightarrow> x^\<^bsup>K nat (i + (- int n - 1))\<^esup> \<cdot>\<^sub>r x = x^\<^bsup>K nat i\<^esup> \<cdot>\<^sub>r x\<^bsup>\<hyphen> K\<^esup>^\<^bsup>K n\<^esup> \<cdot>\<^sub>r (x\<^bsup>\<hyphen> K\<^esup> \<cdot>\<^sub>r x)
 5. \<And>n. \<lbrakk>x \<in> carrier K; x \<noteq> \<zero>; Ring K; x\<^bsup>\<hyphen> K\<^esup> \<in> carrier K; x\<^bsup>\<hyphen> K\<^esup> \<noteq> \<zero>; x^\<^bsup>K nat (i - int n)\<^esup> = x^\<^bsup>K nat i\<^esup> \<cdot>\<^sub>r x\<^bsup>\<hyphen> K\<^esup>^\<^bsup>K n\<^esup>; int n + 1 \<le> i; nat (i - int n - 1) = nat (i - int n) - Suc 0; Idomain K; x^\<^bsup>K nat i\<^esup> \<in> carrier K; x\<^bsup>\<hyphen> K\<^esup>^\<^bsup>K nat i\<^esup> \<in> carrier K; x\<^bsup>\<hyphen> K\<^esup>^\<^bsup>K n\<^esup> \<in> carrier K\<rbrakk> \<Longrightarrow> 0 < nat (i - int n)
 6. \<lbrakk>x \<in> carrier K; x \<noteq> \<zero>; 0 \<le> i; Ring K\<rbrakk> \<Longrightarrow> x \<in> carrier K - {\<zero>}
[PROOF STEP]
apply (rule Ring.ring_tOp_closed[of K], assumption+)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>n. \<lbrakk>x \<in> carrier K; x \<noteq> \<zero>; Ring K; x\<^bsup>\<hyphen> K\<^esup> \<in> carrier K; x\<^bsup>\<hyphen> K\<^esup> \<noteq> \<zero>; x^\<^bsup>K nat (i - int n)\<^esup> = x^\<^bsup>K nat i\<^esup> \<cdot>\<^sub>r x\<^bsup>\<hyphen> K\<^esup>^\<^bsup>K n\<^esup>; int n + 1 \<le> i; nat (i - int n - 1) = nat (i - int n) - Suc 0; Idomain K; x^\<^bsup>K nat i\<^esup> \<in> carrier K; x\<^bsup>\<hyphen> K\<^esup>^\<^bsup>K nat i\<^esup> \<in> carrier K; x\<^bsup>\<hyphen> K\<^esup>^\<^bsup>K n\<^esup> \<in> carrier K\<rbrakk> \<Longrightarrow> x^\<^bsup>K nat (i + (- int n - 1))\<^esup> \<cdot>\<^sub>r x = x^\<^bsup>K nat i\<^esup> \<cdot>\<^sub>r x\<^bsup>\<hyphen> K\<^esup>^\<^bsup>K n\<^esup> \<cdot>\<^sub>r (x\<^bsup>\<hyphen> K\<^esup> \<cdot>\<^sub>r x)
 2. \<And>n. \<lbrakk>x \<in> carrier K; x \<noteq> \<zero>; Ring K; x\<^bsup>\<hyphen> K\<^esup> \<in> carrier K; x\<^bsup>\<hyphen> K\<^esup> \<noteq> \<zero>; x^\<^bsup>K nat (i - int n)\<^esup> = x^\<^bsup>K nat i\<^esup> \<cdot>\<^sub>r x\<^bsup>\<hyphen> K\<^esup>^\<^bsup>K n\<^esup>; int n + 1 \<le> i; nat (i - int n - 1) = nat (i - int n) - Suc 0; Idomain K; x^\<^bsup>K nat i\<^esup> \<in> carrier K; x\<^bsup>\<hyphen> K\<^esup>^\<^bsup>K nat i\<^esup> \<in> carrier K; x\<^bsup>\<hyphen> K\<^esup>^\<^bsup>K n\<^esup> \<in> carrier K\<rbrakk> \<Longrightarrow> 0 < nat (i - int n)
 3. \<lbrakk>x \<in> carrier K; x \<noteq> \<zero>; 0 \<le> i; Ring K\<rbrakk> \<Longrightarrow> x \<in> carrier K - {\<zero>}
[PROOF STEP]
apply (simp add: linvf)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>n. \<lbrakk>x \<in> carrier K; x \<noteq> \<zero>; Ring K; x\<^bsup>\<hyphen> K\<^esup> \<in> carrier K; x\<^bsup>\<hyphen> K\<^esup> \<noteq> \<zero>; x^\<^bsup>K nat (i - int n)\<^esup> = x^\<^bsup>K nat i\<^esup> \<cdot>\<^sub>r x\<^bsup>\<hyphen> K\<^esup>^\<^bsup>K n\<^esup>; int n + 1 \<le> i; nat (i - int n - 1) = nat (i - int n) - Suc 0; Idomain K; x^\<^bsup>K nat i\<^esup> \<in> carrier K; x\<^bsup>\<hyphen> K\<^esup>^\<^bsup>K nat i\<^esup> \<in> carrier K; x\<^bsup>\<hyphen> K\<^esup>^\<^bsup>K n\<^esup> \<in> carrier K\<rbrakk> \<Longrightarrow> x^\<^bsup>K nat (i + (- int n - 1))\<^esup> \<cdot>\<^sub>r x = x^\<^bsup>K nat i\<^esup> \<cdot>\<^sub>r x\<^bsup>\<hyphen> K\<^esup>^\<^bsup>K n\<^esup> \<cdot>\<^sub>r 1\<^sub>r
 2. \<And>n. \<lbrakk>x \<in> carrier K; x \<noteq> \<zero>; Ring K; x\<^bsup>\<hyphen> K\<^esup> \<in> carrier K; x\<^bsup>\<hyphen> K\<^esup> \<noteq> \<zero>; x^\<^bsup>K nat (i - int n)\<^esup> = x^\<^bsup>K nat i\<^esup> \<cdot>\<^sub>r x\<^bsup>\<hyphen> K\<^esup>^\<^bsup>K n\<^esup>; int n + 1 \<le> i; nat (i - int n - 1) = nat (i - int n) - Suc 0; Idomain K; x^\<^bsup>K nat i\<^esup> \<in> carrier K; x\<^bsup>\<hyphen> K\<^esup>^\<^bsup>K nat i\<^esup> \<in> carrier K; x\<^bsup>\<hyphen> K\<^esup>^\<^bsup>K n\<^esup> \<in> carrier K\<rbrakk> \<Longrightarrow> 0 < nat (i - int n)
 3. \<lbrakk>x \<in> carrier K; x \<noteq> \<zero>; 0 \<le> i; Ring K\<rbrakk> \<Longrightarrow> x \<in> carrier K - {\<zero>}
[PROOF STEP]
apply (subst Ring.ring_r_one[of K], assumption)
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<And>n. \<lbrakk>x \<in> carrier K; x \<noteq> \<zero>; Ring K; x\<^bsup>\<hyphen> K\<^esup> \<in> carrier K; x\<^bsup>\<hyphen> K\<^esup> \<noteq> \<zero>; x^\<^bsup>K nat (i - int n)\<^esup> = x^\<^bsup>K nat i\<^esup> \<cdot>\<^sub>r x\<^bsup>\<hyphen> K\<^esup>^\<^bsup>K n\<^esup>; int n + 1 \<le> i; nat (i - int n - 1) = nat (i - int n) - Suc 0; Idomain K; x^\<^bsup>K nat i\<^esup> \<in> carrier K; x\<^bsup>\<hyphen> K\<^esup>^\<^bsup>K nat i\<^esup> \<in> carrier K; x\<^bsup>\<hyphen> K\<^esup>^\<^bsup>K n\<^esup> \<in> carrier K\<rbrakk> \<Longrightarrow> x^\<^bsup>K nat i\<^esup> \<cdot>\<^sub>r x\<^bsup>\<hyphen> K\<^esup>^\<^bsup>K n\<^esup> \<in> carrier K
 2. \<And>n. \<lbrakk>x \<in> carrier K; x \<noteq> \<zero>; Ring K; x\<^bsup>\<hyphen> K\<^esup> \<in> carrier K; x\<^bsup>\<hyphen> K\<^esup> \<noteq> \<zero>; x^\<^bsup>K nat (i - int n)\<^esup> = x^\<^bsup>K nat i\<^esup> \<cdot>\<^sub>r x\<^bsup>\<hyphen> K\<^esup>^\<^bsup>K n\<^esup>; int n + 1 \<le> i; nat (i - int n - 1) = nat (i - int n) - Suc 0; Idomain K; x^\<^bsup>K nat i\<^esup> \<in> carrier K; x\<^bsup>\<hyphen> K\<^esup>^\<^bsup>K nat i\<^esup> \<in> carrier K; x\<^bsup>\<hyphen> K\<^esup>^\<^bsup>K n\<^esup> \<in> carrier K\<rbrakk> \<Longrightarrow> x^\<^bsup>K nat (i + (- int n - 1))\<^esup> \<cdot>\<^sub>r x = x^\<^bsup>K nat i\<^esup> \<cdot>\<^sub>r x\<^bsup>\<hyphen> K\<^esup>^\<^bsup>K n\<^esup>
 3. \<And>n. \<lbrakk>x \<in> carrier K; x \<noteq> \<zero>; Ring K; x\<^bsup>\<hyphen> K\<^esup> \<in> carrier K; x\<^bsup>\<hyphen> K\<^esup> \<noteq> \<zero>; x^\<^bsup>K nat (i - int n)\<^esup> = x^\<^bsup>K nat i\<^esup> \<cdot>\<^sub>r x\<^bsup>\<hyphen> K\<^esup>^\<^bsup>K n\<^esup>; int n + 1 \<le> i; nat (i - int n - 1) = nat (i - int n) - Suc 0; Idomain K; x^\<^bsup>K nat i\<^esup> \<in> carrier K; x\<^bsup>\<hyphen> K\<^esup>^\<^bsup>K nat i\<^esup> \<in> carrier K; x\<^bsup>\<hyphen> K\<^esup>^\<^bsup>K n\<^esup> \<in> carrier K\<rbrakk> \<Longrightarrow> 0 < nat (i - int n)
 4. \<lbrakk>x \<in> carrier K; x \<noteq> \<zero>; 0 \<le> i; Ring K\<rbrakk> \<Longrightarrow> x \<in> carrier K - {\<zero>}
[PROOF STEP]
apply auto
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>n. \<lbrakk>x \<in> carrier K; x \<noteq> \<zero>; Ring K; x\<^bsup>\<hyphen> K\<^esup> \<in> carrier K; x\<^bsup>\<hyphen> K\<^esup> \<noteq> \<zero>; x^\<^bsup>K nat (i - int n)\<^esup> = x^\<^bsup>K nat i\<^esup> \<cdot>\<^sub>r x\<^bsup>\<hyphen> K\<^esup>^\<^bsup>K n\<^esup>; int n + 1 \<le> i; nat (i - int n - 1) = nat (i - int n) - Suc 0; Idomain K; x^\<^bsup>K nat i\<^esup> \<in> carrier K; x\<^bsup>\<hyphen> K\<^esup>^\<^bsup>K nat i\<^esup> \<in> carrier K; x\<^bsup>\<hyphen> K\<^esup>^\<^bsup>K n\<^esup> \<in> carrier K\<rbrakk> \<Longrightarrow> x^\<^bsup>K nat i\<^esup> \<cdot>\<^sub>r x\<^bsup>\<hyphen> K\<^esup>^\<^bsup>K n\<^esup> \<in> carrier K
 2. \<And>n. \<lbrakk>x \<in> carrier K; x \<noteq> \<zero>; Ring K; x\<^bsup>\<hyphen> K\<^esup> \<in> carrier K; x\<^bsup>\<hyphen> K\<^esup> \<noteq> \<zero>; x^\<^bsup>K nat (i - int n)\<^esup> = x^\<^bsup>K nat i\<^esup> \<cdot>\<^sub>r x\<^bsup>\<hyphen> K\<^esup>^\<^bsup>K n\<^esup>; int n + 1 \<le> i; nat (i - int n - 1) = nat (i - int n) - Suc 0; Idomain K; x^\<^bsup>K nat i\<^esup> \<in> carrier K; x\<^bsup>\<hyphen> K\<^esup>^\<^bsup>K nat i\<^esup> \<in> carrier K; x\<^bsup>\<hyphen> K\<^esup>^\<^bsup>K n\<^esup> \<in> carrier K\<rbrakk> \<Longrightarrow> x^\<^bsup>K nat (i + (- int n - 1))\<^esup> \<cdot>\<^sub>r x = x^\<^bsup>K nat i\<^esup> \<cdot>\<^sub>r x\<^bsup>\<hyphen> K\<^esup>^\<^bsup>K n\<^esup>
[PROOF STEP]
apply (metis Ring.npClose)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>n. \<lbrakk>x \<in> carrier K; x \<noteq> \<zero>; Ring K; x\<^bsup>\<hyphen> K\<^esup> \<in> carrier K; x\<^bsup>\<hyphen> K\<^esup> \<noteq> \<zero>; x^\<^bsup>K nat (i - int n)\<^esup> = x^\<^bsup>K nat i\<^esup> \<cdot>\<^sub>r x\<^bsup>\<hyphen> K\<^esup>^\<^bsup>K n\<^esup>; int n + 1 \<le> i; nat (i - int n - 1) = nat (i - int n) - Suc 0; Idomain K; x^\<^bsup>K nat i\<^esup> \<in> carrier K; x\<^bsup>\<hyphen> K\<^esup>^\<^bsup>K nat i\<^esup> \<in> carrier K; x\<^bsup>\<hyphen> K\<^esup>^\<^bsup>K n\<^esup> \<in> carrier K\<rbrakk> \<Longrightarrow> x^\<^bsup>K nat (i + (- int n - 1))\<^esup> \<cdot>\<^sub>r x = x^\<^bsup>K nat i\<^esup> \<cdot>\<^sub>r x\<^bsup>\<hyphen> K\<^esup>^\<^bsup>K n\<^esup>
[PROOF STEP]
apply (simp only: uminus_add_conv_diff [symmetric] add.assoc [symmetric])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>n. \<lbrakk>x \<in> carrier K; x \<noteq> \<zero>; Ring K; x\<^bsup>\<hyphen> K\<^esup> \<in> carrier K; x\<^bsup>\<hyphen> K\<^esup> \<noteq> \<zero>; x^\<^bsup>K nat (- int n + i)\<^esup> = x^\<^bsup>K nat i\<^esup> \<cdot>\<^sub>r x\<^bsup>\<hyphen> K\<^esup>^\<^bsup>K n\<^esup>; int n + 1 \<le> i; nat (- 1 + - int n + i) = nat (- int n + i) - Suc 0; Idomain K; x^\<^bsup>K nat i\<^esup> \<in> carrier K; x\<^bsup>\<hyphen> K\<^esup>^\<^bsup>K nat i\<^esup> \<in> carrier K; x\<^bsup>\<hyphen> K\<^esup>^\<^bsup>K n\<^esup> \<in> carrier K\<rbrakk> \<Longrightarrow> x^\<^bsup>K nat (i + - 1 + - int n)\<^esup> \<cdot>\<^sub>r x = x^\<^bsup>K nat i\<^esup> \<cdot>\<^sub>r x\<^bsup>\<hyphen> K\<^esup>^\<^bsup>K n\<^esup>
[PROOF STEP]
apply (simp add: algebra_simps nat_diff_distrib Suc_diff_Suc)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>n. \<lbrakk>x \<in> carrier K; x \<noteq> \<zero>; Ring K; x\<^bsup>\<hyphen> K\<^esup> \<in> carrier K; x\<^bsup>\<hyphen> K\<^esup> \<noteq> \<zero>; x^\<^bsup>K (nat i - n)\<^esup> = x^\<^bsup>K nat i\<^esup> \<cdot>\<^sub>r x\<^bsup>\<hyphen> K\<^esup>^\<^bsup>K n\<^esup>; 1 + int n \<le> i; nat i - nat (1 + int n) = nat i - Suc n; Idomain K; x^\<^bsup>K nat i\<^esup> \<in> carrier K; x\<^bsup>\<hyphen> K\<^esup>^\<^bsup>K nat i\<^esup> \<in> carrier K; x\<^bsup>\<hyphen> K\<^esup>^\<^bsup>K n\<^esup> \<in> carrier K\<rbrakk> \<Longrightarrow> x^\<^bsup>K (nat i - Suc n)\<^esup> \<cdot>\<^sub>r x = x^\<^bsup>K nat i\<^esup> \<cdot>\<^sub>r x\<^bsup>\<hyphen> K\<^esup>^\<^bsup>K n\<^esup>
[PROOF STEP]
apply (smt Ring.npMulElmR Suc_nat_eq_nat_zadd1 nat_diff_distrib' nat_int of_nat_0_le_iff)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma (in Corps) npow_exp_minusTr2:"\<lbrakk>x \<in> carrier K; x \<noteq> \<zero>; 0 \<le> i; 0 \<le> j;
                 0 \<le> i - j\<rbrakk>  \<Longrightarrow>  x\<^bsub>K\<^esub>\<^bsup>(i - j)\<^esup> = x^\<^bsup>K (nat i)\<^esup> \<cdot>\<^sub>r (x\<^bsup>\<hyphen>K\<^esup>)^\<^bsup>K (nat j)\<^esup>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>x \<in> carrier K; x \<noteq> \<zero>; 0 \<le> i; 0 \<le> j; 0 \<le> i - j\<rbrakk> \<Longrightarrow> x\<^bsub>K\<^esub>\<^bsup>(i - j)\<^esup> = x^\<^bsup>K nat i\<^esup> \<cdot>\<^sub>r x\<^bsup>\<hyphen> K\<^esup>^\<^bsup>K nat j\<^esup>
[PROOF STEP]
apply (frule npow_exp_minusTr1[of "x" "i" "nat j"], assumption+)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>x \<in> carrier K; x \<noteq> \<zero>; 0 \<le> i; 0 \<le> j; 0 \<le> i - j; 0 \<le> i - int (nat j) \<longrightarrow> x\<^bsub>K\<^esub>\<^bsup>(i - int (nat j))\<^esup> = x^\<^bsup>K nat i\<^esup> \<cdot>\<^sub>r x\<^bsup>\<hyphen> K\<^esup>^\<^bsup>K nat j\<^esup>\<rbrakk> \<Longrightarrow> x\<^bsub>K\<^esub>\<^bsup>(i - j)\<^esup> = x^\<^bsup>K nat i\<^esup> \<cdot>\<^sub>r x\<^bsup>\<hyphen> K\<^esup>^\<^bsup>K nat j\<^esup>
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma (in Corps) npowf_inv:"\<lbrakk>x \<in> carrier K; x \<noteq> \<zero>; 0 \<le> j\<rbrakk> \<Longrightarrow> x\<^bsub>K\<^esub>\<^bsup>j\<^esup> = (x\<^bsup>\<hyphen>K\<^esup>)\<^bsub>K\<^esub>\<^bsup>(-j)\<^esup>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>x \<in> carrier K; x \<noteq> \<zero>; 0 \<le> j\<rbrakk> \<Longrightarrow> x\<^bsub>K\<^esub>\<^bsup>j\<^esup> = x\<^bsup>\<hyphen> K\<^esup>\<^bsub>K\<^esub>\<^bsup>- j\<^esup>
[PROOF STEP]
apply (simp add:npowf_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>x \<in> carrier K; x \<noteq> \<zero>; 0 \<le> j\<rbrakk> \<Longrightarrow> j \<noteq> 0 \<longrightarrow> x^\<^bsup>K nat j\<^esup> = x\<^bsup>\<hyphen> K\<^esup>\<^bsup>\<hyphen> K\<^esup>^\<^bsup>K nat j\<^esup>
[PROOF STEP]
apply (rule impI, simp add:zle)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>x \<in> carrier K; x \<noteq> \<zero>; \<not> j < 0; j \<noteq> 0\<rbrakk> \<Longrightarrow> x^\<^bsup>K nat j\<^esup> = x\<^bsup>\<hyphen> K\<^esup>\<^bsup>\<hyphen> K\<^esup>^\<^bsup>K nat j\<^esup>
[PROOF STEP]
apply (simp add:field_inv_inv)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma (in Corps) npowf_inv1:"\<lbrakk>x \<in> carrier K; x \<noteq> \<zero>; \<not> 0 \<le> j\<rbrakk> \<Longrightarrow>
                                      x\<^bsub>K\<^esub>\<^bsup>j\<^esup> = (x\<^bsup>\<hyphen>K\<^esup>)\<^bsub>K\<^esub>\<^bsup>(-j)\<^esup>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>x \<in> carrier K; x \<noteq> \<zero>; \<not> 0 \<le> j\<rbrakk> \<Longrightarrow> x\<^bsub>K\<^esub>\<^bsup>j\<^esup> = x\<^bsup>\<hyphen> K\<^esup>\<^bsub>K\<^esub>\<^bsup>- j\<^esup>
[PROOF STEP]
apply (simp add:npowf_def)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma (in Corps) npowf_inverse:"\<lbrakk>x \<in> carrier K; x \<noteq> \<zero>\<rbrakk> \<Longrightarrow> x\<^bsub>K\<^esub>\<^bsup>j\<^esup> = (x\<^bsup>\<hyphen>K\<^esup>)\<^bsub>K\<^esub>\<^bsup>(-j)\<^esup>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>x \<in> carrier K; x \<noteq> \<zero>\<rbrakk> \<Longrightarrow> x\<^bsub>K\<^esub>\<^bsup>j\<^esup> = x\<^bsup>\<hyphen> K\<^esup>\<^bsub>K\<^esub>\<^bsup>- j\<^esup>
[PROOF STEP]
apply (case_tac "0 \<le> j")
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>x \<in> carrier K; x \<noteq> \<zero>; 0 \<le> j\<rbrakk> \<Longrightarrow> x\<^bsub>K\<^esub>\<^bsup>j\<^esup> = x\<^bsup>\<hyphen> K\<^esup>\<^bsub>K\<^esub>\<^bsup>- j\<^esup>
 2. \<lbrakk>x \<in> carrier K; x \<noteq> \<zero>; \<not> 0 \<le> j\<rbrakk> \<Longrightarrow> x\<^bsub>K\<^esub>\<^bsup>j\<^esup> = x\<^bsup>\<hyphen> K\<^esup>\<^bsub>K\<^esub>\<^bsup>- j\<^esup>
[PROOF STEP]
apply (simp add:npowf_inv, simp add:npowf_inv1)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma (in Corps) npowf_expTr1:"\<lbrakk>x \<in> carrier K; x \<noteq> \<zero>; 0 \<le> i; 0 \<le> j;
                 0 \<le> i - j\<rbrakk> \<Longrightarrow> x\<^bsub>K\<^esub>\<^bsup>(i - j)\<^esup> = x\<^bsub>K\<^esub>\<^bsup>i\<^esup> \<cdot>\<^sub>r x\<^bsub>K\<^esub>\<^bsup>(- j)\<^esup>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>x \<in> carrier K; x \<noteq> \<zero>; 0 \<le> i; 0 \<le> j; 0 \<le> i - j\<rbrakk> \<Longrightarrow> x\<^bsub>K\<^esub>\<^bsup>(i - j)\<^esup> = x\<^bsub>K\<^esub>\<^bsup>i\<^esup> \<cdot>\<^sub>r x\<^bsub>K\<^esub>\<^bsup>- j\<^esup>
[PROOF STEP]
apply (simp add:npow_exp_minusTr2)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>x \<in> carrier K; x \<noteq> \<zero>; 0 \<le> j; j \<le> i\<rbrakk> \<Longrightarrow> x^\<^bsup>K nat i\<^esup> \<cdot>\<^sub>r x\<^bsup>\<hyphen> K\<^esup>^\<^bsup>K nat j\<^esup> = x\<^bsub>K\<^esub>\<^bsup>i\<^esup> \<cdot>\<^sub>r x\<^bsub>K\<^esub>\<^bsup>- j\<^esup>
[PROOF STEP]
apply (simp add:npowf_def)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma (in Corps) npowf_expTr2:"\<lbrakk>x \<in> carrier K; x \<noteq> \<zero>; 0 \<le> i + j\<rbrakk> \<Longrightarrow>
                          x\<^bsub>K\<^esub>\<^bsup>(i + j)\<^esup> = x\<^bsub>K\<^esub>\<^bsup>i\<^esup> \<cdot>\<^sub>r x\<^bsub>K\<^esub>\<^bsup>j\<^esup>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>x \<in> carrier K; x \<noteq> \<zero>; 0 \<le> i + j\<rbrakk> \<Longrightarrow> x\<^bsub>K\<^esub>\<^bsup>(i + j)\<^esup> = x\<^bsub>K\<^esub>\<^bsup>i\<^esup> \<cdot>\<^sub>r x\<^bsub>K\<^esub>\<^bsup>j\<^esup>
[PROOF STEP]
apply (cut_tac field_is_ring)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>x \<in> carrier K; x \<noteq> \<zero>; 0 \<le> i + j; Ring K\<rbrakk> \<Longrightarrow> x\<^bsub>K\<^esub>\<^bsup>(i + j)\<^esup> = x\<^bsub>K\<^esub>\<^bsup>i\<^esup> \<cdot>\<^sub>r x\<^bsub>K\<^esub>\<^bsup>j\<^esup>
[PROOF STEP]
apply (case_tac "0 \<le> i")
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>x \<in> carrier K; x \<noteq> \<zero>; 0 \<le> i + j; Ring K; 0 \<le> i\<rbrakk> \<Longrightarrow> x\<^bsub>K\<^esub>\<^bsup>(i + j)\<^esup> = x\<^bsub>K\<^esub>\<^bsup>i\<^esup> \<cdot>\<^sub>r x\<^bsub>K\<^esub>\<^bsup>j\<^esup>
 2. \<lbrakk>x \<in> carrier K; x \<noteq> \<zero>; 0 \<le> i + j; Ring K; \<not> 0 \<le> i\<rbrakk> \<Longrightarrow> x\<^bsub>K\<^esub>\<^bsup>(i + j)\<^esup> = x\<^bsub>K\<^esub>\<^bsup>i\<^esup> \<cdot>\<^sub>r x\<^bsub>K\<^esub>\<^bsup>j\<^esup>
[PROOF STEP]
apply (case_tac "0 \<le> j")
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<lbrakk>x \<in> carrier K; x \<noteq> \<zero>; 0 \<le> i + j; Ring K; 0 \<le> i; 0 \<le> j\<rbrakk> \<Longrightarrow> x\<^bsub>K\<^esub>\<^bsup>(i + j)\<^esup> = x\<^bsub>K\<^esub>\<^bsup>i\<^esup> \<cdot>\<^sub>r x\<^bsub>K\<^esub>\<^bsup>j\<^esup>
 2. \<lbrakk>x \<in> carrier K; x \<noteq> \<zero>; 0 \<le> i + j; Ring K; 0 \<le> i; \<not> 0 \<le> j\<rbrakk> \<Longrightarrow> x\<^bsub>K\<^esub>\<^bsup>(i + j)\<^esup> = x\<^bsub>K\<^esub>\<^bsup>i\<^esup> \<cdot>\<^sub>r x\<^bsub>K\<^esub>\<^bsup>j\<^esup>
 3. \<lbrakk>x \<in> carrier K; x \<noteq> \<zero>; 0 \<le> i + j; Ring K; \<not> 0 \<le> i\<rbrakk> \<Longrightarrow> x\<^bsub>K\<^esub>\<^bsup>(i + j)\<^esup> = x\<^bsub>K\<^esub>\<^bsup>i\<^esup> \<cdot>\<^sub>r x\<^bsub>K\<^esub>\<^bsup>j\<^esup>
[PROOF STEP]
apply (simp add:npowf_def, simp add:nat_add_distrib,
         rule Ring.npMulDistr[THEN sym], assumption+)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>x \<in> carrier K; x \<noteq> \<zero>; 0 \<le> i + j; Ring K; 0 \<le> i; \<not> 0 \<le> j\<rbrakk> \<Longrightarrow> x\<^bsub>K\<^esub>\<^bsup>(i + j)\<^esup> = x\<^bsub>K\<^esub>\<^bsup>i\<^esup> \<cdot>\<^sub>r x\<^bsub>K\<^esub>\<^bsup>j\<^esup>
 2. \<lbrakk>x \<in> carrier K; x \<noteq> \<zero>; 0 \<le> i + j; Ring K; \<not> 0 \<le> i\<rbrakk> \<Longrightarrow> x\<^bsub>K\<^esub>\<^bsup>(i + j)\<^esup> = x\<^bsub>K\<^esub>\<^bsup>i\<^esup> \<cdot>\<^sub>r x\<^bsub>K\<^esub>\<^bsup>j\<^esup>
[PROOF STEP]
apply (subst zminus_minus[THEN sym, of "i" "j"],
        subst npow_exp_minusTr2[of "x" "i" "-j"], assumption+)
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<lbrakk>x \<in> carrier K; x \<noteq> \<zero>; 0 \<le> i + j; Ring K; 0 \<le> i; \<not> 0 \<le> j\<rbrakk> \<Longrightarrow> 0 \<le> - j
 2. \<lbrakk>x \<in> carrier K; x \<noteq> \<zero>; 0 \<le> i + j; Ring K; 0 \<le> i; \<not> 0 \<le> j\<rbrakk> \<Longrightarrow> 0 \<le> i - - j
 3. \<lbrakk>x \<in> carrier K; x \<noteq> \<zero>; 0 \<le> i + j; Ring K; 0 \<le> i; \<not> 0 \<le> j\<rbrakk> \<Longrightarrow> x^\<^bsup>K nat i\<^esup> \<cdot>\<^sub>r x\<^bsup>\<hyphen> K\<^esup>^\<^bsup>K nat (- j)\<^esup> = x\<^bsub>K\<^esub>\<^bsup>i\<^esup> \<cdot>\<^sub>r x\<^bsub>K\<^esub>\<^bsup>j\<^esup>
 4. \<lbrakk>x \<in> carrier K; x \<noteq> \<zero>; 0 \<le> i + j; Ring K; \<not> 0 \<le> i\<rbrakk> \<Longrightarrow> x\<^bsub>K\<^esub>\<^bsup>(i + j)\<^esup> = x\<^bsub>K\<^esub>\<^bsup>i\<^esup> \<cdot>\<^sub>r x\<^bsub>K\<^esub>\<^bsup>j\<^esup>
[PROOF STEP]
apply (simp add:zle, simp add:zless_imp_zle, simp add:npowf_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>x \<in> carrier K; x \<noteq> \<zero>; 0 \<le> i + j; Ring K; \<not> 0 \<le> i\<rbrakk> \<Longrightarrow> x\<^bsub>K\<^esub>\<^bsup>(i + j)\<^esup> = x\<^bsub>K\<^esub>\<^bsup>i\<^esup> \<cdot>\<^sub>r x\<^bsub>K\<^esub>\<^bsup>j\<^esup>
[PROOF STEP]
apply (simp add:add.commute[of "i" "j"],
        subst zminus_minus[THEN sym, of "j" "i"],
        subst npow_exp_minusTr2[of "x" "j" "-i"], assumption+)
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<lbrakk>x \<in> carrier K; x \<noteq> \<zero>; 0 \<le> j + i; Ring K; \<not> 0 \<le> i\<rbrakk> \<Longrightarrow> 0 \<le> j
 2. \<lbrakk>x \<in> carrier K; x \<noteq> \<zero>; 0 \<le> j + i; Ring K; \<not> 0 \<le> i\<rbrakk> \<Longrightarrow> 0 \<le> - i
 3. \<lbrakk>x \<in> carrier K; x \<noteq> \<zero>; 0 \<le> j + i; Ring K; \<not> 0 \<le> i\<rbrakk> \<Longrightarrow> 0 \<le> j - - i
 4. \<lbrakk>x \<in> carrier K; x \<noteq> \<zero>; 0 \<le> j + i; Ring K; \<not> 0 \<le> i\<rbrakk> \<Longrightarrow> x^\<^bsup>K nat j\<^esup> \<cdot>\<^sub>r x\<^bsup>\<hyphen> K\<^esup>^\<^bsup>K nat (- i)\<^esup> = x\<^bsub>K\<^esub>\<^bsup>i\<^esup> \<cdot>\<^sub>r x\<^bsub>K\<^esub>\<^bsup>j\<^esup>
[PROOF STEP]
apply (simp add:zle, simp add:zless_imp_zle, simp)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>x \<in> carrier K; x \<noteq> \<zero>; 0 \<le> j + i; Ring K; \<not> 0 \<le> i\<rbrakk> \<Longrightarrow> x^\<^bsup>K nat j\<^esup> \<cdot>\<^sub>r x\<^bsup>\<hyphen> K\<^esup>^\<^bsup>K nat (- i)\<^esup> = x\<^bsub>K\<^esub>\<^bsup>i\<^esup> \<cdot>\<^sub>r x\<^bsub>K\<^esub>\<^bsup>j\<^esup>
[PROOF STEP]
apply (frule npowf_mem[of "x" "i"], assumption+,
         frule npowf_mem[of "x" "j"], assumption+,
         simp add:field_tOp_commute[of "x\<^bsub>K\<^esub>\<^bsup>i\<^esup>" "x\<^bsub>K\<^esub>\<^bsup>j\<^esup>"])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>x \<in> carrier K; x \<noteq> \<zero>; 0 \<le> j + i; Ring K; \<not> 0 \<le> i; x\<^bsub>K\<^esub>\<^bsup>i\<^esup> \<in> carrier K; x\<^bsub>K\<^esub>\<^bsup>j\<^esup> \<in> carrier K\<rbrakk> \<Longrightarrow> x^\<^bsup>K nat j\<^esup> \<cdot>\<^sub>r x\<^bsup>\<hyphen> K\<^esup>^\<^bsup>K nat (- i)\<^esup> = x\<^bsub>K\<^esub>\<^bsup>j\<^esup> \<cdot>\<^sub>r x\<^bsub>K\<^esub>\<^bsup>i\<^esup>
[PROOF STEP]
apply (simp add:npowf_def)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma (in Corps) npowf_exp_add:"\<lbrakk>x \<in> carrier K; x \<noteq> \<zero>\<rbrakk> \<Longrightarrow>
                          x\<^bsub>K\<^esub>\<^bsup>(i + j)\<^esup> = x\<^bsub>K\<^esub>\<^bsup>i\<^esup> \<cdot>\<^sub>r x\<^bsub>K\<^esub>\<^bsup>j\<^esup>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>x \<in> carrier K; x \<noteq> \<zero>\<rbrakk> \<Longrightarrow> x\<^bsub>K\<^esub>\<^bsup>(i + j)\<^esup> = x\<^bsub>K\<^esub>\<^bsup>i\<^esup> \<cdot>\<^sub>r x\<^bsub>K\<^esub>\<^bsup>j\<^esup>
[PROOF STEP]
apply (case_tac "0 \<le> i + j")
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>x \<in> carrier K; x \<noteq> \<zero>; 0 \<le> i + j\<rbrakk> \<Longrightarrow> x\<^bsub>K\<^esub>\<^bsup>(i + j)\<^esup> = x\<^bsub>K\<^esub>\<^bsup>i\<^esup> \<cdot>\<^sub>r x\<^bsub>K\<^esub>\<^bsup>j\<^esup>
 2. \<lbrakk>x \<in> carrier K; x \<noteq> \<zero>; \<not> 0 \<le> i + j\<rbrakk> \<Longrightarrow> x\<^bsub>K\<^esub>\<^bsup>(i + j)\<^esup> = x\<^bsub>K\<^esub>\<^bsup>i\<^esup> \<cdot>\<^sub>r x\<^bsub>K\<^esub>\<^bsup>j\<^esup>
[PROOF STEP]
apply (simp add:npowf_expTr2)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>x \<in> carrier K; x \<noteq> \<zero>; \<not> 0 \<le> i + j\<rbrakk> \<Longrightarrow> x\<^bsub>K\<^esub>\<^bsup>(i + j)\<^esup> = x\<^bsub>K\<^esub>\<^bsup>i\<^esup> \<cdot>\<^sub>r x\<^bsub>K\<^esub>\<^bsup>j\<^esup>
[PROOF STEP]
apply (simp add:npowf_inv1[of "x" "i + j"])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>x \<in> carrier K; x \<noteq> \<zero>; \<not> 0 \<le> i + j\<rbrakk> \<Longrightarrow> x\<^bsup>\<hyphen> K\<^esup>\<^bsub>K\<^esub>\<^bsup>(- i - j)\<^esup> = x\<^bsub>K\<^esub>\<^bsup>i\<^esup> \<cdot>\<^sub>r x\<^bsub>K\<^esub>\<^bsup>j\<^esup>
[PROOF STEP]
apply (simp add:zle)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>x \<in> carrier K; x \<noteq> \<zero>; i + j < 0\<rbrakk> \<Longrightarrow> x\<^bsup>\<hyphen> K\<^esup>\<^bsub>K\<^esub>\<^bsup>(- i - j)\<^esup> = x\<^bsub>K\<^esub>\<^bsup>i\<^esup> \<cdot>\<^sub>r x\<^bsub>K\<^esub>\<^bsup>j\<^esup>
[PROOF STEP]
apply (subgoal_tac "0 < -i + -j")
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>x \<in> carrier K; x \<noteq> \<zero>; i + j < 0; 0 < - i + - j\<rbrakk> \<Longrightarrow> x\<^bsup>\<hyphen> K\<^esup>\<^bsub>K\<^esub>\<^bsup>(- i - j)\<^esup> = x\<^bsub>K\<^esub>\<^bsup>i\<^esup> \<cdot>\<^sub>r x\<^bsub>K\<^esub>\<^bsup>j\<^esup>
 2. \<lbrakk>x \<in> carrier K; x \<noteq> \<zero>; i + j < 0\<rbrakk> \<Longrightarrow> 0 < - i + - j
[PROOF STEP]
prefer 2
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>x \<in> carrier K; x \<noteq> \<zero>; i + j < 0\<rbrakk> \<Longrightarrow> 0 < - i + - j
 2. \<lbrakk>x \<in> carrier K; x \<noteq> \<zero>; i + j < 0; 0 < - i + - j\<rbrakk> \<Longrightarrow> x\<^bsup>\<hyphen> K\<^esup>\<^bsub>K\<^esub>\<^bsup>(- i - j)\<^esup> = x\<^bsub>K\<^esub>\<^bsup>i\<^esup> \<cdot>\<^sub>r x\<^bsub>K\<^esub>\<^bsup>j\<^esup>
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>x \<in> carrier K; x \<noteq> \<zero>; i + j < 0; 0 < - i + - j\<rbrakk> \<Longrightarrow> x\<^bsup>\<hyphen> K\<^esup>\<^bsub>K\<^esub>\<^bsup>(- i - j)\<^esup> = x\<^bsub>K\<^esub>\<^bsup>i\<^esup> \<cdot>\<^sub>r x\<^bsub>K\<^esub>\<^bsup>j\<^esup>
[PROOF STEP]
apply (thin_tac "i + j < 0")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>x \<in> carrier K; x \<noteq> \<zero>; 0 < - i + - j\<rbrakk> \<Longrightarrow> x\<^bsup>\<hyphen> K\<^esup>\<^bsub>K\<^esub>\<^bsup>(- i - j)\<^esup> = x\<^bsub>K\<^esub>\<^bsup>i\<^esup> \<cdot>\<^sub>r x\<^bsub>K\<^esub>\<^bsup>j\<^esup>
[PROOF STEP]
apply (frule zless_imp_zle[of "0" "-i + -j"])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>x \<in> carrier K; x \<noteq> \<zero>; 0 < - i + - j; 0 \<le> - i + - j\<rbrakk> \<Longrightarrow> x\<^bsup>\<hyphen> K\<^esup>\<^bsub>K\<^esub>\<^bsup>(- i - j)\<^esup> = x\<^bsub>K\<^esub>\<^bsup>i\<^esup> \<cdot>\<^sub>r x\<^bsub>K\<^esub>\<^bsup>j\<^esup>
[PROOF STEP]
apply (thin_tac "0 < -i + -j")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>x \<in> carrier K; x \<noteq> \<zero>; 0 \<le> - i + - j\<rbrakk> \<Longrightarrow> x\<^bsup>\<hyphen> K\<^esup>\<^bsub>K\<^esub>\<^bsup>(- i - j)\<^esup> = x\<^bsub>K\<^esub>\<^bsup>i\<^esup> \<cdot>\<^sub>r x\<^bsub>K\<^esub>\<^bsup>j\<^esup>
[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>; 0 \<le> - i + - j; x\<^bsup>\<hyphen> K\<^esup> \<in> carrier K - {\<zero>}\<rbrakk> \<Longrightarrow> x\<^bsup>\<hyphen> K\<^esup>\<^bsub>K\<^esub>\<^bsup>(- i - j)\<^esup> = x\<^bsub>K\<^esub>\<^bsup>i\<^esup> \<cdot>\<^sub>r x\<^bsub>K\<^esub>\<^bsup>j\<^esup>
 2. \<lbrakk>x \<in> carrier K; x \<noteq> \<zero>; 0 \<le> - i + - j\<rbrakk> \<Longrightarrow> x \<in> carrier K - {\<zero>}
[PROOF STEP]
apply (simp, erule conjE,
       frule npowf_expTr2[of "x\<^bsup>\<hyphen>K\<^esup>" "-i" "-j"], assumption+)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<lbrakk>x \<in> carrier K; x \<noteq> \<zero>; j \<le> - i; x\<^bsup>\<hyphen> K\<^esup> \<in> carrier K; x\<^bsup>\<hyphen> K\<^esup> \<noteq> \<zero>\<rbrakk> \<Longrightarrow> 0 \<le> - i + - j
 2. \<lbrakk>x \<in> carrier K; x \<noteq> \<zero>; j \<le> - i; x\<^bsup>\<hyphen> K\<^esup> \<in> carrier K; x\<^bsup>\<hyphen> K\<^esup> \<noteq> \<zero>; x\<^bsup>\<hyphen> K\<^esup>\<^bsub>K\<^esub>\<^bsup>(- i + - j)\<^esup> = x\<^bsup>\<hyphen> K\<^esup>\<^bsub>K\<^esub>\<^bsup>- i\<^esup> \<cdot>\<^sub>r x\<^bsup>\<hyphen> K\<^esup>\<^bsub>K\<^esub>\<^bsup>- j\<^esup>\<rbrakk> \<Longrightarrow> x\<^bsup>\<hyphen> K\<^esup>\<^bsub>K\<^esub>\<^bsup>(- i - j)\<^esup> = x\<^bsub>K\<^esub>\<^bsup>i\<^esup> \<cdot>\<^sub>r x\<^bsub>K\<^esub>\<^bsup>j\<^esup>
 3. \<lbrakk>x \<in> carrier K; x \<noteq> \<zero>; 0 \<le> - i + - j\<rbrakk> \<Longrightarrow> x \<in> carrier K - {\<zero>}
[PROOF STEP]
apply (simp add:zdiff[THEN sym])
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>x \<in> carrier K; x \<noteq> \<zero>; j \<le> - i; x\<^bsup>\<hyphen> K\<^esup> \<in> carrier K; x\<^bsup>\<hyphen> K\<^esup> \<noteq> \<zero>; x\<^bsup>\<hyphen> K\<^esup>\<^bsub>K\<^esub>\<^bsup>(- i + - j)\<^esup> = x\<^bsup>\<hyphen> K\<^esup>\<^bsub>K\<^esub>\<^bsup>- i\<^esup> \<cdot>\<^sub>r x\<^bsup>\<hyphen> K\<^esup>\<^bsub>K\<^esub>\<^bsup>- j\<^esup>\<rbrakk> \<Longrightarrow> x\<^bsup>\<hyphen> K\<^esup>\<^bsub>K\<^esub>\<^bsup>(- i - j)\<^esup> = x\<^bsub>K\<^esub>\<^bsup>i\<^esup> \<cdot>\<^sub>r x\<^bsub>K\<^esub>\<^bsup>j\<^esup>
 2. \<lbrakk>x \<in> carrier K; x \<noteq> \<zero>; 0 \<le> - i + - j\<rbrakk> \<Longrightarrow> x \<in> carrier K - {\<zero>}
[PROOF STEP]
apply (simp add:npowf_inverse, simp)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma (in Corps) npowf_exp_1_add:"\<lbrakk>x \<in> carrier K; x \<noteq> \<zero>\<rbrakk> \<Longrightarrow>
                                        x\<^bsub>K\<^esub>\<^bsup>(1 + j)\<^esup> = x \<cdot>\<^sub>r x\<^bsub>K\<^esub>\<^bsup>j\<^esup>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>x \<in> carrier K; x \<noteq> \<zero>\<rbrakk> \<Longrightarrow> x\<^bsub>K\<^esub>\<^bsup>(1 + j)\<^esup> = x \<cdot>\<^sub>r x\<^bsub>K\<^esub>\<^bsup>j\<^esup>
[PROOF STEP]
apply (simp add:npowf_exp_add[of "x" "1" "j"])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>x \<in> carrier K; x \<noteq> \<zero>\<rbrakk> \<Longrightarrow> x\<^bsub>K\<^esub>\<^bsup>1\<^esup> \<cdot>\<^sub>r x\<^bsub>K\<^esub>\<^bsup>j\<^esup> = x \<cdot>\<^sub>r x\<^bsub>K\<^esub>\<^bsup>j\<^esup>
[PROOF STEP]
apply (cut_tac field_is_ring)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>x \<in> carrier K; x \<noteq> \<zero>; Ring K\<rbrakk> \<Longrightarrow> x\<^bsub>K\<^esub>\<^bsup>1\<^esup> \<cdot>\<^sub>r x\<^bsub>K\<^esub>\<^bsup>j\<^esup> = x \<cdot>\<^sub>r x\<^bsub>K\<^esub>\<^bsup>j\<^esup>
[PROOF STEP]
apply (simp add:npowf_def, simp add:Ring.ring_l_one)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


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


[STATEMENT]
lemma (in Ring) residue_fieldTr:"\<lbrakk>maximal_ideal R mx; x \<in> carrier(qring R mx);
 x \<noteq> \<zero>\<^bsub>(qring R mx)\<^esub>\<rbrakk> \<Longrightarrow>\<exists>y\<in>carrier (qring R mx). y \<cdot>\<^sub>r\<^bsub>(qring R mx)\<^esub> x = 1\<^sub>r\<^bsub>(qring R mx)\<^esub>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>maximal_ideal R mx; x \<in> carrier (R /\<^sub>r mx); x \<noteq> \<zero>\<^bsub>R /\<^sub>r mx\<^esub>\<rbrakk> \<Longrightarrow> \<exists>y\<in>carrier (R /\<^sub>r mx). y \<cdot>\<^sub>r\<^bsub>R /\<^sub>r mx\<^esub> x = 1\<^sub>r\<^bsub>R /\<^sub>r mx\<^esub>
[PROOF STEP]
apply (frule maximal_ideal_ideal[of "mx"])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>maximal_ideal R mx; x \<in> carrier (R /\<^sub>r mx); x \<noteq> \<zero>\<^bsub>R /\<^sub>r mx\<^esub>; ideal R mx\<rbrakk> \<Longrightarrow> \<exists>y\<in>carrier (R /\<^sub>r mx). y \<cdot>\<^sub>r\<^bsub>R /\<^sub>r mx\<^esub> x = 1\<^sub>r\<^bsub>R /\<^sub>r mx\<^esub>
[PROOF STEP]
apply (simp add:qring_carrier)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>maximal_ideal R mx; \<exists>a\<in>carrier R. a \<uplus>\<^bsub>R\<^esub> mx = x; x \<noteq> \<zero>\<^bsub>R /\<^sub>r mx\<^esub>; ideal R mx\<rbrakk> \<Longrightarrow> \<exists>y. (\<exists>a\<in>carrier R. a \<uplus>\<^bsub>R\<^esub> mx = y) \<and> y \<cdot>\<^sub>r\<^bsub>R /\<^sub>r mx\<^esub> x = 1\<^sub>r\<^bsub>R /\<^sub>r mx\<^esub>
[PROOF STEP]
apply (simp add:qring_zero)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>maximal_ideal R mx; \<exists>a\<in>carrier R. a \<uplus>\<^bsub>R\<^esub> mx = x; x \<noteq> mx; ideal R mx\<rbrakk> \<Longrightarrow> \<exists>y. (\<exists>a\<in>carrier R. a \<uplus>\<^bsub>R\<^esub> mx = y) \<and> y \<cdot>\<^sub>r\<^bsub>R /\<^sub>r mx\<^esub> x = 1\<^sub>r\<^bsub>R /\<^sub>r mx\<^esub>
[PROOF STEP]
apply (simp add:qring_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>maximal_ideal R mx; \<exists>a\<in>carrier R. a \<uplus>\<^bsub>R\<^esub> mx = x; x \<noteq> mx; ideal R mx\<rbrakk> \<Longrightarrow> \<exists>y. (\<exists>a\<in>carrier R. a \<uplus>\<^bsub>R\<^esub> mx = y) \<and> rcostOp R mx y x = 1\<^sub>r \<uplus>\<^bsub>R\<^esub> mx
[PROOF STEP]
apply (erule bexE)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a. \<lbrakk>maximal_ideal R mx; x \<noteq> mx; ideal R mx; a \<in> carrier R; a \<uplus>\<^bsub>R\<^esub> mx = x\<rbrakk> \<Longrightarrow> \<exists>y. (\<exists>a\<in>carrier R. a \<uplus>\<^bsub>R\<^esub> mx = y) \<and> rcostOp R mx y x = 1\<^sub>r \<uplus>\<^bsub>R\<^esub> mx
[PROOF STEP]
apply (frule sym, thin_tac "a \<uplus>\<^bsub>R\<^esub> mx = x", simp)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a. \<lbrakk>maximal_ideal R mx; a \<uplus>\<^bsub>R\<^esub> mx \<noteq> mx; ideal R mx; a \<in> carrier R; x = a \<uplus>\<^bsub>R\<^esub> mx\<rbrakk> \<Longrightarrow> \<exists>y. (\<exists>a\<in>carrier R. a \<uplus>\<^bsub>R\<^esub> mx = y) \<and> rcostOp R mx y (a \<uplus>\<^bsub>R\<^esub> mx) = 1\<^sub>r \<uplus>\<^bsub>R\<^esub> mx
[PROOF STEP]
apply (frule_tac a = a in ar_coset_same4_1[of "mx"], assumption+)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a. \<lbrakk>maximal_ideal R mx; a \<uplus>\<^bsub>R\<^esub> mx \<noteq> mx; ideal R mx; a \<in> carrier R; x = a \<uplus>\<^bsub>R\<^esub> mx; a \<notin> mx\<rbrakk> \<Longrightarrow> \<exists>y. (\<exists>a\<in>carrier R. a \<uplus>\<^bsub>R\<^esub> mx = y) \<and> rcostOp R mx y (a \<uplus>\<^bsub>R\<^esub> mx) = 1\<^sub>r \<uplus>\<^bsub>R\<^esub> mx
[PROOF STEP]
apply (frule_tac x = a in maximal_prime_Tr0[of "mx"], assumption+)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a. \<lbrakk>maximal_ideal R mx; a \<uplus>\<^bsub>R\<^esub> mx \<noteq> mx; ideal R mx; a \<in> carrier R; x = a \<uplus>\<^bsub>R\<^esub> mx; a \<notin> mx; mx \<minusplus> R \<diamondsuit>\<^sub>p a = carrier R\<rbrakk> \<Longrightarrow> \<exists>y. (\<exists>a\<in>carrier R. a \<uplus>\<^bsub>R\<^esub> mx = y) \<and> rcostOp R mx y (a \<uplus>\<^bsub>R\<^esub> mx) = 1\<^sub>r \<uplus>\<^bsub>R\<^esub> mx
[PROOF STEP]
apply (cut_tac ring_one)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a. \<lbrakk>maximal_ideal R mx; a \<uplus>\<^bsub>R\<^esub> mx \<noteq> mx; ideal R mx; a \<in> carrier R; x = a \<uplus>\<^bsub>R\<^esub> mx; a \<notin> mx; mx \<minusplus> R \<diamondsuit>\<^sub>p a = carrier R; 1\<^sub>r \<in> carrier R\<rbrakk> \<Longrightarrow> \<exists>y. (\<exists>a\<in>carrier R. a \<uplus>\<^bsub>R\<^esub> mx = y) \<and> rcostOp R mx y (a \<uplus>\<^bsub>R\<^esub> mx) = 1\<^sub>r \<uplus>\<^bsub>R\<^esub> mx
[PROOF STEP]
apply (rotate_tac -2, frule sym, thin_tac "mx \<minusplus> R \<diamondsuit>\<^sub>p a = carrier R")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a. \<lbrakk>1\<^sub>r \<in> carrier R; maximal_ideal R mx; a \<uplus>\<^bsub>R\<^esub> mx \<noteq> mx; ideal R mx; a \<in> carrier R; x = a \<uplus>\<^bsub>R\<^esub> mx; a \<notin> mx; carrier R = mx \<minusplus> R \<diamondsuit>\<^sub>p a\<rbrakk> \<Longrightarrow> \<exists>y. (\<exists>a\<in>carrier R. a \<uplus>\<^bsub>R\<^esub> mx = y) \<and> rcostOp R mx y (a \<uplus>\<^bsub>R\<^esub> mx) = 1\<^sub>r \<uplus>\<^bsub>R\<^esub> mx
[PROOF STEP]
apply (frule_tac B = "mx \<minusplus> R \<diamondsuit>\<^sub>p a" in eq_set_inc[of "1\<^sub>r" "carrier R"],
                  assumption+,
        thin_tac "carrier R = mx \<minusplus> R \<diamondsuit>\<^sub>p a")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a. \<lbrakk>1\<^sub>r \<in> carrier R; maximal_ideal R mx; a \<uplus>\<^bsub>R\<^esub> mx \<noteq> mx; ideal R mx; a \<in> carrier R; x = a \<uplus>\<^bsub>R\<^esub> mx; a \<notin> mx; 1\<^sub>r \<in> mx \<minusplus> R \<diamondsuit>\<^sub>p a\<rbrakk> \<Longrightarrow> \<exists>y. (\<exists>a\<in>carrier R. a \<uplus>\<^bsub>R\<^esub> mx = y) \<and> rcostOp R mx y (a \<uplus>\<^bsub>R\<^esub> mx) = 1\<^sub>r \<uplus>\<^bsub>R\<^esub> mx
[PROOF STEP]
apply (frule ideal_subset1[of mx])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a. \<lbrakk>1\<^sub>r \<in> carrier R; maximal_ideal R mx; a \<uplus>\<^bsub>R\<^esub> mx \<noteq> mx; ideal R mx; a \<in> carrier R; x = a \<uplus>\<^bsub>R\<^esub> mx; a \<notin> mx; 1\<^sub>r \<in> mx \<minusplus> R \<diamondsuit>\<^sub>p a; mx \<subseteq> carrier R\<rbrakk> \<Longrightarrow> \<exists>y. (\<exists>a\<in>carrier R. a \<uplus>\<^bsub>R\<^esub> mx = y) \<and> rcostOp R mx y (a \<uplus>\<^bsub>R\<^esub> mx) = 1\<^sub>r \<uplus>\<^bsub>R\<^esub> mx
[PROOF STEP]
apply (frule_tac a = a in principal_ideal,
        frule_tac I = "R \<diamondsuit>\<^sub>p a" in ideal_subset1)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a. \<lbrakk>1\<^sub>r \<in> carrier R; maximal_ideal R mx; a \<uplus>\<^bsub>R\<^esub> mx \<noteq> mx; ideal R mx; a \<in> carrier R; x = a \<uplus>\<^bsub>R\<^esub> mx; a \<notin> mx; 1\<^sub>r \<in> mx \<minusplus> R \<diamondsuit>\<^sub>p a; mx \<subseteq> carrier R; ideal R (R \<diamondsuit>\<^sub>p a); R \<diamondsuit>\<^sub>p a \<subseteq> carrier R\<rbrakk> \<Longrightarrow> \<exists>y. (\<exists>a\<in>carrier R. a \<uplus>\<^bsub>R\<^esub> mx = y) \<and> rcostOp R mx y (a \<uplus>\<^bsub>R\<^esub> mx) = 1\<^sub>r \<uplus>\<^bsub>R\<^esub> mx
[PROOF STEP]
apply (cut_tac ring_is_ag,
        simp add:aGroup.set_sum, (erule bexE)+)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a h k. \<lbrakk>1\<^sub>r \<in> carrier R; maximal_ideal R mx; a \<uplus>\<^bsub>R\<^esub> mx \<noteq> mx; ideal R mx; a \<in> carrier R; x = a \<uplus>\<^bsub>R\<^esub> mx; a \<notin> mx; mx \<subseteq> carrier R; ideal R (R \<diamondsuit>\<^sub>p a); R \<diamondsuit>\<^sub>p a \<subseteq> carrier R; aGroup R; h \<in> mx; k \<in> R \<diamondsuit>\<^sub>p a; 1\<^sub>r = h \<plusminus> k\<rbrakk> \<Longrightarrow> \<exists>y. (\<exists>a\<in>carrier R. a \<uplus>\<^bsub>R\<^esub> mx = y) \<and> rcostOp R mx y (a \<uplus>\<^bsub>R\<^esub> mx) = 1\<^sub>r \<uplus>\<^bsub>R\<^esub> mx
[PROOF STEP]
apply (thin_tac "ideal R (R \<diamondsuit>\<^sub>p a)", thin_tac "R \<diamondsuit>\<^sub>p a \<subseteq> carrier R",
        simp add:Rxa_def, (erule bexE)+, simp, thin_tac "k = r \<cdot>\<^sub>r a")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a h k r. \<lbrakk>h \<plusminus> r \<cdot>\<^sub>r a \<in> carrier R; maximal_ideal R mx; a \<uplus>\<^bsub>R\<^esub> mx \<noteq> mx; ideal R mx; a \<in> carrier R; x = a \<uplus>\<^bsub>R\<^esub> mx; a \<notin> mx; mx \<subseteq> carrier R; aGroup R; h \<in> mx; 1\<^sub>r = h \<plusminus> r \<cdot>\<^sub>r a; r \<in> carrier R\<rbrakk> \<Longrightarrow> \<exists>y. (\<exists>a\<in>carrier R. a \<uplus>\<^bsub>R\<^esub> mx = y) \<and> rcostOp R mx y (a \<uplus>\<^bsub>R\<^esub> mx) = (h \<plusminus> r \<cdot>\<^sub>r a) \<uplus>\<^bsub>R\<^esub> mx
[PROOF STEP]
apply (frule_tac a = r and b = a in rcostOp[of "mx"], assumption+)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a h k r. \<lbrakk>h \<plusminus> r \<cdot>\<^sub>r a \<in> carrier R; maximal_ideal R mx; a \<uplus>\<^bsub>R\<^esub> mx \<noteq> mx; ideal R mx; a \<in> carrier R; x = a \<uplus>\<^bsub>R\<^esub> mx; a \<notin> mx; mx \<subseteq> carrier R; aGroup R; h \<in> mx; 1\<^sub>r = h \<plusminus> r \<cdot>\<^sub>r a; r \<in> carrier R; rcostOp R mx (r \<uplus>\<^bsub>R\<^esub> mx) (a \<uplus>\<^bsub>R\<^esub> mx) = r \<cdot>\<^sub>r a \<uplus>\<^bsub>R\<^esub> mx\<rbrakk> \<Longrightarrow> \<exists>y. (\<exists>a\<in>carrier R. a \<uplus>\<^bsub>R\<^esub> mx = y) \<and> rcostOp R mx y (a \<uplus>\<^bsub>R\<^esub> mx) = (h \<plusminus> r \<cdot>\<^sub>r a) \<uplus>\<^bsub>R\<^esub> mx
[PROOF STEP]
apply (frule_tac x = r and y = a in ring_tOp_closed, assumption+)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a h k r. \<lbrakk>h \<plusminus> r \<cdot>\<^sub>r a \<in> carrier R; maximal_ideal R mx; a \<uplus>\<^bsub>R\<^esub> mx \<noteq> mx; ideal R mx; a \<in> carrier R; x = a \<uplus>\<^bsub>R\<^esub> mx; a \<notin> mx; mx \<subseteq> carrier R; aGroup R; h \<in> mx; 1\<^sub>r = h \<plusminus> r \<cdot>\<^sub>r a; r \<in> carrier R; rcostOp R mx (r \<uplus>\<^bsub>R\<^esub> mx) (a \<uplus>\<^bsub>R\<^esub> mx) = r \<cdot>\<^sub>r a \<uplus>\<^bsub>R\<^esub> mx; r \<cdot>\<^sub>r a \<in> carrier R\<rbrakk> \<Longrightarrow> \<exists>y. (\<exists>a\<in>carrier R. a \<uplus>\<^bsub>R\<^esub> mx = y) \<and> rcostOp R mx y (a \<uplus>\<^bsub>R\<^esub> mx) = (h \<plusminus> r \<cdot>\<^sub>r a) \<uplus>\<^bsub>R\<^esub> mx
[PROOF STEP]
apply (frule_tac a = "r \<cdot>\<^sub>r a" and x = h and b = "1\<^sub>r" in
        aGroup.ag_eq_sol2[of "R"], assumption+)
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<And>a h k r. \<lbrakk>h \<plusminus> r \<cdot>\<^sub>r a \<in> carrier R; maximal_ideal R mx; a \<uplus>\<^bsub>R\<^esub> mx \<noteq> mx; ideal R mx; a \<in> carrier R; x = a \<uplus>\<^bsub>R\<^esub> mx; a \<notin> mx; mx \<subseteq> carrier R; aGroup R; h \<in> mx; 1\<^sub>r = h \<plusminus> r \<cdot>\<^sub>r a; r \<in> carrier R; rcostOp R mx (r \<uplus>\<^bsub>R\<^esub> mx) (a \<uplus>\<^bsub>R\<^esub> mx) = r \<cdot>\<^sub>r a \<uplus>\<^bsub>R\<^esub> mx; r \<cdot>\<^sub>r a \<in> carrier R\<rbrakk> \<Longrightarrow> h \<in> carrier R
 2. \<And>a h k r. \<lbrakk>h \<plusminus> r \<cdot>\<^sub>r a \<in> carrier R; maximal_ideal R mx; a \<uplus>\<^bsub>R\<^esub> mx \<noteq> mx; ideal R mx; a \<in> carrier R; x = a \<uplus>\<^bsub>R\<^esub> mx; a \<notin> mx; mx \<subseteq> carrier R; aGroup R; h \<in> mx; 1\<^sub>r = h \<plusminus> r \<cdot>\<^sub>r a; r \<in> carrier R; rcostOp R mx (r \<uplus>\<^bsub>R\<^esub> mx) (a \<uplus>\<^bsub>R\<^esub> mx) = r \<cdot>\<^sub>r a \<uplus>\<^bsub>R\<^esub> mx; r \<cdot>\<^sub>r a \<in> carrier R\<rbrakk> \<Longrightarrow> 1\<^sub>r \<in> carrier R
 3. \<And>a h k r. \<lbrakk>h \<plusminus> r \<cdot>\<^sub>r a \<in> carrier R; maximal_ideal R mx; a \<uplus>\<^bsub>R\<^esub> mx \<noteq> mx; ideal R mx; a \<in> carrier R; x = a \<uplus>\<^bsub>R\<^esub> mx; a \<notin> mx; mx \<subseteq> carrier R; aGroup R; h \<in> mx; 1\<^sub>r = h \<plusminus> r \<cdot>\<^sub>r a; r \<in> carrier R; rcostOp R mx (r \<uplus>\<^bsub>R\<^esub> mx) (a \<uplus>\<^bsub>R\<^esub> mx) = r \<cdot>\<^sub>r a \<uplus>\<^bsub>R\<^esub> mx; r \<cdot>\<^sub>r a \<in> carrier R\<rbrakk> \<Longrightarrow> h \<plusminus> r \<cdot>\<^sub>r a = 1\<^sub>r
 4. \<And>a h k r. \<lbrakk>h \<plusminus> r \<cdot>\<^sub>r a \<in> carrier R; maximal_ideal R mx; a \<uplus>\<^bsub>R\<^esub> mx \<noteq> mx; ideal R mx; a \<in> carrier R; x = a \<uplus>\<^bsub>R\<^esub> mx; a \<notin> mx; mx \<subseteq> carrier R; aGroup R; h \<in> mx; 1\<^sub>r = h \<plusminus> r \<cdot>\<^sub>r a; r \<in> carrier R; rcostOp R mx (r \<uplus>\<^bsub>R\<^esub> mx) (a \<uplus>\<^bsub>R\<^esub> mx) = r \<cdot>\<^sub>r a \<uplus>\<^bsub>R\<^esub> mx; r \<cdot>\<^sub>r a \<in> carrier R; h = 1\<^sub>r \<plusminus> -\<^sub>a r \<cdot>\<^sub>r a\<rbrakk> \<Longrightarrow> \<exists>y. (\<exists>a\<in>carrier R. a \<uplus>\<^bsub>R\<^esub> mx = y) \<and> rcostOp R mx y (a \<uplus>\<^bsub>R\<^esub> mx) = (h \<plusminus> r \<cdot>\<^sub>r a) \<uplus>\<^bsub>R\<^esub> mx
[PROOF STEP]
apply (simp add:ideal_subset)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>a h k r. \<lbrakk>h \<plusminus> r \<cdot>\<^sub>r a \<in> carrier R; maximal_ideal R mx; a \<uplus>\<^bsub>R\<^esub> mx \<noteq> mx; ideal R mx; a \<in> carrier R; x = a \<uplus>\<^bsub>R\<^esub> mx; a \<notin> mx; mx \<subseteq> carrier R; aGroup R; h \<in> mx; 1\<^sub>r = h \<plusminus> r \<cdot>\<^sub>r a; r \<in> carrier R; rcostOp R mx (r \<uplus>\<^bsub>R\<^esub> mx) (a \<uplus>\<^bsub>R\<^esub> mx) = r \<cdot>\<^sub>r a \<uplus>\<^bsub>R\<^esub> mx; r \<cdot>\<^sub>r a \<in> carrier R\<rbrakk> \<Longrightarrow> 1\<^sub>r \<in> carrier R
 2. \<And>a h k r. \<lbrakk>h \<plusminus> r \<cdot>\<^sub>r a \<in> carrier R; maximal_ideal R mx; a \<uplus>\<^bsub>R\<^esub> mx \<noteq> mx; ideal R mx; a \<in> carrier R; x = a \<uplus>\<^bsub>R\<^esub> mx; a \<notin> mx; mx \<subseteq> carrier R; aGroup R; h \<in> mx; 1\<^sub>r = h \<plusminus> r \<cdot>\<^sub>r a; r \<in> carrier R; rcostOp R mx (r \<uplus>\<^bsub>R\<^esub> mx) (a \<uplus>\<^bsub>R\<^esub> mx) = r \<cdot>\<^sub>r a \<uplus>\<^bsub>R\<^esub> mx; r \<cdot>\<^sub>r a \<in> carrier R\<rbrakk> \<Longrightarrow> h \<plusminus> r \<cdot>\<^sub>r a = 1\<^sub>r
 3. \<And>a h k r. \<lbrakk>h \<plusminus> r \<cdot>\<^sub>r a \<in> carrier R; maximal_ideal R mx; a \<uplus>\<^bsub>R\<^esub> mx \<noteq> mx; ideal R mx; a \<in> carrier R; x = a \<uplus>\<^bsub>R\<^esub> mx; a \<notin> mx; mx \<subseteq> carrier R; aGroup R; h \<in> mx; 1\<^sub>r = h \<plusminus> r \<cdot>\<^sub>r a; r \<in> carrier R; rcostOp R mx (r \<uplus>\<^bsub>R\<^esub> mx) (a \<uplus>\<^bsub>R\<^esub> mx) = r \<cdot>\<^sub>r a \<uplus>\<^bsub>R\<^esub> mx; r \<cdot>\<^sub>r a \<in> carrier R; h = 1\<^sub>r \<plusminus> -\<^sub>a r \<cdot>\<^sub>r a\<rbrakk> \<Longrightarrow> \<exists>y. (\<exists>a\<in>carrier R. a \<uplus>\<^bsub>R\<^esub> mx = y) \<and> rcostOp R mx y (a \<uplus>\<^bsub>R\<^esub> mx) = (h \<plusminus> r \<cdot>\<^sub>r a) \<uplus>\<^bsub>R\<^esub> mx
[PROOF STEP]
apply (simp add:ring_one, simp)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a h k r. \<lbrakk>h \<plusminus> r \<cdot>\<^sub>r a \<in> carrier R; maximal_ideal R mx; a \<uplus>\<^bsub>R\<^esub> mx \<noteq> mx; ideal R mx; a \<in> carrier R; x = a \<uplus>\<^bsub>R\<^esub> mx; a \<notin> mx; mx \<subseteq> carrier R; aGroup R; h \<in> mx; 1\<^sub>r = h \<plusminus> r \<cdot>\<^sub>r a; r \<in> carrier R; rcostOp R mx (r \<uplus>\<^bsub>R\<^esub> mx) (a \<uplus>\<^bsub>R\<^esub> mx) = r \<cdot>\<^sub>r a \<uplus>\<^bsub>R\<^esub> mx; r \<cdot>\<^sub>r a \<in> carrier R; h = 1\<^sub>r \<plusminus> -\<^sub>a r \<cdot>\<^sub>r a\<rbrakk> \<Longrightarrow> \<exists>y. (\<exists>a\<in>carrier R. a \<uplus>\<^bsub>R\<^esub> mx = y) \<and> rcostOp R mx y (a \<uplus>\<^bsub>R\<^esub> mx) = (h \<plusminus> r \<cdot>\<^sub>r a) \<uplus>\<^bsub>R\<^esub> mx
[PROOF STEP]
apply (frule_tac a = h and b = "1\<^sub>r \<plusminus> -\<^sub>a (r \<cdot>\<^sub>r a)" and A = mx in
              eq_elem_in, assumption+)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a h k r. \<lbrakk>h \<plusminus> r \<cdot>\<^sub>r a \<in> carrier R; maximal_ideal R mx; a \<uplus>\<^bsub>R\<^esub> mx \<noteq> mx; ideal R mx; a \<in> carrier R; x = a \<uplus>\<^bsub>R\<^esub> mx; a \<notin> mx; mx \<subseteq> carrier R; aGroup R; h \<in> mx; 1\<^sub>r = h \<plusminus> r \<cdot>\<^sub>r a; r \<in> carrier R; rcostOp R mx (r \<uplus>\<^bsub>R\<^esub> mx) (a \<uplus>\<^bsub>R\<^esub> mx) = r \<cdot>\<^sub>r a \<uplus>\<^bsub>R\<^esub> mx; r \<cdot>\<^sub>r a \<in> carrier R; h = 1\<^sub>r \<plusminus> -\<^sub>a r \<cdot>\<^sub>r a; 1\<^sub>r \<plusminus> -\<^sub>a r \<cdot>\<^sub>r a \<in> mx\<rbrakk> \<Longrightarrow> \<exists>y. (\<exists>a\<in>carrier R. a \<uplus>\<^bsub>R\<^esub> mx = y) \<and> rcostOp R mx y (a \<uplus>\<^bsub>R\<^esub> mx) = (h \<plusminus> r \<cdot>\<^sub>r a) \<uplus>\<^bsub>R\<^esub> mx
[PROOF STEP]
apply (frule_tac a = "r \<cdot>\<^sub>r a" and b = "1\<^sub>r" in ar_coset_same1[of "mx"],
        rule ring_tOp_closed, assumption+, rule ring_one, assumption)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a h k r. \<lbrakk>h \<plusminus> r \<cdot>\<^sub>r a \<in> carrier R; maximal_ideal R mx; a \<uplus>\<^bsub>R\<^esub> mx \<noteq> mx; ideal R mx; a \<in> carrier R; x = a \<uplus>\<^bsub>R\<^esub> mx; a \<notin> mx; mx \<subseteq> carrier R; aGroup R; h \<in> mx; 1\<^sub>r = h \<plusminus> r \<cdot>\<^sub>r a; r \<in> carrier R; rcostOp R mx (r \<uplus>\<^bsub>R\<^esub> mx) (a \<uplus>\<^bsub>R\<^esub> mx) = r \<cdot>\<^sub>r a \<uplus>\<^bsub>R\<^esub> mx; r \<cdot>\<^sub>r a \<in> carrier R; h = 1\<^sub>r \<plusminus> -\<^sub>a r \<cdot>\<^sub>r a; 1\<^sub>r \<plusminus> -\<^sub>a r \<cdot>\<^sub>r a \<in> mx; r \<cdot>\<^sub>r a \<uplus>\<^bsub>R\<^esub> mx = 1\<^sub>r \<uplus>\<^bsub>R\<^esub> mx\<rbrakk> \<Longrightarrow> \<exists>y. (\<exists>a\<in>carrier R. a \<uplus>\<^bsub>R\<^esub> mx = y) \<and> rcostOp R mx y (a \<uplus>\<^bsub>R\<^esub> mx) = (h \<plusminus> r \<cdot>\<^sub>r a) \<uplus>\<^bsub>R\<^esub> mx
[PROOF STEP]
apply (frule_tac a1 = "r \<cdot>\<^sub>r a" and h1 = h in aGroup.arcos_fixed[THEN sym,
         of R mx],  unfold ideal_def, erule conjE, assumption+,
         thin_tac "R +> mx \<and> (\<forall>r\<in>carrier R. \<forall>x\<in>mx. r \<cdot>\<^sub>r x \<in> mx)",
         thin_tac "x = a \<uplus>\<^bsub>R\<^esub> mx",
         thin_tac "1\<^sub>r = h \<plusminus> r \<cdot>\<^sub>r a",
         thin_tac "h = 1\<^sub>r \<plusminus> -\<^sub>a (r \<cdot>\<^sub>r a)", thin_tac "1\<^sub>r \<plusminus> -\<^sub>a (r \<cdot>\<^sub>r a) \<in> mx")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a h k r. \<lbrakk>h \<plusminus> r \<cdot>\<^sub>r a \<in> carrier R; maximal_ideal R mx; a \<uplus>\<^bsub>R\<^esub> mx \<noteq> mx; a \<in> carrier R; a \<notin> mx; mx \<subseteq> carrier R; aGroup R; h \<in> mx; r \<in> carrier R; rcostOp R mx (r \<uplus>\<^bsub>R\<^esub> mx) (a \<uplus>\<^bsub>R\<^esub> mx) = r \<cdot>\<^sub>r a \<uplus>\<^bsub>R\<^esub> mx; r \<cdot>\<^sub>r a \<in> carrier R; r \<cdot>\<^sub>r a \<uplus>\<^bsub>R\<^esub> mx = 1\<^sub>r \<uplus>\<^bsub>R\<^esub> mx; (h \<plusminus> r \<cdot>\<^sub>r a) \<uplus>\<^bsub>R\<^esub> mx = r \<cdot>\<^sub>r a \<uplus>\<^bsub>R\<^esub> mx\<rbrakk> \<Longrightarrow> \<exists>y. (\<exists>a\<in>carrier R. a \<uplus>\<^bsub>R\<^esub> mx = y) \<and> rcostOp R mx y (a \<uplus>\<^bsub>R\<^esub> mx) = (h \<plusminus> r \<cdot>\<^sub>r a) \<uplus>\<^bsub>R\<^esub> mx
[PROOF STEP]
apply (rename_tac b h k r)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>b h k r. \<lbrakk>h \<plusminus> r \<cdot>\<^sub>r b \<in> carrier R; maximal_ideal R mx; b \<uplus>\<^bsub>R\<^esub> mx \<noteq> mx; b \<in> carrier R; b \<notin> mx; mx \<subseteq> carrier R; aGroup R; h \<in> mx; r \<in> carrier R; rcostOp R mx (r \<uplus>\<^bsub>R\<^esub> mx) (b \<uplus>\<^bsub>R\<^esub> mx) = r \<cdot>\<^sub>r b \<uplus>\<^bsub>R\<^esub> mx; r \<cdot>\<^sub>r b \<in> carrier R; r \<cdot>\<^sub>r b \<uplus>\<^bsub>R\<^esub> mx = 1\<^sub>r \<uplus>\<^bsub>R\<^esub> mx; (h \<plusminus> r \<cdot>\<^sub>r b) \<uplus>\<^bsub>R\<^esub> mx = r \<cdot>\<^sub>r b \<uplus>\<^bsub>R\<^esub> mx\<rbrakk> \<Longrightarrow> \<exists>y. (\<exists>a\<in>carrier R. a \<uplus>\<^bsub>R\<^esub> mx = y) \<and> rcostOp R mx y (b \<uplus>\<^bsub>R\<^esub> mx) = (h \<plusminus> r \<cdot>\<^sub>r b) \<uplus>\<^bsub>R\<^esub> mx
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>b h r. \<lbrakk>h \<plusminus> r \<cdot>\<^sub>r b \<in> carrier R; maximal_ideal R mx; b \<uplus>\<^bsub>R\<^esub> mx \<noteq> mx; b \<in> carrier R; b \<notin> mx; mx \<subseteq> carrier R; aGroup R; h \<in> mx; r \<in> carrier R; rcostOp R mx (r \<uplus>\<^bsub>R\<^esub> mx) (b \<uplus>\<^bsub>R\<^esub> mx) = 1\<^sub>r \<uplus>\<^bsub>R\<^esub> mx; r \<cdot>\<^sub>r b \<in> carrier R; r \<cdot>\<^sub>r b \<uplus>\<^bsub>R\<^esub> mx = 1\<^sub>r \<uplus>\<^bsub>R\<^esub> mx; (h \<plusminus> r \<cdot>\<^sub>r b) \<uplus>\<^bsub>R\<^esub> mx = 1\<^sub>r \<uplus>\<^bsub>R\<^esub> mx\<rbrakk> \<Longrightarrow> \<exists>y. (\<exists>a\<in>carrier R. a \<uplus>\<^bsub>R\<^esub> mx = y) \<and> rcostOp R mx y (b \<uplus>\<^bsub>R\<^esub> mx) = 1\<^sub>r \<uplus>\<^bsub>R\<^esub> mx
[PROOF STEP]
apply blast
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma (in Ring) residue_field_cd:"maximal_ideal R mx \<Longrightarrow>
                                           Corps (qring R mx)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. maximal_ideal R mx \<Longrightarrow> Corps (R /\<^sub>r mx)
[PROOF STEP]
apply (rule Corps.intro)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. maximal_ideal R mx \<Longrightarrow> Ring (R /\<^sub>r mx)
 2. maximal_ideal R mx \<Longrightarrow> \<forall>x\<in>carrier (R /\<^sub>r mx) - {\<zero>\<^bsub>R /\<^sub>r mx\<^esub>}. \<exists>x'\<in>carrier (R /\<^sub>r mx). x' \<cdot>\<^sub>r\<^bsub>R /\<^sub>r mx\<^esub> x = 1\<^sub>r\<^bsub>R /\<^sub>r mx\<^esub>
[PROOF STEP]
apply (rule Ring.qring_ring, rule Ring_axioms)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. maximal_ideal R mx \<Longrightarrow> ideal R mx
 2. maximal_ideal R mx \<Longrightarrow> \<forall>x\<in>carrier (R /\<^sub>r mx) - {\<zero>\<^bsub>R /\<^sub>r mx\<^esub>}. \<exists>x'\<in>carrier (R /\<^sub>r mx). x' \<cdot>\<^sub>r\<^bsub>R /\<^sub>r mx\<^esub> x = 1\<^sub>r\<^bsub>R /\<^sub>r mx\<^esub>
[PROOF STEP]
apply (simp add:maximal_ideal_ideal)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. maximal_ideal R mx \<Longrightarrow> \<forall>x\<in>carrier (R /\<^sub>r mx) - {\<zero>\<^bsub>R /\<^sub>r mx\<^esub>}. \<exists>x'\<in>carrier (R /\<^sub>r mx). x' \<cdot>\<^sub>r\<^bsub>R /\<^sub>r mx\<^esub> x = 1\<^sub>r\<^bsub>R /\<^sub>r mx\<^esub>
[PROOF STEP]
apply (simp add:residue_fieldTr[of "mx"])
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma (in Ring) maximal_set_idealTr:
       "maximal_set {I. ideal R I \<and> S \<inter> I = {}} mx \<Longrightarrow> ideal R mx"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. maximal_set {I. ideal R I \<and> S \<inter> I = {}} mx \<Longrightarrow> ideal R mx
[PROOF STEP]
by (simp add:maximal_set_def)


[STATEMENT]
lemma (in Ring) maximal_setTr:"\<lbrakk>maximal_set {I. ideal R I \<and> S \<inter> I = {}} mx;
                                         ideal R J; mx \<subset> J \<rbrakk> \<Longrightarrow> S \<inter> J \<noteq> {}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>maximal_set {I. ideal R I \<and> S \<inter> I = {}} mx; ideal R J; mx \<subset> J\<rbrakk> \<Longrightarrow> S \<inter> J \<noteq> {}
[PROOF STEP]
by (rule contrapos_pp, simp+, simp add:psubset_eq, erule conjE,
       simp add:maximal_set_def, blast)