let L be algebraic-closed domRing; for p being non-zero Polynomial of L st p . ((len p) -' 1) = 1. L holds
p = poly_with_roots (BRoots p)
let p be non-zero Polynomial of L; ( p . ((len p) -' 1) = 1. L implies p = poly_with_roots (BRoots p) )
assume A1:
p . ((len p) -' 1) = 1. L
; p = poly_with_roots (BRoots p)
defpred S1[ Nat] means for p being non-zero Polynomial of L st len p = $1 & $1 >= 1 & p . ((len p) -' 1) = 1. L holds
p = poly_with_roots (BRoots p);
len p > 0
by Th14;
then A2:
len p >= 0 + 1
by NAT_1:13;
A3:
for n being Nat st n >= 1 & S1[n] holds
S1[n + 1]
proof
let n be
Nat;
( n >= 1 & S1[n] implies S1[n + 1] )
assume that A4:
n >= 1
and A5:
S1[
n]
;
S1[n + 1]
let p be
non-zero Polynomial of
L;
( len p = n + 1 & n + 1 >= 1 & p . ((len p) -' 1) = 1. L implies p = poly_with_roots (BRoots p) )
assume that A6:
len p = n + 1
and
n + 1
>= 1
and A7:
p . ((len p) -' 1) = 1. L
;
p = poly_with_roots (BRoots p)
n + 1
> 1
by A4, NAT_1:13;
then
p is
with_roots
by A6, POLYNOM5:def 9;
then consider x being
Element of
L such that A8:
x is_a_root_of p
;
set r =
<%(- x),(1. L)%>;
set q =
poly_quotient (
p,
x);
A9:
p = <%(- x),(1. L)%> *' (poly_quotient (p,x))
by A8, Th47;
then reconsider q =
poly_quotient (
p,
x) as
non-zero Polynomial of
L by Th31;
A10:
len <%(- x),(1. L)%> = 2
by POLYNOM5:40;
then A11:
<%(- x),(1. L)%> . ((len <%(- x),(1. L)%>) -' 1) <> 0. L
by Th15;
len q > 0
by Th14;
then
q . ((len q) -' 1) <> 0. L
by Th15;
then
(<%(- x),(1. L)%> . ((len <%(- x),(1. L)%>) -' 1)) * (q . ((len q) -' 1)) <> 0. L
by A11, VECTSP_2:def 1;
then A12:
len p = ((len q) + (1 + 1)) - 1
by A9, A10, POLYNOM4:10;
q . ((len q) -' 1) = 1. L
by A7, A9, Th38;
then A13:
q = poly_with_roots (BRoots q)
by A4, A5, A6, A12;
A14:
poly_with_roots (({x},1) -bag) = <%(- x),(1. L)%>
by Th58;
BRoots <%(- x),(1. L)%> = (
{x},1)
-bag
by Th51;
then
BRoots p = (({x},1) -bag) + (BRoots q)
by A9, Th53;
hence
p = poly_with_roots (BRoots p)
by A9, A13, A14, Th61;
verum
end;
A15:
S1[1]
for n being Nat st n >= 1 holds
S1[n]
from NAT_1:sch 8(A15, A3);
hence
p = poly_with_roots (BRoots p)
by A1, A2; verum