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) by Def8
.=z/[*1,0*] by Th37,NEWTON:19
.=z by COMPLEX1:85,L1;
A4: z ExpSeq.0=z#N 0/ (0!c) by Def8
.=1r/1r by Th1,COMSEQ_3:11
.=1r by COMPLEX1:85;
|.z #N n.|=|.z.||^ n
proof
defpred X[Nat] means |.z #N $1.|=|.z.||^ $1;
|.z #N 0 .|=|.z GeoSeq.0 .| by COMSEQ_3:def 2
.=1 by COMPLEX1:134,COMSEQ_3:def 1;
then A5: X[0] by Lm12;
A6: for k st X[k] holds X[k+1]
proof
let k such that
A7: |.z #N k.|=|.z.||^ k;
|.z #N (k+1).|=|.z GeoSeq.(k+1).| by COMSEQ_3:def 2
.=|.z*(z GeoSeq.k).| by COMSEQ_3:def 1
.=|.z*(z#N k).| by COMSEQ_3:def 2
.=|.z.||^ k *|.z.| by A7,COMPLEX1:151
.=|.z.||^(k+1) by NEWTON:11;
hence thesis;
end;
for n holds X[n] from Ind(A5,A6);
hence thesis;
end;
hence thesis by A1,A2,A3,A4;
end;
Lm15: for th holds Sum([*th,0*] ExpSeq)=[*Sum(th ExpSeq),0*]
proof
let th;
A1: for n holds Im(Partial_Sums([*th,0*] ExpSeq)).n=0
proof
defpred X[Nat] means Im(Partial_Sums([*th,0*] ExpSeq)).$1=0;
Im(Partial_Sums([*th,0*] ExpSeq)).0
=Im(Partial_Sums([*th,0*] ExpSeq).0) by COMSEQ_3:def 4
.=Im(([*th,0*] ExpSeq).0) by COMSEQ_3:def 7
.=0 by Lm14,COMPLEX1:15;
then
A2: X[0];
A3: for n st X[n] holds X[n+1]
proof
let n such that
A4: Im(Partial_Sums([*th,0*] ExpSeq)).n=0;
Im(Partial_Sums([*th,0*] ExpSeq)).(n+1)
=Im(Partial_Sums([*th,0*] ExpSeq).(n+1)) by COMSEQ_3:def 4
.=Im(Partial_Sums([*th,0*] ExpSeq).n+([*th,0*] ExpSeq).(n+1))
by COMSEQ_3:def 7
.=Im(Partial_Sums([*th,0*] ExpSeq).n)+Im(([*th,0*] ExpSeq).(n+1))
by COMPLEX1:19
.=0+Im(([*th,0*] ExpSeq).(n+1)) by A4,COMSEQ_3:def 4
.=Im(([*th,0*] #N(n+1))/((n+1)!c)) by Def8
.=Im([*(th|^ (n+1)) /((n+1)!),0*]) by Th45
.=0 by COMPLEX1:7;
hence thesis;
end;
for n holds X[n] from Ind(A2,A3);
hence thesis;
end;
then Im(Partial_Sums([*th,0*] ExpSeq)) is constant by SEQM_3:def 6;
then A5: lim(Im(Partial_Sums([*th,0*] ExpSeq)))
=Im(Partial_Sums([*th,0*] ExpSeq)).0 by SEQ_4:41
.=0 by A1;
A6: Im(Sum([*th,0*] ExpSeq))
=Im(lim(Partial_Sums([*th,0*] ExpSeq))) by COMSEQ_3:def 8
.=0 by A5,COMSEQ_3:41;
Sum([*th,0*] ExpSeq)
=[*Re(Sum([*th,0*] ExpSeq)),Im(Sum([*th,0*] ExpSeq))*] by COMPLEX1:8
.=[*Sum(th ExpSeq),0*] by A6,Th49;
hence thesis;
end;
theorem Th50: for p,q holds
Sum((p+q) ExpSeq)= (Sum(p ExpSeq))*(Sum(q ExpSeq))
proof
let p,q;
Sum((p+q) ExpSeq)=Re(Sum([*p+q,0+0*] ExpSeq)) by Th49
.=Re(Sum(([*p,0*]+[*q,0*]) ExpSeq)) by Lm13
.=Re((Sum([*p,0*] ExpSeq)) *(Sum([*q,0*] ExpSeq))) by Lm4
.=Re([*Re(Sum([*p,0*] ExpSeq)),Im(Sum([*p,0*] ExpSeq))*]
*(Sum([*q,0*] ExpSeq))) by COMPLEX1:8
.= Re([*Re(Sum([*p,0*] ExpSeq)),Im(Sum([*p,0*] ExpSeq))*]*
[*Re(Sum([*q,0*] ExpSeq)),Im(Sum([*q,0*] ExpSeq))*])
by COMPLEX1:8
.= Re([*Sum(p ExpSeq),Im(Sum([*p,0*] ExpSeq))*]*
[*Re(Sum([*q,0*] ExpSeq)),Im(Sum([*q,0*] ExpSeq))*])
by Th49
.= Re([*Sum(p ExpSeq), 0*]*
[*Re(Sum([*q,0*] ExpSeq)),Im(Sum([*q,0*] ExpSeq))*])
by Th46
.= Re([*Sum(p ExpSeq), 0*]* [*Sum(q ExpSeq),
Im(Sum([*q,0*] ExpSeq))*]) by Th49
.= Re([*Sum(p ExpSeq), 0*]* [*Sum(q ExpSeq),0*]) by Th46
.=Re([*(Sum(p ExpSeq))*(Sum(q ExpSeq)),0*(Sum(q ExpSeq))*])
by Lm10
.=(Sum(p ExpSeq))*(Sum(q ExpSeq)) by COMPLEX1:7;
hence thesis;
end;
definition
func exp -> PartFunc of REAL, REAL means :Def26:
dom it= REAL & for d being real number holds it.d=Sum(d ExpSeq);
existence
proof
defpred X[set] means $1 in REAL;
deffunc U(Element of REAL) = Sum($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 real number holds f.d = Sum(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 real number holds f.d = Sum(d ExpSeq)
proof
let d be real number;
A5: d is Real by XREAL_0:def 1;
then A6: d in dom f by A1;
then f/.d = Sum(d ExpSeq) by A2,A5;
hence f.d = Sum(d ExpSeq) by A6,FINSEQ_4:def 4;
end;
hence thesis by A3;
end;
hence thesis;
end;
uniqueness
proof
let f1,f2 be PartFunc of REAL, REAL;
assume
A7: dom f1= REAL & for d being real number holds f1.d=Sum(d ExpSeq);
assume
A8: dom f2= REAL & for d being real number holds f2.d=Sum(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=Sum(d ExpSeq) by A7
.=f2.d by A8;
end;
hence f1=f2 by A7,A8,PARTFUN1:34;
end;
end;
definition let th be real number;
func exp th equals:Def27:
exp.th;
correctness;
end;
definition
let th be real number;
cluster exp th -> real;
correctness
proof
exp th = exp.th by Def27;
hence thesis;
end;
end;
definition let th be Real;
redefine func exp th -> Real;
correctness by XREAL_0:def 1;
end;
theorem Th51: dom(exp)=REAL by Def26;
canceled;
theorem Th53: for th holds exp.th = Re(Sum([*th,0*] ExpSeq))
proof
let th;
exp.th = Sum(th ExpSeq) by Def26;
hence thesis by Th49;
end;
theorem exp([*th,0*])=[*exp(th ),0*]
proof
thus exp([*th,0*])=Sum([*th,0*] ExpSeq) by Lm5
.=[*Sum(th ExpSeq),0*] by Lm15
.=[*exp.(th ),0*] by Def26
.=[*exp(th ),0*] by Def27;
end;
Lm16:for p,q holds exp.(p+q) = exp.p * exp.q
proof
let p,q;
exp.(p+q) = Sum((p+q) ExpSeq) by Def26
.= (Sum(p ExpSeq))*(Sum(q ExpSeq)) by Th50
.=exp.p *(Sum(q ExpSeq)) by Def26
.=exp.p * exp.q by Def26;
hence thesis;
end;
theorem
exp(p+q) = exp(p) * exp(q)
proof
thus exp(p+q) = exp.(p+q) by Def27
.=exp.p * exp.q by Lm16
.=exp.p *exp(q) by Def27
.=exp(p) * exp(q) by Def27;
end;
Lm17: exp.0 =1
proof
exp.0 = Sum(0 ExpSeq) by Def26
.=1 by Th10,Th49,COMPLEX1:15,L0;
hence thesis;
end;
theorem exp(0) =1 by Def27,Lm17;
theorem Th57: for th st th >0 holds exp.th >=1
proof
let th such that
A1: th >0;
A2:for n holds Partial_Sums(th ExpSeq).n>=1
proof
defpred X[Nat] means Partial_Sums(th ExpSeq).$1>=1;
Partial_Sums(th ExpSeq).0=(th ExpSeq).0 by SERIES_1:def 1
.=th |^ 0 /(0!) by Def9
.=1 by Lm12,NEWTON:18;
then A3: X[0];
A4: for n st X[n] holds X[n+1]
proof
let n;
assume
A5: Partial_Sums(th ExpSeq).n>=1;
A6: Partial_Sums(th ExpSeq).(n+1)
=Partial_Sums(th ExpSeq).n+(th ExpSeq).(n+1) by SERIES_1:def 1
.=Partial_Sums(th ExpSeq).n+th |^(n+1)/((n+1)!) by Def9;
A7: th |^(n+1) >0 by A1,PREPOWER:13;
(n+1)!>0 by Th42;
then th |^(n+1)/((n+1)!)>0 by A7,REAL_2:127;
then Partial_Sums(th ExpSeq).n+th |^(n+1)/((n+1)!)>Partial_Sums(th
ExpSeq).n
by REAL_1:69;
hence thesis by A5,A6,AXIOMS:22;
end;
for n holds X[n] from Ind(A3,A4);
hence thesis;
end;
(th ExpSeq) is summable by Th49;
then Partial_Sums(th ExpSeq) is convergent&
lim(Partial_Sums(th ExpSeq))=Sum(th ExpSeq) by SERIES_1:def 2,def 3;
then Sum(th ExpSeq)>=1 by A2,Th41;
hence thesis by Def26;
end;
theorem Th58: for th st th <0 holds 0<exp.th & exp.th <=1
proof
let th; assume th <0;
then -th >0 by REAL_1:26,50;
then A1: exp.(-th)>=1 by Th57;
then A2: exp.(-th)> 0 by AXIOMS:22;
exp.(-th)*exp.th=exp.(-th+th) by Lm16
.=1 by Lm17,XCMPLX_0:def 6;
then A3:exp.th=1/(exp.(-th)) by XCMPLX_1:74;
hence 0<exp.th by A2,REAL_2:127;
thus exp.th <=1 by A1,A3,REAL_2:164;
end;
theorem Th59: for th holds exp.th>0
proof
let th;
now per cases;
suppose th=0;
hence exp.th>0 by Lm17;
suppose A1: th<>0;
now per cases by A1;
suppose th<0;
hence exp.th>0 by Th58;
suppose th>0;
then exp.th >=1 by Th57;
hence exp.th>0 by AXIOMS:22;
end;
hence exp.th>0;
end;
hence thesis;
end;
theorem for th holds exp(th)>0
proof
let th;
exp(th)=exp.(th) by Def27;
hence thesis by Th59;
end;
begin ::Differential of sin, cos, and Exponential Function
definition let z be Element of COMPLEX;
deffunc U(Nat) = (z#N($1+1))/(($1+2)!c);
func z P_dt -> Complex_Sequence means :Def28:
for n holds it.n = (z#N(n+1))/((n+2)!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;
deffunc U(Nat) = (z#N($1))/(($1+2)!c);
func z P_t -> Complex_Sequence means
for n holds it.n = (z#N(n))/((n+2)!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;
Lm18: for z,p holds Re([*0,p*]*z)=-p*Im z & Im([*0,p*]*z)=p*Re z
&Re([*p,0*]*z)=p*Re z & Im([*p,0*]*z)=p*Im z
proof
let z,p;
A1: ([*0,p*]*z)=([*0,p*]*[*Re z,Im z*]) by COMPLEX1:8
.=([*-p* Im z,p*Re z*]) by Lm10;
([*p,0*]*z)=([*p,0*]*[*Re z,Im z*]) by COMPLEX1:8
.=([*p* Re z,p*Im z*]) by Lm10;
hence thesis by A1,COMPLEX1:7;
end;
Lm19: for z,p st p>0 holds Re(z/[*0,p*])=Im z /p & Im(z/[*0,p*])=-Re z /p
&|.z/[*p,0*].|=|.z.|/p
proof
let z,p such that
A1: p>0;
A2: Re[*0,p*]=0 & Im[*0,p*]=p&Re[*p,0*]=p&Im[*p,0*]=0 by COMPLEX1:7;
then A3: z/[*0,p*]
=[*(Re z * 0+Im z * p)/((0)+(p)^2),
(0* Im z- Re z * p)/((0)+(p)^2)*] by COMPLEX1:def 14,SQUARE_1:60
.=[*(Im z * p)/((p)^2), (-Re z * p)/((p)^2)*] by XCMPLX_1:150
.=[*(Im z * p)/((p)^2), (-Re z * p)/(p*p)*] by SQUARE_1:def 3
.=[*(Im z * p)/(p*p), (-Re z * p)/(p*p)*] by SQUARE_1:def 3
.=[*(Im z * p)/(p*p), ((-Re z) * p)/(p*p)*] by XCMPLX_1:175
.=[*(Im z * p)/(p*p),(-Re z) /p *] by A1,XCMPLX_1:92
.=[*(Im z * p)/(p*p),-Re z/p *] by XCMPLX_1:188
.=[*Im z /p,-Re z /p *] by A1,XCMPLX_1:92;
[*p,0*]<>0c by A1,ARYTM_0:def 7;
then |.z/[*p,0*].|=|.z.|/|.[*p,0*].| by COMPLEX1:153
.=|.z.|/sqrt((p)^2 + (0)^2) by A2,COMPLEX1:def 16
.=|.z.|/sqrt((p)^2) by SQUARE_1:60;
hence thesis by A1,A3,COMPLEX1:7,SQUARE_1:89;
end;
theorem Th61: for z holds z P_dt is absolutely_summable
proof
let z;
Partial_Sums(|.z P_dt.|) is bounded_above
proof
ex r st for n holds Partial_Sums(|.z P_dt.|).n<r
proof
A1: for n holds
Partial_Sums(|.z P_dt.|).n<Partial_Sums(|.z ExpSeq.|).(n+1)
proof
let n;
Partial_Sums(|.z P_dt.|).0=|.z P_dt.|.0 by SERIES_1:def 1
.=|.z P_dt.0 .| by COMSEQ_1:def 14
.=|.(z#N(0+1))/((0+2)!c).| by Def28
.=|.z/((2)!c).| by Lm14
.=|.z/[*2,0*].| by Th37,NEWTON:20;
then A2: Partial_Sums(|.z P_dt.|).0=|.z.|/2 by Lm19;
Partial_Sums(|.z ExpSeq.|).(0+1)
=Partial_Sums(|.z ExpSeq.|).0+|.z ExpSeq.|.(0+1) by SERIES_1:def 1
.=|.z ExpSeq.|.0+|.z ExpSeq.|.1 by SERIES_1:def 1
.=|.z ExpSeq.|.0+|.z ExpSeq.1 .| by COMSEQ_1:def 14
.=|.z ExpSeq.0 .|+|.z ExpSeq.1 .| by COMSEQ_1:def 14
.=|.z ExpSeq.0 .|+|.z .| by Lm14
.=1+|.z .| by Lm14,COMPLEX1:134;
then A3: Partial_Sums(|.z ExpSeq.|).(0+1)-Partial_Sums(|.z P_dt.|).0
=1+(|.z .| - |.z.|/2) by A2,XCMPLX_1:29;
|.z.|=|.z.|/2+|.z.|/2 by XCMPLX_1:66;
then A4: Partial_Sums(|.z ExpSeq.|).(0+1)-Partial_Sums(|.z P_dt.|).0
=1+|.z .|/2 by A3,XCMPLX_1:26;
A5: 1+|.z.|/2>|.z.|/2 by REAL_1:69;
defpred X[Nat] means
Partial_Sums(|.z P_dt.|).$1 <Partial_Sums(|.z ExpSeq.|).($1+1);
0 <= |.z.| by COMPLEX1:132; then |.z.|/2>=0 by REAL_2:125;
then A6: X[0] by A4,A5,REAL_2:106;
A7: for n st X[n] holds X[n+1]
proof
let n such that
A8: Partial_Sums(|.z P_dt.|).n <Partial_Sums(|.z ExpSeq.|).(n+1);
A9:Partial_Sums(|.z P_dt.|).(n+1)
=Partial_Sums(|.z P_dt.|).n+|.z P_dt.|.(n+1) by SERIES_1:def 1
.=Partial_Sums(|.z P_dt.|).n+|.z P_dt.(n+1).| by COMSEQ_1:def 14
.=Partial_Sums(|.z P_dt.|).n+|.(z#N((n+1)+1))/(((n+1)+2)!c).| by Def28
.=Partial_Sums(|.z P_dt.|).n+|.(z#N((n+1)+1))/((n+(1+2))!c).|
by XCMPLX_1:1
.=Partial_Sums(|.z P_dt.|).n+|.(z#N(n+(1+1)))/((n+(1+2))!c).|
by XCMPLX_1:1
.=Partial_Sums(|.z P_dt.|).n+|.(z#N(n+2))/[*(n+3)!,0*].| by Th37;
(n+3)!>0 by Th42;
then A10: Partial_Sums(|.z P_dt.|).(n+1)
=Partial_Sums(|.z P_dt.|).n+|.(z#N(n+2)).|/((n+3)!) by A9,Lm19;
A11: Partial_Sums(|.z ExpSeq.|).((n+1)+1)
=Partial_Sums(|.z ExpSeq.|).(n+1)+|.z ExpSeq.|.((n+1)+1)
by SERIES_1:def 1
.= Partial_Sums(|.z ExpSeq.|).(n+1)+|.z ExpSeq.|.(n+(1+1)) by XCMPLX_1:
1
.=Partial_Sums(|.z ExpSeq.|).(n+1)+|.z ExpSeq.(n+2).| by COMSEQ_1:def 14
.=Partial_Sums(|.z ExpSeq.|).(n+1)+|.(z#N(n+2))/((n+2)!c).| by Def8
.=Partial_Sums(|.z ExpSeq.|).(n+1)+|.(z#N(n+2))/[*(n+2)!,0*].|
by Th37;
(n+2)!>0 by Th42;
then A12: Partial_Sums(|.z ExpSeq.|).((n+1)+1)
=Partial_Sums(|.z ExpSeq.|).(n+1)+|.(z#N(n+2)).|/((n+2)!)
by A11,Lm19;
(n+2)<(n+3) by REAL_1:53;
then A13:0<(n+2)! & (n+2)!<=(n+3)! by Th42;
|.(z#N(n+2)).|>=0 by COMPLEX1:132;
then |.(z#N(n+2)).|/((n+2)!)>=|.(z#N(n+2)).|/((n+3)!) by A13,REAL_2:201
;
then A14: Partial_Sums(|.z P_dt.|).n+|.(z#N(n+2)).|/((n+3)!)<=
Partial_Sums(|.z P_dt.|).n+|.(z#N(n+2)).|/((n+2)!) by AXIOMS:24;
Partial_Sums(|.z P_dt.|).n+|.(z#N(n+2)).|/((n+2)!)<
Partial_Sums(|.z ExpSeq.|).(n+1)+|.(z#N(n+2)).|/((n+2)!)
by A8,REAL_1:53;
hence thesis by A10,A12,A14,AXIOMS:22;
end;
for n holds X[n] from Ind(A6,A7);
hence thesis;
end;
consider r be real number such that
A15:for n holds Partial_Sums(|.z ExpSeq.|).n<r by SEQ_2:def 3;
A16: for n holds Partial_Sums(|.z P_dt.|).n<r
proof
let n;
A17: Partial_Sums(|.z P_dt.|).n<Partial_Sums(|.z ExpSeq.|).
(n+1) by A1;
Partial_Sums(|.z ExpSeq.|).(n+1)<r by A15;
hence thesis by A17,AXIOMS:22;
end;
take r;
thus thesis by A16,XREAL_0:def 1;
end;
hence thesis by SEQ_2:def 3;
end;
hence thesis by COMSEQ_3:62;
end;
theorem Th62: for z holds z*(Sum(z P_dt))=(Sum(z ExpSeq))-1r-z
proof
let z;
A1:for z holds z (#) (z P_dt)=(z ExpSeq)^\ 2
proof
let z;
for n holds (z(#)(z P_dt)).n=((z ExpSeq)^\ 2).n
proof
let n;
(z(#)(z P_dt)).n=z*(z P_dt).(n) by COMSEQ_1:def 7
.=z*((z#N(n+1))/((n+2)!c)) by Def28;
then (z(#)(z P_dt)).n= (z*(z#N(n+1)))/((n+2)!c) by XCMPLX_1:75
.=(z#N(n+1+1))/((n+2)!c) by Lm14
.=(z#N(n+(1+1)))/((n+2)!c) by XCMPLX_1:1
.=z ExpSeq.(n+2) by Def8
.=((z ExpSeq)^\ 2).n by COMSEQ_3:def 6;
hence thesis;
end;
hence thesis by COMSEQ_1:6;
end;
Sum(z ExpSeq)= Partial_Sums(z ExpSeq).1 + Sum(z ExpSeq^\(1+1)) by COMSEQ_3:
61
.=Partial_Sums(z ExpSeq).1 + Sum(z ExpSeq^\(2));
then Sum(z ExpSeq)= Partial_Sums(z ExpSeq).1 + Sum(z (#) (z P_dt)) by A1;
then A2: Sum(z (#) (z P_dt))=Sum(z ExpSeq) - Partial_Sums(z ExpSeq).(0+1)
by XCMPLX_1:26
.=Sum(z ExpSeq)-(Partial_Sums(z ExpSeq).0+z ExpSeq.1)
by COMSEQ_3:def 7
.=Sum(z ExpSeq)-(z ExpSeq.0+z ExpSeq.1) by COMSEQ_3:def 7
.=Sum(z ExpSeq)-(1r+z ExpSeq.1) by Lm14
.=Sum(z ExpSeq)-(1r+z) by Lm14
.=(Sum(z ExpSeq))-1r-z by XCMPLX_1:36;
reconsider BBB=z P_dt as absolutely_summable Complex_Sequence by Th61;
BBB is summable;
hence thesis by A2,COMSEQ_3:57;
end;
theorem Th63: for p st p>0 holds ex q st q>0 & for z st |.z.|<q
holds |.(Sum(z P_dt)).|<p
proof
A1: for z holds |.(Sum(z P_dt)).| <= Sum (|.z P_dt.|)
proof
let z;
A2:
for k holds
|.Partial_Sums(z P_dt).|.k <= Partial_Sums(|.z P_dt.|).k
proof
let k;
|.Partial_Sums(z P_dt).k.|=|.Partial_Sums(z P_dt).|.k by COMSEQ_1:def 14
;
hence thesis by COMSEQ_3:30;
end;
z P_dt is absolutely_summable by Th61;
then |.z P_dt.| is summable by COMSEQ_3:def 11;
then A3:
Partial_Sums(|.z P_dt.|) is convergent by SERIES_1:def 2;
z P_dt is absolutely_summable by Th61;
then A4: z P_dt is summable by COMSEQ_3:64;
then A5:
Partial_Sums(z P_dt) is convergent Complex_Sequence by COMSEQ_3:def 10;
reconsider PS = Partial_Sums(z P_dt) as convergent Complex_Sequence by A4,
COMSEQ_3:def 10;
A6: |.PS.| is convergent;
A7:
lim|.Partial_Sums(z P_dt).|=|.lim(Partial_Sums(z P_dt)).|
by A5,COMSEQ_2:11;
lim|.Partial_Sums(z P_dt).|<=lim(Partial_Sums(|.z P_dt.|)) by A2,A3,A6,
SEQ_2:32;
then |.lim(Partial_Sums(z P_dt)).|<=Sum (|.z P_dt.|) by A7,SERIES_1:def 3;
hence thesis by COMSEQ_3:def 8;
end;
A8: for z,n holds
|.z P_dt.|.n<=|.z.|*|.z.| GeoSeq.n
proof
let z,n;
A9:|.z P_dt.|.n=|.z P_dt.n.| by COMSEQ_1:def 14
.=|.(z#N(n+1))/((n+2)!c).| by Def28
.=|.(z#N(n+1))/[*(n+2)!,0*].| by Th37;
(n+2)!>0 by Th42;
then A10: |.z P_dt.|.n=|.(z#N(n+1)).|/((n+2)!) by A9,Lm19
.=|.z.||^(n+1)/((n+2)!) by Lm14;
A11: |.z.|*|.z.| GeoSeq.n=|.z.|* (|.z.||^ n) by PREPOWER:def 1
.=|.z.||^(n+1) by NEWTON:11;
n+2-1=n+(2-1) by XCMPLX_1:29
.=n+1;
then 0<=n+2-1 by NAT_1:18; then 1<=n+2 by REAL_2:105;
then 0< n+2 by AXIOMS:22;
then A12: (n+2)!>=1 by Th42,NEWTON:18;
|.z.|>=0 by COMPLEX1:132;
then |.z.||^(n+1) >=0 by POWER:3;
then |.z.||^(n+1)/1>=|.z.||^(n+1)/((n+2)!) by A12,REAL_2:201;
hence thesis by A10,A11;
end;
let p; assume
A13: p>0;
then A14: p+1>0 by Lm13;
consider q such that
A15: q=p/(p+1);
p+1>p by REAL_1:69;
then A16: q <1 by A13,A15,REAL_2:142;
A17: for z st |.z.|<q holds |.(Sum(z P_dt)).|<p
proof
let z; assume
A18: |.z.|<q;
then A19: |.z.|<1 by A16,AXIOMS:22;
abs(|.z.|)<1
proof
0<=|.z.| by COMPLEX1:132;
hence thesis by A19,ABSVALUE:def 1;
end;
then A20: |.z.| GeoSeq is summable & Sum(|.z.| GeoSeq) = 1/(1- |.z.|)
by SERIES_1:28;
then A21: |.z.|(#)|.z.| GeoSeq is summable &
Sum(|.z.|(#)|.z.| GeoSeq) =|.z.|*Sum(|.z.| GeoSeq) by SERIES_1:13;
A22: for n holds |.z P_dt.|.n<=(|.z.|(#)|.z.| GeoSeq).n
proof
let n;
|.z P_dt.|.n<=|.z.|*|.z.| GeoSeq.n by A8;
hence thesis by SEQ_1:13;
end;
for n holds 0<=|.z P_dt.|.n
proof
let n;
|.z P_dt.|.n=|.z P_dt.n.| by COMSEQ_1:def 14;
hence thesis by COMPLEX1:132;
end;
then A23:(|.z P_dt.|) is summable
& Sum(|.z P_dt.|)<=Sum(|.z.|(#)|.z.| GeoSeq) by A21,A22,SERIES_1:24;
A24: Sum(|.z.|(#)|.z.| GeoSeq) =|.z.|/(1- |.z.|) by A20,A21,XCMPLX_1:100
;
|.z.|/(1- |.z.|)<p
proof
A25: |.z.|*(p+1)<(p/(p+1))*(p+1) by A14,A15,A18,REAL_1:70;
A26:(p/(p+1))*(p+1)=p by A14,XCMPLX_1:88;
|.z.|*(p+1)=|.z.|*p+|.z.|*1 by XCMPLX_1:8
.=p*|.z.|+|.z.|;
then A27: p*|.z.|+|.z.|-p*|.z.|<p-p*|.z.| by A25,A26,REAL_1:54;
A28: p*|.z.|+|.z.|-p*|.z.|=p*|.z.|-p*|.z.|+|.z.| by XCMPLX_1:29
.=0+|.z.| by XCMPLX_1:14
.=|.z.|;
A29: p-p*|.z.|= p*1 -p*|.z.|
.=p*(1- |.z.|) by XCMPLX_1:40;
A30: 1- |.z.|>0 by A19,SQUARE_1:11;
then |.z.|/(1- |.z.|)< p*(1- |.z.|)/(1- |.z.|) by A27,A28,A29,
REAL_1:73;
hence thesis by A30,XCMPLX_1:90;
end;
then Sum(|.z P_dt.|)<p & |.(Sum(z P_dt)).|<=Sum
(|.z P_dt.|) by A1,A23,A24,AXIOMS:22;
hence thesis by AXIOMS:22;
end;
take q;
thus thesis by A13,A14,A15,A17,REAL_2:127;
end;
theorem Th64: for z,z1 holds (Sum((z1+z) ExpSeq))-(Sum(z1 ExpSeq))
=(Sum(z1 ExpSeq))*z+z*(Sum(z P_dt))*(Sum(z1 ExpSeq))
proof let z,z1;
(Sum((z1+z) ExpSeq))-(Sum(z1 ExpSeq))
= (Sum(z1 ExpSeq))*(Sum(z ExpSeq))-(Sum(z1 ExpSeq)) by Lm4
.=(Sum(z1 ExpSeq))*(Sum(z ExpSeq))-(Sum(z1 ExpSeq))*1r by COMPLEX1:29
.=(Sum(z1 ExpSeq))*((Sum(z ExpSeq))-1r) by XCMPLX_1:40
.=(Sum(z1 ExpSeq))*(((Sum(z ExpSeq))-1r)-z+z) by XCMPLX_1:27
.=(Sum(z1 ExpSeq))* (z*(Sum(z P_dt))+z) by Th62
.=(Sum(z1 ExpSeq))*z +z*(Sum(z P_dt))*(Sum(z1 ExpSeq)) by XCMPLX_1:8;
hence thesis;
end;
theorem Th65: for p,q holds cos.(p+q)-cos.p=
-q*sin.p -q*Im((Sum([*0,q*] P_dt))* [*cos.p,sin.p*])
proof
let p,q;
cos.(p+q)-cos.p=cos.(p+q)-Re(Sum([*0,p*] ExpSeq)) by Def22
.=Re(Sum([*0,p+q*] ExpSeq))-Re(Sum([*0,p*] ExpSeq)) by Def22
.=Re(Sum([*0+0,p+q*] ExpSeq)-Sum([*0,p*] ExpSeq)) by COMPLEX1:48
.=Re(Sum(([*0,p*]+[*0,q*]) ExpSeq)-Sum([*0,p*] ExpSeq)) by Lm13
.=Re((Sum([*0,p*] ExpSeq))*[*0,q*]
+[*0,q*]*(Sum([*0,q*] P_dt))*(Sum([*0,p*] ExpSeq))) by Th64
.=Re([*cos.p,sin.p*]*[*0,q*]+[*0,q*]*(Sum([*0,q*] P_dt))*(Sum
([*0,p*] ExpSeq)))
by Lm6
.= Re([*cos.p,sin.p*]*[*0,q*]+[*0,q*]*(Sum([*0,q*] P_dt))* [*cos.p,sin.p*])
by Lm6
.= Re([*cos.p,sin.p*]*[*0,q*])+
Re([*0,q*]*(Sum([*0,q*] P_dt))* [*cos.p,sin.p*])
by COMPLEX1:19
.=Re[*-q*sin.p,q*cos.p*]+Re([*0,q*]*(Sum([*0,q*] P_dt))* [*cos.p,sin.p*])
by Lm10
.= -q*sin.p +Re([*0,q*]*(Sum([*0,q*] P_dt))* [*cos.p,sin.p*]) by COMPLEX1:7
.=-q*sin.p+Re([*0,q*]*((Sum([*0,q*] P_dt))* [*cos.p,sin.p*])) by XCMPLX_1:4
.=-q*sin.p+-q*Im((Sum([*0,q*] P_dt))* [*cos.p,sin.p*]) by Lm18
.=-q*sin.p-q*Im((Sum([*0,q*] P_dt))* [*cos.p,sin.p*]) by XCMPLX_0:def 8;
hence thesis;
end;
theorem Th66: for p,q holds sin.(p+q)-sin.p=
q*cos.p+q*Re((Sum([*0,q*] P_dt))* [*cos.p,sin.p*])
proof
let p,q;
sin.(p+q)-sin.p=sin.(p+q)-Im(Sum([*0,p*] ExpSeq)) by Def20
.=Im(Sum([*0,p+q*] ExpSeq))-Im(Sum([*0,p*] ExpSeq)) by Def20
.=Im(Sum([*0+0,p+q*] ExpSeq)-Sum([*0,p*] ExpSeq)) by COMPLEX1:48
.=Im(Sum(([*0,p*]+[*0,q*]) ExpSeq)-Sum([*0,p*] ExpSeq)) by Lm13
.=Im((Sum([*0,p*] ExpSeq))*[*0,q*]
+[*0,q*]*(Sum([*0,q*] P_dt))*(Sum([*0,p*] ExpSeq))) by Th64
.=Im([*cos.p,sin.p*]*[*0,q*]+[*0,q*]*(Sum([*0,q*] P_dt))*(Sum
([*0,p*] ExpSeq)))
by Lm6
.= Im([*cos.p,sin.p*]*[*0,q*]+[*0,q*]*(Sum([*0,q*] P_dt))* [*cos.p,sin.p*])
by Lm6
.= Im([*cos.p,sin.p*]*[*0,q*])+
Im([*0,q*]*(Sum([*0,q*] P_dt))* [*cos.p,sin.p*])
by COMPLEX1:19
.=Im[*-q*sin.p,q*cos.p*]+Im([*0,q*]*(Sum([*0,q*] P_dt))* [*cos.p,sin.p*])
by Lm10
.= q*cos.p +Im([*0,q*]*(Sum([*0,q*] P_dt))* [*cos.p,sin.p*]) by COMPLEX1:7
.=q*cos.p+Im([*0,q*]*((Sum([*0,q*] P_dt))* [*cos.p,sin.p*])) by XCMPLX_1:4
.=q*cos.p+q*Re((Sum([*0,q*] P_dt))* [*cos.p,sin.p*]) by Lm18;
hence thesis;
end;
theorem Th67: for p,q holds exp.(p+q)-exp.p=
q* (exp.p)+q*exp.p*Re((Sum([*q,0*] P_dt)))
proof
let p,q;
exp.(p+q)-exp.p=exp.(p+q)-Re(Sum([*p,0*] ExpSeq)) by Th53
.=Re(Sum([*p+q,0*] ExpSeq))-Re(Sum([*p,0*] ExpSeq)) by Th53
.=Re(Sum([*p+q,0+0*] ExpSeq)-Sum([*p,0*] ExpSeq)) by COMPLEX1:48
.=Re(Sum(([*p,0*]+[*q,0*]) ExpSeq)-Sum([*p,0*] ExpSeq)) by Lm13
.=Re((Sum([*p,0*] ExpSeq))*[*q,0*]
+[*q,0*]*(Sum([*q,0*] P_dt))*(Sum([*p,0*] ExpSeq))) by Th64
.=Re((Sum([*p,0*] ExpSeq))*[*q,0*])+
Re([*q,0*]*(Sum([*q,0*] P_dt))*(Sum([*p,0*] ExpSeq))) by COMPLEX1:19
.=q*Re(Sum([*p,0*] ExpSeq))+
Re([*q,0*]*(Sum([*q,0*] P_dt))*(Sum([*p,0*] ExpSeq))) by Lm18
.=q* (exp.p)+ Re([*q,0*]*(Sum([*q,0*] P_dt))*(Sum([*p,0*] ExpSeq))) by Th53
.=q* (exp.p)+ Re([*q,0*]*((Sum([*q,0*] P_dt))*(Sum([*p,0*] ExpSeq))))
by XCMPLX_1:4
.=q* (exp.p)+ q*Re((Sum([*q,0*] P_dt))*(Sum([*p,0*] ExpSeq))) by Lm18
.=q* (exp.p)+ q*Re((Sum([*q,0*] P_dt))*[*Sum(p ExpSeq),0*]) by Lm15
.=q* (exp.p)+q*Re((Sum([*q,0*] P_dt))*[*exp.p,0*]) by Def26
.=q* (exp.p)+q*(exp.p*Re((Sum([*q,0*] P_dt)))) by Lm18
.=q* (exp.p)+q*exp.p*Re((Sum([*q,0*] P_dt))) by XCMPLX_1:4;
hence thesis;
end;
theorem Th68:
for p holds cos is_differentiable_in p & diff(cos,p)=-sin.p
proof
let p;
defpred X[set] means $1 in REAL;
deffunc U(Element of REAL) =
- $1* Im((Sum([*0,$1*] P_dt))* [*cos.p,sin.p*]);
consider C_r being PartFunc of REAL, REAL such that
A1: for th be Real holds th in dom C_r iff X[th] and
A2: for th be Real st th in dom C_r holds C_r/.th = U(th)
from LambdaPFD;
A3:dom C_r=REAL
proof
A4: dom(C_r) c=REAL by RELSET_1:12;
for x be set st x in REAL holds x in dom C_r by A1;
then REAL c=dom(C_r) by TARSKI:def 3;
hence dom(C_r)=REAL by A4,XBOOLE_0:def 10;
end;
then A5: C_r is total by PARTFUN1:def 4;
A6: C_r.d = - d* Im((Sum([*0,d*] P_dt))* [*cos.p,sin.p*])
proof
A7: d in dom C_r by A1;
then C_r/.d = -d* Im((Sum([*0,d*] P_dt))* [*cos.p,sin.p*]) by A2;
hence C_r.d = -d* Im((Sum([*0,d*] P_dt))* [*cos.p,sin.p*])
by A7,FINSEQ_4:def 4;
end;
C_r is REST-like PartFunc of REAL,REAL
proof
for hy1 holds
(hy1")(#)(C_r*hy1) is convergent & lim ((hy1")(#)(C_r*hy1)) = 0
proof
let hy1;
A8: for n holds
((hy1")(#)(C_r*hy1)).n
=-Im((Sum([*0,(hy1.n)*] P_dt))* [*cos.p,sin.p*])
proof
let n;
A9: ((hy1")(#)(C_r*hy1)).n=(hy1".n)*((C_r*hy1).n) by SEQ_1:12
.=(hy1.n)"*((C_r*hy1).n) by SEQ_1:def 8;
rng hy1 c= dom C_r by A3;
then A10: ((hy1")(#)(C_r*hy1)).n=
(hy1.n)"*(C_r.(hy1.n)) by A9,RFUNCT_2:21
.=(hy1.n)"*( -(hy1.n)* Im((Sum([*0,(hy1.n)*] P_dt))*
[*cos.p,sin.p*])) by A6
.= -(hy1.n)"*((hy1.n)* Im((Sum([*0,(hy1.n)*] P_dt))*
[*cos.p,sin.p*])) by XCMPLX_1:175
.=-(hy1.n)"*(hy1.n)* Im((Sum([*0,(hy1.n)*] P_dt))*
[*cos.p,sin.p*]) by XCMPLX_1:4;
hy1 is_not_0 by FDIFF_1:def 1; then hy1.n<>0 by SEQ_1:7;
then ((hy1")(#)(C_r*hy1)).n
=-1*Im((Sum([*0,(hy1.n)*] P_dt))* [*cos.p,sin.p*])
by A10,XCMPLX_0:def 7
.=-Im((Sum([*0,(hy1.n)*] P_dt))* [*cos.p,sin.p*]);
hence thesis;
end;
deffunc U(Real) = -Im((Sum([*0,(hy1.$1)*] P_dt))* [*cos.p,sin.p*]);
consider rseq such that
A11: for n holds rseq.n= U(n) from ExRealSeq;
deffunc U(Nat) = (Sum([*0,(hy1.$1)*] P_dt))* [*cos.p,sin.p*];
consider cq1 such that
A12: for n holds
cq1.n=U(n) from ExComplexSeq;
A13:cq1 is convergent & lim(cq1)=0c
proof
A14: for q be Real st q>0 holds ex k st for m st k<=m holds
|.cq1.m-0c.|<q
proof
let q be Real such that
A15: q>0;
ex k st for m st k<=m holds |.cq1.m-0c.|<q
proof
consider r such that
A16: r>0 & for z st |.z.|<r holds |.(Sum
(z P_dt)).|<q by A15,Th63;
hy1 is convergent&lim(hy1)=0 by FDIFF_1:def 1;
then consider k such that
A17: for m st k<=m holds abs(hy1.m-0)<r by A16,SEQ_2:def 7;
A18: now let m such that
A19: k<=m;
A20: |.cq1.m-0c.|= |.(Sum([*0,(hy1.m)*] P_dt))* [*cos.p,sin.p*]
.| by A12
.= |.(Sum([*0,(hy1.m)*] P_dt)).|* |.[*cos.p,sin.p*].| by COMPLEX1:151
.= |.(Sum([*0,(hy1.m)*] P_dt)).|* |.Sum([*0,p*] ExpSeq ).| by Lm6
.=|.(Sum([*0,(hy1.m)*] P_dt)).|*1 by Lm8
.=|.(Sum([*0,(hy1.m)*] P_dt)).|;
A21: abs(hy1.m-0)<r by A17,A19;
Re[*0,(hy1.m)*]=0 & Im[*0,(hy1.m)*]=hy1.m by COMPLEX1:7;
then |.[*0,(hy1.m)*].|
= sqrt((0)^2 + (hy1.m)^2) by COMPLEX1:def 16
.=abs(hy1.m) by SQUARE_1:60,91;
hence |.cq1.m-0c.|<q by A16,A20,A21;
end;
take k;
thus for m st k<=m holds |.cq1.m-0c.|<q by A18;
end;
hence thesis;
end;
then cq1 is convergent by COMSEQ_2:def 4;
hence thesis by A14,COMSEQ_2:def 5;
end;
then A22: -cq1 is convergent by COMSEQ_2:21;
A23: lim(-cq1)=0c by A13,COMSEQ_2:22,REAL_1:26;
A24: for n holds Im(-cq1).n= rseq.n
proof
A25: for n holds
Im(-cq1).n=-Im((Sum([*0,(hy1.n)*] P_dt))* [*cos.p,sin.p*])
proof
let n;
Im(-cq1).n=Im((-cq1).n) by COMSEQ_3:def 4
.=Im(-cq1.n) by COMSEQ_1:def 9
.=Im(-(Sum([*0,(hy1.n)*] P_dt))* [*cos.p,sin.p*])
by A12
.=-Im((Sum([*0,(hy1.n)*] P_dt))* [*cos.p,sin.p*])
by COMPLEX1:34;
hence thesis;
end;
let n;
rseq.n=-Im((Sum([*0,(hy1.n)*] P_dt))* [*cos.p,sin.p*]) by A11;
hence thesis by A25;
end;
rseq=(hy1")(#)(C_r*hy1)
proof
for n holds rseq.n=((hy1")(#)(C_r*hy1)).n
proof
let n;
rseq.n=-Im((Sum([*0,(hy1.n)*] P_dt))* [*cos.p,sin.p*]) by A11;
hence thesis by A8;
end;
hence thesis by FUNCT_2:113;
end;
then (hy1")(#)(C_r*hy1)=Im(-cq1) by A24,FUNCT_2:113;
hence thesis by A22,A23,COMPLEX1:12,COMSEQ_3:41;
end;
hence thesis by A5,FDIFF_1:def 3;
end;
then reconsider PR = C_r as REST-like PartFunc of REAL,REAL;
reconsider PR as REST;
defpred X[set] means $1 in REAL;
deffunc U(Element of REAL) = -$1*sin.p;
consider CL being PartFunc of REAL, REAL such that
A26: for th be Real holds th in dom CL iff X[th] and
A27: for th be Real st th in dom CL holds CL/.th= U(th)
from LambdaPFD;
A28: for d be real number holds CL.d = -d*sin.p
proof
let d be real number;
A29: d is Real by XREAL_0:def 1;
then A30: d in dom CL by A26;
then CL/.d = -d*sin.p by A27,A29;
hence CL.d = -d*sin.p by A30,FINSEQ_4:def 4;
end;
dom CL=REAL
proof
A31: dom(CL) c=REAL by RELSET_1:12;
for x be set st x in REAL holds x in dom CL by A26;
then REAL c=dom(CL) by TARSKI:def 3;
hence dom(CL)=REAL by A31,XBOOLE_0:def 10;
end;
then A32: CL is total by PARTFUN1:def 4;
CL is linear PartFunc of REAL,REAL
proof
ex r be Real st for q be Real holds CL.q=r*q
proof
A33: for q be Real holds CL.q=(-sin.p)*q
proof
let q be Real;
CL.q= -q*sin.p by A28
.=(-sin.p)*q by XCMPLX_1:175;
hence thesis;
end;
take (-sin.p);
thus thesis by A33;
end;
hence thesis by A32,FDIFF_1:def 4;
end;
then reconsider PL = CL as linear PartFunc of REAL,REAL;
reconsider PL as LINEAR;
A34: ex N being Neighbourhood of p st N c= dom cos &
for r st r in N holds
cos.r - cos.p = PL.(r-p) + PR.(r-p)
proof
A35: for r st r in ].p-1,p+1 .[ holds cos.r - cos.p = PL.(r-p) + PR.(r-p)
proof
let r;
r=r+p-p by XCMPLX_1:26
.=p+(r-p) by XCMPLX_1:29;
then cos.r - cos.p
=-(r-p)*sin.p -(r-p)*Im((Sum([*0,(r-p)*] P_dt))* [*cos.p,sin.p*]) by Th65
.=-(r-p)*sin.p+(-(r-p)*Im((Sum([*0,(r-p)*] P_dt))*[*cos.p,sin.p*]))
by XCMPLX_0:def 8
.=-(r-p)*sin.p+C_r.(r-p) by A6
.=PL.(r-p) + PR.(r-p) by A28;
hence thesis;
end;
take ].p-1,p+1 .[;
thus thesis by A35,Th27,RCOMP_1:def 7;
end;
then A36: cos is_differentiable_in p by FDIFF_1:def 5;
PL.1= -1*sin.p by A28
.=-sin.p;
hence thesis by A34,A36,FDIFF_1:def 6;
end;
theorem Th69:
for p holds sin is_differentiable_in p & diff(sin,p)=cos.p
proof
let p;
defpred X[set] means $1 in REAL;
deffunc U(Element of REAL) =
$1 *Re((Sum([*0,$1*] P_dt))* [*cos.p,sin.p*]);
consider C_r being PartFunc of REAL, REAL such that
A1: for th be Real holds th in dom C_r iff X[th] and
A2: for th be Real st th in dom C_r holds C_r/.th = U(th) from LambdaPFD;
A3:dom C_r=REAL
proof
A4: dom(C_r) c=REAL by RELSET_1:12;
for x be set st x in REAL holds x in dom C_r by A1;
then REAL c=dom(C_r) by TARSKI:def 3;
hence dom(C_r)=REAL by A4,XBOOLE_0:def 10;
end;
then A5: C_r is total by PARTFUN1:def 4;
A6: C_r.d = d*Re((Sum([*0,d*] P_dt))* [*cos.p,sin.p*])
proof
A7: d in dom C_r by A1;
then C_r/.d = d*Re((Sum([*0,d*] P_dt))* [*cos.p,sin.p*]) by A2;
hence C_r.d = d*Re((Sum([*0,d*] P_dt))* [*cos.p,sin.p*])
by A7,FINSEQ_4:def 4;
end;
C_r is REST-like PartFunc of REAL,REAL
proof
for hy1 holds
(hy1")(#)(C_r*hy1) is convergent & lim ((hy1")(#)(C_r*hy1)) = 0
proof
let hy1;
A8: for n holds
((hy1")(#)(C_r*hy1)).n
=Re((Sum([*0,hy1.n*] P_dt))* [*cos.p,sin.p*])
proof
let n;
A9: ((hy1")(#)(C_r*hy1)).n=(hy1".n)*((C_r*hy1).n) by SEQ_1:12
.=(hy1.n)"*((C_r*hy1).n) by SEQ_1:def 8;
rng hy1 c= dom C_r by A3;
then A10: ((hy1")(#)(C_r*hy1)).n=
(hy1.n)"*(C_r.(hy1.n)) by A9,RFUNCT_2:21
.=(hy1.n)"*( (hy1.n)*Re((Sum([*0,hy1.n*] P_dt))*
[*cos.p,sin.p*])) by A6
.=(hy1.n)"*(hy1.n)* Re((Sum([*0,hy1.n*] P_dt))*
[*cos.p,sin.p*]) by XCMPLX_1:4;
hy1 is_not_0 by FDIFF_1:def 1; then hy1.n<>0 by SEQ_1:7;
then ((hy1")(#)(C_r*hy1)).n
=1*Re((Sum([*0,hy1.n*] P_dt))* [*cos.p,sin.p*])
by A10,XCMPLX_0:def 7
.=Re((Sum([*0,hy1.n*] P_dt))* [*cos.p,sin.p*]);
hence thesis;
end;
deffunc U(Real) = Re((Sum([*0,hy1.$1*] P_dt))* [*cos.p,sin.p*]);
consider rseq such that
A11: for n holds rseq.n= U(n) from ExRealSeq;
deffunc U(Nat) = (Sum([*0,(hy1.$1)*] P_dt))* [*cos.p,sin.p*];
consider cq1 such that
A12: for n holds
cq1.n= U(n) from ExComplexSeq;
A13:cq1 is convergent & lim(cq1)=0c
proof
A14: for q be Real st q>0 holds ex k st for m st k<=m holds
|.cq1.m-0c.|<q
proof
let q be Real such that
A15: q>0;
ex k st for m st k<=m holds |.cq1.m-0c.|<q
proof
consider r such that
A16: r>0 & for z st |.z.|<r holds |.(Sum
(z P_dt)).|<q by A15,Th63;
hy1 is convergent&lim(hy1)=0 by FDIFF_1:def 1;
then consider k such that
A17: for m st k<=m holds abs(hy1.m-0)<r by A16,SEQ_2:def 7;
A18: now let m such that
A19: k<=m;
A20: |.cq1.m-0c.|= |.(Sum([*0,(hy1.m)*] P_dt))* [*cos.p,sin.p*].| by A12
.= |.(Sum([*0,(hy1.m)*] P_dt)).|* |.[*cos.p,sin.p*].|
by COMPLEX1:151
.= |.(Sum([*0,(hy1.m)*] P_dt)).|* |.Sum([*0,p*] ExpSeq ).|
by Lm6
.=|.(Sum([*0,(hy1.m)*] P_dt)).|*1 by Lm8
.=|.(Sum([*0,(hy1.m)*] P_dt)).|;
A21: abs(hy1.m-0)<r by A17,A19;
Re[*0,(hy1.m)*]=0 & Im[*0,(hy1.m)*]=hy1.m by COMPLEX1:7;
then |.[*0,(hy1.m)*].|
= sqrt((0)^2 + (hy1.m)^2) by COMPLEX1:def 16
.=abs(hy1.m) by SQUARE_1:60,91;
hence |.cq1.m-0c.|<q by A16,A20,A21;
end;
take k;
thus for m st k<=m holds |.cq1.m-0c.|<q by A18;
end;
hence thesis;
end;
then cq1 is convergent by COMSEQ_2:def 4;
hence thesis by A14,COMSEQ_2:def 5;
end;
A22: for n holds Re(cq1).n= rseq.n
proof
let n;
Re(cq1).n=Re((cq1).n) by COMSEQ_3:def 3
.=Re((Sum([*0,(hy1.n)*] P_dt))* [*cos.p,sin.p*]) by A12;
hence thesis by A11;
end;
rseq=(hy1")(#)(C_r*hy1)
proof
for n holds rseq.n=((hy1")(#)(C_r*hy1)).n
proof
let n;
rseq.n=Re((Sum([*0,(hy1.n)*] P_dt))* [*cos.p,sin.p*]) by A11
;
hence thesis by A8;
end;
hence thesis by FUNCT_2:113;
end;
then (hy1")(#)(C_r*hy1)=Re(cq1) by A22,FUNCT_2:113;
hence thesis by A13,COMPLEX1:12,COMSEQ_3:41;
end;
hence thesis by A5,FDIFF_1:def 3;
end;
then reconsider PR = C_r as REST-like PartFunc of REAL,REAL;
reconsider PR as REST;
defpred X[set] means $1 in REAL;
deffunc U(Element of REAL) = $1*cos.p;
consider CL being PartFunc of REAL, REAL such that
A23: for th be Real holds th in dom CL iff X[th] and
A24: for th be Real st th in dom CL holds CL/.th=U(th) from LambdaPFD;
A25: for d be real number holds CL.d = d*cos.p
proof
let d be real number;
A26: d is Real by XREAL_0:def 1;
then A27: d in dom CL by A23;
then CL/.d = d*cos.p by A24,A26;
hence CL.d = d*cos.p by A27,FINSEQ_4:def 4;
end;
dom CL=REAL
proof
A28: dom(CL) c=REAL by RELSET_1:12;
for x be set st x in REAL holds x in dom CL by A23;
then REAL c=dom(CL) by TARSKI:def 3;
hence dom(CL)=REAL by A28,XBOOLE_0:def 10;
end;
then A29: CL is total by PARTFUN1:def 4;
CL is linear PartFunc of REAL,REAL
proof
ex r be Real st for q be Real holds CL.q=r*q
proof
take (cos.p);
thus thesis by A25;
end;
hence thesis by A29,FDIFF_1:def 4;
end;
then reconsider PL = CL as linear PartFunc of REAL,REAL;
reconsider PL as LINEAR;
A30: ex N being Neighbourhood of p st N c= dom sin &
for r st r in N holds
sin.r - sin.p = PL.(r-p) + PR.(r-p)
proof
A31: for r st r in ].p-1,p+1 .[ holds sin.r - sin.p = PL.(r-p) + PR.(r-p)
proof
let r;
r=r+p-p by XCMPLX_1:26
.=p+(r-p) by XCMPLX_1:29;
then sin.r - sin.p
=(r-p)*cos.p +(r-p)*Re((Sum([*0,(r-p)*] P_dt))* [*cos.p,sin.p*]) by Th66
.=(r-p)*cos.p +C_r.(r-p) by A6
.=PL.(r-p) + PR.(r-p) by A25;
hence thesis;
end;
take ].p-1,p+1 .[;
thus thesis by A31,Th27,RCOMP_1:def 7;
end;
then A32: sin is_differentiable_in p by FDIFF_1:def 5;
PL.1= 1*cos.p by A25;
hence thesis by A30,A32,FDIFF_1:def 6;
end;
theorem Th70:
for p holds exp is_differentiable_in p & diff(exp,p)=exp.p
proof
let p;
defpred X[set] means $1 in REAL;
deffunc U(Element of REAL) = $1 *exp.p*Re((Sum([*$1,0*] P_dt)));
consider C_r being PartFunc of REAL, REAL such that
A1: for th be Real holds th in dom C_r iff X[th] and
A2: for th be Real st th in dom C_r holds C_r/.th =U(th)
from LambdaPFD;
A3:dom C_r=REAL
proof
A4: dom(C_r) c=REAL by RELSET_1:12;
for x be set st x in REAL holds x in dom C_r by A1;
then REAL c=dom(C_r) by TARSKI:def 3;
hence dom(C_r)=REAL by A4,XBOOLE_0:def 10;
end;
then A5: C_r is total by PARTFUN1:def 4;
A6: C_r.d = d*exp.p*Re((Sum([*d,0*] P_dt)))
proof
A7: d in dom C_r by A1;
then C_r/.d = d*exp.p*Re((Sum([*d,0*] P_dt))) by A2;
hence C_r.d = d*exp.p*Re((Sum([*d,0*] P_dt))) by A7,FINSEQ_4:def 4;
end;
C_r is REST-like PartFunc of REAL,REAL
proof
for hy1 holds
(hy1")(#)(C_r*hy1) is convergent & lim ((hy1")(#)(C_r*hy1)) = 0
proof
let hy1;
A8: for n holds
((hy1")(#)(C_r*hy1)).n
=exp.p*Re((Sum([*(hy1.n),0*] P_dt)))
proof
let n;
A9: ((hy1")(#)(C_r*hy1)).n=(hy1".n)*((C_r*hy1).n) by SEQ_1:12
.=(hy1.n)"*((C_r*hy1).n) by SEQ_1:def 8;
rng hy1 c= dom C_r by A3;
then A10: ((hy1")(#)(C_r*hy1)).n=
(hy1.n)"*(C_r.(hy1.n)) by A9,RFUNCT_2:21
.=(hy1.n)"*( (hy1.n)*exp.p*Re((Sum([*(hy1.n),0*] P_dt))))
by A6
.=(hy1.n)"*( (hy1.n)*(exp.p*Re((Sum([*(hy1.n),0*] P_dt)))))
by XCMPLX_1:4
.=(hy1.n)"*(hy1.n)* (exp.p*Re((Sum([*(hy1.n),0*] P_dt))))
by XCMPLX_1:4;
hy1 is_not_0 by FDIFF_1:def 1; then hy1.n<>0 by SEQ_1:7;
then ((hy1")(#)(C_r*hy1)).n
=1*(exp.p*Re((Sum([*(hy1.n),0*] P_dt)))) by A10,XCMPLX_0:def
7
.=exp.p*Re((Sum([*(hy1.n),0*] P_dt)));
hence thesis;
end;
deffunc U(Real) = exp.p*Re((Sum([*(hy1.$1),0*] P_dt)));
consider rseq such that
A11: for n holds rseq.n= U(n) from ExRealSeq;
deffunc U(Nat) = (Sum([*(hy1.$1),0*] P_dt))*[*exp.p,0*];
consider cq1 such that
A12: for n holds
cq1.n= U(n) from ExComplexSeq;
A13:cq1 is convergent & lim(cq1)=0c
proof
A14: for q be Real st q>0 holds ex k st for m st k<=m holds
|.cq1.m-0c.|<q
proof
let q be Real such that
A15: q>0;
ex k st for m st k<=m holds |.cq1.m-0c.|<q
proof
exp.p>0 by Th59;
then q/exp.p>0 by A15,REAL_2:127;
then consider r such that
A16: r>0 & for z st |.z.|<r holds |.(Sum(z P_dt)).|<q/exp.p
by Th63;
hy1 is convergent&lim(hy1)=0 by FDIFF_1:def 1;
then consider k such that
A17: for m st k<=m holds abs(hy1.m-0)<r by A16,SEQ_2:def 7;
A18: now let m such that
A19: k<=m;
A20: |.cq1.m-0c.|= |.(Sum([*(hy1.m),0*] P_dt))* [*exp.p,0*].|
by A12
.= |.(Sum([*(hy1.m),0*] P_dt)).|* |.[*exp.p,0*].|
by COMPLEX1:151
.= |.(Sum([*(hy1.m),0*] P_dt)).|*
sqrt((Re [*exp.p,0*])^2 + (Im [*exp.p,0*])^2) by COMPLEX1:def 16;
A21: Re[*exp.p,0*]=exp.p & Im[*exp.p,0*]=0 by COMPLEX1:7;
A22: exp.p>0 by Th59;
then A23: |.cq1.m-0c.|
=|.(Sum([*(hy1.m),0*] P_dt)).|* (exp.p)
by A20,A21,SQUARE_1:60,89;
A24: abs(hy1.m-0)<r by A17,A19;
Re[*(hy1.m),0*]=hy1.m & Im[*(hy1.m),0*]=0 by COMPLEX1:7;
then |.[*(hy1.m),0*].|= sqrt( (hy1.m)^2+(0)^2 ) by COMPLEX1:
def 16
.=abs(hy1.m) by SQUARE_1:60,91;
then |.(Sum([*(hy1.m),0*] P_dt)).|<q/exp.p by A16,A24;
then |.cq1.m-0c.|<q/exp.p * exp.p by A22,A23,REAL_1:70;
hence |.cq1.m-0c.|<q by A22,XCMPLX_1:88;
end;
take k;
thus for m st k<=m holds |.cq1.m-0c.|<q by A18;
end;
hence thesis;
end;
then cq1 is convergent by COMSEQ_2:def 4;
hence thesis by A14,COMSEQ_2:def 5;
end;
A25: for n holds Re(cq1).n= rseq.n
proof
A26: for n holds
Re(cq1).n=exp.p*Re((Sum([*(hy1.n),0*] P_dt)))
proof
let n;
Re(cq1).n=Re(cq1.n) by COMSEQ_3:def 3
.=Re((Sum([*(hy1.n),0*] P_dt))*[*exp.p,0*])
by A12
.=exp.p*Re((Sum([*(hy1.n),0*] P_dt)))
by Lm18;
hence thesis;
end;
let n;
rseq.n=exp.p*Re((Sum([*(hy1.n),0*] P_dt))) by A11;
hence thesis by A26;
end;
rseq=(hy1")(#)(C_r*hy1)
proof
for n holds rseq.n=((hy1")(#)(C_r*hy1)).n
proof
let n;
rseq.n=exp.p*Re((Sum([*(hy1.n),0*] P_dt))) by A11;
hence thesis by A8;
end;
hence thesis by FUNCT_2:113;
end;
then (hy1")(#)(C_r*hy1)=Re(cq1) by A25,FUNCT_2:113;
hence thesis by A13,COMPLEX1:12,COMSEQ_3:41;
end;
hence thesis by A5,FDIFF_1:def 3;
end;
then reconsider PR = C_r as REST-like PartFunc of REAL,REAL;
reconsider PR as REST;
defpred X[set] means $1 in REAL;
deffunc U(Element of REAL) = $1* (exp.p);
consider CL being PartFunc of REAL, REAL such that
A27: for th be Real holds th in dom CL iff X[th] and
A28: for th be Real st th in dom CL holds CL/.th=U(th) from LambdaPFD;
A29: for d be real number holds CL.d = d* (exp.p)
proof
let d be real number;
A30: d is Real by XREAL_0:def 1;
then A31: d in dom CL by A27;
then CL/.d = d* (exp.p) by A28,A30;
hence CL.d =d* (exp.p) by A31,FINSEQ_4:def 4;
end;
dom CL=REAL
proof
A32: dom(CL) c=REAL by RELSET_1:12;
for x be set st x in REAL holds x in dom CL by A27;
then REAL c=dom(CL) by TARSKI:def 3;
hence dom(CL)=REAL by A32,XBOOLE_0:def 10;
end;
then A33: CL is total by PARTFUN1:def 4;
CL is linear PartFunc of REAL,REAL
proof
ex r be Real st for q be Real holds CL.q=r*q
proof
take (exp.p);
thus thesis by A29;
end;
hence thesis by A33,FDIFF_1:def 4;
end;
then reconsider PL = CL as linear PartFunc of REAL,REAL;
reconsider PL as LINEAR;
A34: ex N being Neighbourhood of p st N c= dom exp &
for r st r in N holds
exp.r - exp.p = PL.(r-p) + PR.(r-p)
proof
A35: for r st r in ].p-1,p+1 .[ holds exp.r - exp.p = PL.(r-p) + PR.(r-p)
proof
let r;
r=r+p-p by XCMPLX_1:26
.=p+(r-p) by XCMPLX_1:29;
then exp.r - exp.p =(r-p)* (exp.p)+(r-p)*exp.p*Re((Sum([*(r-p),0*] P_dt)))
by Th67
.=(r-p)* (exp.p)+C_r.(r-p) by A6
.=PL.(r-p) + PR.(r-p) by A29;
hence thesis;
end;
take ].p-1,p+1 .[;
thus thesis by A35,Th51,RCOMP_1:def 7;
end;
then A36: exp is_differentiable_in p by FDIFF_1:def 5;
PL.1= 1*exp.p by A29;
hence thesis by A34,A36,FDIFF_1:def 6;
end;
theorem
(exp is_differentiable_on REAL) &
(for th st th in REAL holds diff(exp,th)=exp.(th))
proof
REAL is open Subset of REAL&
REAL c=dom exp & for r st r in REAL holds exp is_differentiable_in r
by Def26,Th70,FCONT_3:4,SUBSET_1:def 4;
hence thesis by Th70,FDIFF_1:16;
end;
theorem Th72:
(cos is_differentiable_on REAL) &
(for th st th in REAL holds diff(cos,th)=-sin.(th))
proof
REAL is open Subset of REAL&
REAL c=dom cos & for r st r in REAL holds cos is_differentiable_in r
by Def22,Th68,FCONT_3:4,SUBSET_1:def 4;
hence thesis by Th68,FDIFF_1:16;
end;
theorem Th73:
sin is_differentiable_on REAL &
(for th holds diff(sin,th)=cos.(th))
proof
REAL is open Subset of REAL&
REAL c=dom sin & for r st r in REAL holds sin is_differentiable_in r
by Def20,Th69,FCONT_3:4,SUBSET_1:def 4;
hence thesis by Th69,FDIFF_1:16;
end;
theorem Th74:
for th st th in [.0,1 .] holds 0<cos.(th) & cos.(th)>=1/2
proof
let th; assume th in [.0,1 .];
then A1: 0<=th & th<=1 by TOPREAL5:1;
A2: (Partial_Sums(th P_cos))*bq is_subsequence_of Partial_Sums(th P_cos)
by SEQM_3:def 10;
A3: Partial_Sums(th P_cos) is convergent & cos.th=Sum
(th P_cos) by Th39,Th40;
then A4: (Partial_Sums(th P_cos))*bq is convergent by A2,SEQ_4:29;
lim ((Partial_Sums(th P_cos))*bq )=lim(Partial_Sums(th P_cos)) by A2,A3,
SEQ_4:30;
then A5: lim ((Partial_Sums(th P_cos))*bq )= cos.th by A3,SERIES_1:def 3;
for n holds ((Partial_Sums(th P_cos))*bq).n >=1/2
proof
let n;
A6: ((Partial_Sums(th P_cos))*bq).0=(Partial_Sums(th P_cos)).(bq.0)
by SEQM_3:31
.= (Partial_Sums(th P_cos)).(2*0+1) by Lm11
.= (Partial_Sums(th P_cos)).0+(th P_cos).(0+1) by SERIES_1:def 1
.= (th P_cos).0 +(th P_cos).(0+1) by SERIES_1:def 1
.= (-1)|^ 0 * (th)|^ (2*0)/((2*0)!)+(th P_cos).1 by Def25
.= (-1)|^ 0 * (th)|^ (2*0)/((2*0)!)+
(-1)|^ 1 * (th)|^ (2*1)/((2*1)!) by Def25
.= 1* (th)|^ (2*0)/((2*0)!)+
(-1)|^ 1 * (th)|^ (2*1)/((2*1)!) by Lm12
.= 1/1 + (-1)|^ 1 * (th)|^ (2*1)/((2*1)!) by Lm12,NEWTON:18
.= 1+ (-1)* (th)|^ (2*1)/((2*1)!) by Lm12
.= 1+ (-1)*(th*th)/((2*1)!) by Lm12
.= 1+(-(th*th))/2 by NEWTON:20,XCMPLX_1:180
.= 1+ -(th*th)/2 by XCMPLX_1:188
.= 1-(th*th)/2 by XCMPLX_0:def 8
.= 1-(th^2)/2 by SQUARE_1:def 3;
A7: 1 - 1/2 = 1/2;
defpred X[Nat] means ((Partial_Sums(th P_cos))*bq).$1 >= 1/2;
th^2 <= 1^2 by A1,SQUARE_1:77;
then th^2 <=1*1 by SQUARE_1:def 3;
then (th^2)/2<=1/2 by REAL_1:73;
then A8: X[0] by A6,A7,REAL_2:106;
A9: for k st X[k] holds X[k+1]
proof
let k; assume
A10: ((Partial_Sums(th P_cos))*bq).k >= 1/2;
((Partial_Sums(th P_cos))*bq).(k+1)
=(Partial_Sums(th P_cos)).(bq.(k+1)) by SEQM_3:31
.=(Partial_Sums(th P_cos)).(2*(k+1)+1) by Lm11
.=(Partial_Sums(th P_cos)).(2*(k+1)) +(th P_cos).(2*(k+1)+1)
by SERIES_1:def 1
.= (Partial_Sums(th P_cos)).(2*k+2*1) +(th P_cos).(2*(k+1)+1)
by XCMPLX_1:8
.= (Partial_Sums(th P_cos)).(2*k+(1+1))+(th P_cos).(2*(k+1)+1)
.=(Partial_Sums(th P_cos)).(2*k+1+1)+(th P_cos).(2*(k+1)+1)
by XCMPLX_1:1
.=(Partial_Sums(th P_cos)).(2*k+1) + (th P_cos).(2*k+1+1)+
(th P_cos).(2*(k+1)+1) by SERIES_1:def 1
.= (Partial_Sums(th P_cos)).(bq.k)+ (th P_cos).(2*k+1+1)+
(th P_cos).(2*(k+1)+1) by Lm11
.=((Partial_Sums(th P_cos))*bq).k+ (th P_cos).(2*k+1+1)+
(th P_cos).(2*(k+1)+1) by SEQM_3:31;
then A11:
((Partial_Sums(th P_cos))*bq).(k+1)-((Partial_Sums(th P_cos))*bq).k
= ((Partial_Sums(th P_cos))*bq).k+((th P_cos).(2*k+1+1)
+ (th P_cos).(2*(k+1)+1))-((Partial_Sums(th P_cos))*bq).k
by XCMPLX_1:1
.=((Partial_Sums(th P_cos))*bq).k-((Partial_Sums(th P_cos))*bq).k
+((th P_cos).(2*k+1+1)+ (th P_cos).(2*(k+1)+1)) by XCMPLX_1:29
.=0+((th P_cos).(2*k+1+1)+ (th P_cos).(2*(k+1)+1)) by XCMPLX_1:14
.=(th P_cos).(2*k+1+1)+ (th P_cos).(2*(k+1)+1);
A12: (th P_cos).(2*k+1+1)=(th P_cos).(2*k+(1+1)) by XCMPLX_1:1
.=(th P_cos).(2*k+2*1)
.=(th P_cos).(2*(k+1)) by XCMPLX_1:8
.=(-1)|^ (2*(k+1)) * (th)|^ (2*(2*(k+1)))/((2*(2*(k+1)))!) by Def25
.=(1)* (th)|^ (2*(2*(k+1)))/((2*(2*(k+1)))!) by Lm12
.=(th)|^ (2*(2*(k+1)))/((2*(2*(k+1)))!);
(th P_cos).(2*(k+1)+1)
= (-1)|^ (2*(k+1)+1) * (th)|^ (2*(2*(k+1)+1))/((2*(2*(k+1)+1))!)
by Def25
.=((-1) * (th)|^ (2*(2*(k+1)+1)))/((2*(2*(k+1)+1))!) by Lm12;
then A13:(th P_cos).(2*(k+1)+1)
=(-1) * ((th)|^ (2*(2*(k+1)+1))/((2*(2*(k+1)+1))!))
by XCMPLX_1:75
.=-(th)|^ (2*(2*(k+1)+1))/((2*(2*(k+1)+1))!) by XCMPLX_1:180;
2*(k+1) < 2*(k+1)+1 by REAL_1:69;
then A14: 2*(2*(k+1))<2*(2*(k+1)+1) by REAL_1:70;
then A15: (2*(2*(k+1)))! <= (2*(2*(k+1)+1))! by Th42;
A16: (th)|^ (2*(2*(k+1)+1)) <= (th)|^ (2*(2*(k+1))) by A1,A14,Th43;
A17: 0 <= (th)|^ (2*(2*(k+1)+1)) by POWER:3;
A18:(2*(2*(k+1)))!>0 & (2*(2*(k+1)+1))! >0 by Th42;
then A19: 1/((2*(2*(k+1)+1))!)<=1/((2*(2*(k+1)))!) by A15,REAL_2:152;
0<1/((2*(2*(k+1)+1))!) by A18,REAL_2:127;
then A20: (th)|^ (2*(2*(k+1)+1))*(1/((2*(2*(k+1)+1))!))<=
(th)|^ (2*(2*(k+1)))*(1/((2*(2*(k+1)))!)) by A16,A17,A19,REAL_2:197;
A21: (th)|^ (2*(2*(k+1)+1))*(1/((2*(2*(k+1)+1))!))
=((th)|^ (2*(2*(k+1)+1))*1)/((2*(2*(k+1)+1))!) by XCMPLX_1:75
.=(th)|^ (2*(2*(k+1)+1))/((2*(2*(k+1)+1))!);
(th)|^ (2*(2*(k+1)))*(1/((2*(2*(k+1)))!))
=(th)|^ (2*(2*(k+1)))*1/((2*(2*(k+1)))!) by XCMPLX_1:75;
then A22: ((th)|^ (2*(2*(k+1)))*1)/((2*(2*(k+1)))!)-
((th)|^ (2*(2*(k+1)+1))*1)/((2*(2*(k+1)+1))!)>=0 by A20,A21,SQUARE_1:
12;
((Partial_Sums(th P_cos))*bq).(k+1)-((Partial_Sums(th P_cos))*bq).k
= ((th)|^ (2*(2*(k+1)))*1)/((2*(2*(k+1)))!)-
((th)|^ (2*(2*(k+1)+1))*1)/((2*(2*(k+1)+1))!) by A11,A12,A13,XCMPLX_0:
def 8;
then ((Partial_Sums(th P_cos))*bq).(k+1)>=((Partial_Sums(th P_cos))*bq
).k
by A22,REAL_2:105;
hence thesis by A10,AXIOMS:22;
end;
for n holds X[n] from Ind(A8,A9);
hence thesis;
end;
then cos.th >= 1/2 by A4,A5,Th41;
hence thesis by AXIOMS:22;
end;
theorem Th75: [.0,1 .] c= dom (sin/cos) & ].0,1 .[c=dom(sin/cos)
proof
[.0,1 .] c= dom cos \ cos"{0}
proof
A1: [.0,1 .] \ cos"{0} c=dom cos \ cos"{0} by Th27,XBOOLE_1:33;
[.0,1 .] /\ cos"{0}={}
proof
assume [.0,1 .] /\ cos"{0}<>{};
then consider rr such that
A2:rr in [.0,1 .] /\ cos"{0} by XBOOLE_0:def 1;
A3:rr in [.0,1 .] & rr in cos"{0} by A2,XBOOLE_0:def 3;
then A4:cos.(rr) <>0 by Th74;
cos.(rr) in {0} by A3,FUNCT_1:def 13;
hence contradiction by A4,TARSKI:def 1;
end;
then [.0,1 .] misses cos"{0} by XBOOLE_0:def 7;
hence thesis by A1,XBOOLE_1:83;
end;
then [.0,1 .] c= dom sin /\ (dom cos \ cos"{0}) by Th27,XBOOLE_1:19;
then A5:[.0,1 .] c= dom (sin/cos) by RFUNCT_1:def 4;
].0,1 .[c=[.0,1 .] by RCOMP_1:15;
hence thesis by A5,XBOOLE_1:1;
end;
Lm20: dom((sin/cos)|[.0,1 .]) = [.0,1 .] &
(for th st th in [.0,1 .] holds (sin/cos)|[.0,1 .].th=(sin/cos).th)
proof
dom((sin/cos)|[.0,1 .])=dom (sin/cos) /\ [.0,1 .] by RELAT_1:90;
then dom((sin/cos)|[.0,1 .]) = [.0,1 .] by Th75,XBOOLE_1:28;
hence thesis by FUNCT_1:68;
end;
Lm21:
sin/cos is_differentiable_on ].0,1 .[ & for th st th in ].0,1 .[ holds
diff(sin/cos,th)>0
proof
A1: sin is_differentiable_on ].0,1 .[ by Th73,FDIFF_1:34;
A2: cos is_differentiable_on ].0,1 .[ by Th72,FDIFF_1:34;
A3:for th be Real st th in ].0,1 .[ holds cos.th<>0
proof
let th be Real such that
A4: th in ].0,1 .[;
].0,1 .[ c=[.0,1 .] by RCOMP_1:15;
hence cos.th<>0 by A4,Th74;
end;
for th st th in ].0,1 .[ holds diff(sin/cos,th)>0
proof
let th such that
A5: th in ].0,1 .[;
A6: cos is_differentiable_in th by Th68;
A7: sin is_differentiable_in th by Th69;
A8: cos.th<>0 by A3,A5;
then A9: diff(sin/cos,th)=(diff(sin,th)*cos.th-diff(cos,th)*sin.th)/(cos.th)
^2
by A6,A7,FDIFF_2:14
.=(cos.th*cos.th-diff(cos,th)*sin.th)/(cos.th)^2 by Th69
.=(cos.th*cos.th-(-sin.th)*sin.th)/(cos.th)^2 by Th68
.=(cos.th*cos.th--(sin.th)*sin.th)/(cos.th)^2 by XCMPLX_1:175
.=(cos.th*cos.th+(sin.th)*sin.th)/(cos.th)^2 by XCMPLX_1:151
.=((cos.th)^2+(sin.th)*sin.th)/(cos.th)^2 by SQUARE_1:def 3
.=((cos.th)^2+(sin.th)^2)/(cos.th)^2 by SQUARE_1:def 3
.=1/(cos.th)^2 by Th31;
(cos.th)^2>0 by A8,SQUARE_1:74;
hence thesis by A9,REAL_2:127;
end;
hence thesis by A1,A2,A3,FDIFF_2:21;
end;
theorem Th76: sin/cos is_continuous_on [. 0, 1 .]
proof
for th be real number st th in [.0,1 .] holds
(sin/cos)|[.0,1 .] is_continuous_in th
proof
let th be real number such that
A1: th in [.0,1 .];
A2: th is Real by XREAL_0:def 1;
A3:[#] REAL = REAL by SUBSET_1:def 4;
then sin is_differentiable_in th by A2,Th73,FCONT_3:4,FDIFF_1:16;
then A4: sin is_continuous_in th by FDIFF_1:32;
cos is_differentiable_in th by A2,A3,Th72,FCONT_3:4,FDIFF_1:16;
then A5: cos is_continuous_in th by FDIFF_1:32;
cos.(th) <> 0 by A1,Th74;
then A6: sin/cos is_continuous_in th by A4,A5,FCONT_1:11;
th in dom ((sin/cos)|[.0,1 .]) &
for rseq st rng rseq c= dom ((sin/cos)|[.0,1 .]) &
rseq is convergent & lim rseq = th
holds ((sin/cos)|[.0,1 .])*rseq is convergent
& ((sin/cos)|[.0,1 .]).th = lim (((sin/cos)|[.0,1 .])*rseq)
proof
now
let rseq; assume
A7: rng rseq c= dom ((sin/cos)|[.0,1 .]) &
rseq is convergent & lim rseq = th;
then A8:rng rseq c= dom (sin/cos) by Lm20,Th75,XBOOLE_1:1;
then A9: (sin/cos)*rseq is convergent & (sin/cos).th
= lim ((sin/cos)*rseq) by A6,A7,FCONT_1:def 1;
((sin/cos)|[.0,1 .])*rseq =(sin/cos)*rseq
proof
now let k1 be Nat;
dom (rseq) = NAT by SEQ_1:3;
then rseq.k1 in rng rseq by FUNCT_1:def 5;
then A10: ((sin/cos)|[.0,1 .]).(rseq.k1)=(sin/cos).(rseq.k1) by A7,
Lm20;
((sin/cos)|[.0,1 .]).(rseq.k1)=(((sin/cos)|[.0,1 .])*rseq).k1
by A7,RFUNCT_2:21;
hence (((sin/cos)|[.0,1 .])*rseq).k1=((sin/cos)*rseq).k1
by A8,A10,RFUNCT_2:21;
end;
hence thesis by FUNCT_2:113;
end;
hence ((sin/cos)|[.0,1 .])*rseq is convergent
& ((sin/cos)|[.0,1 .]).th = lim (((sin/cos)|[.0,1 .])*rseq)
by A1,A9,Lm20;
end;
hence thesis by A1,Lm20;
end;
hence thesis by FCONT_1:def 1;
end;
hence sin/cos is_continuous_on [. 0, 1 .] by Th75,FCONT_1:def 2;
end;
theorem Th77: for th1,th2 st th1 in ].0,1 .[ & th2 in ].0,1 .[ &
(sin/cos).th1=(sin/cos).th2 holds th1=th2
proof
let th1,th2; assume
A1: th1 in ].0,1 .[ & th2 in ].0,1 .[ & (sin/cos).(th1)=(sin/cos).(th2);
then A2: 0<th1 & th1<1 & 0<th2 & th2<1 by JORDAN6:45;
assume A3: th1<>th2;
ex th st th in ].0,1 .[ & diff((sin/cos),(th))=0
proof
now per cases by A3,REAL_1:def 5;
suppose A4: th1<th2;
A5: ].th1,th2.[ is open Subset of REAL & ].th1,th2.[c=].0,1 .[&
[.th1,th2.]c=[.0,1 .]
proof
A6: for th be Real st th in ].th1,th2.[ holds th in ].0,1 .[
proof
let th be Real; assume
th in ].th1,th2.[;
then A7: th1<th& th< th2 by JORDAN6:45;
then A8: 0< th by A2,AXIOMS:22;
th <1 by A2,A7,AXIOMS:22;
hence thesis by A8,JORDAN6:45;
end;
for th be Real st th in [.th1,th2.] holds th in [.0,1 .]
proof
let th be Real; assume
th in [.th1,th2.];
then A9: th1<=th& th<= th2 by TOPREAL5:1;
then A10: 0<= th by A2,AXIOMS:22;
th <=1 by A2,A9,AXIOMS:22;
hence thesis by A10,TOPREAL5:1;
end;
hence thesis by A6,SUBSET_1:7;
end;
then A11: (sin/cos) is_differentiable_on ].th1,th2.[ by Lm21,FDIFF_1:34;
(sin/cos) is_continuous_on [.th1,th2.] by A5,Th76,FCONT_1:17;
then consider r such that
A12: r in ].th1,th2.[ & diff((sin/cos),r)=0
by A1,A4,A11,ROLLE:1;
take th=r;
thus th in ].0,1 .[ & diff((sin/cos),(th))=0 by A5,A12;
suppose A13: th2<th1;
A14: ].th2,th1 .[ is open Subset of REAL & ].th2,th1 .[c=].0,1 .[&
[.th2,th1 .]c=[.0,1 .]
proof
A15: for th be Real st th in ].th2,th1 .[ holds th in ].0,1 .[
proof
let th be Real; assume
th in ].th2,th1 .[;
then A16: th2<th& th< th1 by JORDAN6:45;
then A17: 0< th by A2,AXIOMS:22;
th <1 by A2,A16,AXIOMS:22;
hence thesis by A17,JORDAN6:45;
end;
for th be Real st th in [.th2,th1 .] holds th in [.0,1 .]
proof
let th be Real; assume
th in [.th2,th1 .];
then A18: th2<=th& th<= th1 by TOPREAL5:1;
then A19: 0<= th by A2,AXIOMS:22;
th <=1 by A2,A18,AXIOMS:22;
hence thesis by A19,TOPREAL5:1;
end;
hence thesis by A15,SUBSET_1:7;
end;
then A20: (sin/cos) is_differentiable_on ].th2,th1 .[ by Lm21,
FDIFF_1:34;
(sin/cos) is_continuous_on [.th2,th1 .] by A14,Th76,FCONT_1:17;
then consider r such that
A21: r in ].th2,th1 .[ & diff((sin/cos),r)=0 by A1,A13,A20,ROLLE:1;
take th=r;
thus th in ].0,1 .[ & diff((sin/cos),(th))=0 by A14,A21;
end;
hence thesis;
end;
hence thesis by Lm21;
end;
Lm22: (sin/cos).(0) =0 & (sin/cos).(1) >1
proof
0 in [.0,1 .] by TOPREAL5:1;
then A1: (sin/cos).(0)=(sin.0)* (cos.0)" by Th75,RFUNCT_1:def 4
.=0 by Th33;
1 in [.0,1 .] by TOPREAL5:1;
then (sin/cos).(1)=(sin.1)* (cos.1)" by Th75,RFUNCT_1:def 4
.=(sin.1)/ (cos.1) by XCMPLX_0:def 9;
hence thesis by A1,Th47,REAL_2:142;
end;
begin :: Existence of Circle Ratio
definition
func PI -> real number means :Def30:
(sin/cos).(it/4) = 1 & it in ]. 0, 4 .[;
existence
proof
A1: 1 in [.(sin/cos).0,(sin/cos).1 .]
proof
[.(sin/cos).0,(sin/cos).1 .] = {r : (sin/cos).0<=r & r<=
(sin/cos).1 }
by RCOMP_1:def 1;
hence 1 in [.(sin/cos).0,(sin/cos).1 .] by Lm22;
end;
(sin/cos).1 > (sin/cos).0 by Lm22,AXIOMS:22;
then [.(sin/cos).1,(sin/cos).0 .]= {} by RCOMP_1:13;
then 1 in [.(sin/cos).0,(sin/cos).1 .] \/ [.(sin/cos).1,(sin/cos).0 .]
by A1;
then consider th be Real such that
A2: th in [.0, 1 .] & (sin/cos).(th)=1 by Th76,FCONT_2:16;
0<=th & th <= 1 by A2,TOPREAL5:1;
then A3: 0 <th & th <1 by A2,Lm22,REAL_1:def 5;
take th1 =th*4;
thus (sin/cos).(th1/4)=1 by A2,XCMPLX_1:90;
0*4<th*4 & th*4<1*4 by A3,REAL_1:70;
hence thesis by JORDAN6:45;
end;
uniqueness
proof let th1,th2 be real number such that
A4: (sin/cos).(th1/4) = 1 & th1 in ]. 0, 4 .[ and
A5: (sin/cos).(th2/4) = 1 & th2 in ]. 0, 4 .[;
th1/4 in ].0,1 .[ & th2/4 in ]. 0, 1 .[
proof
0<th1 & th1 <4 by A4,JORDAN6:45;
then 0/4<th1/4 & th1/4 <4/4 by REAL_1:73;
hence th1/4 in ]. 0, 1 .[ by JORDAN6:45;
0<th2 & th2 < 4 by A5,JORDAN6:45;
then 0/4<th2/4 & th2/4 <4/4 by REAL_1:73;
hence th2/4 in ]. 0, 1 .[ by JORDAN6:45;
end;
then th1/4=th2/4 by A4,A5,Th77;
hence th1=th2 by XCMPLX_1:53;
end;
end;
definition
redefine func PI -> Real;
coherence by XREAL_0:def 1;
end;
theorem Th78:
sin.(PI/4) = cos.(PI/4)
proof
PI in ].0, 4.[ by Def30;
then 0< PI & PI < 4 by JORDAN6:45;
then 0/4 <PI/4 & PI/4 < 4/4 by REAL_1:73;
then A1: PI/4 in ].0,1 .[ by JORDAN6:45;
(sin/cos).(PI/4) =1 by Def30;
then sin.(PI/4) * (cos.(PI/4))"=1 by A1,Th75,RFUNCT_1:def 4;
hence sin.(PI/4) = cos.(PI/4) by XCMPLX_1:210;
end;
begin ::Formulas of sin and cos
theorem Th79:
sin.(th1+th2)=(sin.(th1)) *(cos.(th2))+(cos.(th1)) * (sin.(th2)) &
cos.(th1+th2)=(cos.(th1)) *(cos.(th2))-(sin.(th1)) * (sin.(th2))
proof
A1: Sum([*0,th1*] ExpSeq ) * Sum([*0,th2*] ExpSeq )
=Sum(([*0,th1*]+[*0,th2*]) ExpSeq ) by Lm4
.=Sum([*0+0, th1+th2*] ExpSeq ) by Lm3
.=[*cos.(th1+th2),sin.(th1+th2)*] by Lm6;
Sum(([*0,th1*] ExpSeq) ) * Sum(([*0,th2*] ExpSeq) )
=[*cos.(th1),sin.(th1)*]* Sum(([*0,th2*] ExpSeq) ) by Lm6
.=[*cos.(th1),sin.(th1)*]*[*cos.(th2),sin.(th2)*] by Lm6
.=[*(cos.(th1)) *( cos.(th2))-(sin.(th1)) * (sin.(th2)),
(sin.(th1)) * (cos.(th2))+(cos.(th1)) * (sin.(th2))*] by Lm3;
hence thesis by A1,ARYTM_0:12;
end;
theorem
sin(th1+th2)=(sin(th1)) *(cos(th2))+(cos(th1)) * (sin(th2)) &
cos(th1+th2)=(cos(th1)) *(cos(th2))-(sin(th1)) * (sin(th2))
proof
thus sin(th1+th2)=sin.(th1+th2) by Def21
.=(sin.(th1)) *(cos.(th2))+(cos.(th1)) * (sin.(th2)) by Th79
.=(sin(th1)) *(cos.(th2))+(cos.(th1)) * (sin.(th2)) by Def21
.=(sin(th1)) *(cos(th2))+(cos.(th1)) * (sin.(th2)) by Def23
.=(sin(th1)) *(cos(th2))+(cos(th1)) * (sin.(th2)) by Def23
.=(sin(th1)) *(cos(th2))+(cos(th1)) * (sin(th2)) by Def21;
thus cos(th1+th2)=cos.(th1+th2) by Def23
.=(cos.(th1)) *(cos.(th2))-(sin.(th1)) * (sin.(th2)) by Th79
.=(cos(th1)) *(cos.(th2))-(sin.(th1)) * (sin.(th2)) by Def23
.=(cos(th1)) *(cos(th2))-(sin.(th1)) * (sin.(th2)) by Def23
.=(cos(th1)) *(cos(th2))-(sin(th1)) * (sin.(th2)) by Def21
.=(cos(th1)) *(cos(th2))-(sin(th1)) * (sin(th2)) by Def21;
end;
theorem Th81:
cos.(PI/2) = 0 & sin.(PI/2) = 1 &
cos.(PI) = -1 & sin.(PI) = 0 &
cos.(PI+PI/2) = 0 & sin.(PI+PI/2) = -1 &
cos.(2 * PI) = 1 & sin.(2 * PI) =0
proof
thus A1: cos.(PI/2)=cos.(PI/4+PI/4) by XCMPLX_1:72
.=(cos.(PI/4)) * (cos.(PI/4))
-(cos.(PI/4)) * (cos.(PI/4)) by Th78,Th79
.=0 by XCMPLX_1:14;
thus A2: sin.(PI/2)=sin.(PI/4+PI/4) by XCMPLX_1:72
.= (cos.(PI/4)) *( cos.(PI/4))
+(sin.(PI/4)) * (sin.(PI/4)) by Th78,Th79
.=1 by Th31;
thus A3: cos.(PI)=cos.(PI/2+PI/2) by XCMPLX_1:66
.=0 * 0-sin.(PI/2) * sin.(PI/2) by A1,Th79
.=-1 by A2;
thus A4: sin.(PI)=sin.(PI/2+PI/2) by XCMPLX_1:66
.=(sin.(PI/2)) *( cos.(PI/2))
+(cos.(PI/2) )*( sin.(PI/2)) by Th79
.=0 by A1;
thus cos.(PI+PI/2)
=(cos.(PI)) *( cos.(PI/2))
-(sin.(PI)) * (sin.(PI/2)) by Th79
.=0 by A1,A4;
thus sin.(PI+PI/2) =(sin.(PI) )*( cos.(PI/2))
+(cos.(PI)) *( sin.(PI/2) ) by Th79
.=-1 by A1,A2,A3;
thus cos.(2 * PI)=cos.(PI+PI) by XCMPLX_1:11
.=(-1 ) * (-1) -sin.(PI) * sin.(PI) by A3,Th79
.=1 by A4;
thus sin.(2 * PI)=sin.(PI+PI) by XCMPLX_1:11
.=(sin.(PI)) * (cos.(PI))+(cos.(PI)) * (sin.(PI)) by Th79
.=0 by A4;
end;
theorem
cos(PI/2) = 0 & sin(PI/2) = 1 &
cos(PI) = -1 & sin(PI) = 0 &
cos(PI+PI/2) = 0 & sin(PI+PI/2) = -1 &
cos(2 * PI) = 1 & sin(2 * PI) =0 by Def21,Def23,Th81;
theorem Th83:
sin.(th+2 * PI) = sin.th &
cos.(th+2 * PI) = cos.th &
sin.(PI/2-th) = cos.th &
cos.(PI/2-th) = sin.th &
sin.(PI/2+th) = cos.th &
cos.(PI/2+th) = -sin.th &
sin.(PI+th) = -sin.th &
cos.(PI+th) = -cos.th
proof
thus sin.(th+2 * PI)=sin.(th) * 1 +cos.(th) * 0 by Th79,Th81
.=sin.th;
thus cos.(th+2 * PI)=cos.(th) * 1 - sin.(th) * 0 by Th79,Th81
.=cos.th;
thus sin.(PI/2-th) =sin.(PI/2+(-th)) by XCMPLX_0:def 8
.=(sin.(PI/2) )* (cos.(-th))
+ (cos.(PI/2)) *( sin.(-th)) by Th79
.=cos.(th) by Th33,Th81;
thus cos.(PI/2-th) =cos.(PI/2+(-th)) by XCMPLX_0:def 8
.=(cos.(PI/2)) * (cos.(-th))
- ( sin.(PI/2)) *( sin.(-th)) by Th79
.=0 - 1 * (-sin.(th)) by Th33,Th81
.=0 + - 1 * (-sin.(th)) by XCMPLX_0:def 8
.=sin.(th);
thus sin.(PI/2+th) =1 * cos.(th) + 0 * (sin.(th)) by Th79,Th81
.=cos.(th);
thus cos.(PI/2+th) =(cos.(PI/2)) *( cos.(th))
-( sin.(PI/2) )*( sin.(th)) by Th79
.=0 + - 1 * sin.(th) by Th81,XCMPLX_0:def 8
.=-sin.(th);
thus sin.(PI+th) =(sin.(PI)) * (cos.(th))
+( cos.(PI) )*( sin.(th)) by Th79
.=0 + -sin.(th) * 1 by Th81,XCMPLX_1:175
.=-sin.(th);
thus cos.(PI+th) =(-1) * cos.(th) - 0 * sin.(th) by Th79,Th81
.=-cos.(th) * 1 - 0 by XCMPLX_1:175
.=-cos.(th);
end;
theorem
sin(th+2 * PI) = sin(th) &
cos(th+2 * PI) = cos(th) &
sin(PI/2-th) = cos(th) &
cos(PI/2-th) = sin(th) &
sin(PI/2+th) = cos(th) &
cos(PI/2+th) = -sin(th) &
sin(PI+th) = -sin(th) &
cos(PI+th) = -cos(th)
proof
thus sin(th+2 * PI) =sin.(th+2 * PI) by Def21
.=sin.th by Th83
.=sin(th) by Def21;
thus cos(th+2 * PI) = cos.(th+2 * PI) by Def23
.=cos.th by Th83
.=cos(th) by Def23;
thus sin(PI/2-th) = sin.(PI/2-th) by Def21
.=cos.(th) by Th83
.=cos(th) by Def23;
thus cos(PI/2-th) =cos.(PI/2-th) by Def23
.=sin.(th) by Th83
.= sin(th) by Def21;
thus sin(PI/2+th)=sin.(PI/2+th) by Def21
.= cos.th by Th83
.= cos(th) by Def23;
thus cos(PI/2+th)=cos.(PI/2+th) by Def23
.= -sin.th by Th83
.= -sin(th) by Def21;
thus sin(PI+th)=sin.(PI+th) by Def21
.= -sin.th by Th83
.= -sin(th) by Def21;
thus cos(PI+th)=cos.(PI+th) by Def23
.= -cos.th by Th83
.= -cos(th) by Def23;
end;
Lm23: for th st th in [.0,1 .] holds sin.th>=0
proof
let th; assume A1: th in [.0,1 .];
then A2: 0<=th & th<=1 by TOPREAL5:1;
sin.th>= sin.0
proof
now per cases by A1,TOPREAL5:1;
suppose th=0;
hence sin.th>= sin.0;
suppose A3: 0<th;
A4: sin is_differentiable_on ].0,th.[ by Th73,FDIFF_1:34;
sin is_continuous_on REAL by Th73,FDIFF_1:33;
then sin is_continuous_on [.0,th.] by FCONT_1:17;
then consider r be Real such that
A5: r in ].0,th.[ & diff(sin,r)=(sin.th-sin.0)/(th-0) by A3,A4,ROLLE:3;
A6: diff(sin,r)=cos.r by Th73;
0<r & r < th by A5,JORDAN6:45;
then 0<r & r <1 by A2,AXIOMS:22;
then r in [.0,1 .] by TOPREAL5:1;
then A7: cos.r >0 by Th74;
sin.th-sin.0= cos.r* th by A3,A5,A6,XCMPLX_1:88;
then sin.th-sin.0 >0 by A3,A7,REAL_2:122;
hence sin.th>=sin.0 by REAL_2:106;
end;
hence thesis;
end;
hence thesis by Th33;
end;
theorem Th85:
for th st th in ].0,PI/2.[ holds cos.th > 0
proof
given th1 such that
A1:th1 in ].0,PI/2.[ & cos.th1 <= 0;
reconsider th1 as Real;
cos is_continuous_on REAL by Th72,FDIFF_1:33;
then A2:cos is_continuous_on [.0,th1 .] by FCONT_1:17;
A3:0 < th1 by A1,JORDAN6:45;
cos.th1 <= cos.0 by A1,Th33,AXIOMS:22;
then A4:[.cos.0,cos.th1 .] \/ [.cos.th1,cos.0 .] = [.cos.th1,cos.0 .]
by RCOMP_1:18;
0 in [.cos.th1,cos.0 .] by A1,Th33,TOPREAL5:1;
then ex th2 be Real st th2 in [.0,th1 .] & cos.th2 = 0 by A2,A3,A4,FCONT_2:16;
then consider th2 be Real such that
A5:th2 in [.0,th1 .] & 0 < th1 & cos.th2 = 0 by A3;
A6: 0 <= th2 & th2 <= th1 & th1 < PI/2 by A1,A5,JORDAN6:45,TOPREAL5:1;
then A7: 0<th2 & th2<PI/2 by A5,Th33,AXIOMS:21,22;
A8:PI/2/2 = PI/(2*2) by XCMPLX_1:79
.= PI/4;
A9: 0/2<th2/2 & th2/2 < PI/2/2 by A7,REAL_1:73;
PI in ].0, 4.[ by Def30;
then 0< PI & PI < 4 by JORDAN6:45;
then PI/4 < 4/4 by REAL_1:73;
then A10: 0 < th2/2 & th2/2 < 1 by A8,A9,AXIOMS:22;
0 = cos.(th2/2*2) by A5,XCMPLX_1:88
.= cos.(th2/2 + th2/2) by XCMPLX_1:11
.= (cos.(th2/2)) * (cos.(th2/2))
-(sin.(th2/2)) * (sin.(th2/2)) by Th79
.= (cos.(th2/2))^2 - (sin.(th2/2)) * (sin.(th2/2)) by SQUARE_1:def 3
.= (cos.(th2/2))^2 - (sin.(th2/2))^2 by SQUARE_1:def 3
.= ((cos.(th2/2)) - (sin.(th2/2))) *
((cos.(th2/2)) + (sin.(th2/2))) by SQUARE_1:67;
then cos.(th2/2) - sin.(th2/2) = 0 or
cos.(th2/2) + sin.(th2/2) = 0 by XCMPLX_1:6;
then A11: cos.(th2/2) = sin.(th2/2) or
cos.(th2/2) = -sin.(th2/2) by XCMPLX_0:def 6,XCMPLX_1:15;
A12: th2/2 in ].0,1 .[ by A10,JORDAN6:45;
A13: ].0,1 .[ c= [.0,1 .] by RCOMP_1:15;
then A14: cos.(th2/2) > 0 by A12,Th74;
A15: sin.(th2/2) >= 0 by A12,A13,Lm23;
(2*th2) in ].0,4.[ & (sin/cos).((2*th2)/4) = 1
proof
A16: 4*0 < 4*(th2/2) & 4*(th2/2) < 4*1 by A10,Lm1;
A17: 4*(th2/2) = 2*th2 & (2*th2)/4 = th2/2
proof
thus 4*(th2/2) = (th2*4)/2 by XCMPLX_1:75
.= th2*(4/2) by XCMPLX_1:75
.= 2*th2;
thus (2*th2)/4 = th2/(4/2) by XCMPLX_1:78
.= th2/2;
end;
hence (2*th2) in ].0,4.[ by A16,JORDAN6:45;
(sin.(th2/2)) * (cos.(th2/2))"=1 by A11,A14,A15,REAL_1:26,50,XCMPLX_0:def 7
;
hence (sin/cos).((2*th2)/4) =1 by A12,A17,Th75,RFUNCT_1:def 4;
end;
then A18: 2*th2 =PI by Def30;
th2 = th2*(2/2)
.= PI/2 by A18,XCMPLX_1:75;
hence contradiction by A6;
end;
theorem
for th st th in ].0,PI/2.[ holds cos(th) > 0
proof
let th such that
A1: th in ].0,PI/2.[;
cos(th)=cos.th by Def23;
hence thesis by A1,Th85;
end;