:: Basic properties of even and odd functions
:: by Bo Li and Yanhong Men
::
:: Received May 25, 2009
:: Copyright (c) 2009-2015 Association of Mizar Users
definition
let
A
be
set
;
attr
A
is
symmetrical
means
:
Def1
:
:: FUNCT_8:def 1
for
x
being
Complex
st
x
in
A
holds
-
x
in
A
;
end;
::
deftheorem
Def1
defines
symmetrical
FUNCT_8:def 1 :
for
A
being
set
holds
(
A
is
symmetrical
iff for
x
being
Complex
st
x
in
A
holds
-
x
in
A
);
registration
cluster
complex-membered
symmetrical
for
Element
of
K16
(
COMPLEX
);
existence
ex
b
1
being
Subset
of
COMPLEX
st
b
1
is
symmetrical
proof
end;
end;
registration
cluster
complex-membered
ext-real-membered
real-membered
symmetrical
for
Element
of
K16
(
REAL
);
existence
ex
b
1
being
Subset
of
REAL
st
b
1
is
symmetrical
proof
end;
end;
definition
let
R
be
Relation
;
attr
R
is
with_symmetrical_domain
means
:
Def2
:
:: FUNCT_8:def 2
dom
R
is
symmetrical
;
end;
::
deftheorem
Def2
defines
with_symmetrical_domain
FUNCT_8:def 2 :
for
R
being
Relation
holds
(
R
is
with_symmetrical_domain
iff
dom
R
is
symmetrical
);
registration
cluster
Relation-like
empty
->
with_symmetrical_domain
for
set
;
coherence
for
b
1
being
Relation
st
b
1
is
empty
holds
b
1
is
with_symmetrical_domain
proof
end;
end;
registration
let
R
be
with_symmetrical_domain
Relation
;
cluster
dom
R
->
symmetrical
;
coherence
dom
R
is
symmetrical
by
Def2
;
end;
definition
let
X
,
Y
be
complex-membered
set
;
let
F
be
PartFunc
of
X
,
Y
;
attr
F
is
quasi_even
means
:
Def3
:
:: FUNCT_8:def 3
for
x
being
Real
st
x
in
dom
F
&
-
x
in
dom
F
holds
F
.
(
-
x
)
=
F
.
x
;
end;
::
deftheorem
Def3
defines
quasi_even
FUNCT_8:def 3 :
for
X
,
Y
being
complex-membered
set
for
F
being
PartFunc
of
X
,
Y
holds
(
F
is
quasi_even
iff for
x
being
Real
st
x
in
dom
F
&
-
x
in
dom
F
holds
F
.
(
-
x
)
=
F
.
x
);
definition
let
X
,
Y
be
complex-membered
set
;
let
F
be
PartFunc
of
X
,
Y
;
attr
F
is
even
means
:: FUNCT_8:def 4
(
F
is
with_symmetrical_domain
&
F
is
quasi_even
);
end;
::
deftheorem
defines
even
FUNCT_8:def 4 :
for
X
,
Y
being
complex-membered
set
for
F
being
PartFunc
of
X
,
Y
holds
(
F
is
even
iff (
F
is
with_symmetrical_domain
&
F
is
quasi_even
) );
registration
let
X
,
Y
be
complex-membered
set
;
cluster
Function-like
with_symmetrical_domain
quasi_even
->
even
for
Element
of
K16
(
K17
(
X
,
Y
));
coherence
for
b
1
being
PartFunc
of
X
,
Y
st
b
1
is
with_symmetrical_domain
&
b
1
is
quasi_even
holds
b
1
is
even
;
cluster
Function-like
even
->
with_symmetrical_domain
quasi_even
for
Element
of
K16
(
K17
(
X
,
Y
));
coherence
for
b
1
being
PartFunc
of
X
,
Y
st
b
1
is
even
holds
(
b
1
is
with_symmetrical_domain
&
b
1
is
quasi_even
)
;
end;
definition
let
A
be
set
;
let
X
,
Y
be
complex-membered
set
;
let
F
be
PartFunc
of
X
,
Y
;
pred
F
is_even_on
A
means
:: FUNCT_8:def 5
(
A
c=
dom
F
&
F
|
A
is
even
);
end;
::
deftheorem
defines
is_even_on
FUNCT_8:def 5 :
for
A
being
set
for
X
,
Y
being
complex-membered
set
for
F
being
PartFunc
of
X
,
Y
holds
(
F
is_even_on
A
iff (
A
c=
dom
F
&
F
|
A
is
even
) );
definition
let
X
,
Y
be
complex-membered
set
;
let
F
be
PartFunc
of
X
,
Y
;
attr
F
is
quasi_odd
means
:
Def6
:
:: FUNCT_8:def 6
for
x
being
Real
st
x
in
dom
F
&
-
x
in
dom
F
holds
F
.
(
-
x
)
=
-
(
F
.
x
)
;
end;
::
deftheorem
Def6
defines
quasi_odd
FUNCT_8:def 6 :
for
X
,
Y
being
complex-membered
set
for
F
being
PartFunc
of
X
,
Y
holds
(
F
is
quasi_odd
iff for
x
being
Real
st
x
in
dom
F
&
-
x
in
dom
F
holds
F
.
(
-
x
)
=
-
(
F
.
x
)
);
definition
let
X
,
Y
be
complex-membered
set
;
let
F
be
PartFunc
of
X
,
Y
;
attr
F
is
odd
means
:: FUNCT_8:def 7
(
F
is
with_symmetrical_domain
&
F
is
quasi_odd
);
end;
::
deftheorem
defines
odd
FUNCT_8:def 7 :
for
X
,
Y
being
complex-membered
set
for
F
being
PartFunc
of
X
,
Y
holds
(
F
is
odd
iff (
F
is
with_symmetrical_domain
&
F
is
quasi_odd
) );
registration
let
X
,
Y
be
complex-membered
set
;
cluster
Function-like
with_symmetrical_domain
quasi_odd
->
odd
for
Element
of
K16
(
K17
(
X
,
Y
));
coherence
for
b
1
being
PartFunc
of
X
,
Y
st
b
1
is
with_symmetrical_domain
&
b
1
is
quasi_odd
holds
b
1
is
odd
;
cluster
Function-like
odd
->
with_symmetrical_domain
quasi_odd
for
Element
of
K16
(
K17
(
X
,
Y
));
coherence
for
b
1
being
PartFunc
of
X
,
Y
st
b
1
is
odd
holds
(
b
1
is
with_symmetrical_domain
&
b
1
is
quasi_odd
)
;
end;
definition
let
A
be
set
;
let
X
,
Y
be
complex-membered
set
;
let
F
be
PartFunc
of
X
,
Y
;
pred
F
is_odd_on
A
means
:: FUNCT_8:def 8
(
A
c=
dom
F
&
F
|
A
is
odd
);
end;
::
deftheorem
defines
is_odd_on
FUNCT_8:def 8 :
for
A
being
set
for
X
,
Y
being
complex-membered
set
for
F
being
PartFunc
of
X
,
Y
holds
(
F
is_odd_on
A
iff (
A
c=
dom
F
&
F
|
A
is
odd
) );
theorem
:: FUNCT_8:1
for
A
being
symmetrical
Subset
of
COMPLEX
for
F
being
PartFunc
of
REAL
,
REAL
holds
(
F
is_odd_on
A
iff (
A
c=
dom
F
& ( for
x
being
Real
st
x
in
A
holds
(
F
.
x
)
+
(
F
.
(
-
x
)
)
=
0
) ) )
proof
end;
theorem
:: FUNCT_8:2
for
A
being
symmetrical
Subset
of
COMPLEX
for
F
being
PartFunc
of
REAL
,
REAL
holds
(
F
is_even_on
A
iff (
A
c=
dom
F
& ( for
x
being
Real
st
x
in
A
holds
(
F
.
x
)
-
(
F
.
(
-
x
)
)
=
0
) ) )
proof
end;
theorem
:: FUNCT_8:3
for
A
being
symmetrical
Subset
of
COMPLEX
for
F
being
PartFunc
of
REAL
,
REAL
st
F
is_odd_on
A
& ( for
x
being
Real
st
x
in
A
holds
F
.
x
<>
0
) holds
(
A
c=
dom
F
& ( for
x
being
Real
st
x
in
A
holds
(
F
.
x
)
/
(
F
.
(
-
x
)
)
=
-
1 ) )
proof
end;
theorem
:: FUNCT_8:4
for
A
being
symmetrical
Subset
of
COMPLEX
for
F
being
PartFunc
of
REAL
,
REAL
st
A
c=
dom
F
& ( for
x
being
Real
st
x
in
A
holds
(
F
.
x
)
/
(
F
.
(
-
x
)
)
=
-
1 ) holds
F
is_odd_on
A
proof
end;
theorem
:: FUNCT_8:5
for
A
being
symmetrical
Subset
of
COMPLEX
for
F
being
PartFunc
of
REAL
,
REAL
st
F
is_even_on
A
& ( for
x
being
Real
st
x
in
A
holds
F
.
x
<>
0
) holds
(
A
c=
dom
F
& ( for
x
being
Real
st
x
in
A
holds
(
F
.
x
)
/
(
F
.
(
-
x
)
)
=
1 ) )
proof
end;
theorem
:: FUNCT_8:6
for
A
being
symmetrical
Subset
of
COMPLEX
for
F
being
PartFunc
of
REAL
,
REAL
st
A
c=
dom
F
& ( for
x
being
Real
st
x
in
A
holds
(
F
.
x
)
/
(
F
.
(
-
x
)
)
=
1 ) holds
F
is_even_on
A
proof
end;
theorem
:: FUNCT_8:7
for
A
being
symmetrical
Subset
of
COMPLEX
for
F
being
PartFunc
of
REAL
,
REAL
st
F
is_even_on
A
&
F
is_odd_on
A
holds
for
x
being
Real
st
x
in
A
holds
F
.
x
=
0
proof
end;
theorem
:: FUNCT_8:8
for
A
being
symmetrical
Subset
of
COMPLEX
for
F
being
PartFunc
of
REAL
,
REAL
st
F
is_even_on
A
holds
for
x
being
Real
st
x
in
A
holds
F
.
x
=
F
.
|.
x
.|
proof
end;
theorem
:: FUNCT_8:9
for
A
being
symmetrical
Subset
of
COMPLEX
for
F
being
PartFunc
of
REAL
,
REAL
st
A
c=
dom
F
& ( for
x
being
Real
st
x
in
A
holds
F
.
x
=
F
.
|.
x
.|
) holds
F
is_even_on
A
proof
end;
theorem
:: FUNCT_8:10
for
A
being
symmetrical
Subset
of
COMPLEX
for
F
,
G
being
PartFunc
of
REAL
,
REAL
st
F
is_odd_on
A
&
G
is_odd_on
A
holds
F
+
G
is_odd_on
A
proof
end;
theorem
:: FUNCT_8:11
for
A
being
symmetrical
Subset
of
COMPLEX
for
F
,
G
being
PartFunc
of
REAL
,
REAL
st
F
is_even_on
A
&
G
is_even_on
A
holds
F
+
G
is_even_on
A
proof
end;
theorem
:: FUNCT_8:12
for
A
being
symmetrical
Subset
of
COMPLEX
for
F
,
G
being
PartFunc
of
REAL
,
REAL
st
F
is_odd_on
A
&
G
is_odd_on
A
holds
F
-
G
is_odd_on
A
proof
end;
theorem
:: FUNCT_8:13
for
A
being
symmetrical
Subset
of
COMPLEX
for
F
,
G
being
PartFunc
of
REAL
,
REAL
st
F
is_even_on
A
&
G
is_even_on
A
holds
F
-
G
is_even_on
A
proof
end;
theorem
:: FUNCT_8:14
for
r
being
Real
for
A
being
symmetrical
Subset
of
COMPLEX
for
F
being
PartFunc
of
REAL
,
REAL
st
F
is_odd_on
A
holds
r
(#)
F
is_odd_on
A
proof
end;
theorem
:: FUNCT_8:15
for
r
being
Real
for
A
being
symmetrical
Subset
of
COMPLEX
for
F
being
PartFunc
of
REAL
,
REAL
st
F
is_even_on
A
holds
r
(#)
F
is_even_on
A
proof
end;
theorem
Th16
:
:: FUNCT_8:16
for
A
being
symmetrical
Subset
of
COMPLEX
for
F
being
PartFunc
of
REAL
,
REAL
st
F
is_odd_on
A
holds
-
F
is_odd_on
A
proof
end;
theorem
Th17
:
:: FUNCT_8:17
for
A
being
symmetrical
Subset
of
COMPLEX
for
F
being
PartFunc
of
REAL
,
REAL
st
F
is_even_on
A
holds
-
F
is_even_on
A
proof
end;
theorem
Th18
:
:: FUNCT_8:18
for
A
being
symmetrical
Subset
of
COMPLEX
for
F
being
PartFunc
of
REAL
,
REAL
st
F
is_odd_on
A
holds
F
"
is_odd_on
A
proof
end;
theorem
Th19
:
:: FUNCT_8:19
for
A
being
symmetrical
Subset
of
COMPLEX
for
F
being
PartFunc
of
REAL
,
REAL
st
F
is_even_on
A
holds
F
"
is_even_on
A
proof
end;
theorem
Th20
:
:: FUNCT_8:20
for
A
being
symmetrical
Subset
of
COMPLEX
for
F
being
PartFunc
of
REAL
,
REAL
st
F
is_odd_on
A
holds
|.
F
.|
is_even_on
A
proof
end;
theorem
Th21
:
:: FUNCT_8:21
for
A
being
symmetrical
Subset
of
COMPLEX
for
F
being
PartFunc
of
REAL
,
REAL
st
F
is_even_on
A
holds
|.
F
.|
is_even_on
A
proof
end;
theorem
Th22
:
:: FUNCT_8:22
for
A
being
symmetrical
Subset
of
COMPLEX
for
F
,
G
being
PartFunc
of
REAL
,
REAL
st
F
is_odd_on
A
&
G
is_odd_on
A
holds
F
(#)
G
is_even_on
A
proof
end;
theorem
Th23
:
:: FUNCT_8:23
for
A
being
symmetrical
Subset
of
COMPLEX
for
F
,
G
being
PartFunc
of
REAL
,
REAL
st
F
is_even_on
A
&
G
is_even_on
A
holds
F
(#)
G
is_even_on
A
proof
end;
theorem
:: FUNCT_8:24
for
A
being
symmetrical
Subset
of
COMPLEX
for
F
,
G
being
PartFunc
of
REAL
,
REAL
st
F
is_even_on
A
&
G
is_odd_on
A
holds
F
(#)
G
is_odd_on
A
proof
end;
theorem
:: FUNCT_8:25
for
r
being
Real
for
A
being
symmetrical
Subset
of
COMPLEX
for
F
being
PartFunc
of
REAL
,
REAL
st
F
is_even_on
A
holds
r
+
F
is_even_on
A
proof
end;
theorem
:: FUNCT_8:26
for
r
being
Real
for
A
being
symmetrical
Subset
of
COMPLEX
for
F
being
PartFunc
of
REAL
,
REAL
st
F
is_even_on
A
holds
F
-
r
is_even_on
A
proof
end;
theorem
:: FUNCT_8:27
for
A
being
symmetrical
Subset
of
COMPLEX
for
F
being
PartFunc
of
REAL
,
REAL
st
F
is_even_on
A
holds
F
^2
is_even_on
A
by
Th23
;
theorem
:: FUNCT_8:28
for
A
being
symmetrical
Subset
of
COMPLEX
for
F
being
PartFunc
of
REAL
,
REAL
st
F
is_odd_on
A
holds
F
^2
is_even_on
A
by
Th22
;
theorem
:: FUNCT_8:29
for
A
being
symmetrical
Subset
of
COMPLEX
for
F
,
G
being
PartFunc
of
REAL
,
REAL
st
F
is_odd_on
A
&
G
is_odd_on
A
holds
F
/"
G
is_even_on
A
proof
end;
theorem
:: FUNCT_8:30
for
A
being
symmetrical
Subset
of
COMPLEX
for
F
,
G
being
PartFunc
of
REAL
,
REAL
st
F
is_even_on
A
&
G
is_even_on
A
holds
F
/"
G
is_even_on
A
proof
end;
theorem
:: FUNCT_8:31
for
A
being
symmetrical
Subset
of
COMPLEX
for
F
,
G
being
PartFunc
of
REAL
,
REAL
st
F
is_odd_on
A
&
G
is_even_on
A
holds
F
/"
G
is_odd_on
A
proof
end;
theorem
:: FUNCT_8:32
for
A
being
symmetrical
Subset
of
COMPLEX
for
F
,
G
being
PartFunc
of
REAL
,
REAL
st
F
is_even_on
A
&
G
is_odd_on
A
holds
F
/"
G
is_odd_on
A
proof
end;
theorem
:: FUNCT_8:33
for
F
being
PartFunc
of
REAL
,
REAL
st
F
is
odd
holds
-
F
is
odd
proof
end;
theorem
:: FUNCT_8:34
for
F
being
PartFunc
of
REAL
,
REAL
st
F
is
even
holds
-
F
is
even
proof
end;
theorem
:: FUNCT_8:35
for
F
being
PartFunc
of
REAL
,
REAL
st
F
is
odd
holds
F
"
is
odd
proof
end;
theorem
:: FUNCT_8:36
for
F
being
PartFunc
of
REAL
,
REAL
st
F
is
even
holds
F
"
is
even
proof
end;
theorem
:: FUNCT_8:37
for
F
being
PartFunc
of
REAL
,
REAL
st
F
is
odd
holds
|.
F
.|
is
even
proof
end;
theorem
:: FUNCT_8:38
for
F
being
PartFunc
of
REAL
,
REAL
st
F
is
even
holds
|.
F
.|
is
even
proof
end;
theorem
:: FUNCT_8:39
for
F
being
PartFunc
of
REAL
,
REAL
st
F
is
odd
holds
F
^2
is
even
proof
end;
theorem
:: FUNCT_8:40
for
F
being
PartFunc
of
REAL
,
REAL
st
F
is
even
holds
F
^2
is
even
proof
end;
theorem
:: FUNCT_8:41
for
r
being
Real
for
F
being
PartFunc
of
REAL
,
REAL
st
F
is
even
holds
r
+
F
is
even
proof
end;
theorem
:: FUNCT_8:42
for
r
being
Real
for
F
being
PartFunc
of
REAL
,
REAL
st
F
is
even
holds
F
-
r
is
even
proof
end;
theorem
:: FUNCT_8:43
for
r
being
Real
for
F
being
PartFunc
of
REAL
,
REAL
st
F
is
odd
holds
r
(#)
F
is
odd
proof
end;
theorem
:: FUNCT_8:44
for
r
being
Real
for
F
being
PartFunc
of
REAL
,
REAL
st
F
is
even
holds
r
(#)
F
is
even
proof
end;
theorem
:: FUNCT_8:45
for
F
,
G
being
PartFunc
of
REAL
,
REAL
st
F
is
odd
&
G
is
odd
&
(
dom
F
)
/\
(
dom
G
)
is
symmetrical
holds
F
+
G
is
odd
proof
end;
theorem
:: FUNCT_8:46
for
F
,
G
being
PartFunc
of
REAL
,
REAL
st
F
is
even
&
G
is
even
&
(
dom
F
)
/\
(
dom
G
)
is
symmetrical
holds
F
+
G
is
even
proof
end;
theorem
:: FUNCT_8:47
for
F
,
G
being
PartFunc
of
REAL
,
REAL
st
F
is
odd
&
G
is
odd
&
(
dom
F
)
/\
(
dom
G
)
is
symmetrical
holds
F
-
G
is
odd
proof
end;
theorem
:: FUNCT_8:48
for
F
,
G
being
PartFunc
of
REAL
,
REAL
st
F
is
even
&
G
is
even
&
(
dom
F
)
/\
(
dom
G
)
is
symmetrical
holds
F
-
G
is
even
proof
end;
theorem
:: FUNCT_8:49
for
F
,
G
being
PartFunc
of
REAL
,
REAL
st
F
is
odd
&
G
is
odd
&
(
dom
F
)
/\
(
dom
G
)
is
symmetrical
holds
F
(#)
G
is
even
proof
end;
theorem
:: FUNCT_8:50
for
F
,
G
being
PartFunc
of
REAL
,
REAL
st
F
is
even
&
G
is
even
&
(
dom
F
)
/\
(
dom
G
)
is
symmetrical
holds
F
(#)
G
is
even
proof
end;
theorem
:: FUNCT_8:51
for
F
,
G
being
PartFunc
of
REAL
,
REAL
st
F
is
even
&
G
is
odd
&
(
dom
F
)
/\
(
dom
G
)
is
symmetrical
holds
F
(#)
G
is
odd
proof
end;
theorem
:: FUNCT_8:52
for
F
,
G
being
PartFunc
of
REAL
,
REAL
st
F
is
odd
&
G
is
odd
&
(
dom
F
)
/\
(
dom
G
)
is
symmetrical
holds
F
/"
G
is
even
proof
end;
theorem
:: FUNCT_8:53
for
F
,
G
being
PartFunc
of
REAL
,
REAL
st
F
is
even
&
G
is
even
&
(
dom
F
)
/\
(
dom
G
)
is
symmetrical
holds
F
/"
G
is
even
proof
end;
theorem
:: FUNCT_8:54
for
F
,
G
being
PartFunc
of
REAL
,
REAL
st
F
is
odd
&
G
is
even
&
(
dom
F
)
/\
(
dom
G
)
is
symmetrical
holds
F
/"
G
is
odd
proof
end;
theorem
:: FUNCT_8:55
for
F
,
G
being
PartFunc
of
REAL
,
REAL
st
F
is
even
&
G
is
odd
&
(
dom
F
)
/\
(
dom
G
)
is
symmetrical
holds
F
/"
G
is
odd
proof
end;
definition
func
signum
->
Function
of
REAL
,
REAL
means
:
Def9
:
:: FUNCT_8:def 9
for
x
being
Real
holds
it
.
x
=
sgn
x
;
existence
ex
b
1
being
Function
of
REAL
,
REAL
st
for
x
being
Real
holds
b
1
.
x
=
sgn
x
proof
end;
uniqueness
for
b
1
,
b
2
being
Function
of
REAL
,
REAL
st ( for
x
being
Real
holds
b
1
.
x
=
sgn
x
) & ( for
x
being
Real
holds
b
2
.
x
=
sgn
x
) holds
b
1
=
b
2
proof
end;
end;
::
deftheorem
Def9
defines
signum
FUNCT_8:def 9 :
for
b
1
being
Function
of
REAL
,
REAL
holds
(
b
1
=
signum
iff for
x
being
Real
holds
b
1
.
x
=
sgn
x
);
theorem
Th56
:
:: FUNCT_8:56
for
x
being
Real
st
x
>
0
holds
signum
.
x
=
1
proof
end;
theorem
Th57
:
:: FUNCT_8:57
for
x
being
Real
st
x
<
0
holds
signum
.
x
=
-
1
proof
end;
theorem
Th58
:
:: FUNCT_8:58
signum
.
0
=
0
proof
end;
theorem
Th59
:
:: FUNCT_8:59
for
x
being
Real
holds
signum
.
(
-
x
)
=
-
(
signum
.
x
)
proof
end;
theorem
:: FUNCT_8:60
for
A
being
symmetrical
Subset
of
REAL
holds
signum
is_odd_on
A
proof
end;
theorem
Th61
:
:: FUNCT_8:61
for
x
being
Real
st
x
>=
0
holds
absreal
.
x
=
x
proof
end;
theorem
Th62
:
:: FUNCT_8:62
for
x
being
Real
st
x
<
0
holds
absreal
.
x
=
-
x
proof
end;
theorem
Th63
:
:: FUNCT_8:63
for
x
being
Real
holds
absreal
.
(
-
x
)
=
absreal
.
x
proof
end;
theorem
:: FUNCT_8:64
for
A
being
symmetrical
Subset
of
REAL
holds
absreal
is_even_on
A
proof
end;
theorem
Th65
:
:: FUNCT_8:65
for
A
being
symmetrical
Subset
of
REAL
holds
sin
is_odd_on
A
proof
end;
theorem
Th66
:
:: FUNCT_8:66
for
A
being
symmetrical
Subset
of
REAL
holds
cos
is_even_on
A
proof
end;
registration
cluster
sin
->
odd
;
coherence
sin
is
odd
proof
end;
end;
registration
cluster
cos
->
even
;
coherence
cos
is
even
proof
end;
end;
theorem
:: FUNCT_8:67
for
A
being
symmetrical
Subset
of
REAL
holds
sinh
is_odd_on
A
proof
end;
theorem
:: FUNCT_8:68
for
A
being
symmetrical
Subset
of
REAL
holds
cosh
is_even_on
A
proof
end;
registration
cluster
sinh
->
odd
;
coherence
sinh
is
odd
proof
end;
end;
registration
cluster
cosh
->
even
;
coherence
cosh
is
even
proof
end;
end;
theorem
:: FUNCT_8:69
for
A
being
symmetrical
Subset
of
COMPLEX
st
A
c=
].
(
-
(
PI
/
2
)
)
,
(
PI
/
2
)
.[
holds
tan
is_odd_on
A
proof
end;
theorem
:: FUNCT_8:70
for
A
being
symmetrical
Subset
of
COMPLEX
st
A
c=
dom
tan
holds
tan
is_odd_on
A
proof
end;
theorem
:: FUNCT_8:71
for
A
being
symmetrical
Subset
of
COMPLEX
st
A
c=
dom
cot
holds
cot
is_odd_on
A
proof
end;
theorem
:: FUNCT_8:72
for
A
being
symmetrical
Subset
of
COMPLEX
st
A
c=
[.
(
-
1
)
,1
.]
holds
arctan
is_odd_on
A
proof
end;
theorem
:: FUNCT_8:73
for
A
being
symmetrical
Subset
of
REAL
holds
|.
sin
.|
is_even_on
A
proof
end;
theorem
:: FUNCT_8:74
for
A
being
symmetrical
Subset
of
REAL
holds
|.
cos
.|
is_even_on
A
proof
end;
theorem
:: FUNCT_8:75
for
A
being
symmetrical
Subset
of
REAL
holds
sin
"
is_odd_on
A
proof
end;
theorem
:: FUNCT_8:76
for
A
being
symmetrical
Subset
of
REAL
holds
cos
"
is_even_on
A
proof
end;
theorem
:: FUNCT_8:77
for
A
being
symmetrical
Subset
of
REAL
holds
-
sin
is_odd_on
A
proof
end;
theorem
:: FUNCT_8:78
for
A
being
symmetrical
Subset
of
REAL
holds
-
cos
is_even_on
A
proof
end;
theorem
:: FUNCT_8:79
for
A
being
symmetrical
Subset
of
REAL
holds
sin
^2
is_even_on
A
proof
end;
theorem
:: FUNCT_8:80
for
A
being
symmetrical
Subset
of
REAL
holds
cos
^2
is_even_on
A
proof
end;
theorem
Th81
:
:: FUNCT_8:81
for
B
being
symmetrical
Subset
of
REAL
st
B
c=
dom
sec
holds
sec
is_even_on
B
proof
end;
theorem
:: FUNCT_8:82
for
B
being
symmetrical
Subset
of
REAL
st ( for
x
being
Real
st
x
in
B
holds
cos
.
x
<>
0
) holds
sec
is_even_on
B
proof
end;
theorem
Th83
:
:: FUNCT_8:83
for
B
being
symmetrical
Subset
of
REAL
st
B
c=
dom
cosec
holds
cosec
is_odd_on
B
proof
end;
theorem
:: FUNCT_8:84
for
B
being
symmetrical
Subset
of
REAL
st ( for
x
being
Real
st
x
in
B
holds
sin
.
x
<>
0
) holds
cosec
is_odd_on
B
proof
end;