:: Trigonometric Functions and Existence of Circle Ratio :: by Yuguang Yang and Yasunari Shidama :: :: Received October 22, 1998 :: Copyright (c) 1998-2012 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, ORDINAL1, SUBSET_1, COMSEQ_1, SEQ_1, FDIFF_1, XXREAL_0, CARD_1, COMPLEX1, FUNCT_1, RELAT_1, XCMPLX_0, ARYTM_3, NAT_1, REALSET1, COMSEQ_3, 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; notations TARSKI, XBOOLE_0, SUBSET_1, ORDINAL1, NUMBERS, XCMPLX_0, XXREAL_0, XREAL_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, SEQ_1, RECDEF_1, SEQM_3, SERIES_1, SEQ_2, VALUED_1, RELSET_1, ABIAN, BINOP_2, RVSUM_1; 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; requirements REAL, NUMERALS, SUBSET, BOOLE, ARITHM; definitions COMSEQ_3, SQUARE_1, SUBSET_1, VALUED_1, XCMPLX_0, COMPLEX1; 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; schemes NAT_1, SEQ_1, COMSEQ_1, CLASSES1, BINOP_2, FUNCT_2; begin reserve q,th,r for Real, a,b,p for real number, w,z for Element of COMPLEX, k,l,m,n,n1,n2 for Element of 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 Element of NAT; 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 Element of NAT; cluster CHK(m,k) -> real; coherence by Def1; end; scheme ExComplexCASE{F(Nat,Nat)->complex number}: 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[set,set] means ex n st (n=$1 & (n <= k implies $2=F(k,n)) & (n > k implies $2=0c) ); A1: now let x be set; assume x in NAT; then consider n such that A2: n=x; A3: now assume n <= k; hence CHK(n,k) * F (k,n) =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 set; 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 set 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; ex l be Element of NAT st l=n & (l <= k implies seq.n=F(k,l)) & (l > k implies seq.n=0c) by A6; hence thesis; end; scheme ExRealCASE{F(Nat,Nat)->real number}: for k holds ex rseq st for n holds (n <= k implies rseq.n=F(k,n)) & (n > k implies rseq.n=0) proof let k; defpred P[set,set] means ex n st (n=$1 & (n <= k implies $2=F(k,n )) & (n > k implies $2=0) ); A1: now let x be set; assume x in NAT; then consider n such that A2: n=x; A3: now assume n <= k; hence 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 set; 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 set 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=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; ex l be Element of NAT st l=n & (l <= k implies rseq.n=F(k,l)) & (l > k implies rseq.n=0) by A6; hence thesis; end; 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,Element of REAL) = $2 * ($1+1); consider f being Function of NAT,REAL such that A1: f.0 = 1 & for n being Nat holds f.(n+1) = U(n,f.n) from NAT_1:sch 12; take f; thus thesis by A1; end; uniqueness proof let rseq1,rseq2; assume that A2: rseq1.0=1 and A3: for n holds rseq1.(n+1)=rseq1.n * (n+1) and A4: rseq2.0=1 and A5: for n holds rseq2.(n+1)=rseq2.n * (n+1); defpred X[Element of NAT] means rseq1.$1 = rseq2.$1; A6: X[0] by A2,A4; A7: for k be Element of NAT st X[k] holds X[k+1] proof let k be Element of NAT; assume rseq1.k =rseq2.k; hence rseq1.(k+1) = rseq2.k * (k+1) by A3 .= rseq2.(k+1) by A5; end; for n holds X[n] from NAT_1:sch 1(A6,A7); hence rseq1 = rseq2 by FUNCT_2:63; end; end; definition let n be Nat; redefine func n! equals 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]; l in NAT by ORDINAL1:def 12; then 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 number; deffunc U(Element of NAT) = z #N $1 /($1!); func z ExpSeq -> Complex_Sequence means :Def4: for n holds it.n = z #N 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 thus for s1,s2 being Complex_Sequence st (for x being Element of NAT holds s1.x = U(x)) & (for x being Element of NAT holds s2.x = U(x)) holds s1 = s2 from BINOP_2:sch 1; end; end; definition let a be real number; deffunc U(Element of 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 thus for s1,s2 being Real_Sequence st (for x being Element of NAT holds s1.x = U(x)) & (for x being Element of NAT holds s2.x = U(x)) holds s1 = s2 from BINOP_2:sch 1; 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*) by Th1 .=((m-'k)! ) * (m-k+1+0*) by A2,XREAL_1:233 .=((m-'k)! ) * (m+1-k); end; hence thesis by A1; end; definition let n be Element of NAT; func Coef(n) -> Complex_Sequence means :Def6: for k be Element of NAT holds (k <= n implies it.k = n! /( (k! ) * ((n-'k)! ))) & (k > n implies it.k = 0); existence proof deffunc U(Element of NAT,Element of 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; 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 by FUNCT_2:63; end; end; definition let n be Element of NAT; func Coef_e(n) -> Complex_Sequence means :Def7: for k be Element of NAT holds (k <= n implies it.k = 1r/((k! ) * ((n-'k)! ))) & (k > n implies it.k=0); existence proof deffunc U(Element of NAT,Element of 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; 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 by FUNCT_2:63; end; end; definition let seq; func Shift seq -> Complex_Sequence means :Def8: it.0=0 & for k be Element of NAT holds it.(k+1) = seq.k; existence proof deffunc U(Nat,Element of COMPLEX) = seq.$1; consider f being Function of NAT,COMPLEX such that A1: f.0 = 0c & for n being Nat holds f.(n+1)=U(n,f.n) from 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[Element of NAT] means seq1.$1 = seq2.$1; A6: X[0] by A2,A4; A7: for k be Element of NAT st X[k] holds X[k+1] proof let k be Element of NAT; assume seq1.k =seq2.k; thus seq1.(k+1) = seq.k by A3 .= seq2.(k+1) by A5; end; for n holds X[n] from NAT_1:sch 1(A6,A7); hence seq1 = seq2 by FUNCT_2:63; end; end; definition let n; let z,w be Element of COMPLEX; func Expan(n,z,w) -> Complex_Sequence means :Def9: for k be Element of 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(Element of NAT,Element of NAT) = ((Coef($1)).$2) * (z #N $2) * (w #N ($1-'$2)); for n holds ex seq st for k holds (k <= n implies seq.k = U(n,k)) & (k > n implies seq.k=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; 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 by FUNCT_2:63; end; end; definition let n; let z,w be Element of COMPLEX; func Expan_e(n,z,w) -> Complex_Sequence means :Def10: for k be Element of 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(Element of NAT,Element of NAT) = ((Coef_e($1)).$2) * (z #N $2) * (w #N ($1-'$2)); for n holds ex seq st for k holds (k <= n implies seq.k = U(n,k)) & (k > n implies seq.k=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; 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 by FUNCT_2:63; end; end; definition let n; let z,w be Element of COMPLEX; func Alfa(n,z,w) -> Complex_Sequence means :Def11: for k be Element of 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(Element of NAT,Element of 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; 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 by FUNCT_2:63; end; end; definition let a,b be real number; let n be Element of NAT; func Conj(n,a,b) -> Real_Sequence means for k be Element of 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(Element of NAT,Element of 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; 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 by FUNCT_2:63; end; end; definition let z, w be Element of COMPLEX; let n be Element of NAT; func Conj(n,z,w) -> Complex_Sequence means :Def13: for k be Element of NAT holds ( k <= n implies it.k= (z ExpSeq).k * (Partial_Sums(w ExpSeq).n -Partial_Sums(w ExpSeq).(n-'k))) & (n < k implies it.k=0); existence proof deffunc U(Element of NAT,Element of 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; 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 by FUNCT_2:63; end; end; Lm1: for p1,p2,g1,g2 being Element of REAL holds (p1+g1*)*(p2+g2*) =(p1*p2-g1*g2+(p1*g2+p2*g1)*) & (p2+g2*)*'=(p2+(-g2)*) proof let p1,p2,g1,g2 be Element of REAL; thus (p1+g1*)*(p2+g2*) =(p1*p2-g1*g2+(p1*g2+p2*g1)*); thus (p2+g2*)*' = p2-Im(p2+g2*)* by COMPLEX1:12 .= p2-g2* by COMPLEX1:12 .=(p2+(-g2)*); end; theorem Th3: for z being complex number holds z ExpSeq.(n+1) = z ExpSeq.n * z /(n+1+0*) & z ExpSeq.0=1 & |.(z ExpSeq).n .| = (|.z.| rExpSeq ).n proof let z be complex number; A1: now let n be Element of 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*)) by Th1 .=(z |^ n / (n! ) )*( z / (n+1+0*)) by XCMPLX_1:76 .=(z |^ n / (n! ) * z) / (n+1+0*) .=z ExpSeq.n * z /(n+1+0*) by Def4; end; A2: (z ExpSeq).0=z |^ 0 /(0! ) by Def4 .=1 by Th1,COMSEQ_3:def 1; defpred X[Element of 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*).|=n+1 by ABSVALUE:def 1; |. ((z ExpSeq)).(n+1) .| =|. z ExpSeq.n * z /(n+1+0*) .| by A1 .=|. z ExpSeq.n * z .|/|.(n+1+0*).| by COMPLEX1:67 .=(( |.z.| rExpSeq ).n) * |.z .|/|.(n+1+0*).| by A5,COMPLEX1:65 .= (|.z.| |^ n)/(n!) * |.z .|/|.(n+1+0*).| by Def5 .=( (|.z.| |^ n) * |.z .| )/( (n!) * |.(n+1+0*).| ) 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 1(A3,A4); hence thesis by A1,A2; end; theorem Th4: 0 < k implies (Shift(seq)).k=seq.(k-'1) proof assume A1: 0 < k; then A2: 0+1 <= k by INT_1:7; consider m be Nat such that A3: m+1=k by A1,NAT_1:6; A4: m=k-1 by A3; m in NAT by ORDINAL1:def 12; hence (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[Element of 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 1(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[Element of 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: (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)) by FUNCT_2:63 ; then A6: ( z+w) |^ (n+1) =( Partial_Sums(z (#) (Expan(n,z,w))) +Partial_Sums ((w (#) (Expan(n,z,w))))).n by A5,COMSEQ_3:27 .= Partial_Sums((z (#) Expan(n,z,w))).n +Partial_Sums((w (#) Expan(n,z,w))).n by VALUED_1:1; A7: 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 A8: Expan(n,z,w).(n+1)=0c by Def9; A9: 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; A10: 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 A11: Partial_Sums((z (#) Expan(n,z,w))).(n+1) =Partial_Sums(Shift((z (#) Expan(n,z,w)))).(n+1) +0c by A10,VALUED_1:6 .= Partial_Sums(Shift((z (#) Expan(n,z,w)))).(n+1); now let k be Element of NAT; A12: now assume A13: n+1 < k; A14: 0+1 <= n+1 by XREAL_1:6; A15: n+1-1 < k -1 by A13,XREAL_1:9; then A16: n+0 < k-1+1 by XREAL_1:8; A17: k-1 = k-'1 by A13,A14,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 A16,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 A16,Def9 .=0c + (z * 0c) by A15,A17,Def9 .=0c; hence ((w (#) Expan(n,z,w))+Shift((z (#) Expan(n,z,w)))).k =Expan(n+1,z,w).k by A13,Def9; end; now assume A18: k <= (n+1); A19: now assume A20: k=n+1; A21: n < n+1 by XREAL_1:29; A22: n-'n= n-n by XREAL_1:233 .= 0; A23: n+1-'(n+1)= n+1-(n+1) by XREAL_1:233 .= 0; A24: (Coef(n)).(n) = n! /((n! ) * (0! )) by A22,Def6 .= 1 by Th1,XCMPLX_1:60; A25: (Coef(n+1)).(n+1) = (n+1)! /(((n+1)! ) * (0! )) by A23,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 A20,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 A21,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 A24,A25,COMSEQ_3:def 1 .= Expan(n+1,z,w).k by A20,A22,A23,Def9; hence ((w (#) Expan(n,z,w))+Shift((z (#) Expan(n,z,w)))).k=Expan(n+1,z,w) . k; end; now assume A26: k < n+1; A27: now assume A28: k=0; A29: n-'0 =n-0 by XREAL_1:233; A30: n+1-'0 =n+1-0 by XREAL_1:233; A31: (Coef(n)).0 = n! /((0! ) * (n! )) by A29,Def6 .= 1 by Th1,XCMPLX_1:60; A32: (Coef(n+1)).0 = (n+1)! /((0! ) * ((n+1)! )) by A30,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 A28,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 A29 .= (Coef(n+1)).0 * (z |^ 0) * (w |^ (n+1-'0)) by A30,A31,A32,COMSEQ_3:def 1 .= Expan(n+1,z,w).k by A28,Def9; hence ((w (#) Expan(n,z,w))+Shift((z (#) Expan(n,z,w)))).k =Expan(n+1,z,w). k; end; now assume A33: k<>0; then A34: 0+1 <= k by INT_1:7; A35: k+1-1 <= n+1-1 by A26,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 A35,XXREAL_0:2; then A36: k-'1 <= n by A34,XREAL_1:233; A37: ((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 A33,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 A35,Def9 .=(w * ((Coef n).k * (z |^ k)) * (w |^ (n-'k))) + (z * ((Coef n).(k-'1) * (z |^ (k-'1)) * (w |^ (n-'(k-'1))))) by A36,Def9 .=((Coef n).k * (w * (z |^ k) * (w |^ (n-'k)) ) + ((Coef n).(k-'1) * ((z |^ (k-'1)) * z * (w |^ (n-'(k-'1)))))); A38: (n-'k)+1=n-k+1 by A35,XREAL_1:233 .=n+1-k .=n+1-'k by A26,XREAL_1:233; A39: n-'(k-'1)=n-(k-'1) by A36,XREAL_1:233 .=n-(k-1) by A34,XREAL_1:233 .=n+1-k .=n+1-'k by A26,XREAL_1:233; (k-'1)+1 =k-1+1 by A34,XREAL_1:233 .=k; then A40: ( w |^ (n-'k)) * w = w |^ (n-'k+1) & (z |^ (k-'1)) * z = z |^ k by COMSEQ_3:def 1 ; A41: (Coef n).k +(Coef n).(k-'1) =n! /((k!) * ((n-'k)!)) +(Coef n).(k-'1) by A35,Def6 .=n! /((k!) * ((n-'k)!)) +n! /(((k-'1)!) * (((n-'(k-'1)))! )) by A36,Def6; A42: ((k!) * ((n-'k)!)) * (n+1-k+0*) =(k!) * (((n-'k)!) * (n+1-k+0*)); A43: (((k-'1)!) * (((n-'(k-'1)))! )) * (k+0*) =(k+0*) * ((k-'1)!) * (((n-'(k-'1)))! ) .=(k!) * ((n+1-'k)!) by A33,A39,Th2; (n+1-k+0*) <>0c by A26; then A44: n ! /((k!) * ((n-'k)!)) =(n! * (n+1-k+0*)) /(((k!) * ((n-'k)!)) * (n+1-k+0*)) by XCMPLX_1:91 .=(n! * (n+1-k+0*))/((k!) * ((n+1-'k)!)) by A35,A42,Th2; n! /(((k-'1)!) * (((n-'(k-'1)))! )) =(n! * (k+0*))/((k!) * ((n+1-'k)! )) by A33,A43,XCMPLX_1:91; then (Coef n).k +(Coef n).(k-'1) =( n! * (n+1-k+k+(0+0)*)) / ((k!) * ((n+1-'k)!)) by A41,A44 .=((n+1)! ) / ((k!) * ((n+1-'k)!)) by Th1 .=(Coef(n+1)).k by A26,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 A37,A38,A39,A40 .=Expan(n+1,z,w).k by A26,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 A27; end; hence ((w (#) Expan(n,z,w))+Shift((z (#) Expan(n,z,w)))).k =Expan(n+1,z,w).k by A18,A19,XXREAL_0:1; end; hence ((w (#) Expan(n,z,w))+Shift((z (#) Expan(n,z,w)))).k =Expan(n+1,z,w).k by A12; end; then A45: (w (#) Expan(n,z,w))+Shift((z (#) Expan(n,z,w))) =Expan(n+1,z,w) by FUNCT_2:63; thus (z+w) |^ (n+1) =(Partial_Sums((w (#) Expan(n,z,w))) + Partial_Sums(Shift((z (#) Expan(n,z,w))))).(n+1) by A6,A7,A8,A9,A11,VALUED_1:1 .=Partial_Sums(Expan(n+1,z,w)).(n+1) by A45,COMSEQ_3:27; end; for n holds X[n] from NAT_1:sch 1(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 ) .| by A4,Th3 .=1 by COMPLEX1:44; end; for n being Nat holds X[n] from NAT_1:sch 2(A1,A2); then Partial_Sums(|.(0c qua complex number) ExpSeq.|) is constant by VALUED_0:def 18; then A5: |.(0c qua complex number) ExpSeq.| is summable by SERIES_1:def 2; defpred X[set] means Partial_Sums((0c qua complex number) ExpSeq).$1=1; Partial_Sums((0c qua complex number) ExpSeq).0 =((0c qua complex number) ExpSeq).0 by SERIES_1:def 1 .=1 by Th3; then A6: X[0]; A7: for n st X[n] holds X[n+1] proof let n such that A8: Partial_Sums((0c qua complex number) ExpSeq).n=1; thus Partial_Sums((0c qua complex number) ExpSeq).(n+1) =1r + ((0c qua complex number) ExpSeq).(n+1) by A8,SERIES_1:def 1 .=1r + ((0c qua complex number) ExpSeq.n) * 0c/(n+1+0*) by Th3 .=1; end; for n holds X[n] from NAT_1:sch 1(A6,A7); hence thesis by A5,COMSEQ_2:10,COMSEQ_3:def 9; end; registration let z be complex number; 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*)=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(Element of NAT) = |.(z ExpSeq).|.($1+1)/|.(z ExpSeq).|.$1; thus A6: for n holds X[n] from NAT_1:sch 1(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*)) /(z ExpSeq).n.| by Th3 .=|.((z ExpSeq).n * (z/(n+1+0*))) /(z ExpSeq).n.| .=|.(z/(n+1+0*)) .| by A6,XCMPLX_1:89 .=|.z.|/abs(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 now let l be Element of NAT; 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; 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; 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[Element of 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 1(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: (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 .=Partial_Sums((((Partial_Sums(w ExpSeq).k) (#) (z ExpSeq))) -(Alfa(k,z,w))).k by COMSEQ_3:28; for l be Element of 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 Element of NAT such that A2: l <= k; thus ( ( Partial_Sums(w ExpSeq).k) (#) (z ExpSeq) - (Alfa(k,z,w)) ).l =(( Partial_Sums(w ExpSeq).k) (#) (z ExpSeq)).l +(-Alfa(k,z,w)).l by VALUED_1:1 .=(( 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 A2,Def11 .=((z ExpSeq).l) * ( Partial_Sums(w ExpSeq).k -Partial_Sums(w ExpSeq).(k-'l) ) .=Conj(k,z,w).l by A2,Def13; end; hence thesis by A1,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[Element of 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 1(A2,A3); thus then |. Partial_Sums(( z ExpSeq)).k .| <= Partial_Sums((|.z.| rExpSeq)).k; now let k be set 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 by FUNCT_2:12; 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: abs((Partial_Sums(|.z .| rExpSeq)).n) = Partial_Sums(|.z .| rExpSeq).n & (n <= m implies abs((Partial_Sums(|.z .| rExpSeq).m-Partial_Sums(|.z .| rExpSeq).n)) = Partial_Sums(|.z .| rExpSeq).m-Partial_Sums(|.z .| rExpSeq).n) proof for n holds 0 <= (|. z .| rExpSeq).n by Th18; hence thesis by COMSEQ_3:9; end; theorem Th20: abs(Partial_Sums(|.Conj(k,z,w).|).n)=Partial_Sums(|.Conj(k,z,w).|).n proof A1: now let n; |.Conj(k,z,w).|.n=|.(Conj(k,z,w)).n.| by 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 number st p>0 ex n st for k st n <= k holds abs(Partial_Sums(|.Conj(k,z,w).|).k) < p proof let p be real number such that A1: p>0; reconsider pp = p as Real by XREAL_0:def 1; A2: 1 <= Sum(|.z.| 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 set 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 by FUNCT_2:12; then consider n1 such that A6: for k,l be Element of NAT st n1 <= k & n1 <= l holds abs(Partial_Sums(( |.z.| rExpSeq )).k - Partial_Sums(( |.z.| rExpSeq )).l) < p1 by A4,COMSEQ_3:4; consider n2 such that A7: for k,l be Element of 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 Element of 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 Element of NAT st l <= k holds |.Conj(k,z,w).|.l =(|.z.| rExpSeq).l * |.(Partial_Sums(w ExpSeq).k -Partial_Sums(w ExpSeq).(k-'l)).|; end; A10: now let k; now let l be Element of 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 Element of 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 Element of 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 Element of 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; abs((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 abs(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(Element of 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 number; assume p>0; then consider n such that A6: for k st n <= k holds abs(Partial_Sums(|.Conj(k,z,w).|).k) < p by Th21; take n; now let k such that A7: n <= k; abs(rseq.k-0)=abs(Partial_Sums(|.Conj(k,z,w).|).k) by A3; hence abs(rseq.k-0) < p by A6,A7; end; hence for k st n <= k holds abs(rseq.k-0) < p; end; 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 number holds Sum(z ExpSeq) * Sum(w ExpSeq) = Sum((z+w) ExpSeq) proof let z0,w0 be complex number; reconsider z=z0, w=w0 as Element of COMPLEX by XCMPLX_0:def 2; deffunc U(Element of 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; 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) by FUNCT_2:63; 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 number 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 number; 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 number holds f1.z=Sum(z ExpSeq); assume A3: for z being complex number 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 by FUNCT_2:63; end; end; definition let z be complex number; func exp z -> complex number equals exp.z; coherence; end; definition let z be complex number; redefine func exp z -> Element of COMPLEX; coherence by XCMPLX_0:def 2; end; theorem for z1, z2 being complex number holds exp(z1+z2)=exp(z1) *exp(z2) proof let z1,z2 be complex number; 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 definition func sin -> Function of REAL, REAL means :Def16: for d being Element of REAL holds it.d = Im(Sum(d* ExpSeq)); existence proof deffunc U(Element of REAL) = Im(Sum($1* 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; thus thesis by A1; end; uniqueness proof let f1,f2 be Function of REAL, REAL; assume A2: for d being Element of REAL holds f1.d=Im(Sum(d* ExpSeq)); assume A3: for d being Element of REAL holds f2.d=Im(Sum(d* 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*) ExpSeq)) by A2 .=f2.d by A3; end; hence f1=f2 by FUNCT_2:63; end; end; definition let th be real number; func sin th equals sin.th; coherence; end; registration let th be real number; cluster sin th -> real; coherence; end; definition let th be Real; redefine func sin th -> Real; coherence; end; reserve d for Real; definition func cos -> Function of REAL, REAL means :Def18: for d holds it.d = Re(Sum(d* ExpSeq)); existence proof deffunc U(Element of REAL) = Re(Sum(($1*) 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; thus thesis by A1; end; uniqueness proof let f1,f2 be Function of REAL, REAL; assume A2: for d holds f1.d=Re(Sum(d* ExpSeq)); assume A3: for d holds f2.d=Re(Sum(d* ExpSeq)); for d holds f1.d=f2.d proof let d; thus f1.d=Re(Sum((d*) ExpSeq)) by A2 .=f2.d by A3; end; hence f1=f2 by FUNCT_2:63; end; end; definition let th be real number; func cos th equals cos.th; coherence; end; registration let th be real number; cluster cos th -> real; coherence; end; definition let th be Real; redefine func cos th -> Real; coherence; end; theorem Th24: dom(sin)=REAL & dom(cos)=REAL by FUNCT_2:def 1; Lm3: Sum(th* ExpSeq)=cos.(th)+(sin.th)* proof Im (Sum(th* ExpSeq))=sin.(th) & Re(Sum(th* ExpSeq))=cos.(th) by Def16,Def18; hence thesis by COMPLEX1:13; end; theorem exp(th*)=cos(th)+(sin th)* proof exp(th*)=Sum(th* ExpSeq ) by Def14 .=cos(th)+(sin th)* by Lm3; hence thesis; end; Lm4: (Sum((th*) ExpSeq))*' = Sum((-(th*)) ExpSeq) proof Partial_Sums(((th*) ExpSeq))*' =Partial_Sums((-(th*)) ExpSeq) proof A1: for n holds (((th*) ExpSeq).n)*' = ((-(th*)) ExpSeq).n proof defpred X[Element of NAT] means (((th*) ExpSeq).$1)*' = ((-(th*)) ExpSeq).$1; (((th*) ExpSeq).0)*' =1r by Th3,COMPLEX1:30 .=((-(th*)) ExpSeq).0 by Th3; then A2: X[0]; A3: for n st X[n] holds X[n+1] proof let n; assume A4: ((th* ExpSeq).n)*' = ((-(th*)) ExpSeq).n; thus (((th*) ExpSeq).(n+1))*' =(((th*) ExpSeq).n * (th*)/(n+1+0*))*' by Th3 .=((th* ExpSeq).n * ((th*)/(n+1+0*)))*' .=((-(th*)) ExpSeq).n * ((th*)/(n+1))*' by A4,COMPLEX1:35 .=((-(th*)) ExpSeq).n * ((0+th*)*'/((n+1))*') by COMPLEX1:37 .=((-(th*)) ExpSeq).n * ((0+(-th)*) /(n+1+0*)*') by Lm1 .=((-(th*)) ExpSeq).n * ((0+(-th)*)/(n+1+(-0)*)) by Lm1 .=((-(th*)) ExpSeq).n * (-(th*))/(n+1+0*) .=((-(th*)) ExpSeq).(n+1) by Th3; end; thus for n holds X[n] from NAT_1:sch 1(A2,A3); end; defpred X[Element of NAT] means (Partial_Sums(((th*) ExpSeq))*').$1 =Partial_Sums((-(th*)) ExpSeq).$1; (Partial_Sums((th*) ExpSeq)*').0 =(Partial_Sums((th*) ExpSeq).0)*' by COMSEQ_2:def 2 .=(((th*) ExpSeq).0)*' by SERIES_1:def 1 .=1 by Th3,COMPLEX1:30 .=((-(th*)) ExpSeq).0 by Th3 .=Partial_Sums((-(th*)) ExpSeq).0 by SERIES_1:def 1; then A5: X[0]; A6: for n st X[n] holds X[n+1] proof let n such that A7: (Partial_Sums(((th*) ExpSeq))*').n =Partial_Sums((-(th*)) ExpSeq).n; thus (Partial_Sums((th*) ExpSeq)*').(n+1) =(Partial_Sums((th*) ExpSeq).(n+1))*' by COMSEQ_2:def 2 .=(Partial_Sums((th*) ExpSeq).n+((th*) ExpSeq).(n+1))*' by SERIES_1:def 1 .=(Partial_Sums((th*) ExpSeq).n)*'+(((th*) ExpSeq).(n+1))*' by COMPLEX1:32 .=Partial_Sums((-(th*)) ExpSeq).n+(((th*) ExpSeq).(n+1))*' by A7,COMSEQ_2:def 2 .=Partial_Sums((-(th*)) ExpSeq).n+((-(th*)) ExpSeq).(n+1) by A1 .=Partial_Sums((-(th*)) ExpSeq).(n+1) by SERIES_1:def 1; end; for n holds X[n] from NAT_1:sch 1(A5,A6); hence thesis by FUNCT_2:63; end; hence thesis by COMSEQ_2:12; end; theorem (exp((th*)))*'=exp(-(th*)) proof (exp((th*)))*'=(Sum((th*) ExpSeq))*' by Def14 .=Sum((-(th*)) ExpSeq) by Lm4 .=exp(-(th*)) by Def14; hence thesis; end; Lm5: for th1 being real number st th = th1 holds |.Sum(th* ExpSeq ).| = 1 & abs(sin.th1) <= 1 & abs(cos.th1) <= 1 proof let th1 be real number such that A1: th = th1; A2: Sum((th*) ExpSeq ) * Sum((-(th*)) ExpSeq ) =Sum(((th*)+(-(th*))) ExpSeq ) by Lm2 .=1r by Th9; |.Sum((th*) ExpSeq ).| * |.Sum((th*) ExpSeq ).| =|.Sum((th*) ExpSeq )*Sum((th*) ExpSeq ).| by COMPLEX1:65 .=|.Sum((th*) ExpSeq ) * Sum((th*) ExpSeq)*'.| by COMPLEX1:69 .=1 by A2,Lm4,COMPLEX1:48; then A3: |.Sum((th*) ExpSeq ).| =1/|.Sum((th*) ExpSeq ).| & |.Sum((th*) ExpSeq ).| <> 0 by XCMPLX_1:73; |.Sum((th*) ExpSeq ).| <> -1 by COMPLEX1:46; thus then A4: |.Sum(th* ExpSeq ).|=1 by A3,XCMPLX_1:199; abs (sin.th)=abs(Im(Sum((th*) ExpSeq ))) & abs(cos.th)=abs(Re(Sum((th*) ExpSeq ))) by Def16,Def18; hence thesis by A1,A4,COMSEQ_3:13; end; theorem |.exp((th*)).| = 1 & for th being real number holds abs(sin th) <= 1 & abs(cos th) <= 1 proof thus |.exp((th*)).| =|.Sum((th*) ExpSeq ).| by Def14 .=1 by Lm5; let th be real number; A1: th is Real by XREAL_0:def 1; hence abs(sin(th)) <= 1 by Lm5; thus thesis by A1,Lm5; end; reserve th,th1,th2 for real number; theorem Th28: (cos.th)^2+(sin.th)^2=1 & (cos.th)*(cos.th)+(sin.th)*(sin.th)=1 proof reconsider th1=th as Real by XREAL_0:def 1; A1: Sum((th1*) ExpSeq ) * Sum((-(th1*)) ExpSeq ) =Sum(((th1*)+(-(th1*))) ExpSeq ) by Lm2 .=1r by Th9; thus (cos.(th))^2+(sin.(th))^2 =(Re(Sum((th1*) ExpSeq )))^2+(sin.(th))^2 by Def18 .=(Re(Sum((th1*) ExpSeq )))^2+(Im(Sum((th1*) ExpSeq )))^2 by Def16 .=|.Sum((th1*) ExpSeq )*Sum((th1*) ExpSeq ).| by COMPLEX1:68 .=|.Sum((th1*) ExpSeq ) * Sum((th1*) 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* ExpSeq)) by Def18 .= 1 by Th9,COMPLEX1:6; thus sin.0 = Im(Sum(0* ExpSeq)) by Def16 .= 0 by Th9,COMPLEX1:6; reconsider th1=th as Real by XREAL_0:def 1; thus cos.(-th) = Re( Sum((-0+(-th1)*) ExpSeq) ) by Def18 .= Re( Sum((-(th1*)) ExpSeq) ) .= Re(Sum((th1*) ExpSeq)*') by Lm4 .= Re((cos.(th)+(sin.th)*)*') by Lm3 .= Re(cos.(th)+(-sin.th)*) by Lm1 .= cos.(th) by COMPLEX1:12; thus sin.(-th) = Im( Sum((-0+(-th1)*) ExpSeq) ) by Def16 .= Im( Sum((-(th1*)) ExpSeq) ) .= Im(Sum((th1*) ExpSeq)*') by Lm4 .= Im((cos.(th)+(sin.th)*)*') by Lm3 .= Im(cos.(th)+(-sin.th)*) 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 number; deffunc U(Element of 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 thus for s1,s2 being Real_Sequence st (for x being Element of NAT holds s1.x = U(x)) & (for x being Element of NAT holds s2.x = U(x)) holds s1 = s2 from BINOP_2:sch 1; end; deffunc U(Element of 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 thus for s1,s2 being Real_Sequence st (for x being Element of NAT holds s1.x = U(x)) & (for x being Element of NAT holds s2.x = U(x)) holds s1 = s2 from BINOP_2:sch 1; end; end; theorem Th32: for z being complex number, k holds z|^ (2*k) = (z|^ k)|^ 2& z|^ (2*k)= (z|^ 2)|^ k proof let z be complex number, k; defpred X[Element of 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 by NEWTON:5 .= 1|^(1+1) by NEWTON:6 .= (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 1(A2,A3); hence thesis; end; theorem Th33: for th being Real holds (th*) |^ (2*k)=(-1)|^ k* (th |^ (2*k)) & (th*) |^ (2*k+1)=(-1)|^ k* (th |^ (2*k+1))* proof let th be Real; A1: (-1)|^ 0* (th |^ (2*0))*=(-1)|^ 0* th GeoSeq.0* by PREPOWER:def 1 .=(-1)|^ 0*(1)* by PREPOWER:3 .=(-1)GeoSeq.0* by PREPOWER:def 1 .=1* by PREPOWER:3; A2: (th*) |^ (2*0+1)=(th*) GeoSeq.0*(th*) by COMSEQ_3:def 1 .=1*(th*) by COMSEQ_3:def 1 .=(th*); defpred X[Element of NAT] means (th*) |^ (2*$1)=(-1)|^ $1* (th |^ (2*$1)) & (th*) |^ (2*$1+1)=(-1)|^ $1* (th |^ (2*$1+1))*; (-1)|^ 0 * (th |^ (2*0+1))*=(-1)|^ 0 * (th GeoSeq.(2*0+1))* by PREPOWER:def 1 .= (-1)|^ 0* (th GeoSeq.0*th)* by PREPOWER:3 .=(-1)|^ 0* (1*th)* by PREPOWER:3 .= ((-1)GeoSeq.0)* th * by PREPOWER:def 1 .=(1)* th * by PREPOWER:3 .=(th*); then A3: X[0] by A1,A2,COMSEQ_3:def 1; A4: for k st X[k] holds X[k+1] proof let k; assume that A5: (th*) |^ (2*k)=(-1)|^ k* (th |^ (2*k)) and A6: (th*) |^ (2*k+1)=(-1)|^ k* (th |^ (2*k+1))*; A7: (th*) |^ (2*(k+1))= ((th*) |^ 2)|^(k+1) by Th32 .=((th*) |^ 2)|^ k * ((th*) |^ 2) by COMSEQ_3:def 1 .= (-1)|^ k* (th |^ (2*k))* ((th*)GeoSeq.(1+1)) by A5,Th32 .=(-1)|^ k* (th |^ (2*k))* ((th*)GeoSeq.(0+1)*(th*)) by COMSEQ_3:def 1 .=(-1)|^ k* (th |^ (2*k))* ((th*)GeoSeq.0*(th*) *(th*)) by COMSEQ_3:def 1 .= (-1)|^ k* (th |^ (2*k))* (1r*(th*)*(th*)) 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*) |^ (2*(k+1)+1)= (th*)GeoSeq.(2*k+1+1)*(th*) by COMSEQ_3:def 1 .=(th*)GeoSeq.(2*k+1)*(th*)*(th*) by COMSEQ_3:def 1 .=(-1)|^ k*(-1)* (th |^ (2*k+1))*th*th* by A6 .=(-1)GeoSeq.k*(-1)* (th |^ (2*k+1))*th*th* by PREPOWER:def 1 .=(-1)GeoSeq.(k+1)* (th |^ (2*k+1))*th*th* by PREPOWER:3 .=(-1)|^ (k+1)* (th |^ (2*k+1))*th*th* by PREPOWER:def 1 .=(-1)|^ (k+1)* (th GeoSeq.(2*k+1))*th*th* by PREPOWER:def 1 .=(-1)|^ (k+1)* (th GeoSeq.(2*k+1)*th)*th* .=(-1)|^ (k+1)* (th GeoSeq.(((2*k+1)+1)))*th* by PREPOWER:3 .=(-1)|^ (k+1)* (th GeoSeq.((2*k+1+1))*th)* .= (-1)|^ (k+1)* (th GeoSeq.(2*(k+1)+1))* by PREPOWER:3 .=(-1)|^ (k+1)*(th |^ (2*(k+1)+1))* by PREPOWER:def 1; hence thesis by A7; end; for k holds X[k] from NAT_1:sch 1(A3,A4); hence thesis; end; theorem n! = n!; theorem Th35: for th being Real holds Partial_Sums(th P_sin).n = Partial_Sums(Im ((th*) ExpSeq)).(2*n+1) & Partial_Sums(th P_cos).n = Partial_Sums(Re ((th*) ExpSeq)).(2*n) proof let th be Real; 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: (th)|^ (2*0+1)= th GeoSeq.(0+1) by PREPOWER:def 1 .= th GeoSeq.0 * th by PREPOWER:3 .= 1* th by PREPOWER:3 .= th; A3: ((2*0+1)!)= 0! * 1 by NEWTON:15 .= 1 by NEWTON:12; A4: (-1)|^ 0 = (-1) GeoSeq.0 by PREPOWER:def 1 .= 1 by PREPOWER:3; A5: 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 A4,NEWTON:12,PREPOWER:def 1 .=1 by PREPOWER:3; A6: ( Im ((th*) ExpSeq)).0= Im (((th*) ExpSeq).0) & (Im ((th*) ExpSeq)). 1= Im (((th*) ExpSeq).1) by COMSEQ_3:def 6; A7: (th*) = 0+th*; A8: Partial_Sums(Im ((th*) ExpSeq)).(2*0+1) = Partial_Sums(Im ((th*) ExpSeq)).0 + (Im ((th*) ExpSeq)).1 by SERIES_1:def 1 .= (Im ((th*) ExpSeq)).0+ (Im ((th*) ExpSeq)).1 by SERIES_1:def 1 .= 0 + Im (((th*) ExpSeq).(0+1)) by A6,Th3,COMPLEX1:6 .=0 + Im ((((th*) ExpSeq).0)* (th*) /(0+1+0*)) by Th3 .= Im (1* (th*) /1) by Th3 .=th by A7,COMPLEX1:12; defpred X[Element of NAT] means Partial_Sums(th P_sin).$1 = Partial_Sums(Im ((th*) ExpSeq)).(2*$1+1) & Partial_Sums(th P_cos).$1 = Partial_Sums(Re ((th*) ExpSeq)).(2*$1); Partial_Sums(Re ((th*) ExpSeq)).(2*0) = (Re ((th*) ExpSeq)).0 by SERIES_1:def 1 .= Re (((th*) ExpSeq).0) by COMSEQ_3:def 5 .=1 by Th3,COMPLEX1:6; then A9: X[0] by A1,A2,A3,A4,A5,A8; A10: for k st X[k] holds X[k+1] proof let k be Element of NAT; assume that A11: Partial_Sums(th P_sin).k = Partial_Sums(Im ((th*) ExpSeq)).(2*k+1) and A12: Partial_Sums(th P_cos).k = Partial_Sums(Re ((th*) ExpSeq)).(2*k); Partial_Sums(Im ((th*) ExpSeq)).(2*(k+1)+1) = Partial_Sums(Im ((th*) ExpSeq)).((2*k+1)+1) + (Im ((th*) ExpSeq)).(2*(k+1)+1) by SERIES_1:def 1 .= Partial_Sums(th P_sin).k + (Im((th*) ExpSeq)).(2*(k+1))+(Im ((th*) ExpSeq)).(2*(k+1)+1) by A11,SERIES_1:def 1 .= Partial_Sums(th P_sin).k + Im (((th*) ExpSeq).(2*(k+1)))+(Im((th*) ExpSeq)).(2*(k+1)+1) by COMSEQ_3:def 6 .=Partial_Sums(th P_sin).k + Im (((th*) ExpSeq).(2*(k+1)))+Im(((th*) ExpSeq).(2*(k+1)+1)) by COMSEQ_3:def 6 .= Partial_Sums(th P_sin).k + Im((th*) |^ (2*(k+1))/((2*(k+1))!))+ Im(((th*) ExpSeq).(2*(k+1)+1)) by Def4 .= Partial_Sums(th P_sin).k + Im((th*) |^ (2*(k+1))/((2*(k+1))!))+ Im((th*) |^ (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*) |^ (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))*/((2*(k+1)+1)!)) by Th33; then Partial_Sums(Im ((th*) ExpSeq)).(2*(k+1)+1) = Partial_Sums(th P_sin).k + Im( (((-1)|^ (k+1)* (th |^ (2*(k+1))))/((2*(k+1))!)+0/((2*(k+1))!)*)) + Im( ((-1)|^ (k+1)* (th |^ (2*(k+1)+1))*)/((2*(k+1)+1)!)); then Partial_Sums(Im ((th*) 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)!)*) 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 A13: Partial_Sums(Im ((th*) 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*) ExpSeq)).(2*(k+1)) = Partial_Sums(Re ((th*) ExpSeq)).(2*k+1)+ (Re ((th*) ExpSeq)).((2*k+1)+1) by SERIES_1:def 1 .=Partial_Sums(th P_cos).k + (Re ((th*) ExpSeq)).(2*k+1)+ (Re ((th*) ExpSeq)).((2*k+1)+1) by A12,SERIES_1:def 1 .= Partial_Sums(th P_cos).k + Re (((th*) ExpSeq).(2*k+1))+ (Re ((th*) ExpSeq)).((2*k+1)+1) by COMSEQ_3:def 5 .= Partial_Sums(th P_cos).k + Re (((th*) ExpSeq).(2*k+1))+ Re (((th*) ExpSeq).((2*k+1)+1)) by COMSEQ_3:def 5 .=Partial_Sums(th P_cos).k + Re ((th*)|^ (2*k+1)/ ((2*k+1)!))+ Re (((th*) ExpSeq).((2*k+1)+1)) by Def4 .= Partial_Sums(th P_cos).k + Re ((th*)|^ (2*k+1)/ ((2*k+1)!))+ Re ((th*)|^ (2*(k+1))/(((2*k+1)+1)!)) by Def4 .= Partial_Sums(th P_cos).k + Re ( (-1)|^ k* (th |^ (2*k+1))*/((2*k+1)!))+ Re ((th*)|^ (2*(k+1))/((2*(k+1))!)) by Th33 .= Partial_Sums(th P_cos).k + Re ( (-1)|^ k* (th |^ (2*k+1))*/((2*k+1)!))+ Re ((-1)|^ (k+1)* (th |^ (2*(k+1)))/((2*(k+1))!)) by Th33; then Partial_Sums(Re ((th*) ExpSeq)).(2*(k+1)) = Partial_Sums(th P_cos).k + Re ( (0/((2*k+1)!)+((-1)|^ k* (th |^ (2*k+1)))/((2*k+1)!)*)) + Re ((-1)|^ (k+1)* (th |^ (2*(k+1)))/((2*(k+1))!)); then Partial_Sums(Re ((th*) 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))!))*) 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*) 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 A13; end; thus for n holds X[n] from NAT_1:sch 1(A9,A10); end; hence thesis; end; theorem Th36: for th being Real holds Partial_Sums(th P_sin) is convergent & Sum(th P_sin)=Im(Sum ((th*) ExpSeq)) &Partial_Sums(th P_cos) is convergent & Sum(th P_cos)=Re(Sum ((th*) ExpSeq)) proof let th be Real; A1: Sum(((th*) ExpSeq)) =Sum(Re ((th*) ExpSeq))+Sum(Im ((th*) ExpSeq))* by COMSEQ_3:53; then A2: Sum(Re ((th*) ExpSeq))= Re (Sum(((th*) ExpSeq))) by COMPLEX1:12; A3: Sum(Im ((th*) ExpSeq))=Im (Sum(((th*) ExpSeq))) by A1,COMPLEX1:12; A4: Partial_Sums (Re ((th*) ExpSeq)) is convergent & lim Partial_Sums(Re ((th* ) ExpSeq))= Re (Sum(((th*) ExpSeq))) by A2,SERIES_1:def 2,def 3; A5: Partial_Sums (Im ((th*) ExpSeq)) is convergent & lim Partial_Sums(Im ((th* ) ExpSeq))=Im (Sum(((th*) ExpSeq))) by A3,SERIES_1:def 2,def 3; A6: now let p be real number; assume p>0; then consider n such that A7: for k st n <= k holds abs(Partial_Sums(Re ((th*) ExpSeq)).k- Re (Sum(((th*) ExpSeq)))) < p by A4,SEQ_2:def 7; take n; now let k such that A8: n <= k; abs (Partial_Sums(th P_cos).k-Re (Sum(((th*) ExpSeq)))) =abs(Partial_Sums( Re ((th*) ExpSeq)).(2*k)- Re (Sum(((th*) ExpSeq)))) & 2*k=k+k by Th35; hence abs(Partial_Sums(th P_cos).k-Re (Sum(((th*) ExpSeq)))) < p by A7,A8,NAT_1:12; end; hence for k st n <= k holds abs(Partial_Sums(th P_cos).k-Re (Sum(((th*) 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*) ExpSeq)) by A6, SEQ_2:def 7; A10: now let p be real number; assume p>0; then consider n such that A11: for k st n <= k holds abs(Partial_Sums(Im ((th*) ExpSeq)).k- Im (Sum(((th*) ExpSeq)))) < p by A5,SEQ_2:def 7; take n; now let k such that A12: n <= k; A13: abs(Partial_Sums(th P_sin).k-Im (Sum(((th*) ExpSeq)))) =abs(Partial_Sums(Im ((th*) ExpSeq)).(2*k+1)- Im (Sum(((th*) ExpSeq)))) by Th35; 2*k=k+k; then n <= 2*k by A12,NAT_1:12; then n<2*k+1 by NAT_1:13; hence abs(Partial_Sums(th P_sin).k-Im (Sum(((th*) ExpSeq)))) < p by A11,A13; end; hence for k st n <= k holds abs(Partial_Sums(th P_sin).k-Im (Sum(((th*) ExpSeq)))) < p; end; then Partial_Sums(th P_sin) is convergent by SEQ_2:def 6; then lim(Partial_Sums(th P_sin))=Im(Sum ((th*) ExpSeq)) by A10,SEQ_2:def 7; hence thesis by A6,A9,A10,SEQ_2:def 6,SERIES_1:def 3; end; theorem Th37: cos.th=Sum(th P_cos) & sin.th=Sum(th P_sin) proof reconsider th as Real by XREAL_0:def 1; sin.th = Im(Sum((th*) ExpSeq)) & cos.th=Re(Sum((th*) ExpSeq)) by Def16 ,Def18; hence thesis by Th36; 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 n0 proof let l; defpred X[Element of 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 1(A4,A5); hence thesis; end; then A7: rseq is non-decreasing by SEQM_3:def 8; n!=rseq.n & k! = rseq.k by A3; hence thesis by A1,A7,SEQM_3:6; end; theorem Th40: 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[Element of 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 1(A4,A5); hence thesis; end; then A7: th GeoSeq is non-increasing by SEQM_3:def 9; th |^ k=th GeoSeq. k & th |^ n=th GeoSeq. n by PREPOWER:def 1; hence thesis by A3,A7,SEQM_3:8; end; theorem for th being Real holds th |^ n /(n!)=(th|^ n) /(n!); theorem Th42: for p being real number holds Im(Sum(p ExpSeq))=0 proof let p be real number; A1: for n holds (Partial_Sums(Im(p ExpSeq))).n=0 proof let n; defpred X[Element of 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*) .=0 by COMPLEX1:12; hence thesis; end; for n holds X[n] from NAT_1:sch 1(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; n in NAT by ORDINAL1:def 12; then 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))*)) by COMSEQ_3:53 .= Sum(Im (p ExpSeq )) by COMPLEX1:12; hence thesis by A4,SERIES_1:def 3; end; theorem Th43: cos.1>0 & sin.1>0 & cos.1=1/2 proof let n; defpred X[Element of 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:4,12 .=1+ (-1)* (1)|^ (2*1)/((2*1)!) by NEWTON:5 .=1+ (-1)*1/((2*1)!) by NEWTON:10 .=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; assume A6: ((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; then A7: ( (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); A8: (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)))!) by NEWTON:10; A9: (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))!) by NEWTON:10 .=(-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 Th39; 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 A7,A8,A9,XREAL_1:49; hence thesis by A6,XXREAL_0:2; end; for n holds X[n] from NAT_1:sch 1(A4,A5); hence thesis; end; then A10: cos.1>=1/2 by A1,A3,PREPOWER:1,SEQ_4:16; A11: Partial_Sums(1 P_sin) is convergent by Th36; A12: sin.1=Sum(1 P_sin) by Th37; lim ((Partial_Sums(1 P_sin))*bq )=lim(Partial_Sums(1 P_sin)) by A11,SEQ_4:17; then A13: lim ((Partial_Sums(1 P_sin))*bq )= sin.1 by A12,SERIES_1:def 3; for n holds ((Partial_Sums(1 P_sin))*bq).n >=5/6 proof let n; defpred X[Element of 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)!) by NEWTON:5 .=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:5,12 .=1+ (-1)*1/((2*1+1)!) by NEWTON:10 .=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 A14: X[0]; A15: for k st X[k] holds X[k+1] proof let k; assume A16: ((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; then A17: ( (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); A18: (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)!) by NEWTON:10; A19: (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)!) by NEWTON:10 .=(-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 Th39; 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 A17,A18,A19,XREAL_1:49; hence thesis by A16,XXREAL_0:2; end; for n holds X[n] from NAT_1:sch 1(A14,A15); hence thesis; end; then A20: sin.1>=5/6 by A11,A13,PREPOWER:1,SEQ_4:16; A21: (cos.(1))^2+(sin.(1))^2=1 by Th28; A22: (sin.(1))^2>=(5/6)^2 by A20,SQUARE_1:15; then 1-(1-(cos.(1))^2)<=1-25/36 by A21,XREAL_1:10; then (cos.(1))^2<25/36 by XXREAL_0:2; then (sin.(1))^2> (cos.(1))^2 by A22,XXREAL_0:2; then A23: sqrt(cos.(1))^2)) by Def4 .=Re((th|^ n) /(n!)+0*) .=(th|^ n) /(n!) by COMPLEX1:12 .=(th rExpSeq).n by Def5; hence thesis; end; hence thesis by FUNCT_2:63; end; theorem Th45: for th being Real holds th rExpSeq is summable & Sum(th rExpSeq)=Re(Sum(th ExpSeq)) proof let th be Real; Sum(th ExpSeq) =Sum(Re (th ExpSeq))+(Sum(Im (th ExpSeq)))* & Sum(th rExpSeq)=Sum(Re (th ExpSeq)) by Th44,COMSEQ_3:53; hence thesis by Th44,COMPLEX1:12; end; Lm8: for z being complex number holds z ExpSeq.1=z & z ExpSeq.0=1r & |.z |^ n.|=|.z.| |^n proof let z be complex number; A1: z in COMPLEX by XCMPLX_0:def 2; z|^1=z by NEWTON:5; then A2: z ExpSeq.1= z/(1!) by Def4 .=z by NEWTON:13; A3: z ExpSeq.0=z|^ 0/ (0!) by Def4 .=1r by A1,Th1,COMSEQ_3:11; |.z |^ n.|=|.z.| |^ n proof defpred X[Element of NAT] means |.z |^ $1.|=|.z.| |^ $1; |.z |^ 0 .|=1 by COMPLEX1:48,COMSEQ_3:def 1; then A4: X[0] by NEWTON:4; A5: for k st X[k] holds X[k+1] proof let k such that A6: |.z |^ k.|=|.z.| |^ k; |.z |^ (k+1).|=|.z*(z GeoSeq.k).| by COMSEQ_3:def 1 .=|.z.| |^ k *|.z.| by A6,COMPLEX1:65 .=|.z.| |^(k+1) by NEWTON:6; hence thesis; end; for n holds X[n] from NAT_1:sch 1(A4,A5); hence thesis; end; hence thesis by A2,A3; end; Lm9: for th being Real holds Sum(th ExpSeq)=Sum(th rExpSeq) proof let th be Real; A1: for n being Nat holds Im(Partial_Sums(th ExpSeq)).n=0 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; A5: n in NAT by ORDINAL1:def 12; 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 A5,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,A5,COMSEQ_3:def 6 .=Im((th|^ (n+1)) /((n+1)!)+0*) 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* by COMPLEX1:13 .=Sum(th rExpSeq) by Th45; hence thesis; end; theorem Th46: for p,q being real number holds Sum((p+q) rExpSeq) = (Sum(p rExpSeq))*(Sum(q rExpSeq)) proof let p,q be real number; reconsider p,q as Real by XREAL_0:def 1; Sum((p+q) rExpSeq)=Re(Sum((p+q) ExpSeq)) by Th45 .=Re((Sum(p ExpSeq)) *(Sum(q ExpSeq))) by Lm2 .=Re((Re(Sum(p ExpSeq))+Im(Sum(p ExpSeq))*)*(Sum(q ExpSeq))) by COMPLEX1:13 .= Re((Re(Sum(p ExpSeq))+Im(Sum(p ExpSeq))*)* (Re(Sum(q ExpSeq))+Im(Sum(q ExpSeq))*)) by COMPLEX1:13 .= Re((Sum(p rExpSeq)+Im(Sum(p ExpSeq))*)* (Re(Sum(q ExpSeq))+Im(Sum(q ExpSeq))*)) by Th45 .= Re((Sum(p rExpSeq)+0*)* (Re(Sum(q ExpSeq))+Im(Sum(q ExpSeq))*)) by Th42 .= Re(Sum(p rExpSeq)*(Sum(q rExpSeq)+Im(Sum(q ExpSeq))*)) by Th45 .= Re(Sum(p rExpSeq)*(Sum(q rExpSeq)+0*)) by Th42 .= Re((Sum(p rExpSeq))*(Sum(q rExpSeq))+0*) .= (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 number holds it.d = Sum(d rExpSeq); existence proof deffunc U(Element of REAL) = Sum($1 rExpSeq); 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 number; d in REAL by XREAL_0:def 1; hence thesis by A1; end; uniqueness proof let f1,f2 be Function of REAL, REAL; assume A2: for d being real number holds f1.d=Sum(d rExpSeq); assume A3: for d being real number 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 by FUNCT_2:63; end; end; definition let th be real number; func exp_R th equals exp_R.th; coherence; end; registration let th be real number; cluster exp_R th -> real; coherence; end; definition let th be Real; redefine func exp_R th -> Real; coherence; end; theorem Th47: dom(exp_R)=REAL by FUNCT_2:def 1; theorem Th48: for th being Real holds exp_R.th = Re(Sum(th ExpSeq)) proof let th be Real; exp_R.th = Sum(th rExpSeq) by Def22; hence thesis by Th45; end; theorem for th being Real holds exp th=exp_R th proof let th be Real; 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 number holds exp_R.(p+q) = exp_R.p * exp_R.q proof let p,q be real number; exp_R.(p+q) = Sum((p+q) rExpSeq) by Def22 .= (Sum(p rExpSeq))*(Sum(q rExpSeq)) by Th46 .=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 number 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,Th45,COMPLEX1:6; hence thesis; end; theorem exp_R(0) =1 by Lm11; theorem Th52: 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[Element of 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 1(A3,A4); hence thesis; end; th is Real by XREAL_0:def 1; then th rExpSeq is summable by Th45; 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 Th53: th < 0 implies 0=1 by Th52; 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 00 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 Th53; end; suppose th>0; hence thesis by Th52; end; end; hence thesis; end; end; hence thesis; end; theorem exp_R(th)>0 by Th54; begin :: Differential of sin, cos, and Exponential Function definition let z be complex number; deffunc U(Element of NAT) = (z#N($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 thus for s1,s2 being Complex_Sequence st (for x being Element of NAT holds s1.x = U(x)) & (for x being Element of NAT holds s2.x = U(x)) holds s1 = s2 from BINOP_2:sch 1; end; deffunc U(Element of NAT) = (z#N($1))/(($1+2)!); func z P_t -> Complex_Sequence means for n holds it.n = (z#N(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 thus for s1,s2 being Complex_Sequence st (for x being Element of NAT holds s1.x = U(x)) & (for x being Element of NAT holds s2.x = U(x)) holds s1 = s2 from BINOP_2:sch 1; end; end; Lm12: for p being Real, z being complex number holds Re(p**z)=-p*Im z & Im(p**z)=p*Re z &Re(p*z)=p*Re z & Im(p*z)=p*Im z proof let p being Real, z be complex number; A1: (p**z) =p**(Re z+Im z*) by COMPLEX1:13 .=-p* Im z+(p*Re z)*; (p*z) =(p*(Re z+Im z*)) by COMPLEX1:13 .=p* Re z+(p*Im z)*; hence thesis by A1,COMPLEX1:12; end; Lm13: for p being real number, z being complex number st p>0 holds Re(z/(p*))=Im z /p & Im(z/(p*))=-Re z /p &|.z/p.|=|.z.|/p proof let p be real number, z being complex number such that A1: p>0; A2: Re(0+p*)=0 & Im(0+p*)=p by COMPLEX1:12; A3: Im(p+0*)=0 by COMPLEX1:12; A4: z/(p*) = (Re z * 0 + Im z * p) / (0^2 + p^2) + (0 * Im z - Re z * p) / (0^2 + p^2)* by A2,COMPLEX1:def 10 .=(Im z * p)/(p*p)+ ((-Re z) * p)/(p*p)* .=(Im z * p)/(p*p)+(-Re z) /p * by A1,XCMPLX_1:91 .=Im z /p+(-Re z /p)* 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 Th56: for z being complex number holds z P_dt is absolutely_summable proof let z be complex number; ex r st for n holds Partial_Sums(|.z P_dt.|).n=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 1(A4,A5); hence thesis; end; consider r be real number such that A11: for n holds Partial_Sums(|.z ExpSeq.|).n0 holds ex q st q>0 & for z being complex number st |.z.|=1 & |.z.| |^(n+1) >=0 by Th39,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 number; assume A9: p0>0; reconsider p = p0 as Real by XREAL_0:def 1; 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.|0 by A14,XREAL_1:50; then |.z.|/(1- |.z.|)< p*(1- |.z.|)/(1- |.z.|) by A23,XREAL_1:74; then |.z.|/(1- |.z.|)

