for th being Real st th in dom (tan | [.0,1.]) holds
tan | [.0,1.] is_continuous_in th
proof
let th be Real; :: thesis: ( th in dom (tan | [.0,1.]) implies tan | [.0,1.] is_continuous_in th )
assume A1: th in dom (tan | [.0,1.]) ; :: thesis: tan | [.0,1.] is_continuous_in th
then A2: th in [.0,1.] by RELAT_1:57;
dom sin = REAL by FUNCT_2:def 1;
then A3: th in dom sin by XREAL_0:def 1;
A4: th in [#] REAL by XREAL_0:def 1;
then sin is_differentiable_in th by Th67, FDIFF_1:9;
then A5: sin is_continuous_in th by FDIFF_1:24;
cos is_differentiable_in th by A4, Th66, FDIFF_1:9;
then A6: cos is_continuous_in th by FDIFF_1:24;
cos . th <> 0 by A2, Th68;
then A7: tan is_continuous_in th by A3, A5, A6, FCONT_1:11;
now :: thesis: for rseq being Real_Sequence st rng rseq c= dom (tan | [.0,1.]) & rseq is convergent & lim rseq = th holds
( (tan | [.0,1.]) /* rseq is convergent & (tan | [.0,1.]) . th = lim ((tan | [.0,1.]) /* rseq) )
let rseq be Real_Sequence; :: thesis: ( rng rseq c= dom (tan | [.0,1.]) & rseq is convergent & lim rseq = th implies ( (tan | [.0,1.]) /* rseq is convergent & (tan | [.0,1.]) . th = lim ((tan | [.0,1.]) /* rseq) ) )
assume that
A8: rng rseq c= dom (tan | [.0,1.]) and
A9: ( rseq is convergent & lim rseq = th ) ; :: thesis: ( (tan | [.0,1.]) /* rseq is convergent & (tan | [.0,1.]) . th = lim ((tan | [.0,1.]) /* rseq) )
A10: rng rseq c= dom tan by A8, Lm14, Th69, XBOOLE_1:1;
then A11: tan . th = lim (tan /* rseq) by A7, A9, FCONT_1:def 1;
now :: thesis: for k1 being Element of NAT holds ((tan | [.0,1.]) /* rseq) . k1 = (tan /* rseq) . k1
let k1 be Element of NAT ; :: thesis: ((tan | [.0,1.]) /* rseq) . k1 = (tan /* rseq) . k1
dom rseq = NAT by SEQ_1:1;
then rseq . k1 in rng rseq by FUNCT_1:def 3;
then A12: (tan | [.0,1.]) . (rseq . k1) = tan . (rseq . k1) by A8, Lm14;
(tan | [.0,1.]) . (rseq . k1) = ((tan | [.0,1.]) /* rseq) . k1 by A8, FUNCT_2:108;
hence ((tan | [.0,1.]) /* rseq) . k1 = (tan /* rseq) . k1 by A8, A12, Lm14, Th69, FUNCT_2:108, XBOOLE_1:1; :: thesis: verum
end;
then (tan | [.0,1.]) /* rseq = tan /* rseq ;
hence ( (tan | [.0,1.]) /* rseq is convergent & (tan | [.0,1.]) . th = lim ((tan | [.0,1.]) /* rseq) ) by A1, A7, A9, A10, A11, Lm14, FCONT_1:def 1; :: thesis: verum
end;
hence tan | [.0,1.] is_continuous_in th by FCONT_1:def 1; :: thesis: verum
end;
hence tan | [.0,1.] is continuous by FCONT_1:def 2; :: thesis: verum