let R be Field; :: thesis: for p being Element of the carrier of (Polynom-Ring R) holds
( ( p = 0_. R or p is Unit of (Polynom-Ring R) or ex q being Element of the carrier of (Polynom-Ring R) st
( q divides p & 1 <= deg q & deg q < deg p ) ) iff p is reducible )
let p be Element of the carrier of (Polynom-Ring R); :: thesis: ( ( p = 0_. R or p is Unit of (Polynom-Ring R) or ex q being Element of the carrier of (Polynom-Ring R) st
( q divides p & 1 <= deg q & deg q < deg p ) ) iff p is reducible )
set K = Polynom-Ring R;
reconsider pp = p as Polynomial of R ;

A: now :: thesis: ( not p is reducible or p = 0_. R or p is Unit of (Polynom-Ring R) or ex q being Element of the carrier of (Polynom-Ring R) st
( q divides p & 1 <= deg q & deg q < deg p ) )

assume p is reducible ; :: thesis: ( p = 0_. R or p is Unit of (Polynom-Ring R) or ex q being Element of the carrier of (Polynom-Ring R) st
( q divides p & 1 <= deg q & deg q < deg p ) )
then AS: ( p = 0. (Polynom-Ring R) or p is Unit of (Polynom-Ring R) or ex a being Element of (Polynom-Ring R) st
( a divides p & a is not Unit of (Polynom-Ring R) & not a is_associated_to p ) ) by RING_2:def 9;
thus ( p = 0_. R or p is Unit of (Polynom-Ring R) or ex q being Element of the carrier of (Polynom-Ring R) st
( q divides p & 1 <= deg q & deg q < deg p ) ) :: thesis: verum

proof

assume A0: ( not p = 0_. R & p is not Unit of (Polynom-Ring R) ) ; :: thesis: ex q being Element of the carrier of (Polynom-Ring R) st
( q divides p & 1 <= deg q & deg q < deg p )
then consider a being Element of (Polynom-Ring R) such that
A1: ( a divides p & a is not Unit of (Polynom-Ring R) & not a is_associated_to p ) by AS, POLYNOM3:def 10;
reconsider q = a as Polynomial of R by POLYNOM3:def 10;
q divides pp by A1;
then consider r being Polynomial of R such that
A2: pp = q *' r by T2;
reconsider rr = r as Element of (Polynom-Ring R) by POLYNOM3:def 10;
A10: p = a * rr by A2, POLYNOM3:def 10;
A5: q <> 0_. R by A0, A2, POLYNOM3:34;
A6: r <> 0_. R by A0, A2, POLYNOM3:34;
then A9: deg p = (deg q) + (deg r) by A2, A5, HURWITZ:23;
A11: ( deg q is Element of NAT & deg r is Element of NAT ) by A5, A6, T8b;
then A7: deg q <= deg p by A9, NAT_1:11;

A3: now :: thesis: not deg q = deg p

assume deg q = deg p ; :: thesis: contradiction
then rr is Unit of (Polynom-Ring R) by A9, T8;
hence contradiction by A1, A10, GCD_1:18; :: thesis: verum

end;

thus ex b being Element of the carrier of (Polynom-Ring R) st
( b divides p & 1 <= deg b & deg b < deg p ) :: thesis: verum

proof

reconsider qq = q as Element of the carrier of (Polynom-Ring R) ;
take qq ; :: thesis: ( qq divides p & 1 <= deg qq & deg qq < deg p )
thus qq divides p by A1; :: thesis: ( 1 <= deg qq & deg qq < deg p )
thus 1 <= deg qq by A1, A11, T8, NAT_1:14; :: thesis: deg qq < deg p
thus deg qq < deg p by A3, A7, XXREAL_0:1; :: thesis: verum

end;

end;

end;

now :: thesis: ( ( p = 0_. R or p is Unit of (Polynom-Ring R) or ex q being Element of the carrier of (Polynom-Ring R) st
( q divides p & 1 <= deg q & deg q < deg p ) ) implies p is reducible )

assume AS: ( p = 0_. R or p is Unit of (Polynom-Ring R) or ex q being Element of the carrier of (Polynom-Ring R) st
( q divides p & 1 <= deg q & deg q < deg p ) ) ; :: thesis: p is reducible

per cases ( p = 0_. R or p is Unit of (Polynom-Ring R) or ex q being Element of the carrier of (Polynom-Ring R) st
( q divides p & 1 <= deg q & deg q < deg p ) ) by AS;

suppose p = 0_. R ; :: thesis: p is reducible

then p = 0. (Polynom-Ring R) by POLYNOM3:def 10;
hence p is reducible ; :: thesis: verum

end;

suppose p is Unit of (Polynom-Ring R) ; :: thesis: p is reducible

hence p is reducible ; :: thesis: verum

end;

suppose ex q being Element of the carrier of (Polynom-Ring R) st
( q divides p & 1 <= deg q & deg q < deg p ) ; :: thesis: p is reducible

hence p is reducible by T88a; :: thesis: verum

end;

end;

end;

hence ( ( p = 0_. R or p is Unit of (Polynom-Ring R) or ex q being Element of the carrier of (Polynom-Ring R) st
( q divides p & 1 <= deg q & deg q < deg p ) ) iff p is reducible ) by A; :: thesis: verum