let R be finite domRing; 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);
( 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;
not q is with_roots
hence
not
q is
with_roots
;
verum
end;
hence
not R is algebraic-closed
by POLYNOM5:def 9; verum