let L be algebraic-closed domRing; :: thesis: for p being non-zero Polynomial of L holds degree (BRoots p) = (len p) -' 1

let p be non-zero Polynomial of L; :: thesis: degree (BRoots p) = (len p) -' 1

defpred S_{1}[ Nat] means for p being non-zero Polynomial of L st len p = $1 & $1 > 0 holds

degree (BRoots p) = (len p) -' 1;

A1: for k being Nat st ( for n being Nat st n < k holds

S_{1}[n] ) holds

S_{1}[k]
_{1}[n]
from NAT_1:sch 4(A1);

len p > 0 by Th14;

hence degree (BRoots p) = (len p) -' 1 by A26; :: thesis: verum

let p be non-zero Polynomial of L; :: thesis: degree (BRoots p) = (len p) -' 1

defpred S

degree (BRoots p) = (len p) -' 1;

A1: for k being Nat st ( for n being Nat st n < k holds

S

S

proof

A26:
for n being Nat holds S
let k be Nat; :: thesis: ( ( for n being Nat st n < k holds

S_{1}[n] ) implies S_{1}[k] )

assume A2: for n being Nat st n < k holds

S_{1}[n]
; :: thesis: S_{1}[k]

let p be non-zero Polynomial of L; :: thesis: ( len p = k & k > 0 implies degree (BRoots p) = (len p) -' 1 )

assume that

A3: len p = k and

A4: k > 0 ; :: thesis: degree (BRoots p) = (len p) -' 1

A5: k >= 0 + 1 by A4, NAT_1:13;

thus degree (BRoots p) = (len p) -' 1 :: thesis: verum

end;S

assume A2: for n being Nat st n < k holds

S

let p be non-zero Polynomial of L; :: thesis: ( len p = k & k > 0 implies degree (BRoots p) = (len p) -' 1 )

assume that

A3: len p = k and

A4: k > 0 ; :: thesis: degree (BRoots p) = (len p) -' 1

A5: k >= 0 + 1 by A4, NAT_1:13;

thus degree (BRoots p) = (len p) -' 1 :: thesis: verum

proof
end;

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

end;

suppose A6:
k = 1
; :: thesis: degree (BRoots p) = (len p) -' 1

hence degree (BRoots p) =
1 - 1
by A3, Th54

.= (len p) -' 1 by A3, A6, XREAL_1:233 ;

:: thesis: verum

end;.= (len p) -' 1 by A3, A6, XREAL_1:233 ;

:: thesis: verum

suppose A7:
k > 1
; :: thesis: degree (BRoots p) = (len p) -' 1

then
p is with_roots
by A3, POLYNOM5:def 9;

then consider x being Element of L such that

A8: x is_a_root_of p ;

A9: multiplicity (p,x) >= 1 by A8, Th49;

set r = <%(- x),(1. L)%>;

consider F being non empty finite Subset of NAT such that

A10: F = { l where l is Element of NAT : ex q being Polynomial of L st p = (<%(- x),(1. L)%> `^ l) *' q } and

A11: multiplicity (p,x) = max F by Def7;

max F in F by XXREAL_2:def 8;

then consider l being Element of NAT such that

A12: l = max F and

A13: ex q being Polynomial of L st p = (<%(- x),(1. L)%> `^ l) *' q by A10;

set rr = <%(- x),(1. L)%> `^ l;

consider q being Polynomial of L such that

A14: p = (<%(- x),(1. L)%> `^ l) *' q by A13;

reconsider q = q as non-zero Polynomial of L by A14, Th31;

len q > 0 by Th14;

then A15: len q >= 0 + 1 by NAT_1:13;

thus degree (BRoots p) = (len p) -' 1 :: thesis: verum

end;then consider x being Element of L such that

A8: x is_a_root_of p ;

A9: multiplicity (p,x) >= 1 by A8, Th49;

set r = <%(- x),(1. L)%>;

consider F being non empty finite Subset of NAT such that

A10: F = { l where l is Element of NAT : ex q being Polynomial of L st p = (<%(- x),(1. L)%> `^ l) *' q } and

A11: multiplicity (p,x) = max F by Def7;

max F in F by XXREAL_2:def 8;

then consider l being Element of NAT such that

A12: l = max F and

A13: ex q being Polynomial of L st p = (<%(- x),(1. L)%> `^ l) *' q by A10;

set rr = <%(- x),(1. L)%> `^ l;

consider q being Polynomial of L such that

A14: p = (<%(- x),(1. L)%> `^ l) *' q by A13;

reconsider q = q as non-zero Polynomial of L by A14, Th31;

len q > 0 by Th14;

then A15: len q >= 0 + 1 by NAT_1:13;

thus degree (BRoots p) = (len p) -' 1 :: thesis: verum

proof

len q > 0
by Th14;

then A16: q . ((len q) -' 1) <> 0. L by Th15;

len (<%(- x),(1. L)%> `^ l) > 0 by Th14;

then (<%(- x),(1. L)%> `^ l) . ((len (<%(- x),(1. L)%> `^ l)) -' 1) <> 0. L by Th15;

then A17: ((<%(- x),(1. L)%> `^ l) . ((len (<%(- x),(1. L)%> `^ l)) -' 1)) * (q . ((len q) -' 1)) <> 0. L by A16, VECTSP_2:def 1;

A18: ((l * 2) - l) + 1 = l + 1 ;

A19: len <%(- x),(1. L)%> = 2 by POLYNOM5:40;

then A20: len (<%(- x),(1. L)%> `^ l) = ((l * 2) - l) + 1 by POLYNOM5:23;

then A21: len (<%(- x),(1. L)%> `^ l) > 1 by A9, A11, A12, NAT_1:13;

end;then A16: q . ((len q) -' 1) <> 0. L by Th15;

len (<%(- x),(1. L)%> `^ l) > 0 by Th14;

then (<%(- x),(1. L)%> `^ l) . ((len (<%(- x),(1. L)%> `^ l)) -' 1) <> 0. L by Th15;

then A17: ((<%(- x),(1. L)%> `^ l) . ((len (<%(- x),(1. L)%> `^ l)) -' 1)) * (q . ((len q) -' 1)) <> 0. L by A16, VECTSP_2:def 1;

A18: ((l * 2) - l) + 1 = l + 1 ;

A19: len <%(- x),(1. L)%> = 2 by POLYNOM5:40;

then A20: len (<%(- x),(1. L)%> `^ l) = ((l * 2) - l) + 1 by POLYNOM5:23;

then A21: len (<%(- x),(1. L)%> `^ l) > 1 by A9, A11, A12, NAT_1:13;

per cases
( len q = 1 or len q > 1 )
by A15, XXREAL_0:1;

end;

suppose A22:
len q = 1
; :: thesis: degree (BRoots p) = (len p) -' 1

A23: len p =
((len (<%(- x),(1. L)%> `^ l)) + (len q)) - 1
by A14, A17, POLYNOM4:10

.= len (<%(- x),(1. L)%> `^ l) by A22 ;

thus degree (BRoots p) = (degree (BRoots (<%(- x),(1. L)%> `^ l))) + (degree (BRoots q)) by A14, Lm2

.= (degree (BRoots (<%(- x),(1. L)%> `^ l))) + 0 by A22, Th54

.= (((2 * l) - l) + 1) - 1 by Th55

.= (len p) -' 1 by A3, A5, A20, A23, XREAL_1:233 ; :: thesis: verum

end;.= len (<%(- x),(1. L)%> `^ l) by A22 ;

thus degree (BRoots p) = (degree (BRoots (<%(- x),(1. L)%> `^ l))) + (degree (BRoots q)) by A14, Lm2

.= (degree (BRoots (<%(- x),(1. L)%> `^ l))) + 0 by A22, Th54

.= (((2 * l) - l) + 1) - 1 by Th55

.= (len p) -' 1 by A3, A5, A20, A23, XREAL_1:233 ; :: thesis: verum

suppose A24:
len q > 1
; :: thesis: degree (BRoots p) = (len p) -' 1

then A25:
( degree (BRoots (<%(- x),(1. L)%> `^ l)) = (l + 1) -' 1 & degree (BRoots q) = (len q) -' 1 )
by A2, A3, A14, A20, A21, Th33;

thus degree (BRoots p) = (degree (BRoots (<%(- x),(1. L)%> `^ l))) + (degree (BRoots q)) by A14, Lm2

.= ((len (<%(- x),(1. L)%> `^ l)) -' 1) + ((len q) -' 1) by A19, A18, A25, POLYNOM5:23

.= ((len (<%(- x),(1. L)%> `^ l)) - 1) + ((len q) -' 1) by A21, XREAL_1:233

.= ((len (<%(- x),(1. L)%> `^ l)) - 1) + ((len q) - 1) by A24, XREAL_1:233

.= (((len (<%(- x),(1. L)%> `^ l)) + (len q)) - 1) - 1

.= (len p) - 1 by A14, A17, POLYNOM4:10

.= (len p) -' 1 by A3, A7, XREAL_1:233 ; :: thesis: verum

end;thus degree (BRoots p) = (degree (BRoots (<%(- x),(1. L)%> `^ l))) + (degree (BRoots q)) by A14, Lm2

.= ((len (<%(- x),(1. L)%> `^ l)) -' 1) + ((len q) -' 1) by A19, A18, A25, POLYNOM5:23

.= ((len (<%(- x),(1. L)%> `^ l)) - 1) + ((len q) -' 1) by A21, XREAL_1:233

.= ((len (<%(- x),(1. L)%> `^ l)) - 1) + ((len q) - 1) by A24, XREAL_1:233

.= (((len (<%(- x),(1. L)%> `^ l)) + (len q)) - 1) - 1

.= (len p) - 1 by A14, A17, POLYNOM4:10

.= (len p) -' 1 by A3, A7, XREAL_1:233 ; :: thesis: verum

len p > 0 by Th14;

hence degree (BRoots p) = (len p) -' 1 by A26; :: thesis: verum