for th being Real st th in dom (sec | ].(PI / 2),PI.]) holds
sec | ].(PI / 2),PI.] is_continuous_in th
proof
let th be
Real;
( th in dom (sec | ].(PI / 2),PI.]) implies sec | ].(PI / 2),PI.] is_continuous_in th )
A1:
cos is_differentiable_in th
by SIN_COS:63;
assume A2:
th in dom (sec | ].(PI / 2),PI.])
;
sec | ].(PI / 2),PI.] is_continuous_in th
then
th in ].(PI / 2),PI.]
by RELAT_1:57;
then
cos . th <> 0
by Lm2, COMPTRIG:13;
then A3:
sec is_continuous_in th
by A1, FCONT_1:10, FDIFF_1:24;
now for rseq being Real_Sequence st rng rseq c= dom (sec | ].(PI / 2),PI.]) & rseq is convergent & lim rseq = th holds
( (sec | ].(PI / 2),PI.]) /* rseq is convergent & (sec | ].(PI / 2),PI.]) . th = lim ((sec | ].(PI / 2),PI.]) /* rseq) )let rseq be
Real_Sequence;
( rng rseq c= dom (sec | ].(PI / 2),PI.]) & rseq is convergent & lim rseq = th implies ( (sec | ].(PI / 2),PI.]) /* rseq is convergent & (sec | ].(PI / 2),PI.]) . th = lim ((sec | ].(PI / 2),PI.]) /* rseq) ) )assume that A4:
rng rseq c= dom (sec | ].(PI / 2),PI.])
and A5:
(
rseq is
convergent &
lim rseq = th )
;
( (sec | ].(PI / 2),PI.]) /* rseq is convergent & (sec | ].(PI / 2),PI.]) . th = lim ((sec | ].(PI / 2),PI.]) /* rseq) )A6:
dom (sec | ].(PI / 2),PI.]) = ].(PI / 2),PI.]
by Th2, RELAT_1:62;
now for n being Element of NAT holds ((sec | ].(PI / 2),PI.]) /* rseq) . n = (sec /* rseq) . nlet n be
Element of
NAT ;
((sec | ].(PI / 2),PI.]) /* rseq) . n = (sec /* rseq) . n
dom rseq = NAT
by SEQ_1:1;
then
rseq . n in rng rseq
by FUNCT_1:def 3;
then A7:
(sec | ].(PI / 2),PI.]) . (rseq . n) = sec . (rseq . n)
by A4, A6, FUNCT_1:49;
(sec | ].(PI / 2),PI.]) . (rseq . n) = ((sec | ].(PI / 2),PI.]) /* rseq) . n
by A4, FUNCT_2:108;
hence
((sec | ].(PI / 2),PI.]) /* rseq) . n = (sec /* rseq) . n
by A4, A6, A7, Th2, FUNCT_2:108, XBOOLE_1:1;
verum end; then A8:
(sec | ].(PI / 2),PI.]) /* rseq = sec /* rseq
by FUNCT_2:63;
A9:
rng rseq c= dom sec
by A4, A6, Th2;
then
sec . th = lim (sec /* rseq)
by A3, A5, FCONT_1:def 1;
hence
(
(sec | ].(PI / 2),PI.]) /* rseq is
convergent &
(sec | ].(PI / 2),PI.]) . th = lim ((sec | ].(PI / 2),PI.]) /* rseq) )
by A2, A3, A5, A9, A8, Lm34, FCONT_1:def 1;
verum end;
hence
sec | ].(PI / 2),PI.] is_continuous_in th
by FCONT_1:def 1;
verum
end;
hence
sec | ].(PI / 2),PI.] is continuous
by FCONT_1:def 2; verum