A1:
( sin is_differentiable_on ].0,1.[ & cos is_differentiable_on ].0,1.[ )
by Th66, Th67, FDIFF_1:26;
A2:
for th being Real st th in ].0,1.[ holds
cos . th <> 0
for th being Real st th in ].0,1.[ holds
diff (tan,th) > 0
proof
let th be
Real;
( th in ].0,1.[ implies diff (tan,th) > 0 )
assume A4:
th in ].0,1.[
;
diff (tan,th) > 0
A5:
(
th is
Real &
cos is_differentiable_in th )
by Th62;
A6:
sin is_differentiable_in th
by Th63;
A7:
cos . th <> 0
by A2, A4;
then A8:
diff (
tan,
th) =
(((diff (sin,th)) * (cos . th)) - ((diff (cos,th)) * (sin . th))) / ((cos . th) ^2)
by A5, A6, FDIFF_2:14
.=
(((cos . th) * (cos . th)) - ((diff (cos,th)) * (sin . th))) / ((cos . th) ^2)
by Th63
.=
(((cos . th) * (cos . th)) - ((- (sin . th)) * (sin . th))) / ((cos . th) ^2)
by Th62
.=
(((cos . th) ^2) + ((sin . th) * (sin . th))) / ((cos . th) ^2)
.=
1
/ ((cos . th) ^2)
by Th28
;
(cos . th) ^2 > 0
by A7, SQUARE_1:12;
hence
diff (
tan,
th)
> 0
by A8;
verum
end;
hence
( tan is_differentiable_on ].0,1.[ & ( for th being Real st th in ].0,1.[ holds
diff (tan,th) > 0 ) )
by A1, A2, FDIFF_2:21; verum