let X be 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 !) * ((n -' k) !)) * ((n + 1) - k) = (k !) * (((n -' k) !) * ((n + 1) - k))
;
A10:
(k + 1) - 1
<= (n + 1) - 1
by A7, INT_1:20;
then A11:
(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 A12:
(n !) / ((k !) * ((n -' k) !)) =
((n !) * ((n + 1) - k)) / (((k !) * ((n -' k) !)) * ((n + 1) - k))
by XCMPLX_1:92
.=
((n !) * ((n + 1) - k)) / ((k !) * (((n + 1) -' k) !))
by A10, A9, Th13
;
assume A13:
k <> 0
;
(((Expan (n,z,w)) * w) + (Shift ((Expan (n,z,w)) * z))) . k = (Expan ((n + 1),z,w)) . kthen 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 A10, 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
;
A18:
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
;
(((k -' 1) !) * ((n -' (k -' 1)) !)) * k =
(k * ((k -' 1) !)) * ((n -' (k -' 1)) !)
.=
(k !) * (((n + 1) -' k) !)
by A13, A18, Th13
;
then A19:
(n !) / (((k -' 1) !) * ((n -' (k -' 1)) !)) = ((n !) * k) / ((k !) * (((n + 1) -' k) !))
by A13, XCMPLX_1:92;
(((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 LOPBAN_3:def 10
.=
(((Expan (n,z,w)) . k) * w) + (((Expan (n,z,w)) * z) . (k -' 1))
by A13, Th15
.=
(((Expan (n,z,w)) . k) * w) + (((Expan (n,z,w)) . (k -' 1)) * z)
by LOPBAN_3:def 10
.=
(((((Coef n) . k) * (z #N k)) * (w #N (n -' k))) * w) + (((Expan (n,z,w)) . (k -' 1)) * z)
by A10, Def6
.=
(((((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, Def6
.=
((((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 LOPBAN_3:43
.=
((((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 LOPBAN_3:43
.=
((((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 LOPBAN_3:43
.=
((((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 LOPBAN_3:43
.=
((((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 A20:
(((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, A17, A15, LOPBAN_3:43
.=
(((Coef n) . k) * ((z #N k) * (w #N ((n + 1) -' k)))) + (((Coef n) . (k -' 1)) * ((z #N k) * (w #N ((n + 1) -' k))))
by LOPBAN_3:43
.=
(((Coef n) . k) + ((Coef n) . (k -' 1))) * ((z #N k) * (w #N ((n + 1) -' k)))
by LOPBAN_3:43
;
((Coef n) . k) + ((Coef n) . (k -' 1)) =
((n !) / ((k !) * ((n -' k) !))) + ((Coef n) . (k -' 1))
by A10, Def3
.=
((n !) / ((k !) * ((n -' k) !))) + ((n !) / (((k -' 1) !) * ((n -' (k -' 1)) !)))
by A16, Def3
;
then ((Coef n) . k) + ((Coef n) . (k -' 1)) =
(((n !) * ((n + 1) - k)) + ((n !) * k)) / ((k !) * (((n + 1) -' k) !))
by A12, A19, XCMPLX_1:63
.=
((n !) * (((n + 1) - k) + k)) / ((k !) * (((n + 1) -' k) !))
.=
((n + 1) !) / ((k !) * (((n + 1) -' k) !))
by NEWTON:21
.=
(Coef (n + 1)) . k
by A7, Def3
;
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, LOPBAN_3:43
.=
(Expan ((n + 1),z,w)) . k
by A7, Def6
;
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
by NEWTON:23;
A22:
(n + 1) -' 0 = (n + 1) - 0
by XREAL_1:235;
then A23:
(Coef (n + 1)) . 0 =
((n + 1) !) / ((0 !) * ((n + 1) !))
by Def3
.=
1
by A21, NEWTON:18, XCMPLX_1:60
;
A24:
n ! <> 0
by NEWTON:23;
A25:
n -' 0 = n - 0
by XREAL_1:235;
then A26:
(Coef n) . 0 =
(n !) / ((0 !) * (n !))
by Def3
.=
1
by A24, NEWTON:18, XCMPLX_1:60
;
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 LOPBAN_3:def 10
.=
(((Expan (n,z,w)) . 0) * w) + (0. X)
by Def5
.=
((Expan (n,z,w)) . 0) * w
by LOPBAN_3:43
.=
((((Coef n) . 0) * (z #N 0)) * (w #N (n -' 0))) * w
by Def6
.=
(((Coef n) . 0) * (z #N 0)) * ((w #N (n -' 0)) * w)
by LOPBAN_3:43
.=
(((Coef (n + 1)) . 0) * (z #N 0)) * (w #N ((n + 1) -' 0))
by A25, A22, A26, A23, Lm1
.=
(Expan ((n + 1),z,w)) . k
by A27, Def6
;
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) ! <> 0
by NEWTON:23;
A30:
(n + 1) -' (n + 1) =
(n + 1) - (n + 1)
by XREAL_1:235
.=
0
;
then A31:
(Coef (n + 1)) . (n + 1) =
((n + 1) !) / (((n + 1) !) * (0 !))
by Def3
.=
1
by A29, NEWTON:18, XCMPLX_1:60
;
A32:
n ! <> 0
by NEWTON:23;
A33:
n -' n =
n - n
by XREAL_1:235
.=
0
;
then A34:
(Coef n) . n =
(n !) / ((n !) * (0 !))
by Def3
.=
1
by A32, NEWTON:18, XCMPLX_1:60
;
A35:
n < n + 1
by XREAL_1:31;
assume A36:
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 LOPBAN_3:def 10
.=
((0. X) * w) + ((Shift ((Expan (n,z,w)) * z)) . (n + 1))
by A35, Def6
.=
(0. X) + ((Shift ((Expan (n,z,w)) * z)) . (n + 1))
by LOPBAN_3:43
.=
(Shift ((Expan (n,z,w)) * z)) . (n + 1)
by LOPBAN_3:43
.=
((Expan (n,z,w)) * z) . n
by Def5
.=
((Expan (n,z,w)) . n) * z
by LOPBAN_3:def 10
.=
((((Coef n) . n) * (z #N n)) * (w #N (n -' n))) * z
by Def6
.=
(((Coef n) . n) * (z #N n)) * ((w #N (n -' n)) * z)
by LOPBAN_3:43
.=
(((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 LOPBAN_3:43
.=
(((Coef n) . n) * ((z #N n) * z)) * (w #N (n -' n))
by LOPBAN_3:43
.=
(((Coef (n + 1)) . (n + 1)) * (z #N (n + 1))) * (w #N (n -' n))
by A34, A31, Lm1
.=
(Expan ((n + 1),z,w)) . k
by A36, A33, A30, Def6
;
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 A37:
n + 1
< k
;
(((Expan (n,z,w)) * w) + (Shift ((Expan (n,z,w)) * z))) . k = (Expan ((n + 1),z,w)) . kthen A38:
(n + 1) - 1
< k - 1
by XREAL_1:11;
then A39:
n + 0 < (k - 1) + 1
by XREAL_1:10;
0 + 1
<= n + 1
by XREAL_1:8;
then A40:
k - 1
= k -' 1
by A37, 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 LOPBAN_3:def 10
.=
(((Expan (n,z,w)) . k) * w) + (((Expan (n,z,w)) * z) . (k -' 1))
by A39, Th15
.=
(((Expan (n,z,w)) . k) * w) + (((Expan (n,z,w)) . (k -' 1)) * z)
by LOPBAN_3:def 10
.=
((0. X) * w) + (((Expan (n,z,w)) . (k -' 1)) * z)
by A39, Def6
.=
(0. X) + (((Expan (n,z,w)) . (k -' 1)) * z)
by LOPBAN_3:43
.=
(0. X) + ((0. X) * z)
by A38, A40, Def6
.=
(0. X) + (0. X)
by LOPBAN_3:43
.=
0. X
by LOPBAN_3:43
;
hence
(((Expan (n,z,w)) * w) + (Shift ((Expan (n,z,w)) * z))) . k = (Expan ((n + 1),z,w)) . k
by A37, Def6;
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 A41:
((Expan (n,z,w)) * w) + (Shift ((Expan (n,z,w)) * z)) = Expan (
(n + 1),
z,
w)
by FUNCT_2:113;
A42:
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 LOPBAN_3:def 10
;
then A43:
(Partial_Sums ((Expan (n,z,w)) * w)) . (n + 1) =
((Partial_Sums ((Expan (n,z,w)) * w)) . n) + ((0. X) * w)
by A42, Def6
.=
((Partial_Sums ((Expan (n,z,w)) * w)) . n) + (0. X)
by LOPBAN_3:43
.=
(Partial_Sums ((Expan (n,z,w)) * w)) . n
by LOPBAN_3:43
;
(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 10
;
then A44:
(Partial_Sums ((Expan (n,z,w)) * z)) . (n + 1) =
((Partial_Sums ((Expan (n,z,w)) * z)) . n) + ((0. X) * z)
by A4, Def6
.=
((Partial_Sums ((Expan (n,z,w)) * z)) . n) + (0. X)
by LOPBAN_3:43
.=
(Partial_Sums ((Expan (n,z,w)) * z)) . n
by LOPBAN_3:43
;
0 + n < n + 1
by XREAL_1:31;
then A45:
(Expan (n,z,w)) . (n + 1) = 0. X
by Def6;
(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 Th16;
then A46:
(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 10
.=
((Partial_Sums (Shift ((Expan (n,z,w)) * z))) . (n + 1)) + (0. X)
by A45, LOPBAN_3:43
.=
(Partial_Sums (Shift ((Expan (n,z,w)) * z))) . (n + 1)
by LOPBAN_3:43
;
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 LOPBAN_3:def 10
.=
(((Expan (n,z,w)) . k) * z) + (((Expan (n,z,w)) . k) * w)
by LOPBAN_3:43
.=
(((Expan (n,z,w)) * z) . k) + (((Expan (n,z,w)) . k) * w)
by LOPBAN_3:def 10
.=
(((Expan (n,z,w)) * z) . k) + (((Expan (n,z,w)) * w) . k)
by LOPBAN_3:def 10
.=
(((Expan (n,z,w)) * z) + ((Expan (n,z,w)) * w)) . k
by NORMSP_1:def 5
;
verum end;
then A47:
(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) * (z + w)
by LOPBAN_3:def 13
.=
((Partial_Sums (Expan (n,z,w))) * (z + w)) . n
by A3, LOPBAN_3:def 10
.=
(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 A47, LOPBAN_3:20
.=
((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 A44, A43, A46, NORMSP_1:def 5
.=
(Partial_Sums (Expan ((n + 1),z,w))) . (n + 1)
by A41, LOPBAN_3:20
;
verum
end;
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, Def6
.=
((1 / (1 * 1)) * (z #N 0)) * (w #N 0)
by A48, Def3, NEWTON:18
.=
((z GeoSeq) . 0) * (w #N 0)
by RLVECT_1:def 11
.=
(1. X) * ((w GeoSeq) . 0)
by LOPBAN_3:def 13
.=
(1. X) * (1. X)
by LOPBAN_3:def 13
.=
1. X
by LOPBAN_3:43
;
then A49:
S1[ 0 ]
by LOPBAN_3:def 13;
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