for th being Real st th in dom (cosec | [.(- (PI / 2)),0.[) holds
cosec | [.(- (PI / 2)),0.[ is_continuous_in th
proof
let th be
Real;
( th in dom (cosec | [.(- (PI / 2)),0.[) implies cosec | [.(- (PI / 2)),0.[ is_continuous_in th )
assume A1:
th in dom (cosec | [.(- (PI / 2)),0.[)
;
cosec | [.(- (PI / 2)),0.[ is_continuous_in th
then A2:
th in [.(- (PI / 2)),0.[
by RELAT_1:57;
then
th < 0
by Lm3, XXREAL_1:4;
then A3:
th + (2 * PI) < 0 + (2 * PI)
by XREAL_1:8;
- PI < th
by A2, Lm3, XXREAL_1:4;
then
(- PI) + (2 * PI) < th + (2 * PI)
by XREAL_1:8;
then
th + (2 * PI) in ].PI,(2 * PI).[
by A3;
then
sin . (th + (2 * PI)) <> 0
by COMPTRIG:9;
then A4:
sin . th <> 0
by SIN_COS:78;
sin is_differentiable_in th
by SIN_COS:64;
then A5:
cosec is_continuous_in th
by A4, FCONT_1:10, FDIFF_1:24;
now for rseq being Real_Sequence st rng rseq c= dom (cosec | [.(- (PI / 2)),0.[) & rseq is convergent & lim rseq = th holds
( (cosec | [.(- (PI / 2)),0.[) /* rseq is convergent & (cosec | [.(- (PI / 2)),0.[) . th = lim ((cosec | [.(- (PI / 2)),0.[) /* rseq) )let rseq be
Real_Sequence;
( rng rseq c= dom (cosec | [.(- (PI / 2)),0.[) & rseq is convergent & lim rseq = th implies ( (cosec | [.(- (PI / 2)),0.[) /* rseq is convergent & (cosec | [.(- (PI / 2)),0.[) . th = lim ((cosec | [.(- (PI / 2)),0.[) /* rseq) ) )assume that A6:
rng rseq c= dom (cosec | [.(- (PI / 2)),0.[)
and A7:
(
rseq is
convergent &
lim rseq = th )
;
( (cosec | [.(- (PI / 2)),0.[) /* rseq is convergent & (cosec | [.(- (PI / 2)),0.[) . th = lim ((cosec | [.(- (PI / 2)),0.[) /* rseq) )A8:
dom (cosec | [.(- (PI / 2)),0.[) = [.(- (PI / 2)),0.[
by Th3, RELAT_1:62;
now for n being Element of NAT holds ((cosec | [.(- (PI / 2)),0.[) /* rseq) . n = (cosec /* rseq) . nlet n be
Element of
NAT ;
((cosec | [.(- (PI / 2)),0.[) /* rseq) . n = (cosec /* rseq) . n
dom rseq = NAT
by SEQ_1:1;
then
rseq . n in rng rseq
by FUNCT_1:def 3;
then A9:
(cosec | [.(- (PI / 2)),0.[) . (rseq . n) = cosec . (rseq . n)
by A6, A8, FUNCT_1:49;
(cosec | [.(- (PI / 2)),0.[) . (rseq . n) = ((cosec | [.(- (PI / 2)),0.[) /* rseq) . n
by A6, FUNCT_2:108;
hence
((cosec | [.(- (PI / 2)),0.[) /* rseq) . n = (cosec /* rseq) . n
by A6, A8, A9, Th3, FUNCT_2:108, XBOOLE_1:1;
verum end; then A10:
(cosec | [.(- (PI / 2)),0.[) /* rseq = cosec /* rseq
by FUNCT_2:63;
A11:
rng rseq c= dom cosec
by A6, A8, Th3;
then
cosec . th = lim (cosec /* rseq)
by A5, A7, FCONT_1:def 1;
hence
(
(cosec | [.(- (PI / 2)),0.[) /* rseq is
convergent &
(cosec | [.(- (PI / 2)),0.[) . th = lim ((cosec | [.(- (PI / 2)),0.[) /* rseq) )
by A1, A5, A7, A11, A10, Lm35, FCONT_1:def 1;
verum end;
hence
cosec | [.(- (PI / 2)),0.[ is_continuous_in th
by FCONT_1:def 1;
verum
end;
hence
cosec | [.(- (PI / 2)),0.[ is continuous
by FCONT_1:def 2; verum