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