let z, w be Element of COMPLEX ; :: thesis: for n being Element of NAT holds (z + w) |^ n = (Partial_Sums (Expan (n,z,w))) . n
let n be Element of NAT ; :: thesis: (z + w) |^ n = (Partial_Sums (Expan (n,z,w))) . n
A1: 0 -' 0 = 0 by XREAL_1:234;
defpred S₁[ Element of NAT ] means (z + w) |^ $1 = (Partial_Sums (Expan ($1,z,w))) . $1;
(Partial_Sums (Expan (0,z,w))) . 0 = (Expan (0,z,w)) . 0 by SERIES_1:def 1
.= (((Coef 0) . 0) * (z |^ 0)) * (w |^ 0) by A1, Def13
.= ((1 / (1 * 1)) * (z |^ 0)) * (w |^ 0) by A1, Def10, Th1
.= 1r * ((w GeoSeq) . 0) by COMSEQ_3:def 1
.= 1r by COMSEQ_3:def 1 ;
then A3: S₁[ 0 ] by COMSEQ_3:def 1;
A4: for n being Element of NAT st S₁[n] holds
S₁[n + 1]

proof

let n be Element of NAT ; :: thesis: ( S₁[n] implies S₁[n + 1] )
assume A5: (z + w) |^ n = (Partial_Sums (Expan (n,z,w))) . n ; :: thesis: S₁[n + 1]
A6: (z + w) |^ (n + 1) = (((z + w) GeoSeq) . n) * (z + w) by COMSEQ_3:def 1
.= ((z + w) (#) (Partial_Sums (Expan (n,z,w)))) . n by A5, VALUED_1:6
.= (Partial_Sums ((z + w) (#) (Expan (n,z,w)))) . n by COMSEQ_3:29 ;

now

let k be Element of NAT ; :: thesis: ((z + w) (#) (Expan (n,z,w))) . k = ((z (#) (Expan (n,z,w))) + (w (#) (Expan (n,z,w)))) . k
thus ((z + w) (#) (Expan (n,z,w))) . k = (z + w) * ((Expan (n,z,w)) . k) by VALUED_1:6
.= (z * ((Expan (n,z,w)) . k)) + (w * ((Expan (n,z,w)) . k))
.= ((z (#) (Expan (n,z,w))) . k) + (w * ((Expan (n,z,w)) . k)) by VALUED_1:6
.= ((z (#) (Expan (n,z,w))) . k) + ((w (#) (Expan (n,z,w))) . k) by VALUED_1:6
.= ((z (#) (Expan (n,z,w))) + (w (#) (Expan (n,z,w)))) . k by VALUED_1:1 ; :: thesis: verum

end;

then (z + w) (#) (Expan (n,z,w)) = (z (#) (Expan (n,z,w))) + (w (#) (Expan (n,z,w))) by FUNCT_2:113;
then A9: (z + w) |^ (n + 1) = ((Partial_Sums (z (#) (Expan (n,z,w)))) + (Partial_Sums (w (#) (Expan (n,z,w))))) . n by A6, COMSEQ_3:27
.= ((Partial_Sums (z (#) (Expan (n,z,w)))) . n) + ((Partial_Sums (w (#) (Expan (n,z,w)))) . n) by VALUED_1:1 ;
A10: (Partial_Sums (z (#) (Expan (n,z,w)))) . (n + 1) = ((Partial_Sums (z (#) (Expan (n,z,w)))) . n) + ((z (#) (Expan (n,z,w))) . (n + 1)) by SERIES_1:def 1
.= ((Partial_Sums (z (#) (Expan (n,z,w)))) . n) + (z * ((Expan (n,z,w)) . (n + 1))) by VALUED_1:6 ;
n < n + 1 by XREAL_1:31;
then A12: (Expan (n,z,w)) . (n + 1) = 0c by Def13;
A13: (Partial_Sums (w (#) (Expan (n,z,w)))) . (n + 1) = ((Partial_Sums (w (#) (Expan (n,z,w)))) . n) + ((w (#) (Expan (n,z,w))) . (n + 1)) by SERIES_1:def 1
.= ((Partial_Sums (w (#) (Expan (n,z,w)))) . n) + (w * ((Expan (n,z,w)) . (n + 1))) by VALUED_1:6 ;
A14: (Partial_Sums (z (#) (Expan (n,z,w)))) . (n + 1) = ((Partial_Sums (Shift (z (#) (Expan (n,z,w))))) . (n + 1)) + ((z (#) (Expan (n,z,w))) . (n + 1)) by Th6;
0 + n < n + 1 by XREAL_1:31;
then (Expan (n,z,w)) . (n + 1) = 0c by Def13;
then z * ((Expan (n,z,w)) . (n + 1)) = 0c ;
then A18: (Partial_Sums (z (#) (Expan (n,z,w)))) . (n + 1) = ((Partial_Sums (Shift (z (#) (Expan (n,z,w))))) . (n + 1)) + 0c by A14, VALUED_1:6
.= (Partial_Sums (Shift (z (#) (Expan (n,z,w))))) . (n + 1) ;

now

let k be Element of NAT ; :: thesis: ((w (#) (Expan (n,z,w))) + (Shift (z (#) (Expan (n,z,w))))) . k = (Expan ((n + 1),z,w)) . k

A20: now

assume A21: n + 1 < k ; :: thesis: ((w (#) (Expan (n,z,w))) + (Shift (z (#) (Expan (n,z,w))))) . k = (Expan ((n + 1),z,w)) . k
A22: 0 + 1 <= n + 1 by XREAL_1:8;
A23: (n + 1) - 1 < k - 1 by A21, XREAL_1:11;
then A24: n + 0 < (k - 1) + 1 by XREAL_1:10;
A25: k - 1 = k -' 1 by A21, A22, XREAL_1:235, XXREAL_0:2;
((w (#) (Expan (n,z,w))) + (Shift (z (#) (Expan (n,z,w))))) . k = ((w (#) (Expan (n,z,w))) . k) + ((Shift (z (#) (Expan (n,z,w)))) . k) by VALUED_1:1
.= (w * ((Expan (n,z,w)) . k)) + ((Shift (z (#) (Expan (n,z,w)))) . k) by VALUED_1:6
.= (w * ((Expan (n,z,w)) . k)) + ((z (#) (Expan (n,z,w))) . (k -' 1)) by A24, Th5
.= (w * ((Expan (n,z,w)) . k)) + (z * ((Expan (n,z,w)) . (k -' 1))) by VALUED_1:6
.= (w * 0c) + (z * ((Expan (n,z,w)) . (k -' 1))) by A24, Def13
.= 0c + (z * 0c) by A23, A25, Def13
.= 0c ;
hence ((w (#) (Expan (n,z,w))) + (Shift (z (#) (Expan (n,z,w))))) . k = (Expan ((n + 1),z,w)) . k by A21, Def13; :: thesis: verum

end;

now

assume A28: k <= n + 1 ; :: thesis: ((w (#) (Expan (n,z,w))) + (Shift (z (#) (Expan (n,z,w))))) . k = (Expan ((n + 1),z,w)) . k

A29: now

assume A30: k = n + 1 ; :: thesis: ((w (#) (Expan (n,z,w))) + (Shift (z (#) (Expan (n,z,w))))) . k = (Expan ((n + 1),z,w)) . k
A31: n < n + 1 by XREAL_1:31;
A32: n -' n = n - n by XREAL_1:235
.= 0 ;
A33: (n + 1) -' (n + 1) = (n + 1) - (n + 1) by XREAL_1:235
.= 0 ;
A34: (Coef n) . n = (n !c) / ((n !c) * (0 !c)) by A32, Def10
.= 1 by Th1, XCMPLX_1:60 ;
A35: (Coef (n + 1)) . (n + 1) = ((n + 1) !c) / (((n + 1) !c) * (0 !c)) by A33, Def10
.= 1 by Th1, XCMPLX_1:60 ;
((w (#) (Expan (n,z,w))) + (Shift (z (#) (Expan (n,z,w))))) . k = ((w (#) (Expan (n,z,w))) . (n + 1)) + ((Shift (z (#) (Expan (n,z,w)))) . (n + 1)) by A30, VALUED_1:1
.= (w * ((Expan (n,z,w)) . (n + 1))) + ((Shift (z (#) (Expan (n,z,w)))) . (n + 1)) by VALUED_1:6
.= (w * 0c) + ((Shift (z (#) (Expan (n,z,w)))) . (n + 1)) by A31, Def13
.= (z (#) (Expan (n,z,w))) . n by Def12
.= z * ((Expan (n,z,w)) . n) by VALUED_1:6
.= z * ((((Coef n) . n) * (z |^ n)) * (w |^ (n -' n))) by Def13
.= (((Coef n) . n) * (((z GeoSeq) . n) * z)) * (w |^ (n -' n))
.= (((Coef (n + 1)) . (n + 1)) * (z |^ (n + 1))) * (w |^ (n -' n)) by A34, A35, COMSEQ_3:def 1
.= (Expan ((n + 1),z,w)) . k by A30, A32, A33, Def13 ;
hence ((w (#) (Expan (n,z,w))) + (Shift (z (#) (Expan (n,z,w))))) . k = (Expan ((n + 1),z,w)) . k ; :: thesis: verum

end;

now

assume A38: k < n + 1 ; :: thesis: ((w (#) (Expan (n,z,w))) + (Shift (z (#) (Expan (n,z,w))))) . k = (Expan ((n + 1),z,w)) . k

A39: now

assume A40: k = 0 ; :: thesis: ((w (#) (Expan (n,z,w))) + (Shift (z (#) (Expan (n,z,w))))) . k = (Expan ((n + 1),z,w)) . k
A41: n -' 0 = n - 0 by XREAL_1:235;
A42: (n + 1) -' 0 = (n + 1) - 0 by XREAL_1:235;
A43: (Coef n) . 0 = (n !c) / ((0 !c) * (n !c)) by A41, Def10
.= 1 by Th1, XCMPLX_1:60 ;
A44: (Coef (n + 1)) . 0 = ((n + 1) !c) / ((0 !c) * ((n + 1) !c)) by A42, Def10
.= 1 by Th1, XCMPLX_1:60 ;
((w (#) (Expan (n,z,w))) + (Shift (z (#) (Expan (n,z,w))))) . k = ((w (#) (Expan (n,z,w))) . 0) + ((Shift (z (#) (Expan (n,z,w)))) . 0) by A40, VALUED_1:1
.= (w * ((Expan (n,z,w)) . 0)) + ((Shift (z (#) (Expan (n,z,w)))) . 0) by VALUED_1:6
.= (w * ((Expan (n,z,w)) . 0)) + 0c by Def12
.= w * ((((Coef n) . 0) * (z |^ 0)) * (w |^ (n -' 0))) by Def13
.= (((Coef n) . 0) * (z |^ 0)) * (((w GeoSeq) . n) * w) by A41
.= (((Coef (n + 1)) . 0) * (z |^ 0)) * (w |^ ((n + 1) -' 0)) by A42, A43, A44, COMSEQ_3:def 1
.= (Expan ((n + 1),z,w)) . k by A40, Def13 ;
hence ((w (#) (Expan (n,z,w))) + (Shift (z (#) (Expan (n,z,w))))) . k = (Expan ((n + 1),z,w)) . k ; :: thesis: verum

end;

now

assume A47: k <> 0 ; :: thesis: ((w (#) (Expan (n,z,w))) + (Shift (z (#) (Expan (n,z,w))))) . k = (Expan ((n + 1),z,w)) . k
then A48: 0 + 1 <= k by INT_1:20;
A49: (k + 1) - 1 <= (n + 1) - 1 by A38, INT_1:20;
k < k + 1 by XREAL_1:31;
then k - 1 <= (k + 1) - 1 by XREAL_1:11;
then k - 1 <= n by A49, XXREAL_0:2;
then A53: k -' 1 <= n by A48, XREAL_1:235;
A54: ((w (#) (Expan (n,z,w))) + (Shift (z (#) (Expan (n,z,w))))) . k = ((w (#) (Expan (n,z,w))) . k) + ((Shift (z (#) (Expan (n,z,w)))) . k) by VALUED_1:1
.= (w * ((Expan (n,z,w)) . k)) + ((Shift (z (#) (Expan (n,z,w)))) . k) by VALUED_1:6
.= (w * ((Expan (n,z,w)) . k)) + ((z (#) (Expan (n,z,w))) . (k -' 1)) by A47, Th5
.= (w * ((Expan (n,z,w)) . k)) + (z * ((Expan (n,z,w)) . (k -' 1))) by VALUED_1:6
.= (w * ((((Coef n) . k) * (z |^ k)) * (w |^ (n -' k)))) + (z * ((Expan (n,z,w)) . (k -' 1))) by A49, Def13
.= ((w * (((Coef n) . k) * (z |^ k))) * (w |^ (n -' k))) + (z * ((((Coef n) . (k -' 1)) * (z |^ (k -' 1))) * (w |^ (n -' (k -' 1))))) by A53, Def13
.= (((Coef n) . k) * ((w * (z |^ k)) * (w |^ (n -' k)))) + (((Coef n) . (k -' 1)) * (((z |^ (k -' 1)) * z) * (w |^ (n -' (k -' 1))))) ;
A55: (n -' k) + 1 = (n - k) + 1 by A49, XREAL_1:235
.= (n + 1) - k
.= (n + 1) -' k by A38, XREAL_1:235 ;
A56: n -' (k -' 1) = n - (k -' 1) by A53, XREAL_1:235
.= n - (k - 1) by A48, XREAL_1:235
.= (n + 1) - k
.= (n + 1) -' k by A38, XREAL_1:235 ;
(k -' 1) + 1 = (k - 1) + 1 by A48, XREAL_1:235
.= k ;
then A58: ( (w |^ (n -' k)) * w = w |^ ((n -' k) + 1) & (z |^ (k -' 1)) * z = z |^ k ) by COMSEQ_3:def 1;
A59: ((Coef n) . k) + ((Coef n) . (k -' 1)) = ((n !c) / ((k !c) * ((n -' k) !c))) + ((Coef n) . (k -' 1)) by A49, Def10
.= ((n !c) / ((k !c) * ((n -' k) !c))) + ((n !c) / (((k -' 1) !c) * ((n -' (k -' 1)) !c))) by A53, Def10 ;
A60: ((k !c) * ((n -' k) !c)) * (((n + 1) - k) + (0 * <i>)) = (k !c) * (((n -' k) !c) * (((n + 1) - k) + (0 * <i>))) ;
A61: (((k -' 1) !c) * ((n -' (k -' 1)) !c)) * (k + (0 * <i>)) = ((k + (0 * <i>)) * ((k -' 1) !c)) * ((n -' (k -' 1)) !c)
.= (k !c) * (((n + 1) -' k) !c) by A47, A56, Th3 ;
((n + 1) - k) + (0 * <i>) <> 0c by A38;
then A63: (n !c) / ((k !c) * ((n -' k) !c)) = ((n !c) * (((n + 1) - k) + (0 * <i>))) / (((k !c) * ((n -' k) !c)) * (((n + 1) - k) + (0 * <i>))) by XCMPLX_1:92
.= ((n !c) * (((n + 1) - k) + (0 * <i>))) / ((k !c) * (((n + 1) -' k) !c)) by A49, A60, Th3 ;
(n !c) / (((k -' 1) !c) * ((n -' (k -' 1)) !c)) = ((n !c) * (k + (0 * <i>))) / ((k !c) * (((n + 1) -' k) !c)) by A47, A61, XCMPLX_1:92;
then ((Coef n) . k) + ((Coef n) . (k -' 1)) = ((n !c) * ((((n + 1) - k) + k) + ((0 + 0) * <i>))) / ((k !c) * (((n + 1) -' k) !c)) by A59, A63
.= ((n + 1) !c) / ((k !c) * (((n + 1) -' k) !c)) by Th1
.= (Coef (n + 1)) . k by A38, Def10 ;
then ((w (#) (Expan (n,z,w))) + (Shift (z (#) (Expan (n,z,w))))) . k = (((Coef (n + 1)) . k) * (z |^ k)) * (w |^ ((n + 1) -' k)) by A54, A55, A56, A58
.= (Expan ((n + 1),z,w)) . k by A38, Def13 ;
hence ((w (#) (Expan (n,z,w))) + (Shift (z (#) (Expan (n,z,w))))) . k = (Expan ((n + 1),z,w)) . k ; :: thesis: verum

end;

hence ((w (#) (Expan (n,z,w))) + (Shift (z (#) (Expan (n,z,w))))) . k = (Expan ((n + 1),z,w)) . k by A39; :: thesis: verum

end;

hence ((w (#) (Expan (n,z,w))) + (Shift (z (#) (Expan (n,z,w))))) . k = (Expan ((n + 1),z,w)) . k by A28, A29, XXREAL_0:1; :: thesis: verum

end;

hence ((w (#) (Expan (n,z,w))) + (Shift (z (#) (Expan (n,z,w))))) . k = (Expan ((n + 1),z,w)) . k by A20; :: thesis: verum

end;

then A67: (w (#) (Expan (n,z,w))) + (Shift (z (#) (Expan (n,z,w)))) = Expan ((n + 1),z,w) by FUNCT_2:113;
thus (z + w) |^ (n + 1) = ((Partial_Sums (w (#) (Expan (n,z,w)))) + (Partial_Sums (Shift (z (#) (Expan (n,z,w)))))) . (n + 1) by A9, A10, A12, A13, A18, VALUED_1:1
.= (Partial_Sums (Expan ((n + 1),z,w))) . (n + 1) by A67, COMSEQ_3:27 ; :: thesis: verum

end;

for n being Element of NAT holds S₁[n] from NAT_1:sch 1(A3, A4);
hence (z + w) |^ n = (Partial_Sums (Expan (n,z,w))) . n ; :: thesis: verum