0 by A9,A10; let z being complex number; z in COMPLEX by XCMPLX_0:def 2; hence thesis by A12; end; theorem Th59: for z,z1 being complex number 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 number; (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 Th57 .=(Sum(z1 ExpSeq))*z +z*(Sum(z P_dt))*(Sum(z1 ExpSeq)); hence thesis; end; theorem Th60: for p,q being Real holds cos.(p+q)-cos.p= -q*sin.p -q*Im((Sum(q* P_dt))* (cos.p+(sin.p)*)) proof let p,q be Real; cos.(p+q)-cos.p=cos.(p+q)-Re(Sum(p* ExpSeq)) by Def18 .=Re(Sum((p+q)* ExpSeq))-Re(Sum(p* ExpSeq)) by Def18 .=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 Th59 .=Re((cos.p+(sin.p)*)*(q*) +q**(Sum(q* P_dt))*(Sum(p* ExpSeq))) by Lm3 .= Re((cos.p+(sin.p)*)*(q*) +q**(Sum(q* P_dt))* (cos.p+(sin.p)*)) by Lm3 .=Re(-q*sin.p+q*cos.p*)+Re(q**(Sum(q* P_dt))* (cos.p+(sin.p)*)) by COMPLEX1:8 .=-q*sin.p+ Re(q**((Sum(q* P_dt))* (cos.p+(sin.p)*))) by COMPLEX1:12 .=-q*sin.p -q*Im((Sum(q* P_dt))* (cos.p+(sin.p)*)) by Lm12; hence thesis; end; theorem Th61: for p,q being Real holds sin.(p+q)-sin.p= q*cos.p+q*Re((Sum((q*) P_dt))* (cos.p+sin.p*)) proof let p,q be Real; sin.(p+q)-sin.p=sin.(p+q)-Im(Sum((p*) ExpSeq)) by Def16 .=Im(Sum(((p+q)*) ExpSeq))-Im(Sum((p*) ExpSeq)) by Def16 .=Im(Sum(((p*)+(q*)) ExpSeq)-Sum((p*) ExpSeq)) by COMPLEX1:19 .=Im((Sum((p*) ExpSeq))*(q*) +(q*)*(Sum((q*) P_dt))*(Sum((p*) ExpSeq))) by Th59 .=Im((cos.p+(sin.p)*)*(q*) +(q*)*(Sum((q*) P_dt))*(Sum((p*) ExpSeq))) by Lm3 .= Im((cos.p+sin.p*)*(q*) +(q*)*(Sum((q*) P_dt))* (cos.p+(sin.p)*)) by Lm3 .=Im(-q*sin.p+(q*cos.p)*)+Im((q*)*(Sum((q*) P_dt)) * (cos.p+sin.p*)) by COMPLEX1:8 .=q*cos.p+Im((q*)*((Sum((q*) P_dt))* (cos.p+sin.p*))) by COMPLEX1:12 .=q*cos.p+q*Re((Sum((q*) P_dt))* (cos.p+sin.p*)) by Lm12; hence thesis; end; theorem Th62: 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 Th48 .=Re(Sum((p+q) ExpSeq))-Re(Sum(p ExpSeq)) by Th48 .=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 Th59 .=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 Th48 .=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*)) 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 Th63: cos is_differentiable_in p & diff(cos,p)=-sin.p proof reconsider p as Real by XREAL_0:def 1; deffunc U(Element of REAL) = - $1* Im((Sum($1* P_dt))* (cos.p+sin.p*)); consider Cr being Function of REAL, REAL such that A1: for th be 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)* P_dt))* (cos.p+sin.p*)) proof let n; A3: ((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 A4: ((hy1")(#)(Cr/*hy1)).n= (hy1.n)"*(Cr.(hy1.n)) by A3,FUNCT_2:108 .=(hy1.n)"*( -(hy1.n)* Im((Sum((hy1.n)* P_dt))* (cos.p+sin.p*))) by A1 .=-(hy1.n)"*(hy1.n)* Im((Sum((hy1.n)* P_dt))*(cos.p+sin.p*)); hy1.n<>0 by SEQ_1:5; then ((hy1")(#)(Cr/*hy1)).n =-1*Im((Sum((hy1.n)* P_dt))* (cos.p+sin.p*)) by A4,XCMPLX_0:def 7 .=-Im((Sum((hy1.n)* P_dt))* (cos.p+sin.p*)); hence thesis; end; deffunc U(Real) = -Im((Sum((hy1.$1)* P_dt))*(cos.p+(sin.p)*)); consider rseq such that A5: for n holds rseq.n= U(n) from SEQ_1:sch 1; deffunc U(Element of NAT) = (Sum((hy1.$1)* P_dt))*(cos.p+(sin.p)*); consider cq1 such that A6: for n holds cq1.n=U(n) from COMSEQ_1:sch 1; A7: for q be Real st q>0 holds ex k st for m st k<=m holds |.cq1.m-0c.|0; ex k st for m st k<=m holds |.cq1.m-0c.|0 and A10: for z being complex number st |.z.| P_dt))* (cos.p+(sin.p)*) .| by A6 .= |.(Sum((hy1.m)* P_dt)).|* |.cos.p+(sin.p)*.| by COMPLEX1:65 .= |.(Sum((hy1.m)* P_dt)).|* |.Sum(p* ExpSeq ).| by Lm3 .=|.(Sum((hy1.m)* P_dt)).|*1 by Lm5 .=|.(Sum((hy1.m)* P_dt)).|; A15: abs(hy1.m-0) = 0+(hy1.m)*; then Re ((hy1.m)*)=0 & Im((hy1.m)*)=hy1.m by COMPLEX1:12; then |.(hy1.m)*.| =abs(hy1.m) by COMPLEX1:72; hence |.cq1.m-0c.| P_dt))* (cos.p+(sin.p)*)) 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)* P_dt))* (cos.p+(sin.p)*)) by A6 .=-Im((Sum((hy1.n)* P_dt))* (cos.p+(sin.p)*)) by COMPLEX1:17; hence thesis; end; let n; rseq.n=-Im((Sum((hy1.n)* P_dt))* (cos.p+(sin.p)*)) by A5; hence thesis by A19; end; for n holds rseq.n=((hy1")(#)(Cr/*hy1)).n proof let n; rseq.n=-Im((Sum((hy1.n)* P_dt))* (cos.p+(sin.p)*)) by A5; hence thesis by A2; end; then rseq=(hy1")(#)(Cr/*hy1) by FUNCT_2:63; then (hy1")(#)(Cr/*hy1)=Im(-cq1) by A18,FUNCT_2:63; hence thesis by A16,A17,COMPLEX1:4,COMSEQ_3:41; end; then reconsider PR = Cr as RestFunc by FDIFF_1:def 2; deffunc U(Element of REAL) = -$1*sin.p; consider CL being Function of REAL, REAL such that A20: for th be Real holds CL.th= U(th) from FUNCT_2:sch 4; ex r be Real st for q be Real holds CL.q=r*q proof A21: for q be Real holds CL.q=(-sin.p)*q proof let q be Real; CL.q= -q*sin.p by A20 .=(-sin.p)*q; hence thesis; end; take (-sin.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 cos & for r st r in N holds cos.r - cos.p = PL.(r-p) + PR.(r-p) proof A23: for r st r in ].p-1,p+1 .[ holds cos.r - cos.p = PL.(r-p) + PR.(r-p) proof let r; r=p+(r-p); then cos.r - cos.p =-(r-p)*sin.p -(r-p)*Im((Sum((r-p)* P_dt))* (cos.p+sin.p*)) by Th60 .=-(r-p)*sin.p+Cr.(r-p) by A1 .=PL.(r-p) + PR.(r-p) by A20; hence thesis; end; take ].p-1,p+1 .[; thus thesis by A23,Th24,RCOMP_1:def 6; end; then A24: cos is_differentiable_in p by FDIFF_1:def 4; PL.1= -1*sin.p by A20 .=-sin.p; hence thesis by A22,A24,FDIFF_1:def 5; end; theorem Th64: sin is_differentiable_in p & diff(sin,p)=cos.p proof reconsider p as Real by XREAL_0:def 1; deffunc U(Element of REAL) = $1 *Re((Sum($1* P_dt))* (cos.p+(sin.p)*)); consider Cr being Function of REAL, REAL such that A1: for th be 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* P_dt))* (cos.p+(sin.p)*)) proof let n; A3: ((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 A4: ((hy1")(#)(Cr/*hy1)).n= (hy1.n)"*(Cr.(hy1.n)) by A3,FUNCT_2:108 .=(hy1.n)"*( (hy1.n)*Re((Sum(hy1.n* P_dt))* (cos.p+(sin.p)*))) by A1 .=(hy1.n)"*(hy1.n)* Re((Sum(hy1.n* P_dt))* (cos.p+(sin.p)*)); hy1.n<>0 by SEQ_1:5; then ((hy1")(#)(Cr/*hy1)).n =1*Re((Sum(hy1.n* P_dt))* (cos.p+(sin.p)*)) by A4,XCMPLX_0:def 7 .=Re((Sum(hy1.n* P_dt))* (cos.p+(sin.p)*)); hence thesis; end; deffunc U(Real) = Re((Sum(hy1.$1* P_dt))* (cos.p+(sin.p)*)); consider rseq such that A5: for n holds rseq.n= U(n) from SEQ_1:sch 1; deffunc U(Element of NAT) = (Sum((hy1.$1)* P_dt))* (cos.p+(sin.p)*); consider cq1 such that A6: for n holds cq1.n= U(n) from COMSEQ_1:sch 1; A7: for q be Real st q>0 holds ex k st for m st k<=m holds |.cq1.m-0c.|0; ex k st for m st k<=m holds |.cq1.m-0c.|0 and A10: for z being complex number st |.z.| P_dt))* (cos.p+(sin.p)*).| by A6 .= |.(Sum((hy1.m)* P_dt)).|* |.cos.p+(sin.p)*.| by COMPLEX1:65 .= |.(Sum((hy1.m)* P_dt)).|* |.Sum(p* ExpSeq ).| by Lm3 .=|.(Sum((hy1.m)* P_dt)).|*1 by Lm5 .=|.(Sum((hy1.m)* P_dt)).|; A15: abs(hy1.m-0) = 0+(hy1.m)*; then Re ((hy1.m)*)=0 & Im((hy1.m)*)=hy1.m by COMPLEX1:12; then |.(hy1.m)*.| =abs(hy1.m) by COMPLEX1:72; hence |.cq1.m-0c.| P_dt))* (cos.p+(sin.p)*)) by A6; hence thesis by A5; end; for n holds rseq.n=((hy1")(#)(Cr/*hy1)).n proof let n; rseq.n=Re((Sum((hy1.n)* P_dt))* (cos.p+(sin.p)*)) by A5; hence thesis by A2; end; then rseq=(hy1")(#)(Cr/*hy1) by FUNCT_2:63; then (hy1")(#)(Cr/*hy1)=Re(cq1) by A18,FUNCT_2:63; hence thesis by A16,A17,COMPLEX1:4,COMSEQ_3:41; end; then reconsider PR = Cr as RestFunc by FDIFF_1:def 2; deffunc U(Element of REAL) = $1*cos.p; consider CL being Function of REAL, REAL such that A19: for th be Real holds CL.th=U(th) from FUNCT_2:sch 4; A20: for d be real number holds CL.d = d*cos.p proof let d be real number; d is Real by XREAL_0:def 1; hence thesis by A19; end; ex r be Real st for q be Real holds CL.q=r*q proof take (cos.p); thus thesis by A20; end; then reconsider PL = CL as LinearFunc by FDIFF_1:def 3; A21: 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 A22: for r st r in ].p-1,p+1 .[ holds sin.r - sin.p = PL.(r-p) + PR.(r-p) proof let r; r=p+(r-p); then sin.r - sin.p =(r-p)*cos.p +(r-p)*Re((Sum((r-p)* P_dt))* (cos.p+sin.p*)) by Th61 .=(r-p)*cos.p +Cr.(r-p) by A1 .=PL.(r-p) + PR.(r-p) by A20; hence thesis; end; take ].p-1,p+1 .[; thus thesis by A22,Th24,RCOMP_1:def 6; end; then A23: sin is_differentiable_in p by FDIFF_1:def 4; PL.1= 1*cos.p by A20; hence thesis by A21,A23,FDIFF_1:def 5; end; theorem Th65: exp_R is_differentiable_in p & diff(exp_R,p)=exp_R.p proof deffunc U(Element of REAL) = $1 * exp_R.p*Re((Sum($1 P_dt))); consider Cr being Function of REAL, REAL such that A1: for th be 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: ((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 A4: ((hy1")(#)(Cr/*hy1)).n= (hy1.n)"*(Cr.(hy1.n)) by A3,FUNCT_2:108 .=(hy1.n)"*((hy1.n)*exp_R.p*Re((Sum((hy1.n) P_dt)))) 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 A4,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 A5: for n holds rseq.n= U(n) from SEQ_1:sch 1; deffunc U(Element of NAT) = Sum((hy1.$1) P_dt)*exp_R.p; consider cq1 such that A6: for n holds cq1.n= U(n) from COMSEQ_1:sch 1; A7: for q be Real st q>0 holds ex k st for m st k<=m holds |.cq1.m-0c.|0; ex k st for m st k<=m holds |.cq1.m-0c.|0 by Th54; then consider r such that A9: r>0 and A10: for z being complex number st |.z.|; then A15: Re(exp_R.p)=exp_R.p & Im(exp_R.p)=0 by COMPLEX1:12; A16: exp_R.p>0 by Th54; then A17: |.cq1.m-0c.| =|.(Sum((hy1.m) P_dt)).|* ( exp_R.p) by A14,A15,SQUARE_1:22; abs(hy1.m-0)=1/2 proof assume th in [.0,1 .]; then A1: 0<=th & th<=1 by XXREAL_1:1; th is Real by XREAL_0:def 1; then A2: Partial_Sums(th P_cos) is convergent by Th36; A3: cos.th=Sum (th P_cos) by Th37; 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)!) by NEWTON:5 .= 1+ (-1)*(th*th)/((2*1)!) by NEWTON:81 .= 1-(th^2)/2 by NEWTON:14; defpred X[Element of 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; assume A8: ((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; then A9: ( (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); A10: (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)))!); A11: (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; A12: 2*(2*(k+1))<2*(2*(k+1)+1) by XREAL_1:29,68; then A13: (2*(2*(k+1)))! <= (2*(2*(k+1)+1))! by Th39; A14: (th)|^ (2*(2*(k+1)+1)) <= (th)|^ (2*(2*(k+1))) by A1,A12,Th40; A15: 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 A13,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 A14,A15,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 A9,A10,A11,XREAL_1:49; hence thesis by A8,XXREAL_0:2; end; for n holds X[n] from NAT_1:sch 1(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 Th70: [.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 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,Th69; 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 Th70,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 Th67,Th68,FDIFF_1:26; A2: for th be Real st th in ].0,1 .[ holds cos.th<>0 proof let th be Real such that A3: th in ].0,1 .[; ].0,1 .[ c=[.0,1 .] by XXREAL_1:25; hence thesis by A3,Th69; 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 Th63,XREAL_0:def 1; A6: sin is_differentiable_in th by Th64; 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 Th64 .=(cos.th*cos.th-(-sin.th)*sin.th)/(cos.th)^2 by Th63 .=((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 Th71: tan|[.0,1 .] is continuous proof for th be real number st th in dom(tan|[.0,1 .]) holds tan|[.0,1 .] is_continuous_in th proof let th be real number; 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 Th68,FDIFF_1:9; then A5: sin is_continuous_in th by FDIFF_1:24; cos is_differentiable_in th by A4,Th67,FDIFF_1:9; then A6: cos is_continuous_in th by FDIFF_1:24; cos.(th) <> 0 by A2,Th69; 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,Th70,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,Th70,FUNCT_2:108,XBOOLE_1:1; end; then (tan|[.0,1 .])/*rseq =tan/*rseq by FUNCT_2:63; 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 Th72: 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: 0th2; now per cases by A8,XXREAL_0:1; suppose A9: th11 proof 0 in [.0,1 .] by XXREAL_1:1; then A1: tan.0=(sin.0)* (cos.0)" by Th70,RFUNCT_1:def 1 .=0 by Th30; 1 in [.0,1 .] by XXREAL_1:1; then tan.1 =(sin.1)/(cos.1) by Th70,RFUNCT_1:def 1; hence thesis by A1,Th43,XREAL_1:187; end; begin :: Existence of Circle Ratio definition func PI -> real number 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 be Real such that A2: th in [.0, 1 .] and A3: tan.(th)=1 by Th70,Th71,FCONT_2:15; A4: 0<=th by A2,XXREAL_1:1; A5: th <= 1 by A2,XXREAL_1:1; A6: 0 Real; coherence by XREAL_0:def 1; end; theorem Th73: 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,Th70,RFUNCT_1:def 1; hence thesis by XCMPLX_1:209; end; begin :: Formulas of sin and cos theorem Th74: 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 by XREAL_0:def 1; A1: (th1+th2)* = 0+0+(th1+th2)*; A2: Sum(th1* ExpSeq ) * Sum(th2* ExpSeq ) =Sum((th1*+th2*) ExpSeq ) by Lm2 .=cos.(th1+th2)+(sin.(th1+th2))* by A1,Lm3; Sum((th1* ExpSeq) ) * Sum((th2* ExpSeq) ) =(cos.(th1)+(sin.th1)*)* Sum((th2* ExpSeq) ) by Lm3 .=(cos.(th1)+sin.(th1)*)*(cos.(th2)+(sin.th2)*) by Lm3 .=((cos.(th1)) *( cos.(th2))-(sin.(th1)) * (sin.(th2))+ ((sin.(th1)) * (cos.(th2))+(cos.(th1)) * (sin.(th2)))*); 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 Th74; theorem Th76: 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 Th73,Th74 .=0; thus A2: sin.(PI/2)=sin.(PI/4+PI/4) .= (cos.(PI/4)) *( cos.(PI/4)) +(sin.(PI/4)) * (sin.(PI/4)) by Th73,Th74 .=1 by Th28; thus A3: cos.(PI)=cos.(PI/2+PI/2) .=0 * 0-sin.(PI/2) * sin.(PI/2) by A1,Th74 .=-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 Th74 .=0 by A1; thus cos.(PI+PI/2) =(cos.(PI)) *( cos.(PI/2)) -(sin.(PI)) * (sin.(PI/2)) by Th74 .=0 by A1,A4; thus sin.(PI+PI/2) =(sin.(PI) )*( cos.(PI/2)) +(cos.(PI)) *( sin.(PI/2) ) by Th74 .=-1 by A1,A2,A3; thus cos.(2 * PI)=cos.(PI+PI) .=(-1 ) * (-1) -sin.(PI) * sin.(PI) by A3,Th74 .=1 by A4; thus sin.(2 * PI)=sin.(PI+PI) .=(sin.(PI)) * (cos.(PI))+(cos.(PI)) * (sin.(PI)) by Th74 .=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 Th76; theorem Th78: 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 Th74,Th76 .=sin.th; thus cos.(th+2 * PI)=cos.(th) * 1 - sin.(th) * 0 by Th74,Th76 .=cos.th; thus sin.(PI/2-th) =(sin.(PI/2) )* (cos.(-th)) + (cos.(PI/2)) *( sin.(-th)) by Th74 .=cos.(th) by Th30,Th76; thus cos.(PI/2-th) =(cos.(PI/2)) * (cos.(-th)) - ( sin.(PI/2)) *( sin.(-th)) by Th74 .=0 - 1 * (-sin.(th)) by Th30,Th76 .=sin.(th); thus sin.(PI/2+th) =1 * cos.(th) + 0 * (sin.(th)) by Th74,Th76 .=cos.(th); thus cos.(PI/2+th) =(cos.(PI/2)) *( cos.(th)) -( sin.(PI/2) )*( sin.(th)) by Th74 .=-sin.(th) by Th76; thus sin.(PI+th) =(sin.(PI)) * (cos.(th)) +( cos.(PI) )*( sin.(th)) by Th74 .=-sin.(th) by Th76; thus cos.(PI+th) =(-1) * cos.(th) - 0 * sin.(th) by Th74,Th76 .=-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 Th78; 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: 00 by Th69; then sin.th-sin.0 >0 by A3,A5,Th68; hence thesis by XREAL_1:47; end; end; hence thesis; end; hence thesis by Th30; end; theorem Th80: 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 Th67,FDIFF_1:25; then A3: cos|[.0,th.] is continuous by FCONT_1:16; A4: 0 < th by A1,XXREAL_1:4; A5: th is Real by XREAL_0:def 1; [. 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 be Real st th2 in [.0,th .] & cos.th2 = 0 by A3,A4,A5,Th24,FCONT_2:15; then consider th2 be Real such that A6: th2 in [.0,th .] and 0 < th and A7: cos.th2 = 0 by A4; A8: 0 <= th2 by A6,XXREAL_1:1; A9: th2 <= th by A6,XXREAL_1:1; A10: th < PI/2 by A1,XXREAL_1:4; A11: 0 0 & sin.(th2/2) >= -0 by A15,Lm17,Th69; 4*(th2/2) < 4*1 by A13,XREAL_1:68; then A17: (2*th2) in ].0,4.[ by A11,XXREAL_1:4; (sin.(th2/2)) * (cos.(th2/2))"=1 by A14,A16,XCMPLX_0:def 7; then tan.((2*th2)/4) = 1 by A15,Th70,RFUNCT_1:def 1; then 2*th2 =PI by A17,Def28; hence contradiction by A1,A9,XXREAL_1:4; end; theorem th in ].0,PI/2.[ implies cos(th) > 0 by Th80; 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 Th74 .=(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 Th74 .=(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 Th68,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 Th67,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 Th66,FDIFF_1:25 ,FUNCT_2:def 1; hence thesis by RELAT_1:69; end; end;