let X be Complex_Banach_Algebra; for n being Element of NAT
for z, w being Element of X st z,w are_commutative holds
(z + w) #N n = (Partial_Sums (Expan n,z,w)) . n
let n be Element of NAT ; for z, w being Element of X st z,w are_commutative holds
(z + w) #N n = (Partial_Sums (Expan n,z,w)) . n
let z, w be Element of X; ( z,w are_commutative implies (z + w) #N n = (Partial_Sums (Expan n,z,w)) . n )
assume A1:
z,w are_commutative
; (z + w) #N n = (Partial_Sums (Expan n,z,w)) . n
defpred S1[ Element of NAT ] means (z + w) #N $1 = (Partial_Sums (Expan $1,z,w)) . $1;
A2:
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 A3:
(z + w) #N n = (Partial_Sums (Expan n,z,w)) . n
;
S1[n + 1]
A4:
n < n + 1
by XREAL_1:31;
now let k be
Element of
NAT ;
(((Expan n,z,w) * w) + (Shift ((Expan n,z,w) * z))) . k = (Expan (n + 1),z,w) . kA5:
now A6:
now assume A7:
k < n + 1
;
(((Expan n,z,w) * w) + (Shift ((Expan n,z,w) * z))) . k = (Expan (n + 1),z,w) . kA8:
now A9:
(k + 1) - 1
<= (n + 1) - 1
by A7, INT_1:20;
then A10:
(n -' k) + 1 =
(n - k) + 1
by XREAL_1:235
.=
(n + 1) - k
.=
(n + 1) -' k
by A7, XREAL_1:235
;
(n + 1) - k <> 0
by A7;
then A11:
(n !c ) / ((k !c ) * ((n -' k) !c )) =
((n !c ) * ((n + 1) - k)) / (((k !c ) * ((n -' k) !c )) * (((n + 1) - k) + (0 * <i> )))
by XCMPLX_1:92
.=
((n !c ) * ((n + 1) - k)) / ((k !c ) * (((n -' k) !c ) * (((n + 1) - k) + (0 * <i> ))))
.=
((n !c ) * ((n + 1) - k)) / ((k !c ) * (((n + 1) -' k) !c ))
by A9, SIN_COS:3
;
assume A12:
k <> 0
;
(((Expan n,z,w) * w) + (Shift ((Expan n,z,w) * z))) . k = (Expan (n + 1),z,w) . kthen A13:
0 < k
by NAT_1:3;
then A14:
0 + 1
<= k
by INT_1:20;
then A15:
(k -' 1) + 1 =
(k - 1) + 1
by XREAL_1:235
.=
k
;
k < k + 1
by XREAL_1:31;
then
k - 1
<= (k + 1) - 1
by XREAL_1:11;
then
k - 1
<= n
by A9, XXREAL_0:2;
then A16:
k -' 1
<= n
by A14, XREAL_1:235;
then A17:
n -' (k -' 1) =
n - (k -' 1)
by XREAL_1:235
.=
n - (k - 1)
by A14, XREAL_1:235
.=
(n + 1) - k
.=
(n + 1) -' k
by A7, XREAL_1:235
;
(((k -' 1) !c ) * ((n -' (k -' 1)) !c )) * k =
(k * ((k -' 1) !c )) * ((n -' (k -' 1)) !c )
.=
((k + (0 * <i> )) * ((k -' 1) !c )) * ((n -' (k -' 1)) !c )
.=
(k !c ) * (((n + 1) -' k) !c )
by A13, A17, SIN_COS:3
;
then A18:
(n !c ) / (((k -' 1) !c ) * ((n -' (k -' 1)) !c )) = ((n !c ) * k) / ((k !c ) * (((n + 1) -' k) !c ))
by A12, XCMPLX_1:92;
((Coef n) . k) + ((Coef n) . (k -' 1)) =
((n !c ) / ((k !c ) * ((n -' k) !c ))) + ((Coef n) . (k -' 1))
by A9, SIN_COS:def 10
.=
((n !c ) / ((k !c ) * ((n -' k) !c ))) + ((n !c ) / (((k -' 1) !c ) * ((n -' (k -' 1)) !c )))
by A16, SIN_COS:def 10
;
then A19:
((Coef n) . k) + ((Coef n) . (k -' 1)) =
(((n !c ) * ((n + 1) - k)) + ((n !c ) * k)) / ((k !c ) * (((n + 1) -' k) !c ))
by A11, A18, XCMPLX_1:63
.=
((n !c ) * (((n + 1) - k) + k)) / ((k !c ) * (((n + 1) -' k) !c ))
.=
((n !c ) * ((((n + 1) - k) + k) + ((0 + 0 ) * <i> ))) / ((k !c ) * (((n + 1) -' k) !c ))
.=
((n + 1) !c ) / ((k !c ) * (((n + 1) -' k) !c ))
by SIN_COS:1
.=
(Coef (n + 1)) . k
by A7, SIN_COS:def 10
;
A20:
n -' (k -' 1) =
n - (k -' 1)
by A16, XREAL_1:235
.=
n - (k - 1)
by A14, XREAL_1:235
.=
(n + 1) - k
.=
(n + 1) -' k
by A7, XREAL_1:235
;
(((Expan n,z,w) * w) + (Shift ((Expan n,z,w) * z))) . k =
(((Expan n,z,w) * w) . k) + ((Shift ((Expan n,z,w) * z)) . k)
by NORMSP_1:def 5
.=
(((Expan n,z,w) . k) * w) + ((Shift ((Expan n,z,w) * z)) . k)
by CLOPBAN3:def 9
.=
(((Expan n,z,w) . k) * w) + (((Expan n,z,w) * z) . (k -' 1))
by A12, LOPBAN_4:15, NAT_1:3
.=
(((Expan n,z,w) . k) * w) + (((Expan n,z,w) . (k -' 1)) * z)
by CLOPBAN3:def 9
.=
(((((Coef n) . k) * (z #N k)) * (w #N (n -' k))) * w) + (((Expan n,z,w) . (k -' 1)) * z)
by A9, Def4
.=
(((((Coef n) . k) * (z #N k)) * (w #N (n -' k))) * w) + (((((Coef n) . (k -' 1)) * (z #N (k -' 1))) * (w #N (n -' (k -' 1)))) * z)
by A16, Def4
.=
((((Coef n) . k) * (z #N k)) * ((w #N (n -' k)) * w)) + (((((Coef n) . (k -' 1)) * (z #N (k -' 1))) * (w #N (n -' (k -' 1)))) * z)
by CLOPBAN3:42
.=
((((Coef n) . k) * (z #N k)) * (w #N ((n -' k) + 1))) + (((((Coef n) . (k -' 1)) * (z #N (k -' 1))) * (w #N (n -' (k -' 1)))) * z)
by Lm1
.=
((((Coef n) . k) * (z #N k)) * (w #N ((n -' k) + 1))) + ((((Coef n) . (k -' 1)) * (z #N (k -' 1))) * ((w #N (n -' (k -' 1))) * z))
by CLOPBAN3:42
.=
((((Coef n) . k) * (z #N k)) * (w #N ((n -' k) + 1))) + ((((Coef n) . (k -' 1)) * (z #N (k -' 1))) * (z * (w #N (n -' (k -' 1)))))
by A1, Lm2
.=
((((Coef n) . k) * (z #N k)) * (w #N ((n -' k) + 1))) + (((((Coef n) . (k -' 1)) * (z #N (k -' 1))) * z) * (w #N (n -' (k -' 1))))
by CLOPBAN3:42
.=
((((Coef n) . k) * (z #N k)) * (w #N ((n -' k) + 1))) + ((((Coef n) . (k -' 1)) * ((z #N (k -' 1)) * z)) * (w #N (n -' (k -' 1))))
by CLOPBAN3:42
.=
((((Coef n) . k) * (z #N k)) * (w #N ((n -' k) + 1))) + ((((Coef n) . (k -' 1)) * (z #N ((k -' 1) + 1))) * (w #N (n -' (k -' 1))))
by Lm1
;
then (((Expan n,z,w) * w) + (Shift ((Expan n,z,w) * z))) . k =
(((Coef n) . k) * ((z #N k) * (w #N ((n + 1) -' k)))) + ((((Coef n) . (k -' 1)) * (z #N k)) * (w #N ((n + 1) -' k)))
by A10, A20, A15, CLOPBAN3:42
.=
(((Coef n) . k) * ((z #N k) * (w #N ((n + 1) -' k)))) + (((Coef n) . (k -' 1)) * ((z #N k) * (w #N ((n + 1) -' k))))
by CLOPBAN3:42
.=
(((Coef n) . k) + ((Coef n) . (k -' 1))) * ((z #N k) * (w #N ((n + 1) -' k)))
by CLOPBAN3:42
;
then (((Expan n,z,w) * w) + (Shift ((Expan n,z,w) * z))) . k =
(((Coef (n + 1)) . k) * (z #N k)) * (w #N ((n + 1) -' k))
by A19, CLOPBAN3:42
.=
(Expan (n + 1),z,w) . k
by A7, Def4
;
hence
(((Expan n,z,w) * w) + (Shift ((Expan n,z,w) * z))) . k = (Expan (n + 1),z,w) . k
;
verum end; now A21:
(n + 1) -' 0 = (n + 1) - 0
by NAT_1:2, XREAL_1:235;
then A22:
(Coef (n + 1)) . 0 =
((n + 1) !c ) / (1 * ((n + 1) !c ))
by SIN_COS:1, SIN_COS:def 10
.=
1
by SIN_COS:1, XCMPLX_1:60
;
A23:
n -' 0 = n - 0
by NAT_1:2, XREAL_1:235;
then A24:
(Coef n) . 0 =
(n !c ) / (1 * (n !c ))
by SIN_COS:1, SIN_COS:def 10
.=
1
by SIN_COS:1, XCMPLX_1:60
;
A25:
0 <= n + 1
by NAT_1:2;
A26:
0 <= n
by NAT_1:2;
assume A27:
k = 0
;
(((Expan n,z,w) * w) + (Shift ((Expan n,z,w) * z))) . k = (Expan (n + 1),z,w) . kthen (((Expan n,z,w) * w) + (Shift ((Expan n,z,w) * z))) . k =
(((Expan n,z,w) * w) . 0 ) + ((Shift ((Expan n,z,w) * z)) . 0 )
by NORMSP_1:def 5
.=
(((Expan n,z,w) . 0 ) * w) + ((Shift ((Expan n,z,w) * z)) . 0 )
by CLOPBAN3:def 9
.=
(((Expan n,z,w) . 0 ) * w) + (0. X)
by LOPBAN_4:def 5
.=
((Expan n,z,w) . 0 ) * w
by CLOPBAN3:42
.=
((((Coef n) . 0 ) * (z #N 0 )) * (w #N (n -' 0 ))) * w
by A26, Def4
.=
(((Coef n) . 0 ) * (z #N 0 )) * ((w #N (n -' 0 )) * w)
by CLOPBAN3:42
.=
(((Coef (n + 1)) . 0 ) * (z #N 0 )) * (w #N ((n + 1) -' 0 ))
by A23, A21, A24, A22, Lm1
.=
(Expan (n + 1),z,w) . k
by A27, A25, Def4
;
hence
(((Expan n,z,w) * w) + (Shift ((Expan n,z,w) * z))) . k = (Expan (n + 1),z,w) . k
;
verum end; hence
(((Expan n,z,w) * w) + (Shift ((Expan n,z,w) * z))) . k = (Expan (n + 1),z,w) . k
by A8;
verum end; A28:
now A29:
(n + 1) -' (n + 1) =
(n + 1) - (n + 1)
by XREAL_1:235
.=
0
;
then A30:
(Coef (n + 1)) . (n + 1) =
((n + 1) !c ) / (((n + 1) !c ) * 1)
by SIN_COS:1, SIN_COS:def 10
.=
1
by SIN_COS:1, XCMPLX_1:60
;
A31:
n < n + 1
by XREAL_1:31;
A32:
n -' n =
n - n
by XREAL_1:235
.=
0
;
then A33:
(Coef n) . n =
(n !c ) / ((n !c ) * 1)
by SIN_COS:1, SIN_COS:def 10
.=
1
by SIN_COS:1, XCMPLX_1:60
;
assume A34:
k = n + 1
;
(((Expan n,z,w) * w) + (Shift ((Expan n,z,w) * z))) . k = (Expan (n + 1),z,w) . kthen (((Expan n,z,w) * w) + (Shift ((Expan n,z,w) * z))) . k =
(((Expan n,z,w) * w) . (n + 1)) + ((Shift ((Expan n,z,w) * z)) . (n + 1))
by NORMSP_1:def 5
.=
(((Expan n,z,w) . (n + 1)) * w) + ((Shift ((Expan n,z,w) * z)) . (n + 1))
by CLOPBAN3:def 9
.=
((0. X) * w) + ((Shift ((Expan n,z,w) * z)) . (n + 1))
by A31, Def4
.=
(0. X) + ((Shift ((Expan n,z,w) * z)) . (n + 1))
by CLOPBAN3:42
.=
(Shift ((Expan n,z,w) * z)) . (n + 1)
by CLOPBAN3:42
.=
((Expan n,z,w) * z) . n
by LOPBAN_4:def 5
.=
((Expan n,z,w) . n) * z
by CLOPBAN3:def 9
.=
((((Coef n) . n) * (z #N n)) * (w #N (n -' n))) * z
by Def4
.=
(((Coef n) . n) * (z #N n)) * ((w #N (n -' n)) * z)
by CLOPBAN3:42
.=
(((Coef n) . n) * (z #N n)) * (z * (w #N (n -' n)))
by A1, Lm2
.=
((((Coef n) . n) * (z #N n)) * z) * (w #N (n -' n))
by CLOPBAN3:42
.=
(((Coef n) . n) * ((z #N n) * z)) * (w #N (n -' n))
by CLOPBAN3:42
.=
(((Coef (n + 1)) . (n + 1)) * (z #N (n + 1))) * (w #N (n -' n))
by A33, A30, Lm1
.=
(Expan (n + 1),z,w) . k
by A34, A32, A29, Def4
;
hence
(((Expan n,z,w) * w) + (Shift ((Expan n,z,w) * z))) . k = (Expan (n + 1),z,w) . k
;
verum end; assume
k <= n + 1
;
(((Expan n,z,w) * w) + (Shift ((Expan n,z,w) * z))) . k = (Expan (n + 1),z,w) . khence
(((Expan n,z,w) * w) + (Shift ((Expan n,z,w) * z))) . k = (Expan (n + 1),z,w) . k
by A28, A6, XXREAL_0:1;
verum now assume A35:
n + 1
< k
;
(((Expan n,z,w) * w) + (Shift ((Expan n,z,w) * z))) . k = (Expan (n + 1),z,w) . kthen A36:
(n + 1) - 1
< k - 1
by XREAL_1:11;
then A37:
n + 0 < (k - 1) + 1
by XREAL_1:10;
0 <= n
by NAT_1:2;
then A38:
0 + 1
<= n + 1
by XREAL_1:8;
then A39:
k - 1
= k -' 1
by A35, XREAL_1:235, XXREAL_0:2;
(((Expan n,z,w) * w) + (Shift ((Expan n,z,w) * z))) . k =
(((Expan n,z,w) * w) . k) + ((Shift ((Expan n,z,w) * z)) . k)
by NORMSP_1:def 5
.=
(((Expan n,z,w) . k) * w) + ((Shift ((Expan n,z,w) * z)) . k)
by CLOPBAN3:def 9
.=
(((Expan n,z,w) . k) * w) + (((Expan n,z,w) * z) . (k -' 1))
by A35, A38, LOPBAN_4:15
.=
(((Expan n,z,w) . k) * w) + (((Expan n,z,w) . (k -' 1)) * z)
by CLOPBAN3:def 9
.=
((0. X) * w) + (((Expan n,z,w) . (k -' 1)) * z)
by A37, Def4
.=
(0. X) + (((Expan n,z,w) . (k -' 1)) * z)
by CLOPBAN3:42
.=
(0. X) + ((0. X) * z)
by A36, A39, Def4
.=
(0. X) + (0. X)
by CLOPBAN3:42
.=
0. X
by CLOPBAN3:42
;
hence
(((Expan n,z,w) * w) + (Shift ((Expan n,z,w) * z))) . k = (Expan (n + 1),z,w) . k
by A35, Def4;
verum end; hence
(((Expan n,z,w) * w) + (Shift ((Expan n,z,w) * z))) . k = (Expan (n + 1),z,w) . k
by A5;
verum end;
then A40:
((Expan n,z,w) * w) + (Shift ((Expan n,z,w) * z)) = Expan (n + 1),
z,
w
by FUNCT_2:113;
A41:
n < n + 1
by XREAL_1:31;
(Partial_Sums ((Expan n,z,w) * w)) . (n + 1) =
((Partial_Sums ((Expan n,z,w) * w)) . n) + (((Expan n,z,w) * w) . (n + 1))
by BHSP_4:def 1
.=
((Partial_Sums ((Expan n,z,w) * w)) . n) + (((Expan n,z,w) . (n + 1)) * w)
by CLOPBAN3:def 9
;
then A42:
(Partial_Sums ((Expan n,z,w) * w)) . (n + 1) =
((Partial_Sums ((Expan n,z,w) * w)) . n) + ((0. X) * w)
by A41, Def4
.=
((Partial_Sums ((Expan n,z,w) * w)) . n) + (0. X)
by CLOPBAN3:42
.=
(Partial_Sums ((Expan n,z,w) * w)) . n
by CLOPBAN3:42
;
(Partial_Sums ((Expan n,z,w) * z)) . (n + 1) =
((Partial_Sums ((Expan n,z,w) * z)) . n) + (((Expan n,z,w) * z) . (n + 1))
by BHSP_4:def 1
.=
((Partial_Sums ((Expan n,z,w) * z)) . n) + (((Expan n,z,w) . (n + 1)) * z)
by CLOPBAN3:def 9
;
then A43:
(Partial_Sums ((Expan n,z,w) * z)) . (n + 1) =
((Partial_Sums ((Expan n,z,w) * z)) . n) + ((0. X) * z)
by A4, Def4
.=
((Partial_Sums ((Expan n,z,w) * z)) . n) + (0. X)
by CLOPBAN3:42
.=
(Partial_Sums ((Expan n,z,w) * z)) . n
by CLOPBAN3:42
;
0 + n < n + 1
by XREAL_1:31;
then A44:
(Expan n,z,w) . (n + 1) = 0. X
by Def4;
(Partial_Sums ((Expan n,z,w) * z)) . (n + 1) = ((Partial_Sums (Shift ((Expan n,z,w) * z))) . (n + 1)) + (((Expan n,z,w) * z) . (n + 1))
by Th15;
then A45:
(Partial_Sums ((Expan n,z,w) * z)) . (n + 1) =
((Partial_Sums (Shift ((Expan n,z,w) * z))) . (n + 1)) + (((Expan n,z,w) . (n + 1)) * z)
by CLOPBAN3:def 9
.=
((Partial_Sums (Shift ((Expan n,z,w) * z))) . (n + 1)) + (0. X)
by A44, CLOPBAN3:42
.=
(Partial_Sums (Shift ((Expan n,z,w) * z))) . (n + 1)
by CLOPBAN3:42
;
now let k be
Element of
NAT ;
((Expan n,z,w) * (z + w)) . k = (((Expan n,z,w) * z) + ((Expan n,z,w) * w)) . kthus ((Expan n,z,w) * (z + w)) . k =
((Expan n,z,w) . k) * (z + w)
by CLOPBAN3:def 9
.=
(((Expan n,z,w) . k) * z) + (((Expan n,z,w) . k) * w)
by CLOPBAN3:42
.=
(((Expan n,z,w) * z) . k) + (((Expan n,z,w) . k) * w)
by CLOPBAN3:def 9
.=
(((Expan n,z,w) * z) . k) + (((Expan n,z,w) * w) . k)
by CLOPBAN3:def 9
.=
(((Expan n,z,w) * z) + ((Expan n,z,w) * w)) . k
by NORMSP_1:def 5
;
verum end;
then A46:
(Expan n,z,w) * (z + w) = ((Expan n,z,w) * z) + ((Expan n,z,w) * w)
by FUNCT_2:113;
(z + w) #N (n + 1) =
((z + w) GeoSeq ) . (n + 1)
by CLOPBAN3:def 13
.=
(((z + w) GeoSeq ) . n) * (z + w)
by CLOPBAN3:def 12
.=
((Partial_Sums (Expan n,z,w)) . n) * (z + w)
by A3, CLOPBAN3:def 13
.=
((Partial_Sums (Expan n,z,w)) * (z + w)) . n
by CLOPBAN3:def 9
.=
(Partial_Sums ((Expan n,z,w) * (z + w))) . n
by Th9
;
then (z + w) #N (n + 1) =
((Partial_Sums ((Expan n,z,w) * z)) + (Partial_Sums ((Expan n,z,w) * w))) . n
by A46, CLOPBAN3:19
.=
((Partial_Sums ((Expan n,z,w) * z)) . n) + ((Partial_Sums ((Expan n,z,w) * w)) . n)
by NORMSP_1:def 5
;
hence (z + w) #N (n + 1) =
((Partial_Sums ((Expan n,z,w) * w)) + (Partial_Sums (Shift ((Expan n,z,w) * z)))) . (n + 1)
by A43, A42, A45, NORMSP_1:def 5
.=
(Partial_Sums (Expan (n + 1),z,w)) . (n + 1)
by A40, CLOPBAN3:19
;
verum
end;
A47: (z + w) #N 0 =
((z + w) GeoSeq ) . 0
by CLOPBAN3:def 13
.=
1. X
by CLOPBAN3:def 12
;
A48: 0 -' 0 =
0 - 0
by XREAL_0:def 2
.=
0
;
(Partial_Sums (Expan 0 ,z,w)) . 0 =
(Expan 0 ,z,w) . 0
by BHSP_4:def 1
.=
(((Coef 0 ) . 0 ) * (z #N 0 )) * (w #N 0 )
by A48, Def4
.=
((1r / (1r * 1r )) * (z #N 0 )) * (w #N 0 )
by A48, COMPLEX1:def 7, SIN_COS:1, SIN_COS:def 10
.=
(z #N 0 ) * (w #N 0 )
by CLVECT_1:def 2, COMPLEX1:def 7
.=
((z GeoSeq ) . 0 ) * (w #N 0 )
by CLOPBAN3:def 13
.=
((z GeoSeq ) . 0 ) * ((w GeoSeq ) . 0 )
by CLOPBAN3:def 13
.=
(1. X) * ((w GeoSeq ) . 0 )
by CLOPBAN3:def 12
.=
(1. X) * (1. X)
by CLOPBAN3:def 12
.=
1. X
by CLOPBAN3:42
;
then A49:
S1[ 0 ]
by A47;
for n being Element of NAT holds S1[n]
from NAT_1:sch 1(A49, A2);
hence
(z + w) #N n = (Partial_Sums (Expan n,z,w)) . n
; verum