:: Basic properties of even and odd functions :: by Bo Li and Yanhong Men :: :: Received May 25, 2009 :: Copyright (c) 2009-2018 Association of Mizar Users :: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland). :: This code can be distributed under the GNU General Public Licence :: version 3.0 or later, or the Creative Commons Attribution-ShareAlike :: License version 3.0 or later, subject to the binding interpretation :: detailed in file COPYING.interpretation. :: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these :: licenses, or see http://www.gnu.org/licenses/gpl.html and :: http://creativecommons.org/licenses/by-sa/3.0/. environ vocabularies NUMBERS, REAL_1, XCMPLX_0, ARYTM_1, SUBSET_1, RELAT_1, XBOOLE_0, MEMBERED, PARTFUN1, FUNCT_1, ABIAN, TARSKI, ARYTM_3, CARD_1, COMPLEX1, VALUED_1, SQUARE_1, ABSVALUE, XXREAL_0, EUCLID, SIN_COS, SIN_COS2, XXREAL_1, SIN_COS9, SIN_COS4, FUNCT_8, FUNCT_7; notations COMPLEX1, XCMPLX_0, ORDINAL1, NUMBERS, XREAL_0, XXREAL_0, REAL_1, MEMBERED, ABSVALUE, PARTFUN1, TARSKI, XBOOLE_0, SUBSET_1, EUCLID, RELAT_1, FUNCT_1, FUNCT_2, SIN_COS, SIN_COS2, VALUED_1, RCOMP_1, SIN_COS4, SQUARE_1, SIN_COS9, RELSET_1, FDIFF_9; constructors REAL_1, RCOMP_1, EUCLID, SQUARE_1, ABSVALUE, SIN_COS2, RFUNCT_1, RELSET_1, SIN_COS9, BINOP_2, SIN_COS, FDIFF_9, SIN_COS4, NEWTON; registrations XXREAL_0, XREAL_0, XBOOLE_0, MEMBERED, XCMPLX_0, NUMBERS, VALUED_0, FUNCT_1, RELAT_1, FUNCT_2, RELSET_1, SIN_COS9, ORDINAL1; requirements REAL, NUMERALS, SUBSET, ARITHM, BOOLE; begin :: Even and odd functions reserve x, r for Real; definition let A be set; attr A is symmetrical means :: FUNCT_8:def 1 for x being Complex st x in A holds -x in A; end; registration cluster symmetrical for Subset of COMPLEX; end; registration cluster symmetrical for Subset of REAL; end; reserve A for symmetrical Subset of COMPLEX; definition let R be Relation; attr R is with_symmetrical_domain means :: FUNCT_8:def 2 dom R is symmetrical; end; registration cluster empty -> with_symmetrical_domain for Relation; end; registration let R be with_symmetrical_domain Relation; cluster dom R -> symmetrical; end; definition let X,Y be complex-membered set; let F be PartFunc of X, Y; attr F is quasi_even means :: FUNCT_8:def 3 for x st x in dom F & -x in dom F holds F. (-x)=F.x; end; 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 quasi_even; end; registration let X,Y be complex-membered set; cluster with_symmetrical_domain quasi_even -> even for PartFunc of X, Y; cluster even -> with_symmetrical_domain quasi_even for PartFunc of X, Y; 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; definition let X,Y be complex-membered set; let F be PartFunc of X, Y; attr F is quasi_odd means :: FUNCT_8:def 6 for x st x in dom F & -x in dom F holds F.( -x)=-F.x; end; 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 quasi_odd; end; registration let X,Y be complex-membered set; cluster with_symmetrical_domain quasi_odd -> odd for PartFunc of X, Y; cluster odd -> with_symmetrical_domain quasi_odd for PartFunc of X, Y; 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; reserve F,G for PartFunc of REAL, REAL; theorem :: FUNCT_8:1 F is_odd_on A iff (A c= dom F & for x st x in A holds F.x+F.(-x)=0); theorem :: FUNCT_8:2 F is_even_on A iff (A c= dom F & for x st x in A holds F.x-F.(-x)=0); theorem :: FUNCT_8:3 (F is_odd_on A & for x st x in A holds F.x<>0) implies (A c= dom F & for x st x in A holds F.x / F.(-x)=-1); theorem :: FUNCT_8:4 (A c= dom F & for x st x in A holds F.x / F.(-x)=-1) implies F is_odd_on A; theorem :: FUNCT_8:5 (F is_even_on A & for x st x in A holds F.x<>0 ) implies (A c= dom F & for x st x in A holds F.x / F.(-x)=1); theorem :: FUNCT_8:6 (A c= dom F & for x st x in A holds F.x / F.(-x)=1) implies F is_even_on A; theorem :: FUNCT_8:7 F is_even_on A & F is_odd_on A implies for x st x in A holds F.x=0; theorem :: FUNCT_8:8 F is_even_on A implies for x st x in A holds F.x = F. |.x.|; theorem :: FUNCT_8:9 (A c= dom F & for x st x in A holds F.x = F. |.x.|) implies F is_even_on A; theorem :: FUNCT_8:10 F is_odd_on A & G is_odd_on A implies F + G is_odd_on A; theorem :: FUNCT_8:11 F is_even_on A & G is_even_on A implies F + G is_even_on A; theorem :: FUNCT_8:12 F is_odd_on A & G is_odd_on A implies F - G is_odd_on A; theorem :: FUNCT_8:13 F is_even_on A & G is_even_on A implies F - G is_even_on A; theorem :: FUNCT_8:14 F is_odd_on A implies r (#) F is_odd_on A; theorem :: FUNCT_8:15 F is_even_on A implies r (#) F is_even_on A; theorem :: FUNCT_8:16 F is_odd_on A implies -F is_odd_on A; theorem :: FUNCT_8:17 F is_even_on A implies -F is_even_on A; theorem :: FUNCT_8:18 F is_odd_on A implies F" is_odd_on A; theorem :: FUNCT_8:19 F is_even_on A implies F" is_even_on A; theorem :: FUNCT_8:20 F is_odd_on A implies |. F .| is_even_on A; theorem :: FUNCT_8:21 F is_even_on A implies |. F .| is_even_on A; theorem :: FUNCT_8:22 F is_odd_on A & G is_odd_on A implies F (#) G is_even_on A; theorem :: FUNCT_8:23 F is_even_on A & G is_even_on A implies F (#) G is_even_on A; theorem :: FUNCT_8:24 F is_even_on A & G is_odd_on A implies F (#) G is_odd_on A; theorem :: FUNCT_8:25 F is_even_on A implies r+F is_even_on A; theorem :: FUNCT_8:26 F is_even_on A implies F-r is_even_on A; theorem :: FUNCT_8:27 F is_even_on A implies F^2 is_even_on A; theorem :: FUNCT_8:28 F is_odd_on A implies F^2 is_even_on A; theorem :: FUNCT_8:29 F is_odd_on A & G is_odd_on A implies F /" G is_even_on A; theorem :: FUNCT_8:30 F is_even_on A & G is_even_on A implies F /" G is_even_on A; theorem :: FUNCT_8:31 F is_odd_on A & G is_even_on A implies F /" G is_odd_on A; theorem :: FUNCT_8:32 F is_even_on A & G is_odd_on A implies F /" G is_odd_on A; theorem :: FUNCT_8:33 F is odd implies -F is odd; theorem :: FUNCT_8:34 F is even implies -F is even; theorem :: FUNCT_8:35 F is odd implies F" is odd; theorem :: FUNCT_8:36 F is even implies F" is even; theorem :: FUNCT_8:37 F is odd implies |. F .| is even; theorem :: FUNCT_8:38 F is even implies |. F .| is even; theorem :: FUNCT_8:39 F is odd implies F^2 is even; theorem :: FUNCT_8:40 F is even implies F^2 is even; theorem :: FUNCT_8:41 F is even implies r+F is even; theorem :: FUNCT_8:42 F is even implies F-r is even; theorem :: FUNCT_8:43 F is odd implies r (#) F is odd; theorem :: FUNCT_8:44 F is even implies r (#) F is even; theorem :: FUNCT_8:45 F is odd & G is odd & dom F /\ dom G is symmetrical implies F + G is odd; theorem :: FUNCT_8:46 F is even & G is even & dom F /\ dom G is symmetrical implies F + G is even; theorem :: FUNCT_8:47 F is odd & G is odd & dom F /\ dom G is symmetrical implies F - G is odd; theorem :: FUNCT_8:48 F is even & G is even & dom F /\ dom G is symmetrical implies F - G is even; theorem :: FUNCT_8:49 F is odd & G is odd & dom F /\ dom G is symmetrical implies F (#) G is even; theorem :: FUNCT_8:50 F is even & G is even & dom F /\ dom G is symmetrical implies F (#) G is even ; theorem :: FUNCT_8:51 F is even & G is odd & dom F /\ dom G is symmetrical implies F (#) G is odd; theorem :: FUNCT_8:52 F is odd & G is odd & dom F /\ dom G is symmetrical implies F /" G is even; theorem :: FUNCT_8:53 F is even & G is even & dom F /\ dom G is symmetrical implies F /" G is even; theorem :: FUNCT_8:54 F is odd & G is even & dom F /\ dom G is symmetrical implies F /" G is odd; theorem :: FUNCT_8:55 F is even & G is odd & dom F /\ dom G is symmetrical implies F /" G is odd; begin :: Examples definition func signum -> Function of REAL, REAL means :: FUNCT_8:def 9 for x being Real holds it .x = sgn x; end; theorem :: FUNCT_8:56 for x being Real st x > 0 holds signum.x = 1; theorem :: FUNCT_8:57 for x being Real st x < 0 holds signum.x = -1; theorem :: FUNCT_8:58 signum.0 = 0; theorem :: FUNCT_8:59 for x being Real holds signum.(-x) = -signum.x; theorem :: FUNCT_8:60 for A being symmetrical Subset of REAL holds signum is_odd_on A; theorem :: FUNCT_8:61 for x being Real st x >= 0 holds absreal.x = x; theorem :: FUNCT_8:62 for x being Real st x < 0 holds absreal.x = -x; theorem :: FUNCT_8:63 for x being Real holds absreal.(-x) = absreal.x; theorem :: FUNCT_8:64 for A being symmetrical Subset of REAL holds absreal is_even_on A; theorem :: FUNCT_8:65 for A being symmetrical Subset of REAL holds sin is_odd_on A; theorem :: FUNCT_8:66 for A being symmetrical Subset of REAL holds cos is_even_on A; registration cluster sin -> odd; end; registration cluster cos -> even; end; theorem :: FUNCT_8:67 for A being symmetrical Subset of REAL holds sinh is_odd_on A; theorem :: FUNCT_8:68 for A being symmetrical Subset of REAL holds cosh is_even_on A; registration cluster sinh -> odd; end; registration cluster cosh -> even; end; theorem :: FUNCT_8:69 A c= ].-PI/2,PI/2.[ implies tan is_odd_on A; theorem :: FUNCT_8:70 A c= dom tan implies tan is_odd_on A; theorem :: FUNCT_8:71 A c= dom cot implies cot is_odd_on A; theorem :: FUNCT_8:72 A c= [.-1,1.] implies arctan is_odd_on A; theorem :: FUNCT_8:73 for A being symmetrical Subset of REAL holds |. sin .| is_even_on A; theorem :: FUNCT_8:74 for A being symmetrical Subset of REAL holds |. cos .| is_even_on A; theorem :: FUNCT_8:75 for A being symmetrical Subset of REAL holds sin" is_odd_on A; theorem :: FUNCT_8:76 for A being symmetrical Subset of REAL holds cos" is_even_on A; theorem :: FUNCT_8:77 for A being symmetrical Subset of REAL holds -sin is_odd_on A; theorem :: FUNCT_8:78 for A being symmetrical Subset of REAL holds -cos is_even_on A; theorem :: FUNCT_8:79 for A being symmetrical Subset of REAL holds sin^2 is_even_on A; theorem :: FUNCT_8:80 for A being symmetrical Subset of REAL holds cos^2 is_even_on A; reserve B for symmetrical Subset of REAL; theorem :: FUNCT_8:81 B c= dom (sec) implies sec is_even_on B; theorem :: FUNCT_8:82 (for x being Real st x in B holds cos.x<>0) implies sec is_even_on B; theorem :: FUNCT_8:83 B c= dom (cosec) implies cosec is_odd_on B; theorem :: FUNCT_8:84 (for x being Real st x in B holds sin.x<>0) implies cosec is_odd_on B;