let n be Nat; for Z being open Subset of REAL st Z c= dom ((#Z n) * tan) & 1 <= n holds
( (#Z n) * tan is_differentiable_on Z & ( for x being Real st x in Z holds
(((#Z n) * tan) `| Z) . x = (n * ((sin . x) #Z (n - 1))) / ((cos . x) #Z (n + 1)) ) )
let Z be open Subset of REAL; ( Z c= dom ((#Z n) * tan) & 1 <= n implies ( (#Z n) * tan is_differentiable_on Z & ( for x being Real st x in Z holds
(((#Z n) * tan) `| Z) . x = (n * ((sin . x) #Z (n - 1))) / ((cos . x) #Z (n + 1)) ) ) )
assume that
A1:
Z c= dom ((#Z n) * tan)
and
A2:
1 <= n
; ( (#Z n) * tan is_differentiable_on Z & ( for x being Real st x in Z holds
(((#Z n) * tan) `| Z) . x = (n * ((sin . x) #Z (n - 1))) / ((cos . x) #Z (n + 1)) ) )
A3:
dom ((#Z n) * tan) c= dom tan
by RELAT_1:25;
A4:
for x being Real st x in Z holds
cos . x <> 0
A5:
for x being Real st x in Z holds
(#Z n) * tan is_differentiable_in x
then A6:
(#Z n) * tan is_differentiable_on Z
by A1, FDIFF_1:9;
for x being Real st x in Z holds
(((#Z n) * tan) `| Z) . x = (n * ((sin . x) #Z (n - 1))) / ((cos . x) #Z (n + 1))
proof
set m =
n - 1;
let x be
Real;
( x in Z implies (((#Z n) * tan) `| Z) . x = (n * ((sin . x) #Z (n - 1))) / ((cos . x) #Z (n + 1)) )
A7:
ex
m being
Nat st
n = m + 1
by A2, NAT_1:6;
assume A8:
x in Z
;
(((#Z n) * tan) `| Z) . x = (n * ((sin . x) #Z (n - 1))) / ((cos . x) #Z (n + 1))
then A9:
cos . x <> 0
by A4;
then A10:
tan is_differentiable_in x
by FDIFF_7:46;
(((#Z n) * tan) `| Z) . x =
diff (
((#Z n) * tan),
x)
by A6, A8, FDIFF_1:def 7
.=
(n * ((tan . x) #Z (n - 1))) * (diff (tan,x))
by A10, TAYLOR_1:3
.=
(n * ((tan . x) #Z (n - 1))) * (1 / ((cos . x) ^2))
by A9, FDIFF_7:46
.=
(n * (((sin . x) #Z (n - 1)) / ((cos . x) #Z (n - 1)))) / ((cos . x) ^2)
by A1, A3, A8, A7, Th3, XBOOLE_1:1
.=
((n * ((sin . x) #Z (n - 1))) / ((cos . x) #Z (n - 1))) / ((cos . x) ^2)
.=
(n * ((sin . x) #Z (n - 1))) / (((cos . x) #Z (n - 1)) * ((cos . x) ^2))
by XCMPLX_1:78
.=
(n * ((sin . x) #Z (n - 1))) / (((cos . x) #Z (n - 1)) * ((cos . x) #Z 2))
by FDIFF_7:1
.=
(n * ((sin . x) #Z (n - 1))) / ((cos . x) #Z ((n - 1) + 2))
by A4, A8, PREPOWER:44
.=
(n * ((sin . x) #Z (n - 1))) / ((cos . x) #Z (n + 1))
;
hence
(((#Z n) * tan) `| Z) . x = (n * ((sin . x) #Z (n - 1))) / ((cos . x) #Z (n + 1))
;
verum
end;
hence
( (#Z n) * tan is_differentiable_on Z & ( for x being Real st x in Z holds
(((#Z n) * tan) `| Z) . x = (n * ((sin . x) #Z (n - 1))) / ((cos . x) #Z (n + 1)) ) )
by A1, A5, FDIFF_1:9; verum