let R be Field; :: thesis: ( R is algebraic-closed iff for p being monic Element of the carrier of (Polynom-Ring R) holds
( p is irreducible iff deg p = 1 ) )

now :: thesis: ( ( for p being monic Element of the carrier of (Polynom-Ring R) holds
( p is irreducible iff deg p = 1 ) ) implies R is algebraic-closed )

assume AS: for p being monic Element of the carrier of (Polynom-Ring R) holds
( p is irreducible iff deg p = 1 ) ; :: thesis: R is algebraic-closed

now :: thesis: for p being Polynomial of R st len p > 1 holds
p is with_roots

let p be Polynomial of R; :: thesis: ( len p > 1 implies p is with_roots )
assume A: len p > 1 ; :: thesis: p is with_roots
then A1: p <> 0_. R by POLYNOM4:3;
A4: (len p) - 1 > 1 - 1 by A, XREAL_1:9;
then deg p is Element of NAT by INT_1:3;
then A3: deg p >= 1 by NAT_1:14, A4;
defpred S₁[ Nat] means for p being Polynomial of R st deg p = $1 holds
p is with_roots ;
II: for k being Nat st k >= 1 & ( for n being Nat st n >= 1 & n < k holds
S₁[n] ) holds
S₁[k]

proof

let k be Nat; :: thesis: ( k >= 1 & ( for n being Nat st n >= 1 & n < k holds
S₁[n] ) implies S₁[k] )
assume IAS: ( k >= 1 & ( for n being Nat st n >= 1 & n < k holds
S₁[n] ) ) ; :: thesis: S₁[k]

per cases ( k = 1 or k > 1 ) by IAS, XXREAL_0:1;

suppose IA1: k = 1 ; :: thesis: S₁[k]

thus S₁[k] :: thesis: verum

proof

now :: thesis: for p being Polynomial of R st deg p = 1 holds
p is with_roots

let p be Polynomial of R; :: thesis: ( deg p = 1 implies p is with_roots )
assume deg p = 1 ; :: thesis: p is with_roots
then consider x, z being Element of R such that
I1: ( x <> 0. R & p = x * (rpoly (1,z)) ) by HURWITZ:28;
eval (p,z) = x * (eval ((rpoly (1,z)),z)) by I1, POLYNOM5:30
.= x * (z - z) by HURWITZ:29
.= x * (0. R) by RLVECT_1:15 ;
hence p is with_roots by POLYNOM5:def 8, POLYNOM5:def 7; :: thesis: verum

end;

hence S₁[k] by IA1; :: thesis: verum

end;

end;

suppose IA1: k > 1 ; :: thesis: S₁[k]

thus S₁[k] :: thesis: verum

proof

now :: thesis: for p being Polynomial of R st deg p = k holds
p is with_roots

let p be Polynomial of R; :: thesis: ( deg p = k implies p is with_roots )
reconsider pp = p as Element of (Polynom-Ring R) by POLYNOM3:def 10;
set q = NormPolynomial p;
reconsider qq = NormPolynomial p as Element of (Polynom-Ring R) by POLYNOM3:def 10;
assume K: deg p = k ; :: thesis: p is with_roots
then len p <> 0 ;
then I3: deg (NormPolynomial p) > 1 by K, IA1, POLYNOM5:57;
p <> 0_. R by K, HURWITZ:20;
then not p is zero by UPROOTS:def 5;
then I4: qq is reducible by AS, I3;
I5: pp <> 0_. R by K, HURWITZ:20;
p is not Unit of (Polynom-Ring R) by T8, K, IA1;
then consider r being Element of the carrier of (Polynom-Ring R) such that
I6: ( r divides p & 1 <= deg r & deg r < deg p ) by I4, I5, T88b, thirr2;
r <> 0_. R by I6, HURWITZ:20;
then deg r is Element of NAT by T8b;
then consider x being Element of R such that
I8: x is_a_root_of r by K, I6, IAS, POLYNOM5:def 8;
reconsider rr = r, ppp = p as Element of (Polynom-Ring R) by POLYNOM3:def 10;
rr divides ppp by I6;
then consider u being Element of the carrier of (Polynom-Ring R) such that
I10: ppp = rr * u ;
p = r *' u by I10, POLYNOM3:def 10;
then eval (p,x) = (eval (r,x)) * (eval (u,x)) by POLYNOM4:24
.= (0. R) * (eval (u,x)) by I8, POLYNOM5:def 7
.= 0. R ;
hence p is with_roots by POLYNOM5:def 8, POLYNOM5:def 7; :: thesis: verum

end;

hence S₁[k] ; :: thesis: verum

end;

end;

end;

end;

I: for k being Nat st 1 <= k holds
S₁[k] from NAT_1:sch 9(II);
deg p is Element of NAT by A1, T8b;
then consider n being Nat such that
H: ( n >= 1 & deg p = n ) by A3;
thus p is with_roots by H, I; :: thesis: verum

end;

hence R is algebraic-closed by POLYNOM5:def 9; :: thesis: verum

end;

hence ( R is algebraic-closed iff for p being monic Element of the carrier of (Polynom-Ring R) holds
( p is irreducible iff deg p = 1 ) ) by thirr1; :: thesis: verum