[STATEMENT]
lemma (in PolynRg) divisionTr4:"\<lbrakk>Corps S; g \<in> carrier R; g \<noteq> \<zero>;
       0 < deg_n R S X g; f \<in> carrier R\<rbrakk> \<Longrightarrow>
   \<exists>q\<in>carrier R. (f = q \<cdot>\<^sub>r g) \<or> (\<exists>r\<in>carrier R. r \<noteq> \<zero> \<and> (f = (q \<cdot>\<^sub>r g) \<plusminus> r)
     \<and> (deg_n R S X r) < (deg_n R S X g))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>Corps S; g \<in> carrier R; g \<noteq> \<zero>; 0 < deg_n R S X g; f \<in> carrier R\<rbrakk> \<Longrightarrow> \<exists>q\<in>carrier R. f = q \<cdot>\<^sub>r g \<or> (\<exists>r\<in>carrier R. r \<noteq> \<zero> \<and> f = q \<cdot>\<^sub>r g \<plusminus> r \<and> deg_n R S X r < deg_n R S X g)
[PROOF STEP]
apply (cut_tac is_Ring,
       cut_tac ring_is_ag)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>Corps S; g \<in> carrier R; g \<noteq> \<zero>; 0 < deg_n R S X g; f \<in> carrier R; Ring R; aGroup R\<rbrakk> \<Longrightarrow> \<exists>q\<in>carrier R. f = q \<cdot>\<^sub>r g \<or> (\<exists>r\<in>carrier R. r \<noteq> \<zero> \<and> f = q \<cdot>\<^sub>r g \<plusminus> r \<and> deg_n R S X r < deg_n R S X g)
[PROOF STEP]
apply (frule divisionTr3[of g f], assumption+,
       erule bexE,
       frule_tac x = q in ring_tOp_closed[of  _ g], assumption+,
       erule disjE)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>q. \<lbrakk>Corps S; g \<in> carrier R; g \<noteq> \<zero>; 0 < deg_n R S X g; f \<in> carrier R; Ring R; aGroup R; q \<in> carrier R; q \<cdot>\<^sub>r g \<in> carrier R; f \<plusminus> -\<^sub>a q \<cdot>\<^sub>r g = \<zero>\<rbrakk> \<Longrightarrow> \<exists>q\<in>carrier R. f = q \<cdot>\<^sub>r g \<or> (\<exists>r\<in>carrier R. r \<noteq> \<zero> \<and> f = q \<cdot>\<^sub>r g \<plusminus> r \<and> deg_n R S X r < deg_n R S X g)
 2. \<And>q. \<lbrakk>Corps S; g \<in> carrier R; g \<noteq> \<zero>; 0 < deg_n R S X g; f \<in> carrier R; Ring R; aGroup R; q \<in> carrier R; q \<cdot>\<^sub>r g \<in> carrier R; f \<plusminus> -\<^sub>a q \<cdot>\<^sub>r g \<noteq> \<zero> \<and> deg_n R S X (f \<plusminus> -\<^sub>a q \<cdot>\<^sub>r g) < deg_n R S X g\<rbrakk> \<Longrightarrow> \<exists>q\<in>carrier R. f = q \<cdot>\<^sub>r g \<or> (\<exists>r\<in>carrier R. r \<noteq> \<zero> \<and> f = q \<cdot>\<^sub>r g \<plusminus> r \<and> deg_n R S X r < deg_n R S X g)
[PROOF STEP]
apply (simp add:aGroup.ag_eq_diffzero[THEN sym, of "R" "f"], blast)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>q. \<lbrakk>Corps S; g \<in> carrier R; g \<noteq> \<zero>; 0 < deg_n R S X g; f \<in> carrier R; Ring R; aGroup R; q \<in> carrier R; q \<cdot>\<^sub>r g \<in> carrier R; f \<plusminus> -\<^sub>a q \<cdot>\<^sub>r g \<noteq> \<zero> \<and> deg_n R S X (f \<plusminus> -\<^sub>a q \<cdot>\<^sub>r g) < deg_n R S X g\<rbrakk> \<Longrightarrow> \<exists>q\<in>carrier R. f = q \<cdot>\<^sub>r g \<or> (\<exists>r\<in>carrier R. r \<noteq> \<zero> \<and> f = q \<cdot>\<^sub>r g \<plusminus> r \<and> deg_n R S X r < deg_n R S X g)
[PROOF STEP]
apply (subgoal_tac "f = q \<cdot>\<^sub>r g \<plusminus> (f \<plusminus> -\<^sub>a (q \<cdot>\<^sub>r g))",
       subgoal_tac "(f \<plusminus> -\<^sub>a (q \<cdot>\<^sub>r g)) \<in> carrier R", blast,
       rule aGroup.ag_pOp_closed, assumption+,
       rule aGroup.ag_mOp_closed, assumption+)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>q. \<lbrakk>Corps S; g \<in> carrier R; g \<noteq> \<zero>; 0 < deg_n R S X g; f \<in> carrier R; Ring R; aGroup R; q \<in> carrier R; q \<cdot>\<^sub>r g \<in> carrier R; f \<plusminus> -\<^sub>a q \<cdot>\<^sub>r g \<noteq> \<zero> \<and> deg_n R S X (f \<plusminus> -\<^sub>a q \<cdot>\<^sub>r g) < deg_n R S X g\<rbrakk> \<Longrightarrow> f = q \<cdot>\<^sub>r g \<plusminus> (f \<plusminus> -\<^sub>a q \<cdot>\<^sub>r g)
[PROOF STEP]
apply (frule_tac x = "q \<cdot>\<^sub>r g" in aGroup.ag_mOp_closed, assumption+,
       subst aGroup.ag_pOp_assoc[THEN sym], assumption+,
       subst aGroup.ag_pOp_commute[of R _ f], assumption+,
       subst aGroup.ag_pOp_assoc, assumption+,
              simp add:aGroup.ag_r_inv1, simp add:aGroup.ag_r_zero)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma (in PolynRg) divisionTr:"\<lbrakk>Corps S; g \<in> carrier R; 0 < deg R S X g;
       f \<in> carrier R\<rbrakk> \<Longrightarrow>
       \<exists>q\<in>carrier R. (\<exists>r\<in>carrier R. (f = (q \<cdot>\<^sub>r g) \<plusminus> r) \<and>
                                  (deg R S X r) < (deg R S X g))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>Corps S; g \<in> carrier R; 0 < deg R S X g; f \<in> carrier R\<rbrakk> \<Longrightarrow> \<exists>q\<in>carrier R. \<exists>r\<in>carrier R. f = q \<cdot>\<^sub>r g \<plusminus> r \<and> deg R S X r < deg R S X g
[PROOF STEP]
apply (subgoal_tac "g \<noteq> \<zero>",
       frule divisionTr4[of g f], assumption+,
       simp add:deg_def, simp only:an_0[THEN sym],
       cut_tac aless_nat_less[of "0" "deg_n R S X g"],  simp, assumption)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>Corps S; g \<in> carrier R; 0 < deg R S X g; f \<in> carrier R; g \<noteq> \<zero>; \<exists>q\<in>carrier R. f = q \<cdot>\<^sub>r g \<or> (\<exists>r\<in>carrier R. r \<noteq> \<zero> \<and> f = q \<cdot>\<^sub>r g \<plusminus> r \<and> deg_n R S X r < deg_n R S X g)\<rbrakk> \<Longrightarrow> \<exists>q\<in>carrier R. \<exists>r\<in>carrier R. f = q \<cdot>\<^sub>r g \<plusminus> r \<and> deg R S X r < deg R S X g
 2. \<lbrakk>Corps S; g \<in> carrier R; 0 < deg R S X g; f \<in> carrier R\<rbrakk> \<Longrightarrow> g \<noteq> \<zero>
[PROOF STEP]
apply (erule bexE, erule disjE,
       cut_tac ring_is_ag, frule aGroup.ag_r_zero[of "R" "f"], simp, simp,
       rotate_tac -1, frule sym,
       cut_tac ring_zero,
       subgoal_tac "deg R S X \<zero> < deg R S X g", blast,
       simp add:deg_def an_def)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>q. \<lbrakk>Corps S; g \<in> carrier R; 0 < deg R S X g; f \<in> carrier R; g \<noteq> \<zero>; q \<in> carrier R; \<exists>r\<in>carrier R. r \<noteq> \<zero> \<and> f = q \<cdot>\<^sub>r g \<plusminus> r \<and> deg_n R S X r < deg_n R S X g\<rbrakk> \<Longrightarrow> \<exists>q\<in>carrier R. \<exists>r\<in>carrier R. f = q \<cdot>\<^sub>r g \<plusminus> r \<and> deg R S X r < deg R S X g
 2. \<lbrakk>Corps S; g \<in> carrier R; 0 < deg R S X g; f \<in> carrier R\<rbrakk> \<Longrightarrow> g \<noteq> \<zero>
[PROOF STEP]
apply (erule bexE, (erule conjE)+,
       cut_tac n1 = "deg_n R S X r" and m1 = "deg_n R S X g" in
       aless_natless[THEN sym], simp add:deg_def,
       drule sym, simp, rotate_tac -1, drule sym, blast)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>Corps S; g \<in> carrier R; 0 < deg R S X g; f \<in> carrier R\<rbrakk> \<Longrightarrow> g \<noteq> \<zero>
[PROOF STEP]
apply (rule contrapos_pp, simp+,
       simp add:deg_def, frule aless_imp_le[of "0" "-\<infinity>"],
       cut_tac minf_le_any[of "0"])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>Corps S; \<zero> \<in> carrier R; 0 < - \<infinity>; f \<in> carrier R; g = \<zero>; 0 \<le> - \<infinity>; - \<infinity> \<le> 0\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
apply (frule ale_antisym[of "0" "-\<infinity>"], assumption)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>Corps S; \<zero> \<in> carrier R; 0 < - \<infinity>; f \<in> carrier R; g = \<zero>; 0 \<le> - \<infinity>; - \<infinity> \<le> 0; 0 = - \<infinity>\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma (in PolynRg) rel_prime_equation:"\<lbrakk>Corps S; f \<in> carrier R; g \<in> carrier R;
      0 < deg R S X f; 0 < deg R S X g; rel_prime_pols R S X f g;
      h \<in> carrier R\<rbrakk> \<Longrightarrow>
     \<exists>u \<in> carrier R. \<exists>v \<in> carrier R.
     (deg R S X u \<le> amax ((deg R S X h) - (deg R S X f)) (deg R S X g)) \<and>
     (deg R S X v \<le> (deg R S X f)) \<and> (u \<cdot>\<^sub>r f \<plusminus> (v \<cdot>\<^sub>r g) = h)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>Corps S; f \<in> carrier R; g \<in> carrier R; 0 < deg R S X f; 0 < deg R S X g; rel_prime_pols R S X f g; h \<in> carrier R\<rbrakk> \<Longrightarrow> \<exists>u\<in>carrier R. \<exists>v\<in>carrier R. deg R S X u \<le> amax (deg R S X h - deg R S X f) (deg R S X g) \<and> deg R S X v \<le> deg R S X f \<and> u \<cdot>\<^sub>r f \<plusminus> v \<cdot>\<^sub>r g = h
[PROOF STEP]
apply (cut_tac ring_is_ag,
       cut_tac ring_zero, cut_tac subring, frule subring_Ring,
       frule aless_imp_le [of "0" "deg R S X f"],
       frule  pol_nonzero[of f], simp,
       frule aless_imp_le [of "0" "deg R S X g"],
       frule  pol_nonzero[of g], simp,
       frule Corps.field_is_idom[of "S"],
       cut_tac polyn_ring_integral, simp,
       frule Idomain.idom_tOp_nonzeros[of R f g], assumption+)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>Corps S; f \<in> carrier R; g \<in> carrier R; 0 < deg R S X f; 0 < deg R S X g; rel_prime_pols R S X f g; h \<in> carrier R; aGroup R; \<zero> \<in> carrier R; Subring R S; Ring S; f \<noteq> \<zero>; 0 \<le> deg R S X f; g \<noteq> \<zero>; 0 \<le> deg R S X g; Idomain R; Idomain S; f \<cdot>\<^sub>r g \<noteq> \<zero>\<rbrakk> \<Longrightarrow> \<exists>u\<in>carrier R. deg R S X u \<le> amax (deg R S X h - deg R S X f) (deg R S X g) \<and> (\<exists>v\<in>carrier R. deg R S X v \<le> deg R S X f \<and> u \<cdot>\<^sub>r f \<plusminus> v \<cdot>\<^sub>r g = h)
[PROOF STEP]
apply (case_tac "h = \<zero>\<^bsub>R\<^esub>")
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>Corps S; f \<in> carrier R; g \<in> carrier R; 0 < deg R S X f; 0 < deg R S X g; rel_prime_pols R S X f g; h \<in> carrier R; aGroup R; \<zero> \<in> carrier R; Subring R S; Ring S; f \<noteq> \<zero>; 0 \<le> deg R S X f; g \<noteq> \<zero>; 0 \<le> deg R S X g; Idomain R; Idomain S; f \<cdot>\<^sub>r g \<noteq> \<zero>; h = \<zero>\<rbrakk> \<Longrightarrow> \<exists>u\<in>carrier R. deg R S X u \<le> amax (deg R S X h - deg R S X f) (deg R S X g) \<and> (\<exists>v\<in>carrier R. deg R S X v \<le> deg R S X f \<and> u \<cdot>\<^sub>r f \<plusminus> v \<cdot>\<^sub>r g = h)
 2. \<lbrakk>Corps S; f \<in> carrier R; g \<in> carrier R; 0 < deg R S X f; 0 < deg R S X g; rel_prime_pols R S X f g; h \<in> carrier R; aGroup R; \<zero> \<in> carrier R; Subring R S; Ring S; f \<noteq> \<zero>; 0 \<le> deg R S X f; g \<noteq> \<zero>; 0 \<le> deg R S X g; Idomain R; Idomain S; f \<cdot>\<^sub>r g \<noteq> \<zero>; h \<noteq> \<zero>\<rbrakk> \<Longrightarrow> \<exists>u\<in>carrier R. deg R S X u \<le> amax (deg R S X h - deg R S X f) (deg R S X g) \<and> (\<exists>v\<in>carrier R. deg R S X v \<le> deg R S X f \<and> u \<cdot>\<^sub>r f \<plusminus> v \<cdot>\<^sub>r g = h)
