:: Basic properties of even and odd functions
:: by Bo Li and Yanhong Men
::
:: Received May 25, 2009
:: Copyright (c) 2009-2012 Association of Mizar Users


begin

definition
let A be set ;
attrA is symmetrical  means :Def1: :: FUNCT_8:def 1
 for x being complex number 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 number st x in A holds
- x in A );

registration
cluster complex-membered symmetrical for Element of K6(COMPLEX);
existence
 ex b1 being Subset of COMPLEX st b1 is symmetrical
proofend;
end;

registration
cluster complex-membered ext-real-membered real-membered symmetrical for Element of K6(REAL);
existence
 ex b1 being Subset of REAL st b1 is symmetrical
proofend;
end;

definition
let R be Relation;
attrR 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 empty Relation-like  ->  with_symmetrical_domain for set ;
coherence
 for b1 being Relation st b1 is empty holds
b1 is with_symmetrical_domain
proofend;
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;
attrF 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;
attrF is even  means :Def4: :: FUNCT_8:def 4
( F is with_symmetrical_domain & F is quasi_even );
end;

:: deftheorem Def4 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 K6(K7(X,Y));
coherence
 for b1 being PartFunc of X,Y st b1 is with_symmetrical_domain & b1 is quasi_even holds
b1 is even by Def4;
cluster Function-like even  ->  with_symmetrical_domain quasi_even for Element of K6(K7(X,Y));
coherence
 for b1 being PartFunc of X,Y st b1 is even holds
( b1 is with_symmetrical_domain & b1 is quasi_even ) by Def4;
end;

definition
let A be set ;
let X, Y be complex-membered set ;
let F be PartFunc of X,Y;
predF is_even_on A means :Def5: :: FUNCT_8:def 5
( A c= dom F & F | A is even );
end;

:: deftheorem Def5 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;
attrF 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;
attrF is odd  means :Def7: :: FUNCT_8:def 7
( F is with_symmetrical_domain & F is quasi_odd );
end;

:: deftheorem Def7 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 K6(K7(X,Y));
coherence
 for b1 being PartFunc of X,Y st b1 is with_symmetrical_domain & b1 is quasi_odd holds
b1 is odd by Def7;
cluster Function-like odd  ->  with_symmetrical_domain quasi_odd for Element of K6(K7(X,Y));
coherence
 for b1 being PartFunc of X,Y st b1 is odd holds
( b1 is with_symmetrical_domain & b1 is quasi_odd ) by Def7;
end;

definition
let A be set ;
let X, Y be complex-membered set ;
let F be PartFunc of X,Y;
predF is_odd_on A means :Def8: :: FUNCT_8:def 8
( A c= dom F & F | A is odd );
end;

:: deftheorem Def8 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 ) ) )
proofend;

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 ) ) )
proofend;

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 &amp; ( for x being Real st x in A holds
(F . x) / (F . (- x)) = - 1 ) )
proofend;

theorem :: FUNCT_8:4
for A being symmetrical Subset of COMPLEX
for F being PartFunc of REAL,REAL st A c= dom F &amp; ( for x being Real st x in A holds
(F . x) / (F . (- x)) = - 1 ) holds
F is_odd_on A
proofend;

theorem :: FUNCT_8:5
for A being symmetrical Subset of COMPLEX
for F being PartFunc of REAL,REAL st F is_even_on A &amp; ( for x being Real st x in A holds
F . x <> 0 ) holds
( A c= dom F &amp; ( for x being Real st x in A holds
(F . x) / (F . (- x)) = 1 ) )
proofend;

theorem :: FUNCT_8:6
for A being symmetrical Subset of COMPLEX
for F being PartFunc of REAL,REAL st A c= dom F &amp; ( for x being Real st x in A holds
(F . x) / (F . (- x)) = 1 ) holds
F is_even_on A
proofend;

theorem :: FUNCT_8:7
for A being symmetrical Subset of COMPLEX
for F being PartFunc of REAL,REAL st F is_even_on A &amp; F is_odd_on A holds
for x being Real st x in A holds
F . x = 0
proofend;

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 . (abs x)
proofend;

