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 )
proof
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
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;
now :: thesis: not q is with_roots
assume 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;
hence not q is with_roots ; :: thesis: verum
end;
hence not R is algebraic-closed by POLYNOM5:def 9; :: thesis: verum