let z, w be Element of COMPLEX ; for n being Element of NAT holds Expan_e n,z,w = (1r / (n !c )) (#) (Expan n,z,w)
let n be Element of NAT ; Expan_e n,z,w = (1r / (n !c )) (#) (Expan n,z,w)
A1:
now let k be
Element of
NAT ;
(Expan_e n,z,w) . k = ((1r / (n !c )) (#) (Expan n,z,w)) . kA2:
now assume A3:
n < k
;
(Expan_e n,z,w) . k = ((1r / (n !c )) (#) (Expan n,z,w)) . kthus (Expan_e n,z,w) . k =
(1r / (n !c )) * 0c
by A3, Def14
.=
(1r / (n !c )) * ((Expan n,z,w) . k)
by A3, Def13
.=
((1r / (n !c )) (#) (Expan n,z,w)) . k
by VALUED_1:6
;
verum end; A4:
now assume A5:
k <= n
;
(Expan_e n,z,w) . k = ((1r / (n !c )) (#) (Expan n,z,w)) . kA6:
(Expan_e n,z,w) . k =
(((Coef_e n) . k) * (z |^ k)) * (w |^ (n -' k))
by A5, Def14
.=
((1r / ((k !c ) * ((n -' k) !c ))) * (z |^ k)) * (w |^ (n -' k))
by A5, Def11
;
A7:
1r / ((k !c ) * ((n -' k) !c )) =
(((n !c ) * 1r ) / (n !c )) / ((k !c ) * ((n -' k) !c ))
by Th1, XCMPLX_1:60
.=
((1r / (n !c )) * (n !c )) / ((k !c ) * ((n -' k) !c ))
;
thus (Expan_e n,z,w) . k =
(((1r / (n !c )) * (n !c )) / ((k !c ) * ((n -' k) !c ))) * ((z |^ k) * (w |^ (n -' k)))
by A6, A7
.=
(1r / (n !c )) * ((((n !c ) / ((k !c ) * ((n -' k) !c ))) * (z |^ k)) * (w |^ (n -' k)))
.=
(1r / (n !c )) * ((((Coef n) . k) * (z |^ k)) * (w |^ (n -' k)))
by A5, Def10
.=
(1r / (n !c )) * ((Expan n,z,w) . k)
by A5, Def13
.=
((1r / (n !c )) (#) (Expan n,z,w)) . k
by VALUED_1:6
;
verum end; thus
(Expan_e n,z,w) . k = ((1r / (n !c )) (#) (Expan n,z,w)) . k
by A2, A4;
verum end;
thus
Expan_e n,z,w = (1r / (n !c )) (#) (Expan n,z,w)
by A1, FUNCT_2:113; verum