:: Trigonometric Functions and Existence of Circle Ratio
:: by Yuguang Yang and Yasunari Shidama
::
:: Received October 22, 1998
:: Copyright (c) 1998-2026 Association of Mizar Users
:: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.
environ
vocabularies NUMBERS, REAL_1, XREAL_0, SUBSET_1, COMSEQ_1, SEQ_1, FDIFF_1,
XXREAL_0, CARD_1, COMPLEX1, FUNCT_1, RELAT_1, XCMPLX_0, ARYTM_3, NAT_1,
REALSET1, NEWTON, ARYTM_1, VALUED_1, SERIES_1, PREPOWER, CARD_3, SEQ_2,
ORDINAL2, SQUARE_1, VALUED_0, XXREAL_2, FUNCT_2, TARSKI, RCOMP_1,
XXREAL_1, PARTFUN1, XBOOLE_0, FCONT_1, SIN_COS, FUNCT_7, ORDINAL1;
notations TARSKI, XBOOLE_0, SUBSET_1, ORDINAL1, NUMBERS, XXREAL_0, XREAL_0,
ABIAN, XCMPLX_0, COMPLEX1, REAL_1, RELAT_1, FUNCT_1, RELSET_1, FCONT_1,
FUNCT_2, VALUED_1, SEQ_1, SEQ_2, FDIFF_1, SERIES_1, NAT_1, NEWTON,
SQUARE_1, PARTFUN1, VALUED_0, RCOMP_1, NAT_D, RFUNCT_1, COMSEQ_1,
COMSEQ_2, COMSEQ_3, PREPOWER;
constructors PARTFUN1, FUNCT_4, ARYTM_0, REAL_1, SQUARE_1, NAT_1, RCOMP_1,
RFUNCT_1, COMSEQ_2, RFUNCT_2, FCONT_1, FDIFF_1, PREPOWER, COMSEQ_3,
NAT_D, RECDEF_1, SEQM_3, SERIES_1, SEQ_2, VALUED_1, RELSET_1, ABIAN,
BINOP_2, RVSUM_1, XXREAL_2, NUMBERS;
registrations XBOOLE_0, ORDINAL1, RELSET_1, FUNCT_2, NUMBERS, XCMPLX_0,
XXREAL_0, XREAL_0, SQUARE_1, NAT_1, MEMBERED, RCOMP_1, COMSEQ_2, FDIFF_1,
NEWTON, COMSEQ_3, VALUED_0, VALUED_1, SEQ_4, FCONT_3, ABIAN, SEQ_2,
INT_1;
requirements REAL, NUMERALS, SUBSET, BOOLE, ARITHM;
definitions FUNCT_2;
equalities COMSEQ_3, SQUARE_1, SUBSET_1, VALUED_1, XCMPLX_0, COMPLEX1;
expansions COMSEQ_3, VALUED_1, FUNCT_2;
theorems NAT_1, ABSVALUE, INT_1, SEQ_1, SEQ_2, SERIES_1, SEQM_3, SEQ_4,
PREPOWER, COMPLEX1, COMSEQ_1, COMSEQ_2, SQUARE_1, COMSEQ_3, FCONT_2,
RCOMP_1, FUNCT_1, FDIFF_1, FDIFF_2, FCONT_1, TARSKI, FUNCT_2, RFUNCT_1,
SUBSET_1, POWER, ROLLE, NEWTON, RELAT_1, XREAL_0, XBOOLE_0, XBOOLE_1,
XCMPLX_0, XCMPLX_1, XREAL_1, XXREAL_0, ORDINAL1, VALUED_1, XXREAL_1,
VALUED_0, NUMBERS;
schemes NAT_1, SEQ_1, COMSEQ_1, CLASSES1, FUNCT_2;
begin
reserve q,th,r for Real,
a,b,p for Real,
w,z for 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 0-convergent non-zero Real_Sequence;
:: Some definitions and properties of complex sequence
definition
let m,k be natural Number;
func CHK(m,k) -> Element of COMPLEX equals
:Def1:
1 if m <= k otherwise 0;
correctness
proof
0c = 0;
hence thesis by COMPLEX1:def 4;
end;
end;
registration
let m,k be natural Number;
cluster CHK(m,k) -> real;
coherence by Def1;
end;
scheme ExComplexCASE{F(Nat,Nat)->Complex}:
for k holds ex seq st for n holds (n <= k implies seq.n=F(k,n)) &
(n > k implies seq.n=0)
proof
let k;
defpred P[object,object] means
ex n st (n=$1 & (n <= k implies $2=F(k,n)) &
(n > k implies $2=0c) );
A1: now
let x be object;
assume x in NAT;
then consider n such that
A2: n=x;
A3: now
assume n <= k;
hence CHK(n,k) * F (k,n) =1 * F(k,n) by Def1
.=F(k,n);
end;
A4: now
assume n > k;
hence CHK(n,k) * F (k,n) =0 * F(k,n) by Def1
.=0;
end;
reconsider y=CHK(n,k) * F (k,n) as object;
take y;
thus P[x,y] by A2,A3,A4;
end;
consider f be Function such that
A5: dom f = NAT and
A6: for x be object st x in NAT holds P[x,f.x] from CLASSES1:sch 1(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 A6;
hence f.x is Element of COMPLEX by XCMPLX_0:def 2;
end;
then reconsider f as Complex_Sequence by A5,COMSEQ_1:1;
take seq=f;
let n;
n in NAT by ORDINAL1:def 12;
then P[n,f.n] by A6;
then ex l be Nat st l=n &
(l <= k implies seq.n=F(k,l)) & (l > k implies seq.n=0c);
hence thesis;
end;
scheme ExRealCASE{F(Nat,Nat)->Real}: 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[object,object] means
ex n st (n=$1 & (n <= k implies $2=F(k,n )) &
(n > k implies $2=0) );
A1: now
let x be object;
assume x in NAT;
then consider n such that
A2: n=x;
A3: now
assume n <= k;
hence CHK(n,k) * F (k,n) =1 * F(k,n) by Def1
.=F(k,n);
end;
A4: now
assume n > k;
hence CHK(n,k) * F (k,n) =0 * F(k,n) by Def1
.=0;
end;
reconsider y=CHK(n,k) * F (k,n) as object;
take y;
thus P[x,y] by A2,A3,A4;
end;
consider f be Function such that
A5: dom f = NAT and
A6: for x be object st x in NAT holds P[x,f.x] from CLASSES1:sch 1(A1);
now
let x be object;
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 A6;
hence f.x is real;
end;
then reconsider f as Real_Sequence by A5,SEQ_1:1;
take rseq=f;
let n;
n in NAT by ORDINAL1:def 12;
then
ex l be Nat st l=n &
(l <= k implies rseq.n=F(k,l)) & (l > k implies rseq.n=0) by A6;
hence thesis;
end;
1 in NAT;
then reconsider jj=1 as Element of REAL by NUMBERS:19;
definition
func Prod_real_n -> Real_Sequence means
:Def2:
it.0 = 1 & for n holds it.(n+1) = it.n * (n+1);
existence
proof
deffunc U(Nat,Real) = In($2 * ($1+1),REAL);
consider f being sequence of REAL such that
A1: f.0 = jj and
A2: for n being Nat holds f.(n+1) = U(n,f.n) from NAT_1:sch 12;
take f;
thus f.0 = 1 by A1;
let n;
thus f.(n+1) = U(n,f.n) by A2
.= f.n * (n+1);
end;
uniqueness
proof
let rseq1,rseq2;
assume that
A3: rseq1.0=1 and
A4: for n holds rseq1.(n+1)=rseq1.n * (n+1) and
A5: rseq2.0=1 and
A6: for n holds rseq2.(n+1)=rseq2.n * (n+1);
defpred X[Nat] means rseq1.$1 = rseq2.$1;
A7: X[0] by A3,A5;
A8: 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 A4
.= rseq2.(k+1) by A6;
end;
for n being Nat holds X[n] from NAT_1:sch 2(A7,A8);
hence rseq1 = rseq2;
end;
end;
definition
let n be Nat;
redefine func n! equals :: redefines ! (NEWTON, definition)
Prod_real_n.n;
compatibility
proof
defpred X[Nat] means Prod_real_n.$1 = $1!;
A1: X[0] by Def2,NEWTON:12;
A2: now
let l be Nat;
assume
A3: X[l];
Prod_real_n.(l+1) = Prod_real_n.l * (l+1) by Def2
.= (l+1)! by A3,NEWTON:15;
hence X[l+1];
end;
for k be Nat holds X[k] from NAT_1:sch 2(A1,A2);
hence thesis;
end;
end;
definition
let z be Complex;
deffunc U(Nat) = z |^ $1 /($1!);
func z ExpSeq -> Complex_Sequence means
:Def4:
for n holds it.n = z |^ n / (n!);
existence
proof
thus ex s being Complex_Sequence st
for n holds s.n = U(n) from COMSEQ_1:sch 1;
end;
uniqueness
proof let s1,s2 be Complex_Sequence such that
A1: for x being Nat holds s1.x = U(x) and
A2: for x being Nat holds s2.x = U(x);
let x be Element of NAT;
thus s1.x = U(x) by A1 .= s2.x by A2;
end;
end;
definition
let a be Real;
deffunc U(Nat) = a |^ $1 /($1!);
func a rExpSeq -> Real_Sequence means
:Def5:
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 SEQ_1:sch 1;
end;
uniqueness
proof let s1,s2 be Real_Sequence such that
A1: for x being Nat holds s1.x = U(x) and
A2: for x being Nat holds s2.x = U(x);
let x be Element of NAT;
thus s1.x = U(x) by A1 .= s2.x by A2;
end;
end;
theorem Th1:
0! = 1 & n! <> 0 & (n+1)! = n! * (n+1) by Def2;
theorem Th2:
(0 < k implies ((k-'1)! ) * k = k!) &
(k <= m implies ((m-'k)!) * (m+1-k) = (m+1-'k)!)
proof
A1: now
let k;
assume 0 < k;
then 0+1 <= k by INT_1:7;
then k-'1+1=k-1+1 by XREAL_1:233
.=k;
hence k! =(k-'1)! * k by Th1;
end;
now
let m,k such that
A2: k <= m;
m <= m+1 by XREAL_1:29;
then m+1-'k=m+1-k by A2,XREAL_1:233,XXREAL_0:2
.=m-k+1
.=m-'k+1 by A2,XREAL_1:233;
hence (m+1-'k)!=((m-'k)! ) * (m-'k+1+0*<i>) by Th1
.=((m-'k)! ) * (m-k+1+0*<i>) by A2,XREAL_1:233
.=((m-'k)! ) * (m+1-k);
end;
hence thesis by A1;
end;
definition
let n be Nat;
func Coef(n) -> Complex_Sequence means
:Def6:
for k be Nat holds
(k <= n implies it.k = n! /( (k! ) * ((n-'k)! ))) &
(k > n implies it.k = 0);
existence
proof
deffunc U(Nat,Nat) = $1! /( ($2! ) * (($1-'$2)!));
for n holds ex seq st for k holds (k <= n implies seq.k = U(n,k)) &
(k > n implies seq.k=0 ) from ExComplexCASE;
hence thesis;
end;
uniqueness
proof
let seq1,seq2;
assume that
A1: for k holds (k <= n implies seq1.k = n! /( (k! ) * ((n-'k)!))) &
(k > n implies seq1.k=0) and
A2: for k holds (k <= n implies seq2.k = n! /( (k! ) * ((n-'k)!))) &
(k > n implies seq2.k=0);
now
let k be Element of NAT;
per cases;
suppose
A3: k <= n;
hence seq1.k = n! /( (k! ) * ((n-'k)!)) by A1
.= seq2.k by A2,A3;
end;
suppose
A4: k > n;
hence seq1.k = 0c by A1
.= seq2.k by A2,A4;
end;
end;
hence seq1=seq2;
end;
end;
definition
let n be Nat;
func Coef_e(n) -> Complex_Sequence means
:Def7:
for k be Nat holds
(k <= n implies it.k = 1r/((k! ) * ((n-'k)! ))) & (k > n implies it.k=0);
existence
proof
deffunc U(Nat,Nat) = 1r/(($2! ) * (($1-'$2)! ));
for n holds ex seq st for k holds (k <= n implies seq.k = U(n,k)) &
(k > n implies seq.k=0) from ExComplexCASE;
hence thesis;
end;
uniqueness
proof
let seq1,seq2;
assume that
A1: for k holds (k <= n implies seq1.k = 1r/((k! ) * ((n-'k)! ))) &
(k > n implies seq1.k=0) and
A2: for k holds (k <= n implies seq2.k = 1r/((k! ) * ((n-'k)! ))) &
(k > n implies seq2.k=0);
now
let k be Element of NAT;
per cases;
suppose
A3: k <= n;
hence seq1.k =1r/((k! ) * ((n-'k)! )) by A1
.= seq2.k by A2,A3;
end;
suppose
A4: k > n;
hence seq1.k = 0c by A1
.= seq2.k by A2,A4;
end;
end;
hence seq1=seq2;
end;
end;
definition
let seq;
func Shift seq -> Complex_Sequence means
:Def8:
it.0=0 & for k be Nat holds it.(k+1) = seq.k;
existence
proof
deffunc U(Nat,Element of COMPLEX) = seq.$1;
consider f being sequence of COMPLEX such that
A1: f.0 = 0c & for n being Nat holds f.(n+1)=U(n,f.n) from NAT_1:sch 12;
take f;
thus thesis by A1;
end;
uniqueness
proof
let seq1,seq2;
assume that
A2: seq1.0=0 and
A3: for n holds seq1.(n+1)=seq.n and
A4: seq2.0=0 and
A5: for n holds seq2.(n+1)=seq.n;
defpred X[Nat] means seq1.$1 = seq2.$1;
A6: X[0] by A2,A4;
A7: 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 A3
.= seq2.(k+1) by A5;
end;
for n being Nat holds X[n] from NAT_1:sch 2(A6,A7);
hence seq1 = seq2;
end;
end;
definition
let n;
let z,w be Complex;
func Expan(n,z,w) -> Complex_Sequence means
:Def9:
for k be Nat holds ( k <= n implies
it.k=((Coef(n)).k) * (z |^ k) * (w |^ (n-'k)) ) & (n < k implies it.k=0);
existence
proof
deffunc U(Nat,Nat)
= ((Coef($1)).$2) * (z |^ $2) * (w |^ ($1-'$2));
for n holds ex seq st for k holds (k <= n implies seq.k = U(n,k)) &
(k > n implies seq.k=0) from ExComplexCASE;
hence thesis;
end;
uniqueness
proof
let seq1,seq2;
assume that
A1: for k holds
(k <= n implies seq1.k =((Coef(n)).k) * (z |^ k) * (w |^ (n-'k)))&
(k > n implies seq1.k=0) and
A2: for k holds
(k <= n implies seq2.k = ((Coef(n)).k) * (z |^ k) * (w |^ (n-'k)) )&
(k > n implies seq2.k=0);
now
let k be Element of NAT;
per cases;
suppose
A3: k <= n;
hence seq1.k =((Coef(n)).k) * (z |^ k) * (w |^ (n-'k)) by A1
.= seq2.k by A2,A3;
end;
suppose
A4: k > n;
hence seq1.k = 0c by A1
.= seq2.k by A2,A4;
end;
end;
hence seq1=seq2;
end;
end;
definition
let n;
let z,w be Complex;
func Expan_e(n,z,w) -> Complex_Sequence means
:Def10:
for k be Nat holds ( k <= n implies
it.k=((Coef_e(n)).k) * (z |^ k) * (w |^ (n-'k)) ) & (n < k implies it.k=0);
existence
proof
deffunc U(Nat,Nat)
= ((Coef_e($1)).$2) * (z |^ $2) * (w |^ ($1-'$2));
for n holds ex seq st for k holds (k <= n implies seq.k = U(n,k)) &
(k > n implies seq.k=0) from ExComplexCASE;
hence thesis;
end;
uniqueness
proof
let seq1,seq2;
assume that
A1: for k holds
(k <= n implies seq1.k =((Coef_e(n)).k) * (z |^ k) * (w |^ (n-'k)) ) &
(k > n implies seq1.k=0) and
A2: for k holds
(k <= n implies seq2.k = ((Coef_e(n)).k) * (z |^ k) * (w |^ (n-'k)) ) &
(k > n implies seq2.k=0);
now
let k be Element of NAT;
per cases;
suppose
A3: k <= n;
hence seq1.k =((Coef_e(n)).k) * (z |^ k) * (w |^ (n-'k)) by A1
.= seq2.k by A2,A3;
end;
suppose
A4: k > n;
hence seq1.k = 0c by A1
.= seq2.k by A2,A4;
end;
end;
hence seq1=seq2;
end;
end;
definition
let n;
let z,w be Complex;
func Alfa(n,z,w) -> Complex_Sequence means
:Def11:
for k be Nat holds ( k <= n implies
it.k= (z ExpSeq).k * Partial_Sums(w ExpSeq).(n-'k) ) &
( n < k implies it.k=0);
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=0 ) from ExComplexCASE;
hence thesis;
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=0) and
A2: for k holds
(k <= n implies seq2.k = (z ExpSeq).k * Partial_Sums(w ExpSeq).(n-'k) )
& (k > n implies seq2.k=0);
now
let k be Element of NAT;
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;
end;
suppose
A4: k > n;
hence seq1.k = 0c by A1
.= seq2.k by A2,A4;
end;
end;
hence seq1=seq2;
end;
end;
definition
let a,b be Real;
let n be Nat;
func Conj(n,a,b) -> Real_Sequence means
for k be Nat holds
( k <= n implies it.k= (a rExpSeq).k * (Partial_Sums(b rExpSeq).n
-Partial_Sums(b rExpSeq).(n-'k))) & (n < k implies it.k=0);
existence
proof
deffunc U(Nat,Nat)
= (a rExpSeq).$2 * (Partial_Sums(b rExpSeq).$1
-Partial_Sums(b rExpSeq).($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 ExRealCASE;
hence thesis;
end;
uniqueness
proof
let rseq1,rseq2;
assume that
A1: for k holds
(k <= n implies rseq1.k =(a rExpSeq).k * (Partial_Sums(b rExpSeq).n
-Partial_Sums(b rExpSeq).(n-'k)) ) & (k > n implies rseq1.k=0) and
A2: for k holds
(k <= n implies rseq2.k = (a rExpSeq).k * (Partial_Sums(b rExpSeq).n
-Partial_Sums(b rExpSeq).(n-'k)) ) & (k > n implies rseq2.k=0);
now
let k be Element of NAT;
per cases;
suppose
A3: k <= n;
hence rseq1.k =(a rExpSeq).k * (Partial_Sums(b rExpSeq).n
-Partial_Sums(b rExpSeq).(n-'k)) by A1
.= rseq2.k by A2,A3;
end;
suppose
A4: k > n;
hence rseq1.k = 0 by A1
.= rseq2.k by A2,A4;
end;
end;
hence rseq1=rseq2;
end;
end;
definition
let z, w be Complex;
let n be Nat;
func Conj(n,z,w) -> Complex_Sequence means
:Def13:
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=0);
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=0) from ExComplexCASE;
hence thesis;
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=0) 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=0);
now
let k be Element of NAT;
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;
end;
suppose
A4: k > n;
hence seq1.k = 0c by A1
.= seq2.k by A2,A4;
end;
end;
hence seq1=seq2;
end;
end;
Lm1: for p1,p2,g1,g2 being Real holds
(p1+g1*<i>)*(p2+g2*<i>) =(p1*p2-g1*g2+(p1*g2+p2*g1)*<i>)
& (p2+g2*<i>)*'=(p2+(-g2)*<i>)
proof
let p1,p2,g1,g2 be Real;
thus (p1+g1*<i>)*(p2+g2*<i>) =(p1*p2-g1*g2+(p1*g2+p2*g1)*<i>);
thus (p2+g2*<i>)*' = p2-Im(p2+g2*<i>)*<i> by COMPLEX1:12
.= p2-g2*<i> by COMPLEX1:12
.=(p2+(-g2)*<i>);
end;
theorem Th3:
for z being Complex holds
z ExpSeq.(n+1) = z ExpSeq.n * z /(n+1+0*<i>) & z ExpSeq.0=1 &
|.(z ExpSeq).n .| = (|.z.| rExpSeq ).n
proof
let z be Complex;
A1: now
let n be Nat;
thus (z ExpSeq).(n+1)=z |^ (n+1) / ((n+1) ! ) by Def4
.=(z GeoSeq).n * z /((n+1)! ) by COMSEQ_3:def 1
.=z |^ n * z /(n! * (n+1+0*<i>)) by Th1
.=(z |^ n / (n! ) )*( z / (n+1+0*<i>)) by XCMPLX_1:76
.=(z |^ n / (n! ) * z) / (n+1+0*<i>)
.=z ExpSeq.n * z /(n+1+0*<i>) by Def4;
end;
A2: (z ExpSeq).0=z |^ 0 /(0! ) by Def4
.=1 by Th1,COMSEQ_3:def 1;
defpred X[Nat] means
|. ((z ExpSeq)).$1 .| =( |.z.| rExpSeq ).$1;
( |.z.| rExpSeq ).0 = ((|.z .|) |^ 0)/ (0!) by Def5
.= 1/((Prod_real_n).0) by NEWTON:4
.= 1/1 by Def2
.= 1;
then A3: X[0] by A2,COMPLEX1:48;
A4: now
let n such that
A5: X[n];
A6: |.(n+1+0*<i>).|=n+1 by ABSVALUE:def 1;
|. ((z ExpSeq)).(n+1) .| =|. z ExpSeq.n * z /(n+1+0*<i>) .| by A1
.=|. z ExpSeq.n * z .|/|.(n+1+0*<i>).| by COMPLEX1:67
.=(( |.z.| rExpSeq ).n) * |.z .|/|.(n+1+0*<i>).| by A5,COMPLEX1:65
.= (|.z.| |^ n)/(n!) * |.z .|/|.(n+1+0*<i>).| by Def5
.=( (|.z.| |^ n) * |.z .| )/( (n!) * |.(n+1+0*<i>).| ) by XCMPLX_1:83
.=( (|.z.| |^ n) * |.z .| )/( (n+1)! ) by A6,NEWTON:15
.=( (|.z.| |^ (n+1)) )/( (n+1)! ) by NEWTON:6
.=( |.z.| rExpSeq ).(n+1) by Def5;
hence X[n+1];
end;
for n holds X[n] from NAT_1:sch 2(A3,A4);
hence thesis by A1,A2;
end;
theorem Th4:
0 < k implies (Shift(seq)).k=seq.(k-'1)
proof
assume
A1: 0 < k;
A2: 0+1 <= k by INT_1:7,A1;
consider m be Nat such that
A3: m+1=k by A1,NAT_1:6;
A4: m=k-1 by A3;
thus (Shift seq).k=seq.m by A3,Def8
.=seq.(k-'1) by A2,A4,XREAL_1:233;
end;
theorem Th5:
Partial_Sums(seq).k=Partial_Sums(Shift(seq)).k+seq.k
proof
defpred X[Nat] means
Partial_Sums(seq).$1=Partial_Sums(Shift(seq)).$1+seq.$1;
Partial_Sums(seq).0=0c + seq.0 by SERIES_1:def 1
.=(Shift(seq)).0 + seq.0 by Def8
.=Partial_Sums(Shift(seq)).0+seq.0 by SERIES_1:def 1;
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(Shift(seq)).k+seq.k;
thus
Partial_Sums(seq).(k+1) = (Partial_Sums(Shift(seq)).k+seq.k) + seq.(k+1)
by A3,SERIES_1:def 1
.=(Partial_Sums(Shift(seq)).k+(Shift(seq)).(k+1)) + seq.(k+1) by Def8
.=Partial_Sums(Shift(seq)).(k+1)+seq.(k+1) by SERIES_1:def 1;
end;
for k holds X[k] from NAT_1:sch 2(A1,A2);
hence thesis;
end;
theorem Th6:
(z+w) |^ n = Partial_Sums(Expan(n,z,w)).n
proof
A1: 0-'0=0 by XREAL_1:232;
defpred X[Nat] means
(z+w) |^ $1 = Partial_Sums(Expan($1,z,w)).$1;
Partial_Sums(Expan(0,z,w)).0 = Expan(0,z,w).0 by SERIES_1:def 1
.= (Coef(0)).0 * (z |^ 0) * (w |^ 0) by A1,Def9
.= 1/(1 * 1) * z |^ 0 * w |^ 0 by A1,Def6,Th1
.= 1r * (w GeoSeq).0 by COMSEQ_3:def 1
.= 1r by COMSEQ_3:def 1;
then A2: X[0] by COMSEQ_3:def 1;
A3: for n st X[n] holds X[n+1]
proof
let n such that
A4: (z+w) |^ n = Partial_Sums(Expan(n,z,w)).n;
A5: n in NAT by ORDINAL1:def 12;
A6: (z+w) |^ (n+1) =((z+w) GeoSeq ).n * (z+w) by COMSEQ_3:def 1
.=((z+w) (#) Partial_Sums(Expan(n,z,w))).n by A4,VALUED_1:6
.=(Partial_Sums((z+w) (#) Expan(n,z,w))).n by COMSEQ_3:29;
now
let k be Element of NAT;
thus
((z+w) (#) Expan(n,z,w)).k=(z+w) * Expan(n,z,w).k by VALUED_1:6
.=z * Expan(n,z,w).k+w * Expan(n,z,w).k
.=(z (#) Expan(n,z,w)).k+w * Expan(n,z,w).k by VALUED_1:6
.=(z (#) Expan(n,z,w)).k+(w (#) Expan(n,z,w)).k by VALUED_1:6
.=((z (#) Expan(n,z,w))+(w (#) Expan(n,z,w))).k by VALUED_1:1;
end;
then
(z+w) (#) Expan(n,z,w)=(z (#) Expan(n,z,w))+(w (#) Expan(n,z,w));
then A7: (
z+w) |^ (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 VALUED_1:1,A5;
A8: 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 SERIES_1:def 1
.=Partial_Sums((z (#) Expan(n,z,w))).n
+z * Expan(n,z,w).(n+1) by VALUED_1:6;
n < n+1 by XREAL_1:29;
then A9: Expan(n,z,w).(n+1)=0c by Def9;
A10: 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 SERIES_1:def 1
.=Partial_Sums((w (#) Expan(n,z,w))).n
+w * Expan(n,z,w).(n+1) by VALUED_1:6;
A11: Partial_Sums((z (#) Expan(n,z,w))).(n+1)
=Partial_Sums(Shift((z (#) Expan(n,z,w)))).(n+1)
+(z (#) Expan(n,z,w)).(n+1) by Th5;
0 +n < n+1 by XREAL_1:29;
then Expan(n,z,w).(n+1)=0c by Def9;
then z * Expan(n,z,w).(n+1)=0c;
then A12: Partial_Sums((z (#) Expan(n,z,w))).(n+1)
=Partial_Sums(Shift((z (#) Expan(n,z,w)))).(n+1) +0c by A11,VALUED_1:6
.= Partial_Sums(Shift((z (#) Expan(n,z,w)))).(n+1);
now
let k be Element of NAT;
A13: now
assume
A14: n+1 < k;
A15: 0+1 <= n+1 by XREAL_1:6;
A16: n+1-1 < k -1 by A14,XREAL_1:9;
then A17: n+0 < k-1+1 by XREAL_1:8;
A18: k-1 = k-'1 by A14,A15,XREAL_1:233,XXREAL_0:2;
((w (#) Expan(n,z,w))+Shift((z (#) Expan(n,z,w)))).k
=(w (#) Expan(n,z,w)).k + (Shift((z (#) Expan(n,z,w)))).k
by VALUED_1:1
.=(w * Expan(n,z,w).k) + (Shift((z (#) Expan(n,z,w)))).k
by VALUED_1:6
.=(w * Expan(n,z,w).k) + ((z (#) Expan(n,z,w))).(k-'1) by A17,Th4
.=(w * Expan(n,z,w).k) + (z * (Expan(n,z,w).(k-'1))) by VALUED_1:6
.=(w * 0c )+ (z * ((Expan(n,z,w).(k-'1)))) by A17,Def9
.=0c + (z * 0c) by A16,A18,Def9
.=0c;
hence ((w (#) Expan(n,z,w))+Shift((z (#) Expan(n,z,w)))).k
=Expan(n+1,z,w).k by A14,Def9;
end;
now
assume
A19: k <= (n+1);
A20: now
assume
A21: k=n+1;
A22: n < n+1 by XREAL_1:29;
A23: n-'n= n-n by XREAL_1:233
.= 0;
A24: n+1-'(n+1)= n+1-(n+1) by XREAL_1:233
.= 0;
A25: (Coef(n)).(n) = n! /((n! ) * (0! )) by A23,Def6
.= 1 by Th1,XCMPLX_1:60;
A26: (Coef(n+1)).(n+1) = (n+1)! /(((n+1)! ) * (0! )) by A24,Def6
.= 1 by Th1,XCMPLX_1:60;
((w (#) Expan(n,z,w))+Shift((z (#) Expan(n,z,w)))).k =
(w (#) Expan(n,z,w)).(n+1)+(Shift((z (#) Expan(n,z,w)))).(n+1)
by A21,VALUED_1:1
.=(w * Expan(n,z,w).(n+1)) + (Shift((z (#) Expan(n,z,w)))).(n+1) by VALUED_1:6
.=( w * 0c) + (Shift((z (#) Expan(n,z,w)))).(n+1) by A22,Def9
.=((z (#) Expan(n,z,w))).n by Def8
.=z * (Expan(n,z,w)).n by VALUED_1:6
.=z * ((Coef(n)).n * (z |^ n) * (w |^ (n-'n))) by Def9
.= ((Coef(n)).n * ((z GeoSeq).n * z) * (w |^ (n-'n)))
.= ((Coef(n+1)).(n+1) * (z |^ (n+1)) * (w |^ (n-'n)))
by A25,A26,COMSEQ_3:def 1
.= Expan(n+1,z,w).k by A21,A23,A24,Def9;
hence ((w (#) Expan(n,z,w))+Shift((z (#) Expan(n,z,w)))).k=Expan(n+1,z,w) .
k;
end;
now
assume
A27: k < n+1;
A28: now
assume
A29: k=0;
A30: n-'0 =n-0 by XREAL_1:233;
A31: n+1-'0 =n+1-0 by XREAL_1:233;
A32: (Coef(n)).0 = n! /((0! ) * (n! )) by A30,Def6
.= 1 by Th1,XCMPLX_1:60;
A33: (Coef(n+1)).0 = (n+1)! /((0! ) * ((n+1)! )) by A31,Def6
.= 1 by Th1,XCMPLX_1:60;
((w (#) Expan(n,z,w))+Shift((z (#) Expan(n,z,w)))).k =
(w (#) Expan(n,z,w)).0+(Shift((z (#) Expan(n,z,w)))).0
by A29,VALUED_1:1
.=(w * Expan(n,z,w).0) + (Shift((z (#) Expan(n,z,w)))).0
by VALUED_1:6
.=(w * Expan(n,z,w).0) + 0c by Def8
.=w * ((Coef n).0 * (z |^ 0) * (w |^ (n-'0))) by Def9
.= (Coef n).0 * (z |^ 0) * (((w GeoSeq)).n * w) by A30
.= (Coef(n+1)).0 * (z |^ 0) * (w |^ (n+1-'0))
by A31,A32,A33,COMSEQ_3:def 1
.= Expan(n+1,z,w).k by A29,Def9;
hence ((w (#) Expan(n,z,w))+Shift((z (#) Expan(n,z,w)))).k =Expan(n+1,z,w).
k;
end;
now
assume
A34: k<>0;
then A35: 0+1 <= k by INT_1:7;
A36: k+1-1 <= n+1-1 by A27,INT_1:7;
k < k+1 by XREAL_1:29;
then k-1 <= k+1-1 by XREAL_1:9;
then k-1 <= n by A36,XXREAL_0:2;
then A37: k-'1 <= n by A35,XREAL_1:233;
A38: ((w (#) Expan(n,z,w))+Shift((z (#) Expan(n,z,w)))).k
=(w (#) Expan(n,z,w)).k+(Shift((z (#) Expan(n,z,w)))).k
by VALUED_1:1
.=(w * Expan(n,z,w).k) + (Shift((z (#) Expan(n,z,w)))).k
by VALUED_1:6
.=(w * Expan(n,z,w).k) + (z (#) Expan(n,z,w)).(k-'1)
by A34,Th4
.=(w * Expan(n,z,w).k) + (z * Expan(n,z,w).(k-'1))
by VALUED_1:6
.=(w * ((Coef n).k * (z |^ k) * (w |^ (n-'k))))
+ (z * Expan(n,z,w).(k-'1)) by A36,Def9
.=(w * ((Coef n).k * (z |^ k)) * (w |^ (n-'k)))
+ (z * ((Coef n).(k-'1) * (z |^ (k-'1))
* (w |^ (n-'(k-'1))))) by A37,Def9
.=((Coef n).k * (w * (z |^ k) * (w |^ (n-'k)) )
+ ((Coef n).(k-'1) * ((z |^ (k-'1))
* z * (w |^ (n-'(k-'1))))));
A39: (n-'k)+1=n-k+1 by A36,XREAL_1:233
.=n+1-k
.=n+1-'k by A27,XREAL_1:233;
A40: n-'(k-'1)=n-(k-'1) by A37,XREAL_1:233
.=n-(k-1) by A35,XREAL_1:233
.=n+1-k
.=n+1-'k by A27,XREAL_1:233;
(k-'1)+1 =k-1+1 by A35,XREAL_1:233
.=k;
then A41: (
w |^ (n-'k)) * w = w |^ (n-'k+1) & (z |^ (k-'1)) * z = z |^ k by COMSEQ_3:def 1
;
A42: (Coef n).k +(Coef n).(k-'1) =n! /((k!) * ((n-'k)!))
+(Coef n).(k-'1) by A36,Def6
.=n! /((k!) * ((n-'k)!))
+n! /(((k-'1)!) * (((n-'(k-'1)))! )) by A37,Def6;
A43: ((k!) * ((n-'k)!)) * (n+1-k+0*<i>)
=(k!) * (((n-'k)!) * (n+1-k+0*<i>));
A44: (((k-'1)!) * (((n-'(k-'1)))! )) * (k+0*<i>)
=(k+0*<i>) * ((k-'1)!) * (((n-'(k-'1)))! )
.=(k!) * ((n+1-'k)!) by A34,A40,Th2;
(n+1-k+0*<i>) <>0c by A27;
then A45: n ! /((k!) * ((n-'k)!)) =(n! * (n+1-k+0*<i>))
/(((k!) * ((n-'k)!)) * (n+1-k+0*<i>)) by XCMPLX_1:91
.=(n! * (n+1-k+0*<i>))/((k!) * ((n+1-'k)!))
by A36,A43,Th2;
n! /(((k-'1)!) * (((n-'(k-'1)))! ))
=(n! * (k+0*<i>))/((k!) * ((n+1-'k)! ))
by A34,A44,XCMPLX_1:91;
then (Coef n).k +(Coef n).(k-'1)
=( n! * (n+1-k+k+(0+0)*<i>)) / ((k!) * ((n+1-'k)!))
by A42,A45
.=((n+1)! ) / ((k!) * ((n+1-'k)!)) by Th1
.=(Coef(n+1)).k by A27,Def6;
then ((w (#) Expan(n,z,w))+Shift((z (#) Expan(n,z,w)))).k
=(Coef(n+1)).k * (z |^ k) * (w |^ (n+1-'k)) by A38,A39,A40,A41
.=Expan(n+1,z,w).k by A27,Def9;
hence ((w (#) Expan(n,z,w))+Shift((z (#) Expan(n,z,w)))).k =Expan(n+1,z,w).
k;
end;
hence ((w (#) Expan(n,z,w))+Shift((z (#) Expan(n,z,w)))).k
=Expan(n+1,z,w).k by A28;
end;
hence ((w (#) Expan(n,z,w))+Shift((z (#) Expan(n,z,w)))).k
=Expan(n+1,z,w).k by A19,A20,XXREAL_0:1;
end;
hence ((w (#) Expan(n,z,w))+Shift((z (#) Expan(n,z,w)))).k
=Expan(n+1,z,w).k by A13;
end;
then
A46: (w (#) Expan(n,z,w))+Shift((z (#) Expan(n,z,w))) =Expan(n+1,z,w);
thus (z+w) |^ (n+1) =(Partial_Sums((w (#) Expan(n,z,w))) +
Partial_Sums(Shift((z (#) Expan(n,z,w))))).(n+1)
by A7,A8,A9,A10,A12,VALUED_1:1
.=Partial_Sums(Expan(n+1,z,w)).(n+1) by A46,COMSEQ_3:27;
end;
for n holds X[n] from NAT_1:sch 2(A2,A3);
hence thesis;
end;
theorem Th7:
Expan_e(n,z,w)=(1r/(n! )) (#) Expan(n,z,w)
proof
now
let k be Element of NAT;
A1: now
assume
A2: n <k;
hence Expan_e(n,z,w).k =(1r/(n! )) * 0c by Def10
.=(1r/(n! )) * Expan(n,z,w).k by A2,Def9
.=((1r/(n! )) (#) Expan(n,z,w)).k by VALUED_1:6;
end;
now
assume
A3: k <= n;
then
A4: Expan_e(n,z,w).k = (Coef_e(n)).k * (z |^ k) * (w |^ (n-'k)) by Def10
.= 1r/((k! ) * ((n-'k)! )) * (z |^ k) * (w |^ (n-'k)) by A3,Def7;
1r/((k! ) * ((n-'k)! )) =(((n! ) * 1r )/(n! )) /((k! ) * ((n-'k)!))
by XCMPLX_1:60
.= (1r /(n! )) * (n! ) /((k! ) * ((n-'k)! ));
thus
then Expan_e(n,z,w).k = (1r/(n! )) * (n! ) /((k! ) * ((n-'k)! ))
* ((z |^ k) * (w |^ (n-'k))) by A4
.= (1r/(n! )) * ((n! ) /((k! ) * ((n-'k)! ))
* (z |^ k) * (w |^ (n-'k)))
.= (1r/(n! )) * ((Coef(n)).k * ((z |^ k))
* (w |^ (n-'k))) by A3,Def6
.= (1r/(n! )) * Expan(n,z,w).k by A3,Def9
.= ( (1r/(n! )) (#) Expan(n,z,w) ).k by VALUED_1:6;
end;
hence Expan_e(n,z,w).k = ( (1r/(n! )) (#) Expan(n,z,w) ).k by A1;
end;
hence thesis;
end;
theorem Th8:
((z+w) |^ n) / (n!) = Partial_Sums(Expan_e(n,z,w)).n
proof
thus ((z+w) |^ n)/(n! )
= (Partial_Sums(Expan(n,z,w)).n) * (1r/(n! )) by Th6
.= ((1r/(n! )) (#) (Partial_Sums(Expan(n,z,w)))).n by VALUED_1:6
.= Partial_Sums( (1r/(n! )) (#) Expan(n,z,w)).n by COMSEQ_3:29
.= Partial_Sums(Expan_e(n,z,w)).n by Th7;
end;
theorem Th9:
((0c qua Complex) ExpSeq is absolutely_summable)
& Sum((0c qua Complex) ExpSeq)=1r
proof
defpred X[set] means Partial_Sums(|.(0c qua Complex) ExpSeq.|).$1=jj;
Partial_Sums(|.((0c qua Complex) ExpSeq).|).0
=|.((0c qua Complex) ExpSeq).|.0 by SERIES_1:def 1
.=|. ((0c qua Complex) ExpSeq).0 .| by VALUED_1:18
.=1 by Th3,COMPLEX1:48;
then A1: X[0];
A2: for n being Nat st X[n] holds X[n+1]
proof
let n being Nat such that
A3: Partial_Sums(|.(0c qua Complex) ExpSeq.|).n=jj;
thus Partial_Sums(|.(0c qua Complex) ExpSeq.|).(n+1)
=1 + |.(0c qua Complex) ExpSeq.|.(n+1) by A3,SERIES_1:def 1
.=1 + |.((0c qua Complex) ExpSeq).(n+1).| by VALUED_1:18
.=1 + |.((0c qua Complex) ExpSeq.n) * 0c/(n+1+0*<i>) .| by Th3
.=jj by COMPLEX1:44;
end;
for n being Nat holds X[n] from NAT_1:sch 2(A1,A2);
then Partial_Sums(|.(0c qua Complex) ExpSeq.|)
is constant by VALUED_0:def 18;
then A4: |.(0c qua Complex) ExpSeq.| is summable by SERIES_1:def 2;
defpred X[set] means Partial_Sums((0c qua Complex) ExpSeq).$1=1;
Partial_Sums((0c qua Complex) ExpSeq).0
=((0c qua Complex) ExpSeq).0 by SERIES_1:def 1
.=1 by Th3;
then A5: X[0];
A6: for n st X[n] holds X[n+1]
proof
let n such that
A7: Partial_Sums((0c qua Complex) ExpSeq).n=1;
thus Partial_Sums((0c qua Complex) ExpSeq).(n+1)
=1r + ((0c qua Complex) ExpSeq).(n+1) by A7,SERIES_1:def 1
.=1r + ((0c qua Complex) ExpSeq.n) * 0c/(n+1+0*<i>) by Th3
.=1;
end;
for n holds X[n] from NAT_1:sch 2(A5,A6);
hence thesis by A4,COMSEQ_2:10;
end;
registration
let z be Complex;
cluster z ExpSeq -> absolutely_summable;
coherence
proof
now
assume
A1: z<>0c;
defpred X[set] means (z ExpSeq).$1 <> 0c;
A2: X[0] by Th3;
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 (z ExpSeq).(n+1) = 0c;
then A5: ((z ExpSeq).n * z)/(n+1+0*<i>)=0c by Th3;
0c = 0c/z .=(z ExpSeq).n * z/z by A5,XCMPLX_1:50
.=(z ExpSeq).n * (z/z)
.=(z ExpSeq).n * 1 by A1,XCMPLX_1:60
.=(z ExpSeq).n;
hence contradiction by A4;
end;
end;
deffunc U(Nat) = |.(z ExpSeq).|.($1+1)/|.(z ExpSeq).|.$1;
thus
A6: for n holds X[n] from NAT_1:sch 2(A2,A3);
ex rseq st for n holds rseq.n= U(n) from SEQ_1:sch 1;
then consider rseq such that
A7: for n holds rseq.n=|.z ExpSeq.|.(n+1)/|.z ExpSeq.|.n;
now
let n;
thus rseq.n =|.z ExpSeq.|.(n+1)/|.z ExpSeq.|.n by A7
.=|.(z ExpSeq).(n+1).|/|.z ExpSeq.|.n by VALUED_1:18
.=|.(z ExpSeq).(n+1).|/|.(z ExpSeq).n.| by VALUED_1:18
.=|.(z ExpSeq).(n+1)/(z ExpSeq).n.| by COMPLEX1:67
.=|.((z ExpSeq).n * z/(n+1+0*<i>)) /(z ExpSeq).n.| by Th3
.=|.((z ExpSeq).n * (z/(n+1+0*<i>))) /(z ExpSeq).n.|
.=|.(z/(n+1+0*<i>)) .| by A6,XCMPLX_1:89
.=|.z.|/|.n+1.| by COMPLEX1:67
.=|.z.|/(n+1) by ABSVALUE:def 1;
end;
then rseq is convergent & lim rseq < 1 by SEQ_4:31;
hence thesis by A6,A7,COMSEQ_3:75;
end;
hence thesis by Th9;
end;
end;
theorem Th10:
(z ExpSeq).0 = 1 & Expan(0,z,w).0 = 1
proof
thus (z ExpSeq).0 = (z |^ 0)/(0! ) by Def4
.= 1 by Th1,COMSEQ_3:def 1;
A1: 0-'0=0 by XREAL_1:232;
hence Expan(0,z,w).0 = (Coef(0)).0 * (z |^ 0) * (w |^ 0) by Def9
.= 1/(1 * 1) * z |^ 0 * w |^ 0 by A1,Def6,Th1
.= 1r * (w GeoSeq).0 by COMSEQ_3:def 1
.= 1 by COMSEQ_3:def 1;
end;
theorem Th11:
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;
A2: k < k+1 by XREAL_1:29;
then A3: l <= k+1 by A1,XXREAL_0:2;
(k+1-'l)=k+1-l by A1,A2,XREAL_1:233,XXREAL_0:2;
then A4: (k+1-'l)=k-l+1
.=(k-'l)+1 by A1,XREAL_1:233;
then A5: (Alfa(k+1,z,w)).l
=(z ExpSeq).l * (Partial_Sums(w ExpSeq).((k-'l)+1)) by A3,Def11
.=(z ExpSeq).l * (Partial_Sums(w ExpSeq).((k-'l))
+(w ExpSeq).((k+1-'l))) by A4,SERIES_1:def 1
.=((z ExpSeq).l * (Partial_Sums(w ExpSeq).((k-'l)))
+((z ExpSeq).l * (w ExpSeq).((k+1-'l))))
.=(Alfa(k,z,w)).l+((z ExpSeq).l * (w ExpSeq).((k+1-'l))) by A1,Def11;
(z ExpSeq).l * (w ExpSeq).((k+1-'l))
=(z |^ l/(l! )) * (w ExpSeq).((k+1-'l)) by Def4
.=(z |^ l/(l! )) * (w |^ ((k+1-'l))/(((k+1-'l))! )) by Def4
.=(((z |^ l) * (w |^ ((k+1-'l))) * 1r)/((l! ) * (((k+1-'l))! )))
by XCMPLX_1:76
.=((z |^ l) * (w |^ ((k+1-'l))) * ((1r/((l! ) * (((k+1-'l))! )))))
.= ((Coef_e(k+1)).l) * ((z |^ l) * (w |^ ((k+1-'l)))) by A3,Def7
.= ((Coef_e(k+1)).l) * (z |^ l) * (w |^ ((k+1-'l)))
.=Expan_e(k+1,z,w).l by A3,Def10;
hence thesis by A5;
end;
theorem Th12:
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
A1: k in NAT by ORDINAL1:def 12;
now
let l be Nat;
A2: l in NAT by ORDINAL1:def 12;
assume l <= k;
hence
(Alfa(k+1,z,w)).l = (Alfa(k,z,w)).l + Expan_e(k+1,z,w).l by Th11
.= ( (Alfa(k,z,w)) + Expan_e(k+1,z,w)).l by VALUED_1:1,A2;
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 VALUED_1:1,A1;
end;
theorem Th13:
(z ExpSeq).k=(Expan_e(k,z,w)).k
proof
A1: 0 = k -k;
then A2: k-'k=0 by XREAL_1:233;
A3: (k-'k)! =1 by A1,Th1,XREAL_1:233;
thus (Expan_e(k,z,w)).(k)=((Coef_e(k)).k) * (z |^ k) * (w |^ 0) by A2,Def10
.=( (Coef_e(k)).k) * (z |^ k) * 1r by COMSEQ_3:11
.=(1r/((k! ) * 1r)) * (z |^ k) by A3,Def7
.=((z |^ k) * 1r)/(k! )
.=(z ExpSeq).k by Def4;
end;
theorem Th14:
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 SERIES_1:def 1
.=1 by Th10;
defpred X[Nat] means
Partial_Sums((z+w) ExpSeq).$1=Partial_Sums(Alfa($1,z,w)).$1;
A2: 0-'0=0 by XREAL_1:232;
Partial_Sums(Alfa(0,z,w)).0 = Alfa(0,z,w).0 by SERIES_1:def 1
.= (z ExpSeq).0 * Partial_Sums(w ExpSeq).0 by A2,Def11
.= (z ExpSeq).0 * (w ExpSeq).0 by SERIES_1:def 1
.=1r * (w ExpSeq).0 by Th10
.= 1 by Th10;
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;
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 SERIES_1:def 1
.=((Partial_Sums(( Alfa(k,z,w) ))).k
+ (Partial_Sums(( Expan_e(k+1,z,w) ))).k )
+ (Alfa(k+1,z,w)).(k+1) by Th12
.= Partial_Sums((z+w) ExpSeq).k
+ ((Partial_Sums(( Expan_e(k+1,z,w) ))).k
+ (Alfa(k+1,z,w)).(k+1)) by A5;
k+1-'(k+1)=0 by XREAL_1:232;
then (Alfa(k+1,z,w)).(k+1)
=(z ExpSeq).(k+1) * Partial_Sums(w ExpSeq).0 by Def11
.=(z ExpSeq).(k+1) * ((w ExpSeq).0) by SERIES_1:def 1
.=(z ExpSeq).(k+1) * 1 by Th10
.=(Expan_e(k+1,z,w)).(k+1) by Th13;
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 SERIES_1:def 1
.=(z+w) |^ (k+1) /((k+1)! ) by Th8;
then Partial_Sums((Alfa(k+1,z,w))).(k+1) =Partial_Sums((z+w) ExpSeq).k
+(z+w) ExpSeq.(k+1) by A6,Def4
.=Partial_Sums((z+w) ExpSeq).(k+1) by SERIES_1:def 1;
hence
Partial_Sums((z+w) ExpSeq).(k+1)=Partial_Sums(Alfa(k+1,z,w)).(k+1);
end;
for n holds X[n] from NAT_1:sch 2(A3,A4);
hence thesis;
end;
theorem Th15:
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: k in NAT by ORDINAL1:def 12;
A2: (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 Th14
.= ((Partial_Sums(w ExpSeq).k) (#) Partial_Sums(z ExpSeq)).k
-Partial_Sums(Alfa(k,z,w)).k by VALUED_1:6
.=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 VALUED_1:8
.=(Partial_Sums((Partial_Sums(w ExpSeq).k) (#) (z ExpSeq))
-Partial_Sums(Alfa(k,z,w))).k by VALUED_1:1,A1
.=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
A3: l <= k;
A4: l in NAT by ORDINAL1:def 12;
thus ( ( Partial_Sums(w ExpSeq).k) (#) (z ExpSeq) - (Alfa(k,z,w)) ).l
=(( Partial_Sums(w ExpSeq).k) (#) (z ExpSeq)).l
+(-Alfa(k,z,w)).l by VALUED_1:1,A4
.=(( Partial_Sums(w ExpSeq).k) (#) (z ExpSeq)).l -Alfa(k,z,w).l
by VALUED_1:8
.=(( Partial_Sums(w ExpSeq).k ) * ( (z ExpSeq).l ))
-Alfa(k,z,w).l by VALUED_1:6
.=((z ExpSeq).l) * ( Partial_Sums(w ExpSeq).k)
-((z ExpSeq).l) * ( Partial_Sums(w ExpSeq).(k-'l)) by A3,Def11
.=((z ExpSeq).l) * ( Partial_Sums(w ExpSeq).k
-Partial_Sums(w ExpSeq).(k-'l) )
.=Conj(k,z,w).l by A3,Def13;
end;
hence thesis by A2,COMSEQ_3:35;
end;
theorem Th16:
|. Partial_Sums((z ExpSeq)).k .| <= Partial_Sums(|.z.| rExpSeq).k &
Partial_Sums((|.z.| rExpSeq)).k <= Sum(|.z.| rExpSeq) &
|. Partial_Sums(( z ExpSeq)).k .| <= Sum(|.z.| rExpSeq)
proof
defpred X[Nat] means |. Partial_Sums(( z ExpSeq)).$1 .|
<= Partial_Sums((|.z.| rExpSeq)).$1;
A1: |.
Partial_Sums(( z ExpSeq)).0 .| = |. ((z ExpSeq)).0 .| by SERIES_1:def 1
.= |. (z |^ 0)/ (0 !).| by Def4
.= 1 by Th1,COMPLEX1:48,COMSEQ_3:def 1;
Partial_Sums((|.z.| rExpSeq)).0 = ((|.z.| rExpSeq)).0 by SERIES_1:def 1
.= ((|.z .|) |^ 0)/ (0!) by Def5
.= 1 by NEWTON:4,12;
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.| rExpSeq)).k;
|.
Partial_Sums(( z ExpSeq)).(k+1) .| =|. Partial_Sums(( z ExpSeq)).k + ((z
ExpSeq)).(k+1) .| & |. Partial_Sums(( z ExpSeq)).k + ((z ExpSeq)).(k+1) .| <=
|. Partial_Sums(( z ExpSeq)).k.| + |. ((z ExpSeq)).(k+1) .| by COMPLEX1:56
,SERIES_1:def 1;
then A5: |. Partial_Sums(( z ExpSeq)).(k+1) .|
<= |. Partial_Sums(( z ExpSeq)).k.| + (|.z.| rExpSeq).(k+1) by Th3;
A6: |. Partial_Sums(( z ExpSeq)).k.| + (|.z.| rExpSeq).(k+1)
<= Partial_Sums((|.z.| rExpSeq)).k + (|.z.| rExpSeq).(k+1) by A4,XREAL_1:6;
Partial_Sums((|.z.| rExpSeq)).k + (|.z.| rExpSeq).(k+1)
=Partial_Sums((|.z.| rExpSeq)).(k+1) by SERIES_1:def 1;
hence thesis by A5,A6,XXREAL_0:2;
end;
A7: for k holds X[k] from NAT_1:sch 2(A2,A3);
thus
then
|. Partial_Sums(( z ExpSeq)).k .| <= Partial_Sums((|.z.| rExpSeq)).k;
now
let k be object such that
A8: k in NAT;
thus |. (z ExpSeq).|.k = |. (z ExpSeq).k .| by VALUED_1:18
.= (|.z.| rExpSeq).k by A8,Th3;
end;
then A9: |. z ExpSeq .| = |.z.| rExpSeq;
then
Partial_Sums((|.z.| rExpSeq)).k <= lim(Partial_Sums((|.z.| rExpSeq )))
by SEQ_4:37;
hence Partial_Sums((|.z.| rExpSeq)).k <= Sum(|.z.| rExpSeq)
by SERIES_1:def 3;
A10: now
let k;
lim
(Partial_Sums((|.z.| rExpSeq)))=Sum(|.z.| rExpSeq) by SERIES_1:def 3;
hence Partial_Sums((|.z.| rExpSeq)).k <= Sum(|.z.| rExpSeq)
by A9,SEQ_4:37;
end;
A11: |. Partial_Sums(( z ExpSeq)).k .|
<= Partial_Sums((|.z.| rExpSeq)).k by A7;
Partial_Sums((|.z.| rExpSeq)).k <= Sum(|.z.| rExpSeq) by A10;
hence thesis by A11,XXREAL_0:2;
end;
theorem Th17:
1 <= Sum(|.z.| rExpSeq)
proof
|. Partial_Sums(z ExpSeq).0 .|=|. (z ExpSeq).0 .| by SERIES_1:def 1
.=1 by Th3,COMPLEX1:48;
hence thesis by Th16;
end;
theorem Th18:
0 <= (|. z .| rExpSeq).n
proof
(|. z .| rExpSeq).n = |.((z ExpSeq)).n .| by Th3;
hence thesis by COMPLEX1:46;
end;
theorem Th19:
|.(Partial_Sums(|.z .| rExpSeq)).n.| = Partial_Sums(|.z .| rExpSeq).n &
(n <= m implies
|.(Partial_Sums(|.z .| rExpSeq).m-Partial_Sums(|.z .| rExpSeq).n).|
= Partial_Sums(|.z .| rExpSeq).m-Partial_Sums(|.z .| rExpSeq).n)
proof
for n holds 0 <= (|. z .| rExpSeq).n by Th18;
hence thesis by COMSEQ_3:9;
end;
theorem Th20:
|.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 VALUED_1:18;
hence 0 <= |.Conj(k,z,w).|.n by COMPLEX1:46;
end;
A2: Partial_Sums(|.Conj(k,z,w).|).0 <= Partial_Sums(|.Conj(k,z,w).|).n &
Partial_Sums(|.Conj(k,z,w).|).0=(|.Conj(k,z,w).|).0 by SEQM_3:6
,SERIES_1:def 1;
0 <= (|.Conj(k,z,w).|).0 by A1;
hence thesis by A2,ABSVALUE:def 1;
end;
theorem Th21:
for p being Real st p>0 ex n st for k st n <= k
holds |.Partial_Sums(|.Conj(k,z,w).|).k.| < p
proof
let p be Real such that
A1: p>0;
reconsider pp = p as Real;
A2: 1 <= Sum(|.z.| rExpSeq) by Th17;
A3: 0 < Sum(|.w.| rExpSeq) by Th17;
set p1=min((pp/(4 * Sum(|.z.| rExpSeq))),(pp/(4 * Sum(|.w.| rExpSeq))));
A4: p1 > 0 by A1,A2,A3,XXREAL_0:15;
now
let k be object such that
A5: k in NAT;
thus |. (z ExpSeq).|.k = |. (z ExpSeq).k .| by VALUED_1:18
.= (|.z.| rExpSeq).k by A5,Th3;
end;
then |. z ExpSeq .| = |.z.| rExpSeq;
then consider n1 such that
A6: for k,l be Nat st n1 <= k & n1 <= l holds
|.Partial_Sums(( |.z.| rExpSeq )).k - Partial_Sums(( |.z.| rExpSeq )).l.|
< p1 by A4,COMSEQ_3:4;
consider n2 being Nat such that
A7: for k,l be Nat st n2 <= k & n2 <= l holds
|.Partial_Sums(( w ExpSeq )).k - Partial_Sums(( w ExpSeq )).l.|
< p1 by A4,COMSEQ_3:47;
set n3=n1+n2;
take n4 = n3+n3;
A8: now
let n;
let k;
now
let l be Nat such that
A9: l <= k;
thus |.Conj(k,z,w).|.l =|.( Conj(k,z,w).l) .| by VALUED_1:18
.=|.(z ExpSeq).l * (Partial_Sums(w ExpSeq).k
-Partial_Sums(w ExpSeq).(k-'l)) .| by A9,Def13
.=|.(z ExpSeq).l.| * |.(Partial_Sums(w ExpSeq).k
-Partial_Sums(w ExpSeq).(k-'l)).| by COMPLEX1:65
.=(|.z.| rExpSeq).l * |.(Partial_Sums(w ExpSeq).k
-Partial_Sums(w ExpSeq).(k-'l)).| by Th3;
end;
hence for l be Nat st l <= k holds
|.Conj(k,z,w).|.l =(|.z.| rExpSeq).l * |.(Partial_Sums(w ExpSeq).k
-Partial_Sums(w ExpSeq).(k-'l)).|;
end;
A10: now
let k;
now
let l be Nat;
assume l <= k;
then
A11: |.Conj(k,z,w).|.l =(|.z .| rExpSeq).l * |.Partial_Sums(w ExpSeq ).k
-Partial_Sums(w ExpSeq).(k-'l).| by A8;
|.Partial_Sums(w ExpSeq).k .| <= Sum(|.w.| rExpSeq) by Th16;
then A12: |.Partial_Sums(w ExpSeq).k .| + |.Partial_Sums(w ExpSeq).(k-'l ).|
<= Sum(|.w.| rExpSeq) + |.Partial_Sums(w ExpSeq).(k-'l).| by XREAL_1:6;
|.Partial_Sums(w ExpSeq).(k-'l).| <= Sum(|.w.| rExpSeq) by Th16;
then Sum(|.w.| rExpSeq) + |.Partial_Sums(w ExpSeq).(k-'l).|
<= Sum(|.w.| rExpSeq)+ Sum(|.w.| rExpSeq) by XREAL_1:6;
then |.
Partial_Sums(w ExpSeq).k -Partial_Sums(w ExpSeq).(k-'l).| <= |.Partial_Sums
(w ExpSeq).k .| + |.Partial_Sums(w ExpSeq).(k-'l).| & |.Partial_Sums(w ExpSeq)
.k .| + |.Partial_Sums(w ExpSeq).(k-'l).| <= 2 * Sum(|.w.| rExpSeq) by A12,
COMPLEX1:57,XXREAL_0:2;
then A13: |.Partial_Sums(w ExpSeq).k -Partial_Sums(w ExpSeq).(k-'l).|
<= 2 * Sum(|.w.| rExpSeq) by XXREAL_0:2;
0 <= (|.z .| rExpSeq).l by Th18;
thus
then |.Conj(k,z,w).|.l <= (|.z .| rExpSeq).l * (2 * Sum(|.w.| rExpSeq))
by A11,A13,XREAL_1:64;
end;
hence for l be Nat st l <= k holds
|.Conj(k,z,w).|.l <= (|.z .| rExpSeq).l * (2 * Sum(|.w.| rExpSeq));
end;
now
let k such that
A14: n4 <= k;
A15: 0+n3 <= n3+n3 by XREAL_1:6;
then A16: n3 <= k by A14,XXREAL_0:2;
A17: n1+0 <= n1+n2 by XREAL_1:6;
then A18: n1 <= k by A16,XXREAL_0:2;
now
let l be Nat;
assume
A19: l <= n3;
then A20: k-'l=k-l by A16,XREAL_1:233,XXREAL_0:2;
A21: 0+n2 <= n1+n2 by XREAL_1:6;
A22: n4-l <= k-l by A14,XREAL_1:9;
n3+n3-n3 <= n3+n3-l by A19,XREAL_1:10;
then n3 <= k-l by A22,XXREAL_0:2;
then A23: n2 <= k-'l by A20,A21,XXREAL_0:2;
0+n3 <= n3+n3 by XREAL_1:6;
then n2 <= n4 by A21,XXREAL_0:2;
then n2 <= k by A14,XXREAL_0:2;
then A24: |.
Partial_Sums(( w ExpSeq )).k - Partial_Sums(( w ExpSeq )).(k -'l).|
< p1 by A7,A23;
0 <= (|.z .| rExpSeq).l by Th18;
then (|.z .| rExpSeq).l * |.Partial_Sums(( w ExpSeq )).k
- Partial_Sums(( w ExpSeq )).(k-'l).|
<= (|.z .| rExpSeq).l * p1 by A24,XREAL_1:64;
hence
|.Conj(k,z,w).|.l <= p1 * (|.z .| rExpSeq).l by A8,A16,A19,XXREAL_0:2;
end;
then A25: Partial_Sums(|.Conj(k,z,w).|).n3
<= Partial_Sums(|.z .| rExpSeq).n3 * p1 by COMSEQ_3:7;
Partial_Sums(|.z .| rExpSeq).n3 * p1
<= Sum(|.z.| rExpSeq) * p1 by A4,Th16,XREAL_1:64;
then A26: Partial_Sums(|.Conj(k,z,w).|).n3
<= Sum(|.z.| rExpSeq) * p1 by A25,XXREAL_0:2;
A27: Sum(|.z.| rExpSeq) * p1 <= Sum(|.z.| rExpSeq) * (p/(4 * Sum
(|.z.| rExpSeq))) by A2,XREAL_1:64,XXREAL_0:17;
A28: 0 <> Sum(|.z.| rExpSeq) by Th17;
Sum(|.z.| rExpSeq) * (p/(4 * Sum(|.z.| rExpSeq)))
=(Sum(|.z.| rExpSeq) * p)/(4 * Sum(|.z.| rExpSeq))
.=p/4 by A28,XCMPLX_1:91;
then A29: Partial_Sums(|.Conj(k,z,w).|).n3 <= p/4 by A26,A27,XXREAL_0:2;
0+p/4 < p/4 + p/4 by A1,XREAL_1:6;
then A30: Partial_Sums(|.Conj(k,z,w).|).n3 < p/2 by A29,XXREAL_0:2;
k-'n3=k-n3 by A14,A15,XREAL_1:233,XXREAL_0:2;
then A31: k=(k-'n3)+n3;
for l be Nat st l <= k holds
|.Conj(k,z,w).|.l <= (2 * Sum(|.w.| rExpSeq)) * (|.z .| rExpSeq).l by A10;
then A32: Partial_Sums(|.Conj(k,z,w).|).(k) -Partial_Sums(|.Conj(k,z,w).|). n3
<= (Partial_Sums(|.z .| rExpSeq).(k) -Partial_Sums(|.z .| rExpSeq).n3)
* (2 * Sum(|.w.| rExpSeq)) by A31,COMSEQ_3:8;
|.(Partial_Sums(|.z .| rExpSeq).k-Partial_Sums(|.z .| rExpSeq).n3).|
<= p1 by A6,A17,A18;
then Partial_Sums(|.z .| rExpSeq).k-Partial_Sums(|.z .| rExpSeq).n3
<= p1 by A14,A15,Th19,XXREAL_0:2;
then (Partial_Sums(|.z .| rExpSeq).k -Partial_Sums(|.z .| rExpSeq).n3)
* (2 * Sum(|.w.| rExpSeq))
<= p1 * (2 * Sum(|.w.| rExpSeq)) by A3,XREAL_1:64;
then A33: Partial_Sums(|.Conj(k,z,w).|).k-Partial_Sums(|.Conj(k,z,w).|).n3
<= p1 * (2 * Sum(|.w.| rExpSeq)) by A32,XXREAL_0:2;
A34: (2 * Sum(|.w.| rExpSeq)) * p1
<= (2 * Sum(|.w.| rExpSeq)) * (p/(4 * Sum(|.w.| rExpSeq)))
by A3,XREAL_1:64,XXREAL_0:17;
A35: 0 <> Sum(|.w.| rExpSeq) by Th17;
(2 * Sum(|.w.| rExpSeq) ) * (p/(4 * Sum(|.w.| rExpSeq)))
=((2 * p ) * Sum(|.w.| rExpSeq) ) /(4 * Sum(|.w.| rExpSeq))
.= (p +p )/4 by A35,XCMPLX_1:91
.= p/2;
then Partial_Sums(|.Conj(k,z,w).|).k-Partial_Sums(|.Conj(k,z,w).|).n3
<= p/2 by A33,A34,XXREAL_0:2;
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 A30,XREAL_1:8;
hence |.Partial_Sums(|.Conj(k,z,w).|).k.| < p by Th20;
end;
hence thesis;
end;
theorem Th22:
(for k holds seq.k=Partial_Sums((Conj(k,z,w))).k) implies
seq is convergent & lim seq = 0
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 SEQ_1:sch 1;
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;
A5: now
let p be Real;
assume p>0;
then consider n such that
A6: for k st n <= k
holds |.Partial_Sums(|.Conj(k,z,w).|).k.| < p by Th21;
take n;
now
let k such that
A7: n <= k;
|.rseq.k-0.|=|.Partial_Sums(|.Conj(k,z,w).|).k.| by A3;
hence |.rseq.k-0.| < p by A6,A7;
end;
hence for k st n <= k holds |.rseq.k-0.| < p;
end;
then A8: rseq is convergent by SEQ_2:def 6;
then lim(rseq) =0 by A5,SEQ_2:def 7;
hence seq is convergent & lim(seq)=0c by A4,A8,COMSEQ_3:48;
end;
hence thesis;
end;
Lm2: for z,w being Complex holds
Sum(z ExpSeq) * Sum(w ExpSeq) = Sum((z+w) ExpSeq)
proof
let z0,w0 be Complex;
reconsider z=z0, w=w0 as Element of COMPLEX by XCMPLX_0:def 2;
deffunc U(Nat) = Partial_Sums(Conj($1,z,w)).$1;
ex seq st for k holds seq.k= U(k) from COMSEQ_1:sch 1;
then consider seq such that
A1: for k holds seq.k=Partial_Sums(Conj(k,z,w)).k;
now
let k be Element of NAT;
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 Th15
.=(Partial_Sums(z ExpSeq) (#) Partial_Sums(w ExpSeq)).k
-Partial_Sums((z+w) ExpSeq).k by VALUED_1:5
.=(Partial_Sums(z ExpSeq) (#) Partial_Sums(w ExpSeq)).k
+(-Partial_Sums((z+w) ExpSeq)).k by VALUED_1:8
.=(Partial_Sums(z ExpSeq) (#) Partial_Sums(w ExpSeq)
-Partial_Sums((z+w) ExpSeq) ).k by VALUED_1:1;
end;
then A2: seq=Partial_Sums(z ExpSeq) (#) Partial_Sums(w ExpSeq)
-Partial_Sums((z+w) ExpSeq);
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:30;
lim(seq)=0c by A1,Th22;
hence thesis by A2,A3,COMSEQ_3:10;
end;
begin :: Definition of Exponential Function on Complex
definition
func exp -> Function of COMPLEX, COMPLEX means
:Def14:
for z being Complex holds it.z=Sum(z ExpSeq);
existence
proof
deffunc U(Element of COMPLEX) = Sum($1 ExpSeq);
consider f being Function of COMPLEX, COMPLEX such that
A1: for x being Element of COMPLEX holds f.x = U(x) from FUNCT_2:sch 4;
take f;
let z be Complex;
z in COMPLEX by XCMPLX_0:def 2;
hence thesis by A1;
end;
uniqueness
proof
let f1,f2 be Function of COMPLEX, COMPLEX;
assume
A2: for z being Complex holds f1.z=Sum(z ExpSeq);
assume
A3: for z being Complex holds f2.z=Sum(z ExpSeq);
for z being Element of COMPLEX holds f1.z = f2.z
proof
let z be Element of COMPLEX;
thus f1.z=Sum(z ExpSeq) by A2
.=f2.z by A3;
end;
hence f1=f2;
end;
end;
definition
let z be Complex;
func exp z -> Complex equals
exp.z;
coherence;
end;
definition
let z be Complex;
redefine func exp z -> Element of COMPLEX; :: redefines exp (SIN_COS, definition)
coherence by XCMPLX_0:def 2;
end;
theorem
for z1, z2 being Complex holds exp(z1+z2)=exp(z1) *exp(z2)
proof
let z1,z2 be Complex;
exp(z1+z2)=Sum((z1+z2) ExpSeq) by Def14
.=Sum(z1 ExpSeq)*Sum(z2 ExpSeq) by Lm2
.=exp(z1)*Sum(z2 ExpSeq) by Def14
.=exp(z1) *exp(z2) by Def14;
hence thesis;
end;
begin :: Definition of Sinus, Cosine, and Exponential Function on REAL
reserve d for Real;
definition
func sin -> Function of REAL, REAL means
:Def16:
for d holds it.d = Im(Sum(d*<i> ExpSeq));
existence
proof
deffunc U(Real) = Im(Sum($1*<i> ExpSeq));
consider f being Function of REAL, REAL such that
A1: for x being Element of REAL holds f.x = U(x) from FUNCT_2:sch 4;
take f;
let x be Real;
reconsider x as Element of REAL by XREAL_0:def 1;
f.x = U(x) by A1;
hence thesis;
end;
uniqueness
proof
let f1,f2 be Function of REAL, REAL;
assume
A2: for d holds f1.d=Im(Sum(d*<i> ExpSeq));
assume
A3: for d holds f2.d=Im(Sum(d*<i> ExpSeq));
for d being Element of REAL holds f1.d = f2.d
proof
let d be Element of REAL;
thus f1.d=Im(Sum((d*<i>) ExpSeq)) by A2
.=f2.d by A3;
end;
hence f1=f2;
end;
end;
definition
let th be Real;
func sin th -> number equals
sin.th;
coherence;
end;
registration
let th be Real;
cluster sin th -> real;
coherence;
end;
definition
func cos -> Function of REAL, REAL means
:Def18:
for d holds it.d = Re(Sum(d*<i> ExpSeq));
existence
proof
deffunc U(Real) = Re(Sum(($1*<i>) ExpSeq));
consider f being Function of REAL, REAL such that
A1: for x being Element of REAL holds f.x = U(x) from FUNCT_2:sch 4;
take f;
let d;
reconsider d as Element of REAL by XREAL_0:def 1;
f.d = U(d) by A1;
hence thesis;
end;
uniqueness
proof
let f1,f2 be Function of REAL, REAL;
assume
A2: for d holds f1.d=Re(Sum(d*<i> ExpSeq));
assume
A3: for d holds f2.d=Re(Sum(d*<i> ExpSeq));
for d being Element of REAL holds f1.d=f2.d
proof
let d be Element of REAL;
thus f1.d=Re(Sum((d*<i>) ExpSeq)) by A2
.=f2.d by A3;
end;
hence f1=f2;
end;
end;
definition
let th be Real;
func cos th -> number equals
cos.th;
coherence;
end;
registration
let th be Real;
cluster cos th -> real;
coherence;
end;
theorem Th24:
dom(sin)=REAL & dom(cos)=REAL by FUNCT_2:def 1;
Lm3: Sum(th*<i> ExpSeq)=cos.(th)+(sin.th)*<i>
proof
Im(Sum(th*<i> ExpSeq))=sin.(th) & Re(Sum(th*<i> ExpSeq))=cos.(th)
by Def16,Def18;
hence thesis by COMPLEX1:13;
end;
theorem
exp(th*<i>)=cos(th)+(sin th)*<i>
proof
exp(th*<i>)=Sum(th*<i> ExpSeq ) by Def14
.=cos(th)+(sin th)*<i> by Lm3;
hence thesis;
end;
Lm4: (Sum((th*<i>) ExpSeq))*' = Sum((-(th*<i>)) ExpSeq)
proof
Partial_Sums(((th*<i>) ExpSeq))*' =Partial_Sums((-(th*<i>)) ExpSeq)
proof
A1: for n holds (((th*<i>) ExpSeq).n)*' = ((-(th*<i>)) ExpSeq).n
proof
defpred X[Nat] means
(((th*<i>) ExpSeq).$1)*' = ((-(th*<i>)) ExpSeq).$1;
(((th*<i>) ExpSeq).0)*' =1r by Th3,COMPLEX1:30
.=((-(th*<i>)) ExpSeq).0 by Th3;
then A2: X[0];
A3: for n st X[n] holds X[n+1]
proof
let n;
assume
A4: ((th*<i> ExpSeq).n)*' = ((-(th*<i>)) ExpSeq).n;
thus (((th*<i>) ExpSeq).(n+1))*'
=(((th*<i>) ExpSeq).n * (th*<i>)/(n+1+0*<i>))*' by Th3
.=((th*<i> ExpSeq).n * ((th*<i>)/(n+1+0*<i>)))*'
.=((-(th*<i>)) ExpSeq).n * ((th*<i>)/(n+1))*' by A4,COMPLEX1:35
.=((-(th*<i>)) ExpSeq).n * ((0+th*<i>)*'/((n+1))*') by COMPLEX1:37
.=((-(th*<i>)) ExpSeq).n * ((0+(-th)*<i>) /(n+1+0*<i>)*') by Lm1
.=((-(th*<i>)) ExpSeq).n * ((0+(-th)*<i>)/(n+1+(-0)*<i>)) by Lm1
.=((-(th*<i>)) ExpSeq).n * (-(th*<i>))/(n+1+0*<i>)
.=((-(th*<i>)) ExpSeq).(n+1) by Th3;
end;
thus for n holds X[n] from NAT_1:sch 2(A2,A3);
end;
defpred X[Nat] means
(Partial_Sums(((th*<i>) ExpSeq))*').$1
=Partial_Sums((-(th*<i>)) ExpSeq).$1;
(Partial_Sums((th*<i>) ExpSeq)*').0
=(Partial_Sums((th*<i>) ExpSeq).0)*' by COMSEQ_2:def 2
.=(((th*<i>) ExpSeq).0)*' by SERIES_1:def 1
.=1 by Th3,COMPLEX1:30
.=((-(th*<i>)) ExpSeq).0 by Th3
.=Partial_Sums((-(th*<i>)) ExpSeq).0 by SERIES_1:def 1;
then A5: X[0];
A6: for n being Nat st X[n] holds X[n+1]
proof
let n be Nat such that
A7: (Partial_Sums(((th*<i>) ExpSeq))*').n
=Partial_Sums((-(th*<i>)) ExpSeq).n;
A8: n in NAT by ORDINAL1:def 12;
thus (Partial_Sums((th*<i>) ExpSeq)*').(n+1)
=(Partial_Sums((th*<i>) ExpSeq).(n+1))*' by COMSEQ_2:def 2
.=(Partial_Sums((th*<i>) ExpSeq).n+((th*<i>) ExpSeq).(n+1))*'
by SERIES_1:def 1
.=(Partial_Sums((th*<i>) ExpSeq).n)*'+(((th*<i>) ExpSeq).(n+1))*'
by COMPLEX1:32
.=Partial_Sums((-(th*<i>)) ExpSeq).n+(((th*<i>) ExpSeq).(n+1))*'
by A7,COMSEQ_2:def 2,A8
.=Partial_Sums((-(th*<i>)) ExpSeq).n+((-(th*<i>)) ExpSeq).(n+1) by A1
.=Partial_Sums((-(th*<i>)) ExpSeq).(n+1) by SERIES_1:def 1;
end;
for n being Nat holds X[n] from NAT_1:sch 2(A5,A6);
hence thesis;
end;
hence thesis by COMSEQ_2:12;
end;
theorem
(exp((th*<i>)))*'=exp(-(th*<i>))
proof
(exp((th*<i>)))*'=(Sum((th*<i>) ExpSeq))*' by Def14
.=Sum((-(th*<i>)) ExpSeq) by Lm4
.=exp(-(th*<i>)) by Def14;
hence thesis;
end;
Lm5: for th1 being Real st th = th1 holds
|.Sum(th*<i> ExpSeq ).| = 1 & |.sin.th1.| <= 1 & |.cos.th1.| <= 1
proof
let th1 be Real such that
A1: th = th1;
A2: Sum((th*<i>) ExpSeq ) * Sum((-(th*<i>)) ExpSeq )
=Sum(((th*<i>)+(-(th*<i>))) ExpSeq ) by Lm2
.=1r by Th9;
|.Sum((th*<i>) ExpSeq ).| * |.Sum((th*<i>) ExpSeq ).|
=|.Sum((th*<i>) ExpSeq )*Sum((th*<i>) ExpSeq ).| by COMPLEX1:65
.=|.Sum((th*<i>) ExpSeq ) * Sum((th*<i>) ExpSeq)*'.| by COMPLEX1:69
.=1 by A2,Lm4,COMPLEX1:48;
then
A3: |.Sum((th*<i>) ExpSeq ).| =1/|.Sum((th*<i>) ExpSeq ).| & |.Sum((th*<i>)
ExpSeq ).| <> 0 by XCMPLX_1:73;
|.Sum((th*<i>) ExpSeq ).| <> -1 by COMPLEX1:46;
hence A4: |.Sum(th*<i> ExpSeq ).|=1 by A3,XCMPLX_1:199;
|.sin.th.|=|.Im(Sum((th*<i>) ExpSeq )).| & |.cos.th.|=|.Re(Sum((th*<i>)
ExpSeq )).| by Def16,Def18;
hence thesis by A1,A4,COMSEQ_3:13;
end;
theorem
|.exp((th*<i>)).| = 1 &
for th being Real holds |.sin th.| <= 1 & |.cos th.| <= 1
proof
thus |.exp((th*<i>)).| =|.Sum((th*<i>) ExpSeq ).| by Def14
.=1 by Lm5;
let th be Real;
thus |.sin(th).| <= 1 by Lm5;
thus thesis by Lm5;
end;
reserve th,th1,th2 for Real;
theorem Th28:
(cos.th)^2+(sin.th)^2=1 & (cos.th)*(cos.th)+(sin.th)*(sin.th)=1
proof
reconsider th1=th as Real;
A1: Sum((th1*<i>) ExpSeq ) * Sum((-(th1*<i>)) ExpSeq )
=Sum(((th1*<i>)+(-(th1*<i>))) ExpSeq ) by Lm2
.=1r by Th9;
thus
(cos.(th))^2+(sin.(th))^2
=(Re(Sum((th1*<i>) ExpSeq )))^2+(sin.(th))^2 by Def18
.=(Re(Sum((th1*<i>) ExpSeq )))^2+(Im(Sum((th1*<i>) ExpSeq )))^2 by Def16
.=|.Sum((th1*<i>) ExpSeq )*Sum((th1*<i>) ExpSeq ).| by COMPLEX1:68
.=|.Sum((th1*<i>) ExpSeq ) * Sum((th1*<i>) ExpSeq)*'.| by COMPLEX1:69
.=1 by A1,Lm4,COMPLEX1:48;
hence thesis;
end;
theorem
(cos(th))^2+(sin(th))^2=1 &
(cos(th))*(cos(th))+(sin(th))*(sin(th))=1 by Th28;
theorem Th30:
cos.0=1 & sin.0=0 & cos.(-th)=cos.th & sin.(-th)=-sin.th
proof
thus cos.0 = Re(Sum(0*<i> ExpSeq)) by Def18
.= 1 by Th9,COMPLEX1:6;
thus sin.0 = Im(Sum(0*<i> ExpSeq)) by Def16
.= 0 by Th9,COMPLEX1:6;
reconsider th1=th as Real;
thus cos.(-th) = Re( Sum((-0+(-th1)*<i>) ExpSeq) ) by Def18
.= Re( Sum((-(th1*<i>)) ExpSeq) )
.= Re(Sum((th1*<i>) ExpSeq)*') by Lm4
.= Re((cos.(th)+(sin.th)*<i>)*') by Lm3
.= Re(cos.(th)+(-sin.th)*<i>) by Lm1
.= cos.(th) by COMPLEX1:12;
thus sin.(-th) = Im( Sum((-0+(-th1)*<i>) ExpSeq) ) by Def16
.= Im( Sum((-(th1*<i>)) ExpSeq) )
.= Im(Sum((th1*<i>) ExpSeq)*') by Lm4
.= Im((cos.(th)+(sin.th)*<i>)*') by Lm3
.= Im(cos.(th)+(-sin.th)*<i>) by Lm1
.= -sin.(th) by COMPLEX1:12;
end;
theorem
cos(0)=1 & sin(0)=0 & cos(-th)=cos(th) & sin(-th)=-sin(th) by Th30;
definition
let th be Real;
deffunc U(Nat) = (-1)|^ $1 * (th)|^ (2*$1+1)/((2*$1+1)!);
func th P_sin -> Real_Sequence means
:Def20:
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 SEQ_1:sch 1;
end;
uniqueness
proof let s1,s2 be Real_Sequence such that
A1: for x being Nat holds s1.x = U(x) and
A2: for x being Nat holds s2.x = U(x);
let x be Element of NAT;
thus s1.x = U(x) by A1 .= s2.x by A2;
end;
deffunc U(Nat) = (-1)|^ $1 * (th)|^ (2*$1)/((2*$1)!);
func th P_cos -> Real_Sequence means
:Def21:
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 SEQ_1:sch 1;
end;
uniqueness
proof let s1,s2 be Real_Sequence such that
A3: for x being Nat holds s1.x = U(x) and
A4: for x being Nat holds s2.x = U(x);
let x be Element of NAT;
thus s1.x = U(x) by A3 .= s2.x by A4;
end;
end;
theorem Th32:
for z being Complex,
k holds z|^ (2*k) = (z|^ k)|^ 2& z|^ (2*k)= (z|^ 2)|^ k
proof
let z be Complex, k;
defpred X[Nat] means
z|^ (2*$1) = (z|^ $1)|^ 2 & z|^ (2*$1)= (z|^ 2)|^ $1;
A1: z|^ (2*0) =1*1 by NEWTON:4
.= 1|^1*1
.= 1|^(1+1)
.= (z|^ 0)|^2 by NEWTON:4;
z|^ (2*0) = 1 by NEWTON:4
.= (z|^ 2)|^ 0 by NEWTON:4;
then A2: X[0] by A1;
A3: for k st X[k] holds X[k+1]
proof
let k;
assume that
A4: z|^ (2*k) = (z|^ k)|^ 2 and
A5: z|^ (2*k)= (z|^ 2)|^ k;
A6: z|^ (2*(k+1))=z GeoSeq.(2*k+1+1) .=z GeoSeq.(2*k+1)*z by COMSEQ_3:def 1
.=z|^ (2*k)*z*z by COMSEQ_3:def 1;
then A7: z|^ (2*(k+1)) =((z|^ k)GeoSeq.(1+1))*z*z by A4
.=((z|^ k)GeoSeq.(0+1)*(z|^ k))*z*z by COMSEQ_3:def 1
.=((z|^ k)GeoSeq.0*(z|^ k)*(z|^ k))*z*z by COMSEQ_3:def 1
.=((1r)*(z|^ k)*(z|^ k))*z*z by COMSEQ_3:def 1
.=(1r)*(z GeoSeq.k*z)*((z|^ k)*z)
.=(1r)*(z GeoSeq.(k+1))*(z GeoSeq.k*z) by COMSEQ_3:def 1
.=(1r)*(z|^(k+1))*(z GeoSeq.(k+1)) by COMSEQ_3:def 1
.=((z|^(k+1))GeoSeq.0)*(z|^(k+1))*(z|^(k+1)) by COMSEQ_3:def 1
.=((z|^(k+1))GeoSeq.(0+1))*(z|^(k+1)) by COMSEQ_3:def 1
.=(z|^(k+1))GeoSeq.(0+1+1) by COMSEQ_3:def 1
.=(z|^(k+1))|^ 2;
z|^ (2*(k+1))= (z|^ 2)|^ k*(1r*z*z) by A5,A6
.= (z|^ 2)|^ k*(z GeoSeq.0 *z*z) by COMSEQ_3:def 1
.=(z|^ 2)|^ k*(z GeoSeq.(0+1) *z) by COMSEQ_3:def 1
.=(z|^ 2)|^ k*z GeoSeq.(0+1+1) by COMSEQ_3:def 1
.= (z|^ 2)|^ (k+1) by COMSEQ_3:def 1;
hence thesis by A7;
end;
for k holds X[k] from NAT_1:sch 2(A2,A3);
hence thesis;
end;
theorem Th33:
for th holds (th*<i>) |^ (2*k)=(-1)|^ k* (th |^ (2*k))
& (th*<i>) |^ (2*k+1)=(-1)|^ k* (th |^ (2*k+1))*<i>
proof
let th;
A1: (-1)|^ 0* (th |^ (2*0))*<i>=(-1)|^ 0* th GeoSeq.0*<i> by PREPOWER:def 1
.=(-1)|^ 0*(1)*<i> by PREPOWER:3
.=(-1)GeoSeq.0*<i> by PREPOWER:def 1
.=1*<i> by PREPOWER:3;
defpred X[Nat] means
(th*<i>) |^ (2*$1)=(-1)|^ $1* (th |^ (2*$1))
& (th*<i>) |^ (2*$1+1)=(-1)|^ $1* (th |^ (2*$1+1))*<i>;
(-1)|^ 0 * (th |^ (2*0+1))*<i>=(-1)|^ 0 * (th GeoSeq.(2*0+1))*<i>
by PREPOWER:def 1
.= (-1)|^ 0* (th GeoSeq.0*th)*<i> by PREPOWER:3
.=(-1)|^ 0* (1*th)*<i> by PREPOWER:3
.= ((-1)GeoSeq.0)* th *<i> by PREPOWER:def 1
.=(1)* th *<i> by PREPOWER:3
.=(th*<i>);
then A2: X[0] by A1,COMSEQ_3:def 1;
A3: for k st X[k] holds X[k+1]
proof
let k;
assume that
A4: (th*<i>) |^ (2*k)=(-1)|^ k* (th |^ (2*k)) and
A5: (th*<i>) |^ (2*k+1)=(-1)|^ k* (th |^ (2*k+1))*<i>;
A6: (th*<i>) |^ (2*(k+1))= ((th*<i>) |^ 2)|^(k+1) by Th32
.=((th*<i>) |^ 2)|^ k * ((th*<i>) |^ 2) by COMSEQ_3:def 1
.= (-1)|^ k* (th |^ (2*k))* ((th*<i>)GeoSeq.(1+1)) by A4,Th32
.=(-1)|^ k* (th |^ (2*k))* ((th*<i>)GeoSeq.(0+1)*(th*<i>))
by COMSEQ_3:def 1
.=(-1)|^ k* (th |^ (2*k))* ((th*<i>)GeoSeq.0*(th*<i>)
*(th*<i>)) by COMSEQ_3:def 1
.= (-1)|^ k* (th |^ (2*k))* (1r*(th*<i>)*(th*<i>))
by COMSEQ_3:def 1
.=(-1)|^ k*(-1)* (th |^ (2*k))*th*th
.=(-1)GeoSeq.k*(-1)* (th |^ (2*k))*th*th by PREPOWER:def 1
.=(-1)GeoSeq.(k+1)* (th |^ (2*k))*th*th by PREPOWER:3
.=(-1)|^(k+1)* (th |^ (2*k))*th*th by PREPOWER:def 1
.=(-1)|^(k+1)* (th GeoSeq.(2*k))*th*th by PREPOWER:def 1
.= (-1)|^(k+1)* (th GeoSeq.(2*k)*th)*th
.=(-1)|^(k+1)* (th GeoSeq.(2*k+1))*th by PREPOWER:3
.=(-1)|^(k+1)* (th GeoSeq.(2*k+1)*th)
.=(-1)|^(k+1)* (th GeoSeq.(2*k+1+1)) by PREPOWER:3
.=(-1)|^(k+1)* (th |^ (2*(k+1))) by PREPOWER:def 1;
(th*<i>) |^ (2*(k+1)+1)=
(th*<i>)GeoSeq.(2*k+1+1)*(th*<i>) by COMSEQ_3:def 1
.=(th*<i>)GeoSeq.(2*k+1)*(th*<i>)*(th*<i>) by COMSEQ_3:def 1
.=(-1)|^ k*(-1)* (th |^ (2*k+1))*th*th*<i> by A5
.=(-1)GeoSeq.k*(-1)* (th |^ (2*k+1))*th*th*<i> by PREPOWER:def 1
.=(-1)GeoSeq.(k+1)* (th |^ (2*k+1))*th*th*<i> by PREPOWER:3
.=(-1)|^ (k+1)* (th |^ (2*k+1))*th*th*<i> by PREPOWER:def 1
.=(-1)|^ (k+1)* (th GeoSeq.(2*k+1))*th*th*<i> by PREPOWER:def 1
.=(-1)|^ (k+1)* (th GeoSeq.(2*k+1)*th)*th*<i>
.=(-1)|^ (k+1)* (th GeoSeq.(((2*k+1)+1)))*th*<i> by PREPOWER:3
.=(-1)|^ (k+1)* (th GeoSeq.((2*k+1+1))*th)*<i>
.= (-1)|^ (k+1)* (th GeoSeq.(2*(k+1)+1))*<i> by PREPOWER:3
.=(-1)|^ (k+1)*(th |^ (2*(k+1)+1))*<i> by PREPOWER:def 1;
hence thesis by A6;
end;
for k holds X[k] from NAT_1:sch 2(A2,A3);
hence thesis;
end;
::$CT
theorem Th34:
for th holds
Partial_Sums(th P_sin).n = Partial_Sums(Im ((th*<i>) ExpSeq)).(2*n+1) &
Partial_Sums(th P_cos).n = Partial_Sums(Re ((th*<i>) 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 Def20;
A2: ((2*0+1)!)= 0! * 1 by NEWTON:15
.= 1 by NEWTON:12;
A3: (-1)|^ 0 = (-1) GeoSeq.0 by PREPOWER:def 1
.= 1 by PREPOWER:3;
A4: Partial_Sums(th P_cos).0= (th P_cos).0 by SERIES_1:def 1
.=(-1)|^ 0 * (th)|^ (2*0)/((2*0)!) by Def21
.= 1* th GeoSeq.0 / 1 by A3,NEWTON:12,PREPOWER:def 1
.=1 by PREPOWER:3;
A5: (
Im ((th*<i>) ExpSeq)).0= Im (((th*<i>) ExpSeq).0) & (Im ((th*<i>) ExpSeq)).
1= Im (((th*<i>) ExpSeq).1) by COMSEQ_3:def 6;
A6: (th*<i>) = 0+th*<i>;
A7: Partial_Sums(Im ((th*<i>) ExpSeq)).(2*0+1)
= Partial_Sums(Im ((th*<i>) ExpSeq)).0 +
(Im ((th*<i>) ExpSeq)).1 by SERIES_1:def 1
.= (Im ((th*<i>) ExpSeq)).0+
(Im ((th*<i>) ExpSeq)).1 by SERIES_1:def 1
.= 0 + Im (((th*<i>) ExpSeq).(0+1)) by A5,Th3,COMPLEX1:6
.=0 + Im ((((th*<i>) ExpSeq).0)* (th*<i>) /(0+1+0*<i>)) by Th3
.= Im (1* (th*<i>) /1) by Th3
.=th by A6,COMPLEX1:12;
defpred X[Nat] means
Partial_Sums(th P_sin).$1 = Partial_Sums(Im ((th*<i>) ExpSeq)).(2*$1+1) &
Partial_Sums(th P_cos).$1 = Partial_Sums(Re ((th*<i>) ExpSeq)).(2*$1);
Partial_Sums(Re ((th*<i>) ExpSeq)).(2*0)
= (Re ((th*<i>) ExpSeq)).0 by SERIES_1:def 1
.= Re (((th*<i>) ExpSeq).0) by COMSEQ_3:def 5
.=1 by Th3,COMPLEX1:6;
then A8: X[0] by A1,A2,A3,A4,A7;
A9: for k st X[k] holds X[k+1]
proof
let k be Nat;
assume that
A10: Partial_Sums(th P_sin).k = Partial_Sums(Im ((th*<i>) ExpSeq)).(2*k+1) and
A11: Partial_Sums(th P_cos).k = Partial_Sums(Re ((th*<i>) ExpSeq)).(2*k);
Partial_Sums(Im ((th*<i>) ExpSeq)).(2*(k+1)+1)
= Partial_Sums(Im ((th*<i>) ExpSeq)).((2*k+1)+1) +
(Im ((th*<i>) ExpSeq)).(2*(k+1)+1) by SERIES_1:def 1
.= Partial_Sums(th P_sin).k +
(Im((th*<i>) ExpSeq)).(2*(k+1))+(Im ((th*<i>) ExpSeq)).(2*(k+1)+1)
by A10,SERIES_1:def 1
.= Partial_Sums(th P_sin).k +
Im (((th*<i>) ExpSeq).(2*(k+1)))+(Im((th*<i>) ExpSeq)).(2*(k+1)+1)
by COMSEQ_3:def 6
.=Partial_Sums(th P_sin).k +
Im (((th*<i>) ExpSeq).(2*(k+1)))+Im(((th*<i>) ExpSeq).(2*(k+1)+1))
by COMSEQ_3:def 6
.= Partial_Sums(th P_sin).k +
Im((th*<i>) |^ (2*(k+1))/((2*(k+1))!))+
Im(((th*<i>) ExpSeq).(2*(k+1)+1)) by Def4
.= Partial_Sums(th P_sin).k +
Im((th*<i>) |^ (2*(k+1))/((2*(k+1))!))+
Im((th*<i>) |^ (2*(k+1)+1)/((2*(k+1)+1)!)) by Def4
.= Partial_Sums(th P_sin).k +
Im( (-1)|^ (k+1)* (th |^ (2*(k+1)))/ ((2*(k+1))!))
+Im((th*<i>) |^ (2*(k+1)+1)/((2*(k+1)+1)!)) by Th33
.= Partial_Sums(th P_sin).k +
Im( (-1)|^ (k+1)* (th |^ (2*(k+1)))/ ((2*(k+1))!))
+ Im( (-1)|^ (k+1)* (th |^ (2*(k+1)+1))*<i>/((2*(k+1)+1)!)) by Th33;
then Partial_Sums(Im ((th*<i>) 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))!)*<i>))
+ Im( ((-1)|^ (k+1)* (th |^ (2*(k+1)+1))*<i>)/((2*(k+1)+1)!));
then Partial_Sums(Im ((th*<i>) ExpSeq)).(2*(k+1)+1)
= Partial_Sums(th P_sin).k + 0 + Im(0/((2*(k+1)+1)!)+
((-1)|^ (k+1)* (th |^ (2*(k+1)+1)))/((2*(k+1)+1)!)*<i>)
by COMPLEX1:12
.= Partial_Sums(th P_sin).k + (0/((2*(k+1))!)) +
(-1)|^ (k+1)* (th |^ (2*(k+1)+1))/((2*(k+1)+1)!) by COMPLEX1:12;
then A12: Partial_Sums(Im ((th*<i>) ExpSeq)).(2*(k+1)+1)
= Partial_Sums(th P_sin).k + th P_sin.(k+1) by Def20
.= Partial_Sums(th P_sin).(k+1) by SERIES_1:def 1;
Partial_Sums(Re ((th*<i>) ExpSeq)).(2*(k+1))
= Partial_Sums(Re ((th*<i>) ExpSeq)).(2*k+1)+
(Re ((th*<i>) ExpSeq)).((2*k+1)+1) by SERIES_1:def 1
.=Partial_Sums(th P_cos).k + (Re ((th*<i>) ExpSeq)).(2*k+1)+
(Re ((th*<i>) ExpSeq)).((2*k+1)+1) by A11,SERIES_1:def 1
.= Partial_Sums(th P_cos).k + Re (((th*<i>) ExpSeq).(2*k+1))+
(Re ((th*<i>) ExpSeq)).((2*k+1)+1) by COMSEQ_3:def 5
.= Partial_Sums(th P_cos).k + Re (((th*<i>) ExpSeq).(2*k+1))+
Re (((th*<i>) ExpSeq).((2*k+1)+1)) by COMSEQ_3:def 5
.=Partial_Sums(th P_cos).k + Re ((th*<i>)|^ (2*k+1)/ ((2*k+1)!))+
Re (((th*<i>) ExpSeq).((2*k+1)+1)) by Def4
.= Partial_Sums(th P_cos).k + Re ((th*<i>)|^ (2*k+1)/ ((2*k+1)!))+
Re ((th*<i>)|^ (2*(k+1))/(((2*k+1)+1)!)) by Def4
.= Partial_Sums(th P_cos).k +
Re ( (-1)|^ k* (th |^ (2*k+1))*<i>/((2*k+1)!))+
Re ((th*<i>)|^ (2*(k+1))/((2*(k+1))!)) by Th33
.= Partial_Sums(th P_cos).k +
Re ( (-1)|^ k* (th |^ (2*k+1))*<i>/((2*k+1)!))+
Re ((-1)|^ (k+1)* (th |^ (2*(k+1)))/((2*(k+1))!)) by Th33;
then
Partial_Sums(Re ((th*<i>) ExpSeq)).(2*(k+1)) = Partial_Sums(th P_cos).k +
Re ( (0/((2*k+1)!)+((-1)|^ k* (th |^ (2*k+1)))/((2*k+1)!)*<i>)) +
Re ((-1)|^ (k+1)* (th |^ (2*(k+1)))/((2*(k+1))!));
then Partial_Sums(Re ((th*<i>) ExpSeq)).(2*(k+1))
= 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))!))*<i>)
by COMPLEX1:12
.= Partial_Sums(th P_cos).k +0/((2*k+1)!)+
(-1)|^ (k+1)* (th |^ (2*(k+1)))/((2*(k+1))!) by COMPLEX1:12;
then Partial_Sums(Re ((th*<i>) ExpSeq)).(2*(k+1))
= Partial_Sums(th P_cos).k + th P_cos.(k+1) by Def21
.= Partial_Sums(th P_cos).(k+1) by SERIES_1:def 1;
hence thesis by A12;
end;
thus for n holds X[n] from NAT_1:sch 2(A8,A9);
end;
hence thesis;
end;
theorem Th35:
for th holds
Partial_Sums(th P_sin) is convergent & Sum(th P_sin)=Im(Sum
((th*<i>) ExpSeq))
&Partial_Sums(th P_cos) is convergent & Sum(th P_cos)=Re(Sum
((th*<i>) ExpSeq))
proof
let th;
A1: Sum(((th*<i>) ExpSeq))
=Sum(Re ((th*<i>) ExpSeq))+Sum(Im ((th*<i>) ExpSeq))*<i> by COMSEQ_3:53;
then
A2: Sum(Re ((th*<i>) ExpSeq))= Re (Sum(((th*<i>) ExpSeq))) by COMPLEX1:12;
A3: Sum(Im ((th*<i>) ExpSeq))=Im (Sum(((th*<i>) ExpSeq))) by A1,COMPLEX1:12;
A4: Partial_Sums
(Re ((th*<i>) ExpSeq)) is convergent & lim Partial_Sums(Re ((th*
<i>) ExpSeq))= Re (Sum(((th*<i>) ExpSeq))) by A2,SERIES_1:def 2,def 3;
A5: Partial_Sums
(Im ((th*<i>) ExpSeq)) is convergent & lim Partial_Sums(Im ((th*
<i>) ExpSeq))=Im (Sum(((th*<i>) ExpSeq))) by A3,SERIES_1:def 2,def 3;
A6: now
let p be Real;
assume p>0;
then consider n such that
A7: for k st n <= k holds |.Partial_Sums(Re ((th*<i>) ExpSeq)).k-
Re (Sum(((th*<i>) ExpSeq))).| < p by A4,SEQ_2:def 7;
take n;
now
let k such that
A8: n <= k;
|.Partial_Sums(th P_cos).k-Re (Sum(((th*<i>) ExpSeq))).| =|.Partial_Sums(
Re ((th*<i>) ExpSeq)).(2*k)- Re (Sum(((th*<i>) ExpSeq))).| & 2*k=k+k by Th34;
hence |.Partial_Sums(th P_cos).k-Re (Sum(((th*<i>) ExpSeq))).|
< p by A7,A8,NAT_1:12;
end;
hence for k st n <= k holds
|.Partial_Sums(th P_cos).k-Re (Sum(((th*<i>) ExpSeq))).| < p;
end;
then Partial_Sums(th P_cos) is convergent by SEQ_2:def 6;
then A9: lim(Partial_Sums(th P_cos))=Re(Sum ((th*<i>) ExpSeq)) by A6,
SEQ_2:def 7;
A10: now
let p be Real;
assume p>0;
then consider n such that
A11: for k st n <= k holds |.Partial_Sums(Im ((th*<i>) ExpSeq)).k-
Im (Sum(((th*<i>) ExpSeq))).| < p by A5,SEQ_2:def 7;
take n;
now
let k such that
A12: n <= k;
A13: |.Partial_Sums(th P_sin).k-Im (Sum(((th*<i>) ExpSeq))).|
=|.Partial_Sums(Im ((th*<i>) ExpSeq)).(2*k+1)-
Im (Sum(((th*<i>) ExpSeq))).| by Th34;
2*k=k+k;
then n <= 2*k by A12,NAT_1:12;
then n<2*k+1 by NAT_1:13;
hence |.Partial_Sums(th P_sin).k-Im (Sum(((th*<i>) ExpSeq))).|
< p by A11,A13;
end;
hence for k st n <= k holds
|.Partial_Sums(th P_sin).k-Im (Sum(((th*<i>) 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
((th*<i>) ExpSeq)) by A10,SEQ_2:def 7;
hence thesis by A6,A9,A10,SEQ_2:def 6,SERIES_1:def 3;
end;
theorem Th36:
cos.th=Sum(th P_cos) & sin.th=Sum(th P_sin)
proof
reconsider th as Real;
sin.th = Im(Sum((th*<i>) ExpSeq)) & cos.th=Re(Sum((th*<i>) ExpSeq)) by Def16
,Def18;
hence thesis by Th35;
end;
theorem
for p,th,rseq st rseq is convergent &
lim(rseq)=th & (for n holds rseq.n >= p) holds th >= p by PREPOWER:1;
deffunc U(Real) = 2*$1+1;
consider bq being Real_Sequence such that
Lm6: for n holds bq.n= U(n) from SEQ_1:sch 1;
bq is increasing sequence of NAT
proof
A1: for n,k st n<k holds bq.n<bq.k
proof
let n,k;
assume n<k;
then 2*n<2*k by XREAL_1:68;
then 2*n+1<2*k+1 by XREAL_1:6;
then bq.n<2*k+1 by Lm6;
hence thesis by Lm6;
end;
for n holds bq.n is Element of NAT
proof
let n;
2*n+1 is Element of NAT;
hence thesis by Lm6;
end;
hence thesis by A1,SEQM_3:1,13;
end;
then reconsider bq as increasing sequence of NAT;
Lm7: for th,th1,th2,th3 be Real holds
th |^ (2*n)=(th |^ n)|^ 2 & (-1)|^(2*n)=1 & (-1)|^ (2*n+1)=-1
proof
let th,th1,th2,th3 be Real;
reconsider 2n = 2*n as Element of NAT by ORDINAL1:def 12;
thus th |^ (2*n)=(th |^ n)|^ 2 by NEWTON:9;
(-1)|^(2n)=(1)|^(2n) by POWER:1
.=1;
hence
A1: (-1)|^(2*n)= 1;
thus (-1)|^ (2*n+1)=(-1)|^ (2*n)*(-1) by NEWTON:6
.=-1 by A1;
end;
theorem Th38:
n <= k implies n! <= k!
proof
assume
A1: n <= k;
A2: for m holds 1<= m+1
proof
let m;
0+1<= m+1 by XREAL_1:6;
hence thesis;
end;
deffunc U(Nat) = $1!;
consider rseq such that
A3: for l holds rseq.l=U(l) from SEQ_1:sch 1;
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;
rseq.(0+1)=(0+1)! by A3
.=0!*1 by NEWTON:15
.=1 by NEWTON:12; then
A4: X[0] by A3,NEWTON:12;
A5: for l st X[l] holds X[l+1]
proof
let l;
assume
A6: rseq.l<=rseq.(l+1) & rseq.l>0;
rseq.(l+1+1)= (l+1+1)! by A3
.=(l+1)!*(l+1+1) by NEWTON:15
.=rseq.(l+1) *(l+1+1) by A3;
hence thesis by A2,A6,XREAL_1:151;
end;
for l holds X[l] from NAT_1:sch 2(A4,A5);
hence thesis;
end;
then A7: rseq is non-decreasing;
n!=rseq.n & k! = rseq.k by A3;
hence thesis by A1,A7,SEQM_3:6;
end;
theorem Th39:
0<=th & th <=1 & n<=k implies th |^ k <= th |^ n
proof
assume that
A1: 0<=th and
A2: th <=1 and
A3: n<=k;
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:3
.= 1*th by PREPOWER:3
.=th;
then A4: X[0] by A2,PREPOWER:3;
A5: for m st X[m] holds X[m+1]
proof
let m;
assume that
th GeoSeq.(m+1)<=th GeoSeq.m and
A6: th GeoSeq.m >=0;
th GeoSeq.(m+1+1)=th GeoSeq.(m+1)*th &
th GeoSeq.(m+1)=th GeoSeq.(m)*th by PREPOWER:3;
hence thesis by A1,A2,A6,XREAL_1:153;
end;
for m holds X[m] from NAT_1:sch 2(A4,A5);
hence thesis;
end;
then A7: th GeoSeq is non-increasing;
th |^ k=th GeoSeq. k & th |^ n=th GeoSeq. n by PREPOWER:def 1;
hence thesis by A3,A7,SEQM_3:8;
end;
::$CT
theorem Th41:
for p being Real holds Im(Sum(p ExpSeq))=0
proof
let p be Real;
A1: for n holds (Partial_Sums(Im(p ExpSeq))).n=0
proof
let n;
defpred X[Nat] means (Partial_Sums(Im(p ExpSeq))).$1=0;
(Partial_Sums(Im(p ExpSeq))).0=Im(p ExpSeq).0 by SERIES_1:def 1
.=Im(p ExpSeq.0) by COMSEQ_3:def 6
.=0 by Th3,COMPLEX1:6;
then A2: X[0];
A3: for k st X[k] holds X[k+1]
proof
let k;
assume (Partial_Sums(Im(p ExpSeq))).k=0; then
(Partial_Sums(Im(p ExpSeq))).(k+1)
=0+ (Im(p ExpSeq)).(k+1) by SERIES_1:def 1
.=Im((p ExpSeq).(k+1)) by COMSEQ_3:def 6
.=Im(p |^ (k+1) /((k+1)!) ) by Def4
.=Im((p|^ (k+1))/((k+1)!)+0*<i>)
.=0 by COMPLEX1:12;
hence thesis;
end;
for n holds X[n] from NAT_1:sch 2(A2,A3);
hence thesis;
end;
for n,m being Nat holds (Partial_Sums(Im(p ExpSeq))).n=
(Partial_Sums(Im(p ExpSeq))).m
proof
let n,m be Nat;
m in NAT & (Partial_Sums(Im(p ExpSeq))).n=0 by A1,ORDINAL1:def 12;
hence thesis by A1;
end;
then A4: lim Partial_Sums(Im(p ExpSeq))=Partial_Sums(Im(p
ExpSeq)).0 by SEQ_4:26,VALUED_0:24
.= 0 by A1;
Im(Sum(p ExpSeq))
= Im(Sum(Re (p ExpSeq))+(Sum(Im (p ExpSeq))*<i>)) by COMSEQ_3:53
.= Sum(Im (p ExpSeq )) by COMPLEX1:12;
hence thesis by A4,SERIES_1:def 3;
end;
theorem Th42:
cos.1>0 & sin.1>0 & cos.1<sin.1
proof
A1: Partial_Sums(1 P_cos) is convergent by Th35;
A2: cos.1=Sum(1 P_cos) by Th36;
lim ((Partial_Sums(1 P_cos))*bq )=lim(Partial_Sums(1 P_cos)) by A1,SEQ_4:17;
then A3: lim ((Partial_Sums(1 P_cos))*bq )= cos.1 by A2,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 FUNCT_2:15
.= (Partial_Sums(1 P_cos)).(2*0+1) by Lm6
.=(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 Def21
.= (-1)|^ 0 * (1)|^ (2*0)/((2*0)!)+
(-1)|^ 1 * (1)|^ (2*1)/((2*1)!) by Def21
.=1* (1)|^ (2*0)/((2*0)!)+
(-1)|^ 1 * (1)|^ (2*1)/((2*1)!) by Lm7
.=1/1 + (-1)|^ 1 * (1)|^ (2*1)/((2*1)!) by NEWTON:12
.=1+ (-1)* (1)|^ (2*1)/((2*1)!)
.=1+ (-1)*1/((2*1)!)
.=1+(-1)/(1! * (1+1)) by NEWTON:15
.=1+(-1)/(0! * (0+1) *2) by NEWTON:15
.=1/2 by NEWTON:12;
then A4: X[0];
A5: for k st X[k] holds X[k+1]
proof
let k;
A6: k in NAT by ORDINAL1:def 12;
assume
A7: ((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 FUNCT_2:15
.=(Partial_Sums(1 P_cos)).(2*(k+1)+1) by Lm6
.=(Partial_Sums(1 P_cos)).(2*k+1+1)+(1 P_cos).(2*(k+1)+1) by
SERIES_1:def 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 Lm6
.=((Partial_Sums(1 P_cos))*bq).k+ (1 P_cos).(2*k+1+1)+
(1 P_cos).(2*(k+1)+1) by FUNCT_2:15,A6;
then
A8: ( (Partial_Sums(1 P_cos))*bq).(k+1)-((Partial_Sums(1 P_cos))*bq).k
=(1 P_cos).(2*k+1+1)+ (1 P_cos).(2*(k+1)+1);
A9: (1 P_cos).(2*k+1+1)=(-1)|^ (2*(k+1)) * (1)|^ (2*(2*(k+1)))/((2*(2*
(k+1)))!) by Def21
.= 1 * 1|^ (2*(2*(k+1)))/((2*(2*(k+1)))!) by Lm7
.=1/((2*(2*(k+1)))!);
A10: (1 P_cos).(2*(k+1)+1)
= (-1)|^ (2*(k+1)+1) * (1)|^ (2*(2*(k+1)+1))/((2*(2*(k+1)+1))!)
by Def21
.=(-1) * (1)|^ (2*(2*(k+1)+1))/((2*(2*(k+1)+1))!) by Lm7
.=(-1) * 1/((2*(2*(k+1)+1))!)
.=(-1)/((2*(2*(k+1)+1))!);
2*(2*(k+1))<2*(2*(k+1)+1) by XREAL_1:29,68;
then (2*(2*(k+1)))! <= (2*(2*(k+1)+1))! by Th38;
then 1/((2*(2*(k+1)))!) >= 1/((2*(2*(k+1)+1))!) by XREAL_1:85;
then 1/((2*(2*(k+1)))!)-1/(2*(2*(k+1)+1)!)>=0 by XREAL_1:48;
then ((Partial_Sums(1 P_cos))*bq).(k+1)>=((Partial_Sums(1 P_cos))*bq).
k by A8,A9,A10,XREAL_1:49;
hence thesis by A7,XXREAL_0:2;
end;
for n holds X[n] from NAT_1:sch 2(A4,A5);
hence thesis;
end;
then A11: cos.1>=1/2 by A1,A3,PREPOWER:1,SEQ_4:16;
A12: Partial_Sums(1 P_sin) is convergent by Th35;
A13: sin.1=Sum(1 P_sin) by Th36;
lim ((Partial_Sums(1 P_sin))*bq )=lim(Partial_Sums(1 P_sin)) by A12,SEQ_4:17;
then A14: lim ((Partial_Sums(1 P_sin))*bq )= sin.1 by A13,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 FUNCT_2:15
.= (Partial_Sums(1 P_sin)).(2*0+1) by Lm6
.=(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 Def20
.= (-1)|^ 0 * (1)|^ (2*0+1)/((2*0+1)!)+
(-1)|^ 1 * (1)|^ (2*1+1)/((2*1+1)!) by Def20
.=1* (1)|^ (2*0+1)/((2*0+1)!)+
(-1)|^ 1 * (1)|^ (2*1+1)/((2*1+1)!) by Lm7
.=1/((0+1)!)+(-1)|^ 1 * (1)|^ (2*1+1)/((2*1+1)!)
.=1/(0!*1)+(-1)|^ 1 * (1)|^ (2*1+1)/((2*1+1)!) by NEWTON:15
.=1+ (-1)* (1)|^ (2*1+1)/((2*1+1)!) by NEWTON:12
.=1+ (-1)*1/((2*1+1)!)
.=1+ (-1)/((2*1)!*(2*1+1)) by NEWTON:15
.=1+(-1)/(1! * (1+1)*3) by NEWTON:15
.=1+(-1)/((0+1)! *(2*3))
.=1+(-1)/(1* 1 *6) by NEWTON:12,15
.=5/6;
then A15: X[0];
A16: for k st X[k] holds X[k+1]
proof
let k;
A17: k in NAT by ORDINAL1:def 12;
assume
A18: ((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 FUNCT_2:15
.=(Partial_Sums(1 P_sin)).(2*(k+1)+1) by Lm6
.=(Partial_Sums(1 P_sin)).(2*k+1+1)+(1 P_sin).(2*(k+1)+1) by
SERIES_1:def 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 Lm6
.=((Partial_Sums(1 P_sin))*bq).k+ (1 P_sin).(2*k+1+1)+
(1 P_sin).(2*(k+1)+1) by FUNCT_2:15,A17;
then
A19: ( (Partial_Sums(1 P_sin))*bq).(k+1)-((Partial_Sums(1 P_sin))*bq).k
=(1 P_sin).(2*k+1+1)+ (1 P_sin).(2*(k+1)+1);
A20: (1 P_sin).(2*k+1+1)=(-1)|^ (2*(k+1)) * (1)|^ (2*(2*(k+1))+1)/((2*
(2*(k+1))+1)!) by Def20
.=(1)* (1)|^ (2*(2*(k+1))+1)/((2*(2*(k+1))+1)!) by Lm7
.=1/((2*(2*(k+1))+1)!);
A21: (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 Def20
.=(-1) * (1)|^ (2*(2*(k+1)+1)+1)/((2*(2*(k+1)+1)+1)!) by Lm7
.=(-1) * 1/((2*(2*(k+1)+1)+1)!)
.=(-1)/((2*(2*(k+1)+1)+1)!);
2*(2*(k+1))<2*(2*(k+1)+1) by XREAL_1:29,68;
then 2*(2*(k+1))+1<2*(2*(k+1)+1) +1 by XREAL_1:6;
then (2*(2*(k+1))+1)! <= (2*(2*(k+1)+1)+1)! by Th38;
then 1/((2*(2*(k+1))+1)!) >= 1/((2*(2*(k+1)+1)+1)!) by XREAL_1:85;
then 1/((2*(2*(k+1))+1)!)-1/((2*(2*(k+1)+1)+1)!)>=0 by XREAL_1:48;
then ((Partial_Sums(1 P_sin))*bq).(k+1)>=((Partial_Sums(1 P_sin))*bq)
.k by A19,A20,A21,XREAL_1:49;
hence thesis by A18,XXREAL_0:2;
end;
for n holds X[n] from NAT_1:sch 2(A15,A16);
hence thesis;
end;
then A22: sin.1>=5/6 by A12,A14,PREPOWER:1,SEQ_4:16;
A23: (cos.(1))^2+(sin.(1))^2=1 by Th28;
A24: (sin.(1))^2>=(5/6)^2 by A22,SQUARE_1:15;
then 1-(1-(cos.(1))^2)<=1-25/36 by A23,XREAL_1:10;
then (cos.(1))^2<25/36 by XXREAL_0:2;
then (sin.(1))^2> (cos.(1))^2 by A24,XXREAL_0:2;
then A25: sqrt(cos.(1))^2<sqrt(sin.(1))^2 by SQUARE_1:27,XREAL_1:63;
sqrt(cos.(1))^2 = cos.1 by A11,SQUARE_1:22;
hence thesis by A11,A22,A25,SQUARE_1:22;
end;
theorem Th43:
for th holds th rExpSeq=Re(th ExpSeq)
proof
let th;
for n being Element of NAT holds (th rExpSeq).n=Re(th ExpSeq).n
proof
let n be Element of NAT;
Re(th ExpSeq).n= Re (th ExpSeq.n) by COMSEQ_3:def 5
.=Re(th |^ n /(n!+0*<i>)) by Def4
.=Re((th|^ n) /(n!)+0*<i>)
.=(th|^ n) /(n!) by COMPLEX1:12
.=(th rExpSeq).n by Def5;
hence thesis;
end;
hence thesis;
end;
theorem Th44:
for th holds th rExpSeq is summable &
Sum(th rExpSeq)=Re(Sum(th ExpSeq))
proof
let th;
Sum(th ExpSeq) =Sum(Re (th ExpSeq))+(Sum(Im (th ExpSeq)))*<i> & Sum(th
rExpSeq)=Sum(Re (th ExpSeq)) by Th43,COMSEQ_3:53;
hence thesis by Th43,COMPLEX1:12;
end;
Lm8: for z being Complex holds
z ExpSeq.1=z & z ExpSeq.0=1r & |.z |^ n.|=|.z.| |^n
proof
let z be Complex;
z|^1=z;
then A1: z ExpSeq.1= z/(1!) by Def4
.=z by NEWTON:13;
A2: z ExpSeq.0=z|^ 0/ (0!) by Def4
.=1r by Th1,COMSEQ_3:11;
|.z |^ n.|=|.z.| |^ n
proof
defpred X[Nat] means |.z |^ $1.|=|.z.| |^ $1;
|.z |^ 0 .|=1 by COMPLEX1:48,COMSEQ_3:def 1;
then A3: X[0] by NEWTON:4;
A4: for k st X[k] holds X[k+1]
proof
let k such that
A5: |.z |^ k.|=|.z.| |^ k;
|.z |^ (k+1).|=|.z*(z GeoSeq.k).| by COMSEQ_3:def 1
.=|.z.| |^ k *|.z.| by A5,COMPLEX1:65
.=|.z.| |^(k+1) by NEWTON:6;
hence thesis;
end;
for n holds X[n] from NAT_1:sch 2(A3,A4);
hence thesis;
end;
hence thesis by A1,A2;
end;
Lm9: for th holds Sum(th ExpSeq)=Sum(th rExpSeq)
proof
let th;
A1: for n being Nat holds Im(Partial_Sums(th ExpSeq)).n=In(0,REAL)
proof
defpred X[Nat] means Im(Partial_Sums(th ExpSeq)).$1=0;
Im(Partial_Sums(th ExpSeq)).0
=Im(Partial_Sums(th ExpSeq).0) by COMSEQ_3:def 6
.=Im((th ExpSeq).0) by SERIES_1:def 1
.=0 by Lm8,COMPLEX1:6;
then A2: X[0];
A3: for n being Nat st X[n] holds X[n+1]
proof
let n being Nat such that
A4: Im(Partial_Sums(th ExpSeq)).n=0;
Im(Partial_Sums(th ExpSeq)).(n+1)
=Im(Partial_Sums(th ExpSeq).(n+1)) by COMSEQ_3:def 6
.=Im(Partial_Sums(th ExpSeq).n+(th ExpSeq).(n+1))
by SERIES_1:def 1
.=Im(Partial_Sums(th ExpSeq).n)+Im((th ExpSeq).(n+1))
by COMPLEX1:8
.=0+Im((th ExpSeq).(n+1)) by A4,COMSEQ_3:def 6
.=Im((th|^ (n+1)) /((n+1)!)+0*<i>) by Def4
.=0 by COMPLEX1:12;
hence thesis;
end;
for n being Nat holds X[n] from NAT_1:sch 2(A2,A3);
hence thesis;
end;
then Im(Partial_Sums(th ExpSeq)) is constant by VALUED_0:def 18;
then lim(Im(Partial_Sums(th ExpSeq)))
=Im(Partial_Sums(th ExpSeq)).0 by SEQ_4:26
.=0 by A1;
then Im(Sum(th ExpSeq)) =0 by COMSEQ_3:41;
then Sum(th ExpSeq) =Re(Sum(th ExpSeq))+0*<i> by COMPLEX1:13
.=Sum(th rExpSeq) by Th44;
hence thesis;
end;
theorem Th45:
for p,q being Real holds
Sum((p+q) rExpSeq) = (Sum(p rExpSeq))*(Sum(q rExpSeq))
proof
let p,q be Real;
reconsider p,q as Real;
Sum((p+q) rExpSeq)=Re(Sum((p+q) ExpSeq)) by Th44
.=Re((Sum(p ExpSeq)) *(Sum(q ExpSeq))) by Lm2
.=Re((Re(Sum(p ExpSeq))+Im(Sum(p ExpSeq))*<i>)*(Sum(q ExpSeq)))
by COMPLEX1:13
.= Re((Re(Sum(p ExpSeq))+Im(Sum(p ExpSeq))*<i>)*
(Re(Sum(q ExpSeq))+Im(Sum(q ExpSeq))*<i>)) by COMPLEX1:13
.= Re((Sum(p rExpSeq)+Im(Sum(p ExpSeq))*<i>)*
(Re(Sum(q ExpSeq))+Im(Sum(q ExpSeq))*<i>)) by Th44
.= Re((Sum(p rExpSeq)+0*<i>)*
(Re(Sum(q ExpSeq))+Im(Sum(q ExpSeq))*<i>)) by Th41
.= Re(Sum(p rExpSeq)*(Sum(q rExpSeq)+Im(Sum(q ExpSeq))*<i>)) by Th44
.= Re(Sum(p rExpSeq)*(Sum(q rExpSeq)+0*<i>)) by Th41
.= Re((Sum(p rExpSeq))*(Sum(q rExpSeq))+0*<i>)
.= (Sum(p rExpSeq))*(Sum(q rExpSeq)) by COMPLEX1:12;
hence thesis;
end;
definition
func exp_R -> Function of REAL, REAL means
:Def22:
for d being Real holds it.d = Sum(d rExpSeq);
existence
proof
deffunc U(Real) = In(Sum($1 rExpSeq),REAL);
consider f being Function of REAL, REAL such that
A1: for d be Element of REAL holds f.d = U(d) from FUNCT_2:sch 4;
take f;
let d be Real;
d in REAL by XREAL_0:def 1;
then f.d = U(d) by A1;
hence thesis;
end;
uniqueness
proof
let f1,f2 be Function of REAL, REAL;
assume
A2: for d being Real holds f1.d=Sum(d rExpSeq);
assume
A3: for d being Real holds f2.d=Sum(d rExpSeq);
for d being Element of REAL holds f1.d = f2.d
proof
let d be Element of REAL;
thus f1.d=Sum(d rExpSeq) by A2
.=f2.d by A3;
end;
hence f1=f2;
end;
end;
definition
let th be Real;
func exp_R th -> number equals
exp_R.th;
coherence;
end;
registration
let th be Real;
cluster exp_R th -> real;
coherence;
end;
theorem Th46:
dom(exp_R)=REAL by FUNCT_2:def 1;
theorem Th47:
for th holds exp_R.th = Re(Sum(th ExpSeq))
proof
let th;
exp_R.th = Sum(th rExpSeq) by Def22;
hence thesis by Th44;
end;
theorem
for th holds exp th=exp_R th
proof
let th;
thus exp th=Sum(th ExpSeq) by Def14
.=Sum(th rExpSeq) by Lm9
.=exp_R th by Def22;
end;
Lm10: for p,q being Real holds exp_R.(p+q) = exp_R.p * exp_R.q
proof
let p,q be Real;
exp_R.(p+q) = Sum((p+q) rExpSeq) by Def22
.= (Sum(p rExpSeq))*(Sum(q rExpSeq)) by Th45
.=exp_R.p *(Sum(q rExpSeq)) by Def22
.=exp_R.p * exp_R.q by Def22;
hence thesis;
end;
theorem
for p,q being Real holds exp_R(p+q) = exp_R(p) * exp_R(q) by Lm10;
Lm11: exp_R.0 =1
proof
exp_R.0 = Sum(0 rExpSeq) by Def22
.=1 by Th9,Th44,COMPLEX1:6;
hence thesis;
end;
theorem
exp_R(0) =1 by Lm11;
theorem Th51:
th > 0 implies exp_R.th >=1
proof
assume
A1: th >0;
A2: for n holds Partial_Sums(th rExpSeq).n>=1
proof
defpred X[Nat] means Partial_Sums(th rExpSeq).$1>=1;
Partial_Sums(th rExpSeq).0=(th rExpSeq).0 by SERIES_1:def 1
.=th |^ 0 /(0!) by Def5
.=1 by NEWTON:4,12;
then A3: X[0];
A4: for n st X[n] holds X[n+1]
proof
let n;
assume
A5: Partial_Sums(th rExpSeq).n>=1;
A6: Partial_Sums(th rExpSeq).(n+1)
=Partial_Sums(th rExpSeq).n+(th rExpSeq).(n+1) by SERIES_1:def 1
.=Partial_Sums(th rExpSeq).n+th |^(n+1)/((n+1)!) by Def5;
th |^(n+1) >0 & (n+1)!>0 by A1,PREPOWER:6;
then Partial_Sums(th rExpSeq).n+th |^(n+1)/((n+1)!)>Partial_Sums(th
rExpSeq).n by XREAL_1:29;
hence thesis by A5,A6,XXREAL_0:2;
end;
for n holds X[n] from NAT_1:sch 2(A3,A4);
hence thesis;
end;
th rExpSeq is summable by Th44;
then A7: Partial_Sums(th rExpSeq) is convergent by SERIES_1:def 2;
lim(Partial_Sums(th rExpSeq))=Sum(th rExpSeq) by SERIES_1:def 3;
then Sum(th rExpSeq)>=1 by A2,A7,PREPOWER:1;
hence thesis by Def22;
end;
theorem Th52:
th < 0 implies 0<exp_R.th & exp_R.th <=1
proof
assume th <0;
then A1: exp_R.(-th)>=1 by Th51;
A2: exp_R.(-th)*exp_R.th=exp_R.(-th+th) by Lm10
.=1 by Lm11;
then A3: exp_R.th=1/(exp_R.(-th)) by XCMPLX_1:73;
thus 0<exp_R.th by A1,A2;
thus thesis by A1,A3,XREAL_1:211;
end;
theorem Th53:
exp_R.th>0
proof
now per cases;
suppose
th=0;
hence thesis by Lm11;
end;
suppose
A1: th<>0;
now per cases by A1;
suppose
th<0;
hence thesis by Th52;
end;
suppose
th>0;
hence thesis by Th51;
end;
end;
hence thesis;
end;
end;
hence thesis;
end;
theorem
exp_R(th)>0 by Th53;
begin :: Differential of sin, cos, and Exponential Function
definition
let z be Complex;
deffunc U(Nat) = (z|^($1+1))/(($1+2)!);
func z P_dt -> Complex_Sequence means
:Def24:
for n holds it.n = (z|^(n+1))/((n+2)!);
existence
proof
thus ex s being Complex_Sequence st
for n holds s.n = U(n) from COMSEQ_1:sch 1;
end;
uniqueness
proof let s1,s2 be Complex_Sequence such that
A1: for x being Nat holds s1.x = U(x) and
A2: for x being Nat holds s2.x = U(x);
let x be Element of NAT;
thus s1.x = U(x) by A1 .= s2.x by A2;
end;
deffunc U(Nat) = (z|^($1))/(($1+2)!);
func z P_t -> Complex_Sequence means
for n holds it.n = (z|^(n))/((n+2)!);
existence
proof
thus ex s being Complex_Sequence st
for n holds s.n = U(n) from COMSEQ_1:sch 1;
end;
uniqueness
proof let s1,s2 be Complex_Sequence such that
A3: for x being Nat holds s1.x = U(x) and
A4: for x being Nat holds s2.x = U(x);
let x be Element of NAT;
thus s1.x = U(x) by A3 .= s2.x by A4;
end;
end;
Lm12: for p being Real, z being Complex
holds Re(p*<i>*z)=-p*Im z & Im(p*<i>*z)=p*Re z
&Re(p*z)=p*Re z & Im(p*z)=p*Im z
proof
let p being Real, z be Complex;
A1: (p*<i>*z) =p*<i>*(Re z+Im z*<i>) by COMPLEX1:13
.=-p* Im z+(p*Re z)*<i>;
(p*z) =(p*(Re z+Im z*<i>)) by COMPLEX1:13
.=p* Re z+(p*Im z)*<i>;
hence thesis by A1,COMPLEX1:12;
end;
Lm13: for p being Real, z being Complex
st p>0 holds Re(z/(p*<i>))=Im z /p & Im(z/(p*<i>))=-Re z /p
&|.z/p.|=|.z.|/p
proof
let p be Real, z being Complex such that
A1: p>0;
A2: Re(0+p*<i>)=0 & Im(0+p*<i>)=p by COMPLEX1:12;
A3: Im(p+0*<i>)=0 by COMPLEX1:12;
A4: z/(p*<i>) = (Re z * 0 + Im z * p) / (0^2 + p^2) +
(0 * Im z - Re z * p) / (0^2 + p^2)*<i>
by A2,COMPLEX1:86
.=(Im z * p)/(p*p)+ ((-Re z) * p)/(p*p)*<i>
.=(Im z * p)/(p*p)+(-Re z) /p *<i> by A1,XCMPLX_1:91
.=Im z /p+(-Re z /p)*<i> by A1,XCMPLX_1:91;
|.z/p.|=|.z.|/|.p.| by COMPLEX1:67
.=|.z.|/sqrt((p)^2) by A3,COMPLEX1:12;
hence thesis by A1,A4,COMPLEX1:12,SQUARE_1:22;
end;
theorem Th55:
for z being Complex holds z P_dt is absolutely_summable
proof
let z be Complex;
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 VALUED_1:18
.=|.(z|^(0+1))/((0+2)!).| by Def24
.=|.z/2.| by NEWTON:14;
then A2: Partial_Sums(|.z P_dt.|).0=|.z.|/2 by Lm13;
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 VALUED_1:18
.=|.z ExpSeq.0 .|+|.z ExpSeq.1 .| by VALUED_1:18
.=|.z ExpSeq.0 .|+|.z .| by Lm8
.=1+|.z .| by Lm8,COMPLEX1:48;
then A3: Partial_Sums(|.z ExpSeq.|).(0+1)-Partial_Sums(|.z P_dt.|). 0
=1+(|.z .| - |.z.|/2) by A2;
defpred X[Nat] means
Partial_Sums(|.z P_dt.|).$1 <Partial_Sums(|.z ExpSeq.|).($1+1);
0 <= |.z.| by COMPLEX1:46;
then A4: X[0] by A3,XREAL_1:47;
A5: for n st X[n] holds X[n+1]
proof
let n such that
A6: Partial_Sums(|.z P_dt.|).n <Partial_Sums(|.z ExpSeq.|).(n+1);
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 VALUED_1:18
.=Partial_Sums(|.z P_dt.|).n+|.(z|^((n+1)+1))/(((n+1)+2)!).| by Def24
.=Partial_Sums(|.z P_dt.|).n+|.(z|^(n+2))/((n+3)!).|;
then A7: Partial_Sums(|.z P_dt.|).(n+1)
=Partial_Sums(|.z P_dt.|).n+|.(z|^(n+2)).|/((n+3)!) by Lm13;
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+2).| by VALUED_1:18
.=Partial_Sums(|.z ExpSeq.|).(n+1)+|.(z|^(n+2))/((n+2)!).| by Def4
.=Partial_Sums(|.z ExpSeq.|).(n+1)+|.(z|^(n+2))/((n+2)!).|;
then A8: Partial_Sums(|.z ExpSeq.|).((n+1)+1)
=Partial_Sums(|.z ExpSeq.|).(n+1)+|.(z|^(n+2)).|/((n+2)!)
by Lm13;
(n+2)<(n+3) by XREAL_1:6;
then A9: (n+2)!<=(n+3)! by Th38;
|.(z|^(n+2)).|>=0 by COMPLEX1:46;
then |.(z|^(n+2)).|/((n+2)!)>=|.(z|^(n+2)).|/((n+3)!) by A9,XREAL_1:118;
then A10: Partial_Sums(|.z P_dt.|).n+|.(z|^(n+2)).|/((n+3)!)<=
Partial_Sums(|.z P_dt.|).n+|.(z|^(n+2)).|/((n+2)!) by XREAL_1:6;
Partial_Sums(|.z P_dt.|).n+|.(z|^(n+2)).|/((n+2)!)<
Partial_Sums(|.z ExpSeq.|).(n+1)+|.(z|^(n+2)).|/((n+2)!)
by A6,XREAL_1:6;
hence thesis by A7,A8,A10,XXREAL_0:2;
end;
for n holds X[n] from NAT_1:sch 2(A4,A5);
hence thesis;
end;
consider r be Real such that
A11: for n holds Partial_Sums(|.z ExpSeq.|).n<r by SEQ_2:def 3;
A12: for n holds Partial_Sums(|.z P_dt.|).n<r
proof
let n;
Partial_Sums(|.z P_dt.|).n<Partial_Sums(|.z ExpSeq.|). (n+1) by A1;
hence thesis by A11,XXREAL_0:2;
end;
take r;
thus thesis by A12;
end;
then Partial_Sums(|.z P_dt.|) is bounded_above by SEQ_2:def 3;
hence thesis by COMSEQ_3:61;
end;
theorem Th56:
for z being Complex holds z*(Sum(z P_dt))=(Sum(z ExpSeq))-1r-z
proof
let z be Complex;
A1: for z being Complex holds z (#) (z P_dt)=(z ExpSeq)^\ 2
proof
let z be Complex;
for n being Element of NAT holds (z(#)(z P_dt)).n=((z ExpSeq)^\ 2).n
proof
let n be Element of NAT;
(z(#)(z P_dt)).n=z*(z P_dt).(n) by VALUED_1:6
.=z*((z|^(n+1))/((n+2)!)) by Def24;
then (z(#)(z P_dt)).n= (z*(z|^(n+1)))/((n+2)!)
.=(z|^(n+1+1))/((n+2)!) by NEWTON:6
.=z ExpSeq.(n+2) by Def4
.=((z ExpSeq)^\ 2).n by NAT_1:def 3;
hence thesis;
end;
hence thesis;
end;
Sum
(z ExpSeq)= Partial_Sums(z ExpSeq).1 + Sum(z ExpSeq^\(1+1)) by COMSEQ_3:60
.=Partial_Sums(z ExpSeq).1 + Sum(z ExpSeq^\(2));
then
A2: Sum(z (#) (z P_dt))=Sum(z ExpSeq) - Partial_Sums(z ExpSeq).(0+1) by A1
.=Sum(z ExpSeq)-(Partial_Sums(z ExpSeq).0+z ExpSeq.1) by SERIES_1:def 1
.=Sum(z ExpSeq)-(z ExpSeq.0+z ExpSeq.1) by SERIES_1:def 1
.=Sum(z ExpSeq)-(1r+z ExpSeq.1) by Lm8
.=Sum(z ExpSeq)-(1r+z) by Lm8
.=(Sum(z ExpSeq))-1r-z;
reconsider BBB=z P_dt as absolutely_summable Complex_Sequence by Th55;
BBB is summable;
hence thesis by A2,COMSEQ_3:56;
end;
theorem Th57:
for p st p>0 holds ex q st q>0 &
for z being Complex 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 VALUED_1:18;
hence thesis by COMSEQ_3:30;
end;
A3: z P_dt is absolutely_summable by Th55;
A4: z P_dt is summable by Th55,COMSEQ_3:63;
A5: lim|.Partial_Sums(z P_dt).|=|.lim(Partial_Sums(z P_dt)).|
by A4,SEQ_2:27;
lim|.Partial_Sums(z P_dt).|<=lim(Partial_Sums(|.z P_dt.|)) by A2,A3,SEQ_2:18;
hence thesis by A5,SERIES_1:def 3;
end;
A6: for z,n holds |.z P_dt.|.n<=|.z.|*|.z.| GeoSeq.n
proof
let z,n;
|.z P_dt.|.n=|.z P_dt.n.| by VALUED_1:18
.=|.(z|^(n+1))/((n+2)!).| by Def24
.=|.(z|^(n+1))/((n+2)!).|;
then A7: |.z P_dt.|.n=|.(z|^(n+1)).|/((n+2)!) by Lm13
.=|.z.| |^(n+1)/((n+2)!) by Lm8;
A8: |.z.|*|.z.| GeoSeq.n=|.z.|* (|.z.| |^ n) by PREPOWER:def 1
.=|.z.| |^(n+1) by NEWTON:6;
(n+2)!>=1 & |.z.| |^(n+1) >=0 by Th38,COMPLEX1:46,NEWTON:12,POWER:3;
then |.z.| |^(n+1)/1>=|.z.| |^(n+1)/((n+2)!) by XREAL_1:118;
hence thesis by A7,A8;
end;
let p0 be Real;
assume
A9: p0>0;
reconsider p = p0 as Real;
consider q such that
A10: q=p/(p+1);
p+1>p by XREAL_1:29;
then A11: q <1 by A9,A10,XREAL_1:189;
A12: for z st |.z.|<q holds |.(Sum(z P_dt)).|<p
proof
let z;
assume
A13: |.z.|<q;
then A14: |.z.|<1 by A11,XXREAL_0:2;
A15: |.|.z.|.|<1 by A11,A13,XXREAL_0:2;
then A16: |.z.| GeoSeq is summable by SERIES_1:24;
A17: Sum(|.z.| GeoSeq) = 1/(1- |.z.|) by A15,SERIES_1:24;
A18: |.z.|(#)|.z.| GeoSeq is summable by A16,SERIES_1:10;
A19: for n holds |.z P_dt.|.n<=(|.z.|(#)|.z.| GeoSeq).n
proof
let n;
|.z P_dt.|.n<=|.z.|*|.z.| GeoSeq.n by A6;
hence thesis by SEQ_1:9;
end;
for n holds 0<=|.z P_dt.|.n
proof
let n;
|.z P_dt.|.n=|.z P_dt.n.| by VALUED_1:18;
hence thesis by COMPLEX1:46;
end;
then
A20: Sum(|.z P_dt.|)<=Sum(|.z.|(#)|.z.| GeoSeq) by A18,A19,SERIES_1:20;
A21: Sum(|.z.|(#)|.z.| GeoSeq) =|.z.|/(1- |.z.|) by A16,A17,SERIES_1:10;
A22: |.z.|*(p+1)<(p/(p+1))*(p+1) by A9,A10,A13,XREAL_1:68;
(p/(p+1))*(p+1)=p by A9,XCMPLX_1:87;
then A23: p*|.z.|+|.z.|-p*|.z.|<p-p*|.z.| by A22,XREAL_1:9;
A24: 1- |.z.|>0 by A14,XREAL_1:50;
then |.z.|/(1- |.z.|)< p*(1- |.z.|)/(1- |.z.|) by A23,XREAL_1:74;
then |.z.|/(1- |.z.|)<p by A24,XCMPLX_1:89;
then A25: Sum(|.z P_dt.|)<p by A20,A21,XXREAL_0:2;
|.(Sum(z P_dt)).|<=Sum (|.z P_dt.|) by A1;
hence thesis by A25,XXREAL_0:2;
end;
take q;
thus q>0 by A9,A10;
let z being Complex;
thus thesis by A12;
end;
theorem Th58:
for z,z1 being Complex holds (Sum((z1+z) ExpSeq))-(Sum(z1 ExpSeq))
=(Sum(z1 ExpSeq))*z+z*(Sum(z P_dt))*(Sum(z1 ExpSeq))
proof
let z,z1 be Complex;
(Sum((z1+z) ExpSeq))-(Sum(z1 ExpSeq))
=(Sum(z1 ExpSeq))*(Sum(z ExpSeq))-(Sum(z1 ExpSeq))*1r by Lm2
.=(Sum(z1 ExpSeq))*(((Sum(z ExpSeq))-1r)-z+z)
.=(Sum(z1 ExpSeq))* (z*(Sum(z P_dt))+z) by Th56
.=(Sum(z1 ExpSeq))*z +z*(Sum(z P_dt))*(Sum(z1 ExpSeq));
hence thesis;
end;
theorem Th59:
for p,q being Real holds cos.(p+q)-cos.p=
-q*sin.p -q*Im((Sum(q*<i> P_dt))* (cos.p+(sin.p)*<i>))
proof
let p,q be Real;
cos.(p+q)-cos.p=cos.(p+q)-Re(Sum(p*<i> ExpSeq)) by Def18
.=Re(Sum((p+q)*<i> ExpSeq))-Re(Sum(p*<i> ExpSeq)) by Def18
.=Re(Sum((p*<i>+q*<i>) ExpSeq)-Sum(p*<i> ExpSeq)) by COMPLEX1:19
.=Re((Sum(p*<i> ExpSeq))*(q*<i>)+q*<i>*(Sum((q*<i>) P_dt))*
(Sum(p*<i> ExpSeq)))
by Th58
.=Re((cos.p+(sin.p)*<i>)*(q*<i>)
+q*<i>*(Sum(q*<i> P_dt))*(Sum(p*<i> ExpSeq))) by Lm3
.= Re((cos.p+(sin.p)*<i>)*(q*<i>)
+q*<i>*(Sum(q*<i> P_dt))* (cos.p+(sin.p)*<i>)) by Lm3
.=Re(-q*sin.p+q*cos.p*<i>)+Re(q*<i>*(Sum(q*<i> P_dt))*
(cos.p+(sin.p)*<i>)) by COMPLEX1:8
.=-q*sin.p+ Re(q*<i>*((Sum(q*<i> P_dt))* (cos.p+(sin.p)*<i>)))
by COMPLEX1:12
.=-q*sin.p -q*Im((Sum(q*<i> P_dt))* (cos.p+(sin.p)*<i>)) by Lm12;
hence thesis;
end;
theorem Th60:
for p,q being Real holds sin.(p+q)-sin.p=
q*cos.p+q*Re((Sum((q*<i>) P_dt))* (cos.p+sin.p*<i>))
proof
let p,q be Real;
sin.(p+q)-sin.p=sin.(p+q)-Im(Sum((p*<i>) ExpSeq)) by Def16
.=Im(Sum(((p+q)*<i>) ExpSeq))-Im(Sum((p*<i>) ExpSeq)) by Def16
.=Im(Sum(((p*<i>)+(q*<i>)) ExpSeq)-Sum((p*<i>) ExpSeq)) by COMPLEX1:19
.=Im((Sum((p*<i>) ExpSeq))*(q*<i>)
+(q*<i>)*(Sum((q*<i>) P_dt))*(Sum((p*<i>) ExpSeq))) by Th58
.=Im((cos.p+(sin.p)*<i>)*(q*<i>)
+(q*<i>)*(Sum((q*<i>) P_dt))*(Sum((p*<i>) ExpSeq))) by Lm3
.= Im((cos.p+sin.p*<i>)*(q*<i>)
+(q*<i>)*(Sum((q*<i>) P_dt))* (cos.p+(sin.p)*<i>)) by Lm3
.=Im(-q*sin.p+(q*cos.p)*<i>)+Im((q*<i>)*(Sum((q*<i>) P_dt))
* (cos.p+sin.p*<i>)) by COMPLEX1:8
.=q*cos.p+Im((q*<i>)*((Sum((q*<i>) P_dt))* (cos.p+sin.p*<i>)))
by COMPLEX1:12
.=q*cos.p+q*Re((Sum((q*<i>) P_dt))* (cos.p+sin.p*<i>)) by Lm12;
hence thesis;
end;
theorem Th61:
for p,q being Real holds exp_R.(p+q)-exp_R.p=
q * (exp_R.p)+q*exp_R.p*Re((Sum(q P_dt)))
proof
let p,q be Real;
exp_R.(p+q)-exp_R.p=exp_R.(p+q)-Re(Sum(p ExpSeq)) by Th47
.=Re(Sum((p+q) ExpSeq))-Re(Sum(p ExpSeq)) by Th47
.=Re(Sum((p+q) ExpSeq)-Sum(p ExpSeq)) by COMPLEX1:19
.=Re((Sum(p ExpSeq))*q
+q*(Sum(q P_dt))*(Sum(p ExpSeq))) by Th58
.=Re((Sum(p ExpSeq))*q)+
Re(q*(Sum(q P_dt))*(Sum(p ExpSeq))) by COMPLEX1:8
.=q*Re(Sum(p ExpSeq))+
Re(q*(Sum(q P_dt))*(Sum(p ExpSeq))) by Lm12
.=q* (exp_R.p)+ Re(q*((Sum(q P_dt))*(Sum(p ExpSeq))))
by Th47
.=q* (exp_R.p)+ q*Re((Sum(q P_dt))*(Sum(p ExpSeq))) by Lm12
.=q* (exp_R.p)+ q*Re((Sum(q P_dt))*Sum(p rExpSeq)) by Lm9
.=q* (exp_R.p)+q*Re((Sum(q P_dt))*(exp_R.p+0*<i>)) by Def22
.=q* (exp_R.p)+q*(exp_R.p*Re((Sum(q P_dt)))) by Lm12
.=q* (exp_R.p)+q*exp_R.p*Re((Sum(q P_dt)));
hence thesis;
end;
theorem Th62:
cos is_differentiable_in p & diff(cos,p)=-sin.p
proof
reconsider p as Element of REAL by XREAL_0:def 1;
deffunc U(Real) =
In(- $1* Im((Sum($1*<i> P_dt))* (cos.p+sin.p*<i>)),REAL);
consider Cr being Function of REAL, REAL such that
A1: for th be Element of REAL holds Cr.th = U(th) from FUNCT_2:sch 4;
for hy1 holds
(hy1")(#)(Cr/*hy1) is convergent & lim ((hy1")(#)(Cr/*hy1)) = 0
proof
let hy1;
A2: for n holds ((hy1")(#)(Cr/*hy1)).n
=-Im((Sum((hy1.n)*<i> P_dt))* (cos.p+sin.p*<i>))
proof
let n;
A3: n in NAT by ORDINAL1:def 12;
A4: ((hy1")(#)(Cr/*hy1)).n=(hy1".n)*((Cr/*hy1).n) by SEQ_1:8
.=(hy1.n)"*((Cr/*hy1).n) by VALUED_1:10;
dom Cr = REAL by FUNCT_2:def 1;
then rng hy1 c= dom Cr;
then A5: ((hy1")(#)(Cr/*hy1)).n
= (hy1.n)"*(Cr.(hy1.n)) by A4,FUNCT_2:108,A3
.= (hy1.n)"*U(hy1.n) by A1
.=-(hy1.n)"*(hy1.n)* Im((Sum((hy1.n)*<i> P_dt))*(cos.p+sin.p*<i>));
hy1.n<>0 by SEQ_1:5;
then
((hy1")(#)(Cr/*hy1)).n =-1*Im((Sum((hy1.n)*<i> P_dt))* (cos.p+sin.p*<i>))
by A5,XCMPLX_0:def 7
.=-Im((Sum((hy1.n)*<i> P_dt))* (cos.p+sin.p*<i>));
hence thesis;
end;
deffunc U(Real) = -Im((Sum((hy1.$1)*<i> P_dt))*(cos.p+(sin.p)*<i>));
consider rseq such that
A6: for n holds rseq.n= U(n) from SEQ_1:sch 1;
deffunc U(Nat) =
(Sum((hy1.$1)*<i> P_dt))*(cos.p+(sin.p)*<i>);
consider cq1 such that
A7: for n holds cq1.n=U(n) from COMSEQ_1:sch 1;
A8: 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
A9: q>0;
ex k st for m st k<=m holds |.cq1.m-0c.|<q
proof
consider r such that
A10: r>0 and
A11: for z being Complex st |.z.|<r holds |.(Sum (z P_dt)).|<q
by A9,Th57;
hy1 is convergent & lim(hy1)=0;
then consider k such that
A12: for m st k<=m holds |.hy1.m-0.|<r by A10,SEQ_2:def 7;
A13: now
let m such that
A14: k<=m;
A15: |.cq1.m-0c.|= |.(Sum((hy1.m)*<i> P_dt))* (cos.p+(sin.p)*<i>)
.| by A7
.= |.(Sum((hy1.m)*<i> P_dt)).|* |.cos.p+(sin.p)*<i>.| by COMPLEX1:65
.= |.(Sum((hy1.m)*<i> P_dt)).|* |.Sum(p*<i> ExpSeq ).| by Lm3
.=|.(Sum((hy1.m)*<i> P_dt)).|*1 by Lm5
.=|.(Sum((hy1.m)*<i> P_dt)).|;
A16: |.hy1.m-0.|<r by A12,A14;
(hy1.m)*<i> = 0+(hy1.m)*<i>;
then Re
((hy1.m)*<i>)=0 & Im((hy1.m)*<i>)=hy1.m by COMPLEX1:12;
then |.(hy1.m)*<i>.| =|.hy1.m.| by COMPLEX1:72;
hence |.cq1.m-0c.|<q by A11,A15,A16;
end;
take k;
thus thesis by A13;
end;
hence thesis;
end;
then A17: cq1 is convergent by COMSEQ_2:def 5;
then lim(cq1)=0c by A8,COMSEQ_2:def 6;
then A18: lim(-cq1)=-0c by A17,COMSEQ_2:22;
A19: for n being Element of NAT holds Im(-cq1).n= rseq.n
proof
A20: for n holds Im(-cq1).n=-Im((Sum((hy1.n)*<i> P_dt))* (cos.p+(sin.p)*<i>))
proof
let n;
Im(-cq1).n=Im((-cq1).n) by COMSEQ_3:def 6
.=Im(-cq1.n) by VALUED_1:8
.=Im(-(Sum((hy1.n)*<i> P_dt))* (cos.p+(sin.p)*<i>)) by A7
.=-Im((Sum((hy1.n)*<i> P_dt))* (cos.p+(sin.p)*<i>))
by COMPLEX1:17;
hence thesis;
end;
let n;
rseq.n=-Im((Sum((hy1.n)*<i> P_dt))* (cos.p+(sin.p)*<i>)) by A6;
hence thesis by A20;
end;
for n being Element of NAT holds rseq.n=((hy1")(#)(Cr/*hy1)).n
proof
let n be Element of NAT;
rseq.n=-Im((Sum((hy1.n)*<i> P_dt))* (cos.p+(sin.p)*<i>)) by A6;
hence thesis by A2;
end;
then rseq=(hy1")(#)(Cr/*hy1);
then (hy1")(#)(Cr/*hy1)=Im(-cq1) by A19;
hence thesis by A17,A18,COMPLEX1:4,COMSEQ_3:41;
end;
then reconsider PR = Cr as RestFunc by FDIFF_1:def 2;
deffunc U1(Real) = In(-$1*sin.p,REAL);
consider CL being Function of REAL, REAL such that
A21: for th be Element of REAL holds CL.th= U1(th) from FUNCT_2:sch 4;
ex r st
for q holds CL.q=r*q
proof
A22: for q holds CL.q=(-sin.p)*q
proof
let q;
reconsider qq=q as Element of REAL by XREAL_0:def 1;
CL.qq= U1(q) by A21
.=(-sin.p)*q;
hence thesis;
end;
take (-sin.p);
thus thesis by A22;
end;
then reconsider PL = CL as LinearFunc by FDIFF_1:def 3;
A23: 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
A24: for r st r in ].p-1,p+1 .[ holds cos.r - cos.p = PL.(r-p) + PR.(r-p)
proof
let r;
A25: r-p in REAL by XREAL_0:def 1;
r=p+(r-p);
then cos.r - cos.p
=-(r-p)*sin.p -(r-p)*Im((Sum((r-p)*<i> P_dt))* (cos.p+sin.p*<i>))
by Th59
.=-(r-p)*sin.p+U(r-p)
.=-(r-p)*sin.p+Cr.(r-p) by A1,A25
.=U1(r-p)+Cr.(r-p)
.=PL.(r-p) + PR.(r-p) by A21,A25;
hence thesis;
end;
take ].p-1,p+1 .[;
thus thesis by A24,Th24,RCOMP_1:def 6;
end;
then A26: cos is_differentiable_in p by FDIFF_1:def 4;
PL.jj= U1(1) by A21
.=-sin.p;
hence thesis by A23,A26,FDIFF_1:def 5;
end;
theorem Th63:
sin is_differentiable_in p & diff(sin,p)=cos.p
proof
reconsider p as Real;
deffunc U(Real)
= In($1 *Re((Sum($1*<i> P_dt))* (cos.p+(sin.p)*<i>)),REAL);
consider Cr being Function of REAL, REAL such that
A1: for th be Element of REAL holds Cr.th = U(th) from FUNCT_2:sch 4;
for hy1 holds
(hy1")(#)(Cr/*hy1) is convergent & lim ((hy1")(#)(Cr/*hy1)) = 0
proof
let hy1;
A2: for n holds ((hy1")(#)(Cr/*hy1)).n
=Re((Sum(hy1.n*<i> P_dt))* (cos.p+(sin.p)*<i>))
proof
let n;
A3: n in NAT by ORDINAL1:def 12;
A4: ((hy1")(#)(Cr/*hy1)).n=(hy1".n)*((Cr/*hy1).n) by SEQ_1:8
.=(hy1.n)"*((Cr/*hy1).n) by VALUED_1:10;
dom Cr = REAL by FUNCT_2:def 1;
then rng hy1 c= dom Cr;
then
A5: ((hy1")(#)(Cr/*hy1)).n= (hy1.n)"*(Cr.(hy1.n)) by A4,FUNCT_2:108,A3
.=(hy1.n)"*U(hy1.n) by A1
.=(hy1.n)"*(hy1.n)* Re((Sum(hy1.n*<i> P_dt))* (cos.p+(sin.p)*<i>));
hy1.n<>0 by SEQ_1:5;
then
((hy1")(#)(Cr/*hy1)).n =1*Re((Sum(hy1.n*<i> P_dt))* (cos.p+(sin.p)*<i>))
by A5,XCMPLX_0:def 7
.=Re((Sum(hy1.n*<i> P_dt))* (cos.p+(sin.p)*<i>));
hence thesis;
end;
deffunc U(Real) = Re((Sum(hy1.$1*<i> P_dt))* (cos.p+(sin.p)*<i>));
consider rseq such that
A6: for n holds rseq.n= U(n) from SEQ_1:sch 1;
deffunc U(Nat)
= (Sum((hy1.$1)*<i> P_dt))* (cos.p+(sin.p)*<i>);
consider cq1 such that
A7: for n holds cq1.n= U(n) from COMSEQ_1:sch 1;
A8: for q be Real st q>0
ex k st for m st k<=m holds |.cq1.m-0c.|<q
proof
let q be Real such that
A9: q>0;
ex k st for m st k<=m holds |.cq1.m-0c.|<q
proof
consider r such that
A10: r>0 and
A11: for z being Complex st |.z.|<r holds |.(Sum (z P_dt)).|<q
by A9,Th57;
hy1 is convergent & lim(hy1)=0;
then consider k such that
A12: for m st k<=m holds |.hy1.m-0.|<r by A10,SEQ_2:def 7;
A13: now
let m such that
A14: k<=m;
A15: |. cq1.m-0c.|= |.(Sum((hy1.m)*<i> P_dt))* (cos.p+(sin.p)*<i>).|
by A7
.= |.(Sum((hy1.m)*<i> P_dt)).|* |.cos.p+(sin.p)*<i>.|
by COMPLEX1:65
.= |.(Sum((hy1.m)*<i> P_dt)).|* |.Sum(p*<i> ExpSeq ).|
by Lm3
.=|.(Sum((hy1.m)*<i> P_dt)).|*1 by Lm5
.=|.(Sum((hy1.m)*<i> P_dt)).|;
A16: |.hy1.m-0.|<r by A12,A14;
(hy1.m)*<i> = 0+(hy1.m)*<i>;
then Re
((hy1.m)*<i>)=0 & Im((hy1.m)*<i>)=hy1.m by COMPLEX1:12;
then |.(hy1.m)*<i>.| =|.hy1.m.| by COMPLEX1:72;
hence |.cq1.m-0c.|<q by A11,A15,A16;
end;
take k;
thus thesis by A13;
end;
hence thesis;
end;
then A17: cq1 is convergent by COMSEQ_2:def 5;
then A18: lim(cq1)=0c by A8,COMSEQ_2:def 6;
A19: for n being Element of NAT holds Re(cq1).n= rseq.n
proof
let n be Element of NAT;
Re(cq1).n=Re((cq1).n) by COMSEQ_3:def 5
.=Re((Sum((hy1.n)*<i> P_dt))* (cos.p+(sin.p)*<i>)) by A7;
hence thesis by A6;
end;
for n being Element of NAT holds rseq.n=((hy1")(#)(Cr/*hy1)).n
proof
let n be Element of NAT;
rseq.n=Re((Sum((hy1.n)*<i> P_dt))* (cos.p+(sin.p)*<i>)) by A6;
hence thesis by A2;
end;
then rseq=(hy1")(#)(Cr/*hy1);
then (hy1")(#)(Cr/*hy1)=Re(cq1) by A19;
hence thesis by A17,A18,COMPLEX1:4,COMSEQ_3:41;
end;
then reconsider PR = Cr as RestFunc by FDIFF_1:def 2;
deffunc U1(Real) = In($1*cos.p,REAL);
consider CL being Function of REAL, REAL such that
A20: for th be Element of REAL holds CL.th=U1(th) from FUNCT_2:sch 4;
A21: for d be Real holds CL.d = d*cos.p
proof
let d be Real;
d in REAL by XREAL_0:def 1;
then CL.d=U1(d) by A20;
hence thesis;
end;
ex r st for q holds CL.q=r*q
proof
take (cos.p);
thus thesis by A21;
end;
then reconsider PL = CL as LinearFunc by FDIFF_1:def 3;
A22: 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
A23: for r st r in ].p-1,p+1 .[ holds sin.r - sin.p = PL.(r-p) + PR.(r-p)
proof
let r;
A24: r-p in REAL by XREAL_0:def 1;
r=p+(r-p);
then sin.r - sin.p
=(r-p)*cos.p +(r-p)*Re((Sum((r-p)*<i> P_dt))* (cos.p+sin.p*<i>))
by Th60
.=(r-p)*cos.p +U(r-p)
.=(r-p)*cos.p +Cr.(r-p) by A1,A24
.=PL.(r-p) + PR.(r-p) by A21;
hence thesis;
end;
take ].p-1,p+1 .[;
thus thesis by A23,Th24,RCOMP_1:def 6;
end;
then A25: sin is_differentiable_in p by FDIFF_1:def 4;
PL.1= 1*cos.p by A21;
hence thesis by A22,A25,FDIFF_1:def 5;
end;
theorem Th64:
exp_R is_differentiable_in p & diff(exp_R,p)=exp_R.p
proof
deffunc U(Real) = In($1 * exp_R.p*Re((Sum($1 P_dt))),REAL);
consider Cr being Function of REAL, REAL such that
A1: for th be Element of REAL holds Cr.th = U(th) from FUNCT_2:sch 4;
for hy1 holds
(hy1")(#)(Cr/*hy1) is convergent & lim ((hy1")(#)(Cr/*hy1)) = 0
proof
let hy1;
A2: for n holds ((hy1")(#)(Cr/*hy1)).n =exp_R.p*Re((Sum((hy1.n) P_dt)))
proof
let n;
A3: n in NAT by ORDINAL1:def 12;
A4: ((hy1")(#)(Cr/*hy1)).n=(hy1".n)*((Cr/*hy1).n) by SEQ_1:8
.=(hy1.n)"*((Cr/*hy1).n) by VALUED_1:10;
dom Cr = REAL by FUNCT_2:def 1;
then rng hy1 c= dom Cr;
then
A5: ((hy1")(#)(Cr/*hy1)).n= (hy1.n)"*(Cr.(hy1.n)) by A4,FUNCT_2:108,A3
.=(hy1.n)"*U(hy1.n) by A1
.=(hy1.n)"*(hy1.n)* (exp_R.p*Re((Sum((hy1.n) P_dt))));
hy1.n<>0 by SEQ_1:5;
then ((hy1")(#)(Cr/*hy1)).n
=1*(exp_R.p*Re((Sum((hy1.n) P_dt)))) by A5,XCMPLX_0:def 7
.=exp_R.p*Re((Sum((hy1.n) P_dt)));
hence thesis;
end;
deffunc U(Real) = exp_R.p*Re((Sum((hy1.$1) P_dt)));
consider rseq such that
A6: for n holds rseq.n= U(n) from SEQ_1:sch 1;
deffunc U(Nat) = Sum((hy1.$1) P_dt)*exp_R.p;
consider cq1 such that
A7: for n holds cq1.n= U(n) from COMSEQ_1:sch 1;
A8: 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
A9: q>0;
ex k st for m st k<=m holds |.cq1.m-0c.|<q
proof
exp_R.p>0 by Th53;
then consider r such that
A10: r>0 and
A11: for z being Complex st |.z.|<r holds |.(Sum(z P_dt)).|<q/
exp_R.p
by A9,Th57;
hy1 is convergent & lim(hy1)=0;
then consider k such that
A12: for m st k<=m holds |.hy1.m-0.|<r by A10,SEQ_2:def 7;
A13: now
let m such that
A14: k<=m;
A15: |.cq1.m-0c.|= |.(Sum((hy1.m) P_dt))* exp_R.p.| by A7
.= |.(Sum((hy1.m) P_dt)).|* |.exp_R.p.|
by COMPLEX1:65
.= |.(Sum((hy1.m) P_dt)).|*
sqrt((Re(exp_R.p))^2 + (Im(exp_R.p))^2);
exp_R.p = exp_R.p+0*<i>;
then
A16: Re(exp_R.p)=exp_R.p & Im(exp_R.p)=0 by COMPLEX1:12;
A17: exp_R.p>0 by Th53;
then A18: |.cq1.m-0c.| =|.(Sum((hy1.m) P_dt)).|* ( exp_R.p)
by A15,A16,SQUARE_1:22;
|.hy1.m-0.|<r by A12,A14;
then |.cq1.m-0c.|<q/exp_R.p * exp_R.p by A11,A17,A18,XREAL_1:68;
hence |.cq1.m-0c.|<q by A17,XCMPLX_1:87;
end;
take k;
thus thesis by A13;
end;
hence thesis;
end;
then A19: cq1 is convergent by COMSEQ_2:def 5;
then A20: lim(cq1)=0c by A8,COMSEQ_2:def 6;
A21: for n being Element of NAT holds Re(cq1).n= rseq.n
proof
A22: for n holds Re(cq1).n=exp_R.p*Re((Sum((hy1.n) P_dt)))
proof
let n;
Re(cq1).n=Re(cq1.n) by COMSEQ_3:def 5
.=Re((Sum((hy1.n) P_dt))*exp_R.p) by A7
.=exp_R.p*Re((Sum((hy1.n) P_dt))) by Lm12;
hence thesis;
end;
let n;
rseq.n=exp_R.p*Re((Sum((hy1.n) P_dt))) by A6;
hence thesis by A22;
end;
for n being Element of NAT holds rseq.n=((hy1")(#)(Cr/*hy1)).n
proof
let n be Element of NAT;
rseq.n=exp_R.p*Re((Sum((hy1.n) P_dt))) by A6;
hence thesis by A2;
end;
then rseq=(hy1")(#)(Cr/*hy1);
then (hy1")(#)(Cr/*hy1)=Re(cq1) by A21;
hence thesis by A19,A20,COMPLEX1:4,COMSEQ_3:41;
end;
then reconsider PR = Cr as RestFunc by FDIFF_1:def 2;
deffunc U1(Real) = In($1* (exp_R.p),REAL);
consider CL being Function of REAL, REAL such that
A23: for th be Element of REAL holds CL.th=U1(th) from FUNCT_2:sch 4;
A24: for d be Real holds CL.d = d * (exp_R.p)
proof
let d be Real;
d in REAL by XREAL_0:def 1;
then CL.d=U1(d) by A23;
hence thesis;
end;
ex r st for q holds CL.q=r*q
proof
take exp_R.p;
thus thesis by A24;
end;
then reconsider PL = CL as LinearFunc by FDIFF_1:def 3;
A25: ex N being Neighbourhood of p st N c= dom exp_R &
for r st r in N holds exp_R.r - exp_R.p = PL.(r-p) + PR.(r-p)
proof
A26: for r st r in ].p-1,p+1 .[ holds exp_R.r - exp_R.p = PL.(r-p) + PR.(r-p)
proof
let r;
reconsider p as Real;
A27: r-p in REAL by XREAL_0:def 1;
r=p+(r-p);
then exp_R.r - exp_R.p =(r-p)* (exp_R.p)+(r-p)*exp_R.p*
Re((Sum((r-p) P_dt))) by Th61
.=(r-p)* (exp_R.p)+U(r-p)
.=(r-p)* (exp_R.p)+Cr.(r-p) by A1,A27
.=PL.(r-p) + PR.(r-p) by A24;
hence thesis;
end;
take ].p-1,p+1 .[;
thus thesis by A26,Th46,RCOMP_1:def 6;
end;
then A28: exp_R is_differentiable_in p by FDIFF_1:def 4;
PL.1= 1*exp_R.p by A24;
hence thesis by A25,A28,FDIFF_1:def 5;
end;
theorem Th65:
exp_R is_differentiable_on REAL & diff(exp_R,th)=exp_R.th
proof
A1: [#]REAL is open Subset of REAL & REAL c=dom exp_R by FUNCT_2:def 1;
for r st r in REAL holds exp_R is_differentiable_in r by Th64;
hence thesis by A1,Th64,FDIFF_1:9;
end;
theorem Th66:
cos is_differentiable_on REAL & diff(cos,th)=-sin.th
proof
A1: [#]REAL is open Subset of REAL & REAL c=dom cos by FUNCT_2:def 1;
for r st r in REAL holds cos is_differentiable_in r by Th62;
hence thesis by A1,Th62,FDIFF_1:9;
end;
theorem Th67:
sin is_differentiable_on REAL & diff(sin,th)=cos.th
proof
A1: [#]REAL is open Subset of REAL & REAL c=dom sin by FUNCT_2:def 1;
for r st r in REAL holds sin is_differentiable_in r by Th63;
hence thesis by A1,Th63,FDIFF_1:9;
end;
theorem Th68:
th in [.0,1 .] implies 0<cos.th & cos.th>=1/2
proof
assume th in [.0,1 .];
then A1: 0<=th & th<=1 by XXREAL_1:1;
A2: Partial_Sums(th P_cos) is convergent by Th35;
A3: cos.th=Sum (th P_cos) by Th36;
lim ((Partial_Sums(th P_cos))*bq )=lim(Partial_Sums(th P_cos)) by A2,SEQ_4:17;
then A4: 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;
A5: ((Partial_Sums(th P_cos))*bq).0=(Partial_Sums(th P_cos)).(bq.0)
by FUNCT_2:15
.= (Partial_Sums(th P_cos)).(2*0+1) by Lm6
.= (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 Def21
.= (-1)|^ 0 * (th)|^ (2*0)/((2*0)!)+
(-1)|^ 1 * (th)|^ (2*1)/((2*1)!) by Def21
.= 1* (th)|^ (2*0)/((2*0)!)+
(-1)|^ 1 * (th)|^ (2*1)/((2*1)!) by Lm7
.= 1/1 + (-1)|^ 1 * (th)|^ (2*1)/((2*1)!) by NEWTON:4,12
.= 1+ (-1)* (th)|^ (2*1)/((2*1)!)
.= 1+ (-1)*(th*th)/((2*1)!) by NEWTON:81
.= 1-(th^2)/2 by NEWTON:14;
defpred X[Nat] means
((Partial_Sums(th P_cos))*bq).$1 >= 1/2;
th^2 <= 1^2 by A1,SQUARE_1:15;
then 1 - 1/2 = 1/2 & (th^2)/2<=1/2 by XREAL_1:72;
then A6: X[0] by A5,XREAL_1:10;
A7: for k st X[k] holds X[k+1]
proof
let k;
A8: k in NAT by ORDINAL1:def 12;
assume
A9: ((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 FUNCT_2:15
.=(Partial_Sums(th P_cos)).(2*(k+1)+1) by Lm6
.=(Partial_Sums(th P_cos)).(2*k+1+1)+(th P_cos).(2*(k+1)+1) by
SERIES_1:def 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 Lm6
.=((Partial_Sums(th P_cos))*bq).k+ (th P_cos).(2*k+1+1)+
(th P_cos).(2*(k+1)+1) by FUNCT_2:15,A8;
then A10: (
(Partial_Sums(th P_cos))*bq).(k+1)-((Partial_Sums(th P_cos))* bq).k
=(th P_cos).(2*k+1+1)+ (th P_cos).(2*(k+1)+1);
A11: (th P_cos).(2*k+1+1)=(-1)|^ (2*(k+1)) * (th)|^ (2*(2*(k+1)))/((2*(
2*(k+1)))!) by Def21
.=(1)* (th)|^ (2*(2*(k+1)))/((2*(2*(k+1)))!) by Lm7
.=(th)|^ (2*(2*(k+1)))/((2*(2*(k+1)))!);
A12: (th P_cos).(2*(k+1)+1)
= (-1)|^ (2*(k+1)+1) * (th)|^ (2*(2*(k+1)+1))/((2*(2*(k+1)+1))!)
by Def21
.=((-1) * (th)|^ (2*(2*(k+1)+1)))/((2*(2*(k+1)+1))!) by Lm7;
A13: 2*(2*(k+1))<2*(2*(k+1)+1) by XREAL_1:29,68;
then A14: (2*(2*(k+1)))! <= (2*(2*(k+1)+1))! by Th38;
A15: (th)|^ (2*(2*(k+1)+1)) <= (th)|^ (2*(2*(k+1))) by A1,A13,Th39;
A16: 0 <= (th)|^ (2*(2*(k+1)+1)) & (2*(2*(k+1)+1))! >0 by POWER:3;
1/((2*(2*(k+1)+1))!)<=1/((2*(2*(k+1)))!) by A14,XREAL_1:85;
then (th)|^ (2*(2*(k+1)+1))*(1/((2*(2*(k+1)+1))!))<=
(th)|^ (2*(2*(k+1)))*(1/((2*(2*(k+1)))!)) by A15,A16,XREAL_1:66;
then ((th)|^ (2*(2*(k+1)))*1)/((2*(2*(k+1)))!)-
((th)|^ (2*(2*(k+1)+1))*1)/((2*(2*(k+1)+1))!)>=0 by XREAL_1:48;
then ((Partial_Sums(th P_cos))*bq).(k+1)>=((Partial_Sums(th P_cos))*bq
).k by A10,A11,A12,XREAL_1:49;
hence thesis by A9,XXREAL_0:2;
end;
for n holds X[n] from NAT_1:sch 2(A6,A7);
hence thesis;
end;
hence thesis by A2,A4,PREPOWER:1,SEQ_4:16;
end;
definition
func tan -> PartFunc of REAL, REAL equals
sin/cos;
coherence;
func cot -> PartFunc of REAL, REAL equals
cos/sin;
coherence;
end;
theorem Th69:
[.0,1 .] c= dom tan & ].0,1 .[ c= dom tan
proof
A1: [.0,1 .] \ cos"{0} c=dom cos \ cos"{0} by Th24,XBOOLE_1:33;
[.0,1 .] /\ cos"{0}={}
proof
assume [.0,1 .] /\ cos"{0}<>{};
then consider rr being object such that
A2: rr in [.0,1 .] /\ cos"{0} by XBOOLE_0:def 1;
A3: rr in [.0,1 .] by A2,XBOOLE_0:def 4;
A4: rr in cos"{0} by A2,XBOOLE_0:def 4;
A5: cos.(rr) <>0 by A3,Th68;
cos.(rr) in {0} by A4,FUNCT_1:def 7;
hence contradiction by A5,TARSKI:def 1;
end;
then [.0,1 .] misses cos"{0} by XBOOLE_0:def 7;
then [.0,1 .] c= dom cos \ cos"{0} by A1,XBOOLE_1:83;
then [.0,1 .] c= dom sin /\ (dom cos \ cos"{0}) by Th24,XBOOLE_1:19;
then A6: [.0,1 .] c= dom tan by RFUNCT_1:def 1;
].0,1 .[c=[.0,1 .] by XXREAL_1:25;
hence thesis by A6,XBOOLE_1:1;
end;
Lm14: dom(tan|[.0,1 .]) = [.0,1 .] &
for th st th in [.0,1 .] holds tan|[.0,1 .].th=tan.th
proof
dom(tan|[.0,1 .])=dom tan /\ [.0,1 .] by RELAT_1:61;
then dom(tan|[.0,1 .]) = [.0,1 .] by Th69,XBOOLE_1:28;
hence thesis by FUNCT_1:47;
end;
Lm15: tan is_differentiable_on ].0,1 .[ & for th st th in ].0,1 .[ holds
diff(tan,th)>0
proof
A1: sin is_differentiable_on ].0,1 .[ & cos is_differentiable_on ].0,1 .[ by
Th66,Th67,FDIFF_1:26;
A2: for th st th in ].0,1 .[ holds cos.th<>0
proof
let th such that
A3: th in ].0,1 .[;
].0,1 .[ c=[.0,1 .] by XXREAL_1:25;
hence thesis by A3,Th68;
end;
for th st th in ].0,1 .[ holds diff(tan,th)>0
proof
let th such that
A4: th in ].0,1 .[;
A5: th is Real & cos is_differentiable_in th by Th62;
A6: sin is_differentiable_in th by Th63;
A7: cos.th<>0 by A2,A4;
then A8: diff(tan,th)=(diff(sin,th)*cos.th-diff(cos,th)*sin.th)/(cos.th) ^2
by A5,A6,FDIFF_2:14
.=(cos.th*cos.th-diff(cos,th)*sin.th)/(cos.th)^2 by Th63
.=(cos.th*cos.th-(-sin.th)*sin.th)/(cos.th)^2 by Th62
.=((cos.th)^2+(sin.th)*sin.th)/(cos.th)^2
.=1/(cos.th)^2 by Th28;
(cos.th)^2>0 by A7,SQUARE_1:12;
hence thesis by A8;
end;
hence thesis by A1,A2,FDIFF_2:21;
end;
theorem Th70:
tan|[.0,1 .] is continuous
proof
for th be Real st th in dom(tan|[.0,1 .]) holds
tan|[.0,1 .] is_continuous_in th
proof
let th be Real;
assume
A1: th in dom(tan|[.0,1 .]);
then A2: th in [.0,1 .] by RELAT_1:57;
dom sin = REAL by FUNCT_2:def 1;
then A3: th in dom sin by XREAL_0:def 1;
A4: th in [#]REAL by XREAL_0:def 1;
then sin is_differentiable_in th by Th67,FDIFF_1:9;
then A5: sin is_continuous_in th by FDIFF_1:24;
cos is_differentiable_in th by A4,Th66,FDIFF_1:9;
then A6: cos is_continuous_in th by FDIFF_1:24;
cos.(th) <> 0 by A2,Th68;
then A7: tan is_continuous_in th by A3,A5,A6,FCONT_1:11;
now
let rseq;
assume that
A8: rng rseq c= dom (tan|[.0,1 .]) and
A9: rseq is convergent & lim rseq = th;
A10: rng rseq c= dom tan by A8,Lm14,Th69,XBOOLE_1:1;
then A11: tan.th = lim (tan/*rseq) by A7,A9,FCONT_1:def 1;
now
let k1 be Element of NAT;
dom (rseq) = NAT by SEQ_1:1;
then rseq.k1 in rng rseq by FUNCT_1:def 3;
then A12: (tan|[.0,1 .]).(rseq.k1)=tan.(rseq.k1) by A8,Lm14;
(tan|[.0,1 .]).(rseq.k1)=((tan|[.0,1 .])/*rseq).k1 by A8,FUNCT_2:108;
hence ((tan|[.0,1 .])/*rseq).k1=(tan/*rseq).k1
by A8,A12,Lm14,Th69,FUNCT_2:108,XBOOLE_1:1;
end;
then (tan|[.0,1 .])/*rseq =tan/*rseq;
hence (tan|[.0,1 .])/*rseq is convergent
& (tan|[.0,1 .]).th = lim ((tan|[.0,1 .])/*rseq)
by A1,A7,A9,A10,A11,Lm14,FCONT_1:def 1;
end;
hence thesis by FCONT_1:def 1;
end;
hence thesis by FCONT_1:def 2;
end;
theorem Th71:
th1 in ].0,1 .[ & th2 in ].0,1 .[ & tan.th1=tan.th2 implies th1=th2
proof
assume that
A1: th1 in ].0,1 .[ and
A2: th2 in ].0,1 .[ and
A3: tan.(th1)=tan.(th2);
A4: 0<th1 by A1,XXREAL_1:4;
A5: th1<1 by A1,XXREAL_1:4;
A6: 0<th2 by A2,XXREAL_1:4;
A7: th2<1 by A2,XXREAL_1:4;
assume
A8: th1<>th2;
now per cases by A8,XXREAL_0:1;
suppose
A9: th1<th2;
A10: for th be Element of REAL st th in ].th1,th2.[ holds th in ].0,1 .[
proof
let th be Element of REAL;
assume
A11: th in ].th1,th2.[;
then A12: th1<th by XXREAL_1:4;
th< th2 by A11,XXREAL_1:4;
then th <1 by A7,XXREAL_0:2;
hence thesis by A4,A12,XXREAL_1:4;
end;
A13: for th be Element of REAL st th in [.th1,th2.] holds th in [.0,1 .]
proof
let th be Element of REAL;
assume
A14: th in [.th1,th2.];
then A15: th1<=th by XXREAL_1:1;
th<= th2 by A14,XXREAL_1:1;
then th <=1 by A7,XXREAL_0:2;
hence thesis by A4,A15,XXREAL_1:1;
end;
].th1,th2.[c=].0,1 .[ by A10,SUBSET_1:2;
then A16: tan is_differentiable_on ].th1,th2.[ by Lm15,FDIFF_1:26;
[.th1,th2.]c=[. 0,1 .] & tan|[.th1,th2.] is continuous by A13,Th70,
FCONT_1:16,SUBSET_1:2;
then consider r such that
A17: r in ].th1,th2.[ & diff(tan,r)=0
by A3,A9,A16,Th69,ROLLE:1,XBOOLE_1:1;
take th=r;
thus th in ].0,1 .[ & diff(tan,(th))=0 by A10,A17;
end;
suppose
A18: th2<th1;
A19: for th be Element of REAL st th in ].th2,th1 .[ holds th in ].0,1 .[
proof
let th be Element of REAL;
assume
A20: th in ].th2,th1 .[;
then A21: th2<th by XXREAL_1:4;
th< th1 by A20,XXREAL_1:4;
then th <1 by A5,XXREAL_0:2;
hence thesis by A6,A21,XXREAL_1:4;
end;
A22: for th be Element of REAL st th in [.th2,th1 .] holds th in [.0,1 .]
proof
let th be Element of REAL;
assume
A23: th in [.th2,th1 .];
then A24: th2<=th by XXREAL_1:1;
th<= th1 by A23,XXREAL_1:1;
then th <=1 by A5,XXREAL_0:2;
hence thesis by A6,A24,XXREAL_1:1;
end;
].th2,th1 .[c=].0,1 .[ by A19,SUBSET_1:2;
then A25: tan is_differentiable_on ].th2,th1 .[ by Lm15,FDIFF_1:26;
[.
th2,th1 .] c=[.0,1 .] & tan|[.th2,th1.] is continuous by A22,Th70,FCONT_1:16
,SUBSET_1:2;
then consider r such that
A26: r in ].th2,th1 .[ & diff(tan,r)=0
by A3,A18,A25,Th69,ROLLE:1,XBOOLE_1:1;
take th=r;
thus th in ].0,1 .[ & diff(tan,(th))=0 by A19,A26;
end;
end;
hence thesis by Lm15;
end;
Lm16: tan.0 = 0 & tan.1 >1
proof
0 in [.0,1 .] by XXREAL_1:1;
then A1: tan.0=(sin.0)* (cos.0)" by Th69,RFUNCT_1:def 1
.=0 by Th30;
1 in [.0,1 .] by XXREAL_1:1;
then tan.1 =(sin.1)/(cos.1) by Th69,RFUNCT_1:def 1;
hence thesis by A1,Th42,XREAL_1:187;
end;
begin :: Existence of Circle Ratio
definition
func PI -> Real means
:Def28:
tan.(it/4) = 1 & it in ]. 0, 4 .[;
existence
proof
A1: [.tan.0,tan.1 .] = {r : tan.0<=r & r<= tan.1 } by RCOMP_1:def 1;
[.tan.1,tan.0 .]= {} by Lm16,XXREAL_1:29;
then 1 in [.tan.0,tan.1 .] \/ [.tan.1,tan.0 .] by A1,Lm16;
then consider th such that
A2: th in [.0, 1 .] and
A3: tan.(th)=1 by Th69,Th70,FCONT_2:15;
A4: 0<=th by A2,XXREAL_1:1;
A5: th <= 1 by A2,XXREAL_1:1;
A6: 0 <th by A3,A4,Lm16;
A7: th <1 by A3,A5,Lm16,XXREAL_0:1;
take th1 =th*4;
thus tan.(th1/4)=1 by A3;
th*4<1*4 by A7,XREAL_1:68;
hence thesis by A6,XXREAL_1:4;
end;
uniqueness
proof
let th1,th2 be Real such that
A8: tan.(th1/4) = 1 and
A9: th1 in ]. 0, 4 .[ and
A10: tan.(th2/4) = 1 and
A11: th2 in ]. 0, 4 .[;
A12: 0<th1 by A9,XXREAL_1:4;
th1 <4 by A9,XXREAL_1:4;
then th1/4 <4/4 by XREAL_1:74;
then A13: th1/4 in ]. 0, 1 .[ by A12,XXREAL_1:4;
A14: 0<th2 by A11,XXREAL_1:4;
th2 < 4 by A11,XXREAL_1:4;
then th2/4 <4/4 by XREAL_1:74;
then th2/4 in ]. 0, 1 .[ by A14,XXREAL_1:4;
then th1/4=th2/4 by A8,A10,A13,Th71;
hence thesis;
end;
end;
theorem Th72:
sin.(PI/4) = cos.(PI/4)
proof
A1: PI in ].0, 4.[ by Def28;
then A2: 0< PI by XXREAL_1:4;
PI < 4 by A1,XXREAL_1:4;
then PI/4 < 4/4 by XREAL_1:74;
then A3: PI/4 in ].0,1 .[ by A2,XXREAL_1:4;
tan.(PI/4) =1 by Def28;
then sin.(PI/4) * (cos.(PI/4))"=1 by A3,Th69,RFUNCT_1:def 1;
hence thesis by XCMPLX_1:209;
end;
begin :: Formulas of sin and cos
theorem Th73:
sin.(th1+th2)=(sin.(th1)) *(cos.(th2))+(cos.(th1)) * (sin.(th2)) &
cos.(th1+th2)=(cos.(th1)) *(cos.(th2))-(sin.(th1)) * (sin.(th2))
proof
reconsider th1,th2 as Real;
A1: (th1+th2)*<i> = 0+0+(th1+th2)*<i>;
A2: Sum(th1*<i> ExpSeq ) * Sum(th2*<i> ExpSeq )
=Sum((th1*<i>+th2*<i>) ExpSeq ) by Lm2
.=cos.(th1+th2)+(sin.(th1+th2))*<i> by A1,Lm3;
Sum((th1*<i> ExpSeq) ) * Sum((th2*<i> ExpSeq) )
=(cos.(th1)+(sin.th1)*<i>)* Sum((th2*<i> ExpSeq) ) by Lm3
.=(cos.(th1)+sin.(th1)*<i>)*(cos.(th2)+(sin.th2)*<i>) by Lm3
.=((cos.(th1)) *( cos.(th2))-(sin.(th1)) * (sin.(th2))+
((sin.(th1)) * (cos.(th2))+(cos.(th1)) * (sin.(th2)))*<i>);
hence thesis by A2,COMPLEX1:77;
end;
theorem
sin(th1+th2)=(sin(th1)) *(cos(th2))+(cos(th1)) * (sin(th2)) &
cos(th1+th2)=(cos(th1)) *(cos(th2))-(sin(th1)) * (sin(th2)) by Th73;
theorem Th75:
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) .=(cos.(PI/4)) * (cos.(PI/4))
-(cos.(PI/4)) * (cos.(PI/4)) by Th72,Th73
.=0;
thus
A2: sin.(PI/2)=sin.(PI/4+PI/4) .= (cos.(PI/4)) *( cos.(PI/4))
+(sin.(PI/4)) * (sin.(PI/4)) by Th72,Th73
.=1 by Th28;
thus
A3: cos.(PI)=cos.(PI/2+PI/2) .=0 * 0-sin.(PI/2) * sin.(PI/2) by A1,Th73
.=-1 by A2;
thus
A4: sin.(PI)=sin.(PI/2+PI/2) .=(sin.(PI/2)) *( cos.(PI/2))
+(cos.(PI/2) )*( sin.(PI/2)) by Th73
.=0 by A1;
thus cos.(PI+PI/2) =(cos.(PI)) *( cos.(PI/2))
-(sin.(PI)) * (sin.(PI/2)) by Th73
.=0 by A1,A4;
thus sin.(PI+PI/2) =(sin.(PI) )*( cos.(PI/2))
+(cos.(PI)) *( sin.(PI/2) ) by Th73
.=-1 by A1,A2,A3;
thus cos.(2 * PI)=cos.(PI+PI) .=(-1 ) * (-1) -sin.(PI) * sin.(PI) by A3,Th73
.=1 by A4;
thus sin.(2 * PI)=sin.(PI+PI)
.=(sin.(PI)) * (cos.(PI))+(cos.(PI)) * (sin.(PI)) by Th73
.=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 Th75;
theorem Th77:
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 Th73,Th75
.=sin.th;
thus cos.(th+2 * PI)=cos.(th) * 1 - sin.(th) * 0 by Th73,Th75
.=cos.th;
thus sin.(PI/2-th) =(sin.(PI/2) )* (cos.(-th))
+ (cos.(PI/2)) *( sin.(-th)) by Th73
.=cos.(th) by Th30,Th75;
thus cos.(PI/2-th) =(cos.(PI/2)) * (cos.(-th))
- ( sin.(PI/2)) *( sin.(-th)) by Th73
.=0 - 1 * (-sin.(th)) by Th30,Th75
.=sin.(th);
thus sin.(PI/2+th) =1 * cos.(th) + 0 * (sin.(th)) by Th73,Th75
.=cos.(th);
thus cos.(PI/2+th) =(cos.(PI/2)) *( cos.(th))
-( sin.(PI/2) )*( sin.(th)) by Th73
.=-sin.(th) by Th75;
thus
sin.(PI+th) =(sin.(PI)) * (cos.(th)) +( cos.(PI) )*( sin.(th)) by Th73
.=-sin.(th) by Th75;
thus cos.(PI+th) =(-1) * cos.(th) - 0 * sin.(th) by Th73,Th75
.=-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) by Th77;
Lm17: th in [.0,1 .] implies sin.th>=0
proof
assume
A1: th in [.0,1 .];
then A2: th<=1 by XXREAL_1:1;
sin.th>= sin.0
proof
now per cases by A1,XXREAL_1:1;
suppose
th=0;
hence thesis;
end;
suppose
A3: 0<th;
sin|REAL is continuous by Th67,FDIFF_1:25;
then sin|[.0,th.] is continuous by FCONT_1:16;
then consider r such that
A4: r in ].0,th.[ and
A5: diff(sin,r)=(sin.th-sin.0)/(th-0)
by A3,Th24,Th67,FDIFF_1:26,ROLLE:3;
A6: r < th by A4,XXREAL_1:4;
A7: 0<r by A4,XXREAL_1:4;
r <1 by A2,A6,XXREAL_0:2;
then r in [.0,1 .] by A7,XXREAL_1:1;
then cos.r >0 by Th68;
then sin.th-sin.0 >0 by A3,A5,Th67;
hence thesis by XREAL_1:47;
end;
end;
hence thesis;
end;
hence thesis by Th30;
end;
theorem Th79:
th in ].0,PI/2.[ implies cos.th > 0
proof
assume that
A1: th in ].0,PI/2.[ and
A2: cos.th <= 0;
cos|REAL is continuous by Th66,FDIFF_1:25;
then A3: cos|[.0,th.] is continuous by FCONT_1:16;
A4: 0 < th by A1,XXREAL_1:4;
[.
cos.0,cos.th .] \/ [.cos.th,cos.0 .] = [.cos.th,cos.0 .] & 0 in [.cos.th,
cos.0 .] by A2,Th30,XXREAL_1:1,222;
then ex th2 st th2 in [.0,th .] & cos.th2 = 0
by A3,A4,Th24,FCONT_2:15;
then consider th2 be Real such that
A5: th2 in [.0,th .] and 0 < th and
A6: cos.th2 = 0 by A4;
A7: 0 <= th2 by A5,XXREAL_1:1;
A8: th2 <= th by A5,XXREAL_1:1;
A9: th < PI/2 by A1,XXREAL_1:4;
A10: 0<th2 by A6,A7,Th30;
th2<PI/2 by A8,A9,XXREAL_0:2;
then A11: th2/2 < PI/2/2 by XREAL_1:74;
PI in ].0, 4.[ by Def28;
then PI < 4 by XXREAL_1:4;
then PI/4 < 4/4 by XREAL_1:74;
then A12: th2/2 < 1 by A11,XXREAL_0:2;
0 = cos.(th2/2 + th2/2) by A6
.= (cos.(th2/2))^2 - (sin.(th2/2)) * (sin.(th2/2)) by Th73
.= ((cos.(th2/2)) - (sin.(th2/2))) * ((cos.(th2/2)) + (sin.(th2/2)));
then
A13: cos.(th2/2) - sin.(th2/2) = 0 or cos.(th2/2) + sin.(th2/2) = 0;
A14: th2/2 in ].0,1 .[ by A10,A12,XXREAL_1:4;
].0,1 .[ c= [.0,1 .] by XXREAL_1:25;
then A15: cos.(th2/2) > 0 & sin.(th2/2) >= -0 by A14,Lm17,Th68;
4*(th2/2) < 4*1 by A12,XREAL_1:68;
then A16: (2*th2) in ].0,4.[ by A10,XXREAL_1:4;
(sin.(th2/2)) * (cos.(th2/2))"=1 by A13,A15,XCMPLX_0:def 7;
then tan.((2*th2)/4) = 1 by A14,Th69,RFUNCT_1:def 1;
then 2*th2 =PI by A16,Def28;
hence contradiction by A1,A8,XXREAL_1:4;
end;
theorem
th in ].0,PI/2.[ implies cos(th) > 0 by Th79;
begin :: Addenda
:: from COMPLEX2, 2006.03,06, A.T.
theorem
sin(a-b) = sin(a)*cos(b)-cos(a)*sin(b)
proof
thus sin(a-b) =(sin.a) *(cos.(-b))+(cos.a) * (sin.(-b)) by Th73
.=(sin.a) *(cos.b)+(cos.a) * (sin.(-b)) by Th30
.=(sin.a) *(cos.b)+(cos.a) * -(sin.b) by Th30
.=(sin a) *(cos b)-(cos a) * (sin b);
end;
theorem
cos(a-b) = cos(a)*cos(b)+sin(a)*sin(b)
proof
thus cos(a-b) =(cos.a) *(cos.(-b))-(sin.(a)) * (sin.(-b)) by Th73
.=(cos.a) *(cos.b)-(sin.a) * (sin.(-b)) by Th30
.=(cos.a) *(cos.b)-(sin.a) * -(sin.b) by Th30
.=(cos a) *(cos b)+(sin a) * (sin b);
end;
registration
cluster sin -> continuous;
coherence
proof
dom sin = REAL & sin|REAL is continuous by Th67,FDIFF_1:25,FUNCT_2:def 1;
hence thesis by RELAT_1:69;
end;
cluster cos -> continuous;
coherence
proof
dom cos = REAL & cos|REAL is continuous by Th66,FDIFF_1:25,FUNCT_2:def 1;
hence thesis by RELAT_1:69;
end;
cluster exp_R -> continuous;
coherence
proof
dom exp_R = REAL & exp_R|REAL is continuous by Th65,FDIFF_1:25
,FUNCT_2:def 1;
hence thesis by RELAT_1:69;
end;
end;