sin_cos.miz

begin

 reserve q,th,r for Real,

a,b,p for Real,

w,z for Complex,

k,l,m,n,n1,n2 for Nat,

seq,seq1,seq2,cq1 for Complex_Sequence,

rseq,rseq1,rseq2 for Real_Sequence,

rr for set,

hy1 for 0 -convergent non-zero Real_Sequence;

 definition

 let m,k be natural Number;

 :: SIN_COS:def1

 func CHK (m,k) -> Element of COMPLEX equals

 : Def1: 1 if m <= k

 otherwise 0 ;

 correctness

 proof

 0c = 0 ;

 hence thesis by COMPLEX1:def 4;

 end;

 end

 registration

 let m,k be natural Number;

 cluster ( CHK (m,k)) -> real;

 coherence by Def1;

 end

 scheme :: SIN_COS:sch1

 ExComplexCASE { F( Nat, Nat) -> Complex } :

for k holds ex seq st for n holds (n <= k implies (seq . n) = F(k,n)) & (n > k implies (seq . n) = 0 );

 let k;

 defpred P[ object, object] means ex n st (n = $1 & (n <= k implies $2 = F(k,n)) & (n > k implies $2 = 0c ));

 A1:

 now

 let x be object;

 assume x in NAT ;

 then

 consider n such that

 A2: n = x;

 A3:

 now

 assume n <= k;



 hence (( CHK (n,k)) * F(k,n)) = (1 * F(k,n)) by Def1

 .= F(k,n);

 end;

 A4:

 now

 assume n > k;



 hence (( CHK (n,k)) * F(k,n)) = ( 0 * F(k,n)) by Def1

 .= 0 ;

 end;

 reconsider y = (( CHK (n,k)) * F(k,n)) as object;

 take y;

 thus P[x, y] by A2, A3, A4;

 end;

 consider f be Function such that

 A5: ( dom f) = NAT and

 A6: for x be object st x in NAT holds P[x, (f . x)] from CLASSES1:sch 1( A1);

 now

 let x be set;

 assume x in NAT ;

 then ex n st n = x & (n <= k implies (f . x) = F(k,n)) & (n > k implies (f . x) = 0c ) by A6;

 hence (f . x) is Element of COMPLEX by XCMPLX_0:def 2;

 end;

 then

 reconsider f as Complex_Sequence by A5, COMSEQ_1: 1;

 take seq = f;

 let n;

 n in NAT by ORDINAL1:def 12;

 then P[n, (f . n)] by A6;

 then ex l be Nat st l = n & (l <= k implies (seq . n) = F(k,l)) & (l > k implies (seq . n) = 0c );

 hence thesis;

 end;

 scheme :: SIN_COS:sch2

 ExRealCASE { F( Nat, Nat) -> Real } :

