for x being Real st x in ].0,(PI / 2).[ holds
diff (sec,x) > 0
proof
let x be
Real;
( x in ].0,(PI / 2).[ implies diff (sec,x) > 0 )
assume A1:
x in ].0,(PI / 2).[
;
diff (sec,x) > 0
].0,(PI / 2).[ c= ].(- (PI / 2)),(PI / 2).[
by XXREAL_1:46;
then A2:
cos . x > 0
by A1, COMPTRIG:11;
PI / 2
< PI / 1
by XREAL_1:76;
then
].0,(PI / 2).[ c= ].0,PI.[
by XXREAL_1:46;
then
sin . x > 0
by A1, COMPTRIG:7;
then
(sin . x) / ((cos . x) ^2) > 0 / ((cos . x) ^2)
by A2;
hence
diff (
sec,
x)
> 0
by A1, Th5;
verum
end;
hence
sec | ].0,(PI / 2).[ is increasing
by Lm9, Th1, Th5, ROLLE:9, XBOOLE_1:1; verum