let k, n be Nat; :: thesis: for R being commutative Ring

for z0, z1 being Element of R holds

( (<%z0,z1%> `^ 0) . 0 = 1. R & ( n > 0 implies (<%(0. R),z1%> `^ n) . n = z1 |^ n ) & ( k <> n implies (<%(0. R),z1%> `^ n) . k = 0. R ) )

let R be commutative Ring; :: thesis: for z0, z1 being Element of R holds

( (<%z0,z1%> `^ 0) . 0 = 1. R & ( n > 0 implies (<%(0. R),z1%> `^ n) . n = z1 |^ n ) & ( k <> n implies (<%(0. R),z1%> `^ n) . k = 0. R ) )

let z0, z1 be Element of R; :: thesis: ( (<%z0,z1%> `^ 0) . 0 = 1. R & ( n > 0 implies (<%(0. R),z1%> `^ n) . n = z1 |^ n ) & ( k <> n implies (<%(0. R),z1%> `^ n) . k = 0. R ) )

<%z0,z1%> `^ 0 = 1_. R by POLYNOM5:15;

hence (<%z0,z1%> `^ 0) . 0 = 1. R by POLYNOM3:30; :: thesis: ( ( n > 0 implies (<%(0. R),z1%> `^ n) . n = z1 |^ n ) & ( k <> n implies (<%(0. R),z1%> `^ n) . k = 0. R ) )

set P = <%(0. R),z1%>;

defpred S_{1}[ Nat] means ( ( $1 > 0 implies (<%(0. R),z1%> `^ $1) . $1 = z1 |^ $1 ) & ( for k being Nat st k <> $1 holds

(<%(0. R),z1%> `^ $1) . k = 0. R ) );

A1: S_{1}[ 0 ]
_{1}[i] holds

S_{1}[i + 1]
_{1}[i]
from NAT_1:sch 2(A1, A3);

hence ( ( n > 0 implies (<%(0. R),z1%> `^ n) . n = z1 |^ n ) & ( k <> n implies (<%(0. R),z1%> `^ n) . k = 0. R ) ) ; :: thesis: verum

for z0, z1 being Element of R holds

( (<%z0,z1%> `^ 0) . 0 = 1. R & ( n > 0 implies (<%(0. R),z1%> `^ n) . n = z1 |^ n ) & ( k <> n implies (<%(0. R),z1%> `^ n) . k = 0. R ) )

let R be commutative Ring; :: thesis: for z0, z1 being Element of R holds

( (<%z0,z1%> `^ 0) . 0 = 1. R & ( n > 0 implies (<%(0. R),z1%> `^ n) . n = z1 |^ n ) & ( k <> n implies (<%(0. R),z1%> `^ n) . k = 0. R ) )

let z0, z1 be Element of R; :: thesis: ( (<%z0,z1%> `^ 0) . 0 = 1. R & ( n > 0 implies (<%(0. R),z1%> `^ n) . n = z1 |^ n ) & ( k <> n implies (<%(0. R),z1%> `^ n) . k = 0. R ) )

<%z0,z1%> `^ 0 = 1_. R by POLYNOM5:15;

hence (<%z0,z1%> `^ 0) . 0 = 1. R by POLYNOM3:30; :: thesis: ( ( n > 0 implies (<%(0. R),z1%> `^ n) . n = z1 |^ n ) & ( k <> n implies (<%(0. R),z1%> `^ n) . k = 0. R ) )

set P = <%(0. R),z1%>;

defpred S

(<%(0. R),z1%> `^ $1) . k = 0. R ) );

A1: S

proof

A3:
for i being Nat st S
thus
( 0 > 0 implies (<%(0. R),z1%> `^ 0) . 0 = z1 |^ 0 )
; :: thesis: for k being Nat st k <> 0 holds

(<%(0. R),z1%> `^ 0) . k = 0. R

let k be Nat; :: thesis: ( k <> 0 implies (<%(0. R),z1%> `^ 0) . k = 0. R )

assume A2: k <> 0 ; :: thesis: (<%(0. R),z1%> `^ 0) . k = 0. R

<%(0. R),z1%> `^ 0 = 1_. R by POLYNOM5:15;

hence (<%(0. R),z1%> `^ 0) . k = 0. R by A2, POLYNOM3:30; :: thesis: verum

end;(<%(0. R),z1%> `^ 0) . k = 0. R

let k be Nat; :: thesis: ( k <> 0 implies (<%(0. R),z1%> `^ 0) . k = 0. R )

assume A2: k <> 0 ; :: thesis: (<%(0. R),z1%> `^ 0) . k = 0. R

<%(0. R),z1%> `^ 0 = 1_. R by POLYNOM5:15;

hence (<%(0. R),z1%> `^ 0) . k = 0. R by A2, POLYNOM3:30; :: thesis: verum

S

proof

for i being Nat holds S
let i be Nat; :: thesis: ( S_{1}[i] implies S_{1}[i + 1] )

set i1 = i + 1;

assume A4: S_{1}[i]
; :: thesis: S_{1}[i + 1]

A5: <%(0. R),z1%> `^ (i + 1) = (<%(0. R),z1%> `^ i) *' <%(0. R),z1%> by POLYNOM5:19;

