(* ========================================================================= *)
(* Fundamental theorem of algebra.                                           *)
(* ========================================================================= *)

needs "Complex/complex_transc.ml";;
needs "Complex/cpoly.ml";;

prioritize_complex();;

(* ------------------------------------------------------------------------- *)
(* A cute trick to reduce magnitude of unimodular number.                    *)
(* ------------------------------------------------------------------------- *)

let SQRT_SOS_LT_1 = 
prove (`!x y. sqrt(x pow 2 + y pow 2) < &1 <=> x pow 2 + y pow 2 < &1`,
REPEAT GEN_TAC THEN GEN_REWRITE_TAC (LAND_CONV o RAND_CONV) [GSYM SQRT_1] THEN REWRITE_TAC[REAL_POW_2] THEN SIMP_TAC[SQRT_MONO_LT_EQ; REAL_POS; REAL_LE_ADD; REAL_LE_SQUARE]);;
let SQRT_SOS_EQ_1 = 
prove (`!x y. (sqrt(x pow 2 + y pow 2) = &1) <=> (x pow 2 + y pow 2 = &1)`,
REPEAT GEN_TAC THEN GEN_REWRITE_TAC (LAND_CONV o RAND_CONV) [GSYM SQRT_1] THEN REWRITE_TAC[REAL_POW_2] THEN SIMP_TAC[SQRT_INJ; REAL_POS; REAL_LE_ADD; REAL_LE_SQUARE]);;
let UNIMODULAR_REDUCE_NORM = 
prove (`!z. (norm(z) = &1) ==> norm(z + Cx(&1)) < &1 \/ norm(z - Cx(&1)) < &1 \/ norm(z + ii) < &1 \/ norm(z - ii) < &1`,
GEN_TAC THEN REWRITE_TAC[ii; CX_DEF; complex_add; complex_sub; complex_neg; complex_norm; RE; IM; REAL_ADD_RID; REAL_NEG_0; SQRT_SOS_LT_1; SQRT_SOS_EQ_1] THEN SIMP_TAC[REAL_POW_2; REAL_ARITH `a * a + (b + c) * (b + c) = (a * a + b * b) + (&2 * b * c + c * c)`; REAL_ARITH `(b + c) * (b + c) + a * a = (b * b + a * a) + (&2 * b * c + c * c)`] THEN DISCH_TAC THEN REWRITE_TAC[REAL_ARITH `&1 + x < &1 <=> &0 < --x`] THEN REWRITE_TAC[REAL_NEG_ADD; REAL_MUL_LNEG; REAL_MUL_RNEG; REAL_NEG_NEG] THEN REWRITE_TAC[REAL_MUL_RID] THEN MATCH_MP_TAC(REAL_ARITH `~(abs(a) <= &1 /\ abs(b) <= &1) ==> &0 < --a + --(&1) \/ &0 < a + --(&1) \/ &0 < --b + --(&1) \/ &0 < b + --(&1)`) THEN STRIP_TAC THEN UNDISCH_TAC `Re z * Re z + Im z * Im z = &1` THEN REWRITE_TAC[] THEN MATCH_MP_TAC(REAL_ARITH `(&2 * r) * (&2 * r) <= &1 /\ (&2 * i) * (&2 * i) <= &1 ==> ~(r * r + i * i = &1)`) THEN REWRITE_TAC[GSYM REAL_POW_2] THEN ONCE_REWRITE_TAC[GSYM REAL_POW2_ABS] THEN ASM_SIMP_TAC[REAL_POW_1_LE; REAL_ABS_POS]);;
(* ------------------------------------------------------------------------- *) (* Hence we can always reduce modulus of 1 + b z^n if nonzero *) (* ------------------------------------------------------------------------- *)
let REDUCE_POLY_SIMPLE = 
prove (`!b n. ~(b = Cx(&0)) /\ ~(n = 0) ==> ?z. norm(Cx(&1) + b * z pow n) < &1`,
GEN_TAC THEN MATCH_MP_TAC num_WF THEN REPEAT STRIP_TAC THEN ASM_CASES_TAC `EVEN(n)` THENL [FIRST_X_ASSUM(MP_TAC o GEN_REWRITE_RULE I [EVEN_EXISTS]) THEN DISCH_THEN(X_CHOOSE_THEN `m:num` SUBST_ALL_TAC) THEN FIRST_X_ASSUM(MP_TAC o SPEC `m:num`) THEN ASM_SIMP_TAC[ARITH_RULE `~(2 * m = 0) ==> m < 2 * m /\ ~(m = 0)`] THEN DISCH_THEN(X_CHOOSE_TAC `w:complex`) THEN EXISTS_TAC `csqrt w` THEN ASM_REWRITE_TAC[GSYM COMPLEX_POW_POW; CSQRT]; ALL_TAC] THEN MP_TAC(SPEC `Cx(norm b) / b` UNIMODULAR_REDUCE_NORM) THEN ANTS_TAC THENL [REWRITE_TAC[COMPLEX_NORM_DIV; COMPLEX_NORM_CX] THEN ASM_SIMP_TAC[COMPLEX_ABS_NORM; REAL_DIV_REFL; COMPLEX_NORM_ZERO]; ALL_TAC] THEN DISCH_TAC THEN SUBGOAL_THEN `?v. norm(Cx(norm b) / b + v pow n) < &1` MP_TAC THENL [SUBGOAL_THEN `(Cx(&1) pow n = Cx(&1)) /\ (--Cx(&1) pow n = --Cx(&1)) /\ (((ii pow n = ii) /\ (--ii pow n = --ii)) \/ ((ii pow n = --ii) /\ (--ii pow n = ii)))` MP_TAC THENL [ALL_TAC; RULE_ASSUM_TAC(REWRITE_RULE[complex_sub]) THEN ASM_MESON_TAC[]] THEN FIRST_X_ASSUM(MP_TAC o GEN_REWRITE_RULE I [NOT_EVEN]) THEN SIMP_TAC[ODD_EXISTS; LEFT_IMP_EXISTS_THM] THEN X_GEN_TAC `m:num` THEN DISCH_THEN(K ALL_TAC) THEN REWRITE_TAC[complex_pow; COMPLEX_POW_NEG; EVEN; EVEN_MULT; ARITH_EVEN] THEN REWRITE_TAC[GSYM COMPLEX_POW_POW] THEN REWRITE_TAC[COMPLEX_POW_ONE; COMPLEX_POW_II_2; COMPLEX_MUL_LID; COMPLEX_POW_NEG] THEN COND_CASES_TAC THEN REWRITE_TAC[COMPLEX_MUL_RID; COMPLEX_MUL_RNEG; COMPLEX_NEG_NEG]; ALL_TAC] THEN DISCH_THEN(X_CHOOSE_THEN `v:complex` ASSUME_TAC) THEN EXISTS_TAC `v / Cx(root(n) (norm b))` THEN REWRITE_TAC[COMPLEX_POW_DIV; GSYM CX_POW] THEN SUBGOAL_THEN `root n (norm b) pow n = norm b` SUBST1_TAC THENL [UNDISCH_TAC `~(EVEN n)` THEN SPEC_TAC(`n:num`,`n:num`) THEN INDUCT_TAC THEN SIMP_TAC[EVEN; ROOT_POW_POS; COMPLEX_NORM_POS]; ALL_TAC] THEN MATCH_MP_TAC REAL_LT_LCANCEL_IMP THEN EXISTS_TAC `norm(Cx(norm b) / b)` THEN REWRITE_TAC[GSYM COMPLEX_NORM_MUL; COMPLEX_ADD_LDISTRIB] THEN REWRITE_TAC[COMPLEX_MUL_RID; REAL_MUL_RID] THEN SUBGOAL_THEN `norm(Cx(norm b) / b) = &1` SUBST1_TAC THENL [REWRITE_TAC[COMPLEX_NORM_DIV; COMPLEX_NORM_CX; COMPLEX_ABS_NORM] THEN ASM_SIMP_TAC[REAL_DIV_REFL; COMPLEX_NORM_ZERO]; ALL_TAC] THEN REWRITE_TAC[REAL_LT_01; complex_div] THEN ONCE_REWRITE_TAC[AC COMPLEX_MUL_AC `(m * b') * b * p * m' = (m * m') * (b * b') * p`] THEN ASM_SIMP_TAC[COMPLEX_MUL_RINV; COMPLEX_MUL_LID; CX_INJ; COMPLEX_NORM_ZERO] THEN ASM_REWRITE_TAC[GSYM complex_div]);;
(* ------------------------------------------------------------------------- *) (* Basic lemmas about polynomials. *) (* ------------------------------------------------------------------------- *)
let POLY_CMUL_MAP = 
prove (`!p c x. poly (MAP (( * ) c) p) x = c * poly p x`,
LIST_INDUCT_TAC THEN REWRITE_TAC[MAP; poly; COMPLEX_MUL_RZERO] THEN ASM_REWRITE_TAC[COMPLEX_ADD_LDISTRIB] THEN REWRITE_TAC[COMPLEX_MUL_AC]);;
let POLY_0 = 
prove (`!p x. ALL (\b. b = Cx(&0)) p ==> (poly p x = Cx(&0))`,
LIST_INDUCT_TAC THEN ASM_SIMP_TAC[ALL; poly; COMPLEX_MUL_RZERO; COMPLEX_ADD_RID]);;
let POLY_BOUND_EXISTS = 
prove (`!p r. ?m. &0 < m /\ !z. norm(z) <= r ==> norm(poly p z) <= m`,
ONCE_REWRITE_TAC[SWAP_FORALL_THM] THEN GEN_TAC THEN LIST_INDUCT_TAC THENL [EXISTS_TAC `&1` THEN REWRITE_TAC[poly; COMPLEX_NORM_CX] THEN REWRITE_TAC[REAL_ABS_NUM; REAL_LT_01; REAL_POS]; ALL_TAC] THEN POP_ASSUM(X_CHOOSE_THEN `m:real` STRIP_ASSUME_TAC) THEN EXISTS_TAC `&1 + norm(h) + abs(r * m)` THEN ASM_SIMP_TAC[REAL_ARITH `&0 <= x /\ &0 <= y ==> &0 < &1 + x + y`; REAL_ABS_POS; COMPLEX_NORM_POS] THEN X_GEN_TAC `z:complex` THEN DISCH_TAC THEN REWRITE_TAC[poly] THEN MATCH_MP_TAC REAL_LE_TRANS THEN EXISTS_TAC `norm(h) + norm(z * poly t z)` THEN REWRITE_TAC[COMPLEX_NORM_TRIANGLE] THEN MATCH_MP_TAC(REAL_ARITH `y <= z ==> x + y <= &1 + x + abs(z)`) THEN REWRITE_TAC[COMPLEX_NORM_MUL] THEN MATCH_MP_TAC REAL_LE_MUL2 THEN ASM_SIMP_TAC[COMPLEX_NORM_POS]);;
(* ------------------------------------------------------------------------- *) (* Offsetting the variable in a polynomial gives another of same degree. *) (* ------------------------------------------------------------------------- *)
let POLY_OFFSET_LEMMA = 
prove (`!a p. ?b q. (LENGTH q = LENGTH p) /\ !x. poly (CONS b q) x = (a + x) * poly p x`,
GEN_TAC THEN LIST_INDUCT_TAC THENL [EXISTS_TAC `Cx(&0)` THEN EXISTS_TAC `[]:complex list` THEN REWRITE_TAC[poly; LENGTH; COMPLEX_MUL_RZERO; COMPLEX_ADD_RID]; ALL_TAC] THEN POP_ASSUM STRIP_ASSUME_TAC THEN EXISTS_TAC `a * h` THEN EXISTS_TAC `CONS (b + h) q` THEN ASM_REWRITE_TAC[LENGTH; poly] THEN X_GEN_TAC `x:complex ` THEN FIRST_ASSUM(MP_TAC o SPEC `x:complex`) THEN REWRITE_TAC[poly] THEN DISCH_THEN(MP_TAC o AP_TERM `( * ) x`) THEN SIMPLE_COMPLEX_ARITH_TAC);;
let POLY_OFFSET = 
prove (`!a p. ?q. (LENGTH q = LENGTH p) /\ !x. poly q x = poly p (a + x)`,
GEN_TAC THEN LIST_INDUCT_TAC THEN REWRITE_TAC[LENGTH; poly] THENL [EXISTS_TAC `[]:complex list` THEN REWRITE_TAC[poly; LENGTH]; ALL_TAC] THEN POP_ASSUM(X_CHOOSE_THEN `p:complex list` (STRIP_ASSUME_TAC o GSYM)) THEN ASM_REWRITE_TAC[] THEN MP_TAC(SPECL [`a:complex`; `p:complex list`] POLY_OFFSET_LEMMA) THEN DISCH_THEN(X_CHOOSE_THEN `b:complex` (X_CHOOSE_THEN `r: complex list` (STRIP_ASSUME_TAC o GSYM))) THEN EXISTS_TAC `CONS (h + b) r` THEN ASM_REWRITE_TAC[LENGTH] THEN REWRITE_TAC[poly] THEN SIMPLE_COMPLEX_ARITH_TAC);;
(* ------------------------------------------------------------------------- *) (* Bolzano-Weierstrass type property for closed disc in complex plane. *) (* ------------------------------------------------------------------------- *)
let METRIC_BOUND_LEMMA = 
prove (`!x y. norm(x - y) <= abs(Re(x) - Re(y)) + abs(Im(x) - Im(y))`,
REPEAT GEN_TAC THEN REWRITE_TAC[complex_norm] THEN MATCH_MP_TAC(REAL_ARITH `a <= abs(abs x + abs y) ==> a <= abs x + abs y`) THEN GEN_REWRITE_TAC RAND_CONV [GSYM POW_2_SQRT_ABS] THEN MATCH_MP_TAC SQRT_MONO_LE THEN SIMP_TAC[REAL_POW_2; REAL_LE_ADD; REAL_LE_SQUARE] THEN REWRITE_TAC[complex_add; complex_sub; complex_neg; RE; IM] THEN REWRITE_TAC[GSYM real_sub] THEN REWRITE_TAC[REAL_ARITH `(a + b) * (a + b) = a * a + b * b + &2 * a * b`] THEN REWRITE_TAC[GSYM REAL_ABS_MUL] THEN REWRITE_TAC[REAL_ARITH `a + b <= abs a + abs b + &2 * abs c`]);;
let BOLZANO_WEIERSTRASS_COMPLEX_DISC = 
prove (`!s r. (!n. norm(s n) <= r) ==> ?f z. subseq f /\ !e. &0 < e ==> ?N. !n. n >= N ==> norm(s(f n) - z) < e`,
REPEAT STRIP_TAC THEN MP_TAC(SPEC `Re o (s:num->complex)` SEQ_MONOSUB) THEN DISCH_THEN(X_CHOOSE_THEN `f:num->num` MP_TAC) THEN REWRITE_TAC[o_THM] THEN STRIP_TAC THEN MP_TAC(SPEC `Im o (s:num->complex) o (f:num->num)` SEQ_MONOSUB) THEN DISCH_THEN(X_CHOOSE_THEN `g:num->num` MP_TAC) THEN REWRITE_TAC[o_THM] THEN STRIP_TAC THEN EXISTS_TAC `(f:num->num) o (g:num->num)` THEN SUBGOAL_THEN `convergent (\n. Re(s(f n :num))) /\ convergent (\n. Im(s((f:num->num)(g n))))` MP_TAC THENL [CONJ_TAC THEN MATCH_MP_TAC SEQ_BCONV THEN ASM_REWRITE_TAC[bounded] THEN MAP_EVERY EXISTS_TAC [`r + &1`; `&0`; `0`] THEN REWRITE_TAC[GE; LE_0; MR1_DEF; REAL_SUB_LZERO; REAL_ABS_NEG] THEN X_GEN_TAC `n:num` THEN W(fun (_,w) -> FIRST_ASSUM(MP_TAC o SPEC (funpow 3 rand (lhand w)))) THEN REWRITE_TAC[complex_norm] THEN MATCH_MP_TAC(REAL_ARITH `a <= b ==> b <= r ==> a < r + &1`) THEN GEN_REWRITE_TAC LAND_CONV [GSYM POW_2_SQRT_ABS] THEN MATCH_MP_TAC SQRT_MONO_LE THEN REWRITE_TAC[REAL_POW_2; REAL_LE_SQUARE; REAL_LE_ADDR; REAL_LE_ADDL]; ALL_TAC] THEN REWRITE_TAC[convergent; SEQ; GE] THEN DISCH_THEN(CONJUNCTS_THEN2 (X_CHOOSE_TAC `x:real`) (X_CHOOSE_TAC `y:real`)) THEN EXISTS_TAC `complex(x,y)` THEN CONJ_TAC THENL [MAP_EVERY UNDISCH_TAC [`subseq f`; `subseq g`] THEN REWRITE_TAC[subseq; o_THM] THEN MESON_TAC[]; ALL_TAC] THEN X_GEN_TAC `e:real` THEN DISCH_TAC THEN UNDISCH_TAC `!e. &0 < e ==> (?N. !n. N <= n ==> abs(Re(s ((f:num->num) n)) - x) < e)` THEN DISCH_THEN(MP_TAC o SPEC `e / &2`) THEN FIRST_X_ASSUM(MP_TAC o SPEC `e / &2`) THEN ASM_SIMP_TAC[REAL_LT_DIV; REAL_OF_NUM_LT; ARITH] THEN DISCH_THEN(X_CHOOSE_TAC `N2:num`) THEN DISCH_THEN(X_CHOOSE_TAC `N1:num`) THEN EXISTS_TAC `N1 + N2:num` THEN X_GEN_TAC `n:num` THEN DISCH_TAC THEN MATCH_MP_TAC REAL_LTE_TRANS THEN EXISTS_TAC `&2 * e / &2` THEN CONJ_TAC THENL [ALL_TAC; SIMP_TAC[REAL_DIV_LMUL; REAL_OF_NUM_EQ; ARITH; REAL_LE_REFL]] THEN W(MP_TAC o PART_MATCH lhand METRIC_BOUND_LEMMA o lhand o snd) THEN MATCH_MP_TAC(REAL_ARITH `a < c /\ b < c ==> x <= a + b ==> x < &2 * c`) THEN REWRITE_TAC[o_THM; RE; IM] THEN CONJ_TAC THEN FIRST_ASSUM MATCH_MP_TAC THEN ASM_MESON_TAC[LE_ADD; SEQ_SUBLE; LE_TRANS; ADD_SYM]);;
(* ------------------------------------------------------------------------- *) (* Polynomial is continuous. *) (* ------------------------------------------------------------------------- *)
let POLY_CONT = 
prove (`!p z e. &0 < e ==> ?d. &0 < d /\ !w. &0 < norm(w - z) /\ norm(w - z) < d ==> norm(poly p w - poly p z) < e`,
REPEAT STRIP_TAC THEN MP_TAC(SPECL [`z:complex`; `p:complex list`] POLY_OFFSET) THEN DISCH_THEN(X_CHOOSE_THEN `q:complex list` (MP_TAC o CONJUNCT2)) THEN DISCH_THEN(MP_TAC o GEN `w:complex` o SYM o SPEC `w - z`) THEN REWRITE_TAC[COMPLEX_SUB_ADD2] THEN DISCH_THEN(fun th -> ONCE_REWRITE_TAC[th]) THEN REWRITE_TAC[COMPLEX_SUB_REFL] THEN SPEC_TAC(`q:complex list`,`p:complex list`) THEN LIST_INDUCT_TAC THEN ASM_REWRITE_TAC[poly] THENL [EXISTS_TAC `e:real` THEN ASM_REWRITE_TAC[COMPLEX_SUB_REFL; COMPLEX_NORM_CX; REAL_ABS_NUM]; ALL_TAC] THEN REWRITE_TAC[COMPLEX_MUL_LZERO; COMPLEX_ADD_RID; COMPLEX_ADD_SUB] THEN MP_TAC(SPECL [`t:complex list`; `&1`] POLY_BOUND_EXISTS) THEN DISCH_THEN(X_CHOOSE_THEN `m:real` STRIP_ASSUME_TAC) THEN MP_TAC(SPECL [`&1`; `e / m:real`] REAL_DOWN2) THEN ASM_SIMP_TAC[REAL_LT_DIV; REAL_LT_01] THEN MATCH_MP_TAC MONO_EXISTS THEN X_GEN_TAC `d:real` THEN STRIP_TAC THEN ASM_REWRITE_TAC[] THEN X_GEN_TAC `w:complex` THEN STRIP_TAC THEN REWRITE_TAC[COMPLEX_NORM_MUL] THEN MATCH_MP_TAC REAL_LET_TRANS THEN EXISTS_TAC `d * m:real` THEN ASM_SIMP_TAC[GSYM REAL_LT_RDIV_EQ] THEN MATCH_MP_TAC REAL_LE_MUL2 THEN ASM_MESON_TAC[REAL_LT_TRANS; REAL_LT_IMP_LE; COMPLEX_NORM_POS]);;
(* ------------------------------------------------------------------------- *) (* Hence a polynomial attains minimum on a closed disc in the complex plane. *) (* ------------------------------------------------------------------------- *)
let POLY_MINIMUM_MODULUS_DISC = 
prove (`!p r. ?z. !w. norm(w) <= r ==> norm(poly p z) <= norm(poly p w)`,
let lemma = prove
   (`P /\ (m = --x) /\ --x < y <=> (--x = m) /\ P /\ m < y`,
    MESON_TAC[]) in
  REPEAT GEN_TAC THEN
  ASM_CASES_TAC `&0 <= r` THENL
   [ALL_TAC; ASM_MESON_TAC[COMPLEX_NORM_POS; REAL_LE_TRANS]] THEN
  MP_TAC(SPEC `\x. ?z. norm(z) <= r /\ (norm(poly p z) = --x)`
    REAL_SUP_EXISTS) THEN
  REWRITE_TAC[] THEN ANTS_TAC THENL
   [CONJ_TAC THENL
     [MAP_EVERY EXISTS_TAC [`--norm(poly p (Cx(&0)))`; `Cx(&0)`] THEN
      ASM_REWRITE_TAC[REAL_NEG_NEG; COMPLEX_NORM_CX; REAL_ABS_NUM];
      EXISTS_TAC `&1` THEN
      REWRITE_TAC[REAL_ARITH `(a = --b) <=> (--b = a:real)`] THEN
      REWRITE_TAC[REAL_ARITH `x < &1 <=>  --(&1) < --x`] THEN
      SIMP_TAC[LEFT_IMP_EXISTS_THM] THEN
      SIMP_TAC[REAL_ARITH `&0 <= x ==> --(&1) < x`; COMPLEX_NORM_POS]];
    ALL_TAC] THEN
  DISCH_THEN(X_CHOOSE_THEN `s:real` MP_TAC) THEN
  ONCE_REWRITE_TAC[REAL_ARITH `a < b <=> --b < --a:real`] THEN
  ABBREV_TAC `m = --s:real` THEN
  DISCH_THEN(MP_TAC o GEN `y:real` o SPEC `--y:real`) THEN
  REWRITE_TAC[REAL_NEG_NEG] THEN
  REWRITE_TAC[LEFT_AND_EXISTS_THM; GSYM CONJ_ASSOC; lemma] THEN
  ONCE_REWRITE_TAC[SWAP_EXISTS_THM] THEN
  ONCE_REWRITE_TAC[REAL_ARITH `(--a = b) <=> (a = --b:real)`] THEN
  REWRITE_TAC[LEFT_EXISTS_AND_THM; EXISTS_REFL] THEN
  DISCH_THEN(fun th -> MP_TAC th THEN MP_TAC(SPEC `m:real` th)) THEN
  REWRITE_TAC[REAL_LT_REFL; NOT_EXISTS_THM] THEN
  REWRITE_TAC[TAUT `~(a /\ b) <=> a ==> ~b`] THEN
  REWRITE_TAC[REAL_NOT_LT] THEN DISCH_TAC THEN
  DISCH_THEN(MP_TAC o GEN `n:num` o SPEC `m + inv(&(SUC n))`) THEN
  REWRITE_TAC[REAL_LT_ADDR; REAL_LT_INV_EQ; REAL_OF_NUM_LT; LT_0] THEN
  REWRITE_TAC[SKOLEM_THM; FORALL_AND_THM] THEN
  DISCH_THEN(X_CHOOSE_THEN `s:num->complex` STRIP_ASSUME_TAC) THEN
  MP_TAC(SPECL [`s:num->complex`; `r:real`]
    BOLZANO_WEIERSTRASS_COMPLEX_DISC) THEN ASM_REWRITE_TAC[] THEN
  DISCH_THEN(X_CHOOSE_THEN `f:num->num` (X_CHOOSE_THEN `z:complex`
    STRIP_ASSUME_TAC)) THEN
  EXISTS_TAC `z:complex` THEN X_GEN_TAC `w:complex` THEN DISCH_TAC THEN
  SUBGOAL_THEN `norm(poly p z) = m` (fun th -> ASM_SIMP_TAC[th]) THEN
  MATCH_MP_TAC(REAL_ARITH `~(&0 < abs(a - b)) ==> (a = b)`) THEN DISCH_TAC THEN
  ABBREV_TAC `e = abs(norm(poly p z) - m)` THEN
  MP_TAC(SPECL [`p:complex list`; `z:complex`; `e / &2`] POLY_CONT) THEN
  ASM_SIMP_TAC[REAL_LT_DIV; REAL_OF_NUM_LT; ARITH] THEN
  DISCH_THEN(X_CHOOSE_THEN `d:real` STRIP_ASSUME_TAC) THEN
  SUBGOAL_THEN `!w. norm(w - z) < d ==> norm(poly p w - poly p z) < e / &2`
  MP_TAC THENL
   [X_GEN_TAC `u:complex` THEN
    ASM_CASES_TAC `u = z:complex` THEN
    ASM_SIMP_TAC[COMPLEX_SUB_REFL; REAL_LT_DIV; REAL_OF_NUM_LT; ARITH;
                 COMPLEX_NORM_CX; REAL_ABS_NUM] THEN
    DISCH_TAC THEN FIRST_ASSUM MATCH_MP_TAC THEN ASM_REWRITE_TAC[] THEN
    ASM_REWRITE_TAC[COMPLEX_NORM_NZ; COMPLEX_SUB_0]; ALL_TAC] THEN
  FIRST_ASSUM(K ALL_TAC o check (is_conj o lhand o
    snd o dest_forall o concl)) THEN
  DISCH_TAC THEN
  FIRST_X_ASSUM(MP_TAC o SPEC `d:real`) THEN ASM_REWRITE_TAC[GE] THEN
  DISCH_THEN(X_CHOOSE_THEN `N1:num` ASSUME_TAC) THEN
  MP_TAC(SPEC `&2 / e` REAL_ARCH_SIMPLE) THEN
  DISCH_THEN(X_CHOOSE_THEN `N2:num` ASSUME_TAC) THEN
  SUBGOAL_THEN `norm(poly p (s((f:num->num) (N1 + N2))) - poly p z) < e / &2`
  MP_TAC THENL
   [FIRST_ASSUM MATCH_MP_TAC THEN ASM_SIMP_TAC[LE_ADD]; ALL_TAC] THEN
  MATCH_MP_TAC(REAL_ARITH
   `!m. abs(norm(psfn) - m) < e2 /\
        &2 * e2 <= abs(norm(psfn) - m) + norm(psfn - pz)
        ==> norm(psfn - pz) < e2 ==> F`) THEN
  EXISTS_TAC `m:real` THEN CONJ_TAC THENL
   [MATCH_MP_TAC REAL_LTE_TRANS THEN EXISTS_TAC `inv(&(SUC(N1 + N2)))` THEN
    CONJ_TAC THENL
     [MATCH_MP_TAC(REAL_ARITH
       `m <= x /\ x < m + e ==> abs(x - m:real) < e`) THEN
      ASM_SIMP_TAC[] THEN
      MATCH_MP_TAC REAL_LTE_TRANS THEN
      EXISTS_TAC `m + inv(&(SUC(f(N1 + N2:num))))` THEN
      ASM_REWRITE_TAC[REAL_LE_LADD] THEN MATCH_MP_TAC REAL_LE_INV2 THEN
      ASM_SIMP_TAC[REAL_OF_NUM_LT; REAL_OF_NUM_LE; LT_0; LE_SUC; SEQ_SUBLE];
      GEN_REWRITE_TAC RAND_CONV [GSYM REAL_INV_DIV] THEN
      MATCH_MP_TAC REAL_LE_INV2 THEN
      ASM_SIMP_TAC[REAL_LT_DIV; REAL_OF_NUM_LT; ARITH] THEN
      MATCH_MP_TAC REAL_LE_TRANS THEN EXISTS_TAC `&N2` THEN
      ASM_REWRITE_TAC[REAL_OF_NUM_LE] THEN ARITH_TAC]; ALL_TAC] THEN
  SIMP_TAC[REAL_DIV_LMUL; REAL_OF_NUM_EQ; ARITH] THEN
  EXPAND_TAC "e" THEN
  MATCH_MP_TAC(REAL_ARITH
   `abs(norm(psfn) - norm(pz)) <= norm(psfn - pz)
    ==> abs(norm(pz) - m) <= abs(norm(psfn) - m) + norm(psfn - pz)`) THEN
  REWRITE_TAC[COMPLEX_NORM_ABS_NORM]);;