theorem :: FUNCT_8:9
for A being symmetrical Subset of COMPLEX
for F being PartFunc of REAL,REAL st A c= dom F &amp; ( for x being Real st x in A holds
F . x = F . (abs x) ) holds
F is_even_on A
proofend;

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 &amp; G is_odd_on A holds
F + G is_odd_on A
proofend;

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 &amp; G is_even_on A holds
F + G is_even_on A
proofend;

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 &amp; G is_odd_on A holds
F - G is_odd_on A
proofend;

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 &amp; G is_even_on A holds
F - G is_even_on A
proofend;

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
proofend;

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
proofend;

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
proofend;

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
proofend;

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
proofend;

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
proofend;

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
proofend;

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
proofend;

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 &amp; G is_odd_on A holds
F (#) G is_even_on A
proofend;

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 &amp; G is_even_on A holds
F (#) G is_even_on A
proofend;

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 &amp; G is_odd_on A holds
F (#) G is_odd_on A
proofend;

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
proofend;

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
proofend;

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 &amp; G is_odd_on A holds
F /" G is_even_on A
proofend;

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 &amp; G is_even_on A holds
F /" G is_even_on A
proofend;

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 &amp; G is_even_on A holds
F /" G is_odd_on A
proofend;

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 &amp; G is_odd_on A holds
F /" G is_odd_on A
proofend;

theorem :: FUNCT_8:33
for F being PartFunc of REAL,REAL st F is odd holds
- F is odd
proofend;

theorem :: FUNCT_8:34
for F being PartFunc of REAL,REAL st F is even holds
- F is even
proofend;

theorem :: FUNCT_8:35
for F being PartFunc of REAL,REAL st F is odd holds
F " is odd
proofend;

theorem :: FUNCT_8:36
for F being PartFunc of REAL,REAL st F is even holds
F " is even
proofend;

theorem :: FUNCT_8:37
for F being PartFunc of REAL,REAL st F is odd holds
|.F.| is even
proofend;

theorem :: FUNCT_8:38
for F being PartFunc of REAL,REAL st F is even holds
|.F.| is even
proofend;

theorem :: FUNCT_8:39
for F being PartFunc of REAL,REAL st F is odd holds
F ^2 is even
proofend;

theorem :: FUNCT_8:40
for F being PartFunc of REAL,REAL st F is even holds
F ^2 is even
proofend;

theorem :: FUNCT_8:41
for r being Real
for F being PartFunc of REAL,REAL st F is even holds
r + F is even
proofend;

theorem :: FUNCT_8:42
for r being Real
for F being PartFunc of REAL,REAL st F is even holds
F - r is even
proofend;

theorem :: FUNCT_8:43
for r being Real
for F being PartFunc of REAL,REAL st F is odd holds
r (#) F is odd
proofend;

theorem :: FUNCT_8:44
for r being Real
for F being PartFunc of REAL,REAL st F is even holds
r (#) F is even
proofend;

theorem :: FUNCT_8:45
for F, G being PartFunc of REAL,REAL st F is odd &amp; G is odd &amp; (dom F) /\ (dom G) is symmetrical holds
F + G is odd
proofend;

theorem :: FUNCT_8:46
for F, G being PartFunc of REAL,REAL st F is even &amp; G is even &amp; (dom F) /\ (dom G) is symmetrical holds
F + G is even
proofend;

theorem :: FUNCT_8:47
for F, G being PartFunc of REAL,REAL st F is odd &amp; G is odd &amp; (dom F) /\ (dom G) is symmetrical holds
F - G is odd
proofend;

theorem :: FUNCT_8:48
for F, G being PartFunc of REAL,REAL st F is even &amp; G is even &amp; (dom F) /\ (dom G) is symmetrical holds
F - G is even
proofend;

theorem :: FUNCT_8:49
for F, G being PartFunc of REAL,REAL st F is odd &amp; G is odd &amp; (dom F) /\ (dom G) is symmetrical holds
F (#) G is even
proofend;

theorem :: FUNCT_8:50
for F, G being PartFunc of REAL,REAL st F is even &amp; G is even &amp; (dom F) /\ (dom G) is symmetrical holds
F (#) G is even
proofend;

theorem :: FUNCT_8:51
for F, G being PartFunc of REAL,REAL st F is even &amp; G is odd &amp; (dom F) /\ (dom G) is symmetrical holds
F (#) G is odd
proofend;

theorem :: FUNCT_8:52
for F, G being PartFunc of REAL,REAL st F is odd &amp; G is odd &amp; (dom F) /\ (dom G) is symmetrical holds
F /" G is even
proofend;

theorem :: FUNCT_8:53
for F, G being PartFunc of REAL,REAL st F is even &amp; G is even &amp; (dom F) /\ (dom G) is symmetrical holds
F /" G is even
proofend;

theorem :: FUNCT_8:54
for F, G being PartFunc of REAL,REAL st F is odd &amp; G is even &amp; (dom F) /\ (dom G) is symmetrical holds
F /" G is odd
proofend;

theorem :: FUNCT_8:55
for F, G being PartFunc of REAL,REAL st F is even &amp; G is odd &amp; (dom F) /\ (dom G) is symmetrical holds
F /" G is odd
proofend;

begin

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
proofend;
uniqueness
 for b1, b2 being Function of REAL,REAL st ( for x being Real holds b1 . x = sgn x ) &amp; ( for x being Real holds b2 . x = sgn x ) holds
b1 = b2
proofend;
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 number st x > 0 holds
signum . x = 1
proofend;

theorem Th57: :: FUNCT_8:57
for x being real number st x < 0 holds
signum . x = - 1
proofend;

theorem Th58: :: FUNCT_8:58
signum . 0 = 0
proofend;

theorem Th59: :: FUNCT_8:59
for x being real number holds signum . (- x) = - (signum . x)
proofend;

theorem :: FUNCT_8:60
for A being symmetrical Subset of REAL holds signum is_odd_on A
proofend;

theorem Th61: :: FUNCT_8:61
for x being real number st x >= 0 holds
absreal . x = x
proofend;

theorem Th62: :: FUNCT_8:62
for x being real number st x < 0 holds
absreal . x = - x
proofend;

theorem Th63: :: FUNCT_8:63
for x being real number holds absreal . (- x) = absreal . x
proofend;

theorem :: FUNCT_8:64
for A being symmetrical Subset of REAL holds absreal is_even_on A
proofend;

theorem Th65: :: FUNCT_8:65
for A being symmetrical Subset of REAL holds sin is_odd_on A
proofend;

theorem Th66: :: FUNCT_8:66
for A being symmetrical Subset of REAL holds cos is_even_on A
proofend;

registration
cluster sin  ->  odd ;
coherence
 sin is odd
proofend;
end;

registration
cluster cos  ->  even ;
coherence
 cos is even
proofend;
end;

theorem :: FUNCT_8:67
for A being symmetrical Subset of REAL holds sinh is_odd_on A
proofend;

theorem :: FUNCT_8:68
for A being symmetrical Subset of REAL holds cosh is_even_on A
proofend;

registration
cluster sinh  ->  odd ;
coherence
 sinh is odd
proofend;
end;

registration
cluster cosh  ->  even ;
coherence
 cosh is even
proofend;
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
proofend;

theorem :: FUNCT_8:70
for A being symmetrical Subset of COMPLEX st A c= dom tan holds
tan is_odd_on A
proofend;

theorem :: FUNCT_8:71
for A being symmetrical Subset of COMPLEX st A c= dom cot holds
cot is_odd_on A
proofend;

theorem :: FUNCT_8:72
for A being symmetrical Subset of COMPLEX st A c= [.(- 1),1.] holds
arctan is_odd_on A
proofend;

theorem :: FUNCT_8:73
for A being symmetrical Subset of REAL holds |.sin.| is_even_on A
proofend;

theorem :: FUNCT_8:74
for A being symmetrical Subset of REAL holds |.cos.| is_even_on A
proofend;

theorem :: FUNCT_8:75
for A being symmetrical Subset of REAL holds sin " is_odd_on A
proofend;

theorem :: FUNCT_8:76
for A being symmetrical Subset of REAL holds cos " is_even_on A
proofend;

theorem :: FUNCT_8:77
for A being symmetrical Subset of REAL holds - sin is_odd_on A
proofend;

theorem :: FUNCT_8:78
for A being symmetrical Subset of REAL holds - cos is_even_on A
proofend;

theorem :: FUNCT_8:79
for A being symmetrical Subset of REAL holds sin ^2 is_even_on A
proofend;

theorem :: FUNCT_8:80
for A being symmetrical Subset of REAL holds cos ^2 is_even_on A
proofend;

theorem Th81: :: FUNCT_8:81
for B being symmetrical Subset of REAL st B c= dom sec holds
sec is_even_on B
proofend;

theorem :: FUNCT_8:82
for B being symmetrical Subset of REAL st ( for x being real number st x in B holds
cos . x <> 0 ) holds
sec is_even_on B
proofend;

theorem Th83: :: FUNCT_8:83
for B being symmetrical Subset of REAL st B c= dom cosec holds
cosec is_odd_on B
proofend;

theorem :: FUNCT_8:84
for B being symmetrical Subset of REAL st ( for x being real number st x in B holds
sin . x <> 0 ) holds
cosec is_odd_on B
proofend;