:: CLOPBAN4 semantic presentation  Show TPTP formulae Show IDV graph for whole article:: Showing IDV graph ... (Click the Palm Trees again to close it)

definition
let X be non empty Normed_Complex_AlgebraStr ;
let x, y be Element of X;
pred x,y are_commutative means :Def1: :: CLOPBAN4:def 1
x * y = y * x;
symmetry
for x, y being Element of X st x * y = y * x holds
y * x = x * y
;
end;

:: deftheorem Def1 defines are_commutative CLOPBAN4:def 1 :
for X being non empty Normed_Complex_AlgebraStr
for x, y being Element of X holds
( x,y are_commutative iff x * y = y * x );

Lm1: for X being Complex_Banach_Algebra
for z being Element of X
for n being 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 end;

Lm2: for X being Complex_Banach_Algebra
for n being 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 end;

theorem Th1: :: CLOPBAN4:1  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 end;

theorem Th2: :: CLOPBAN4:2  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being Complex_Banach_Algebra
for s being sequence of X
for z being Element of X st ( for n being Nat holds s . n = z ) holds
lim s = z
proof end;

theorem Th3: :: CLOPBAN4:3  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being Complex_Banach_Algebra
for s, s' being sequence of X st s is convergent & s' is convergent holds
s * s' is convergent
proof end;

theorem Th4: :: CLOPBAN4:4  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 end;

theorem Th5: :: CLOPBAN4:5  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 end;

theorem Th6: :: CLOPBAN4:6  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 end;

theorem Th7: :: CLOPBAN4:7  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 end;

theorem Th8: :: CLOPBAN4:8  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being Complex_Banach_Algebra
for s, s' being sequence of X st s is convergent & s' is convergent holds
lim (s * s') = (lim s) * (lim s')
proof end;

theorem Th9: :: CLOPBAN4:9  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 end;

theorem Th10: :: CLOPBAN4:10  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being Complex_Banach_Algebra
for k being Nat
for seq being sequence of X holds ||.((Partial_Sums seq) . k).|| <= (Partial_Sums ||.seq.||) . k
proof end;

theorem Th11: :: CLOPBAN4:11  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being Complex_Banach_Algebra
for m being Nat
for seq1, seq2 being sequence of X st ( for n being Nat st n <= m holds
seq1 . n = seq2 . n ) holds
(Partial_Sums seq1) . m = (Partial_Sums seq2) . m
proof end;

theorem Th12: :: CLOPBAN4:12  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being Complex_Banach_Algebra
for seq being sequence of X
for rseq being Real_Sequence st ( for n being Nat holds ||.(seq . n).|| <= rseq . n ) & rseq is convergent & lim rseq = 0 holds
( seq is convergent & lim seq = 0. X )
proof end;

