[STATEMENT]
lemma (in Corps) val_1mx_pow:"\<lbrakk>valuation K v; x \<in> carrier K;
       0 < (v (1\<^sub>r \<plusminus> -\<^sub>a x))\<rbrakk> \<Longrightarrow> 0 < (v (1\<^sub>r \<plusminus> -\<^sub>a x^\<^bsup>K (Suc n)\<^esup>))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>valuation K v; x \<in> carrier K; 0 < v (1\<^sub>r \<plusminus> -\<^sub>a x)\<rbrakk> \<Longrightarrow> 0 < v (1\<^sub>r \<plusminus> -\<^sub>a x^\<^bsup>K Suc n\<^esup>)
[PROOF STEP]
apply (cut_tac field_is_ring, frule Ring.ring_is_ag[of "K"])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>valuation K v; x \<in> carrier K; 0 < v (1\<^sub>r \<plusminus> -\<^sub>a x); Ring K; aGroup K\<rbrakk> \<Longrightarrow> 0 < v (1\<^sub>r \<plusminus> -\<^sub>a x^\<^bsup>K Suc n\<^esup>)
[PROOF STEP]
apply (subst Ring.one_m_x_times[THEN sym, of K x n], assumption+)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>valuation K v; x \<in> carrier K; 0 < v (1\<^sub>r \<plusminus> -\<^sub>a x); Ring K; aGroup K\<rbrakk> \<Longrightarrow> 0 < v ((1\<^sub>r \<plusminus> -\<^sub>a x) \<cdot>\<^sub>r \<Sigma>\<^sub>e K NPOW x K n)
[PROOF STEP]
apply (frule Ring.ring_one[of "K"],
        frule x_pow_fSum_in_Vr[of v x n],
        subst val_pos_mem_Vr[THEN sym], assumption+,
        frule val_1mx_pos[of "v" "x"], assumption+,
        simp)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>valuation K v; x \<in> carrier K; 0 < v (1\<^sub>r \<plusminus> -\<^sub>a x); Ring K; aGroup K; 1\<^sub>r \<in> carrier K; \<Sigma>\<^sub>e K NPOW x K n \<in> carrier (Vr K v)\<rbrakk> \<Longrightarrow> 0 < v ((1\<^sub>r \<plusminus> -\<^sub>a x) \<cdot>\<^sub>r \<Sigma>\<^sub>e K NPOW x K n)
[PROOF STEP]
apply (subst val_t2p, assumption+,
        rule aGroup.ag_pOp_closed, assumption+,
        simp add:aGroup.ag_mOp_closed, simp add:Vr_mem_f_mem,
        frule val_pos_mem_Vr[THEN sym, of v "nsum K (npow K x) n"],
        simp add:Vr_mem_f_mem, simp)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>valuation K v; x \<in> carrier K; 0 < v (1\<^sub>r \<plusminus> -\<^sub>a x); Ring K; aGroup K; 1\<^sub>r \<in> carrier K; 0 \<le> v (\<Sigma>\<^sub>e K NPOW x K n); \<Sigma>\<^sub>e K NPOW x K n \<in> carrier (Vr K v)\<rbrakk> \<Longrightarrow> 0 < v (1\<^sub>r \<plusminus> -\<^sub>a x) + v (\<Sigma>\<^sub>e K NPOW x K n)
[PROOF STEP]
apply(frule aadd_le_mono[of "0" "v (nsum K (npow K x) n)" "v (1\<^sub>r \<plusminus> -\<^sub>a x)"],
       simp add:aadd_0_l, simp add:aadd_commute)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done