[STATEMENT]
lemma fundamental_theorem_eq_5: assumes i: "3 \<le> i" "i \<le> k" "n i < j" "j < n (i - 1) - 1"
  shows "R j = 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. R j = 0
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. R j = 0
[PROOF STEP]
from BT_lemma_2_23[OF i]
[PROOF STATE]
proof (chain)
picking this:
subresultant j (F (i - 2)) (F (i - 1)) = 0
[PROOF STEP]
have id1: "subresultant j (F (i - 2)) (F (i - 1)) = 0"
[PROOF STATE]
proof (prove)
using this:
subresultant j (F (i - 2)) (F (i - 1)) = 0

goal (1 subgoal):
 1. subresultant j (F (i - 2)) (F (i - 1)) = 0
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
subresultant j (F (i - 2)) (F (i - 1)) = 0

goal (1 subgoal):
 1. R j = 0
[PROOF STEP]
have "n (i - 1) \<le> n 2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. n (i - 1) \<le> n 2
[PROOF STEP]
by (rule n_ge_trans, insert i, auto)
[PROOF STATE]
proof (state)
this:
n (i - 1) \<le> n 2

goal (1 subgoal):
 1. R j = 0
[PROOF STEP]
with n_gt[of "i - 1"] i
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>2 \<le> i - 1; i - 1 < k\<rbrakk> \<Longrightarrow> n (Suc (i - 1)) < n (i - 1)
3 \<le> i
i \<le> k
n i < j
j < n (i - 1) - 1
n (i - 1) \<le> n 2
[PROOF STEP]
have "n (i - 1) - 1 < n 2"
    and lt: "j < n (i - 1)"
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>2 \<le> i - 1; i - 1 < k\<rbrakk> \<Longrightarrow> n (Suc (i - 1)) < n (i - 1)
3 \<le> i
i \<le> k
n i < j
j < n (i - 1) - 1
n (i - 1) \<le> n 2

goal (1 subgoal):
 1. n (i - 1) - 1 < n 2 &&& j < n (i - 1)
[PROOF STEP]
by linarith+
[PROOF STATE]
proof (state)
this:
n (i - 1) - 1 < n 2
j < n (i - 1)

goal (1 subgoal):
 1. R j = 0
[PROOF STEP]
with i
[PROOF STATE]
proof (chain)
picking this:
3 \<le> i
i \<le> k
n i < j
j < n (i - 1) - 1
n (i - 1) - 1 < n 2
j < n (i - 1)
[PROOF STEP]
have "R j = subresultant j G1 G2"
[PROOF STATE]
proof (prove)
using this:
3 \<le> i
i \<le> k
n i < j
j < n (i - 1) - 1
n (i - 1) - 1 < n 2
j < n (i - 1)

goal (1 subgoal):
 1. R j = subresultant j G1 G2
[PROOF STEP]
unfolding R_def
[PROOF STATE]
proof (prove)
using this:
3 \<le> i
i \<le> k
n i < j
j < n (i - 1) - 1
n (i - 1) - 1 < n 2
j < n (i - 1)

goal (1 subgoal):
 1. (if j = n 2 then sdiv_poly (Polynomial.smult (lead_coeff G2 ^ \<delta> 1) G2) (lead_coeff G2) else subresultant j G1 G2) = subresultant j G1 G2
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
R j = subresultant j G1 G2

goal (1 subgoal):
 1. R j = 0
[PROOF STEP]
from arg_cong[OF this, of ffp, unfolded to_fract_hom.subresultant_hom, folded F1 F2]
[PROOF STATE]
proof (chain)
picking this:
ffp (R j) = subresultant j (F 1) (F 2)
[PROOF STEP]
have id2: "ffp (R j) = subresultant j (F 1) (F 2)"
[PROOF STATE]
proof (prove)
using this:
ffp (R j) = subresultant j (F 1) (F 2)

goal (1 subgoal):
 1. ffp (R j) = subresultant j (F 1) (F 2)
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
ffp (R j) = subresultant j (F 1) (F 2)

goal (1 subgoal):
 1. R j = 0
[PROOF STEP]
from i
[PROOF STATE]
proof (chain)
picking this:
3 \<le> i
i \<le> k
n i < j
j < n (i - 1) - 1
[PROOF STEP]
have "3 \<le> i" "i \<le> k + 1"
[PROOF STATE]
proof (prove)
using this:
3 \<le> i
i \<le> k
n i < j
j < n (i - 1) - 1

goal (1 subgoal):
 1. 3 \<le> i &&& i \<le> k + 1
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
3 \<le> i
i \<le> k + 1

goal (1 subgoal):
 1. R j = 0
[PROOF STEP]
note eq_30 = BT_eq_30[OF this lt]
[PROOF STATE]
proof (state)
this:
Polynomial.smult (\<Prod>l\<leftarrow>[3..<i]. \<alpha> l ^ (n (l - 1) - j)) (subresultant j (F 1) (F 2)) = Polynomial.smult (\<Prod>l\<leftarrow>[3..<i]. \<beta> l ^ (n (l - 1) - j) * f (l - 1) ^ (\<delta> (l - 2) + \<delta> (l - 1)) * (- 1) ^ ((n (l - 2) - j) * (n (l - 1) - j))) (subresultant j (F (i - 2)) (F (i - 1)))

goal (1 subgoal):
 1. R j = 0
