let a, b be Real; for n, i being Nat holds ((a,b) Subnomial n) . i <= ((|.a.|,|.b.|) Subnomial n) . i
let n, i be Nat; ((a,b) Subnomial n) . i <= ((|.a.|,|.b.|) Subnomial n) . i
reconsider f = (|.a.|,|.b.|) Subnomial n as nonnegative-yielding FinSequence of REAL ;
per cases
( not i in dom ((a,b) Subnomial n) or i in dom ((a,b) Subnomial n) )
;
suppose A0:
i in dom ((a,b) Subnomial n)
;
((a,b) Subnomial n) . i <= ((|.a.|,|.b.|) Subnomial n) . ithen A1:
( 1
<= i &
i <= len ((a,b) Subnomial ((n + 1) - 1)) )
by FINSEQ_3:25;
then reconsider l =
i - 1 as
Nat ;
ex
k being
Nat st
n + 1
= (l + 1) + k
by A1, NAT_1:10;
then reconsider k =
(n + 1) - (l + 1) as
Nat ;
A2:
(
k = n - l &
l = i - 1 )
;
A3:
(
|.a.| |^ k = |.(a |^ k).| &
|.b.| |^ l = |.(b |^ l).| )
by TAYLOR_2:1;
A4:
dom ((a,b) Subnomial n) =
dom (Newton_Coeff n)
by DOMN
.=
dom ((|.a.|,|.b.|) Subnomial n)
by DOMN
;
|.((a |^ k) * (b |^ l)).| >= (a |^ k) * (b |^ l)
by ABSVALUE:4;
then
|.(a |^ k).| * |.(b |^ l).| >= (a |^ k) * (b |^ l)
by COMPLEX1:65;
then
(|.a.| |^ k) * (|.b.| |^ l) >= ((a,b) Subnomial (l + k)) . (l + 1)
by A0, A2, A3, LmS1;
hence
((a,b) Subnomial n) . i <= ((|.a.|,|.b.|) Subnomial n) . i
by A0, A2, A4, LmS1;
verum end;