:: by Bo Li and Yanhong Men

::

:: Received May 25, 2009

:: Copyright (c) 2009-2021 Association of Mizar Users

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

for A being set holds

( A is symmetrical iff for x being Complex st x in A holds

- x in A );

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

for R being Relation holds

( R is with_symmetrical_domain iff dom R is symmetrical );

registration

coherence

for b_{1} being Relation st b_{1} is empty holds

b_{1} is with_symmetrical_domain

end;
for b

b

proof end;

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

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

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

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 ;

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
;

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

for b

b

coherence

for b

( b

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

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

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

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

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

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 ;

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
;

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

for b

b

coherence

for b

( b

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

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

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

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

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

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

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

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

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.|

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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;

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;

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

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

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

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

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: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

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

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

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

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

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

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

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

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

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

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

F /" G is odd

proof end;

definition

ex b_{1} being Function of REAL,REAL st

for x being Real holds b_{1} . x = sgn x

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}
end;

func signum -> Function of REAL,REAL means :Def9: :: FUNCT_8:def 9

for x being Real holds it . x = sgn x;

existence for x being Real holds it . x = sgn x;

ex b

for x being Real holds b

proof end;

uniqueness for b

b

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

for b

( b

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

cos . x <> 0 ) holds

sec is_even_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

sin . x <> 0 ) holds

cosec is_odd_on B

proof end;