let k, n be Nat; 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; 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; (<%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
let i be
Nat;
( 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
;
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;
( 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)
;
( ( 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 )
( k = i implies Fi1 . k = (n choose k) * ((z1 |^ k) * (z0 |^ (n -' k))) )
assume A9:
k = i
;
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;
verum
end;
consider f being sequence of the carrier of (Polynom-Ring R) such that
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
per cases
( k > n or k <= n )
;
suppose A13:
k > n
;
(<%z0,z1%> `^ n) . k = (n choose k) * ((z1 |^ k) * (z0 |^ (n -' k)))defpred S1[
Nat]
means ( $1
<= len F implies for
p being
Polynomial of
R st
p = f . $1 holds
p . k = 0. R );
A14:
S1[
0 ]
by A12;
A15:
for
i being
Nat st
S1[
i] holds
S1[
i + 1]
proof
let i be
Nat;
( S1[i] implies S1[i + 1] )
assume A16:
S1[
i]
;
S1[i + 1]
set i1 =
i + 1;
reconsider fi =
f . i as
Polynomial of
R by POLYNOM3:def 10;
assume A17:
i + 1
<= len F
;
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;
( p = f . (i + 1) implies p . k = 0. R )
assume A21:
p = f . (i + 1)
;
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
;
verum
end;
for
i being
Nat holds
S1[
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
;
verum end; suppose A23:
k <= n
;
(<%z0,z1%> `^ n) . k = (n choose k) * ((z1 |^ k) * (z0 |^ (n -' k)))defpred S1[
Nat]
means ( $1
<= k & $1
<= len F implies for
p being
Polynomial of
R st
p = f . $1 holds
p . k = 0. R );
A24:
S1[
0 ]
by A12;
A25:
for
i being
Nat st
S1[
i] holds
S1[
i + 1]
proof
let i be
Nat;
( S1[i] implies S1[i + 1] )
assume A26:
S1[
i]
;
S1[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 )
;
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;
( p = f . (i + 1) implies p . k = 0. R )
assume A31:
p = f . (i + 1)
;
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
;
verum
end; A33:
for
i being
Nat holds
S1[
i]
from NAT_1:sch 2(A24, A25);
defpred S2[
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:
S2[
k]
proof
assume A35:
k <= n
;
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;
( p = f . (k + 1) implies p . k = (n choose k) * ((z1 |^ k) * (z0 |^ (n -' k))) )
assume A36:
p = f . (k + 1)
;
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
;
verum
end; A39:
for
i being
Nat st
k <= i &
S2[
i] holds
S2[
i + 1]
proof
let i be
Nat;
( k <= i & S2[i] implies S2[i + 1] )
assume A40:
(
k <= i &
S2[
i] )
;
S2[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
;
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;
( p = f . ((i + 1) + 1) implies p . k = (n choose k) * ((z1 |^ k) * (z0 |^ (n -' k))) )
assume A43:
p = f . ((i + 1) + 1)
;
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
;
verum
end;
for
i being
Nat st
k <= i holds
S2[
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;
verum end;