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:
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
.= 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
.= 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 ;
then A6: sin | Z is_differentiable_in x by ;
(diff (sin,Z)) . i = ((- 1) |^ j) (#) (sin | Z) by ;
hence (diff (sin,Z)) . i is_differentiable_in x by ; :: 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 ;
then A8: cos | Z is_differentiable_in x by ;
(diff (sin,Z)) . i = ((- 1) |^ j) (#) (cos | Z) by ;
hence (diff (sin,Z)) . i is_differentiable_in x by ; :: thesis: verum
end;
end;
end;
hence ((diff (sin,Z)) . i) | Z is_differentiable_in x by ; :: thesis: verum
end;
hence (diff (sin,Z)) . i is_differentiable_on Z by ; :: thesis: verum
end;
hence sin is_differentiable_on n,Z ; :: thesis:
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
.= 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
.= 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 ;
then A14: cos | Z is_differentiable_in x by ;
(diff (cos,Z)) . i = ((- 1) |^ j) (#) (cos | Z) by ;
hence (diff (cos,Z)) . i is_differentiable_in x by ; :: 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 ;
then A16: sin | Z is_differentiable_in x by ;
(diff (cos,Z)) . i = ((- 1) |^ (j + 1)) (#) (sin | Z) by ;
hence (diff (cos,Z)) . i is_differentiable_in x by ; :: thesis: verum
end;
end;
end;
hence ((diff (cos,Z)) . i) | Z is_differentiable_in x by ; :: thesis: verum
end;
hence (diff (cos,Z)) . i is_differentiable_on Z by ; :: thesis: verum
end;
hence cos is_differentiable_on n,Z ; :: thesis: verum