let p be real number ; :: thesis: ( cos is_differentiable_in p & diff cos ,p = - (sin . p) )
reconsider p = p as Real by XREAL_0:def 1;
deffunc H₂( Element of REAL ) -> Element of REAL = - ($1 * (Im ((Sum (($1 * <i> ) P_dt )) * ((cos . p) + ((sin . p) * <i> )))));
consider Cr being Function of REAL ,REAL such that
A2: for th being Real holds Cr . th = H₂(th) from FUNCT_2:sch 4();
Cr is REST-like

proof

for hy1 being convergent_to_0 Real_Sequence holds
( (hy1 " ) (#) (Cr /* hy1) is convergent & lim ((hy1 " ) (#) (Cr /* hy1)) = 0 )

proof

let hy1 be convergent_to_0 Real_Sequence; :: thesis: ( (hy1 " ) (#) (Cr /* hy1) is convergent & lim ((hy1 " ) (#) (Cr /* hy1)) = 0 )
A7: for n being Element of NAT holds ((hy1 " ) (#) (Cr /* hy1)) . n = - (Im ((Sum (((hy1 . n) * <i> ) P_dt )) * ((cos . p) + ((sin . p) * <i> ))))

proof

let n be Element of NAT ; :: thesis: ((hy1 " ) (#) (Cr /* hy1)) . n = - (Im ((Sum (((hy1 . n) * <i> ) P_dt )) * ((cos . p) + ((sin . p) * <i> ))))
A8: ((hy1 " ) (#) (Cr /* hy1)) . n = ((hy1 " ) . n) * ((Cr /* hy1) . n) by SEQ_1:12
.= ((hy1 . n) " ) * ((Cr /* hy1) . n) by VALUED_1:10 ;
dom Cr = REAL by FUNCT_2:def 1;
then rng hy1 c= dom Cr ;
then A9: ((hy1 " ) (#) (Cr /* hy1)) . n = ((hy1 . n) " ) * (Cr . (hy1 . n)) by A8, FUNCT_2:185
.= ((hy1 . n) " ) * (- ((hy1 . n) * (Im ((Sum (((hy1 . n) * <i> ) P_dt )) * ((cos . p) + ((sin . p) * <i> )))))) by A2
.= - ((((hy1 . n) " ) * (hy1 . n)) * (Im ((Sum (((hy1 . n) * <i> ) P_dt )) * ((cos . p) + ((sin . p) * <i> ))))) ;
hy1 is non-zero by FDIFF_1:def 1;
then hy1 . n <> 0 by SEQ_1:7;
then ((hy1 " ) (#) (Cr /* hy1)) . n = - (1 * (Im ((Sum (((hy1 . n) * <i> ) P_dt )) * ((cos . p) + ((sin . p) * <i> ))))) by A9, XCMPLX_0:def 7
.= - (Im ((Sum (((hy1 . n) * <i> ) P_dt )) * ((cos . p) + ((sin . p) * <i> )))) ;
hence ((hy1 " ) (#) (Cr /* hy1)) . n = - (Im ((Sum (((hy1 . n) * <i> ) P_dt )) * ((cos . p) + ((sin . p) * <i> )))) ; :: thesis: verum

end;

deffunc H₃( Real) -> Element of REAL = - (Im ((Sum (((hy1 . $1) * <i> ) P_dt )) * ((cos . p) + ((sin . p) * <i> ))));
consider rseq being Real_Sequence such that
A10: for n being Element of NAT holds rseq . n = H₃(n) from SEQ_1:sch 1();
deffunc H₄( Element of NAT ) -> Element of COMPLEX = (Sum (((hy1 . $1) * <i> ) P_dt )) * ((cos . p) + ((sin . p) * <i> ));
consider cq1 being Complex_Sequence such that
A11: for n being Element of NAT holds cq1 . n = H₄(n) from COMSEQ_1:sch 1();
A12: ( cq1 is convergent & lim cq1 = 0c )

proof

A13: for q being Real st q > 0 holds
ex k being Element of NAT st
for m being Element of NAT st k <= m holds
|.((cq1 . m) - 0c ).| < q

proof

let q be Real; :: thesis: ( q > 0 implies ex k being Element of NAT st
for m being Element of NAT st k <= m holds
|.((cq1 . m) - 0c ).| < q )
assume A14: q > 0 ; :: thesis: ex k being Element of NAT st
for m being Element of NAT st k <= m holds
|.((cq1 . m) - 0c ).| < q
ex k being Element of NAT st
for m being Element of NAT st k <= m holds
|.((cq1 . m) - 0c ).| < q

proof

consider r being Real such that
A15: ( r > 0 & ( for z being complex number st |.z.| < r holds
|.(Sum (z P_dt )).| < q ) ) by A14, Th63;
( hy1 is convergent & lim hy1 = 0 ) by FDIFF_1:def 1;
then consider k being Element of NAT such that
A16: for m being Element of NAT st k <= m holds
abs ((hy1 . m) - 0 ) < r by A15, SEQ_2:def 7;

A17: now

let m be Element of NAT ; :: thesis: ( k <= m implies |.((cq1 . m) - 0c ).| < q )
assume A18: k <= m ; :: thesis: |.((cq1 . m) - 0c ).| < q
A19: |.((cq1 . m) - 0c ).| = |.((Sum (((hy1 . m) * <i> ) P_dt )) * ((cos . p) + ((sin . p) * <i> ))).| by A11
.= |.(Sum (((hy1 . m) * <i> ) P_dt )).| * |.((cos . p) + ((sin . p) * <i> )).| by COMPLEX1:151
.= |.(Sum (((hy1 . m) * <i> ) P_dt )).| * |.(Sum ((p * <i> ) ExpSeq )).| by Lm3
.= |.(Sum (((hy1 . m) * <i> ) P_dt )).| * 1 by Lm5
.= |.(Sum (((hy1 . m) * <i> ) P_dt )).| ;
A20: abs ((hy1 . m) - 0 ) < r by A16, A18;
(hy1 . m) * <i> = 0 + ((hy1 . m) * <i> ) ;
then ( Re ((hy1 . m) * <i> ) = 0 & Im ((hy1 . m) * <i> ) = hy1 . m ) by COMPLEX1:28;
then |.((hy1 . m) * <i> ).| = abs (hy1 . m) by COMPLEX1:158;
hence |.((cq1 . m) - 0c ).| < q by A15, A19, A20; :: thesis: verum

end;

take k ; :: thesis: for m being Element of NAT st k <= m holds
|.((cq1 . m) - 0c ).| < q
thus for m being Element of NAT st k <= m holds
|.((cq1 . m) - 0c ).| < q by A17; :: thesis: verum

end;

hence ex k being Element of NAT st
for m being Element of NAT st k <= m holds
|.((cq1 . m) - 0c ).| < q ; :: thesis: verum

end;

then cq1 is convergent by COMSEQ_2:def 4;
hence ( cq1 is convergent & lim cq1 = 0c ) by A13, COMSEQ_2:def 5; :: thesis: verum

end;

A22: lim (- cq1) = - 0c by A12, COMSEQ_2:22;
A23: for n being Element of NAT holds (Im (- cq1)) . n = rseq . n

proof

A24: for n being Element of NAT holds (Im (- cq1)) . n = - (Im ((Sum (((hy1 . n) * <i> ) P_dt )) * ((cos . p) + ((sin . p) * <i> ))))

proof

let n be Element of NAT ; :: thesis: (Im (- cq1)) . n = - (Im ((Sum (((hy1 . n) * <i> ) P_dt )) * ((cos . p) + ((sin . p) * <i> ))))
(Im (- cq1)) . n = Im ((- cq1) . n) by COMSEQ_3:def 4
.= Im (- (cq1 . n)) by VALUED_1:8
.= Im (- ((Sum (((hy1 . n) * <i> ) P_dt )) * ((cos . p) + ((sin . p) * <i> )))) by A11
.= - (Im ((Sum (((hy1 . n) * <i> ) P_dt )) * ((cos . p) + ((sin . p) * <i> )))) by COMPLEX1:34 ;
hence (Im (- cq1)) . n = - (Im ((Sum (((hy1 . n) * <i> ) P_dt )) * ((cos . p) + ((sin . p) * <i> )))) ; :: thesis: verum

end;

let n be Element of NAT ; :: thesis: (Im (- cq1)) . n = rseq . n
rseq . n = - (Im ((Sum (((hy1 . n) * <i> ) P_dt )) * ((cos . p) + ((sin . p) * <i> )))) by A10;
hence (Im (- cq1)) . n = rseq . n by A24; :: thesis: verum

end;

rseq = (hy1 " ) (#) (Cr /* hy1)

proof

for n being Element of NAT holds rseq . n = ((hy1 " ) (#) (Cr /* hy1)) . n

proof

let n be Element of NAT ; :: thesis: rseq . n = ((hy1 " ) (#) (Cr /* hy1)) . n
rseq . n = - (Im ((Sum (((hy1 . n) * <i> ) P_dt )) * ((cos . p) + ((sin . p) * <i> )))) by A10;
hence rseq . n = ((hy1 " ) (#) (Cr /* hy1)) . n by A7; :: thesis: verum

end;

hence rseq = (hy1 " ) (#) (Cr /* hy1) by FUNCT_2:113; :: thesis: verum

end;

then (hy1 " ) (#) (Cr /* hy1) = Im (- cq1) by A23, FUNCT_2:113;
hence ( (hy1 " ) (#) (Cr /* hy1) is convergent & lim ((hy1 " ) (#) (Cr /* hy1)) = 0 ) by A12, A22, COMPLEX1:12, COMSEQ_3:41; :: thesis: verum

end;

hence Cr is REST-like by FDIFF_1:def 3; :: thesis: verum

end;

then reconsider PR = Cr as REST ;
deffunc H₃( Element of REAL ) -> Element of REAL = - ($1 * (sin . p));
consider CL being Function of REAL ,REAL such that
A26: for th being Real holds CL . th = H₃(th) from FUNCT_2:sch 4();
CL is linear

proof

ex r being Real st
for q being Real holds CL . q = r * q

proof

A30: for q being Real holds CL . q = (- (sin . p)) * q

proof

let q be Real; :: thesis: CL . q = (- (sin . p)) * q
CL . q = - (q * (sin . p)) by A26
.= (- (sin . p)) * q ;
hence CL . q = (- (sin . p)) * q ; :: thesis: verum

end;

take - (sin . p) ; :: thesis: for q being Real holds CL . q = (- (sin . p)) * q
thus for q being Real holds CL . q = (- (sin . p)) * q by A30; :: thesis: verum

end;

hence CL is linear by FDIFF_1:def 4; :: thesis: verum

end;

then reconsider PL = CL as LINEAR ;
A31: ex N being Neighbourhood of p st
( N c= dom cos & ( for r being Real st r in N holds
(cos . r) - (cos . p) = (PL . (r - p)) + (PR . (r - p)) ) )

proof

A32: for r being Real st r in ].(p - 1),(p + 1).[ holds
(cos . r) - (cos . p) = (PL . (r - p)) + (PR . (r - p))

proof

let r be Real; :: thesis: ( r in ].(p - 1),(p + 1).[ implies (cos . r) - (cos . p) = (PL . (r - p)) + (PR . (r - p)) )
r = p + (r - p) ;
then (cos . r) - (cos . p) = (- ((r - p) * (sin . p))) - ((r - p) * (Im ((Sum (((r - p) * <i> ) P_dt )) * ((cos . p) + ((sin . p) * <i> ))))) by Th65
.= (- ((r - p) * (sin . p))) + (Cr . (r - p)) by A2
.= (PL . (r - p)) + (PR . (r - p)) by A26 ;
hence ( r in ].(p - 1),(p + 1).[ implies (cos . r) - (cos . p) = (PL . (r - p)) + (PR . (r - p)) ) ; :: thesis: verum

end;

take ].(p - 1),(p + 1).[ ; :: thesis: ( ].(p - 1),(p + 1).[ is Neighbourhood of p & ].(p - 1),(p + 1).[ c= dom cos & ( for r being Real st r in ].(p - 1),(p + 1).[ holds
(cos . r) - (cos . p) = (PL . (r - p)) + (PR . (r - p)) ) )
thus ( ].(p - 1),(p + 1).[ is Neighbourhood of p & ].(p - 1),(p + 1).[ c= dom cos & ( for r being Real st r in ].(p - 1),(p + 1).[ holds
(cos . r) - (cos . p) = (PL . (r - p)) + (PR . (r - p)) ) ) by A32, Th27, RCOMP_1:def 7; :: thesis: verum

end;

then A33: cos is_differentiable_in p by FDIFF_1:def 5;
PL . 1 = - (1 * (sin . p)) by A26
.= - (sin . p) ;
hence ( cos is_differentiable_in p & diff cos ,p = - (sin . p) ) by A31, A33, FDIFF_1:def 6; :: thesis: verum