let a, b be Real; for n being Nat holds (a,b) Subnomial (n + 1) = <*(a |^ (n + 1))*> ^ (b * ((a,b) Subnomial n))
let n be Nat; (a,b) Subnomial (n + 1) = <*(a |^ (n + 1))*> ^ (b * ((a,b) Subnomial n))
A0:
dom ((a,b) Subnomial n) = dom (b * ((a,b) Subnomial n))
by VALUED_1:def 5;
A1:
dom ((a,b) Subnomial (n + 1)) = dom (<*(a |^ (n + 1))*> ^ (b * ((a,b) Subnomial n)))
for i being object st i in dom ((a,b) Subnomial (n + 1)) holds
((a,b) Subnomial (n + 1)) . i = (<*(a |^ (n + 1))*> ^ (b * ((a,b) Subnomial n))) . i
proof
let i be
object ;
( i in dom ((a,b) Subnomial (n + 1)) implies ((a,b) Subnomial (n + 1)) . i = (<*(a |^ (n + 1))*> ^ (b * ((a,b) Subnomial n))) . i )
assume B1:
i in dom ((a,b) Subnomial (n + 1))
;
((a,b) Subnomial (n + 1)) . i = (<*(a |^ (n + 1))*> ^ (b * ((a,b) Subnomial n))) . i
reconsider i =
i as non
zero Nat by B1, FINSEQ_3:25;
B2:
( 1
<= i &
i <= len ((a,b) Subnomial (((n + 1) + 1) - 1)) )
by B1, FINSEQ_3:25;
reconsider j =
i - 1 as
Nat ;
B3:
j + 1
<= (n + 1) + 1
by B2;
then
ex
k being
Nat st
n + 1
= j + k
by XREAL_1:6, NAT_1:10;
then reconsider k =
(n + 1) - j as
Nat ;
set m =
n + 1;
per cases
( j = 0 or j > 0 )
;
suppose C0:
j > 0
;
((a,b) Subnomial (n + 1)) . i = (<*(a |^ (n + 1))*> ^ (b * ((a,b) Subnomial n))) . ithen
(
len ((a,b) Subnomial ((n + 1) - 1)) >= j &
j >= 0 + 1 )
by B3, XREAL_1:6, NAT_1:13;
then C1:
j in dom ((a,b) Subnomial ((n + 1) - 1))
by FINSEQ_3:25;
then C2:
j in dom (b * ((a,b) Subnomial ((n + 1) - 1)))
by VALUED_1:def 5;
then C3:
(
len (b * ((a,b) Subnomial ((n + 1) - 1))) >= j &
j >= 1 )
by FINSEQ_3:25;
reconsider x =
j - 1 as
Nat by C0;
C5:
(
n = x + k &
k = n - x )
;
1
* (len <*(a |^ (n + 1))*>) = 1
;
then (<*(a |^ (n + 1))*> ^ (b * ((a,b) Subnomial n))) . (1 + j) =
(b * ((a,b) Subnomial n)) . j
by C3, FINSEQ_1:65
.=
b * (((a,b) Subnomial ((n + 1) - 1)) . j)
by C2, VALUED_1:def 5
.=
b * ((a |^ k) * (b |^ x))
by C1, C5, Def2
.=
(a |^ k) * (b * (b |^ x))
.=
(a |^ k) * (b |^ (x + 1))
by NEWTON:6
.=
((a,b) Subnomial (((n + 1) + 1) - 1)) . i
by B1, Def2
;
hence
((a,b) Subnomial (n + 1)) . i = (<*(a |^ (n + 1))*> ^ (b * ((a,b) Subnomial n))) . i
;
verum end; end;
end;
hence
(a,b) Subnomial (n + 1) = <*(a |^ (n + 1))*> ^ (b * ((a,b) Subnomial n))
by A1, FUNCT_1:2; verum