let R be finite domRing; :: thesis: not R is algebraic-closed

ex q being Polynomial of R st

( len q > 1 & not q is with_roots )

ex q being Polynomial of R st

( len q > 1 & not q is with_roots )

proof

hence
not R is algebraic-closed
by POLYNOM5:def 9; :: thesis: verum
set p = the Ppoly of R,([#] the carrier of R);

take q = the Ppoly of R,([#] the carrier of R) + (1_. R); :: thesis: ( len q > 1 & not q is with_roots )

A: deg the Ppoly of R,([#] the carrier of R) >= card ([#] the carrier of R) by m00;

then B: deg the Ppoly of R,([#] the carrier of R) >= 1 by NAT_1:14;

C: deg the Ppoly of R,([#] the carrier of R) > deg (1_. R) by A, RATFUNC1:def 2;

then deg q = max ((deg the Ppoly of R,([#] the carrier of R)),(deg (1_. R))) by HURWITZ:21

.= deg the Ppoly of R,([#] the carrier of R) by C, XXREAL_0:def 10 ;

then (len q) - 1 >= 1 by B, HURWITZ:def 2;

then ((len q) - 1) + 1 >= 1 + 1 by XREAL_1:6;

hence len q > 1 by NAT_1:13; :: thesis: not q is with_roots

end;take q = the Ppoly of R,([#] the carrier of R) + (1_. R); :: thesis: ( len q > 1 & not q is with_roots )

A: deg the Ppoly of R,([#] the carrier of R) >= card ([#] the carrier of R) by m00;

then B: deg the Ppoly of R,([#] the carrier of R) >= 1 by NAT_1:14;

C: deg the Ppoly of R,([#] the carrier of R) > deg (1_. R) by A, RATFUNC1:def 2;

then deg q = max ((deg the Ppoly of R,([#] the carrier of R)),(deg (1_. R))) by HURWITZ:21

.= deg the Ppoly of R,([#] the carrier of R) by C, XXREAL_0:def 10 ;

then (len q) - 1 >= 1 by B, HURWITZ:def 2;

then ((len q) - 1) + 1 >= 1 + 1 by XREAL_1:6;

hence len q > 1 by NAT_1:13; :: thesis: not q is with_roots

D: now :: thesis: for a being Element of R holds eval (q,a) = (0. R) + (1. R)

let a be Element of R; :: thesis: eval (q,a) = (0. R) + (1. R)

a in the carrier of R ;

then D1: a in [#] the carrier of R by SUBSET_1:def 3;

thus eval (q,a) = (eval ( the Ppoly of R,([#] the carrier of R),a)) + (eval ((1_. R),a)) by POLYNOM4:19

.= (0. R) + (eval ((1_. R),a)) by D1, m1

.= (0. R) + (1. R) by POLYNOM4:18 ; :: thesis: verum

end;a in the carrier of R ;

then D1: a in [#] the carrier of R by SUBSET_1:def 3;

thus eval (q,a) = (eval ( the Ppoly of R,([#] the carrier of R),a)) + (eval ((1_. R),a)) by POLYNOM4:19

.= (0. R) + (eval ((1_. R),a)) by D1, m1

.= (0. R) + (1. R) by POLYNOM4:18 ; :: thesis: verum

now :: thesis: not q is with_roots

hence
not q is with_roots
; :: thesis: verumassume
q is with_roots
; :: thesis: contradiction

then consider a being Element of R such that

H: a is_a_root_of q by POLYNOM5:def 8;

0. R = eval (q,a) by H, POLYNOM5:def 7

.= 1. R by D ;

hence contradiction ; :: thesis: verum

end;then consider a being Element of R such that

H: a is_a_root_of q by POLYNOM5:def 8;

0. R = eval (q,a) by H, POLYNOM5:def 7

.= 1. R by D ;

hence contradiction ; :: thesis: verum