let F be Field; :: thesis: for p being monic Polynomial of F
for a being Element of F
for n being Nat holds
( p divides (X- a) `^ n iff ex l being Nat st
( l <= n & p = (X- a) `^ l ) )
let p be monic Polynomial of F; :: thesis: for a being Element of F
for n being Nat holds
( p divides (X- a) `^ n iff ex l being Nat st
( l <= n & p = (X- a) `^ l ) )
let a be Element of F; :: thesis: for n being Nat holds
( p divides (X- a) `^ n iff ex l being Nat st
( l <= n & p = (X- a) `^ l ) )
let n be Nat; :: thesis: ( p divides (X- a) `^ n iff ex l being Nat st
( l <= n & p = (X- a) `^ l ) )
reconsider n = n as Element of NAT by ORDINAL1:def 12;

A: now :: thesis: ( p divides (X- a) `^ n implies ex l being Nat st
( l <= n & p = (X- a) `^ l ) )

assume AS: p divides (X- a) `^ n ; :: thesis: ex l being Nat st
( l <= n & p = (X- a) `^ l )
defpred S₁[ Nat] means for p being monic Polynomial of F st deg p = $1 & p divides (X- a) `^ n holds
ex l being Nat st p = (X- a) `^ l;
IA: S₁[ 0 ]

proof

now :: thesis: for p being monic Polynomial of F st deg p = 0 & p divides (X- a) `^ n holds
ex l being Nat st p = (X- a) `^ l

let p be monic Polynomial of F; :: thesis: ( deg p = 0 & p divides (X- a) `^ n implies ex l being Nat st p = (X- a) `^ l )
assume ( deg p = 0 & p divides (X- a) `^ n ) ; :: thesis: ex l being Nat st p = (X- a) `^ l
then p = 1_. F by FIELD_14:16, RATFUNC1:def 2;
then p = (X- a) `^ 0 by POLYNOM5:15;
hence ex l being Nat st p = (X- a) `^ l ; :: thesis: verum

end;

hence S₁[ 0 ] ; :: thesis: verum

end;

IS: now :: thesis: for j being Element of NAT st 0 <= j & j < n & S₁[j] holds
S₁[j + 1]

let j be Element of NAT ; :: thesis: ( 0 <= j & j < n & S₁[j] implies S₁[j + 1] )
assume B0: ( 0 <= j & j < n ) ; :: thesis: ( S₁[j] implies S₁[j + 1] )
assume IV: S₁[j] ; :: thesis: S₁[j + 1]

now :: thesis: for p being monic Polynomial of F st deg p = j + 1 & p divides (X- a) `^ n holds
ex l being Nat st p = (X- a) `^ l

let p be monic Polynomial of F; :: thesis: ( deg p = j + 1 & p divides (X- a) `^ n implies ex l being Nat st l = (X- a) `^ b₂ )
assume C: ( deg p = j + 1 & p divides (X- a) `^ n ) ; :: thesis: ex l being Nat st l = (X- a) `^ b₂
then consider q being Polynomial of F such that
A0: p *' q = (X- a) `^ n by RING_4:1;
reconsider q = q as non zero Polynomial of F by A0;
A1: Roots ((X- a) `^ n) = {a} by B0, Lm12b;

per cases ( Roots p = {a} or Roots p <> {a} ) ;

suppose Roots p = {a} ; :: thesis: ex l being Nat st l = (X- a) `^ b₂

then a in Roots p by TARSKI:def 1;
then a is_a_root_of p by POLYNOM5:def 10;
then consider q1 being Polynomial of F such that
B1: p = (rpoly (1,a)) *' q1 by HURWITZ:33;
( q1 <> 0_. F & p <> 0_. F ) by B1;
then B2: deg p = (deg (rpoly (1,a))) + (deg q1) by B1, HURWITZ:23
.= 1 + (deg q1) by HURWITZ:27 ;
B3: q1 is monic by B1, FIELD_14:15;
q1 *' ((rpoly (1,a)) *' q) = p *' q by B1, POLYNOM3:33;
then consider l being Nat such that
B4: q1 = (X- a) `^ l by B3, B2, C, IV, A0, RING_4:1;
p = (X- a) `^ (l + 1) by B4, B1, POLYNOM5:19;
hence ex l being Nat st p = (X- a) `^ l ; :: thesis: verum

end;

suppose Roots p <> {a} ; :: thesis: ex l being Nat st l = (X- a) `^ b₂

then Roots p c< {a} by A1, A0, FIELD_14:27, XBOOLE_0:def 8;
then card (Roots p) < card {a} by CARD_2:48;
then card (Roots p) < 1 by CARD_2:42;
then Roots p = {} by NAT_1:14;
then D: not a is_a_root_of p by POLYNOM5:def 10;
n = multiplicity ((p *' q),a) by A0, ro0
.= (multiplicity (p,a)) + (multiplicity (q,a)) by UPROOTS:55
.= 0 + (multiplicity (q,a)) by D, NAT_1:14, UPROOTS:52 ;
then E: deg q >= n by ro00;
H: ( p <> 0_. F & q <> 0_. F ) ;
F: n = deg (p *' q) by A0, Lm12a
.= (deg p) + (deg q) by H, HURWITZ:23 ;
then deg q <= n by NAT_1:11;
then deg q = n by E, XXREAL_0:1;
then p = 1_. F by F, RATFUNC1:def 2, FIELD_14:16;
then p = (X- a) `^ 0 by POLYNOM5:15;
hence ex l being Nat st p = (X- a) `^ l ; :: thesis: verum

end;

end;

end;

hence S₁[j + 1] ; :: thesis: verum

end;

I: for i being Element of NAT st 0 <= i & i <= n holds
S₁[i] from INT_1:sch 7(IA, IS);
deg ((X- a) `^ n) = n by Lm12a;
then A5: deg p <= n by AS, RING_5:13;
then consider l being Nat such that
A6: p = (X- a) `^ l by AS, I;
l <= n by A5, A6, Lm12a;
hence ex l being Nat st
( l <= n & p = (X- a) `^ l ) by A6; :: thesis: verum

end;

now :: thesis: ( ex l being Nat st
( l <= n & p = (X- a) `^ l ) implies p divides (X- a) `^ n )

assume ex l being Nat st
( l <= n & p = (X- a) `^ l ) ; :: thesis: p divides (X- a) `^ n
then consider l being Nat such that
A0: ( l <= n & p = (X- a) `^ l ) ;
consider k being Nat such that
A1: l + k = n by A0, NAT_1:10;
( l is Element of NAT & k is Element of NAT ) by ORDINAL1:def 12;
then p *' ((X- a) `^ k) = (X- a) `^ n by A0, A1, FIELD_14:19;
hence p divides (X- a) `^ n by RING_4:1; :: thesis: verum

end;

hence ( p divides (X- a) `^ n iff ex l being Nat st
( l <= n & p = (X- a) `^ l ) ) by A; :: thesis: verum