thus ( i + 1 > 0 implies (<%(0. R),z1%> `^ (i + 1)) . (i + 1) = z1 |^ (i + 1) ) :: thesis: for k being Nat st k <> i + 1 holds

(<%(0. R),z1%> `^ (i + 1)) . k = 0. R

assume A18: j <> i + 1 ; :: thesis: (<%(0. R),z1%> `^ (i + 1)) . j = 0. R

set j1 = j + 1;

j in NAT by ORDINAL1:def 12;

then consider r being FinSequence of the carrier of R such that

A19: ( len r = j + 1 & (<%(0. R),z1%> `^ (i + 1)) . j = Sum r ) and

A20: for k being Element of NAT st k in dom r holds

r . k = ((<%(0. R),z1%> `^ i) . (k -' 1)) * (<%(0. R),z1%> . ((j + 1) -' k)) by A5, POLYNOM3:def 9;

for k being Element of NAT st k in dom r holds

r . k = 0. R

end;set i1 = i + 1;

assume A4: S

A5: <%(0. R),z1%> `^ (i + 1) = (<%(0. R),z1%> `^ i) *' <%(0. R),z1%> by POLYNOM5:19;

thus ( i + 1 > 0 implies (<%(0. R),z1%> `^ (i + 1)) . (i + 1) = z1 |^ (i + 1) ) :: thesis: for k being Nat st k <> i + 1 holds

(<%(0. R),z1%> `^ (i + 1)) . k = 0. R

proof

let j be Nat; :: thesis: ( j <> i + 1 implies (<%(0. R),z1%> `^ (i + 1)) . j = 0. R )
assume
i + 1 > 0
; :: thesis: (<%(0. R),z1%> `^ (i + 1)) . (i + 1) = z1 |^ (i + 1)

end;per cases
( i = 0 or i > 0 )
;

end;

suppose A6:
i = 0
; :: thesis: (<%(0. R),z1%> `^ (i + 1)) . (i + 1) = z1 |^ (i + 1)

then
<%(0. R),z1%> `^ (i + 1) = <%(0. R),z1%>
by POLYNOM5:16;

hence (<%(0. R),z1%> `^ (i + 1)) . (i + 1) = z1 by A6, POLYNOM5:38

.= z1 |^ (i + 1) by A6, BINOM:8 ;

:: thesis: verum

end;hence (<%(0. R),z1%> `^ (i + 1)) . (i + 1) = z1 by A6, POLYNOM5:38

.= z1 |^ (i + 1) by A6, BINOM:8 ;

:: thesis: verum

suppose A7:
i > 0
; :: thesis: (<%(0. R),z1%> `^ (i + 1)) . (i + 1) = z1 |^ (i + 1)

consider r being FinSequence of the carrier of R such that

A8: ( len r = (i + 1) + 1 & (<%(0. R),z1%> `^ (i + 1)) . (i + 1) = Sum r ) and

A9: for k being Element of NAT st k in dom r holds

r . k = ((<%(0. R),z1%> `^ i) . (k -' 1)) * (<%(0. R),z1%> . (((i + 1) + 1) -' k)) by A5, POLYNOM3:def 9;

A10: ( 1 <= i + 1 & i + 1 <= len r ) by A8, NAT_1:11;

then A11: i + 1 in dom r by FINSEQ_3:25;

for k being Element of NAT st k in dom r & k <> i + 1 holds

r /. k = 0. R

( (i + 1) -' 1 = (i + 1) - 1 & ((i + 1) + 1) -' (i + 1) = ((i + 1) + 1) - (i + 1) ) by NAT_1:11, XREAL_1:233;

