let p be Element of the carrier of (Polynom-Ring F); :: thesis: ( not p is linear & p is with_roots implies p is reducible )

assume AS: ( not p is linear & p is with_roots ) ; :: thesis: p is reducible

then consider a being Element of F such that

A: a is_a_root_of p by POLYNOM5:def 8;

consider q1 being Polynomial of F such that

B: p = (rpoly (1,a)) *' q1 by A, HURWITZ:33;

reconsider q = q1 as Element of the carrier of (Polynom-Ring F) by POLYNOM3:def 10;

C: q divides p by B, RING_4:1;

assume AS: ( not p is linear & p is with_roots ) ; :: thesis: p is reducible

then consider a being Element of F such that

A: a is_a_root_of p by POLYNOM5:def 8;

consider q1 being Polynomial of F such that

B: p = (rpoly (1,a)) *' q1 by A, HURWITZ:33;

reconsider q = q1 as Element of the carrier of (Polynom-Ring F) by POLYNOM3:def 10;

C: q divides p by B, RING_4:1;

per cases
( p = 0_. F or p <> 0_. F )
;

end;

suppose L:
p <> 0_. F
; :: thesis: p is reducible

then M:
q1 <> 0_. F
by B;

then D: deg p = (deg (rpoly (1,a))) + (deg q1) by B, HURWITZ:23

.= 1 + (deg q1) by HURWITZ:27 ;

reconsider degp = deg p, degq = deg q as Element of NAT by M, L, FIELD_1:1;

1 + degq >= 1 + 1 by D, AS, NAT_1:23;

then 1 <= degq by XREAL_1:6;

hence p is reducible by C, D, NAT_1:19, RING_4:40; :: thesis: verum

end;then D: deg p = (deg (rpoly (1,a))) + (deg q1) by B, HURWITZ:23

.= 1 + (deg q1) by HURWITZ:27 ;

reconsider degp = deg p, degq = deg q as Element of NAT by M, L, FIELD_1:1;

1 + degq >= 1 + 1 by D, AS, NAT_1:23;

then 1 <= degq by XREAL_1:6;

hence p is reducible by C, D, NAT_1:19, RING_4:40; :: thesis: verum