let X be Complex_Banach_Algebra; :: thesis: 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; :: thesis: 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; :: thesis: ( z,w are_commutative implies (z + w) #N n = (Partial_Sums (Expan (n,z,w))) . n )
assume A1: z,w are_commutative ; :: thesis: (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; :: thesis: ( S1[n] implies S1[n + 1] )
assume A3: (z + w) #N n = (Partial_Sums (Expan (n,z,w))) . n ; :: thesis: S1[n + 1]
A4: n < n + 1 by XREAL_1:29;
now :: thesis: for k being Element of NAT holds (((Expan (n,z,w)) * w) + (Shift ((Expan (n,z,w)) * z))) . k = (Expan ((n + 1),z,w)) . k
let k be Element of NAT ; :: thesis: (((Expan (n,z,w)) * w) + (Shift ((Expan (n,z,w)) * z))) . k = (Expan ((n + 1),z,w)) . k
A5: n in NAT by ORDINAL1:def 12;
A6: now :: thesis: ( k <= n + 1 implies (((Expan (n,z,w)) * w) + (Shift ((Expan (n,z,w)) * z))) . k = (Expan ((n + 1),z,w)) . k )
A7: now :: thesis: ( 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 ; :: thesis: (((Expan (n,z,w)) * w) + (Shift ((Expan (n,z,w)) * z))) . k = (Expan ((n + 1),z,w)) . k
A9: now :: thesis: ( 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 ; :: thesis: (((Expan (n,z,w)) * w) + (Shift ((Expan (n,z,w)) * z))) . k = (Expan ((n + 1),z,w)) . k
then 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 ; :: thesis: verum
end;
now :: thesis: ( 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 ; :: thesis: (((Expan (n,z,w)) * w) + (Shift ((Expan (n,z,w)) * z))) . k = (Expan ((n + 1),z,w)) . k
then (((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 ; :: thesis: verum
end;
hence (((Expan (n,z,w)) * w) + (Shift ((Expan (n,z,w)) * z))) . k = (Expan ((n + 1),z,w)) . k by A9; :: thesis: verum
end;
A27: now :: thesis: ( 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 ; :: thesis: (((Expan (n,z,w)) * w) + (Shift ((Expan (n,z,w)) * z))) . k = (Expan ((n + 1),z,w)) . k
then (((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 ; :: thesis: verum
end;
assume k <= n + 1 ; :: thesis: (((Expan (n,z,w)) * w) + (Shift ((Expan (n,z,w)) * z))) . k = (Expan ((n + 1),z,w)) . k
hence (((Expan (n,z,w)) * w) + (Shift ((Expan (n,z,w)) * z))) . k = (Expan ((n + 1),z,w)) . k by A27, A7, XXREAL_0:1; :: thesis: verum
end;
now :: thesis: ( 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 ; :: thesis: (((Expan (n,z,w)) * w) + (Shift ((Expan (n,z,w)) * z))) . k = (Expan ((n + 1),z,w)) . k
then 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; :: thesis: verum
end;
hence (((Expan (n,z,w)) * w) + (Shift ((Expan (n,z,w)) * z))) . k = (Expan ((n + 1),z,w)) . k by A6; :: thesis: 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 :: thesis: for k being Element of NAT holds ((Expan (n,z,w)) * (z + w)) . k = (((Expan (n,z,w)) * z) + ((Expan (n,z,w)) * w)) . k
let k be Element of NAT ; :: thesis: ((Expan (n,z,w)) * (z + w)) . k = (((Expan (n,z,w)) * z) + ((Expan (n,z,w)) * w)) . k
thus ((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 ; :: thesis: 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 ;
:: thesis: 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 ; :: thesis: verum