let X be Complex_Banach_Algebra; for n being 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 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[ Nat] means (z + w) #N $1 = (Partial_Sums (Expan ($1,z,w))) . $1;
A2:
for n being Nat st S1[n] holds
S1[n + 1]
proof
let n be
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:29;
now for k being Element of NAT holds (((Expan (n,z,w)) * w) + (Shift ((Expan (n,z,w)) * z))) . k = (Expan ((n + 1),z,w)) . klet k be
Element of
NAT ;
(((Expan (n,z,w)) * w) + (Shift ((Expan (n,z,w)) * z))) . k = (Expan ((n + 1),z,w)) . kA5:
n in NAT
by ORDINAL1:def 12;
A6:
now ( k <= n + 1 implies (((Expan (n,z,w)) * w) + (Shift ((Expan (n,z,w)) * z))) . k = (Expan ((n + 1),z,w)) . k )A7:
now ( k < n + 1 implies (((Expan (n,z,w)) * w) + (Shift ((Expan (n,z,w)) * z))) . k = (Expan ((n + 1),z,w)) . k )assume A8:
k < n + 1
;
(((Expan (n,z,w)) * w) + (Shift ((Expan (n,z,w)) * z))) . k = (Expan ((n + 1),z,w)) . kA9:
now ( k <> 0 implies (((Expan (n,z,w)) * w) + (Shift ((Expan (n,z,w)) * z))) . k = (Expan ((n + 1),z,w)) . k )A10:
(k + 1) - 1
<= (n + 1) - 1
by A8, A5, INT_1:7;
then A11:
(n -' k) + 1 =
(n - k) + 1
by XREAL_1:233
.=
(n + 1) - k
.=
(n + 1) -' k
by A8, XREAL_1:233
;
(n + 1) - k <> 0
by A8;
then A12:
(n !) / ((k !) * ((n -' k) !)) =
((n !) * ((n + 1) - k)) / (((k !) * ((n -' k) !)) * (((n + 1) - k) + (0 * <i>)))
by XCMPLX_1:91
.=
((n !) * ((n + 1) - k)) / ((k !) * (((n -' k) !) * (((n + 1) - k) + (0 * <i>))))
.=
((n !) * ((n + 1) - k)) / ((k !) * (((n + 1) -' k) !))
by A10, SIN_COS:2
;
assume A13:
k <> 0
;
(((Expan (n,z,w)) * w) + (Shift ((Expan (n,z,w)) * z))) . k = (Expan ((n + 1),z,w)) . kthen A14:
0 < k
;
then A15:
0 + 1
<= k
by INT_1:7;
then A16:
(k -' 1) + 1 =
(k - 1) + 1
by XREAL_1:233
.=
k
;
k < k + 1
by XREAL_1:29;
then
k - 1
<= (k + 1) - 1
by XREAL_1:9;
then
k - 1
<= n
by A10, XXREAL_0:2;
then A17:
k -' 1
<= n
by A15, XREAL_1:233;
then A18:
n -' (k -' 1) =
n - (k -' 1)
by XREAL_1:233
.=
n - (k - 1)
by A15, XREAL_1:233
.=
(n + 1) - k
.=
(n + 1) -' k
by A8, XREAL_1:233
;
(((k -' 1) !) * ((n -' (k -' 1)) !)) * k =
(k * ((k -' 1) !)) * ((n -' (k -' 1)) !)
.=
((k + (0 * <i>)) * ((k -' 1) !)) * ((n -' (k -' 1)) !)
.=
(k !) * (((n + 1) -' k) !)
by A14, A18, SIN_COS:2
;
then A19:
(n !) / (((k -' 1) !) * ((n -' (k -' 1)) !)) = ((n !) * k) / ((k !) * (((n + 1) -' k) !))
by A13, XCMPLX_1:91;
((Coef n) . k) + ((Coef n) . (k -' 1)) =
((n !) / ((k !) * ((n -' k) !))) + ((Coef n) . (k -' 1))
by A10, SIN_COS:def 6
.=
((n !) / ((k !) * ((n -' k) !))) + ((n !) / (((k -' 1) !) * ((n -' (k -' 1)) !)))
by A17, SIN_COS:def 6
;
then A20:
((Coef n) . k) + ((Coef n) . (k -' 1)) =
(((n !) * ((n + 1) - k)) + ((n !) * k)) / ((k !) * (((n + 1) -' k) !))
by A12, A19, XCMPLX_1:62
.=
((n !) * (((n + 1) - k) + k)) / ((k !) * (((n + 1) -' k) !))
.=
((n !) * ((((n + 1) - k) + k) + ((0 + 0) * <i>))) / ((k !) * (((n + 1) -' k) !))
.=
((n + 1) !) / ((k !) * (((n + 1) -' k) !))
by SIN_COS:1
.=
(Coef (n + 1)) . k
by A8, SIN_COS:def 6
;
A21:
n -' (k -' 1) =
n - (k -' 1)
by A17, XREAL_1:233
.=
n - (k - 1)
by A15, XREAL_1:233
.=
(n + 1) - k
.=
(n + 1) -' k
by A8, XREAL_1:233
;
(((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 2
.=
(((Expan (n,z,w)) . k) * w) + ((Shift ((Expan (n,z,w)) * z)) . k)
by LOPBAN_3:def 6
.=
(((Expan (n,z,w)) . k) * w) + (((Expan (n,z,w)) * z) . (k -' 1))
by A13, LOPBAN_4:15
.=
(((Expan (n,z,w)) . k) * w) + (((Expan (n,z,w)) . (k -' 1)) * z)
by LOPBAN_3:def 6
.=
(((((Coef n) . k) * (z #N k)) * (w #N (n -' k))) * w) + (((Expan (n,z,w)) . (k -' 1)) * z)
by A10, Def2
.=
(((((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 A17, Def2
.=
((((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 GROUP_1:def 3
.=
((((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 GROUP_1:def 3
.=
((((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 GROUP_1:def 3
.=
((((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:38
.=
((((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 A11, A21, A16, CLOPBAN3:38
.=
(((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:38
.=
(((Coef n) . k) + ((Coef n) . (k -' 1))) * ((z #N k) * (w #N ((n + 1) -' k)))
by CLOPBAN3:38
;
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 A20, CLOPBAN3:38
.=
(Expan ((n + 1),z,w)) . k
by A8, Def2
;
hence
(((Expan (n,z,w)) * w) + (Shift ((Expan (n,z,w)) * z))) . k = (Expan ((n + 1),z,w)) . k
;
verum end; now ( k = 0 implies (((Expan (n,z,w)) * w) + (Shift ((Expan (n,z,w)) * z))) . k = (Expan ((n + 1),z,w)) . k )A22:
(n + 1) -' 0 = (n + 1) - 0
by XREAL_1:233;
then A23:
(Coef (n + 1)) . 0 =
((n + 1) !) / (1 * ((n + 1) !))
by SIN_COS:1, SIN_COS:def 6
.=
1
by XCMPLX_1:60
;
A24:
n -' 0 = n - 0
by XREAL_1:233;
then A25:
(Coef n) . 0 =
(n !) / (1 * (n !))
by SIN_COS:1, SIN_COS:def 6
.=
1
by XCMPLX_1:60
;
assume A26:
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 2
.=
(((Expan (n,z,w)) . 0) * w) + ((Shift ((Expan (n,z,w)) * z)) . 0)
by LOPBAN_3:def 6
.=
(((Expan (n,z,w)) . 0) * w) + (0. X)
by LOPBAN_4:def 5
.=
((Expan (n,z,w)) . 0) * w
by RLVECT_1:def 4
.=
((((Coef n) . 0) * (z #N 0)) * (w #N (n -' 0))) * w
by Def2
.=
(((Coef n) . 0) * (z #N 0)) * ((w #N (n -' 0)) * w)
by GROUP_1:def 3
.=
(((Coef (n + 1)) . 0) * (z #N 0)) * (w #N ((n + 1) -' 0))
by A24, A22, A25, A23, Lm1
.=
(Expan ((n + 1),z,w)) . k
by A26, Def2
;
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 A9;
verum end; A27:
now ( k = n + 1 implies (((Expan (n,z,w)) * w) + (Shift ((Expan (n,z,w)) * z))) . k = (Expan ((n + 1),z,w)) . k )A28:
(n + 1) -' (n + 1) =
(n + 1) - (n + 1)
by XREAL_1:233
.=
0
;
then A29:
(Coef (n + 1)) . (n + 1) =
((n + 1) !) / (((n + 1) !) * 1)
by SIN_COS:1, SIN_COS:def 6
.=
1
by XCMPLX_1:60
;
A30:
n < n + 1
by XREAL_1:29;
A31:
n -' n =
n - n
by XREAL_1:233
.=
0
;
then A32:
(Coef n) . n =
(n !) / ((n !) * 1)
by SIN_COS:1, SIN_COS:def 6
.=
1
by XCMPLX_1:60
;
assume A33:
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 2
.=
(((Expan (n,z,w)) . (n + 1)) * w) + ((Shift ((Expan (n,z,w)) * z)) . (n + 1))
by LOPBAN_3:def 6
.=
((0. X) * w) + ((Shift ((Expan (n,z,w)) * z)) . (n + 1))
by A30, Def2
.=
(0. X) + ((Shift ((Expan (n,z,w)) * z)) . (n + 1))
by CLOPBAN3:38
.=
(Shift ((Expan (n,z,w)) * z)) . (n + 1)
by RLVECT_1:def 4
.=
((Expan (n,z,w)) * z) . n
by LOPBAN_4:def 5
.=
((Expan (n,z,w)) . n) * z
by LOPBAN_3:def 6
.=
((((Coef n) . n) * (z #N n)) * (w #N (n -' n))) * z
by Def2
.=
(((Coef n) . n) * (z #N n)) * ((w #N (n -' n)) * z)
by GROUP_1:def 3
.=
(((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 GROUP_1:def 3
.=
(((Coef n) . n) * ((z #N n) * z)) * (w #N (n -' n))
by CLOPBAN3:38
.=
(((Coef (n + 1)) . (n + 1)) * (z #N (n + 1))) * (w #N (n -' n))
by A32, A29, Lm1
.=
(Expan ((n + 1),z,w)) . k
by A33, A31, A28, Def2
;
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 A27, A7, XXREAL_0:1;
verum end; now ( n + 1 < k implies (((Expan (n,z,w)) * w) + (Shift ((Expan (n,z,w)) * z))) . k = (Expan ((n + 1),z,w)) . k )assume A34:
n + 1
< k
;
(((Expan (n,z,w)) * w) + (Shift ((Expan (n,z,w)) * z))) . k = (Expan ((n + 1),z,w)) . kthen A35:
(n + 1) - 1
< k - 1
by XREAL_1:9;
then A36:
n + 0 < (k - 1) + 1
by XREAL_1:8;
0 + 1
<= n + 1
by XREAL_1:6;
then A37:
k - 1
= k -' 1
by A34, XREAL_1:233, 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 2
.=
(((Expan (n,z,w)) . k) * w) + ((Shift ((Expan (n,z,w)) * z)) . k)
by LOPBAN_3:def 6
.=
(((Expan (n,z,w)) . k) * w) + (((Expan (n,z,w)) * z) . (k -' 1))
by A34, LOPBAN_4:15
.=
(((Expan (n,z,w)) . k) * w) + (((Expan (n,z,w)) . (k -' 1)) * z)
by LOPBAN_3:def 6
.=
((0. X) * w) + (((Expan (n,z,w)) . (k -' 1)) * z)
by A36, Def2
.=
(0. X) + (((Expan (n,z,w)) . (k -' 1)) * z)
by CLOPBAN3:38
.=
(0. X) + ((0. X) * z)
by A35, A37, Def2
.=
(0. X) + (0. X)
by CLOPBAN3:38
.=
0. X
by RLVECT_1:def 4
;
hence
(((Expan (n,z,w)) * w) + (Shift ((Expan (n,z,w)) * z))) . k = (Expan ((n + 1),z,w)) . k
by A34, Def2;
verum end; hence
(((Expan (n,z,w)) * w) + (Shift ((Expan (n,z,w)) * z))) . k = (Expan ((n + 1),z,w)) . k
by A6;
verum end;
then A38:
((Expan (n,z,w)) * w) + (Shift ((Expan (n,z,w)) * z)) = Expan (
(n + 1),
z,
w)
by FUNCT_2:63;
A39:
n < n + 1
by XREAL_1:29;
(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 LOPBAN_3:def 6
;
then A40:
(Partial_Sums ((Expan (n,z,w)) * w)) . (n + 1) =
((Partial_Sums ((Expan (n,z,w)) * w)) . n) + ((0. X) * w)
by A39, Def2
.=
((Partial_Sums ((Expan (n,z,w)) * w)) . n) + (0. X)
by CLOPBAN3:38
.=
(Partial_Sums ((Expan (n,z,w)) * w)) . n
by RLVECT_1:def 4
;
(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 LOPBAN_3:def 6
;
then A41:
(Partial_Sums ((Expan (n,z,w)) * z)) . (n + 1) =
((Partial_Sums ((Expan (n,z,w)) * z)) . n) + ((0. X) * z)
by A4, Def2
.=
((Partial_Sums ((Expan (n,z,w)) * z)) . n) + (0. X)
by CLOPBAN3:38
.=
(Partial_Sums ((Expan (n,z,w)) * z)) . n
by RLVECT_1:def 4
;
0 + n < n + 1
by XREAL_1:29;
then A42:
(Expan (n,z,w)) . (n + 1) = 0. X
by Def2;
(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 A43:
(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 LOPBAN_3:def 6
.=
((Partial_Sums (Shift ((Expan (n,z,w)) * z))) . (n + 1)) + (0. X)
by A42, CLOPBAN3:38
.=
(Partial_Sums (Shift ((Expan (n,z,w)) * z))) . (n + 1)
by RLVECT_1:def 4
;
now for k being Element of NAT holds ((Expan (n,z,w)) * (z + w)) . k = (((Expan (n,z,w)) * z) + ((Expan (n,z,w)) * w)) . klet 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 LOPBAN_3:def 6
.=
(((Expan (n,z,w)) . k) * z) + (((Expan (n,z,w)) . k) * w)
by VECTSP_1:def 2
.=
(((Expan (n,z,w)) * z) . k) + (((Expan (n,z,w)) . k) * w)
by LOPBAN_3:def 6
.=
(((Expan (n,z,w)) * z) . k) + (((Expan (n,z,w)) * w) . k)
by LOPBAN_3:def 6
.=
(((Expan (n,z,w)) * z) + ((Expan (n,z,w)) * w)) . k
by NORMSP_1:def 2
;
verum end;
then A44:
(Expan (n,z,w)) * (z + w) = ((Expan (n,z,w)) * z) + ((Expan (n,z,w)) * w)
by FUNCT_2:63;
(z + w) #N (n + 1) =
((z + w) GeoSeq) . (n + 1)
by CLOPBAN3:def 8
.=
(((z + w) GeoSeq) . n) * (z + w)
by CLOPBAN3:def 7
.=
((Partial_Sums (Expan (n,z,w))) . n) * (z + w)
by A3, CLOPBAN3:def 8
.=
((Partial_Sums (Expan (n,z,w))) * (z + w)) . n
by LOPBAN_3:def 6
.=
(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 A44, CLOPBAN3:15
.=
((Partial_Sums ((Expan (n,z,w)) * z)) . n) + ((Partial_Sums ((Expan (n,z,w)) * w)) . n)
by NORMSP_1:def 2
;
hence (z + w) #N (n + 1) =
((Partial_Sums ((Expan (n,z,w)) * w)) + (Partial_Sums (Shift ((Expan (n,z,w)) * z)))) . (n + 1)
by A41, A40, A43, NORMSP_1:def 2
.=
(Partial_Sums (Expan ((n + 1),z,w))) . (n + 1)
by A38, CLOPBAN3:15
;
verum
end;
A45: (z + w) #N 0 =
((z + w) GeoSeq) . 0
by CLOPBAN3:def 8
.=
1. X
by CLOPBAN3:def 7
;
A46: 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 A46, Def2
.=
((1r / (1r * 1r)) * (z #N 0)) * (w #N 0)
by A46, COMPLEX1:def 4, SIN_COS:1, SIN_COS:def 6
.=
(z #N 0) * (w #N 0)
by CLVECT_1:def 5, COMPLEX1:def 4
.=
((z GeoSeq) . 0) * (w #N 0)
by CLOPBAN3:def 8
.=
((z GeoSeq) . 0) * ((w GeoSeq) . 0)
by CLOPBAN3:def 8
.=
(1. X) * ((w GeoSeq) . 0)
by CLOPBAN3:def 7
.=
(1. X) * (1. X)
by CLOPBAN3:def 7
.=
1. X
by VECTSP_1:def 4
;
then A47:
S1[ 0 ]
by A45;
for n being Nat holds S1[n]
from NAT_1:sch 2(A47, A2);
hence
(z + w) #N n = (Partial_Sums (Expan (n,z,w))) . n
; verum