let n be Nat; for a, b being Real holds (a,b) Subnomial (n + 1) = (a * ((a,b) Subnomial n)) ^ <*(b |^ (n + 1))*>
let a, b be Real; (a,b) Subnomial (n + 1) = (a * ((a,b) Subnomial n)) ^ <*(b |^ (n + 1))*>
A0:
(a,b) Subnomial n is FinSequence of COMPLEX
by RVSUM_1:146;
A0a:
len ((a,b) Subnomial n) = len (a * ((a,b) Subnomial n))
by COMPLSP2:3;
A2:
( len ((a,b) Subnomial (((n + 1) + 1) - 1)) = (n + 1) + 1 & len ((a,b) Subnomial ((n + 1) - 1)) = n + 1 )
;
then A3: len ((a,b) Subnomial (n + 1)) =
(len ((a,b) Subnomial n)) + (len <*(b |^ (n + 1))*>)
by FINSEQ_1:39
.=
(len (a * ((a,b) Subnomial n))) + (len <*(b |^ (n + 1))*>)
by COMPLSP2:3
.=
len ((a * ((a,b) Subnomial n)) ^ <*(b |^ (n + 1))*>)
by FINSEQ_1:22
;
for k being Nat st 1 <= k & k <= len ((a,b) Subnomial (n + 1)) holds
((a,b) Subnomial (n + 1)) . k = ((a * ((a,b) Subnomial n)) ^ <*(b |^ (n + 1))*>) . k
proof
let k be
Nat;
( 1 <= k & k <= len ((a,b) Subnomial (n + 1)) implies ((a,b) Subnomial (n + 1)) . k = ((a * ((a,b) Subnomial n)) ^ <*(b |^ (n + 1))*>) . k )
assume B0:
( 1
<= k &
k <= len ((a,b) Subnomial (n + 1)) )
;
((a,b) Subnomial (n + 1)) . k = ((a * ((a,b) Subnomial n)) ^ <*(b |^ (n + 1))*>) . k
reconsider m =
k - 1 as
Nat by B0;
per cases
( k in dom ((a,b) Subnomial n) or not k in dom ((a,b) Subnomial n) )
;
suppose C1:
k in dom ((a,b) Subnomial n)
;
((a,b) Subnomial (n + 1)) . k = ((a * ((a,b) Subnomial n)) ^ <*(b |^ (n + 1))*>) . kthen C2:
( 1
<= k &
k <= len ((a,b) Subnomial n) )
by FINSEQ_3:25;
then
m + 1
<= n + 1
by Def2;
then reconsider l =
n - m as
Element of
NAT by XREAL_1:6, NAT_1:21;
C3:
l + 1
= (n + 1) - m
;
k in dom ((a,b) Subnomial (n + 1))
by B0, FINSEQ_3:25;
then ((a,b) Subnomial (n + 1)) . k =
(a |^ (l + 1)) * (b |^ m)
by Def2, C3
.=
(a * (a |^ l)) * (b |^ m)
by NEWTON:6
.=
a * ((a |^ l) * (b |^ m))
.=
a * (((a,b) Subnomial n) . k)
by C1, Def2
.=
(a * ((a,b) Subnomial n)) . k
by A0, COMPLSP2:16
.=
((a * ((a,b) Subnomial n)) ^ <*(b |^ (n + 1))*>) . k
by A0a, C2, FINSEQ_1:64
;
hence
((a,b) Subnomial (n + 1)) . k = ((a * ((a,b) Subnomial n)) ^ <*(b |^ (n + 1))*>) . k
;
verum end; suppose
not
k in dom ((a,b) Subnomial n)
;
((a,b) Subnomial (n + 1)) . k = ((a * ((a,b) Subnomial n)) ^ <*(b |^ (n + 1))*>) . kthen
not
k <= n + 1
by B0, A2, FINSEQ_3:25;
then
k >= (n + 1) + 1
by INT_1:7;
then C1:
k = (n + 1) + 1
by B0, A2, XXREAL_0:1;
len (a * ((a,b) Subnomial n)) = n + 1
by A2, NEWTON:2;
then
((a * ((a,b) Subnomial n)) ^ <*(b |^ (n + 1))*>) . ((n + 1) + 1) = ((a,b) In_Power (n + 1)) . ((n + 1) + 1)
by NEWTON:29;
hence
((a,b) Subnomial (n + 1)) . k = ((a * ((a,b) Subnomial n)) ^ <*(b |^ (n + 1))*>) . k
by NS, C1;
verum end;
end;
hence
(a,b) Subnomial (n + 1) = (a * ((a,b) Subnomial n)) ^ <*(b |^ (n + 1))*>
by A3; verum