let Z be open Subset of REAL; ( Z c= dom (tan - (id Z)) implies ( tan - (id Z) is_differentiable_on Z & ( for x being Real st x in Z holds
((tan - (id Z)) `| Z) . x = (tan . x) ^2 ) ) )
A1:
for x being Real st x in Z holds
(id Z) . x = (1 * x) + 0
by FUNCT_1:18;
assume A2:
Z c= dom (tan - (id Z))
; ( tan - (id Z) is_differentiable_on Z & ( for x being Real st x in Z holds
((tan - (id Z)) `| Z) . x = (tan . x) ^2 ) )
then
Z c= (dom tan) /\ (dom (id Z))
by VALUED_1:12;
then A3:
Z c= dom tan
by XBOOLE_1:18;
A4:
Z c= dom (id Z)
;
then A5:
id Z is_differentiable_on Z
by A1, FDIFF_1:23;
for x being Real st x in Z holds
tan is_differentiable_in x
then A6:
tan is_differentiable_on Z
by A3, FDIFF_1:9;
for x being Real st x in Z holds
((tan - (id Z)) `| Z) . x = (tan . x) ^2
proof
let x be
Real;
( x in Z implies ((tan - (id Z)) `| Z) . x = (tan . x) ^2 )
assume A7:
x in Z
;
((tan - (id Z)) `| Z) . x = (tan . x) ^2
then A8:
cos . x <> 0
by A3, FDIFF_8:1;
then A9:
(cos . x) ^2 > 0
by SQUARE_1:12;
((tan - (id Z)) `| Z) . x =
(diff (tan,x)) - (diff ((id Z),x))
by A2, A5, A6, A7, FDIFF_1:19
.=
(1 / ((cos . x) ^2)) - (diff ((id Z),x))
by A8, FDIFF_7:46
.=
(1 / ((cos . x) ^2)) - (((id Z) `| Z) . x)
by A5, A7, FDIFF_1:def 7
.=
(1 / ((cos . x) ^2)) - 1
by A4, A1, A7, FDIFF_1:23
.=
(1 / ((cos . x) ^2)) - (((cos . x) ^2) / ((cos . x) ^2))
by A9, XCMPLX_1:60
.=
(1 - ((cos . x) ^2)) / ((cos . x) ^2)
by XCMPLX_1:120
.=
((((sin . x) ^2) + ((cos . x) ^2)) - ((cos . x) ^2)) / ((cos . x) ^2)
by SIN_COS:28
.=
((sin x) / (cos x)) * ((sin . x) / (cos . x))
by XCMPLX_1:76
.=
(tan . x) * (tan x)
by A3, A7, FDIFF_8:1, SIN_COS9:15
.=
(tan . x) ^2
by A3, A7, FDIFF_8:1, SIN_COS9:15
;
hence
((tan - (id Z)) `| Z) . x = (tan . x) ^2
;
verum
end;
hence
( tan - (id Z) is_differentiable_on Z & ( for x being Real st x in Z holds
((tan - (id Z)) `| Z) . x = (tan . x) ^2 ) )
by A2, A5, A6, FDIFF_1:19; verum