Copyright (c) 1998 Association of Mizar Users
environ
vocabulary ARYTM, COMPLEX1, COMSEQ_1, SEQ_1, FDIFF_1, ARYTM_3, ARYTM_1,
FUNCT_1, RELAT_1, QC_LANG1, PREPOWER, SERIES_1, ABSVALUE, RLVECT_1,
SEQM_3, SEQ_2, SUPINF_2, ORDINAL2, PROB_1, SQUARE_1, PARTFUN1, INCSP_1,
RCOMP_1, PRE_TOPC, BOOLE, FCONT_1, SUBSET_1, SIN_COS, FINSEQ_4, GROUP_1;
notation TARSKI, XBOOLE_0, SUBSET_1, ORDINAL1, NUMBERS, ARYTM_0, XCMPLX_0,
XREAL_0, REAL_1, FUNCT_1, FCONT_1, FUNCT_2, SEQ_1, SEQ_2, FDIFF_1,
RELAT_1, SERIES_1, ABSVALUE, NAT_1, FINSEQ_4, NEWTON, COMPLEX1, SQUARE_1,
PREPOWER, PARTFUN1, SEQM_3, RCOMP_1, BINARITH, RFUNCT_1, RFUNCT_2,
COMSEQ_1, COMSEQ_2, COMSEQ_3;
constructors COMSEQ_3, REAL_1, SEQ_2, RCOMP_1, FINSEQ_4, FCONT_1, RFUNCT_1,
FDIFF_1, SQUARE_1, COMSEQ_1, COMSEQ_2, PREPOWER, SERIES_1, PARTFUN1,
BINARITH, RFUNCT_2, COMPLEX1, MEMBERED, ARYTM_0, ARYTM_3, FUNCT_4;
clusters INT_1, COMSEQ_2, COMSEQ_3, XREAL_0, RELSET_1, FDIFF_1, RCOMP_1,
SEQ_1, COMSEQ_1, SEQM_3, NEWTON, COMPLEX1, MEMBERED, ORDINAL2, NUMBERS;
requirements REAL, NUMERALS, SUBSET, BOOLE, ARITHM;
definitions COMSEQ_3;
theorems AXIOMS, NAT_1, REAL_1, ABSVALUE, REAL_2, INT_1, SEQ_1, SEQ_2,
SERIES_1, SEQM_3, SEQ_4, PREPOWER, COMPLEX1, COMSEQ_1, COMSEQ_2,
SQUARE_1, COMSEQ_3, FCONT_2, FINSEQ_4, RCOMP_1, FUNCT_1, FDIFF_1,
FDIFF_2, FCONT_1, FCONT_3, TARSKI, FUNCT_2, RFUNCT_1, SUBSET_1, RFUNCT_2,
RELSET_1, POWER, PARTFUN1, ROLLE, NEWTON, RELAT_1, XREAL_0, JORDAN6,
TOPREAL5, SCMFSA_7, GOBOARD9, XBOOLE_0, XBOOLE_1, XCMPLX_0, XCMPLX_1,
ARYTM_0;
schemes NAT_1, SEQ_1, COMSEQ_1, RECDEF_1, FUNCT_1, PARTFUN2, COMPLSP1;
begin
reserve p,q,th,th1,th2,th3,r for Real,
w,z,z1,z2 for Element of COMPLEX,
k,l,m,n,n1,n2 for Nat,
seq,seq1,seq2,cq1 for Complex_Sequence,
rseq,rseq1,rseq2 for Real_Sequence,
rr for set,
hy1 for convergent_to_0 Real_Sequence;
Lm1:
(for x, y be real number st x <y holds
(for a be real number st a>0 holds
(a * x < a * y & x/a < y/a)) ) &
(for x, y be real number st x < y & 0 < x holds 1 < y/x)
proof
now let x, y be real number such that
A1: x <y;
let a be real number; assume a>0;
hence a * x < a * y & x/a < y/a by A1,REAL_1:70,73;
end;
hence thesis by REAL_2:142;
end;
Lm2:now let n;
0 <= n by NAT_1:18;
hence 0 < n+1 by NAT_1:38;
end;
::Some definitions and properties of complex sequence
definition let m,k be Nat;
canceled;
func CHK(m,k) -> Element of COMPLEX equals :Def2:
1r if m <= k otherwise 0c;
correctness;
func RHK(m,k) equals :Def3:
1 if m <= k otherwise 0;
correctness;
end;
definition let m,k be Nat;
cluster RHK(m,k) -> real;
coherence
proof
m <= k or m > k;
hence thesis by Def3;
end;
end;
definition let m,k be Nat;
redefine func RHK(m,k) -> Real;
coherence by XREAL_0:def 1;
end;
scheme ExComplex_CASE{F(Nat,Nat)->Element of COMPLEX}:
for k holds
ex seq st for n holds ((n <= k implies seq.n=F(k,n)) &
(n > k implies seq.n=0c))
proof
let k;
defpred P[set,set] means ex n st (n=$1 &
(n <= k implies $2=F(k,n )) &
(n > k implies $2=0c) );
A1: now let x be set;
assume x in NAT;
then consider n such that
A2: n=x;
A3: now
assume n <= k;
hence CHK(n,k) * F (k,n) =1r * F(k,n) by Def2
.=F(k,n) by COMPLEX1:29;
end;
A4: now assume n > k;
hence CHK(n,k) * F (k,n) =0c * F(k,n) by Def2
.=0c by COMPLEX1:28;
end;
reconsider y=CHK(n,k) * F (k,n) as set;
take y;
thus P[x,y] by A2,A3,A4;
end;
A5: for x,y,z be set st x in NAT & P[x,y] & P[x,z] holds y=z;
consider f be Function such that
A6: dom f =NAT and
A7: for x be set st x in NAT holds P[x,f.x] from FuncEx(A5,A1);
now let x be set;
assume x in NAT;
then ex n st (n=x & (n <= k implies f.x=F(k,n)) &
(n > k implies f.x=0c)) by A7;
hence f.x is Element of COMPLEX;
end;
then reconsider f as Complex_Sequence by A6,COMSEQ_1:1;
take seq=f;
let n;
ex l be Nat st l=n &
(l <= k implies seq.n=F(k,l)) & (l > k implies seq.n=0c) by A7;
hence ((n <= k implies seq.n=F(k,n)) & (n > k implies seq.n=0c));
end;
scheme ExReal_CASE{F(Nat,Nat)->real number}:
for k holds
ex rseq st for n holds ((n <= k implies rseq.n=F(k,n)) &
(n > k implies rseq.n=0))
proof
let k;
defpred P[set,set] means ex n st (n=$1 &
(n <= k implies $2=F(k,n )) &
(n > k implies $2=0) );
A1: now let x be set;
assume x in NAT;
then consider n such that
A2: n=x;
A3: now
assume n <= k;
hence RHK(n,k ) * F (k,n) =1 * F(k,n) by Def3
.=F(k,n);
end;
A4: now assume n > k;
hence RHK(n,k) * F (k,n) =0 * F(k,n) by Def3
.=0;
end;
reconsider y=RHK(n,k) * F (k,n) as set;
take y;
thus P[x,y] by A2,A3,A4;
end;
A5: for x,y,z be set st x in NAT & P[x,y] & P[x,z] holds y=z;
consider f be Function such that
A6: dom f =NAT and
A7: for x be set st x in NAT holds P[x,f.x] from FuncEx(A5,A1);
now let x be set;
assume x in NAT;
then ex n st (n=x & (n <= k implies f.x=F(k,n)) &
(n > k implies f.x=0)) by A7;
hence f.x is real;
end;
then reconsider f as Real_Sequence by A6,SEQ_1:3;
take rseq=f;
let n;
ex l be Nat st l=n &
(l <= k implies rseq.n=F(k,l)) & (l > k implies rseq.n=0) by A7;
hence ((n <= k implies rseq.n=F(k,n)) & (n > k implies rseq.n=0));
end;
definition
func Prod_complex_n -> Complex_Sequence means :Def4:
it.0 = 1r & for n holds it.(n+1) = it.n * [*(n+1),0*];
existence
proof deffunc U(Nat,Element of COMPLEX) = $2 * [*$1+1,0*];
consider f being Function of NAT,COMPLEX such that
A1: f.0 = 1r & for n being Nat holds f.(n+1) = U(n,f.n) from LambdaRecExD;
reconsider f as Complex_Sequence;
take f;
thus thesis by A1;
end;
uniqueness
proof
let seq1,seq2;
assume that A2: seq1.0=1r & for n holds
seq1.(n+1)=seq1.n * [*(n+1),0*] and
A3: seq2.0=1r & for n holds
seq2.(n+1)=seq2.n * [*(n+1),0*];
defpred X[Nat] means seq1.$1 = seq2.$1;
A4: X[0] by A2,A3;
A5: for k be Nat st X[k] holds X[k+1]
proof let k be Nat;
assume seq1.k =seq2.k;
hence seq1.(k+1) = seq2.k * [*(k+1),0*] by A2
.= seq2.(k+1) by A3;
end;
for n holds X[n] from Ind(A4,A5);
hence seq1 = seq2 by COMSEQ_1:6;
end;
end;
definition
func Prod_real_n -> Real_Sequence means :Def5:
it.0 = 1 & for n holds it.(n+1) = it.n * (n+1);
existence
proof deffunc U(Nat,Element of REAL) = $2 * ($1+1);
consider f being Function of NAT,REAL such that
A1: f.0 = 1 & for n being Nat holds f.(n+1) = U(n,f.n) from LambdaRecExD;
reconsider f as Real_Sequence;
take f;
thus thesis by A1;
end;
uniqueness
proof
let rseq1,rseq2;
assume that A2: rseq1.0=1 & for n holds
rseq1.(n+1)=rseq1.n * (n+1) and
A3: rseq2.0=1 & for n holds
rseq2.(n+1)=rseq2.n * (n+1);
defpred X[Nat] means rseq1.$1 = rseq2.$1;
A4: X[0] by A2,A3;
A5: for k be Nat st X[k] holds X[k+1]
proof let k be Nat;
assume rseq1.k =rseq2.k;
hence rseq1.(k+1) = rseq2.k * (k+1) by A2
.= rseq2.(k+1) by A3;
end;
for n holds X[n] from Ind(A4,A5);
hence rseq1 = rseq2 by FUNCT_2:113;
end;
end;
definition let n be Nat;
func n !c -> Element of COMPLEX equals :Def6:
Prod_complex_n.n;
correctness;
end;
definition let n be Nat;
redefine func n! -> Real equals :Def7:
Prod_real_n.n;
coherence by XREAL_0:def 1;
compatibility
proof
defpred X[Nat] means Prod_real_n.$1 = $1!;
A1: X[0] by Def5,NEWTON:18;
A2: now let l be Nat;
assume A3: X[l];
Prod_real_n.(l+1) = Prod_real_n.l * (l+1) by Def5
.= (l+1)! by A3,NEWTON:21;
hence X[l+1];
end;
for k be Nat holds X[k] from Ind(A1,A2);
hence thesis;
end;
end;
definition let z be Element of COMPLEX;
deffunc U(Nat) = z #N $1 /($1!c);
func z ExpSeq -> Complex_Sequence means :Def8:
for n holds it.n = z #N n /(n!c);
existence
proof
thus ex s being Complex_Sequence st
for n holds s.n = U(n) from ExComplexSeq;
end;
uniqueness
proof
thus for s1,s2 being Complex_Sequence st
(for x being Nat holds s1.x = U(x)) &
(for x being Nat holds s2.x = U(x)) holds s1 = s2
from FuncDefUniq;
end;
end;
definition let a be real number;
deffunc U(Nat) = a |^ $1 /($1!);
func a ExpSeq -> Real_Sequence means :Def9:
for n holds it.n = a |^ n /(n!);
existence
proof
thus ex s being Real_Sequence st
for n holds s.n = U(n) from ExRealSeq;
end;
uniqueness
proof
thus for s1,s2 being Real_Sequence st
(for x being Nat holds s1.x = U(x)) &
(for x being Nat holds s2.x = U(x)) holds s1 = s2
from FuncDefUniq;
end;
end;
theorem Th1:
(0 < n implies [*n,0*] <> 0c) &
0!c = 1r &
n!c <> 0c &
(n+1)!c = n!c * [*n+1,0*]
proof
thus 0 < n implies [*n,0*] <> 0c
proof
assume
A1:0 <n;
assume
[*n,0*] = 0c;
hence contradiction by A1,COMPLEX1:7,12;
end;
defpred X[Nat] means $1!c <> 0c;
thus 0!c = Prod_complex_n.0 by Def6
.= 1r by Def4;
then A2: X[0] by COMPLEX1:133,134;
A3: now let n;
assume
A4: X[n];
A5: (n+1)!c = Prod_complex_n.(n+1) by Def6
.= Prod_complex_n.n * [*n+1,0*] by Def4
.= n!c * [*n+1,0*] by Def6;
[*n+1,0*] <> 0c by COMSEQ_3:1;
hence X[n+1] by A4,A5,XCMPLX_1:6;
end;
for n holds X[n] from Ind(A2,A3);
hence n!c <> 0c;
thus (n+1)!c = Prod_complex_n.(n+1) by Def6
.= Prod_complex_n.n * [*n+1,0*] by Def4
.= n!c * [*n+1,0*] by Def6;
end;
theorem
n! <> 0 & (n+1)! = n! * (n+1) by NEWTON:21,23;
theorem Th3:
(for k st 0 < k holds ((k-'1)!c ) * [*k,0*] = k!c) &
for m,k st k <= m holds ((m-'k)!c ) * [*(m+1-k),0*] = (m+1-'k)!c
proof
A1: now let k; assume 0 < k;
then 0+1 <= k by INT_1:20;
then k-'1+1=k-1+1 by SCMFSA_7:3
.=k by XCMPLX_1:27;
hence k!c =(k-'1)!c * [*k,0*] by Th1;
end;
now
let m,k such that
A2: k <= m;
m <= m+1 by REAL_1:69;
then k <= m+1 by A2,AXIOMS:22;
then m+1-'k=m+1-k by SCMFSA_7:3
.=m-k+1 by XCMPLX_1:29
.=m-'k+1 by A2,SCMFSA_7:3;
hence (m+1-'k)!c=((m-'k)!c ) * [*(m-'k)+1,0*] by Th1
.=((m-'k)!c ) * [*m-k+1,0*] by A2,SCMFSA_7:3
.=((m-'k)!c ) * [*m+1-k,0*] by XCMPLX_1:29;
end;
hence thesis by A1;
end;
definition
let n be Nat;
func Coef(n) -> Complex_Sequence means :Def10:
for k be Nat holds
(k <= n implies it.k = n!c /( (k!c ) * ((n-'k)!c )))
&(k > n implies it.k=0c);
existence
proof
deffunc U(Nat,Nat) = $1!c /( ($2!c ) * (($1-'$2)!c));
for n holds ex seq st for k holds
(k <= n implies seq.k = U(n,k)) &
(k > n implies seq.k=0c ) from ExComplex_CASE;
hence ex seq st for k holds
(k <= n implies seq.k = n!c /( (k!c ) * ((n-'k)!c))) &
(k > n implies seq.k=0c);
end;
uniqueness
proof
let seq1,seq2;
assume that
A1: for k holds (k <= n implies seq1.k = n!c /( (k!c ) * ((n-'k)!c))) &
(k > n implies seq1.k=0c) and
A2: for k holds (k <= n implies seq2.k = n!c /( (k!c ) * ((n-'k)!c))) &
(k > n implies seq2.k=0c);
now let k;
per cases;
suppose A3:k <= n;
hence seq1.k = n!c /( (k!c ) * ((n-'k)!c)) by A1
.= seq2.k by A2,A3;
suppose A4:k > n;
hence seq1.k = 0c by A1
.= seq2.k by A2,A4;
end;
hence seq1=seq2 by COMSEQ_1:6;
end;
end;
definition let n be Nat;
func Coef_e(n) -> Complex_Sequence means :Def11:
for k be Nat holds
(k <= n implies it.k = 1r/((k!c ) * ((n-'k)!c )))
& (k > n implies it.k=0c);
existence
proof
deffunc U(Nat,Nat) = 1r/(($2!c ) * (($1-'$2)!c ));
for n holds ex seq st for k holds
(k <= n implies seq.k = U(n,k)) &
(k > n implies seq.k=0c) from ExComplex_CASE;
hence ex seq st for k holds
(k <= n implies seq.k = 1r/((k!c ) * ((n-'k)!c ))) &
(k > n implies seq.k=0c);
end;
uniqueness
proof
let seq1,seq2;
assume that
A1:for k holds
(k <= n implies seq1.k = 1r/((k!c ) * ((n-'k)!c ))) &
(k > n implies seq1.k=0c) and
A2: for k holds
(k <= n implies seq2.k = 1r/((k!c ) * ((n-'k)!c ))) &
(k > n implies seq2.k=0c);
now let k;
per cases;
suppose A3:k <= n;
hence seq1.k =1r/((k!c ) * ((n-'k)!c )) by A1
.= seq2.k by A2,A3;
suppose A4:k > n;
hence seq1.k = 0c by A1
.= seq2.k by A2,A4;
end;
hence seq1=seq2 by COMSEQ_1:6;
end;
end;
definition let seq;
func Sift seq -> Complex_Sequence means :Def12:
it.0=0c & for k be Nat holds it.(k+1) = seq.k;
existence
proof deffunc U(Nat,Element of COMPLEX) = seq.$1;
consider f being Function of NAT,COMPLEX such that
A1: f.0 = 0c & for n being Nat holds f.(n+1)=U(n,f.n) from LambdaRecExD;
reconsider f as Complex_Sequence;
take f;
thus thesis by A1;
end;
uniqueness
proof
let seq1,seq2;
assume that A2: seq1.0=0c & for n holds
seq1.(n+1)=seq.n and
A3: seq2.0=0c & for n holds
seq2.(n+1)=seq.n;
defpred X[Nat] means seq1.$1 = seq2.$1;
A4: X[0] by A2,A3;
A5: for k be Nat st X[k] holds X[k+1]
proof let k be Nat;
assume seq1.k =seq2.k;
thus seq1.(k+1) = seq.k by A2
.= seq2.(k+1) by A3;
end;
for n holds X[n] from Ind(A4,A5);
hence seq1 = seq2 by COMSEQ_1:6;
end;
end;
definition let n;
let z,w be Element of COMPLEX;
func Expan(n,z,w) -> Complex_Sequence means :Def13:
for k be Nat holds
( k <= n implies
it.k=((Coef(n)).k) * (z #N k) * (w #N (n-'k)) ) &
(n < k implies it.k=0c);
existence
proof
deffunc U(Nat,Nat) = ((Coef($1)).$2) * (z #N $2) * (w #N ($1-'$2));
for n holds ex seq st for k holds
(k <= n implies seq.k = U(n,k)) &
(k > n implies seq.k=0c) from ExComplex_CASE;
hence ex seq st for k holds
(k <= n implies seq.k =((Coef(n)).k) * (z #N k) * (w #N (n-'k))) &
(k > n implies seq.k=0c);
end;
uniqueness
proof
let seq1,seq2;
assume that
A1:for k holds
(k <= n implies seq1.k =((Coef(n)).k) * (z #N k) * (w #N (n-'k)))&
(k > n implies seq1.k=0c) and
A2:for k holds
(k <= n implies seq2.k = ((Coef(n)).k) * (z #N k) * (w #N (n-'k)) )&
(k > n implies seq2.k=0c);
now let k;
per cases;
suppose A3:k <= n;
hence seq1.k =((Coef(n)).k) * (z #N k) * (w #N (n-'k)) by A1
.= seq2.k by A2,A3;
suppose A4:k > n;
hence seq1.k = 0c by A1
.= seq2.k by A2,A4;
end;
hence seq1=seq2 by COMSEQ_1:6;
end;
end;
definition let n;
let z,w be Element of COMPLEX;
func Expan_e(n,z,w) -> Complex_Sequence means :Def14:
for k be Nat holds
( k <= n implies
it.k=((Coef_e(n)).k) * (z #N k) * (w #N (n-'k)) ) &
(n < k implies it.k=0c);
existence
proof
deffunc U(Nat,Nat) = ((Coef_e($1)).$2) * (z #N $2) * (w #N ($1-'$2));
for n holds
ex seq st for k holds
(k <= n implies seq.k = U(n,k)) &
(k > n implies seq.k=0c) from ExComplex_CASE;
hence ex seq st for k holds
(k <= n implies seq.k =((Coef_e(n)).k) * (z #N k) * (w #N (n-'k)) ) &
(k > n implies seq.k=0c);
end;
uniqueness
proof
let seq1,seq2;
assume that A1: for k holds
(k <= n implies seq1.k =((Coef_e(n)).k) * (z #N k) * (w #N (n-'k)) ) &
(k > n implies seq1.k=0c) and
A2:for k holds
(k <= n implies seq2.k = ((Coef_e(n)).k) * (z #N k) * (w #N (n-'k)) ) &
(k > n implies seq2.k=0c);
now let k;
per cases;
suppose A3:k <= n;
hence seq1.k =((Coef_e(n)).k) * (z #N k) * (w #N (n-'k)) by A1
.= seq2.k by A2,A3;
suppose A4:k > n;
hence seq1.k = 0c by A1
.= seq2.k by A2,A4;
end;
hence seq1=seq2 by COMSEQ_1:6;
end;
end;
definition let n;
let z,w be Element of COMPLEX;
func Alfa(n,z,w) -> Complex_Sequence means :Def15:
for k be Nat holds
( k <= n implies
it.k= (z ExpSeq).k * Partial_Sums(w ExpSeq).(n-'k) ) &
( n < k implies it.k=0c);
existence
proof
deffunc U(Nat,Nat) = (z ExpSeq).$2 * Partial_Sums(w ExpSeq).($1-'$2);
for n holds
ex seq st for k holds
(k <= n implies seq.k = U(n,k)) &
(k > n implies seq.k=0c ) from ExComplex_CASE;
hence ex seq st for k holds
(k <= n implies seq.k =(z ExpSeq).k * Partial_Sums(w ExpSeq).(n-'k) ) &
(k > n implies seq.k=0c);
end;
uniqueness
proof
let seq1,seq2;
assume that
A1: for k holds
(k <= n implies seq1.k = (z ExpSeq).k * Partial_Sums(w ExpSeq).(n-'k) )
&
(k > n implies seq1.k=0c) and
A2: for k holds
(k <= n implies seq2.k = (z ExpSeq).k * Partial_Sums(w ExpSeq).(n-'k) )
& (k > n implies seq2.k=0c);
now let k;
per cases;
suppose A3:k <= n;
hence seq1.k = (z ExpSeq).k * Partial_Sums(w ExpSeq).(n-'k) by A1
.= seq2.k by A2,A3;
suppose A4:k > n;
hence seq1.k = 0c by A1
.= seq2.k by A2,A4;
end;
hence seq1=seq2 by COMSEQ_1:6;
end;
end;
definition
let a,b be real number;
let n be Nat;
func Conj(n,a,b) -> Real_Sequence means
for k be Nat holds
( k <= n implies
it.k= (a ExpSeq).k * (Partial_Sums(b ExpSeq).n
-Partial_Sums(b ExpSeq).(n-'k)))
& (n < k implies it.k=0);
existence
proof
deffunc U(Nat,Nat) = (a ExpSeq).$2 * (Partial_Sums(b ExpSeq).$1
-Partial_Sums(b ExpSeq).($1-'$2));
for n holds ex rseq st for k holds
(k <= n implies rseq.k = U(n,k) ) &
(k > n implies rseq.k=0) from ExReal_CASE;
hence ex rseq st for k holds
(k <= n implies rseq.k =(a ExpSeq).k * (Partial_Sums(b ExpSeq).n
-Partial_Sums(b ExpSeq).(n-'k))) &
(k > n implies rseq.k=0);
end;
uniqueness
proof
let rseq1,rseq2;
assume that
A1:for k holds
(k <= n implies rseq1.k =(a ExpSeq).k * (Partial_Sums(b ExpSeq).n
-Partial_Sums(b ExpSeq).(n-'k)) ) &
(k > n implies rseq1.k=0) and
A2:for k holds
(k <= n implies rseq2.k = (a ExpSeq).k * (Partial_Sums(b ExpSeq).n
-Partial_Sums(b ExpSeq).(n-'k)) ) &
(k > n implies rseq2.k=0);
now let k;
per cases;
suppose A3:k <= n;
hence rseq1.k =(a ExpSeq).k * (Partial_Sums(b ExpSeq).n
-Partial_Sums(b ExpSeq).(n-'k)) by A1
.= rseq2.k by A2,A3;
suppose A4:k > n;
hence rseq1.k = 0 by A1
.= rseq2.k by A2,A4;
end;
hence rseq1=rseq2 by FUNCT_2:113;
end;
end;
definition
let z, w be Element of COMPLEX;
let n be Nat;
func Conj(n,z,w) -> Complex_Sequence means :Def17:
for k be 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=0c);
existence
proof
deffunc U(Nat,Nat) = (z ExpSeq).$2 * (Partial_Sums(w ExpSeq).$1
-Partial_Sums(w ExpSeq).($1-'$2));
for n holds
ex seq st for k holds
(k <= n implies seq.k = U(n,k) ) &
(k > n implies seq.k=0c) from ExComplex_CASE;
hence ex seq st for k holds
(k <= n implies seq.k =(z ExpSeq).k * (Partial_Sums(w ExpSeq).n
-Partial_Sums(w ExpSeq).(n-'k)) ) &
(k > n implies seq.k=0c);
end;
uniqueness
proof
let seq1,seq2;
assume that
A1:for k 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=0c) and
A2: for k 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=0c);
now let k;
per cases;
suppose A3:k <= n;
hence seq1.k =(z ExpSeq).k * (Partial_Sums(w ExpSeq).n
-Partial_Sums(w ExpSeq).(n-'k)) by A1
.= seq2.k by A2,A3;
suppose A4:k > n;
hence seq1.k = 0c by A1
.= seq2.k by A2,A4;
end;
hence seq1=seq2 by COMSEQ_1:6;
end;
end;
Lm3:
for p1,p2,g1,g2 being Element of REAL holds
[*p1,g1*]+[*p2,g2*] =[*p1+p2,g1+g2*] &
[*p1,g1*]-[*p2,g2*] =[*p1-p2,g1-g2*]
&[*p1,g1*]*[*p2,g2*] =[* p1*p2-g1*g2,p1*g2+p2*g1 *]
& -[*p2,g2*]=[*-p2,-g2*]
& [*p2,g2*]*'=[*p2,-g2*]
proof
let p1,p2,g1,g2 be Element of REAL;
A1:Re([*p1,g1*])=p1 & Im([*p1,g1*])=g1 by COMPLEX1:7;
A2:Re([*p2,g2*])=p2 & Im([*p2,g2*])=g2 by COMPLEX1:7;
thus
[*p1,g1*]+[*p2,g2*]=[*Re([*p1,g1*])+Re([*p2,g2*]),
Im([*p1,g1*])+Im([*p2,g2*])*] by COMPLEX1:def 9
.=[* p1+p2,
Im([*p1,g1*])+Im([*p2,g2*])*] by A1,COMPLEX1:7
.=[* p1+p2,g1+g2*] by A1,COMPLEX1:7;
thus
[*p1,g1*]-[*p2,g2*]=[*Re([*p1,g1*])-Re([*p2,g2*]),
Im([*p1,g1*])-Im([*p2,g2*])*] by COMPLEX1:def 12
.=[* p1-p2,
Im([*p1,g1*])-Im([*p2,g2*])*] by A1,COMPLEX1:7
.=[* p1-p2,g1-g2*] by A1,COMPLEX1:7;
thus
[*p1,g1*]*[*p2,g2*]=[* p1*p2-g1*g2, p1*g2+p2*g1 *] by A1,A2,COMPLEX1:def 10
;
thus
-[*p2,g2*]=[*-Re([*p2,g2*]),-Im([*p2,g2*])*] by COMPLEX1:def 11
.=[*-p2,-Im([*p2,g2*])*] by COMPLEX1:7
.=[*-p2,-g2*] by COMPLEX1:7;
thus [*p2,g2*]*' =[*Re([*p2,g2*]),-Im([*p2,g2*])*] by COMPLEX1:def 15
.=[*p2,-Im([*p2,g2*])*] by COMPLEX1:7
.=[*p2,-g2*] by COMPLEX1:7;
end;
theorem Th4:
z ExpSeq.(n+1) = z ExpSeq.n * z /[*(n+1),0*] &
z ExpSeq.0=1r &
|.(z ExpSeq).n .| = (|.z.| ExpSeq ).n
proof
A1:
now
let n be Nat;
thus (z ExpSeq).(n+1)=z #N (n+1) / ((n+1) !c ) by Def8
.=(z GeoSeq).(n+1) / ((n+1)!c ) by COMSEQ_3:def 2
.=(z GeoSeq).n * z /((n+1)!c ) by COMSEQ_3:def 1
.=z #N n * z / ((n+1)!c ) by COMSEQ_3:def 2
.=z #N n * z /(n!c * [*n+1,0*]) by Th1
.=(z #N n / (n!c ) )*( z / [*n+1,0*]) by XCMPLX_1:77
.=(z #N n / (n!c ) * z) / [*n+1,0*] by XCMPLX_1:75
.=z ExpSeq.n * z /[*n+1,0*] by Def8;
end;
A2:(z ExpSeq).0=z #N 0 /(0!c ) by Def8
.=(z GeoSeq).0 /(0!c ) by COMSEQ_3:def 2
.=1r/1r by Th1,COMSEQ_3:def 1
.=1r by COMPLEX1:85;
defpred X[Nat] means |. ((z ExpSeq)).$1 .| =( |.z.| ExpSeq ).$1;
( |.z.| ExpSeq ).0 = ((|.z .|) |^ 0)/ (0!) by Def9
.= 1/(0!) by NEWTON:9
.= 1/((Prod_real_n).0) by Def7
.= 1/1 by Def5
.= 1;
then A3: X[0] by A2,COMPLEX1:134;
A4:now let n such that
A5: X[n];
0 < n+1 by Lm2;
then A6:[*(n+1),0*] <> 0c by Th1;
A7:Re([*(n+1),0*])=n+1 & Im([*(n+1),0*])=0 by COMPLEX1:7;
A8: 0 <= n+1 by NAT_1:18;
A9:|.[*(n+1),0*].|=abs(n+1) by A7,COMPLEX1:136
.=n+1 by A8,ABSVALUE:def 1;
|. ((z ExpSeq)).(n+1) .|
=|. z ExpSeq.n * z /[*(n+1),0*] .| by A1
.=|. z ExpSeq.n * z .|/|.[*(n+1),0*].| by A6,COMPLEX1:153
.=(( |.z.| ExpSeq ).n) * |.z .|/|.[*(n+1),0*].| by A5,COMPLEX1:151
.= (|.z.| |^ n)/(n!) * |.z .|/|.[*(n+1),0*].| by Def9
.=( (|.z.| |^ n) * |.z .| )/( (n!) * |.[*(n+1),0*].| )
by XCMPLX_1:84
.=( (|.z.| |^ n) * |.z .| )/( (n+1)! ) by A9,NEWTON:21
.=( (|.z.| |^ (n+1)) )/( (n+1)! ) by NEWTON:11
.=( |.z.| ExpSeq ).(n+1) by Def9;
hence X[n+1];
end;
for n holds X[n] from Ind(A3,A4);
hence thesis by A1,A2;
end;
theorem Th5:
0 < k implies (Sift(seq)).k=seq.(k-'1)
proof
assume
A1: 0 < k;
then A2: 0+1 <= k by INT_1:20;
consider m such that
A3: m+1=k by A1,NAT_1:22;
A4: m=k-1 by A3,XCMPLX_1:26;
thus (Sift(seq)).k=seq.m by A3,Def12
.=seq.(k-'1) by A2,A4,SCMFSA_7:3;
end;
theorem Th6:
Partial_Sums(seq).k=Partial_Sums(Sift(seq)).k+seq.k
proof
defpred X[Nat] means Partial_Sums(seq).$1=Partial_Sums(Sift(seq)).$1+seq.$1;
Partial_Sums(seq).0=0c + seq.0 by COMSEQ_3:def 7
.=(Sift(seq)).0 + seq.0 by Def12
.=Partial_Sums(Sift(seq)).0+seq.0 by COMSEQ_3:def 7;
then
A1: X[0];
A2: for k st X[k] holds X[k+1]
proof let k such that
A3: Partial_Sums(seq).k=Partial_Sums(Sift(seq)).k+seq.k;
thus Partial_Sums(seq).(k+1) = (Partial_Sums(Sift(seq)).k+seq.k) + seq.(k+1)
by A3,COMSEQ_3:def 7
.=(Partial_Sums(Sift(seq)).k+(Sift(seq)).(k+1)) + seq.(k+1) by Def12
.=Partial_Sums(Sift(seq)).(k+1)+seq.(k+1) by COMSEQ_3:def 7;
end;
for k holds X[k] from Ind(A1,A2);
hence thesis;
end;
theorem Th7:
(z+w) #N n = Partial_Sums(Expan(n,z,w)).n
proof
A1:(z+w) #N 0 =((z+w) GeoSeq).0 by COMSEQ_3:def 2
.=1r by COMSEQ_3:def 1;
A2:0-'0=0 by GOBOARD9:1;
defpred X[Nat] means (z+w) #N $1 = Partial_Sums(Expan($1,z,w)).$1;
Partial_Sums(Expan(0,z,w)).0 = Expan(0,z,w).0 by COMSEQ_3:def 7
.= (Coef(0)).0 * (z #N 0) * (w #N 0) by A2,Def13
.= 1r/(1r * 1r) * z #N 0 * w #N 0 by A2,Def10,Th1
.= 1r/1r * z #N 0 * w #N 0 by COMPLEX1:29
.= 1r * z #N 0 * w #N 0 by COMPLEX1:85
.= z #N 0 * w #N 0 by COMPLEX1:29
.= (z GeoSeq).0 * w #N 0 by COMSEQ_3:def 2
.= (z GeoSeq).0 * (w GeoSeq).0 by COMSEQ_3:def 2
.= 1r * (w GeoSeq).0 by COMSEQ_3:def 1
.= 1r * 1r by COMSEQ_3:def 1
.= 1r by COMPLEX1:29;
then A3: X[0] by A1;
A4: for n st X[n] holds X[n+1]
proof let n such that
A5: (z+w) #N n = Partial_Sums(Expan(n,z,w)).n;
A6: (z+w) #N (n+1) =((z+w) GeoSeq ).(n+1) by COMSEQ_3:def 2
.=((z+w) GeoSeq ).n * (z+w) by COMSEQ_3:def 1
.=(Partial_Sums(Expan(n,z,w)).n) * (z+w) by A5,COMSEQ_3:def 2
.=((z+w) (#) Partial_Sums(Expan(n,z,w))).n by COMSEQ_1:def 7
.=(Partial_Sums((z+w) (#) Expan(n,z,w))).n by COMSEQ_3:29;
(z+w) (#) Expan(n,z,w)=(z (#) Expan(n,z,w))+(w (#) Expan(n,z,w))
proof
now let k be Nat;
thus ((z+w) (#) Expan(n,z,w)).k=(z+w) * Expan(n,z,w).k by COMSEQ_1:def 7
.=z * Expan(n,z,w).k+w * Expan(n,z,w).k by XCMPLX_1:8
.=(z (#) Expan(n,z,w)).k+w * Expan(n,z,w).k by COMSEQ_1:def 7
.=(z (#) Expan(n,z,w)).k+(w (#)
Expan(n,z,w)).k by COMSEQ_1:def 7
.=((z (#) Expan(n,z,w))+(w (#)
Expan(n,z,w))).k by COMSEQ_1:def 4;
end;
hence thesis by COMSEQ_1:6;
end;
then A7:(z+w) #N (n+1) =( Partial_Sums(z (#) (Expan(n,z,w)))
+Partial_Sums((w (#)
(Expan(n,z,w))))).n by A6,COMSEQ_3:27
.= Partial_Sums((z (#) Expan(n,z,w))).n
+Partial_Sums((w (#) Expan(n,z,w))).n by COMSEQ_1:def 4;
A8:Partial_Sums((z (#) Expan(n,z,w))).n
=Partial_Sums((z (#) Expan(n,z,w))).(n+1)
proof
A9: Partial_Sums((z (#) Expan(n,z,w))).(n+1)
=Partial_Sums((z (#) Expan(n,z,w))).n+(z (#) Expan(n,z,w)).(n+1)
by COMSEQ_3:def 7
.=Partial_Sums((z (#) Expan(n,z,w))).n
+z * Expan(n,z,w).(n+1) by COMSEQ_1:def 7;
n < n+1 & n+1 is Nat by REAL_1:69;
then Expan(n,z,w).(n+1)=0c by Def13;
hence Partial_Sums((z (#) Expan(n,z,w))).(n+1)
=Partial_Sums((z (#) Expan(n,z,w))).n
+0c by A9,COMPLEX1:28
.=Partial_Sums((z (#) Expan(n,z,w))).n by COMPLEX1:22;
end;
A10:Partial_Sums((w (#) Expan(n,z,w))).n
=Partial_Sums((w (#) Expan(n,z,w))).(n+1)
proof
A11:Partial_Sums((w (#) Expan(n,z,w))).(n+1)
=Partial_Sums((w (#) Expan(n,z,w))).n+(w (#) Expan(n,z,w)).(n+1)
by COMSEQ_3:def 7
.=Partial_Sums((w (#) Expan(n,z,w))).n
+w * Expan(n,z,w).(n+1) by COMSEQ_1:def 7;
n < n+1 & n+1 is Nat by REAL_1:69;
then Expan(n,z,w).(n+1)=0c by Def13;
hence Partial_Sums((w (#) Expan(n,z,w))).(n+1)
=Partial_Sums((w (#) Expan(n,z,w))).n
+0c by A11,COMPLEX1:28
.=Partial_Sums((w (#) Expan(n,z,w))).n by COMPLEX1:22;
end;
A12:Partial_Sums((z (#) Expan(n,z,w))).(n+1)
=Partial_Sums(Sift((z (#) Expan(n,z,w)))).(n+1)
proof
A13:Partial_Sums((z (#) Expan(n,z,w))).(n+1)
=Partial_Sums(Sift((z (#) Expan(n,z,w)))).(n+1)
+(z (#) Expan(n,z,w)).(n+1) by Th6;
0 +n < n+1 by REAL_1:69;
then Expan(n,z,w).(n+1)=0c by Def13;
then z * Expan(n,z,w).(n+1)=0c by COMPLEX1:28;
hence Partial_Sums((z (#) Expan(n,z,w))).(n+1)
=Partial_Sums(Sift((z (#) Expan(n,z,w)))).(n+1)
+0c by A13,COMSEQ_1:def 7
.= Partial_Sums(Sift((z (#) Expan(n,z,w)))).(n+1) by COMPLEX1:22;
end;
A14:(w (#) Expan(n,z,w))+Sift((z (#) Expan(n,z,w)))
=Expan(n+1,z,w)
proof
now let k be Nat;
A15: now assume
A16: n+1 < k;
A17: n < k & 1 <= k & 1 <k & 0 <k & n <k-1 & n < k-'1
proof
0 <= n by NAT_1:18;
then A18: 0+1 <= n+1 by AXIOMS:24;
n+1-1 < k -1 by A16,REAL_1:54;
then A19: n < k-1 by XCMPLX_1:26;
then A20: n+0 < k-1+1 by REAL_1:67;
1 <= k by A16,A18,AXIOMS:22;
hence thesis by A16,A18,A19,A20,AXIOMS:22,SCMFSA_7:3,XCMPLX_1:27;
end;
((w (#) Expan(n,z,w))+Sift((z (#) Expan(n,z,w)))).k
=(w (#) Expan(n,z,w)).k + (Sift((z (#) Expan(n,z,w)))).k by COMSEQ_1:def 4
.=(w * Expan(n,z,w).k) + (Sift((z (#) Expan(n,z,w)))).k by COMSEQ_1:def 7
.=(w * Expan(n,z,w).k) + ((z (#) Expan(n,z,w))).(k-'1) by A17,Th5
.=(w * Expan(n,z,w).k) + (z * (Expan(n,z,w).(k-'1)))
by COMSEQ_1:def 7
.=(w * 0c )+ (z * ((Expan(n,z,w).(k-'1)))) by A17,Def13
.=0c + (z * 0c) by A17,Def13
.=0c + 0c by COMPLEX1:28
.=0c by COMPLEX1:22;
hence ((w (#) Expan(n,z,w))+Sift((z (#) Expan(n,z,w)))).k
=Expan(n+1,z,w).k by A16,Def13;
end;
now assume
A21: k <= (n+1);
A22: now assume
A23: k=n+1;
thus ((w (#) Expan(n,z,w))+Sift((z (#) Expan(n,z,w)))).k=Expan(n+1,z,w).
k
proof
A24: n < n+1 by REAL_1:69;
A25: n-'n= n-n by SCMFSA_7:3
.= 0 by XCMPLX_1:14;
A26: n+1-'(n+1)= n+1-(n+1) by SCMFSA_7:3
.= 0 by XCMPLX_1:14;
A27: n!c <>0c & (n+1)!c <>0c by Th1;
A28: (Coef(n)).(n) = n!c /((n!c ) * (0!c )) by A25,Def10
.= n!c / (n!c ) by Th1,COMPLEX1:29
.= 1r by A27,COMPLEX1:86;
A29: (Coef(n+1)).(n+1) = (n+1)!c /(((n+1)!c ) * (0!c ))
by A26,Def10
.= (n+1)!c / ((n+1)!c ) by Th1,COMPLEX1:29
.= 1r by A27,COMPLEX1:86;
thus ((w (#) Expan(n,z,w))+Sift((z (#) Expan(n,z,w)))).k =
(w (#) Expan(n,z,w)).(n+1)+(Sift((z (#) Expan(n,z,w)))).(n+1)
by A23,COMSEQ_1:def 4
.=(w * Expan(n,z,w).(n+1)) + (Sift((z (#) Expan(n,z,w)))).(n+1)
by COMSEQ_1:def 7
.=( w * 0c) + (Sift((z (#) Expan(n,z,w)))).(n+1) by A24,Def13
.= ((z (#) Expan(n,z,w))).(n) by Def12
.= z * (Expan(n,z,w)).n by COMSEQ_1:def 7
.=z * ((Coef(n)).n * (z #N n) * (w #N (n-'n))) by Def13
.=z * ((Coef(n)).n * ((z #N n) * (w #N (n-'n)))) by XCMPLX_1:4
.=(z * ((Coef(n)).n) * ((z #N n) * (w #N (n-'n)))) by XCMPLX_1:4
.= ((Coef(n)).n * z * (z #N n) * (w #N (n-'n))) by XCMPLX_1:4
.= ((Coef(n)).n * (z * (z #N n) ) * (w #N (n-'n))) by XCMPLX_1:4
.= ((Coef(n)).n * ((z GeoSeq).n * z) * (w #N (n-'n)))
by COMSEQ_3:def 2
.= ((Coef(n)).n * ((z GeoSeq).(n+1)) * (w #N (n-'n))) by COMSEQ_3:def 1
.= ((Coef(n+1)).(n+1) * (z #N (n+1)) * (w #N (n-'n)))
by A28,A29,COMSEQ_3:def 2
.= Expan(n+1,z,w).k by A23,A25,A26,Def13;
end;
end;
now assume
A30: k < n+1;
A31: now assume
A32: k=0;
thus ((w (#) Expan(n,z,w))+Sift((z (#) Expan(n,z,w)))).k
=Expan(n+1,z,w).k
proof
A33: 0 <= n by NAT_1:18;
A34: 0 <= n+1 by NAT_1:18;
A35: n-'0 =n-0 by A33,SCMFSA_7:3;
A36: n+1-'0 =n+1-0 by A34,SCMFSA_7:3;
A37: n!c <>0c & (n+1)!c <>0c by Th1;
A38: (Coef(n)).0 = n!c /((0!c ) * (n!c )) by A33,A35,Def10
.= n!c / (n!c ) by Th1,COMPLEX1:29
.= 1r by A37,COMPLEX1:86;
A39: (Coef(n+1)).0 = (n+1)!c /((0!c ) * ((n+1)!c ))
by A34,A36,Def10
.= (n+1)!c / ((n+1)!c ) by Th1,COMPLEX1:29
.= 1r by A37,COMPLEX1:86;
thus
((w (#) Expan(n,z,w))+Sift((z (#) Expan(n,z,w)))).k =
(w (#) Expan(n,z,w)).0+(Sift((z (#) Expan(n,z,w)))).0
by A32,COMSEQ_1:def 4
.=(w * Expan(n,z,w).0) + (Sift((z (#) Expan(n,z,w)))).0
by COMSEQ_1:def 7
.=(w * Expan(n,z,w).0) + 0c by Def12
.=w * ((Coef(n)).0 * (z #N 0) * (w #N (n-'0))) by A33,Def13
.= ((Coef(n)).0 * (z #N 0) * ((w GeoSeq)).n * w)
by A35,COMSEQ_3:def 2
.= (Coef(n)).0 * (z #N 0) * (((w GeoSeq)).n * w) by XCMPLX_1:4
.= ((Coef(n)).0 * (z #N 0) * ( ((w GeoSeq)).(n+1-'0)) )
by A36,COMSEQ_3:def 1
.= (Coef(n+1)).0 * (z #N 0) * (w #N (n+1-'0))
by A38,A39,COMSEQ_3:def 2
.= Expan(n+1,z,w).k by A32,A34,Def13;
end;
end;
now assume k<>0;
then A40: 0<k by NAT_1:19;
then A41: 0+1 <= k by INT_1:20;
k+1 <= n+1 by A30,INT_1:20;
then k+1-1 <= n+1-1 by REAL_1:49;
then k <= n+1-1 by XCMPLX_1:26;
then A42: k <= n by XCMPLX_1:26;
k < k+1 by REAL_1:69;
then k-1 <= k+1-1 by REAL_1:49;
then k-1 <= k by XCMPLX_1:26;
then k-1 <= n by A42,AXIOMS:22;
then A43: k-'1 <= n by A41,SCMFSA_7:3;
thus ((w (#) Expan(n,z,w))+Sift((z (#) Expan(n,z,w)))).k
=Expan(n+1,z,w).k
proof
A44:
((w (#) Expan(n,z,w))+Sift((z (#) Expan(n,z,w)))).k
=(w (#) Expan(n,z,w)).k+(Sift((z (#) Expan(n,z,w)))).k
by COMSEQ_1:def 4
.=(w * Expan(n,z,w).k) + (Sift((z (#) Expan(n,z,w)))).k
by COMSEQ_1:def 7
.=(w * Expan(n,z,w).k) + (z (#) Expan(n,z,w)).(k-'1)
by A40,Th5
.=(w * Expan(n,z,w).k) + (z * Expan(n,z,w).(k-'1))
by COMSEQ_1:def 7
.=(w * ((Coef(n)).k * (z #N k) * (w #N (n-'k))))
+ (z * Expan(n,z,w).(k-'1)) by A42,Def13
.=(w * ((Coef(n)).k * (z #N k) * (w #N (n-'k))))
+ (z * ((Coef(n)).(k-'1) * (z #N (k-'1))
* (w #N (n-'(k-'1))))) by A43,Def13
.=(w * ((Coef(n)).k * (z #N k)) * (w #N (n-'k)))
+ (z * ((Coef(n)).(k-'1) * (z #N (k-'1))
* (w #N (n-'(k-'1))))) by XCMPLX_1:4
.=(w * (Coef(n)).k * (z #N k) * (w #N (n-'k)))
+ (z * ((Coef(n)).(k-'1) * (z #N (k-'1))
* (w #N (n-'(k-'1))))) by XCMPLX_1:4
.=(w * (Coef(n)).k * (z #N k) * (w #N (n-'k)))
+ (z * ((Coef(n)).(k-'1) * (z #N (k-'1)))
* (w #N (n-'(k-'1)))) by XCMPLX_1:4
.=(w * (Coef(n)).k * (z #N k) * (w #N (n-'k)))
+ (z * (Coef(n)).(k-'1) * (z #N (k-'1))
* (w #N (n-'(k-'1)))) by XCMPLX_1:4
.=((Coef(n)).k * (w * (z #N k)) * (w #N (n-'k) ))
+ (z * (Coef(n)).(k-'1) * (z #N (k-'1))
* (w #N (n-'(k-'1)))) by XCMPLX_1:4
.=((Coef(n)).k * (w * (z #N k)) * (w #N (n-'k) ))
+ (z * ((Coef(n)).(k-'1) * (z #N (k-'1)))
* (w #N (n-'(k-'1)))) by XCMPLX_1:4
.=((Coef(n)).k * ((w * (z #N k)) * (w #N (n-'k) )))
+ ( ( (Coef(n)).(k-'1) ) * ((z #N (k-'1)))
* z * ( w #N (n-'(k-'1)) ) ) by XCMPLX_1:4
.=( (Coef(n)).k * ( w * (z #N k) * (w #N (n-'k)) )
+ ((Coef(n)).(k-'1) * ((z #N (k-'1))
* z) * (w #N (n-'(k-'1))))) by XCMPLX_1:4
.=( (Coef(n)).k * ( w * (z #N k) * (w #N (n-'k)) )
+ ( (Coef(n)).(k-'1) * ((z #N (k-'1))
* z * (w #N (n-'(k-'1)))))) by XCMPLX_1:4;
A45:
(w * (z #N k)) * (w #N (n-'k) )
=(z #N k) * (w #N (n+1-'k) )
proof
n < n+1 by REAL_1:69;
then A46: k <= n+1 by A42,AXIOMS:22;
A47: (n-'k)+1=n-k+1 by A42,SCMFSA_7:3
.=n+1-k by XCMPLX_1:29
.=(n+1-'k) by A46,SCMFSA_7:3;
thus (w * (z #N k)) * (w #N (n-'k) )
=((z #N k) ) * (w * (w #N (n-'k)) ) by XCMPLX_1:4
.=((z #N k) ) * ((w GeoSeq).(n-'k) * w) by COMSEQ_3:def 2
.=((z #N k) ) * ((w GeoSeq).(n+1-'k)) by A47,COMSEQ_3:def 1
.=(z #N k) * (w #N (n+1-'k)) by COMSEQ_3:def 2;
end;
(z #N (k-'1)) * z * (w #N (n-'(k-'1)))
=(z #N k) * (w #N (n+1-'k))
proof
n < n+1 by REAL_1:69;
then A48: k <= n+1 by A42,AXIOMS:22;
A49: (n-'(k-'1))=n-(k-'1) by A43,SCMFSA_7:3
.=n-(k-1) by A41,SCMFSA_7:3
.=n+(1-k) by XCMPLX_1:38
.=n+1-k by XCMPLX_1:29
.=(n+1-'k) by A48,SCMFSA_7:3;
A50: (k-'1)+1 =k-1+1 by A41,SCMFSA_7:3
.=k by XCMPLX_1:27;
(z #N (k-'1)) * z
=(z GeoSeq).(k-'1) * z by COMSEQ_3:def 2
.= (z GeoSeq).k by A50,COMSEQ_3:def 1
.= z #N k by COMSEQ_3:def 2;
hence (z #N (k-'1)) * z * (w #N (n-'(k-'1)))
=(z #N k) * (w #N (n+1-'k)) by A49;
end;
then A51: ((w (#) Expan(n,z,w))+Sift((z (#) Expan(n,z,w)))).k
= ((Coef(n)).k +(Coef(n)).(k-'1) )
* ((z #N k) * (w #N (n+1-'k) )) by A44,A45,XCMPLX_1:8;
A52: (Coef(n)).k +(Coef(n)).(k-'1)
=n!c /( (k!c ) * ((n-'k)!c ) )
+(Coef(n)).(k-'1) by A42,Def10
.=n!c /( (k!c ) * ((n-'k)!c ) )
+n!c /(((k-'1)!c ) * (((n-'(k-'1)))!c )) by A43,Def10;
A53: ( (k!c ) * ((n-'k)!c ) ) * [*(n+1-k),0*]
=(k!c ) * (((n-'k)!c ) * [*(n+1-k),0*]) by XCMPLX_1:4;
A54: (n-'(k-'1)) =n-(k-'1) by A43,SCMFSA_7:3
.=n-(k-1) by A41,SCMFSA_7:3
.=n+(1-k) by XCMPLX_1:38
.=n+1-k by XCMPLX_1:29
.=n+1-'k by A30,SCMFSA_7:3;
A55: (((k-'1)!c ) * (((n-'(k-'1)))!c )) * [*k,0*]
=[*k,0*] * ((k-'1)!c ) * (((n-'(k-'1)))!c ) by XCMPLX_1:4
.=(k!c ) * ((n+1-'k)!c ) by A40,A54,Th3;
A56: (k!c ) <> 0c & (n-'k)!c <>0c & (k-'1)!c <>0c
& ((n-'(k-'1)))!c <>0c & ((n+1-'k))!c <>0c &
[*(n+1-k),0*] <>0c & [*k,0*] <>0c
proof
A57: 0 < n+1-k by A30,SQUARE_1:11;
then n+1-k is Nat by INT_1:16;
hence thesis by A40,A57,Th1;
end;
then A58:
n!c /( (k!c ) * ((n-'k)!c ) )
=(n!c * [*(n+1-k),0*])
/(( (k!c ) * ((n-'k)!c ) ) * [*(n+1-k),0*])
by XCMPLX_1:92
.=(n!c * [*(n+1-k),0*])/((k!c ) * ((n+1-'k)!c ))
by A42,A53,Th3;
n!c /(((k-'1)!c ) * (((n-'(k-'1)))!c ))
=(n!c * [*k,0*])/((k!c ) * ((n+1-'k)!c ))
by A55,A56,XCMPLX_1:92;
then (Coef(n)).k +(Coef(n)).(k-'1)
=((n!c * [*(n+1-k),0*])+(n!c * [*k,0*]))
/ ((k!c ) * ((n+1-'k)!c )) by A52,A58,XCMPLX_1:63
.=( n!c * ([*(n+1-k),0*] + [*k,0*]))
/ ((k!c ) * ((n+1-'k)!c )) by XCMPLX_1:8
.=( n!c * [*n+1-k+k,0+0*])
/ ((k!c ) * ((n+1-'k)!c )) by Lm3
.=( n!c * [*n+1,0*])
/ ((k!c ) * ((n+1-'k)!c )) by XCMPLX_1:27
.=((n+1)!c ) / ((k!c ) * ((n+1-'k)!c )) by Th1
.=(Coef(n+1)).k by A30,Def10;
hence ((w (#) Expan(n,z,w))+Sift((z (#) Expan(n,z,w)))).k
=(Coef(n+1)).k * (z #N k) * (w #N (n+1-'k) )
by A51,XCMPLX_1:4
.=Expan(n+1,z,w).k by A30,Def13;
end;
end;
hence ((w (#) Expan(n,z,w))+Sift((z (#) Expan(n,z,w)))).k
=Expan(n+1,z,w).k by A31;
end;
hence ((w (#) Expan(n,z,w))+Sift((z (#) Expan(n,z,w)))).k
=Expan(n+1,z,w).k by A21,A22,REAL_1:def 5;
end;
hence ((w (#) Expan(n,z,w))+Sift((z (#) Expan(n,z,w)))).k
=Expan(n+1,z,w).k by A15;
end;
hence thesis by COMSEQ_1:6;
end;
thus (z+w) #N (n+1) =(Partial_Sums((w (#) Expan(n,z,w))) +
Partial_Sums(Sift((z (#) Expan(n,z,w))))).(n+1)
by A7,A8,A10,A12,COMSEQ_1:def 4
.=Partial_Sums(Expan(n+1,z,w)).(n+1) by A14,COMSEQ_3:27;
end;
for n holds X[n] from Ind(A3,A4);
hence thesis;
end;
theorem Th8:
Expan_e(n,z,w)=(1r/(n!c )) (#) Expan(n,z,w)
proof
now
let k be Nat;
A1: now assume A2:n <k;
hence Expan_e(n,z,w).k=0c by Def14
.=(1r/(n!c )) * 0c by COMPLEX1:28
.=(1r/(n!c )) * Expan(n,z,w).k by A2,Def13
.=((1r/(n!c )) (#) Expan(n,z,w)).k by COMSEQ_1:def 7;
end;
now assume A3:k <= n;
A4:n!c <> 0c by Th1;
thus
A5:
Expan_e(n,z,w).k
= (Coef_e(n)).k * (z #N k) * (w #N (n-'k)) by A3,Def14
.= 1r/((k!c ) * ((n-'k)!c )) * (z #N k) * (w #N (n-'k))
by A3,Def11;
1r/((k!c ) * ((n-'k)!c ))=((n!c )/(n!c ))/((k!c ) * ((n-'k)!c ))
by A4,COMPLEX1:86
.=(((n!c ) * 1r )/(n!c )) /((k!c ) * ((n-'k)!c)) by COMPLEX1:29
.= (1r /(n!c )) * (n!c ) /((k!c ) * ((n-'k)!c ))
by XCMPLX_1:75;
hence Expan_e(n,z,w).k
= (1r/(n!c )) * (n!c ) /((k!c ) * ((n-'k)!c ))
* ((z #N k) * (w #N (n-'k))) by A5,XCMPLX_1:4
.= (1r/(n!c )) * ( (n!c ) /((k!c ) * ((n-'k)!c )) )
* ((z #N k) * (w #N (n-'k))) by XCMPLX_1:75
.= (1r/(n!c )) * (( (n!c ) /((k!c ) * ((n-'k)!c )) )
* ((z #N k) * (w #N (n-'k)))) by XCMPLX_1:4
.= (1r/(n!c )) * ((n!c ) /((k!c ) * ((n-'k)!c ))
* (z #N k) * (w #N (n-'k))) by XCMPLX_1:4
.= (1r/(n!c )) * ((Coef(n)).k * ((z #N k))
* (w #N (n-'k))) by A3,Def10
.= (1r/(n!c )) * Expan(n,z,w).k by A3,Def13
.= ( (1r/(n!c )) (#) Expan(n,z,w) ).k by COMSEQ_1:def 7;
end;
hence Expan_e(n,z,w).k = ( (1r/(n!c )) (#) Expan(n,z,w) ).k by A1;
end;
hence Expan_e(n,z,w)=((1r/(n!c )) (#) Expan(n,z,w)) by COMSEQ_1:6;
end;
theorem Th9:
((z+w) #N n) / (n!c) = Partial_Sums(Expan_e(n,z,w)).n
proof
thus
((z+w) #N n)/(n!c )= (Partial_Sums(Expan(n,z,w)).n)/(n!c) by Th7
.= ((Partial_Sums(Expan(n,z,w)).n) * 1r)/(n!c ) by COMPLEX1:29
.= (Partial_Sums(Expan(n,z,w)).n) * (1r/(n!c )) by XCMPLX_1:75
.= ((1r/(n!c )) (#) (Partial_Sums(Expan(n,z,w)))).n by COMSEQ_1:def 7
.= Partial_Sums( (1r/(n!c )) (#) Expan(n,z,w)).n by COMSEQ_3:29
.= Partial_Sums(Expan_e(n,z,w)).n by Th8;
end;
theorem Th10:
0c ExpSeq is absolutely_summable & Sum(0c ExpSeq)=1r
proof
defpred X[set] means Partial_Sums(|.0c ExpSeq.|).$1=1;
Partial_Sums(|.(0c ExpSeq).|).0
=|.(0c ExpSeq).|.0 by SERIES_1:def 1
.=|. (0c ExpSeq).0 .| by COMSEQ_1:def 14
.=1 by Th4,COMPLEX1:134;
then
A1: X[0];
A2: for n st X[n] holds X[n+1]
proof let n such that
A3: Partial_Sums(|.0c ExpSeq.|).n=1;
thus Partial_Sums(|.0c ExpSeq.|).(n+1)
=1 + |.0c ExpSeq.|.(n+1) by A3,SERIES_1:def 1
.=1 + |.(0c ExpSeq).(n+1).| by COMSEQ_1:def 14
.=1 + |.(0c ExpSeq.n) * 0c/[*(n+1),0*] .| by Th4
.=1 by COMPLEX1:130;
end;
A4: 0c ExpSeq is absolutely_summable
proof
for n holds X[n] from Ind(A1,A2);
then Partial_Sums(|.0c ExpSeq.|) is constant by SEQM_3:def 6;
then Partial_Sums(|.0c ExpSeq.|) is convergent by SEQ_4:39;
hence |.0c ExpSeq.| is summable by SERIES_1:def 2;
end;
defpred X[set] means Partial_Sums(0c ExpSeq).$1=1r;
Partial_Sums(0c ExpSeq).0
=(0c ExpSeq).0 by COMSEQ_3:def 7
.=1r by Th4;
then
A5: X[0];
A6: for n st X[n] holds X[n+1]
proof let n such that
A7: Partial_Sums(0c ExpSeq).n=1r;
thus Partial_Sums(0c ExpSeq).(n+1)
=1r + (0c ExpSeq).(n+1) by A7,COMSEQ_3:def 7
.=1r + (0c ExpSeq.n) * 0c/[*(n+1),0*] by Th4
.=1r;
end;
for n holds X[n] from Ind(A5,A6);
then lim(Partial_Sums(0c ExpSeq))=1r by COMSEQ_2:10;
hence thesis by A4,COMSEQ_3:def 8;
end;
definition let z;
cluster z ExpSeq -> absolutely_summable;
coherence
proof
now assume
A1:z<>0c;
defpred X[set] means (z ExpSeq).$1 <> 0c;
0c <> 1r by COMPLEX1:def 7;
then A2: X[0] by Th4;
A3: for n st X[n] holds X[n+1]
proof let n;
assume
A4:(z ExpSeq).n <> 0c;
thus (z ExpSeq).(n+1) <> 0c
proof
assume
A5: (z ExpSeq).(n+1) = 0c;
A6: [*(n+1),0*] <>0c by COMSEQ_3:1;
A7: ((z ExpSeq).n * z)/[*(n+1),0*]=0c by A5,Th4;
0c = 0c/z by COMPLEX1:87
.=(z ExpSeq).n * z/z by A6,A7,XCMPLX_1:50
.=(z ExpSeq).n * (z/z) by XCMPLX_1:75
.=(z ExpSeq).n * 1r by A1,COMPLEX1:86
.=(z ExpSeq).n by COMPLEX1:29;
hence contradiction by A4;
end;
end;
deffunc U(Nat) = |.(z ExpSeq).|.($1+1)/|.(z ExpSeq).|.$1;
thus
A8: for n holds X[n] from Ind(A2,A3);
ex rseq st for n holds rseq.n= U(n) from ExRealSeq;
then consider rseq such that
A9:for n holds rseq.n=|.z ExpSeq.|.(n+1)/|.z ExpSeq.|.n;
rseq is convergent & lim rseq < 1
proof
now let n;
A10:(z ExpSeq).n<>0c by A8;
A11:[*(n+1),0*] <> 0c by COMSEQ_3:1;
A12:Im([*(n+1),0*]) = 0 by COMPLEX1:7;
A13:0 <= (n+1) by NAT_1:18;
thus rseq.n =|.z ExpSeq.|.(n+1)/|.z ExpSeq.|.n by A9
.=|.(z ExpSeq).(n+1).|/|.z ExpSeq.|.n by COMSEQ_1:def 14
.=|.(z ExpSeq).(n+1).|/|.(z ExpSeq).n.| by COMSEQ_1:def 14
.=|.(z ExpSeq).(n+1)/(z ExpSeq).n.| by A10,COMPLEX1:153
.=|.((z ExpSeq).n * z/[*(n+1),0*]) /(z ExpSeq).n.| by Th4
.=|.((z ExpSeq).n * (z/[*(n+1),0*])) /(z ExpSeq).n.|
by XCMPLX_1:75
.=|.(z/[*(n+1),0*]) .| by A10,XCMPLX_1:90
.=|.z.|/|.[*(n+1),0*] .| by A11,COMPLEX1:153
.=|.z.|/abs(Re([*(n+1),0*])) by A12,COMPLEX1:136
.=|.z.|/abs(n+1) by COMPLEX1:7
.=|.z.|/(n+1) by A13,ABSVALUE:def 1;
end;
then rseq is convergent & lim(rseq)=0 by SEQ_4:46;
hence thesis;
end;
hence z ExpSeq is absolutely_summable by A8,A9,COMSEQ_3:76;
end;
hence thesis by Th10;
end;
end;
theorem Th11:
(z ExpSeq).0 = 1r & Expan(0,z,w).0 = 1r
proof
thus (z ExpSeq).0
= (z #N 0)/(0!c ) by Def8
.= (z GeoSeq).0/(0!c ) by COMSEQ_3:def 2
.= 1r/1r by Th1,COMSEQ_3:def 1
.= 1r by COMPLEX1:85;
A1: 0-'0=0 by GOBOARD9:1;
hence Expan(0,z,w).0 = (Coef(0)).0 * (z #N 0) * (w #N 0) by Def13
.= 1r/(1r * 1r) * z #N 0 * w #N 0 by A1,Def10,Th1
.= 1r/1r * z #N 0 * w #N 0 by COMPLEX1:29
.= 1r * z #N 0 * w #N 0 by COMPLEX1:85
.= z #N 0 * w #N 0 by COMPLEX1:29
.= (z GeoSeq).0 * w #N 0 by COMSEQ_3:def 2
.= (z GeoSeq).0 * (w GeoSeq).0 by COMSEQ_3:def 2
.= 1r * (w GeoSeq).0 by COMSEQ_3:def 1
.= 1r * 1r by COMSEQ_3:def 1
.= 1r by COMPLEX1:29;
end;
theorem Th12:
l <= k implies (Alfa(k+1,z,w)).l = (Alfa(k,z,w)).l + Expan_e(k+1,z,w).l
proof
assume
A1:l <= k;
k < k+1 by REAL_1:69;
then A2:l <= k+1 by A1,AXIOMS:22;
then (k+1-'l)=k+1-l by SCMFSA_7:3;
then A3: (k+1-'l)=k-l+1 by XCMPLX_1:29
.=(k-'l)+1 by A1,SCMFSA_7:3;
then A4: (Alfa(k+1,z,w)).l
=(z ExpSeq).l * (Partial_Sums(w ExpSeq).((k-'l)+1)) by A2,Def15
.=(z ExpSeq).l * (Partial_Sums(w ExpSeq).((k-'l))
+(w ExpSeq).((k+1-'l))) by A3,COMSEQ_3:def 7
.=((z ExpSeq).l * (Partial_Sums(w ExpSeq).((k-'l)))
+((z ExpSeq).l * (w ExpSeq).((k+1-'l)))) by XCMPLX_1:8
.=(Alfa(k,z,w)).l+((z ExpSeq).l * (w ExpSeq).((k+1-'l)))
by A1,Def15;
(z ExpSeq).l * (w ExpSeq).((k+1-'l))
=(z #N l/(l!c )) * (w ExpSeq).((k+1-'l)) by Def8
.=(z #N l/(l!c )) * (w #N ((k+1-'l))/(((k+1-'l))!c )) by Def8
.=((z #N l) * (w #N ((k+1-'l)))/((l!c ) * (((k+1-'l))!c )))
by XCMPLX_1:77
.=(((z #N l) * (w #N ((k+1-'l))) * 1r)/((l!c ) * (((k+1-'l))!c )))
by COMPLEX1:29
.=((z #N l) * (w #N ((k+1-'l))) * ((1r/((l!c ) * (((k+1-'l))!c )))))
by XCMPLX_1:75
.= ((Coef_e(k+1)).l) * ((z #N l) * (w #N ((k+1-'l)))) by A2,Def11
.= ((Coef_e(k+1)).l) * (z #N l) * (w #N ((k+1-'l))) by XCMPLX_1:4
.=Expan_e(k+1,z,w).l by A2,Def14;
hence (Alfa(k+1,z,w)).l = (Alfa(k,z,w)).l + Expan_e(k+1,z,w).l by A4;
end;
theorem Th13:
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
now let l be Nat; assume
l <= k;
hence (Alfa(k+1,z,w)).l = (Alfa(k,z,w)).l + Expan_e(k+1,z,w).l
by Th12
.= ( (Alfa(k,z,w)) + Expan_e(k+1,z,w)).l by COMSEQ_1:def 4;
end;
hence Partial_Sums((Alfa(k+1,z,w))).k
=Partial_Sums(((Alfa(k,z,w)) + Expan_e(k+1,z,w))).k by COMSEQ_3:35
.=(Partial_Sums(( Alfa(k,z,w)))
+Partial_Sums(( Expan_e(k+1,z,w )))).k by COMSEQ_3:27
.= (Partial_Sums(( Alfa(k,z,w)))).k
+ (Partial_Sums(( Expan_e(k+1,z,w) ))).k by COMSEQ_1:def 4;
end;
theorem Th14:
(z ExpSeq).k=(Expan_e(k,z,w)).k
proof
A1: 0 = k -k by XCMPLX_1:14;
then A2: k-'k=0 by SCMFSA_7:3;
A3: (k-'k)!c =1r by A1,Th1,SCMFSA_7:3;
thus (Expan_e(k,z,w)).(k)=((Coef_e(k)).k) * (z #N k) * (w #N 0) by A2,Def14
.=( (Coef_e(k)).k) * (z #N k) * 1r by COMSEQ_3:11
.=( (Coef_e(k)).k) * (z #N k) by COMPLEX1:29
.=(1r/((k!c ) * 1r)) * (z #N k) by A3,Def11
.=(1r/((k!c ) )) * (z #N k) by COMPLEX1:29
.=((z #N k) * 1r)/(k!c ) by XCMPLX_1:75
.= (z #N k)/(k!c ) by COMPLEX1:29
.=(z ExpSeq).k by Def8;
end;
theorem Th15:
Partial_Sums((z+w) ExpSeq).n = Partial_Sums(Alfa(n,z,w)).n
proof
A1:Partial_Sums((z+w) ExpSeq).0
=((z+w) ExpSeq).0 by COMSEQ_3:def 7
.=1r by Th11;
defpred X[Nat] means
Partial_Sums((z+w) ExpSeq).$1=Partial_Sums(Alfa($1,z,w)).$1;
A2: 0-'0=0 by GOBOARD9:1;
Partial_Sums(Alfa(0,z,w)).0
= Alfa(0,z,w).0 by COMSEQ_3:def 7
.= (z ExpSeq).0 * Partial_Sums(w ExpSeq).0 by A2,Def15
.= (z ExpSeq).0 * (w ExpSeq).0 by COMSEQ_3:def 7
.=1r * (w ExpSeq).0 by Th11
.=1r * 1r by Th11
.= 1r by COMPLEX1:29;
then A3: X[0] by A1;
A4: for k st X[k] holds X[k+1]
proof let k such that
A5:Partial_Sums((z+w) ExpSeq).k=Partial_Sums(Alfa(k,z,w)).k;
thus
Partial_Sums((z+w) ExpSeq).(k+1)=Partial_Sums(Alfa(k+1,z,w)).(k+1)
proof
A6: 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 COMSEQ_3:def 7
.=((Partial_Sums(( Alfa(k,z,w) ))).k
+ (Partial_Sums(( Expan_e(k+1,z,w) ))).k )
+ (Alfa(k+1,z,w)).(k+1) by Th13
.= Partial_Sums((z+w) ExpSeq).k
+ ((Partial_Sums(( Expan_e(k+1,z,w) ))).k
+ (Alfa(k+1,z,w)).(k+1)) by A5,XCMPLX_1:1;
k+1-'(k+1)=0 by GOBOARD9:1;
then (Alfa(k+1,z,w)).(k+1)
=(z ExpSeq).(k+1) * Partial_Sums(w ExpSeq).0 by Def15
.=(z ExpSeq).(k+1) * ((w ExpSeq).0) by COMSEQ_3:def 7
.=(z ExpSeq).(k+1) * 1r by Th11
.=(z ExpSeq).(k+1) by COMPLEX1:29
.=(Expan_e(k+1,z,w)).(k+1) by Th14;
then (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 COMSEQ_3:def 7
.=(z+w) #N (k+1) /((k+1)!c ) by Th9;
hence Partial_Sums((Alfa(k+1,z,w))).(k+1)
=Partial_Sums((z+w) ExpSeq).k
+(z+w) ExpSeq.(k+1) by A6,Def8
.=Partial_Sums((z+w) ExpSeq).(k+1) by COMSEQ_3:def 7;
end;
end;
for n holds X[n] from Ind(A3,A4);
hence thesis;
end;
theorem Th16:
Partial_Sums(z ExpSeq).k * Partial_Sums(w ExpSeq).k
-Partial_Sums((z+w) ExpSeq).k
= Partial_Sums(Conj(k,z,w)).k
proof
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 Th15
.= ((Partial_Sums(w ExpSeq).k) (#) Partial_Sums(z ExpSeq)).k
-Partial_Sums(Alfa(k,z,w)).k by COMSEQ_1:def 7
.=Partial_Sums((Partial_Sums(w ExpSeq).k) (#) (z ExpSeq)).k
-Partial_Sums(Alfa(k,z,w)).k by COMSEQ_3:29
.=Partial_Sums((Partial_Sums(w ExpSeq).k) (#) (z ExpSeq)).k
+-Partial_Sums(Alfa(k,z,w)).k by XCMPLX_0:def 8
.=Partial_Sums((Partial_Sums(w ExpSeq).k) (#) (z ExpSeq)).k
+(-Partial_Sums(Alfa(k,z,w))).k by COMSEQ_1:def 9
.=(Partial_Sums((Partial_Sums(w ExpSeq).k) (#) (z ExpSeq))
+(-Partial_Sums(Alfa(k,z,w)))).k by COMSEQ_1:def 4
.=(Partial_Sums((Partial_Sums(w ExpSeq).k) (#) (z ExpSeq))
-Partial_Sums(Alfa(k,z,w))).k by COMSEQ_1:def 10
.=Partial_Sums((((Partial_Sums(w ExpSeq).k) (#) (z ExpSeq)))
-(Alfa(k,z,w))).k by COMSEQ_3:28;
for l be Nat st l <= k holds
((Partial_Sums(w ExpSeq).k) (#) (z ExpSeq)
- (Alfa(k,z,w))).l
=Conj(k,z,w).l
proof
let l be Nat such that
A2:l <= k;
thus ( ( Partial_Sums(w ExpSeq).k) (#) (z ExpSeq)
- (Alfa(k,z,w)) ).l
=( ( Partial_Sums(w ExpSeq).k) (#) (z ExpSeq)
+-(Alfa(k,z,w)) ).l by COMSEQ_1:def 10
.=(( Partial_Sums(w ExpSeq).k) (#) (z ExpSeq)).l
+(-Alfa(k,z,w)).l by COMSEQ_1:def 4
.=(( Partial_Sums(w ExpSeq).k) (#) (z ExpSeq)).l
+(-Alfa(k,z,w).l) by COMSEQ_1:def 9
.=(( Partial_Sums(w ExpSeq).k) (#) (z ExpSeq)).l
-Alfa(k,z,w).l by XCMPLX_0:def 8
.=(( Partial_Sums(w ExpSeq).k ) * ( (z ExpSeq).l ))
-Alfa(k,z,w).l by COMSEQ_1:def 7
.=((z ExpSeq).l) * ( Partial_Sums(w ExpSeq).k)
-((z ExpSeq).l) * ( Partial_Sums(w ExpSeq).(k-'l))
by A2,Def15
.=((z ExpSeq).l) *
( Partial_Sums(w ExpSeq).k
-Partial_Sums(w ExpSeq).(k-'l) ) by XCMPLX_1:40
.=Conj(k,z,w).l by A2,Def17;
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,COMSEQ_3:35;
end;
theorem Th17:
|. 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
defpred X[Nat] means |. Partial_Sums(( z ExpSeq)).$1 .|
<= Partial_Sums((|.z.| ExpSeq)).$1;
A1: |. Partial_Sums(( z ExpSeq)).0 .|
= |. ((z ExpSeq)).0 .| by COMSEQ_3:def 7
.= |. (z #N 0)/ (0 !c).| by Def8
.= |. ((z GeoSeq)).0/(0 !c) .| by COMSEQ_3:def 2
.= |. 1r /1r .| by Th1,COMSEQ_3:def 1
.= 1 by COMPLEX1:85,134;
Partial_Sums((|.z.| ExpSeq)).0
= ((|.z.| ExpSeq)).0 by SERIES_1:def 1
.= ((|.z .|) |^ 0)/ (0!) by Def9
.= 1 by NEWTON:9,18;
then A2: X[0] by A1;
A3: for k st X[k] holds X[k+1]
proof let k such that
A4: |. Partial_Sums(( z ExpSeq)).k .|
<= Partial_Sums((|.z.| ExpSeq)).k;
A5: |. Partial_Sums(( z ExpSeq)).(k+1) .|
=|. Partial_Sums(( z ExpSeq)).k
+ ((z ExpSeq)).(k+1) .| by COMSEQ_3:def 7;
|. Partial_Sums(( z ExpSeq)).k + ((z ExpSeq)).(k+1) .|
<= |. Partial_Sums(( z ExpSeq)).k.| + |. ((z ExpSeq)).(k+1) .|
by COMPLEX1:142;
then A6: |. Partial_Sums(( z ExpSeq)).(k+1) .|
<= |. Partial_Sums(( z ExpSeq)).k.| + (|.z.| ExpSeq).(k+1) by A5,Th4;
A7: |. Partial_Sums(( z ExpSeq)).k.| + (|.z.| ExpSeq).(k+1)
<= Partial_Sums((|.z.| ExpSeq)).k + (|.z.| ExpSeq).(k+1)
by A4,AXIOMS:24;
Partial_Sums((|.z.| ExpSeq)).k + (|.z.| ExpSeq).(k+1)
=Partial_Sums((|.z.| ExpSeq)).(k+1) by SERIES_1:def 1;
hence |. Partial_Sums(( z ExpSeq)).(k+1) .|
<= Partial_Sums((|.z.| ExpSeq)).(k+1) by A6,A7,AXIOMS:22;
end;
A8: for k holds X[k] from Ind(A2,A3);
hence |. Partial_Sums(( z ExpSeq)).k .|
<= Partial_Sums((|.z.| ExpSeq)).k;
A9: Partial_Sums(|. ( z ExpSeq) .| ) is convergent by SERIES_1:def 2;
A10: for k holds |. ((z ExpSeq)).k.| =(|.z.| ExpSeq).k by Th4;
now let k;
(|.z.| ExpSeq).k = |. ((z ExpSeq)).k.| by Th4;
hence 0 <= (|.z.| ExpSeq).k by COMPLEX1:132;
end;
then A11:Partial_Sums((|.z.| ExpSeq )) is non-decreasing by SERIES_1:19;
dom (|.z.| ExpSeq) = NAT by FUNCT_2:def 1;
then A12:Partial_Sums(|.z.| ExpSeq) is bounded_above by A9,A10,COMSEQ_1:def 14;
then Partial_Sums((|.z.| ExpSeq)).k <= lim(Partial_Sums((|.z.| ExpSeq )))
by A11,SEQ_4:54;
hence Partial_Sums((|.z.| ExpSeq)).k <= Sum(|.z.| ExpSeq) by SERIES_1:def 3
;
A13:now let k;
lim(Partial_Sums((|.z.| ExpSeq)))=Sum(|.z.| ExpSeq)
by SERIES_1:def 3;
hence Partial_Sums((|.z.| ExpSeq)).k <= Sum(|.z.| ExpSeq)
by A11,A12,SEQ_4:54;
end;
A14: |. Partial_Sums(( z ExpSeq)).k .|
<= Partial_Sums((|.z.| ExpSeq)).k by A8;
Partial_Sums((|.z.| ExpSeq)).k <= Sum(|.z.| ExpSeq) by A13;
hence |. Partial_Sums(( z ExpSeq)).k .| <= Sum(|.z.| ExpSeq)
by A14,AXIOMS:22;
end;
theorem Th18:
1 <= Sum(|.z.| ExpSeq)
proof
|. Partial_Sums(z ExpSeq).0 .|=|. (z ExpSeq).0 .| by COMSEQ_3:def 7
.=1 by Th4,COMPLEX1:134;
hence 1 <= Sum(|.z.| ExpSeq) by Th17;
end;
theorem Th19:
0 <= (|. z .| ExpSeq).n
proof
(|. z .| ExpSeq).n = |.((z ExpSeq)).n .| by Th4;
hence 0 <= (|. z .| ExpSeq).n by COMPLEX1:132;
end;
theorem Th20:
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
for n holds 0 <= (|. z .| ExpSeq).n by Th19;
hence thesis by COMSEQ_3:9;
end;
theorem Th21:
abs(Partial_Sums(|.Conj(k,z,w).|).n)=Partial_Sums(|.Conj(k,z,w).|).n
proof
A1:now let n;
|.Conj(k,z,w).|.n=|.(Conj(k,z,w)).n.| by COMSEQ_1:def 14;
hence 0 <= |.Conj(k,z,w).|.n by COMPLEX1:132;
end;
0 <= n by NAT_1:18;
then A2:Partial_Sums(|.Conj(k,z,w).|).0 <= Partial_Sums(|.Conj(k,z,w).|).n
by SEQM_3:12;
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 thesis by A2,A3,ABSVALUE:def 1;
end;
theorem Th22:
for p being real number st p>0 ex n st for k st n <= k
holds abs(Partial_Sums(|.Conj(k,z,w).|).k) < p
proof
let p be real number such that
A1: p>0;
reconsider pp = p as Real by XREAL_0:def 1;
A2: 1 <= Sum(|.z.| ExpSeq) by Th18;
then A3:0 < Sum(|.z.| ExpSeq) by AXIOMS:22;
A4:0 <= Sum(|.z.| ExpSeq) by A2,AXIOMS:22;
0 * Sum(|.z.| ExpSeq) < 4 * Sum(|.z.| ExpSeq) by A3,REAL_1:70;
then A5: 0/(4 * Sum(|.z.| ExpSeq)) < p/(4 * Sum(|.z.| ExpSeq)) by A1,REAL_1
:73;
1 <= Sum(|.w.| ExpSeq) by Th18;
then A6:0 < Sum(|.w.| ExpSeq) by AXIOMS:22;
then 0 * Sum(|.w.| ExpSeq) < 4 * Sum(|.w.| ExpSeq) by REAL_1:70;
then A7: 0/(4 * Sum(|.w.| ExpSeq)) < p/(4 * Sum(|.w.| ExpSeq)) by A1,REAL_1:73;
set p1=min((pp/(4 * Sum(|.z.| ExpSeq))),(pp/(4 * Sum(|.w.| ExpSeq))));
A8:p1 > 0 by A5,A7,SQUARE_1:38;
A9:p1>0 & p1 <= p/(4 * Sum(|.z.| ExpSeq))
& p1 <= p/(4 * Sum(|.w.| ExpSeq)) by A5,A7,SQUARE_1:35,38;
A10: dom (|.z.| ExpSeq) = NAT by FUNCT_2:def 1;
for n holds |. (z ExpSeq).n .| =( |.z.| ExpSeq ).n by Th4;
then |. (z ExpSeq).| = |.z.| ExpSeq by A10,COMSEQ_1:def 14;
then Partial_Sums(( |.z.| ExpSeq )) is convergent by SERIES_1:def 2;
then consider n1 such that
A11: for k,l be Nat st n1 <= k & n1 <= l holds
abs(Partial_Sums(( |.z.| ExpSeq )).k
- Partial_Sums(( |.z.| ExpSeq )).l)
< p1 by A8,COMSEQ_3:4;
consider n2 such that
A12:for k,l be Nat st n2 <= k & n2 <= l holds
|.Partial_Sums(( w ExpSeq )).k
- Partial_Sums(( w ExpSeq )).l.|
< p1 by A8,COMSEQ_3:47;
set n3=n1+n2;
take n4 = n3+n3;
A13:now let n;
let k;
now let l be Nat such that
A14: l <= k;
thus |.Conj(k,z,w).|.l =|.( Conj(k,z,w).l) .| by COMSEQ_1:def 14
.=|.(z ExpSeq).l * (Partial_Sums(w ExpSeq).k
-Partial_Sums(w ExpSeq).(k-'l)) .|
by A14,Def17
.=|.(z ExpSeq).l.| * |.(Partial_Sums(w ExpSeq).k
-Partial_Sums(w ExpSeq).(k-'l)).|
by COMPLEX1:151
.=(|.z.| ExpSeq).l * |.(Partial_Sums(w ExpSeq).k
-Partial_Sums(w ExpSeq).(k-'l)).| by Th4;
end;
hence for l be Nat st l <= k holds
|.Conj(k,z,w).|.l =(|.z.| ExpSeq).l * |.(Partial_Sums(w ExpSeq).k
-Partial_Sums(w ExpSeq).(k-'l)).|;
end;
A15: now let k;
now let l be Nat; assume l <= k;
then A16:|.Conj(k,z,w).|.l
=(|.z .| ExpSeq).l * |.Partial_Sums(w ExpSeq).k
-Partial_Sums(w ExpSeq).(k-'l).| by A13;
A17:|.Partial_Sums(w ExpSeq).k
-Partial_Sums(w ExpSeq).(k-'l).|
<= |.Partial_Sums(w ExpSeq).k .|
+ |.Partial_Sums(w ExpSeq).(k-'l).| by COMPLEX1:143;
|.Partial_Sums(w ExpSeq).k .| <= Sum(|.w.| ExpSeq) by Th17;
then A18:|.Partial_Sums(w ExpSeq).k .|
+ |.Partial_Sums(w ExpSeq).(k-'l).|
<= Sum(|.w.| ExpSeq) + |.Partial_Sums(w ExpSeq).(k-'l).|
by AXIOMS:24;
|.Partial_Sums(w ExpSeq).(k-'l).|
<= Sum(|.w.| ExpSeq) by Th17;
then A19:
Sum(|.w.| ExpSeq) + |.Partial_Sums(w ExpSeq).(k-'l).|
<= Sum(|.w.| ExpSeq)+ Sum(|.w.| ExpSeq) by AXIOMS:24;
Sum(|.w.| ExpSeq)+ Sum(|.w.| ExpSeq)= 2 * Sum(|.w.| ExpSeq) by XCMPLX_1:
11
;
then |.Partial_Sums(w ExpSeq).k .|
+ |.Partial_Sums(w ExpSeq).(k-'l).|
<= 2 * Sum(|.w.| ExpSeq) by A18,A19,AXIOMS:22;
then A20:|.Partial_Sums(w ExpSeq).k
-Partial_Sums(w ExpSeq).(k-'l).|
<= 2 * Sum(|.w.| ExpSeq) by A17,AXIOMS:22;
0 <= (|.z .| ExpSeq).l by Th19;
hence
|.Conj(k,z,w).|.l <= (|.z .| ExpSeq).l * (2 * Sum(|.w.| ExpSeq))
by A16,A20,AXIOMS:25;
end;
hence for l be Nat st l <= k holds
|.Conj(k,z,w).|.l <= (|.z .| ExpSeq).l * (2 * Sum(|.w.| ExpSeq));
end;
now let k such that
A21: n4 <= k;
0 <= n3 by NAT_1:18;
then 0+n3 <= n3+n3 by AXIOMS:24;
then A22:n3 <= k by A21,AXIOMS:22;
0 <= n2 by NAT_1:18;
then A23: n1+0 <= n1+n2 by AXIOMS:24;
then A24:n1 <= k by A22,AXIOMS:22;
A25: Partial_Sums(|.Conj(k,z,w).|).k
=(Partial_Sums(|.Conj(k,z,w).|).k
-Partial_Sums(|.Conj(k,z,w).|).n3)
+Partial_Sums(|.Conj(k,z,w).|).n3 by XCMPLX_1:27;
now let l be Nat; assume
A26:l <= n3;
then A27:l <= k by A22,AXIOMS:22;
then A28:k-'l=k-l by SCMFSA_7:3;
0 <= n1 by NAT_1:18;
then A29: 0+n2 <= n1+n2 by AXIOMS:24;
A30: n4-l <= k-l by A21,REAL_1:49;
n3+n3-n3 <= n3+n3-l by A26,REAL_2:106;
then n3 <= n3+n3-l by XCMPLX_1:26;
then n3 <= k-l by A30,AXIOMS:22;
then A31:n2 <= k-'l by A28,A29,AXIOMS:22;
0 <= n3 by NAT_1:18;
then 0+n3 <= n3+n3 by AXIOMS:24;
then n2 <= n4 by A29,AXIOMS:22;
then n2 <= k by A21,AXIOMS:22;
then A32: |.Partial_Sums(( w ExpSeq )).k
- Partial_Sums(( w ExpSeq )).(k-'l).|
< p1 by A12,A31;
0 <= (|.z .| ExpSeq).l by Th19;
then (|.z .| ExpSeq).l * |.Partial_Sums(( w ExpSeq )).k
- Partial_Sums(( w ExpSeq )).(k-'l).|
<= (|.z .| ExpSeq).l * p1 by A32,AXIOMS:25;
hence |.Conj(k,z,w).|.l <= p1 * (|.z .| ExpSeq).l by A13,A27;
end;
then A33:Partial_Sums(|.Conj(k,z,w).|).n3
<= Partial_Sums(|.z .| ExpSeq).n3 * p1 by COMSEQ_3:7;
Partial_Sums(|.z .| ExpSeq).n3 <= Sum(|.z.| ExpSeq) by Th17;
then Partial_Sums(|.z .| ExpSeq).n3 * p1
<= Sum(|.z.| ExpSeq) * p1 by A8,AXIOMS:25;
then A34: Partial_Sums(|.Conj(k,z,w).|).n3
<= Sum(|.z.| ExpSeq) * p1 by A33,AXIOMS:22;
A35: Sum(|.z.| ExpSeq) * p1 <= Sum(|.z.| ExpSeq) * (p/(4 * Sum
(|.z.| ExpSeq)))
by A4,A9,AXIOMS:25;
A36: 0 <> Sum(|.z.| ExpSeq) & 4 <>0 by Th18;
Sum(|.z.| ExpSeq) * (p/(4 * Sum(|.z.| ExpSeq)))
=Sum(|.z.| ExpSeq) * (p * (4 * Sum(|.z.| ExpSeq))") by XCMPLX_0:def 9
.=(Sum(|.z.| ExpSeq) * p) * (4 * Sum(|.z.| ExpSeq))" by XCMPLX_1:4
.=(Sum(|.z.| ExpSeq) * p)/(4 * Sum(|.z.| ExpSeq)) by XCMPLX_0:def 9
.=p/4 by A36,XCMPLX_1:92;
then A37:Partial_Sums(|.Conj(k,z,w).|).n3 <= p/4 by A34,A35,AXIOMS:22;
0 < p/4 & 0 < p/2 by A1,SEQ_2:3;
then 0+p/4 < p/4 + p/4 by REAL_1:53;
then p/4 < p/2 by XCMPLX_1:72;
then A38: Partial_Sums(|.Conj(k,z,w).|).n3
< p/2 by A37,AXIOMS:22;
k-'n3=k-n3 by A22,SCMFSA_7:3;
then A39:k=(k-'n3)+n3 by XCMPLX_1:27;
for l be Nat st l <= k holds
|.Conj(k,z,w).|.l <= (2 * Sum(|.w.| ExpSeq)) * (|.z .| ExpSeq).l
by A15;
then A40:Partial_Sums(|.Conj(k,z,w).|).(k)
-Partial_Sums(|.Conj(k,z,w).|).n3
<= (Partial_Sums(|.z .| ExpSeq).(k)
-Partial_Sums(|.z .| ExpSeq).n3)
* (2 * Sum(|.w.| ExpSeq)) by A22,A39,COMSEQ_3:8;
abs((Partial_Sums(|.z .| ExpSeq).k-Partial_Sums(|.z .| ExpSeq).n3))
<= p1 by A11,A23,A24;
then A41:
Partial_Sums(|.z .| ExpSeq).k-Partial_Sums(|.z .| ExpSeq).n3
<= p1 by A22,Th20;
A42:0 * Sum(|.w.| ExpSeq) < 2 * Sum(|.w.| ExpSeq) by A6,REAL_1:70;
then (Partial_Sums(|.z .| ExpSeq).k -Partial_Sums(|.z .| ExpSeq).n3)
* (2 * Sum(|.w.| ExpSeq))
<= p1 * (2 * Sum(|.w.| ExpSeq)) by A41,AXIOMS:25;
then A43:
Partial_Sums(|.Conj(k,z,w).|).k-Partial_Sums(|.Conj(k,z,w).|).n3
<= p1 * (2 * Sum(|.w.| ExpSeq)) by A40,AXIOMS:22;
A44:
(2 * Sum(|.w.| ExpSeq)) * p1
<= (2 * Sum(|.w.| ExpSeq)) * (p/(4 * Sum(|.w.| ExpSeq)))
by A9,A42,AXIOMS:25;
A45:
0 <> Sum(|.w.| ExpSeq) & 4 <>0 by Th18;
(2 * Sum(|.w.| ExpSeq) ) * (p/(4 * Sum(|.w.| ExpSeq)))
=(2 * Sum(|.w.| ExpSeq) ) * (p * (4 * Sum
(|.w.| ExpSeq))") by XCMPLX_0:def 9
.=((2 * Sum(|.w.| ExpSeq) ) * p ) * (4 * Sum
(|.w.| ExpSeq))" by XCMPLX_1:4
.=((2 * Sum(|.w.| ExpSeq) ) * p ) /(4 * Sum
(|.w.| ExpSeq)) by XCMPLX_0:def 9
.=((2 * p ) * Sum(|.w.| ExpSeq) ) /(4 * Sum(|.w.| ExpSeq)) by XCMPLX_1:
4
.= (2 * p )/4 by A45,XCMPLX_1:92
.= (p +p )/4 by XCMPLX_1:11
.= p/2 by XCMPLX_1:73;
then Partial_Sums(|.Conj(k,z,w).|).k-Partial_Sums(|.Conj(k,z,w).|).n3
<= p/2 by A43,A44,AXIOMS:22;
then (Partial_Sums(|.Conj(k,z,w).|).k
-Partial_Sums(|.Conj(k,z,w).|).n3)
+Partial_Sums(|.Conj(k,z,w).|).n3 < (p/2)+(p/2) by A38,REAL_1:67;
then Partial_Sums(|.Conj(k,z,w).|).k < p by A25,XCMPLX_1:66;
hence
abs(Partial_Sums(|.Conj(k,z,w).|).k) < p by Th21;
end;
hence for k st n4 <= k
holds abs(Partial_Sums(|.Conj(k,z,w).|).k) < p;
end;
theorem Th23:
for seq st for k holds seq.k=Partial_Sums((Conj(k,z,w))).k
holds seq is convergent & lim(seq)=0c
proof
now let seq such that
A1:for k holds seq.k=Partial_Sums((Conj(k,z,w))).k;
A2: now let k;
|.seq.k.|=|.Partial_Sums((Conj(k,z,w))).k.| by A1;
hence
|.seq.k.| <= Partial_Sums(|.Conj(k,z,w).|).k by COMSEQ_3:30;
end;
deffunc U(Nat) = Partial_Sums(|.Conj($1,z,w).|).$1;
ex rseq be Real_Sequence st for k
holds rseq.k = U(k) from ExRealSeq;
then consider rseq be Real_Sequence such that
A3: for k holds rseq.k=Partial_Sums(|.Conj(k,z,w).|).k;
A4: now let k;
|.seq.k.| <= Partial_Sums(|.Conj(k,z,w).|).k by A2;
hence |.seq.k.| <= rseq.k by A3;
end;
rseq is convergent & lim(rseq) =0
proof
A5:now let p be real number;
assume p>0;
then consider n such that
A6:for k st n <= k
holds abs(Partial_Sums(|.Conj(k,z,w).|).k) < p by Th22;
take n;
now let k such that
A7: n <= k;
abs(rseq.k-0)=abs(Partial_Sums(|.Conj(k,z,w).|).k) by A3;
hence abs(rseq.k-0) < p by A6,A7;
end;
hence for k st n <= k holds abs(rseq.k-0) < p;
end;
hence rseq is convergent by SEQ_2:def 6;
hence lim(rseq)=0 by A5,SEQ_2:def 7;
end;
hence seq is convergent & lim(seq)=0c by A4,COMSEQ_3:48;
end;
hence thesis;
end;
Lm4:
Sum(z ExpSeq) * Sum(w ExpSeq) = Sum((z+w) ExpSeq)
proof deffunc U(Nat) = Partial_Sums(Conj($1,z,w)).$1;
ex seq st
for k holds seq.k= U(k) from ExComplexSeq;
then consider seq such that
A1: for k holds seq.k=Partial_Sums(Conj(k,z,w)).k;
now let k;
thus seq.k=Partial_Sums(Conj(k,z,w)).k by A1
.=Partial_Sums(z ExpSeq).k * Partial_Sums(w ExpSeq).k
-Partial_Sums((z+w) ExpSeq).k by Th16
.=(Partial_Sums(z ExpSeq) (#) Partial_Sums(w ExpSeq)).k
-Partial_Sums((z+w) ExpSeq).k by COMSEQ_1:def 5
.=(Partial_Sums(z ExpSeq) (#) Partial_Sums(w ExpSeq)).k
+(-Partial_Sums((z+w) ExpSeq).k) by XCMPLX_0:def 8
.=(Partial_Sums(z ExpSeq) (#) Partial_Sums(w ExpSeq)).k
+(-Partial_Sums((z+w) ExpSeq)).k by COMSEQ_1:def 9
.=(Partial_Sums(z ExpSeq) (#) Partial_Sums(w ExpSeq)
+(-Partial_Sums((z+w) ExpSeq))).k by COMSEQ_1:def 4
.=(Partial_Sums(z ExpSeq) (#) Partial_Sums(w ExpSeq)
-Partial_Sums((z+w) ExpSeq) ).k by COMSEQ_1:def 10;
end;
then A2: seq=Partial_Sums(z ExpSeq) (#) Partial_Sums(w ExpSeq)
-Partial_Sums((z+w) ExpSeq) by COMSEQ_1:6;
A3: Partial_Sums(z ExpSeq) (#) Partial_Sums(w ExpSeq) is convergent &
lim(Partial_Sums(z ExpSeq) (#) Partial_Sums(w ExpSeq))
=lim(Partial_Sums(z ExpSeq)) * lim(Partial_Sums(w ExpSeq))
by COMSEQ_2:29,30;
A4: seq is convergent & lim(seq)=0c by A1,Th23;
thus Sum((z+w) ExpSeq)
=lim(Partial_Sums((z+w) ExpSeq)) by COMSEQ_3:def 8
.=lim(Partial_Sums(z ExpSeq)) * lim(Partial_Sums(w ExpSeq))
by A2,A3,A4,COMSEQ_3:10
.=Sum(z ExpSeq) * lim(Partial_Sums(w ExpSeq))
by COMSEQ_3:def 8
.=Sum(z ExpSeq) * Sum(w ExpSeq) by COMSEQ_3:def 8;
end;
begin ::Definition of Exponential Function on Complex
definition
func exp -> PartFunc of COMPLEX, COMPLEX means :Def18:
dom it= COMPLEX & for z being Element of COMPLEX holds it.z=Sum(z ExpSeq);
existence
proof
defpred X[set] means $1 in COMPLEX;
deffunc U(Element of COMPLEX) = Sum($1 ExpSeq);
consider f being PartFunc of COMPLEX, COMPLEX such that
A1: for z be Element of COMPLEX holds z in dom f iff X[z] and
A2: for z be Element of COMPLEX st z in dom f holds f/.z = U(z)
from LambdaPFD;
take f;
dom(f)=COMPLEX
&for z be Element of COMPLEX holds f.z = Sum(z ExpSeq)
proof
A3: dom(f)=COMPLEX
proof
A4: dom(f) c=COMPLEX by RELSET_1:12;
for x be set st x in COMPLEX holds x in dom f by A1;
then COMPLEX c=dom(f) by TARSKI:def 3;
hence dom(f)=COMPLEX by A4,XBOOLE_0:def 10;
end;
for z be Element of COMPLEX holds f.z = Sum(z ExpSeq)
proof
let z be Element of COMPLEX;
A5: z in dom f by A1;
then f/.z = Sum(z ExpSeq) by A2;
hence f.z = Sum(z ExpSeq) by A5,FINSEQ_4:def 4;
end;
hence thesis by A3;
end;
hence thesis;
end;
uniqueness
proof
let f1,f2 be PartFunc of COMPLEX, COMPLEX;
assume
A6: dom f1= COMPLEX & for z being Element of COMPLEX
holds f1.z=Sum(z ExpSeq);
assume
A7: dom f2= COMPLEX & for z being Element of COMPLEX
holds f2.z=Sum(z ExpSeq);
for z being Element of COMPLEX st z in COMPLEX holds f1.z = f2.z
proof
let z be Element of COMPLEX such that
z in COMPLEX;
thus f1.z=Sum(z ExpSeq) by A6
.=f2.z by A7;
end;
hence f1=f2 by A6,A7,PARTFUN1:34;
end;
end;
definition let z;
func exp z -> Element of COMPLEX equals:Def19:
exp.z;
correctness
proof
exp.z=Sum(z ExpSeq) by Def18;
hence exp.z is Element of COMPLEX;
end;
end;
Lm5:
for z holds exp(z)=Sum(z ExpSeq)
proof
let z;
thus exp(z)=exp.(z) by Def19
.=Sum(z ExpSeq) by Def18;
end;
theorem
for z1, z2 holds exp(z1+z2)=exp(z1) *exp(z2)
proof
let z1,z2;
exp(z1+z2)= exp.(z1+z2) by Def19
.=Sum((z1+z2) ExpSeq) by Def18
.=Sum(z1 ExpSeq)*Sum(z2 ExpSeq) by Lm4
.=exp(z1)*Sum(z2 ExpSeq) by Lm5
.=exp(z1) *exp(z2) by Lm5;
hence thesis;
end;
begin ::Definition of Sinus, Cosine, and Exponential Function on REAL
definition
func sin -> PartFunc of REAL, REAL means :Def20:
dom it = REAL & for d being Element of REAL holds it.d=Im(Sum([*0,d*]
ExpSeq));
existence
proof
defpred X[set] means $1 in REAL;
deffunc U(Element of REAL) = Im(Sum([*0,$1*] ExpSeq));
consider f being PartFunc of REAL, REAL such that
A1: for d be Element of REAL holds d in dom f iff X[d] and
A2: for d be Element of REAL st d in dom f holds f/.d = U(d)
from LambdaPFD;
take f;
dom(f)=REAL
&for d be Element of REAL holds f.d = Im(Sum([*0,d*]
ExpSeq))
proof
A3: dom(f)=REAL
proof
A4: dom(f) c=REAL by RELSET_1:12;
for x be set st x in REAL holds x in dom f by A1;
then REAL c=dom(f) by TARSKI:def 3;
hence dom(f)=REAL by A4,XBOOLE_0:def 10;
end;
for d be Element of REAL holds f.d = Im(Sum([*0,d*] ExpSeq))
proof
let d be Element of REAL;
A5: d in dom f by A1;
then f/.d = Im(Sum([*0,d*] ExpSeq)) by A2;
hence thesis by A5,FINSEQ_4:def 4;
end;
hence thesis by A3;
end;
hence thesis;
end;
uniqueness
proof
let f1,f2 be PartFunc of REAL, REAL;
assume
A6: dom f1= REAL & for d being Element of REAL
holds f1.d=Im(Sum([*0,d*] ExpSeq));
assume
A7: dom f2= REAL & for d being Element of REAL
holds f2.d=Im(Sum([*0,d*] ExpSeq));
for d being Element of REAL st d in REAL holds f1.d = f2.d
proof
let d be Element of REAL such that
d in REAL;
thus f1.d=Im(Sum([*0,d*] ExpSeq)) by A6
.=f2.d by A7;
end;
hence f1=f2 by A6,A7,PARTFUN1:34;
end;
end;
definition let th be real number;
func sin th equals:Def21:
sin.th;
correctness;
end;
definition
let th be real number;
cluster sin th -> real;
correctness
proof
sin th = sin.th by Def21;
hence thesis;
end;
end;
definition let th be Real;
redefine func sin th -> Real;
correctness by XREAL_0:def 1;
end;
theorem
sin is Function of REAL,REAL
proof
sin is PartFunc of REAL,REAL & dom sin=REAL by Def20;
hence thesis by FUNCT_2:130;
end;
reserve d for Real;
definition
func cos -> PartFunc of REAL, REAL means :Def22:
dom it= REAL & for d holds it.d=Re(Sum([*0,d*] ExpSeq));
existence
proof
defpred X[set] means $1 in REAL;
deffunc U(Element of REAL) = Re(Sum([*0,$1*] ExpSeq));
consider f being PartFunc of REAL, REAL such that
A1: for d holds d in dom f iff X[d] and
A2: for d st d in dom f holds f/.d = U(d) from LambdaPFD;
take f;
dom(f)=REAL
&for d holds f.d = Re(Sum([*0,d*] ExpSeq))
proof
A3: dom(f)=REAL
proof
A4: dom(f) c=REAL by RELSET_1:12;
for x be set st x in REAL holds x in dom f by A1;
then REAL c=dom(f) by TARSKI:def 3;
hence dom(f)=REAL by A4,XBOOLE_0:def 10;
end;
for d holds f.d = Re(Sum([*0,d*] ExpSeq))
proof
let d;
A5: d in dom f by A1;
then f/.d = Re(Sum([*0,d*] ExpSeq)) by A2;
hence thesis by A5,FINSEQ_4:def 4;
end;
hence thesis by A3;
end;
hence thesis;
end;
uniqueness
proof
let f1,f2 be PartFunc of REAL, REAL;
assume
A6: dom f1= REAL & for d holds f1.d=Re(Sum([*0,d*] ExpSeq));
assume
A7: dom f2= REAL & for d holds f2.d=Re(Sum([*0,d*] ExpSeq));
for d st d in REAL holds f1.d = f2.d
proof
let d such that d in REAL;
thus f1.d=Re(Sum([*0,d*] ExpSeq)) by A6
.=f2.d by A7;
end;
hence f1=f2 by A6,A7,PARTFUN1:34;
end;
end;
definition let th be real number;
func cos th equals:Def23:
cos.th;
correctness;
end;
definition
let th be real number;
cluster cos th -> real;
correctness
proof
cos th = cos.th by Def23;
hence thesis;
end;
end;
definition let th be Real;
redefine func cos th -> Real;
correctness by XREAL_0:def 1;
end;
theorem
cos is Function of REAL,REAL
proof
cos is PartFunc of REAL,REAL & dom cos=REAL by Def22;
hence thesis by FUNCT_2:130;
end;
theorem Th27: dom(sin)=REAL & dom(cos)=REAL by Def20,Def22;
Lm6:Sum([*0,th*] ExpSeq )=[*cos.(th),sin.(th)*]
proof
A1:Im(Sum([*0,th*] ExpSeq))=sin.(th) by Def20;
Re(Sum([*0,th*] ExpSeq))=cos.(th) by Def22;
hence thesis by A1,COMPLEX1:8;
end;
theorem
exp([*0,th*])=[*cos(th),sin(th)*]
proof
exp([*0,th*])=Sum([*0,th*] ExpSeq ) by Lm5
.=[*cos.(th),sin.(th)*] by Lm6
.=[*cos(th),sin.(th)*] by Def23
.=[*cos(th),sin(th)*] by Def21;
hence thesis;
end;
Lm7:
(Sum([*0,th*] ExpSeq))*' = Sum((-[*0,th*]) ExpSeq)
proof
A1:
Partial_Sums(([*0,th*] ExpSeq))*'
=Partial_Sums((-[*0,th*]) ExpSeq)
proof
A2:for n holds (([*0,th*] ExpSeq).n)*' = ((-[*0,th*]) ExpSeq).n
proof
defpred X[Nat] means (([*0,th*] ExpSeq).$1)*' = ((-[*0,th*]) ExpSeq).$1;
(([*0,th*] ExpSeq).0)*'
=1r by Th4,COMPLEX1:115
.=((-[*0,th*]) ExpSeq).0 by Th4;
then
A3: X[0];
A4: for n st X[n] holds X[n+1]
proof let n;
assume
A5:(([*0,th*] ExpSeq).n)*' = ((-[*0,th*]) ExpSeq).n;
thus
(([*0,th*] ExpSeq).(n+1))*'
=(([*0,th*] ExpSeq).n * [*0,th*]/[*(n+1),0*])*' by Th4
.=(([*0,th*] ExpSeq).n * ([*0,th*]/[*(n+1),0*]))*'
by XCMPLX_1:75
.=((-[*0,th*]) ExpSeq).n * ([*0,th*]/[*(n+1),0*])*' by A5,COMPLEX1:121
.=((-[*0,th*]) ExpSeq).n * (([*0,th*])*'/([*(n+1),0*])*')
by COMPLEX1:123
.=((-[*0,th*]) ExpSeq).n * ([*0,-th*] /([*(n+1),0*])*') by Lm3
.=((-[*0,th*]) ExpSeq).n * ([*0,-th*]/[*(n+1),-0*]) by Lm3
.=((-[*0,th*]) ExpSeq).n *( (-[*0, th*])/[*(n+1),0*]) by Lm3
.=((-[*0,th*]) ExpSeq).n * (-[*0, th*])/[*(n+1),0*] by XCMPLX_1:75
.=((-[*0,th*]) ExpSeq).(n+1) by Th4;
end;
thus for n holds X[n] from Ind(A3,A4);
end;
defpred X[Nat] means (Partial_Sums(([*0,th*] ExpSeq))*').$1
=Partial_Sums((-[*0,th*]) ExpSeq).$1;
(Partial_Sums([*0,th*] ExpSeq)*').0
=(Partial_Sums([*0,th*] ExpSeq).0)*' by COMSEQ_2:def 2
.=(([*0,th*] ExpSeq).0)*' by COMSEQ_3:def 7
.=1r by Th4,COMPLEX1:115
.=((-[*0,th*]) ExpSeq).0 by Th4
.=Partial_Sums((-[*0,th*]) ExpSeq).0 by COMSEQ_3:def 7;
then
A6: X[0];
A7: for n st X[n] holds X[n+1]
proof let n such that
A8: (Partial_Sums(([*0,th*] ExpSeq))*').n
=Partial_Sums((-[*0,th*]) ExpSeq).n;
thus (Partial_Sums([*0,th*] ExpSeq)*').(n+1)
=(Partial_Sums([*0,th*] ExpSeq).(n+1))*' by COMSEQ_2:def 2
.=(Partial_Sums([*0,th*] ExpSeq).n+([*0,th*] ExpSeq).(n+1))*'
by COMSEQ_3:def 7
.=(Partial_Sums([*0,th*] ExpSeq).n)*'+(([*0,th*] ExpSeq).(n+1))*'
by COMPLEX1:118
.=Partial_Sums((-[*0,th*]) ExpSeq).n+(([*0,th*] ExpSeq).(n+1))*'
by A8,COMSEQ_2:def 2
.=Partial_Sums((-[*0,th*]) ExpSeq).n+((-[*0,th*]) ExpSeq).(n+1) by A2
.=Partial_Sums((-[*0,th*]) ExpSeq).(n+1) by COMSEQ_3:def 7;
end;
for n holds X[n] from Ind(A6,A7);
hence thesis by COMSEQ_1:6;
end;
thus (Sum([*0,th*] ExpSeq))*'
=(lim(Partial_Sums([*0,th*] ExpSeq)))*' by COMSEQ_3:def 8
.= lim(Partial_Sums((-[*0,th*]) ExpSeq)) by A1,COMSEQ_2:12
.= Sum((-[*0,th*]) ExpSeq) by COMSEQ_3:def 8;
end;
theorem
(exp([*0,th*]))*'=exp(-[*0,th*])
proof
(exp([*0,th*]))*'=(Sum([*0,th*] ExpSeq))*' by Lm5
.=Sum((-[*0,th*]) ExpSeq) by Lm7
.=exp(-[*0,th*]) by Lm5;
hence thesis;
end;
Lm8:
|.Sum([*0,th*] ExpSeq ).| = 1 & abs(sin.th) <= 1 & abs(cos.th) <= 1
proof
A1: Sum([*0,th*] ExpSeq ) * Sum((-[*0,th*]) ExpSeq )
=Sum(([*0,th*]+(-[*0,th*])) ExpSeq ) by Lm4
.=1r by Th10,XCMPLX_0:def 6;
A2: |.Sum([*0,th*] ExpSeq ).| * |.Sum([*0,th*] ExpSeq ).|
=|.Sum([*0,th*] ExpSeq )*Sum([*0,th*] ExpSeq ).| by COMPLEX1:151
.=|.Sum([*0,th*] ExpSeq ) * Sum([*0,th*] ExpSeq)*'.| by COMPLEX1:155
.=1 by A1,Lm7,COMPLEX1:134;
thus
A3: |.Sum([*0,th*] ExpSeq ).|=1
proof
A4: |.Sum([*0,th*] ExpSeq ).| =1/|.Sum([*0,th*] ExpSeq ).| by A2,XCMPLX_1:74
;
A5: |.Sum([*0,th*] ExpSeq ).| <> 0 by A2;
|.Sum([*0,th*] ExpSeq ).| <> -1 by COMPLEX1:132;
hence |.Sum([*0,th*] ExpSeq ).|=1 by A4,A5,XCMPLX_1:200;
end;
A6:abs(sin.th)=abs(Im(Sum([*0,th*] ExpSeq ))) by Def20;
abs(cos.th)=abs(Re(Sum([*0,th*] ExpSeq ))) by Def22;
hence thesis by A3,A6,COMSEQ_3:13;
end;
theorem
|.exp([*0,th*]).| = 1 & abs(sin th) <= 1 & abs(cos th) <= 1
proof
thus |.exp([*0,th*]).| =|.Sum([*0,th*] ExpSeq ).| by Lm5
.=1 by Lm8;
abs(sin.th) <= 1 by Lm8;
hence abs(sin(th)) <= 1 by Def21;
abs(cos.th) <= 1 by Lm8;
hence abs(cos(th)) <= 1 by Def23;
end;
theorem Th31:
(cos.(th))^2+(sin.(th))^2=1
&
(cos.(th))*(cos.(th))+(sin.(th))*(sin.(th))=1
proof
A1: Sum([*0,th*] ExpSeq ) * Sum((-[*0,th*]) ExpSeq )
=Sum(([*0,th*]+(-[*0,th*])) ExpSeq ) by Lm4
.=1r by Th10,XCMPLX_0:def 6;
thus A2: (cos.(th))^2+(sin.(th))^2
=(Re(Sum([*0,th*] ExpSeq )))^2+(sin.(th))^2 by Def22
.=(Re(Sum([*0,th*] ExpSeq )))^2+(Im(Sum([*0,th*] ExpSeq )))^2 by Def20
.=|.Sum([*0,th*] ExpSeq )*Sum([*0,th*] ExpSeq ).| by COMPLEX1:154
.=|.Sum([*0,th*] ExpSeq ) * Sum([*0,th*] ExpSeq)*'.| by COMPLEX1:155
.=1 by A1,Lm7,COMPLEX1:134;
thus (cos.(th))*(cos.(th))+(sin.(th))*(sin.(th))
=(cos.(th))^2 +(sin.(th))*(sin.(th)) by SQUARE_1:def 3
.=1 by A2,SQUARE_1:def 3;
end;
theorem
(cos(th))^2+(sin(th))^2=1
&
(cos(th))*(cos(th))+(sin(th))*(sin(th))=1
proof
thus (cos(th))^2+(sin(th))^2=(cos(th))^2+(sin.(th))^2 by Def21
.=(cos.(th))^2+(sin.(th))^2 by Def23
.=1 by Th31;
thus (cos(th))*(cos(th))+(sin(th))*(sin(th))=
(cos.(th))*(cos(th))+(sin(th))*(sin(th)) by Def23
.=(cos.(th))*(cos.(th))+(sin(th))*(sin(th)) by Def23
.=(cos.(th))*(cos.(th))+(sin.(th))*(sin(th)) by Def21
.=(cos.(th))*(cos.(th))+(sin.(th))*(sin.(th)) by Def21
.=1 by Th31;
end;
L0: 0c = [*0,0*] by ARYTM_0:def 7;
theorem Th33:
cos.(0)=1 & sin.(0)=0
&
cos.(-th)=cos.(th) & sin.(-th)=-sin.(th)
proof
thus cos.(0) = 1 by Def22,Th10,COMPLEX1:15,L0;
thus
sin.(0) = 0 by Def20,Th10,COMPLEX1:15,L0;
thus cos.(-th)=Re( Sum(([*-0,-th*]) ExpSeq) ) by Def22
.= Re( Sum((-[*0,th*]) ExpSeq) ) by Lm3
.= Re(Sum([*0,th*] ExpSeq)*') by Lm7
.= Re([*cos.(th),sin.(th)*]*') by Lm6
.= Re([*cos.(th),-sin.(th)*]) by Lm3
.= cos.(th) by COMPLEX1:7;
thus sin.(-th)=Im( Sum(([*-0,-th*]) ExpSeq) ) by Def20
.= Im( Sum((-[*0,th*]) ExpSeq) ) by Lm3
.= Im(Sum([*0,th*] ExpSeq)*') by Lm7
.= Im([*cos.(th),sin.(th)*]*') by Lm6
.= Im([*cos.(th),-sin.(th)*]) by Lm3
.= -sin.(th) by COMPLEX1:7;
end;
theorem
cos(0)=1 & sin(0)=0 &
cos(-th)=cos(th) & sin(-th)=-sin(th)
proof
thus cos(0)=1 & sin(0)=0 by Def21,Def23,Th33;
thus cos(-th)=cos.(-th) by Def23
.=cos.(th) by Th33
.=cos(th) by Def23;
thus sin(-th)=sin.(-th) by Def21
.=-sin.(th) by Th33
.=-sin(th) by Def21;
end;
definition let th be real number;
deffunc U(Nat) = (-1)|^ $1 * (th)|^ (2*$1+1)/((2*$1+1)!);
func th P_sin -> Real_Sequence means :Def24:
for n holds it.n= (-1)|^ n * (th)|^ (2*n+1)/((2*n+1)!);
existence
proof
thus ex s being Real_Sequence st
for n holds s.n = U(n) from ExRealSeq;
end;
uniqueness
proof
thus for s1,s2 being Real_Sequence st
(for x being Nat holds s1.x = U(x)) &
(for x being Nat holds s2.x = U(x)) holds s1 = s2
from FuncDefUniq;
end;
deffunc U(Nat) = (-1)|^ $1 * (th)|^ (2*$1)/((2*$1)!);
func th P_cos -> Real_Sequence means :Def25:
for n holds it.n = (-1)|^ n * (th)|^ (2*n)/((2*n)!);
existence
proof
thus ex s being Real_Sequence st
for n holds s.n = U(n) from ExRealSeq;
end;
uniqueness
proof
thus for s1,s2 being Real_Sequence st
(for x being Nat holds s1.x = U(x)) &
(for x being Nat holds s2.x = U(x)) holds s1 = s2
from FuncDefUniq;
end;
end;
Lm9: for p,q,r st r<>0 holds
[*p,q*]/[*r,0*]=[*p/r,q/r*]& [*p,q*]/[*0,r*]=[*q/r,-p/r*]
proof
let p,q,r;
assume
A1: r<>0;
A2: Re[*p,q*]=p & Im[*p,q*]=q & Re[*r,0*]=r & Im[*r,0*]=0 &
Re[*0,r*]=0 & Im[*0,r*]=r by COMPLEX1:7;
then A3: [*p,q*]/[*r,0*]=
[* (p* r + q* 0) / ((r)^2+ (0)^2),(r * q - p* 0)/((r)^2 +(0)^2)*]
by COMPLEX1:def 14
.=[* (p* r ) / (r*r),(r * q )/((r)^2)*] by SQUARE_1:60,def 3
.=[* (p* r ) / (r*r),(r * q )/(r*r)*] by SQUARE_1:def 3
.=[* p / r,(r * q )/(r*r)*] by A1,XCMPLX_1:92
.= [* p / r, q /r *] by A1,XCMPLX_1:92;
[*p,q*]/[*0,r*]
=[* (p*0+q*r)/ ((0)^2+ (r)^2),(0*q - p*r) /((0)^2+ (r)^2) *]
by A2,COMPLEX1:def 14
.=[* (q*r)/ ((0)^2+ (r)^2),(- p*r) /((0)^2+ (r)^2) *] by XCMPLX_1:150
.=[* (q*r)/ (r*r),(- p*r) /((r)^2) *] by SQUARE_1:60,def 3
.=[* (q*r)/ (r*r),(- p*r) /(r*r) *] by SQUARE_1:def 3
.=[* q/ r,(- p*r) /(r*r) *] by A1,XCMPLX_1:92
.=[* q/ r,((- p)*r) /(r*r) *] by XCMPLX_1:175
.=[* q/ r,(- p) /r *] by A1,XCMPLX_1:92
.=[* q/ r,- p/r *] by XCMPLX_1:188;
hence thesis by A3;
end;
Lm10: [*p,q*]*[*r,0*]=[*p*r,q*r*]&
[*p,q*]*[*0,r*]=[*-q*r,p*r*]
proof
A1: Re[*p,q*]=p & Im[*p,q*]=q& Re[*r,0*]=r & Im[*r,0*]=0 &
Re[*0,r*]=0 & Im[*0,r*]=r by COMPLEX1:7;
then A2: [*p,q*]*[*r,0*]= [*p*r-q*0, p*0+ r*q*] by COMPLEX1:def 10
.=[*p*r,q*r*];
[*p,q*]*[*0,r*]=[* p*0-q*r, p*r+ q*0*] by A1,COMPLEX1:def 10
.=[* p*0+(-q*r), p*r+ q*0*] by XCMPLX_0:def 8
.=[*-q*r,p*r*];
hence thesis by A2;
end;
theorem Th35: for z, k holds z#N (2*k) = (z#N k)#N 2&
z#N (2*k)= (z#N 2)#N k
proof
let z,k;
defpred X[Nat] means z#N (2*$1) = (z#N $1)#N 2 & z#N (2*$1)= (z#N 2)#N $1;
A1: z#N (2*0)=1r by COMSEQ_3:11;
(z#N 0)#N 2 =(1r) #N 2 by COMSEQ_3:11
.=(1r)GeoSeq.(1+1) by COMSEQ_3:def 2
.=(1r)GeoSeq.(0+1)*(1r) by COMSEQ_3:def 1
.=(1r)GeoSeq.0*(1r)*(1r) by COMSEQ_3:def 1
.= (1r)*(1r)*(1r) by COMSEQ_3:def 1
.= (1r)*(1r) by COMPLEX1:29
.= 1r by COMPLEX1:29;
then A2: X[0] by A1,COMSEQ_3:11;
A3: for k st X[k] holds X[k+1]
proof
let k;
assume
A4: z#N (2*k) = (z#N k)#N 2 & z#N (2*k)= (z#N 2)#N k;
A5: z#N (2*(k+1))=z#N (2*k+2*1) by XCMPLX_1:8
.=z#N (2*k+(1+1))
.=z#N (2*k+1+1) by XCMPLX_1:1
.=z GeoSeq.(2*k+1+1) by COMSEQ_3:def 2
.=z GeoSeq.(2*k+1)*z by COMSEQ_3:def 1
.=z GeoSeq.(2*k)*z*z by COMSEQ_3:def 1
.=z#N (2*k)*z*z by COMSEQ_3:def 2;
then A6: z#N (2*(k+1)) =((z#N k)GeoSeq.(1+1))*z*z by A4,COMSEQ_3:def 2
.=((z#N k)GeoSeq.(0+1)*(z#N k))*z*z by COMSEQ_3:def 1
.=((z#N k)GeoSeq.0*(z#N k)*(z#N k))*z*z by COMSEQ_3:def 1
.=((1r)*(z#N k)*(z#N k))*z*z by COMSEQ_3:def 1
.=(1r)*(z#N k)*((z#N k)*z)*z by XCMPLX_1:4
.=(1r)*(z#N k)*z*((z#N k)*z) by XCMPLX_1:4
.=(1r)*((z#N k)*z)*((z#N k)*z) by XCMPLX_1:4
.=(1r)*(z GeoSeq.k*z)*((z#N k)*z) by COMSEQ_3:def 2
.=(1r)*(z GeoSeq.k*z)*(z GeoSeq.k*z) by COMSEQ_3:def 2
.=(1r)*(z GeoSeq.(k+1))*(z GeoSeq.k*z) by COMSEQ_3:def 1
.=(1r)*(z GeoSeq.(k+1))*(z GeoSeq.(k+1)) by COMSEQ_3:def 1
.=(1r)*(z#N(k+1))*(z GeoSeq.(k+1)) by COMSEQ_3:def 2
.=(1r)*(z#N(k+1))*(z#N(k+1)) by COMSEQ_3:def 2
.=((z#N(k+1))GeoSeq.0)*(z#N(k+1))*(z#N(k+1))
by COMSEQ_3:def 1
.=((z#N(k+1))GeoSeq.(0+1))*(z#N(k+1)) by COMSEQ_3:def 1
.=(z#N(k+1))GeoSeq.(0+1+1) by COMSEQ_3:def 1
.=(z#N(k+1))#N 2 by COMSEQ_3:def 2;
z#N (2*(k+1))=(z#N 2)#N k*(z*z) by A4,A5,XCMPLX_1:4
.= (z#N 2)#N k*(1r*z*z) by COMPLEX1:29
.= (z#N 2)#N k*(z GeoSeq.0 *z*z) by COMSEQ_3:def 1
.=(z#N 2)#N k*(z GeoSeq.(0+1) *z) by COMSEQ_3:def 1
.=(z#N 2)#N k*z GeoSeq.(0+1+1) by COMSEQ_3:def 1
.=(z#N 2)#N k*(z#N 2) by COMSEQ_3:def 2
.=(z#N 2)GeoSeq.k*(z#N 2) by COMSEQ_3:def 2
.=(z#N 2)GeoSeq.(k+1) by COMSEQ_3:def 1
.= (z#N 2)#N (k+1) by COMSEQ_3:def 2;
hence thesis by A6;
end;
for k holds X[k] from Ind(A2,A3);
hence thesis;
end;
L1: 1r = [*1,0*] by ARYTM_0:def 7,COMPLEX1:def 7;
theorem Th36:
for k, th holds [*0, th*] #N (2*k)=[*(-1)|^ k* (th |^ (2*k)),0*]
& [*0, th*] #N (2*k+1)=[*0,(-1)|^ k* (th |^ (2*k+1))*]
proof
let k, th;
A1: [*0, th*] #N (2*0)=[*0, th*] GeoSeq.0 by COMSEQ_3:def 2
.=[*1,0*] by COMSEQ_3:def 1,L1;
A2: [*(-1)|^ 0* (th |^ (2*0)),0*]=[*(-1)|^ 0* th GeoSeq.0,0*] by PREPOWER:def
1
.=[*(-1)|^ 0*(1),0*] by PREPOWER:4
.=[*(-1)GeoSeq.0,0*] by PREPOWER:def 1
.=[*1,0*] by PREPOWER:4;
A3: [*0, th*] #N (2*0+1)=[*0, th*] GeoSeq.(0+1) by COMSEQ_3:def 2
.=[*0, th*] GeoSeq.0*[*0,th*] by COMSEQ_3:def 1
.=[*1,0*]*[*0,th*] by COMSEQ_3:def 1,L1
.=[*-0* th,1*th*] by Lm10
.=[*0,th*];
defpred X[Nat] means [*0, th*] #N (2*$1)=[*(-1)|^ $1* (th |^ (2*$1)),0*]
& [*0, th*] #N (2*$1+1)=[*0,(-1)|^ $1* (th |^ (2*$1+1))*];
[*0,(-1)|^ 0 * (th |^ (2*0+1))*]=[*0,(-1)|^ 0 * (th GeoSeq.(2*0+1))*]
by PREPOWER:def 1
.= [*0,(-1)|^ 0* (th GeoSeq.0*th)*] by PREPOWER:4
.=[*0,(-1)|^ 0* (1*th)*] by PREPOWER:4
.= [*0,((-1)GeoSeq.0)* th *] by PREPOWER:def 1
.=[*0,(1)* th *] by PREPOWER:4
.=[*0,th*];
then A4: X[0] by A1,A2,A3;
A5: for k st X[k] holds X[k+1]
proof
let k;
assume
A6: [*0, th*] #N (2*k)=[*(-1)|^ k* (th |^ (2*k)),0*]
& [*0, th*] #N (2*k+1)=[*0,(-1)|^ k* (th |^ (2*k+1))*];
A7: [*0, th*] #N (2*(k+1))= ([*0, th*] #N 2)#N(k+1) by Th35
.=([*0, th*] #N 2) GeoSeq.(k+1) by COMSEQ_3:def 2
.=([*0, th*] #N 2) GeoSeq.k* ([*0, th*] #N 2)
by COMSEQ_3:def 1
.=([*0, th*] #N 2)#N k * ([*0, th*] #N 2)
by COMSEQ_3:def 2
.= [*(-1)|^ k* (th |^ (2*k)),0*]* ([*0, th*] #N 2)
by A6,Th35
.= [*(-1)|^ k* (th |^ (2*k)),0*]* ([*0, th*]GeoSeq.(1+1))
by COMSEQ_3:def 2
.=[*(-1)|^ k* (th |^ (2*k)),0*]*
([*0, th*]GeoSeq.(0+1)*[*0, th*])
by COMSEQ_3:def 1
.=[*(-1)|^ k* (th |^ (2*k)),0*]* ([*0, th*]GeoSeq.0*[*0, th*]
*[*0, th*]) by COMSEQ_3:def 1
.= [*(-1)|^ k* (th |^ (2*k)),0*]* (1r*[*0, th*]*[*0, th*])
by COMSEQ_3:def 1
.= [*(-1)|^ k* (th |^ (2*k)),0*]*([*0, th*]*[*0, th*])
by COMPLEX1:29
.= [*(-1)|^ k* (th |^ (2*k)),0*]* [*-th*th, 0*th*] by Lm10
.=[*(-1)|^ k* (th |^ (2*k))*(-th*th),0*(-th*th)*] by Lm10
.= [*(-1)|^ k* (th |^ (2*k))*((-1)*(th*th)),0*] by XCMPLX_1:180
.= [*(-1)|^ k* (th |^ (2*k))*(-1)*(th*th),0*] by XCMPLX_1:4
.= [*(-1)|^ k* (th |^ (2*k))*(-1)*th*th,0*] by XCMPLX_1:4
.=[*(-1)|^ k*(-1)* (th |^ (2*k))*th*th,0*] by XCMPLX_1:4
.=[*(-1)GeoSeq.k*(-1)* (th |^ (2*k))*th*th,0*]
by PREPOWER:def 1
.=[*(-1)GeoSeq.(k+1)* (th |^ (2*k))*th*th,0*]
by PREPOWER:4
.=[*(-1)|^(k+1)* (th |^ (2*k))*th*th,0*] by PREPOWER:def 1
.=[*(-1)|^(k+1)* (th GeoSeq.(2*k))*th*th,0*]
by PREPOWER:def 1
.= [*(-1)|^(k+1)* (th GeoSeq.(2*k)*th)*th,0*] by XCMPLX_1:4
.=[*(-1)|^(k+1)* (th GeoSeq.(2*k+1))*th,0*] by PREPOWER:4
.=[*(-1)|^(k+1)* (th GeoSeq.(2*k+1)*th),0*] by XCMPLX_1:4
.=[*(-1)|^(k+1)* (th GeoSeq.(2*k+1+1)),0*] by PREPOWER:4
.=[*(-1)|^(k+1)* (th |^ (2*k+1+1)),0*] by PREPOWER:def 1
.=[*(-1)|^(k+1)* (th |^ (2*k+(1+1))),0*] by XCMPLX_1:1
.=[*(-1)|^(k+1)* (th |^ (2*k+2*1)),0*]
.=[*(-1)|^(k+1)* (th |^ (2*(k+1))),0*] by XCMPLX_1:8;
[*0, th*] #N (2*(k+1)+1)=[*0, th*] #N (2*k+2*1+1) by XCMPLX_1:8
.=[*0, th*] #N (2*k+(1+1)+1)
.=[*0, th*] #N (2*k+1+1+1) by XCMPLX_1:1
.=[*0, th*]GeoSeq.(2*k+1+1+1) by COMSEQ_3:def 2
.=[*0, th*]GeoSeq.(2*k+1+1)*[*0, th*] by COMSEQ_3:def 1
.=[*0, th*]GeoSeq.(2*k+1)*[*0, th*]*[*0, th*] by COMSEQ_3:def 1
.=[*0, th*]GeoSeq.(2*k+1)*([*0, th*]*[*0, th*]) by XCMPLX_1:4
.=[*0, th*]GeoSeq.(2*k+1)* [*-th*th, 0*th*] by Lm10
.=[*0,(-1)|^ k* (th |^ (2*k+1))*]* [*-th*th, 0*] by A6,COMSEQ_3:def 2
.=[*0* (-th*th),(-1)|^ k* (th |^ (2*k+1))* (-th*th)*] by Lm10
.=[*0,(-1)|^ k* (th |^ (2*k+1))* ((-1)*(th*th))*] by XCMPLX_1:180
.=[*0,(-1)|^ k* (th |^ (2*k+1))*(-1)*(th*th)*] by XCMPLX_1:4
.=[*0,(-1)|^ k* (th |^ (2*k+1))*(-1)*th*th*] by XCMPLX_1:4
.=[*0,(-1)|^ k*(-1)* (th |^ (2*k+1))*th*th*] by XCMPLX_1:4
.=[*0,(-1)GeoSeq.k*(-1)* (th |^ (2*k+1))*th*th*] by PREPOWER:def 1
.=[*0,(-1)GeoSeq.(k+1)* (th |^ (2*k+1))*th*th*] by PREPOWER:4
.=[*0,(-1)|^ (k+1)* (th |^ (2*k+1))*th*th*] by PREPOWER:def 1
.=[*0,(-1)|^ (k+1)* (th GeoSeq.(2*k+1))*th*th*] by PREPOWER:def 1
.=[*0,(-1)|^ (k+1)* (th GeoSeq.(2*k+1)*th)*th*] by XCMPLX_1:4
.=[*0,(-1)|^ (k+1)* (th GeoSeq.(((2*k+1)+1)))*th*] by PREPOWER:4
.=[*0,(-1)|^ (k+1)* (th GeoSeq.((2*k+1+1))*th)*] by XCMPLX_1:4
.=[*0,(-1)|^ (k+1)* (th GeoSeq.((2*k+1+1)+1))*] by PREPOWER:4
.=[*0,(-1)|^ (k+1)* (th GeoSeq.((2*k+(1+1))+1))*] by XCMPLX_1:1
.=[*0,(-1)|^ (k+1)* (th GeoSeq.(2*k+2*1+1))*]
.= [*0,(-1)|^ (k+1)* (th GeoSeq.(2*(k+1)+1))*] by XCMPLX_1:8
.=[*0,(-1)|^ (k+1)*(th |^ (2*(k+1)+1))*] by PREPOWER:def 1;
hence thesis by A7;
end;
for k holds X[k] from Ind(A4,A5);
hence thesis;
end;
theorem Th37: for n holds n!c=[*n!,0*]
proof
defpred X[Nat] means $1!c=[*$1!,0*];
A1: X[0] by Th1,NEWTON:18,ARYTM_0:def 7,COMPLEX1:def 7;
A2: for k st X[k] holds X[k+1]
proof
let k be Nat;
assume k!c=[*k!,0*]; hence
(k+1)!c=[*k!,0*]*[*(k+1),0*] by Th1
.=[*k!*(k+1), 0*(k+1)*] by Lm10
.=[*(k+1)!,0*] by NEWTON:21;
end;
thus for k holds X[k] from Ind(A1,A2);
end;
theorem Th38:for th, n holds
Partial_Sums(th P_sin).n = Partial_Sums(Im ([*0, th*] ExpSeq)).(2*n+1) &
Partial_Sums(th P_cos).n = Partial_Sums(Re ([*0, th*] ExpSeq)).(2*n)
proof
let th;
now
A1:Partial_Sums(th P_sin).0= (th P_sin).0 by SERIES_1:def 1
.= (-1)|^ 0 * (th)|^ (2*0+1)/((2*0+1)!) by Def24;
A2: (th)|^ (2*0+1)= th GeoSeq.(0+1) by PREPOWER:def 1
.= th GeoSeq.0 * th by PREPOWER:4
.= 1* th by PREPOWER:4
.= th;
A3: ((2*0+1)!)= 0! * 1 by NEWTON:21
.= 1 by NEWTON:18;
A4: (-1)|^ 0 = (-1) GeoSeq.0 by PREPOWER:def 1
.= 1 by PREPOWER:4;
A5: Partial_Sums(th P_cos).0= (th P_cos).0 by SERIES_1:def 1
.=(-1)|^ 0 * (th)|^ (2*0)/((2*0)!) by Def25
.= 1* th GeoSeq.0 / 1 by A4,NEWTON:18,PREPOWER:def 1
.=1 by PREPOWER:4;
A6: (Im ([*0, th*] ExpSeq)).0= Im (([*0, th*] ExpSeq).0) &
(Im ([*0, th*] ExpSeq)).1= Im (([*0, th*] ExpSeq).1) by COMSEQ_3:def 4;
A7: for q st q<>0 holds [*0, th*] /[*q,0*] =[*0,th/q*]
proof
let q; assume
A8: q<>0;
Re[*0, th*]=0 & Im[*0, th*]=th & Re[*q,0*]=q
& Im[*q,0*]=0 by COMPLEX1:7;
then [*0, th*] /[*q,0*] =[*(0*q+ th *0)/ (q^2 + 0^2 ),
(q* th - 0 * 0)/((q)^2 + (0)^2) *] by COMPLEX1:def 14
.=[*0,(q*th)/(q*q)*] by SQUARE_1:60,def 3
.= [*0,(q/q*th)/q*] by XCMPLX_1:84
.=[*0,(1*th)/q*] by A8,XCMPLX_1:60
.=[*0, th/q*];
hence thesis;
end;
A9: Partial_Sums(Im ([*0, th*] ExpSeq)).(2*0+1)
= Partial_Sums(Im ([*0, th*] ExpSeq)).0 +
(Im ([*0, th*] ExpSeq)).1 by SERIES_1:def 1
.= (Im ([*0, th*] ExpSeq)).0+
(Im ([*0, th*] ExpSeq)).1 by SERIES_1:def 1
.= Im (1r) + Im (([*0, th*] ExpSeq).(0+1)) by A6,Th4
.=0 + Im ((([*0, th*] ExpSeq).0)* [*0, th*] /[*(0+1),0*])
by Th4,COMPLEX1:15
.= Im (1r* [*0, th*] /[*1,0*]) by Th4
.= Im([*0, th*] /[*1,0*]) by COMPLEX1:29
.=Im([*0, th/1*]) by A7
.=th by COMPLEX1:7;
defpred X[Nat] means
Partial_Sums(th P_sin).$1 = Partial_Sums(Im ([*0, th*] ExpSeq)).(2*$1+1) &
Partial_Sums(th P_cos).$1 = Partial_Sums(Re ([*0, th*] ExpSeq)).(2*$1);
Partial_Sums(Re ([*0, th*] ExpSeq)).(2*0)
= (Re ([*0, th*] ExpSeq)).0 by SERIES_1:def 1
.= Re (([*0, th*] ExpSeq).0) by COMSEQ_3:def 3
.=1 by Th4,COMPLEX1:15;
then A10: X[0] by A1,A2,A3,A4,A5,A9;
A11: for k st X[k] holds X[k+1]
proof
let k be Nat;
assume
A12:
Partial_Sums(th P_sin).k = Partial_Sums(Im ([*0, th*] ExpSeq)).(2*k+1) &
Partial_Sums(th P_cos).k = Partial_Sums(Re ([*0, th*] ExpSeq)).(2*k);
A13: for k holds 2*(k+1)=(2*k+1)+1
proof
let k;
2*(k+1)= 2*k+2*1 by XCMPLX_1:8;
then 2*(k+1)= 2*k+(1+1)
.=(2*k+1)+1 by XCMPLX_1:1;
hence thesis;
end;
A14: Partial_Sums(Im ([*0, th*] ExpSeq)).(2*(k+1)+1)
= Partial_Sums(Im ([*0, th*] ExpSeq)).(2*(k+1))+
(Im ([*0, th*] ExpSeq)).(2*(k+1)+1) by SERIES_1:def 1
.= Partial_Sums(Im ([*0, th*] ExpSeq)).((2*k+1)+1) +
(Im ([*0, th*] ExpSeq)).(2*(k+1)+1) by A13
.= Partial_Sums(Im ([*0, th*] ExpSeq)).(2*k+1) +
(Im([*0, th*] ExpSeq)).((2*k+1)+1)+(Im ([*0, th*] ExpSeq)).(2*(k+1)+1)
by SERIES_1:def 1
.= Partial_Sums(th P_sin).k +
(Im([*0, th*] ExpSeq)).(2*(k+1))+(Im ([*0, th*] ExpSeq)).(2*(k+1)+1)
by A12,A13
.= Partial_Sums(th P_sin).k +
Im (([*0, th*] ExpSeq).(2*(k+1)))+(Im([*0, th*] ExpSeq)).(2*(k+1)+1)
by COMSEQ_3:def 4
.=Partial_Sums(th P_sin).k +
Im (([*0, th*] ExpSeq).(2*(k+1)))+Im(([*0, th*] ExpSeq).(2*(k+1)+1))
by COMSEQ_3:def 4
.= Partial_Sums(th P_sin).k +
Im([*0, th*] #N (2*(k+1))/((2*(k+1))!c))+
Im(([*0, th*] ExpSeq).(2*(k+1)+1)) by Def8
.= Partial_Sums(th P_sin).k +
Im([*0, th*] #N (2*(k+1))/((2*(k+1))!c))+
Im([*0, th*] #N (2*(k+1)+1)/((2*(k+1)+1)!c)) by Def8
.= Partial_Sums(th P_sin).k +
Im( [*(-1)|^ (k+1)* (th |^ (2*(k+1))),0*]/ ((2*(k+1))!c))
+Im([*0, th*] #N (2*(k+1)+1)/((2*(k+1)+1)!c)) by Th36
.= Partial_Sums(th P_sin).k +
Im( [*(-1)|^ (k+1)* (th |^ (2*(k+1))),0*]/ ((2*(k+1))!c))
+ Im( [*0,(-1)|^ (k+1)* (th |^ (2*(k+1)+1))*]/((2*(k+1)+1)!c))
by Th36
.= Partial_Sums(th P_sin).k +
Im( [*(-1)|^ (k+1)* (th |^ (2*(k+1))),0*]/ [*(2*(k+1))!,0*])
+ Im( [*0,(-1)|^ (k+1)* (th |^ (2*(k+1)+1))*]/((2*(k+1)+1)!c))
by Th37
.= Partial_Sums(th P_sin).k +
Im( [*(-1)|^ (k+1)* (th |^ (2*(k+1))),0*]/ [*(2*(k+1))!,0*])
+ Im( [*0,(-1)|^ (k+1)* (th |^ (2*(k+1)+1))*]/[*(2*(k+1)+1)!,0*])
by Th37;
(2*(k+1))!<>0 by NEWTON:23;
then A15: Partial_Sums(Im ([*0, th*] ExpSeq)).(2*(k+1)+1)
= Partial_Sums(th P_sin).k +
Im( [*((-1)|^ (k+1)* (th |^ (2*(k+1))))/((2*(k+1))!),0/((2*(k+1))!)*])
+ Im( [*0,(-1)|^ (k+1)* (th |^ (2*(k+1)+1))*]/[*(2*(k+1)+1)!,0*])
by A14,Lm9;
(2*(k+1)+1)!<>0 by NEWTON:23;
then Partial_Sums(Im ([*0, th*] ExpSeq)).(2*(k+1)+1)
= Partial_Sums(th P_sin).k +
Im([*((-1)|^ (k+1)* (th |^ (2*(k+1))))/((2*(k+1))!),
0/((2*(k+1))!)*])+ Im( [*0/((2*(k+1)+1)!),
((-1)|^ (k+1)* (th |^ (2*(k+1)+1)))/((2*(k+1)+1)!)*])
by A15,Lm9
.= Partial_Sums(th P_sin).k + (0/((2*(k+1))!)) +
Im( [*0/((2*(k+1)+1)!),
((-1)|^ (k+1)* (th |^ (2*(k+1)+1)))/((2*(k+1)+1)!)*]) by COMPLEX1:7
.= Partial_Sums(th P_sin).k + (0/((2*(k+1))!)) +
(-1)|^ (k+1)* (th |^ (2*(k+1)+1))/((2*(k+1)+1)!) by COMPLEX1:7;
then A16: Partial_Sums(Im ([*0, th*] ExpSeq)).(2*(k+1)+1)
= Partial_Sums(th P_sin).k + th P_sin.(k+1) by Def24
.= Partial_Sums(th P_sin).(k+1) by SERIES_1:def 1;
A17: Partial_Sums(Re ([*0, th*] ExpSeq)).(2*(k+1))
=Partial_Sums(Re ([*0, th*] ExpSeq)).((2*k+1)+1) by A13
.= Partial_Sums(Re ([*0, th*] ExpSeq)).(2*k+1)+
(Re ([*0, th*] ExpSeq)).((2*k+1)+1) by SERIES_1:def 1
.=Partial_Sums(th P_cos).k +
(Re ([*0, th*] ExpSeq)).(2*k+1)+
(Re ([*0, th*] ExpSeq)).((2*k+1)+1) by A12,SERIES_1:def 1
.= Partial_Sums(th P_cos).k +
Re (([*0, th*] ExpSeq).(2*k+1))+
(Re ([*0, th*] ExpSeq)).((2*k+1)+1) by COMSEQ_3:def 3
.= Partial_Sums(th P_cos).k +
Re (([*0, th*] ExpSeq).(2*k+1))+
Re (([*0, th*] ExpSeq).((2*k+1)+1)) by COMSEQ_3:def 3
.=Partial_Sums(th P_cos).k +
Re ([*0, th*]#N (2*k+1)/ ((2*k+1)!c))+
Re (([*0, th*] ExpSeq).((2*k+1)+1)) by Def8
.= Partial_Sums(th P_cos).k +
Re ([*0, th*]#N (2*k+1)/ ((2*k+1)!c))+
Re ([*0, th*]#N ((2*k+1)+1)/(((2*k+1)+1)!c)) by Def8
.= Partial_Sums(th P_cos).k +
Re ([*0, th*]#N (2*k+1)/ ((2*k+1)!c))+
Re ([*0, th*]#N (2*(k+1))/(((2*k+1)+1)!c)) by A13
.= Partial_Sums(th P_cos).k +
Re ([*0, th*]#N (2*k+1)/ ((2*k+1)!c))+
Re ([*0, th*]#N (2*(k+1))/((2*(k+1))!c)) by A13
.= Partial_Sums(th P_cos).k +
Re ( [*0,(-1)|^ k* (th |^ (2*k+1))*]/((2*k+1)!c))+
Re ([*0, th*]#N (2*(k+1))/((2*(k+1))!c)) by Th36
.= Partial_Sums(th P_cos).k +
Re ( [*0,(-1)|^ k* (th |^ (2*k+1))*]/((2*k+1)!c))+
Re ([*(-1)|^ (k+1)* (th |^ (2*(k+1))),0*]/((2*(k+1))!c)) by Th36
.= Partial_Sums(th P_cos).k +
Re ( [*0,(-1)|^ k* (th |^ (2*k+1))*]/[*(2*k+1)!, 0*])+
Re ([*(-1)|^ (k+1)* (th |^ (2*(k+1))),0*]/((2*(k+1))!c)) by Th37
.= Partial_Sums(th P_cos).k +
Re ( [*0,(-1)|^ k* (th |^ (2*k+1))*]/[*(2*k+1)!, 0*])+
Re ([*(-1)|^ (k+1)* (th |^ (2*(k+1))),0*]/[*(2*(k+1))!,0*]) by Th37;
(2*k+1)!<>0 by NEWTON:23;
then A18: Partial_Sums(Re ([*0, th*] ExpSeq)).(2*(k+1))
= Partial_Sums(th P_cos).k +
Re ( [*0/((2*k+1)!),((-1)|^ k* (th |^ (2*k+1)))/((2*k+1)!)*]) +
Re ([*(-1)|^ (k+1)* (th |^ (2*(k+1))),0*]/[*(2*(k+1))!,0*])
by A17,Lm9;
(2*(k+1))! <>0 by NEWTON:23;
then Partial_Sums(Re ([*0, th*] ExpSeq)).(2*(k+1))
= Partial_Sums(th P_cos).k +
Re ( [*0/((2*k+1)!),(-1)|^ k* (th |^ (2*k+1))/((2*k+1)!)*])+
Re ([*(-1)|^ (k+1)* (th |^ (2*(k+1)))/((2*(k+1))!),0/((2*(k+1))!)*])
by A18,Lm9
.= Partial_Sums(th P_cos).k +0/((2*k+1)!)+
Re ([*(-1)|^ (k+1)* (th |^ (2*(k+1)))/((2*(k+1))!),0/((2*(k+1))!)*])
by COMPLEX1:7
.= Partial_Sums(th P_cos).k +0/((2*k+1)!)+
(-1)|^ (k+1)* (th |^ (2*(k+1)))/((2*(k+1))!) by COMPLEX1:7;
then Partial_Sums(Re ([*0, th*] ExpSeq)).(2*(k+1))
= Partial_Sums(th P_cos).k + th P_cos.(k+1) by Def25
.= Partial_Sums(th P_cos).(k+1) by SERIES_1:def 1;
hence thesis by A16;
end;
thus for n holds X[n] from Ind(A10,A11);
end;
hence thesis;
end;
theorem Th39: for th holds
Partial_Sums(th P_sin) is convergent & Sum(th P_sin)=Im(Sum
([*0,th*] ExpSeq))
&Partial_Sums(th P_cos) is convergent & Sum(th P_cos)=Re(Sum
([*0,th*] ExpSeq))
proof
let th;
Re ([*0,th*] ExpSeq) is summable & Im ([*0,th*] ExpSeq) is summable
& Sum(([*0,th*] ExpSeq))=[*Sum(Re ([*0,th*] ExpSeq)),Sum
(Im ([*0,th*] ExpSeq))*]
by COMSEQ_3:54;
then Sum(Re ([*0,th*] ExpSeq))= Re (Sum(([*0,th*] ExpSeq)))&
Sum(Im ([*0,th*] ExpSeq))=Im (Sum(([*0,th*] ExpSeq)))
by COMPLEX1:7;
then A1: Partial_Sums(Re ([*0,th*] ExpSeq)) is convergent &
lim Partial_Sums(Re ([*0,th*] ExpSeq))= Re (Sum(([*0,th*] ExpSeq)))&
Partial_Sums(Im ([*0,th*] ExpSeq)) is convergent &
lim Partial_Sums(Im ([*0,th*] ExpSeq))=Im (Sum(([*0,th*] ExpSeq)))
by SERIES_1:def 2,def 3;
A2: now let p be real number;
assume p>0;
then consider n such that
A3:for k st n <= k
holds abs(Partial_Sums(Re ([*0,th*] ExpSeq)).k-
Re (Sum(([*0,th*] ExpSeq)))) < p by A1,SEQ_2:def 7;
take n;
now let k such that
A4: n <= k;
A5: abs(Partial_Sums(th P_cos).k-Re (Sum(([*0,th*] ExpSeq))))
=abs(Partial_Sums(Re ([*0,th*] ExpSeq)).(2*k)-
Re (Sum(([*0,th*] ExpSeq)))) by Th38;
2*k=k+k by XCMPLX_1:11;
then n <= 2*k by A4,NAT_1:37;
hence
abs(Partial_Sums(th P_cos).k-Re (Sum(([*0,th*] ExpSeq))))
< p by A3,A5;
end;
hence for k st n <= k holds
abs(Partial_Sums(th P_cos).k-Re (Sum(([*0,th*] ExpSeq)))) < p;
end;
then Partial_Sums(th P_cos) is convergent by SEQ_2:def 6;
then A6: lim(Partial_Sums(th P_cos))=Re(Sum
([*0,th*] ExpSeq)) by A2,SEQ_2:def 7;
A7: now let p be real number;
assume p>0;
then consider n such that
A8:for k st n <= k
holds abs(Partial_Sums(Im ([*0,th*] ExpSeq)).k-
Im (Sum(([*0,th*] ExpSeq)))) < p by A1,SEQ_2:def 7;
take n;
now let k such that
A9: n <= k;
A10: abs(Partial_Sums(th P_sin).k-Im (Sum(([*0,th*] ExpSeq))))
=abs(Partial_Sums(Im ([*0,th*] ExpSeq)).(2*k+1)-
Im (Sum(([*0,th*] ExpSeq)))) by Th38;
2*k=k+k by XCMPLX_1:11;
then n <= 2*k by A9,NAT_1:37;
then n<2*k+1 by NAT_1:38;
hence abs(Partial_Sums(th P_sin).k-Im (Sum(([*0,th*] ExpSeq))))
< p by A8,A10;
end;
hence
for k st n <= k holds
abs(Partial_Sums(th P_sin).k-Im (Sum(([*0,th*] ExpSeq)))) < p;
end;
then Partial_Sums(th P_sin) is convergent by SEQ_2:def 6;
then lim(Partial_Sums(th P_sin))=Im(Sum
([*0,th*] ExpSeq)) by A7,SEQ_2:def 7;
hence thesis by A2,A6,A7,SEQ_2:def 6,SERIES_1:def 3;
end;
theorem Th40: for th holds cos.th=Sum(th P_cos) & sin.th=Sum(th P_sin)
proof
let th;
A1: sin.th = Im(Sum([*0,th*] ExpSeq)) by Def20;
cos.th=Re(Sum([*0,th*] ExpSeq)) by Def22;
hence thesis by A1,Th39;
end;
theorem Th41: for p,th,rseq st rseq is convergent&
lim(rseq)=th &(for n holds rseq.n >= p) holds
th >= p
proof
let p,th, rseq such that
A1: rseq is convergent & lim(rseq)=th &(for n holds rseq.n >= p);
deffunc U(Nat) = p;
consider rseq1 such that
A2: for n holds rseq1.n= U(n) from ExRealSeq;
A3:rseq1 is constant by A2,SEQM_3:def 6;
then A4: lim(rseq1)=rseq1.0 by SEQ_4:41
.=p by A2;
A5: rseq1 is convergent by A3,SEQ_4:39;
now let n;
rseq.n >= p by A1; hence
rseq.n >= rseq1.n by A2;
end;
hence thesis by A1,A4,A5,SEQ_2:32;
end;
deffunc U(Real) = 2*$1+1;
consider bq being Real_Sequence such that
Lm11: for n holds bq.n= U(n) from ExRealSeq;
bq is increasing Seq_of_Nat
proof
A1:bq is increasing
proof
for n,k st n<k holds bq.n<bq.k
proof
let n,k; assume
n<k;
then 2*n<2*k by REAL_1:70;
then 2*n+1<2*k+1 by REAL_1:53;
then bq.n<2*k+1 by Lm11;
hence thesis by Lm11;
end;
hence thesis by SEQM_3:7;
end;
for n holds bq.n is Nat
proof
let n;
2*n+1 is Nat;
hence thesis by Lm11;
end;
hence thesis by A1,SEQM_3:29;
end;
then reconsider bq as increasing Seq_of_Nat;
Lm12: for th,th1,th2,th3 be real number holds th |^ 0=1
& th |^ (2*n)=(th |^ n)|^ 2 & th |^ 1=th & th |^ 2=th * th
& (-1)|^(2*n)=1 &(-1)|^ (2*n+1)=-1
proof
let th,th1,th2,th3 be real number;
thus
th |^ 0=th GeoSeq.0 by PREPOWER:def 1
.=1 by PREPOWER:4;
thus
th |^ (2*n)=(th |^ n)|^ 2 by NEWTON:14;
thus A1: th |^ 1=th GeoSeq.(0+1)by PREPOWER:def 1
.=th GeoSeq.0 * th by PREPOWER:4
.=1* th by PREPOWER:4
.=th;
thus
th |^ 2=th |^ (1+1)
.= th*th by A1,NEWTON:13;
thus
A2: (-1)|^(2*n)=(1)|^(2*n) by POWER:1
.=1 by NEWTON:15;
thus
(-1)|^ (2*n+1)=(-1)|^ (2*n)*(-1) by NEWTON:11
.=-1 by A2;
end;
Lm13:
[*th,th1*]+[*th2,th3*]=[*th+th2,th1+th3*]
&(5/6)^2=25/36
&(th>0 & th1>0 implies th+th1>0)
proof
thus [*th,th1*]+[*th2,th3*]=[*th+th2,th1+th3*]
proof
Re[*th,th1*]=th&Im[*th,th1*]=th1&Re[*th2,th3*]=th2
&Im[*th2,th3*]=th3 by COMPLEX1:7;
hence thesis by COMPLEX1:def 9;
end;
thus (5/6)^2=(5/6)*(5/6) by SQUARE_1:def 3
.=25/36;
th>0 implies th1+th>th1 by REAL_1:69;
hence (th>0 & th1>0 implies th+th1>0) by AXIOMS:22;
end;
theorem Th42: for n,k,m st n < k holds m!>0 & n!<=k!
proof
let n,k,m;
assume
A1: n < k;
A2: for m holds 1<= m+1
proof
let m;
0 <= m by NAT_1:18;
then 0+1<= m+1 by AXIOMS:24;
hence 1<= m+1;
end;
deffunc U(Nat) = $1!;
consider rseq such that
A3:for l holds rseq.l=U(l) from ExRealSeq;
A4: rseq is non-decreasing
proof
for l holds rseq.l<=rseq.(l+1)& rseq.l>0
proof
let l;
defpred X[Nat] means rseq.$1<=rseq.($1+1)& rseq.$1>0;
A5: rseq.(0+1)=(0+1)! by A3
.=0!*1 by NEWTON:21
.=1 by NEWTON:18;
rseq.0=1 by A3,NEWTON:18;
then A6: X[0] by A5;
A7: for l st X[l] holds X[l+1]
proof
let l;
assume
rseq.l<=rseq.(l+1)& rseq.l>0;
then A8: rseq.(l+1)>0;
A9: rseq.(l+1+1)= (l+1+1)! by A3
.=(l+1)!*(l+1+1) by NEWTON:21
.=rseq.(l+1) *(l+1+1) by A3;
(l+1+1)>=1 by A2;
hence thesis by A8,A9,REAL_2:146;
end;
for l holds X[l] from Ind(A6,A7);
hence thesis;
end;
hence thesis by SEQM_3:def 13;
end;
then rseq.0 <= rseq.m by SEQM_3:21;
then rseq.0 <= m! by A3;
then A10: m!>=1 by A3,NEWTON:18;
n!=rseq.n & k! =rseq.k by A3;
hence thesis by A1,A4,A10,AXIOMS:22,SEQM_3:12;
end;
theorem Th43: for th,n,k st 0<=th & th <=1 & n<=k holds th |^ k <= th |^ n
proof
let th,n,k;
assume
A1: 0<=th & th <=1& n<=k;
A2: th GeoSeq is non-increasing
proof
for m holds th GeoSeq.(m+1)<=th GeoSeq.m& th GeoSeq.m >=0
proof
let m;
defpred X[Nat] means th GeoSeq.($1+1)<=th GeoSeq.$1 &th GeoSeq.$1 >=0;
th GeoSeq.(0+1)=th GeoSeq.0 * th by PREPOWER:4
.= 1*th by PREPOWER:4
.=th;
then A3: X[0] by A1,PREPOWER:4;
A4: for m st X[m] holds X[m+1]
proof
let m;
assume
A5: th GeoSeq.(m+1)<=th GeoSeq.m &th GeoSeq.m >=0;
A6: th GeoSeq.(m+1+1)=th GeoSeq.(m+1)*th by PREPOWER:4;
th GeoSeq.(m+1)=th GeoSeq.(m)*th by PREPOWER:4;
then th GeoSeq.(m+1)>=0 by A1,A5,REAL_2:121;
hence thesis by A1,A6,REAL_2:147;
end;
for m holds X[m] from Ind(A3,A4);
hence thesis;
end;
hence thesis by SEQM_3:def 14;
end;
A7: th |^ k=th GeoSeq. k by PREPOWER:def 1;
th |^ n=th GeoSeq. n by PREPOWER:def 1;
hence thesis by A1,A2,A7,SEQM_3:14;
end;
theorem Th44: for th,n holds [*th,0*]#N n=[* th |^ n,0 *]
proof
let th, n;
defpred X[Nat] means [*th,0*]#N $1 =[* th |^ $1,0 *];
[*th,0*]#N 0=[* 1,0 *] by COMSEQ_3:11,L1
.=[* th |^ 0,0 *] by Lm12;
then
A1: X[0];
A2: for k st X[k] holds X[k+1]
proof
let k;
assume
A3: [*th,0*]#N k =[* th |^ k,0 *];
[*th,0*]#N (k+1)=[*th,0*] GeoSeq.(k+1) by COMSEQ_3:def 2
.=[*th,0*] GeoSeq.k * [*th,0*] by COMSEQ_3:def 1
.=[* th |^ k,0 *]* [*th,0*] by A3,COMSEQ_3:def 2
.=[* th |^ k*th,0*th *] by Lm10
.=[* th |^ (k+1),0 *] by NEWTON:11;
hence thesis;
end;
for n holds X[n] from Ind(A1,A2);
hence thesis;
end;
theorem Th45:
for th, n holds [*th,0*] #N n /(n!c )=[*(th|^ n) /(n!),0*]
proof
let th, n;
A1: [*th,0*] #N n /(n!c )=[* th |^ n,0 *]/(n!c ) by Th44
.=[* th |^ n,0 *]/[*n!,0*] by Th37;
n!<>0 by NEWTON:23;
then [*th,0*] #N n /(n!c )=[*(th|^ n) /(n!),0/(n!)*] by A1,Lm9;
hence thesis;
end;
theorem Th46: Im(Sum([*p,0*] ExpSeq))=0
proof
A1: for n holds (Partial_Sums(Im([*p,0*] ExpSeq))).n=0
proof
let n;
defpred X[Nat] means (Partial_Sums(Im([*p,0*] ExpSeq))).$1=0;
(Partial_Sums(Im([*p,0*] ExpSeq))).0=Im([*p,0*] ExpSeq).0
by SERIES_1:def 1
.=Im([*p,0*] ExpSeq.0 ) by COMSEQ_3:def 4
.=0 by Th4,COMPLEX1:15;
then
A2: X[0];
A3: for k st X[k] holds X[k+1]
proof
let k;
assume
(Partial_Sums(Im([*p,0*] ExpSeq))).k=0;
then (Partial_Sums(Im([*p,0*] ExpSeq))).(k+1)
=0+ (Im([*p,0*] ExpSeq)).(k+1) by SERIES_1:def 1
.=Im(([*p,0*] ExpSeq).(k+1)) by COMSEQ_3:def 4
.=Im([*p,0*] #N (k+1) /((k+1)!c) ) by Def8
.=Im[*(p|^ (k+1))/((k+1)!),0*] by Th45
.=0 by COMPLEX1:7;
hence thesis;
end;
for n holds X[n] from Ind(A2,A3);
hence thesis;
end;
for n,m holds (Partial_Sums(Im([*p,0*] ExpSeq))).n=
(Partial_Sums(Im([*p,0*] ExpSeq))).m
proof
let n,m;
(Partial_Sums(Im([*p,0*] ExpSeq))).n=0&
(Partial_Sums(Im([*p,0*] ExpSeq))).m=0 by A1;
hence thesis;
end;
then (Partial_Sums(Im([*p,0*] ExpSeq))) is constant by SEQM_3:18;
then A4: lim Partial_Sums(Im([*p,0*] ExpSeq))=Partial_Sums(Im([*p,0*]
ExpSeq)).0
by SEQ_4:41
.= 0 by A1;
Im(Sum([*p,0*] ExpSeq))=Im[*Sum(Re ([*p,0*] ExpSeq)),Sum
(Im ([*p,0*] ExpSeq))*]
by COMSEQ_3:54
.= Sum(Im ([*p,0*] ExpSeq )) by COMPLEX1:7;
hence thesis by A4,SERIES_1:def 3;
end;
theorem Th47: cos.1>0 & sin.1>0 & cos.1<sin.1
proof
A1: cos.1>=1/2
proof
A2: (Partial_Sums(1 P_cos))*bq is_subsequence_of Partial_Sums(1 P_cos)
by SEQM_3:def 10;
A3: Partial_Sums(1 P_cos) is convergent & cos.1=Sum(1 P_cos) by Th39,Th40;
then A4: (Partial_Sums(1 P_cos))*bq is convergent by A2,SEQ_4:29;
lim ((Partial_Sums(1 P_cos))*bq )=lim(Partial_Sums(1 P_cos)) by A2,A3,
SEQ_4:30;
then A5: lim ((Partial_Sums(1 P_cos))*bq )= cos.1 by A3,SERIES_1:def 3;
for n holds ((Partial_Sums(1 P_cos))*bq).n >=1/2
proof
let n;
defpred X[Nat] means ((Partial_Sums(1 P_cos))*bq).$1 >= 1/2;
((Partial_Sums(1 P_cos))*bq).0=(Partial_Sums(1 P_cos)).(bq.0)
by SEQM_3:31
.= (Partial_Sums(1 P_cos)).(2*0+1) by Lm11
.=(Partial_Sums(1 P_cos)).0+(1 P_cos).(0+1)
by SERIES_1:def 1
.= (1 P_cos).0 +(1 P_cos).(0+1) by SERIES_1:def 1
.=(-1)|^ 0 * (1)|^ (2*0)/((2*0)!)+(1 P_cos).(1)
by Def25
.= (-1)|^ 0 * (1)|^ (2*0)/((2*0)!)+
(-1)|^ 1 * (1)|^ (2*1)/((2*1)!) by Def25
.=1* (1)|^ (2*0)/((2*0)!)+
(-1)|^ 1 * (1)|^ (2*1)/((2*1)!) by Lm12
.=1/1 + (-1)|^ 1 * (1)|^ (2*1)/((2*1)!)
by Lm12,NEWTON:18
.=1+ (-1)* (1)|^ (2*1)/((2*1)!) by Lm12
.=1+ (-1)*1/((2*1)!) by NEWTON:15
.=1+(-1)/(1! * (1+1)) by NEWTON:21
.=1+(-1)/(0! * (0+1) *2) by NEWTON:21
.=1/2 by NEWTON:18;
then A6: X[0];
A7: for k st X[k] holds X[k+1]
proof
let k;
assume
A8: ((Partial_Sums(1 P_cos))*bq).k >= 1/2;
((Partial_Sums(1 P_cos))*bq).(k+1)
=(Partial_Sums(1 P_cos)).(bq.(k+1)) by SEQM_3:31
.=(Partial_Sums(1 P_cos)).(2*(k+1)+1) by Lm11
.=(Partial_Sums(1 P_cos)).(2*(k+1)) +(1 P_cos).(2*(k+1)+1)
by SERIES_1:def 1
.= (Partial_Sums(1 P_cos)).(2*k+2*1) +(1 P_cos).(2*(k+1)+1)
by XCMPLX_1:8
.= (Partial_Sums(1 P_cos)).(2*k+(1+1))+(1 P_cos).(2*(k+1)+1)
.=(Partial_Sums(1 P_cos)).(2*k+1+1)+(1 P_cos).(2*(k+1)+1)
by XCMPLX_1:1
.=(Partial_Sums(1 P_cos)).(2*k+1) + (1 P_cos).(2*k+1+1)+
(1 P_cos).(2*(k+1)+1) by SERIES_1:def 1
.= (Partial_Sums(1 P_cos)).(bq.k)+ (1 P_cos).(2*k+1+1)+
(1 P_cos).(2*(k+1)+1) by Lm11
.=((Partial_Sums(1 P_cos))*bq).k+ (1 P_cos).(2*k+1+1)+
(1 P_cos).(2*(k+1)+1) by SEQM_3:31;
then A9:
((Partial_Sums(1 P_cos))*bq).(k+1)-((Partial_Sums(1 P_cos))*bq).k
= ((Partial_Sums(1 P_cos))*bq).k+((1 P_cos).(2*k+1+1)
+ (1 P_cos).(2*(k+1)+1))-((Partial_Sums(1 P_cos))*bq).k by XCMPLX_1:1
.=((Partial_Sums(1 P_cos))*bq).k-((Partial_Sums(1 P_cos))*bq).k
+((1 P_cos).(2*k+1+1)+ (1 P_cos).(2*(k+1)+1)) by XCMPLX_1:29
.=0+((1 P_cos).(2*k+1+1)+ (1 P_cos).(2*(k+1)+1)) by XCMPLX_1:14
.=(1 P_cos).(2*k+1+1)+ (1 P_cos).(2*(k+1)+1);
A10: (1 P_cos).(2*k+1+1)=(1 P_cos).(2*k+(1+1)) by XCMPLX_1:1
.=(1 P_cos).(2*k+2*1)
.=(1 P_cos).(2*(k+1)) by XCMPLX_1:8
.=(-1)|^ (2*(k+1)) * (1)|^ (2*(2*(k+1)))/((2*(2*(k+1)))!) by Def25
.=(1)* (1)|^ (2*(2*(k+1)))/((2*(2*(k+1)))!) by Lm12
.=1/((2*(2*(k+1)))!) by NEWTON:15;
(1 P_cos).(2*(k+1)+1)
= (-1)|^ (2*(k+1)+1) * (1)|^ (2*(2*(k+1)+1))/((2*(2*(k+1)+1))!)
by Def25
.=(-1) * (1)|^ (2*(2*(k+1)+1))/((2*(2*(k+1)+1))!) by Lm12
.=(-1) * 1/((2*(2*(k+1)+1))!) by NEWTON:15
.=(-1)/((2*(2*(k+1)+1))!); then A11:
(1 P_cos).(2*(k+1)+1)=-1/((2*(2*(k+1)+1))!) by XCMPLX_1:188;
2*(k+1) < 2*(k+1)+1 by REAL_1:69;
then 2*(2*(k+1))<2*(2*(k+1)+1) by REAL_1:70;
then A12: (2*(2*(k+1)))! <= (2*(2*(k+1)+1))! by Th42;
(2*(2*(k+1)))!>0 by Th42;
then 1/((2*(2*(k+1)))!) >= 1/((2*(2*(k+1)+1))!) by A12,REAL_2:152;
then A13:
1/((2*(2*(k+1)))!)-1/(2*(2*(k+1)+1)!)>=0 by SQUARE_1:12;
((Partial_Sums(1 P_cos))*bq).(k+1)-((Partial_Sums(1 P_cos))*bq).k
= 1/((2*(2*(k+1)))!)-1/((2*(2*(k+1)+1))!) by A9,A10,A11,XCMPLX_0:def 8
;
then ((Partial_Sums(1 P_cos))*bq).(k+1)>=((Partial_Sums(1 P_cos))*bq).
k
by A13,REAL_2:105;
hence thesis by A8,AXIOMS:22;
end;
for n holds X[n] from Ind(A6,A7);
hence thesis;
end;
hence thesis by A4,A5,Th41;
end;
then A14: cos.1>0 by AXIOMS:22;
A15: sin.1>=5/6
proof
A16: (Partial_Sums(1 P_sin))*bq is_subsequence_of Partial_Sums(1 P_sin)
by SEQM_3:def 10;
A17: Partial_Sums(1 P_sin) is convergent & sin.1=Sum(1 P_sin) by Th39,Th40;
then A18: (Partial_Sums(1 P_sin))*bq is convergent by A16,SEQ_4:29;
lim ((Partial_Sums(1 P_sin))*bq )=lim(Partial_Sums(1 P_sin)) by A16,A17,
SEQ_4:30;
then A19: lim ((Partial_Sums(1 P_sin))*bq )= sin.1 by A17,SERIES_1:def 3;
for n holds ((Partial_Sums(1 P_sin))*bq).n >=5/6
proof
let n;
defpred X[Nat] means ((Partial_Sums(1 P_sin))*bq).$1 >= 5/6;
((Partial_Sums(1 P_sin))*bq).0=(Partial_Sums(1 P_sin)).(bq.0)
by SEQM_3:31
.= (Partial_Sums(1 P_sin)).(2*0+1) by Lm11
.=(Partial_Sums(1 P_sin)).0+(1 P_sin).(0+1)
by SERIES_1:def 1
.= (1 P_sin).0 +(1 P_sin).(0+1) by SERIES_1:def 1
.=(-1)|^ 0 * (1)|^ (2*0+1)/((2*0+1)!)+(1 P_sin).(1)
by Def24
.= (-1)|^ 0 * (1)|^ (2*0+1)/((2*0+1)!)+
(-1)|^ 1 * (1)|^ (2*1+1)/((2*1+1)!) by Def24
.=1* (1)|^ (2*0+1)/((2*0+1)!)+
(-1)|^ 1 * (1)|^ (2*1+1)/((2*1+1)!) by Lm12
.=1/((0+1)!)+(-1)|^ 1 * (1)|^ (2*1+1)/((2*1+1)!) by Lm12
.=1/(0!*1)+(-1)|^ 1 * (1)|^ (2*1+1)/((2*1+1)!) by NEWTON:21
.=1+ (-1)* (1)|^ (2*1+1)/((2*1+1)!) by Lm12,NEWTON:18
.=1+ (-1)*1/((2*1+1)!) by NEWTON:15
.=1+ (-1)/((2*1)!*(2*1+1)) by NEWTON:21
.=1+(-1)/(1! * (1+1)*3) by NEWTON:21
.=1+(-1)/((0+1)! *(2*3)) by XCMPLX_1:4
.=1+(-1)/(1* 1 *6) by NEWTON:18,21
.=5/6;
then A20: X[0];
A21: for k st X[k] holds X[k+1]
proof
let k;
assume
A22: ((Partial_Sums(1 P_sin))*bq).k >= 5/6;
((Partial_Sums(1 P_sin))*bq).(k+1)
=(Partial_Sums(1 P_sin)).(bq.(k+1)) by SEQM_3:31
.=(Partial_Sums(1 P_sin)).(2*(k+1)+1) by Lm11
.=(Partial_Sums(1 P_sin)).(2*(k+1)) +(1 P_sin).(2*(k+1)+1)
by SERIES_1:def 1
.= (Partial_Sums(1 P_sin)).(2*k+2*1) +(1 P_sin).(2*(k+1)+1)
by XCMPLX_1:8
.= (Partial_Sums(1 P_sin)).(2*k+(1+1))+(1 P_sin).(2*(k+1)+1)
.=(Partial_Sums(1 P_sin)).(2*k+1+1)+(1 P_sin).(2*(k+1)+1)
by XCMPLX_1:1
.=(Partial_Sums(1 P_sin)).(2*k+1) + (1 P_sin).(2*k+1+1)+
(1 P_sin).(2*(k+1)+1) by SERIES_1:def 1
.= (Partial_Sums(1 P_sin)).(bq.k)+ (1 P_sin).(2*k+1+1)+
(1 P_sin).(2*(k+1)+1) by Lm11
.=((Partial_Sums(1 P_sin))*bq).k+ (1 P_sin).(2*k+1+1)+
(1 P_sin).(2*(k+1)+1) by SEQM_3:31;
then A23:
((Partial_Sums(1 P_sin))*bq).(k+1)-((Partial_Sums(1 P_sin))*bq).k
= ((Partial_Sums(1 P_sin))*bq).k+((1 P_sin).(2*k+1+1)
+ (1 P_sin).(2*(k+1)+1))-((Partial_Sums(1 P_sin))*bq).k by XCMPLX_1:
1
.=((Partial_Sums(1 P_sin))*bq).k-((Partial_Sums(1 P_sin))*bq).k
+((1 P_sin).(2*k+1+1)+ (1 P_sin).(2*(k+1)+1)) by XCMPLX_1:29
.=0+((1 P_sin).(2*k+1+1)+ (1 P_sin).(2*(k+1)+1)) by XCMPLX_1:14
.=(1 P_sin).(2*k+1+1)+ (1 P_sin).(2*(k+1)+1);
A24: (1 P_sin).(2*k+1+1)=(1 P_sin).(2*k+(1+1)) by XCMPLX_1:1
.=(1 P_sin).(2*k+2*1)
.=(1 P_sin).(2*(k+1)) by XCMPLX_1:8
.=(-1)|^ (2*(k+1)) * (1)|^ (2*(2*(k+1))+1)/((2*(2*(k+1))+1)!)
by Def24
.=(1)* (1)|^ (2*(2*(k+1))+1)/((2*(2*(k+1))+1)!) by Lm12
.=1/((2*(2*(k+1))+1)!) by NEWTON:15;
(1 P_sin).(2*(k+1)+1)
= (-1)|^ (2*(k+1)+1) * (1)|^ (2*(2*(k+1)+1)+1)/((2*(2*(k+1)+1)+1)!)
by Def24
.=(-1) * (1)|^ (2*(2*(k+1)+1)+1)/((2*(2*(k+1)+1)+1)!) by Lm12
.=(-1) * 1/((2*(2*(k+1)+1)+1)!) by NEWTON:15
.=(-1)/((2*(2*(k+1)+1)+1)!); then A25:
(1 P_sin).(2*(k+1)+1)=-1/((2*(2*(k+1)+1)+1)!) by XCMPLX_1:188;
2*(k+1) < 2*(k+1)+1 by REAL_1:69;
then 2*(2*(k+1))<2*(2*(k+1)+1) by REAL_1:70;
then 2*(2*(k+1))+1<2*(2*(k+1)+1) +1 by REAL_1:53;
then A26: (2*(2*(k+1))+1)! <= (2*(2*(k+1)+1)+1)! by Th42;
(2*(2*(k+1))+1)!>0 by Th42;
then 1/((2*(2*(k+1))+1)!) >= 1/((2*(2*(k+1)+1)+1)!) by A26,REAL_2:152
;
then A27:
1/((2*(2*(k+1))+1)!)-1/((2*(2*(k+1)+1)+1)!)>=0 by SQUARE_1:12;
((Partial_Sums(1 P_sin))*bq).(k+1)-((Partial_Sums(1 P_sin))*bq).k
= 1/((2*(2*(k+1))+1)!)-1/((2*(2*(k+1)+1)+1)!)
by A23,A24,A25,XCMPLX_0:def 8;
then ((Partial_Sums(1 P_sin))*bq).(k+1)>=((Partial_Sums(1 P_sin))*bq)
.k
by A27,REAL_2:105;
hence thesis by A22,AXIOMS:22;
end;
for n holds X[n] from Ind(A20,A21);
hence thesis;
end;
hence thesis by A18,A19,Th41;
end;
then A28: sin.1>0 by AXIOMS:22;
sin.1>cos.1
proof
A29: 0 <=(cos.(1))^2 by SQUARE_1:72;
(cos.(1))^2+(sin.(1))^2=1 by Th31;
then A30: (sin.(1))^2=1-(cos.(1))^2 by XCMPLX_1:26;
A31: (sin.(1))^2>=(25/36) by A15,Lm13,SQUARE_1:77;
then A32: 1-(1-(cos.(1))^2)<=1-25/36 by A30,REAL_2:106;
1-(1-(cos.(1))^2)= 1-1+(cos.(1))^2 by XCMPLX_1:37
.=(cos.(1))^2;
then (cos.(1))^2<25/36 by A32,AXIOMS:22;
then (sin.(1))^2> (cos.(1))^2 by A31,AXIOMS:22;
then A33: sqrt(cos.(1))^2<sqrt(sin.(1))^2 by A29,SQUARE_1:95;
sqrt(cos.(1))^2 = cos.1 by A14,SQUARE_1:89;
hence thesis by A28,A33,SQUARE_1:89;
end;
hence thesis by A1,AXIOMS:22;
end;
theorem Th48:for th holds th ExpSeq=Re([*th,0*] ExpSeq)
proof
let th;
for n holds (th ExpSeq).n=Re([*th,0*] ExpSeq).n
proof
let n;
Re([*th,0*] ExpSeq).n= Re ([*th,0*] ExpSeq.n) by COMSEQ_3:def 3
.=Re([*th,0*] #N n /(n!c )) by Def8
.=Re([*(th|^ n) /(n!),0*]) by Th45
.=(th|^ n) /(n!) by COMPLEX1:7
.=(th ExpSeq).n by Def9;
hence thesis;
end;
hence thesis by FUNCT_2:113;
end;
theorem Th49: for th holds (th ExpSeq) is summable &
Sum(th ExpSeq)=Re(Sum([*th,0*] ExpSeq))
proof
let th;
A1: Re([*th,0*] ExpSeq) is summable &
Sum([*th,0*] ExpSeq)=[*Sum(Re ([*th,0*] ExpSeq)),Sum(Im ([*th,0*] ExpSeq))*]
by COMSEQ_3:54;
Sum(th ExpSeq)=Sum(Re ([*th,0*] ExpSeq)) by Th48;
hence thesis by A1,Th48,COMPLEX1:7;
end;
Lm14: for z,n holds z* (z#N n)=z #N (n+1) &z ExpSeq.1=z&z ExpSeq.0=1r&z #N1=z
&|.z #N n.|=|.z.||^n
proof
let z,n;
A1: z* (z#N n)=z*(z GeoSeq.n) by COMSEQ_3:def 2
.=z GeoSeq.(n+1) by COMSEQ_3:def 1
.=z #N (n+1) by COMSEQ_3:def 2;
A2: z #N 1=z GeoSeq.(0+1) by COMSEQ_3:def 2
.=z GeoSeq.0 * z by COMSEQ_3:def 1
.=1r* z by COMSEQ_3:def 1
.=z by COMPLEX1:29;
then A3: z ExpSeq.1= z/(1!c) b