:: Basic properties of even and odd functions
:: by Bo Li and Yanhong Men
::
:: Received May 25, 2009
:: Copyright (c) 2009-2021 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 b1 being Subset of COMPLEX st b1 is symmetrical
proof end;
end;

registration
cluster complex-membered ext-real-membered real-membered symmetrical for Element of K16(REAL);
existence
ex b1 being Subset of REAL st b1 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 b1 being Relation st b1 is empty holds
b1 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 b1 being PartFunc of X,Y st b1 is with_symmetrical_domain & b1 is quasi_even holds
b1 is even ;
cluster Function-like even -> with_symmetrical_domain quasi_even for Element of K16(K17(X,Y));
coherence
for b1 being PartFunc of X,Y st b1 is even holds
( b1 is with_symmetrical_domain & b1 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 b1 being PartFunc of X,Y st b1 is with_symmetrical_domain & b1 is quasi_odd holds
b1 is odd ;
cluster Function-like odd -> with_symmetrical_domain quasi_odd for Element of K16(K17(X,Y));
coherence
for b1 being PartFunc of X,Y st b1 is odd holds
( b1 is with_symmetrical_domain & b1 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 b1 being Function of REAL,REAL st
for x being Real holds b1 . x = sgn x
proof end;
uniqueness
for b1, b2 being Function of REAL,REAL st ( for x being Real holds b1 . x = sgn x ) & ( for x being Real holds b2 . x = sgn x ) holds
b1 = b2
proof end;
end;

:: deftheorem Def9 defines signum FUNCT_8:def 9 :
for b1 being Function of REAL,REAL holds
( b1 = signum iff for x being Real holds b1 . 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;