(* ------------------------------------------------------------------------- *) (* Nonzero polynomial in z goes to infinity as z does. *) (* ------------------------------------------------------------------------- *)
let POLY_INFINITY = 
prove (`!p a. EX (\b. ~(b = Cx(&0))) p ==> !d. ?r. !z. r <= norm(z) ==> d <= norm(poly (CONS a p) z)`,
LIST_INDUCT_TAC THEN REWRITE_TAC[EX] THEN X_GEN_TAC `a:complex` THEN ASM_CASES_TAC `EX (\b. ~(b = Cx(&0))) t` THEN ASM_REWRITE_TAC[] THENL [X_GEN_TAC `d:real` THEN FIRST_X_ASSUM(MP_TAC o SPEC `h:complex`) THEN ASM_REWRITE_TAC[] THEN DISCH_THEN(X_CHOOSE_TAC `r:real` o SPEC `d + norm(a)`) THEN EXISTS_TAC `&1 + abs(r)` THEN X_GEN_TAC `z:complex` THEN DISCH_TAC THEN ONCE_REWRITE_TAC[poly] THEN MATCH_MP_TAC REAL_LE_TRANS THEN EXISTS_TAC `norm(z * poly (CONS h t) z) - norm(a)` THEN CONJ_TAC THENL [ALL_TAC; ONCE_REWRITE_TAC[COMPLEX_ADD_SYM] THEN REWRITE_TAC[REAL_LE_SUB_RADD; COMPLEX_NORM_TRIANGLE_SUB]] THEN REWRITE_TAC[REAL_LE_SUB_LADD] THEN MATCH_MP_TAC REAL_LE_TRANS THEN EXISTS_TAC `&1 * norm(poly (CONS h t) z)` THEN CONJ_TAC THENL [REWRITE_TAC[REAL_MUL_LID] THEN FIRST_ASSUM MATCH_MP_TAC THEN ASM_SIMP_TAC[REAL_ARITH `&1 + abs(r) <= x ==> r <= x`]; REWRITE_TAC[COMPLEX_NORM_MUL] THEN MATCH_MP_TAC REAL_LE_RMUL THEN REWRITE_TAC[COMPLEX_NORM_POS] THEN ASM_MESON_TAC[REAL_ARITH `&1 + abs(r) <= x ==> &1 <= x`]]; RULE_ASSUM_TAC(REWRITE_RULE[NOT_EX]) THEN ASM_SIMP_TAC[poly; POLY_0; COMPLEX_MUL_RZERO; COMPLEX_ADD_RID] THEN DISCH_TAC THEN X_GEN_TAC `d:real` THEN EXISTS_TAC `(abs(d) + norm(a)) / norm(h)` THEN X_GEN_TAC `z:complex` THEN ASM_SIMP_TAC[REAL_LE_LDIV_EQ; COMPLEX_NORM_NZ; GSYM COMPLEX_NORM_MUL] THEN MATCH_MP_TAC(REAL_ARITH `mzh <= mazh + ma ==> abs(d) + ma <= mzh ==> d <= mazh`) THEN ONCE_REWRITE_TAC[COMPLEX_ADD_SYM] THEN REWRITE_TAC[COMPLEX_NORM_TRIANGLE_SUB]]);;
(* ------------------------------------------------------------------------- *) (* Hence polynomial's modulus attains its minimum somewhere. *) (* ------------------------------------------------------------------------- *)
let POLY_MINIMUM_MODULUS = 
prove (`!p. ?z. !w. norm(poly p z) <= norm(poly p w)`,
LIST_INDUCT_TAC THEN REWRITE_TAC[poly; REAL_LE_REFL] THEN ASM_CASES_TAC `EX (\b. ~(b = Cx(&0))) t` THENL [FIRST_ASSUM(MP_TAC o SPEC `h:complex` o MATCH_MP POLY_INFINITY) THEN DISCH_THEN(MP_TAC o SPEC `norm(poly (CONS h t) (Cx(&0)))`) THEN DISCH_THEN(X_CHOOSE_THEN `r:real` ASSUME_TAC) THEN MP_TAC(SPECL [`CONS (h:complex) t`; `abs(r)`] POLY_MINIMUM_MODULUS_DISC) THEN REWRITE_TAC[GSYM(CONJUNCT2 poly)] THEN ASM_MESON_TAC[REAL_ARITH `r <= z \/ z <= abs(r)`; REAL_LE_TRANS; COMPLEX_NORM_CX; REAL_ABS_NUM; REAL_ABS_POS]; FIRST_ASSUM(MP_TAC o GEN_REWRITE_RULE I [NOT_EX]) THEN REWRITE_TAC[] THEN DISCH_THEN(ASSUME_TAC o MATCH_MP POLY_0) THEN ASM_REWRITE_TAC[COMPLEX_MUL_RZERO; REAL_LE_REFL]]);;
(* ------------------------------------------------------------------------- *) (* Constant function (non-syntactic characterization). *) (* ------------------------------------------------------------------------- *)
let constant = new_definition
  `constant f = !w z. f(w) = f(z)`;;
let NONCONSTANT_LENGTH = 
prove (`!p. ~constant(poly p) ==> 2 <= LENGTH p`,
REWRITE_TAC[constant] THEN LIST_INDUCT_TAC THEN REWRITE_TAC[poly] THEN REWRITE_TAC[LENGTH; ARITH_RULE `2 <= SUC n <=> ~(n = 0)`] THEN SIMP_TAC[TAUT `~a ==> ~b <=> b ==> a`; LENGTH_EQ_NIL; poly] THEN REWRITE_TAC[COMPLEX_MUL_RZERO]);;
(* ------------------------------------------------------------------------- *) (* Decomposition of polynomial, skipping zero coefficients after the first. *) (* ------------------------------------------------------------------------- *)
let POLY_DECOMPOSE_LEMMA = 
prove (`!p. ~(!z. ~(z = Cx(&0)) ==> (poly p z = Cx(&0))) ==> ?k a q. ~(a = Cx(&0)) /\ (SUC(LENGTH q + k) = LENGTH p) /\ !z. poly p z = z pow k * poly (CONS a q) z`,
LIST_INDUCT_TAC THENL [REWRITE_TAC[poly]; ALL_TAC] THEN ASM_CASES_TAC `h = Cx(&0)` THENL [GEN_REWRITE_TAC (LAND_CONV o ONCE_DEPTH_CONV) [poly] THEN ASM_SIMP_TAC[COMPLEX_ADD_LID; COMPLEX_ENTIRE] THEN DISCH_THEN(ANTE_RES_THEN MP_TAC) THEN DISCH_THEN(X_CHOOSE_THEN `k:num` (X_CHOOSE_THEN `a:complex` (X_CHOOSE_THEN `q:complex list` STRIP_ASSUME_TAC))) THEN MAP_EVERY EXISTS_TAC [`k + 1`; `a:complex`; `q:complex list`] THEN ASM_REWRITE_TAC[poly; LENGTH; GSYM ADD1; ADD_CLAUSES] THEN REWRITE_TAC[COMPLEX_ADD_LID; complex_pow; GSYM COMPLEX_MUL_ASSOC]; DISCH_THEN(K ALL_TAC) THEN MAP_EVERY EXISTS_TAC [`0`; `h:complex`; `t:complex list`] THEN ASM_REWRITE_TAC[complex_pow; COMPLEX_MUL_LID; ADD_CLAUSES; LENGTH]]);;
let POLY_DECOMPOSE = 
prove (`!p. ~constant(poly p) ==> ?k a q. ~(a = Cx(&0)) /\ ~(k = 0) /\ (LENGTH q + k + 1 = LENGTH p) /\ !z. poly p z = poly p (Cx(&0)) + z pow k * poly (CONS a q) z`,
LIST_INDUCT_TAC THENL [REWRITE_TAC[constant; poly]; ALL_TAC] THEN POP_ASSUM(K ALL_TAC) THEN DISCH_TAC THEN MP_TAC(SPEC `t:complex list` POLY_DECOMPOSE_LEMMA) THEN ANTS_TAC THENL [POP_ASSUM MP_TAC THEN REWRITE_TAC[constant; poly] THEN REWRITE_TAC[TAUT `~b ==> ~a <=> a ==> b`; COMPLEX_EQ_ADD_LCANCEL] THEN SIMP_TAC[TAUT `~a ==> b <=> a \/ b`; GSYM COMPLEX_ENTIRE]; ALL_TAC] THEN DISCH_THEN(X_CHOOSE_THEN `k:num` (X_CHOOSE_THEN `a:complex` (X_CHOOSE_THEN `q:complex list` STRIP_ASSUME_TAC))) THEN MAP_EVERY EXISTS_TAC [`SUC k`; `a:complex`; `q:complex list`] THEN ASM_REWRITE_TAC[ADD_CLAUSES; GSYM ADD1; LENGTH; NOT_SUC] THEN ASM_REWRITE_TAC[poly; COMPLEX_MUL_LZERO; COMPLEX_ADD_RID; complex_pow] THEN REWRITE_TAC[GSYM COMPLEX_MUL_ASSOC]);;
let POLY_REPLICATE_APPEND = 
prove (`!n p x. poly (APPEND (REPLICATE n (Cx(&0))) p) x = x pow n * poly p x`,
INDUCT_TAC THEN REWRITE_TAC[REPLICATE; APPEND; complex_pow; COMPLEX_MUL_LID] THEN ASM_REWRITE_TAC[poly; COMPLEX_ADD_LID] THEN REWRITE_TAC[COMPLEX_MUL_ASSOC]);;
(* ------------------------------------------------------------------------- *) (* Fundamental theorem. *) (* ------------------------------------------------------------------------- *)
let FUNDAMENTAL_THEOREM_OF_ALGEBRA = 
prove (`!p. ~constant(poly p) ==> ?z. poly p z = Cx(&0)`,
SUBGOAL_THEN `!n p. (LENGTH p = n) /\ ~constant(poly p) ==> ?z. poly p z = Cx(&0)` (fun th -> MESON_TAC[th]) THEN MATCH_MP_TAC num_WF THEN X_GEN_TAC `n:num` THEN STRIP_TAC THEN X_GEN_TAC `p:complex list` THEN STRIP_TAC THEN FIRST_ASSUM(MP_TAC o MATCH_MP NONCONSTANT_LENGTH) THEN ASM_REWRITE_TAC[] THEN DISCH_TAC THEN X_CHOOSE_TAC `c:complex` (SPEC `p:complex list` POLY_MINIMUM_MODULUS) THEN ASM_CASES_TAC `poly p c = Cx(&0)` THENL [ASM_MESON_TAC[]; ALL_TAC] THEN MP_TAC(SPECL [`c:complex`; `p:complex list`] POLY_OFFSET) THEN DISCH_THEN(X_CHOOSE_THEN `q:complex list` MP_TAC) THEN DISCH_THEN(CONJUNCTS_THEN2 (SUBST_ALL_TAC o SYM) ASSUME_TAC) THEN SUBGOAL_THEN `~constant(poly q)` ASSUME_TAC THENL [UNDISCH_TAC `~(constant(poly p))` THEN SUBGOAL_THEN `!z. poly q (z - c) = poly p z` (fun th -> MESON_TAC[th; constant]) THEN ASM_MESON_TAC[SIMPLE_COMPLEX_ARITH `a + (x - a) = x`]; ALL_TAC] THEN SUBGOAL_THEN `poly p c = poly q (Cx(&0))` SUBST_ALL_TAC THENL [ASM_MESON_TAC[COMPLEX_ADD_RID]; ALL_TAC] THEN SUBGOAL_THEN `!w. norm(poly q (Cx(&0))) <= norm(poly q w)` MP_TAC THENL [ASM_MESON_TAC[]; ALL_TAC] THEN POP_ASSUM_LIST(MAP_EVERY (fun th -> if free_in `p:complex list` (concl th) then ALL_TAC else ASSUME_TAC th)) THEN MATCH_MP_TAC(TAUT `~a ==> a ==> b`) THEN REWRITE_TAC[NOT_FORALL_THM; REAL_NOT_LE] THEN ABBREV_TAC `a0 = poly q (Cx(&0))` THEN SUBGOAL_THEN `!z. poly q z = poly (MAP (( * ) (inv(a0))) q) z * a0` ASSUME_TAC THENL [REWRITE_TAC[POLY_CMUL_MAP] THEN ONCE_REWRITE_TAC[AC COMPLEX_MUL_AC `(a * b) * c = b * c * a`] THEN ASM_SIMP_TAC[COMPLEX_MUL_RINV; COMPLEX_MUL_RID]; ALL_TAC] THEN ABBREV_TAC `r = MAP (( * ) (inv(a0))) q` THEN SUBGOAL_THEN `LENGTH(q:complex list) = LENGTH(r:complex list)` SUBST_ALL_TAC THENL [EXPAND_TAC "r" THEN REWRITE_TAC[LENGTH_MAP]; ALL_TAC] THEN SUBGOAL_THEN `~(constant(poly r))` ASSUME_TAC THENL [UNDISCH_TAC `~constant(poly q)` THEN ASM_REWRITE_TAC[constant; COMPLEX_EQ_MUL_RCANCEL] THEN MESON_TAC[]; ALL_TAC] THEN SUBGOAL_THEN `poly r (Cx(&0)) = Cx(&1)` ASSUME_TAC THENL [FIRST_X_ASSUM(MP_TAC o SPEC `Cx(&0)`) THEN ASM_REWRITE_TAC[] THEN GEN_REWRITE_TAC (LAND_CONV o LAND_CONV) [GSYM COMPLEX_MUL_LID] THEN ASM_SIMP_TAC[COMPLEX_EQ_MUL_RCANCEL]; ALL_TAC] THEN ASM_REWRITE_TAC[] THEN POP_ASSUM_LIST(MAP_EVERY (fun th -> if free_in `q:complex list` (concl th) then ALL_TAC else ASSUME_TAC th)) THEN ASM_SIMP_TAC[GSYM REAL_LT_RDIV_EQ; COMPLEX_NORM_NZ; COMPLEX_NORM_MUL; REAL_DIV_REFL; COMPLEX_NORM_ZERO] THEN FIRST_ASSUM(MP_TAC o MATCH_MP POLY_DECOMPOSE) THEN DISCH_THEN(X_CHOOSE_THEN `k:num` (X_CHOOSE_THEN `a:complex` (X_CHOOSE_THEN `s:complex list` MP_TAC))) THEN DISCH_THEN(CONJUNCTS_THEN2 ASSUME_TAC MP_TAC) THEN DISCH_THEN(CONJUNCTS_THEN2 ASSUME_TAC MP_TAC) THEN DISCH_THEN(CONJUNCTS_THEN2 (SUBST_ALL_TAC o SYM) MP_TAC) THEN DISCH_THEN(fun th -> ONCE_REWRITE_TAC[th]) THEN ASM_REWRITE_TAC[] THEN ASM_CASES_TAC `k + 1 = n` THENL [UNDISCH_TAC `LENGTH(s:complex list) + k + 1 = n` THEN ASM_REWRITE_TAC[ARITH_RULE `(s + m = m) <=> (s = 0)`; LENGTH_EQ_NIL] THEN REWRITE_TAC[LENGTH_EQ_NIL] THEN DISCH_THEN SUBST1_TAC THEN REWRITE_TAC[poly; COMPLEX_MUL_RZERO; COMPLEX_ADD_RID] THEN ONCE_REWRITE_TAC[COMPLEX_MUL_SYM] THEN MATCH_MP_TAC REDUCE_POLY_SIMPLE THEN ASM_REWRITE_TAC[] THEN MAP_EVERY UNDISCH_TAC [`k + 1 = n`; `2 <= n`] THEN ARITH_TAC; ALL_TAC] THEN FIRST_X_ASSUM(MP_TAC o SPEC `k + 1`) THEN ANTS_TAC THENL [UNDISCH_TAC `~(k + 1 = n)` THEN UNDISCH_TAC `LENGTH(s:complex list) + k + 1 = n` THEN ARITH_TAC; ALL_TAC] THEN DISCH_THEN(MP_TAC o SPEC `CONS (Cx(&1)) (APPEND (REPLICATE (k - 1) (Cx(&0))) [a])`) THEN ANTS_TAC THENL [CONJ_TAC THENL [REWRITE_TAC[LENGTH; LENGTH_APPEND; LENGTH_REPLICATE] THEN UNDISCH_TAC `~(k = 0)` THEN ARITH_TAC; ALL_TAC] THEN REWRITE_TAC[constant; POLY_REPLICATE_APPEND; poly] THEN REWRITE_TAC[COMPLEX_MUL_RZERO; COMPLEX_ADD_RID] THEN DISCH_THEN(MP_TAC o SPECL [`Cx(&0)`; `Cx(&1)`]) THEN REWRITE_TAC[COMPLEX_MUL_LID; COMPLEX_MUL_LZERO; COMPLEX_ADD_RID] THEN ASM_REWRITE_TAC[COMPLEX_ENTIRE; COMPLEX_POW_ONE; SIMPLE_COMPLEX_ARITH `(a = a + b) <=> (b = Cx(&0))`] THEN REWRITE_TAC[CX_INJ; REAL_OF_NUM_EQ; ARITH_EQ]; ALL_TAC] THEN REWRITE_TAC[constant; POLY_REPLICATE_APPEND; poly] THEN REWRITE_TAC[COMPLEX_MUL_RZERO; COMPLEX_ADD_RID] THEN ONCE_REWRITE_TAC[AC COMPLEX_MUL_AC `a * b * c = (a * b) * c`] THEN REWRITE_TAC[GSYM(CONJUNCT2 complex_pow)] THEN ASM_SIMP_TAC[ARITH_RULE `~(k = 0) ==> (SUC(k - 1) = k)`] THEN DISCH_THEN(X_CHOOSE_TAC `w:complex`) THEN MP_TAC(SPECL [`s:complex list`; `norm(w)`] POLY_BOUND_EXISTS) THEN DISCH_THEN(X_CHOOSE_THEN `m:real` STRIP_ASSUME_TAC) THEN SUBGOAL_THEN `~(w = Cx(&0))` ASSUME_TAC THENL [UNDISCH_TAC `Cx(&1) + w pow k * a = Cx(&0)` THEN ONCE_REWRITE_TAC[TAUT `a ==> ~b <=> b ==> ~a`] THEN DISCH_THEN SUBST1_TAC THEN UNDISCH_TAC `~(k = 0)` THEN SPEC_TAC(`k:num`,`k:num`) THEN INDUCT_TAC THEN REWRITE_TAC[complex_pow; COMPLEX_MUL_LZERO] THEN REWRITE_TAC[COMPLEX_ADD_RID; CX_INJ; REAL_OF_NUM_EQ; ARITH_EQ]; ALL_TAC] THEN MP_TAC(SPECL [`&1`; `inv(norm(w) pow (k + 1) * m)`] REAL_DOWN2) THEN ASM_SIMP_TAC[REAL_LT_01; REAL_LT_INV_EQ; REAL_LT_MUL; REAL_POW_LT; COMPLEX_NORM_NZ] THEN DISCH_THEN(X_CHOOSE_THEN `t:real` STRIP_ASSUME_TAC) THEN EXISTS_TAC `Cx(t) * w` THEN REWRITE_TAC[COMPLEX_POW_MUL] THEN REWRITE_TAC[COMPLEX_ADD_LDISTRIB; GSYM COMPLEX_MUL_ASSOC] THEN FIRST_ASSUM(SUBST1_TAC o MATCH_MP (SIMPLE_COMPLEX_ARITH `(a + w = Cx(&0)) ==> (w = --a)`)) THEN REWRITE_TAC[GSYM CX_NEG; GSYM CX_POW; GSYM CX_MUL] THEN REWRITE_TAC[COMPLEX_ADD_ASSOC; GSYM CX_ADD] THEN MATCH_MP_TAC REAL_LET_TRANS THEN EXISTS_TAC `norm(Cx(&1 + t pow k * -- &1)) + norm(Cx(t pow k) * w pow k * Cx t * w * poly s (Cx t * w))` THEN REWRITE_TAC[COMPLEX_NORM_TRIANGLE] THEN REWRITE_TAC[COMPLEX_NORM_CX] THEN MATCH_MP_TAC(REAL_ARITH `&0 <= x /\ x < t /\ t <= &1 ==> abs(&1 + t * --(&1)) + x < &1`) THEN REWRITE_TAC[COMPLEX_NORM_POS] THEN ASM_SIMP_TAC[REAL_POW_1_LE; REAL_LT_IMP_LE] THEN ONCE_REWRITE_TAC[COMPLEX_NORM_MUL] THEN REWRITE_TAC[COMPLEX_NORM_CX] THEN ASM_SIMP_TAC[real_abs; REAL_LT_IMP_LE; REAL_POW_LE] THEN GEN_REWRITE_TAC RAND_CONV [GSYM REAL_MUL_RID] THEN MATCH_MP_TAC REAL_LT_LMUL THEN ASM_SIMP_TAC[REAL_POW_LT] THEN ONCE_REWRITE_TAC[AC COMPLEX_MUL_AC `a * b * c * d = b * (c * a) * d`] THEN REWRITE_TAC[GSYM(CONJUNCT2 complex_pow)] THEN REWRITE_TAC[COMPLEX_NORM_MUL; ADD1; COMPLEX_NORM_CX] THEN MATCH_MP_TAC REAL_LET_TRANS THEN EXISTS_TAC `abs t * norm(w pow (k + 1)) * m` THEN CONJ_TAC THENL [MATCH_MP_TAC REAL_LE_LMUL THEN REWRITE_TAC[REAL_ABS_POS] THEN MATCH_MP_TAC REAL_LE_LMUL THEN REWRITE_TAC[COMPLEX_NORM_POS] THEN FIRST_ASSUM MATCH_MP_TAC THEN REWRITE_TAC[COMPLEX_NORM_MUL] THEN GEN_REWRITE_TAC RAND_CONV [GSYM REAL_MUL_LID] THEN MATCH_MP_TAC REAL_LE_RMUL THEN REWRITE_TAC[COMPLEX_NORM_POS] THEN ASM_SIMP_TAC[COMPLEX_NORM_CX; REAL_ARITH `&0 < t /\ t < &1 ==> abs(t) <= &1`]; ALL_TAC] THEN ASM_SIMP_TAC[GSYM REAL_LT_RDIV_EQ; REAL_LT_MUL; COMPLEX_NORM_POW; REAL_POW_LT; COMPLEX_NORM_NZ] THEN ASM_SIMP_TAC[real_div; REAL_MUL_LID; REAL_ARITH `&0 < t /\ t < x ==> abs(t) < x`]);;
(* ------------------------------------------------------------------------- *) (* Alternative version with a syntactic notion of constant polynomial. *) (* ------------------------------------------------------------------------- *)
let FUNDAMENTAL_THEOREM_OF_ALGEBRA_ALT = 
prove (`!p. ~(?a l. ~(a = Cx(&0)) /\ ALL (\b. b = Cx(&0)) l /\ (p = CONS a l)) ==> ?z. poly p z = Cx(&0)`,
LIST_INDUCT_TAC THEN REWRITE_TAC[poly; CONS_11] THEN POP_ASSUM_LIST(K ALL_TAC) THEN ONCE_REWRITE_TAC[AC CONJ_ACI `a /\ b /\ c /\ d <=> c /\ d /\ a /\ b`] THEN REWRITE_TAC[RIGHT_EXISTS_AND_THM; UNWIND_THM1] THEN ASM_CASES_TAC `h = Cx(&0)` THEN ASM_REWRITE_TAC[COMPLEX_ADD_LID] THENL [EXISTS_TAC `Cx(&0)` THEN ASM_REWRITE_TAC[COMPLEX_MUL_LZERO]; ALL_TAC] THEN DISCH_TAC THEN REWRITE_TAC[GSYM(CONJUNCT2 poly)] THEN MATCH_MP_TAC FUNDAMENTAL_THEOREM_OF_ALGEBRA THEN UNDISCH_TAC `~ALL (\b. b = Cx (&0)) t` THEN REWRITE_TAC[TAUT `~b ==> ~a <=> a ==> b`] THEN POP_ASSUM(K ALL_TAC) THEN REWRITE_TAC[constant; poly; REAL_EQ_LADD] THEN DISCH_THEN(MP_TAC o SPEC `Cx(&0)` o ONCE_REWRITE_RULE[SWAP_FORALL_THM]) THEN REWRITE_TAC[COMPLEX_MUL_LZERO; COMPLEX_EQ_ADD_LCANCEL] THEN REWRITE_TAC[COMPLEX_ENTIRE; TAUT `a \/ b <=> ~a ==> b`] THEN SPEC_TAC(`t:complex list`,`p:complex list`) THEN LIST_INDUCT_TAC THEN REWRITE_TAC[ALL] THEN ASM_CASES_TAC `h = Cx(&0)` THEN ASM_SIMP_TAC[poly; COMPLEX_ADD_LID; COMPLEX_ENTIRE] THEN MP_TAC(SPECL [`t:complex list`; `&1`] POLY_BOUND_EXISTS) THEN DISCH_THEN(X_CHOOSE_THEN `m:real` STRIP_ASSUME_TAC) THEN MP_TAC(SPECL [`norm(h) / m`; `&1`] REAL_DOWN2) THEN ASM_SIMP_TAC[REAL_LT_01; REAL_LT_DIV; COMPLEX_NORM_NZ] THEN DISCH_THEN(X_CHOOSE_THEN `x:real` STRIP_ASSUME_TAC) THEN DISCH_THEN(MP_TAC o SPEC `Cx(x)`) THEN ASM_SIMP_TAC[CX_INJ; REAL_LT_IMP_NZ] THEN REWRITE_TAC[SIMPLE_COMPLEX_ARITH `(x + y = Cx(&0)) <=> (y = --x)`] THEN DISCH_THEN(MP_TAC o AP_TERM `norm`) THEN REWRITE_TAC[COMPLEX_NORM_NEG] THEN MATCH_MP_TAC(REAL_ARITH `abs(a) < abs(b) ==> ~(a = b)`) THEN REWRITE_TAC[real_abs; COMPLEX_NORM_POS] THEN REWRITE_TAC[COMPLEX_NORM_MUL; COMPLEX_NORM_CX] THEN MATCH_MP_TAC REAL_LTE_TRANS THEN EXISTS_TAC `norm(h) / m * m` THEN CONJ_TAC THENL [ALL_TAC; ASM_SIMP_TAC[REAL_LE_REFL; REAL_DIV_RMUL; REAL_LT_IMP_NZ]] THEN MATCH_MP_TAC REAL_LET_TRANS THEN EXISTS_TAC `abs(x) * m` THEN ASM_SIMP_TAC[REAL_LT_RMUL; REAL_ARITH `&0 < x /\ x < a ==> abs(x) < a`] THEN ASM_MESON_TAC[REAL_LE_LMUL; REAL_ABS_POS; COMPLEX_NORM_CX; REAL_ARITH `&0 < x /\ x < &1 ==> abs(x) <= &1`]);;