for k holds ex rseq st for n holds (n <= k implies (rseq . n) = F(k,n)) & (n > k implies (rseq . n) = 0 );

 let k;

 defpred P[ object, object] means ex n st (n = $1 & (n <= k implies $2 = F(k,n)) & (n > k implies $2 = 0 ));

 A1:

 now

 let x be object;

 assume x in NAT ;

 then

 consider n such that

 A2: n = x;

 A3:

 now

 assume n <= k;



 hence (( CHK (n,k)) * F(k,n)) = (1 * F(k,n)) by Def1

 .= F(k,n);

 end;

 A4:

 now

 assume n > k;



 hence (( CHK (n,k)) * F(k,n)) = ( 0 * F(k,n)) by Def1

 .= 0 ;

 end;

 reconsider y = (( CHK (n,k)) * F(k,n)) as object;

 take y;

 thus P[x, y] by A2, A3, A4;

 end;

 consider f be Function such that

 A5: ( dom f) = NAT and

 A6: for x be object st x in NAT holds P[x, (f . x)] from CLASSES1:sch 1( A1);

 now

 let x be object;

 assume x in NAT ;

 then ex n st n = x & (n <= k implies (f . x) = F(k,n)) & (n > k implies (f . x) = 0 ) by A6;

 hence (f . x) is real;

 end;

 then

 reconsider f as Real_Sequence by A5, SEQ_1: 1;

 take rseq = f;

 let n;

 n in NAT by ORDINAL1:def 12;

 then ex l be Nat st l = n & (l <= k implies (rseq . n) = F(k,l)) & (l > k implies (rseq . n) = 0 ) by A6;

 hence thesis;

 end;

 1 in NAT ;

 then

 reconsider jj = 1 as Element of REAL by NUMBERS: 19;

 definition

 :: SIN_COS:def2

 func Prod_real_n -> Real_Sequence means

 : Def2: (it . 0 ) = 1 & for n holds (it . (n + 1)) = ((it . n) * (n + 1));

 existence

 proof

 deffunc U( Nat, Real) = ( In (($2 * ($1 + 1)), REAL ));

 consider f be sequence of REAL such that

 A1: (f . 0 ) = jj and

 A2: for n be Nat holds (f . (n + 1)) = U(n,.) from NAT_1:sch 12;

 take f;

 thus (f . 0 ) = 1 by A1;

 let n;



 thus (f . (n + 1)) = U(n,.) by A2

 .= ((f . n) * (n + 1));

 end;

 uniqueness

 proof

 let rseq1, rseq2;

 assume that

 A3: (rseq1 . 0 ) = 1 and

 A4: for n holds (rseq1 . (n + 1)) = ((rseq1 . n) * (n + 1)) and

 A5: (rseq2 . 0 ) = 1 and

 A6: for n holds (rseq2 . (n + 1)) = ((rseq2 . n) * (n + 1));

 defpred X[ Nat] means (rseq1 . $1) = (rseq2 . $1);



 A7: X[ 0 ] by A3, A5;



 A8: for k be Nat st X[k] holds X[(k + 1)]

 proof

 let k be Nat;

 assume (rseq1 . k) = (rseq2 . k);



 hence (rseq1 . (k + 1)) = ((rseq2 . k) * (k + 1)) by A4

 .= (rseq2 . (k + 1)) by A6;

 end;

 for n be Nat holds X[n] from NAT_1:sch 2( A7, A8);

 hence rseq1 = rseq2;

 end;

 end

 definition

 let n be Nat;

 :: original: !

 redefine

 :: SIN_COS:def3

 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];

 ( Prod_real_n . (l + 1)) = (( Prod_real_n . l) * (l + 1)) by Def2

 .= ((l + 1) ! ) by A3, NEWTON: 15;

 hence X[(l + 1)];

 end;

 for k be Nat holds X[k] from NAT_1:sch 2( A1, A2);

 hence thesis;

 end;

 end

 definition

 let z be Complex;

 deffunc U( Nat) = ((z |^ $1) / ($1 ! ));

 :: SIN_COS:def4

 func z ExpSeq -> Complex_Sequence means

 : Def4: for n holds (it . n) = ((z |^ n) / (n ! ));

 existence

 proof

 thus ex s be Complex_Sequence st for n holds (s . n) = U(n) from COMSEQ_1:sch 1;

 end;

 uniqueness

 proof

 let s1,s2 be Complex_Sequence such that

 A1: for x be Nat holds (s1 . x) = U(x) and

 A2: for x be Nat holds (s2 . x) = U(x);

 let x be Element of NAT ;



 thus (s1 . x) = U(x) by A1

 .= (s2 . x) by A2;

 end;

 end

 definition

 let a be Real;

 deffunc U( Nat) = ((a |^ $1) / ($1 ! ));

 :: SIN_COS:def5

 func a rExpSeq -> Real_Sequence means

 : Def5: for n holds (it . n) = ((a |^ n) / (n ! ));

 existence

 proof

 thus ex s be Real_Sequence st for n holds (s . n) = U(n) from SEQ_1:sch 1;

 end;

 uniqueness

 proof

 let s1,s2 be Real_Sequence such that

 A1: for x be Nat holds (s1 . x) = U(x) and

 A2: for x be Nat holds (s2 . x) = U(x);

 let x be Element of NAT ;



 thus (s1 . x) = U(x) by A1

 .= (s2 . x) by A2;

 end;

 end

 theorem :: SIN_COS:1



 Th1: ( 0 ! ) = 1 & (n ! ) <> 0 & ((n + 1) ! ) = ((n ! ) * (n + 1)) by Def2;

 theorem :: SIN_COS:2



 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 Nat;

 :: SIN_COS:def6

 func Coef (n) -> Complex_Sequence means

 : Def6: for k be Nat holds (k <= n implies (it . k) = ((n ! ) / ((k ! ) * ((n -' k) ! )))) & (k > n implies (it . k) = 0 );

 existence

 proof

 deffunc U( Nat, Nat) = (($1 ! ) / (($2 ! ) * (($1 -' $2) ! )));

 for n holds ex seq st for k holds (k <= n implies (seq . k) = U(n,k)) & (k > n implies (seq . k) = 0 ) from ExComplexCASE;

 hence thesis;

 end;

 uniqueness

 proof

 let seq1, seq2;

 assume that

 A1: for k holds (k <= n implies (seq1 . k) = ((n ! ) / ((k ! ) * ((n -' k) ! )))) & (k > n implies (seq1 . k) = 0 ) and

 A2: for k holds (k <= n implies (seq2 . k) = ((n ! ) / ((k ! ) * ((n -' k) ! )))) & (k > n implies (seq2 . k) = 0 );

 now

 let k be Element of NAT ;

 per cases ;

 suppose

 A3: k <= n;



 hence (seq1 . k) = ((n ! ) / ((k ! ) * ((n -' k) ! ))) by A1

 .= (seq2 . k) by A2, A3;

 end;

 suppose

 A4: k > n;



 hence (seq1 . k) = 0c by A1

 .= (seq2 . k) by A2, A4;

 end;

 end;

 hence seq1 = seq2;

 end;

 end

 definition

 let n be Nat;

 :: SIN_COS:def7

 func Coef_e (n) -> Complex_Sequence means

 : Def7: for k be Nat holds (k <= n implies (it . k) = ( 1r / ((k ! ) * ((n -' k) ! )))) & (k > n implies (it . k) = 0 );

 existence

 proof

 deffunc U( Nat, Nat) = ( 1r / (($2 ! ) * (($1 -' $2) ! )));

 for n holds ex seq st for k holds (k <= n implies (seq . k) = U(n,k)) & (k > n implies (seq . k) = 0 ) from ExComplexCASE;

 hence thesis;

 end;

 uniqueness

 proof

 let seq1, seq2;

 assume that

 A1: for k holds (k <= n implies (seq1 . k) = ( 1r / ((k ! ) * ((n -' k) ! )))) & (k > n implies (seq1 . k) = 0 ) and

 A2: for k holds (k <= n implies (seq2 . k) = ( 1r / ((k ! ) * ((n -' k) ! )))) & (k > n implies (seq2 . k) = 0 );

 now

 let k be Element of NAT ;

 per cases ;

 suppose

 A3: k <= n;



 hence (seq1 . k) = ( 1r / ((k ! ) * ((n -' k) ! ))) by A1

 .= (seq2 . k) by A2, A3;

 end;

 suppose

 A4: k > n;



 hence (seq1 . k) = 0c by A1

 .= (seq2 . k) by A2, A4;

 end;

 end;

 hence seq1 = seq2;

 end;

 end

 definition

 let seq;

 :: SIN_COS:def8

 func Shift seq -> Complex_Sequence means

 : Def8: (it . 0 ) = 0 & for k be Nat holds (it . (k + 1)) = (seq . k);

 existence

 proof

 deffunc U( Nat, Element of COMPLEX ) = (seq . $1);

 consider f be sequence of COMPLEX such that

 A1: (f . 0 ) = 0c & for n be Nat holds (f . (n + 1)) = U(n,.) from NAT_1:sch 12;

 take f;

 thus thesis by A1;

 end;

 uniqueness

 proof

 let seq1, seq2;

 assume that

 A2: (seq1 . 0 ) = 0 and

 A3: for n holds (seq1 . (n + 1)) = (seq . n) and

 A4: (seq2 . 0 ) = 0 and

 A5: for n holds (seq2 . (n + 1)) = (seq . n);

 defpred X[ Nat] means (seq1 . $1) = (seq2 . $1);



 A6: X[ 0 ] by A2, A4;



 A7: for k be Nat st X[k] holds X[(k + 1)]

 proof

 let k be Nat;

 assume (seq1 . k) = (seq2 . k);



 thus (seq1 . (k + 1)) = (seq . k) by A3

 .= (seq2 . (k + 1)) by A5;

 end;

 for n be Nat holds X[n] from NAT_1:sch 2( A6, A7);

 hence seq1 = seq2;

 end;

 end

 definition

 let n;

 let z,w be Complex;

 :: SIN_COS:def9

 func Expan (n,z,w) -> Complex_Sequence means

 : Def9: for k be Nat holds (k <= n implies (it . k) = (((( Coef n) . k) * (z |^ k)) * (w |^ (n -' k)))) & (n < k implies (it . k) = 0 );

 existence

 proof

 deffunc U( Nat, Nat) = (((( Coef $1) . $2) * (z |^ $2)) * (w |^ ($1 -' $2)));

 for n holds ex seq st for k holds (k <= n implies (seq . k) = U(n,k)) & (k > n implies (seq . k) = 0 ) from ExComplexCASE;

 hence thesis;

 end;

 uniqueness

 proof

 let seq1, seq2;

 assume that

 A1: for k holds (k <= n implies (seq1 . k) = (((( Coef n) . k) * (z |^ k)) * (w |^ (n -' k)))) & (k > n implies (seq1 . k) = 0 ) and

 A2: for k holds (k <= n implies (seq2 . k) = (((( Coef n) . k) * (z |^ k)) * (w |^ (n -' k)))) & (k > n implies (seq2 . k) = 0 );

 now

 let k be Element of NAT ;

 per cases ;

 suppose

 A3: k <= n;



 hence (seq1 . k) = (((( Coef n) . k) * (z |^ k)) * (w |^ (n -' k))) by A1

 .= (seq2 . k) by A2, A3;

 end;

 suppose

 A4: k > n;



 hence (seq1 . k) = 0c by A1

 .= (seq2 . k) by A2, A4;

 end;

 end;

 hence seq1 = seq2;

 end;

 end

 definition

 let n;

 let z,w be Complex;

 :: SIN_COS:def10

 func Expan_e (n,z,w) -> Complex_Sequence means

 : Def10: for k be Nat holds (k <= n implies (it . k) = (((( Coef_e n) . k) * (z |^ k)) * (w |^ (n -' k)))) & (n < k implies (it . k) = 0 );

 existence

 proof

 deffunc U( Nat, Nat) = (((( Coef_e $1) . $2) * (z |^ $2)) * (w |^ ($1 -' $2)));

 for n holds ex seq st for k holds (k <= n implies (seq . k) = U(n,k)) & (k > n implies (seq . k) = 0 ) from ExComplexCASE;

 hence thesis;

 end;

 uniqueness

 proof

 let seq1, seq2;

 assume that

 A1: for k holds (k <= n implies (seq1 . k) = (((( Coef_e n) . k) * (z |^ k)) * (w |^ (n -' k)))) & (k > n implies (seq1 . k) = 0 ) and

 A2: for k holds (k <= n implies (seq2 . k) = (((( Coef_e n) . k) * (z |^ k)) * (w |^ (n -' k)))) & (k > n implies (seq2 . k) = 0 );

 now

 let k be Element of NAT ;

 per cases ;

 suppose

 A3: k <= n;



 hence (seq1 . k) = (((( Coef_e n) . k) * (z |^ k)) * (w |^ (n -' k))) by A1

 .= (seq2 . k) by A2, A3;

 end;

 suppose

 A4: k > n;



 hence (seq1 . k) = 0c by A1

 .= (seq2 . k) by A2, A4;

 end;

 end;

 hence seq1 = seq2;

 end;

 end

 definition

 let n;

 let z,w be Complex;

 :: SIN_COS:def11

 func Alfa (n,z,w) -> Complex_Sequence means

 : Def11: for k be Nat holds (k <= n implies (it . k) = (((z ExpSeq ) . k) * (( Partial_Sums (w ExpSeq )) . (n -' k)))) & (n < k implies (it . k) = 0 );

 existence

 proof

 deffunc U( Nat, Nat) = (((z ExpSeq ) . $2) * (( Partial_Sums (w ExpSeq )) . ($1 -' $2)));

 for n holds ex seq st for k holds (k <= n implies (seq . k) = U(n,k)) & (k > n implies (seq . k) = 0 ) from ExComplexCASE;

 hence thesis;

 end;

 uniqueness

 proof

 let seq1, seq2;

 assume that

 A1: for k holds (k <= n implies (seq1 . k) = (((z ExpSeq ) . k) * (( Partial_Sums (w ExpSeq )) . (n -' k)))) & (k > n implies (seq1 . k) = 0 ) and

 A2: for k holds (k <= n implies (seq2 . k) = (((z ExpSeq ) . k) * (( Partial_Sums (w ExpSeq )) . (n -' k)))) & (k > n implies (seq2 . k) = 0 );

 now

 let k be Element of NAT ;

 per cases ;

 suppose

 A3: k <= n;



 hence (seq1 . k) = (((z ExpSeq ) . k) * (( Partial_Sums (w ExpSeq )) . (n -' k))) by A1

 .= (seq2 . k) by A2, A3;

 end;

 suppose

 A4: k > n;



 hence (seq1 . k) = 0c by A1

 .= (seq2 . k) by A2, A4;

 end;

 end;

 hence seq1 = seq2;

 end;

 end

 definition

 let a,b be Real;

 let n be Nat;

 :: SIN_COS:def12

 func Conj (n,a,b) -> Real_Sequence means for k be Nat holds (k <= n implies (it . k) = (((a rExpSeq ) . k) * ((( Partial_Sums (b rExpSeq )) . n) - (( Partial_Sums (b rExpSeq )) . (n -' k))))) & (n < k implies (it . k) = 0 );

 existence

 proof

 deffunc U( Nat, Nat) = (((a rExpSeq ) . $2) * ((( Partial_Sums (b rExpSeq )) . $1) - (( Partial_Sums (b rExpSeq )) . ($1 -' $2))));

 for n holds ex rseq st for k holds (k <= n implies (rseq . k) = U(n,k)) & (k > n implies (rseq . k) = 0 ) from ExRealCASE;

 hence thesis;

 end;

 uniqueness

 proof

 let rseq1, rseq2;

 assume that

 A1: for k holds (k <= n implies (rseq1 . k) = (((a rExpSeq ) . k) * ((( Partial_Sums (b rExpSeq )) . n) - (( Partial_Sums (b rExpSeq )) . (n -' k))))) & (k > n implies (rseq1 . k) = 0 ) and

 A2: for k holds (k <= n implies (rseq2 . k) = (((a rExpSeq ) . k) * ((( Partial_Sums (b rExpSeq )) . n) - (( Partial_Sums (b rExpSeq )) . (n -' k))))) & (k > n implies (rseq2 . k) = 0 );

 now

 let k be Element of NAT ;

 per cases ;

 suppose

 A3: k <= n;



 hence (rseq1 . k) = (((a rExpSeq ) . k) * ((( Partial_Sums (b rExpSeq )) . n) - (( Partial_Sums (b rExpSeq )) . (n -' k)))) by A1

 .= (rseq2 . k) by A2, A3;

 end;

 suppose

 A4: k > n;



 hence (rseq1 . k) = 0 by A1

 .= (rseq2 . k) by A2, A4;

 end;

 end;

 hence rseq1 = rseq2;

 end;

 end

 definition

 let z,w be Complex;

 let n be Nat;

 :: SIN_COS:def13

 func Conj (n,z,w) -> Complex_Sequence means

 : Def13: for k be Nat holds (k <= n implies (it . k) = (((z ExpSeq ) . k) * ((( Partial_Sums (w ExpSeq )) . n) - (( Partial_Sums (w ExpSeq )) . (n -' k))))) & (n < k implies (it . k) = 0 );

 existence

 proof

 deffunc U( Nat, Nat) = (((z ExpSeq ) . $2) * ((( Partial_Sums (w ExpSeq )) . $1) - (( Partial_Sums (w ExpSeq )) . ($1 -' $2))));

 for n holds ex seq st for k holds (k <= n implies (seq . k) = U(n,k)) & (k > n implies (seq . k) = 0 ) from ExComplexCASE;

 hence thesis;

 end;

 uniqueness

 proof

 let seq1, seq2;

 assume that

 A1: for k holds (k <= n implies (seq1 . k) = (((z ExpSeq ) . k) * ((( Partial_Sums (w ExpSeq )) . n) - (( Partial_Sums (w ExpSeq )) . (n -' k))))) & (k > n implies (seq1 . k) = 0 ) and

 A2: for k holds (k <= n implies (seq2 . k) = (((z ExpSeq ) . k) * ((( Partial_Sums (w ExpSeq )) . n) - (( Partial_Sums (w ExpSeq )) . (n -' k))))) & (k > n implies (seq2 . k) = 0 );

 now

 let k be Element of NAT ;

 per cases ;

 suppose

 A3: k <= n;



 hence (seq1 . k) = (((z ExpSeq ) . k) * ((( Partial_Sums (w ExpSeq )) . n) - (( Partial_Sums (w ExpSeq )) . (n -' k)))) by A1

 .= (seq2 . k) by A2, A3;

 end;

 suppose

 A4: k > n;



 hence (seq1 . k) = 0c by A1

 .= (seq2 . k) by A2, A4;

 end;

 end;

 hence seq1 = seq2;

 end;

 end



 Lm1: for p1,p2,g1,g2 be 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 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 :: SIN_COS:3



 Th3: for z be Complex 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;

 A1:

 now

 let n be Nat;



 thus ((z ExpSeq ) . (n + 1)) = ((z |^ (n + 1)) / ((n + 1) ! )) by Def4

 .= ((((z GeoSeq ) . n) * z) / ((n + 1) ! )) by COMSEQ_3:def 1

 .= (((z |^ n) * z) / ((n ! ) * ((n + 1) + ( 0 * )))) 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[ 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 2( A3, A4);

 hence thesis by A1, A2;

 end;

 theorem :: SIN_COS:4



 Th4: 0 < k implies (( Shift seq) . k) = (seq . (k -' 1))

 proof

 assume

 A1: 0 < k;



 A2: ( 0 + 1) <= k by INT_1: 7, A1;

 consider m be Nat such that

 A3: (m + 1) = k by A1, NAT_1: 6;



 A4: m = (k - 1) by A3;



 thus (( Shift seq) . k) = (seq . m) by A3, Def8

 .= (seq . (k -' 1)) by A2, A4, XREAL_1: 233;

 end;

 theorem :: SIN_COS:5



 Th5: (( Partial_Sums seq) . k) = ((( Partial_Sums ( Shift seq)) . k) + (seq . k))

 proof

 defpred X[ Nat] means (( Partial_Sums seq) . $1) = ((( Partial_Sums ( Shift seq)) . $1) + (seq . $1));

 (( Partial_Sums seq) . 0 ) = ( 0c + (seq . 0 )) by SERIES_1:def 1

 .= ((( Shift seq) . 0 ) + (seq . 0 )) by Def8

 .= ((( Partial_Sums ( Shift seq)) . 0 ) + (seq . 0 )) by SERIES_1:def 1;

 then

 A1: X[ 0 ];



 A2: for k st X[k] holds X[(k + 1)]

 proof

 let k such that

 A3: (( Partial_Sums seq) . k) = ((( Partial_Sums ( Shift seq)) . k) + (seq . k));



 thus (( Partial_Sums seq) . (k + 1)) = (((( Partial_Sums ( Shift seq)) . k) + (seq . k)) + (seq . (k + 1))) by A3, SERIES_1:def 1

 .= (((( Partial_Sums ( Shift seq)) . k) + (( Shift seq) . (k + 1))) + (seq . (k + 1))) by Def8

 .= ((( Partial_Sums ( Shift seq)) . (k + 1)) + (seq . (k + 1))) by SERIES_1:def 1;

 end;

 for k holds X[k] from NAT_1:sch 2( A1, A2);

 hence thesis;

 end;

 theorem :: SIN_COS:6



 Th6: ((z + w) |^ n) = (( Partial_Sums ( Expan (n,z,w))) . n)

 proof



 A1: ( 0 -' 0 ) = 0 by XREAL_1: 232;

 defpred X[ Nat] means ((z + w) |^ $1) = (( Partial_Sums ( Expan ($1,z,w))) . $1);

 (( Partial_Sums ( Expan ( 0 ,z,w))) . 0 ) = (( Expan ( 0 ,z,w)) . 0 ) by SERIES_1:def 1

 .= (((( Coef 0 ) . 0 ) * (z |^ 0 )) * (w |^ 0 )) by A1, Def9

 .= (((1 / (1 * 1)) * (z |^ 0 )) * (w |^ 0 )) by A1, Def6, Th1

 .= ( 1r * ((w GeoSeq ) . 0 )) by COMSEQ_3:def 1

 .= 1r by COMSEQ_3:def 1;

 then

 A2: X[ 0 ] by COMSEQ_3:def 1;



 A3: for n st X[n] holds X[(n + 1)]

 proof

 let n such that

 A4: ((z + w) |^ n) = (( Partial_Sums ( Expan (n,z,w))) . n);



 A5: n in NAT by ORDINAL1:def 12;



 A6: ((z + w) |^ (n + 1)) = ((((z + w) GeoSeq ) . n) * (z + w)) by COMSEQ_3:def 1

 .= (((z + w) (#) ( Partial_Sums ( Expan (n,z,w)))) . n) by A4, VALUED_1: 6

 .= (( Partial_Sums ((z + w) (#) ( Expan (n,z,w)))) . n) by COMSEQ_3: 29;

 now

 let k be Element of NAT ;



 thus (((z + w) (#) ( Expan (n,z,w))) . k) = ((z + w) * (( Expan (n,z,w)) . k)) by VALUED_1: 6

 .= ((z * (( Expan (n,z,w)) . k)) + (w * (( Expan (n,z,w)) . k)))

 .= (((z (#) ( Expan (n,z,w))) . k) + (w * (( Expan (n,z,w)) . k))) by VALUED_1: 6

 .= (((z (#) ( Expan (n,z,w))) . k) + ((w (#) ( Expan (n,z,w))) . k)) by VALUED_1: 6

 .= (((z (#) ( Expan (n,z,w))) + (w (#) ( Expan (n,z,w)))) . k) by VALUED_1: 1;

 end;

 then ((z + w) (#) ( Expan (n,z,w))) = ((z (#) ( Expan (n,z,w))) + (w (#) ( Expan (n,z,w))));



 then

 A7: ((z + w) |^ (n + 1)) = ((( Partial_Sums (z (#) ( Expan (n,z,w)))) + ( Partial_Sums (w (#) ( Expan (n,z,w))))) . n) by A6, COMSEQ_3: 27

 .= ((( Partial_Sums (z (#) ( Expan (n,z,w)))) . n) + (( Partial_Sums (w (#) ( Expan (n,z,w)))) . n)) by VALUED_1: 1, A5;



 A8: (( Partial_Sums (z (#) ( Expan (n,z,w)))) . (n + 1)) = ((( Partial_Sums (z (#) ( Expan (n,z,w)))) . n) + ((z (#) ( Expan (n,z,w))) . (n + 1))) by SERIES_1:def 1

 .= ((( Partial_Sums (z (#) ( Expan (n,z,w)))) . n) + (z * (( Expan (n,z,w)) . (n + 1)))) by VALUED_1: 6;

 n < (n + 1) by XREAL_1: 29;

 then

 A9: (( Expan (n,z,w)) . (n + 1)) = 0c by Def9;



 A10: (( Partial_Sums (w (#) ( Expan (n,z,w)))) . (n + 1)) = ((( Partial_Sums (w (#) ( Expan (n,z,w)))) . n) + ((w (#) ( Expan (n,z,w))) . (n + 1))) by SERIES_1:def 1

 .= ((( Partial_Sums (w (#) ( Expan (n,z,w)))) . n) + (w * (( Expan (n,z,w)) . (n + 1)))) by VALUED_1: 6;



 A11: (( Partial_Sums (z (#) ( Expan (n,z,w)))) . (n + 1)) = ((( Partial_Sums ( Shift (z (#) ( Expan (n,z,w))))) . (n + 1)) + ((z (#) ( Expan (n,z,w))) . (n + 1))) by Th5;

 ( 0 + n) < (n + 1) by XREAL_1: 29;

 then (( Expan (n,z,w)) . (n + 1)) = 0c by Def9;

 then (z * (( Expan (n,z,w)) . (n + 1))) = 0c ;



 then

 A12: (( Partial_Sums (z (#) ( Expan (n,z,w)))) . (n + 1)) = ((( Partial_Sums ( Shift (z (#) ( Expan (n,z,w))))) . (n + 1)) + 0c ) by A11, VALUED_1: 6

 .= (( Partial_Sums ( Shift (z (#) ( Expan (n,z,w))))) . (n + 1));

 now

 let k be Element of NAT ;

 A13:

 now

 assume

 A14: (n + 1) < k;



 A15: ( 0 + 1) <= (n + 1) by XREAL_1: 6;



 A16: ((n + 1) - 1) < (k - 1) by A14, XREAL_1: 9;

 then

 A17: (n + 0 ) < ((k - 1) + 1) by XREAL_1: 8;



 A18: (k - 1) = (k -' 1) by A14, A15, XREAL_1: 233, XXREAL_0: 2;

 (((w (#) ( Expan (n,z,w))) + ( Shift (z (#) ( Expan (n,z,w))))) . k) = (((w (#) ( Expan (n,z,w))) . k) + (( Shift (z (#) ( Expan (n,z,w)))) . k)) by VALUED_1: 1

 .= ((w * (( Expan (n,z,w)) . k)) + (( Shift (z (#) ( Expan (n,z,w)))) . k)) by VALUED_1: 6

 .= ((w * (( Expan (n,z,w)) . k)) + ((z (#) ( Expan (n,z,w))) . (k -' 1))) by A17, Th4

 .= ((w * (( Expan (n,z,w)) . k)) + (z * (( Expan (n,z,w)) . (k -' 1)))) by VALUED_1: 6

 .= ((w * 0c ) + (z * (( Expan (n,z,w)) . (k -' 1)))) by A17, Def9

 .= ( 0c + (z * 0c )) by A16, A18, Def9

 .= 0c ;

 hence (((w (#) ( Expan (n,z,w))) + ( Shift (z (#) ( Expan (n,z,w))))) . k) = (( Expan ((n + 1),z,w)) . k) by A14, Def9;

 end;

 now

 assume

 A19: k <= (n + 1);

 A20:

 now

 assume

 A21: k = (n + 1);



 A22: n < (n + 1) by XREAL_1: 29;



 A23: (n -' n) = (n - n) by XREAL_1: 233

 .= 0 ;



 A24: ((n + 1) -' (n + 1)) = ((n + 1) - (n + 1)) by XREAL_1: 233

 .= 0 ;



 A25: (( Coef n) . n) = ((n ! ) / ((n ! ) * ( 0 ! ))) by A23, Def6

 .= 1 by Th1, XCMPLX_1: 60;



 A26: (( Coef (n + 1)) . (n + 1)) = (((n + 1) ! ) / (((n + 1) ! ) * ( 0 ! ))) by A24, Def6

 .= 1 by Th1, XCMPLX_1: 60;

 (((w (#) ( Expan (n,z,w))) + ( Shift (z (#) ( Expan (n,z,w))))) . k) = (((w (#) ( Expan (n,z,w))) . (n + 1)) + (( Shift (z (#) ( Expan (n,z,w)))) . (n + 1))) by A21, VALUED_1: 1

 .= ((w * (( Expan (n,z,w)) . (n + 1))) + (( Shift (z (#) ( Expan (n,z,w)))) . (n + 1))) by VALUED_1: 6

 .= ((w * 0c ) + (( Shift (z (#) ( Expan (n,z,w)))) . (n + 1))) by A22, Def9

 .= ((z (#) ( Expan (n,z,w))) . n) by Def8

 .= (z * (( Expan (n,z,w)) . n)) by VALUED_1: 6

 .= (z * (((( Coef n) . n) * (z |^ n)) * (w |^ (n -' n)))) by Def9

 .= (((( Coef n) . n) * (((z GeoSeq ) . n) * z)) * (w |^ (n -' n)))

 .= (((( Coef (n + 1)) . (n + 1)) * (z |^ (n + 1))) * (w |^ (n -' n))) by A25, A26, COMSEQ_3:def 1

 .= (( Expan ((n + 1),z,w)) . k) by A21, A23, A24, Def9;

 hence (((w (#) ( Expan (n,z,w))) + ( Shift (z (#) ( Expan (n,z,w))))) . k) = (( Expan ((n + 1),z,w)) . k);

 end;

 now

 assume

 A27: k < (n + 1);

 A28:

 now

 assume

 A29: k = 0 ;



 A30: (n -' 0 ) = (n - 0 ) by XREAL_1: 233;



 A31: ((n + 1) -' 0 ) = ((n + 1) - 0 ) by XREAL_1: 233;



 A32: (( Coef n) . 0 ) = ((n ! ) / (( 0 ! ) * (n ! ))) by A30, Def6

 .= 1 by Th1, XCMPLX_1: 60;



 A33: (( Coef (n + 1)) . 0 ) = (((n + 1) ! ) / (( 0 ! ) * ((n + 1) ! ))) by A31, Def6

 .= 1 by Th1, XCMPLX_1: 60;

 (((w (#) ( Expan (n,z,w))) + ( Shift (z (#) ( Expan (n,z,w))))) . k) = (((w (#) ( Expan (n,z,w))) . 0 ) + (( Shift (z (#) ( Expan (n,z,w)))) . 0 )) by A29, VALUED_1: 1

 .= ((w * (( Expan (n,z,w)) . 0 )) + (( Shift (z (#) ( Expan (n,z,w)))) . 0 )) by VALUED_1: 6

 .= ((w * (( Expan (n,z,w)) . 0 )) + 0c ) by Def8

 .= (w * (((( Coef n) . 0 ) * (z |^ 0 )) * (w |^ (n -' 0 )))) by Def9

 .= (((( Coef n) . 0 ) * (z |^ 0 )) * (((w GeoSeq ) . n) * w)) by A30

 .= (((( Coef (n + 1)) . 0 ) * (z |^ 0 )) * (w |^ ((n + 1) -' 0 ))) by A31, A32, A33, COMSEQ_3:def 1

 .= (( Expan ((n + 1),z,w)) . k) by A29, Def9;

 hence (((w (#) ( Expan (n,z,w))) + ( Shift (z (#) ( Expan (n,z,w))))) . k) = (( Expan ((n + 1),z,w)) . k);

 end;

 now

 assume

 A34: k <> 0 ;

 then

 A35: ( 0 + 1) <= k by INT_1: 7;



 A36: ((k + 1) - 1) <= ((n + 1) - 1) by A27, INT_1: 7;

 k < (k + 1) by XREAL_1: 29;

 then (k - 1) <= ((k + 1) - 1) by XREAL_1: 9;

 then (k - 1) <= n by A36, XXREAL_0: 2;

 then

 A37: (k -' 1) <= n by A35, XREAL_1: 233;



 A38: (((w (#) ( Expan (n,z,w))) + ( Shift (z (#) ( Expan (n,z,w))))) . k) = (((w (#) ( Expan (n,z,w))) . k) + (( Shift (z (#) ( Expan (n,z,w)))) . k)) by VALUED_1: 1

 .= ((w * (( Expan (n,z,w)) . k)) + (( Shift (z (#) ( Expan (n,z,w)))) . k)) by VALUED_1: 6

 .= ((w * (( Expan (n,z,w)) . k)) + ((z (#) ( Expan (n,z,w))) . (k -' 1))) by A34, Th4

 .= ((w * (( Expan (n,z,w)) . k)) + (z * (( Expan (n,z,w)) . (k -' 1)))) by VALUED_1: 6

 .= ((w * (((( Coef n) . k) * (z |^ k)) * (w |^ (n -' k)))) + (z * (( Expan (n,z,w)) . (k -' 1)))) by A36, Def9

 .= (((w * ((( Coef n) . k) * (z |^ k))) * (w |^ (n -' k))) + (z * (((( Coef n) . (k -' 1)) * (z |^ (k -' 1))) * (w |^ (n -' (k -' 1)))))) by A37, Def9

 .= (((( Coef n) . k) * ((w * (z |^ k)) * (w |^ (n -' k)))) + ((( Coef n) . (k -' 1)) * (((z |^ (k -' 1)) * z) * (w |^ (n -' (k -' 1))))));



 A39: ((n -' k) + 1) = ((n - k) + 1) by A36, XREAL_1: 233

 .= ((n + 1) - k)

 .= ((n + 1) -' k) by A27, XREAL_1: 233;



 A40: (n -' (k -' 1)) = (n - (k -' 1)) by A37, XREAL_1: 233

 .= (n - (k - 1)) by A35, XREAL_1: 233

 .= ((n + 1) - k)

 .= ((n + 1) -' k) by A27, XREAL_1: 233;

 ((k -' 1) + 1) = ((k - 1) + 1) by A35, XREAL_1: 233

 .= k;

 then

 A41: ((w |^ (n -' k)) * w) = (w |^ ((n -' k) + 1)) & ((z |^ (k -' 1)) * z) = (z |^ k) by COMSEQ_3:def 1;



 A42: ((( Coef n) . k) + (( Coef n) . (k -' 1))) = (((n ! ) / ((k ! ) * ((n -' k) ! ))) + (( Coef n) . (k -' 1))) by A36, Def6

 .= (((n ! ) / ((k ! ) * ((n -' k) ! ))) + ((n ! ) / (((k -' 1) ! ) * ((n -' (k -' 1)) ! )))) by A37, Def6;



 A43: (((k ! ) * ((n -' k) ! )) * (((n + 1) - k) + ( 0 * ))) = ((k ! ) * (((n -' k) ! ) * (((n + 1) - k) + ( 0 * ))));



 A44: ((((k -' 1) ! ) * ((n -' (k -' 1)) ! )) * (k + ( 0 * ))) = (((k + ( 0 * )) * ((k -' 1) ! )) * ((n -' (k -' 1)) ! ))

 .= ((k ! ) * (((n + 1) -' k) ! )) by A34, A40, Th2;

 (((n + 1) - k) + ( 0 * )) <> 0c by A27;



 then

 A45: ((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 A36, A43, Th2;

 ((n ! ) / (((k -' 1) ! ) * ((n -' (k -' 1)) ! ))) = (((n ! ) * (k + ( 0 * ))) / ((k ! ) * (((n + 1) -' k) ! ))) by A34, A44, XCMPLX_1: 91;



 then ((( Coef n) . k) + (( Coef n) . (k -' 1))) = (((n ! ) * ((((n + 1) - k) + k) + (( 0 + 0 ) * ))) / ((k ! ) * (((n + 1) -' k) ! ))) by A42, A45

 .= (((n + 1) ! ) / ((k ! ) * (((n + 1) -' k) ! ))) by Th1

 .= (( Coef (n + 1)) . k) by A27, Def6;



 then (((w (#) ( Expan (n,z,w))) + ( Shift (z (#) ( Expan (n,z,w))))) . k) = (((( Coef (n + 1)) . k) * (z |^ k)) * (w |^ ((n + 1) -' k))) by A38, A39, A40, A41

 .= (( Expan ((n + 1),z,w)) . k) by A27, Def9;

 hence (((w (#) ( Expan (n,z,w))) + ( Shift (z (#) ( Expan (n,z,w))))) . k) = (( Expan ((n + 1),z,w)) . k);

 end;

 hence (((w (#) ( Expan (n,z,w))) + ( Shift (z (#) ( Expan (n,z,w))))) . k) = (( Expan ((n + 1),z,w)) . k) by A28;

 end;

 hence (((w (#) ( Expan (n,z,w))) + ( Shift (z (#) ( Expan (n,z,w))))) . k) = (( Expan ((n + 1),z,w)) . k) by A19, A20, XXREAL_0: 1;

 end;

 hence (((w (#) ( Expan (n,z,w))) + ( Shift (z (#) ( Expan (n,z,w))))) . k) = (( Expan ((n + 1),z,w)) . k) by A13;

 end;

 then

 A46: ((w (#) ( Expan (n,z,w))) + ( Shift (z (#) ( Expan (n,z,w))))) = ( Expan ((n + 1),z,w));



 thus ((z + w) |^ (n + 1)) = ((( Partial_Sums (w (#) ( Expan (n,z,w)))) + ( Partial_Sums ( Shift (z (#) ( Expan (n,z,w)))))) . (n + 1)) by A7, A8, A9, A10, A12, VALUED_1: 1

 .= (( Partial_Sums ( Expan ((n + 1),z,w))) . (n + 1)) by A46, COMSEQ_3: 27;

 end;

 for n holds X[n] from NAT_1:sch 2( A2, A3);

 hence thesis;

 end;

 theorem :: SIN_COS:7



 Th7: ( Expan_e (n,z,w)) = (( 1r / (n ! )) (#) ( Expan (n,z,w)))

 proof

 now

 let k be Element of NAT ;

 A1:

 now

 assume

 A2: n < k;



 hence (( Expan_e (n,z,w)) . k) = (( 1r / (n ! )) * 0c ) by Def10

 .= (( 1r / (n ! )) * (( Expan (n,z,w)) . k)) by A2, Def9

 .= ((( 1r / (n ! )) (#) ( Expan (n,z,w))) . k) by VALUED_1: 6;

 end;

 now

 assume

 A3: k <= n;



 then

 A4: (( Expan_e (n,z,w)) . k) = (((( Coef_e n) . k) * (z |^ k)) * (w |^ (n -' k))) by Def10

 .= ((( 1r / ((k ! ) * ((n -' k) ! ))) * (z |^ k)) * (w |^ (n -' k))) by A3, Def7;

 ( 1r / ((k ! ) * ((n -' k) ! ))) = ((((n ! ) * 1r ) / (n ! )) / ((k ! ) * ((n -' k) ! ))) by XCMPLX_1: 60

 .= ((( 1r / (n ! )) * (n ! )) / ((k ! ) * ((n -' k) ! )));



 hence (( Expan_e (n,z,w)) . k) = (((( 1r / (n ! )) * (n ! )) / ((k ! ) * ((n -' k) ! ))) * ((z |^ k) * (w |^ (n -' k)))) by A4

 .= (( 1r / (n ! )) * ((((n ! ) / ((k ! ) * ((n -' k) ! ))) * (z |^ k)) * (w |^ (n -' k))))

 .= (( 1r / (n ! )) * (((( Coef n) . k) * (z |^ k)) * (w |^ (n -' k)))) by A3, Def6

 .= (( 1r / (n ! )) * (( Expan (n,z,w)) . k)) by A3, Def9

 .= ((( 1r / (n ! )) (#) ( Expan (n,z,w))) . k) by VALUED_1: 6;

 end;

 hence (( Expan_e (n,z,w)) . k) = ((( 1r / (n ! )) (#) ( Expan (n,z,w))) . k) by A1;

 end;

 hence thesis;

 end;

 theorem :: SIN_COS:8



 Th8: (((z + w) |^ n) / (n ! )) = (( Partial_Sums ( Expan_e (n,z,w))) . n)

 proof



 thus (((z + w) |^ n) / (n ! )) = ((( Partial_Sums ( Expan (n,z,w))) . n) * ( 1r / (n ! ))) by Th6

 .= ((( 1r / (n ! )) (#) ( Partial_Sums ( Expan (n,z,w)))) . n) by VALUED_1: 6

 .= (( Partial_Sums (( 1r / (n ! )) (#) ( Expan (n,z,w)))) . n) by COMSEQ_3: 29

 .= (( Partial_Sums ( Expan_e (n,z,w))) . n) by Th7;

 end;

 theorem :: SIN_COS:9



 Th9: (( 0c qua Complex ExpSeq ) is absolutely_summable) & ( Sum ( 0c qua Complex ExpSeq )) = 1r

 proof

 defpred X[ set] means (( Partial_Sums |.( 0c qua Complex ExpSeq ).|) . $1) = jj;

 (( Partial_Sums |.( 0c qua Complex ExpSeq ).|) . 0 ) = ( |.( 0c qua Complex ExpSeq ).| . 0 ) by SERIES_1:def 1

 .= |.(( 0c qua Complex ExpSeq ) . 0 ).| by VALUED_1: 18

 .= 1 by Th3, COMPLEX1: 48;

 then

 A1: X[ 0 ];



 A2: for n be Nat st X[n] holds X[(n + 1)]

 proof

 let n be Nat such that

 A3: (( Partial_Sums |.( 0c qua Complex ExpSeq ).|) . n) = jj;



 thus (( Partial_Sums |.( 0c qua Complex ExpSeq ).|) . (n + 1)) = (1 + ( |.( 0c qua Complex ExpSeq ).| . (n + 1))) by A3, SERIES_1:def 1

 .= (1 + |.(( 0c qua Complex ExpSeq ) . (n + 1)).|) by VALUED_1: 18

 .= (1 + |.(((( 0c qua Complex ExpSeq ) . n) * 0c ) / ((n + 1) + ( 0 * ))).|) by Th3

 .= jj by COMPLEX1: 44;

 end;

 for n be Nat holds X[n] from NAT_1:sch 2( A1, A2);

 then ( Partial_Sums |.( 0c qua Complex ExpSeq ).|) is constant by VALUED_0:def 18;

 then

 A4: |.( 0c qua Complex ExpSeq ).| is summable by SERIES_1:def 2;

 defpred X[ set] means (( Partial_Sums ( 0c qua Complex ExpSeq )) . $1) = 1;

 (( Partial_Sums ( 0c qua Complex ExpSeq )) . 0 ) = (( 0c qua Complex ExpSeq ) . 0 ) by SERIES_1:def 1

 .= 1 by Th3;

 then

 A5: X[ 0 ];



 A6: for n st X[n] holds X[(n + 1)]

 proof

 let n such that

 A7: (( Partial_Sums ( 0c qua Complex ExpSeq )) . n) = 1;



 thus (( Partial_Sums ( 0c qua Complex ExpSeq )) . (n + 1)) = ( 1r + (( 0c qua Complex ExpSeq ) . (n + 1))) by A7, SERIES_1:def 1

 .= ( 1r + (((( 0c qua Complex ExpSeq ) . n) * 0c ) / ((n + 1) + ( 0 * )))) by Th3

 .= 1;

 end;

 for n holds X[n] from NAT_1:sch 2( A5, A6);

 hence thesis by A4, COMSEQ_2: 10;

 end;

 registration

 let z be Complex;

 cluster (z ExpSeq ) -> absolutely_summable;

 coherence

 proof

 now

 assume

 A1: z <> 0c ;

 defpred X[ set] means ((z ExpSeq ) . $1) <> 0c ;



 A2: X[ 0 ] by Th3;



 A3: for n st X[n] holds X[(n + 1)]

 proof

 let n;

 assume

 A4: ((z ExpSeq ) . n) <> 0c ;

 thus ((z ExpSeq ) . (n + 1)) <> 0c

 proof

 assume ((z ExpSeq ) . (n + 1)) = 0c ;

 then

 A5: ((((z ExpSeq ) . n) * z) / ((n + 1) + ( 0 * ))) = 0c by Th3;

 0c = ( 0c / z)

 .= ((((z ExpSeq ) . n) * z) / z) by A5, XCMPLX_1: 50

 .= (((z ExpSeq ) . n) * (z / z))

 .= (((z ExpSeq ) . n) * 1) by A1, XCMPLX_1: 60

 .= ((z ExpSeq ) . n);

 hence contradiction by A4;

 end;

 end;

 deffunc U( Nat) = (( |.(z ExpSeq ).| . ($1 + 1)) / ( |.(z ExpSeq ).| . $1));

 thus

 A6: for n holds X[n] from NAT_1:sch 2( A2, A3);

 ex rseq st for n holds (rseq . n) = U(n) from SEQ_1:sch 1;

 then

 consider rseq such that

 A7: for n holds (rseq . n) = (( |.(z ExpSeq ).| . (n + 1)) / ( |.(z ExpSeq ).| . n));

 now

 let n;



 thus (rseq . n) = (( |.(z ExpSeq ).| . (n + 1)) / ( |.(z ExpSeq ).| . n)) by A7

 .= ( |.((z ExpSeq ) . (n + 1)).| / ( |.(z ExpSeq ).| . n)) by VALUED_1: 18

 .= ( |.((z ExpSeq ) . (n + 1)).| / |.((z ExpSeq ) . n).|) by VALUED_1: 18

 .= |.(((z ExpSeq ) . (n + 1)) / ((z ExpSeq ) . n)).| by COMPLEX1: 67

 .= |.(((((z ExpSeq ) . n) * z) / ((n + 1) + ( 0 * ))) / ((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.| / |.(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 :: SIN_COS:10



 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 :: SIN_COS:11



 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 :: SIN_COS:12



 Th12: (( Partial_Sums ( Alfa ((k + 1),z,w))) . k) = ((( Partial_Sums ( Alfa (k,z,w))) . k) + (( Partial_Sums ( Expan_e ((k + 1),z,w))) . k))

 proof



 A1: k in NAT by ORDINAL1:def 12;

 now

 let l be Nat;



 A2: l in NAT by ORDINAL1:def 12;

 assume l <= k;



 hence (( Alfa ((k + 1),z,w)) . l) = ((( Alfa (k,z,w)) . l) + (( Expan_e ((k + 1),z,w)) . l)) by Th11

 .= ((( Alfa (k,z,w)) + ( Expan_e ((k + 1),z,w))) . l) by VALUED_1: 1, A2;

 end;



 hence (( Partial_Sums ( Alfa ((k + 1),z,w))) . k) = (( Partial_Sums (( Alfa (k,z,w)) + ( Expan_e ((k + 1),z,w)))) . k) by COMSEQ_3: 35

 .= ((( Partial_Sums ( Alfa (k,z,w))) + ( Partial_Sums ( Expan_e ((k + 1),z,w)))) . k) by COMSEQ_3: 27

 .= ((( Partial_Sums ( Alfa (k,z,w))) . k) + (( Partial_Sums ( Expan_e ((k + 1),z,w))) . k)) by VALUED_1: 1, A1;

 end;

 theorem :: SIN_COS:13



 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 :: SIN_COS:14



 Th14: (( Partial_Sums ((z + w) ExpSeq )) . n) = (( Partial_Sums ( Alfa (n,z,w))) . n)

 proof



 A1: (( Partial_Sums ((z + w) ExpSeq )) . 0 ) = (((z + w) ExpSeq ) . 0 ) by SERIES_1:def 1

 .= 1 by Th10;

 defpred X[ Nat] means (( Partial_Sums ((z + w) ExpSeq )) . $1) = (( Partial_Sums ( Alfa ($1,z,w))) . $1);



 A2: ( 0 -' 0 ) = 0 by XREAL_1: 232;

 (( Partial_Sums ( Alfa ( 0 ,z,w))) . 0 ) = (( Alfa ( 0 ,z,w)) . 0 ) by SERIES_1:def 1

 .= (((z ExpSeq ) . 0 ) * (( Partial_Sums (w ExpSeq )) . 0 )) by A2, Def11

 .= (((z ExpSeq ) . 0 ) * ((w ExpSeq ) . 0 )) by SERIES_1:def 1

 .= ( 1r * ((w ExpSeq ) . 0 )) by Th10

 .= 1 by Th10;

 then

 A3: X[ 0 ] by A1;



 A4: for k st X[k] holds X[(k + 1)]

 proof

 let k such that

 A5: (( Partial_Sums ((z + w) ExpSeq )) . k) = (( Partial_Sums ( Alfa (k,z,w))) . k);



 A6: (( Partial_Sums ( Alfa ((k + 1),z,w))) . (k + 1)) = ((( Partial_Sums ( Alfa ((k + 1),z,w))) . k) + (( Alfa ((k + 1),z,w)) . (k + 1))) by SERIES_1:def 1

 .= (((( Partial_Sums ( Alfa (k,z,w))) . k) + (( Partial_Sums ( Expan_e ((k + 1),z,w))) . k)) + (( Alfa ((k + 1),z,w)) . (k + 1))) by Th12

 .= ((( Partial_Sums ((z + w) ExpSeq )) . k) + ((( Partial_Sums ( Expan_e ((k + 1),z,w))) . k) + (( Alfa ((k + 1),z,w)) . (k + 1)))) by A5;

 ((k + 1) -' (k + 1)) = 0 by XREAL_1: 232;



 then (( Alfa ((k + 1),z,w)) . (k + 1)) = (((z ExpSeq ) . (k + 1)) * (( Partial_Sums (w ExpSeq )) . 0 )) by Def11

 .= (((z ExpSeq ) . (k + 1)) * ((w ExpSeq ) . 0 )) by SERIES_1:def 1

 .= (((z ExpSeq ) . (k + 1)) * 1) by Th10

 .= (( Expan_e ((k + 1),z,w)) . (k + 1)) by Th13;



 then ((( Partial_Sums ( Expan_e ((k + 1),z,w))) . k) + (( Alfa ((k + 1),z,w)) . (k + 1))) = (( Partial_Sums ( Expan_e ((k + 1),z,w))) . (k + 1)) by SERIES_1:def 1

 .= (((z + w) |^ (k + 1)) / ((k + 1) ! )) by Th8;



 then (( Partial_Sums ( Alfa ((k + 1),z,w))) . (k + 1)) = ((( Partial_Sums ((z + w) ExpSeq )) . k) + (((z + w) ExpSeq ) . (k + 1))) by A6, Def4

 .= (( Partial_Sums ((z + w) ExpSeq )) . (k + 1)) by SERIES_1:def 1;

 hence (( Partial_Sums ((z + w) ExpSeq )) . (k + 1)) = (( Partial_Sums ( Alfa ((k + 1),z,w))) . (k + 1));

 end;

 for n holds X[n] from NAT_1:sch 2( A3, A4);

 hence thesis;

 end;

 theorem :: SIN_COS:15



 Th15: (((( Partial_Sums (z ExpSeq )) . k) * (( Partial_Sums (w ExpSeq )) . k)) - (( Partial_Sums ((z + w) ExpSeq )) . k)) = (( Partial_Sums ( Conj (k,z,w))) . k)

 proof



 A1: k in NAT by ORDINAL1:def 12;



 A2: (((( Partial_Sums (z ExpSeq )) . k) * (( Partial_Sums (w ExpSeq )) . k)) - (( Partial_Sums ((z + w) ExpSeq )) . k)) = (((( Partial_Sums (z ExpSeq )) . k) * (( Partial_Sums (w ExpSeq )) . k)) - (( Partial_Sums ( Alfa (k,z,w))) . k)) by Th14

 .= ((((( Partial_Sums (w ExpSeq )) . k) (#) ( Partial_Sums (z ExpSeq ))) . k) - (( Partial_Sums ( Alfa (k,z,w))) . k)) by VALUED_1: 6

 .= ((( Partial_Sums ((( Partial_Sums (w ExpSeq )) . k) (#) (z ExpSeq ))) . k) - (( Partial_Sums ( Alfa (k,z,w))) . k)) by COMSEQ_3: 29

 .= ((( Partial_Sums ((( Partial_Sums (w ExpSeq )) . k) (#) (z ExpSeq ))) . k) + (( - ( Partial_Sums ( Alfa (k,z,w)))) . k)) by VALUED_1: 8

 .= ((( Partial_Sums ((( Partial_Sums (w ExpSeq )) . k) (#) (z ExpSeq ))) - ( Partial_Sums ( Alfa (k,z,w)))) . k) by VALUED_1: 1, A1

 .= (( Partial_Sums (((( Partial_Sums (w ExpSeq )) . k) (#) (z ExpSeq )) - ( Alfa (k,z,w)))) . k) by COMSEQ_3: 28;

 for l be Nat st l <= k holds ((((( Partial_Sums (w ExpSeq )) . k) (#) (z ExpSeq )) - ( Alfa (k,z,w))) . l) = (( Conj (k,z,w)) . l)

 proof

 let l be Nat such that

 A3: l <= k;



 A4: l in NAT by ORDINAL1:def 12;



 thus ((((( Partial_Sums (w ExpSeq )) . k) (#) (z ExpSeq )) - ( Alfa (k,z,w))) . l) = ((((( Partial_Sums (w ExpSeq )) . k) (#) (z ExpSeq )) . l) + (( - ( Alfa (k,z,w))) . l)) by VALUED_1: 1, A4

 .= ((((( Partial_Sums (w ExpSeq )) . k) (#) (z ExpSeq )) . l) - (( Alfa (k,z,w)) . l)) by VALUED_1: 8

 .= (((( Partial_Sums (w ExpSeq )) . k) * ((z ExpSeq ) . l)) - (( Alfa (k,z,w)) . l)) by VALUED_1: 6

 .= ((((z ExpSeq ) . l) * (( Partial_Sums (w ExpSeq )) . k)) - (((z ExpSeq ) . l) * (( Partial_Sums (w ExpSeq )) . (k -' l)))) by A3, Def11

 .= (((z ExpSeq ) . l) * ((( Partial_Sums (w ExpSeq )) . k) - (( Partial_Sums (w ExpSeq )) . (k -' l))))

 .= (( Conj (k,z,w)) . l) by A3, Def13;

 end;

 hence thesis by A2, COMSEQ_3: 35;

 end;

 theorem :: SIN_COS:16



 Th16: |.(( Partial_Sums (z ExpSeq )) . k).| <= (( Partial_Sums ( |.z.| rExpSeq )) . k) & (( Partial_Sums ( |.z.| rExpSeq )) . k) <= ( Sum ( |.z.| rExpSeq )) & |.(( Partial_Sums (z ExpSeq )) . k).| <= ( Sum ( |.z.| rExpSeq ))

 proof

 defpred X[ Nat] means |.(( Partial_Sums (z ExpSeq )) . $1).| <= (( Partial_Sums ( |.z.| rExpSeq )) . $1);



 A1: |.(( Partial_Sums (z ExpSeq )) . 0 ).| = |.((z ExpSeq ) . 0 ).| by SERIES_1:def 1

 .= |.((z |^ 0 ) / ( 0 ! )).| by Def4

 .= 1 by Th1, COMPLEX1: 48, COMSEQ_3:def 1;

 (( Partial_Sums ( |.z.| rExpSeq )) . 0 ) = (( |.z.| rExpSeq ) . 0 ) by SERIES_1:def 1

 .= (( |.z.| |^ 0 ) / ( 0 ! )) by Def5

 .= 1 by NEWTON: 4, NEWTON: 12;

 then

 A2: X[ 0 ] by A1;



 A3: for k st X[k] holds X[(k + 1)]

 proof

 let k such that

 A4: |.(( Partial_Sums (z ExpSeq )) . k).| <= (( Partial_Sums ( |.z.| rExpSeq )) . k);

 |.(( Partial_Sums (z ExpSeq )) . (k + 1)).| = |.((( Partial_Sums (z ExpSeq )) . k) + ((z ExpSeq ) . (k + 1))).| & |.((( Partial_Sums (z ExpSeq )) . k) + ((z ExpSeq ) . (k + 1))).| <= ( |.(( Partial_Sums (z ExpSeq )) . k).| + |.((z ExpSeq ) . (k + 1)).|) by COMPLEX1: 56, SERIES_1:def 1;

 then

 A5: |.(( Partial_Sums (z ExpSeq )) . (k + 1)).| <= ( |.(( Partial_Sums (z ExpSeq )) . k).| + (( |.z.| rExpSeq ) . (k + 1))) by Th3;



 A6: ( |.(( Partial_Sums (z ExpSeq )) . k).| + (( |.z.| rExpSeq ) . (k + 1))) <= ((( Partial_Sums ( |.z.| rExpSeq )) . k) + (( |.z.| rExpSeq ) . (k + 1))) by A4, XREAL_1: 6;

 ((( Partial_Sums ( |.z.| rExpSeq )) . k) + (( |.z.| rExpSeq ) . (k + 1))) = (( Partial_Sums ( |.z.| rExpSeq )) . (k + 1)) by SERIES_1:def 1;

 hence thesis by A5, A6, XXREAL_0: 2;

 end;



 A7: for k holds X[k] from NAT_1:sch 2( A2, A3);

 hence |.(( Partial_Sums (z ExpSeq )) . k).| <= (( Partial_Sums ( |.z.| rExpSeq )) . k);

 now

 let k be object such that

 A8: k in NAT ;



 thus ( |.(z ExpSeq ).| . k) = |.((z ExpSeq ) . k).| by VALUED_1: 18

 .= (( |.z.| rExpSeq ) . k) by A8, Th3;

 end;

 then

 A9: |.(z ExpSeq ).| = ( |.z.| rExpSeq );

 then (( Partial_Sums ( |.z.| rExpSeq )) . k) <= ( lim ( Partial_Sums ( |.z.| rExpSeq ))) by SEQ_4: 37;

 hence (( Partial_Sums ( |.z.| rExpSeq )) . k) <= ( Sum ( |.z.| rExpSeq )) by SERIES_1:def 3;

 A10:

 now

 let k;

 ( lim ( Partial_Sums ( |.z.| rExpSeq ))) = ( Sum ( |.z.| rExpSeq )) by SERIES_1:def 3;

 hence (( Partial_Sums ( |.z.| rExpSeq )) . k) <= ( Sum ( |.z.| rExpSeq )) by A9, SEQ_4: 37;

 end;



 A11: |.(( Partial_Sums (z ExpSeq )) . k).| <= (( Partial_Sums ( |.z.| rExpSeq )) . k) by A7;

 (( Partial_Sums ( |.z.| rExpSeq )) . k) <= ( Sum ( |.z.| rExpSeq )) by A10;

 hence thesis by A11, XXREAL_0: 2;

 end;

 theorem :: SIN_COS:17



 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 :: SIN_COS:18



 Th18: 0 <= (( |.z.| rExpSeq ) . n)

 proof

 (( |.z.| rExpSeq ) . n) = |.((z ExpSeq ) . n).| by Th3;

 hence thesis by COMPLEX1: 46;

 end;

 theorem :: SIN_COS:19



 Th19: |.(( Partial_Sums ( |.z.| rExpSeq )) . n).| = (( Partial_Sums ( |.z.| rExpSeq )) . n) & (n <= m implies |.((( Partial_Sums ( |.z.| rExpSeq )) . m) - (( Partial_Sums ( |.z.| rExpSeq )) . n)).| = ((( Partial_Sums ( |.z.| rExpSeq )) . m) - (( Partial_Sums ( |.z.| rExpSeq )) . n)))

 proof

 for n holds 0 <= (( |.z.| rExpSeq ) . n) by Th18;

 hence thesis by COMSEQ_3: 9;

 end;

 theorem :: SIN_COS:20



 Th20: |.(( Partial_Sums |.( Conj (k,z,w)).|) . n).| = (( Partial_Sums |.( Conj (k,z,w)).|) . n)

 proof

 A1:

 now

 let n;

 ( |.( Conj (k,z,w)).| . n) = |.(( Conj (k,z,w)) . n).| by VALUED_1: 18;

 hence 0 <= ( |.( Conj (k,z,w)).| . n) by COMPLEX1: 46;

 end;



 A2: (( Partial_Sums |.( Conj (k,z,w)).|) . 0 ) <= (( Partial_Sums |.( Conj (k,z,w)).|) . n) & (( Partial_Sums |.( Conj (k,z,w)).|) . 0 ) = ( |.( Conj (k,z,w)).| . 0 ) by SEQM_3: 6, SERIES_1:def 1;

 0 <= ( |.( Conj (k,z,w)).| . 0 ) by A1;

 hence thesis by A2, ABSVALUE:def 1;

 end;

 theorem :: SIN_COS:21



 Th21: for p be Real st p > 0 holds ex n st for k st n <= k holds |.(( Partial_Sums |.( Conj (k,z,w)).|) . k).| 0 ;

 reconsider pp = p as Real;



 A2: 1 <= ( Sum ( |.z.| rExpSeq )) by Th17;



 A3: 0 < ( Sum ( |.w.| rExpSeq )) by Th17;

 set p1 = ( min ((pp / (4 * ( Sum ( |.z.| rExpSeq )))),(pp / (4 * ( Sum ( |.w.| rExpSeq ))))));



 A4: p1 > 0 by A1, A2, A3, XXREAL_0: 15;

 now

 let k be object such that

 A5: k in NAT ;



 thus ( |.(z ExpSeq ).| . k) = |.((z ExpSeq ) . k).| by VALUED_1: 18

 .= (( |.z.| rExpSeq ) . k) by A5, Th3;

 end;

 then |.(z ExpSeq ).| = ( |.z.| rExpSeq );

 then

 consider n1 such that

 A6: for k,l be Nat st n1 <= k & n1 <= l holds |.((( Partial_Sums ( |.z.| rExpSeq )) . k) - (( Partial_Sums ( |.z.| rExpSeq )) . l)).| < p1 by A4, COMSEQ_3: 4;

 consider n2 be Nat such that

 A7: for k,l be Nat st n2 <= k & n2 <= l holds |.((( Partial_Sums (w ExpSeq )) . k) - (( Partial_Sums (w ExpSeq )) . l)).| < p1 by A4, COMSEQ_3: 47;

 set n3 = (n1 + n2);

 take n4 = (n3 + n3);

 A8:

 now

 let n;

 let k;

 now

 let l be Nat such that

 A9: l <= k;



 thus ( |.( Conj (k,z,w)).| . l) = |.(( Conj (k,z,w)) . l).| by VALUED_1: 18

 .= |.(((z ExpSeq ) . l) * ((( Partial_Sums (w ExpSeq )) . k) - (( Partial_Sums (w ExpSeq )) . (k -' l)))).| by A9, Def13

 .= ( |.((z ExpSeq ) . l).| * |.((( Partial_Sums (w ExpSeq )) . k) - (( Partial_Sums (w ExpSeq )) . (k -' l))).|) by COMPLEX1: 65

 .= ((( |.z.| rExpSeq ) . l) * |.((( Partial_Sums (w ExpSeq )) . k) - (( Partial_Sums (w ExpSeq )) . (k -' l))).|) by Th3;

 end;

 hence for l be Nat st l <= k holds ( |.( Conj (k,z,w)).| . l) = ((( |.z.| rExpSeq ) . l) * |.((( Partial_Sums (w ExpSeq )) . k) - (( Partial_Sums (w ExpSeq )) . (k -' l))).|);

 end;

 A10:

 now

 let k;

 now

 let l be Nat;

 assume l <= k;

 then

 A11: ( |.( Conj (k,z,w)).| . l) = ((( |.z.| rExpSeq ) . l) * |.((( Partial_Sums (w ExpSeq )) . k) - (( Partial_Sums (w ExpSeq )) . (k -' l))).|) by A8;

 |.(( Partial_Sums (w ExpSeq )) . k).| <= ( Sum ( |.w.| rExpSeq )) by Th16;

 then

 A12: ( |.(( Partial_Sums (w ExpSeq )) . k).| + |.(( Partial_Sums (w ExpSeq )) . (k -' l)).|) <= (( Sum ( |.w.| rExpSeq )) + |.(( Partial_Sums (w ExpSeq )) . (k -' l)).|) by XREAL_1: 6;

 |.(( Partial_Sums (w ExpSeq )) . (k -' l)).| <= ( Sum ( |.w.| rExpSeq )) by Th16;

 then (( Sum ( |.w.| rExpSeq )) + |.(( Partial_Sums (w ExpSeq )) . (k -' l)).|) <= (( Sum ( |.w.| rExpSeq )) + ( Sum ( |.w.| rExpSeq ))) by XREAL_1: 6;

 then |.((( Partial_Sums (w ExpSeq )) . k) - (( Partial_Sums (w ExpSeq )) . (k -' l))).| <= ( |.(( Partial_Sums (w ExpSeq )) . k).| + |.(( Partial_Sums (w ExpSeq )) . (k -' l)).|) & ( |.(( Partial_Sums (w ExpSeq )) . k).| + |.(( Partial_Sums (w ExpSeq )) . (k -' l)).|) <= (2 * ( Sum ( |.w.| rExpSeq ))) by A12, COMPLEX1: 57, XXREAL_0: 2;

 then

 A13: |.((( Partial_Sums (w ExpSeq )) . k) - (( Partial_Sums (w ExpSeq )) . (k -' l))).| <= (2 * ( Sum ( |.w.| rExpSeq ))) by XXREAL_0: 2;

 0 <= (( |.z.| rExpSeq ) . l) by Th18;

 hence ( |.( Conj (k,z,w)).| . l) <= ((( |.z.| rExpSeq ) . l) * (2 * ( Sum ( |.w.| rExpSeq )))) by A11, A13, XREAL_1: 64;

 end;

 hence for l be Nat st l <= k holds ( |.( Conj (k,z,w)).| . l) <= ((( |.z.| rExpSeq ) . l) * (2 * ( Sum ( |.w.| rExpSeq ))));

 end;

 now

 let k such that

 A14: n4 <= k;



 A15: ( 0 + n3) <= (n3 + n3) by XREAL_1: 6;

 then

 A16: n3 <= k by A14, XXREAL_0: 2;



 A17: (n1 + 0 ) <= (n1 + n2) by XREAL_1: 6;

 then

 A18: n1 <= k by A16, XXREAL_0: 2;

 now

 let l be Nat;

 assume

 A19: l <= n3;

 then

 A20: (k -' l) = (k - l) by A16, XREAL_1: 233, XXREAL_0: 2;



 A21: ( 0 + n2) <= (n1 + n2) by XREAL_1: 6;



 A22: (n4 - l) <= (k - l) by A14, XREAL_1: 9;

 ((n3 + n3) - n3) <= ((n3 + n3) - l) by A19, XREAL_1: 10;

 then n3 <= (k - l) by A22, XXREAL_0: 2;

 then

 A23: n2 <= (k -' l) by A20, A21, XXREAL_0: 2;

 ( 0 + n3) <= (n3 + n3) by XREAL_1: 6;

 then n2 <= n4 by A21, XXREAL_0: 2;

 then n2 <= k by A14, XXREAL_0: 2;

 then

 A24: |.((( Partial_Sums (w ExpSeq )) . k) - (( Partial_Sums (w ExpSeq )) . (k -' l))).| < p1 by A7, A23;

 0 <= (( |.z.| rExpSeq ) . l) by Th18;

 then ((( |.z.| rExpSeq ) . l) * |.((( Partial_Sums (w ExpSeq )) . k) - (( Partial_Sums (w ExpSeq )) . (k -' l))).|) <= ((( |.z.| rExpSeq ) . l) * p1) by A24, XREAL_1: 64;

 hence ( |.( Conj (k,z,w)).| . l) <= (p1 * (( |.z.| rExpSeq ) . l)) by A8, A16, A19, XXREAL_0: 2;

 end;

 then

 A25: (( Partial_Sums |.( Conj (k,z,w)).|) . n3) <= ((( Partial_Sums ( |.z.| rExpSeq )) . n3) * p1) by COMSEQ_3: 7;

 ((( Partial_Sums ( |.z.| rExpSeq )) . n3) * p1) <= (( Sum ( |.z.| rExpSeq )) * p1) by A4, Th16, XREAL_1: 64;

 then

 A26: (( Partial_Sums |.( Conj (k,z,w)).|) . n3) <= (( Sum ( |.z.| rExpSeq )) * p1) by A25, XXREAL_0: 2;



 A27: (( Sum ( |.z.| rExpSeq )) * p1) <= (( Sum ( |.z.| rExpSeq )) * (p / (4 * ( Sum ( |.z.| rExpSeq ))))) by A2, XREAL_1: 64, XXREAL_0: 17;



 A28: 0 <> ( Sum ( |.z.| rExpSeq )) by Th17;

 (( Sum ( |.z.| rExpSeq )) * (p / (4 * ( Sum ( |.z.| rExpSeq ))))) = ((( Sum ( |.z.| rExpSeq )) * p) / (4 * ( Sum ( |.z.| rExpSeq ))))

 .= (p / 4) by A28, XCMPLX_1: 91;

 then

 A29: (( Partial_Sums |.( Conj (k,z,w)).|) . n3) <= (p / 4) by A26, A27, XXREAL_0: 2;

 ( 0 + (p / 4)) < ((p / 4) + (p / 4)) by A1, XREAL_1: 6;

 then

 A30: (( Partial_Sums |.( Conj (k,z,w)).|) . n3) < (p / 2) by A29, XXREAL_0: 2;

 (k -' n3) = (k - n3) by A14, A15, XREAL_1: 233, XXREAL_0: 2;

 then

 A31: k = ((k -' n3) + n3);

 for l be Nat st l <= k holds ( |.( Conj (k,z,w)).| . l) <= ((2 * ( Sum ( |.w.| rExpSeq ))) * (( |.z.| rExpSeq ) . l)) by A10;

 then

 A32: ((( Partial_Sums |.( Conj (k,z,w)).|) . k) - (( Partial_Sums |.( Conj (k,z,w)).|) . n3)) <= (((( Partial_Sums ( |.z.| rExpSeq )) . k) - (( Partial_Sums ( |.z.| rExpSeq )) . n3)) * (2 * ( Sum ( |.w.| rExpSeq )))) by A31, COMSEQ_3: 8;

 |.((( Partial_Sums ( |.z.| rExpSeq )) . k) - (( Partial_Sums ( |.z.| rExpSeq )) . n3)).| <= p1 by A6, A17, A18;

 then ((( Partial_Sums ( |.z.| rExpSeq )) . k) - (( Partial_Sums ( |.z.| rExpSeq )) . n3)) <= p1 by A14, A15, Th19, XXREAL_0: 2;

 then (((( Partial_Sums ( |.z.| rExpSeq )) . k) - (( Partial_Sums ( |.z.| rExpSeq )) . n3)) * (2 * ( Sum ( |.w.| rExpSeq )))) <= (p1 * (2 * ( Sum ( |.w.| rExpSeq )))) by A3, XREAL_1: 64;

 then

 A33: ((( Partial_Sums |.( Conj (k,z,w)).|) . k) - (( Partial_Sums |.( Conj (k,z,w)).|) . n3)) <= (p1 * (2 * ( Sum ( |.w.| rExpSeq )))) by A32, XXREAL_0: 2;



 A34: ((2 * ( Sum ( |.w.| rExpSeq ))) * p1) <= ((2 * ( Sum ( |.w.| rExpSeq ))) * (p / (4 * ( Sum ( |.w.| rExpSeq ))))) by A3, XREAL_1: 64, XXREAL_0: 17;



 A35: 0 <> ( Sum ( |.w.| rExpSeq )) by Th17;

 ((2 * ( Sum ( |.w.| rExpSeq ))) * (p / (4 * ( Sum ( |.w.| rExpSeq ))))) = (((2 * p) * ( Sum ( |.w.| rExpSeq ))) / (4 * ( Sum ( |.w.| rExpSeq ))))

 .= ((p + p) / 4) by A35, XCMPLX_1: 91

 .= (p / 2);

 then ((( Partial_Sums |.( Conj (k,z,w)).|) . k) - (( Partial_Sums |.( Conj (k,z,w)).|) . n3)) <= (p / 2) by A33, A34, XXREAL_0: 2;

 then (((( Partial_Sums |.( Conj (k,z,w)).|) . k) - (( Partial_Sums |.( Conj (k,z,w)).|) . n3)) + (( Partial_Sums |.( Conj (k,z,w)).|) . n3)) < ((p / 2) + (p / 2)) by A30, XREAL_1: 8;

 hence |.(( Partial_Sums |.( Conj (k,z,w)).|) . k).| < p by Th20;

 end;

 hence thesis;

 end;

 theorem :: SIN_COS:22



 Th22: (for k holds (seq . k) = (( Partial_Sums ( Conj (k,z,w))) . k)) implies seq is convergent & ( lim seq) = 0

 proof

 now

 let seq such that

 A1: for k holds (seq . k) = (( Partial_Sums ( Conj (k,z,w))) . k);

 A2:

 now

 let k;

 |.(seq . k).| = |.(( Partial_Sums ( Conj (k,z,w))) . k).| by A1;

 hence |.(seq . k).| <= (( Partial_Sums |.( Conj (k,z,w)).|) . k) by COMSEQ_3: 30;

 end;

 deffunc U( Nat) = (( Partial_Sums |.( Conj ($1,z,w)).|) . $1);

 ex rseq be Real_Sequence st for k holds (rseq . k) = U(k) from SEQ_1:sch 1;

 then

 consider rseq be Real_Sequence such that

 A3: for k holds (rseq . k) = (( Partial_Sums |.( Conj (k,z,w)).|) . k);

 A4:

 now

 let k;

 |.(seq . k).| <= (( Partial_Sums |.( Conj (k,z,w)).|) . k) by A2;

 hence |.(seq . k).| <= (rseq . k) by A3;

 end;

 A5:

 now

 let p be Real;

 assume p > 0 ;

 then

 consider n such that

 A6: for k st n <= k holds |.(( Partial_Sums |.( Conj (k,z,w)).|) . k).| < p by Th21;

 take n;

 now

 let k such that

 A7: n <= k;

 |.((rseq . k) - 0 ).| = |.(( Partial_Sums |.( Conj (k,z,w)).|) . k).| by A3;

 hence |.((rseq . k) - 0 ).| < p by A6, A7;

 end;

 hence for k st n <= k holds |.((rseq . k) - 0 ).| < p;

 end;

 then

 A8: rseq is convergent by SEQ_2:def 6;

 then ( lim rseq) = 0 by A5, SEQ_2:def 7;

 hence seq is convergent & ( lim seq) = 0c by A4, A8, COMSEQ_3: 48;

 end;

 hence thesis;

 end;



 Lm2: for z,w be Complex holds (( Sum (z ExpSeq )) * ( Sum (w ExpSeq ))) = ( Sum ((z + w) ExpSeq ))

 proof

 let z0,w0 be Complex;

 reconsider z = z0, w = w0 as Element of COMPLEX by XCMPLX_0:def 2;

 deffunc U( Nat) = (( Partial_Sums ( Conj ($1,z,w))) . $1);

 ex seq st for k holds (seq . k) = U(k) from COMSEQ_1:sch 1;

 then

 consider seq such that

 A1: for k holds (seq . k) = (( Partial_Sums ( Conj (k,z,w))) . k);

 now

 let k be Element of NAT ;



 thus (seq . k) = (( Partial_Sums ( Conj (k,z,w))) . k) by A1

 .= (((( Partial_Sums (z ExpSeq )) . k) * (( Partial_Sums (w ExpSeq )) . k)) - (( Partial_Sums ((z + w) ExpSeq )) . k)) by Th15

 .= (((( Partial_Sums (z ExpSeq )) (#) ( Partial_Sums (w ExpSeq ))) . k) - (( Partial_Sums ((z + w) ExpSeq )) . k)) by VALUED_1: 5

 .= (((( Partial_Sums (z ExpSeq )) (#) ( Partial_Sums (w ExpSeq ))) . k) + (( - ( Partial_Sums ((z + w) ExpSeq ))) . k)) by VALUED_1: 8

 .= (((( Partial_Sums (z ExpSeq )) (#) ( Partial_Sums (w ExpSeq ))) - ( Partial_Sums ((z + w) ExpSeq ))) . k) by VALUED_1: 1;

 end;

 then

 A2: seq = ((( Partial_Sums (z ExpSeq )) (#) ( Partial_Sums (w ExpSeq ))) - ( Partial_Sums ((z + w) ExpSeq )));



 A3: (( Partial_Sums (z ExpSeq )) (#) ( Partial_Sums (w ExpSeq ))) is convergent & ( lim (( Partial_Sums (z ExpSeq )) (#) ( Partial_Sums (w ExpSeq )))) = (( lim ( Partial_Sums (z ExpSeq ))) * ( lim ( Partial_Sums (w ExpSeq )))) by COMSEQ_2: 30;

 ( lim seq) = 0c by A1, Th22;

 hence thesis by A2, A3, COMSEQ_3: 10;

 end;

 begin

 definition

 :: SIN_COS:def14

 func exp -> Function of COMPLEX , COMPLEX means

 : Def14: for z be Complex holds (it . z) = ( Sum (z ExpSeq ));

 existence

 proof

 deffunc U( Element of COMPLEX ) = ( Sum ($1 ExpSeq ));

 consider f be Function of COMPLEX , COMPLEX such that

 A1: for x be Element of COMPLEX holds (f . x) = U(x) from FUNCT_2:sch 4;

 take f;

 let z be Complex;

 z in COMPLEX by XCMPLX_0:def 2;

 hence thesis by A1;

 end;

 uniqueness

 proof

 let f1,f2 be Function of COMPLEX , COMPLEX ;

 assume

 A2: for z be Complex holds (f1 . z) = ( Sum (z ExpSeq ));

 assume

 A3: for z be Complex holds (f2 . z) = ( Sum (z ExpSeq ));

 for z be Element of COMPLEX holds (f1 . z) = (f2 . z)

 proof

 let z be Element of COMPLEX ;



 thus (f1 . z) = ( Sum (z ExpSeq )) by A2

 .= (f2 . z) by A3;

 end;

 hence f1 = f2;

 end;

 end

 definition

 let z be Complex;

 :: SIN_COS:def15

 func exp z -> Complex equals ( exp . z);

 coherence ;

 end

 definition

 let z be Complex;

 :: original: exp

 redefine

 func exp z -> Element of COMPLEX ;

 coherence by XCMPLX_0:def 2;

 end

 theorem :: SIN_COS:23

 for z1,z2 be Complex holds ( exp (z1 + z2)) = (( exp z1) * ( exp z2))

 proof

 let z1,z2 be Complex;

 ( exp (z1 + z2)) = ( Sum ((z1 + z2) ExpSeq )) by Def14

 .= (( Sum (z1 ExpSeq )) * ( Sum (z2 ExpSeq ))) by Lm2

 .= (( exp z1) * ( Sum (z2 ExpSeq ))) by Def14

 .= (( exp z1) * ( exp z2)) by Def14;

 hence thesis;

 end;

 begin

 reserve d for Real;

 definition

 :: SIN_COS:def16

 func sin -> Function of REAL , REAL means

 : Def16: for d holds (it . d) = ( Im ( Sum ((d * ) ExpSeq )));

 existence

 proof

 deffunc U( Real) = ( Im ( Sum (($1 * ) ExpSeq )));

 consider f be Function of REAL , REAL such that

 A1: for x be Element of REAL holds (f . x) = U(x) from FUNCT_2:sch 4;

 take f;

 let x be Real;

 reconsider x as Element of REAL by XREAL_0:def 1;

 (f . x) = U(x) by A1;

 hence thesis;

 end;

 uniqueness

 proof

 let f1,f2 be Function of REAL , REAL ;

 assume

 A2: for d holds (f1 . d) = ( Im ( Sum ((d * ) ExpSeq )));

 assume

 A3: for d holds (f2 . d) = ( Im ( Sum ((d * ) ExpSeq )));

 for d be 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;

 end;

 end

 definition

 let th be Real;

 :: SIN_COS:def17

 func sin th -> number equals ( sin . th);

 coherence ;

 end

 registration

 let th be Real;

 cluster ( sin th) -> real;

 coherence ;

 end

 definition

 :: SIN_COS:def18

 func cos -> Function of REAL , REAL means

 : Def18: for d holds (it . d) = ( Re ( Sum ((d * ) ExpSeq )));

 existence

 proof

 deffunc U( Real) = ( Re ( Sum (($1 * ) ExpSeq )));

 consider f be Function of REAL , REAL such that

 A1: for x be Element of REAL holds (f . x) = U(x) from FUNCT_2:sch 4;

 take f;

 let d;

 reconsider d as Element of REAL by XREAL_0:def 1;

 (f . d) = U(d) by A1;

 hence thesis;

 end;

 uniqueness

 proof

 let f1,f2 be Function of REAL , REAL ;

 assume

 A2: for d holds (f1 . d) = ( Re ( Sum ((d * ) ExpSeq )));

 assume

 A3: for d holds (f2 . d) = ( Re ( Sum ((d * ) ExpSeq )));

 for d be Element of REAL holds (f1 . d) = (f2 . d)

 proof

 let d be Element of REAL ;



 thus (f1 . d) = ( Re ( Sum ((d * ) ExpSeq ))) by A2

 .= (f2 . d) by A3;

 end;

 hence f1 = f2;

 end;

 end

 definition

 let th be Real;

 :: SIN_COS:def19

 func cos th -> number equals ( cos . th);

 coherence ;

 end

 registration

 let th be Real;

 cluster ( cos th) -> real;

 coherence ;

 end

 theorem :: SIN_COS:24



 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 :: SIN_COS:25

 ( 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[ 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 2( A2, A3);

 end;

 defpred X[ 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 be Nat st X[n] holds X[(n + 1)]

 proof

 let n be Nat such that

 A7: ((( Partial_Sums ((th * ) ExpSeq )) *' ) . n) = (( Partial_Sums (( - (th * )) ExpSeq )) . n);



 A8: n in NAT by ORDINAL1:def 12;



 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, A8

 .= ((( 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 be Nat holds X[n] from NAT_1:sch 2( A5, A6);

 hence thesis;

 end;

 hence thesis by COMSEQ_2: 12;

 end;

 theorem :: SIN_COS:26

 (( 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 be Real st th = th1 holds |.( Sum ((th * ) ExpSeq )).| = 1 & |.( sin . th1).| <= 1 & |.( cos . th1).| <= 1

 proof

 let th1 be Real 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;

 hence

 A4: |.( Sum ((th * ) ExpSeq )).| = 1 by A3, XCMPLX_1: 199;

 |.( sin . th).| = |.( Im ( Sum ((th * ) ExpSeq ))).| & |.( cos . th).| = |.( Re ( Sum ((th * ) ExpSeq ))).| by Def16, Def18;

 hence thesis by A1, A4, COMSEQ_3: 13;

 end;

 theorem :: SIN_COS:27

 |.( exp (th * )).| = 1 & for th be Real holds |.( sin th).| <= 1 & |.( cos th).| <= 1

 proof



 thus |.( exp (th * )).| = |.( Sum ((th * ) ExpSeq )).| by Def14

 .= 1 by Lm5;

 let th be Real;

 thus |.( sin th).| <= 1 by Lm5;

 thus thesis by Lm5;

 end;

 reserve th,th1,th2 for Real;

 theorem :: SIN_COS:28



 Th28: ((( cos . th) ^2 ) + (( sin . th) ^2 )) = 1 & ((( cos . th) * ( cos . th)) + (( sin . th) * ( sin . th))) = 1

 proof

 reconsider th1 = th as Real;



 A1: (( Sum ((th1 * ) 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 :: SIN_COS:29

 ((( cos th) ^2 ) + (( sin th) ^2 )) = 1 & ((( cos th) * ( cos th)) + (( sin th) * ( sin th))) = 1 by Th28;

 theorem :: SIN_COS:30



 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;



 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 :: SIN_COS:31

 ( cos 0 ) = 1 & ( sin 0 ) = 0 & ( cos ( - th)) = ( cos th) & ( sin ( - th)) = ( - ( sin th)) by Th30;

 definition

 let th be Real;

 deffunc U( Nat) = (((( - 1) |^ $1) * (th |^ ((2 * $1) + 1))) / (((2 * $1) + 1) ! ));

 :: SIN_COS:def20

 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 be Real_Sequence st for n holds (s . n) = U(n) from SEQ_1:sch 1;

 end;

 uniqueness

 proof

 let s1,s2 be Real_Sequence such that

 A1: for x be Nat holds (s1 . x) = U(x) and

 A2: for x be Nat holds (s2 . x) = U(x);

 let x be Element of NAT ;



 thus (s1 . x) = U(x) by A1

 .= (s2 . x) by A2;

 end;

 deffunc U( Nat) = (((( - 1) |^ $1) * (th |^ (2 * $1))) / ((2 * $1) ! ));

 :: SIN_COS:def21

 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 be Real_Sequence st for n holds (s . n) = U(n) from SEQ_1:sch 1;

 end;

 uniqueness

 proof

 let s1,s2 be Real_Sequence such that

 A3: for x be Nat holds (s1 . x) = U(x) and

 A4: for x be Nat holds (s2 . x) = U(x);

 let x be Element of NAT ;



 thus (s1 . x) = U(x) by A3

 .= (s2 . x) by A4;

 end;

 end

 theorem :: SIN_COS:32



 Th32: for z be Complex, k holds (z |^ (2 * k)) = ((z |^ k) |^ 2) & (z |^ (2 * k)) = ((z |^ 2) |^ k)

 proof

 let z be Complex, k;

 defpred X[ Nat] means (z |^ (2 * $1)) = ((z |^ $1) |^ 2) & (z |^ (2 * $1)) = ((z |^ 2) |^ $1);



 A1: (z |^ (2 * 0 )) = (1 * 1) by NEWTON: 4

 .= ((1 |^ 1) * 1)

 .= (1 |^ (1 + 1))

 .= ((z |^ 0 ) |^ 2) by NEWTON: 4;

 (z |^ (2 * 0 )) = 1 by NEWTON: 4

 .= ((z |^ 2) |^ 0 ) by NEWTON: 4;

 then

 A2: X[ 0 ] by A1;



 A3: for k st X[k] holds X[(k + 1)]

 proof

 let k;

 assume that

 A4: (z |^ (2 * k)) = ((z |^ k) |^ 2) and

 A5: (z |^ (2 * k)) = ((z |^ 2) |^ k);



 A6: (z |^ (2 * (k + 1))) = ((z GeoSeq ) . (((2 * k) + 1) + 1))

 .= (((z GeoSeq ) . ((2 * k) + 1)) * z) by COMSEQ_3:def 1

 .= (((z |^ (2 * k)) * z) * z) by COMSEQ_3:def 1;



 then

 A7: (z |^ (2 * (k + 1))) = (((((z |^ k) GeoSeq ) . (1 + 1)) * z) * z) by A4

 .= ((((((z |^ k) GeoSeq ) . ( 0 + 1)) * (z |^ k)) * z) * z) by COMSEQ_3:def 1

 .= (((((((z |^ k) GeoSeq ) . 0 ) * (z |^ k)) * (z |^ k)) * z) * z) by COMSEQ_3:def 1

 .= (((( 1r * (z |^ k)) * (z |^ k)) * z) * z) by COMSEQ_3:def 1

 .= (( 1r * (((z GeoSeq ) . k) * z)) * ((z |^ k) * z))

 .= (( 1r * ((z GeoSeq ) . (k + 1))) * (((z GeoSeq ) . k) * z)) by COMSEQ_3:def 1

 .= (( 1r * (z |^ (k + 1))) * ((z GeoSeq ) . (k + 1))) by COMSEQ_3:def 1

 .= (((((z |^ (k + 1)) GeoSeq ) . 0 ) * (z |^ (k + 1))) * (z |^ (k + 1))) by COMSEQ_3:def 1

 .= ((((z |^ (k + 1)) GeoSeq ) . ( 0 + 1)) * (z |^ (k + 1))) by COMSEQ_3:def 1

 .= (((z |^ (k + 1)) GeoSeq ) . (( 0 + 1) + 1)) by COMSEQ_3:def 1

 .= ((z |^ (k + 1)) |^ 2);

 (z |^ (2 * (k + 1))) = (((z |^ 2) |^ k) * (( 1r * z) * z)) by A5, A6

 .= (((z |^ 2) |^ k) * ((((z GeoSeq ) . 0 ) * z) * z)) by COMSEQ_3:def 1

 .= (((z |^ 2) |^ k) * (((z GeoSeq ) . ( 0 + 1)) * z)) by COMSEQ_3:def 1

 .= (((z |^ 2) |^ k) * ((z GeoSeq ) . (( 0 + 1) + 1))) by COMSEQ_3:def 1

 .= ((z |^ 2) |^ (k + 1)) by COMSEQ_3:def 1;

 hence thesis by A7;

 end;

 for k holds X[k] from NAT_1:sch 2( A2, A3);

 hence thesis;

 end;

 theorem :: SIN_COS:33



 Th33: for th holds ((th * ) |^ (2 * k)) = ((( - 1) |^ k) * (th |^ (2 * k))) & ((th * ) |^ ((2 * k) + 1)) = (((( - 1) |^ k) * (th |^ ((2 * k) + 1))) * )

 proof

 let th;



 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;

 defpred X[ 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

 A2: X[ 0 ] by A1, COMSEQ_3:def 1;



 A3: for k st X[k] holds X[(k + 1)]

 proof

 let k;

 assume that

 A4: ((th * ) |^ (2 * k)) = ((( - 1) |^ k) * (th |^ (2 * k))) and

 A5: ((th * ) |^ ((2 * k) + 1)) = (((( - 1) |^ k) * (th |^ ((2 * k) + 1))) * );



 A6: ((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 A4, 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 A5

 .= (((((((( - 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 A6;

 end;

 for k holds X[k] from NAT_1:sch 2( A2, A3);

 hence thesis;

 end;

 ::$Canceled

 theorem :: SIN_COS:35



 Th34: for th 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;

 now



 A1: (( Partial_Sums (th P_sin )) . 0 ) = ((th P_sin ) . 0 ) by SERIES_1:def 1

 .= (((( - 1) |^ 0 ) * (th |^ ((2 * 0 ) + 1))) / (((2 * 0 ) + 1) ! )) by Def20;



 A2: (((2 * 0 ) + 1) ! ) = (( 0 ! ) * 1) by NEWTON: 15

 .= 1 by NEWTON: 12;



 A3: (( - 1) |^ 0 ) = ((( - 1) GeoSeq ) . 0 ) by PREPOWER:def 1

 .= 1 by PREPOWER: 3;



 A4: (( Partial_Sums (th P_cos )) . 0 ) = ((th P_cos ) . 0 ) by SERIES_1:def 1

 .= (((( - 1) |^ 0 ) * (th |^ (2 * 0 ))) / ((2 * 0 ) ! )) by Def21

 .= ((1 * ((th GeoSeq ) . 0 )) / 1) by A3, NEWTON: 12, PREPOWER:def 1

 .= 1 by PREPOWER: 3;



 A5: (( Im ((th * ) ExpSeq )) . 0 ) = ( Im (((th * ) ExpSeq ) . 0 )) & (( Im ((th * ) ExpSeq )) . 1) = ( Im (((th * ) ExpSeq ) . 1)) by COMSEQ_3:def 6;



 A6: (th * ) = ( 0 + (th * ));



 A7: (( 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 A5, Th3, COMPLEX1: 6

 .= ( 0 + ( Im (((((th * ) ExpSeq ) . 0 ) * (th * )) / (( 0 + 1) + ( 0 * ))))) by Th3

 .= ( Im ((1 * (th * )) / 1)) by Th3

 .= th by A6, COMPLEX1: 12;

 defpred X[ 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

 A8: X[ 0 ] by A1, A2, A3, A4, A7;



 A9: for k st X[k] holds X[(k + 1)]

 proof

 let k be Nat;

 assume that

 A10: (( Partial_Sums (th P_sin )) . k) = (( Partial_Sums ( Im ((th * ) ExpSeq ))) . ((2 * k) + 1)) and

 A11: (( 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 A10, 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

 A12: (( 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 A11, 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 A12;

 end;

 thus for n holds X[n] from NAT_1:sch 2( A8, A9);

 end;

 hence thesis;

 end;

 theorem :: SIN_COS:36



 Th35: for th 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;



 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, SERIES_1: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, SERIES_1:def 3;

 A6:

 now

 let p be Real;

 assume p > 0 ;

 then

 consider n such that

 A7: for k st n <= k holds |.((( Partial_Sums ( Re ((th * ) ExpSeq ))) . k) - ( Re ( Sum ((th * ) ExpSeq )))).| ) ExpSeq )))).| = |.((( Partial_Sums ( Re ((th * ) ExpSeq ))) . (2 * k)) - ( Re ( Sum ((th * ) ExpSeq )))).| & (2 * k) = (k + k) by Th34;

 hence |.((( Partial_Sums (th P_cos )) . k) - ( Re ( Sum ((th * ) ExpSeq )))).| ) 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;

 assume p > 0 ;

 then

 consider n such that

 A11: for k st n <= k holds |.((( Partial_Sums ( Im ((th * ) ExpSeq ))) . k) - ( Im ( Sum ((th * ) ExpSeq )))).| ) ExpSeq )))).| = |.((( Partial_Sums ( Im ((th * ) ExpSeq ))) . ((2 * k) + 1)) - ( Im ( Sum ((th * ) ExpSeq )))).| by Th34;

 (2 * k) = (k + k);

 then n <= (2 * k) by A12, NAT_1: 12;

 then n < ((2 * k) + 1) by NAT_1: 13;

 hence |.((( Partial_Sums (th P_sin )) . k) - ( Im ( Sum ((th * ) ExpSeq )))).| ) 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 :: SIN_COS:37



 Th36: ( cos . th) = ( Sum (th P_cos )) & ( sin . th) = ( Sum (th P_sin ))

 proof

 reconsider th as Real;

 ( sin . th) = ( Im ( Sum ((th * ) ExpSeq ))) & ( cos . th) = ( Re ( Sum ((th * ) ExpSeq ))) by Def16, Def18;

 hence thesis by Th35;

 end;

 theorem :: SIN_COS:38

 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 be Real_Sequence such that

 Lm6: for n holds (bq . n) = U(n) from SEQ_1:sch 1;

 bq is increasing sequence of NAT

 proof



 A1: for n, k st n < k holds (bq . n) < (bq . k)

 proof

 let n, k;

 assume n < k;

 then (2 * n) < (2 * k) by XREAL_1: 68;

 then ((2 * n) + 1) < ((2 * k) + 1) by XREAL_1: 6;

 then (bq . n) < ((2 * k) + 1) by Lm6;

 hence thesis by Lm6;

 end;

 for n holds (bq . n) is Element of NAT

 proof

 let n;

 ((2 * n) + 1) is Element of NAT ;

 hence thesis by Lm6;

 end;

 hence thesis by A1, SEQM_3: 1, SEQM_3: 13;

 end;

 then

 reconsider bq as increasing sequence of NAT ;



 Lm7: for th,th1,th2,th3 be Real holds (th |^ (2 * n)) = ((th |^ n) |^ 2) & (( - 1) |^ (2 * n)) = 1 & (( - 1) |^ ((2 * n) + 1)) = ( - 1)

 proof

 let th,th1,th2,th3 be Real;

 reconsider 2n = (2 * n) as Element of NAT by ORDINAL1:def 12;

 thus (th |^ (2 * n)) = ((th |^ n) |^ 2) by NEWTON: 9;

 (( - 1) |^ 2n) = (1 |^ 2n) by POWER: 1

 .= 1;

 hence

 A1: (( - 1) |^ (2 * n)) = 1;



 thus (( - 1) |^ ((2 * n) + 1)) = ((( - 1) |^ (2 * n)) * ( - 1)) by NEWTON: 6

 .= ( - 1) by A1;

 end;

 theorem :: SIN_COS:39



 Th38: n <= k implies (n ! ) <= (k ! )

 proof

 assume

 A1: n <= k;



 A2: for m holds 1 <= (m + 1)

 proof

 let m;

 ( 0 + 1) <= (m + 1) by XREAL_1: 6;

 hence thesis;

 end;

 deffunc U( Nat) = ($1 ! );

 consider rseq such that

 A3: for l holds (rseq . l) = U(l) from SEQ_1:sch 1;

 for l holds (rseq . l) <= (rseq . (l + 1)) & (rseq . l) > 0

 proof

 let l;

 defpred X[ Nat] means (rseq . $1) <= (rseq . ($1 + 1)) & (rseq . $1) > 0 ;

 (rseq . ( 0 + 1)) = (( 0 + 1) ! ) by A3

 .= (( 0 ! ) * 1) by NEWTON: 15

 .= 1 by NEWTON: 12;

 then

 A4: X[ 0 ] by A3, NEWTON: 12;



 A5: for l st X[l] holds X[(l + 1)]

 proof

 let l;

 assume

 A6: (rseq . l) <= (rseq . (l + 1)) & (rseq . l) > 0 ;

 (rseq . ((l + 1) + 1)) = (((l + 1) + 1) ! ) by A3

 .= (((l + 1) ! ) * ((l + 1) + 1)) by NEWTON: 15

 .= ((rseq . (l + 1)) * ((l + 1) + 1)) by A3;

 hence thesis by A2, A6, XREAL_1: 151;

 end;

 for l holds X[l] from NAT_1:sch 2( A4, A5);

 hence thesis;

 end;

 then

 A7: rseq is non-decreasing;

 (n ! ) = (rseq . n) & (k ! ) = (rseq . k) by A3;

 hence thesis by A1, A7, SEQM_3: 6;

 end;

 theorem :: SIN_COS:40



 Th39: 0 <= th & th <= 1 & n <= k implies (th |^ k) <= (th |^ n)

 proof

 assume that

 A1: 0 <= th and

 A2: th <= 1 and

 A3: n <= k;

 for m holds ((th GeoSeq ) . (m + 1)) <= ((th GeoSeq ) . m) & ((th GeoSeq ) . m) >= 0

 proof

 let m;

 defpred X[ Nat] means ((th GeoSeq ) . ($1 + 1)) <= ((th GeoSeq ) . $1) & ((th GeoSeq ) . $1) >= 0 ;

 ((th GeoSeq ) . ( 0 + 1)) = (((th GeoSeq ) . 0 ) * th) by PREPOWER: 3

 .= (1 * th) by PREPOWER: 3

 .= th;

 then

 A4: X[ 0 ] by A2, PREPOWER: 3;



 A5: for m st X[m] holds X[(m + 1)]

 proof

 let m;

 assume that ((th GeoSeq ) . (m + 1)) <= ((th GeoSeq ) . m) and

 A6: ((th GeoSeq ) . m) >= 0 ;

 ((th GeoSeq ) . ((m + 1) + 1)) = (((th GeoSeq ) . (m + 1)) * th) & ((th GeoSeq ) . (m + 1)) = (((th GeoSeq ) . m) * th) by PREPOWER: 3;

 hence thesis by A1, A2, A6, XREAL_1: 153;

 end;

 for m holds X[m] from NAT_1:sch 2( A4, A5);

 hence thesis;

 end;

 then

 A7: (th GeoSeq ) is non-increasing;

 (th |^ k) = ((th GeoSeq ) . k) & (th |^ n) = ((th GeoSeq ) . n) by PREPOWER:def 1;

 hence thesis by A3, A7, SEQM_3: 8;

 end;

 ::$Canceled

 theorem :: SIN_COS:42



 Th41: for p be Real holds ( Im ( Sum (p ExpSeq ))) = 0

 proof

 let p be Real;



 A1: for n holds (( Partial_Sums ( Im (p ExpSeq ))) . n) = 0

 proof

 let n;

 defpred X[ Nat] means (( Partial_Sums ( Im (p ExpSeq ))) . $1) = 0 ;

 (( Partial_Sums ( Im (p ExpSeq ))) . 0 ) = (( Im (p ExpSeq )) . 0 ) by SERIES_1:def 1

 .= ( Im ((p ExpSeq ) . 0 )) by COMSEQ_3:def 6

 .= 0 by Th3, COMPLEX1: 6;

 then

 A2: X[ 0 ];



 A3: for k st X[k] holds X[(k + 1)]

 proof

 let k;

 assume (( Partial_Sums ( Im (p ExpSeq ))) . k) = 0 ;



 then (( Partial_Sums ( Im (p ExpSeq ))) . (k + 1)) = ( 0 + (( Im (p ExpSeq )) . (k + 1))) by SERIES_1:def 1

 .= ( Im ((p ExpSeq ) . (k + 1))) by COMSEQ_3:def 6

 .= ( Im ((p |^ (k + 1)) / ((k + 1) ! ))) by Def4

 .= ( Im (((p |^ (k + 1)) / ((k + 1) ! )) + ( 0 * )))

 .= 0 by COMPLEX1: 12;

 hence thesis;

 end;

 for n holds X[n] from NAT_1:sch 2( A2, A3);

 hence thesis;

 end;

 for n,m be Nat holds (( Partial_Sums ( Im (p ExpSeq ))) . n) = (( Partial_Sums ( Im (p ExpSeq ))) . m)

 proof

 let n,m be Nat;

 m in NAT & (( Partial_Sums ( Im (p ExpSeq ))) . n) = 0 by A1, ORDINAL1:def 12;

 hence thesis by A1;

 end;



 then

 A4: ( lim ( Partial_Sums ( Im (p ExpSeq )))) = (( Partial_Sums ( Im (p ExpSeq ))) . 0 ) by SEQ_4: 26, VALUED_0: 24

 .= 0 by A1;

 ( Im ( Sum (p ExpSeq ))) = ( Im (( Sum ( Re (p ExpSeq ))) + (( Sum ( Im (p ExpSeq ))) * ))) by COMSEQ_3: 53

 .= ( Sum ( Im (p ExpSeq ))) by COMPLEX1: 12;

 hence thesis by A4, SERIES_1:def 3;

 end;

 theorem :: SIN_COS:43



 Th42: ( cos . 1) > 0 & ( sin . 1) > 0 & ( cos . 1) < ( sin . 1)

 proof



 A1: ( Partial_Sums (1 P_cos )) is convergent by Th35;



 A2: ( cos . 1) = ( Sum (1 P_cos )) by Th36;

 ( lim (( Partial_Sums (1 P_cos )) * bq)) = ( lim ( Partial_Sums (1 P_cos ))) by A1, SEQ_4: 17;

 then

 A3: ( lim (( Partial_Sums (1 P_cos )) * bq)) = ( cos . 1) by A2, SERIES_1:def 3;

 for n holds ((( Partial_Sums (1 P_cos )) * bq) . n) >= (1 / 2)

 proof

 let n;

 defpred X[ Nat] means ((( Partial_Sums (1 P_cos )) * bq) . $1) >= (1 / 2);

 ((( Partial_Sums (1 P_cos )) * bq) . 0 ) = (( Partial_Sums (1 P_cos )) . (bq . 0 )) by FUNCT_2: 15

 .= (( Partial_Sums (1 P_cos )) . ((2 * 0 ) + 1)) by Lm6

 .= ((( Partial_Sums (1 P_cos )) . 0 ) + ((1 P_cos ) . ( 0 + 1))) by SERIES_1:def 1

 .= (((1 P_cos ) . 0 ) + ((1 P_cos ) . ( 0 + 1))) by SERIES_1:def 1

 .= ((((( - 1) |^ 0 ) * (1 |^ (2 * 0 ))) / ((2 * 0 ) ! )) + ((1 P_cos ) . 1)) by Def21

 .= ((((( - 1) |^ 0 ) * (1 |^ (2 * 0 ))) / ((2 * 0 ) ! )) + (((( - 1) |^ 1) * (1 |^ (2 * 1))) / ((2 * 1) ! ))) by Def21

 .= (((1 * (1 |^ (2 * 0 ))) / ((2 * 0 ) ! )) + (((( - 1) |^ 1) * (1 |^ (2 * 1))) / ((2 * 1) ! ))) by Lm7

 .= ((1 / 1) + (((( - 1) |^ 1) * (1 |^ (2 * 1))) / ((2 * 1) ! ))) by NEWTON: 12

 .= (1 + ((( - 1) * (1 |^ (2 * 1))) / ((2 * 1) ! )))

 .= (1 + ((( - 1) * 1) / ((2 * 1) ! )))

 .= (1 + (( - 1) / ((1 ! ) * (1 + 1)))) by NEWTON: 15

 .= (1 + (( - 1) / ((( 0 ! ) * ( 0 + 1)) * 2))) by NEWTON: 15

 .= (1 / 2) by NEWTON: 12;

 then

 A4: X[ 0 ];



 A5: for k st X[k] holds X[(k + 1)]

 proof

 let k;



 A6: k in NAT by ORDINAL1:def 12;

 assume

 A7: ((( Partial_Sums (1 P_cos )) * bq) . k) >= (1 / 2);

 ((( Partial_Sums (1 P_cos )) * bq) . (k + 1)) = (( Partial_Sums (1 P_cos )) . (bq . (k + 1))) by FUNCT_2: 15

 .= (( Partial_Sums (1 P_cos )) . ((2 * (k + 1)) + 1)) by Lm6

 .= ((( Partial_Sums (1 P_cos )) . (((2 * k) + 1) + 1)) + ((1 P_cos ) . ((2 * (k + 1)) + 1))) by SERIES_1:def 1

 .= (((( Partial_Sums (1 P_cos )) . ((2 * k) + 1)) + ((1 P_cos ) . (((2 * k) + 1) + 1))) + ((1 P_cos ) . ((2 * (k + 1)) + 1))) by SERIES_1:def 1

 .= (((( Partial_Sums (1 P_cos )) . (bq . k)) + ((1 P_cos ) . (((2 * k) + 1) + 1))) + ((1 P_cos ) . ((2 * (k + 1)) + 1))) by Lm6

 .= ((((( Partial_Sums (1 P_cos )) * bq) . k) + ((1 P_cos ) . (((2 * k) + 1) + 1))) + ((1 P_cos ) . ((2 * (k + 1)) + 1))) by FUNCT_2: 15, A6;

 then

 A8: (((( Partial_Sums (1 P_cos )) * bq) . (k + 1)) - ((( Partial_Sums (1 P_cos )) * bq) . k)) = (((1 P_cos ) . (((2 * k) + 1) + 1)) + ((1 P_cos ) . ((2 * (k + 1)) + 1)));



 A9: ((1 P_cos ) . (((2 * k) + 1) + 1)) = (((( - 1) |^ (2 * (k + 1))) * (1 |^ (2 * (2 * (k + 1))))) / ((2 * (2 * (k + 1))) ! )) by Def21

 .= ((1 * (1 |^ (2 * (2 * (k + 1))))) / ((2 * (2 * (k + 1))) ! )) by Lm7

 .= (1 / ((2 * (2 * (k + 1))) ! ));



 A10: ((1 P_cos ) . ((2 * (k + 1)) + 1)) = (((( - 1) |^ ((2 * (k + 1)) + 1)) * (1 |^ (2 * ((2 * (k + 1)) + 1)))) / ((2 * ((2 * (k + 1)) + 1)) ! )) by Def21

 .= ((( - 1) * (1 |^ (2 * ((2 * (k + 1)) + 1)))) / ((2 * ((2 * (k + 1)) + 1)) ! )) by Lm7

 .= ((( - 1) * 1) / ((2 * ((2 * (k + 1)) + 1)) ! ))

 .= (( - 1) / ((2 * ((2 * (k + 1)) + 1)) ! ));

 (2 * (2 * (k + 1))) < (2 * ((2 * (k + 1)) + 1)) by XREAL_1: 29, XREAL_1: 68;

 then ((2 * (2 * (k + 1))) ! ) <= ((2 * ((2 * (k + 1)) + 1)) ! ) by Th38;

 then (1 / ((2 * (2 * (k + 1))) ! )) >= (1 / ((2 * ((2 * (k + 1)) + 1)) ! )) by XREAL_1: 85;

 then ((1 / ((2 * (2 * (k + 1))) ! )) - (1 / ((2 * ((2 * (k + 1)) + 1)) ! ))) >= 0 by XREAL_1: 48;

 then ((( Partial_Sums (1 P_cos )) * bq) . (k + 1)) >= ((( Partial_Sums (1 P_cos )) * bq) . k) by A8, A9, A10, XREAL_1: 49;

 hence thesis by A7, XXREAL_0: 2;

 end;

 for n holds X[n] from NAT_1:sch 2( A4, A5);

 hence thesis;

 end;

 then

 A11: ( cos . 1) >= (1 / 2) by A1, A3, PREPOWER: 1, SEQ_4: 16;



 A12: ( Partial_Sums (1 P_sin )) is convergent by Th35;



 A13: ( sin . 1) = ( Sum (1 P_sin )) by Th36;

 ( lim (( Partial_Sums (1 P_sin )) * bq)) = ( lim ( Partial_Sums (1 P_sin ))) by A12, SEQ_4: 17;

 then

 A14: ( lim (( Partial_Sums (1 P_sin )) * bq)) = ( sin . 1) by A13, SERIES_1:def 3;

 for n holds ((( Partial_Sums (1 P_sin )) * bq) . n) >= (5 / 6)

 proof

 let n;

 defpred X[ Nat] means ((( Partial_Sums (1 P_sin )) * bq) . $1) >= (5 / 6);

 ((( Partial_Sums (1 P_sin )) * bq) . 0 ) = (( Partial_Sums (1 P_sin )) . (bq . 0 )) by FUNCT_2: 15

 .= (( Partial_Sums (1 P_sin )) . ((2 * 0 ) + 1)) by Lm6

 .= ((( Partial_Sums (1 P_sin )) . 0 ) + ((1 P_sin ) . ( 0 + 1))) by SERIES_1:def 1

 .= (((1 P_sin ) . 0 ) + ((1 P_sin ) . ( 0 + 1))) by SERIES_1:def 1

 .= ((((( - 1) |^ 0 ) * (1 |^ ((2 * 0 ) + 1))) / (((2 * 0 ) + 1) ! )) + ((1 P_sin ) . 1)) by Def20

 .= ((((( - 1) |^ 0 ) * (1 |^ ((2 * 0 ) + 1))) / (((2 * 0 ) + 1) ! )) + (((( - 1) |^ 1) * (1 |^ ((2 * 1) + 1))) / (((2 * 1) + 1) ! ))) by Def20

 .= (((1 * (1 |^ ((2 * 0 ) + 1))) / (((2 * 0 ) + 1) ! )) + (((( - 1) |^ 1) * (1 |^ ((2 * 1) + 1))) / (((2 * 1) + 1) ! ))) by Lm7

 .= ((1 / (( 0 + 1) ! )) + (((( - 1) |^ 1) * (1 |^ ((2 * 1) + 1))) / (((2 * 1) + 1) ! )))

 .= ((1 / (( 0 ! ) * 1)) + (((( - 1) |^ 1) * (1 |^ ((2 * 1) + 1))) / (((2 * 1) + 1) ! ))) by NEWTON: 15

 .= (1 + ((( - 1) * (1 |^ ((2 * 1) + 1))) / (((2 * 1) + 1) ! ))) by NEWTON: 12

 .= (1 + ((( - 1) * 1) / (((2 * 1) + 1) ! )))

 .= (1 + (( - 1) / (((2 * 1) ! ) * ((2 * 1) + 1)))) by NEWTON: 15

 .= (1 + (( - 1) / (((1 ! ) * (1 + 1)) * 3))) by NEWTON: 15

 .= (1 + (( - 1) / ((( 0 + 1) ! ) * (2 * 3))))

 .= (1 + (( - 1) / ((1 * 1) * 6))) by NEWTON: 12, NEWTON: 15

 .= (5 / 6);

 then

 A15: X[ 0 ];



 A16: for k st X[k] holds X[(k + 1)]

 proof

 let k;



 A17: k in NAT by ORDINAL1:def 12;

 assume

 A18: ((( Partial_Sums (1 P_sin )) * bq) . k) >= (5 / 6);

 ((( Partial_Sums (1 P_sin )) * bq) . (k + 1)) = (( Partial_Sums (1 P_sin )) . (bq . (k + 1))) by FUNCT_2: 15

 .= (( Partial_Sums (1 P_sin )) . ((2 * (k + 1)) + 1)) by Lm6

 .= ((( Partial_Sums (1 P_sin )) . (((2 * k) + 1) + 1)) + ((1 P_sin ) . ((2 * (k + 1)) + 1))) by SERIES_1:def 1

 .= (((( Partial_Sums (1 P_sin )) . ((2 * k) + 1)) + ((1 P_sin ) . (((2 * k) + 1) + 1))) + ((1 P_sin ) . ((2 * (k + 1)) + 1))) by SERIES_1:def 1

 .= (((( Partial_Sums (1 P_sin )) . (bq . k)) + ((1 P_sin ) . (((2 * k) + 1) + 1))) + ((1 P_sin ) . ((2 * (k + 1)) + 1))) by Lm6

 .= ((((( Partial_Sums (1 P_sin )) * bq) . k) + ((1 P_sin ) . (((2 * k) + 1) + 1))) + ((1 P_sin ) . ((2 * (k + 1)) + 1))) by FUNCT_2: 15, A17;

 then

 A19: (((( Partial_Sums (1 P_sin )) * bq) . (k + 1)) - ((( Partial_Sums (1 P_sin )) * bq) . k)) = (((1 P_sin ) . (((2 * k) + 1) + 1)) + ((1 P_sin ) . ((2 * (k + 1)) + 1)));



 A20: ((1 P_sin ) . (((2 * k) + 1) + 1)) = (((( - 1) |^ (2 * (k + 1))) * (1 |^ ((2 * (2 * (k + 1))) + 1))) / (((2 * (2 * (k + 1))) + 1) ! )) by Def20

 .= ((1 * (1 |^ ((2 * (2 * (k + 1))) + 1))) / (((2 * (2 * (k + 1))) + 1) ! )) by Lm7

 .= (1 / (((2 * (2 * (k + 1))) + 1) ! ));



 A21: ((1 P_sin ) . ((2 * (k + 1)) + 1)) = (((( - 1) |^ ((2 * (k + 1)) + 1)) * (1 |^ ((2 * ((2 * (k + 1)) + 1)) + 1))) / (((2 * ((2 * (k + 1)) + 1)) + 1) ! )) by Def20

 .= ((( - 1) * (1 |^ ((2 * ((2 * (k + 1)) + 1)) + 1))) / (((2 * ((2 * (k + 1)) + 1)) + 1) ! )) by Lm7

 .= ((( - 1) * 1) / (((2 * ((2 * (k + 1)) + 1)) + 1) ! ))

 .= (( - 1) / (((2 * ((2 * (k + 1)) + 1)) + 1) ! ));

 (2 * (2 * (k + 1))) < (2 * ((2 * (k + 1)) + 1)) by XREAL_1: 29, XREAL_1: 68;

 then ((2 * (2 * (k + 1))) + 1) < ((2 * ((2 * (k + 1)) + 1)) + 1) by XREAL_1: 6;

 then (((2 * (2 * (k + 1))) + 1) ! ) <= (((2 * ((2 * (k + 1)) + 1)) + 1) ! ) by Th38;

 then (1 / (((2 * (2 * (k + 1))) + 1) ! )) >= (1 / (((2 * ((2 * (k + 1)) + 1)) + 1) ! )) by XREAL_1: 85;

 then ((1 / (((2 * (2 * (k + 1))) + 1) ! )) - (1 / (((2 * ((2 * (k + 1)) + 1)) + 1) ! ))) >= 0 by XREAL_1: 48;

 then ((( Partial_Sums (1 P_sin )) * bq) . (k + 1)) >= ((( Partial_Sums (1 P_sin )) * bq) . k) by A19, A20, A21, XREAL_1: 49;

 hence thesis by A18, XXREAL_0: 2;

 end;

 for n holds X[n] from NAT_1:sch 2( A15, A16);

 hence thesis;

 end;

 then

 A22: ( sin . 1) >= (5 / 6) by A12, A14, PREPOWER: 1, SEQ_4: 16;



 A23: ((( cos . 1) ^2 ) + (( sin . 1) ^2 )) = 1 by Th28;



 A24: (( sin . 1) ^2 ) >= ((5 / 6) ^2 ) by A22, SQUARE_1: 15;

 then (1 - (1 - (( cos . 1) ^2 ))) <= (1 - (25 / 36)) by A23, XREAL_1: 10;

 then (( cos . 1) ^2 ) < (25 / 36) by XXREAL_0: 2;

 then (( sin . 1) ^2 ) > (( cos . 1) ^2 ) by A24, XXREAL_0: 2;

 then

 A25: ( sqrt (( cos . 1) ^2 )) < ( sqrt (( sin . 1) ^2 )) by SQUARE_1: 27, XREAL_1: 63;

 ( sqrt (( cos . 1) ^2 )) = ( cos . 1) by A11, SQUARE_1: 22;

 hence thesis by A11, A22, A25, SQUARE_1: 22;

 end;

 theorem :: SIN_COS:44



 Th43: for th holds (th rExpSeq ) = ( Re (th ExpSeq ))

 proof

 let th;

 for n be Element of NAT holds ((th rExpSeq ) . n) = (( Re (th ExpSeq )) . n)

 proof

 let n be Element of NAT ;

 (( Re (th ExpSeq )) . n) = ( Re ((th ExpSeq ) . n)) by COMSEQ_3:def 5

 .= ( Re ((th |^ n) / ((n ! ) + ( 0 * )))) by Def4

 .= ( Re (((th |^ n) / (n ! )) + ( 0 * )))

 .= ((th |^ n) / (n ! )) by COMPLEX1: 12

 .= ((th rExpSeq ) . n) by Def5;

 hence thesis;

 end;

 hence thesis;

 end;

 theorem :: SIN_COS:45



 Th44: for th holds (th rExpSeq ) is summable & ( Sum (th rExpSeq )) = ( Re ( Sum (th ExpSeq )))

 proof

 let th;

 ( Sum (th ExpSeq )) = (( Sum ( Re (th ExpSeq ))) + (( Sum ( Im (th ExpSeq ))) * )) & ( Sum (th rExpSeq )) = ( Sum ( Re (th ExpSeq ))) by Th43, COMSEQ_3: 53;

 hence thesis by Th43, COMPLEX1: 12;

 end;



 Lm8: for z be Complex holds ((z ExpSeq ) . 1) = z & ((z ExpSeq ) . 0 ) = 1r & |.(z |^ n).| = ( |.z.| |^ n)

 proof

 let z be Complex;

 (z |^ 1) = z;



 then

 A1: ((z ExpSeq ) . 1) = (z / (1 ! )) by Def4

 .= z by NEWTON: 13;



 A2: ((z ExpSeq ) . 0 ) = ((z |^ 0 ) / ( 0 ! )) by Def4

 .= 1r by Th1, COMSEQ_3: 11;

 |.(z |^ n).| = ( |.z.| |^ n)

 proof

 defpred X[ Nat] means |.(z |^ $1).| = ( |.z.| |^ $1);

 |.(z |^ 0 ).| = 1 by COMPLEX1: 48, COMSEQ_3:def 1;

 then

 A3: X[ 0 ] by NEWTON: 4;



 A4: for k st X[k] holds X[(k + 1)]

 proof

 let k such that

 A5: |.(z |^ k).| = ( |.z.| |^ k);

 |.(z |^ (k + 1)).| = |.(z * ((z GeoSeq ) . k)).| by COMSEQ_3:def 1

 .= (( |.z.| |^ k) * |.z.|) by A5, COMPLEX1: 65

 .= ( |.z.| |^ (k + 1)) by NEWTON: 6;

 hence thesis;

 end;

 for n holds X[n] from NAT_1:sch 2( A3, A4);

 hence thesis;

 end;

 hence thesis by A1, A2;

 end;



 Lm9: for th holds ( Sum (th ExpSeq )) = ( Sum (th rExpSeq ))

 proof

 let th;



 A1: for n be Nat holds (( Im ( Partial_Sums (th ExpSeq ))) . n) = ( In ( 0 , REAL ))

 proof

 defpred X[ Nat] means (( Im ( Partial_Sums (th ExpSeq ))) . $1) = 0 ;

 (( Im ( Partial_Sums (th ExpSeq ))) . 0 ) = ( Im (( Partial_Sums (th ExpSeq )) . 0 )) by COMSEQ_3:def 6

 .= ( Im ((th ExpSeq ) . 0 )) by SERIES_1:def 1

 .= 0 by Lm8, COMPLEX1: 6;

 then

 A2: X[ 0 ];



 A3: for n be Nat st X[n] holds X[(n + 1)]

 proof

 let n be Nat such that

 A4: (( Im ( Partial_Sums (th ExpSeq ))) . n) = 0 ;

 (( Im ( Partial_Sums (th ExpSeq ))) . (n + 1)) = ( Im (( Partial_Sums (th ExpSeq )) . (n + 1))) by COMSEQ_3:def 6

 .= ( Im ((( Partial_Sums (th ExpSeq )) . n) + ((th ExpSeq ) . (n + 1)))) by SERIES_1:def 1

 .= (( Im (( Partial_Sums (th ExpSeq )) . n)) + ( Im ((th ExpSeq ) . (n + 1)))) by COMPLEX1: 8

 .= ( 0 + ( Im ((th ExpSeq ) . (n + 1)))) by A4, COMSEQ_3:def 6

 .= ( Im (((th |^ (n + 1)) / ((n + 1) ! )) + ( 0 * ))) by Def4

 .= 0 by COMPLEX1: 12;

 hence thesis;

 end;

 for n be 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 Th44;

 hence thesis;

 end;

 theorem :: SIN_COS:46



 Th45: for p,q be Real holds ( Sum ((p + q) rExpSeq )) = (( Sum (p rExpSeq )) * ( Sum (q rExpSeq )))

 proof

 let p,q be Real;

 reconsider p, q as Real;

 ( Sum ((p + q) rExpSeq )) = ( Re ( Sum ((p + q) ExpSeq ))) by Th44

 .= ( Re (( Sum (p ExpSeq )) * ( Sum (q ExpSeq )))) by Lm2

 .= ( Re ((( Re ( Sum (p ExpSeq ))) + (( Im ( Sum (p ExpSeq ))) * )) * ( 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 Th44

 .= ( Re ((( Sum (p rExpSeq )) + ( 0 * )) * (( Re ( Sum (q ExpSeq ))) + (( Im ( Sum (q ExpSeq ))) * )))) by Th41

 .= ( Re (( Sum (p rExpSeq )) * (( Sum (q rExpSeq )) + (( Im ( Sum (q ExpSeq ))) * )))) by Th44

 .= ( Re (( Sum (p rExpSeq )) * (( Sum (q rExpSeq )) + ( 0 * )))) by Th41

 .= ( Re ((( Sum (p rExpSeq )) * ( Sum (q rExpSeq ))) + ( 0 * )))

 .= (( Sum (p rExpSeq )) * ( Sum (q rExpSeq ))) by COMPLEX1: 12;

 hence thesis;

 end;

 definition

 :: SIN_COS:def22

 func exp_R -> Function of REAL , REAL means

 : Def22: for d be Real holds (it . d) = ( Sum (d rExpSeq ));

 existence

 proof

 deffunc U( Real) = ( In (( Sum ($1 rExpSeq )), REAL ));

 consider f be Function of REAL , REAL such that

 A1: for d be Element of REAL holds (f . d) = U(d) from FUNCT_2:sch 4;

 take f;

 let d be Real;

 d in REAL by XREAL_0:def 1;

 then (f . d) = U(d) by A1;

 hence thesis;

 end;

 uniqueness

 proof

 let f1,f2 be Function of REAL , REAL ;

 assume

 A2: for d be Real holds (f1 . d) = ( Sum (d rExpSeq ));

 assume

 A3: for d be Real holds (f2 . d) = ( Sum (d rExpSeq ));

 for d be Element of REAL holds (f1 . d) = (f2 . d)

 proof

 let d be Element of REAL ;



 thus (f1 . d) = ( Sum (d rExpSeq )) by A2

 .= (f2 . d) by A3;

 end;

 hence f1 = f2;

 end;

 end

 definition

 let th be Real;

 :: SIN_COS:def23

 func exp_R th -> number equals ( exp_R . th);

 coherence ;

 end

 registration

 let th be Real;

 cluster ( exp_R th) -> real;

 coherence ;

 end

 theorem :: SIN_COS:47



 Th46: ( dom exp_R ) = REAL by FUNCT_2:def 1;

 theorem :: SIN_COS:48



 Th47: for th holds ( exp_R . th) = ( Re ( Sum (th ExpSeq )))

 proof

 let th;

 ( exp_R . th) = ( Sum (th rExpSeq )) by Def22;

 hence thesis by Th44;

 end;

 theorem :: SIN_COS:49

 for th holds ( exp th) = ( exp_R th)

 proof

 let th;



 thus ( exp th) = ( Sum (th ExpSeq )) by Def14

 .= ( Sum (th rExpSeq )) by Lm9

 .= ( exp_R th) by Def22;

 end;



 Lm10: for p,q be Real holds ( exp_R . (p + q)) = (( exp_R . p) * ( exp_R . q))

 proof

 let p,q be Real;

 ( exp_R . (p + q)) = ( Sum ((p + q) rExpSeq )) by Def22

 .= (( Sum (p rExpSeq )) * ( Sum (q rExpSeq ))) by Th45

 .= (( exp_R . p) * ( Sum (q rExpSeq ))) by Def22

 .= (( exp_R . p) * ( exp_R . q)) by Def22;

 hence thesis;

 end;

 theorem :: SIN_COS:50

 for p,q be Real holds ( exp_R (p + q)) = (( exp_R p) * ( exp_R q)) by Lm10;



 Lm11: ( exp_R . 0 ) = 1

 proof

 ( exp_R . 0 ) = ( Sum ( 0 rExpSeq )) by Def22

 .= 1 by Th9, Th44, COMPLEX1: 6;

 hence thesis;

 end;

 theorem :: SIN_COS:51

 ( exp_R 0 ) = 1 by Lm11;

 theorem :: SIN_COS:52



 Th51: th > 0 implies ( exp_R . th) >= 1

 proof

 assume

 A1: th > 0 ;



 A2: for n holds (( Partial_Sums (th rExpSeq )) . n) >= 1

 proof

 defpred X[ Nat] means (( Partial_Sums (th rExpSeq )) . $1) >= 1;

 (( Partial_Sums (th rExpSeq )) . 0 ) = ((th rExpSeq ) . 0 ) by SERIES_1:def 1

 .= ((th |^ 0 ) / ( 0 ! )) by Def5

 .= 1 by NEWTON: 4, NEWTON: 12;

 then

 A3: X[ 0 ];



 A4: for n st X[n] holds X[(n + 1)]

 proof

 let n;

 assume

 A5: (( Partial_Sums (th rExpSeq )) . n) >= 1;



 A6: (( Partial_Sums (th rExpSeq )) . (n + 1)) = ((( Partial_Sums (th rExpSeq )) . n) + ((th rExpSeq ) . (n + 1))) by SERIES_1:def 1

 .= ((( Partial_Sums (th rExpSeq )) . n) + ((th |^ (n + 1)) / ((n + 1) ! ))) by Def5;

 (th |^ (n + 1)) > 0 & ((n + 1) ! ) > 0 by A1, PREPOWER: 6;

 then ((( Partial_Sums (th rExpSeq )) . n) + ((th |^ (n + 1)) / ((n + 1) ! ))) > (( Partial_Sums (th rExpSeq )) . n) by XREAL_1: 29;

 hence thesis by A5, A6, XXREAL_0: 2;

 end;

 for n holds X[n] from NAT_1:sch 2( A3, A4);

 hence thesis;

 end;

 (th rExpSeq ) is summable by Th44;

 then

 A7: ( Partial_Sums (th rExpSeq )) is convergent by SERIES_1:def 2;

 ( lim ( Partial_Sums (th rExpSeq ))) = ( Sum (th rExpSeq )) by SERIES_1:def 3;

 then ( Sum (th rExpSeq )) >= 1 by A2, A7, PREPOWER: 1;

 hence thesis by Def22;

 end;

 theorem :: SIN_COS:53



 Th52: th < 0 implies 0 < ( exp_R . th) & ( exp_R . th) <= 1

 proof

 assume th < 0 ;

 then

 A1: ( exp_R . ( - th)) >= 1 by Th51;



 A2: (( exp_R . ( - th)) * ( exp_R . th)) = ( exp_R . (( - th) + th)) by Lm10

 .= 1 by Lm11;

 then

 A3: ( exp_R . th) = (1 / ( exp_R . ( - th))) by XCMPLX_1: 73;

 thus 0 < ( exp_R . th) by A1, A2;

 thus thesis by A1, A3, XREAL_1: 211;

 end;

 theorem :: SIN_COS:54



 Th53: ( exp_R . th) > 0

 proof

 now

 per cases ;

 suppose th = 0 ;

 hence thesis by Lm11;

 end;

 suppose

 A1: th <> 0 ;

 now

 per cases by A1;

 suppose th < 0 ;

 hence thesis by Th52;

 end;

 suppose th > 0 ;

 hence thesis by Th51;

 end;

 end;

 hence thesis;

 end;

 end;

 hence thesis;

 end;

 theorem :: SIN_COS:55

 ( exp_R th) > 0 by Th53;

 begin

 definition

 let z be Complex;

 deffunc U( Nat) = ((z |^ ($1 + 1)) / (($1 + 2) ! ));

 :: SIN_COS:def24

 func z P_dt -> Complex_Sequence means

 : Def24: for n holds (it . n) = ((z |^ (n + 1)) / ((n + 2) ! ));

 existence

 proof

 thus ex s be Complex_Sequence st for n holds (s . n) = U(n) from COMSEQ_1:sch 1;

 end;

 uniqueness

 proof

 let s1,s2 be Complex_Sequence such that

 A1: for x be Nat holds (s1 . x) = U(x) and

 A2: for x be Nat holds (s2 . x) = U(x);

 let x be Element of NAT ;



 thus (s1 . x) = U(x) by A1

 .= (s2 . x) by A2;

 end;

 deffunc U( Nat) = ((z |^ $1) / (($1 + 2) ! ));

 :: SIN_COS:def25

 func z P_t -> Complex_Sequence means for n holds (it . n) = ((z |^ n) / ((n + 2) ! ));

 existence

 proof

 thus ex s be Complex_Sequence st for n holds (s . n) = U(n) from COMSEQ_1:sch 1;

 end;

 uniqueness

 proof

 let s1,s2 be Complex_Sequence such that

 A3: for x be Nat holds (s1 . x) = U(x) and

 A4: for x be Nat holds (s2 . x) = U(x);

 let x be Element of NAT ;



 thus (s1 . x) = U(x) by A3

 .= (s2 . x) by A4;

 end;

 end



 Lm12: for p be Real, z be Complex 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 be Real, z be Complex;



 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 be Real, z be Complex 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, z be Complex 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: 86

 .= (((( 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 :: SIN_COS:56



 Th55: for z be Complex holds (z P_dt ) is absolutely_summable

 proof

 let z be Complex;

 ex r st for n holds (( Partial_Sums |.(z P_dt ).|) . n) < r

 proof



 A1: for n holds (( Partial_Sums |.(z P_dt ).|) . n) < (( Partial_Sums |.(z ExpSeq ).|) . (n + 1))

 proof

 let n;

 (( Partial_Sums |.(z P_dt ).|) . 0 ) = ( |.(z P_dt ).| . 0 ) by SERIES_1:def 1

 .= |.((z P_dt ) . 0 ).| by VALUED_1: 18

 .= |.((z |^ ( 0 + 1)) / (( 0 + 2) ! )).| by Def24

 .= |.(z / 2).| by NEWTON: 14;

 then

 A2: (( Partial_Sums |.(z P_dt ).|) . 0 ) = ( |.z.| / 2) by Lm13;

 (( Partial_Sums |.(z ExpSeq ).|) . ( 0 + 1)) = ((( Partial_Sums |.(z ExpSeq ).|) . 0 ) + ( |.(z ExpSeq ).| . ( 0 + 1))) by SERIES_1:def 1

 .= (( |.(z ExpSeq ).| . 0 ) + ( |.(z ExpSeq ).| . 1)) by SERIES_1:def 1

 .= (( |.(z ExpSeq ).| . 0 ) + |.((z ExpSeq ) . 1).|) by VALUED_1: 18

 .= ( |.((z ExpSeq ) . 0 ).| + |.((z ExpSeq ) . 1).|) by VALUED_1: 18

 .= ( |.((z ExpSeq ) . 0 ).| + |.z.|) by Lm8

 .= (1 + |.z.|) by Lm8, COMPLEX1: 48;

 then

 A3: ((( Partial_Sums |.(z ExpSeq ).|) . ( 0 + 1)) - (( Partial_Sums |.(z P_dt ).|) . 0 )) = (1 + ( |.z.| - ( |.z.| / 2))) by A2;

 defpred X[ Nat] means (( Partial_Sums |.(z P_dt ).|) . $1) < (( Partial_Sums |.(z ExpSeq ).|) . ($1 + 1));

 0 <= |.z.| by COMPLEX1: 46;

 then

 A4: X[ 0 ] by A3, XREAL_1: 47;



 A5: for n st X[n] holds X[(n + 1)]

 proof

 let n such that

 A6: (( Partial_Sums |.(z P_dt ).|) . n) < (( Partial_Sums |.(z ExpSeq ).|) . (n + 1));

 (( Partial_Sums |.(z P_dt ).|) . (n + 1)) = ((( Partial_Sums |.(z P_dt ).|) . n) + ( |.(z P_dt ).| . (n + 1))) by SERIES_1:def 1

 .= ((( Partial_Sums |.(z P_dt ).|) . n) + |.((z P_dt ) . (n + 1)).|) by VALUED_1: 18

 .= ((( Partial_Sums |.(z P_dt ).|) . n) + |.((z |^ ((n + 1) + 1)) / (((n + 1) + 2) ! )).|) by Def24

 .= ((( Partial_Sums |.(z P_dt ).|) . n) + |.((z |^ (n + 2)) / ((n + 3) ! )).|);

 then

 A7: (( Partial_Sums |.(z P_dt ).|) . (n + 1)) = ((( Partial_Sums |.(z P_dt ).|) . n) + ( |.(z |^ (n + 2)).| / ((n + 3) ! ))) by Lm13;

 (( Partial_Sums |.(z ExpSeq ).|) . ((n + 1) + 1)) = ((( Partial_Sums |.(z ExpSeq ).|) . (n + 1)) + ( |.(z ExpSeq ).| . (n + (1 + 1)))) by SERIES_1:def 1

 .= ((( Partial_Sums |.(z ExpSeq ).|) . (n + 1)) + |.((z ExpSeq ) . (n + 2)).|) by VALUED_1: 18

 .= ((( Partial_Sums |.(z ExpSeq ).|) . (n + 1)) + |.((z |^ (n + 2)) / ((n + 2) ! )).|) by Def4

 .= ((( Partial_Sums |.(z ExpSeq ).|) . (n + 1)) + |.((z |^ (n + 2)) / ((n + 2) ! )).|);

 then

 A8: (( Partial_Sums |.(z ExpSeq ).|) . ((n + 1) + 1)) = ((( Partial_Sums |.(z ExpSeq ).|) . (n + 1)) + ( |.(z |^ (n + 2)).| / ((n + 2) ! ))) by Lm13;

 (n + 2) < (n + 3) by XREAL_1: 6;

 then

 A9: ((n + 2) ! ) <= ((n + 3) ! ) by Th38;

 |.(z |^ (n + 2)).| >= 0 by COMPLEX1: 46;

 then ( |.(z |^ (n + 2)).| / ((n + 2) ! )) >= ( |.(z |^ (n + 2)).| / ((n + 3) ! )) by A9, XREAL_1: 118;

 then

 A10: ((( Partial_Sums |.(z P_dt ).|) . n) + ( |.(z |^ (n + 2)).| / ((n + 3) ! ))) <= ((( Partial_Sums |.(z P_dt ).|) . n) + ( |.(z |^ (n + 2)).| / ((n + 2) ! ))) by XREAL_1: 6;

 ((( Partial_Sums |.(z P_dt ).|) . n) + ( |.(z |^ (n + 2)).| / ((n + 2) ! ))) < ((( Partial_Sums |.(z ExpSeq ).|) . (n + 1)) + ( |.(z |^ (n + 2)).| / ((n + 2) ! ))) by A6, XREAL_1: 6;

 hence thesis by A7, A8, A10, XXREAL_0: 2;

 end;

 for n holds X[n] from NAT_1:sch 2( A4, A5);

 hence thesis;

 end;

 consider r be Real such that

 A11: for n holds (( Partial_Sums |.(z ExpSeq ).|) . n) < r by SEQ_2:def 3;



 A12: for n holds (( Partial_Sums |.(z P_dt ).|) . n) < r

 proof

 let n;

 (( Partial_Sums |.(z P_dt ).|) . n) < (( Partial_Sums |.(z ExpSeq ).|) . (n + 1)) by A1;

 hence thesis by A11, XXREAL_0: 2;

 end;

 take r;

 thus thesis by A12;

 end;

 then ( Partial_Sums |.(z P_dt ).|) is bounded_above by SEQ_2:def 3;

 hence thesis by COMSEQ_3: 61;

 end;

 theorem :: SIN_COS:57



 Th56: for z be Complex holds (z * ( Sum (z P_dt ))) = ((( Sum (z ExpSeq )) - 1r ) - z)

 proof

 let z be Complex;



 A1: for z be Complex holds (z (#) (z P_dt )) = ((z ExpSeq ) ^\ 2)

 proof

 let z be Complex;

 for n be Element of NAT holds ((z (#) (z P_dt )) . n) = (((z ExpSeq ) ^\ 2) . n)

 proof

 let n be Element of NAT ;

 ((z (#) (z P_dt )) . n) = (z * ((z P_dt ) . n)) by VALUED_1: 6

 .= (z * ((z |^ (n + 1)) / ((n + 2) ! ))) by Def24;



 then ((z (#) (z P_dt )) . n) = ((z * (z |^ (n + 1))) / ((n + 2) ! ))

 .= ((z |^ ((n + 1) + 1)) / ((n + 2) ! )) by NEWTON: 6

 .= ((z ExpSeq ) . (n + 2)) by Def4

 .= (((z ExpSeq ) ^\ 2) . n) by NAT_1:def 3;

 hence thesis;

 end;

 hence thesis;

 end;

 ( Sum (z ExpSeq )) = ((( Partial_Sums (z ExpSeq )) . 1) + ( Sum ((z ExpSeq ) ^\ (1 + 1)))) by COMSEQ_3: 60

 .= ((( Partial_Sums (z ExpSeq )) . 1) + ( Sum ((z ExpSeq ) ^\ 2)));



 then

 A2: ( Sum (z (#) (z P_dt ))) = (( Sum (z ExpSeq )) - (( Partial_Sums (z ExpSeq )) . ( 0 + 1))) by A1

 .= (( Sum (z ExpSeq )) - ((( Partial_Sums (z ExpSeq )) . 0 ) + ((z ExpSeq ) . 1))) by SERIES_1:def 1

 .= (( Sum (z ExpSeq )) - (((z ExpSeq ) . 0 ) + ((z ExpSeq ) . 1))) by SERIES_1:def 1

 .= (( Sum (z ExpSeq )) - ( 1r + ((z ExpSeq ) . 1))) by Lm8

 .= (( Sum (z ExpSeq )) - ( 1r + z)) by Lm8

 .= ((( Sum (z ExpSeq )) - 1r ) - z);

 reconsider BBB = (z P_dt ) as absolutely_summable Complex_Sequence by Th55;

 BBB is summable;

 hence thesis by A2, COMSEQ_3: 56;

 end;

 theorem :: SIN_COS:58



 Th57: for p st p > 0 holds ex q st q > 0 & for z be Complex st |.z.| < q holds |.( Sum (z P_dt )).| < p

 proof



 A1: for z holds |.( Sum (z P_dt )).| <= ( Sum |.(z P_dt ).|)

 proof

 let z;



 A2: for k holds ( |.( Partial_Sums (z P_dt )).| . k) <= (( Partial_Sums |.(z P_dt ).|) . k)

 proof

 let k;

 |.(( Partial_Sums (z P_dt )) . k).| = ( |.( Partial_Sums (z P_dt )).| . k) by VALUED_1: 18;

 hence thesis by COMSEQ_3: 30;

 end;



 A3: (z P_dt ) is absolutely_summable by Th55;



 A4: (z P_dt ) is summable by Th55, COMSEQ_3: 63;



 A5: ( lim |.( Partial_Sums (z P_dt )).|) = |.( lim ( Partial_Sums (z P_dt ))).| by A4, SEQ_2: 27;

 ( lim |.( Partial_Sums (z P_dt )).|) <= ( lim ( Partial_Sums |.(z P_dt ).|)) by A2, A3, SEQ_2: 18;

 hence thesis by A5, SERIES_1:def 3;

 end;



 A6: for z, n holds ( |.(z P_dt ).| . n) <= ( |.z.| * (( |.z.| GeoSeq ) . n))

 proof

 let z, n;

 ( |.(z P_dt ).| . n) = |.((z P_dt ) . n).| by VALUED_1: 18

 .= |.((z |^ (n + 1)) / ((n + 2) ! )).| by Def24

 .= |.((z |^ (n + 1)) / ((n + 2) ! )).|;



 then

 A7: ( |.(z P_dt ).| . n) = ( |.(z |^ (n + 1)).| / ((n + 2) ! )) by Lm13

 .= (( |.z.| |^ (n + 1)) / ((n + 2) ! )) by Lm8;



 A8: ( |.z.| * (( |.z.| GeoSeq ) . n)) = ( |.z.| * ( |.z.| |^ n)) by PREPOWER:def 1

 .= ( |.z.| |^ (n + 1)) by NEWTON: 6;

 ((n + 2) ! ) >= 1 & ( |.z.| |^ (n + 1)) >= 0 by Th38, COMPLEX1: 46, NEWTON: 12, POWER: 3;

 then (( |.z.| |^ (n + 1)) / 1) >= (( |.z.| |^ (n + 1)) / ((n + 2) ! )) by XREAL_1: 118;

 hence thesis by A7, A8;

 end;

 let p0 be Real;

 assume

 A9: p0 > 0 ;

 reconsider p = p0 as Real;

 consider q such that

 A10: q = (p / (p + 1));

 (p + 1) > p by XREAL_1: 29;

 then

 A11: q < 1 by A9, A10, XREAL_1: 189;



 A12: for z st |.z.| < q holds |.( Sum (z P_dt )).| < p

 proof

 let z;

 assume

 A13: |.z.| < q;

 then

 A14: |.z.| < 1 by A11, XXREAL_0: 2;



 A15: |. |.z.|.| < 1 by A11, A13, XXREAL_0: 2;

 then

 A16: ( |.z.| GeoSeq ) is summable by SERIES_1: 24;



 A17: ( Sum ( |.z.| GeoSeq )) = (1 / (1 - |.z.|)) by A15, SERIES_1: 24;



 A18: ( |.z.| (#) ( |.z.| GeoSeq )) is summable by A16, SERIES_1: 10;



 A19: for n holds ( |.(z P_dt ).| . n) <= (( |.z.| (#) ( |.z.| GeoSeq )) . n)

 proof

 let n;

 ( |.(z P_dt ).| . n) <= ( |.z.| * (( |.z.| GeoSeq ) . n)) by A6;

 hence thesis by SEQ_1: 9;

 end;

 for n holds 0 <= ( |.(z P_dt ).| . n)

 proof

 let n;

 ( |.(z P_dt ).| . n) = |.((z P_dt ) . n).| by VALUED_1: 18;

 hence thesis by COMPLEX1: 46;

 end;

 then

 A20: ( Sum |.(z P_dt ).|) <= ( Sum ( |.z.| (#) ( |.z.| GeoSeq ))) by A18, A19, SERIES_1: 20;



 A21: ( Sum ( |.z.| (#) ( |.z.| GeoSeq ))) = ( |.z.| / (1 - |.z.|)) by A16, A17, SERIES_1: 10;



 A22: ( |.z.| * (p + 1)) < ((p / (p + 1)) * (p + 1)) by A9, A10, A13, XREAL_1: 68;

 ((p / (p + 1)) * (p + 1)) = p by A9, XCMPLX_1: 87;

 then

 A23: (((p * |.z.|) + |.z.|) - (p * |.z.|)) < (p - (p * |.z.|)) by A22, XREAL_1: 9;



 A24: (1 - |.z.|) > 0 by A14, XREAL_1: 50;

 then ( |.z.| / (1 - |.z.|)) < ((p * (1 - |.z.|)) / (1 - |.z.|)) by A23, XREAL_1: 74;

 then ( |.z.| / (1 - |.z.|)) < p by A24, XCMPLX_1: 89;

 then

 A25: ( Sum |.(z P_dt ).|) 0 by A9, A10;

 let z be Complex;

 thus thesis by A12;

 end;

 theorem :: SIN_COS:59



 Th58: for z,z1 be Complex holds (( Sum ((z1 + z) ExpSeq )) - ( Sum (z1 ExpSeq ))) = ((( Sum (z1 ExpSeq )) * z) + ((z * ( Sum (z P_dt ))) * ( Sum (z1 ExpSeq ))))

 proof

 let z,z1 be Complex;

 (( Sum ((z1 + z) ExpSeq )) - ( Sum (z1 ExpSeq ))) = ((( Sum (z1 ExpSeq )) * ( Sum (z ExpSeq ))) - (( Sum (z1 ExpSeq )) * 1r )) by Lm2

 .= (( Sum (z1 ExpSeq )) * (((( Sum (z ExpSeq )) - 1r ) - z) + z))

 .= (( Sum (z1 ExpSeq )) * ((z * ( Sum (z P_dt ))) + z)) by Th56

 .= ((( Sum (z1 ExpSeq )) * z) + ((z * ( Sum (z P_dt ))) * ( Sum (z1 ExpSeq ))));

 hence thesis;

 end;

 theorem :: SIN_COS:60



 Th59: for p,q be 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 Th58

 .= ( 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 :: SIN_COS:61



 Th60: for p,q be 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 Th58

 .= ( 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 :: SIN_COS:62



 Th61: for p,q be Real holds (( exp_R . (p + q)) - ( exp_R . p)) = ((q * ( exp_R . p)) + ((q * ( exp_R . p)) * ( Re ( Sum (q P_dt )))))

 proof

 let p,q be Real;

 (( exp_R . (p + q)) - ( exp_R . p)) = (( exp_R . (p + q)) - ( Re ( Sum (p ExpSeq )))) by Th47

 .= (( Re ( Sum ((p + q) ExpSeq ))) - ( Re ( Sum (p ExpSeq )))) by Th47

 .= ( Re (( Sum ((p + q) ExpSeq )) - ( Sum (p ExpSeq )))) by COMPLEX1: 19

 .= ( Re ((( Sum (p ExpSeq )) * q) + ((q * ( Sum (q P_dt ))) * ( Sum (p ExpSeq ))))) by Th58

 .= (( Re (( Sum (p ExpSeq )) * q)) + ( Re ((q * ( Sum (q P_dt ))) * ( Sum (p ExpSeq ))))) by COMPLEX1: 8

 .= ((q * ( Re ( Sum (p ExpSeq )))) + ( Re ((q * ( Sum (q P_dt ))) * ( Sum (p ExpSeq ))))) by Lm12

 .= ((q * ( exp_R . p)) + ( Re (q * (( Sum (q P_dt )) * ( Sum (p ExpSeq )))))) by Th47

 .= ((q * ( exp_R . p)) + (q * ( Re (( Sum (q P_dt )) * ( Sum (p ExpSeq )))))) by Lm12

 .= ((q * ( exp_R . p)) + (q * ( Re (( Sum (q P_dt )) * ( Sum (p rExpSeq )))))) by Lm9

 .= ((q * ( exp_R . p)) + (q * ( Re (( Sum (q P_dt )) * (( exp_R . p) + ( 0 * )))))) 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 :: SIN_COS:63



 Th62: cos is_differentiable_in p & ( diff ( cos ,p)) = ( - ( sin . p))

 proof

 reconsider p as Element of REAL by XREAL_0:def 1;

 deffunc U( Real) = ( In (( - ($1 * ( Im (( Sum (($1 * ) P_dt )) * (( cos . p) + (( sin . p) * )))))), REAL ));

 consider Cr be Function of REAL , REAL such that

 A1: for th be Element of REAL holds (Cr . th) = U(th) from FUNCT_2:sch 4;

 for hy1 holds ((hy1 " ) (#) (Cr /* hy1)) is convergent & ( lim ((hy1 " ) (#) (Cr /* hy1))) = 0

 proof

 let hy1;



 A2: for n holds (((hy1 " ) (#) (Cr /* hy1)) . n) = ( - ( Im (( Sum (((hy1 . n) * ) P_dt )) * (( cos . p) + (( sin . p) * )))))

 proof

 let n;



 A3: n in NAT by ORDINAL1:def 12;



 A4: (((hy1 " ) (#) (Cr /* hy1)) . n) = (((hy1 " ) . n) * ((Cr /* hy1) . n)) by SEQ_1: 8

 .= (((hy1 . n) " ) * ((Cr /* hy1) . n)) by VALUED_1: 10;

 ( dom Cr) = REAL by FUNCT_2:def 1;

 then ( rng hy1) c= ( dom Cr);



 then

 A5: (((hy1 " ) (#) (Cr /* hy1)) . n) = (((hy1 . n) " ) * (Cr . (hy1 . n))) by A4, FUNCT_2: 108, A3

 .= (((hy1 . n) " ) * U(.)) 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 A5, 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

 A6: for n holds (rseq . n) = U(n) from SEQ_1:sch 1;

 deffunc U( Nat) = (( Sum (((hy1 . $1) * ) P_dt )) * (( cos . p) + (( sin . p) * )));

 consider cq1 such that

 A7: for n holds (cq1 . n) = U(n) from COMSEQ_1:sch 1;



 A8: for q be Real st q > 0 holds ex k st for m st k <= m holds |.((cq1 . m) - 0c ).| < q

 proof

 let q be Real such that

 A9: q > 0 ;

 ex k st for m st k <= m holds |.((cq1 . m) - 0c ).| < q

 proof

 consider r such that

 A10: r > 0 and

 A11: for z be Complex st |.z.| < r holds |.( Sum (z P_dt )).| < q by A9, Th57;

 hy1 is convergent & ( lim hy1) = 0 ;

 then

 consider k such that

 A12: for m st k <= m holds |.((hy1 . m) - 0 ).| < r by A10, SEQ_2:def 7;

 A13:

 now

 let m such that

 A14: k <= m;



 A15: |.((cq1 . m) - 0c ).| = |.(( Sum (((hy1 . m) * ) P_dt )) * (( cos . p) + (( sin . p) * ))).| by A7

 .= ( |.( 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 )).|;



 A16: |.((hy1 . m) - 0 ).| < r by A12, A14;

 ((hy1 . m) * ) = ( 0 + ((hy1 . m) * ));

 then ( Re ((hy1 . m) * )) = 0 & ( Im ((hy1 . m) * )) = (hy1 . m) by COMPLEX1: 12;

 then |.((hy1 . m) * ).| = |.(hy1 . m).| by COMPLEX1: 72;

 hence |.((cq1 . m) - 0c ).| < q by A11, A15, A16;

 end;

 take k;

 thus thesis by A13;

 end;

 hence thesis;

 end;

 then

 A17: cq1 is convergent by COMSEQ_2:def 5;

 then ( lim cq1) = 0c by A8, COMSEQ_2:def 6;

 then

 A18: ( lim ( - cq1)) = ( - 0c ) by A17, COMSEQ_2: 22;



 A19: for n be Element of NAT holds (( Im ( - cq1)) . n) = (rseq . n)

 proof



 A20: for n holds (( Im ( - cq1)) . n) = ( - ( Im (( Sum (((hy1 . n) * ) 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 A7

 .= ( - ( 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 A6;

 hence thesis by A20;

 end;

 for n be Element of NAT holds (rseq . n) = (((hy1 " ) (#) (Cr /* hy1)) . n)

 proof

 let n be Element of NAT ;

 (rseq . n) = ( - ( Im (( Sum (((hy1 . n) * ) P_dt )) * (( cos . p) + (( sin . p) * ))))) by A6;

 hence thesis by A2;

 end;

 then rseq = ((hy1 " ) (#) (Cr /* hy1));

 then ((hy1 " ) (#) (Cr /* hy1)) = ( Im ( - cq1)) by A19;

 hence thesis by A17, A18, COMPLEX1: 4, COMSEQ_3: 41;

 end;

 then

 reconsider PR = Cr as RestFunc by FDIFF_1:def 2;

 deffunc U1( Real) = ( In (( - ($1 * ( sin . p))), REAL ));

 consider CL be Function of REAL , REAL such that

 A21: for th be Element of REAL holds (CL . th) = U1(th) from FUNCT_2:sch 4;

 ex r st for q holds (CL . q) = (r * q)

 proof



 A22: for q holds (CL . q) = (( - ( sin . p)) * q)

 proof

 let q;

 reconsider qq = q as Element of REAL by XREAL_0:def 1;

 (CL . qq) = U1(q) by A21

 .= (( - ( sin . p)) * q);

 hence thesis;

 end;

 take ( - ( sin . p));

 thus thesis by A22;

 end;

 then

 reconsider PL = CL as LinearFunc by FDIFF_1:def 3;



 A23: ex N be Neighbourhood of p st N c= ( dom cos ) & for r st r in N holds (( cos . r) - ( cos . p)) = ((PL . (r - p)) + (PR . (r - p)))

 proof



 A24: for r st r in ].(p - 1), (p + 1).[ holds (( cos . r) - ( cos . p)) = ((PL . (r - p)) + (PR . (r - p)))

 proof

 let r;



 A25: (r - p) in REAL by XREAL_0:def 1;

 r = (p + (r - p));



 then (( cos . r) - ( cos . p)) = (( - ((r - p) * ( sin . p))) - ((r - p) * ( Im (( Sum (((r - p) * ) P_dt )) * (( cos . p) + (( sin . p) * )))))) by Th59

 .= (( - ((r - p) * ( sin . p))) + U(-))

 .= (( - ((r - p) * ( sin . p))) + (Cr . (r - p))) by A1, A25

 .= ( U1(-) + (Cr . (r - p)))

 .= ((PL . (r - p)) + (PR . (r - p))) by A21, A25;

 hence thesis;

 end;

 take ].(p - 1), (p + 1).[;

 thus thesis by A24, Th24, RCOMP_1:def 6;

 end;

 then

 A26: cos is_differentiable_in p by FDIFF_1:def 4;

 (PL . jj) = U1() by A21

 .= ( - ( sin . p));

 hence thesis by A23, A26, FDIFF_1:def 5;

 end;

 theorem :: SIN_COS:64



 Th63: sin is_differentiable_in p & ( diff ( sin ,p)) = ( cos . p)

 proof

 reconsider p as Real;

 deffunc U( Real) = ( In (($1 * ( Re (( Sum (($1 * ) P_dt )) * (( cos . p) + (( sin . p) * ))))), REAL ));

 consider Cr be Function of REAL , REAL such that

 A1: for th be Element of REAL holds (Cr . th) = U(th) from FUNCT_2:sch 4;

 for hy1 holds ((hy1 " ) (#) (Cr /* hy1)) is convergent & ( lim ((hy1 " ) (#) (Cr /* hy1))) = 0

 proof

 let hy1;



 A2: for n holds (((hy1 " ) (#) (Cr /* hy1)) . n) = ( Re (( Sum (((hy1 . n) * ) P_dt )) * (( cos . p) + (( sin . p) * ))))

 proof

 let n;



 A3: n in NAT by ORDINAL1:def 12;



 A4: (((hy1 " ) (#) (Cr /* hy1)) . n) = (((hy1 " ) . n) * ((Cr /* hy1) . n)) by SEQ_1: 8

 .= (((hy1 . n) " ) * ((Cr /* hy1) . n)) by VALUED_1: 10;

 ( dom Cr) = REAL by FUNCT_2:def 1;

 then ( rng hy1) c= ( dom Cr);



 then

 A5: (((hy1 " ) (#) (Cr /* hy1)) . n) = (((hy1 . n) " ) * (Cr . (hy1 . n))) by A4, FUNCT_2: 108, A3

 .= (((hy1 . n) " ) * U(.)) 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 A5, 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

 A6: for n holds (rseq . n) = U(n) from SEQ_1:sch 1;

 deffunc U( Nat) = (( Sum (((hy1 . $1) * ) P_dt )) * (( cos . p) + (( sin . p) * )));

 consider cq1 such that

 A7: for n holds (cq1 . n) = U(n) from COMSEQ_1:sch 1;



 A8: for q be Real st q > 0 holds ex k st for m st k <= m holds |.((cq1 . m) - 0c ).| < q

 proof

 let q be Real such that

 A9: q > 0 ;

 ex k st for m st k <= m holds |.((cq1 . m) - 0c ).| < q

 proof

 consider r such that

 A10: r > 0 and

 A11: for z be Complex st |.z.| < r holds |.( Sum (z P_dt )).| < q by A9, Th57;

 hy1 is convergent & ( lim hy1) = 0 ;

 then

 consider k such that

 A12: for m st k <= m holds |.((hy1 . m) - 0 ).| < r by A10, SEQ_2:def 7;

 A13:

 now

 let m such that

 A14: k <= m;



 A15: |.((cq1 . m) - 0c ).| = |.(( Sum (((hy1 . m) * ) P_dt )) * (( cos . p) + (( sin . p) * ))).| by A7

 .= ( |.( 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 )).|;



 A16: |.((hy1 . m) - 0 ).| < r by A12, A14;

 ((hy1 . m) * ) = ( 0 + ((hy1 . m) * ));

 then ( Re ((hy1 . m) * )) = 0 & ( Im ((hy1 . m) * )) = (hy1 . m) by COMPLEX1: 12;

 then |.((hy1 . m) * ).| = |.(hy1 . m).| by COMPLEX1: 72;

 hence |.((cq1 . m) - 0c ).| < q by A11, A15, A16;

 end;

 take k;

 thus thesis by A13;

 end;

 hence thesis;

 end;

 then

 A17: cq1 is convergent by COMSEQ_2:def 5;

 then

 A18: ( lim cq1) = 0c by A8, COMSEQ_2:def 6;



 A19: for n be Element of NAT holds (( Re cq1) . n) = (rseq . n)

 proof

 let n be Element of NAT ;

 (( Re cq1) . n) = ( Re (cq1 . n)) by COMSEQ_3:def 5

 .= ( Re (( Sum (((hy1 . n) * ) P_dt )) * (( cos . p) + (( sin . p) * )))) by A7;

 hence thesis by A6;

 end;

 for n be Element of NAT holds (rseq . n) = (((hy1 " ) (#) (Cr /* hy1)) . n)

 proof

 let n be Element of NAT ;

 (rseq . n) = ( Re (( Sum (((hy1 . n) * ) P_dt )) * (( cos . p) + (( sin . p) * )))) by A6;

 hence thesis by A2;

 end;

 then rseq = ((hy1 " ) (#) (Cr /* hy1));

 then ((hy1 " ) (#) (Cr /* hy1)) = ( Re cq1) by A19;

 hence thesis by A17, A18, COMPLEX1: 4, COMSEQ_3: 41;

 end;

 then

 reconsider PR = Cr as RestFunc by FDIFF_1:def 2;

 deffunc U1( Real) = ( In (($1 * ( cos . p)), REAL ));

 consider CL be Function of REAL , REAL such that

 A20: for th be Element of REAL holds (CL . th) = U1(th) from FUNCT_2:sch 4;



 A21: for d be Real holds (CL . d) = (d * ( cos . p))

 proof

 let d be Real;

 d in REAL by XREAL_0:def 1;

 then (CL . d) = U1(d) by A20;

 hence thesis;

 end;

 ex r st for q holds (CL . q) = (r * q)

 proof

 take ( cos . p);

 thus thesis by A21;

 end;

 then

 reconsider PL = CL as LinearFunc by FDIFF_1:def 3;



 A22: ex N be Neighbourhood of p st N c= ( dom sin ) & for r st r in N holds (( sin . r) - ( sin . p)) = ((PL . (r - p)) + (PR . (r - p)))

 proof



 A23: for r st r in ].(p - 1), (p + 1).[ holds (( sin . r) - ( sin . p)) = ((PL . (r - p)) + (PR . (r - p)))

 proof

 let r;



 A24: (r - p) in REAL by XREAL_0:def 1;

 r = (p + (r - p));



 then (( sin . r) - ( sin . p)) = (((r - p) * ( cos . p)) + ((r - p) * ( Re (( Sum (((r - p) * ) P_dt )) * (( cos . p) + (( sin . p) * )))))) by Th60

 .= (((r - p) * ( cos . p)) + U(-))

 .= (((r - p) * ( cos . p)) + (Cr . (r - p))) by A1, A24

 .= ((PL . (r - p)) + (PR . (r - p))) by A21;

 hence thesis;

 end;

 take ].(p - 1), (p + 1).[;

 thus thesis by A23, Th24, RCOMP_1:def 6;

 end;

 then

 A25: sin is_differentiable_in p by FDIFF_1:def 4;

 (PL . 1) = (1 * ( cos . p)) by A21;

 hence thesis by A22, A25, FDIFF_1:def 5;

 end;

 theorem :: SIN_COS:65



 Th64: exp_R is_differentiable_in p & ( diff ( exp_R ,p)) = ( exp_R . p)

 proof

 deffunc U( Real) = ( In ((($1 * ( exp_R . p)) * ( Re ( Sum ($1 P_dt )))), REAL ));

 consider Cr be Function of REAL , REAL such that

 A1: for th be Element of REAL holds (Cr . th) = U(th) from FUNCT_2:sch 4;

 for hy1 holds ((hy1 " ) (#) (Cr /* hy1)) is convergent & ( lim ((hy1 " ) (#) (Cr /* hy1))) = 0

 proof

 let hy1;



 A2: for n holds (((hy1 " ) (#) (Cr /* hy1)) . n) = (( exp_R . p) * ( Re ( Sum ((hy1 . n) P_dt ))))

 proof

 let n;



 A3: n in NAT by ORDINAL1:def 12;



 A4: (((hy1 " ) (#) (Cr /* hy1)) . n) = (((hy1 " ) . n) * ((Cr /* hy1) . n)) by SEQ_1: 8

 .= (((hy1 . n) " ) * ((Cr /* hy1) . n)) by VALUED_1: 10;

 ( dom Cr) = REAL by FUNCT_2:def 1;

 then ( rng hy1) c= ( dom Cr);



 then

 A5: (((hy1 " ) (#) (Cr /* hy1)) . n) = (((hy1 . n) " ) * (Cr . (hy1 . n))) by A4, FUNCT_2: 108, A3

 .= (((hy1 . n) " ) * U(.)) by A1

 .= ((((hy1 . n) " ) * (hy1 . n)) * (( exp_R . p) * ( Re ( Sum ((hy1 . n) P_dt )))));

 (hy1 . n) <> 0 by SEQ_1: 5;



 then (((hy1 " ) (#) (Cr /* hy1)) . n) = (1 * (( exp_R . p) * ( Re ( Sum ((hy1 . n) P_dt ))))) by A5, XCMPLX_0:def 7

 .= (( exp_R . p) * ( Re ( Sum ((hy1 . n) P_dt ))));

 hence thesis;

 end;

 deffunc U( Real) = (( exp_R . p) * ( Re ( Sum ((hy1 . $1) P_dt ))));

 consider rseq such that

 A6: for n holds (rseq . n) = U(n) from SEQ_1:sch 1;

 deffunc U( Nat) = (( Sum ((hy1 . $1) P_dt )) * ( exp_R . p));

 consider cq1 such that

 A7: for n holds (cq1 . n) = U(n) from COMSEQ_1:sch 1;



 A8: for q be Real st q > 0 holds ex k st for m st k <= m holds |.((cq1 . m) - 0c ).| < q

 proof

 let q be Real such that

 A9: q > 0 ;

 ex k st for m st k <= m holds |.((cq1 . m) - 0c ).| < q

 proof

 ( exp_R . p) > 0 by Th53;

 then

 consider r such that

 A10: r > 0 and

 A11: for z be Complex st |.z.| < r holds |.( Sum (z P_dt )).| < (q / ( exp_R . p)) by A9, Th57;

 hy1 is convergent & ( lim hy1) = 0 ;

 then

 consider k such that

 A12: for m st k <= m holds |.((hy1 . m) - 0 ).| < r by A10, SEQ_2:def 7;

 A13:

 now

 let m such that

 A14: k <= m;



 A15: |.((cq1 . m) - 0c ).| = |.(( Sum ((hy1 . m) P_dt )) * ( exp_R . p)).| by A7

 .= ( |.( Sum ((hy1 . m) P_dt )).| * |.( exp_R . p).|) by COMPLEX1: 65

 .= ( |.( Sum ((hy1 . m) P_dt )).| * ( sqrt ((( Re ( exp_R . p)) ^2 ) + (( Im ( exp_R . p)) ^2 ))));

 ( exp_R . p) = (( exp_R . p) + ( 0 * ));

 then

 A16: ( Re ( exp_R . p)) = ( exp_R . p) & ( Im ( exp_R . p)) = 0 by COMPLEX1: 12;



 A17: ( exp_R . p) > 0 by Th53;

 then

 A18: |.((cq1 . m) - 0c ).| = ( |.( Sum ((hy1 . m) P_dt )).| * ( exp_R . p)) by A15, A16, SQUARE_1: 22;

 |.((hy1 . m) - 0 ).| < r by A12, A14;

 then |.((cq1 . m) - 0c ).| < ((q / ( exp_R . p)) * ( exp_R . p)) by A11, A17, A18, XREAL_1: 68;

 hence |.((cq1 . m) - 0c ).| < q by A17, XCMPLX_1: 87;

 end;

 take k;

 thus thesis by A13;

 end;

 hence thesis;

 end;

 then

 A19: cq1 is convergent by COMSEQ_2:def 5;

 then

 A20: ( lim cq1) = 0c by A8, COMSEQ_2:def 6;



 A21: for n be Element of NAT holds (( Re cq1) . n) = (rseq . n)

 proof



 A22: for n holds (( Re cq1) . n) = (( exp_R . p) * ( Re ( Sum ((hy1 . n) P_dt ))))

 proof

 let n;

 (( Re cq1) . n) = ( Re (cq1 . n)) by COMSEQ_3:def 5

 .= ( Re (( Sum ((hy1 . n) P_dt )) * ( exp_R . p))) by A7

 .= (( exp_R . p) * ( Re ( Sum ((hy1 . n) P_dt )))) by Lm12;

 hence thesis;

 end;

 let n;

 (rseq . n) = (( exp_R . p) * ( Re ( Sum ((hy1 . n) P_dt )))) by A6;

 hence thesis by A22;

 end;

 for n be Element of NAT holds (rseq . n) = (((hy1 " ) (#) (Cr /* hy1)) . n)

 proof

 let n be Element of NAT ;

 (rseq . n) = (( exp_R . p) * ( Re ( Sum ((hy1 . n) P_dt )))) by A6;

 hence thesis by A2;

 end;

 then rseq = ((hy1 " ) (#) (Cr /* hy1));

 then ((hy1 " ) (#) (Cr /* hy1)) = ( Re cq1) by A21;

 hence thesis by A19, A20, COMPLEX1: 4, COMSEQ_3: 41;

 end;

 then

 reconsider PR = Cr as RestFunc by FDIFF_1:def 2;

 deffunc U1( Real) = ( In (($1 * ( exp_R . p)), REAL ));

 consider CL be Function of REAL , REAL such that

 A23: for th be Element of REAL holds (CL . th) = U1(th) from FUNCT_2:sch 4;



 A24: for d be Real holds (CL . d) = (d * ( exp_R . p))

 proof

 let d be Real;

 d in REAL by XREAL_0:def 1;

 then (CL . d) = U1(d) by A23;

 hence thesis;

 end;

 ex r st for q holds (CL . q) = (r * q)

 proof

 take ( exp_R . p);

 thus thesis by A24;

 end;

 then

 reconsider PL = CL as LinearFunc by FDIFF_1:def 3;



 A25: ex N be Neighbourhood of p st N c= ( dom exp_R ) & for r st r in N holds (( exp_R . r) - ( exp_R . p)) = ((PL . (r - p)) + (PR . (r - p)))

 proof



 A26: for r st r in ].(p - 1), (p + 1).[ holds (( exp_R . r) - ( exp_R . p)) = ((PL . (r - p)) + (PR . (r - p)))

 proof

 let r;

 reconsider p as Real;



 A27: (r - p) in REAL by XREAL_0:def 1;

 r = (p + (r - p));



 then (( exp_R . r) - ( exp_R . p)) = (((r - p) * ( exp_R . p)) + (((r - p) * ( exp_R . p)) * ( Re ( Sum ((r - p) P_dt ))))) by Th61

 .= (((r - p) * ( exp_R . p)) + U(-))

 .= (((r - p) * ( exp_R . p)) + (Cr . (r - p))) by A1, A27

 .= ((PL . (r - p)) + (PR . (r - p))) by A24;

 hence thesis;

 end;

 take ].(p - 1), (p + 1).[;

 thus thesis by A26, Th46, RCOMP_1:def 6;

 end;

 then

 A28: exp_R is_differentiable_in p by FDIFF_1:def 4;

 (PL . 1) = (1 * ( exp_R . p)) by A24;

 hence thesis by A25, A28, FDIFF_1:def 5;

 end;

 theorem :: SIN_COS:66



 Th65: exp_R is_differentiable_on REAL & ( diff ( exp_R ,th)) = ( exp_R . th)

 proof



 A1: ( [#] REAL ) is open Subset of REAL & REAL c= ( dom exp_R ) by FUNCT_2:def 1;

 for r st r in REAL holds exp_R is_differentiable_in r by Th64;

 hence thesis by A1, Th64, FDIFF_1: 9;

 end;

 theorem :: SIN_COS:67



 Th66: cos is_differentiable_on REAL & ( diff ( cos ,th)) = ( - ( sin . th))

 proof



 A1: ( [#] REAL ) is open Subset of REAL & REAL c= ( dom cos ) by FUNCT_2:def 1;

 for r st r in REAL holds cos is_differentiable_in r by Th62;

 hence thesis by A1, Th62, FDIFF_1: 9;

 end;

 theorem :: SIN_COS:68



 Th67: sin is_differentiable_on REAL & ( diff ( sin ,th)) = ( cos . th)

 proof



 A1: ( [#] REAL ) is open Subset of REAL & REAL c= ( dom sin ) by FUNCT_2:def 1;

 for r st r in REAL holds sin is_differentiable_in r by Th63;

 hence thesis by A1, Th63, FDIFF_1: 9;

 end;

 theorem :: SIN_COS:69



 Th68: th in [. 0 , 1.] implies 0 < ( cos . th) & ( cos . th) >= (1 / 2)

 proof

 assume th in [. 0 , 1.];

 then

 A1: 0 <= th & th <= 1 by XXREAL_1: 1;



 A2: ( Partial_Sums (th P_cos )) is convergent by Th35;



 A3: ( cos . th) = ( Sum (th P_cos )) by Th36;

 ( lim (( Partial_Sums (th P_cos )) * bq)) = ( lim ( Partial_Sums (th P_cos ))) by A2, SEQ_4: 17;

 then

 A4: ( lim (( Partial_Sums (th P_cos )) * bq)) = ( cos . th) by A3, SERIES_1:def 3;

 for n holds ((( Partial_Sums (th P_cos )) * bq) . n) >= (1 / 2)

 proof

 let n;



 A5: ((( Partial_Sums (th P_cos )) * bq) . 0 ) = (( Partial_Sums (th P_cos )) . (bq . 0 )) by FUNCT_2: 15

 .= (( Partial_Sums (th P_cos )) . ((2 * 0 ) + 1)) by Lm6

 .= ((( Partial_Sums (th P_cos )) . 0 ) + ((th P_cos ) . ( 0 + 1))) by SERIES_1:def 1

 .= (((th P_cos ) . 0 ) + ((th P_cos ) . ( 0 + 1))) by SERIES_1:def 1

 .= ((((( - 1) |^ 0 ) * (th |^ (2 * 0 ))) / ((2 * 0 ) ! )) + ((th P_cos ) . 1)) by Def21

 .= ((((( - 1) |^ 0 ) * (th |^ (2 * 0 ))) / ((2 * 0 ) ! )) + (((( - 1) |^ 1) * (th |^ (2 * 1))) / ((2 * 1) ! ))) by Def21

 .= (((1 * (th |^ (2 * 0 ))) / ((2 * 0 ) ! )) + (((( - 1) |^ 1) * (th |^ (2 * 1))) / ((2 * 1) ! ))) by Lm7

 .= ((1 / 1) + (((( - 1) |^ 1) * (th |^ (2 * 1))) / ((2 * 1) ! ))) by NEWTON: 4, NEWTON: 12

 .= (1 + ((( - 1) * (th |^ (2 * 1))) / ((2 * 1) ! )))

 .= (1 + ((( - 1) * (th * th)) / ((2 * 1) ! ))) by NEWTON: 81

 .= (1 - ((th ^2 ) / 2)) by NEWTON: 14;

 defpred X[ Nat] means ((( Partial_Sums (th P_cos )) * bq) . $1) >= (1 / 2);

 (th ^2 ) <= (1 ^2 ) by A1, SQUARE_1: 15;

 then (1 - (1 / 2)) = (1 / 2) & ((th ^2 ) / 2) <= (1 / 2) by XREAL_1: 72;

 then

 A6: X[ 0 ] by A5, XREAL_1: 10;



 A7: for k st X[k] holds X[(k + 1)]

 proof

 let k;



 A8: k in NAT by ORDINAL1:def 12;

 assume

 A9: ((( Partial_Sums (th P_cos )) * bq) . k) >= (1 / 2);

 ((( Partial_Sums (th P_cos )) * bq) . (k + 1)) = (( Partial_Sums (th P_cos )) . (bq . (k + 1))) by FUNCT_2: 15

 .= (( Partial_Sums (th P_cos )) . ((2 * (k + 1)) + 1)) by Lm6

 .= ((( Partial_Sums (th P_cos )) . (((2 * k) + 1) + 1)) + ((th P_cos ) . ((2 * (k + 1)) + 1))) by SERIES_1:def 1

 .= (((( Partial_Sums (th P_cos )) . ((2 * k) + 1)) + ((th P_cos ) . (((2 * k) + 1) + 1))) + ((th P_cos ) . ((2 * (k + 1)) + 1))) by SERIES_1:def 1

 .= (((( Partial_Sums (th P_cos )) . (bq . k)) + ((th P_cos ) . (((2 * k) + 1) + 1))) + ((th P_cos ) . ((2 * (k + 1)) + 1))) by Lm6

 .= ((((( Partial_Sums (th P_cos )) * bq) . k) + ((th P_cos ) . (((2 * k) + 1) + 1))) + ((th P_cos ) . ((2 * (k + 1)) + 1))) by FUNCT_2: 15, A8;

 then

 A10: (((( Partial_Sums (th P_cos )) * bq) . (k + 1)) - ((( Partial_Sums (th P_cos )) * bq) . k)) = (((th P_cos ) . (((2 * k) + 1) + 1)) + ((th P_cos ) . ((2 * (k + 1)) + 1)));



 A11: ((th P_cos ) . (((2 * k) + 1) + 1)) = (((( - 1) |^ (2 * (k + 1))) * (th |^ (2 * (2 * (k + 1))))) / ((2 * (2 * (k + 1))) ! )) by Def21

 .= ((1 * (th |^ (2 * (2 * (k + 1))))) / ((2 * (2 * (k + 1))) ! )) by Lm7

 .= ((th |^ (2 * (2 * (k + 1)))) / ((2 * (2 * (k + 1))) ! ));



 A12: ((th P_cos ) . ((2 * (k + 1)) + 1)) = (((( - 1) |^ ((2 * (k + 1)) + 1)) * (th |^ (2 * ((2 * (k + 1)) + 1)))) / ((2 * ((2 * (k + 1)) + 1)) ! )) by Def21

 .= ((( - 1) * (th |^ (2 * ((2 * (k + 1)) + 1)))) / ((2 * ((2 * (k + 1)) + 1)) ! )) by Lm7;



 A13: (2 * (2 * (k + 1))) < (2 * ((2 * (k + 1)) + 1)) by XREAL_1: 29, XREAL_1: 68;

 then

 A14: ((2 * (2 * (k + 1))) ! ) <= ((2 * ((2 * (k + 1)) + 1)) ! ) by Th38;



 A15: (th |^ (2 * ((2 * (k + 1)) + 1))) <= (th |^ (2 * (2 * (k + 1)))) by A1, A13, Th39;



 A16: 0 <= (th |^ (2 * ((2 * (k + 1)) + 1))) & ((2 * ((2 * (k + 1)) + 1)) ! ) > 0 by POWER: 3;

 (1 / ((2 * ((2 * (k + 1)) + 1)) ! )) <= (1 / ((2 * (2 * (k + 1))) ! )) by A14, XREAL_1: 85;

 then ((th |^ (2 * ((2 * (k + 1)) + 1))) * (1 / ((2 * ((2 * (k + 1)) + 1)) ! ))) <= ((th |^ (2 * (2 * (k + 1)))) * (1 / ((2 * (2 * (k + 1))) ! ))) by A15, A16, XREAL_1: 66;

 then ((((th |^ (2 * (2 * (k + 1)))) * 1) / ((2 * (2 * (k + 1))) ! )) - (((th |^ (2 * ((2 * (k + 1)) + 1))) * 1) / ((2 * ((2 * (k + 1)) + 1)) ! ))) >= 0 by XREAL_1: 48;

 then ((( Partial_Sums (th P_cos )) * bq) . (k + 1)) >= ((( Partial_Sums (th P_cos )) * bq) . k) by A10, A11, A12, XREAL_1: 49;

 hence thesis by A9, XXREAL_0: 2;

 end;

 for n holds X[n] from NAT_1:sch 2( A6, A7);

 hence thesis;

 end;

 hence thesis by A2, A4, PREPOWER: 1, SEQ_4: 16;

 end;

 definition

 :: SIN_COS:def26

 func tan -> PartFunc of REAL , REAL equals ( sin / cos );

 coherence ;

 :: SIN_COS:def27

 func cot -> PartFunc of REAL , REAL equals ( cos / sin );

 coherence ;

 end

 theorem :: SIN_COS:70



 Th69: [. 0 , 1.] c= ( dom tan ) & ]. 0 , 1.[ c= ( dom tan )

 proof



 A1: ( [. 0 , 1.] \ ( cos " { 0 })) c= (( dom cos ) \ ( cos " { 0 })) by Th24, XBOOLE_1: 33;

 ( [. 0 , 1.] /\ ( cos " { 0 })) = {}

 proof

 assume ( [. 0 , 1.] /\ ( cos " { 0 })) <> {} ;

 then

 consider rr be object such that

 A2: rr in ( [. 0 , 1.] /\ ( cos " { 0 })) by XBOOLE_0:def 1;



 A3: rr in [. 0 , 1.] by A2, XBOOLE_0:def 4;



 A4: rr in ( cos " { 0 }) by A2, XBOOLE_0:def 4;



 A5: ( cos . rr) <> 0 by A3, Th68;

 ( cos . rr) in { 0 } by A4, FUNCT_1:def 7;

 hence contradiction by A5, TARSKI:def 1;

 end;

 then [. 0 , 1.] misses ( cos " { 0 }) by XBOOLE_0:def 7;

 then [. 0 , 1.] c= (( dom cos ) \ ( cos " { 0 })) by A1, XBOOLE_1: 83;

 then [. 0 , 1.] c= (( dom sin ) /\ (( dom cos ) \ ( cos " { 0 }))) by Th24, XBOOLE_1: 19;

 then

 A6: [. 0 , 1.] c= ( dom tan ) by RFUNCT_1:def 1;

 ]. 0 , 1.[ c= [. 0 , 1.] by XXREAL_1: 25;

 hence thesis by A6, XBOOLE_1: 1;

 end;



 Lm14: ( dom ( tan | [. 0 , 1.])) = [. 0 , 1.] & for th st th in [. 0 , 1.] holds (( tan | [. 0 , 1.]) . th) = ( tan . th)

 proof

 ( dom ( tan | [. 0 , 1.])) = (( dom tan ) /\ [. 0 , 1.]) by RELAT_1: 61;

 then ( dom ( tan | [. 0 , 1.])) = [. 0 , 1.] by Th69, XBOOLE_1: 28;

 hence thesis by FUNCT_1: 47;

 end;



 Lm15: tan is_differentiable_on ]. 0 , 1.[ & for th st th in ]. 0 , 1.[ holds ( diff ( tan ,th)) > 0

 proof



 A1: sin is_differentiable_on ]. 0 , 1.[ & cos is_differentiable_on ]. 0 , 1.[ by Th66, Th67, FDIFF_1: 26;



 A2: for th st th in ]. 0 , 1.[ holds ( cos . th) <> 0

 proof

 let th such that

 A3: th in ]. 0 , 1.[;

 ]. 0 , 1.[ c= [. 0 , 1.] by XXREAL_1: 25;

 hence thesis by A3, Th68;

 end;

 for th st th in ]. 0 , 1.[ holds ( diff ( tan ,th)) > 0

 proof

 let th such that

 A4: th in ]. 0 , 1.[;



 A5: th is Real & cos is_differentiable_in th by Th62;



 A6: sin is_differentiable_in th by Th63;



 A7: ( cos . th) <> 0 by A2, A4;



 then

 A8: ( diff ( tan ,th)) = (((( diff ( sin ,th)) * ( cos . th)) - (( diff ( cos ,th)) * ( sin . th))) / (( cos . th) ^2 )) by A5, A6, FDIFF_2: 14

 .= (((( cos . th) * ( cos . th)) - (( diff ( cos ,th)) * ( sin . th))) / (( cos . th) ^2 )) by Th63

 .= (((( cos . th) * ( cos . th)) - (( - ( sin . th)) * ( sin . th))) / (( cos . th) ^2 )) by Th62

 .= (((( cos . th) ^2 ) + (( sin . th) * ( sin . th))) / (( cos . th) ^2 ))

 .= (1 / (( cos . th) ^2 )) by Th28;

 (( cos . th) ^2 ) > 0 by A7, SQUARE_1: 12;

 hence thesis by A8;

 end;

 hence thesis by A1, A2, FDIFF_2: 21;

 end;

 theorem :: SIN_COS:71



 Th70: ( tan | [. 0 , 1.]) is continuous

 proof

 for th be Real st th in ( dom ( tan | [. 0 , 1.])) holds ( tan | [. 0 , 1.]) is_continuous_in th

 proof

 let th be Real;

 assume

 A1: th in ( dom ( tan | [. 0 , 1.]));

 then

 A2: th in [. 0 , 1.] by RELAT_1: 57;

 ( dom sin ) = REAL by FUNCT_2:def 1;

 then

 A3: th in ( dom sin ) by XREAL_0:def 1;



 A4: th in ( [#] REAL ) by XREAL_0:def 1;

 then sin is_differentiable_in th by Th67, FDIFF_1: 9;

 then

 A5: sin is_continuous_in th by FDIFF_1: 24;

 cos is_differentiable_in th by A4, Th66, FDIFF_1: 9;

 then

 A6: cos is_continuous_in th by FDIFF_1: 24;

 ( cos . th) <> 0 by A2, Th68;

 then

 A7: tan is_continuous_in th by A3, A5, A6, FCONT_1: 11;

 now

 let rseq;

 assume that

 A8: ( rng rseq) c= ( dom ( tan | [. 0 , 1.])) and

 A9: rseq is convergent & ( lim rseq) = th;



 A10: ( rng rseq) c= ( dom tan ) by A8, Lm14, Th69, XBOOLE_1: 1;

 then

 A11: ( tan . th) = ( lim ( tan /* rseq)) by A7, A9, FCONT_1:def 1;

 now

 let k1 be Element of NAT ;

 ( dom rseq) = NAT by SEQ_1: 1;

 then (rseq . k1) in ( rng rseq) by FUNCT_1:def 3;

 then

 A12: (( tan | [. 0 , 1.]) . (rseq . k1)) = ( tan . (rseq . k1)) by A8, Lm14;

 (( tan | [. 0 , 1.]) . (rseq . k1)) = ((( tan | [. 0 , 1.]) /* rseq) . k1) by A8, FUNCT_2: 108;

 hence ((( tan | [. 0 , 1.]) /* rseq) . k1) = (( tan /* rseq) . k1) by A8, A12, Lm14, Th69, FUNCT_2: 108, XBOOLE_1: 1;

 end;

 then (( tan | [. 0 , 1.]) /* rseq) = ( tan /* rseq);

 hence (( tan | [. 0 , 1.]) /* rseq) is convergent & (( tan | [. 0 , 1.]) . th) = ( lim (( tan | [. 0 , 1.]) /* rseq)) by A1, A7, A9, A10, A11, Lm14, FCONT_1:def 1;

 end;

 hence thesis by FCONT_1:def 1;

 end;

 hence thesis by FCONT_1:def 2;

 end;

 theorem :: SIN_COS:72



 Th71: th1 in ]. 0 , 1.[ & th2 in ]. 0 , 1.[ & ( tan . th1) = ( tan . th2) implies th1 = th2

 proof

 assume that

 A1: th1 in ]. 0 , 1.[ and

 A2: th2 in ]. 0 , 1.[ and

 A3: ( tan . th1) = ( tan . th2);



 A4: 0 < th1 by A1, XXREAL_1: 4;



 A5: th1 < 1 by A1, XXREAL_1: 4;



 A6: 0 < th2 by A2, XXREAL_1: 4;



 A7: th2 < 1 by A2, XXREAL_1: 4;

 assume

 A8: th1 <> th2;

 now

 per cases by A8, XXREAL_0: 1;

 suppose

 A9: th1 < th2;



 A10: for th be Element of REAL st th in ].th1, th2.[ holds th in ]. 0 , 1.[

 proof

 let th be Element of REAL ;

 assume

 A11: th in ].th1, th2.[;

 then

 A12: th1 < th by XXREAL_1: 4;

 th < th2 by A11, XXREAL_1: 4;

 then th < 1 by A7, XXREAL_0: 2;

 hence thesis by A4, A12, XXREAL_1: 4;

 end;



 A13: for th be Element of REAL st th in [.th1, th2.] holds th in [. 0 , 1.]

 proof

 let th be Element of REAL ;

 assume

 A14: th in [.th1, th2.];

 then

 A15: th1 <= th by XXREAL_1: 1;

 th <= th2 by A14, XXREAL_1: 1;

 then th <= 1 by A7, XXREAL_0: 2;

 hence thesis by A4, A15, XXREAL_1: 1;

 end;

 ].th1, th2.[ c= ]. 0 , 1.[ by A10, SUBSET_1: 2;

 then

 A16: tan is_differentiable_on ].th1, th2.[ by Lm15, FDIFF_1: 26;

 [.th1, th2.] c= [. 0 , 1.] & ( tan | [.th1, th2.]) is continuous by A13, Th70, FCONT_1: 16, SUBSET_1: 2;

 then

 consider r such that

 A17: r in ].th1, th2.[ & ( diff ( tan ,r)) = 0 by A3, A9, A16, Th69, ROLLE: 1, XBOOLE_1: 1;

 take th = r;

 thus th in ]. 0 , 1.[ & ( diff ( tan ,th)) = 0 by A10, A17;

 end;

 suppose

 A18: th2 < th1;



 A19: for th be Element of REAL st th in ].th2, th1.[ holds th in ]. 0 , 1.[

 proof

 let th be Element of REAL ;

 assume

 A20: th in ].th2, th1.[;

 then

 A21: th2 < th by XXREAL_1: 4;

 th < th1 by A20, XXREAL_1: 4;

 then th < 1 by A5, XXREAL_0: 2;

 hence thesis by A6, A21, XXREAL_1: 4;

 end;



 A22: for th be Element of REAL st th in [.th2, th1.] holds th in [. 0 , 1.]

 proof

 let th be Element of REAL ;

 assume

 A23: th in [.th2, th1.];

 then

 A24: th2 <= th by XXREAL_1: 1;

 th <= th1 by A23, XXREAL_1: 1;

 then th <= 1 by A5, XXREAL_0: 2;

 hence thesis by A6, A24, XXREAL_1: 1;

 end;

 ].th2, th1.[ c= ]. 0 , 1.[ by A19, SUBSET_1: 2;

 then

 A25: tan is_differentiable_on ].th2, th1.[ by Lm15, FDIFF_1: 26;

 [.th2, th1.] c= [. 0 , 1.] & ( tan | [.th2, th1.]) is continuous by A22, Th70, FCONT_1: 16, SUBSET_1: 2;

 then

 consider r such that

 A26: r in ].th2, th1.[ & ( diff ( tan ,r)) = 0 by A3, A18, A25, Th69, ROLLE: 1, XBOOLE_1: 1;

 take th = r;

 thus th in ]. 0 , 1.[ & ( diff ( tan ,th)) = 0 by A19, A26;

 end;

 end;

 hence thesis by Lm15;

 end;



 Lm16: ( tan . 0 ) = 0 & ( tan . 1) > 1

 proof

 0 in [. 0 , 1.] by XXREAL_1: 1;



 then

 A1: ( tan . 0 ) = (( sin . 0 ) * (( cos . 0 ) " )) by Th69, RFUNCT_1:def 1

 .= 0 by Th30;

 1 in [. 0 , 1.] by XXREAL_1: 1;

 then ( tan . 1) = (( sin . 1) / ( cos . 1)) by Th69, RFUNCT_1:def 1;

 hence thesis by A1, Th42, XREAL_1: 187;

 end;

 begin

 definition

 :: SIN_COS:def28

 func PI -> Real means

 : Def28: ( tan . (it / 4)) = 1 & it in ]. 0 , 4.[;

 existence

 proof



 A1: [.( tan . 0 ), ( tan . 1).] = { r : ( tan . 0 ) <= r & r <= ( tan . 1) } by RCOMP_1:def 1;

 [.( tan . 1), ( tan . 0 ).] = {} by Lm16, XXREAL_1: 29;

 then 1 in ( [.( tan . 0 ), ( tan . 1).] \/ [.( tan . 1), ( tan . 0 ).]) by A1, Lm16;

 then

 consider th such that

 A2: th in [. 0 , 1.] and

 A3: ( tan . th) = 1 by Th69, Th70, FCONT_2: 15;



 A4: 0 <= th by A2, XXREAL_1: 1;



 A5: th <= 1 by A2, XXREAL_1: 1;



 A6: 0 < th by A3, A4, Lm16;



 A7: th < 1 by A3, A5, Lm16, XXREAL_0: 1;

 take th1 = (th * 4);

 thus ( tan . (th1 / 4)) = 1 by A3;

 (th * 4) < (1 * 4) by A7, XREAL_1: 68;

 hence thesis by A6, XXREAL_1: 4;

 end;

 uniqueness

 proof

 let th1,th2 be Real such that

 A8: ( tan . (th1 / 4)) = 1 and

 A9: th1 in ]. 0 , 4.[ and

 A10: ( tan . (th2 / 4)) = 1 and

 A11: th2 in ]. 0 , 4.[;



 A12: 0 < th1 by A9, XXREAL_1: 4;

 th1 < 4 by A9, XXREAL_1: 4;

 then (th1 / 4) < (4 / 4) by XREAL_1: 74;

 then

 A13: (th1 / 4) in ]. 0 , 1.[ by A12, XXREAL_1: 4;



 A14: 0 < th2 by A11, XXREAL_1: 4;

 th2 < 4 by A11, XXREAL_1: 4;

 then (th2 / 4) < (4 / 4) by XREAL_1: 74;

 then (th2 / 4) in ]. 0 , 1.[ by A14, XXREAL_1: 4;

 then (th1 / 4) = (th2 / 4) by A8, A10, A13, Th71;

 hence thesis;

 end;

 end

 theorem :: SIN_COS:73



 Th72: ( sin . ( PI / 4)) = ( cos . ( PI / 4))

 proof



 A1: PI in ]. 0 , 4.[ by Def28;

 then

 A2: 0 < PI by XXREAL_1: 4;

 PI < 4 by A1, XXREAL_1: 4;

 then ( PI / 4) < (4 / 4) by XREAL_1: 74;

 then

 A3: ( PI / 4) in ]. 0 , 1.[ by A2, XXREAL_1: 4;

 ( tan . ( PI / 4)) = 1 by Def28;

 then (( sin . ( PI / 4)) * (( cos . ( PI / 4)) " )) = 1 by A3, Th69, RFUNCT_1:def 1;

 hence thesis by XCMPLX_1: 209;

 end;

 begin

 theorem :: SIN_COS:74



 Th73: ( sin . (th1 + th2)) = ((( sin . th1) * ( cos . th2)) + (( cos . th1) * ( sin . th2))) & ( cos . (th1 + th2)) = ((( cos . th1) * ( cos . th2)) - (( sin . th1) * ( sin . th2)))

 proof

 reconsider th1, th2 as Real;



 A1: ((th1 + th2) * ) = (( 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_COS:75

 ( sin (th1 + th2)) = ((( sin th1) * ( cos th2)) + (( cos th1) * ( sin th2))) & ( cos (th1 + th2)) = ((( cos th1) * ( cos th2)) - (( sin th1) * ( sin th2))) by Th73;

 theorem :: SIN_COS:76



 Th75: ( cos . ( PI / 2)) = 0 & ( sin . ( PI / 2)) = 1 & ( cos . PI ) = ( - 1) & ( sin . PI ) = 0 & ( cos . ( PI + ( PI / 2))) = 0 & ( sin . ( PI + ( PI / 2))) = ( - 1) & ( cos . (2 * PI )) = 1 & ( sin . (2 * PI )) = 0

 proof



 thus

 A1: ( cos . ( PI / 2)) = ( cos . (( PI / 4) + ( PI / 4)))

 .= ((( cos . ( PI / 4)) * ( cos . ( PI / 4))) - (( cos . ( PI / 4)) * ( cos . ( PI / 4)))) by Th72, Th73

 .= 0 ;



 thus

 A2: ( sin . ( PI / 2)) = ( sin . (( PI / 4) + ( PI / 4)))

 .= ((( cos . ( PI / 4)) * ( cos . ( PI / 4))) + (( sin . ( PI / 4)) * ( sin . ( PI / 4)))) by Th72, Th73

 .= 1 by Th28;



 thus

 A3: ( cos . PI ) = ( cos . (( PI / 2) + ( PI / 2)))

 .= (( 0 * 0 ) - (( sin . ( PI / 2)) * ( sin . ( PI / 2)))) by A1, Th73

 .= ( - 1) by A2;



 thus

 A4: ( sin . PI ) = ( sin . (( PI / 2) + ( PI / 2)))

 .= ((( sin . ( PI / 2)) * ( cos . ( PI / 2))) + (( cos . ( PI / 2)) * ( sin . ( PI / 2)))) by Th73

 .= 0 by A1;



 thus ( cos . ( PI + ( PI / 2))) = ((( cos . PI ) * ( cos . ( PI / 2))) - (( sin . PI ) * ( sin . ( PI / 2)))) by Th73

 .= 0 by A1, A4;



 thus ( sin . ( PI + ( PI / 2))) = ((( sin . PI ) * ( cos . ( PI / 2))) + (( cos . PI ) * ( sin . ( PI / 2)))) by Th73

 .= ( - 1) by A1, A2, A3;



 thus ( cos . (2 * PI )) = ( cos . ( PI + PI ))

 .= ((( - 1) * ( - 1)) - (( sin . PI ) * ( sin . PI ))) by A3, Th73

 .= 1 by A4;



 thus ( sin . (2 * PI )) = ( sin . ( PI + PI ))

 .= ((( sin . PI ) * ( cos . PI )) + (( cos . PI ) * ( sin . PI ))) by Th73

 .= 0 by A4;

 end;

 theorem :: SIN_COS:77

 ( cos ( PI / 2)) = 0 & ( sin ( PI / 2)) = 1 & ( cos PI ) = ( - 1) & ( sin PI ) = 0 & ( cos ( PI + ( PI / 2))) = 0 & ( sin ( PI + ( PI / 2))) = ( - 1) & ( cos (2 * PI )) = 1 & ( sin (2 * PI )) = 0 by Th75;

 theorem :: SIN_COS:78



 Th77: ( sin . (th + (2 * PI ))) = ( sin . th) & ( cos . (th + (2 * PI ))) = ( cos . th) & ( sin . (( PI / 2) - th)) = ( cos . th) & ( cos . (( PI / 2) - th)) = ( sin . th) & ( sin . (( PI / 2) + th)) = ( cos . th) & ( cos . (( PI / 2) + th)) = ( - ( sin . th)) & ( sin . ( PI + th)) = ( - ( sin . th)) & ( cos . ( PI + th)) = ( - ( cos . th))

 proof



 thus ( sin . (th + (2 * PI ))) = ((( sin . th) * 1) + (( cos . th) * 0 )) by Th73, Th75

 .= ( sin . th);



 thus ( cos . (th + (2 * PI ))) = ((( cos . th) * 1) - (( sin . th) * 0 )) by Th73, Th75

 .= ( cos . th);



 thus ( sin . (( PI / 2) - th)) = ((( sin . ( PI / 2)) * ( cos . ( - th))) + (( cos . ( PI / 2)) * ( sin . ( - th)))) by Th73

 .= ( cos . th) by Th30, Th75;



 thus ( cos . (( PI / 2) - th)) = ((( cos . ( PI / 2)) * ( cos . ( - th))) - (( sin . ( PI / 2)) * ( sin . ( - th)))) by Th73

 .= ( 0 - (1 * ( - ( sin . th)))) by Th30, Th75

 .= ( sin . th);



 thus ( sin . (( PI / 2) + th)) = ((1 * ( cos . th)) + ( 0 * ( sin . th))) by Th73, Th75

 .= ( cos . th);



 thus ( cos . (( PI / 2) + th)) = ((( cos . ( PI / 2)) * ( cos . th)) - (( sin . ( PI / 2)) * ( sin . th))) by Th73

 .= ( - ( sin . th)) by Th75;



 thus ( sin . ( PI + th)) = ((( sin . PI ) * ( cos . th)) + (( cos . PI ) * ( sin . th))) by Th73

 .= ( - ( sin . th)) by Th75;



 thus ( cos . ( PI + th)) = ((( - 1) * ( cos . th)) - ( 0 * ( sin . th))) by Th73, Th75

 .= ( - ( cos . th));

 end;

 theorem :: SIN_COS:79

 ( sin (th + (2 * PI ))) = ( sin th) & ( cos (th + (2 * PI ))) = ( cos th) & ( sin (( PI / 2) - th)) = ( cos th) & ( cos (( PI / 2) - th)) = ( sin th) & ( sin (( PI / 2) + th)) = ( cos th) & ( cos (( PI / 2) + th)) = ( - ( sin th)) & ( sin ( PI + th)) = ( - ( sin th)) & ( cos ( PI + th)) = ( - ( cos th)) by Th77;



 Lm17: th in [. 0 , 1.] implies ( sin . th) >= 0

 proof

 assume

 A1: th in [. 0 , 1.];

 then

 A2: th <= 1 by XXREAL_1: 1;

 ( sin . th) >= ( sin . 0 )

 proof

 now

 per cases by A1, XXREAL_1: 1;

 suppose th = 0 ;

 hence thesis;

 end;

 suppose

 A3: 0 < th;

 ( sin | REAL ) is continuous by Th67, FDIFF_1: 25;

 then ( sin | [. 0 , th.]) is continuous by FCONT_1: 16;

 then

 consider r such that

 A4: r in ]. 0 , th.[ and

 A5: ( diff ( sin ,r)) = ((( sin . th) - ( sin . 0 )) / (th - 0 )) by A3, Th24, Th67, FDIFF_1: 26, ROLLE: 3;



 A6: r < th by A4, XXREAL_1: 4;



 A7: 0 < r by A4, XXREAL_1: 4;

 r < 1 by A2, A6, XXREAL_0: 2;

 then r in [. 0 , 1.] by A7, XXREAL_1: 1;

 then ( cos . r) > 0 by Th68;

 then (( sin . th) - ( sin . 0 )) > 0 by A3, A5, Th67;

 hence thesis by XREAL_1: 47;

 end;

 end;

 hence thesis;

 end;

 hence thesis by Th30;

 end;

 theorem :: SIN_COS:80



 Th79: th in ]. 0 , ( PI / 2).[ implies ( cos . th) > 0

 proof

 assume that

 A1: th in ]. 0 , ( PI / 2).[ and

 A2: ( cos . th) <= 0 ;

 ( cos | REAL ) is continuous by Th66, FDIFF_1: 25;

 then

 A3: ( cos | [. 0 , th.]) is continuous by FCONT_1: 16;



 A4: 0 < th by A1, XXREAL_1: 4;

 ( [.( cos . 0 ), ( cos . th).] \/ [.( cos . th), ( cos . 0 ).]) = [.( cos . th), ( cos . 0 ).] & 0 in [.( cos . th), ( cos . 0 ).] by A2, Th30, XXREAL_1: 1, XXREAL_1: 222;

 then ex th2 st th2 in [. 0 , th.] & ( cos . th2) = 0 by A3, A4, Th24, FCONT_2: 15;

 then

 consider th2 be Real such that

 A5: th2 in [. 0 , th.] and 0 < th and

 A6: ( cos . th2) = 0 by A4;



 A7: 0 <= th2 by A5, XXREAL_1: 1;



 A8: th2 <= th by A5, XXREAL_1: 1;



 A9: th < ( PI / 2) by A1, XXREAL_1: 4;



 A10: 0 < th2 by A6, A7, Th30;

 th2 < ( PI / 2) by A8, A9, XXREAL_0: 2;

 then

 A11: (th2 / 2) < (( PI / 2) / 2) by XREAL_1: 74;

 PI in ]. 0 , 4.[ by Def28;

 then PI < 4 by XXREAL_1: 4;

 then ( PI / 4) < (4 / 4) by XREAL_1: 74;

 then

 A12: (th2 / 2) < 1 by A11, XXREAL_0: 2;

 0 = ( cos . ((th2 / 2) + (th2 / 2))) by A6

 .= ((( cos . (th2 / 2)) ^2 ) - (( sin . (th2 / 2)) * ( sin . (th2 / 2)))) by Th73

 .= ((( cos . (th2 / 2)) - ( sin . (th2 / 2))) * (( cos . (th2 / 2)) + ( sin . (th2 / 2))));

 then

 A13: (( cos . (th2 / 2)) - ( sin . (th2 / 2))) = 0 or (( cos . (th2 / 2)) + ( sin . (th2 / 2))) = 0 ;



 A14: (th2 / 2) in ]. 0 , 1.[ by A10, A12, XXREAL_1: 4;

 ]. 0 , 1.[ c= [. 0 , 1.] by XXREAL_1: 25;

 then

 A15: ( cos . (th2 / 2)) > 0 & ( sin . (th2 / 2)) >= ( - 0 ) by A14, Lm17, Th68;

 (4 * (th2 / 2)) < (4 * 1) by A12, XREAL_1: 68;

 then

 A16: (2 * th2) in ]. 0 , 4.[ by A10, XXREAL_1: 4;

 (( sin . (th2 / 2)) * (( cos . (th2 / 2)) " )) = 1 by A13, A15, XCMPLX_0:def 7;

 then ( tan . ((2 * th2) / 4)) = 1 by A14, Th69, RFUNCT_1:def 1;

 then (2 * th2) = PI by A16, Def28;

 hence contradiction by A1, A8, XXREAL_1: 4;

 end;

 theorem :: SIN_COS:81

 th in ]. 0 , ( PI / 2).[ implies ( cos th) > 0 by Th79;

 begin

 theorem :: SIN_COS:82

 ( sin (a - b)) = ((( sin a) * ( cos b)) - (( cos a) * ( sin b)))

 proof



 thus ( sin (a - b)) = ((( sin . a) * ( cos . ( - b))) + (( cos . a) * ( sin . ( - b)))) by Th73

 .= ((( sin . a) * ( cos . b)) + (( cos . a) * ( sin . ( - b)))) by Th30

 .= ((( sin . a) * ( cos . b)) + (( cos . a) * ( - ( sin . b)))) by Th30

 .= ((( sin a) * ( cos b)) - (( cos a) * ( sin b)));

 end;

 theorem :: SIN_COS:83

 ( cos (a - b)) = ((( cos a) * ( cos b)) + (( sin a) * ( sin b)))

 proof



 thus ( cos (a - b)) = ((( cos . a) * ( cos . ( - b))) - (( sin . a) * ( sin . ( - b)))) by Th73

 .= ((( cos . a) * ( cos . b)) - (( sin . a) * ( sin . ( - b)))) by Th30

 .= ((( cos . a) * ( cos . b)) - (( sin . a) * ( - ( sin . b)))) by Th30

 .= ((( cos a) * ( cos b)) + (( sin a) * ( sin b)));

 end;

 registration

 cluster sin -> continuous;

 coherence

 proof

 ( dom sin ) = REAL & ( sin | REAL ) is continuous by Th67, FDIFF_1: 25, FUNCT_2:def 1;

 hence thesis by RELAT_1: 69;

 end;

 cluster cos -> continuous;

 coherence

 proof

 ( dom cos ) = REAL & ( cos | REAL ) is continuous by Th66, FDIFF_1: 25, FUNCT_2:def 1;

 hence thesis by RELAT_1: 69;

 end;

 cluster exp_R -> continuous;

 coherence

 proof

 ( dom exp_R ) = REAL & ( exp_R | REAL ) is continuous by Th65, FDIFF_1: 25, FUNCT_2:def 1;

 hence thesis by RELAT_1: 69;

 end;

 end