then ( (<%(0. R),z1%> `^ i) . ((i + 1) -' 1) = z1 |^ i & <%(0. R),z1%> . (((i + 1) + 1) -' (i + 1)) = z1 ) by A7, A4, POLYNOM5:38;

then ( r . (i + 1) = (z1 |^ i) * z1 & z1 = z1 |^ 1 ) by A9, A10, FINSEQ_3:25, BINOM:8;

then r . (i + 1) = z1 |^ (i + 1) by BINOM:10;

hence (<%(0. R),z1%> `^ (i + 1)) . (i + 1) = z1 |^ (i + 1) by A17, A8, A11, PARTFUN1:def 6; :: thesis: verum

end;A8: ( len r = (i + 1) + 1 & (<%(0. R),z1%> `^ (i + 1)) . (i + 1) = Sum r ) and

A9: for k being Element of NAT st k in dom r holds

r . k = ((<%(0. R),z1%> `^ i) . (k -' 1)) * (<%(0. R),z1%> . (((i + 1) + 1) -' k)) by A5, POLYNOM3:def 9;

A10: ( 1 <= i + 1 & i + 1 <= len r ) by A8, NAT_1:11;

then A11: i + 1 in dom r by FINSEQ_3:25;

for k being Element of NAT st k in dom r & k <> i + 1 holds

r /. k = 0. R

proof

then A17:
Sum r = r /. (i + 1)
by A10, FINSEQ_3:25, POLYNOM2:3;
let k be Element of NAT ; :: thesis: ( k in dom r & k <> i + 1 implies r /. k = 0. R )

assume A12: ( k in dom r & k <> i + 1 ) ; :: thesis: r /. k = 0. R

A13: k <= (i + 1) + 1 by A8, A12, FINSEQ_3:25;

A14: r /. k = r . k by PARTFUN1:def 6, A12;

end;assume A12: ( k in dom r & k <> i + 1 ) ; :: thesis: r /. k = 0. R

A13: k <= (i + 1) + 1 by A8, A12, FINSEQ_3:25;

A14: r /. k = r . k by PARTFUN1:def 6, A12;

per cases
( k > i + 1 or k < i + 1 )
by A12, XXREAL_0:1;

end;

suppose
k > i + 1
; :: thesis: r /. k = 0. R

then
k >= (i + 1) + 1
by NAT_1:13;

then k = (i + 1) + 1 by A13, XXREAL_0:1;

then ((i + 1) + 1) -' k = 0 by XREAL_1:232;

then <%(0. R),z1%> . (((i + 1) + 1) -' k) = 0. R by POLYNOM5:38;

then ((<%(0. R),z1%> `^ i) . (k -' 1)) * (<%(0. R),z1%> . (((i + 1) + 1) -' k)) = 0. R ;

hence r /. k = 0. R by A14, A12, A9; :: thesis: verum

end;then k = (i + 1) + 1 by A13, XXREAL_0:1;

then ((i + 1) + 1) -' k = 0 by XREAL_1:232;

then <%(0. R),z1%> . (((i + 1) + 1) -' k) = 0. R by POLYNOM5:38;

then ((<%(0. R),z1%> `^ i) . (k -' 1)) * (<%(0. R),z1%> . (((i + 1) + 1) -' k)) = 0. R ;

hence r /. k = 0. R by A14, A12, A9; :: thesis: verum

suppose A15:
k < i + 1
; :: thesis: r /. k = 0. R

then
k < (i + 1) + 1
by NAT_1:13;

then A16: ((i + 1) + 1) -' k = ((i + 1) + 1) - k by XREAL_1:233;

k <= i by A15, NAT_1:13;

then i - k >= 0 by XREAL_1:48;

then (i - k) + 2 >= 0 + 2 by XREAL_1:6;

then <%(0. R),z1%> . (((i + 1) + 1) -' k) = 0. R by A16, POLYNOM5:38;

then ((<%(0. R),z1%> `^ i) . (k -' 1)) * (<%(0. R),z1%> . (((i + 1) + 1) -' k)) = 0. R ;

hence r /. k = 0. R by A14, A12, A9; :: thesis: verum

end;then A16: ((i + 1) + 1) -' k = ((i + 1) + 1) - k by XREAL_1:233;

k <= i by A15, NAT_1:13;

then i - k >= 0 by XREAL_1:48;

then (i - k) + 2 >= 0 + 2 by XREAL_1:6;

then <%(0. R),z1%> . (((i + 1) + 1) -' k) = 0. R by A16, POLYNOM5:38;

then ((<%(0. R),z1%> `^ i) . (k -' 1)) * (<%(0. R),z1%> . (((i + 1) + 1) -' k)) = 0. R ;

hence r /. k = 0. R by A14, A12, A9; :: thesis: verum

( (i + 1) -' 1 = (i + 1) - 1 & ((i + 1) + 1) -' (i + 1) = ((i + 1) + 1) - (i + 1) ) by NAT_1:11, XREAL_1:233;

then ( (<%(0. R),z1%> `^ i) . ((i + 1) -' 1) = z1 |^ i & <%(0. R),z1%> . (((i + 1) + 1) -' (i + 1)) = z1 ) by A7, A4, POLYNOM5:38;

then ( r . (i + 1) = (z1 |^ i) * z1 & z1 = z1 |^ 1 ) by A9, A10, FINSEQ_3:25, BINOM:8;

then r . (i + 1) = z1 |^ (i + 1) by BINOM:10;

hence (<%(0. R),z1%> `^ (i + 1)) . (i + 1) = z1 |^ (i + 1) by A17, A8, A11, PARTFUN1:def 6; :: thesis: verum

assume A18: j <> i + 1 ; :: thesis: (<%(0. R),z1%> `^ (i + 1)) . j = 0. R

set j1 = j + 1;

j in NAT by ORDINAL1:def 12;

then consider r being FinSequence of the carrier of R such that

A19: ( len r = j + 1 & (<%(0. R),z1%> `^ (i + 1)) . j = Sum r ) and

A20: for k being Element of NAT st k in dom r holds

r . k = ((<%(0. R),z1%> `^ i) . (k -' 1)) * (<%(0. R),z1%> . ((j + 1) -' k)) by A5, POLYNOM3:def 9;

for k being Element of NAT st k in dom r holds

r . k = 0. R

proof

hence
(<%(0. R),z1%> `^ (i + 1)) . j = 0. R
by A19, POLYNOM3:1; :: thesis: verum
let k be Element of NAT ; :: thesis: ( k in dom r implies r . k = 0. R )

assume A21: k in dom r ; :: thesis: r . k = 0. R

A22: ( 1 <= k & k <= j + 1 ) by A19, A21, FINSEQ_3:25;

end;assume A21: k in dom r ; :: thesis: r . k = 0. R

A22: ( 1 <= k & k <= j + 1 ) by A19, A21, FINSEQ_3:25;

per cases
( k = j or k > j or k < j )
by XXREAL_0:1;

end;

suppose
k = j
; :: thesis: r . k = 0. R

then
k -' 1 = j - 1
by A22, XREAL_1:233;

then k -' 1 <> i by A18;

then (<%(0. R),z1%> `^ i) . (k -' 1) = 0. R by A4;

then ((<%(0. R),z1%> `^ i) . (k -' 1)) * (<%(0. R),z1%> . ((j + 1) -' k)) = 0. R ;

hence r . k = 0. R by A21, A20; :: thesis: verum

end;then k -' 1 <> i by A18;

then (<%(0. R),z1%> `^ i) . (k -' 1) = 0. R by A4;

then ((<%(0. R),z1%> `^ i) . (k -' 1)) * (<%(0. R),z1%> . ((j + 1) -' k)) = 0. R ;

hence r . k = 0. R by A21, A20; :: thesis: verum

suppose
k > j
; :: thesis: r . k = 0. R

then
k >= j + 1
by NAT_1:13;

then k = j + 1 by A22, XXREAL_0:1;

then (j + 1) -' k = 0 by XREAL_1:232;

then <%(0. R),z1%> . ((j + 1) -' k) = 0. R by POLYNOM5:38;

then ((<%(0. R),z1%> `^ i) . (k -' 1)) * (<%(0. R),z1%> . ((j + 1) -' k)) = 0. R ;

hence r . k = 0. R by A21, A20; :: thesis: verum

end;then k = j + 1 by A22, XXREAL_0:1;

then (j + 1) -' k = 0 by XREAL_1:232;

then <%(0. R),z1%> . ((j + 1) -' k) = 0. R by POLYNOM5:38;

then ((<%(0. R),z1%> `^ i) . (k -' 1)) * (<%(0. R),z1%> . ((j + 1) -' k)) = 0. R ;

hence r . k = 0. R by A21, A20; :: thesis: verum

suppose A23:
k < j
; :: thesis: r . k = 0. R

then
k < j + 1
by NAT_1:13;

then A24: (j + 1) -' k = (j + 1) - k by XREAL_1:233;

j - k > 0 by A23, XREAL_1:50;

then (j - k) + 1 > 0 + 1 by XREAL_1:6;

then (j + 1) -' k >= 1 + 1 by NAT_1:13, A24;

then <%(0. R),z1%> . ((j + 1) -' k) = 0. R by POLYNOM5:38;

then ((<%(0. R),z1%> `^ i) . (k -' 1)) * (<%(0. R),z1%> . ((j + 1) -' k)) = 0. R ;

hence r . k = 0. R by A21, A20; :: thesis: verum

end;then A24: (j + 1) -' k = (j + 1) - k by XREAL_1:233;

j - k > 0 by A23, XREAL_1:50;

then (j - k) + 1 > 0 + 1 by XREAL_1:6;

then (j + 1) -' k >= 1 + 1 by NAT_1:13, A24;

then <%(0. R),z1%> . ((j + 1) -' k) = 0. R by POLYNOM5:38;

then ((<%(0. R),z1%> `^ i) . (k -' 1)) * (<%(0. R),z1%> . ((j + 1) -' k)) = 0. R ;

hence r . k = 0. R by A21, A20; :: thesis: verum

hence ( ( n > 0 implies (<%(0. R),z1%> `^ n) . n = z1 |^ n ) & ( k <> n implies (<%(0. R),z1%> `^ n) . k = 0. R ) ) ; :: thesis: verum