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

for z0, z1 being Element of R holds (<%z0,z1%> `^ n) . k = (n choose k) * ((z1 |^ k) * (z0 |^ (n -' k)))

let R be commutative Ring; :: thesis: for z0, z1 being Element of R holds (<%z0,z1%> `^ n) . k = (n choose k) * ((z1 |^ k) * (z0 |^ (n -' k)))

let z0, z1 be Element of R; :: thesis: (<%z0,z1%> `^ n) . k = (n choose k) * ((z1 |^ k) * (z0 |^ (n -' k)))

set Z0 = <%z0%>;

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

set C = (n choose k) * ((z1 |^ k) * (z0 |^ (n -' k)));

set PRR = Polynom-Ring R;

<%z0,z1%> = <%z0%> + <%(0. R),z1%> by Th4;

then consider F being FinSequence of (Polynom-Ring R) such that

A1: <%z0,z1%> `^ n = Sum F and

A2: len F = n + 1 and

A3: for k being Nat st k <= n holds

F . (k + 1) = (n choose k) * ((<%(0. R),z1%> `^ k) *' (<%z0%> `^ (n -' k))) by Lm1;

A4: for i being Nat st i <= n holds

for Fi1 being Polynomial of R st Fi1 = F . (i + 1) holds

( ( k <> i implies Fi1 . k = 0. R ) & ( k = i implies Fi1 . k = (n choose k) * ((z1 |^ k) * (z0 |^ (n -' k))) ) )

A10: Sum F = f . (len F) and

A11: ( f . 0 = 0. (Polynom-Ring R) & ( for j being Nat

for v being Element of (Polynom-Ring R) st j < len F & v = F . (j + 1) holds

f . (j + 1) = (f . j) + v ) ) by RLVECT_1:def 12;

set L = len F;

reconsider fL = f . (len F) as Polynomial of R by POLYNOM3:def 10;

A12: for p being Polynomial of R st p = f . 0 holds

p . k = 0. R

for z0, z1 being Element of R holds (<%z0,z1%> `^ n) . k = (n choose k) * ((z1 |^ k) * (z0 |^ (n -' k)))

let R be commutative Ring; :: thesis: for z0, z1 being Element of R holds (<%z0,z1%> `^ n) . k = (n choose k) * ((z1 |^ k) * (z0 |^ (n -' k)))

let z0, z1 be Element of R; :: thesis: (<%z0,z1%> `^ n) . k = (n choose k) * ((z1 |^ k) * (z0 |^ (n -' k)))

set Z0 = <%z0%>;

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

set C = (n choose k) * ((z1 |^ k) * (z0 |^ (n -' k)));

set PRR = Polynom-Ring R;

<%z0,z1%> = <%z0%> + <%(0. R),z1%> by Th4;

then consider F being FinSequence of (Polynom-Ring R) such that

A1: <%z0,z1%> `^ n = Sum F and

A2: len F = n + 1 and

A3: for k being Nat st k <= n holds

F . (k + 1) = (n choose k) * ((<%(0. R),z1%> `^ k) *' (<%z0%> `^ (n -' k))) by Lm1;

A4: for i being Nat st i <= n holds

for Fi1 being Polynomial of R st Fi1 = F . (i + 1) holds

( ( k <> i implies Fi1 . k = 0. R ) & ( k = i implies Fi1 . k = (n choose k) * ((z1 |^ k) * (z0 |^ (n -' k))) ) )

proof

consider f being sequence of the carrier of (Polynom-Ring R) such that
let i be Nat; :: thesis: ( i <= n implies for Fi1 being Polynomial of R st Fi1 = F . (i + 1) holds

( ( k <> i implies Fi1 . k = 0. R ) & ( k = i implies Fi1 . k = (n choose k) * ((z1 |^ k) * (z0 |^ (n -' k))) ) ) )

assume A5: i <= n ; :: thesis: for Fi1 being Polynomial of R st Fi1 = F . (i + 1) holds

( ( k <> i implies Fi1 . k = 0. R ) & ( k = i implies Fi1 . k = (n choose k) * ((z1 |^ k) * (z0 |^ (n -' k))) ) )

let Fi1 be Polynomial of R; :: thesis: ( Fi1 = F . (i + 1) implies ( ( k <> i implies Fi1 . k = 0. R ) & ( k = i implies Fi1 . k = (n choose k) * ((z1 |^ k) * (z0 |^ (n -' k))) ) ) )

assume A6: Fi1 = F . (i + 1) ; :: thesis: ( ( k <> i implies Fi1 . k = 0. R ) & ( k = i implies Fi1 . k = (n choose k) * ((z1 |^ k) * (z0 |^ (n -' k))) ) )

Fi1 = (n choose i) * ((<%(0. R),z1%> `^ i) *' (<%z0%> `^ (n -' i))) by A5, A6, A3;

then A7: Fi1 . k = (n choose i) * (((<%(0. R),z1%> `^ i) *' (<%z0%> `^ (n -' i))) . k) by Th12;

<%(z0 |^ (n -' i))%> = <%z0%> `^ (n -' i) by Th8;

then A8: ((<%(0. R),z1%> `^ i) *' (<%z0%> `^ (n -' i))) . k = ((<%(0. R),z1%> `^ i) . k) * (z0 |^ (n -' i)) by Th7;

thus ( k <> i implies Fi1 . k = 0. R ) :: thesis: ( k = i implies Fi1 . k = (n choose k) * ((z1 |^ k) * (z0 |^ (n -' k))) )

then ( i = 0 implies (<%(0. R),z1%> `^ i) . k = 1_ R ) by Th9;

then ( i = 0 implies (<%(0. R),z1%> `^ i) . k = z1 |^ k ) by A9, BINOM:8;

hence Fi1 . k = (n choose k) * ((z1 |^ k) * (z0 |^ (n -' k))) by A9, Th9, A7, A8; :: thesis: verum

end;( ( k <> i implies Fi1 . k = 0. R ) & ( k = i implies Fi1 . k = (n choose k) * ((z1 |^ k) * (z0 |^ (n -' k))) ) ) )

assume A5: i <= n ; :: thesis: for Fi1 being Polynomial of R st Fi1 = F . (i + 1) holds

( ( k <> i implies Fi1 . k = 0. R ) & ( k = i implies Fi1 . k = (n choose k) * ((z1 |^ k) * (z0 |^ (n -' k))) ) )

let Fi1 be Polynomial of R; :: thesis: ( Fi1 = F . (i + 1) implies ( ( k <> i implies Fi1 . k = 0. R ) & ( k = i implies Fi1 . k = (n choose k) * ((z1 |^ k) * (z0 |^ (n -' k))) ) ) )

assume A6: Fi1 = F . (i + 1) ; :: thesis: ( ( k <> i implies Fi1 . k = 0. R ) & ( k = i implies Fi1 . k = (n choose k) * ((z1 |^ k) * (z0 |^ (n -' k))) ) )

Fi1 = (n choose i) * ((<%(0. R),z1%> `^ i) *' (<%z0%> `^ (n -' i))) by A5, A6, A3;

then A7: Fi1 . k = (n choose i) * (((<%(0. R),z1%> `^ i) *' (<%z0%> `^ (n -' i))) . k) by Th12;

<%(z0 |^ (n -' i))%> = <%z0%> `^ (n -' i) by Th8;

then A8: ((<%(0. R),z1%> `^ i) *' (<%z0%> `^ (n -' i))) . k = ((<%(0. R),z1%> `^ i) . k) * (z0 |^ (n -' i)) by Th7;

thus ( k <> i implies Fi1 . k = 0. R ) :: thesis: ( k = i implies Fi1 . k = (n choose k) * ((z1 |^ k) * (z0 |^ (n -' k))) )

proof

assume A9:
k = i
; :: thesis: Fi1 . k = (n choose k) * ((z1 |^ k) * (z0 |^ (n -' k)))
assume
k <> i
; :: thesis: Fi1 . k = 0. R

then (<%(0. R),z1%> `^ i) . k = 0. R by Th9;

hence Fi1 . k = 0. R by A7, A8; :: thesis: verum

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

hence Fi1 . k = 0. R by A7, A8; :: thesis: verum

then ( i = 0 implies (<%(0. R),z1%> `^ i) . k = 1_ R ) by Th9;

then ( i = 0 implies (<%(0. R),z1%> `^ i) . k = z1 |^ k ) by A9, BINOM:8;

hence Fi1 . k = (n choose k) * ((z1 |^ k) * (z0 |^ (n -' k))) by A9, Th9, A7, A8; :: thesis: verum

A10: Sum F = f . (len F) and

A11: ( f . 0 = 0. (Polynom-Ring R) & ( for j being Nat

for v being Element of (Polynom-Ring R) st j < len F & v = F . (j + 1) holds

f . (j + 1) = (f . j) + v ) ) by RLVECT_1:def 12;

set L = len F;

reconsider fL = f . (len F) as Polynomial of R by POLYNOM3:def 10;

A12: for p being Polynomial of R st p = f . 0 holds

p . k = 0. R

proof

let p be Polynomial of R; :: thesis: ( p = f . 0 implies p . k = 0. R )

assume p = f . 0 ; :: thesis: p . k = 0. R

then ( p = 0_. R & k in NAT ) by A11, POLYNOM3:def 10, ORDINAL1:def 12;

hence p . k = 0. R by FUNCOP_1:7; :: thesis: verum

end;assume p = f . 0 ; :: thesis: p . k = 0. R

then ( p = 0_. R & k in NAT ) by A11, POLYNOM3:def 10, ORDINAL1:def 12;

hence p . k = 0. R by FUNCOP_1:7; :: thesis: verum

per cases
( k > n or k <= n )
;

end;

suppose A13:
k > n
; :: thesis: (<%z0,z1%> `^ n) . k = (n choose k) * ((z1 |^ k) * (z0 |^ (n -' k)))

defpred S_{1}[ Nat] means ( $1 <= len F implies for p being Polynomial of R st p = f . $1 holds

p . k = 0. R );

A14: S_{1}[ 0 ]
by A12;

A15: for i being Nat st S_{1}[i] holds

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

hence (<%z0,z1%> `^ n) . k = 0. R by A10, A1

.= 0 * ((z1 |^ k) * (z0 |^ (n -' k))) by BINOM:12

.= (n choose k) * ((z1 |^ k) * (z0 |^ (n -' k))) by A13, NEWTON:def 3 ;

:: thesis: verum

end;p . k = 0. R );

A14: S

A15: for i being Nat st S

S

proof

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

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

set i1 = i + 1;

reconsider fi = f . i as Polynomial of R by POLYNOM3:def 10;

assume A17: i + 1 <= len F ; :: thesis: for p being Polynomial of R st p = f . (i + 1) holds

p . k = 0. R

then A18: i < len F by NAT_1:13;

A19: fi . k = 0. R by A16, A17, NAT_1:13;

i + 1 in dom F by NAT_1:11, A17, FINSEQ_3:25;

then A20: F /. (i + 1) = F . (i + 1) by PARTFUN1:def 6;

then reconsider Fi1 = F . (i + 1) as Polynomial of R by POLYNOM3:def 10;

let p be Polynomial of R; :: thesis: ( p = f . (i + 1) implies p . k = 0. R )

assume A21: p = f . (i + 1) ; :: thesis: p . k = 0. R

A22: i <= n by A2, A18, NAT_1:13;

p = (f . i) + (F /. (i + 1)) by A20, A17, NAT_1:13, A11, A21

.= fi + Fi1 by A20, POLYNOM3:def 10 ;

hence p . k = (fi . k) + (Fi1 . k) by NORMSP_1:def 2

.= 0. R by A4, A13, A19, A22 ;

:: thesis: verum

end;assume A16: S

set i1 = i + 1;

reconsider fi = f . i as Polynomial of R by POLYNOM3:def 10;

assume A17: i + 1 <= len F ; :: thesis: for p being Polynomial of R st p = f . (i + 1) holds

p . k = 0. R

then A18: i < len F by NAT_1:13;

A19: fi . k = 0. R by A16, A17, NAT_1:13;

i + 1 in dom F by NAT_1:11, A17, FINSEQ_3:25;

then A20: F /. (i + 1) = F . (i + 1) by PARTFUN1:def 6;

then reconsider Fi1 = F . (i + 1) as Polynomial of R by POLYNOM3:def 10;

let p be Polynomial of R; :: thesis: ( p = f . (i + 1) implies p . k = 0. R )

assume A21: p = f . (i + 1) ; :: thesis: p . k = 0. R

A22: i <= n by A2, A18, NAT_1:13;

p = (f . i) + (F /. (i + 1)) by A20, A17, NAT_1:13, A11, A21

.= fi + Fi1 by A20, POLYNOM3:def 10 ;

hence p . k = (fi . k) + (Fi1 . k) by NORMSP_1:def 2

.= 0. R by A4, A13, A19, A22 ;

:: thesis: verum

hence (<%z0,z1%> `^ n) . k = 0. R by A10, A1

.= 0 * ((z1 |^ k) * (z0 |^ (n -' k))) by BINOM:12

.= (n choose k) * ((z1 |^ k) * (z0 |^ (n -' k))) by A13, NEWTON:def 3 ;

:: thesis: verum

suppose A23:
k <= n
; :: thesis: (<%z0,z1%> `^ n) . k = (n choose k) * ((z1 |^ k) * (z0 |^ (n -' k)))

defpred S_{1}[ Nat] means ( $1 <= k & $1 <= len F implies for p being Polynomial of R st p = f . $1 holds

p . k = 0. R );

A24: S_{1}[ 0 ]
by A12;

A25: for i being Nat st S_{1}[i] holds

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

defpred S_{2}[ Nat] means ( $1 <= n implies for p being Polynomial of R st p = f . ($1 + 1) holds

p . k = (n choose k) * ((z1 |^ k) * (z0 |^ (n -' k))) );

A34: S_{2}[k]
_{2}[i] holds

S_{2}[i + 1]

S_{2}[i]
from NAT_1:sch 8(A34, A39);

hence (<%z0,z1%> `^ n) . k = (n choose k) * ((z1 |^ k) * (z0 |^ (n -' k))) by A10, A1, A23, A2; :: thesis: verum

end;p . k = 0. R );

A24: S

A25: for i being Nat st S

S

proof

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

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

set i1 = i + 1;

reconsider fi = f . i as Polynomial of R by POLYNOM3:def 10;

assume A27: ( i + 1 <= k & i + 1 <= len F ) ; :: thesis: for p being Polynomial of R st p = f . (i + 1) holds

p . k = 0. R

then A28: ( i < k & i < len F ) by NAT_1:13;

A29: fi . k = 0. R by A26, A27, NAT_1:13;

i + 1 in dom F by A27, NAT_1:11, FINSEQ_3:25;

then A30: F /. (i + 1) = F . (i + 1) by PARTFUN1:def 6;

then reconsider Fi1 = F . (i + 1) as Polynomial of R by POLYNOM3:def 10;

let p be Polynomial of R; :: thesis: ( p = f . (i + 1) implies p . k = 0. R )

assume A31: p = f . (i + 1) ; :: thesis: p . k = 0. R

A32: i <= n by A2, A28, NAT_1:13;

p = (f . i) + (F /. (i + 1)) by A30, A27, NAT_1:13, A11, A31

.= fi + Fi1 by A30, POLYNOM3:def 10 ;

hence p . k = (fi . k) + (Fi1 . k) by NORMSP_1:def 2

.= 0. R by A32, A28, A4, A29 ;

:: thesis: verum

end;assume A26: S

set i1 = i + 1;

reconsider fi = f . i as Polynomial of R by POLYNOM3:def 10;

assume A27: ( i + 1 <= k & i + 1 <= len F ) ; :: thesis: for p being Polynomial of R st p = f . (i + 1) holds

p . k = 0. R

then A28: ( i < k & i < len F ) by NAT_1:13;

A29: fi . k = 0. R by A26, A27, NAT_1:13;

i + 1 in dom F by A27, NAT_1:11, FINSEQ_3:25;

then A30: F /. (i + 1) = F . (i + 1) by PARTFUN1:def 6;

then reconsider Fi1 = F . (i + 1) as Polynomial of R by POLYNOM3:def 10;

let p be Polynomial of R; :: thesis: ( p = f . (i + 1) implies p . k = 0. R )

assume A31: p = f . (i + 1) ; :: thesis: p . k = 0. R

A32: i <= n by A2, A28, NAT_1:13;

p = (f . i) + (F /. (i + 1)) by A30, A27, NAT_1:13, A11, A31

.= fi + Fi1 by A30, POLYNOM3:def 10 ;

hence p . k = (fi . k) + (Fi1 . k) by NORMSP_1:def 2

.= 0. R by A32, A28, A4, A29 ;

:: thesis: verum

defpred S

p . k = (n choose k) * ((z1 |^ k) * (z0 |^ (n -' k))) );

A34: S

proof

A39:
for i being Nat st k <= i & S
assume A35:
k <= n
; :: thesis: for p being Polynomial of R st p = f . (k + 1) holds

p . k = (n choose k) * ((z1 |^ k) * (z0 |^ (n -' k)))

set k1 = k + 1;

let p be Polynomial of R; :: thesis: ( p = f . (k + 1) implies p . k = (n choose k) * ((z1 |^ k) * (z0 |^ (n -' k))) )

assume A36: p = f . (k + 1) ; :: thesis: p . k = (n choose k) * ((z1 |^ k) * (z0 |^ (n -' k)))

reconsider fk = f . k as Polynomial of R by POLYNOM3:def 10;

( 1 <= k + 1 & k + 1 <= len F ) by A2, A35, NAT_1:11, XREAL_1:6;

then k + 1 in dom F by FINSEQ_3:25;

then A37: F /. (k + 1) = F . (k + 1) by PARTFUN1:def 6;

then reconsider Fk1 = F . (k + 1) as Polynomial of R by POLYNOM3:def 10;

A38: k < len F by A35, A2, NAT_1:13;

then p = (f . k) + (F /. (k + 1)) by A37, A11, A36

.= fk + Fk1 by A37, POLYNOM3:def 10 ;

hence p . k = (fk . k) + (Fk1 . k) by NORMSP_1:def 2

.= (0. R) + (Fk1 . k) by A38, A33

.= (n choose k) * ((z1 |^ k) * (z0 |^ (n -' k))) by A4, A35 ;

:: thesis: verum

end;p . k = (n choose k) * ((z1 |^ k) * (z0 |^ (n -' k)))

set k1 = k + 1;

let p be Polynomial of R; :: thesis: ( p = f . (k + 1) implies p . k = (n choose k) * ((z1 |^ k) * (z0 |^ (n -' k))) )

assume A36: p = f . (k + 1) ; :: thesis: p . k = (n choose k) * ((z1 |^ k) * (z0 |^ (n -' k)))

reconsider fk = f . k as Polynomial of R by POLYNOM3:def 10;

( 1 <= k + 1 & k + 1 <= len F ) by A2, A35, NAT_1:11, XREAL_1:6;

then k + 1 in dom F by FINSEQ_3:25;

then A37: F /. (k + 1) = F . (k + 1) by PARTFUN1:def 6;

then reconsider Fk1 = F . (k + 1) as Polynomial of R by POLYNOM3:def 10;

A38: k < len F by A35, A2, NAT_1:13;

then p = (f . k) + (F /. (k + 1)) by A37, A11, A36

.= fk + Fk1 by A37, POLYNOM3:def 10 ;

hence p . k = (fk . k) + (Fk1 . k) by NORMSP_1:def 2

.= (0. R) + (Fk1 . k) by A38, A33

.= (n choose k) * ((z1 |^ k) * (z0 |^ (n -' k))) by A4, A35 ;

:: thesis: verum

S

proof

for i being Nat st k <= i holds
let i be Nat; :: thesis: ( k <= i & S_{2}[i] implies S_{2}[i + 1] )

assume A40: ( k <= i & S_{2}[i] )
; :: thesis: S_{2}[i + 1]

set i1 = i + 1;

set i2 = (i + 1) + 1;

reconsider fi1 = f . (i + 1) as Polynomial of R by POLYNOM3:def 10;

assume A41: i + 1 <= n ; :: thesis: for p being Polynomial of R st p = f . ((i + 1) + 1) holds

p . k = (n choose k) * ((z1 |^ k) * (z0 |^ (n -' k)))

( 1 <= (i + 1) + 1 & (i + 1) + 1 <= len F ) by A41, A2, NAT_1:11, XREAL_1:6;

then (i + 1) + 1 in dom F by FINSEQ_3:25;

then A42: F /. ((i + 1) + 1) = F . ((i + 1) + 1) by PARTFUN1:def 6;

then reconsider Fi2 = F . ((i + 1) + 1) as Polynomial of R by POLYNOM3:def 10;

let p be Polynomial of R; :: thesis: ( p = f . ((i + 1) + 1) implies p . k = (n choose k) * ((z1 |^ k) * (z0 |^ (n -' k))) )

assume A43: p = f . ((i + 1) + 1) ; :: thesis: p . k = (n choose k) * ((z1 |^ k) * (z0 |^ (n -' k)))

A44: i + 1 < len F by A41, NAT_1:13, A2;

A45: i + 1 <> k by A40, NAT_1:13;

A46: Fi2 . k = 0. R by A45, A41, A4;

p = (f . (i + 1)) + (F /. ((i + 1) + 1)) by A44, A42, A11, A43

.= fi1 + Fi2 by A42, POLYNOM3:def 10 ;

hence p . k = (fi1 . k) + (Fi2 . k) by NORMSP_1:def 2

.= (n choose k) * ((z1 |^ k) * (z0 |^ (n -' k))) by A40, A41, A46, NAT_1:13 ;

:: thesis: verum

end;assume A40: ( k <= i & S

set i1 = i + 1;

set i2 = (i + 1) + 1;

reconsider fi1 = f . (i + 1) as Polynomial of R by POLYNOM3:def 10;

assume A41: i + 1 <= n ; :: thesis: for p being Polynomial of R st p = f . ((i + 1) + 1) holds

p . k = (n choose k) * ((z1 |^ k) * (z0 |^ (n -' k)))

( 1 <= (i + 1) + 1 & (i + 1) + 1 <= len F ) by A41, A2, NAT_1:11, XREAL_1:6;

then (i + 1) + 1 in dom F by FINSEQ_3:25;

then A42: F /. ((i + 1) + 1) = F . ((i + 1) + 1) by PARTFUN1:def 6;

then reconsider Fi2 = F . ((i + 1) + 1) as Polynomial of R by POLYNOM3:def 10;

let p be Polynomial of R; :: thesis: ( p = f . ((i + 1) + 1) implies p . k = (n choose k) * ((z1 |^ k) * (z0 |^ (n -' k))) )

assume A43: p = f . ((i + 1) + 1) ; :: thesis: p . k = (n choose k) * ((z1 |^ k) * (z0 |^ (n -' k)))

A44: i + 1 < len F by A41, NAT_1:13, A2;

A45: i + 1 <> k by A40, NAT_1:13;

A46: Fi2 . k = 0. R by A45, A41, A4;

p = (f . (i + 1)) + (F /. ((i + 1) + 1)) by A44, A42, A11, A43

.= fi1 + Fi2 by A42, POLYNOM3:def 10 ;

hence p . k = (fi1 . k) + (Fi2 . k) by NORMSP_1:def 2

.= (n choose k) * ((z1 |^ k) * (z0 |^ (n -' k))) by A40, A41, A46, NAT_1:13 ;

:: thesis: verum

S

hence (<%z0,z1%> `^ n) . k = (n choose k) * ((z1 |^ k) * (z0 |^ (n -' k))) by A10, A1, A23, A2; :: thesis: verum