for x being Real st x in ].0,(PI / 2).[ holds
diff (cosec,x) < 0
proof
let x be
Real;
( x in ].0,(PI / 2).[ implies diff (cosec,x) < 0 )
assume A1:
x in ].0,(PI / 2).[
;
diff (cosec,x) < 0
].0,(PI / 2).[ c= ].(- (PI / 2)),(PI / 2).[
by XXREAL_1:46;
then A2:
cos . x > 0
by A1, COMPTRIG:11;
].0,(PI / 2).[ c= ].0,PI.[
by COMPTRIG:5, XXREAL_1:46;
then
sin . x > 0
by A1, COMPTRIG:7;
then
- ((cos . x) / ((sin . x) ^2)) < - 0
by A2;
hence
diff (
cosec,
x)
< 0
by A1, Th8;
verum
end;
hence
cosec | ].0,(PI / 2).[ is decreasing
by Lm17, Th4, Th8, ROLLE:10, XBOOLE_1:1; verum