[PROOF STEP]
apply (cut_tac ring_is_ag,
        cut_tac ring_zero,
        subgoal_tac "deg R S X \<zero> \<le>
                      amax (deg R S X h - deg R S X f) (deg R S X g)",
        subgoal_tac "deg R S X \<zero> \<le> deg R S X f \<and>
                     \<zero> \<cdot>\<^sub>r f \<plusminus> \<zero> \<cdot>\<^sub>r g = h", blast)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<lbrakk>Corps S; f \<in> carrier R; g \<in> carrier R; 0 < deg R S X f; 0 < deg R S X g; rel_prime_pols R S X f g; h \<in> carrier R; aGroup R; \<zero> \<in> carrier R; Subring R S; Ring S; f \<noteq> \<zero>; 0 \<le> deg R S X f; g \<noteq> \<zero>; 0 \<le> deg R S X g; Idomain R; Idomain S; f \<cdot>\<^sub>r g \<noteq> \<zero>; h = \<zero>; aGroup R; \<zero> \<in> carrier R; deg R S X \<zero> \<le> amax (deg R S X h - deg R S X f) (deg R S X g)\<rbrakk> \<Longrightarrow> deg R S X \<zero> \<le> deg R S X f \<and> \<zero> \<cdot>\<^sub>r f \<plusminus> \<zero> \<cdot>\<^sub>r g = h
 2. \<lbrakk>Corps S; f \<in> carrier R; g \<in> carrier R; 0 < deg R S X f; 0 < deg R S X g; rel_prime_pols R S X f g; h \<in> carrier R; aGroup R; \<zero> \<in> carrier R; Subring R S; Ring S; f \<noteq> \<zero>; 0 \<le> deg R S X f; g \<noteq> \<zero>; 0 \<le> deg R S X g; Idomain R; Idomain S; f \<cdot>\<^sub>r g \<noteq> \<zero>; h = \<zero>; aGroup R; \<zero> \<in> carrier R\<rbrakk> \<Longrightarrow> deg R S X \<zero> \<le> amax (deg R S X h - deg R S X f) (deg R S X g)
 3. \<lbrakk>Corps S; f \<in> carrier R; g \<in> carrier R; 0 < deg R S X f; 0 < deg R S X g; rel_prime_pols R S X f g; h \<in> carrier R; aGroup R; \<zero> \<in> carrier R; Subring R S; Ring S; f \<noteq> \<zero>; 0 \<le> deg R S X f; g \<noteq> \<zero>; 0 \<le> deg R S X g; Idomain R; Idomain S; f \<cdot>\<^sub>r g \<noteq> \<zero>; h \<noteq> \<zero>\<rbrakk> \<Longrightarrow> \<exists>u\<in>carrier R. deg R S X u \<le> amax (deg R S X h - deg R S X f) (deg R S X g) \<and> (\<exists>v\<in>carrier R. deg R S X v \<le> deg R S X f \<and> u \<cdot>\<^sub>r f \<plusminus> v \<cdot>\<^sub>r g = h)
[PROOF STEP]
apply (simp add:ring_times_0_x, simp add:aGroup.ag_r_zero,
        simp add:deg_def)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>Corps S; f \<in> carrier R; g \<in> carrier R; 0 < deg R S X f; 0 < deg R S X g; rel_prime_pols R S X f g; h \<in> carrier R; aGroup R; \<zero> \<in> carrier R; Subring R S; Ring S; f \<noteq> \<zero>; 0 \<le> deg R S X f; g \<noteq> \<zero>; 0 \<le> deg R S X g; Idomain R; Idomain S; f \<cdot>\<^sub>r g \<noteq> \<zero>; h = \<zero>; aGroup R; \<zero> \<in> carrier R\<rbrakk> \<Longrightarrow> deg R S X \<zero> \<le> amax (deg R S X h - deg R S X f) (deg R S X g)
 2. \<lbrakk>Corps S; f \<in> carrier R; g \<in> carrier R; 0 < deg R S X f; 0 < deg R S X g; rel_prime_pols R S X f g; h \<in> carrier R; aGroup R; \<zero> \<in> carrier R; Subring R S; Ring S; f \<noteq> \<zero>; 0 \<le> deg R S X f; g \<noteq> \<zero>; 0 \<le> deg R S X g; Idomain R; Idomain S; f \<cdot>\<^sub>r g \<noteq> \<zero>; h \<noteq> \<zero>\<rbrakk> \<Longrightarrow> \<exists>u\<in>carrier R. deg R S X u \<le> amax (deg R S X h - deg R S X f) (deg R S X g) \<and> (\<exists>v\<in>carrier R. deg R S X v \<le> deg R S X f \<and> u \<cdot>\<^sub>r f \<plusminus> v \<cdot>\<^sub>r g = h)
[PROOF STEP]
apply (simp add:deg_def amax_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>Corps S; f \<in> carrier R; g \<in> carrier R; 0 < deg R S X f; 0 < deg R S X g; rel_prime_pols R S X f g; h \<in> carrier R; aGroup R; \<zero> \<in> carrier R; Subring R S; Ring S; f \<noteq> \<zero>; 0 \<le> deg R S X f; g \<noteq> \<zero>; 0 \<le> deg R S X g; Idomain R; Idomain S; f \<cdot>\<^sub>r g \<noteq> \<zero>; h \<noteq> \<zero>\<rbrakk> \<Longrightarrow> \<exists>u\<in>carrier R. deg R S X u \<le> amax (deg R S X h - deg R S X f) (deg R S X g) \<and> (\<exists>v\<in>carrier R. deg R S X v \<le> deg R S X f \<and> u \<cdot>\<^sub>r f \<plusminus> v \<cdot>\<^sub>r g = h)
[PROOF STEP]
apply (simp add:rel_prime_pols_def,
       frule principal_ideal[of f], frule principal_ideal[of g],
       frule ideals_set_sum[of "R \<diamondsuit>\<^sub>p f" "R \<diamondsuit>\<^sub>p g" "1\<^sub>r"], assumption+,
       thin_tac "1\<^sub>r \<in> R \<diamondsuit>\<^sub>p f \<minusplus> R \<diamondsuit>\<^sub>p g",
       (erule bexE)+,
       thin_tac "ideal R (R \<diamondsuit>\<^sub>p f)", thin_tac "ideal R (R \<diamondsuit>\<^sub>p g)",
       simp add:Rxa_def, (erule bexE)+, simp,
       thin_tac "ha = r \<cdot>\<^sub>r f", thin_tac "k = ra \<cdot>\<^sub>r g")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>ha k r ra. \<lbrakk>Corps S; f \<in> carrier R; g \<in> carrier R; 0 < deg R S X f; 0 < deg R S X g; h \<in> carrier R; aGroup R; \<zero> \<in> carrier R; Subring R S; Ring S; f \<noteq> \<zero>; 0 \<le> deg R S X f; g \<noteq> \<zero>; 0 \<le> deg R S X g; Idomain R; Idomain S; f \<cdot>\<^sub>r g \<noteq> \<zero>; h \<noteq> \<zero>; 1\<^sub>r = r \<cdot>\<^sub>r f \<plusminus> ra \<cdot>\<^sub>r g; r \<in> carrier R; ra \<in> carrier R\<rbrakk> \<Longrightarrow> \<exists>u\<in>carrier R. deg R S X u \<le> amax (deg R S X h - deg R S X f) (deg R S X g) \<and> (\<exists>v\<in>carrier R. deg R S X v \<le> deg R S X f \<and> u \<cdot>\<^sub>r f \<plusminus> v \<cdot>\<^sub>r g = h)
[PROOF STEP]
apply (frule_tac x = r in ring_tOp_closed[of _ f], assumption+,
       frule_tac x = ra in ring_tOp_closed[of _ g], assumption+,
       frule_tac y1 = "r \<cdot>\<^sub>r f" and z1 = "ra \<cdot>\<^sub>r g" in ring_distrib1[THEN sym,
       of "h"], assumption+, simp add:ring_r_one, drule sym,
       simp,
       thin_tac "r \<cdot>\<^sub>r f \<plusminus> ra \<cdot>\<^sub>r g = 1\<^sub>r",
       simp add:ring_tOp_assoc[THEN sym], simp add:ring_r_one)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>r ra. \<lbrakk>Corps S; f \<in> carrier R; g \<in> carrier R; 0 < deg R S X f; 0 < deg R S X g; h \<in> carrier R; aGroup R; \<zero> \<in> carrier R; Subring R S; Ring S; f \<noteq> \<zero>; 0 \<le> deg R S X f; g \<noteq> \<zero>; 0 \<le> deg R S X g; Idomain R; Idomain S; f \<cdot>\<^sub>r g \<noteq> \<zero>; h \<noteq> \<zero>; r \<in> carrier R; ra \<in> carrier R; r \<cdot>\<^sub>r f \<in> carrier R; ra \<cdot>\<^sub>r g \<in> carrier R; h \<cdot>\<^sub>r r \<cdot>\<^sub>r f \<plusminus> h \<cdot>\<^sub>r ra \<cdot>\<^sub>r g = h\<rbrakk> \<Longrightarrow> \<exists>u\<in>carrier R. deg R S X u \<le> amax (deg R S X h - deg R S X f) (deg R S X g) \<and> (\<exists>v\<in>carrier R. deg R S X v \<le> deg R S X f \<and> u \<cdot>\<^sub>r f \<plusminus> v \<cdot>\<^sub>r g = h)
[PROOF STEP]
apply (frule_tac f = "h \<cdot>\<^sub>r r" in divisionTr[of g], assumption+,
       simp add:ring_tOp_closed,
       frule_tac f = "h \<cdot>\<^sub>r ra" in divisionTr[of f], assumption+,
       simp add:ring_tOp_closed,
       (erule bexE)+, (erule conjE)+)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>r ra q qa rb rc. \<lbrakk>Corps S; f \<in> carrier R; g \<in> carrier R; 0 < deg R S X f; 0 < deg R S X g; h \<in> carrier R; aGroup R; \<zero> \<in> carrier R; Subring R S; Ring S; f \<noteq> \<zero>; 0 \<le> deg R S X f; g \<noteq> \<zero>; 0 \<le> deg R S X g; Idomain R; Idomain S; f \<cdot>\<^sub>r g \<noteq> \<zero>; h \<noteq> \<zero>; r \<in> carrier R; ra \<in> carrier R; r \<cdot>\<^sub>r f \<in> carrier R; ra \<cdot>\<^sub>r g \<in> carrier R; h \<cdot>\<^sub>r r \<cdot>\<^sub>r f \<plusminus> h \<cdot>\<^sub>r ra \<cdot>\<^sub>r g = h; q \<in> carrier R; qa \<in> carrier R; rb \<in> carrier R; rc \<in> carrier R; h \<cdot>\<^sub>r r = q \<cdot>\<^sub>r g \<plusminus> rb; deg R S X rb < deg R S X g; h \<cdot>\<^sub>r ra = qa \<cdot>\<^sub>r f \<plusminus> rc; deg R S X rc < deg R S X f\<rbrakk> \<Longrightarrow> \<exists>u\<in>carrier R. deg R S X u \<le> amax (deg R S X h - deg R S X f) (deg R S X g) \<and> (\<exists>v\<in>carrier R. deg R S X v \<le> deg R S X f \<and> u \<cdot>\<^sub>r f \<plusminus> v \<cdot>\<^sub>r g = h)
[PROOF STEP]
(** final **)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>r ra q qa rb rc. \<lbrakk>Corps S; f \<in> carrier R; g \<in> carrier R; 0 < deg R S X f; 0 < deg R S X g; h \<in> carrier R; aGroup R; \<zero> \<in> carrier R; Subring R S; Ring S; f \<noteq> \<zero>; 0 \<le> deg R S X f; g \<noteq> \<zero>; 0 \<le> deg R S X g; Idomain R; Idomain S; f \<cdot>\<^sub>r g \<noteq> \<zero>; h \<noteq> \<zero>; r \<in> carrier R; ra \<in> carrier R; r \<cdot>\<^sub>r f \<in> carrier R; ra \<cdot>\<^sub>r g \<in> carrier R; h \<cdot>\<^sub>r r \<cdot>\<^sub>r f \<plusminus> h \<cdot>\<^sub>r ra \<cdot>\<^sub>r g = h; q \<in> carrier R; qa \<in> carrier R; rb \<in> carrier R; rc \<in> carrier R; h \<cdot>\<^sub>r r = q \<cdot>\<^sub>r g \<plusminus> rb; deg R S X rb < deg R S X g; h \<cdot>\<^sub>r ra = qa \<cdot>\<^sub>r f \<plusminus> rc; deg R S X rc < deg R S X f\<rbrakk> \<Longrightarrow> \<exists>u\<in>carrier R. deg R S X u \<le> amax (deg R S X h - deg R S X f) (deg R S X g) \<and> (\<exists>v\<in>carrier R. deg R S X v \<le> deg R S X f \<and> u \<cdot>\<^sub>r f \<plusminus> v \<cdot>\<^sub>r g = h)
[PROOF STEP]
apply (thin_tac " r \<in> carrier R",
       thin_tac "ra \<in> carrier R",
       thin_tac "r \<cdot>\<^sub>r f \<in> carrier R",
       thin_tac "ra \<cdot>\<^sub>r g \<in> carrier R")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>r ra q qa rb rc. \<lbrakk>Corps S; f \<in> carrier R; g \<in> carrier R; 0 < deg R S X f; 0 < deg R S X g; h \<in> carrier R; aGroup R; \<zero> \<in> carrier R; Subring R S; Ring S; f \<noteq> \<zero>; 0 \<le> deg R S X f; g \<noteq> \<zero>; 0 \<le> deg R S X g; Idomain R; Idomain S; f \<cdot>\<^sub>r g \<noteq> \<zero>; h \<noteq> \<zero>; h \<cdot>\<^sub>r r \<cdot>\<^sub>r f \<plusminus> h \<cdot>\<^sub>r ra \<cdot>\<^sub>r g = h; q \<in> carrier R; qa \<in> carrier R; rb \<in> carrier R; rc \<in> carrier R; h \<cdot>\<^sub>r r = q \<cdot>\<^sub>r g \<plusminus> rb; deg R S X rb < deg R S X g; h \<cdot>\<^sub>r ra = qa \<cdot>\<^sub>r f \<plusminus> rc; deg R S X rc < deg R S X f\<rbrakk> \<Longrightarrow> \<exists>u\<in>carrier R. deg R S X u \<le> amax (deg R S X h - deg R S X f) (deg R S X g) \<and> (\<exists>v\<in>carrier R. deg R S X v \<le> deg R S X f \<and> u \<cdot>\<^sub>r f \<plusminus> v \<cdot>\<^sub>r g = h)
[PROOF STEP]
apply (frule_tac x = q in ring_tOp_closed[of _ g], assumption+,
       frule_tac x = qa in ring_tOp_closed[of _ f], assumption+,
       frule_tac x = "q \<cdot>\<^sub>r g" and y = rb in aGroup.ag_pOp_commute, assumption+,
       simp,
       thin_tac "q \<cdot>\<^sub>r g \<plusminus> rb = rb \<plusminus> q \<cdot>\<^sub>r g",
       thin_tac  "h \<cdot>\<^sub>r r =  rb \<plusminus> q \<cdot>\<^sub>r g",
       thin_tac "h \<cdot>\<^sub>r ra =  qa \<cdot>\<^sub>r f \<plusminus> rc")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>r ra q qa rb rc. \<lbrakk>Corps S; f \<in> carrier R; g \<in> carrier R; 0 < deg R S X f; 0 < deg R S X g; h \<in> carrier R; aGroup R; \<zero> \<in> carrier R; Subring R S; Ring S; f \<noteq> \<zero>; 0 \<le> deg R S X f; g \<noteq> \<zero>; 0 \<le> deg R S X g; Idomain R; Idomain S; f \<cdot>\<^sub>r g \<noteq> \<zero>; h \<noteq> \<zero>; (rb \<plusminus> q \<cdot>\<^sub>r g) \<cdot>\<^sub>r f \<plusminus> (qa \<cdot>\<^sub>r f \<plusminus> rc) \<cdot>\<^sub>r g = h; q \<in> carrier R; qa \<in> carrier R; rb \<in> carrier R; rc \<in> carrier R; deg R S X rb < deg R S X g; deg R S X rc < deg R S X f; q \<cdot>\<^sub>r g \<in> carrier R; qa \<cdot>\<^sub>r f \<in> carrier R\<rbrakk> \<Longrightarrow> \<exists>u\<in>carrier R. deg R S X u \<le> amax (deg R S X h - deg R S X f) (deg R S X g) \<and> (\<exists>v\<in>carrier R. deg R S X v \<le> deg R S X f \<and> u \<cdot>\<^sub>r f \<plusminus> v \<cdot>\<^sub>r g = h)
[PROOF STEP]
apply (simp add:ring_distrib2[of g],
     frule_tac x = rb and y = "q \<cdot>\<^sub>r g" in aGroup.ag_pOp_closed[of R],
       assumption+,
     frule_tac x = "rb \<plusminus> q \<cdot>\<^sub>r g" and y = f in ring_tOp_closed,
      assumption+,
     frule_tac x = "qa \<cdot>\<^sub>r f" and y = g in ring_tOp_closed, assumption+,
     frule_tac x = rc and y = g in ring_tOp_closed, assumption+,
     simp add:aGroup.ag_pOp_assoc[THEN sym, of "R"],
     simp add:ring_tOp_assoc[of _ f g],
     simp add:ring_tOp_commute[of f g],
     simp add:ring_tOp_assoc[THEN sym, of  _ g f],
     frule_tac x = qa and y = g in ring_tOp_closed, assumption+,
     simp add:ring_distrib2[THEN sym],
     simp add:aGroup.ag_pOp_assoc,
     simp add:ring_distrib2[THEN sym],
     case_tac "q \<plusminus>\<^bsub>R\<^esub> qa = \<zero>\<^bsub>R\<^esub>", simp add:ring_times_0_x,
          simp add:aGroup.ag_r_zero,
     subgoal_tac "deg R S X rb \<le>
                         amax (deg R S X h - deg R S X f) (deg R S X g)",
            subgoal_tac "deg R S X rc \<le> deg R S X f",
            blast,
        simp add:aless_imp_le,
        frule_tac x = "deg R S X rb" and y = "deg R S X g" in
           aless_imp_le,
        rule_tac i = "deg R S X rb" in ale_trans[of _ "deg R S X g"
          "amax (deg R S X h - deg R S X f) (deg R S X g)"], assumption,
           simp add:amax_def, simp add:aneg_le aless_imp_le)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>q qa rb rc. \<lbrakk>Corps S; f \<in> carrier R; g \<in> carrier R; 0 < deg R S X f; 0 < deg R S X g; h \<in> carrier R; aGroup R; \<zero> \<in> carrier R; Subring R S; Ring S; f \<noteq> \<zero>; 0 \<le> deg R S X f; g \<noteq> \<zero>; 0 \<le> deg R S X g; Idomain R; Idomain S; g \<cdot>\<^sub>r f \<noteq> \<zero>; h \<noteq> \<zero>; (rb \<plusminus> (q \<plusminus> qa) \<cdot>\<^sub>r g) \<cdot>\<^sub>r f \<plusminus> rc \<cdot>\<^sub>r g = h; q \<in> carrier R; qa \<in> carrier R; rb \<in> carrier R; rc \<in> carrier R; deg R S X rb < deg R S X g; deg R S X rc < deg R S X f; q \<cdot>\<^sub>r g \<in> carrier R; qa \<cdot>\<^sub>r f \<in> carrier R; rb \<plusminus> q \<cdot>\<^sub>r g \<in> carrier R; (rb \<plusminus> q \<cdot>\<^sub>r g) \<cdot>\<^sub>r f \<in> carrier R; qa \<cdot>\<^sub>r g \<cdot>\<^sub>r f \<in> carrier R; rc \<cdot>\<^sub>r g \<in> carrier R; qa \<cdot>\<^sub>r g \<in> carrier R; q \<plusminus> qa \<noteq> \<zero>\<rbrakk> \<Longrightarrow> \<exists>u\<in>carrier R. deg R S X u \<le> amax (deg R S X h - deg R S X f) (deg R S X g) \<and> (\<exists>v\<in>carrier R. deg R S X v \<le> deg R S X f \<and> u \<cdot>\<^sub>r f \<plusminus> v \<cdot>\<^sub>r g = h)
[PROOF STEP]
apply (subgoal_tac "rb \<plusminus> (q \<plusminus> qa) \<cdot>\<^sub>r g \<in> carrier R",
       subgoal_tac "deg R S X (rb \<plusminus> (q \<plusminus> qa) \<cdot>\<^sub>r g) \<le>
                    amax (deg R S X h - deg R S X f) (deg R S X g)",
       subgoal_tac "deg R S X rc \<le> deg R S X f",  blast,
     simp add:aless_imp_le,
     frule_tac x = q and y = qa in aGroup.ag_pOp_closed[of "R"], assumption+,
     frule_tac p = rb and q = "(q \<plusminus> qa) \<cdot>\<^sub>r g" in deg_pols_add1,
     rule ring_tOp_closed, assumption+, simp add:deg_mult_pols1,
     frule_tac p1 = "q \<plusminus> qa" in pol_nonzero[THEN sym], simp)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>q qa rb rc. \<lbrakk>Corps S; f \<in> carrier R; g \<in> carrier R; 0 < deg R S X f; 0 < deg R S X g; h \<in> carrier R; aGroup R; \<zero> \<in> carrier R; Subring R S; Ring S; f \<noteq> \<zero>; 0 \<le> deg R S X f; g \<noteq> \<zero>; 0 \<le> deg R S X g; Idomain R; Idomain S; g \<cdot>\<^sub>r f \<noteq> \<zero>; h \<noteq> \<zero>; (rb \<plusminus> (q \<plusminus> qa) \<cdot>\<^sub>r g) \<cdot>\<^sub>r f \<plusminus> rc \<cdot>\<^sub>r g = h; q \<in> carrier R; qa \<in> carrier R; rb \<in> carrier R; rc \<in> carrier R; deg R S X rb < deg R S X g; deg R S X rc < deg R S X f; q \<cdot>\<^sub>r g \<in> carrier R; qa \<cdot>\<^sub>r f \<in> carrier R; rb \<plusminus> q \<cdot>\<^sub>r g \<in> carrier R; (rb \<plusminus> q \<cdot>\<^sub>r g) \<cdot>\<^sub>r f \<in> carrier R; qa \<cdot>\<^sub>r g \<cdot>\<^sub>r f \<in> carrier R; rc \<cdot>\<^sub>r g \<in> carrier R; qa \<cdot>\<^sub>r g \<in> carrier R; 0 \<le> deg R S X (q \<plusminus> qa); rb \<plusminus> (q \<plusminus> qa) \<cdot>\<^sub>r g \<in> carrier R; q \<plusminus> qa \<in> carrier R; q \<plusminus> qa \<noteq> \<zero>\<rbrakk> \<Longrightarrow> deg R S X rb < deg R S X (q \<plusminus> qa) + deg R S X g
 2. \<And>q qa rb rc. \<lbrakk>Corps S; f \<in> carrier R; g \<in> carrier R; 0 < deg R S X f; 0 < deg R S X g; h \<in> carrier R; aGroup R; \<zero> \<in> carrier R; Subring R S; Ring S; f \<noteq> \<zero>; 0 \<le> deg R S X f; g \<noteq> \<zero>; 0 \<le> deg R S X g; Idomain R; Idomain S; g \<cdot>\<^sub>r f \<noteq> \<zero>; h \<noteq> \<zero>; (rb \<plusminus> (q \<plusminus> qa) \<cdot>\<^sub>r g) \<cdot>\<^sub>r f \<plusminus> rc \<cdot>\<^sub>r g = h; q \<in> carrier R; qa \<in> carrier R; rb \<in> carrier R; rc \<in> carrier R; deg R S X rb < deg R S X g; deg R S X rc < deg R S X f; q \<cdot>\<^sub>r g \<in> carrier R; qa \<cdot>\<^sub>r f \<in> carrier R; rb \<plusminus> q \<cdot>\<^sub>r g \<in> carrier R; (rb \<plusminus> q \<cdot>\<^sub>r g) \<cdot>\<^sub>r f \<in> carrier R; qa \<cdot>\<^sub>r g \<cdot>\<^sub>r f \<in> carrier R; rc \<cdot>\<^sub>r g \<in> carrier R; qa \<cdot>\<^sub>r g \<in> carrier R; q \<plusminus> qa \<noteq> \<zero>; rb \<plusminus> (q \<plusminus> qa) \<cdot>\<^sub>r g \<in> carrier R; q \<plusminus> qa \<in> carrier R; deg R S X (rb \<plusminus> (q \<plusminus> qa) \<cdot>\<^sub>r g) = deg R S X ((q \<plusminus> qa) \<cdot>\<^sub>r g)\<rbrakk> \<Longrightarrow> deg R S X (rb \<plusminus> (q \<plusminus> qa) \<cdot>\<^sub>r g) \<le> amax (deg R S X h - deg R S X f) (deg R S X g)
 3. \<And>q qa rb rc. \<lbrakk>Corps S; f \<in> carrier R; g \<in> carrier R; 0 < deg R S X f; 0 < deg R S X g; h \<in> carrier R; aGroup R; \<zero> \<in> carrier R; Subring R S; Ring S; f \<noteq> \<zero>; 0 \<le> deg R S X f; g \<noteq> \<zero>; 0 \<le> deg R S X g; Idomain R; Idomain S; g \<cdot>\<^sub>r f \<noteq> \<zero>; h \<noteq> \<zero>; (rb \<plusminus> (q \<plusminus> qa) \<cdot>\<^sub>r g) \<cdot>\<^sub>r f \<plusminus> rc \<cdot>\<^sub>r g = h; q \<in> carrier R; qa \<in> carrier R; rb \<in> carrier R; rc \<in> carrier R; deg R S X rb < deg R S X g; deg R S X rc < deg R S X f; q \<cdot>\<^sub>r g \<in> carrier R; qa \<cdot>\<^sub>r f \<in> carrier R; rb \<plusminus> q \<cdot>\<^sub>r g \<in> carrier R; (rb \<plusminus> q \<cdot>\<^sub>r g) \<cdot>\<^sub>r f \<in> carrier R; qa \<cdot>\<^sub>r g \<cdot>\<^sub>r f \<in> carrier R; rc \<cdot>\<^sub>r g \<in> carrier R; qa \<cdot>\<^sub>r g \<in> carrier R; q \<plusminus> qa \<noteq> \<zero>\<rbrakk> \<Longrightarrow> rb \<plusminus> (q \<plusminus> qa) \<cdot>\<^sub>r g \<in> carrier R
[PROOF STEP]
apply (frule_tac y = "deg R S X (q \<plusminus> qa)" and z = "deg R S X rb" in
                                   aadd_le_mono[of "0"], simp add:aadd_0_l)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>q qa rb rc. \<lbrakk>Corps S; f \<in> carrier R; g \<in> carrier R; 0 < deg R S X f; 0 < deg R S X g; h \<in> carrier R; aGroup R; \<zero> \<in> carrier R; Subring R S; Ring S; f \<noteq> \<zero>; 0 \<le> deg R S X f; g \<noteq> \<zero>; 0 \<le> deg R S X g; Idomain R; Idomain S; g \<cdot>\<^sub>r f \<noteq> \<zero>; h \<noteq> \<zero>; (rb \<plusminus> (q \<plusminus> qa) \<cdot>\<^sub>r g) \<cdot>\<^sub>r f \<plusminus> rc \<cdot>\<^sub>r g = h; q \<in> carrier R; qa \<in> carrier R; rb \<in> carrier R; rc \<in> carrier R; deg R S X rb < deg R S X g; deg R S X rc < deg R S X f; q \<cdot>\<^sub>r g \<in> carrier R; qa \<cdot>\<^sub>r f \<in> carrier R; rb \<plusminus> q \<cdot>\<^sub>r g \<in> carrier R; (rb \<plusminus> q \<cdot>\<^sub>r g) \<cdot>\<^sub>r f \<in> carrier R; qa \<cdot>\<^sub>r g \<cdot>\<^sub>r f \<in> carrier R; rc \<cdot>\<^sub>r g \<in> carrier R; qa \<cdot>\<^sub>r g \<in> carrier R; 0 \<le> deg R S X (q \<plusminus> qa); rb \<plusminus> (q \<plusminus> qa) \<cdot>\<^sub>r g \<in> carrier R; q \<plusminus> qa \<in> carrier R; q \<plusminus> qa \<noteq> \<zero>; deg R S X rb \<le> deg R S X (q \<plusminus> qa) + deg R S X rb\<rbrakk> \<Longrightarrow> deg R S X rb < deg R S X (q \<plusminus> qa) + deg R S X g
 2. \<And>q qa rb rc. \<lbrakk>Corps S; f \<in> carrier R; g \<in> carrier R; 0 < deg R S X f; 0 < deg R S X g; h \<in> carrier R; aGroup R; \<zero> \<in> carrier R; Subring R S; Ring S; f \<noteq> \<zero>; 0 \<le> deg R S X f; g \<noteq> \<zero>; 0 \<le> deg R S X g; Idomain R; Idomain S; g \<cdot>\<^sub>r f \<noteq> \<zero>; h \<noteq> \<zero>; (rb \<plusminus> (q \<plusminus> qa) \<cdot>\<^sub>r g) \<cdot>\<^sub>r f \<plusminus> rc \<cdot>\<^sub>r g = h; q \<in> carrier R; qa \<in> carrier R; rb \<in> carrier R; rc \<in> carrier R; deg R S X rb < deg R S X g; deg R S X rc < deg R S X f; q \<cdot>\<^sub>r g \<in> carrier R; qa \<cdot>\<^sub>r f \<in> carrier R; rb \<plusminus> q \<cdot>\<^sub>r g \<in> carrier R; (rb \<plusminus> q \<cdot>\<^sub>r g) \<cdot>\<^sub>r f \<in> carrier R; qa \<cdot>\<^sub>r g \<cdot>\<^sub>r f \<in> carrier R; rc \<cdot>\<^sub>r g \<in> carrier R; qa \<cdot>\<^sub>r g \<in> carrier R; q \<plusminus> qa \<noteq> \<zero>; rb \<plusminus> (q \<plusminus> qa) \<cdot>\<^sub>r g \<in> carrier R; q \<plusminus> qa \<in> carrier R; deg R S X (rb \<plusminus> (q \<plusminus> qa) \<cdot>\<^sub>r g) = deg R S X ((q \<plusminus> qa) \<cdot>\<^sub>r g)\<rbrakk> \<Longrightarrow> deg R S X (rb \<plusminus> (q \<plusminus> qa) \<cdot>\<^sub>r g) \<le> amax (deg R S X h - deg R S X f) (deg R S X g)
 3. \<And>q qa rb rc. \<lbrakk>Corps S; f \<in> carrier R; g \<in> carrier R; 0 < deg R S X f; 0 < deg R S X g; h \<in> carrier R; aGroup R; \<zero> \<in> carrier R; Subring R S; Ring S; f \<noteq> \<zero>; 0 \<le> deg R S X f; g \<noteq> \<zero>; 0 \<le> deg R S X g; Idomain R; Idomain S; g \<cdot>\<^sub>r f \<noteq> \<zero>; h \<noteq> \<zero>; (rb \<plusminus> (q \<plusminus> qa) \<cdot>\<^sub>r g) \<cdot>\<^sub>r f \<plusminus> rc \<cdot>\<^sub>r g = h; q \<in> carrier R; qa \<in> carrier R; rb \<in> carrier R; rc \<in> carrier R; deg R S X rb < deg R S X g; deg R S X rc < deg R S X f; q \<cdot>\<^sub>r g \<in> carrier R; qa \<cdot>\<^sub>r f \<in> carrier R; rb \<plusminus> q \<cdot>\<^sub>r g \<in> carrier R; (rb \<plusminus> q \<cdot>\<^sub>r g) \<cdot>\<^sub>r f \<in> carrier R; qa \<cdot>\<^sub>r g \<cdot>\<^sub>r f \<in> carrier R; rc \<cdot>\<^sub>r g \<in> carrier R; qa \<cdot>\<^sub>r g \<in> carrier R; q \<plusminus> qa \<noteq> \<zero>\<rbrakk> \<Longrightarrow> rb \<plusminus> (q \<plusminus> qa) \<cdot>\<^sub>r g \<in> carrier R
[PROOF STEP]
apply (frule_tac p = "q \<plusminus> qa" in deg_ant_int, assumption+,
       frule_tac x = "deg R S X rb" and y = "deg R S X g" and
                 z = "int (deg_n R S X ( q \<plusminus> qa))" in aadd_less_mono_z,
       simp add:aadd_commute)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>q qa rb rc. \<lbrakk>Corps S; f \<in> carrier R; g \<in> carrier R; 0 < deg R S X f; 0 < deg R S X g; h \<in> carrier R; aGroup R; \<zero> \<in> carrier R; Subring R S; Ring S; f \<noteq> \<zero>; 0 \<le> deg R S X f; g \<noteq> \<zero>; 0 \<le> deg R S X g; Idomain R; Idomain S; g \<cdot>\<^sub>r f \<noteq> \<zero>; h \<noteq> \<zero>; (rb \<plusminus> (q \<plusminus> qa) \<cdot>\<^sub>r g) \<cdot>\<^sub>r f \<plusminus> rc \<cdot>\<^sub>r g = h; q \<in> carrier R; qa \<in> carrier R; rb \<in> carrier R; rc \<in> carrier R; deg R S X rb < deg R S X g; deg R S X rc < deg R S X f; q \<cdot>\<^sub>r g \<in> carrier R; qa \<cdot>\<^sub>r f \<in> carrier R; rb \<plusminus> q \<cdot>\<^sub>r g \<in> carrier R; (rb \<plusminus> q \<cdot>\<^sub>r g) \<cdot>\<^sub>r f \<in> carrier R; qa \<cdot>\<^sub>r g \<cdot>\<^sub>r f \<in> carrier R; rc \<cdot>\<^sub>r g \<in> carrier R; qa \<cdot>\<^sub>r g \<in> carrier R; q \<plusminus> qa \<noteq> \<zero>; rb \<plusminus> (q \<plusminus> qa) \<cdot>\<^sub>r g \<in> carrier R; q \<plusminus> qa \<in> carrier R; deg R S X (rb \<plusminus> (q \<plusminus> qa) \<cdot>\<^sub>r g) = deg R S X ((q \<plusminus> qa) \<cdot>\<^sub>r g)\<rbrakk> \<Longrightarrow> deg R S X (rb \<plusminus> (q \<plusminus> qa) \<cdot>\<^sub>r g) \<le> amax (deg R S X h - deg R S X f) (deg R S X g)
 2. \<And>q qa rb rc. \<lbrakk>Corps S; f \<in> carrier R; g \<in> carrier R; 0 < deg R S X f; 0 < deg R S X g; h \<in> carrier R; aGroup R; \<zero> \<in> carrier R; Subring R S; Ring S; f \<noteq> \<zero>; 0 \<le> deg R S X f; g \<noteq> \<zero>; 0 \<le> deg R S X g; Idomain R; Idomain S; g \<cdot>\<^sub>r f \<noteq> \<zero>; h \<noteq> \<zero>; (rb \<plusminus> (q \<plusminus> qa) \<cdot>\<^sub>r g) \<cdot>\<^sub>r f \<plusminus> rc \<cdot>\<^sub>r g = h; q \<in> carrier R; qa \<in> carrier R; rb \<in> carrier R; rc \<in> carrier R; deg R S X rb < deg R S X g; deg R S X rc < deg R S X f; q \<cdot>\<^sub>r g \<in> carrier R; qa \<cdot>\<^sub>r f \<in> carrier R; rb \<plusminus> q \<cdot>\<^sub>r g \<in> carrier R; (rb \<plusminus> q \<cdot>\<^sub>r g) \<cdot>\<^sub>r f \<in> carrier R; qa \<cdot>\<^sub>r g \<cdot>\<^sub>r f \<in> carrier R; rc \<cdot>\<^sub>r g \<in> carrier R; qa \<cdot>\<^sub>r g \<in> carrier R; q \<plusminus> qa \<noteq> \<zero>\<rbrakk> \<Longrightarrow> rb \<plusminus> (q \<plusminus> qa) \<cdot>\<^sub>r g \<in> carrier R
[PROOF STEP]
apply (simp add:deg_mult_pols1,
       frule_tac p = "rb \<plusminus> (q \<plusminus> qa) \<cdot>\<^sub>r g" and q = f in
            deg_mult_pols1, assumption+, simp,
       thin_tac "deg R S X (rb \<plusminus> (q \<plusminus> qa) \<cdot>\<^sub>r g) =
                       deg R S X (q \<plusminus> qa) + deg R S X g",
       frule_tac x = "rb \<plusminus> (q \<plusminus> qa) \<cdot>\<^sub>r g" and y = f in
       ring_tOp_closed,  assumption+, simp only:aGroup.ag_pOp_commute,
       frule_tac p = "rc \<cdot>\<^sub>r g" and q = "(rb \<plusminus> (q \<plusminus> qa) \<cdot>\<^sub>r g) \<cdot>\<^sub>r f" in
        deg_pols_add1, assumption+, simp,
       thin_tac "deg R S X ((rb \<plusminus> (q \<plusminus> qa) \<cdot>\<^sub>r g) \<cdot>\<^sub>r f) =
        deg R S X (q \<plusminus> qa) + deg R S X g + deg R S X f")
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>q qa rb rc. \<lbrakk>Corps S; f \<in> carrier R; g \<in> carrier R; 0 < deg R S X f; 0 < deg R S X g; h \<in> carrier R; aGroup R; \<zero> \<in> carrier R; Subring R S; Ring S; f \<noteq> \<zero>; 0 \<le> deg R S X f; g \<noteq> \<zero>; 0 \<le> deg R S X g; Idomain R; Idomain S; g \<cdot>\<^sub>r f \<noteq> \<zero>; h \<noteq> \<zero>; rc \<cdot>\<^sub>r g \<plusminus> (rb \<plusminus> (q \<plusminus> qa) \<cdot>\<^sub>r g) \<cdot>\<^sub>r f = h; q \<in> carrier R; qa \<in> carrier R; rb \<in> carrier R; rc \<in> carrier R; deg R S X rb < deg R S X g; deg R S X rc < deg R S X f; q \<cdot>\<^sub>r g \<in> carrier R; qa \<cdot>\<^sub>r f \<in> carrier R; rb \<plusminus> q \<cdot>\<^sub>r g \<in> carrier R; (rb \<plusminus> q \<cdot>\<^sub>r g) \<cdot>\<^sub>r f \<in> carrier R; qa \<cdot>\<^sub>r g \<cdot>\<^sub>r f \<in> carrier R; rc \<cdot>\<^sub>r g \<in> carrier R; qa \<cdot>\<^sub>r g \<in> carrier R; q \<plusminus> qa \<noteq> \<zero>; rb \<plusminus> (q \<plusminus> qa) \<cdot>\<^sub>r g \<in> carrier R; q \<plusminus> qa \<in> carrier R; (rb \<plusminus> (q \<plusminus> qa) \<cdot>\<^sub>r g) \<cdot>\<^sub>r f \<in> carrier R\<rbrakk> \<Longrightarrow> deg R S X (rc \<cdot>\<^sub>r g) < deg R S X (q \<plusminus> qa) + deg R S X g + deg R S X f
 2. \<And>q qa rb rc. \<lbrakk>Corps S; f \<in> carrier R; g \<in> carrier R; 0 < deg R S X f; 0 < deg R S X g; h \<in> carrier R; aGroup R; \<zero> \<in> carrier R; Subring R S; Ring S; f \<noteq> \<zero>; 0 \<le> deg R S X f; g \<noteq> \<zero>; 0 \<le> deg R S X g; Idomain R; Idomain S; g \<cdot>\<^sub>r f \<noteq> \<zero>; h \<noteq> \<zero>; rc \<cdot>\<^sub>r g \<plusminus> (rb \<plusminus> (q \<plusminus> qa) \<cdot>\<^sub>r g) \<cdot>\<^sub>r f = h; q \<in> carrier R; qa \<in> carrier R; rb \<in> carrier R; rc \<in> carrier R; deg R S X rb < deg R S X g; deg R S X rc < deg R S X f; q \<cdot>\<^sub>r g \<in> carrier R; qa \<cdot>\<^sub>r f \<in> carrier R; rb \<plusminus> q \<cdot>\<^sub>r g \<in> carrier R; (rb \<plusminus> q \<cdot>\<^sub>r g) \<cdot>\<^sub>r f \<in> carrier R; qa \<cdot>\<^sub>r g \<cdot>\<^sub>r f \<in> carrier R; rc \<cdot>\<^sub>r g \<in> carrier R; qa \<cdot>\<^sub>r g \<in> carrier R; q \<plusminus> qa \<noteq> \<zero>; rb \<plusminus> (q \<plusminus> qa) \<cdot>\<^sub>r g \<in> carrier R; q \<plusminus> qa \<in> carrier R; deg R S X ((rb \<plusminus> (q \<plusminus> qa) \<cdot>\<^sub>r g) \<cdot>\<^sub>r f) = deg R S X (q \<plusminus> qa) + deg R S X g + deg R S X f; (rb \<plusminus> (q \<plusminus> qa) \<cdot>\<^sub>r g) \<cdot>\<^sub>r f \<in> carrier R; deg R S X (rc \<cdot>\<^sub>r g \<plusminus> (rb \<plusminus> (q \<plusminus> qa) \<cdot>\<^sub>r g) \<cdot>\<^sub>r f) = deg R S X ((rb \<plusminus> (q \<plusminus> qa) \<cdot>\<^sub>r g) \<cdot>\<^sub>r f)\<rbrakk> \<Longrightarrow> deg R S X (q \<plusminus> qa) + deg R S X g \<le> amax (deg R S X h - deg R S X f) (deg R S X g)
 3. \<And>q qa rb rc. \<lbrakk>Corps S; f \<in> carrier R; g \<in> carrier R; 0 < deg R S X f; 0 < deg R S X g; h \<in> carrier R; aGroup R; \<zero> \<in> carrier R; Subring R S; Ring S; f \<noteq> \<zero>; 0 \<le> deg R S X f; g \<noteq> \<zero>; 0 \<le> deg R S X g; Idomain R; Idomain S; g \<cdot>\<^sub>r f \<noteq> \<zero>; h \<noteq> \<zero>; (rb \<plusminus> (q \<plusminus> qa) \<cdot>\<^sub>r g) \<cdot>\<^sub>r f \<plusminus> rc \<cdot>\<^sub>r g = h; q \<in> carrier R; qa \<in> carrier R; rb \<in> carrier R; rc \<in> carrier R; deg R S X rb < deg R S X g; deg R S X rc < deg R S X f; q \<cdot>\<^sub>r g \<in> carrier R; qa \<cdot>\<^sub>r f \<in> carrier R; rb \<plusminus> q \<cdot>\<^sub>r g \<in> carrier R; (rb \<plusminus> q \<cdot>\<^sub>r g) \<cdot>\<^sub>r f \<in> carrier R; qa \<cdot>\<^sub>r g \<cdot>\<^sub>r f \<in> carrier R; rc \<cdot>\<^sub>r g \<in> carrier R; qa \<cdot>\<^sub>r g \<in> carrier R; q \<plusminus> qa \<noteq> \<zero>\<rbrakk> \<Longrightarrow> rb \<plusminus> (q \<plusminus> qa) \<cdot>\<^sub>r g \<in> carrier R
[PROOF STEP]
apply (simp add:deg_mult_pols1,
       frule_tac p1 = "q \<plusminus> qa" in pol_nonzero[THEN sym], simp,
       simp add:deg_ant_int[of g])
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>q qa rb rc. \<lbrakk>Corps S; f \<in> carrier R; g \<in> carrier R; 0 < deg R S X f; 0 < deg_n R S X g; h \<in> carrier R; aGroup R; \<zero> \<in> carrier R; Subring R S; Ring S; f \<noteq> \<zero>; 0 \<le> deg R S X f; g \<noteq> \<zero>; 0 \<le> ant (int (deg_n R S X g)); Idomain R; Idomain S; g \<cdot>\<^sub>r f \<noteq> \<zero>; h \<noteq> \<zero>; rc \<cdot>\<^sub>r g \<plusminus> (rb \<plusminus> (q \<plusminus> qa) \<cdot>\<^sub>r g) \<cdot>\<^sub>r f = h; q \<in> carrier R; qa \<in> carrier R; rb \<in> carrier R; rc \<in> carrier R; deg R S X rb < ant (int (deg_n R S X g)); deg R S X rc < deg R S X f; q \<cdot>\<^sub>r g \<in> carrier R; qa \<cdot>\<^sub>r f \<in> carrier R; rb \<plusminus> q \<cdot>\<^sub>r g \<in> carrier R; (rb \<plusminus> q \<cdot>\<^sub>r g) \<cdot>\<^sub>r f \<in> carrier R; qa \<cdot>\<^sub>r g \<cdot>\<^sub>r f \<in> carrier R; rc \<cdot>\<^sub>r g \<in> carrier R; qa \<cdot>\<^sub>r g \<in> carrier R; 0 \<le> deg R S X (q \<plusminus> qa); rb \<plusminus> (q \<plusminus> qa) \<cdot>\<^sub>r g \<in> carrier R; q \<plusminus> qa \<in> carrier R; (rb \<plusminus> (q \<plusminus> qa) \<cdot>\<^sub>r g) \<cdot>\<^sub>r f \<in> carrier R; q \<plusminus> qa \<noteq> \<zero>\<rbrakk> \<Longrightarrow> deg R S X rc + ant (int (deg_n R S X g)) < deg R S X (q \<plusminus> qa) + ant (int (deg_n R S X g)) + deg R S X f
 2. \<And>q qa rb rc. \<lbrakk>Corps S; f \<in> carrier R; g \<in> carrier R; 0 < deg R S X f; 0 < deg R S X g; h \<in> carrier R; aGroup R; \<zero> \<in> carrier R; Subring R S; Ring S; f \<noteq> \<zero>; 0 \<le> deg R S X f; g \<noteq> \<zero>; 0 \<le> deg R S X g; Idomain R; Idomain S; g \<cdot>\<^sub>r f \<noteq> \<zero>; h \<noteq> \<zero>; rc \<cdot>\<^sub>r g \<plusminus> (rb \<plusminus> (q \<plusminus> qa) \<cdot>\<^sub>r g) \<cdot>\<^sub>r f = h; q \<in> carrier R; qa \<in> carrier R; rb \<in> carrier R; rc \<in> carrier R; deg R S X rb < deg R S X g; deg R S X rc < deg R S X f; q \<cdot>\<^sub>r g \<in> carrier R; qa \<cdot>\<^sub>r f \<in> carrier R; rb \<plusminus> q \<cdot>\<^sub>r g \<in> carrier R; (rb \<plusminus> q \<cdot>\<^sub>r g) \<cdot>\<^sub>r f \<in> carrier R; qa \<cdot>\<^sub>r g \<cdot>\<^sub>r f \<in> carrier R; rc \<cdot>\<^sub>r g \<in> carrier R; qa \<cdot>\<^sub>r g \<in> carrier R; q \<plusminus> qa \<noteq> \<zero>; rb \<plusminus> (q \<plusminus> qa) \<cdot>\<^sub>r g \<in> carrier R; q \<plusminus> qa \<in> carrier R; deg R S X ((rb \<plusminus> (q \<plusminus> qa) \<cdot>\<^sub>r g) \<cdot>\<^sub>r f) = deg R S X (q \<plusminus> qa) + deg R S X g + deg R S X f; (rb \<plusminus> (q \<plusminus> qa) \<cdot>\<^sub>r g) \<cdot>\<^sub>r f \<in> carrier R; deg R S X (rc \<cdot>\<^sub>r g \<plusminus> (rb \<plusminus> (q \<plusminus> qa) \<cdot>\<^sub>r g) \<cdot>\<^sub>r f) = deg R S X ((rb \<plusminus> (q \<plusminus> qa) \<cdot>\<^sub>r g) \<cdot>\<^sub>r f)\<rbrakk> \<Longrightarrow> deg R S X (q \<plusminus> qa) + deg R S X g \<le> amax (deg R S X h - deg R S X f) (deg R S X g)
 3. \<And>q qa rb rc. \<lbrakk>Corps S; f \<in> carrier R; g \<in> carrier R; 0 < deg R S X f; 0 < deg R S X g; h \<in> carrier R; aGroup R; \<zero> \<in> carrier R; Subring R S; Ring S; f \<noteq> \<zero>; 0 \<le> deg R S X f; g \<noteq> \<zero>; 0 \<le> deg R S X g; Idomain R; Idomain S; g \<cdot>\<^sub>r f \<noteq> \<zero>; h \<noteq> \<zero>; (rb \<plusminus> (q \<plusminus> qa) \<cdot>\<^sub>r g) \<cdot>\<^sub>r f \<plusminus> rc \<cdot>\<^sub>r g = h; q \<in> carrier R; qa \<in> carrier R; rb \<in> carrier R; rc \<in> carrier R; deg R S X rb < deg R S X g; deg R S X rc < deg R S X f; q \<cdot>\<^sub>r g \<in> carrier R; qa \<cdot>\<^sub>r f \<in> carrier R; rb \<plusminus> q \<cdot>\<^sub>r g \<in> carrier R; (rb \<plusminus> q \<cdot>\<^sub>r g) \<cdot>\<^sub>r f \<in> carrier R; qa \<cdot>\<^sub>r g \<cdot>\<^sub>r f \<in> carrier R; rc \<cdot>\<^sub>r g \<in> carrier R; qa \<cdot>\<^sub>r g \<in> carrier R; q \<plusminus> qa \<noteq> \<zero>\<rbrakk> \<Longrightarrow> rb \<plusminus> (q \<plusminus> qa) \<cdot>\<^sub>r g \<in> carrier R
[PROOF STEP]
apply (frule_tac x = "deg R S X rc" and y = "deg R S X f" and
        z = "int (deg_n R S X g)" in aadd_less_mono_z,
       frule_tac a = "deg R S X ( q \<plusminus> qa)" in aadd_pos_le[of _
                   "deg R S X f + ant (int (deg_n R S X g))"],
       frule_tac x = "deg R S X rc + ant (int (deg_n R S X g))" and
        y = "deg R S X f + ant (int (deg_n R S X g))" and
        z = "deg R S X ( q \<plusminus> qa) + (deg R S X f + ant (int (deg_n R S X g)))"
       in aless_le_trans, assumption+,
       thin_tac "deg R S X rc + ant (int (deg_n R S X g))
                       < deg R S X f + ant (int (deg_n R S X g))",
       thin_tac "deg R S X f + ant (int (deg_n R S X g))
           \<le> deg R S X ( q \<plusminus> qa) + (deg R S X f + ant (int (deg_n R S X g)))")
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>q qa rb rc. \<lbrakk>Corps S; f \<in> carrier R; g \<in> carrier R; 0 < deg R S X f; 0 < deg_n R S X g; h \<in> carrier R; aGroup R; \<zero> \<in> carrier R; Subring R S; Ring S; f \<noteq> \<zero>; 0 \<le> deg R S X f; g \<noteq> \<zero>; 0 \<le> ant (int (deg_n R S X g)); Idomain R; Idomain S; g \<cdot>\<^sub>r f \<noteq> \<zero>; h \<noteq> \<zero>; rc \<cdot>\<^sub>r g \<plusminus> (rb \<plusminus> (q \<plusminus> qa) \<cdot>\<^sub>r g) \<cdot>\<^sub>r f = h; q \<in> carrier R; qa \<in> carrier R; rb \<in> carrier R; rc \<in> carrier R; deg R S X rb < ant (int (deg_n R S X g)); deg R S X rc < deg R S X f; q \<cdot>\<^sub>r g \<in> carrier R; qa \<cdot>\<^sub>r f \<in> carrier R; rb \<plusminus> q \<cdot>\<^sub>r g \<in> carrier R; (rb \<plusminus> q \<cdot>\<^sub>r g) \<cdot>\<^sub>r f \<in> carrier R; qa \<cdot>\<^sub>r g \<cdot>\<^sub>r f \<in> carrier R; rc \<cdot>\<^sub>r g \<in> carrier R; qa \<cdot>\<^sub>r g \<in> carrier R; 0 \<le> deg R S X (q \<plusminus> qa); rb \<plusminus> (q \<plusminus> qa) \<cdot>\<^sub>r g \<in> carrier R; q \<plusminus> qa \<in> carrier R; (rb \<plusminus> (q \<plusminus> qa) \<cdot>\<^sub>r g) \<cdot>\<^sub>r f \<in> carrier R; q \<plusminus> qa \<noteq> \<zero>; deg R S X rc + ant (int (deg_n R S X g)) < deg R S X (q \<plusminus> qa) + (deg R S X f + ant (int (deg_n R S X g)))\<rbrakk> \<Longrightarrow> deg R S X rc + ant (int (deg_n R S X g)) < deg R S X (q \<plusminus> qa) + ant (int (deg_n R S X g)) + deg R S X f
 2. \<And>q qa rb rc. \<lbrakk>Corps S; f \<in> carrier R; g \<in> carrier R; 0 < deg R S X f; 0 < deg R S X g; h \<in> carrier R; aGroup R; \<zero> \<in> carrier R; Subring R S; Ring S; f \<noteq> \<zero>; 0 \<le> deg R S X f; g \<noteq> \<zero>; 0 \<le> deg R S X g; Idomain R; Idomain S; g \<cdot>\<^sub>r f \<noteq> \<zero>; h \<noteq> \<zero>; rc \<cdot>\<^sub>r g \<plusminus> (rb \<plusminus> (q \<plusminus> qa) \<cdot>\<^sub>r g) \<cdot>\<^sub>r f = h; q \<in> carrier R; qa \<in> carrier R; rb \<in> carrier R; rc \<in> carrier R; deg R S X rb < deg R S X g; deg R S X rc < deg R S X f; q \<cdot>\<^sub>r g \<in> carrier R; qa \<cdot>\<^sub>r f \<in> carrier R; rb \<plusminus> q \<cdot>\<^sub>r g \<in> carrier R; (rb \<plusminus> q \<cdot>\<^sub>r g) \<cdot>\<^sub>r f \<in> carrier R; qa \<cdot>\<^sub>r g \<cdot>\<^sub>r f \<in> carrier R; rc \<cdot>\<^sub>r g \<in> carrier R; qa \<cdot>\<^sub>r g \<in> carrier R; q \<plusminus> qa \<noteq> \<zero>; rb \<plusminus> (q \<plusminus> qa) \<cdot>\<^sub>r g \<in> carrier R; q \<plusminus> qa \<in> carrier R; deg R S X ((rb \<plusminus> (q \<plusminus> qa) \<cdot>\<^sub>r g) \<cdot>\<^sub>r f) = deg R S X (q \<plusminus> qa) + deg R S X g + deg R S X f; (rb \<plusminus> (q \<plusminus> qa) \<cdot>\<^sub>r g) \<cdot>\<^sub>r f \<in> carrier R; deg R S X (rc \<cdot>\<^sub>r g \<plusminus> (rb \<plusminus> (q \<plusminus> qa) \<cdot>\<^sub>r g) \<cdot>\<^sub>r f) = deg R S X ((rb \<plusminus> (q \<plusminus> qa) \<cdot>\<^sub>r g) \<cdot>\<^sub>r f)\<rbrakk> \<Longrightarrow> deg R S X (q \<plusminus> qa) + deg R S X g \<le> amax (deg R S X h - deg R S X f) (deg R S X g)
 3. \<And>q qa rb rc. \<lbrakk>Corps S; f \<in> carrier R; g \<in> carrier R; 0 < deg R S X f; 0 < deg R S X g; h \<in> carrier R; aGroup R; \<zero> \<in> carrier R; Subring R S; Ring S; f \<noteq> \<zero>; 0 \<le> deg R S X f; g \<noteq> \<zero>; 0 \<le> deg R S X g; Idomain R; Idomain S; g \<cdot>\<^sub>r f \<noteq> \<zero>; h \<noteq> \<zero>; (rb \<plusminus> (q \<plusminus> qa) \<cdot>\<^sub>r g) \<cdot>\<^sub>r f \<plusminus> rc \<cdot>\<^sub>r g = h; q \<in> carrier R; qa \<in> carrier R; rb \<in> carrier R; rc \<in> carrier R; deg R S X rb < deg R S X g; deg R S X rc < deg R S X f; q \<cdot>\<^sub>r g \<in> carrier R; qa \<cdot>\<^sub>r f \<in> carrier R; rb \<plusminus> q \<cdot>\<^sub>r g \<in> carrier R; (rb \<plusminus> q \<cdot>\<^sub>r g) \<cdot>\<^sub>r f \<in> carrier R; qa \<cdot>\<^sub>r g \<cdot>\<^sub>r f \<in> carrier R; rc \<cdot>\<^sub>r g \<in> carrier R; qa \<cdot>\<^sub>r g \<in> carrier R; q \<plusminus> qa \<noteq> \<zero>\<rbrakk> \<Longrightarrow> rb \<plusminus> (q \<plusminus> qa) \<cdot>\<^sub>r g \<in> carrier R
[PROOF STEP]
apply (simp add:deg_ant_int[THEN sym])
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>q qa rb rc. \<lbrakk>Corps S; f \<in> carrier R; g \<in> carrier R; 0 < deg R S X f; 0 < deg_n R S X g; h \<in> carrier R; aGroup R; \<zero> \<in> carrier R; Subring R S; Ring S; f \<noteq> \<zero>; 0 \<le> deg R S X f; g \<noteq> \<zero>; 0 \<le> deg R S X g; Idomain R; Idomain S; g \<cdot>\<^sub>r f \<noteq> \<zero>; h \<noteq> \<zero>; rc \<cdot>\<^sub>r g \<plusminus> (rb \<plusminus> (q \<plusminus> qa) \<cdot>\<^sub>r g) \<cdot>\<^sub>r f = h; q \<in> carrier R; qa \<in> carrier R; rb \<in> carrier R; rc \<in> carrier R; deg R S X rb < deg R S X g; deg R S X rc < deg R S X f; q \<cdot>\<^sub>r g \<in> carrier R; qa \<cdot>\<^sub>r f \<in> carrier R; rb \<plusminus> q \<cdot>\<^sub>r g \<in> carrier R; (rb \<plusminus> q \<cdot>\<^sub>r g) \<cdot>\<^sub>r f \<in> carrier R; qa \<cdot>\<^sub>r g \<cdot>\<^sub>r f \<in> carrier R; rc \<cdot>\<^sub>r g \<in> carrier R; qa \<cdot>\<^sub>r g \<in> carrier R; 0 \<le> deg R S X (q \<plusminus> qa); rb \<plusminus> (q \<plusminus> qa) \<cdot>\<^sub>r g \<in> carrier R; q \<plusminus> qa \<in> carrier R; (rb \<plusminus> (q \<plusminus> qa) \<cdot>\<^sub>r g) \<cdot>\<^sub>r f \<in> carrier R; q \<plusminus> qa \<noteq> \<zero>; deg R S X rc + deg R S X g < deg R S X (q \<plusminus> qa) + (deg R S X f + deg R S X g)\<rbrakk> \<Longrightarrow> deg R S X rc + deg R S X g < deg R S X (q \<plusminus> qa) + deg R S X g + deg R S X f
 2. \<And>q qa rb rc. \<lbrakk>Corps S; f \<in> carrier R; g \<in> carrier R; 0 < deg R S X f; 0 < deg R S X g; h \<in> carrier R; aGroup R; \<zero> \<in> carrier R; Subring R S; Ring S; f \<noteq> \<zero>; 0 \<le> deg R S X f; g \<noteq> \<zero>; 0 \<le> deg R S X g; Idomain R; Idomain S; g \<cdot>\<^sub>r f \<noteq> \<zero>; h \<noteq> \<zero>; rc \<cdot>\<^sub>r g \<plusminus> (rb \<plusminus> (q \<plusminus> qa) \<cdot>\<^sub>r g) \<cdot>\<^sub>r f = h; q \<in> carrier R; qa \<in> carrier R; rb \<in> carrier R; rc \<in> carrier R; deg R S X rb < deg R S X g; deg R S X rc < deg R S X f; q \<cdot>\<^sub>r g \<in> carrier R; qa \<cdot>\<^sub>r f \<in> carrier R; rb \<plusminus> q \<cdot>\<^sub>r g \<in> carrier R; (rb \<plusminus> q \<cdot>\<^sub>r g) \<cdot>\<^sub>r f \<in> carrier R; qa \<cdot>\<^sub>r g \<cdot>\<^sub>r f \<in> carrier R; rc \<cdot>\<^sub>r g \<in> carrier R; qa \<cdot>\<^sub>r g \<in> carrier R; q \<plusminus> qa \<noteq> \<zero>; rb \<plusminus> (q \<plusminus> qa) \<cdot>\<^sub>r g \<in> carrier R; q \<plusminus> qa \<in> carrier R; deg R S X ((rb \<plusminus> (q \<plusminus> qa) \<cdot>\<^sub>r g) \<cdot>\<^sub>r f) = deg R S X (q \<plusminus> qa) + deg R S X g + deg R S X f; (rb \<plusminus> (q \<plusminus> qa) \<cdot>\<^sub>r g) \<cdot>\<^sub>r f \<in> carrier R; deg R S X (rc \<cdot>\<^sub>r g \<plusminus> (rb \<plusminus> (q \<plusminus> qa) \<cdot>\<^sub>r g) \<cdot>\<^sub>r f) = deg R S X ((rb \<plusminus> (q \<plusminus> qa) \<cdot>\<^sub>r g) \<cdot>\<^sub>r f)\<rbrakk> \<Longrightarrow> deg R S X (q \<plusminus> qa) + deg R S X g \<le> amax (deg R S X h - deg R S X f) (deg R S X g)
 3. \<And>q qa rb rc. \<lbrakk>Corps S; f \<in> carrier R; g \<in> carrier R; 0 < deg R S X f; 0 < deg R S X g; h \<in> carrier R; aGroup R; \<zero> \<in> carrier R; Subring R S; Ring S; f \<noteq> \<zero>; 0 \<le> deg R S X f; g \<noteq> \<zero>; 0 \<le> deg R S X g; Idomain R; Idomain S; g \<cdot>\<^sub>r f \<noteq> \<zero>; h \<noteq> \<zero>; (rb \<plusminus> (q \<plusminus> qa) \<cdot>\<^sub>r g) \<cdot>\<^sub>r f \<plusminus> rc \<cdot>\<^sub>r g = h; q \<in> carrier R; qa \<in> carrier R; rb \<in> carrier R; rc \<in> carrier R; deg R S X rb < deg R S X g; deg R S X rc < deg R S X f; q \<cdot>\<^sub>r g \<in> carrier R; qa \<cdot>\<^sub>r f \<in> carrier R; rb \<plusminus> q \<cdot>\<^sub>r g \<in> carrier R; (rb \<plusminus> q \<cdot>\<^sub>r g) \<cdot>\<^sub>r f \<in> carrier R; qa \<cdot>\<^sub>r g \<cdot>\<^sub>r f \<in> carrier R; rc \<cdot>\<^sub>r g \<in> carrier R; qa \<cdot>\<^sub>r g \<in> carrier R; q \<plusminus> qa \<noteq> \<zero>\<rbrakk> \<Longrightarrow> rb \<plusminus> (q \<plusminus> qa) \<cdot>\<^sub>r g \<in> carrier R
[PROOF STEP]
apply (frule_tac p = "q \<plusminus> qa" in deg_in_aug_minf,
        frule_tac p = "g" in deg_in_aug_minf,
        frule_tac p = "f" in deg_in_aug_minf,
        simp add:aadd_commute[of "deg R S X f" "deg R S X g"],
        simp only:aadd_assoc_m[THEN sym], simp)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>q qa rb rc. \<lbrakk>Corps S; f \<in> carrier R; g \<in> carrier R; 0 < deg R S X f; 0 < deg R S X g; h \<in> carrier R; aGroup R; \<zero> \<in> carrier R; Subring R S; Ring S; f \<noteq> \<zero>; 0 \<le> deg R S X f; g \<noteq> \<zero>; 0 \<le> deg R S X g; Idomain R; Idomain S; g \<cdot>\<^sub>r f \<noteq> \<zero>; h \<noteq> \<zero>; rc \<cdot>\<^sub>r g \<plusminus> (rb \<plusminus> (q \<plusminus> qa) \<cdot>\<^sub>r g) \<cdot>\<^sub>r f = h; q \<in> carrier R; qa \<in> carrier R; rb \<in> carrier R; rc \<in> carrier R; deg R S X rb < deg R S X g; deg R S X rc < deg R S X f; q \<cdot>\<^sub>r g \<in> carrier R; qa \<cdot>\<^sub>r f \<in> carrier R; rb \<plusminus> q \<cdot>\<^sub>r g \<in> carrier R; (rb \<plusminus> q \<cdot>\<^sub>r g) \<cdot>\<^sub>r f \<in> carrier R; qa \<cdot>\<^sub>r g \<cdot>\<^sub>r f \<in> carrier R; rc \<cdot>\<^sub>r g \<in> carrier R; qa \<cdot>\<^sub>r g \<in> carrier R; q \<plusminus> qa \<noteq> \<zero>; rb \<plusminus> (q \<plusminus> qa) \<cdot>\<^sub>r g \<in> carrier R; q \<plusminus> qa \<in> carrier R; deg R S X ((rb \<plusminus> (q \<plusminus> qa) \<cdot>\<^sub>r g) \<cdot>\<^sub>r f) = deg R S X (q \<plusminus> qa) + deg R S X g + deg R S X f; (rb \<plusminus> (q \<plusminus> qa) \<cdot>\<^sub>r g) \<cdot>\<^sub>r f \<in> carrier R; deg R S X h = deg R S X (q \<plusminus> qa) + deg R S X g + deg R S X f\<rbrakk> \<Longrightarrow> deg R S X (q \<plusminus> qa) + deg R S X g \<le> amax (deg R S X (q \<plusminus> qa) + deg R S X g + deg R S X f - deg R S X f) (deg R S X g)
 2. \<And>q qa rb rc. \<lbrakk>Corps S; f \<in> carrier R; g \<in> carrier R; 0 < deg R S X f; 0 < deg R S X g; h \<in> carrier R; aGroup R; \<zero> \<in> carrier R; Subring R S; Ring S; f \<noteq> \<zero>; 0 \<le> deg R S X f; g \<noteq> \<zero>; 0 \<le> deg R S X g; Idomain R; Idomain S; g \<cdot>\<^sub>r f \<noteq> \<zero>; h \<noteq> \<zero>; (rb \<plusminus> (q \<plusminus> qa) \<cdot>\<^sub>r g) \<cdot>\<^sub>r f \<plusminus> rc \<cdot>\<^sub>r g = h; q \<in> carrier R; qa \<in> carrier R; rb \<in> carrier R; rc \<in> carrier R; deg R S X rb < deg R S X g; deg R S X rc < deg R S X f; q \<cdot>\<^sub>r g \<in> carrier R; qa \<cdot>\<^sub>r f \<in> carrier R; rb \<plusminus> q \<cdot>\<^sub>r g \<in> carrier R; (rb \<plusminus> q \<cdot>\<^sub>r g) \<cdot>\<^sub>r f \<in> carrier R; qa \<cdot>\<^sub>r g \<cdot>\<^sub>r f \<in> carrier R; rc \<cdot>\<^sub>r g \<in> carrier R; qa \<cdot>\<^sub>r g \<in> carrier R; q \<plusminus> qa \<noteq> \<zero>\<rbrakk> \<Longrightarrow> rb \<plusminus> (q \<plusminus> qa) \<cdot>\<^sub>r g \<in> carrier R
[PROOF STEP]
apply (frule_tac p = "g" in deg_in_aug_minf,
        frule_tac p = "f" in deg_in_aug_minf,
        frule_tac p = "q \<plusminus> qa" in deg_in_aug_minf,
        simp add:diff_ant_def,
        subgoal_tac "-(deg R S X f) \<in> Z\<^sub>-\<^sub>\<infinity>")
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>q qa rb rc. \<lbrakk>Corps S; f \<in> carrier R; g \<in> carrier R; 0 < deg R S X f; 0 < deg R S X g; h \<in> carrier R; aGroup R; \<zero> \<in> carrier R; Subring R S; Ring S; f \<noteq> \<zero>; 0 \<le> deg R S X f; g \<noteq> \<zero>; 0 \<le> deg R S X g; Idomain R; Idomain S; g \<cdot>\<^sub>r f \<noteq> \<zero>; h \<noteq> \<zero>; rc \<cdot>\<^sub>r g \<plusminus> (rb \<plusminus> (q \<plusminus> qa) \<cdot>\<^sub>r g) \<cdot>\<^sub>r f = h; q \<in> carrier R; qa \<in> carrier R; rb \<in> carrier R; rc \<in> carrier R; deg R S X rb < deg R S X g; deg R S X rc < deg R S X f; q \<cdot>\<^sub>r g \<in> carrier R; qa \<cdot>\<^sub>r f \<in> carrier R; rb \<plusminus> q \<cdot>\<^sub>r g \<in> carrier R; (rb \<plusminus> q \<cdot>\<^sub>r g) \<cdot>\<^sub>r f \<in> carrier R; qa \<cdot>\<^sub>r g \<cdot>\<^sub>r f \<in> carrier R; rc \<cdot>\<^sub>r g \<in> carrier R; qa \<cdot>\<^sub>r g \<in> carrier R; q \<plusminus> qa \<noteq> \<zero>; rb \<plusminus> (q \<plusminus> qa) \<cdot>\<^sub>r g \<in> carrier R; q \<plusminus> qa \<in> carrier R; deg R S X ((rb \<plusminus> (q \<plusminus> qa) \<cdot>\<^sub>r g) \<cdot>\<^sub>r f) = deg R S X (q \<plusminus> qa) + deg R S X g + deg R S X f; (rb \<plusminus> (q \<plusminus> qa) \<cdot>\<^sub>r g) \<cdot>\<^sub>r f \<in> carrier R; deg R S X h = deg R S X (q \<plusminus> qa) + deg R S X g + deg R S X f; deg R S X g \<in> Z\<^sub>-\<^sub>\<infinity>; deg R S X f \<in> Z\<^sub>-\<^sub>\<infinity>; deg R S X (q \<plusminus> qa) \<in> Z\<^sub>-\<^sub>\<infinity>; - deg R S X f \<in> Z\<^sub>-\<^sub>\<infinity>\<rbrakk> \<Longrightarrow> deg R S X (q \<plusminus> qa) + deg R S X g \<le> amax (deg R S X (q \<plusminus> qa) + deg R S X g + deg R S X f + - deg R S X f) (deg R S X g)
 2. \<And>q qa rb rc. \<lbrakk>Corps S; f \<in> carrier R; g \<in> carrier R; 0 < deg R S X f; 0 < deg R S X g; h \<in> carrier R; aGroup R; \<zero> \<in> carrier R; Subring R S; Ring S; f \<noteq> \<zero>; 0 \<le> deg R S X f; g \<noteq> \<zero>; 0 \<le> deg R S X g; Idomain R; Idomain S; g \<cdot>\<^sub>r f \<noteq> \<zero>; h \<noteq> \<zero>; rc \<cdot>\<^sub>r g \<plusminus> (rb \<plusminus> (q \<plusminus> qa) \<cdot>\<^sub>r g) \<cdot>\<^sub>r f = h; q \<in> carrier R; qa \<in> carrier R; rb \<in> carrier R; rc \<in> carrier R; deg R S X rb < deg R S X g; deg R S X rc < deg R S X f; q \<cdot>\<^sub>r g \<in> carrier R; qa \<cdot>\<^sub>r f \<in> carrier R; rb \<plusminus> q \<cdot>\<^sub>r g \<in> carrier R; (rb \<plusminus> q \<cdot>\<^sub>r g) \<cdot>\<^sub>r f \<in> carrier R; qa \<cdot>\<^sub>r g \<cdot>\<^sub>r f \<in> carrier R; rc \<cdot>\<^sub>r g \<in> carrier R; qa \<cdot>\<^sub>r g \<in> carrier R; q \<plusminus> qa \<noteq> \<zero>; rb \<plusminus> (q \<plusminus> qa) \<cdot>\<^sub>r g \<in> carrier R; q \<plusminus> qa \<in> carrier R; deg R S X ((rb \<plusminus> (q \<plusminus> qa) \<cdot>\<^sub>r g) \<cdot>\<^sub>r f) = deg R S X (q \<plusminus> qa) + deg R S X g + deg R S X f; (rb \<plusminus> (q \<plusminus> qa) \<cdot>\<^sub>r g) \<cdot>\<^sub>r f \<in> carrier R; deg R S X h = deg R S X (q \<plusminus> qa) + deg R S X g + deg R S X f; deg R S X g \<in> Z\<^sub>-\<^sub>\<infinity>; deg R S X f \<in> Z\<^sub>-\<^sub>\<infinity>; deg R S X (q \<plusminus> qa) \<in> Z\<^sub>-\<^sub>\<infinity>\<rbrakk> \<Longrightarrow> - deg R S X f \<in> Z\<^sub>-\<^sub>\<infinity>
 3. \<And>q qa rb rc. \<lbrakk>Corps S; f \<in> carrier R; g \<in> carrier R; 0 < deg R S X f; 0 < deg R S X g; h \<in> carrier R; aGroup R; \<zero> \<in> carrier R; Subring R S; Ring S; f \<noteq> \<zero>; 0 \<le> deg R S X f; g \<noteq> \<zero>; 0 \<le> deg R S X g; Idomain R; Idomain S; g \<cdot>\<^sub>r f \<noteq> \<zero>; h \<noteq> \<zero>; (rb \<plusminus> (q \<plusminus> qa) \<cdot>\<^sub>r g) \<cdot>\<^sub>r f \<plusminus> rc \<cdot>\<^sub>r g = h; q \<in> carrier R; qa \<in> carrier R; rb \<in> carrier R; rc \<in> carrier R; deg R S X rb < deg R S X g; deg R S X rc < deg R S X f; q \<cdot>\<^sub>r g \<in> carrier R; qa \<cdot>\<^sub>r f \<in> carrier R; rb \<plusminus> q \<cdot>\<^sub>r g \<in> carrier R; (rb \<plusminus> q \<cdot>\<^sub>r g) \<cdot>\<^sub>r f \<in> carrier R; qa \<cdot>\<^sub>r g \<cdot>\<^sub>r f \<in> carrier R; rc \<cdot>\<^sub>r g \<in> carrier R; qa \<cdot>\<^sub>r g \<in> carrier R; q \<plusminus> qa \<noteq> \<zero>\<rbrakk> \<Longrightarrow> rb \<plusminus> (q \<plusminus> qa) \<cdot>\<^sub>r g \<in> carrier R
[PROOF STEP]
apply (subst aadd_assoc_m[of _ "deg R S X f" "- deg R S X f"],
       simp add:Zminf_pOp_closed, assumption+,
       (simp add:aadd_minus_r, simp add:aadd_0_r), simp add:amax_ge_l,
       simp add:deg_ant_int, simp add:aminus, simp add:z_in_aug_minf)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>q qa rb rc. \<lbrakk>Corps S; f \<in> carrier R; g \<in> carrier R; 0 < deg R S X f; 0 < deg R S X g; h \<in> carrier R; aGroup R; \<zero> \<in> carrier R; Subring R S; Ring S; f \<noteq> \<zero>; 0 \<le> deg R S X f; g \<noteq> \<zero>; 0 \<le> deg R S X g; Idomain R; Idomain S; g \<cdot>\<^sub>r f \<noteq> \<zero>; h \<noteq> \<zero>; (rb \<plusminus> (q \<plusminus> qa) \<cdot>\<^sub>r g) \<cdot>\<^sub>r f \<plusminus> rc \<cdot>\<^sub>r g = h; q \<in> carrier R; qa \<in> carrier R; rb \<in> carrier R; rc \<in> carrier R; deg R S X rb < deg R S X g; deg R S X rc < deg R S X f; q \<cdot>\<^sub>r g \<in> carrier R; qa \<cdot>\<^sub>r f \<in> carrier R; rb \<plusminus> q \<cdot>\<^sub>r g \<in> carrier R; (rb \<plusminus> q \<cdot>\<^sub>r g) \<cdot>\<^sub>r f \<in> carrier R; qa \<cdot>\<^sub>r g \<cdot>\<^sub>r f \<in> carrier R; rc \<cdot>\<^sub>r g \<in> carrier R; qa \<cdot>\<^sub>r g \<in> carrier R; q \<plusminus> qa \<noteq> \<zero>\<rbrakk> \<Longrightarrow> rb \<plusminus> (q \<plusminus> qa) \<cdot>\<^sub>r g \<in> carrier R
[PROOF STEP]
apply (rule aGroup.ag_pOp_closed, assumption+,
        rule ring_tOp_closed,
        rule aGroup.ag_pOp_closed, assumption+)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma (in PolynRg) P_mod_whole:"p \<in> carrier R \<Longrightarrow>
                         P_mod R S X (carrier S) p"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. p \<in> carrier R \<Longrightarrow> P_mod R S X (carrier S) p
[PROOF STEP]
apply (case_tac "p = \<zero>\<^bsub>R\<^esub>", simp add:P_mod_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>p \<in> carrier R; p \<noteq> \<zero>\<rbrakk> \<Longrightarrow> P_mod R S X (carrier S) p
[PROOF STEP]
apply (simp add:P_mod_def,
       rule allI, rule impI,
       rule pol_coeff_mem,
       simp add:s_cf_pol_coeff,
       assumption)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma (in PolynRg) zero_P_mod:"ideal S I \<Longrightarrow> P_mod R S X I \<zero>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ideal S I \<Longrightarrow> P_mod R S X I \<zero>
[PROOF STEP]
by (simp add:P_mod_def)


[STATEMENT]
lemma (in PolynRg) P_mod_mod:"\<lbrakk>ideal S I; p \<in> carrier R; pol_coeff S c;
                     p = polyn_expr R X (fst c) c\<rbrakk> \<Longrightarrow>
                     (\<forall>j \<le> (fst c). (snd c) j \<in> I) = (P_mod R S X I p)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ideal S I; p \<in> carrier R; pol_coeff S c; p = polyn_expr R X (fst c) c\<rbrakk> \<Longrightarrow> (\<forall>j\<le>fst c. snd c j \<in> I) = P_mod R S X I p
[PROOF STEP]
apply (cut_tac subring, frule subring_Ring)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ideal S I; p \<in> carrier R; pol_coeff S c; p = polyn_expr R X (fst c) c; Subring R S; Ring S\<rbrakk> \<Longrightarrow> (\<forall>j\<le>fst c. snd c j \<in> I) = P_mod R S X I p
[PROOF STEP]
apply (case_tac "p = \<zero>\<^bsub>R\<^esub>")
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>ideal S I; p \<in> carrier R; pol_coeff S c; p = polyn_expr R X (fst c) c; Subring R S; Ring S; p = \<zero>\<rbrakk> \<Longrightarrow> (\<forall>j\<le>fst c. snd c j \<in> I) = P_mod R S X I p
 2. \<lbrakk>ideal S I; p \<in> carrier R; pol_coeff S c; p = polyn_expr R X (fst c) c; Subring R S; Ring S; p \<noteq> \<zero>\<rbrakk> \<Longrightarrow> (\<forall>j\<le>fst c. snd c j \<in> I) = P_mod R S X I p
[PROOF STEP]
apply (simp add:P_mod_def,
          drule sym,
          frule coeff_0_pol_0[THEN sym, of c "fst c"], simp, simp)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>ideal S I; \<zero> \<in> carrier R; pol_coeff S c; Subring R S; Ring S; p = \<zero>; \<forall>j\<le>fst c. snd c j = \<zero>\<^bsub>S\<^esub>; polyn_expr R X (fst c) c = \<zero>\<rbrakk> \<Longrightarrow> (\<exists>j. j \<le> fst c) \<longrightarrow> \<zero>\<^bsub>S\<^esub> \<in> I
 2. \<lbrakk>ideal S I; p \<in> carrier R; pol_coeff S c; p = polyn_expr R X (fst c) c; Subring R S; Ring S; p \<noteq> \<zero>\<rbrakk> \<Longrightarrow> (\<forall>j\<le>fst c. snd c j \<in> I) = P_mod R S X I p
[PROOF STEP]
apply (rule impI,
          simp add:Ring.ideal_zero)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ideal S I; p \<in> carrier R; pol_coeff S c; p = polyn_expr R X (fst c) c; Subring R S; Ring S; p \<noteq> \<zero>\<rbrakk> \<Longrightarrow> (\<forall>j\<le>fst c. snd c j \<in> I) = P_mod R S X I p
[PROOF STEP]
apply (frule s_cf_expr[of p],
       simp add:P_mod_def, (erule conjE)+)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ideal S I; p \<in> carrier R; pol_coeff S c; p = polyn_expr R X (fst c) c; Subring R S; Ring S; p \<noteq> \<zero>; pol_coeff S (s_cf R S X p); p = polyn_expr R X (fst (s_cf R S X p)) (s_cf R S X p); snd (s_cf R S X p) (fst (s_cf R S X p)) \<noteq> \<zero>\<^bsub>S\<^esub>\<rbrakk> \<Longrightarrow> (\<forall>j\<le>fst c. snd c j \<in> I) = P_mod R S X I p
[PROOF STEP]
apply (frule polyn_c_max[of c])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ideal S I; p \<in> carrier R; pol_coeff S c; p = polyn_expr R X (fst c) c; Subring R S; Ring S; p \<noteq> \<zero>; pol_coeff S (s_cf R S X p); p = polyn_expr R X (fst (s_cf R S X p)) (s_cf R S X p); snd (s_cf R S X p) (fst (s_cf R S X p)) \<noteq> \<zero>\<^bsub>S\<^esub>; polyn_expr R X (fst c) c = polyn_expr R X (c_max S c) c\<rbrakk> \<Longrightarrow> (\<forall>j\<le>fst c. snd c j \<in> I) = P_mod R S X I p
[PROOF STEP]
apply (frule coeff_nonzero_polyn_nonzero[of c "fst c"], simp)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ideal S I; p \<in> carrier R; pol_coeff S c; p = polyn_expr R X (fst c) c; Subring R S; Ring S; p \<noteq> \<zero>; pol_coeff S (s_cf R S X p); p = polyn_expr R X (fst (s_cf R S X p)) (s_cf R S X p); snd (s_cf R S X p) (fst (s_cf R S X p)) \<noteq> \<zero>\<^bsub>S\<^esub>; polyn_expr R X (fst c) c = polyn_expr R X (c_max S c) c; (polyn_expr R X (fst c) c \<noteq> \<zero>) = (\<exists>j\<le>fst c. snd c j \<noteq> \<zero>\<^bsub>S\<^esub>)\<rbrakk> \<Longrightarrow> (\<forall>j\<le>fst c. snd c j \<in> I) = P_mod R S X I p
[PROOF STEP]
apply (frule coeff_max_nonzeroTr[of c], simp)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ideal S I; p \<in> carrier R; pol_coeff S c; p = polyn_expr R X (fst c) c; Subring R S; Ring S; p \<noteq> \<zero>; pol_coeff S (s_cf R S X p); p = polyn_expr R X (fst (s_cf R S X p)) (s_cf R S X p); snd (s_cf R S X p) (fst (s_cf R S X p)) \<noteq> \<zero>\<^bsub>S\<^esub>; polyn_expr R X (fst c) c = polyn_expr R X (c_max S c) c; (polyn_expr R X (fst c) c \<noteq> \<zero>) = (\<exists>j\<le>fst c. snd c j \<noteq> \<zero>\<^bsub>S\<^esub>); snd c (c_max S c) \<noteq> \<zero>\<^bsub>S\<^esub>\<rbrakk> \<Longrightarrow> (\<forall>j\<le>fst c. snd c j \<in> I) = P_mod R S X I p
[PROOF STEP]
apply (thin_tac "(polyn_expr R X (fst c) c \<noteq> \<zero>) = (\<exists>j\<le>fst c. snd c j \<noteq> \<zero>\<^bsub>S\<^esub>)")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ideal S I; p \<in> carrier R; pol_coeff S c; p = polyn_expr R X (fst c) c; Subring R S; Ring S; p \<noteq> \<zero>; pol_coeff S (s_cf R S X p); p = polyn_expr R X (fst (s_cf R S X p)) (s_cf R S X p); snd (s_cf R S X p) (fst (s_cf R S X p)) \<noteq> \<zero>\<^bsub>S\<^esub>; polyn_expr R X (fst c) c = polyn_expr R X (c_max S c) c; snd c (c_max S c) \<noteq> \<zero>\<^bsub>S\<^esub>\<rbrakk> \<Longrightarrow> (\<forall>j\<le>fst c. snd c j \<in> I) = P_mod R S X I p
[PROOF STEP]
apply (frule coeff_max_bddTr[of c])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ideal S I; p \<in> carrier R; pol_coeff S c; p = polyn_expr R X (fst c) c; Subring R S; Ring S; p \<noteq> \<zero>; pol_coeff S (s_cf R S X p); p = polyn_expr R X (fst (s_cf R S X p)) (s_cf R S X p); snd (s_cf R S X p) (fst (s_cf R S X p)) \<noteq> \<zero>\<^bsub>S\<^esub>; polyn_expr R X (fst c) c = polyn_expr R X (c_max S c) c; snd c (c_max S c) \<noteq> \<zero>\<^bsub>S\<^esub>; c_max S c \<le> fst c\<rbrakk> \<Longrightarrow> (\<forall>j\<le>fst c. snd c j \<in> I) = P_mod R S X I p
[PROOF STEP]
apply (frule polyn_expr_short[of c "c_max S c"], assumption+)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ideal S I; p \<in> carrier R; pol_coeff S c; p = polyn_expr R X (fst c) c; Subring R S; Ring S; p \<noteq> \<zero>; pol_coeff S (s_cf R S X p); p = polyn_expr R X (fst (s_cf R S X p)) (s_cf R S X p); snd (s_cf R S X p) (fst (s_cf R S X p)) \<noteq> \<zero>\<^bsub>S\<^esub>; polyn_expr R X (fst c) c = polyn_expr R X (c_max S c) c; snd c (c_max S c) \<noteq> \<zero>\<^bsub>S\<^esub>; c_max S c \<le> fst c; polyn_expr R X (c_max S c) c = polyn_expr R X (c_max S c) (c_max S c, snd c)\<rbrakk> \<Longrightarrow> (\<forall>j\<le>fst c. snd c j \<in> I) = P_mod R S X I p
[PROOF STEP]
apply (frule pol_expr_unique[of p "(c_max S c, snd c)" "s_cf R S X p"],
        assumption+, rule split_pol_coeff[of c], assumption+,
        simp, simp, assumption+)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ideal S I; p \<in> carrier R; pol_coeff S c; p = polyn_expr R X (fst c) c; Subring R S; Ring S; p \<noteq> \<zero>; pol_coeff S (s_cf R S X p); p = polyn_expr R X (fst (s_cf R S X p)) (s_cf R S X p); snd (s_cf R S X p) (fst (s_cf R S X p)) \<noteq> \<zero>\<^bsub>S\<^esub>; polyn_expr R X (fst c) c = polyn_expr R X (c_max S c) c; snd c (c_max S c) \<noteq> \<zero>\<^bsub>S\<^esub>; c_max S c \<le> fst c; polyn_expr R X (c_max S c) c = polyn_expr R X (c_max S c) (c_max S c, snd c); fst (c_max S c, snd c) = fst (s_cf R S X p) \<and> (\<forall>j\<le>fst (c_max S c, snd c). snd (c_max S c, snd c) j = snd (s_cf R S X p) j)\<rbrakk> \<Longrightarrow> (\<forall>j\<le>fst c. snd c j \<in> I) = P_mod R S X I p
[PROOF STEP]
apply (thin_tac "p = polyn_expr R X (fst c) c",
        thin_tac "p = polyn_expr R X (fst (s_cf R S X p)) (s_cf R S X p)",
        thin_tac "polyn_expr R X (fst c) c = polyn_expr R X (c_max S c) c",
        thin_tac "polyn_expr R X (c_max S c) c =
                      polyn_expr R X (c_max S c) (c_max S c, snd c)")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ideal S I; p \<in> carrier R; pol_coeff S c; Subring R S; Ring S; p \<noteq> \<zero>; pol_coeff S (s_cf R S X p); snd (s_cf R S X p) (fst (s_cf R S X p)) \<noteq> \<zero>\<^bsub>S\<^esub>; snd c (c_max S c) \<noteq> \<zero>\<^bsub>S\<^esub>; c_max S c \<le> fst c; fst (c_max S c, snd c) = fst (s_cf R S X p) \<and> (\<forall>j\<le>fst (c_max S c, snd c). snd (c_max S c, snd c) j = snd (s_cf R S X p) j)\<rbrakk> \<Longrightarrow> (\<forall>j\<le>fst c. snd c j \<in> I) = P_mod R S X I p
[PROOF STEP]
apply (frule coeff_max_zeroTr[of c], (erule conjE)+)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ideal S I; p \<in> carrier R; pol_coeff S c; Subring R S; Ring S; p \<noteq> \<zero>; pol_coeff S (s_cf R S X p); snd (s_cf R S X p) (fst (s_cf R S X p)) \<noteq> \<zero>\<^bsub>S\<^esub>; snd c (c_max S c) \<noteq> \<zero>\<^bsub>S\<^esub>; c_max S c \<le> fst c; \<forall>j. j \<le> fst c \<and> c_max S c < j \<longrightarrow> snd c j = \<zero>\<^bsub>S\<^esub>; fst (c_max S c, snd c) = fst (s_cf R S X p); \<forall>j\<le>fst (c_max S c, snd c). snd (c_max S c, snd c) j = snd (s_cf R S X p) j\<rbrakk> \<Longrightarrow> (\<forall>j\<le>fst c. snd c j \<in> I) = P_mod R S X I p
[PROOF STEP]
apply (subst P_mod_def, simp)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ideal S I; p \<in> carrier R; pol_coeff S c; Subring R S; Ring S; p \<noteq> \<zero>; pol_coeff S (s_cf R S X p); snd (s_cf R S X p) (fst (s_cf R S X p)) \<noteq> \<zero>\<^bsub>S\<^esub>; fst (s_cf R S X p) \<le> fst c; \<forall>j. j \<le> fst c \<and> fst (s_cf R S X p) < j \<longrightarrow> snd c j = \<zero>\<^bsub>S\<^esub>; c_max S c = fst (s_cf R S X p); \<forall>j\<le>fst (s_cf R S X p). snd c j = snd (s_cf R S X p) j\<rbrakk> \<Longrightarrow> (\<forall>j\<le>fst c. snd c j \<in> I) = (\<forall>j\<le>fst (s_cf R S X p). snd (s_cf R S X p) j \<in> I)
[PROOF STEP]
apply (rule iffI, rule allI, rule impI)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>j. \<lbrakk>ideal S I; p \<in> carrier R; pol_coeff S c; Subring R S; Ring S; p \<noteq> \<zero>; pol_coeff S (s_cf R S X p); snd (s_cf R S X p) (fst (s_cf R S X p)) \<noteq> \<zero>\<^bsub>S\<^esub>; fst (s_cf R S X p) \<le> fst c; \<forall>j. j \<le> fst c \<and> fst (s_cf R S X p) < j \<longrightarrow> snd c j = \<zero>\<^bsub>S\<^esub>; c_max S c = fst (s_cf R S X p); \<forall>j\<le>fst (s_cf R S X p). snd c j = snd (s_cf R S X p) j; \<forall>j\<le>fst c. snd c j \<in> I; j \<le> fst (s_cf R S X p)\<rbrakk> \<Longrightarrow> snd (s_cf R S X p) j \<in> I
 2. \<lbrakk>ideal S I; p \<in> carrier R; pol_coeff S c; Subring R S; Ring S; p \<noteq> \<zero>; pol_coeff S (s_cf R S X p); snd (s_cf R S X p) (fst (s_cf R S X p)) \<noteq> \<zero>\<^bsub>S\<^esub>; fst (s_cf R S X p) \<le> fst c; \<forall>j. j \<le> fst c \<and> fst (s_cf R S X p) < j \<longrightarrow> snd c j = \<zero>\<^bsub>S\<^esub>; c_max S c = fst (s_cf R S X p); \<forall>j\<le>fst (s_cf R S X p). snd c j = snd (s_cf R S X p) j; \<forall>j\<le>fst (s_cf R S X p). snd (s_cf R S X p) j \<in> I\<rbrakk> \<Longrightarrow> \<forall>j\<le>fst c. snd c j \<in> I
[PROOF STEP]
apply (rotate_tac 10,
        drule_tac a = j in forall_spec,
        drule_tac x = j in spec, assumption,
        frule_tac i = j and j = "fst (s_cf R S X p)" and k = "fst c" in
                  le_trans, assumption+,
        drule_tac a = j in forall_spec, assumption, simp)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ideal S I; p \<in> carrier R; pol_coeff S c; Subring R S; Ring S; p \<noteq> \<zero>; pol_coeff S (s_cf R S X p); snd (s_cf R S X p) (fst (s_cf R S X p)) \<noteq> \<zero>\<^bsub>S\<^esub>; fst (s_cf R S X p) \<le> fst c; \<forall>j. j \<le> fst c \<and> fst (s_cf R S X p) < j \<longrightarrow> snd c j = \<zero>\<^bsub>S\<^esub>; c_max S c = fst (s_cf R S X p); \<forall>j\<le>fst (s_cf R S X p). snd c j = snd (s_cf R S X p) j; \<forall>j\<le>fst (s_cf R S X p). snd (s_cf R S X p) j \<in> I\<rbrakk> \<Longrightarrow> \<forall>j\<le>fst c. snd c j \<in> I
[PROOF STEP]
apply (rule allI, rule impI)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>j. \<lbrakk>ideal S I; p \<in> carrier R; pol_coeff S c; Subring R S; Ring S; p \<noteq> \<zero>; pol_coeff S (s_cf R S X p); snd (s_cf R S X p) (fst (s_cf R S X p)) \<noteq> \<zero>\<^bsub>S\<^esub>; fst (s_cf R S X p) \<le> fst c; \<forall>j. j \<le> fst c \<and> fst (s_cf R S X p) < j \<longrightarrow> snd c j = \<zero>\<^bsub>S\<^esub>; c_max S c = fst (s_cf R S X p); \<forall>j\<le>fst (s_cf R S X p). snd c j = snd (s_cf R S X p) j; \<forall>j\<le>fst (s_cf R S X p). snd (s_cf R S X p) j \<in> I; j \<le> fst c\<rbrakk> \<Longrightarrow> snd c j \<in> I
[PROOF STEP]
apply (case_tac "fst (s_cf R S X p) < j",
        drule_tac a = j in forall_spec, simp,
        simp add:Ring.ideal_zero,
        frule_tac x = "fst (s_cf R S X p)" and y = j in leI,
        thin_tac "\<forall>j. j \<le> fst c \<and> fst (s_cf R S X p) < j \<longrightarrow> snd c j = \<zero>\<^bsub>S\<^esub>",
        drule_tac a = j in forall_spec, assumption,
        drule_tac a = j in forall_spec, assumption, simp)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma (in PolynRg) monomial_P_mod_mod:"\<lbrakk>ideal S I; c \<in> carrier S;
       p = c \<cdot>\<^sub>r (X^\<^bsup>R d\<^esup>)\<rbrakk> \<Longrightarrow>  (c \<in> I) = (P_mod R S X I p)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ideal S I; c \<in> carrier S; p = c \<cdot>\<^sub>r X^\<^bsup>R d\<^esup>\<rbrakk> \<Longrightarrow> (c \<in> I) = P_mod R S X I p
[PROOF STEP]
apply (cut_tac subring, frule subring_Ring)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ideal S I; c \<in> carrier S; p = c \<cdot>\<^sub>r X^\<^bsup>R d\<^esup>; Subring R S; Ring S\<rbrakk> \<Longrightarrow> (c \<in> I) = P_mod R S X I p
[PROOF STEP]
apply (cut_tac monomial_d[THEN sym, of "(0, \<lambda>j. c)" "d"], simp)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>ideal S I; c \<in> carrier S; p = polyn_expr R X d (ext_cf S d (0, \<lambda>j. c)); Subring R S; Ring S; c \<cdot>\<^sub>r X^\<^bsup>R d\<^esup> = polyn_expr R X d (ext_cf S d (0, \<lambda>j. c))\<rbrakk> \<Longrightarrow> (c \<in> I) = P_mod R S X I (polyn_expr R X d (ext_cf S d (0, \<lambda>j. c)))
 2. \<lbrakk>ideal S I; c \<in> carrier S; p = c \<cdot>\<^sub>r X^\<^bsup>R d\<^esup>; Subring R S; Ring S\<rbrakk> \<Longrightarrow> pol_coeff S (0, \<lambda>j. c)
[PROOF STEP]
apply (drule sym, simp)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>ideal S I; c \<in> carrier S; Subring R S; Ring S; c \<cdot>\<^sub>r X^\<^bsup>R d\<^esup> = p; polyn_expr R X d (ext_cf S d (0, \<lambda>j. c)) = p\<rbrakk> \<Longrightarrow> (c \<in> I) = P_mod R S X I p
 2. \<lbrakk>ideal S I; c \<in> carrier S; p = c \<cdot>\<^sub>r X^\<^bsup>R d\<^esup>; Subring R S; Ring S\<rbrakk> \<Longrightarrow> pol_coeff S (0, \<lambda>j. c)
[PROOF STEP]
apply (subst P_mod_mod[THEN sym, of I p "ext_cf S d (0, \<lambda>j. c)"],
       assumption+)
[PROOF STATE]
proof (prove)
goal (5 subgoals):
 1. \<lbrakk>ideal S I; c \<in> carrier S; Subring R S; Ring S; c \<cdot>\<^sub>r X^\<^bsup>R d\<^esup> = p; polyn_expr R X d (ext_cf S d (0, \<lambda>j. c)) = p\<rbrakk> \<Longrightarrow> p \<in> carrier R
 2. \<lbrakk>ideal S I; c \<in> carrier S; Subring R S; Ring S; c \<cdot>\<^sub>r X^\<^bsup>R d\<^esup> = p; polyn_expr R X d (ext_cf S d (0, \<lambda>j. c)) = p\<rbrakk> \<Longrightarrow> pol_coeff S (ext_cf S d (0, \<lambda>j. c))
 3. \<lbrakk>ideal S I; c \<in> carrier S; Subring R S; Ring S; c \<cdot>\<^sub>r X^\<^bsup>R d\<^esup> = p; polyn_expr R X d (ext_cf S d (0, \<lambda>j. c)) = p\<rbrakk> \<Longrightarrow> p = polyn_expr R X (fst (ext_cf S d (0, \<lambda>j. c))) (ext_cf S d (0, \<lambda>j. c))
 4. \<lbrakk>ideal S I; c \<in> carrier S; Subring R S; Ring S; c \<cdot>\<^sub>r X^\<^bsup>R d\<^esup> = p; polyn_expr R X d (ext_cf S d (0, \<lambda>j. c)) = p\<rbrakk> \<Longrightarrow> (c \<in> I) = (\<forall>j\<le>fst (ext_cf S d (0, \<lambda>j. c)). snd (ext_cf S d (0, \<lambda>j. c)) j \<in> I)
 5. \<lbrakk>ideal S I; c \<in> carrier S; p = c \<cdot>\<^sub>r X^\<^bsup>R d\<^esup>; Subring R S; Ring S\<rbrakk> \<Longrightarrow> pol_coeff S (0, \<lambda>j. c)
[PROOF STEP]
apply (frule mem_subring_mem_ring[of S c], assumption,
          cut_tac X_mem_R,
          frule npClose[of X d], drule sym, simp add:ring_tOp_closed)
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<lbrakk>ideal S I; c \<in> carrier S; Subring R S; Ring S; c \<cdot>\<^sub>r X^\<^bsup>R d\<^esup> = p; polyn_expr R X d (ext_cf S d (0, \<lambda>j. c)) = p\<rbrakk> \<Longrightarrow> pol_coeff S (ext_cf S d (0, \<lambda>j. c))
 2. \<lbrakk>ideal S I; c \<in> carrier S; Subring R S; Ring S; c \<cdot>\<^sub>r X^\<^bsup>R d\<^esup> = p; polyn_expr R X d (ext_cf S d (0, \<lambda>j. c)) = p\<rbrakk> \<Longrightarrow> p = polyn_expr R X (fst (ext_cf S d (0, \<lambda>j. c))) (ext_cf S d (0, \<lambda>j. c))
 3. \<lbrakk>ideal S I; c \<in> carrier S; Subring R S; Ring S; c \<cdot>\<^sub>r X^\<^bsup>R d\<^esup> = p; polyn_expr R X d (ext_cf S d (0, \<lambda>j. c)) = p\<rbrakk> \<Longrightarrow> (c \<in> I) = (\<forall>j\<le>fst (ext_cf S d (0, \<lambda>j. c)). snd (ext_cf S d (0, \<lambda>j. c)) j \<in> I)
 4. \<lbrakk>ideal S I; c \<in> carrier S; p = c \<cdot>\<^sub>r X^\<^bsup>R d\<^esup>; Subring R S; Ring S\<rbrakk> \<Longrightarrow> pol_coeff S (0, \<lambda>j. c)
[PROOF STEP]
apply (simp add:pol_coeff_def, rule allI, rule impI,
       simp add:ext_cf_def sliden_def, rule impI, simp add:Ring.ring_zero,
       subst ext_cf_len, simp add:pol_coeff_def,
       simp)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>ideal S I; c \<in> carrier S; Subring R S; Ring S; c \<cdot>\<^sub>r X^\<^bsup>R d\<^esup> = p; polyn_expr R X d (ext_cf S d (0, \<lambda>j. c)) = p\<rbrakk> \<Longrightarrow> (c \<in> I) = (\<forall>j\<le>fst (ext_cf S d (0, \<lambda>j. c)). snd (ext_cf S d (0, \<lambda>j. c)) j \<in> I)
 2. \<lbrakk>ideal S I; c \<in> carrier S; p = c \<cdot>\<^sub>r X^\<^bsup>R d\<^esup>; Subring R S; Ring S\<rbrakk> \<Longrightarrow> pol_coeff S (0, \<lambda>j. c)
[PROOF STEP]
apply (subst ext_cf_len, simp add:pol_coeff_def,
          simp add:ext_cf_def)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>ideal S I; c \<in> carrier S; Subring R S; Ring S; c \<cdot>\<^sub>r X^\<^bsup>R d\<^esup> = p; polyn_expr R X d (d, \<lambda>i. if d \<le> i then snd (0, \<lambda>j. c) (sliden d i) else \<zero>\<^bsub>S\<^esub>) = p\<rbrakk> \<Longrightarrow> (c \<in> I) = (\<forall>j. (d = j \<longrightarrow> c \<in> I) \<and> (d \<noteq> j \<longrightarrow> j \<le> d \<longrightarrow> \<zero>\<^bsub>S\<^esub> \<in> I))
 2. \<lbrakk>ideal S I; c \<in> carrier S; p = c \<cdot>\<^sub>r X^\<^bsup>R d\<^esup>; Subring R S; Ring S\<rbrakk> \<Longrightarrow> pol_coeff S (0, \<lambda>j. c)
[PROOF STEP]
apply (rule iffI)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<lbrakk>ideal S I; c \<in> carrier S; Subring R S; Ring S; c \<cdot>\<^sub>r X^\<^bsup>R d\<^esup> = p; polyn_expr R X d (d, \<lambda>i. if d \<le> i then snd (0, \<lambda>j. c) (sliden d i) else \<zero>\<^bsub>S\<^esub>) = p; c \<in> I\<rbrakk> \<Longrightarrow> \<forall>j. (d = j \<longrightarrow> c \<in> I) \<and> (d \<noteq> j \<longrightarrow> j \<le> d \<longrightarrow> \<zero>\<^bsub>S\<^esub> \<in> I)
 2. \<lbrakk>ideal S I; c \<in> carrier S; Subring R S; Ring S; c \<cdot>\<^sub>r X^\<^bsup>R d\<^esup> = p; polyn_expr R X d (d, \<lambda>i. if d \<le> i then snd (0, \<lambda>j. c) (sliden d i) else \<zero>\<^bsub>S\<^esub>) = p; \<forall>j. (d = j \<longrightarrow> c \<in> I) \<and> (d \<noteq> j \<longrightarrow> j \<le> d \<longrightarrow> \<zero>\<^bsub>S\<^esub> \<in> I)\<rbrakk> \<Longrightarrow> c \<in> I
 3. \<lbrakk>ideal S I; c \<in> carrier S; p = c \<cdot>\<^sub>r X^\<^bsup>R d\<^esup>; Subring R S; Ring S\<rbrakk> \<Longrightarrow> pol_coeff S (0, \<lambda>j. c)
[PROOF STEP]
apply (simp add:Ring.ideal_zero,
          drule_tac x = d in spec,
          simp, simp add:pol_coeff_def)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done