let Z be open Subset of REAL; :: thesis: for n being Element of NAT holds
( sin is_differentiable_on n,Z & cos is_differentiable_on n,Z )
let n be Element of NAT ; :: thesis: ( sin is_differentiable_on n,Z & cos is_differentiable_on n,Z )

now :: thesis: for i being Nat st i <= n - 1 holds
(diff (sin,Z)) . i is_differentiable_on Z

let i be Nat; :: thesis: ( i <= n - 1 implies (diff (sin,Z)) . i is_differentiable_on Z )
assume i <= n - 1 ; :: thesis: (diff (sin,Z)) . i is_differentiable_on Z

A1: now :: thesis: dom ((diff (sin,Z)) . i) = Z

per cases ( i is even or i is odd ) ;

suppose i is even ; :: thesis: dom ((diff (sin,Z)) . i) = Z

then consider j being Nat such that
A2: i = 2 * j by ABIAN:def 2;
thus dom ((diff (sin,Z)) . i) = dom (((- 1) |^ j) (#) (sin | Z)) by A2, Th19
.= dom (sin | Z) by VALUED_1:def 5
.= Z by Th17 ; :: thesis: verum

end;

suppose i is odd ; :: thesis: dom ((diff (sin,Z)) . i) = Z

then consider j being Nat such that
A3: i = (2 * j) + 1 by ABIAN:9;
thus dom ((diff (sin,Z)) . i) = dom (((- 1) |^ j) (#) (cos | Z)) by A3, Th19
.= dom (cos | Z) by VALUED_1:def 5
.= Z by Th17 ; :: thesis: verum

end;

end;

end;

for x being Real st x in Z holds
((diff (sin,Z)) . i) | Z is_differentiable_in x

proof

let x be Real; :: thesis: ( x in Z implies ((diff (sin,Z)) . i) | Z is_differentiable_in x )
assume A4: x in Z ; :: thesis: ((diff (sin,Z)) . i) | Z is_differentiable_in x

now :: thesis: (diff (sin,Z)) . i is_differentiable_in x

per cases ( i is even or i is odd ) ;

suppose i is even ; :: thesis: (diff (sin,Z)) . i is_differentiable_in x

then consider j being Nat such that
A5: i = 2 * j by ABIAN:def 2;
sin is_differentiable_on Z by FDIFF_1:26, SIN_COS:68;
then A6: sin | Z is_differentiable_in x by A4, FDIFF_1:def 6;
(diff (sin,Z)) . i = ((- 1) |^ j) (#) (sin | Z) by A5, Th19;
hence (diff (sin,Z)) . i is_differentiable_in x by A6, FDIFF_1:15; :: thesis: verum

end;

suppose i is odd ; :: thesis: (diff (sin,Z)) . i is_differentiable_in x

then consider j being Nat such that
A7: i = (2 * j) + 1 by ABIAN:9;
cos is_differentiable_on Z by FDIFF_1:26, SIN_COS:67;
then A8: cos | Z is_differentiable_in x by A4, FDIFF_1:def 6;
(diff (sin,Z)) . i = ((- 1) |^ j) (#) (cos | Z) by A7, Th19;
hence (diff (sin,Z)) . i is_differentiable_in x by A8, FDIFF_1:15; :: thesis: verum

end;

end;

end;

hence ((diff (sin,Z)) . i) | Z is_differentiable_in x by A1, RELAT_1:68; :: thesis: verum

end;

hence (diff (sin,Z)) . i is_differentiable_on Z by A1, FDIFF_1:def 6; :: thesis: verum

end;

hence sin is_differentiable_on n,Z ; :: thesis: cos is_differentiable_on n,Z

now :: thesis: for i being Nat st i <= n - 1 holds
(diff (cos,Z)) . i is_differentiable_on Z

let i be Nat; :: thesis: ( i <= n - 1 implies (diff (cos,Z)) . i is_differentiable_on Z )
assume i <= n - 1 ; :: thesis: (diff (cos,Z)) . i is_differentiable_on Z

A9: now :: thesis: dom ((diff (cos,Z)) . i) = Z

per cases ( i is even or i is odd ) ;

suppose i is even ; :: thesis: dom ((diff (cos,Z)) . i) = Z

then consider j being Nat such that
A10: i = 2 * j by ABIAN:def 2;
thus dom ((diff (cos,Z)) . i) = dom (((- 1) |^ j) (#) (cos | Z)) by A10, Th19
.= dom (cos | Z) by VALUED_1:def 5
.= Z by Th17 ; :: thesis: verum

end;

suppose i is odd ; :: thesis: dom ((diff (cos,Z)) . i) = Z

then consider j being Nat such that
A11: i = (2 * j) + 1 by ABIAN:9;
thus dom ((diff (cos,Z)) . i) = dom (((- 1) |^ (j + 1)) (#) (sin | Z)) by A11, Th19
.= dom (sin | Z) by VALUED_1:def 5
.= Z by Th17 ; :: thesis: verum

end;

end;

end;

for x being Real st x in Z holds
((diff (cos,Z)) . i) | Z is_differentiable_in x

proof

let x be Real; :: thesis: ( x in Z implies ((diff (cos,Z)) . i) | Z is_differentiable_in x )
assume A12: x in Z ; :: thesis: ((diff (cos,Z)) . i) | Z is_differentiable_in x

now :: thesis: (diff (cos,Z)) . i is_differentiable_in x

per cases ( i is even or i is odd ) ;

suppose i is even ; :: thesis: (diff (cos,Z)) . i is_differentiable_in x

then consider j being Nat such that
A13: i = 2 * j by ABIAN:def 2;
cos is_differentiable_on Z by FDIFF_1:26, SIN_COS:67;
then A14: cos | Z is_differentiable_in x by A12, FDIFF_1:def 6;
(diff (cos,Z)) . i = ((- 1) |^ j) (#) (cos | Z) by A13, Th19;
hence (diff (cos,Z)) . i is_differentiable_in x by A14, FDIFF_1:15; :: thesis: verum

end;

suppose i is odd ; :: thesis: (diff (cos,Z)) . i is_differentiable_in x

then consider j being Nat such that
A15: i = (2 * j) + 1 by ABIAN:9;
sin is_differentiable_on Z by FDIFF_1:26, SIN_COS:68;
then A16: sin | Z is_differentiable_in x by A12, FDIFF_1:def 6;
(diff (cos,Z)) . i = ((- 1) |^ (j + 1)) (#) (sin | Z) by A15, Th19;
hence (diff (cos,Z)) . i is_differentiable_in x by A16, FDIFF_1:15; :: thesis: verum

end;

end;

end;

hence ((diff (cos,Z)) . i) | Z is_differentiable_in x by A9, RELAT_1:68; :: thesis: verum

end;

hence (diff (cos,Z)) . i is_differentiable_on Z by A9, FDIFF_1:def 6; :: thesis: verum

end;

hence cos is_differentiable_on n,Z ; :: thesis: verum