let z, w be Element of COMPLEX ; for n being Element of NAT holds (z + w) |^ n = (Partial_Sums (Expan n,z,w)) . n
let n be Element of NAT ; (z + w) |^ n = (Partial_Sums (Expan n,z,w)) . n
A1:
0 -' 0 = 0
by XREAL_1:234;
defpred S1[ 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:
S1[ 0 ]
by COMSEQ_3:def 1;
A4:
for n being Element of NAT st S1[n] holds
S1[n + 1]
proof
let n be
Element of
NAT ;
( S1[n] implies S1[n + 1] )
assume A5:
(z + w) |^ n = (Partial_Sums (Expan n,z,w)) . n
;
S1[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 ;
((z + w) (#) (Expan n,z,w)) . k = ((z (#) (Expan n,z,w)) + (w (#) (Expan n,z,w))) . kthus ((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
;
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 ;
((w (#) (Expan n,z,w)) + (Shift (z (#) (Expan n,z,w)))) . k = (Expan (n + 1),z,w) . kA20:
now assume A21:
n + 1
< k
;
((w (#) (Expan n,z,w)) + (Shift (z (#) (Expan n,z,w)))) . k = (Expan (n + 1),z,w) . kA22:
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;
verum end; now assume A28:
k <= n + 1
;
((w (#) (Expan n,z,w)) + (Shift (z (#) (Expan n,z,w)))) . k = (Expan (n + 1),z,w) . kA29:
now assume A30:
k = n + 1
;
((w (#) (Expan n,z,w)) + (Shift (z (#) (Expan n,z,w)))) . k = (Expan (n + 1),z,w) . kA31:
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
;
verum end; now assume A38:
k < n + 1
;
((w (#) (Expan n,z,w)) + (Shift (z (#) (Expan n,z,w)))) . k = (Expan (n + 1),z,w) . kA39:
now assume A40:
k = 0
;
((w (#) (Expan n,z,w)) + (Shift (z (#) (Expan n,z,w)))) . k = (Expan (n + 1),z,w) . kA41:
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
;
verum end; now assume A47:
k <> 0
;
((w (#) (Expan n,z,w)) + (Shift (z (#) (Expan n,z,w)))) . k = (Expan (n + 1),z,w) . kthen 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
;
verum end; hence
((w (#) (Expan n,z,w)) + (Shift (z (#) (Expan n,z,w)))) . k = (Expan (n + 1),z,w) . k
by A39;
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;
verum end; hence
((w (#) (Expan n,z,w)) + (Shift (z (#) (Expan n,z,w)))) . k = (Expan (n + 1),z,w) . k
by A20;
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
;
verum
end;
for n being Element of NAT holds S1[n]
from NAT_1:sch 1(A3, A4);
hence
(z + w) |^ n = (Partial_Sums (Expan n,z,w)) . n
; verum