definition
let X be Complex_Banach_Algebra;
let z be Element of X;
func z ExpSeq -> sequence of X means :Def2: :: CLOPBAN4:def 2
for n being Nat holds it . n = (1r / (n !c )) * (z #N n);
existence
ex b1 being sequence of X st
for n being Nat holds b1 . n = (1r / (n !c )) * (z #N n)
proof end;
uniqueness
for b1, b2 being sequence of X st ( for n being Nat holds b1 . n = (1r / (n !c )) * (z #N n) ) & ( for n being Nat holds b2 . n = (1r / (n !c )) * (z #N n) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def2 defines ExpSeq CLOPBAN4:def 2 :
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 Nat holds b3 . n = (1r / (n !c )) * (z #N n) );

scheme :: CLOPBAN4:sch 1
ExNormSpaceCASE{ F1() -> non empty Complex_Banach_Algebra, F2( Nat, Nat) -> Point of F1() } :
for k being Nat ex seq being sequence of F1() st
for n being Nat holds
( ( n <= k implies seq . n = F2(k,n) ) & ( n > k implies seq . n = 0. F1() ) )
proof end;

definition
let X be Complex_Banach_Algebra;
let seq be sequence of X;
func Sift seq -> sequence of X means :Def3: :: CLOPBAN4:def 3
( it . 0 = 0. X & ( for k being Nat holds it . (k + 1) = seq . k ) );
existence
ex b1 being sequence of X st
( b1 . 0 = 0. X & ( for k being Nat holds b1 . (k + 1) = seq . k ) )
proof end;
uniqueness
for b1, b2 being sequence of X st b1 . 0 = 0. X & ( for k being Nat holds b1 . (k + 1) = seq . k ) & b2 . 0 = 0. X & ( for k being Nat holds b2 . (k + 1) = seq . k ) holds
b1 = b2
proof end;
end;

:: deftheorem Def3 defines Sift CLOPBAN4:def 3 :
for X being Complex_Banach_Algebra
for seq, b3 being sequence of X holds
( b3 = Sift seq iff ( b3 . 0 = 0. X & ( for k being Nat holds b3 . (k + 1) = seq . k ) ) );

definition
let n be Nat;
let X be Complex_Banach_Algebra;
let z, w be Element of X;
func Expan n,z,w -> sequence of X means :Def4: :: CLOPBAN4:def 4
for k being 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 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 end;
uniqueness
for b1, b2 being sequence of X st ( for k being 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 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 end;
end;

:: deftheorem Def4 defines Expan CLOPBAN4:def 4 :
for n being 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 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 Nat;
let X be Complex_Banach_Algebra;
let z, w be Element of X;
func Expan_e n,z,w -> sequence of X means :Def5: :: CLOPBAN4:def 5
for k being 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 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 end;
uniqueness
for b1, b2 being sequence of X st ( for k being 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 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 end;
end;

:: deftheorem Def5 defines Expan_e CLOPBAN4:def 5 :
for n being 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 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 Nat;
let X be Complex_Banach_Algebra;
let z, w be Element of X;
func Alfa n,z,w -> sequence of X means :Def6: :: CLOPBAN4:def 6
for k being 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 Nat holds
( ( k <= n implies b1 . k = ((z ExpSeq ) . k) * ((Partial_Sums (w ExpSeq )) . (n -' k)) ) & ( n < k implies b1 . k = 0. X ) )
proof end;
uniqueness
for b1, b2 being sequence of X st ( for k being 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 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 end;
end;

:: deftheorem Def6 defines Alfa CLOPBAN4:def 6 :
for n being 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 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 Nat;
func Conj n,z,w -> sequence of X means :Def7: :: CLOPBAN4:def 7
for k being 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 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 end;
uniqueness
for b1, b2 being sequence of X st ( for k being 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 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 end;
end;

:: deftheorem Def7 defines Conj CLOPBAN4:def 7 :
for X being Complex_Banach_Algebra
for z, w being Element of X
for n being Nat
for b5 being sequence of X holds
( b5 = Conj n,z,w iff for k being 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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being Complex_Banach_Algebra
for z being Element of X
for n being Nat holds
( (z ExpSeq ) . (n + 1) = ((1r / [*(n + 1),0*]) * z) * ((z ExpSeq ) . n) & (z ExpSeq ) . 0 = 1. X & ||.((z ExpSeq ) . n).|| <= (||.z.|| ExpSeq ) . n )
proof end;

theorem Th14: :: CLOPBAN4:14  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being Complex_Banach_Algebra
for k being Nat
for seq being sequence of X st 0 < k holds
(Sift seq) . k = seq . (k -' 1)
proof end;

theorem Th15: :: CLOPBAN4:15  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being Complex_Banach_Algebra
for k being Nat
for seq being sequence of X holds (Partial_Sums seq) . k = ((Partial_Sums (Sift seq)) . k) + (seq . k)
proof end;

theorem Th16: :: CLOPBAN4:16  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being Complex_Banach_Algebra
for n being Nat
for z, w being Element of X st z,w are_commutative holds
(z + w) #N n = (Partial_Sums (Expan n,z,w)) . n
proof end;

theorem Th17: :: CLOPBAN4:17  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being Complex_Banach_Algebra
for z, w being Element of X
for n being Nat holds Expan_e n,z,w = (1r / (n !c )) * (Expan n,z,w)
proof end;

theorem Th18: :: CLOPBAN4:18  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being Complex_Banach_Algebra
for n being Nat
for z, w being Element of X st z,w are_commutative holds
(1r / (n !c )) * ((z + w) #N n) = (Partial_Sums (Expan_e n,z,w)) . n
proof end;

theorem Th19: :: CLOPBAN4:19  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being Complex_Banach_Algebra holds
( (0. X) ExpSeq is norm_summable & Sum ((0. X) ExpSeq ) = 1. X )
proof end;

registration
let X be Complex_Banach_Algebra;
let z be Element of X;
cluster z ExpSeq -> norm_summable ;
coherence
z ExpSeq is norm_summable
proof end;
end;

theorem Th20: :: CLOPBAN4:20  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 end;

theorem Th21: :: CLOPBAN4:21  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being Complex_Banach_Algebra
for z, w being Element of X
for l, k being Nat st l <= k holds
(Alfa (k + 1),z,w) . l = ((Alfa k,z,w) . l) + ((Expan_e (k + 1),z,w) . l)
proof end;

theorem Th22: :: CLOPBAN4:22  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being Complex_Banach_Algebra
for z, w being Element of X
for k being 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 end;

theorem Th23: :: CLOPBAN4:23  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being Complex_Banach_Algebra
for z, w being Element of X
for k being Nat holds (z ExpSeq ) . k = (Expan_e k,z,w) . k
proof end;

theorem Th24: :: CLOPBAN4:24  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being Complex_Banach_Algebra
for n being 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 end;

theorem Th25: :: CLOPBAN4:25  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being Complex_Banach_Algebra
for k being 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 end;

theorem Th26: :: CLOPBAN4:26  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being Complex_Banach_Algebra
for z being Element of X
for n being Nat holds 0 <= (||.z.|| ExpSeq ) . n
proof end;

theorem Th27: :: CLOPBAN4:27  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being Complex_Banach_Algebra
for z being Element of X
for k being Nat holds
( ||.((Partial_Sums (z ExpSeq )) . k).|| <= (Partial_Sums (||.z.|| ExpSeq )) . k & (Partial_Sums (||.z.|| ExpSeq )) . k <= Sum (||.z.|| ExpSeq ) & ||.((Partial_Sums (z ExpSeq )) . k).|| <= Sum (||.z.|| ExpSeq ) )
proof end;

theorem Th28: :: CLOPBAN4:28  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being Complex_Banach_Algebra
for z being Element of X holds 1 <= Sum (||.z.|| ExpSeq )
proof end;

theorem Th29: :: CLOPBAN4:29  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being Complex_Banach_Algebra
for z being Element of X
for n, m being Nat holds
( abs ((Partial_Sums (||.z.|| ExpSeq )) . n) = (Partial_Sums (||.z.|| ExpSeq )) . n & ( n <= m implies abs (((Partial_Sums (||.z.|| ExpSeq )) . m) - ((Partial_Sums (||.z.|| ExpSeq )) . n)) = ((Partial_Sums (||.z.|| ExpSeq )) . m) - ((Partial_Sums (||.z.|| ExpSeq )) . n) ) )
proof end;

theorem Th30: :: CLOPBAN4:30  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being Complex_Banach_Algebra
for z, w being Element of X
for k, n being Nat holds abs ((Partial_Sums ||.(Conj k,z,w).||) . n) = (Partial_Sums ||.(Conj k,z,w).||) . n
proof end;

theorem Th31: :: CLOPBAN4:31  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 Nat st
for k being Nat st n <= k holds
abs ((Partial_Sums ||.(Conj k,z,w).||) . k) < p
proof end;

theorem Th32: :: CLOPBAN4:32  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being Complex_Banach_Algebra
for z, w being Element of X
for seq being sequence of X st ( for k being Nat holds seq . k = (Partial_Sums (Conj k,z,w)) . k ) holds
( seq is convergent & lim seq = 0. X )
proof 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 end;

definition
let X be Complex_Banach_Algebra;
func exp_ X -> Function of the carrier of X,the carrier of X means :Def8: :: CLOPBAN4:def 8
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 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 end;
end;

:: deftheorem Def8 defines exp_ CLOPBAN4:def 8 :
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 9
(exp_ X) . z;
correctness
coherence
(exp_ X) . z is Element of X
;
;
end;

:: deftheorem defines exp CLOPBAN4:def 9 :
for X being Complex_Banach_Algebra
for z being Element of X holds exp z = (exp_ X) . z;

theorem Th33: :: CLOPBAN4:33  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being Complex_Banach_Algebra
for z being Element of X holds exp z = Sum (z ExpSeq ) by Def8;

theorem Th34: :: CLOPBAN4:34  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 end;

theorem :: CLOPBAN4:35  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 end;

theorem Th36: :: CLOPBAN4:36  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being Complex_Banach_Algebra holds exp (0. X) = 1. X
proof end;

theorem Th37: :: CLOPBAN4:37  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 end;

theorem :: CLOPBAN4:38  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 end;

theorem Th39: :: CLOPBAN4:39  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 end;

theorem :: CLOPBAN4:40  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 end;