[PROOF STEP]
let ?c3 = "\<Prod>l\<leftarrow>[3..<i]. \<alpha> l ^ (n (l - 1) - j)"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. R j = 0
[PROOF STEP]
let ?c2 = "\<Prod>l\<leftarrow>[3..<i]. \<beta> l ^ (n (l - 1) - j) * f (l - 1) ^ (\<delta> (l - 2) + \<delta> (l - 1)) *
                  (- 1) ^ ((n (l - 2) - j) * (n (l - 1) - j))"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. R j = 0
[PROOF STEP]
have "?c3 \<noteq> 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Prod>l\<leftarrow>[3..<i]. \<alpha> l ^ (n (l - 1) - j)) \<noteq> 0
[PROOF STEP]
by (rule nonzero_alphaprod, insert i, auto)
[PROOF STATE]
proof (state)
this:
(\<Prod>l\<leftarrow>[3..<i]. \<alpha> l ^ (n (l - 1) - j)) \<noteq> 0

goal (1 subgoal):
 1. R j = 0
[PROOF STEP]
with arg_cong[OF eq_30, of "smult (inverse ?c3)"]
[PROOF STATE]
proof (chain)
picking this:
Polynomial.smult (inverse (\<Prod>l\<leftarrow>[3..<i]. \<alpha> l ^ (n (l - 1) - j))) (Polynomial.smult (\<Prod>l\<leftarrow>[3..<i]. \<alpha> l ^ (n (l - 1) - j)) (subresultant j (F 1) (F 2))) = Polynomial.smult (inverse (\<Prod>l\<leftarrow>[3..<i]. \<alpha> l ^ (n (l - 1) - j))) (Polynomial.smult (\<Prod>l\<leftarrow>[3..<i]. \<beta> l ^ (n (l - 1) - j) * f (l - 1) ^ (\<delta> (l - 2) + \<delta> (l - 1)) * (- 1) ^ ((n (l - 2) - j) * (n (l - 1) - j))) (subresultant j (F (i - 2)) (F (i - 1))))
(\<Prod>l\<leftarrow>[3..<i]. \<alpha> l ^ (n (l - 1) - j)) \<noteq> 0
[PROOF STEP]
have id3: "subresultant j (F 1) (F 2) = smult (inverse ?c3 * ?c2)
     (subresultant j (F (i - 2)) (F (i - 1)))"
[PROOF STATE]
proof (prove)
using this:
Polynomial.smult (inverse (\<Prod>l\<leftarrow>[3..<i]. \<alpha> l ^ (n (l - 1) - j))) (Polynomial.smult (\<Prod>l\<leftarrow>[3..<i]. \<alpha> l ^ (n (l - 1) - j)) (subresultant j (F 1) (F 2))) = Polynomial.smult (inverse (\<Prod>l\<leftarrow>[3..<i]. \<alpha> l ^ (n (l - 1) - j))) (Polynomial.smult (\<Prod>l\<leftarrow>[3..<i]. \<beta> l ^ (n (l - 1) - j) * f (l - 1) ^ (\<delta> (l - 2) + \<delta> (l - 1)) * (- 1) ^ ((n (l - 2) - j) * (n (l - 1) - j))) (subresultant j (F (i - 2)) (F (i - 1))))
(\<Prod>l\<leftarrow>[3..<i]. \<alpha> l ^ (n (l - 1) - j)) \<noteq> 0

goal (1 subgoal):
 1. subresultant j (F 1) (F 2) = Polynomial.smult (inverse (\<Prod>l\<leftarrow>[3..<i]. \<alpha> l ^ (n (l - 1) - j)) * (\<Prod>l\<leftarrow>[3..<i]. \<beta> l ^ (n (l - 1) - j) * f (l - 1) ^ (\<delta> (l - 2) + \<delta> (l - 1)) * (- 1) ^ ((n (l - 2) - j) * (n (l - 1) - j)))) (subresultant j (F (i - 2)) (F (i - 1)))
[PROOF STEP]
by (auto intro: poly_eqI)
[PROOF STATE]
proof (state)
this:
subresultant j (F 1) (F 2) = Polynomial.smult (inverse (\<Prod>l\<leftarrow>[3..<i]. \<alpha> l ^ (n (l - 1) - j)) * (\<Prod>l\<leftarrow>[3..<i]. \<beta> l ^ (n (l - 1) - j) * f (l - 1) ^ (\<delta> (l - 2) + \<delta> (l - 1)) * (- 1) ^ ((n (l - 2) - j) * (n (l - 1) - j)))) (subresultant j (F (i - 2)) (F (i - 1)))

goal (1 subgoal):
 1. R j = 0
[PROOF STEP]
have "ffp (R j) = 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ffp (R j) = 0
[PROOF STEP]
unfolding id1 id2 id3
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Polynomial.smult (inverse (\<Prod>l\<leftarrow>[3..<i]. \<alpha> l ^ (n (l - 1) - j)) * (\<Prod>l\<leftarrow>[3..<i]. \<beta> l ^ (n (l - 1) - j) * f (l - 1) ^ (\<delta> (l - 2) + \<delta> (l - 1)) * (- 1) ^ ((n (l - 2) - j) * (n (l - 1) - j)))) 0 = 0
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
ffp (R j) = 0

goal (1 subgoal):
 1. R j = 0
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
ffp (R j) = 0

goal (1 subgoal):
 1. R j = 0
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
R j = 0

goal:
No subgoals!
[PROOF STEP]
qed