let A be symmetrical Subset of COMPLEX; ( A c= ].(- (PI / 2)),(PI / 2).[ implies tan is_odd_on A )
assume A1:
A c= ].(- (PI / 2)),(PI / 2).[
; tan is_odd_on A
then A2:
A c= dom tan
by SIN_COS9:1;
A3:
dom (tan | A) = A
by A1, RELAT_1:62, SIN_COS9:1, XBOOLE_1:1;
A4:
for x being Real st x in A holds
tan . (- x) = - (tan . x)
for x being Real st x in dom (tan | A) & - x in dom (tan | A) holds
(tan | A) . (- x) = - ((tan | A) . x)
proof
let x be
Real;
( x in dom (tan | A) & - x in dom (tan | A) implies (tan | A) . (- x) = - ((tan | A) . x) )
assume that A6:
x in dom (tan | A)
and A7:
- x in dom (tan | A)
;
(tan | A) . (- x) = - ((tan | A) . x)
reconsider x =
x as
Element of
REAL by XREAL_0:def 1;
(tan | A) . (- x) =
(tan | A) /. (- x)
by A7, PARTFUN1:def 6
.=
tan /. (- x)
by A2, A3, A7, PARTFUN2:17
.=
tan . (- x)
by A2, A7, PARTFUN1:def 6
.=
- (tan . x)
by A4, A6
.=
- (tan /. x)
by A2, A6, PARTFUN1:def 6
.=
- ((tan | A) /. x)
by A2, A3, A6, PARTFUN2:17
.=
- ((tan | A) . x)
by A6, PARTFUN1:def 6
;
hence
(tan | A) . (- x) = - ((tan | A) . x)
;
verum
end;
then
( tan | A is with_symmetrical_domain & tan | A is quasi_odd )
by A3;
hence
tan is_odd_on A
by A2; verum