let p be Element of the carrier of (Polynom-Ring F); ( not p is linear & p is with_roots implies p is reducible )
assume AS:
( not p is linear & p is with_roots )
; 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 )
;
suppose L:
p <> 0_. F
;
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;
verum end; end;