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

begin

definition

let A be set ;
attr A 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 Element of K6(COMPLEX);
existence
ex b₁ being Subset of COMPLEX st b₁ is symmetrical

proof end;

end;

registration

cluster complex-membered ext-real-membered real-membered symmetrical Element of K6(REAL);
existence
ex b₁ being Subset of REAL st b₁ 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 empty Relation-like -> with_symmetrical_domain set ;
coherence
for b₁ being Relation st b₁ is zero holds
b₁ is with_symmetrical_domain

proof end;

end;

registration

let R be with_symmetrical_domain Relation;
cluster proj1 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 :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 Element of K6(K7(X,Y));
coherence
for b₁ being PartFunc of X,Y st b₁ is with_symmetrical_domain & b₁ is quasi_even holds
b₁ is even by Def4;
cluster Function-like even -> with_symmetrical_domain quasi_even Element of K6(K7(X,Y));
coherence
for b₁ being PartFunc of X,Y st b₁ is even holds
( b₁ is with_symmetrical_domain & b₁ 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;
pred F 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;
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 :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 Element of K6(K7(X,Y));
coherence
for b₁ being PartFunc of X,Y st b₁ is with_symmetrical_domain & b₁ is quasi_odd holds
b₁ is odd by Def7;
cluster Function-like odd -> with_symmetrical_domain quasi_odd Element of K6(K7(X,Y));
coherence
for b₁ being PartFunc of X,Y st b₁ is odd holds
( b₁ is with_symmetrical_domain & b₁ 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;
pred F 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 ) ) )

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

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 b₁ being Function of REAL,REAL st
for x being Real holds b₁ . x = sgn x

proof end;

uniqueness
for b₁, b₂ being Function of REAL,REAL st ( for x being Real holds b₁ . x = sgn x ) & ( for x being Real holds b₂ . x = sgn x ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def9 defines signum FUNCT_8:def 9 :
for b₁ being Function of REAL,REAL holds
( b₁ = signum iff for x being Real holds b₁ . x = sgn x );

registration

let x be real number ;
cluster signum . x -> real ;
coherence
signum . x is real ;

end;

theorem Th56: :: FUNCT_8:56

for x being real number st x > 0 holds
signum . x = 1

proof end;

theorem Th57: :: FUNCT_8:57

for x being real number 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 number 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 number st x >= 0 holds
absreal . x = x

proof end;

theorem Th62: :: FUNCT_8:62

for x being real number st x < 0 holds
absreal . x = - x

proof end;

theorem Th63: :: FUNCT_8:63

for x being real number 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 number 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 number st x in B holds
sin . x <> 0 ) holds
cosec is_odd_on B

proof end;