:: CLOPBAN4 semantic presentation begin Lm1: for X being Complex_Banach_Algebra for z being Element of X for n being Element of NAT holds ( z * (z #N n) = z #N (n + 1) & (z #N n) * z = z #N (n + 1) & z * (z #N n) = (z #N n) * z ) proof let X be Complex_Banach_Algebra; ::_thesis: for z being Element of X for n being Element of NAT holds ( z * (z #N n) = z #N (n + 1) & (z #N n) * z = z #N (n + 1) & z * (z #N n) = (z #N n) * z ) let z be Element of X; ::_thesis: for n being Element of NAT holds ( z * (z #N n) = z #N (n + 1) & (z #N n) * z = z #N (n + 1) & z * (z #N n) = (z #N n) * z ) let n be Element of NAT ; ::_thesis: ( z * (z #N n) = z #N (n + 1) & (z #N n) * z = z #N (n + 1) & z * (z #N n) = (z #N n) * z ) defpred S1[ Element of NAT ] means z * (z #N $1) = z #N ($1 + 1); A1: z #N (0 + 1) = (z GeoSeq) . (0 + 1) by CLOPBAN3:def_8 .= ((z GeoSeq) . 0) * z by CLOPBAN3:def_7 .= (1. X) * z by CLOPBAN3:def_7 .= z by CLOPBAN3:38 ; A2: for k being Element of NAT st S1[k] holds S1[k + 1] proof let k be Element of NAT ; ::_thesis: ( S1[k] implies S1[k + 1] ) assume A3: S1[k] ; ::_thesis: S1[k + 1] thus z * (z #N (k + 1)) = z * ((z GeoSeq) . (k + 1)) by CLOPBAN3:def_8 .= z * (((z GeoSeq) . k) * z) by CLOPBAN3:def_7 .= z * ((z #N k) * z) by CLOPBAN3:def_8 .= (z * (z #N k)) * z by CLOPBAN3:38 .= ((z GeoSeq) . (k + 1)) * z by A3, CLOPBAN3:def_8 .= (z GeoSeq) . ((k + 1) + 1) by CLOPBAN3:def_7 .= z #N ((k + 1) + 1) by CLOPBAN3:def_8 ; ::_thesis: verum end; z * (z #N 0) = z * ((z GeoSeq) . 0) by CLOPBAN3:def_8 .= z * (1. X) by CLOPBAN3:def_7 .= z by CLOPBAN3:38 ; then A4: S1[ 0 ] by A1; A5: for n being Element of NAT holds S1[n] from NAT_1:sch_1(A4, A2); now__::_thesis:_for_n_being_Element_of_NAT_holds_ (_z_*_(z_#N_n)_=_z_#N_(n_+_1)_&_(z_#N_n)_*_z_=_z_#N_(n_+_1)_&_z_*_(z_#N_n)_=_(z_#N_n)_*_z_) let n be Element of NAT ; ::_thesis: ( z * (z #N n) = z #N (n + 1) & (z #N n) * z = z #N (n + 1) & z * (z #N n) = (z #N n) * z ) thus z * (z #N n) = z #N (n + 1) by A5; ::_thesis: ( (z #N n) * z = z #N (n + 1) & z * (z #N n) = (z #N n) * z ) thus (z #N n) * z = ((z GeoSeq) . n) * z by CLOPBAN3:def_8 .= (z GeoSeq) . (n + 1) by CLOPBAN3:def_7 .= z #N (n + 1) by CLOPBAN3:def_8 ; ::_thesis: z * (z #N n) = (z #N n) * z hence z * (z #N n) = (z #N n) * z by A5; ::_thesis: verum end; hence ( z * (z #N n) = z #N (n + 1) & (z #N n) * z = z #N (n + 1) & z * (z #N n) = (z #N n) * z ) ; ::_thesis: verum end; Lm2: for X being Complex_Banach_Algebra for n being Element of NAT for z, w being Element of X st z,w are_commutative holds ( w * (z #N n) = (z #N n) * w & z * (w #N n) = (w #N n) * z ) proof let X be Complex_Banach_Algebra; ::_thesis: for n being Element of NAT for z, w being Element of X st z,w are_commutative holds ( w * (z #N n) = (z #N n) * w & z * (w #N n) = (w #N n) * z ) let n be Element of NAT ; ::_thesis: for z, w being Element of X st z,w are_commutative holds ( w * (z #N n) = (z #N n) * w & z * (w #N n) = (w #N n) * z ) let z, w be Element of X; ::_thesis: ( z,w are_commutative implies ( w * (z #N n) = (z #N n) * w & z * (w #N n) = (w #N n) * z ) ) assume A1: z,w are_commutative ; ::_thesis: ( w * (z #N n) = (z #N n) * w & z * (w #N n) = (w #N n) * z ) defpred S1[ Element of NAT ] means ( w * (z #N $1) = (z #N $1) * w & z * (w #N $1) = (w #N $1) * z ); A2: for k being Element of NAT st S1[k] holds S1[k + 1] proof let k be Element of NAT ; ::_thesis: ( S1[k] implies S1[k + 1] ) assume A3: S1[k] ; ::_thesis: S1[k + 1] A4: z * (w #N (k + 1)) = z * ((w #N k) * w) by Lm1 .= (z * (w #N k)) * w by CLOPBAN3:38 .= (w #N k) * (z * w) by A3, CLOPBAN3:38 .= (w #N k) * (w * z) by A1, LOPBAN_4:def_1 .= ((w #N k) * w) * z by CLOPBAN3:38 .= (w #N (k + 1)) * z by Lm1 ; w * (z #N (k + 1)) = w * ((z #N k) * z) by Lm1 .= (w * (z #N k)) * z by CLOPBAN3:38 .= (z #N k) * (w * z) by A3, CLOPBAN3:38 .= (z #N k) * (z * w) by A1, LOPBAN_4:def_1 .= ((z #N k) * z) * w by CLOPBAN3:38 .= (z #N (k + 1)) * w by Lm1 ; hence S1[k + 1] by A4; ::_thesis: verum end; A5: w #N 0 = (w GeoSeq) . 0 by CLOPBAN3:def_8 .= 1. X by CLOPBAN3:def_7 ; then A6: z * (w #N 0) = z by CLOPBAN3:38 .= (w #N 0) * z by A5, CLOPBAN3:38 ; A7: z #N 0 = (z GeoSeq) . 0 by CLOPBAN3:def_8 .= 1. X by CLOPBAN3:def_7 ; then w * (z #N 0) = w by CLOPBAN3:38 .= (z #N 0) * w by A7, CLOPBAN3:38 ; then A8: S1[ 0 ] by A6; for n being Element of NAT holds S1[n] from NAT_1:sch_1(A8, A2); hence ( w * (z #N n) = (z #N n) * w & z * (w #N n) = (w #N n) * z ) ; ::_thesis: verum end; theorem Th1: :: CLOPBAN4:1 for X being Complex_Banach_Algebra for seq1, seq2 being sequence of X st seq1 is convergent & seq2 is convergent & lim (seq1 - seq2) = 0. X holds lim seq1 = lim seq2 proof let X be Complex_Banach_Algebra; ::_thesis: for seq1, seq2 being sequence of X st seq1 is convergent & seq2 is convergent & lim (seq1 - seq2) = 0. X holds lim seq1 = lim seq2 let seq1, seq2 be sequence of X; ::_thesis: ( seq1 is convergent & seq2 is convergent & lim (seq1 - seq2) = 0. X implies lim seq1 = lim seq2 ) assume that A1: seq1 is convergent and A2: seq2 is convergent and A3: lim (seq1 - seq2) = 0. X ; ::_thesis: lim seq1 = lim seq2 (lim seq1) - (lim seq2) = 0. X by A1, A2, A3, CLVECT_1:120; then ((lim seq1) - (lim seq2)) + (lim seq2) = lim seq2 by CLOPBAN3:38; then (lim seq1) - ((lim seq2) - (lim seq2)) = lim seq2 by CLOPBAN3:38; then (lim seq1) - (0. X) = lim seq2 by RLVECT_1:15; hence lim seq1 = lim seq2 by RLVECT_1:13; ::_thesis: verum end; theorem Th2: :: CLOPBAN4:2 for X being Complex_Banach_Algebra for s being sequence of X for z being Element of X st ( for n being Element of NAT holds s . n = z ) holds lim s = z proof let X be Complex_Banach_Algebra; ::_thesis: for s being sequence of X for z being Element of X st ( for n being Element of NAT holds s . n = z ) holds lim s = z let s be sequence of X; ::_thesis: for z being Element of X st ( for n being Element of NAT holds s . n = z ) holds lim s = z let z be Element of X; ::_thesis: ( ( for n being Element of NAT holds s . n = z ) implies lim s = z ) assume A1: for n being Element of NAT holds s . n = z ; ::_thesis: lim s = z A2: now__::_thesis:_for_p_being_Real_st_0_<_p_holds_ ex_k_being_Element_of_NAT_st_ for_n_being_Element_of_NAT_st_k_<=_n_holds_ ||.((s_._n)_-_z).||_<_p let p be Real; ::_thesis: ( 0 < p implies ex k being Element of NAT st for n being Element of NAT st k <= n holds ||.((s . n) - z).|| < p ) assume A3: 0 < p ; ::_thesis: ex k being Element of NAT st for n being Element of NAT st k <= n holds ||.((s . n) - z).|| < p take k = 0 ; ::_thesis: for n being Element of NAT st k <= n holds ||.((s . n) - z).|| < p let n be Element of NAT ; ::_thesis: ( k <= n implies ||.((s . n) - z).|| < p ) assume k <= n ; ::_thesis: ||.((s . n) - z).|| < p s . n = z by A1; hence ||.((s . n) - z).|| < p by A3, CLVECT_1:107; ::_thesis: verum end; then s is convergent by CLVECT_1:def_15; hence lim s = z by A2, CLVECT_1:def_16; ::_thesis: verum end; theorem Th3: :: CLOPBAN4:3 for X being Complex_Banach_Algebra for s, s9 being sequence of X st s is convergent & s9 is convergent holds s * s9 is convergent proof let X be Complex_Banach_Algebra; ::_thesis: for s, s9 being sequence of X st s is convergent & s9 is convergent holds s * s9 is convergent let s, s9 be sequence of X; ::_thesis: ( s is convergent & s9 is convergent implies s * s9 is convergent ) assume that A1: s is convergent and A2: s9 is convergent ; ::_thesis: s * s9 is convergent consider g1 being Point of X such that A3: for p being Real st 0 < p holds ex n being Element of NAT st for m being Element of NAT st n <= m holds ||.((s . m) - g1).|| < p by A1, CLVECT_1:def_15; ||.s.|| is bounded by A1, CLVECT_1:117, SEQ_2:13; then consider R being real number such that A4: for n being Element of NAT holds ||.s.|| . n < R by SEQ_2:def_3; A5: now__::_thesis:_for_n_being_Element_of_NAT_holds_||.(s_._n).||_<_R let n be Element of NAT ; ::_thesis: ||.(s . n).|| < R ||.(s . n).|| = ||.s.|| . n by NORMSP_0:def_4; hence ||.(s . n).|| < R by A4; ::_thesis: verum end; ||.(s . 1).|| = ||.s.|| . 1 by NORMSP_0:def_4; then 0 <= ||.s.|| . 1 by CLVECT_1:105; then A6: 0 < R by A4; consider g2 being Point of X such that A7: for p being Real st 0 < p holds ex n being Element of NAT st for m being Element of NAT st n <= m holds ||.((s9 . m) - g2).|| < p by A2, CLVECT_1:def_15; take g = g1 * g2; :: according to CLVECT_1:def_15 ::_thesis: for b1 being Element of REAL holds ( b1 <= 0 or ex b2 being Element of NAT st for b3 being Element of NAT holds ( not b2 <= b3 or not b1 <= ||.(((s * s9) . b3) - g).|| ) ) let p be Real; ::_thesis: ( p <= 0 or ex b1 being Element of NAT st for b2 being Element of NAT holds ( not b1 <= b2 or not p <= ||.(((s * s9) . b2) - g).|| ) ) reconsider R = R as Real by XREAL_0:def_1; A8: 0 + 0 < ||.g2.|| + R by A6, CLVECT_1:105, XREAL_1:8; assume A9: 0 < p ; ::_thesis: ex b1 being Element of NAT st for b2 being Element of NAT holds ( not b1 <= b2 or not p <= ||.(((s * s9) . b2) - g).|| ) then consider n1 being Element of NAT such that A10: for m being Element of NAT st n1 <= m holds ||.((s . m) - g1).|| < p / (||.g2.|| + R) by A3, A8; consider n2 being Element of NAT such that A11: for m being Element of NAT st n2 <= m holds ||.((s9 . m) - g2).|| < p / (||.g2.|| + R) by A7, A8, A9; take n = n1 + n2; ::_thesis: for b1 being Element of NAT holds ( not n <= b1 or not p <= ||.(((s * s9) . b1) - g).|| ) let m be Element of NAT ; ::_thesis: ( not n <= m or not p <= ||.(((s * s9) . m) - g).|| ) assume A12: n <= m ; ::_thesis: not p <= ||.(((s * s9) . m) - g).|| n2 <= n by NAT_1:12; then n2 <= m by A12, XXREAL_0:2; then A13: ||.((s9 . m) - g2).|| < p / (||.g2.|| + R) by A11; A14: 0 <= ||.(s . m).|| by CLVECT_1:105; A15: ||.((s . m) * ((s9 . m) - g2)).|| <= ||.(s . m).|| * ||.((s9 . m) - g2).|| by CLOPBAN3:38; A16: 0 <= ||.((s9 . m) - g2).|| by CLVECT_1:105; n1 <= n1 + n2 by NAT_1:12; then n1 <= m by A12, XXREAL_0:2; then A17: ||.((s . m) - g1).|| <= p / (||.g2.|| + R) by A10; ||.(((s * s9) . m) - g).|| = ||.(((s . m) * (s9 . m)) - (g1 * g2)).|| by CLOPBAN3:def_6 .= ||.((((s . m) * (s9 . m)) - ((s . m) * g2)) + (((s . m) * g2) - (g1 * g2))).|| by CLOPBAN3:38 .= ||.(((s . m) * ((s9 . m) - g2)) + (((s . m) * g2) - (g1 * g2))).|| by CLOPBAN3:38 .= ||.(((s . m) * ((s9 . m) - g2)) + (((s . m) - g1) * g2)).|| by CLOPBAN3:38 ; then A18: ||.(((s * s9) . m) - g).|| <= ||.((s . m) * ((s9 . m) - g2)).|| + ||.(((s . m) - g1) * g2).|| by CLVECT_1:def_13; ||.(s . m).|| < R by A5; then ||.(s . m).|| * ||.((s9 . m) - g2).|| < R * (p / (||.g2.|| + R)) by A14, A16, A13, XREAL_1:96; then A19: ||.((s . m) * ((s9 . m) - g2)).|| < R * (p / (||.g2.|| + R)) by A15, XXREAL_0:2; A20: ||.(((s . m) - g1) * g2).|| <= ||.g2.|| * ||.((s . m) - g1).|| by CLOPBAN3:38; 0 <= ||.g2.|| by CLVECT_1:105; then ||.g2.|| * ||.((s . m) - g1).|| <= ||.g2.|| * (p / (||.g2.|| + R)) by A17, XREAL_1:64; then A21: ||.(((s . m) - g1) * g2).|| <= ||.g2.|| * (p / (||.g2.|| + R)) by A20, XXREAL_0:2; (R * (p / (||.g2.|| + R))) + (||.g2.|| * (p / (||.g2.|| + R))) = (p / (||.g2.|| + R)) * (||.g2.|| + R) .= p by A8, XCMPLX_1:87 ; then ||.((s . m) * ((s9 . m) - g2)).|| + ||.(((s . m) - g1) * g2).|| < p by A19, A21, XREAL_1:8; hence not p <= ||.(((s * s9) . m) - g).|| by A18, XXREAL_0:2; ::_thesis: verum end; theorem Th4: :: CLOPBAN4:4 for X being Complex_Banach_Algebra for z being Element of X for s being sequence of X st s is convergent holds z * s is convergent proof let X be Complex_Banach_Algebra; ::_thesis: for z being Element of X for s being sequence of X st s is convergent holds z * s is convergent let z be Element of X; ::_thesis: for s being sequence of X st s is convergent holds z * s is convergent let s be sequence of X; ::_thesis: ( s is convergent implies z * s is convergent ) A1: 0 <= ||.z.|| by CLVECT_1:105; assume s is convergent ; ::_thesis: z * s is convergent then consider g1 being Point of X such that A2: for p being Real st 0 < p holds ex n being Element of NAT st for m being Element of NAT st n <= m holds ||.((s . m) - g1).|| < p by CLVECT_1:def_15; take g = z * g1; :: according to CLVECT_1:def_15 ::_thesis: for b1 being Element of REAL holds ( b1 <= 0 or ex b2 being Element of NAT st for b3 being Element of NAT holds ( not b2 <= b3 or not b1 <= ||.(((z * s) . b3) - g).|| ) ) let p be Real; ::_thesis: ( p <= 0 or ex b1 being Element of NAT st for b2 being Element of NAT holds ( not b1 <= b2 or not p <= ||.(((z * s) . b2) - g).|| ) ) assume A3: 0 < p ; ::_thesis: ex b1 being Element of NAT st for b2 being Element of NAT holds ( not b1 <= b2 or not p <= ||.(((z * s) . b2) - g).|| ) A4: 0 + 0 < ||.z.|| + 1 by CLVECT_1:105, XREAL_1:8; then consider n being Element of NAT such that A5: for m being Element of NAT st n <= m holds ||.((s . m) - g1).|| < p / (||.z.|| + 1) by A2, A3; take n ; ::_thesis: for b1 being Element of NAT holds ( not n <= b1 or not p <= ||.(((z * s) . b1) - g).|| ) let m be Element of NAT ; ::_thesis: ( not n <= m or not p <= ||.(((z * s) . m) - g).|| ) assume n <= m ; ::_thesis: not p <= ||.(((z * s) . m) - g).|| then A6: ||.((s . m) - g1).|| < p / (||.z.|| + 1) by A5; A7: ||.(z * ((s . m) - g1)).|| <= ||.z.|| * ||.((s . m) - g1).|| by CLOPBAN3:38; 0 <= ||.((s . m) - g1).|| by CLVECT_1:105; then ||.z.|| * ||.((s . m) - g1).|| <= ||.z.|| * (p / (||.z.|| + 1)) by A1, A6, XREAL_1:66; then A8: ||.(z * ((s . m) - g1)).|| <= ||.z.|| * (p / (||.z.|| + 1)) by A7, XXREAL_0:2; A9: ||.(((z * s) . m) - g).|| = ||.((z * (s . m)) - (z * g1)).|| by CLOPBAN3:def_4 .= ||.(z * ((s . m) - g1)).|| by CLOPBAN3:38 ; 0 + ||.z.|| < ||.z.|| + 1 by XREAL_1:8; then A10: ||.z.|| * (p / (||.z.|| + 1)) < (||.z.|| + 1) * (p / (||.z.|| + 1)) by A1, A3, XREAL_1:97; (||.z.|| + 1) * (p / (||.z.|| + 1)) = p by A4, XCMPLX_1:87; hence not p <= ||.(((z * s) . m) - g).|| by A9, A8, A10, XXREAL_0:2; ::_thesis: verum end; theorem Th5: :: CLOPBAN4:5 for X being Complex_Banach_Algebra for z being Element of X for s being sequence of X st s is convergent holds s * z is convergent proof let X be Complex_Banach_Algebra; ::_thesis: for z being Element of X for s being sequence of X st s is convergent holds s * z is convergent let z be Element of X; ::_thesis: for s being sequence of X st s is convergent holds s * z is convergent let s be sequence of X; ::_thesis: ( s is convergent implies s * z is convergent ) A1: 0 <= ||.z.|| by CLVECT_1:105; assume s is convergent ; ::_thesis: s * z is convergent then consider g1 being Point of X such that A2: for p being Real st 0 < p holds ex n being Element of NAT st for m being Element of NAT st n <= m holds ||.((s . m) - g1).|| < p by CLVECT_1:def_15; take g = g1 * z; :: according to CLVECT_1:def_15 ::_thesis: for b1 being Element of REAL holds ( b1 <= 0 or ex b2 being Element of NAT st for b3 being Element of NAT holds ( not b2 <= b3 or not b1 <= ||.(((s * z) . b3) - g).|| ) ) let p be Real; ::_thesis: ( p <= 0 or ex b1 being Element of NAT st for b2 being Element of NAT holds ( not b1 <= b2 or not p <= ||.(((s * z) . b2) - g).|| ) ) assume A3: 0 < p ; ::_thesis: ex b1 being Element of NAT st for b2 being Element of NAT holds ( not b1 <= b2 or not p <= ||.(((s * z) . b2) - g).|| ) A4: 0 + 0 < ||.z.|| + 1 by CLVECT_1:105, XREAL_1:8; then consider n being Element of NAT such that A5: for m being Element of NAT st n <= m holds ||.((s . m) - g1).|| < p / (||.z.|| + 1) by A2, A3; take n ; ::_thesis: for b1 being Element of NAT holds ( not n <= b1 or not p <= ||.(((s * z) . b1) - g).|| ) let m be Element of NAT ; ::_thesis: ( not n <= m or not p <= ||.(((s * z) . m) - g).|| ) assume n <= m ; ::_thesis: not p <= ||.(((s * z) . m) - g).|| then A6: ||.((s . m) - g1).|| < p / (||.z.|| + 1) by A5; A7: ||.(((s . m) - g1) * z).|| <= ||.((s . m) - g1).|| * ||.z.|| by CLOPBAN3:38; 0 <= ||.((s . m) - g1).|| by CLVECT_1:105; then ||.((s . m) - g1).|| * ||.z.|| <= (p / (||.z.|| + 1)) * ||.z.|| by A1, A6, XREAL_1:66; then A8: ||.(((s . m) - g1) * z).|| <= (p / (||.z.|| + 1)) * ||.z.|| by A7, XXREAL_0:2; A9: ||.(((s * z) . m) - g).|| = ||.(((s . m) * z) - (g1 * z)).|| by CLOPBAN3:def_5 .= ||.(((s . m) - g1) * z).|| by CLOPBAN3:38 ; 0 + ||.z.|| < ||.z.|| + 1 by XREAL_1:8; then A10: (p / (||.z.|| + 1)) * ||.z.|| < (p / (||.z.|| + 1)) * (||.z.|| + 1) by A1, A3, XREAL_1:97; (p / (||.z.|| + 1)) * (||.z.|| + 1) = p by A4, XCMPLX_1:87; hence not p <= ||.(((s * z) . m) - g).|| by A9, A8, A10, XXREAL_0:2; ::_thesis: verum end; theorem Th6: :: CLOPBAN4:6 for X being Complex_Banach_Algebra for z being Element of X for s being sequence of X st s is convergent holds lim (z * s) = z * (lim s) proof let X be Complex_Banach_Algebra; ::_thesis: for z being Element of X for s being sequence of X st s is convergent holds lim (z * s) = z * (lim s) let z be Element of X; ::_thesis: for s being sequence of X st s is convergent holds lim (z * s) = z * (lim s) let s be sequence of X; ::_thesis: ( s is convergent implies lim (z * s) = z * (lim s) ) assume A1: s is convergent ; ::_thesis: lim (z * s) = z * (lim s) set g1 = lim s; set g = z * (lim s); A2: 0 + 0 < ||.z.|| + 1 by CLVECT_1:105, XREAL_1:8; A3: 0 <= ||.z.|| by CLVECT_1:105; A4: now__::_thesis:_for_p_being_Real_st_0_<_p_holds_ ex_n_being_Element_of_NAT_st_ for_m_being_Element_of_NAT_st_n_<=_m_holds_ ||.(((z_*_s)_._m)_-_(z_*_(lim_s))).||_<_p let p be Real; ::_thesis: ( 0 < p implies ex n being Element of NAT st for m being Element of NAT st n <= m holds ||.(((z * s) . m) - (z * (lim s))).|| < p ) assume A5: 0 < p ; ::_thesis: ex n being Element of NAT st for m being Element of NAT st n <= m holds ||.(((z * s) . m) - (z * (lim s))).|| < p then consider n being Element of NAT such that A6: for m being Element of NAT st n <= m holds ||.((s . m) - (lim s)).|| < p / (||.z.|| + 1) by A1, A2, CLVECT_1:def_16; take n = n; ::_thesis: for m being Element of NAT st n <= m holds ||.(((z * s) . m) - (z * (lim s))).|| < p let m be Element of NAT ; ::_thesis: ( n <= m implies ||.(((z * s) . m) - (z * (lim s))).|| < p ) assume n <= m ; ::_thesis: ||.(((z * s) . m) - (z * (lim s))).|| < p then A7: ||.((s . m) - (lim s)).|| < p / (||.z.|| + 1) by A6; 0 <= ||.((s . m) - (lim s)).|| by CLVECT_1:105; then A8: ||.z.|| * ||.((s . m) - (lim s)).|| <= ||.z.|| * (p / (||.z.|| + 1)) by A3, A7, XREAL_1:66; ||.(z * ((s . m) - (lim s))).|| <= ||.z.|| * ||.((s . m) - (lim s)).|| by CLOPBAN3:38; then A9: ||.(z * ((s . m) - (lim s))).|| <= ||.z.|| * (p / (||.z.|| + 1)) by A8, XXREAL_0:2; A10: ||.(((z * s) . m) - (z * (lim s))).|| = ||.((z * (s . m)) - (z * (lim s))).|| by CLOPBAN3:def_4 .= ||.(z * ((s . m) - (lim s))).|| by CLOPBAN3:38 ; 0 + ||.z.|| < ||.z.|| + 1 by XREAL_1:8; then A11: ||.z.|| * (p / (||.z.|| + 1)) < (||.z.|| + 1) * (p / (||.z.|| + 1)) by A3, A5, XREAL_1:97; (||.z.|| + 1) * (p / (||.z.|| + 1)) = p by A2, XCMPLX_1:87; hence ||.(((z * s) . m) - (z * (lim s))).|| < p by A10, A9, A11, XXREAL_0:2; ::_thesis: verum end; z * s is convergent by A1, Th4; hence lim (z * s) = z * (lim s) by A4, CLVECT_1:def_16; ::_thesis: verum end; theorem Th7: :: CLOPBAN4:7 for X being Complex_Banach_Algebra for z being Element of X for s being sequence of X st s is convergent holds lim (s * z) = (lim s) * z proof let X be Complex_Banach_Algebra; ::_thesis: for z being Element of X for s being sequence of X st s is convergent holds lim (s * z) = (lim s) * z let z be Element of X; ::_thesis: for s being sequence of X st s is convergent holds lim (s * z) = (lim s) * z let s be sequence of X; ::_thesis: ( s is convergent implies lim (s * z) = (lim s) * z ) assume A1: s is convergent ; ::_thesis: lim (s * z) = (lim s) * z set g1 = lim s; set g = (lim s) * z; A2: 0 + 0 < ||.z.|| + 1 by CLVECT_1:105, XREAL_1:8; A3: 0 <= ||.z.|| by CLVECT_1:105; A4: now__::_thesis:_for_p_being_Real_st_0_<_p_holds_ ex_n_being_Element_of_NAT_st_ for_m_being_Element_of_NAT_st_n_<=_m_holds_ ||.(((s_*_z)_._m)_-_((lim_s)_*_z)).||_<_p let p be Real; ::_thesis: ( 0 < p implies ex n being Element of NAT st for m being Element of NAT st n <= m holds ||.(((s * z) . m) - ((lim s) * z)).|| < p ) assume A5: 0 < p ; ::_thesis: ex n being Element of NAT st for m being Element of NAT st n <= m holds ||.(((s * z) . m) - ((lim s) * z)).|| < p then consider n being Element of NAT such that A6: for m being Element of NAT st n <= m holds ||.((s . m) - (lim s)).|| < p / (||.z.|| + 1) by A1, A2, CLVECT_1:def_16; take n = n; ::_thesis: for m being Element of NAT st n <= m holds ||.(((s * z) . m) - ((lim s) * z)).|| < p let m be Element of NAT ; ::_thesis: ( n <= m implies ||.(((s * z) . m) - ((lim s) * z)).|| < p ) assume n <= m ; ::_thesis: ||.(((s * z) . m) - ((lim s) * z)).|| < p then A7: ||.((s . m) - (lim s)).|| < p / (||.z.|| + 1) by A6; 0 <= ||.((s . m) - (lim s)).|| by CLVECT_1:105; then A8: ||.((s . m) - (lim s)).|| * ||.z.|| <= (p / (||.z.|| + 1)) * ||.z.|| by A3, A7, XREAL_1:66; ||.(((s . m) - (lim s)) * z).|| <= ||.((s . m) - (lim s)).|| * ||.z.|| by CLOPBAN3:38; then A9: ||.(((s . m) - (lim s)) * z).|| <= (p / (||.z.|| + 1)) * ||.z.|| by A8, XXREAL_0:2; A10: ||.(((s * z) . m) - ((lim s) * z)).|| = ||.(((s . m) * z) - ((lim s) * z)).|| by CLOPBAN3:def_5 .= ||.(((s . m) - (lim s)) * z).|| by CLOPBAN3:38 ; 0 + ||.z.|| < ||.z.|| + 1 by XREAL_1:8; then A11: (p / (||.z.|| + 1)) * ||.z.|| < (p / (||.z.|| + 1)) * (||.z.|| + 1) by A3, A5, XREAL_1:97; (p / (||.z.|| + 1)) * (||.z.|| + 1) = p by A2, XCMPLX_1:87; hence ||.(((s * z) . m) - ((lim s) * z)).|| < p by A10, A9, A11, XXREAL_0:2; ::_thesis: verum end; s * z is convergent by A1, Th5; hence lim (s * z) = (lim s) * z by A4, CLVECT_1:def_16; ::_thesis: verum end; theorem Th8: :: CLOPBAN4:8 for X being Complex_Banach_Algebra for s, s9 being sequence of X st s is convergent & s9 is convergent holds lim (s * s9) = (lim s) * (lim s9) proof let X be Complex_Banach_Algebra; ::_thesis: for s, s9 being sequence of X st s is convergent & s9 is convergent holds lim (s * s9) = (lim s) * (lim s9) let s, s9 be sequence of X; ::_thesis: ( s is convergent & s9 is convergent implies lim (s * s9) = (lim s) * (lim s9) ) assume that A1: s is convergent and A2: s9 is convergent ; ::_thesis: lim (s * s9) = (lim s) * (lim s9) ||.s.|| is bounded by A1, CLVECT_1:117, SEQ_2:13; then consider R being real number such that A3: for n being Element of NAT holds ||.s.|| . n < R by SEQ_2:def_3; set g2 = lim s9; set g1 = lim s; set g = (lim s) * (lim s9); A4: now__::_thesis:_for_n_being_Element_of_NAT_holds_||.(s_._n).||_<_R let n be Element of NAT ; ::_thesis: ||.(s . n).|| < R ||.(s . n).|| = ||.s.|| . n by NORMSP_0:def_4; hence ||.(s . n).|| < R by A3; ::_thesis: verum end; ||.(s . 1).|| = ||.s.|| . 1 by NORMSP_0:def_4; then 0 <= ||.s.|| . 1 by CLVECT_1:105; then A5: 0 < R by A3; reconsider R = R as Real by XREAL_0:def_1; A6: 0 + 0 < ||.(lim s9).|| + R by A5, CLVECT_1:105, XREAL_1:8; A7: 0 <= ||.(lim s9).|| by CLVECT_1:105; A8: now__::_thesis:_for_p_being_Real_st_0_<_p_holds_ ex_n_being_Element_of_NAT_st_ for_m_being_Element_of_NAT_st_n_<=_m_holds_ ||.(((s_*_s9)_._m)_-_((lim_s)_*_(lim_s9))).||_<_p let p be Real; ::_thesis: ( 0 < p implies ex n being Element of NAT st for m being Element of NAT st n <= m holds ||.(((s * s9) . m) - ((lim s) * (lim s9))).|| < p ) assume A9: 0 < p ; ::_thesis: ex n being Element of NAT st for m being Element of NAT st n <= m holds ||.(((s * s9) . m) - ((lim s) * (lim s9))).|| < p then consider n1 being Element of NAT such that A10: for m being Element of NAT st n1 <= m holds ||.((s . m) - (lim s)).|| < p / (||.(lim s9).|| + R) by A1, A6, CLVECT_1:def_16; consider n2 being Element of NAT such that A11: for m being Element of NAT st n2 <= m holds ||.((s9 . m) - (lim s9)).|| < p / (||.(lim s9).|| + R) by A2, A6, A9, CLVECT_1:def_16; take n = n1 + n2; ::_thesis: for m being Element of NAT st n <= m holds ||.(((s * s9) . m) - ((lim s) * (lim s9))).|| < p let m be Element of NAT ; ::_thesis: ( n <= m implies ||.(((s * s9) . m) - ((lim s) * (lim s9))).|| < p ) assume A12: n <= m ; ::_thesis: ||.(((s * s9) . m) - ((lim s) * (lim s9))).|| < p n1 <= n1 + n2 by NAT_1:12; then n1 <= m by A12, XXREAL_0:2; then ||.((s . m) - (lim s)).|| <= p / (||.(lim s9).|| + R) by A10; then A13: ||.(lim s9).|| * ||.((s . m) - (lim s)).|| <= ||.(lim s9).|| * (p / (||.(lim s9).|| + R)) by A7, XREAL_1:64; ||.(((s . m) - (lim s)) * (lim s9)).|| <= ||.(lim s9).|| * ||.((s . m) - (lim s)).|| by CLOPBAN3:38; then A14: ||.(((s . m) - (lim s)) * (lim s9)).|| <= ||.(lim s9).|| * (p / (||.(lim s9).|| + R)) by A13, XXREAL_0:2; A15: 0 <= ||.(s . m).|| by CLVECT_1:105; ||.(((s * s9) . m) - ((lim s) * (lim s9))).|| = ||.(((s . m) * (s9 . m)) - ((lim s) * (lim s9))).|| by CLOPBAN3:def_6 .= ||.((((s . m) * (s9 . m)) - ((s . m) * (lim s9))) + (((s . m) * (lim s9)) - ((lim s) * (lim s9)))).|| by CLOPBAN3:38 .= ||.(((s . m) * ((s9 . m) - (lim s9))) + (((s . m) * (lim s9)) - ((lim s) * (lim s9)))).|| by CLOPBAN3:38 .= ||.(((s . m) * ((s9 . m) - (lim s9))) + (((s . m) - (lim s)) * (lim s9))).|| by CLOPBAN3:38 ; then A16: ||.(((s * s9) . m) - ((lim s) * (lim s9))).|| <= ||.((s . m) * ((s9 . m) - (lim s9))).|| + ||.(((s . m) - (lim s)) * (lim s9)).|| by CLVECT_1:def_13; A17: ||.((s . m) * ((s9 . m) - (lim s9))).|| <= ||.(s . m).|| * ||.((s9 . m) - (lim s9)).|| by CLOPBAN3:38; n2 <= n by NAT_1:12; then n2 <= m by A12, XXREAL_0:2; then A18: ||.((s9 . m) - (lim s9)).|| < p / (||.(lim s9).|| + R) by A11; A19: 0 <= ||.((s9 . m) - (lim s9)).|| by CLVECT_1:105; ||.(s . m).|| < R by A4; then ||.(s . m).|| * ||.((s9 . m) - (lim s9)).|| < R * (p / (||.(lim s9).|| + R)) by A15, A19, A18, XREAL_1:96; then A20: ||.((s . m) * ((s9 . m) - (lim s9))).|| < R * (p / (||.(lim s9).|| + R)) by A17, XXREAL_0:2; (R * (p / (||.(lim s9).|| + R))) + (||.(lim s9).|| * (p / (||.(lim s9).|| + R))) = (p / (||.(lim s9).|| + R)) * (||.(lim s9).|| + R) .= p by A6, XCMPLX_1:87 ; then ||.((s . m) * ((s9 . m) - (lim s9))).|| + ||.(((s . m) - (lim s)) * (lim s9)).|| < p by A20, A14, XREAL_1:8; hence ||.(((s * s9) . m) - ((lim s) * (lim s9))).|| < p by A16, XXREAL_0:2; ::_thesis: verum end; s * s9 is convergent by A1, A2, Th3; hence lim (s * s9) = (lim s) * (lim s9) by A8, CLVECT_1:def_16; ::_thesis: verum end; theorem Th9: :: CLOPBAN4:9 for X being Complex_Banach_Algebra for z being Element of X for seq being sequence of X holds ( Partial_Sums (z * seq) = z * (Partial_Sums seq) & Partial_Sums (seq * z) = (Partial_Sums seq) * z ) proof let X be Complex_Banach_Algebra; ::_thesis: for z being Element of X for seq being sequence of X holds ( Partial_Sums (z * seq) = z * (Partial_Sums seq) & Partial_Sums (seq * z) = (Partial_Sums seq) * z ) let z be Element of X; ::_thesis: for seq being sequence of X holds ( Partial_Sums (z * seq) = z * (Partial_Sums seq) & Partial_Sums (seq * z) = (Partial_Sums seq) * z ) let seq be sequence of X; ::_thesis: ( Partial_Sums (z * seq) = z * (Partial_Sums seq) & Partial_Sums (seq * z) = (Partial_Sums seq) * z ) A1: Partial_Sums (seq * z) = (Partial_Sums seq) * z proof defpred S1[ Element of NAT ] means (Partial_Sums (seq * z)) . $1 = ((Partial_Sums seq) * z) . $1; A2: now__::_thesis:_for_n_being_Element_of_NAT_st_S1[n]_holds_ S1[n_+_1] let n be Element of NAT ; ::_thesis: ( S1[n] implies S1[n + 1] ) assume A3: S1[n] ; ::_thesis: S1[n + 1] (Partial_Sums (seq * z)) . (n + 1) = ((Partial_Sums (seq * z)) . n) + ((seq * z) . (n + 1)) by BHSP_4:def_1 .= (((Partial_Sums seq) . n) * z) + ((seq * z) . (n + 1)) by A3, CLOPBAN3:def_5 .= (((Partial_Sums seq) . n) * z) + ((seq . (n + 1)) * z) by CLOPBAN3:def_5 .= (((Partial_Sums seq) . n) + (seq . (n + 1))) * z by CLOPBAN3:38 .= ((Partial_Sums seq) . (n + 1)) * z by BHSP_4:def_1 .= ((Partial_Sums seq) * z) . (n + 1) by CLOPBAN3:def_5 ; hence S1[n + 1] ; ::_thesis: verum end; (Partial_Sums (seq * z)) . 0 = (seq * z) . 0 by BHSP_4:def_1 .= (seq . 0) * z by CLOPBAN3:def_5 .= ((Partial_Sums seq) . 0) * z by BHSP_4:def_1 .= ((Partial_Sums seq) * z) . 0 by CLOPBAN3:def_5 ; then A4: S1[ 0 ] ; for n being Element of NAT holds S1[n] from NAT_1:sch_1(A4, A2); hence Partial_Sums (seq * z) = (Partial_Sums seq) * z by FUNCT_2:63; ::_thesis: verum end; Partial_Sums (z * seq) = z * (Partial_Sums seq) proof defpred S1[ Element of NAT ] means (Partial_Sums (z * seq)) . $1 = (z * (Partial_Sums seq)) . $1; A5: now__::_thesis:_for_n_being_Element_of_NAT_st_S1[n]_holds_ S1[n_+_1] let n be Element of NAT ; ::_thesis: ( S1[n] implies S1[n + 1] ) assume A6: S1[n] ; ::_thesis: S1[n + 1] (Partial_Sums (z * seq)) . (n + 1) = ((Partial_Sums (z * seq)) . n) + ((z * seq) . (n + 1)) by BHSP_4:def_1 .= (z * ((Partial_Sums seq) . n)) + ((z * seq) . (n + 1)) by A6, CLOPBAN3:def_4 .= (z * ((Partial_Sums seq) . n)) + (z * (seq . (n + 1))) by CLOPBAN3:def_4 .= z * (((Partial_Sums seq) . n) + (seq . (n + 1))) by CLOPBAN3:38 .= z * ((Partial_Sums seq) . (n + 1)) by BHSP_4:def_1 .= (z * (Partial_Sums seq)) . (n + 1) by CLOPBAN3:def_4 ; hence S1[n + 1] ; ::_thesis: verum end; (Partial_Sums (z * seq)) . 0 = (z * seq) . 0 by BHSP_4:def_1 .= z * (seq . 0) by CLOPBAN3:def_4 .= z * ((Partial_Sums seq) . 0) by BHSP_4:def_1 .= (z * (Partial_Sums seq)) . 0 by CLOPBAN3:def_4 ; then A7: S1[ 0 ] ; for n being Element of NAT holds S1[n] from NAT_1:sch_1(A7, A5); hence Partial_Sums (z * seq) = z * (Partial_Sums seq) by FUNCT_2:63; ::_thesis: verum end; hence ( Partial_Sums (z * seq) = z * (Partial_Sums seq) & Partial_Sums (seq * z) = (Partial_Sums seq) * z ) by A1; ::_thesis: verum end; theorem Th10: :: CLOPBAN4:10 for X being Complex_Banach_Algebra for k being Element of NAT for seq being sequence of X holds ||.((Partial_Sums seq) . k).|| <= (Partial_Sums ||.seq.||) . k proof let X be Complex_Banach_Algebra; ::_thesis: for k being Element of NAT for seq being sequence of X holds ||.((Partial_Sums seq) . k).|| <= (Partial_Sums ||.seq.||) . k let k be Element of NAT ; ::_thesis: for seq being sequence of X holds ||.((Partial_Sums seq) . k).|| <= (Partial_Sums ||.seq.||) . k let seq be sequence of X; ::_thesis: ||.((Partial_Sums seq) . k).|| <= (Partial_Sums ||.seq.||) . k defpred S1[ Element of NAT ] means ||.((Partial_Sums seq) . $1).|| <= (Partial_Sums ||.seq.||) . $1; A1: now__::_thesis:_for_k_being_Element_of_NAT_st_S1[k]_holds_ S1[k_+_1] let k be Element of NAT ; ::_thesis: ( S1[k] implies S1[k + 1] ) assume S1[k] ; ::_thesis: S1[k + 1] then A2: ||.((Partial_Sums seq) . k).|| + ||.(seq . (k + 1)).|| <= ((Partial_Sums ||.seq.||) . k) + ||.(seq . (k + 1)).|| by XREAL_1:6; A3: ||.(((Partial_Sums seq) . k) + (seq . (k + 1))).|| <= ||.((Partial_Sums seq) . k).|| + ||.(seq . (k + 1)).|| by CLVECT_1:def_13; ||.((Partial_Sums seq) . (k + 1)).|| = ||.(((Partial_Sums seq) . k) + (seq . (k + 1))).|| by BHSP_4:def_1; then ||.((Partial_Sums seq) . (k + 1)).|| <= ((Partial_Sums ||.seq.||) . k) + ||.(seq . (k + 1)).|| by A3, A2, XXREAL_0:2; then ||.((Partial_Sums seq) . (k + 1)).|| <= ((Partial_Sums ||.seq.||) . k) + (||.seq.|| . (k + 1)) by NORMSP_0:def_4; hence S1[k + 1] by SERIES_1:def_1; ::_thesis: verum end; (Partial_Sums ||.seq.||) . 0 = ||.seq.|| . 0 by SERIES_1:def_1 .= ||.(seq . 0).|| by NORMSP_0:def_4 ; then A4: S1[ 0 ] by BHSP_4:def_1; for k being Element of NAT holds S1[k] from NAT_1:sch_1(A4, A1); hence ||.((Partial_Sums seq) . k).|| <= (Partial_Sums ||.seq.||) . k ; ::_thesis: verum end; theorem Th11: :: CLOPBAN4:11 for X being Complex_Banach_Algebra for m being Element of NAT for seq1, seq2 being sequence of X st ( for n being Element of NAT st n <= m holds seq1 . n = seq2 . n ) holds (Partial_Sums seq1) . m = (Partial_Sums seq2) . m proof let X be Complex_Banach_Algebra; ::_thesis: for m being Element of NAT for seq1, seq2 being sequence of X st ( for n being Element of NAT st n <= m holds seq1 . n = seq2 . n ) holds (Partial_Sums seq1) . m = (Partial_Sums seq2) . m let m be Element of NAT ; ::_thesis: for seq1, seq2 being sequence of X st ( for n being Element of NAT st n <= m holds seq1 . n = seq2 . n ) holds (Partial_Sums seq1) . m = (Partial_Sums seq2) . m let seq1, seq2 be sequence of X; ::_thesis: ( ( for n being Element of NAT st n <= m holds seq1 . n = seq2 . n ) implies (Partial_Sums seq1) . m = (Partial_Sums seq2) . m ) defpred S1[ Element of NAT ] means ( $1 <= m implies (Partial_Sums seq1) . $1 = (Partial_Sums seq2) . $1 ); assume A1: for n being Element of NAT st n <= m holds seq1 . n = seq2 . n ; ::_thesis: (Partial_Sums seq1) . m = (Partial_Sums seq2) . m A2: for k being Element of NAT st S1[k] holds S1[k + 1] proof let k be Element of NAT ; ::_thesis: ( S1[k] implies S1[k + 1] ) assume A3: S1[k] ; ::_thesis: S1[k + 1] assume A4: k + 1 <= m ; ::_thesis: (Partial_Sums seq1) . (k + 1) = (Partial_Sums seq2) . (k + 1) k < k + 1 by XREAL_1:29; hence (Partial_Sums seq1) . (k + 1) = ((Partial_Sums seq2) . k) + (seq1 . (k + 1)) by A3, A4, BHSP_4:def_1, XXREAL_0:2 .= ((Partial_Sums seq2) . k) + (seq2 . (k + 1)) by A1, A4 .= (Partial_Sums seq2) . (k + 1) by BHSP_4:def_1 ; ::_thesis: verum end; A5: S1[ 0 ] proof assume 0 <= m ; ::_thesis: (Partial_Sums seq1) . 0 = (Partial_Sums seq2) . 0 thus (Partial_Sums seq1) . 0 = seq1 . 0 by BHSP_4:def_1 .= seq2 . 0 by A1 .= (Partial_Sums seq2) . 0 by BHSP_4:def_1 ; ::_thesis: verum end; for k being Element of NAT holds S1[k] from NAT_1:sch_1(A5, A2); hence (Partial_Sums seq1) . m = (Partial_Sums seq2) . m ; ::_thesis: verum end; theorem Th12: :: CLOPBAN4:12 for X being Complex_Banach_Algebra for seq being sequence of X for rseq being Real_Sequence st ( for n being Element of NAT holds ||.(seq . n).|| <= rseq . n ) & rseq is convergent & lim rseq = 0 holds ( seq is convergent & lim seq = 0. X ) proof let X be Complex_Banach_Algebra; ::_thesis: for seq being sequence of X for rseq being Real_Sequence st ( for n being Element of NAT holds ||.(seq . n).|| <= rseq . n ) & rseq is convergent & lim rseq = 0 holds ( seq is convergent & lim seq = 0. X ) let seq be sequence of X; ::_thesis: for rseq being Real_Sequence st ( for n being Element of NAT holds ||.(seq . n).|| <= rseq . n ) & rseq is convergent & lim rseq = 0 holds ( seq is convergent & lim seq = 0. X ) let rseq be Real_Sequence; ::_thesis: ( ( for n being Element of NAT holds ||.(seq . n).|| <= rseq . n ) & rseq is convergent & lim rseq = 0 implies ( seq is convergent & lim seq = 0. X ) ) assume that A1: for n being Element of NAT holds ||.(seq . n).|| <= rseq . n and A2: rseq is convergent and A3: lim rseq = 0 ; ::_thesis: ( seq is convergent & lim seq = 0. X ) now__::_thesis:_for_p_being_real_number_st_0_<_p_holds_ ex_n_being_Element_of_NAT_st_ for_m_being_Element_of_NAT_st_n_<=_m_holds_ ||.((seq_._m)_-_(0._X)).||_<_p let p be real number ; ::_thesis: ( 0 < p implies ex n being Element of NAT st for m being Element of NAT st n <= m holds ||.((seq . m) - (0. X)).|| < p ) assume 0 < p ; ::_thesis: ex n being Element of NAT st for m being Element of NAT st n <= m holds ||.((seq . m) - (0. X)).|| < p then consider n being Element of NAT such that A4: for m being Element of NAT st n <= m holds abs ((rseq . m) - 0) < p by A2, A3, SEQ_2:def_7; now__::_thesis:_for_m_being_Element_of_NAT_st_n_<=_m_holds_ ||.((seq_._m)_-_(0._X)).||_<_p let m be Element of NAT ; ::_thesis: ( n <= m implies ||.((seq . m) - (0. X)).|| < p ) assume n <= m ; ::_thesis: ||.((seq . m) - (0. X)).|| < p then A5: abs ((rseq . m) - 0) < p by A4; A6: ||.((seq . m) - (0. X)).|| = ||.(seq . m).|| by RLVECT_1:13; A7: rseq . m <= abs (rseq . m) by ABSVALUE:4; ||.(seq . m).|| <= rseq . m by A1; then ||.((seq . m) - (0. X)).|| <= abs (rseq . m) by A6, A7, XXREAL_0:2; hence ||.((seq . m) - (0. X)).|| < p by A5, XXREAL_0:2; ::_thesis: verum end; hence ex n being Element of NAT st for m being Element of NAT st n <= m holds ||.((seq . m) - (0. X)).|| < p ; ::_thesis: verum end; then A8: for p being Real st 0 < p holds ex n being Element of NAT st for m being Element of NAT st n <= m holds ||.((seq . m) - (0. X)).|| < p ; hence seq is convergent by CLVECT_1:def_15; ::_thesis: lim seq = 0. X hence lim seq = 0. X by A8, CLVECT_1:def_16; ::_thesis: verum end; definition let X be Complex_Banach_Algebra; let z be Element of X; funcz ExpSeq -> sequence of X means :Def1: :: CLOPBAN4:def 1 for n being Element of NAT holds it . n = (1r / (n !)) * (z #N n); existence ex b1 being sequence of X st for n being Element of NAT holds b1 . n = (1r / (n !)) * (z #N n) proof deffunc H1( Element of NAT ) -> Element of the carrier of X = (1r / ($1 !)) * (z #N $1); thus ex s being sequence of X st for n being Element of NAT holds s . n = H1(n) from FUNCT_2:sch_4(); ::_thesis: verum end; uniqueness for b1, b2 being sequence of X st ( for n being Element of NAT holds b1 . n = (1r / (n !)) * (z #N n) ) & ( for n being Element of NAT holds b2 . n = (1r / (n !)) * (z #N n) ) holds b1 = b2 proof let S1, S2 be sequence of X; ::_thesis: ( ( for n being Element of NAT holds S1 . n = (1r / (n !)) * (z #N n) ) & ( for n being Element of NAT holds S2 . n = (1r / (n !)) * (z #N n) ) implies S1 = S2 ) assume that A1: for n being Element of NAT holds S1 . n = (1r / (n !)) * (z #N n) and A2: for n being Element of NAT holds S2 . n = (1r / (n !)) * (z #N n) ; ::_thesis: S1 = S2 for n being Element of NAT holds S1 . n = S2 . n proof let n be Element of NAT ; ::_thesis: S1 . n = S2 . n S1 . n = (1r / (n !)) * (z #N n) by A1; hence S1 . n = S2 . n by A2; ::_thesis: verum end; hence S1 = S2 by FUNCT_2:63; ::_thesis: verum end; end; :: deftheorem Def1 defines ExpSeq CLOPBAN4:def_1_:_ for X being Complex_Banach_Algebra for z being Element of X for b3 being sequence of X holds ( b3 = z ExpSeq iff for n being Element of NAT holds b3 . n = (1r / (n !)) * (z #N n) ); scheme :: CLOPBAN4:sch 1 ExNormSpaceCASE{ F1() -> Complex_Banach_Algebra, F2( Element of NAT , Element of NAT ) -> Point of F1() } : for k being Element of NAT ex seq being sequence of F1() st for n being Element of NAT holds ( ( n <= k implies seq . n = F2(k,n) ) & ( n > k implies seq . n = 0. F1() ) ) proof let k be Element of NAT ; ::_thesis: ex seq being sequence of F1() st for n being Element of NAT holds ( ( n <= k implies seq . n = F2(k,n) ) & ( n > k implies seq . n = 0. F1() ) ) defpred S1[ set , set ] means ex n being Element of NAT st ( n = $1 & ( n <= k implies $2 = F2(k,n) ) & ( n > k implies $2 = 0. F1() ) ); A1: now__::_thesis:_for_x_being_set_st_x_in_NAT_holds_ ex_y_being_set_st_S1[x,y] let x be set ; ::_thesis: ( x in NAT implies ex y being set st S1[x,y] ) assume x in NAT ; ::_thesis: ex y being set st S1[x,y] then consider n being Element of NAT such that A2: n = x ; reconsider y = (CHK (n,k)) * F2(k,n) as set ; A3: now__::_thesis:_(_n_>_k_implies_(CHK_(n,k))_*_F2(k,n)_=_0._F1()_) assume n > k ; ::_thesis: (CHK (n,k)) * F2(k,n) = 0. F1() hence (CHK (n,k)) * F2(k,n) = 0c * F2(k,n) by SIN_COS:def_1 .= 0. F1() by CLVECT_1:1 ; ::_thesis: verum end; take y = y; ::_thesis: S1[x,y] now__::_thesis:_(_n_<=_k_implies_(CHK_(n,k))_*_F2(k,n)_=_F2(k,n)_) assume n <= k ; ::_thesis: (CHK (n,k)) * F2(k,n) = F2(k,n) hence (CHK (n,k)) * F2(k,n) = 1r * F2(k,n) by COMPLEX1:def_4, SIN_COS:def_1 .= F2(k,n) by CLVECT_1:def_5 ; ::_thesis: verum end; hence S1[x,y] by A2, A3; ::_thesis: verum end; consider f being Function such that A4: dom f = NAT and A5: for x being set st x in NAT holds S1[x,f . x] from CLASSES1:sch_1(A1); now__::_thesis:_for_x_being_set_st_x_in_NAT_holds_ f_._x_in_the_carrier_of_F1() let x be set ; ::_thesis: ( x in NAT implies f . x in the carrier of F1() ) assume x in NAT ; ::_thesis: f . x in the carrier of F1() then ex n being Element of NAT st ( n = x & ( n <= k implies f . x = F2(k,n) ) & ( n > k implies f . x = 0. F1() ) ) by A5; hence f . x in the carrier of F1() ; ::_thesis: verum end; then reconsider f = f as sequence of F1() by A4, FUNCT_2:3; take seq = f; ::_thesis: for n being Element of NAT holds ( ( n <= k implies seq . n = F2(k,n) ) & ( n > k implies seq . n = 0. F1() ) ) let n be Element of NAT ; ::_thesis: ( ( n <= k implies seq . n = F2(k,n) ) & ( n > k implies seq . n = 0. F1() ) ) ex l being Element of NAT st ( l = n & ( l <= k implies seq . n = F2(k,l) ) & ( l > k implies seq . n = 0. F1() ) ) by A5; hence ( ( n <= k implies seq . n = F2(k,n) ) & ( n > k implies seq . n = 0. F1() ) ) ; ::_thesis: verum end; definition let n be Element of NAT ; let X be Complex_Banach_Algebra; let z, w be Element of X; func Expan (n,z,w) -> sequence of X means :Def2: :: CLOPBAN4:def 2 for k being Element of NAT holds ( ( k <= n implies it . k = (((Coef n) . k) * (z #N k)) * (w #N (n -' k)) ) & ( n < k implies it . k = 0. X ) ); existence ex b1 being sequence of X st for k being Element of NAT holds ( ( k <= n implies b1 . k = (((Coef n) . k) * (z #N k)) * (w #N (n -' k)) ) & ( n < k implies b1 . k = 0. X ) ) proof deffunc H1( Element of NAT , Element of NAT ) -> Element of the carrier of X = (((Coef $1) . $2) * (z #N $2)) * (w #N ($1 -' $2)); for n being Element of NAT ex seq being sequence of X st for k being Element of NAT holds ( ( k <= n implies seq . k = H1(n,k) ) & ( k > n implies seq . k = 0. X ) ) from CLOPBAN4:sch_1(); hence ex b1 being sequence of X st for k being Element of NAT holds ( ( k <= n implies b1 . k = (((Coef n) . k) * (z #N k)) * (w #N (n -' k)) ) & ( n < k implies b1 . k = 0. X ) ) ; ::_thesis: verum end; uniqueness for b1, b2 being sequence of X st ( for k being Element of NAT holds ( ( k <= n implies b1 . k = (((Coef n) . k) * (z #N k)) * (w #N (n -' k)) ) & ( n < k implies b1 . k = 0. X ) ) ) & ( for k being Element of NAT holds ( ( k <= n implies b2 . k = (((Coef n) . k) * (z #N k)) * (w #N (n -' k)) ) & ( n < k implies b2 . k = 0. X ) ) ) holds b1 = b2 proof let seq1, seq2 be sequence of X; ::_thesis: ( ( for k being Element of NAT holds ( ( k <= n implies seq1 . k = (((Coef n) . k) * (z #N k)) * (w #N (n -' k)) ) & ( n < k implies seq1 . k = 0. X ) ) ) & ( for k being Element of NAT holds ( ( k <= n implies seq2 . k = (((Coef n) . k) * (z #N k)) * (w #N (n -' k)) ) & ( n < k implies seq2 . k = 0. X ) ) ) implies seq1 = seq2 ) assume that A1: for k being Element of NAT holds ( ( k <= n implies seq1 . k = (((Coef n) . k) * (z #N k)) * (w #N (n -' k)) ) & ( k > n implies seq1 . k = 0. X ) ) and A2: for k being Element of NAT holds ( ( k <= n implies seq2 . k = (((Coef n) . k) * (z #N k)) * (w #N (n -' k)) ) & ( k > n implies seq2 . k = 0. X ) ) ; ::_thesis: seq1 = seq2 now__::_thesis:_for_k_being_Element_of_NAT_holds_seq1_._k_=_seq2_._k let k be Element of NAT ; ::_thesis: seq1 . b1 = seq2 . b1 percases ( k <= n or k > n ) ; supposeA3: k <= n ; ::_thesis: seq1 . b1 = seq2 . b1 hence seq1 . k = (((Coef n) . k) * (z #N k)) * (w #N (n -' k)) by A1 .= seq2 . k by A2, A3 ; ::_thesis: verum end; supposeA4: k > n ; ::_thesis: seq1 . b1 = seq2 . b1 hence seq1 . k = 0. X by A1 .= seq2 . k by A2, A4 ; ::_thesis: verum end; end; end; hence seq1 = seq2 by FUNCT_2:63; ::_thesis: verum end; end; :: deftheorem Def2 defines Expan CLOPBAN4:def_2_:_ for n being Element of NAT for X being Complex_Banach_Algebra for z, w being Element of X for b5 being sequence of X holds ( b5 = Expan (n,z,w) iff for k being Element of NAT holds ( ( k <= n implies b5 . k = (((Coef n) . k) * (z #N k)) * (w #N (n -' k)) ) & ( n < k implies b5 . k = 0. X ) ) ); definition let n be Element of NAT ; let X be Complex_Banach_Algebra; let z, w be Element of X; func Expan_e (n,z,w) -> sequence of X means :Def3: :: CLOPBAN4:def 3 for k being Element of NAT holds ( ( k <= n implies it . k = (((Coef_e n) . k) * (z #N k)) * (w #N (n -' k)) ) & ( n < k implies it . k = 0. X ) ); existence ex b1 being sequence of X st for k being Element of NAT holds ( ( k <= n implies b1 . k = (((Coef_e n) . k) * (z #N k)) * (w #N (n -' k)) ) & ( n < k implies b1 . k = 0. X ) ) proof deffunc H1( Element of NAT , Element of NAT ) -> Element of the carrier of X = (((Coef_e $1) . $2) * (z #N $2)) * (w #N ($1 -' $2)); for n being Element of NAT ex seq being sequence of X st for k being Element of NAT holds ( ( k <= n implies seq . k = H1(n,k) ) & ( k > n implies seq . k = 0. X ) ) from CLOPBAN4:sch_1(); hence ex b1 being sequence of X st for k being Element of NAT holds ( ( k <= n implies b1 . k = (((Coef_e n) . k) * (z #N k)) * (w #N (n -' k)) ) & ( n < k implies b1 . k = 0. X ) ) ; ::_thesis: verum end; uniqueness for b1, b2 being sequence of X st ( for k being Element of NAT holds ( ( k <= n implies b1 . k = (((Coef_e n) . k) * (z #N k)) * (w #N (n -' k)) ) & ( n < k implies b1 . k = 0. X ) ) ) & ( for k being Element of NAT holds ( ( k <= n implies b2 . k = (((Coef_e n) . k) * (z #N k)) * (w #N (n -' k)) ) & ( n < k implies b2 . k = 0. X ) ) ) holds b1 = b2 proof let seq1, seq2 be sequence of X; ::_thesis: ( ( for k being Element of NAT holds ( ( k <= n implies seq1 . k = (((Coef_e n) . k) * (z #N k)) * (w #N (n -' k)) ) & ( n < k implies seq1 . k = 0. X ) ) ) & ( for k being Element of NAT holds ( ( k <= n implies seq2 . k = (((Coef_e n) . k) * (z #N k)) * (w #N (n -' k)) ) & ( n < k implies seq2 . k = 0. X ) ) ) implies seq1 = seq2 ) assume that A1: for k being Element of NAT holds ( ( k <= n implies seq1 . k = (((Coef_e n) . k) * (z #N k)) * (w #N (n -' k)) ) & ( k > n implies seq1 . k = 0. X ) ) and A2: for k being Element of NAT holds ( ( k <= n implies seq2 . k = (((Coef_e n) . k) * (z #N k)) * (w #N (n -' k)) ) & ( k > n implies seq2 . k = 0. X ) ) ; ::_thesis: seq1 = seq2 now__::_thesis:_for_k_being_Element_of_NAT_holds_seq1_._k_=_seq2_._k let k be Element of NAT ; ::_thesis: seq1 . b1 = seq2 . b1 percases ( k <= n or k > n ) ; supposeA3: k <= n ; ::_thesis: seq1 . b1 = seq2 . b1 hence seq1 . k = (((Coef_e n) . k) * (z #N k)) * (w #N (n -' k)) by A1 .= seq2 . k by A2, A3 ; ::_thesis: verum end; supposeA4: k > n ; ::_thesis: seq1 . b1 = seq2 . b1 hence seq1 . k = 0. X by A1 .= seq2 . k by A2, A4 ; ::_thesis: verum end; end; end; hence seq1 = seq2 by FUNCT_2:63; ::_thesis: verum end; end; :: deftheorem Def3 defines Expan_e CLOPBAN4:def_3_:_ for n being Element of NAT for X being Complex_Banach_Algebra for z, w being Element of X for b5 being sequence of X holds ( b5 = Expan_e (n,z,w) iff for k being Element of NAT holds ( ( k <= n implies b5 . k = (((Coef_e n) . k) * (z #N k)) * (w #N (n -' k)) ) & ( n < k implies b5 . k = 0. X ) ) ); definition let n be Element of NAT ; let X be Complex_Banach_Algebra; let z, w be Element of X; func Alfa (n,z,w) -> sequence of X means :Def4: :: CLOPBAN4:def 4 for k being Element of NAT holds ( ( k <= n implies it . k = ((z ExpSeq) . k) * ((Partial_Sums (w ExpSeq)) . (n -' k)) ) & ( n < k implies it . k = 0. X ) ); existence ex b1 being sequence of X st for k being Element of NAT holds ( ( k <= n implies b1 . k = ((z ExpSeq) . k) * ((Partial_Sums (w ExpSeq)) . (n -' k)) ) & ( n < k implies b1 . k = 0. X ) ) proof deffunc H1( Element of NAT , Element of NAT ) -> Element of the carrier of X = ((z ExpSeq) . $2) * ((Partial_Sums (w ExpSeq)) . ($1 -' $2)); for n being Element of NAT ex seq being sequence of X st for k being Element of NAT holds ( ( k <= n implies seq . k = H1(n,k) ) & ( k > n implies seq . k = 0. X ) ) from CLOPBAN4:sch_1(); hence ex b1 being sequence of X st for k being Element of NAT holds ( ( k <= n implies b1 . k = ((z ExpSeq) . k) * ((Partial_Sums (w ExpSeq)) . (n -' k)) ) & ( n < k implies b1 . k = 0. X ) ) ; ::_thesis: verum end; uniqueness for b1, b2 being sequence of X st ( for k being Element of NAT holds ( ( k <= n implies b1 . k = ((z ExpSeq) . k) * ((Partial_Sums (w ExpSeq)) . (n -' k)) ) & ( n < k implies b1 . k = 0. X ) ) ) & ( for k being Element of NAT holds ( ( k <= n implies b2 . k = ((z ExpSeq) . k) * ((Partial_Sums (w ExpSeq)) . (n -' k)) ) & ( n < k implies b2 . k = 0. X ) ) ) holds b1 = b2 proof let seq1, seq2 be sequence of X; ::_thesis: ( ( for k being Element of NAT holds ( ( k <= n implies seq1 . k = ((z ExpSeq) . k) * ((Partial_Sums (w ExpSeq)) . (n -' k)) ) & ( n < k implies seq1 . k = 0. X ) ) ) & ( for k being Element of NAT holds ( ( k <= n implies seq2 . k = ((z ExpSeq) . k) * ((Partial_Sums (w ExpSeq)) . (n -' k)) ) & ( n < k implies seq2 . k = 0. X ) ) ) implies seq1 = seq2 ) assume that A1: for k being Element of NAT holds ( ( k <= n implies seq1 . k = ((z ExpSeq) . k) * ((Partial_Sums (w ExpSeq)) . (n -' k)) ) & ( k > n implies seq1 . k = 0. X ) ) and A2: for k being Element of NAT holds ( ( k <= n implies seq2 . k = ((z ExpSeq) . k) * ((Partial_Sums (w ExpSeq)) . (n -' k)) ) & ( k > n implies seq2 . k = 0. X ) ) ; ::_thesis: seq1 = seq2 now__::_thesis:_for_k_being_Element_of_NAT_holds_seq1_._k_=_seq2_._k let k be Element of NAT ; ::_thesis: seq1 . b1 = seq2 . b1 percases ( k <= n or k > n ) ; supposeA3: k <= n ; ::_thesis: seq1 . b1 = seq2 . b1 hence seq1 . k = ((z ExpSeq) . k) * ((Partial_Sums (w ExpSeq)) . (n -' k)) by A1 .= seq2 . k by A2, A3 ; ::_thesis: verum end; supposeA4: k > n ; ::_thesis: seq1 . b1 = seq2 . b1 hence seq1 . k = 0. X by A1 .= seq2 . k by A2, A4 ; ::_thesis: verum end; end; end; hence seq1 = seq2 by FUNCT_2:63; ::_thesis: verum end; end; :: deftheorem Def4 defines Alfa CLOPBAN4:def_4_:_ for n being Element of NAT for X being Complex_Banach_Algebra for z, w being Element of X for b5 being sequence of X holds ( b5 = Alfa (n,z,w) iff for k being Element of NAT holds ( ( k <= n implies b5 . k = ((z ExpSeq) . k) * ((Partial_Sums (w ExpSeq)) . (n -' k)) ) & ( n < k implies b5 . k = 0. X ) ) ); definition let X be Complex_Banach_Algebra; let z, w be Element of X; let n be Element of NAT ; func Conj (n,z,w) -> sequence of X means :Def5: :: CLOPBAN4:def 5 for k being Element of NAT holds ( ( k <= n implies it . k = ((z ExpSeq) . k) * (((Partial_Sums (w ExpSeq)) . n) - ((Partial_Sums (w ExpSeq)) . (n -' k))) ) & ( n < k implies it . k = 0. X ) ); existence ex b1 being sequence of X st for k being Element of NAT holds ( ( k <= n implies b1 . k = ((z ExpSeq) . k) * (((Partial_Sums (w ExpSeq)) . n) - ((Partial_Sums (w ExpSeq)) . (n -' k))) ) & ( n < k implies b1 . k = 0. X ) ) proof deffunc H1( Element of NAT , Element of NAT ) -> Element of the carrier of X = ((z ExpSeq) . $2) * (((Partial_Sums (w ExpSeq)) . $1) - ((Partial_Sums (w ExpSeq)) . ($1 -' $2))); for n being Element of NAT ex seq being sequence of X st for k being Element of NAT holds ( ( k <= n implies seq . k = H1(n,k) ) & ( k > n implies seq . k = 0. X ) ) from CLOPBAN4:sch_1(); hence ex b1 being sequence of X st for k being Element of NAT holds ( ( k <= n implies b1 . k = ((z ExpSeq) . k) * (((Partial_Sums (w ExpSeq)) . n) - ((Partial_Sums (w ExpSeq)) . (n -' k))) ) & ( n < k implies b1 . k = 0. X ) ) ; ::_thesis: verum end; uniqueness for b1, b2 being sequence of X st ( for k being Element of NAT holds ( ( k <= n implies b1 . k = ((z ExpSeq) . k) * (((Partial_Sums (w ExpSeq)) . n) - ((Partial_Sums (w ExpSeq)) . (n -' k))) ) & ( n < k implies b1 . k = 0. X ) ) ) & ( for k being Element of NAT holds ( ( k <= n implies b2 . k = ((z ExpSeq) . k) * (((Partial_Sums (w ExpSeq)) . n) - ((Partial_Sums (w ExpSeq)) . (n -' k))) ) & ( n < k implies b2 . k = 0. X ) ) ) holds b1 = b2 proof let seq1, seq2 be sequence of X; ::_thesis: ( ( for k being Element of NAT holds ( ( k <= n implies seq1 . k = ((z ExpSeq) . k) * (((Partial_Sums (w ExpSeq)) . n) - ((Partial_Sums (w ExpSeq)) . (n -' k))) ) & ( n < k implies seq1 . k = 0. X ) ) ) & ( for k being Element of NAT holds ( ( k <= n implies seq2 . k = ((z ExpSeq) . k) * (((Partial_Sums (w ExpSeq)) . n) - ((Partial_Sums (w ExpSeq)) . (n -' k))) ) & ( n < k implies seq2 . k = 0. X ) ) ) implies seq1 = seq2 ) assume that A1: for k being Element of NAT holds ( ( k <= n implies seq1 . k = ((z ExpSeq) . k) * (((Partial_Sums (w ExpSeq)) . n) - ((Partial_Sums (w ExpSeq)) . (n -' k))) ) & ( k > n implies seq1 . k = 0. X ) ) and A2: for k being Element of NAT holds ( ( k <= n implies seq2 . k = ((z ExpSeq) . k) * (((Partial_Sums (w ExpSeq)) . n) - ((Partial_Sums (w ExpSeq)) . (n -' k))) ) & ( k > n implies seq2 . k = 0. X ) ) ; ::_thesis: seq1 = seq2 now__::_thesis:_for_k_being_Element_of_NAT_holds_seq1_._k_=_seq2_._k let k be Element of NAT ; ::_thesis: seq1 . b1 = seq2 . b1 percases ( k <= n or k > n ) ; supposeA3: k <= n ; ::_thesis: seq1 . b1 = seq2 . b1 hence seq1 . k = ((z ExpSeq) . k) * (((Partial_Sums (w ExpSeq)) . n) - ((Partial_Sums (w ExpSeq)) . (n -' k))) by A1 .= seq2 . k by A2, A3 ; ::_thesis: verum end; supposeA4: k > n ; ::_thesis: seq1 . b1 = seq2 . b1 hence seq1 . k = 0. X by A1 .= seq2 . k by A2, A4 ; ::_thesis: verum end; end; end; hence seq1 = seq2 by FUNCT_2:63; ::_thesis: verum end; end; :: deftheorem Def5 defines Conj CLOPBAN4:def_5_:_ for X being Complex_Banach_Algebra for z, w being Element of X for n being Element of NAT for b5 being sequence of X holds ( b5 = Conj (n,z,w) iff for k being Element of NAT holds ( ( k <= n implies b5 . k = ((z ExpSeq) . k) * (((Partial_Sums (w ExpSeq)) . n) - ((Partial_Sums (w ExpSeq)) . (n -' k))) ) & ( n < k implies b5 . k = 0. X ) ) ); theorem Th13: :: CLOPBAN4:13 for X being Complex_Banach_Algebra for z being Element of X for n being Element of NAT holds ( (z ExpSeq) . (n + 1) = ((1r / (n + 1)) * z) * ((z ExpSeq) . n) & (z ExpSeq) . 0 = 1. X & ||.((z ExpSeq) . n).|| <= (||.z.|| rExpSeq) . n ) proof let X be Complex_Banach_Algebra; ::_thesis: for z being Element of X for n being Element of NAT holds ( (z ExpSeq) . (n + 1) = ((1r / (n + 1)) * z) * ((z ExpSeq) . n) & (z ExpSeq) . 0 = 1. X & ||.((z ExpSeq) . n).|| <= (||.z.|| rExpSeq) . n ) let z be Element of X; ::_thesis: for n being Element of NAT holds ( (z ExpSeq) . (n + 1) = ((1r / (n + 1)) * z) * ((z ExpSeq) . n) & (z ExpSeq) . 0 = 1. X & ||.((z ExpSeq) . n).|| <= (||.z.|| rExpSeq) . n ) let n be Element of NAT ; ::_thesis: ( (z ExpSeq) . (n + 1) = ((1r / (n + 1)) * z) * ((z ExpSeq) . n) & (z ExpSeq) . 0 = 1. X & ||.((z ExpSeq) . n).|| <= (||.z.|| rExpSeq) . n ) defpred S1[ Nat] means ||.((z ExpSeq) . $1).|| <= (||.z.|| rExpSeq) . $1; A1: (z ExpSeq) . 0 = (1r / (0 !)) * (z #N 0) by Def1 .= (1r / (0 !)) * ((z GeoSeq) . 0) by CLOPBAN3:def_8 .= 1r * (1. X) by CLOPBAN3:def_7, SIN_COS:1 .= 1. X by CLVECT_1:def_5 ; A2: now__::_thesis:_for_n_being_Element_of_NAT_holds_(z_ExpSeq)_._(n_+_1)_=_((1r_/_(n_+_1))_*_z)_*_((z_ExpSeq)_._n) let n be Element of NAT ; ::_thesis: (z ExpSeq) . (n + 1) = ((1r / (n + 1)) * z) * ((z ExpSeq) . n) thus (z ExpSeq) . (n + 1) = (1r / ((n + 1) !)) * (z #N (n + 1)) by Def1 .= (1r / ((n + 1) !)) * ((z GeoSeq) . (n + 1)) by CLOPBAN3:def_8 .= (1r / ((n + 1) !)) * (((z GeoSeq) . n) * z) by CLOPBAN3:def_7 .= (1r / ((n + 1) !)) * ((z #N n) * z) by CLOPBAN3:def_8 .= (1r / ((n !) * (n + 1))) * ((z #N n) * z) by SIN_COS:1 .= ((1r * 1r) / ((n !) * (n + 1))) * (z * (z #N n)) by Lm1, COMPLEX1:def_4 .= ((1r / (n !)) * (1r / (n + 1))) * (z * (z #N n)) by XCMPLX_1:76 .= ((1r / (n + 1)) * z) * ((1r / (n !)) * (z #N n)) by CLOPBAN3:38 .= ((1r / (n + 1)) * z) * ((z ExpSeq) . n) by Def1 ; ::_thesis: verum end; A3: for n being Element of NAT st S1[n] holds S1[n + 1] proof let n be Element of NAT ; ::_thesis: ( S1[n] implies S1[n + 1] ) assume A4: S1[n] ; ::_thesis: S1[n + 1] 0 <= ||.((1r / (n + 1)) * z).|| by CLVECT_1:105; then A5: ||.((1r / (n + 1)) * z).|| * ||.((z ExpSeq) . n).|| <= ||.((1r / (n + 1)) * z).|| * ((||.z.|| rExpSeq) . n) by A4, XREAL_1:64; A6: ||.(((1r / (n + 1)) * z) * ((z ExpSeq) . n)).|| <= ||.((1r / (n + 1)) * z).|| * ||.((z ExpSeq) . n).|| by CLOPBAN3:38; |.(n + 1).| = n + 1 by ABSVALUE:def_1; then |.(1r / (n + 1)).| = 1 / (n + 1) by COMPLEX1:48, COMPLEX1:67; then A7: ||.((1r / (n + 1)) * z).|| = (1 / (n + 1)) * ||.z.|| by CLVECT_1:def_13; A8: ((1 / (n + 1)) * ||.z.||) * ((||.z.|| rExpSeq) . n) = (1 / (n + 1)) * (((||.z.|| rExpSeq) . n) * ||.z.||) .= (1 / (n + 1)) * (((||.z.|| |^ n) / (n !)) * ||.z.||) by SIN_COS:def_5 .= (1 / (n + 1)) * (((||.z.|| |^ n) * ||.z.||) / (n !)) by XCMPLX_1:74 .= (1 / (n + 1)) * ((||.z.|| |^ (n + 1)) / (n !)) by NEWTON:6 .= (||.z.|| |^ (n + 1)) / ((n !) * (n + 1)) by XCMPLX_1:103 .= (||.z.|| |^ (n + 1)) / ((n + 1) !) by NEWTON:15 .= (||.z.|| rExpSeq) . (n + 1) by SIN_COS:def_5 ; ||.((z ExpSeq) . (n + 1)).|| = ||.(((1r / (n + 1)) * z) * ((z ExpSeq) . n)).|| by A2; hence S1[n + 1] by A6, A7, A5, A8, XXREAL_0:2; ::_thesis: verum end; (||.z.|| rExpSeq) . 0 = (||.z.|| |^ 0) / (0 !) by SIN_COS:def_5 .= 1 / (0 !) by NEWTON:4 .= 1 / (Prod_real_n . 0) by SIN_COS:def_3 .= 1 / 1 by SIN_COS:def_2 .= 1 ; then A9: S1[ 0 ] by A1, CLOPBAN3:38; for n being Element of NAT holds S1[n] from NAT_1:sch_1(A9, A3); hence ( (z ExpSeq) . (n + 1) = ((1r / (n + 1)) * z) * ((z ExpSeq) . n) & (z ExpSeq) . 0 = 1. X & ||.((z ExpSeq) . n).|| <= (||.z.|| rExpSeq) . n ) by A2, A1; ::_thesis: verum end; theorem :: CLOPBAN4:14 for X being Complex_Banach_Algebra for k being Element of NAT for seq being sequence of X st 0 < k holds (Shift seq) . k = seq . (k -' 1) by LOPBAN_4:15; theorem Th15: :: CLOPBAN4:15 for X being Complex_Banach_Algebra for k being Element of NAT for seq being sequence of X holds (Partial_Sums seq) . k = ((Partial_Sums (Shift seq)) . k) + (seq . k) proof let X be Complex_Banach_Algebra; ::_thesis: for k being Element of NAT for seq being sequence of X holds (Partial_Sums seq) . k = ((Partial_Sums (Shift seq)) . k) + (seq . k) let k be Element of NAT ; ::_thesis: for seq being sequence of X holds (Partial_Sums seq) . k = ((Partial_Sums (Shift seq)) . k) + (seq . k) let seq be sequence of X; ::_thesis: (Partial_Sums seq) . k = ((Partial_Sums (Shift seq)) . k) + (seq . k) defpred S1[ Element of NAT ] means (Partial_Sums seq) . $1 = ((Partial_Sums (Shift seq)) . $1) + (seq . $1); A1: for k being Element of NAT st S1[k] holds S1[k + 1] proof let k be Element of NAT ; ::_thesis: ( S1[k] implies S1[k + 1] ) assume (Partial_Sums seq) . k = ((Partial_Sums (Shift seq)) . k) + (seq . k) ; ::_thesis: S1[k + 1] hence (Partial_Sums seq) . (k + 1) = (((Partial_Sums (Shift seq)) . k) + (seq . k)) + (seq . (k + 1)) by BHSP_4:def_1 .= (((Partial_Sums (Shift seq)) . k) + ((Shift seq) . (k + 1))) + (seq . (k + 1)) by LOPBAN_4:def_5 .= ((Partial_Sums (Shift seq)) . (k + 1)) + (seq . (k + 1)) by BHSP_4:def_1 ; ::_thesis: verum end; (Partial_Sums seq) . 0 = seq . 0 by BHSP_4:def_1 .= (0. X) + (seq . 0) by RLVECT_1:4 .= ((Shift seq) . 0) + (seq . 0) by LOPBAN_4:def_5 .= ((Partial_Sums (Shift seq)) . 0) + (seq . 0) by BHSP_4:def_1 ; then A2: S1[ 0 ] ; for k being Element of NAT holds S1[k] from NAT_1:sch_1(A2, A1); hence (Partial_Sums seq) . k = ((Partial_Sums (Shift seq)) . k) + (seq . k) ; ::_thesis: verum end; theorem Th16: :: CLOPBAN4:16 for X being 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 proof let X be Complex_Banach_Algebra; ::_thesis: 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 ; ::_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[ 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 ; ::_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: now__::_thesis:_(_k_<=_n_+_1_implies_(((Expan_(n,z,w))_*_w)_+_(Shift_((Expan_(n,z,w))_*_z)))_._k_=_(Expan_((n_+_1),z,w))_._k_) 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_) assume A7: k < n + 1 ; ::_thesis: (((Expan (n,z,w)) * w) + (Shift ((Expan (n,z,w)) * z))) . k = (Expan ((n + 1),z,w)) . k A8: now__::_thesis:_(_k_<>_0_implies_(((Expan_(n,z,w))_*_w)_+_(Shift_((Expan_(n,z,w))_*_z)))_._k_=_(Expan_((n_+_1),z,w))_._k_) A9: (k + 1) - 1 <= (n + 1) - 1 by A7, INT_1:7; then A10: (n -' k) + 1 = (n - k) + 1 by XREAL_1:233 .= (n + 1) - k .= (n + 1) -' k by A7, XREAL_1:233 ; (n + 1) - k <> 0 by A7; then A11: (n !) / ((k !) * ((n -' k) !)) = ((n !) * ((n + 1) - k)) / (((k !) * ((n -' k) !)) * (((n + 1) - k) + (0 * ))) by XCMPLX_1:91 .= ((n !) * ((n + 1) - k)) / ((k !) * (((n -' k) !) * (((n + 1) - k) + (0 * )))) .= ((n !) * ((n + 1) - k)) / ((k !) * (((n + 1) -' k) !)) by A9, SIN_COS:2 ; assume A12: k <> 0 ; ::_thesis: (((Expan (n,z,w)) * w) + (Shift ((Expan (n,z,w)) * z))) . k = (Expan ((n + 1),z,w)) . k then A13: 0 < k ; then A14: 0 + 1 <= k by INT_1:7; then A15: (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 A9, XXREAL_0:2; then A16: k -' 1 <= n by A14, XREAL_1:233; then A17: n -' (k -' 1) = n - (k -' 1) by XREAL_1:233 .= n - (k - 1) by A14, XREAL_1:233 .= (n + 1) - k .= (n + 1) -' k by A7, XREAL_1:233 ; (((k -' 1) !) * ((n -' (k -' 1)) !)) * k = (k * ((k -' 1) !)) * ((n -' (k -' 1)) !) .= ((k + (0 * )) * ((k -' 1) !)) * ((n -' (k -' 1)) !) .= (k !) * (((n + 1) -' k) !) by A13, A17, SIN_COS:2 ; then A18: (n !) / (((k -' 1) !) * ((n -' (k -' 1)) !)) = ((n !) * k) / ((k !) * (((n + 1) -' k) !)) by A12, XCMPLX_1:91; ((Coef n) . k) + ((Coef n) . (k -' 1)) = ((n !) / ((k !) * ((n -' k) !))) + ((Coef n) . (k -' 1)) by A9, SIN_COS:def_6 .= ((n !) / ((k !) * ((n -' k) !))) + ((n !) / (((k -' 1) !) * ((n -' (k -' 1)) !))) by A16, SIN_COS:def_6 ; then A19: ((Coef n) . k) + ((Coef n) . (k -' 1)) = (((n !) * ((n + 1) - k)) + ((n !) * k)) / ((k !) * (((n + 1) -' k) !)) by A11, A18, XCMPLX_1:62 .= ((n !) * (((n + 1) - k) + k)) / ((k !) * (((n + 1) -' k) !)) .= ((n !) * ((((n + 1) - k) + k) + ((0 + 0) * ))) / ((k !) * (((n + 1) -' k) !)) .= ((n + 1) !) / ((k !) * (((n + 1) -' k) !)) by SIN_COS:1 .= (Coef (n + 1)) . k by A7, SIN_COS:def_6 ; A20: n -' (k -' 1) = n - (k -' 1) by A16, XREAL_1:233 .= n - (k - 1) by A14, XREAL_1:233 .= (n + 1) - k .= (n + 1) -' k by A7, 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 CLOPBAN3:def_5 .= (((Expan (n,z,w)) . k) * w) + (((Expan (n,z,w)) * z) . (k -' 1)) by A12, LOPBAN_4:15 .= (((Expan (n,z,w)) . k) * w) + (((Expan (n,z,w)) . (k -' 1)) * z) by CLOPBAN3:def_5 .= (((((Coef n) . k) * (z #N k)) * (w #N (n -' k))) * w) + (((Expan (n,z,w)) . (k -' 1)) * z) by A9, 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 A16, 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 CLOPBAN3:38 .= ((((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:38 .= ((((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:38 .= ((((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 A10, A20, A15, 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 A19, CLOPBAN3:38 .= (Expan ((n + 1),z,w)) . k by A7, 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_) A21: (n + 1) -' 0 = (n + 1) - 0 by XREAL_1:233; then A22: (Coef (n + 1)) . 0 = ((n + 1) !) / (1 * ((n + 1) !)) by SIN_COS:1, SIN_COS:def_6 .= 1 by XCMPLX_1:60 ; A23: n -' 0 = n - 0 by XREAL_1:233; then A24: (Coef n) . 0 = (n !) / (1 * (n !)) by SIN_COS:1, SIN_COS:def_6 .= 1 by XCMPLX_1:60 ; assume A25: 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 CLOPBAN3:def_5 .= (((Expan (n,z,w)) . 0) * w) + (0. X) by LOPBAN_4:def_5 .= ((Expan (n,z,w)) . 0) * w by CLOPBAN3:38 .= ((((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 CLOPBAN3:38 .= (((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 A25, 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 A8; ::_thesis: verum end; A26: now__::_thesis:_(_k_=_n_+_1_implies_(((Expan_(n,z,w))_*_w)_+_(Shift_((Expan_(n,z,w))_*_z)))_._k_=_(Expan_((n_+_1),z,w))_._k_) A27: (n + 1) -' (n + 1) = (n + 1) - (n + 1) by XREAL_1:233 .= 0 ; then A28: (Coef (n + 1)) . (n + 1) = ((n + 1) !) / (((n + 1) !) * 1) by SIN_COS:1, SIN_COS:def_6 .= 1 by XCMPLX_1:60 ; A29: n < n + 1 by XREAL_1:29; A30: n -' n = n - n by XREAL_1:233 .= 0 ; then A31: (Coef n) . n = (n !) / ((n !) * 1) by SIN_COS:1, SIN_COS:def_6 .= 1 by XCMPLX_1:60 ; assume A32: 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 CLOPBAN3:def_5 .= ((0. X) * w) + ((Shift ((Expan (n,z,w)) * z)) . (n + 1)) by A29, Def2 .= (0. X) + ((Shift ((Expan (n,z,w)) * z)) . (n + 1)) by CLOPBAN3:38 .= (Shift ((Expan (n,z,w)) * z)) . (n + 1) by CLOPBAN3:38 .= ((Expan (n,z,w)) * z) . n by LOPBAN_4:def_5 .= ((Expan (n,z,w)) . n) * z by CLOPBAN3:def_5 .= ((((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 CLOPBAN3:38 .= (((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:38 .= (((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 A31, A28, Lm1 .= (Expan ((n + 1),z,w)) . k by A32, A30, A27, 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 A26, A6, 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 A33: n + 1 < k ; ::_thesis: (((Expan (n,z,w)) * w) + (Shift ((Expan (n,z,w)) * z))) . k = (Expan ((n + 1),z,w)) . k then A34: (n + 1) - 1 < k - 1 by XREAL_1:9; then A35: n + 0 < (k - 1) + 1 by XREAL_1:8; 0 + 1 <= n + 1 by XREAL_1:6; then A36: k - 1 = k -' 1 by A33, 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 CLOPBAN3:def_5 .= (((Expan (n,z,w)) . k) * w) + (((Expan (n,z,w)) * z) . (k -' 1)) by A33, LOPBAN_4:15 .= (((Expan (n,z,w)) . k) * w) + (((Expan (n,z,w)) . (k -' 1)) * z) by CLOPBAN3:def_5 .= ((0. X) * w) + (((Expan (n,z,w)) . (k -' 1)) * z) by A35, Def2 .= (0. X) + (((Expan (n,z,w)) . (k -' 1)) * z) by CLOPBAN3:38 .= (0. X) + ((0. X) * z) by A34, A36, Def2 .= (0. X) + (0. X) by CLOPBAN3:38 .= 0. X by CLOPBAN3:38 ; hence (((Expan (n,z,w)) * w) + (Shift ((Expan (n,z,w)) * z))) . k = (Expan ((n + 1),z,w)) . k by A33, Def2; ::_thesis: verum end; hence (((Expan (n,z,w)) * w) + (Shift ((Expan (n,z,w)) * z))) . k = (Expan ((n + 1),z,w)) . k by A5; ::_thesis: verum end; then A37: ((Expan (n,z,w)) * w) + (Shift ((Expan (n,z,w)) * z)) = Expan ((n + 1),z,w) by FUNCT_2:63; A38: 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 CLOPBAN3:def_5 ; then A39: (Partial_Sums ((Expan (n,z,w)) * w)) . (n + 1) = ((Partial_Sums ((Expan (n,z,w)) * w)) . n) + ((0. X) * w) by A38, Def2 .= ((Partial_Sums ((Expan (n,z,w)) * w)) . n) + (0. X) by CLOPBAN3:38 .= (Partial_Sums ((Expan (n,z,w)) * w)) . n by CLOPBAN3:38 ; (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_5 ; then A40: (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 CLOPBAN3:38 ; 0 + n < n + 1 by XREAL_1:29; then A41: (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 A42: (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_5 .= ((Partial_Sums (Shift ((Expan (n,z,w)) * z))) . (n + 1)) + (0. X) by A41, CLOPBAN3:38 .= (Partial_Sums (Shift ((Expan (n,z,w)) * z))) . (n + 1) by CLOPBAN3:38 ; 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 CLOPBAN3:def_5 .= (((Expan (n,z,w)) . k) * z) + (((Expan (n,z,w)) . k) * w) by CLOPBAN3:38 .= (((Expan (n,z,w)) * z) . k) + (((Expan (n,z,w)) . k) * w) by CLOPBAN3:def_5 .= (((Expan (n,z,w)) * z) . k) + (((Expan (n,z,w)) * w) . k) by CLOPBAN3:def_5 .= (((Expan (n,z,w)) * z) + ((Expan (n,z,w)) * w)) . k by NORMSP_1:def_2 ; ::_thesis: verum end; then A43: (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 CLOPBAN3:def_5 .= (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 A43, 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 A40, A39, A42, NORMSP_1:def_2 .= (Partial_Sums (Expan ((n + 1),z,w))) . (n + 1) by A37, CLOPBAN3:15 ; ::_thesis: verum end; A44: (z + w) #N 0 = ((z + w) GeoSeq) . 0 by CLOPBAN3:def_8 .= 1. X by CLOPBAN3:def_7 ; A45: 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 A45, Def2 .= ((1r / (1r * 1r)) * (z #N 0)) * (w #N 0) by A45, 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 CLOPBAN3:38 ; then A46: S1[ 0 ] by A44; for n being Element of NAT holds S1[n] from NAT_1:sch_1(A46, A2); hence (z + w) #N n = (Partial_Sums (Expan (n,z,w))) . n ; ::_thesis: verum end; theorem Th17: :: CLOPBAN4:17 for X being Complex_Banach_Algebra for z, w being Element of X for n being Element of NAT holds Expan_e (n,z,w) = (1r / (n !)) * (Expan (n,z,w)) proof let X be Complex_Banach_Algebra; ::_thesis: for z, w being Element of X for n being Element of NAT holds Expan_e (n,z,w) = (1r / (n !)) * (Expan (n,z,w)) let z, w be Element of X; ::_thesis: for n being Element of NAT holds Expan_e (n,z,w) = (1r / (n !)) * (Expan (n,z,w)) let n be Element of NAT ; ::_thesis: Expan_e (n,z,w) = (1r / (n !)) * (Expan (n,z,w)) now__::_thesis:_for_k_being_Element_of_NAT_holds_(Expan_e_(n,z,w))_._k_=_((1r_/_(n_!))_*_(Expan_(n,z,w)))_._k let k be Element of NAT ; ::_thesis: (Expan_e (n,z,w)) . k = ((1r / (n !)) * (Expan (n,z,w))) . k A1: now__::_thesis:_(_k_<=_n_implies_(_(Expan_e_(n,z,w))_._k_=_((1r_/_((k_!)_*_((n_-'_k)_!)))_*_(z_#N_k))_*_(w_#N_(n_-'_k))_&_(Expan_e_(n,z,w))_._k_=_((1r_/_(n_!))_*_(Expan_(n,z,w)))_._k_)_) reconsider s = n ! as Element of COMPLEX by XCMPLX_0:def_2; A2: 1r / ((k !) * ((n -' k) !)) = (((n !) * 1r) / (n !)) / ((k !) * ((n -' k) !)) by COMPLEX1:def_4, XCMPLX_1:60 .= ((1r / (n !)) * (n !)) / ((k !) * ((n -' k) !)) by XCMPLX_1:74 ; assume A3: k <= n ; ::_thesis: ( (Expan_e (n,z,w)) . k = ((1r / ((k !) * ((n -' k) !))) * (z #N k)) * (w #N (n -' k)) & (Expan_e (n,z,w)) . k = ((1r / (n !)) * (Expan (n,z,w))) . k ) hence (Expan_e (n,z,w)) . k = (((Coef_e n) . k) * (z #N k)) * (w #N (n -' k)) by Def3 .= ((1r / ((k !) * ((n -' k) !))) * (z #N k)) * (w #N (n -' k)) by A3, SIN_COS:def_7 ; ::_thesis: (Expan_e (n,z,w)) . k = ((1r / (n !)) * (Expan (n,z,w))) . k hence (Expan_e (n,z,w)) . k = (((1r / (n !)) * (n !)) / ((k !) * ((n -' k) !))) * ((z #N k) * (w #N (n -' k))) by A2, CLOPBAN3:38 .= ((1r / (n !)) * ((n !) / ((k !) * ((n -' k) !)))) * ((z #N k) * (w #N (n -' k))) by XCMPLX_1:74 .= (1r / s) * ((s / ((k !) * ((n -' k) !))) * ((z #N k) * (w #N (n -' k)))) by CLOPBAN3:38 .= (1r / s) * (((s / ((k !) * ((n -' k) !))) * (z #N k)) * (w #N (n -' k))) by CLOPBAN3:38 .= (1r / (n !)) * ((((Coef n) . k) * (z #N k)) * (w #N (n -' k))) by A3, SIN_COS:def_6 .= (1r / (n !)) * ((Expan (n,z,w)) . k) by A3, Def2 .= ((1r / (n !)) * (Expan (n,z,w))) . k by CLVECT_1:def_14 ; ::_thesis: verum end; now__::_thesis:_(_n_<_k_implies_(Expan_e_(n,z,w))_._k_=_((1r_/_(n_!))_*_(Expan_(n,z,w)))_._k_) assume A4: n < k ; ::_thesis: (Expan_e (n,z,w)) . k = ((1r / (n !)) * (Expan (n,z,w))) . k hence (Expan_e (n,z,w)) . k = 0. X by Def3 .= (1r / (n !)) * (0. X) by CLOPBAN3:38 .= (1r / (n !)) * ((Expan (n,z,w)) . k) by A4, Def2 .= ((1r / (n !)) * (Expan (n,z,w))) . k by CLVECT_1:def_14 ; ::_thesis: verum end; hence (Expan_e (n,z,w)) . k = ((1r / (n !)) * (Expan (n,z,w))) . k by A1; ::_thesis: verum end; hence Expan_e (n,z,w) = (1r / (n !)) * (Expan (n,z,w)) by FUNCT_2:63; ::_thesis: verum end; theorem Th18: :: CLOPBAN4:18 for X being Complex_Banach_Algebra for n being Element of NAT for z, w being Element of X st z,w are_commutative holds (1r / (n !)) * ((z + w) #N n) = (Partial_Sums (Expan_e (n,z,w))) . n proof let X be Complex_Banach_Algebra; ::_thesis: for n being Element of NAT for z, w being Element of X st z,w are_commutative holds (1r / (n !)) * ((z + w) #N n) = (Partial_Sums (Expan_e (n,z,w))) . n let n be Element of NAT ; ::_thesis: for z, w being Element of X st z,w are_commutative holds (1r / (n !)) * ((z + w) #N n) = (Partial_Sums (Expan_e (n,z,w))) . n let z, w be Element of X; ::_thesis: ( z,w are_commutative implies (1r / (n !)) * ((z + w) #N n) = (Partial_Sums (Expan_e (n,z,w))) . n ) assume z,w are_commutative ; ::_thesis: (1r / (n !)) * ((z + w) #N n) = (Partial_Sums (Expan_e (n,z,w))) . n hence (1r / (n !)) * ((z + w) #N n) = (1r / (n !)) * ((Partial_Sums (Expan (n,z,w))) . n) by Th16 .= ((1r / (n !)) * (Partial_Sums (Expan (n,z,w)))) . n by CLVECT_1:def_14 .= (Partial_Sums ((1r / (n !)) * (Expan (n,z,w)))) . n by CLOPBAN3:19 .= (Partial_Sums (Expan_e (n,z,w))) . n by Th17 ; ::_thesis: verum end; theorem Th19: :: CLOPBAN4:19 for X being Complex_Banach_Algebra holds ( (0. X) ExpSeq is norm_summable & Sum ((0. X) ExpSeq) = 1. X ) proof let X be Complex_Banach_Algebra; ::_thesis: ( (0. X) ExpSeq is norm_summable & Sum ((0. X) ExpSeq) = 1. X ) defpred S1[ set ] means (Partial_Sums ||.((0. X) ExpSeq).||) . $1 = 1; A1: for n being Nat st S1[n] holds S1[n + 1] proof let n be Nat; ::_thesis: ( S1[n] implies S1[n + 1] ) assume A2: (Partial_Sums ||.((0. X) ExpSeq).||) . n = 1 ; ::_thesis: S1[n + 1] A3: n in NAT by ORDINAL1:def_12; hence (Partial_Sums ||.((0. X) ExpSeq).||) . (n + 1) = 1 + (||.((0. X) ExpSeq).|| . (n + 1)) by A2, SERIES_1:def_1 .= 1 + ||.(((0. X) ExpSeq) . (n + 1)).|| by NORMSP_0:def_4 .= 1 + ||.(((1r / (n + 1)) * (0. X)) * (((0. X) ExpSeq) . n)).|| by A3, Th13 .= 1 + ||.((0. X) * (((0. X) ExpSeq) . n)).|| by CLOPBAN3:38 .= 1 + ||.(0. X).|| by CLOPBAN3:38 .= 1 + 0 by CLOPBAN3:38 .= 1 ; ::_thesis: verum end; (Partial_Sums ||.((0. X) ExpSeq).||) . 0 = ||.((0. X) ExpSeq).|| . 0 by SERIES_1:def_1 .= ||.(((0. X) ExpSeq) . 0).|| by NORMSP_0:def_4 .= ||.(1. X).|| by Th13 .= 1 by CLOPBAN3:38 ; then A4: S1[ 0 ] ; for n being Nat holds S1[n] from NAT_1:sch_2(A4, A1); then Partial_Sums ||.((0. X) ExpSeq).|| is constant by VALUED_0:def_18; then A5: ||.((0. X) ExpSeq).|| is summable by SERIES_1:def_2; defpred S2[ set ] means (Partial_Sums ((0. X) ExpSeq)) . $1 = 1. X; A6: for n being Element of NAT st S2[n] holds S2[n + 1] proof let n be Element of NAT ; ::_thesis: ( S2[n] implies S2[n + 1] ) assume (Partial_Sums ((0. X) ExpSeq)) . n = 1. X ; ::_thesis: S2[n + 1] hence (Partial_Sums ((0. X) ExpSeq)) . (n + 1) = (1. X) + (((0. X) ExpSeq) . (n + 1)) by BHSP_4:def_1 .= (1. X) + (((1r / (n + 1)) * (0. X)) * (((0. X) ExpSeq) . n)) by Th13 .= (1. X) + ((0. X) * (((0. X) ExpSeq) . n)) by CLOPBAN3:38 .= (1. X) + (0. X) by CLOPBAN3:38 .= 1. X by CLOPBAN3:38 ; ::_thesis: verum end; (Partial_Sums ((0. X) ExpSeq)) . 0 = ((0. X) ExpSeq) . 0 by BHSP_4:def_1 .= 1. X by Th13 ; then A7: S2[ 0 ] ; for n being Element of NAT holds S2[n] from NAT_1:sch_1(A7, A6); then lim (Partial_Sums ((0. X) ExpSeq)) = 1. X by Th2; hence ( (0. X) ExpSeq is norm_summable & Sum ((0. X) ExpSeq) = 1. X ) by A5, CLOPBAN3:def_2, CLOPBAN3:def_3; ::_thesis: verum end; registration let X be Complex_Banach_Algebra; let z be Element of X; clusterz ExpSeq -> norm_summable ; coherence z ExpSeq is norm_summable proof ex m being Element of NAT st for n being Element of NAT st m <= n holds ||.((z ExpSeq) . n).|| <= (||.z.|| rExpSeq) . n proof take 0 ; ::_thesis: for n being Element of NAT st 0 <= n holds ||.((z ExpSeq) . n).|| <= (||.z.|| rExpSeq) . n thus for n being Element of NAT st 0 <= n holds ||.((z ExpSeq) . n).|| <= (||.z.|| rExpSeq) . n by Th13; ::_thesis: verum end; hence z ExpSeq is norm_summable by CLOPBAN3:27, SIN_COS:45; ::_thesis: verum end; end; theorem Th20: :: CLOPBAN4:20 for X being Complex_Banach_Algebra for z, w being Element of X holds ( (z ExpSeq) . 0 = 1. X & (Expan (0,z,w)) . 0 = 1. X ) proof let X be Complex_Banach_Algebra; ::_thesis: for z, w being Element of X holds ( (z ExpSeq) . 0 = 1. X & (Expan (0,z,w)) . 0 = 1. X ) let z, w be Element of X; ::_thesis: ( (z ExpSeq) . 0 = 1. X & (Expan (0,z,w)) . 0 = 1. X ) thus (z ExpSeq) . 0 = (1r / (0 !)) * (z #N 0) by Def1 .= (1r / (0 !)) * ((z GeoSeq) . 0) by CLOPBAN3:def_8 .= 1r * (1. X) by CLOPBAN3:def_7, SIN_COS:1 .= 1. X by CLOPBAN3:38 ; ::_thesis: (Expan (0,z,w)) . 0 = 1. X A1: 0 -' 0 = 0 by XREAL_1:232; hence (Expan (0,z,w)) . 0 = (((Coef 0) . 0) * (z #N 0)) * (w #N 0) by Def2 .= ((1r / (1r * 1r)) * (z #N 0)) * (w #N 0) by A1, COMPLEX1:def_4, SIN_COS:1, SIN_COS:def_6 .= (z #N 0) * (w #N 0) by CLOPBAN3:38, 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 CLOPBAN3:38 ; ::_thesis: verum end; theorem Th21: :: CLOPBAN4:21 for X being Complex_Banach_Algebra for z, w being Element of X for l, k being Element of NAT st l <= k holds (Alfa ((k + 1),z,w)) . l = ((Alfa (k,z,w)) . l) + ((Expan_e ((k + 1),z,w)) . l) proof let X be Complex_Banach_Algebra; ::_thesis: for z, w being Element of X for l, k being Element of NAT st l <= k holds (Alfa ((k + 1),z,w)) . l = ((Alfa (k,z,w)) . l) + ((Expan_e ((k + 1),z,w)) . l) let z, w be Element of X; ::_thesis: for l, k being Element of NAT st l <= k holds (Alfa ((k + 1),z,w)) . l = ((Alfa (k,z,w)) . l) + ((Expan_e ((k + 1),z,w)) . l) let l, k be Element of NAT ; ::_thesis: ( l <= k implies (Alfa ((k + 1),z,w)) . l = ((Alfa (k,z,w)) . l) + ((Expan_e ((k + 1),z,w)) . l) ) assume A1: l <= k ; ::_thesis: (Alfa ((k + 1),z,w)) . l = ((Alfa (k,z,w)) . l) + ((Expan_e ((k + 1),z,w)) . l) A2: k < k + 1 by XREAL_1:29; then A3: l <= k + 1 by A1, XXREAL_0:2; A4: ((z ExpSeq) . l) * ((w ExpSeq) . ((k + 1) -' l)) = ((1r / (l !)) * (z #N l)) * ((w ExpSeq) . ((k + 1) -' l)) by Def1 .= ((1r / (l !)) * (z #N l)) * ((1r / (((k + 1) -' l) !)) * (w #N ((k + 1) -' l))) by Def1 .= ((1r / (l !)) * (1r / (((k + 1) -' l) !))) * ((z #N l) * (w #N ((k + 1) -' l))) by CLOPBAN3:38 .= ((1r * 1r) / ((l !) * (((k + 1) -' l) !))) * ((z #N l) * (w #N ((k + 1) -' l))) by XCMPLX_1:76 .= ((Coef_e (k + 1)) . l) * ((z #N l) * (w #N ((k + 1) -' l))) by A3, COMPLEX1:def_4, SIN_COS:def_7 .= (((Coef_e (k + 1)) . l) * (z #N l)) * (w #N ((k + 1) -' l)) by CLOPBAN3:38 .= (Expan_e ((k + 1),z,w)) . l by A3, Def3 ; (k + 1) -' l = (k + 1) - l by A1, A2, XREAL_1:233, XXREAL_0:2; then A5: (k + 1) -' l = (k - l) + 1 .= (k -' l) + 1 by A1, XREAL_1:233 ; then (Alfa ((k + 1),z,w)) . l = ((z ExpSeq) . l) * ((Partial_Sums (w ExpSeq)) . ((k -' l) + 1)) by A3, Def4 .= ((z ExpSeq) . l) * (((Partial_Sums (w ExpSeq)) . (k -' l)) + ((w ExpSeq) . ((k + 1) -' l))) by A5, BHSP_4:def_1 .= (((z ExpSeq) . l) * ((Partial_Sums (w ExpSeq)) . (k -' l))) + (((z ExpSeq) . l) * ((w ExpSeq) . ((k + 1) -' l))) by CLOPBAN3:38 .= ((Alfa (k,z,w)) . l) + (((z ExpSeq) . l) * ((w ExpSeq) . ((k + 1) -' l))) by A1, Def4 ; hence (Alfa ((k + 1),z,w)) . l = ((Alfa (k,z,w)) . l) + ((Expan_e ((k + 1),z,w)) . l) by A4; ::_thesis: verum end; theorem Th22: :: CLOPBAN4:22 for X being Complex_Banach_Algebra for z, w being Element of X for k being Element of NAT holds (Partial_Sums (Alfa ((k + 1),z,w))) . k = ((Partial_Sums (Alfa (k,z,w))) . k) + ((Partial_Sums (Expan_e ((k + 1),z,w))) . k) proof let X be Complex_Banach_Algebra; ::_thesis: for z, w being Element of X for k being Element of NAT holds (Partial_Sums (Alfa ((k + 1),z,w))) . k = ((Partial_Sums (Alfa (k,z,w))) . k) + ((Partial_Sums (Expan_e ((k + 1),z,w))) . k) let z, w be Element of X; ::_thesis: for k being Element of NAT holds (Partial_Sums (Alfa ((k + 1),z,w))) . k = ((Partial_Sums (Alfa (k,z,w))) . k) + ((Partial_Sums (Expan_e ((k + 1),z,w))) . k) let k be Element of NAT ; ::_thesis: (Partial_Sums (Alfa ((k + 1),z,w))) . k = ((Partial_Sums (Alfa (k,z,w))) . k) + ((Partial_Sums (Expan_e ((k + 1),z,w))) . k) now__::_thesis:_for_l_being_Element_of_NAT_st_l_<=_k_holds_ (Alfa_((k_+_1),z,w))_._l_=_((Alfa_(k,z,w))_+_(Expan_e_((k_+_1),z,w)))_._l let l be Element of NAT ; ::_thesis: ( l <= k implies (Alfa ((k + 1),z,w)) . l = ((Alfa (k,z,w)) + (Expan_e ((k + 1),z,w))) . l ) assume l <= k ; ::_thesis: (Alfa ((k + 1),z,w)) . l = ((Alfa (k,z,w)) + (Expan_e ((k + 1),z,w))) . l hence (Alfa ((k + 1),z,w)) . l = ((Alfa (k,z,w)) . l) + ((Expan_e ((k + 1),z,w)) . l) by Th21 .= ((Alfa (k,z,w)) + (Expan_e ((k + 1),z,w))) . l by NORMSP_1:def_2 ; ::_thesis: verum end; hence (Partial_Sums (Alfa ((k + 1),z,w))) . k = (Partial_Sums ((Alfa (k,z,w)) + (Expan_e ((k + 1),z,w)))) . k by Th11 .= ((Partial_Sums (Alfa (k,z,w))) + (Partial_Sums (Expan_e ((k + 1),z,w)))) . k by CLOPBAN3:15 .= ((Partial_Sums (Alfa (k,z,w))) . k) + ((Partial_Sums (Expan_e ((k + 1),z,w))) . k) by NORMSP_1:def_2 ; ::_thesis: verum end; theorem Th23: :: CLOPBAN4:23 for X being Complex_Banach_Algebra for z, w being Element of X for k being Element of NAT holds (z ExpSeq) . k = (Expan_e (k,z,w)) . k proof let X be Complex_Banach_Algebra; ::_thesis: for z, w being Element of X for k being Element of NAT holds (z ExpSeq) . k = (Expan_e (k,z,w)) . k let z, w be Element of X; ::_thesis: for k being Element of NAT holds (z ExpSeq) . k = (Expan_e (k,z,w)) . k let k be Element of NAT ; ::_thesis: (z ExpSeq) . k = (Expan_e (k,z,w)) . k 0 = k - k ; then A1: k -' k = 0 by XREAL_1:233; hence (Expan_e (k,z,w)) . k = (((Coef_e k) . k) * (z #N k)) * (w #N 0) by Def3 .= (((Coef_e k) . k) * (z #N k)) * (1. X) by CLOPBAN3:39 .= ((Coef_e k) . k) * (z #N k) by CLOPBAN3:38 .= (1r / ((k !) * 1r)) * (z #N k) by A1, COMPLEX1:def_4, SIN_COS:1, SIN_COS:def_7 .= (z ExpSeq) . k by Def1, COMPLEX1:def_4 ; ::_thesis: verum end; theorem Th24: :: CLOPBAN4:24 for X being Complex_Banach_Algebra for n being Element of NAT for z, w being Element of X st z,w are_commutative holds (Partial_Sums ((z + w) ExpSeq)) . n = (Partial_Sums (Alfa (n,z,w))) . n proof let X be Complex_Banach_Algebra; ::_thesis: for n being Element of NAT for z, w being Element of X st z,w are_commutative holds (Partial_Sums ((z + w) ExpSeq)) . n = (Partial_Sums (Alfa (n,z,w))) . n let n be Element of NAT ; ::_thesis: for z, w being Element of X st z,w are_commutative holds (Partial_Sums ((z + w) ExpSeq)) . n = (Partial_Sums (Alfa (n,z,w))) . n let z, w be Element of X; ::_thesis: ( z,w are_commutative implies (Partial_Sums ((z + w) ExpSeq)) . n = (Partial_Sums (Alfa (n,z,w))) . n ) assume A1: z,w are_commutative ; ::_thesis: (Partial_Sums ((z + w) ExpSeq)) . n = (Partial_Sums (Alfa (n,z,w))) . n defpred S1[ Element of NAT ] means (Partial_Sums ((z + w) ExpSeq)) . $1 = (Partial_Sums (Alfa ($1,z,w))) . $1; A2: for k being Element of NAT st S1[k] holds S1[k + 1] proof let k be Element of NAT ; ::_thesis: ( S1[k] implies S1[k + 1] ) assume A3: (Partial_Sums ((z + w) ExpSeq)) . k = (Partial_Sums (Alfa (k,z,w))) . k ; ::_thesis: S1[k + 1] (k + 1) -' (k + 1) = 0 by XREAL_1:232; then (Alfa ((k + 1),z,w)) . (k + 1) = ((z ExpSeq) . (k + 1)) * ((Partial_Sums (w ExpSeq)) . 0) by Def4 .= ((z ExpSeq) . (k + 1)) * ((w ExpSeq) . 0) by BHSP_4:def_1 .= ((z ExpSeq) . (k + 1)) * (1. X) by Th20 .= (z ExpSeq) . (k + 1) by CLOPBAN3:38 .= (Expan_e ((k + 1),z,w)) . (k + 1) by Th23 ; then A4: ((Partial_Sums (Expan_e ((k + 1),z,w))) . k) + ((Alfa ((k + 1),z,w)) . (k + 1)) = (Partial_Sums (Expan_e ((k + 1),z,w))) . (k + 1) by BHSP_4:def_1 .= (1r / ((k + 1) !)) * ((z + w) #N (k + 1)) by A1, Th18 ; (Partial_Sums (Alfa ((k + 1),z,w))) . (k + 1) = ((Partial_Sums (Alfa ((k + 1),z,w))) . k) + ((Alfa ((k + 1),z,w)) . (k + 1)) by BHSP_4:def_1 .= (((Partial_Sums (Alfa (k,z,w))) . k) + ((Partial_Sums (Expan_e ((k + 1),z,w))) . k)) + ((Alfa ((k + 1),z,w)) . (k + 1)) by Th22 .= ((Partial_Sums ((z + w) ExpSeq)) . k) + (((Partial_Sums (Expan_e ((k + 1),z,w))) . k) + ((Alfa ((k + 1),z,w)) . (k + 1))) by A3, CLOPBAN3:38 ; then (Partial_Sums (Alfa ((k + 1),z,w))) . (k + 1) = ((Partial_Sums ((z + w) ExpSeq)) . k) + (((z + w) ExpSeq) . (k + 1)) by A4, Def1 .= (Partial_Sums ((z + w) ExpSeq)) . (k + 1) by BHSP_4:def_1 ; hence (Partial_Sums ((z + w) ExpSeq)) . (k + 1) = (Partial_Sums (Alfa ((k + 1),z,w))) . (k + 1) ; ::_thesis: verum end; A5: (Partial_Sums ((z + w) ExpSeq)) . 0 = ((z + w) ExpSeq) . 0 by BHSP_4:def_1 .= 1. X by Th20 ; A6: 0 -' 0 = 0 by XREAL_1:232; (Partial_Sums (Alfa (0,z,w))) . 0 = (Alfa (0,z,w)) . 0 by BHSP_4:def_1 .= ((z ExpSeq) . 0) * ((Partial_Sums (w ExpSeq)) . 0) by A6, Def4 .= ((z ExpSeq) . 0) * ((w ExpSeq) . 0) by BHSP_4:def_1 .= (1. X) * ((w ExpSeq) . 0) by Th20 .= (1. X) * (1. X) by Th20 .= 1. X by CLOPBAN3:38 ; then A7: S1[ 0 ] by A5; for n being Element of NAT holds S1[n] from NAT_1:sch_1(A7, A2); hence (Partial_Sums ((z + w) ExpSeq)) . n = (Partial_Sums (Alfa (n,z,w))) . n ; ::_thesis: verum end; theorem Th25: :: CLOPBAN4:25 for X being Complex_Banach_Algebra for k being Element of NAT for z, w being Element of X st z,w are_commutative holds (((Partial_Sums (z ExpSeq)) . k) * ((Partial_Sums (w ExpSeq)) . k)) - ((Partial_Sums ((z + w) ExpSeq)) . k) = (Partial_Sums (Conj (k,z,w))) . k proof let X be Complex_Banach_Algebra; ::_thesis: for k being Element of NAT for z, w being Element of X st z,w are_commutative holds (((Partial_Sums (z ExpSeq)) . k) * ((Partial_Sums (w ExpSeq)) . k)) - ((Partial_Sums ((z + w) ExpSeq)) . k) = (Partial_Sums (Conj (k,z,w))) . k let k be Element of NAT ; ::_thesis: for z, w being Element of X st z,w are_commutative holds (((Partial_Sums (z ExpSeq)) . k) * ((Partial_Sums (w ExpSeq)) . k)) - ((Partial_Sums ((z + w) ExpSeq)) . k) = (Partial_Sums (Conj (k,z,w))) . k let z, w be Element of X; ::_thesis: ( z,w are_commutative implies (((Partial_Sums (z ExpSeq)) . k) * ((Partial_Sums (w ExpSeq)) . k)) - ((Partial_Sums ((z + w) ExpSeq)) . k) = (Partial_Sums (Conj (k,z,w))) . k ) assume z,w are_commutative ; ::_thesis: (((Partial_Sums (z ExpSeq)) . k) * ((Partial_Sums (w ExpSeq)) . k)) - ((Partial_Sums ((z + w) ExpSeq)) . k) = (Partial_Sums (Conj (k,z,w))) . k then A1: (((Partial_Sums (z ExpSeq)) . k) * ((Partial_Sums (w ExpSeq)) . k)) - ((Partial_Sums ((z + w) ExpSeq)) . k) = (((Partial_Sums (z ExpSeq)) . k) * ((Partial_Sums (w ExpSeq)) . k)) - ((Partial_Sums (Alfa (k,z,w))) . k) by Th24 .= (((Partial_Sums (z ExpSeq)) * ((Partial_Sums (w ExpSeq)) . k)) . k) - ((Partial_Sums (Alfa (k,z,w))) . k) by CLOPBAN3:def_5 .= ((Partial_Sums ((z ExpSeq) * ((Partial_Sums (w ExpSeq)) . k))) . k) - ((Partial_Sums (Alfa (k,z,w))) . k) by Th9 .= ((Partial_Sums ((z ExpSeq) * ((Partial_Sums (w ExpSeq)) . k))) - (Partial_Sums (Alfa (k,z,w)))) . k by NORMSP_1:def_3 .= (Partial_Sums (((z ExpSeq) * ((Partial_Sums (w ExpSeq)) . k)) - (Alfa (k,z,w)))) . k by CLOPBAN3:16 ; for l being Element of NAT st l <= k holds (((z ExpSeq) * ((Partial_Sums (w ExpSeq)) . k)) - (Alfa (k,z,w))) . l = (Conj (k,z,w)) . l proof let l be Element of NAT ; ::_thesis: ( l <= k implies (((z ExpSeq) * ((Partial_Sums (w ExpSeq)) . k)) - (Alfa (k,z,w))) . l = (Conj (k,z,w)) . l ) assume A2: l <= k ; ::_thesis: (((z ExpSeq) * ((Partial_Sums (w ExpSeq)) . k)) - (Alfa (k,z,w))) . l = (Conj (k,z,w)) . l thus (((z ExpSeq) * ((Partial_Sums (w ExpSeq)) . k)) - (Alfa (k,z,w))) . l = (((z ExpSeq) * ((Partial_Sums (w ExpSeq)) . k)) . l) - ((Alfa (k,z,w)) . l) by NORMSP_1:def_3 .= (((z ExpSeq) . l) * ((Partial_Sums (w ExpSeq)) . k)) - ((Alfa (k,z,w)) . l) by CLOPBAN3:def_5 .= (((z ExpSeq) . l) * ((Partial_Sums (w ExpSeq)) . k)) - (((z ExpSeq) . l) * ((Partial_Sums (w ExpSeq)) . (k -' l))) by A2, Def4 .= ((z ExpSeq) . l) * (((Partial_Sums (w ExpSeq)) . k) - ((Partial_Sums (w ExpSeq)) . (k -' l))) by CLOPBAN3:38 .= (Conj (k,z,w)) . l by A2, Def5 ; ::_thesis: verum end; hence (((Partial_Sums (z ExpSeq)) . k) * ((Partial_Sums (w ExpSeq)) . k)) - ((Partial_Sums ((z + w) ExpSeq)) . k) = (Partial_Sums (Conj (k,z,w))) . k by A1, Th11; ::_thesis: verum end; theorem Th26: :: CLOPBAN4:26 for X being Complex_Banach_Algebra for z being Element of X for n being Element of NAT holds 0 <= (||.z.|| rExpSeq) . n proof let X be Complex_Banach_Algebra; ::_thesis: for z being Element of X for n being Element of NAT holds 0 <= (||.z.|| rExpSeq) . n let z be Element of X; ::_thesis: for n being Element of NAT holds 0 <= (||.z.|| rExpSeq) . n let n be Element of NAT ; ::_thesis: 0 <= (||.z.|| rExpSeq) . n defpred S1[ Element of NAT ] means 0 <= ||.z.|| |^ $1; A1: for k being Element of NAT st S1[k] holds S1[k + 1] proof let k be Element of NAT ; ::_thesis: ( S1[k] implies S1[k + 1] ) assume A2: S1[k] ; ::_thesis: S1[k + 1] A3: 0 <= ||.z.|| by CLVECT_1:105; ||.z.|| |^ (k + 1) = (||.z.|| |^ k) * ||.z.|| by NEWTON:6; hence S1[k + 1] by A2, A3; ::_thesis: verum end; A4: S1[ 0 ] by NEWTON:4; for k being Element of NAT holds S1[k] from NAT_1:sch_1(A4, A1); then A5: 0 <= ||.z.|| |^ n ; A6: (||.z.|| |^ n) / (n !) = (||.z.|| |^ n) * ((n !) ") by XCMPLX_0:def_9; thus 0 <= (||.z.|| rExpSeq) . n by A5, A6, SIN_COS:def_5; ::_thesis: verum end; theorem Th27: :: CLOPBAN4:27 for X being Complex_Banach_Algebra for z being Element of X for k being Element of NAT holds ( ||.((Partial_Sums (z ExpSeq)) . k).|| <= (Partial_Sums (||.z.|| rExpSeq)) . k & (Partial_Sums (||.z.|| rExpSeq)) . k <= Sum (||.z.|| rExpSeq) & ||.((Partial_Sums (z ExpSeq)) . k).|| <= Sum (||.z.|| rExpSeq) ) proof let X be Complex_Banach_Algebra; ::_thesis: for z being Element of X for k being Element of NAT holds ( ||.((Partial_Sums (z ExpSeq)) . k).|| <= (Partial_Sums (||.z.|| rExpSeq)) . k & (Partial_Sums (||.z.|| rExpSeq)) . k <= Sum (||.z.|| rExpSeq) & ||.((Partial_Sums (z ExpSeq)) . k).|| <= Sum (||.z.|| rExpSeq) ) let z be Element of X; ::_thesis: for k being Element of NAT holds ( ||.((Partial_Sums (z ExpSeq)) . k).|| <= (Partial_Sums (||.z.|| rExpSeq)) . k & (Partial_Sums (||.z.|| rExpSeq)) . k <= Sum (||.z.|| rExpSeq) & ||.((Partial_Sums (z ExpSeq)) . k).|| <= Sum (||.z.|| rExpSeq) ) let k be Element of NAT ; ::_thesis: ( ||.((Partial_Sums (z ExpSeq)) . k).|| <= (Partial_Sums (||.z.|| rExpSeq)) . k & (Partial_Sums (||.z.|| rExpSeq)) . k <= Sum (||.z.|| rExpSeq) & ||.((Partial_Sums (z ExpSeq)) . k).|| <= Sum (||.z.|| rExpSeq) ) defpred S1[ Element of NAT ] means ||.((Partial_Sums (z ExpSeq)) . $1).|| <= (Partial_Sums (||.z.|| rExpSeq)) . $1; A1: (Partial_Sums (||.z.|| rExpSeq)) . 0 = (||.z.|| rExpSeq) . 0 by SERIES_1:def_1 .= (||.z.|| |^ 0) / (0 !) by SIN_COS:def_5 .= 1 by NEWTON:4, NEWTON:12 ; A2: for k being Element of NAT st S1[k] holds S1[k + 1] proof let k be Element of NAT ; ::_thesis: ( S1[k] implies S1[k + 1] ) assume ||.((Partial_Sums (z ExpSeq)) . k).|| <= (Partial_Sums (||.z.|| rExpSeq)) . k ; ::_thesis: S1[k + 1] then A3: ||.((Partial_Sums (z ExpSeq)) . k).|| + ((||.z.|| rExpSeq) . (k + 1)) <= ((Partial_Sums (||.z.|| rExpSeq)) . k) + ((||.z.|| rExpSeq) . (k + 1)) by XREAL_1:6; A4: ||.(((Partial_Sums (z ExpSeq)) . k) + ((z ExpSeq) . (k + 1))).|| <= ||.((Partial_Sums (z ExpSeq)) . k).|| + ||.((z ExpSeq) . (k + 1)).|| by CLOPBAN3:38; ||.((z ExpSeq) . (k + 1)).|| <= (||.z.|| rExpSeq) . (k + 1) by Th13; then A5: ||.((Partial_Sums (z ExpSeq)) . k).|| + ||.((z ExpSeq) . (k + 1)).|| <= ||.((Partial_Sums (z ExpSeq)) . k).|| + ((||.z.|| rExpSeq) . (k + 1)) by XREAL_1:7; A6: ((Partial_Sums (||.z.|| rExpSeq)) . k) + ((||.z.|| rExpSeq) . (k + 1)) = (Partial_Sums (||.z.|| rExpSeq)) . (k + 1) by SERIES_1:def_1; ||.((Partial_Sums (z ExpSeq)) . (k + 1)).|| = ||.(((Partial_Sums (z ExpSeq)) . k) + ((z ExpSeq) . (k + 1))).|| by BHSP_4:def_1; then ||.((Partial_Sums (z ExpSeq)) . (k + 1)).|| <= ||.((Partial_Sums (z ExpSeq)) . k).|| + ((||.z.|| rExpSeq) . (k + 1)) by A4, A5, XXREAL_0:2; hence S1[k + 1] by A3, A6, XXREAL_0:2; ::_thesis: verum end; ||.((Partial_Sums (z ExpSeq)) . 0).|| = ||.((z ExpSeq) . 0).|| by BHSP_4:def_1 .= ||.((1r / (0 !)) * (z #N 0)).|| by Def1 .= ||.((1r / (0 !)) * ((z GeoSeq) . 0)).|| by CLOPBAN3:def_8 .= ||.(1r * (1. X)).|| by CLOPBAN3:def_7, SIN_COS:1 .= ||.(1. X).|| by CLOPBAN3:38 .= 1 by CLOPBAN3:38 ; then A7: S1[ 0 ] by A1; A8: for k being Element of NAT holds S1[k] from NAT_1:sch_1(A7, A2); hence ||.((Partial_Sums (z ExpSeq)) . k).|| <= (Partial_Sums (||.z.|| rExpSeq)) . k ; ::_thesis: ( (Partial_Sums (||.z.|| rExpSeq)) . k <= Sum (||.z.|| rExpSeq) & ||.((Partial_Sums (z ExpSeq)) . k).|| <= Sum (||.z.|| rExpSeq) ) A9: for n being Element of NAT holds 0 <= (||.z.|| rExpSeq) . n by Th26; ||.z.|| rExpSeq is summable by SIN_COS:45; then A10: Partial_Sums (||.z.|| rExpSeq) is bounded_above by A9, SERIES_1:17; then (Partial_Sums (||.z.|| rExpSeq)) . k <= lim (Partial_Sums (||.z.|| rExpSeq)) by A9, SEQ_4:37, SERIES_1:16; hence (Partial_Sums (||.z.|| rExpSeq)) . k <= Sum (||.z.|| rExpSeq) by SERIES_1:def_3; ::_thesis: ||.((Partial_Sums (z ExpSeq)) . k).|| <= Sum (||.z.|| rExpSeq) now__::_thesis:_for_k_being_Element_of_NAT_holds_(Partial_Sums_(||.z.||_rExpSeq))_._k_<=_Sum_(||.z.||_rExpSeq) let k be Element of NAT ; ::_thesis: (Partial_Sums (||.z.|| rExpSeq)) . k <= Sum (||.z.|| rExpSeq) lim (Partial_Sums (||.z.|| rExpSeq)) = Sum (||.z.|| rExpSeq) by SERIES_1:def_3; hence (Partial_Sums (||.z.|| rExpSeq)) . k <= Sum (||.z.|| rExpSeq) by A9, A10, SEQ_4:37, SERIES_1:16; ::_thesis: verum end; then A11: (Partial_Sums (||.z.|| rExpSeq)) . k <= Sum (||.z.|| rExpSeq) ; ||.((Partial_Sums (z ExpSeq)) . k).|| <= (Partial_Sums (||.z.|| rExpSeq)) . k by A8; hence ||.((Partial_Sums (z ExpSeq)) . k).|| <= Sum (||.z.|| rExpSeq) by A11, XXREAL_0:2; ::_thesis: verum end; theorem Th28: :: CLOPBAN4:28 for X being Complex_Banach_Algebra for z being Element of X holds 1 <= Sum (||.z.|| rExpSeq) proof let X be Complex_Banach_Algebra; ::_thesis: for z being Element of X holds 1 <= Sum (||.z.|| rExpSeq) let z be Element of X; ::_thesis: 1 <= Sum (||.z.|| rExpSeq) ||.((Partial_Sums (z ExpSeq)) . 0).|| = ||.((z ExpSeq) . 0).|| by BHSP_4:def_1 .= ||.(1. X).|| by Th13 .= 1 by CLOPBAN3:38 ; hence 1 <= Sum (||.z.|| rExpSeq) by Th27; ::_thesis: verum end; theorem Th29: :: CLOPBAN4:29 for X being Complex_Banach_Algebra for z being Element of X for n, m being Element of NAT holds ( abs ((Partial_Sums (||.z.|| rExpSeq)) . n) = (Partial_Sums (||.z.|| rExpSeq)) . n & ( n <= m implies abs (((Partial_Sums (||.z.|| rExpSeq)) . m) - ((Partial_Sums (||.z.|| rExpSeq)) . n)) = ((Partial_Sums (||.z.|| rExpSeq)) . m) - ((Partial_Sums (||.z.|| rExpSeq)) . n) ) ) proof let X be Complex_Banach_Algebra; ::_thesis: for z being Element of X for n, m being Element of NAT holds ( abs ((Partial_Sums (||.z.|| rExpSeq)) . n) = (Partial_Sums (||.z.|| rExpSeq)) . n & ( n <= m implies abs (((Partial_Sums (||.z.|| rExpSeq)) . m) - ((Partial_Sums (||.z.|| rExpSeq)) . n)) = ((Partial_Sums (||.z.|| rExpSeq)) . m) - ((Partial_Sums (||.z.|| rExpSeq)) . n) ) ) let z be Element of X; ::_thesis: for n, m being Element of NAT holds ( abs ((Partial_Sums (||.z.|| rExpSeq)) . n) = (Partial_Sums (||.z.|| rExpSeq)) . n & ( n <= m implies abs (((Partial_Sums (||.z.|| rExpSeq)) . m) - ((Partial_Sums (||.z.|| rExpSeq)) . n)) = ((Partial_Sums (||.z.|| rExpSeq)) . m) - ((Partial_Sums (||.z.|| rExpSeq)) . n) ) ) let n, m be Element of NAT ; ::_thesis: ( abs ((Partial_Sums (||.z.|| rExpSeq)) . n) = (Partial_Sums (||.z.|| rExpSeq)) . n & ( n <= m implies abs (((Partial_Sums (||.z.|| rExpSeq)) . m) - ((Partial_Sums (||.z.|| rExpSeq)) . n)) = ((Partial_Sums (||.z.|| rExpSeq)) . m) - ((Partial_Sums (||.z.|| rExpSeq)) . n) ) ) for n being Element of NAT holds 0 <= (||.z.|| rExpSeq) . n by Th26; hence ( abs ((Partial_Sums (||.z.|| rExpSeq)) . n) = (Partial_Sums (||.z.|| rExpSeq)) . n & ( n <= m implies abs (((Partial_Sums (||.z.|| rExpSeq)) . m) - ((Partial_Sums (||.z.|| rExpSeq)) . n)) = ((Partial_Sums (||.z.|| rExpSeq)) . m) - ((Partial_Sums (||.z.|| rExpSeq)) . n) ) ) by COMSEQ_3:9; ::_thesis: verum end; theorem Th30: :: CLOPBAN4:30 for X being Complex_Banach_Algebra for z, w being Element of X for k, n being Element of NAT holds abs ((Partial_Sums ||.(Conj (k,z,w)).||) . n) = (Partial_Sums ||.(Conj (k,z,w)).||) . n proof let X be Complex_Banach_Algebra; ::_thesis: for z, w being Element of X for k, n being Element of NAT holds abs ((Partial_Sums ||.(Conj (k,z,w)).||) . n) = (Partial_Sums ||.(Conj (k,z,w)).||) . n let z, w be Element of X; ::_thesis: for k, n being Element of NAT holds abs ((Partial_Sums ||.(Conj (k,z,w)).||) . n) = (Partial_Sums ||.(Conj (k,z,w)).||) . n let k, n be Element of NAT ; ::_thesis: abs ((Partial_Sums ||.(Conj (k,z,w)).||) . n) = (Partial_Sums ||.(Conj (k,z,w)).||) . n A1: now__::_thesis:_for_n_being_Element_of_NAT_holds_0_<=_||.(Conj_(k,z,w)).||_._n let n be Element of NAT ; ::_thesis: 0 <= ||.(Conj (k,z,w)).|| . n ||.(Conj (k,z,w)).|| . n = ||.((Conj (k,z,w)) . n).|| by NORMSP_0:def_4; hence 0 <= ||.(Conj (k,z,w)).|| . n by CLVECT_1:105; ::_thesis: verum end; then Partial_Sums ||.(Conj (k,z,w)).|| is non-decreasing by SERIES_1:16; then A2: (Partial_Sums ||.(Conj (k,z,w)).||) . 0 <= (Partial_Sums ||.(Conj (k,z,w)).||) . n by SEQM_3:6; A3: (Partial_Sums ||.(Conj (k,z,w)).||) . 0 = ||.(Conj (k,z,w)).|| . 0 by SERIES_1:def_1; 0 <= ||.(Conj (k,z,w)).|| . 0 by A1; hence abs ((Partial_Sums ||.(Conj (k,z,w)).||) . n) = (Partial_Sums ||.(Conj (k,z,w)).||) . n by A2, A3, ABSVALUE:def_1; ::_thesis: verum end; theorem Th31: :: CLOPBAN4:31 for X being Complex_Banach_Algebra for z, w being Element of X for p being real number st p > 0 holds ex n being Element of NAT st for k being Element of NAT st n <= k holds abs ((Partial_Sums ||.(Conj (k,z,w)).||) . k) < p proof let X be Complex_Banach_Algebra; ::_thesis: for z, w being Element of X for p being real number st p > 0 holds ex n being Element of NAT st for k being Element of NAT st n <= k holds abs ((Partial_Sums ||.(Conj (k,z,w)).||) . k) < p let z, w be Element of X; ::_thesis: for p being real number st p > 0 holds ex n being Element of NAT st for k being Element of NAT st n <= k holds abs ((Partial_Sums ||.(Conj (k,z,w)).||) . k) < p let p be real number ; ::_thesis: ( p > 0 implies ex n being Element of NAT st for k being Element of NAT st n <= k holds abs ((Partial_Sums ||.(Conj (k,z,w)).||) . k) < p ) assume A1: p > 0 ; ::_thesis: ex n being Element of NAT st for k being Element of NAT st n <= k holds abs ((Partial_Sums ||.(Conj (k,z,w)).||) . k) < p reconsider pp = p as Real by XREAL_0:def_1; set p1 = min ((pp / (4 * (Sum (||.z.|| rExpSeq)))),(pp / (4 * (Sum (||.w.|| rExpSeq))))); A2: 1 <= Sum (||.w.|| rExpSeq) by Th28; A3: 1 <= Sum (||.z.|| rExpSeq) by Th28; then A4: min ((pp / (4 * (Sum (||.z.|| rExpSeq)))),(pp / (4 * (Sum (||.w.|| rExpSeq))))) > 0 by A1, A2, XXREAL_0:15; Partial_Sums (w ExpSeq) is convergent by CLOPBAN3:def_1; then for s being Real st 0 < s holds ex n being Element of NAT st for m being Element of NAT st n <= m holds ||.(((Partial_Sums (w ExpSeq)) . m) - ((Partial_Sums (w ExpSeq)) . n)).|| < s by CLOPBAN3:4; then Partial_Sums (w ExpSeq) is Cauchy_sequence_by_Norm by CLOPBAN3:5; then consider n2 being Element of NAT such that A5: for k, l being Element of NAT st n2 <= k & n2 <= l holds ||.(((Partial_Sums (w ExpSeq)) . k) - ((Partial_Sums (w ExpSeq)) . l)).|| < min ((pp / (4 * (Sum (||.z.|| rExpSeq)))),(pp / (4 * (Sum (||.w.|| rExpSeq))))) by A4, CSSPACE3:8; ||.z.|| rExpSeq is summable by SIN_COS:45; then Partial_Sums (||.z.|| rExpSeq) is convergent by SERIES_1:def_2; then consider n1 being Element of NAT such that A6: for k, l being Element of NAT st n1 <= k & n1 <= l holds abs (((Partial_Sums (||.z.|| rExpSeq)) . k) - ((Partial_Sums (||.z.|| rExpSeq)) . l)) < min ((pp / (4 * (Sum (||.z.|| rExpSeq)))),(pp / (4 * (Sum (||.w.|| rExpSeq))))) by A4, COMSEQ_3:4; set n3 = n1 + n2; take n4 = (n1 + n2) + (n1 + n2); ::_thesis: for k being Element of NAT st n4 <= k holds abs ((Partial_Sums ||.(Conj (k,z,w)).||) . k) < p A7: now__::_thesis:_for_n,_k,_l_being_Element_of_NAT_st_l_<=_k_holds_ ||.(Conj_(k,z,w)).||_._l_<=_((||.z.||_rExpSeq)_._l)_*_||.(((Partial_Sums_(w_ExpSeq))_._k)_-_((Partial_Sums_(w_ExpSeq))_._(k_-'_l))).|| let n, k be Element of NAT ; ::_thesis: for l being Element of NAT st l <= k holds ||.(Conj (k,z,w)).|| . l <= ((||.z.|| rExpSeq) . l) * ||.(((Partial_Sums (w ExpSeq)) . k) - ((Partial_Sums (w ExpSeq)) . (k -' l))).|| now__::_thesis:_for_l_being_Element_of_NAT_st_l_<=_k_holds_ ||.(Conj_(k,z,w)).||_._l_<=_((||.z.||_rExpSeq)_._l)_*_||.(((Partial_Sums_(w_ExpSeq))_._k)_-_((Partial_Sums_(w_ExpSeq))_._(k_-'_l))).|| let l be Element of NAT ; ::_thesis: ( l <= k implies ||.(Conj (k,z,w)).|| . l <= ((||.z.|| rExpSeq) . l) * ||.(((Partial_Sums (w ExpSeq)) . k) - ((Partial_Sums (w ExpSeq)) . (k -' l))).|| ) assume A8: l <= k ; ::_thesis: ||.(Conj (k,z,w)).|| . l <= ((||.z.|| rExpSeq) . l) * ||.(((Partial_Sums (w ExpSeq)) . k) - ((Partial_Sums (w ExpSeq)) . (k -' l))).|| A9: ||.(((z ExpSeq) . l) * (((Partial_Sums (w ExpSeq)) . k) - ((Partial_Sums (w ExpSeq)) . (k -' l)))).|| <= ||.((z ExpSeq) . l).|| * ||.(((Partial_Sums (w ExpSeq)) . k) - ((Partial_Sums (w ExpSeq)) . (k -' l))).|| by CLOPBAN3:38; 0 <= ||.(((Partial_Sums (w ExpSeq)) . k) - ((Partial_Sums (w ExpSeq)) . (k -' l))).|| by CLVECT_1:105; then A10: ||.((z ExpSeq) . l).|| * ||.(((Partial_Sums (w ExpSeq)) . k) - ((Partial_Sums (w ExpSeq)) . (k -' l))).|| <= ((||.z.|| rExpSeq) . l) * ||.(((Partial_Sums (w ExpSeq)) . k) - ((Partial_Sums (w ExpSeq)) . (k -' l))).|| by Th13, XREAL_1:64; ||.(Conj (k,z,w)).|| . l = ||.((Conj (k,z,w)) . l).|| by NORMSP_0:def_4 .= ||.(((z ExpSeq) . l) * (((Partial_Sums (w ExpSeq)) . k) - ((Partial_Sums (w ExpSeq)) . (k -' l)))).|| by A8, Def5 ; hence ||.(Conj (k,z,w)).|| . l <= ((||.z.|| rExpSeq) . l) * ||.(((Partial_Sums (w ExpSeq)) . k) - ((Partial_Sums (w ExpSeq)) . (k -' l))).|| by A9, A10, XXREAL_0:2; ::_thesis: verum end; hence for l being Element of NAT st l <= k holds ||.(Conj (k,z,w)).|| . l <= ((||.z.|| rExpSeq) . l) * ||.(((Partial_Sums (w ExpSeq)) . k) - ((Partial_Sums (w ExpSeq)) . (k -' l))).|| ; ::_thesis: verum end; A11: now__::_thesis:_for_k,_l_being_Element_of_NAT_st_l_<=_k_holds_ ||.(Conj_(k,z,w)).||_._l_<=_((||.z.||_rExpSeq)_._l)_*_(2_*_(Sum_(||.w.||_rExpSeq))) let k be Element of NAT ; ::_thesis: for l being Element of NAT st l <= k holds ||.(Conj (k,z,w)).|| . l <= ((||.z.|| rExpSeq) . l) * (2 * (Sum (||.w.|| rExpSeq))) now__::_thesis:_for_l_being_Element_of_NAT_st_l_<=_k_holds_ ||.(Conj_(k,z,w)).||_._l_<=_((||.z.||_rExpSeq)_._l)_*_(2_*_(Sum_(||.w.||_rExpSeq))) let l be Element of NAT ; ::_thesis: ( l <= k implies ||.(Conj (k,z,w)).|| . l <= ((||.z.|| rExpSeq) . l) * (2 * (Sum (||.w.|| rExpSeq))) ) A12: ||.(((Partial_Sums (w ExpSeq)) . k) - ((Partial_Sums (w ExpSeq)) . (k -' l))).|| <= ||.((Partial_Sums (w ExpSeq)) . k).|| + ||.((Partial_Sums (w ExpSeq)) . (k -' l)).|| by CLVECT_1:104; ||.((Partial_Sums (w ExpSeq)) . (k -' l)).|| <= Sum (||.w.|| rExpSeq) by Th27; then A13: (Sum (||.w.|| rExpSeq)) + ||.((Partial_Sums (w ExpSeq)) . (k -' l)).|| <= (Sum (||.w.|| rExpSeq)) + (Sum (||.w.|| rExpSeq)) by XREAL_1:6; ||.((Partial_Sums (w ExpSeq)) . k).|| <= Sum (||.w.|| rExpSeq) by Th27; then ||.((Partial_Sums (w ExpSeq)) . k).|| + ||.((Partial_Sums (w ExpSeq)) . (k -' l)).|| <= (Sum (||.w.|| rExpSeq)) + ||.((Partial_Sums (w ExpSeq)) . (k -' l)).|| by XREAL_1:6; then ||.((Partial_Sums (w ExpSeq)) . k).|| + ||.((Partial_Sums (w ExpSeq)) . (k -' l)).|| <= 2 * (Sum (||.w.|| rExpSeq)) by A13, XXREAL_0:2; then A14: ||.(((Partial_Sums (w ExpSeq)) . k) - ((Partial_Sums (w ExpSeq)) . (k -' l))).|| <= 2 * (Sum (||.w.|| rExpSeq)) by A12, XXREAL_0:2; assume l <= k ; ::_thesis: ||.(Conj (k,z,w)).|| . l <= ((||.z.|| rExpSeq) . l) * (2 * (Sum (||.w.|| rExpSeq))) then A15: ||.(Conj (k,z,w)).|| . l <= ((||.z.|| rExpSeq) . l) * ||.(((Partial_Sums (w ExpSeq)) . k) - ((Partial_Sums (w ExpSeq)) . (k -' l))).|| by A7; 0 <= (||.z.|| rExpSeq) . l by Th26; then ((||.z.|| rExpSeq) . l) * ||.(((Partial_Sums (w ExpSeq)) . k) - ((Partial_Sums (w ExpSeq)) . (k -' l))).|| <= ((||.z.|| rExpSeq) . l) * (2 * (Sum (||.w.|| rExpSeq))) by A14, XREAL_1:64; hence ||.(Conj (k,z,w)).|| . l <= ((||.z.|| rExpSeq) . l) * (2 * (Sum (||.w.|| rExpSeq))) by A15, XXREAL_0:2; ::_thesis: verum end; hence for l being Element of NAT st l <= k holds ||.(Conj (k,z,w)).|| . l <= ((||.z.|| rExpSeq) . l) * (2 * (Sum (||.w.|| rExpSeq))) ; ::_thesis: verum end; now__::_thesis:_for_k_being_Element_of_NAT_st_n4_<=_k_holds_ abs_((Partial_Sums_||.(Conj_(k,z,w)).||)_._k)_<_p A16: 0 <> Sum (||.w.|| rExpSeq) by Th28; A17: (2 * (Sum (||.w.|| rExpSeq))) * (p / (4 * (Sum (||.w.|| rExpSeq)))) = (2 * (Sum (||.w.|| rExpSeq))) * (p * ((4 * (Sum (||.w.|| rExpSeq))) ")) by XCMPLX_0:def_9 .= ((2 * (Sum (||.w.|| rExpSeq))) * p) * ((4 * (Sum (||.w.|| rExpSeq))) ") .= ((2 * p) * (Sum (||.w.|| rExpSeq))) / (4 * (Sum (||.w.|| rExpSeq))) by XCMPLX_0:def_9 .= (2 * p) / 4 by A16, XCMPLX_1:91 .= p / 2 ; A18: 0 <> Sum (||.z.|| rExpSeq) by Th28; A19: (Sum (||.z.|| rExpSeq)) * (p / (4 * (Sum (||.z.|| rExpSeq)))) = (Sum (||.z.|| rExpSeq)) * (p * ((4 * (Sum (||.z.|| rExpSeq))) ")) by XCMPLX_0:def_9 .= ((Sum (||.z.|| rExpSeq)) * p) * ((4 * (Sum (||.z.|| rExpSeq))) ") .= ((Sum (||.z.|| rExpSeq)) * p) / (4 * (Sum (||.z.|| rExpSeq))) by XCMPLX_0:def_9 .= p / 4 by A18, XCMPLX_1:91 ; let k be Element of NAT ; ::_thesis: ( n4 <= k implies abs ((Partial_Sums ||.(Conj (k,z,w)).||) . k) < p ) assume A20: n4 <= k ; ::_thesis: abs ((Partial_Sums ||.(Conj (k,z,w)).||) . k) < p A21: 0 + (n1 + n2) <= (n1 + n2) + (n1 + n2) by XREAL_1:6; then k -' (n1 + n2) = k - (n1 + n2) by A20, XREAL_1:233, XXREAL_0:2; then A22: k = (k -' (n1 + n2)) + (n1 + n2) ; A23: n1 + n2 <= k by A20, A21, XXREAL_0:2; now__::_thesis:_for_l_being_Element_of_NAT_st_l_<=_n1_+_n2_holds_ ||.(Conj_(k,z,w)).||_._l_<=_(min_((pp_/_(4_*_(Sum_(||.z.||_rExpSeq)))),(pp_/_(4_*_(Sum_(||.w.||_rExpSeq))))))_*_((||.z.||_rExpSeq)_._l) let l be Element of NAT ; ::_thesis: ( l <= n1 + n2 implies ||.(Conj (k,z,w)).|| . l <= (min ((pp / (4 * (Sum (||.z.|| rExpSeq)))),(pp / (4 * (Sum (||.w.|| rExpSeq)))))) * ((||.z.|| rExpSeq) . l) ) assume A24: l <= n1 + n2 ; ::_thesis: ||.(Conj (k,z,w)).|| . l <= (min ((pp / (4 * (Sum (||.z.|| rExpSeq)))),(pp / (4 * (Sum (||.w.|| rExpSeq)))))) * ((||.z.|| rExpSeq) . l) then A25: ((n1 + n2) + (n1 + n2)) - (n1 + n2) <= ((n1 + n2) + (n1 + n2)) - l by XREAL_1:10; n4 - l <= k - l by A20, XREAL_1:9; then A26: n1 + n2 <= k - l by A25, XXREAL_0:2; A27: 0 + n2 <= n1 + n2 by XREAL_1:6; l <= k by A23, A24, XXREAL_0:2; then A28: ||.(Conj (k,z,w)).|| . l <= ((||.z.|| rExpSeq) . l) * ||.(((Partial_Sums (w ExpSeq)) . k) - ((Partial_Sums (w ExpSeq)) . (k -' l))).|| by A7; A29: 0 <= (||.z.|| rExpSeq) . l by Th26; 0 + (n1 + n2) <= (n1 + n2) + (n1 + n2) by XREAL_1:6; then n2 <= n4 by A27, XXREAL_0:2; then A30: n2 <= k by A20, XXREAL_0:2; k -' l = k - l by A23, A24, XREAL_1:233, XXREAL_0:2; then n2 <= k -' l by A27, A26, XXREAL_0:2; then ||.(((Partial_Sums (w ExpSeq)) . k) - ((Partial_Sums (w ExpSeq)) . (k -' l))).|| < min ((pp / (4 * (Sum (||.z.|| rExpSeq)))),(pp / (4 * (Sum (||.w.|| rExpSeq))))) by A5, A30; then ((||.z.|| rExpSeq) . l) * ||.(((Partial_Sums (w ExpSeq)) . k) - ((Partial_Sums (w ExpSeq)) . (k -' l))).|| <= ((||.z.|| rExpSeq) . l) * (min ((pp / (4 * (Sum (||.z.|| rExpSeq)))),(pp / (4 * (Sum (||.w.|| rExpSeq)))))) by A29, XREAL_1:64; hence ||.(Conj (k,z,w)).|| . l <= (min ((pp / (4 * (Sum (||.z.|| rExpSeq)))),(pp / (4 * (Sum (||.w.|| rExpSeq)))))) * ((||.z.|| rExpSeq) . l) by A28, XXREAL_0:2; ::_thesis: verum end; then A31: (Partial_Sums ||.(Conj (k,z,w)).||) . (n1 + n2) <= ((Partial_Sums (||.z.|| rExpSeq)) . (n1 + n2)) * (min ((pp / (4 * (Sum (||.z.|| rExpSeq)))),(pp / (4 * (Sum (||.w.|| rExpSeq)))))) by COMSEQ_3:7; A32: n1 + 0 <= n1 + n2 by XREAL_1:6; then n1 <= k by A23, XXREAL_0:2; then abs (((Partial_Sums (||.z.|| rExpSeq)) . k) - ((Partial_Sums (||.z.|| rExpSeq)) . (n1 + n2))) <= min ((pp / (4 * (Sum (||.z.|| rExpSeq)))),(pp / (4 * (Sum (||.w.|| rExpSeq))))) by A6, A32; then ((Partial_Sums (||.z.|| rExpSeq)) . k) - ((Partial_Sums (||.z.|| rExpSeq)) . (n1 + n2)) <= min ((pp / (4 * (Sum (||.z.|| rExpSeq)))),(pp / (4 * (Sum (||.w.|| rExpSeq))))) by A20, A21, Th29, XXREAL_0:2; then A33: (((Partial_Sums (||.z.|| rExpSeq)) . k) - ((Partial_Sums (||.z.|| rExpSeq)) . (n1 + n2))) * (2 * (Sum (||.w.|| rExpSeq))) <= (min ((pp / (4 * (Sum (||.z.|| rExpSeq)))),(pp / (4 * (Sum (||.w.|| rExpSeq)))))) * (2 * (Sum (||.w.|| rExpSeq))) by A2, XREAL_1:64; for l being Element of NAT st l <= k holds ||.(Conj (k,z,w)).|| . l <= (2 * (Sum (||.w.|| rExpSeq))) * ((||.z.|| rExpSeq) . l) by A11; then ((Partial_Sums ||.(Conj (k,z,w)).||) . k) - ((Partial_Sums ||.(Conj (k,z,w)).||) . (n1 + n2)) <= (((Partial_Sums (||.z.|| rExpSeq)) . k) - ((Partial_Sums (||.z.|| rExpSeq)) . (n1 + n2))) * (2 * (Sum (||.w.|| rExpSeq))) by A22, COMSEQ_3:8; then A34: ((Partial_Sums ||.(Conj (k,z,w)).||) . k) - ((Partial_Sums ||.(Conj (k,z,w)).||) . (n1 + n2)) <= (min ((pp / (4 * (Sum (||.z.|| rExpSeq)))),(pp / (4 * (Sum (||.w.|| rExpSeq)))))) * (2 * (Sum (||.w.|| rExpSeq))) by A33, XXREAL_0:2; A35: 0 + (p / 4) < (p / 4) + (p / 4) by A1, XREAL_1:6; ((Partial_Sums (||.z.|| rExpSeq)) . (n1 + n2)) * (min ((pp / (4 * (Sum (||.z.|| rExpSeq)))),(pp / (4 * (Sum (||.w.|| rExpSeq)))))) <= (Sum (||.z.|| rExpSeq)) * (min ((pp / (4 * (Sum (||.z.|| rExpSeq)))),(pp / (4 * (Sum (||.w.|| rExpSeq)))))) by A4, Th27, XREAL_1:64; then A36: (Partial_Sums ||.(Conj (k,z,w)).||) . (n1 + n2) <= (Sum (||.z.|| rExpSeq)) * (min ((pp / (4 * (Sum (||.z.|| rExpSeq)))),(pp / (4 * (Sum (||.w.|| rExpSeq)))))) by A31, XXREAL_0:2; (Sum (||.z.|| rExpSeq)) * (min ((pp / (4 * (Sum (||.z.|| rExpSeq)))),(pp / (4 * (Sum (||.w.|| rExpSeq)))))) <= (Sum (||.z.|| rExpSeq)) * (p / (4 * (Sum (||.z.|| rExpSeq)))) by A3, XREAL_1:64, XXREAL_0:17; then (Partial_Sums ||.(Conj (k,z,w)).||) . (n1 + n2) <= p / 4 by A36, A19, XXREAL_0:2; then A37: (Partial_Sums ||.(Conj (k,z,w)).||) . (n1 + n2) < p / 2 by A35, XXREAL_0:2; (2 * (Sum (||.w.|| rExpSeq))) * (min ((pp / (4 * (Sum (||.z.|| rExpSeq)))),(pp / (4 * (Sum (||.w.|| rExpSeq)))))) <= (2 * (Sum (||.w.|| rExpSeq))) * (p / (4 * (Sum (||.w.|| rExpSeq)))) by A2, XREAL_1:64, XXREAL_0:17; then ((Partial_Sums ||.(Conj (k,z,w)).||) . k) - ((Partial_Sums ||.(Conj (k,z,w)).||) . (n1 + n2)) <= p / 2 by A34, A17, XXREAL_0:2; then (((Partial_Sums ||.(Conj (k,z,w)).||) . k) - ((Partial_Sums ||.(Conj (k,z,w)).||) . (n1 + n2))) + ((Partial_Sums ||.(Conj (k,z,w)).||) . (n1 + n2)) < (p / 2) + (p / 2) by A37, XREAL_1:8; hence abs ((Partial_Sums ||.(Conj (k,z,w)).||) . k) < p by Th30; ::_thesis: verum end; hence for k being Element of NAT st n4 <= k holds abs ((Partial_Sums ||.(Conj (k,z,w)).||) . k) < p ; ::_thesis: verum end; theorem Th32: :: CLOPBAN4:32 for X being Complex_Banach_Algebra for z, w being Element of X for seq being sequence of X st ( for k being Element of NAT holds seq . k = (Partial_Sums (Conj (k,z,w))) . k ) holds ( seq is convergent & lim seq = 0. X ) proof let X be Complex_Banach_Algebra; ::_thesis: for z, w being Element of X for seq being sequence of X st ( for k being Element of NAT holds seq . k = (Partial_Sums (Conj (k,z,w))) . k ) holds ( seq is convergent & lim seq = 0. X ) let z, w be Element of X; ::_thesis: for seq being sequence of X st ( for k being Element of NAT holds seq . k = (Partial_Sums (Conj (k,z,w))) . k ) holds ( seq is convergent & lim seq = 0. X ) deffunc H1( Element of NAT ) -> Element of REAL = (Partial_Sums ||.(Conj ($1,z,w)).||) . $1; ex rseq being Real_Sequence st for k being Element of NAT holds rseq . k = H1(k) from SEQ_1:sch_1(); then consider rseq being Real_Sequence such that A1: for k being Element of NAT holds rseq . k = (Partial_Sums ||.(Conj (k,z,w)).||) . k ; let seq be sequence of X; ::_thesis: ( ( for k being Element of NAT holds seq . k = (Partial_Sums (Conj (k,z,w))) . k ) implies ( seq is convergent & lim seq = 0. X ) ) assume A2: for k being Element of NAT holds seq . k = (Partial_Sums (Conj (k,z,w))) . k ; ::_thesis: ( seq is convergent & lim seq = 0. X ) A3: now__::_thesis:_for_k_being_Element_of_NAT_holds_||.(seq_._k).||_<=_(Partial_Sums_||.(Conj_(k,z,w)).||)_._k let k be Element of NAT ; ::_thesis: ||.(seq . k).|| <= (Partial_Sums ||.(Conj (k,z,w)).||) . k ||.(seq . k).|| = ||.((Partial_Sums (Conj (k,z,w))) . k).|| by A2; hence ||.(seq . k).|| <= (Partial_Sums ||.(Conj (k,z,w)).||) . k by Th10; ::_thesis: verum end; A4: now__::_thesis:_for_k_being_Element_of_NAT_holds_||.(seq_._k).||_<=_rseq_._k let k be Element of NAT ; ::_thesis: ||.(seq . k).|| <= rseq . k ||.(seq . k).|| <= (Partial_Sums ||.(Conj (k,z,w)).||) . k by A3; hence ||.(seq . k).|| <= rseq . k by A1; ::_thesis: verum end; A5: now__::_thesis:_for_p_being_real_number_st_p_>_0_holds_ ex_n_being_Element_of_NAT_st_ for_k_being_Element_of_NAT_st_n_<=_k_holds_ abs_((rseq_._k)_-_0)_<_p let p be real number ; ::_thesis: ( p > 0 implies ex n being Element of NAT st for k being Element of NAT st n <= k holds abs ((rseq . k) - 0) < p ) assume p > 0 ; ::_thesis: ex n being Element of NAT st for k being Element of NAT st n <= k holds abs ((rseq . k) - 0) < p then consider n being Element of NAT such that A6: for k being Element of NAT st n <= k holds abs ((Partial_Sums ||.(Conj (k,z,w)).||) . k) < p by Th31; take n = n; ::_thesis: for k being Element of NAT st n <= k holds abs ((rseq . k) - 0) < p now__::_thesis:_for_k_being_Element_of_NAT_st_n_<=_k_holds_ abs_((rseq_._k)_-_0)_<_p let k be Element of NAT ; ::_thesis: ( n <= k implies abs ((rseq . k) - 0) < p ) assume A7: n <= k ; ::_thesis: abs ((rseq . k) - 0) < p abs ((rseq . k) - 0) = abs ((Partial_Sums ||.(Conj (k,z,w)).||) . k) by A1; hence abs ((rseq . k) - 0) < p by A6, A7; ::_thesis: verum end; hence for k being Element of NAT st n <= k holds abs ((rseq . k) - 0) < p ; ::_thesis: verum end; then A8: rseq is convergent by SEQ_2:def_6; then lim rseq = 0 by A5, SEQ_2:def_7; hence ( seq is convergent & lim seq = 0. X ) by A4, A8, Th12; ::_thesis: verum end; Lm3: for X being Complex_Banach_Algebra for z, w being Element of X st z,w are_commutative holds (Sum (z ExpSeq)) * (Sum (w ExpSeq)) = Sum ((z + w) ExpSeq) proof let X be Complex_Banach_Algebra; ::_thesis: for z, w being Element of X st z,w are_commutative holds (Sum (z ExpSeq)) * (Sum (w ExpSeq)) = Sum ((z + w) ExpSeq) let z, w be Element of X; ::_thesis: ( z,w are_commutative implies (Sum (z ExpSeq)) * (Sum (w ExpSeq)) = Sum ((z + w) ExpSeq) ) assume A1: z,w are_commutative ; ::_thesis: (Sum (z ExpSeq)) * (Sum (w ExpSeq)) = Sum ((z + w) ExpSeq) deffunc H1( Element of NAT ) -> Element of the carrier of X = (Partial_Sums (Conj ($1,z,w))) . $1; ex seq being sequence of X st for k being Element of NAT holds seq . k = H1(k) from FUNCT_2:sch_4(); then consider seq being sequence of X such that A2: for k being Element of NAT holds seq . k = (Partial_Sums (Conj (k,z,w))) . k ; now__::_thesis:_for_k_being_Element_of_NAT_holds_seq_._k_=_(((Partial_Sums_(z_ExpSeq))_*_(Partial_Sums_(w_ExpSeq)))_-_(Partial_Sums_((z_+_w)_ExpSeq)))_._k let k be Element of NAT ; ::_thesis: seq . k = (((Partial_Sums (z ExpSeq)) * (Partial_Sums (w ExpSeq))) - (Partial_Sums ((z + w) ExpSeq))) . k thus seq . k = (Partial_Sums (Conj (k,z,w))) . k by A2 .= (((Partial_Sums (z ExpSeq)) . k) * ((Partial_Sums (w ExpSeq)) . k)) - ((Partial_Sums ((z + w) ExpSeq)) . k) by A1, Th25 .= (((Partial_Sums (z ExpSeq)) * (Partial_Sums (w ExpSeq))) . k) - ((Partial_Sums ((z + w) ExpSeq)) . k) by CLOPBAN3:def_6 .= (((Partial_Sums (z ExpSeq)) * (Partial_Sums (w ExpSeq))) - (Partial_Sums ((z + w) ExpSeq))) . k by NORMSP_1:def_3 ; ::_thesis: verum end; then A3: seq = ((Partial_Sums (z ExpSeq)) * (Partial_Sums (w ExpSeq))) - (Partial_Sums ((z + w) ExpSeq)) by FUNCT_2:63; A4: Partial_Sums (w ExpSeq) is convergent by CLOPBAN3:def_1; A5: lim seq = 0. X by A2, Th32; A6: Partial_Sums ((z + w) ExpSeq) is convergent by CLOPBAN3:def_1; A7: Partial_Sums (z ExpSeq) is convergent by CLOPBAN3:def_1; then A8: (Partial_Sums (z ExpSeq)) * (Partial_Sums (w ExpSeq)) is convergent by A4, Th3; A9: lim ((Partial_Sums (z ExpSeq)) * (Partial_Sums (w ExpSeq))) = (lim (Partial_Sums (z ExpSeq))) * (lim (Partial_Sums (w ExpSeq))) by A7, A4, Th8; thus Sum ((z + w) ExpSeq) = lim (Partial_Sums ((z + w) ExpSeq)) by CLOPBAN3:def_2 .= (lim (Partial_Sums (z ExpSeq))) * (lim (Partial_Sums (w ExpSeq))) by A3, A6, A8, A9, A5, Th1 .= (Sum (z ExpSeq)) * (lim (Partial_Sums (w ExpSeq))) by CLOPBAN3:def_2 .= (Sum (z ExpSeq)) * (Sum (w ExpSeq)) by CLOPBAN3:def_2 ; ::_thesis: verum end; definition let X be Complex_Banach_Algebra; func exp_ X -> Function of the carrier of X, the carrier of X means :Def6: :: CLOPBAN4:def 6 for z being Element of X holds it . z = Sum (z ExpSeq); existence ex b1 being Function of the carrier of X, the carrier of X st for z being Element of X holds b1 . z = Sum (z ExpSeq) proof deffunc H1( Element of X) -> Element of the carrier of X = Sum ($1 ExpSeq); ex f being Function of the carrier of X, the carrier of X st for z being Element of X holds f . z = H1(z) from FUNCT_2:sch_4(); hence ex b1 being Function of the carrier of X, the carrier of X st for z being Element of X holds b1 . z = Sum (z ExpSeq) ; ::_thesis: verum end; uniqueness for b1, b2 being Function of the carrier of X, the carrier of X st ( for z being Element of X holds b1 . z = Sum (z ExpSeq) ) & ( for z being Element of X holds b2 . z = Sum (z ExpSeq) ) holds b1 = b2 proof let f1, f2 be Function of the carrier of X, the carrier of X; ::_thesis: ( ( for z being Element of X holds f1 . z = Sum (z ExpSeq) ) & ( for z being Element of X holds f2 . z = Sum (z ExpSeq) ) implies f1 = f2 ) assume that A1: for z being Element of X holds f1 . z = Sum (z ExpSeq) and A2: for z being Element of X holds f2 . z = Sum (z ExpSeq) ; ::_thesis: f1 = f2 for z being Element of X holds f1 . z = f2 . z proof let z be Element of X; ::_thesis: f1 . z = f2 . z thus f1 . z = Sum (z ExpSeq) by A1 .= f2 . z by A2 ; ::_thesis: verum end; hence f1 = f2 by FUNCT_2:63; ::_thesis: verum end; end; :: deftheorem Def6 defines exp_ CLOPBAN4:def_6_:_ for X being Complex_Banach_Algebra for b2 being Function of the carrier of X, the carrier of X holds ( b2 = exp_ X iff for z being Element of X holds b2 . z = Sum (z ExpSeq) ); definition let X be Complex_Banach_Algebra; let z be Element of X; func exp z -> Element of X equals :: CLOPBAN4:def 7 (exp_ X) . z; correctness coherence (exp_ X) . z is Element of X; ; end; :: deftheorem defines exp CLOPBAN4:def_7_:_ for X being Complex_Banach_Algebra for z being Element of X holds exp z = (exp_ X) . z; theorem :: CLOPBAN4:33 for X being Complex_Banach_Algebra for z being Element of X holds exp z = Sum (z ExpSeq) by Def6; theorem Th34: :: CLOPBAN4:34 for X being Complex_Banach_Algebra for z1, z2 being Element of X st z1,z2 are_commutative holds ( exp (z1 + z2) = (exp z1) * (exp z2) & exp (z2 + z1) = (exp z2) * (exp z1) & exp (z1 + z2) = exp (z2 + z1) & exp z1, exp z2 are_commutative ) proof let X be Complex_Banach_Algebra; ::_thesis: for z1, z2 being Element of X st z1,z2 are_commutative holds ( exp (z1 + z2) = (exp z1) * (exp z2) & exp (z2 + z1) = (exp z2) * (exp z1) & exp (z1 + z2) = exp (z2 + z1) & exp z1, exp z2 are_commutative ) let z1, z2 be Element of X; ::_thesis: ( z1,z2 are_commutative implies ( exp (z1 + z2) = (exp z1) * (exp z2) & exp (z2 + z1) = (exp z2) * (exp z1) & exp (z1 + z2) = exp (z2 + z1) & exp z1, exp z2 are_commutative ) ) assume A1: z1,z2 are_commutative ; ::_thesis: ( exp (z1 + z2) = (exp z1) * (exp z2) & exp (z2 + z1) = (exp z2) * (exp z1) & exp (z1 + z2) = exp (z2 + z1) & exp z1, exp z2 are_commutative ) A2: exp (z2 + z1) = Sum ((z2 + z1) ExpSeq) by Def6 .= (Sum (z2 ExpSeq)) * (Sum (z1 ExpSeq)) by A1, Lm3 .= (exp z2) * (Sum (z1 ExpSeq)) by Def6 .= (exp z2) * (exp z1) by Def6 ; exp (z1 + z2) = Sum ((z1 + z2) ExpSeq) by Def6 .= (Sum (z1 ExpSeq)) * (Sum (z2 ExpSeq)) by A1, Lm3 .= (exp z1) * (Sum (z2 ExpSeq)) by Def6 .= (exp z1) * (exp z2) by Def6 ; hence ( exp (z1 + z2) = (exp z1) * (exp z2) & exp (z2 + z1) = (exp z2) * (exp z1) & exp (z1 + z2) = exp (z2 + z1) & exp z1, exp z2 are_commutative ) by A2, LOPBAN_4:def_1; ::_thesis: verum end; theorem :: CLOPBAN4:35 for X being Complex_Banach_Algebra for z1, z2 being Element of X st z1,z2 are_commutative holds z1 * (exp z2) = (exp z2) * z1 proof let X be Complex_Banach_Algebra; ::_thesis: for z1, z2 being Element of X st z1,z2 are_commutative holds z1 * (exp z2) = (exp z2) * z1 let z1, z2 be Element of X; ::_thesis: ( z1,z2 are_commutative implies z1 * (exp z2) = (exp z2) * z1 ) assume A1: z1,z2 are_commutative ; ::_thesis: z1 * (exp z2) = (exp z2) * z1 now__::_thesis:_for_n_being_Element_of_NAT_holds_(z1_*_(z2_ExpSeq))_._n_=_((z2_ExpSeq)_*_z1)_._n let n be Element of NAT ; ::_thesis: (z1 * (z2 ExpSeq)) . n = ((z2 ExpSeq) * z1) . n thus (z1 * (z2 ExpSeq)) . n = z1 * ((z2 ExpSeq) . n) by CLOPBAN3:def_4 .= z1 * ((1r / (n !)) * (z2 #N n)) by Def1 .= (1r / (n !)) * (z1 * (z2 #N n)) by CLOPBAN3:38 .= (1r / (n !)) * ((z2 #N n) * z1) by A1, Lm2 .= ((1r / (n !)) * (z2 #N n)) * z1 by CLOPBAN3:38 .= ((z2 ExpSeq) . n) * z1 by Def1 .= ((z2 ExpSeq) * z1) . n by CLOPBAN3:def_5 ; ::_thesis: verum end; then A2: z1 * (z2 ExpSeq) = (z2 ExpSeq) * z1 by FUNCT_2:63; A3: Partial_Sums (z2 ExpSeq) is convergent by CLOPBAN3:def_1; thus z1 * (exp z2) = z1 * (Sum (z2 ExpSeq)) by Def6 .= z1 * (lim (Partial_Sums (z2 ExpSeq))) by CLOPBAN3:def_2 .= lim (z1 * (Partial_Sums (z2 ExpSeq))) by A3, Th6 .= lim (Partial_Sums (z1 * (z2 ExpSeq))) by Th9 .= lim ((Partial_Sums (z2 ExpSeq)) * z1) by A2, Th9 .= (lim (Partial_Sums (z2 ExpSeq))) * z1 by A3, Th7 .= (Sum (z2 ExpSeq)) * z1 by CLOPBAN3:def_2 .= (exp z2) * z1 by Def6 ; ::_thesis: verum end; theorem Th36: :: CLOPBAN4:36 for X being Complex_Banach_Algebra holds exp (0. X) = 1. X proof let X be Complex_Banach_Algebra; ::_thesis: exp (0. X) = 1. X exp (0. X) = Sum ((0. X) ExpSeq) by Def6 .= 1. X by Th19 ; hence exp (0. X) = 1. X ; ::_thesis: verum end; theorem Th37: :: CLOPBAN4:37 for X being Complex_Banach_Algebra for z being Element of X holds ( (exp z) * (exp (- z)) = 1. X & (exp (- z)) * (exp z) = 1. X ) proof let X be Complex_Banach_Algebra; ::_thesis: for z being Element of X holds ( (exp z) * (exp (- z)) = 1. X & (exp (- z)) * (exp z) = 1. X ) let z be Element of X; ::_thesis: ( (exp z) * (exp (- z)) = 1. X & (exp (- z)) * (exp z) = 1. X ) z * (- z) = z * ((- 1r) * z) by CLOPBAN3:38 .= (- 1r) * (z * z) by CLOPBAN3:38 .= ((- 1r) * z) * z by CLOPBAN3:38 .= (- z) * z by CLOPBAN3:38 ; then A1: z, - z are_commutative by LOPBAN_4:def_1; hence (exp z) * (exp (- z)) = exp (z + (- z)) by Th34 .= exp (0. X) by RLVECT_1:5 .= 1. X by Th36 ; ::_thesis: (exp (- z)) * (exp z) = 1. X thus (exp (- z)) * (exp z) = exp ((- z) + z) by A1, Th34 .= exp (0. X) by RLVECT_1:5 .= 1. X by Th36 ; ::_thesis: verum end; theorem :: CLOPBAN4:38 for X being Complex_Banach_Algebra for z being Element of X holds ( exp z is invertible & (exp z) " = exp (- z) & exp (- z) is invertible & (exp (- z)) " = exp z ) proof let X be Complex_Banach_Algebra; ::_thesis: for z being Element of X holds ( exp z is invertible & (exp z) " = exp (- z) & exp (- z) is invertible & (exp (- z)) " = exp z ) let z be Element of X; ::_thesis: ( exp z is invertible & (exp z) " = exp (- z) & exp (- z) is invertible & (exp (- z)) " = exp z ) A1: (exp (- z)) * (exp z) = 1. X by Th37; A2: (exp z) * (exp (- z)) = 1. X by Th37; hence exp z is invertible by A1, LOPBAN_3:def_4; ::_thesis: ( (exp z) " = exp (- z) & exp (- z) is invertible & (exp (- z)) " = exp z ) hence (exp z) " = exp (- z) by A2, A1, LOPBAN_3:def_8; ::_thesis: ( exp (- z) is invertible & (exp (- z)) " = exp z ) thus exp (- z) is invertible by A2, A1, LOPBAN_3:def_4; ::_thesis: (exp (- z)) " = exp z hence (exp (- z)) " = exp z by A2, A1, LOPBAN_3:def_8; ::_thesis: verum end; theorem Th39: :: CLOPBAN4:39 for X being Complex_Banach_Algebra for z being Element of X for s, t being Complex holds s * z,t * z are_commutative proof let X be Complex_Banach_Algebra; ::_thesis: for z being Element of X for s, t being Complex holds s * z,t * z are_commutative let z be Element of X; ::_thesis: for s, t being Complex holds s * z,t * z are_commutative let s, t be Complex; ::_thesis: s * z,t * z are_commutative A1: ( s in COMPLEX & t in COMPLEX ) by XCMPLX_0:def_2; then (s * z) * (t * z) = (s * t) * (z * z) by CLOPBAN3:38 .= (t * z) * (s * z) by A1, CLOPBAN3:38 ; hence s * z,t * z are_commutative by LOPBAN_4:def_1; ::_thesis: verum end; theorem :: CLOPBAN4:40 for X being Complex_Banach_Algebra for z being Element of X for s, t being Complex holds ( (exp (s * z)) * (exp (t * z)) = exp ((s + t) * z) & (exp (t * z)) * (exp (s * z)) = exp ((t + s) * z) & exp ((s + t) * z) = exp ((t + s) * z) & exp (s * z), exp (t * z) are_commutative ) proof let X be Complex_Banach_Algebra; ::_thesis: for z being Element of X for s, t being Complex holds ( (exp (s * z)) * (exp (t * z)) = exp ((s + t) * z) & (exp (t * z)) * (exp (s * z)) = exp ((t + s) * z) & exp ((s + t) * z) = exp ((t + s) * z) & exp (s * z), exp (t * z) are_commutative ) let z be Element of X; ::_thesis: for s, t being Complex holds ( (exp (s * z)) * (exp (t * z)) = exp ((s + t) * z) & (exp (t * z)) * (exp (s * z)) = exp ((t + s) * z) & exp ((s + t) * z) = exp ((t + s) * z) & exp (s * z), exp (t * z) are_commutative ) let s, t be Complex; ::_thesis: ( (exp (s * z)) * (exp (t * z)) = exp ((s + t) * z) & (exp (t * z)) * (exp (s * z)) = exp ((t + s) * z) & exp ((s + t) * z) = exp ((t + s) * z) & exp (s * z), exp (t * z) are_commutative ) A1: ( s in COMPLEX & t in COMPLEX ) by XCMPLX_0:def_2; A2: s * z,t * z are_commutative by Th39; hence A3: (exp (s * z)) * (exp (t * z)) = exp ((s * z) + (t * z)) by Th34 .= exp ((s + t) * z) by A1, CLOPBAN3:38 ; ::_thesis: ( (exp (t * z)) * (exp (s * z)) = exp ((t + s) * z) & exp ((s + t) * z) = exp ((t + s) * z) & exp (s * z), exp (t * z) are_commutative ) thus A4: (exp (t * z)) * (exp (s * z)) = exp ((t * z) + (s * z)) by A2, Th34 .= exp ((t + s) * z) by A1, CLOPBAN3:38 ; ::_thesis: ( exp ((s + t) * z) = exp ((t + s) * z) & exp (s * z), exp (t * z) are_commutative ) thus exp ((s + t) * z) = exp ((t + s) * z) ; ::_thesis: exp (s * z), exp (t * z) are_commutative thus exp (s * z), exp (t * z) are_commutative by A3, A4, LOPBAN_4:def_1; ::_thesis: verum end;