:: Basic properties of even and odd functions
:: by Bo Li and Yanhong Men
::
:: Received May 25, 2009
:: Copyright (c) 2009-2026 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;
definitions MEMBERED;
equalities SIN_COS4, VALUED_1, SIN_COS, SIN_COS9, XCMPLX_0, SQUARE_1,
SUBSET_1, FDIFF_9;
expansions MEMBERED;
theorems SIN_COS4, XREAL_0, ABSVALUE, FUNCT_2, COMPLEX1, XBOOLE_0, EUCLID,
XCMPLX_1, SIN_COS9, XXREAL_1, VALUED_1, XBOOLE_1, SIN_COS, SIN_COS2,
RFUNCT_1, XCMPLX_0, RELAT_1, PARTFUN2, FUNCT_1, TARSKI, PARTFUN1,
NUMBERS, FDIFF_8;
schemes FUNCT_2;
begin :: Even and odd functions
reserve x, r for Real;
definition
let A be set;
attr A is symmetrical means
:Def1:
for x being Complex st x in A holds -x in A;
end;
registration
cluster symmetrical for Subset of COMPLEX;
existence
proof
take [#]COMPLEX;
let x be Complex;
thus thesis by XCMPLX_0:def 2;
end;
end;
registration
cluster symmetrical for Subset of REAL;
existence
proof
take [#]REAL;
let x be Complex;
for x st x in REAL holds -x in REAL by XREAL_0:def 1;
hence thesis;
end;
end;
reserve A for symmetrical Subset of COMPLEX;
definition
let R be Relation;
attr R is with_symmetrical_domain means
:Def2:
dom R is symmetrical;
end;
registration
cluster empty -> with_symmetrical_domain for Relation;
coherence
proof
A1: {} is symmetrical;
thus thesis by A1;
end;
end;
registration
let R be with_symmetrical_domain Relation;
cluster dom R -> symmetrical;
coherence 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:
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
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;
coherence;
cluster even -> with_symmetrical_domain quasi_even for PartFunc of X, Y;
coherence;
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
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
:Def6:
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
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;
coherence;
cluster odd -> with_symmetrical_domain quasi_odd for PartFunc of X, Y;
coherence;
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
A c= dom F & F|A is odd;
end;
reserve F,G for PartFunc of REAL, REAL;
theorem
F is_odd_on A iff (A c= dom F & for x st x in A holds F.x+F.(-x)=0)
proof
A1: (A c= dom F & for x st x in A holds F.x+F.(-x)=0) implies F is_odd_on A
proof
assume that
A2: A c= dom F and
A3: for x st x in A holds F.x+F.(-x)=0;
A4: dom(F|A) = A by A2,RELAT_1:62;
A5: for x st x in A holds F.(-x)=-F.x
proof
let x;
assume x in A;
then F.x+F.(-x)=0 by A3;
hence thesis;
end;
for x st x in dom(F|A) & -x in dom(F|A) holds F|A.(-x)=-F|A.x
proof
let x be Real;
assume that
A6: x in dom(F|A) and
A7: -x in dom(F|A);
reconsider x as Element of REAL by XREAL_0:def 1;
F|A.(-x)=F|A/.(-x) by A7,PARTFUN1:def 6
.=F/.(-x) by A2,A4,A7,PARTFUN2:17
.=F.(-x) by A2,A7,PARTFUN1:def 6
.=-F.x by A5,A6
.=-F/.x by A2,A6,PARTFUN1:def 6
.=-F|A/.x by A2,A4,A6,PARTFUN2:17
.=-F|A.x by A6,PARTFUN1:def 6;
hence thesis;
end;
then F|A is with_symmetrical_domain quasi_odd by A4;
hence thesis by A2;
end;
F is_odd_on A implies (A c= dom F & for x st x in A holds F.x+F.(-x)=0)
proof
assume
A8: F is_odd_on A;
then
A9: A c= dom F;
A10: F|A is odd by A8;
for x st x in A holds F.x+F.(-x)=0
proof
let x;
assume
A11: x in A;
then
A12: x in dom(F|A) by A9,RELAT_1:62;
A13: -x in A by A11,Def1;
then
A14: -x in dom(F|A) by A9,RELAT_1:62;
reconsider x as Element of REAL by XREAL_0:def 1;
F.x+F.(-x)=F/.x+F.(-x) by A9,A11,PARTFUN1:def 6
.=F/.x+F/.(-x) by A9,A13,PARTFUN1:def 6
.=F|A/.x+F/.(-x) by A9,A11,PARTFUN2:17
.=F|A/.x+F|A/.(-x) by A9,A13,PARTFUN2:17
.=F|A/.x+F|A.(-x) by A14,PARTFUN1:def 6
.=F|A.x+F|A.(-x) by A12,PARTFUN1:def 6
.=F|A.x+(-F|A.x) by A10,A12,A14,Def6
.=0;
hence thesis;
end;
hence thesis by A8;
end;
hence thesis by A1;
end;
theorem
F is_even_on A iff (A c= dom F & for x st x in A holds F.x-F.(-x)=0)
proof
A1: (A c= dom F & for x st x in A holds F.x-F.(-x)=0) implies F is_even_on A
proof
assume that
A2: A c= dom F and
A3: for x st x in A holds F.x-F.(-x)=0;
A4: dom(F|A) = A by A2,RELAT_1:62;
A5: for x st x in A holds F.(-x)=F.x
proof
let x;
assume x in A;
then F.x-F.(-x)=0 by A3;
hence thesis;
end;
for x st x in dom(F|A) & -x in dom(F|A) holds F|A.(-x)=F|A.x
proof
let x;
assume that
A6: x in dom(F|A) and
A7: -x in dom(F|A);
reconsider x as Element of REAL by XREAL_0:def 1;
F|A.(-x)=F|A/.(-x) by A7,PARTFUN1:def 6
.=F/.(-x) by A2,A4,A7,PARTFUN2:17
.=F.(-x) by A2,A7,PARTFUN1:def 6
.=F.x by A5,A6
.=F/.x by A2,A6,PARTFUN1:def 6
.=F|A/.x by A2,A4,A6,PARTFUN2:17
.=F|A.x by A6,PARTFUN1:def 6;
hence thesis;
end;
then F|A is with_symmetrical_domain quasi_even by A4;
hence thesis by A2;
end;
F is_even_on A implies (A c= dom F & for x st x in A holds F.x-F.(-x)=0)
proof
assume
A8: F is_even_on A;
then
A9: A c= dom F;
A10: F|A is even by A8;
for x st x in A holds F.x-F.(-x)=0
proof
let x;
assume
A11: x in A;
then
A12: x in dom(F|A) by A9,RELAT_1:62;
A13: -x in A by A11,Def1;
then
A14: -x in dom(F|A) by A9,RELAT_1:62;
reconsider x as Element of REAL by XREAL_0:def 1;
F.x-F.(-x)=F/.x-F.(-x) by A9,A11,PARTFUN1:def 6
.=F/.x-F/.(-x) by A9,A13,PARTFUN1:def 6
.=F|A/.x-F/.(-x) by A9,A11,PARTFUN2:17
.=F|A/.x-F|A/.(-x) by A9,A13,PARTFUN2:17
.=F|A.x-F|A/.(-x) by A12,PARTFUN1:def 6
.=F|A.x-F|A.(-x) by A14,PARTFUN1:def 6
.=F|A.x-F|A.x by A10,A12,A14,Def3
.=0;
hence thesis;
end;
hence thesis by A8;
end;
hence thesis by A1;
end;
theorem
(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)
proof
assume that
A1: F is_odd_on A and
A2: for x st x in A holds F.x<>0;
A3: A c= dom F by A1;
A4: F|A is odd by A1;
for x st x in A holds F.x / F.(-x)=-1
proof
let x;
assume
A5: x in A;
then
A6: x in dom(F|A) by A3,RELAT_1:62;
reconsider x as Element of REAL by XREAL_0:def 1;
A7: F.x=F/.x by A3,A5,PARTFUN1:def 6
.=F|A/.x by A3,A5,PARTFUN2:17
.=F|A.x by A6,PARTFUN1:def 6;
A8: -x in A by A5,Def1;
then
A9: -x in dom(F|A) by A3,RELAT_1:62;
F.x / F.(-x)=F/.x / F.(-x) by A3,A5,PARTFUN1:def 6
.=F/.x / F/.(-x) by A3,A8,PARTFUN1:def 6
.=F|A/.x / F/.(-x) by A3,A5,PARTFUN2:17
.=F|A/.x / F|A/.(-x) by A3,A8,PARTFUN2:17
.=F|A.x / F|A/.(-x) by A6,PARTFUN1:def 6
.=F|A.x / F|A.(-x) by A9,PARTFUN1:def 6
.=F|A.x / (-F|A.x) by A4,A6,A9,Def6
.=-(F|A.x / F|A.x) by XCMPLX_1:188
.=-1 by A2,A5,A7,XCMPLX_1:60;
hence thesis;
end;
hence thesis by A1;
end;
theorem
(A c= dom F & for x st x in A holds F.x / F.(-x)=-1) implies F is_odd_on A
proof
assume that
A1: A c= dom F and
A2: for x st x in A holds F.x / F.(-x)=-1;
A3: dom(F|A) = A by A1,RELAT_1:62;
A4: for x st x in A holds F.(-x)=-F.x
proof
let x;
assume x in A;
then F.x / F.(-x)=-1 by A2;
hence thesis by XCMPLX_1:195;
end;
for x st x in dom(F|A) & -x in dom(F|A) holds F|A.(-x)=-F|A.x
proof
let x;
assume that
A5: x in dom(F|A) and
A6: -x in dom(F|A);
reconsider x as Element of REAL by XREAL_0:def 1;
F|A.(-x)=F|A/.(-x) by A6,PARTFUN1:def 6
.=F/.(-x) by A1,A3,A6,PARTFUN2:17
.=F.(-x) by A1,A6,PARTFUN1:def 6
.=-F.x by A4,A5
.=-F/.x by A1,A5,PARTFUN1:def 6
.=-F|A/.x by A1,A3,A5,PARTFUN2:17
.=-F|A.x by A5,PARTFUN1:def 6;
hence thesis;
end;
then F|A is with_symmetrical_domain quasi_odd by A3;
hence thesis by A1;
end;
theorem
(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)
proof
assume that
A1: F is_even_on A and
A2: for x st x in A holds F.x<>0;
A3: A c= dom F by A1;
A4: F|A is even by A1;
for x st x in A holds F.x / F.(-x)=1
proof
let x;
assume
A5: x in A;
then
A6: x in dom(F|A) by A3,RELAT_1:62;
reconsider x as Element of REAL by XREAL_0:def 1;
A7: F.x=F/.x by A3,A5,PARTFUN1:def 6
.=F|A/.x by A3,A5,PARTFUN2:17
.=F|A.x by A6,PARTFUN1:def 6;
A8: -x in A by A5,Def1;
then
A9: -x in dom(F|A) by A3,RELAT_1:62;
F.x / F.(-x)=F/.x / F.(-x) by A3,A5,PARTFUN1:def 6
.=F/.x / F/.(-x) by A3,A8,PARTFUN1:def 6
.=F|A/.x / F/.(-x) by A3,A5,PARTFUN2:17
.=F|A/.x / F|A/.(-x) by A3,A8,PARTFUN2:17
.=F|A.x / F|A/.(-x) by A6,PARTFUN1:def 6
.=F|A.x / F|A.(-x) by A9,PARTFUN1:def 6
.=F|A.x / F|A.x by A4,A6,A9,Def3
.=1 by A2,A5,A7,XCMPLX_1:60;
hence thesis;
end;
hence thesis by A1;
end;
theorem
(A c= dom F & for x st x in A holds F.x / F.(-x)=1) implies F is_even_on A
proof
assume that
A1: A c= dom F and
A2: for x st x in A holds F.x / F.(-x)=1;
A3: dom(F|A) = A by A1,RELAT_1:62;
A4: for x st x in A holds F.(-x)=F.x
proof
let x;
assume x in A;
then F.x / F.(-x)=1 by A2;
hence thesis by XCMPLX_1:58;
end;
for x st x in dom(F|A) & -x in dom(F|A) holds F|A.(-x)=F|A.x
proof
let x;
assume that
A5: x in dom(F|A) and
A6: -x in dom(F|A);
reconsider x as Element of REAL by XREAL_0:def 1;
F|A.(-x)=F|A/.(-x) by A6,PARTFUN1:def 6
.=F/.(-x) by A1,A3,A6,PARTFUN2:17
.=F.(-x) by A1,A6,PARTFUN1:def 6
.=F.x by A4,A5
.=F/.x by A1,A5,PARTFUN1:def 6
.=F|A/.x by A1,A3,A5,PARTFUN2:17
.=F|A.x by A5,PARTFUN1:def 6;
hence thesis;
end;
then F|A is with_symmetrical_domain quasi_even by A3;
hence thesis by A1;
end;
theorem
F is_even_on A & F is_odd_on A implies for x st x in A holds F.x=0
proof
assume that
A1: F is_even_on A and
A2: F is_odd_on A;
A3: F|A is even by A1;
A4: F|A is odd by A2;
let x;
assume
A5: x in A;
A6: A c= dom F by A1;
then
A7: x in dom(F|A) by A5,RELAT_1:62;
-x in A by A5,Def1;
then
A8: -x in dom(F|A) by A6,RELAT_1:62;
reconsider x as Element of REAL by XREAL_0:def 1;
F.x=F/.x by A6,A5,PARTFUN1:def 6
.=F|A/.x by A6,A5,PARTFUN2:17
.=F|A.x by A7,PARTFUN1:def 6
.=F|A.(-x) by A3,A7,A8,Def3
.=-F|A.x by A4,A7,A8,Def6
.=-F|A/.x by A7,PARTFUN1:def 6
.=-F/.x by A6,A5,PARTFUN2:17
.=-F.x by A6,A5,PARTFUN1:def 6;
hence thesis;
end;
theorem
F is_even_on A implies for x st x in A holds F.x = F. |.x.|
proof
assume
A1: F is_even_on A;
then
A2: A c= dom F;
A3: F|A is even by A1;
let x such that
A4: x in A;
A5: x in dom(F|A) by A2,A4,RELAT_1:62;
A6: -x in A by A4,Def1;
then
A7: -x in dom(F|A) by A2,RELAT_1:62;
reconsider x as Element of REAL by XREAL_0:def 1;
per cases;
suppose
x < 0;
then F. |.x.|=F.(-x) by ABSVALUE:def 1
.=F/.(-x) by A2,A6,PARTFUN1:def 6
.=F|A/.(-x) by A2,A6,PARTFUN2:17
.=F|A.(-x) by A7,PARTFUN1:def 6
.=F|A.x by A3,A5,A7,Def3
.=F|A/.x by A5,PARTFUN1:def 6
.=F/.x by A2,A4,PARTFUN2:17
.=F.x by A2,A4,PARTFUN1:def 6;
hence thesis;
end;
suppose
0 < x;
hence thesis by ABSVALUE:def 1;
end;
suppose
x = 0;
hence thesis by ABSVALUE:def 1;
end;
end;
theorem
(A c= dom F & for x st x in A holds F.x = F. |.x.|) implies F is_even_on A
proof
assume that
A1: A c= dom F and
A2: for x st x in A holds F.x = F. |.x.|;
A3: dom(F|A) = A by A1,RELAT_1:62;
A4: for x st x in A holds -x in A by Def1;
A5: for x st x in A holds F.(-x) = F.(x)
proof
let x;
assume
A6: x in A;
per cases;
suppose
x < 0;
then F.(-x)=F. |.x.| by ABSVALUE:def 1
.=F.x by A2,A6;
hence thesis;
end;
suppose
0 < x;
then |.-x.|=-(-x) by ABSVALUE:def 1
.=x;
hence thesis by A2,A4,A6;
end;
suppose
x = 0;
hence thesis;
end;
end;
for x st x in dom(F|A) & -x in dom(F|A) holds F|A.(-x)=F|A.x
proof
let x;
assume that
A7: x in dom(F|A) and
A8: -x in dom(F|A);
reconsider x as Element of REAL by XREAL_0:def 1;
F|A.(-x)=F|A/.(-x) by A8,PARTFUN1:def 6
.=F/.(-x) by A1,A3,A8,PARTFUN2:17
.=F.(-x) by A1,A8,PARTFUN1:def 6
.=F.x by A5,A7
.=F/.x by A1,A7,PARTFUN1:def 6
.=F|A/.x by A1,A3,A7,PARTFUN2:17
.=F|A.x by A7,PARTFUN1:def 6;
hence thesis;
end;
then F|A is with_symmetrical_domain quasi_even by A3;
hence thesis by A1;
end;
theorem
F is_odd_on A & G is_odd_on A implies F + G is_odd_on A
proof
assume that
A1: F is_odd_on A and
A2: G is_odd_on A;
A3: A c= dom G by A2;
A4: G|A is odd by A2;
A5: A c= dom F by A1;
then
A6: A c= dom F /\ dom G by A3,XBOOLE_1:19;
A7: dom F /\ dom G=dom (F + G) by VALUED_1:def 1;
then
A8: dom((F + G)|A) = A by A5,A3,RELAT_1:62,XBOOLE_1:19;
A9: F|A is odd by A1;
for x st x in dom((F + G)|A) & -x in dom((F + G)|A) holds (F + G)|A.(-x
)=-(F + G)|A.x
proof
let x;
assume that
A10: x in dom((F + G)|A) and
A11: -x in dom((F + G)|A);
A12: x in dom(F|A) by A5,A8,A10,RELAT_1:62;
A13: x in dom(G|A) by A3,A8,A10,RELAT_1:62;
A14: -x in dom(F|A) by A5,A8,A11,RELAT_1:62;
A15: -x in dom(G|A) by A3,A8,A11,RELAT_1:62;
reconsider x as Element of REAL by XREAL_0:def 1;
(F + G)|A.(-x)=(F + G)|A/.(-x) by A11,PARTFUN1:def 6
.=(F + G)/.(-x) by A6,A7,A8,A11,PARTFUN2:17
.=(F + G).(-x) by A6,A7,A11,PARTFUN1:def 6
.=F.(-x) + G.(-x) by A6,A7,A11,VALUED_1:def 1
.=F/.(-x) + G.(-x) by A5,A11,PARTFUN1:def 6
.=F/.(-x) + G/.(-x) by A3,A11,PARTFUN1:def 6
.=F|A/.(-x) + G/.(-x) by A5,A8,A11,PARTFUN2:17
.=F|A/.(-x) + G|A/.(-x) by A3,A8,A11,PARTFUN2:17
.=F|A.(-x) + G|A/.(-x) by A14,PARTFUN1:def 6
.=F|A.(-x) + G|A.(-x) by A15,PARTFUN1:def 6
.=(-F|A.x) + G|A.(-x) by A9,A12,A14,Def6
.=(-F|A.x) + (-G|A.x) by A4,A13,A15,Def6
.=-(F|A.x + G|A.x)
.=-(F|A/.x + G|A.x) by A12,PARTFUN1:def 6
.=-(F|A/.x + G|A/.x) by A13,PARTFUN1:def 6
.=-(F/.x + G|A/.x) by A5,A8,A10,PARTFUN2:17
.=-(F/.x + G/.x) by A3,A8,A10,PARTFUN2:17
.=-(F.x + G/.x) by A5,A10,PARTFUN1:def 6
.=-(F.x + G.x) by A3,A10,PARTFUN1:def 6
.=-(F + G).x by A6,A7,A10,VALUED_1:def 1
.=-(F + G)/.x by A6,A7,A10,PARTFUN1:def 6
.=-(F + G)|A/.x by A6,A7,A8,A10,PARTFUN2:17
.=-(F + G)|A.x by A10,PARTFUN1:def 6;
hence thesis;
end;
then (F + G)|A is with_symmetrical_domain quasi_odd by A8;
hence thesis by A6,A7;
end;
theorem
F is_even_on A & G is_even_on A implies F + G is_even_on A
proof
assume that
A1: F is_even_on A and
A2: G is_even_on A;
A3: A c= dom G by A2;
A4: G|A is even by A2;
A5: A c= dom F by A1;
then
A6: A c= dom F /\ dom G by A3,XBOOLE_1:19;
A7: dom F /\ dom G=dom (F + G) by VALUED_1:def 1;
then
A8: dom((F + G)|A) = A by A5,A3,RELAT_1:62,XBOOLE_1:19;
A9: F|A is even by A1;
for x st x in dom((F + G)|A) & -x in dom((F + G)|A) holds (F + G)|A.(-x
)=(F + G)|A.x
proof
let x;
assume that
A10: x in dom((F + G)|A) and
A11: -x in dom((F + G)|A);
A12: x in dom(F|A) by A5,A8,A10,RELAT_1:62;
A13: x in dom(G|A) by A3,A8,A10,RELAT_1:62;
A14: -x in dom(F|A) by A5,A8,A11,RELAT_1:62;
A15: -x in dom(G|A) by A3,A8,A11,RELAT_1:62;
reconsider x as Element of REAL by XREAL_0:def 1;
(F + G)|A.(-x)=(F + G)|A/.(-x) by A11,PARTFUN1:def 6
.=(F + G)/.(-x) by A6,A7,A8,A11,PARTFUN2:17
.=(F + G).(-x) by A6,A7,A11,PARTFUN1:def 6
.=F.(-x) + G.(-x) by A6,A7,A11,VALUED_1:def 1
.=F/.(-x) + G.(-x) by A5,A11,PARTFUN1:def 6
.=F/.(-x) + G/.(-x) by A3,A11,PARTFUN1:def 6
.=F|A/.(-x) + G/.(-x) by A5,A8,A11,PARTFUN2:17
.=F|A/.(-x) + G|A/.(-x) by A3,A8,A11,PARTFUN2:17
.=F|A.(-x) + G|A/.(-x) by A14,PARTFUN1:def 6
.=F|A.(-x) + G|A.(-x) by A15,PARTFUN1:def 6
.=F|A.x + G|A.(-x) by A9,A12,A14,Def3
.=F|A.x + G|A.x by A4,A13,A15,Def3
.=F|A/.x + G|A.x by A12,PARTFUN1:def 6
.=F|A/.x + G|A/.x by A13,PARTFUN1:def 6
.=F/.x + G|A/.x by A5,A8,A10,PARTFUN2:17
.=F/.x + G/.x by A3,A8,A10,PARTFUN2:17
.=F.x + G/.x by A5,A10,PARTFUN1:def 6
.=F.x + G.x by A3,A10,PARTFUN1:def 6
.=(F + G).x by A6,A7,A10,VALUED_1:def 1
.=(F + G)/.x by A6,A7,A10,PARTFUN1:def 6
.=(F + G)|A/.x by A6,A7,A8,A10,PARTFUN2:17
.=(F + G)|A.x by A10,PARTFUN1:def 6;
hence thesis;
end;
then (F + G)|A is with_symmetrical_domain quasi_even by A8;
hence thesis by A6,A7;
end;
theorem
F is_odd_on A & G is_odd_on A implies F - G is_odd_on A
proof
assume that
A1: F is_odd_on A and
A2: G is_odd_on A;
A3: A c= dom G by A2;
A4: G|A is odd by A2;
A5: A c= dom F by A1;
then
A6: A c= dom F /\ dom G by A3,XBOOLE_1:19;
A7: dom F /\ dom G=dom (F - G) by VALUED_1:12;
then
A8: dom((F - G)|A) = A by A5,A3,RELAT_1:62,XBOOLE_1:19;
A9: F|A is odd by A1;
for x st x in dom((F - G)|A) & -x in dom((F - G)|A) holds (F - G)|A.(-x
)=-(F - G)|A.x
proof
let x;
assume that
A10: x in dom((F - G)|A) and
A11: -x in dom((F - G)|A);
A12: x in dom(F|A) by A5,A8,A10,RELAT_1:62;
A13: x in dom(G|A) by A3,A8,A10,RELAT_1:62;
A14: -x in dom(F|A) by A5,A8,A11,RELAT_1:62;
A15: -x in dom(G|A) by A3,A8,A11,RELAT_1:62;
reconsider x as Element of REAL by XREAL_0:def 1;
(F - G)|A.(-x)=(F - G)|A/.(-x) by A11,PARTFUN1:def 6
.=(F - G)/.(-x) by A6,A7,A8,A11,PARTFUN2:17
.=(F - G).(-x) by A6,A7,A11,PARTFUN1:def 6
.=F.(-x) - G.(-x) by A6,A7,A11,VALUED_1:13
.=F/.(-x) - G.(-x) by A5,A11,PARTFUN1:def 6
.=F/.(-x) - G/.(-x) by A3,A11,PARTFUN1:def 6
.=F|A/.(-x) - G/.(-x) by A5,A8,A11,PARTFUN2:17
.=F|A/.(-x) - G|A/.(-x) by A3,A8,A11,PARTFUN2:17
.=F|A.(-x) - G|A/.(-x) by A14,PARTFUN1:def 6
.=F|A.(-x) - G|A.(-x) by A15,PARTFUN1:def 6
.=(-F|A.x) - G|A.(-x) by A9,A12,A14,Def6
.=(-F|A.x) - (-G|A.x) by A4,A13,A15,Def6
.=-(F|A.x - G|A.x)
.=-(F|A/.x - G|A.x) by A12,PARTFUN1:def 6
.=-(F|A/.x - G|A/.x) by A13,PARTFUN1:def 6
.=-(F/.x - G|A/.x) by A5,A8,A10,PARTFUN2:17
.=-(F/.x - G/.x) by A3,A8,A10,PARTFUN2:17
.=-(F.x - G/.x) by A5,A10,PARTFUN1:def 6
.=-(F.x - G.x) by A3,A10,PARTFUN1:def 6
.=-(F - G).x by A6,A7,A10,VALUED_1:13
.=-(F - G)/.x by A6,A7,A10,PARTFUN1:def 6
.=-(F - G)|A/.x by A6,A7,A8,A10,PARTFUN2:17
.=-(F - G)|A.x by A10,PARTFUN1:def 6;
hence thesis;
end;
then (F - G)|A is with_symmetrical_domain quasi_odd by A8;
hence thesis by A6,A7;
end;
theorem
F is_even_on A & G is_even_on A implies F - G is_even_on A
proof
assume that
A1: F is_even_on A and
A2: G is_even_on A;
A3: A c= dom G by A2;
A4: G|A is even by A2;
A5: A c= dom F by A1;
then
A6: A c= dom F /\ dom G by A3,XBOOLE_1:19;
A7: dom F /\ dom G=dom (F - G) by VALUED_1:12;
then
A8: dom((F - G)|A) = A by A5,A3,RELAT_1:62,XBOOLE_1:19;
A9: F|A is even by A1;
for x st x in dom((F - G)|A) & -x in dom((F - G)|A) holds (F - G)|A.(-x
)=(F - G)|A.x
proof
let x;
assume that
A10: x in dom((F - G)|A) and
A11: -x in dom((F - G)|A);
A12: x in dom(F|A) by A5,A8,A10,RELAT_1:62;
A13: x in dom(G|A) by A3,A8,A10,RELAT_1:62;
A14: -x in dom(F|A) by A5,A8,A11,RELAT_1:62;
A15: -x in dom(G|A) by A3,A8,A11,RELAT_1:62;
reconsider x as Element of REAL by XREAL_0:def 1;
(F - G)|A.(-x)=(F - G)|A/.(-x) by A11,PARTFUN1:def 6
.=(F - G)/.(-x) by A6,A7,A8,A11,PARTFUN2:17
.=(F - G).(-x) by A6,A7,A11,PARTFUN1:def 6
.=F.(-x) - G.(-x) by A6,A7,A11,VALUED_1:13
.=F/.(-x) - G.(-x) by A5,A11,PARTFUN1:def 6
.=F/.(-x) - G/.(-x) by A3,A11,PARTFUN1:def 6
.=F|A/.(-x) - G/.(-x) by A5,A8,A11,PARTFUN2:17
.=F|A/.(-x) - G|A/.(-x) by A3,A8,A11,PARTFUN2:17
.=F|A.(-x) - G|A/.(-x) by A14,PARTFUN1:def 6
.=F|A.(-x) - G|A.(-x) by A15,PARTFUN1:def 6
.=F|A.x - G|A.(-x) by A9,A12,A14,Def3
.=F|A.x - G|A.x by A4,A13,A15,Def3
.=F|A/.x - G|A.x by A12,PARTFUN1:def 6
.=F|A/.x - G|A/.x by A13,PARTFUN1:def 6
.=F/.x - G|A/.x by A5,A8,A10,PARTFUN2:17
.=F/.x - G/.x by A3,A8,A10,PARTFUN2:17
.=F.x - G/.x by A5,A10,PARTFUN1:def 6
.=F.x - G.x by A3,A10,PARTFUN1:def 6
.=(F - G).x by A6,A7,A10,VALUED_1:13
.=(F - G)/.x by A6,A7,A10,PARTFUN1:def 6
.=(F - G)|A/.x by A6,A7,A8,A10,PARTFUN2:17
.=(F - G)|A.x by A10,PARTFUN1:def 6;
hence thesis;
end;
then (F - G)|A is with_symmetrical_domain quasi_even by A8;
hence thesis by A6,A7;
end;
theorem
F is_odd_on A implies r (#) F is_odd_on A
proof
assume
A1: F is_odd_on A;
then
A2: A c= dom F;
then
A3: A c= dom (r (#) F) by VALUED_1:def 5;
then
A4: dom((r (#) F)|A) = A by RELAT_1:62;
A5: F|A is odd by A1;
for x st x in dom((r (#) F)|A) & -x in dom((r (#) F)|A) holds (r (#) F)|
A.(-x)=-(r (#) F)|A.x
proof
let x;
assume that
A6: x in dom((r (#) F)|A) and
A7: -x in dom((r (#) F)|A);
A8: x in dom(F|A) by A2,A4,A6,RELAT_1:62;
A9: -x in dom(F|A) by A2,A4,A7,RELAT_1:62;
reconsider x as Element of REAL by XREAL_0:def 1;
(r (#) F)|A.(-x)=(r (#) F)|A/.(-x) by A7,PARTFUN1:def 6
.=(r (#) F)/.(-x) by A3,A4,A7,PARTFUN2:17
.=(r (#) F).(-x) by A3,A7,PARTFUN1:def 6
.=r * F.(-x) by A3,A7,VALUED_1:def 5
.=r * F/.(-x) by A2,A7,PARTFUN1:def 6
.=r * F|A/.(-x) by A2,A4,A7,PARTFUN2:17
.=r * F|A.(-x) by A9,PARTFUN1:def 6
.=r * (-F|A.x) by A5,A8,A9,Def6
.=-(r * F|A.x)
.=-(r * F|A/.x) by A8,PARTFUN1:def 6
.=-(r * F/.x) by A2,A4,A6,PARTFUN2:17
.=-(r * F.x) by A2,A6,PARTFUN1:def 6
.=-(r (#) F).x by A3,A6,VALUED_1:def 5
.=-(r (#) F)/.x by A3,A6,PARTFUN1:def 6
.=-(r (#) F)|A/.x by A3,A4,A6,PARTFUN2:17
.=-(r (#) F)|A.x by A6,PARTFUN1:def 6;
hence thesis;
end;
then (r (#) F)|A is with_symmetrical_domain quasi_odd by A4;
hence thesis by A3;
end;
theorem
F is_even_on A implies r (#) F is_even_on A
proof
assume
A1: F is_even_on A;
then
A2: A c= dom F;
then
A3: A c= dom (r (#) F) by VALUED_1:def 5;
then
A4: dom((r (#) F)|A) = A by RELAT_1:62;
A5: F|A is even by A1;
for x st x in dom((r (#) F)|A) & -x in dom((r (#) F)|A) holds (r (#) F)|
A.(-x)=(r (#) F)|A.x
proof
let x;
assume that
A6: x in dom((r (#) F)|A) and
A7: -x in dom((r (#) F)|A);
A8: x in dom(F|A) by A2,A4,A6,RELAT_1:62;
A9: -x in dom(F|A) by A2,A4,A7,RELAT_1:62;
reconsider x as Element of REAL by XREAL_0:def 1;
(r (#) F)|A.(-x)=(r (#) F)|A/.(-x) by A7,PARTFUN1:def 6
.=(r (#) F)/.(-x) by A3,A4,A7,PARTFUN2:17
.=(r (#) F).(-x) by A3,A7,PARTFUN1:def 6
.=r * F.(-x) by A3,A7,VALUED_1:def 5
.=r * F/.(-x) by A2,A7,PARTFUN1:def 6
.=r * F|A/.(-x) by A2,A4,A7,PARTFUN2:17
.=r * F|A.(-x) by A9,PARTFUN1:def 6
.=r * F|A.x by A5,A8,A9,Def3
.=r * F|A/.x by A8,PARTFUN1:def 6
.=r * F/.x by A2,A4,A6,PARTFUN2:17
.=r * F.x by A2,A6,PARTFUN1:def 6
.=(r (#) F).x by A3,A6,VALUED_1:def 5
.=(r (#) F)/.x by A3,A6,PARTFUN1:def 6
.=(r (#) F)|A/.x by A3,A4,A6,PARTFUN2:17
.=(r (#) F)|A.x by A6,PARTFUN1:def 6;
hence thesis;
end;
then (r (#) F)|A is with_symmetrical_domain quasi_even by A4;
hence thesis by A3;
end;
theorem Th16:
F is_odd_on A implies -F is_odd_on A
proof
assume
A1: F is_odd_on A;
then
A2: A c= dom F;
then
A3: A c= dom (-F) by VALUED_1:8;
then
A4: dom((-F)|A) = A by RELAT_1:62;
A5: F|A is odd by A1;
for x st x in dom((-F)|A) & -x in dom((-F)|A) holds (-F)|A.(-x)=-(-F)|A. x
proof
let x;
assume that
A6: x in dom((-F)|A) and
A7: -x in dom((-F)|A);
A8: x in dom(F|A) by A2,A4,A6,RELAT_1:62;
A9: -x in dom(F|A) by A2,A4,A7,RELAT_1:62;
reconsider x as Element of REAL by XREAL_0:def 1;
(-F)|A.(-x)=(-F)|A/.(-x) by A7,PARTFUN1:def 6
.=(-F)/.(-x) by A3,A4,A7,PARTFUN2:17
.=(-F).(-x) by A3,A7,PARTFUN1:def 6
.=-F.(-x) by VALUED_1:8
.=-F/.(-x) by A2,A7,PARTFUN1:def 6
.=-F|A/.(-x) by A2,A4,A7,PARTFUN2:17
.=-F|A.(-x) by A9,PARTFUN1:def 6
.=-(-F|A.x) by A5,A8,A9,Def6
.=-(-F|A/.x) by A8,PARTFUN1:def 6
.=-(-F/.x) by A2,A4,A6,PARTFUN2:17
.=-(-F.x) by A2,A6,PARTFUN1:def 6
.=-(-F).x by VALUED_1:8
.=-(-F)/.x by A3,A6,PARTFUN1:def 6
.=-(-F)|A/.x by A3,A4,A6,PARTFUN2:17
.=-(-F)|A.x by A6,PARTFUN1:def 6;
hence thesis;
end;
then (-F)|A is with_symmetrical_domain quasi_odd by A4;
hence thesis by A3;
end;
theorem Th17:
F is_even_on A implies -F is_even_on A
proof
assume
A1: F is_even_on A;
then
A2: A c= dom F;
then
A3: A c= dom (-F) by VALUED_1:8;
then
A4: dom((-F)|A) = A by RELAT_1:62;
A5: F|A is even by A1;
for x st x in dom((-F)|A) & -x in dom((-F)|A) holds (-F)|A.(-x)=(-F)|A.x
proof
let x;
assume that
A6: x in dom((-F)|A) and
A7: -x in dom((-F)|A);
A8: x in dom(F|A) by A2,A4,A6,RELAT_1:62;
A9: -x in dom(F|A) by A2,A4,A7,RELAT_1:62;
reconsider x as Element of REAL by XREAL_0:def 1;
(-F)|A.(-x)=(-F)|A/.(-x) by A7,PARTFUN1:def 6
.=(-F)/.(-x) by A3,A4,A7,PARTFUN2:17
.=(-F).(-x) by A3,A7,PARTFUN1:def 6
.=-F.(-x) by VALUED_1:8
.=-F/.(-x) by A2,A7,PARTFUN1:def 6
.=-F|A/.(-x) by A2,A4,A7,PARTFUN2:17
.=-F|A.(-x) by A9,PARTFUN1:def 6
.=-F|A.x by A5,A8,A9,Def3
.=-F|A/.x by A8,PARTFUN1:def 6
.=-F/.x by A2,A4,A6,PARTFUN2:17
.=-F.x by A2,A6,PARTFUN1:def 6
.=(-F).x by VALUED_1:8
.=(-F)/.x by A3,A6,PARTFUN1:def 6
.=(-F)|A/.x by A3,A4,A6,PARTFUN2:17
.=(-F)|A.x by A6,PARTFUN1:def 6;
hence thesis;
end;
then (-F)|A is with_symmetrical_domain quasi_even by A4;
hence thesis by A3;
end;
theorem Th18:
F is_odd_on A implies F" is_odd_on A
proof
assume
A1: F is_odd_on A;
then
A2: A c= dom F;
then
A3: A c= dom (F") by VALUED_1:def 7;
then
A4: dom((F")|A) = A by RELAT_1:62;
A5: F|A is odd by A1;
for x st x in dom((F")|A) & -x in dom((F")|A) holds (F")|A.(-x)=-(F")|A. x
proof
let x;
assume that
A6: x in dom((F")|A) and
A7: -x in dom((F")|A);
A8: x in dom(F|A) by A2,A4,A6,RELAT_1:62;
A9: -x in dom(F|A) by A2,A4,A7,RELAT_1:62;
reconsider x as Element of REAL by XREAL_0:def 1;
(F")|A.(-x)=(F")|A/.(-x) by A7,PARTFUN1:def 6
.=(F")/.(-x) by A3,A4,A7,PARTFUN2:17
.=(F").(-x) by A3,A7,PARTFUN1:def 6
.=(F.(-x))" by A3,A7,VALUED_1:def 7
.=(F/.(-x))" by A2,A7,PARTFUN1:def 6
.=(F|A/.(-x))" by A2,A4,A7,PARTFUN2:17
.=(F|A.(-x))" by A9,PARTFUN1:def 6
.=(-F|A.x)" by A5,A8,A9,Def6
.=(-F|A/.x)" by A8,PARTFUN1:def 6
.=(-F/.x)" by A2,A4,A6,PARTFUN2:17
.=(-F.x)" by A2,A6,PARTFUN1:def 6
.=-(F.x)" by XCMPLX_1:222
.=-(F").x by A3,A6,VALUED_1:def 7
.=-(F")/.x by A3,A6,PARTFUN1:def 6
.=-(F")|A/.x by A3,A4,A6,PARTFUN2:17
.=-(F")|A.x by A6,PARTFUN1:def 6;
hence thesis;
end;
then (F")|A is with_symmetrical_domain quasi_odd by A4;
hence thesis by A3;
end;
theorem Th19:
F is_even_on A implies F" is_even_on A
proof
assume
A1: F is_even_on A;
then
A2: A c= dom F;
then
A3: A c= dom (F") by VALUED_1:def 7;
then
A4: dom((F")|A) = A by RELAT_1:62;
A5: F|A is even by A1;
for x st x in dom((F")|A) & -x in dom((F")|A) holds (F")|A.(-x)=(F")|A.x
proof
let x;
assume that
A6: x in dom((F")|A) and
A7: -x in dom((F")|A);
A8: x in dom(F|A) by A2,A4,A6,RELAT_1:62;
A9: -x in dom(F|A) by A2,A4,A7,RELAT_1:62;
reconsider x as Element of REAL by XREAL_0:def 1;
(F")|A.(-x)=(F")|A/.(-x) by A7,PARTFUN1:def 6
.=(F")/.(-x) by A3,A4,A7,PARTFUN2:17
.=(F").(-x) by A3,A7,PARTFUN1:def 6
.=(F.(-x))" by A3,A7,VALUED_1:def 7
.=(F/.(-x))" by A2,A7,PARTFUN1:def 6
.=(F|A/.(-x))" by A2,A4,A7,PARTFUN2:17
.=(F|A.(-x))" by A9,PARTFUN1:def 6
.=(F|A.x)" by A5,A8,A9,Def3
.=(F|A/.x)" by A8,PARTFUN1:def 6
.=(F/.x)" by A2,A4,A6,PARTFUN2:17
.=(F.x)" by A2,A6,PARTFUN1:def 6
.=(F").x by A3,A6,VALUED_1:def 7
.=(F")/.x by A3,A6,PARTFUN1:def 6
.=(F")|A/.x by A3,A4,A6,PARTFUN2:17
.=(F")|A.x by A6,PARTFUN1:def 6;
hence thesis;
end;
then (F")|A is with_symmetrical_domain quasi_even by A4;
hence thesis by A3;
end;
theorem Th20:
F is_odd_on A implies |. F .| is_even_on A
proof
assume
A1: F is_odd_on A;
then
A2: A c= dom F;
then
A3: A c= dom (|. F .|) by VALUED_1:def 11;
then
A4: dom((|. F .|)|A) = A by RELAT_1:62;
A5: F|A is odd by A1;
for x st x in dom((|. F .|)|A) & -x in dom((|. F .|)|A) holds (|. F .|)|
A.(-x)=(|. F .|)|A.x
proof
let x;
assume that
A6: x in dom((|. F .|)|A) and
A7: -x in dom((|. F .|)|A);
A8: x in dom(F|A) by A2,A4,A6,RELAT_1:62;
A9: -x in dom(F|A) by A2,A4,A7,RELAT_1:62;
reconsider x as Element of REAL by XREAL_0:def 1;
(|. F .|)|A.(-x)=(|. F .|)|A/.(-x) by A7,PARTFUN1:def 6
.=(|. F .|)/.(-x) by A3,A4,A7,PARTFUN2:17
.=(|. F .|).(-x) by A3,A7,PARTFUN1:def 6
.=|. F.(-x) .| by A3,A7,VALUED_1:def 11
.=|. F/.(-x) .| by A2,A7,PARTFUN1:def 6
.=|. F|A/.(-x) .| by A2,A4,A7,PARTFUN2:17
.=|. F|A.(-x) .| by A9,PARTFUN1:def 6
.=|. -F|A.x .| by A5,A8,A9,Def6
.=|. -F|A/.x .| by A8,PARTFUN1:def 6
.=|. -F/.x .| by A2,A4,A6,PARTFUN2:17
.=|. -F.x .| by A2,A6,PARTFUN1:def 6
.=|. F.x .| by COMPLEX1:52
.=(|. F .|).x by A3,A6,VALUED_1:def 11
.=(|. F .|)/.x by A3,A6,PARTFUN1:def 6
.=(|. F .|)|A/.x by A3,A4,A6,PARTFUN2:17
.=(|. F .|)|A.x by A6,PARTFUN1:def 6;
hence thesis;
end;
then (|. F .|)|A is with_symmetrical_domain quasi_even by A4;
hence thesis by A3;
end;
theorem Th21:
F is_even_on A implies |. F .| is_even_on A
proof
assume
A1: F is_even_on A;
then
A2: A c= dom F;
then
A3: A c= dom (|. F .|) by VALUED_1:def 11;
then
A4: dom((|. F .|)|A) = A by RELAT_1:62;
A5: F|A is even by A1;
for x st x in dom((|. F .|)|A) & -x in dom((|. F .|)|A) holds (|. F .|)|
A.(-x)=(|. F .|)|A.x
proof
let x;
assume that
A6: x in dom((|. F .|)|A) and
A7: -x in dom((|. F .|)|A);
A8: x in dom(F|A) by A2,A4,A6,RELAT_1:62;
A9: -x in dom(F|A) by A2,A4,A7,RELAT_1:62;
reconsider x as Element of REAL by XREAL_0:def 1;
(|. F .|)|A.(-x)=(|. F .|)|A/.(-x) by A7,PARTFUN1:def 6
.=(|. F .|)/.(-x) by A3,A4,A7,PARTFUN2:17
.=(|. F .|).(-x) by A3,A7,PARTFUN1:def 6
.=|. F.(-x) .| by A3,A7,VALUED_1:def 11
.=|. F/.(-x) .| by A2,A7,PARTFUN1:def 6
.=|. F|A/.(-x) .| by A2,A4,A7,PARTFUN2:17
.=|. F|A.(-x) .| by A9,PARTFUN1:def 6
.=|. F|A.x .| by A5,A8,A9,Def3
.=|. F|A/.x .| by A8,PARTFUN1:def 6
.=|. F/.x .| by A2,A4,A6,PARTFUN2:17
.=|. F.x .| by A2,A6,PARTFUN1:def 6
.=(|. F .|).x by A3,A6,VALUED_1:def 11
.=(|. F .|)/.x by A3,A6,PARTFUN1:def 6
.=(|. F .|)|A/.x by A3,A4,A6,PARTFUN2:17
.=(|. F .|)|A.x by A6,PARTFUN1:def 6;
hence thesis;
end;
then (|. F .|)|A is with_symmetrical_domain quasi_even by A4;
hence thesis by A3;
end;
theorem Th22:
F is_odd_on A & G is_odd_on A implies F (#) G is_even_on A
proof
assume that
A1: F is_odd_on A and
A2: G is_odd_on A;
A3: A c= dom G by A2;
A4: G|A is odd by A2;
A5: A c= dom F by A1;
then
A6: A c= dom F /\ dom G by A3,XBOOLE_1:19;
A7: dom F /\ dom G=dom (F (#) G) by VALUED_1:def 4;
then
A8: dom((F (#) G)|A) = A by A5,A3,RELAT_1:62,XBOOLE_1:19;
A9: F|A is odd by A1;
for x st x in dom((F (#) G)|A) & -x in dom((F (#) G)|A) holds (F (#) G)
|A.(-x)=(F (#) G)|A.x
proof
let x;
assume that
A10: x in dom((F (#) G)|A) and
A11: -x in dom((F (#) G)|A);
A12: x in dom(F|A) by A5,A8,A10,RELAT_1:62;
A13: x in dom(G|A) by A3,A8,A10,RELAT_1:62;
A14: -x in dom(F|A) by A5,A8,A11,RELAT_1:62;
A15: -x in dom(G|A) by A3,A8,A11,RELAT_1:62;
reconsider x as Element of REAL by XREAL_0:def 1;
(F (#) G)|A.(-x)=(F (#) G)|A/.(-x) by A11,PARTFUN1:def 6
.=(F (#) G)/.(-x) by A6,A7,A8,A11,PARTFUN2:17
.=(F (#) G).(-x) by A6,A7,A11,PARTFUN1:def 6
.=F.(-x) * G.(-x) by A6,A7,A11,VALUED_1:def 4
.=F/.(-x) * G.(-x) by A5,A11,PARTFUN1:def 6
.=F/.(-x) * G/.(-x) by A3,A11,PARTFUN1:def 6
.=F|A/.(-x) * G/.(-x) by A5,A8,A11,PARTFUN2:17
.=F|A/.(-x) * G|A/.(-x) by A3,A8,A11,PARTFUN2:17
.=F|A.(-x) * G|A/.(-x) by A14,PARTFUN1:def 6
.=F|A.(-x) * G|A.(-x) by A15,PARTFUN1:def 6
.=(-F|A.x) * G|A.(-x) by A9,A12,A14,Def6
.=(-F|A.x) * (-G|A.x) by A4,A13,A15,Def6
.=F|A.x * G|A.x
.=F|A/.x * G|A.x by A12,PARTFUN1:def 6
.=F|A/.x * G|A/.x by A13,PARTFUN1:def 6
.=F/.x * G|A/.x by A5,A8,A10,PARTFUN2:17
.=F/.x * G/.x by A3,A8,A10,PARTFUN2:17
.=F.x * G/.x by A5,A10,PARTFUN1:def 6
.=F.x * G.x by A3,A10,PARTFUN1:def 6
.=(F (#) G).x by A6,A7,A10,VALUED_1:def 4
.=(F (#) G)/.x by A6,A7,A10,PARTFUN1:def 6
.=(F (#) G)|A/.x by A6,A7,A8,A10,PARTFUN2:17
.=(F (#) G)|A.x by A10,PARTFUN1:def 6;
hence thesis;
end;
then (F (#) G)|A is with_symmetrical_domain quasi_even by A8;
hence thesis by A6,A7;
end;
theorem Th23:
F is_even_on A & G is_even_on A implies F (#) G is_even_on A
proof
assume that
A1: F is_even_on A and
A2: G is_even_on A;
A3: A c= dom G by A2;
A4: G|A is even by A2;
A5: A c= dom F by A1;
then
A6: A c= dom F /\ dom G by A3,XBOOLE_1:19;
A7: dom F /\ dom G=dom (F (#) G) by VALUED_1:def 4;
then
A8: dom((F (#) G)|A) = A by A5,A3,RELAT_1:62,XBOOLE_1:19;
A9: F|A is even by A1;
for x st x in dom((F (#) G)|A) & -x in dom((F (#) G)|A) holds (F (#) G)
|A.(-x)=(F (#) G)|A.x
proof
let x;
assume that
A10: x in dom((F (#) G)|A) and
A11: -x in dom((F (#) G)|A);
A12: x in dom(F|A) by A5,A8,A10,RELAT_1:62;
A13: x in dom(G|A) by A3,A8,A10,RELAT_1:62;
A14: -x in dom(F|A) by A5,A8,A11,RELAT_1:62;
A15: -x in dom(G|A) by A3,A8,A11,RELAT_1:62;
reconsider x as Element of REAL by XREAL_0:def 1;
(F (#) G)|A.(-x)=(F (#) G)|A/.(-x) by A11,PARTFUN1:def 6
.=(F (#) G)/.(-x) by A6,A7,A8,A11,PARTFUN2:17
.=(F (#) G).(-x) by A6,A7,A11,PARTFUN1:def 6
.=F.(-x) * G.(-x) by A6,A7,A11,VALUED_1:def 4
.=F/.(-x) * G.(-x) by A5,A11,PARTFUN1:def 6
.=F/.(-x) * G/.(-x) by A3,A11,PARTFUN1:def 6
.=F|A/.(-x) * G/.(-x) by A5,A8,A11,PARTFUN2:17
.=F|A/.(-x) * G|A/.(-x) by A3,A8,A11,PARTFUN2:17
.=F|A.(-x) * G|A/.(-x) by A14,PARTFUN1:def 6
.=F|A.(-x) * G|A.(-x) by A15,PARTFUN1:def 6
.=F|A.x * G|A.(-x) by A9,A12,A14,Def3
.=F|A.x * G|A.x by A4,A13,A15,Def3
.=F|A/.x * G|A.x by A12,PARTFUN1:def 6
.=F|A/.x * G|A/.x by A13,PARTFUN1:def 6
.=F/.x * G|A/.x by A5,A8,A10,PARTFUN2:17
.=F/.x * G/.x by A3,A8,A10,PARTFUN2:17
.=F.x * G/.x by A5,A10,PARTFUN1:def 6
.=F.x * G.x by A3,A10,PARTFUN1:def 6
.=(F (#) G).x by A6,A7,A10,VALUED_1:def 4
.=(F (#) G)/.x by A6,A7,A10,PARTFUN1:def 6
.=(F (#) G)|A/.x by A6,A7,A8,A10,PARTFUN2:17
.=(F (#) G)|A.x by A10,PARTFUN1:def 6;
hence thesis;
end;
then (F (#) G)|A is with_symmetrical_domain quasi_even by A8;
hence thesis by A6,A7;
end;
theorem
F is_even_on A & G is_odd_on A implies F (#) G is_odd_on A
proof
assume that
A1: F is_even_on A and
A2: G is_odd_on A;
A3: A c= dom G by A2;
A4: G|A is odd by A2;
A5: A c= dom F by A1;
then
A6: A c= dom F /\ dom G by A3,XBOOLE_1:19;
A7: dom F /\ dom G=dom (F (#) G) by VALUED_1:def 4;
then
A8: dom((F (#) G)|A) = A by A5,A3,RELAT_1:62,XBOOLE_1:19;
A9: F|A is even by A1;
for x st x in dom((F (#) G)|A) & -x in dom((F (#) G)|A) holds (F (#) G)
|A.(-x)=-(F (#) G)|A.x
proof
let x;
assume that
A10: x in dom((F (#) G)|A) and
A11: -x in dom((F (#) G)|A);
A12: x in dom(F|A) by A5,A8,A10,RELAT_1:62;
A13: x in dom(G|A) by A3,A8,A10,RELAT_1:62;
A14: -x in dom(F|A) by A5,A8,A11,RELAT_1:62;
A15: -x in dom(G|A) by A3,A8,A11,RELAT_1:62;
reconsider x as Element of REAL by XREAL_0:def 1;
(F (#) G)|A.(-x)=(F (#) G)|A/.(-x) by A11,PARTFUN1:def 6
.=(F (#) G)/.(-x) by A6,A7,A8,A11,PARTFUN2:17
.=(F (#) G).(-x) by A6,A7,A11,PARTFUN1:def 6
.=F.(-x) * G.(-x) by A6,A7,A11,VALUED_1:def 4
.=F/.(-x) * G.(-x) by A5,A11,PARTFUN1:def 6
.=F/.(-x) * G/.(-x) by A3,A11,PARTFUN1:def 6
.=F|A/.(-x) * G/.(-x) by A5,A8,A11,PARTFUN2:17
.=F|A/.(-x) * G|A/.(-x) by A3,A8,A11,PARTFUN2:17
.=F|A.(-x) * G|A/.(-x) by A14,PARTFUN1:def 6
.=F|A.(-x) * G|A.(-x) by A15,PARTFUN1:def 6
.=F|A.x * G|A.(-x) by A9,A12,A14,Def3
.=F|A.x * (-G|A.x) by A4,A13,A15,Def6
.=-(F|A.x * G|A.x)
.=-(F|A/.x * G|A.x) by A12,PARTFUN1:def 6
.=-(F|A/.x * G|A/.x) by A13,PARTFUN1:def 6
.=-(F/.x * G|A/.x) by A5,A8,A10,PARTFUN2:17
.=-(F/.x * G/.x) by A3,A8,A10,PARTFUN2:17
.=-(F.x * G/.x) by A5,A10,PARTFUN1:def 6
.=-(F.x * G.x) by A3,A10,PARTFUN1:def 6
.=-(F (#) G).x by A6,A7,A10,VALUED_1:def 4
.=-(F (#) G)/.x by A6,A7,A10,PARTFUN1:def 6
.=-(F (#) G)|A/.x by A6,A7,A8,A10,PARTFUN2:17
.=-(F (#) G)|A.x by A10,PARTFUN1:def 6;
hence thesis;
end;
then (F (#) G)|A is with_symmetrical_domain quasi_odd by A8;
hence thesis by A6,A7;
end;
theorem
F is_even_on A implies r+F is_even_on A
proof
assume
A1: F is_even_on A;
then
A2: A c= dom F;
then
A3: A c= dom (r+F) by VALUED_1:def 2;
then
A4: dom((r+F)|A) = A by RELAT_1:62;
A5: F|A is even by A1;
for x st x in dom((r+F)|A) & -x in dom((r+F)|A) holds (r+F)|A.(-x)=(r+F) |A.x
proof
let x;
assume that
A6: x in dom((r+F)|A) and
A7: -x in dom((r+F)|A);
A8: x in dom(F|A) by A2,A4,A6,RELAT_1:62;
A9: -x in dom(F|A) by A2,A4,A7,RELAT_1:62;
reconsider x as Element of REAL by XREAL_0:def 1;
(r+F)|A.(-x)=(r+F)|A/.(-x) by A7,PARTFUN1:def 6
.=(r+F)/.(-x) by A3,A4,A7,PARTFUN2:17
.=(r+F).(-x) by A3,A7,PARTFUN1:def 6
.=r + F.(-x) by A3,A7,VALUED_1:def 2
.=r + F/.(-x) by A2,A7,PARTFUN1:def 6
.=r + F|A/.(-x) by A2,A4,A7,PARTFUN2:17
.=r + F|A.(-x) by A9,PARTFUN1:def 6
.=r + F|A.x by A5,A8,A9,Def3
.=r + F|A/.x by A8,PARTFUN1:def 6
.=r + F/.x by A2,A4,A6,PARTFUN2:17
.=r + F.x by A2,A6,PARTFUN1:def 6
.=(r+F).x by A3,A6,VALUED_1:def 2
.=(r+F)/.x by A3,A6,PARTFUN1:def 6
.=(r+F)|A/.x by A3,A4,A6,PARTFUN2:17
.=(r+F)|A.x by A6,PARTFUN1:def 6;
hence thesis;
end;
then (r+F)|A is with_symmetrical_domain quasi_even by A4;
hence thesis by A3;
end;
theorem
F is_even_on A implies F-r is_even_on A
proof
assume
A1: F is_even_on A;
then
A2: A c= dom F;
then
A3: A c= dom (F-r) by VALUED_1:3;
then
A4: dom((F-r)|A) = A by RELAT_1:62;
A5: F|A is even by A1;
for x st x in dom((F-r)|A) & -x in dom((F-r)|A) holds (F-r)|A.(-x)=(F-r) |A.x
proof
let x;
assume that
A6: x in dom((F-r)|A) and
A7: -x in dom((F-r)|A);
A8: x in dom(F|A) by A2,A4,A6,RELAT_1:62;
A9: -x in dom(F|A) by A2,A4,A7,RELAT_1:62;
reconsider x as Element of REAL by XREAL_0:def 1;
(F-r)|A.(-x)=(F-r)|A/.(-x) by A7,PARTFUN1:def 6
.=(F-r)/.(-x) by A3,A4,A7,PARTFUN2:17
.=(F-r).(-x) by A3,A7,PARTFUN1:def 6
.=F.(-x)-r by A2,A7,VALUED_1:3
.=F/.(-x)-r by A2,A7,PARTFUN1:def 6
.=F|A/.(-x)-r by A2,A4,A7,PARTFUN2:17
.=F|A.(-x)-r by A9,PARTFUN1:def 6
.=F|A.x-r by A5,A8,A9,Def3
.=F|A/.x-r by A8,PARTFUN1:def 6
.=F/.x-r by A2,A4,A6,PARTFUN2:17
.=F.x-r by A2,A6,PARTFUN1:def 6
.=(F-r).x by A2,A6,VALUED_1:3
.=(F-r)/.x by A3,A6,PARTFUN1:def 6
.=(F-r)|A/.x by A3,A4,A6,PARTFUN2:17
.=(F-r)|A.x by A6,PARTFUN1:def 6;
hence thesis;
end;
then (F-r)|A is with_symmetrical_domain quasi_even by A4;
hence thesis by A3;
end;
theorem
F is_even_on A implies F^2 is_even_on A by Th23;
theorem
F is_odd_on A implies F^2 is_even_on A by Th22;
theorem
F is_odd_on A & G is_odd_on A implies F /" G is_even_on A
proof
assume that
A1: F is_odd_on A and
A2: G is_odd_on A;
A3: A c= dom G by A2;
A4: G|A is odd by A2;
A5: A c= dom F by A1;
then
A6: A c= dom F /\ dom G by A3,XBOOLE_1:19;
A7: dom F /\ dom G=dom (F /" G) by VALUED_1:16;
then
A8: dom((F /" G)|A) = A by A5,A3,RELAT_1:62,XBOOLE_1:19;
A9: F|A is odd by A1;
for x st x in dom((F /" G)|A) & -x in dom((F /" G)|A) holds (F /" G)|A.
(-x)=(F /" G)|A.x
proof
let x;
assume that
A10: x in dom((F /" G)|A) and
A11: -x in dom((F /" G)|A);
A12: x in dom(F|A) by A5,A8,A10,RELAT_1:62;
A13: x in dom(G|A) by A3,A8,A10,RELAT_1:62;
A14: -x in dom(F|A) by A5,A8,A11,RELAT_1:62;
A15: -x in dom(G|A) by A3,A8,A11,RELAT_1:62;
reconsider x as Element of REAL by XREAL_0:def 1;
(F /" G)|A.(-x)=(F /" G)|A/.(-x) by A11,PARTFUN1:def 6
.=(F /" G)/.(-x) by A6,A7,A8,A11,PARTFUN2:17
.=(F /" G).(-x) by A6,A7,A11,PARTFUN1:def 6
.=F.(-x) / G.(-x) by VALUED_1:17
.=F/.(-x) / G.(-x) by A5,A11,PARTFUN1:def 6
.=F/.(-x) / G/.(-x) by A3,A11,PARTFUN1:def 6
.=F|A/.(-x) / G/.(-x) by A5,A8,A11,PARTFUN2:17
.=F|A/.(-x) / G|A/.(-x) by A3,A8,A11,PARTFUN2:17
.=F|A.(-x) / G|A/.(-x) by A14,PARTFUN1:def 6
.=F|A.(-x) / G|A.(-x) by A15,PARTFUN1:def 6
.=(-F|A.x) / G|A.(-x) by A9,A12,A14,Def6
.=(-F|A.x) / (-G|A.x) by A4,A13,A15,Def6
.=F|A.x / G|A.x by XCMPLX_1:191
.=F|A/.x / G|A.x by A12,PARTFUN1:def 6
.=F|A/.x / G|A/.x by A13,PARTFUN1:def 6
.=F/.x / G|A/.x by A5,A8,A10,PARTFUN2:17
.=F/.x / G/.x by A3,A8,A10,PARTFUN2:17
.=F.x / G/.x by A5,A10,PARTFUN1:def 6
.=F.x / G.x by A3,A10,PARTFUN1:def 6
.=(F /" G).x by VALUED_1:17
.=(F /" G)/.x by A6,A7,A10,PARTFUN1:def 6
.=(F /" G)|A/.x by A6,A7,A8,A10,PARTFUN2:17
.=(F /" G)|A.x by A10,PARTFUN1:def 6;
hence thesis;
end;
then (F /" G)|A is with_symmetrical_domain quasi_even by A8;
hence thesis by A6,A7;
end;
theorem
F is_even_on A & G is_even_on A implies F /" G is_even_on A
proof
assume that
A1: F is_even_on A and
A2: G is_even_on A;
A3: A c= dom G by A2;
A4: G|A is even by A2;
A5: A c= dom F by A1;
then
A6: A c= dom F /\ dom G by A3,XBOOLE_1:19;
A7: dom F /\ dom G=dom (F /" G) by VALUED_1:16;
then
A8: dom((F /" G)|A) = A by A5,A3,RELAT_1:62,XBOOLE_1:19;
A9: F|A is even by A1;
for x st x in dom((F /" G)|A) & -x in dom((F /" G)|A) holds (F /" G)|A.
(-x)=(F /" G)|A.x
proof
let x;
assume that
A10: x in dom((F /" G)|A) and
A11: -x in dom((F /" G)|A);
A12: x in dom(F|A) by A5,A8,A10,RELAT_1:62;
A13: x in dom(G|A) by A3,A8,A10,RELAT_1:62;
A14: -x in dom(F|A) by A5,A8,A11,RELAT_1:62;
A15: -x in dom(G|A) by A3,A8,A11,RELAT_1:62;
reconsider x as Element of REAL by XREAL_0:def 1;
(F /" G)|A.(-x)=(F /" G)|A/.(-x) by A11,PARTFUN1:def 6
.=(F /" G)/.(-x) by A6,A7,A8,A11,PARTFUN2:17
.=(F /" G).(-x) by A6,A7,A11,PARTFUN1:def 6
.=F.(-x) / G.(-x) by VALUED_1:17
.=F/.(-x) / G.(-x) by A5,A11,PARTFUN1:def 6
.=F/.(-x) / G/.(-x) by A3,A11,PARTFUN1:def 6
.=F|A/.(-x) / G/.(-x) by A5,A8,A11,PARTFUN2:17
.=F|A/.(-x) / G|A/.(-x) by A3,A8,A11,PARTFUN2:17
.=F|A.(-x) / G|A/.(-x) by A14,PARTFUN1:def 6
.=F|A.(-x) / G|A.(-x) by A15,PARTFUN1:def 6
.=F|A.x / G|A.(-x) by A9,A12,A14,Def3
.=F|A.x / G|A.x by A4,A13,A15,Def3
.=F|A/.x / G|A.x by A12,PARTFUN1:def 6
.=F|A/.x / G|A/.x by A13,PARTFUN1:def 6
.=F/.x / G|A/.x by A5,A8,A10,PARTFUN2:17
.=F/.x / G/.x by A3,A8,A10,PARTFUN2:17
.=F.x / G/.x by A5,A10,PARTFUN1:def 6
.=F.x / G.x by A3,A10,PARTFUN1:def 6
.=(F /" G).x by VALUED_1:17
.=(F /" G)/.x by A6,A7,A10,PARTFUN1:def 6
.=(F /" G)|A/.x by A6,A7,A8,A10,PARTFUN2:17
.=(F /" G)|A.x by A10,PARTFUN1:def 6;
hence thesis;
end;
then (F /" G)|A is with_symmetrical_domain quasi_even by A8;
hence thesis by A6,A7;
end;
theorem
F is_odd_on A & G is_even_on A implies F /" G is_odd_on A
proof
assume that
A1: F is_odd_on A and
A2: G is_even_on A;
A3: A c= dom G by A2;
A4: G|A is even by A2;
A5: A c= dom F by A1;
then
A6: A c= dom F /\ dom G by A3,XBOOLE_1:19;
A7: dom F /\ dom G=dom (F /" G) by VALUED_1:16;
then
A8: dom((F /" G)|A) = A by A5,A3,RELAT_1:62,XBOOLE_1:19;
A9: F|A is odd by A1;
for x st x in dom((F /" G)|A) & -x in dom((F /" G)|A) holds (F /" G)|A.
(-x)=-(F /" G)|A.x
proof
let x;
assume that
A10: x in dom((F /" G)|A) and
A11: -x in dom((F /" G)|A);
A12: x in dom(F|A) by A5,A8,A10,RELAT_1:62;
A13: x in dom(G|A) by A3,A8,A10,RELAT_1:62;
A14: -x in dom(F|A) by A5,A8,A11,RELAT_1:62;
A15: -x in dom(G|A) by A3,A8,A11,RELAT_1:62;
reconsider x as Element of REAL by XREAL_0:def 1;
(F /" G)|A.(-x)=(F /" G)|A/.(-x) by A11,PARTFUN1:def 6
.=(F /" G)/.(-x) by A6,A7,A8,A11,PARTFUN2:17
.=(F /" G).(-x) by A6,A7,A11,PARTFUN1:def 6
.=F.(-x) / G.(-x) by VALUED_1:17
.=F/.(-x) / G.(-x) by A5,A11,PARTFUN1:def 6
.=F/.(-x) / G/.(-x) by A3,A11,PARTFUN1:def 6
.=F|A/.(-x) / G/.(-x) by A5,A8,A11,PARTFUN2:17
.=F|A/.(-x) / G|A/.(-x) by A3,A8,A11,PARTFUN2:17
.=F|A.(-x) / G|A/.(-x) by A14,PARTFUN1:def 6
.=F|A.(-x) / G|A.(-x) by A15,PARTFUN1:def 6
.=(-F|A.x) / G|A.(-x) by A9,A12,A14,Def6
.=(-F|A.x) / G|A.x by A4,A13,A15,Def3
.=-(F|A.x / G|A.x)
.=-(F|A/.x / G|A.x) by A12,PARTFUN1:def 6
.=-(F|A/.x / G|A/.x) by A13,PARTFUN1:def 6
.=-(F/.x / G|A/.x) by A5,A8,A10,PARTFUN2:17
.=-(F/.x / G/.x) by A3,A8,A10,PARTFUN2:17
.=-(F.x / G/.x) by A5,A10,PARTFUN1:def 6
.=-(F.x / G.x) by A3,A10,PARTFUN1:def 6
.=-(F /" G).x by VALUED_1:17
.=-(F /" G)/.x by A6,A7,A10,PARTFUN1:def 6
.=-(F /" G)|A/.x by A6,A7,A8,A10,PARTFUN2:17
.=-(F /" G)|A.x by A10,PARTFUN1:def 6;
hence thesis;
end;
then (F /" G)|A is with_symmetrical_domain quasi_odd by A8;
hence thesis by A6,A7;
end;
theorem
F is_even_on A & G is_odd_on A implies F /" G is_odd_on A
proof
assume that
A1: F is_even_on A and
A2: G is_odd_on A;
A3: A c= dom G by A2;
A4: G|A is odd by A2;
A5: A c= dom F by A1;
then
A6: A c= dom F /\ dom G by A3,XBOOLE_1:19;
A7: dom F /\ dom G=dom (F /" G) by VALUED_1:16;
then
A8: dom((F /" G)|A) = A by A5,A3,RELAT_1:62,XBOOLE_1:19;
A9: F|A is even by A1;
for x st x in dom((F /" G)|A) & -x in dom((F /" G)|A) holds (F /" G)|A.
(-x)=-(F /" G)|A.x
proof
let x;
assume that
A10: x in dom((F /" G)|A) and
A11: -x in dom((F /" G)|A);
A12: x in dom(F|A) by A5,A8,A10,RELAT_1:62;
A13: x in dom(G|A) by A3,A8,A10,RELAT_1:62;
A14: -x in dom(F|A) by A5,A8,A11,RELAT_1:62;
A15: -x in dom(G|A) by A3,A8,A11,RELAT_1:62;
reconsider x as Element of REAL by XREAL_0:def 1;
(F /" G)|A.(-x)=(F /" G)|A/.(-x) by A11,PARTFUN1:def 6
.=(F /" G)/.(-x) by A6,A7,A8,A11,PARTFUN2:17
.=(F /" G).(-x) by A6,A7,A11,PARTFUN1:def 6
.=F.(-x) / G.(-x) by VALUED_1:17
.=F/.(-x) / G.(-x) by A5,A11,PARTFUN1:def 6
.=F/.(-x) / G/.(-x) by A3,A11,PARTFUN1:def 6
.=F|A/.(-x) / G/.(-x) by A5,A8,A11,PARTFUN2:17
.=F|A/.(-x) / G|A/.(-x) by A3,A8,A11,PARTFUN2:17
.=F|A.(-x) / G|A/.(-x) by A14,PARTFUN1:def 6
.=F|A.(-x) / G|A.(-x) by A15,PARTFUN1:def 6
.=F|A.x / G|A.(-x) by A9,A12,A14,Def3
.=F|A.x / (-G|A.x) by A4,A13,A15,Def6
.=-(F|A.x / G|A.x) by XCMPLX_1:188
.=-(F|A/.x / G|A.x) by A12,PARTFUN1:def 6
.=-(F|A/.x / G|A/.x) by A13,PARTFUN1:def 6
.=-(F/.x / G|A/.x) by A5,A8,A10,PARTFUN2:17
.=-(F/.x / G/.x) by A3,A8,A10,PARTFUN2:17
.=-(F.x / G/.x) by A5,A10,PARTFUN1:def 6
.=-(F.x / G.x) by A3,A10,PARTFUN1:def 6
.=-(F /" G).x by VALUED_1:17
.=-(F /" G)/.x by A6,A7,A10,PARTFUN1:def 6
.=-(F /" G)|A/.x by A6,A7,A8,A10,PARTFUN2:17
.=-(F /" G)|A.x by A10,PARTFUN1:def 6;
hence thesis;
end;
then (F /" G)|A is with_symmetrical_domain quasi_odd by A8;
hence thesis by A6,A7;
end;
theorem
F is odd implies -F is odd
proof
A1: dom F=dom(-F) by VALUED_1:8;
assume
A2: F is odd;
for x st x in dom(-F) & -x in dom(-F) holds (-F).(-x)=-(-F).x
proof
let x;
assume
A3: x in dom(-F) & -x in dom(-F);
(-F).(-x)=-F.(-x) by VALUED_1:8
.=-(-F.x) by A2,A1,A3,Def6
.=-(-F).x by VALUED_1:8;
hence thesis;
end;
then -F is with_symmetrical_domain quasi_odd by A2,A1;
hence thesis;
end;
theorem
F is even implies -F is even
proof
A1: dom F=dom(-F) by VALUED_1:8;
assume
A2: F is even;
for x st x in dom(-F) & -x in dom(-F) holds (-F).(-x)=(-F).x
proof
let x;
assume
A3: x in dom(-F) & -x in dom(-F);
(-F).(-x)=-F.(-x) by VALUED_1:8
.=-F.x by A2,A1,A3,Def3
.=(-F).x by VALUED_1:8;
hence thesis;
end;
then -F is with_symmetrical_domain quasi_even by A2,A1;
hence thesis;
end;
theorem
F is odd implies F" is odd
proof
A1: dom F=dom(F") by VALUED_1:def 7;
assume
A2: F is odd;
for x st x in dom(F") & -x in dom(F") holds (F").(-x)=-(F").x
proof
let x;
assume that
A3: x in dom(F") and
A4: -x in dom(F");
(F").(-x)=(F.(-x))" by A4,VALUED_1:def 7
.=(-F.x)" by A2,A1,A3,A4,Def6
.=-(F.x)" by XCMPLX_1:222
.=-(F").x by A3,VALUED_1:def 7;
hence thesis;
end;
then F" is with_symmetrical_domain quasi_odd by A2,A1;
hence thesis;
end;
theorem
F is even implies F" is even
proof
A1: dom F=dom(F") by VALUED_1:def 7;
assume
A2: F is even;
for x st x in dom(F") & -x in dom(F") holds (F").(-x)=(F").x
proof
let x;
assume that
A3: x in dom(F") and
A4: -x in dom(F");
(F").(-x)=(F.(-x))" by A4,VALUED_1:def 7
.=(F.x)" by A2,A1,A3,A4,Def3
.=(F").x by A3,VALUED_1:def 7;
hence thesis;
end;
then F" is with_symmetrical_domain quasi_even by A2,A1;
hence thesis;
end;
theorem
F is odd implies |. F .| is even
proof
A1: dom F=dom(|. F .|) by VALUED_1:def 11;
assume
A2: F is odd;
for x st x in dom(|. F .|) & -x in dom(|. F .|) holds (|. F .|).(-x)=(|.
F .|).x
proof
let x;
assume that
A3: x in dom(|. F .|) and
A4: -x in dom(|. F .|);
(|. F .|).(-x)=|. F.(-x) .| by A4,VALUED_1:def 11
.=|. -F.x .| by A2,A1,A3,A4,Def6
.=|. F.x .| by COMPLEX1:52
.=(|. F .|).x by A3,VALUED_1:def 11;
hence thesis;
end;
then |. F .| is with_symmetrical_domain quasi_even by A2,A1;
hence thesis;
end;
theorem
F is even implies |. F .| is even
proof
A1: dom F=dom(|. F .|) by VALUED_1:def 11;
assume
A2: F is even;
for x st x in dom(|. F .|) & -x in dom(|. F .|) holds (|. F .|).(-x)=(|.
F .|).x
proof
let x;
assume that
A3: x in dom(|. F .|) and
A4: -x in dom(|. F .|);
(|. F .|).(-x)=|. F.(-x) .| by A4,VALUED_1:def 11
.=|. F.x .| by A2,A1,A3,A4,Def3
.=(|. F .|).x by A3,VALUED_1:def 11;
hence thesis;
end;
then |. F .| is with_symmetrical_domain quasi_even by A2,A1;
hence thesis;
end;
theorem
F is odd implies F^2 is even
proof
A1: dom F=dom(F^2) by VALUED_1:11;
assume
A2: F is odd;
for x st x in dom(F^2) & -x in dom(F^2) holds (F^2).(-x)=(F^2).x
proof
let x;
assume
A3: x in dom(F^2) & -x in dom(F^2);
(F^2).(-x)=(F.(-x))^2 by VALUED_1:11
.=(-F.x)^2 by A2,A1,A3,Def6
.=(F.x)^2
.=(F^2).x by VALUED_1:11;
hence thesis;
end;
then F^2 is with_symmetrical_domain quasi_even by A2,A1;
hence thesis;
end;
theorem
F is even implies F^2 is even
proof
A1: dom F=dom(F^2) by VALUED_1:11;
assume
A2: F is even;
for x st x in dom(F^2) & -x in dom(F^2) holds (F^2).(-x)=(F^2).x
proof
let x;
assume
A3: x in dom(F^2) & -x in dom(F^2);
(F^2).(-x)=(F.(-x))^2 by VALUED_1:11
.=(F.x)^2 by A2,A1,A3,Def3
.=(F^2).x by VALUED_1:11;
hence thesis;
end;
then F^2 is with_symmetrical_domain quasi_even by A2,A1;
hence thesis;
end;
theorem
F is even implies r+F is even
proof
A1: dom F=dom(r+F ) by VALUED_1:def 2;
assume
A2: F is even;
for x st x in dom(r+F) & -x in dom(r+F) holds (r+F).(-x)=(r+F).x
proof
let x;
assume that
A3: x in dom(r+F) and
A4: -x in dom(r+F);
(r+F).(-x)=r+F.(-x) by A4,VALUED_1:def 2
.=r+F.x by A2,A1,A3,A4,Def3
.=(r+F).x by A3,VALUED_1:def 2;
hence thesis;
end;
then r+F is with_symmetrical_domain quasi_even by A2,A1;
hence thesis;
end;
theorem
F is even implies F-r is even
proof
A1: dom F=dom(F-r ) by VALUED_1:3;
assume
A2: F is even;
for x st x in dom(F-r) & -x in dom(F-r) holds (F-r).(-x)=(F-r).x
proof
let x;
assume that
A3: x in dom(F-r) and
A4: -x in dom(F-r);
A5: x in dom F by A3,VALUED_1:3;
-x in dom F by A4,VALUED_1:3;
then (F-r).(-x)=F.(-x)-r by VALUED_1:3
.=F.x -r by A2,A1,A3,A4,Def3
.=(F-r).x by A5,VALUED_1:3;
hence thesis;
end;
then F-r is with_symmetrical_domain quasi_even by A2,A1;
hence thesis;
end;
theorem
F is odd implies r (#) F is odd
proof
A1: dom F=dom( r (#) F) by VALUED_1:def 5;
assume
A2: F is odd;
for x st x in dom( r (#) F) & -x in dom( r (#) F) holds ( r (#) F).(-x)=
-( r (#) F).x
proof
let x;
assume that
A3: x in dom( r (#) F) and
A4: -x in dom( r (#) F);
( r (#) F).(-x)=r * F.(-x) by A4,VALUED_1:def 5
.=r * (-F.x) by A2,A1,A3,A4,Def6
.=-(r * F.x)
.=-(r (#) F).x by A3,VALUED_1:def 5;
hence thesis;
end;
then r (#) F is with_symmetrical_domain quasi_odd by A2,A1;
hence thesis;
end;
theorem
F is even implies r (#) F is even
proof
A1: dom F=dom(r (#) F) by VALUED_1:def 5;
assume
A2: F is even;
for x st x in dom(r (#) F) & -x in dom(r (#) F) holds (r (#) F).(-x)=(r
(#) F).x
proof
let x;
assume that
A3: x in dom(r (#) F) and
A4: -x in dom(r (#) F);
(r (#) F).(-x)=r * F.(-x) by A4,VALUED_1:def 5
.=r * F.x by A2,A1,A3,A4,Def3
.=( r (#) F).x by A3,VALUED_1:def 5;
hence thesis;
end;
then r (#) F is with_symmetrical_domain quasi_even by A2,A1;
hence thesis;
end;
theorem
F is odd & G is odd & dom F /\ dom G is symmetrical implies F + G is odd
proof
assume that
A1: F is odd and
A2: G is odd and
A3: dom F /\ dom G is symmetrical;
A4: dom F /\ dom G=dom (F + G) by VALUED_1:def 1;
then
A5: dom (F + G) c= dom G by XBOOLE_1:17;
A6: dom (F + G) c= dom F by A4,XBOOLE_1:17;
for x st x in dom(F + G) & -x in dom(F + G) holds (F + G).(-x)=-(F + G). x
proof
let x;
assume that
A7: x in dom(F + G) and
A8: -x in dom(F + G);
(F + G).(-x)=F.(-x) + G.(-x) by A8,VALUED_1:def 1
.=(-F.x) + G.(-x) by A1,A6,A7,A8,Def6
.=(-F.x) + (-G.x) by A2,A5,A7,A8,Def6
.=-(F.x + G.x)
.=-(F + G).x by A7,VALUED_1:def 1;
hence thesis;
end;
then (F + G) is with_symmetrical_domain quasi_odd by A3,A4;
hence thesis;
end;
theorem
F is even & G is even & dom F /\ dom G is symmetrical implies F + G is even
proof
assume that
A1: F is even and
A2: G is even and
A3: dom F /\ dom G is symmetrical;
A4: dom F /\ dom G=dom (F + G) by VALUED_1:def 1;
then
A5: dom (F + G) c= dom G by XBOOLE_1:17;
A6: dom (F + G) c= dom F by A4,XBOOLE_1:17;
for x st x in dom(F + G) & -x in dom(F + G) holds (F + G).(-x)=(F + G).x
proof
let x;
assume that
A7: x in dom(F + G) and
A8: -x in dom(F + G);
(F + G).(-x)=F.(-x) + G.(-x) by A8,VALUED_1:def 1
.=F.x + G.(-x) by A1,A6,A7,A8,Def3
.=F.x + G.x by A2,A5,A7,A8,Def3
.=(F + G).x by A7,VALUED_1:def 1;
hence thesis;
end;
then (F + G) is with_symmetrical_domain quasi_even by A3,A4;
hence thesis;
end;
theorem
F is odd & G is odd & dom F /\ dom G is symmetrical implies F - G is odd
proof
assume that
A1: F is odd and
A2: G is odd and
A3: dom F /\ dom G is symmetrical;
A4: dom F /\ dom G=dom (F - G) by VALUED_1:12;
then
A5: dom (F - G) c= dom G by XBOOLE_1:17;
A6: dom (F - G) c= dom F by A4,XBOOLE_1:17;
for x st x in dom(F - G) & -x in dom(F - G) holds (F - G).(-x)=-(F - G). x
proof
let x;
assume that
A7: x in dom(F - G) and
A8: -x in dom(F - G);
(F - G).(-x)=F.(-x) - G.(-x) by A8,VALUED_1:13
.=(-F.x) - G.(-x) by A1,A6,A7,A8,Def6
.=(-F.x) - (-G.x) by A2,A5,A7,A8,Def6
.=-(F.x - G.x)
.=-(F - G).x by A7,VALUED_1:13;
hence thesis;
end;
then (F - G) is with_symmetrical_domain quasi_odd by A3,A4;
hence thesis;
end;
theorem
F is even & G is even & dom F /\ dom G is symmetrical implies F - G is even
proof
assume that
A1: F is even and
A2: G is even and
A3: dom F /\ dom G is symmetrical;
A4: dom F /\ dom G=dom (F - G) by VALUED_1:12;
then
A5: dom (F - G) c= dom G by XBOOLE_1:17;
A6: dom (F - G) c= dom F by A4,XBOOLE_1:17;
for x st x in dom(F - G) & -x in dom(F - G) holds (F - G).(-x)=(F - G).x
proof
let x;
assume that
A7: x in dom(F - G) and
A8: -x in dom(F - G);
(F - G).(-x)=F.(-x) - G.(-x) by A8,VALUED_1:13
.=F.x - G.(-x) by A1,A6,A7,A8,Def3
.=F.x - G.x by A2,A5,A7,A8,Def3
.=(F - G).x by A7,VALUED_1:13;
hence thesis;
end;
then (F - G) is with_symmetrical_domain quasi_even by A3,A4;
hence thesis;
end;
theorem
F is odd & G is odd & dom F /\ dom G is symmetrical implies F (#) G is even
proof
assume that
A1: F is odd and
A2: G is odd and
A3: dom F /\ dom G is symmetrical;
A4: dom F /\ dom G=dom (F (#) G) by VALUED_1:def 4;
then
A5: dom (F (#) G) c= dom G by XBOOLE_1:17;
A6: dom (F (#) G) c= dom F by A4,XBOOLE_1:17;
for x st x in dom(F (#) G) & -x in dom(F (#) G) holds (F (#) G).(-x)=(F
(#) G).x
proof
let x;
assume that
A7: x in dom(F (#) G) and
A8: -x in dom(F (#) G);
(F (#) G).(-x)=F.(-x) * G.(-x) by A8,VALUED_1:def 4
.=(-F.x) * G.(-x) by A1,A6,A7,A8,Def6
.=(-F.x) * (-G.x) by A2,A5,A7,A8,Def6
.=(F.x * G.x)
.=(F (#) G).x by A7,VALUED_1:def 4;
hence thesis;
end;
then (F (#) G) is with_symmetrical_domain quasi_even by A3,A4;
hence thesis;
end;
theorem
F is even & G is even & dom F /\ dom G is symmetrical implies F (#) G is even
proof
assume that
A1: F is even and
A2: G is even and
A3: dom F /\ dom G is symmetrical;
A4: dom F /\ dom G=dom (F (#) G) by VALUED_1:def 4;
then
A5: dom (F (#) G) c= dom G by XBOOLE_1:17;
A6: dom (F (#) G) c= dom F by A4,XBOOLE_1:17;
for x st x in dom(F (#) G) & -x in dom(F (#) G) holds (F (#) G).(-x)=(F
(#) G).x
proof
let x;
assume that
A7: x in dom(F (#) G) and
A8: -x in dom(F (#) G);
(F (#) G).(-x)=F.(-x) * G.(-x) by A8,VALUED_1:def 4
.=(F.x) * G.(-x) by A1,A6,A7,A8,Def3
.=(F.x * G.x) by A2,A5,A7,A8,Def3
.=(F (#) G).x by A7,VALUED_1:def 4;
hence thesis;
end;
then (F (#) G) is with_symmetrical_domain quasi_even by A3,A4;
hence thesis;
end;
theorem
F is even & G is odd & dom F /\ dom G is symmetrical implies F (#) G is odd
proof
assume that
A1: F is even and
A2: G is odd and
A3: dom F /\ dom G is symmetrical;
A4: dom F /\ dom G=dom (F (#) G) by VALUED_1:def 4;
then
A5: dom (F (#) G) c= dom G by XBOOLE_1:17;
A6: dom (F (#) G) c= dom F by A4,XBOOLE_1:17;
for x st x in dom(F (#) G) & -x in dom(F (#) G) holds (F (#) G).(-x)=-(F
(#) G).x
proof
let x;
assume that
A7: x in dom(F (#) G) and
A8: -x in dom(F (#) G);
(F (#) G).(-x)=F.(-x) * G.(-x) by A8,VALUED_1:def 4
.=F.x * G.(-x) by A1,A6,A7,A8,Def3
.=F.x * (-G.x) by A2,A5,A7,A8,Def6
.=-(F.x * G.x)
.=-(F (#) G).x by A7,VALUED_1:def 4;
hence thesis;
end;
then (F (#) G) is with_symmetrical_domain quasi_odd by A3,A4;
hence thesis;
end;
theorem
F is odd & G is odd & dom F /\ dom G is symmetrical implies F /" G is even
proof
assume that
A1: F is odd and
A2: G is odd and
A3: dom F /\ dom G is symmetrical;
A4: dom F /\ dom G=dom (F /" G) by VALUED_1:16;
then
A5: dom (F /" G) c= dom G by XBOOLE_1:17;
A6: dom (F /" G) c= dom F by A4,XBOOLE_1:17;
for x st x in dom(F /" G) & -x in dom(F /" G) holds (F /" G).(-x)=(F /" G).x
proof
let x;
assume
A7: x in dom(F /" G) & -x in dom(F /" G);
(F /" G).(-x)=F.(-x) / G.(-x) by VALUED_1:17
.=(-F.x) / G.(-x) by A1,A6,A7,Def6
.=(-F.x) / (-G.x) by A2,A5,A7,Def6
.=(F.x / G.x) by XCMPLX_1:191
.=(F /" G).x by VALUED_1:17;
hence thesis;
end;
then (F /" G) is with_symmetrical_domain quasi_even by A3,A4;
hence thesis;
end;
theorem
F is even & G is even & dom F /\ dom G is symmetrical implies F /" G is even
proof
assume that
A1: F is even and
A2: G is even and
A3: dom F /\ dom G is symmetrical;
A4: dom F /\ dom G=dom (F /" G) by VALUED_1:16;
then
A5: dom (F /" G) c= dom G by XBOOLE_1:17;
A6: dom (F /" G) c= dom F by A4,XBOOLE_1:17;
for x st x in dom(F /" G) & -x in dom(F /" G) holds (F /" G).(-x)=(F /" G).x
proof
let x;
assume
A7: x in dom(F /" G) & -x in dom(F /" G);
(F /" G).(-x)=F.(-x) / G.(-x) by VALUED_1:17
.=(F.x) / G.(-x) by A1,A6,A7,Def3
.=(F.x / G.x) by A2,A5,A7,Def3
.=(F /" G).x by VALUED_1:17;
hence thesis;
end;
then (F /" G) is with_symmetrical_domain quasi_even by A3,A4;
hence thesis;
end;
theorem
F is odd & G is even & dom F /\ dom G is symmetrical implies F /" G is odd
proof
assume that
A1: F is odd and
A2: G is even and
A3: dom F /\ dom G is symmetrical;
A4: dom F /\ dom G=dom (F /" G) by VALUED_1:16;
then
A5: dom (F /" G) c= dom G by XBOOLE_1:17;
A6: dom (F /" G) c= dom F by A4,XBOOLE_1:17;
for x st x in dom(F /" G) & -x in dom(F /" G) holds (F /" G).(-x)=-(F /" G).x
proof
let x;
assume
A7: x in dom(F /" G) & -x in dom(F /" G);
(F /" G).(-x)=F.(-x) / G.(-x) by VALUED_1:17
.=(-F.x) / G.(-x) by A1,A6,A7,Def6
.=(-F.x) / G.x by A2,A5,A7,Def3
.=-(F.x / G.x)
.=-(F /" G).x by VALUED_1:17;
hence thesis;
end;
then (F /" G) is with_symmetrical_domain quasi_odd by A3,A4;
hence thesis;
end;
theorem
F is even & G is odd & dom F /\ dom G is symmetrical implies F /" G is odd
proof
assume that
A1: F is even and
A2: G is odd and
A3: dom F /\ dom G is symmetrical;
A4: dom F /\ dom G=dom (F /" G) by VALUED_1:16;
then
A5: dom (F /" G) c= dom G by XBOOLE_1:17;
A6: dom (F /" G) c= dom F by A4,XBOOLE_1:17;
for x st x in dom(F /" G) & -x in dom(F /" G) holds (F /" G).(-x)=-(F /" G).x
proof
let x;
assume
A7: x in dom(F /" G) & -x in dom(F /" G);
(F /" G).(-x)=F.(-x) / G.(-x) by VALUED_1:17
.=F.x / G.(-x) by A1,A6,A7,Def3
.=F.x / (-G.x) by A2,A5,A7,Def6
.=-(F.x / G.x) by XCMPLX_1:188
.=-(F /" G).x by VALUED_1:17;
hence thesis;
end;
then (F /" G) is with_symmetrical_domain quasi_odd by A3,A4;
hence thesis;
end;
begin :: Examples
definition
func signum -> Function of REAL, REAL means
:Def9:
for x being Real holds it .x = sgn x;
existence
proof
deffunc U(Real) = In(sgn$1,REAL);
consider f being Function of REAL, REAL such that
A1: for x being Element of REAL holds f.x = U(x) from FUNCT_2:sch 4;
take f;
let x be Real;
x in REAL by XREAL_0:def 1;
then f.x = U(x) by A1;
hence thesis;
end;
uniqueness
proof
let f1,f2 be Function of REAL, REAL;
assume
A2: for x being Real holds f1.x=sgn x;
assume
A3: for x being Real holds f2.x=sgn x;
for x being Element of REAL holds f1.x = f2.x
proof
let x be Element of REAL;
thus f1.x=sgn x by A2
.=f2.x by A3;
end;
hence f1=f2 by FUNCT_2:63;
end;
end;
theorem Th56:
for x being Real st x > 0 holds signum.x = 1
proof
let x be Real;
assume
A1: 0 < x;
signum.x = sgn x by Def9
.= 1 by A1,ABSVALUE:def 2;
hence thesis;
end;
theorem Th57:
for x being Real st x < 0 holds signum.x = -1
proof
let x be Real;
assume
A1: 0 > x;
signum.x = sgn x by Def9
.= -1 by A1,ABSVALUE:def 2;
hence thesis;
end;
theorem Th58:
signum.0 = 0
proof
signum.0 = sgn 0 by Def9
.= 0 by ABSVALUE:def 2;
hence thesis;
end;
theorem Th59:
for x being Real holds signum.(-x) = -signum.x
proof
let x be Real;
per cases;
suppose
A1: x < 0;
then signum.x = -1 by Th57;
hence thesis by A1,Th56;
end;
suppose
A2: 0 < x;
then signum.x = 1 by Th56;
hence thesis by A2,Th57;
end;
suppose x = 0;
hence thesis by Th58;
end;
end;
theorem
for A being symmetrical Subset of REAL holds signum is_odd_on A
proof
let A be symmetrical Subset of REAL;
A1: dom signum = REAL by FUNCT_2:def 1;
then
A2: dom(signum|A) = A by RELAT_1:62;
for x st x in dom(signum|A) & -x in dom(signum|A) holds signum|A.(-x)=-
signum|A.x
proof
let x;
assume that
A3: x in dom(signum|A) and
A4: -x in dom(signum|A);
reconsider x as Element of REAL by XREAL_0:def 1;
signum|A.(-x)=signum|A/.(-x) by A4,PARTFUN1:def 6
.=signum/.(-x) by A1,A4,PARTFUN2:17
.=-signum/.x by Th59
.=-signum|A/.x by A1,A3,PARTFUN2:17
.=-signum|A.x by A3,PARTFUN1:def 6;
hence thesis;
end;
then signum|A is with_symmetrical_domain quasi_odd by A2;
hence thesis by A1;
end;
theorem Th61:
for x being Real st x >= 0 holds absreal.x = x
proof
let x be Real;
assume
A1: 0 <= x;
absreal.x = |.x.| by EUCLID:def 2
.= x by A1,ABSVALUE:def 1;
hence thesis;
end;
theorem Th62:
for x being Real st x < 0 holds absreal.x = -x
proof
let x be Real;
assume
A1: 0 > x;
absreal.x = |.x.| by EUCLID:def 2
.= -x by A1,ABSVALUE:def 1;
hence thesis;
end;
theorem Th63:
for x being Real holds absreal.(-x) = absreal.x
proof
let x be Real;
per cases;
suppose
A1: x < 0;
then absreal.(-x) = -x by Th61;
hence thesis by A1,Th62;
end;
suppose
A2: 0 < x;
then absreal.(-x) = -(-x) by Th62
.=x;
hence thesis by A2,Th61;
end;
suppose
x = 0;
hence thesis;
end;
end;
theorem
for A being symmetrical Subset of REAL holds absreal is_even_on A
proof
let A be symmetrical Subset of REAL;
A1: dom absreal = REAL by FUNCT_2:def 1;
then
A2: dom(absreal|A) = A by RELAT_1:62;
for x st x in dom(absreal|A) & -x in dom(absreal|A) holds absreal|A.(-x)
=absreal|A.x
proof
let x;
assume that
A3: x in dom(absreal|A) and
A4: -x in dom(absreal|A);
reconsider x as Element of REAL by XREAL_0:def 1;
absreal|A.(-x)=absreal|A/.(-x) by A4,PARTFUN1:def 6
.=absreal/.(-x) by A1,A4,PARTFUN2:17
.=absreal/.x by Th63
.=absreal|A/.x by A1,A3,PARTFUN2:17
.=absreal|A.x by A3,PARTFUN1:def 6;
hence thesis;
end;
then absreal|A is with_symmetrical_domain quasi_even by A2;
hence thesis by A1;
end;
theorem Th65:
for A being symmetrical Subset of REAL holds sin is_odd_on A
proof
let A be symmetrical Subset of REAL;
A1: dom(sin|A) = A by RELAT_1:62,SIN_COS:24;
for x st x in dom(sin|A) & -x in dom(sin|A) holds sin|A.(-x)=-sin|A.x
proof
let x;
assume that
A2: x in dom(sin|A) and
A3: -x in dom(sin|A);
reconsider x as Element of REAL by XREAL_0:def 1;
sin|A.(-x)=sin|A/.(-x) by A3,PARTFUN1:def 6
.=sin/.(-x) by A3,PARTFUN2:17,SIN_COS:24
.=-sin/.x by SIN_COS:30
.=-sin|A/.x by A2,PARTFUN2:17,SIN_COS:24
.=-sin|A.x by A2,PARTFUN1:def 6;
hence thesis;
end;
then sin|A is with_symmetrical_domain quasi_odd by A1;
hence thesis by SIN_COS:24;
end;
theorem Th66:
for A being symmetrical Subset of REAL holds cos is_even_on A
proof
let A be symmetrical Subset of REAL;
A1: dom(cos|A) = A by RELAT_1:62,SIN_COS:24;
for x st x in dom(cos|A) & -x in dom(cos|A) holds cos|A.(-x)=cos|A.x
proof
let x;
assume that
A2: x in dom(cos|A) and
A3: -x in dom(cos|A);
reconsider x as Element of REAL by XREAL_0:def 1;
cos|A.(-x)=cos|A/.(-x) by A3,PARTFUN1:def 6
.=cos/.(-x) by A3,PARTFUN2:17,SIN_COS:24
.=cos/.x by SIN_COS:30
.=cos|A/.x by A2,PARTFUN2:17,SIN_COS:24
.=cos|A.x by A2,PARTFUN1:def 6;
hence thesis;
end;
then cos|A is with_symmetrical_domain quasi_even by A1;
hence thesis by SIN_COS:24;
end;
registration
cluster sin -> odd;
coherence
proof
for x being Complex st x in REAL holds -x in REAL by XREAL_0:def 1;
then
(for x st x in dom sin & -x in dom sin holds sin.(-x)=-sin.x)& REAL is
symmetrical by SIN_COS:30;
then sin is with_symmetrical_domain quasi_odd by SIN_COS:24;
hence thesis;
end;
end;
registration
cluster cos -> even;
coherence
proof
for x st x in dom cos & -x in dom cos holds cos.(-x)=cos.x by SIN_COS:30;
then cos is with_symmetrical_domain quasi_even by SIN_COS:24;
hence thesis;
end;
end;
theorem
for A being symmetrical Subset of REAL holds sinh is_odd_on A
proof
let A be symmetrical Subset of REAL;
A1: dom sinh = REAL by FUNCT_2:def 1;
then
A2: dom(sinh|A) = A by RELAT_1:62;
for x st x in dom(sinh|A) & -x in dom(sinh|A) holds sinh|A.(-x)=-sinh|A. x
proof
let x;
assume that
A3: x in dom(sinh|A) and
A4: -x in dom(sinh|A);
reconsider x as Element of REAL by XREAL_0:def 1;
sinh|A.(-x)=sinh|A/.(-x) by A4,PARTFUN1:def 6
.=sinh/.(-x) by A1,A4,PARTFUN2:17
.=-sinh/.x by SIN_COS2:19
.=-sinh|A/.x by A1,A3,PARTFUN2:17
.=-sinh|A.x by A3,PARTFUN1:def 6;
hence thesis;
end;
then sinh|A is with_symmetrical_domain quasi_odd by A2;
hence thesis by A1;
end;
theorem
for A being symmetrical Subset of REAL holds cosh is_even_on A
proof
let A be symmetrical Subset of REAL;
A1: dom cosh = REAL by FUNCT_2:def 1;
then
A2: dom(cosh|A) = A by RELAT_1:62;
for x st x in dom(cosh|A) & -x in dom(cosh|A) holds cosh|A.(-x)=cosh|A.x
proof
let x;
assume that
A3: x in dom(cosh|A) and
A4: -x in dom(cosh|A);
reconsider x as Element of REAL by XREAL_0:def 1;
cosh|A.(-x)=cosh|A/.(-x) by A4,PARTFUN1:def 6
.=cosh/.(-x) by A1,A4,PARTFUN2:17
.=cosh/.x by SIN_COS2:19
.=cosh|A/.x by A1,A3,PARTFUN2:17
.=cosh|A.x by A3,PARTFUN1:def 6;
hence thesis;
end;
then cosh|A is with_symmetrical_domain quasi_even by A2;
hence thesis by A1;
end;
registration
cluster sinh -> odd;
coherence
proof
for x being Complex st x in REAL holds -x in REAL by XREAL_0:def 1;
then
A1: REAL is symmetrical;
(for x st x in dom sinh & -x in dom sinh holds sinh.(-x)=-sinh.x)& dom
(sinh)= REAL by FUNCT_2:def 1,SIN_COS2:19;
then sinh is with_symmetrical_domain quasi_odd by A1;
hence thesis;
end;
end;
registration
cluster cosh -> even;
coherence
proof
for x being Complex st x in REAL holds -x in REAL by XREAL_0:def 1;
then
A1: REAL is symmetrical;
(for x st x in dom cosh & -x in dom cosh holds cosh.(-x)=cosh.x)& dom
(cosh)= REAL by FUNCT_2:def 1,SIN_COS2:19;
then cosh is with_symmetrical_domain quasi_even by A1;
hence thesis;
end;
end;
theorem
A c= ].-PI/2,PI/2.[ implies tan is_odd_on A
proof
assume
A1: A c= ].-PI/2,PI/2.[;
then
A2: A c= dom (tan) by SIN_COS9:1;
A3: dom(tan|A) = A by A1,RELAT_1:62,SIN_COS9:1,XBOOLE_1:1;
A4: for x st x in A holds tan.(-x) = -tan.x
proof
let x;
assume
A5: x in A;
then -x in A by Def1;
then tan.(-x)=tan (-x) by A1,SIN_COS9:13
.= -tan x by SIN_COS4:1
.= -tan.x by A1,A5,SIN_COS9:13;
hence thesis;
end;
for x st x in dom(tan|A) & -x in dom(tan|A) holds tan|A.(-x)=-tan|A.x
proof
let x;
assume that
A6: x in dom(tan|A) and
A7: -x in dom(tan|A);
reconsider x as Element of REAL by XREAL_0:def 1;
tan|A.(-x)=tan|A/.(-x) by A7,PARTFUN1:def 6
.=tan/.(-x) by A2,A3,A7,PARTFUN2:17
.=tan.(-x) by A2,A7,PARTFUN1:def 6
.=-tan.x by A4,A6
.=-tan/.x by A2,A6,PARTFUN1:def 6
.=-tan|A/.x by A2,A3,A6,PARTFUN2:17
.=-tan|A.x by A6,PARTFUN1:def 6;
hence thesis;
end;
then tan|A is with_symmetrical_domain quasi_odd by A3;
hence thesis by A2;
end;
theorem
A c= dom tan implies tan is_odd_on A
proof
assume that
A1: A c= dom tan;
A2: dom(tan|A) = A by A1,RELAT_1:62;
A3: for x st x in A holds tan.(-x) = -tan.x
proof
let x;
assume
A4: x in A; then
A5: cos.x <> 0 by A1,FDIFF_8:1;
-x in A by Def1,A4; then
tan.(-x) = tan (-x) by A1,FDIFF_8:1,SIN_COS9:15
.=-tan x by SIN_COS4:1
.=-tan.x by A5,SIN_COS9:15;
hence thesis;
end;
for x st x in dom(tan|A) & -x in dom(tan|A) holds tan|A.(-x)=-tan|A.x
proof
let x;
assume that
A6: x in dom(tan|A) and
A7: -x in dom(tan|A);
reconsider x as Element of REAL by XREAL_0:def 1;
tan|A.(-x)=tan|A/.(-x) by A7,PARTFUN1:def 6
.=tan/.(-x) by A1,A2,A7,PARTFUN2:17
.=tan.(-x) by A1,A7,PARTFUN1:def 6
.=-tan.x by A3,A6
.=-tan/.x by A1,A6,PARTFUN1:def 6
.=-tan|A/.x by A1,A2,A6,PARTFUN2:17
.=-tan|A.x by A6,PARTFUN1:def 6;
hence thesis;
end;
then tan|A is with_symmetrical_domain quasi_odd by A2;
hence thesis by A1;
end;
theorem
A c= dom cot implies cot is_odd_on A
proof
assume that
A1: A c= dom cot;
A2: dom(cot|A) = A by A1,RELAT_1:62;
A3: for x st x in A holds cot.(-x) = -cot.x
proof
let x;
assume
A4: x in A; then
A5: sin.x <> 0 by A1,FDIFF_8:2;
-x in A by A4,Def1; then
cot.(-x)= cot (-x) by A1,FDIFF_8:2,SIN_COS9:16
.=-cot x by SIN_COS4:3
.=-cot.x by A5,SIN_COS9:16;
hence thesis;
end;
for x st x in dom(cot|A) & -x in dom(cot|A) holds cot|A.(-x)=-cot|A.x
proof
let x;
assume that
A6: x in dom(cot|A) and
A7: -x in dom(cot|A);
reconsider x as Element of REAL by XREAL_0:def 1;
cot|A.(-x)=cot|A/.(-x) by A7,PARTFUN1:def 6
.=cot/.(-x) by A1,A2,A7,PARTFUN2:17
.=cot.(-x) by A1,A7,PARTFUN1:def 6
.=-cot.x by A3,A6
.=-cot/.x by A1,A6,PARTFUN1:def 6
.=-cot|A/.x by A1,A2,A6,PARTFUN2:17
.=-cot|A.x by A6,PARTFUN1:def 6;
hence thesis;
end;
then cot|A is with_symmetrical_domain quasi_odd by A2;
hence thesis by A1;
end;
theorem
A c= [.-1,1.] implies arctan is_odd_on A
proof
assume
A1: A c= [.-1,1.];
then
A2: A c= dom arctan by SIN_COS9:23;
A3: dom(arctan|A) = A by A1,RELAT_1:62,SIN_COS9:23,XBOOLE_1:1;
A4: for x st x in A holds arctan.(-x) = -arctan.x
proof
let x;
assume x in A;
then -1 <= x & x <= 1 by A1,XXREAL_1:1;
then arctan x = -arctan (-x) by SIN_COS9:67;
hence thesis;
end;
for x st x in dom(arctan|A) & -x in dom(arctan|A) holds arctan|A.(-x)=-
arctan|A.x
proof
let x;
assume that
A5: x in dom(arctan|A) and
A6: -x in dom(arctan|A);
reconsider x as Element of REAL by XREAL_0:def 1;
arctan|A.(-x)=arctan|A/.(-x) by A6,PARTFUN1:def 6
.=arctan/.(-x) by A2,A3,A6,PARTFUN2:17
.=arctan.(-x) by A2,A6,PARTFUN1:def 6
.=-arctan.x by A4,A5
.=-arctan/.x by A2,A5,PARTFUN1:def 6
.=-arctan|A/.x by A2,A3,A5,PARTFUN2:17
.=-arctan|A.x by A5,PARTFUN1:def 6;
hence thesis;
end;
then arctan|A is with_symmetrical_domain quasi_odd by A3;
hence thesis by A2;
end;
theorem
for A being symmetrical Subset of REAL holds |. sin .| is_even_on A
proof
let A be symmetrical Subset of REAL;
A is symmetrical Subset of COMPLEX by NUMBERS:11,XBOOLE_1:1;
hence thesis by Th20,Th65;
end;
theorem
for A being symmetrical Subset of REAL holds |. cos .| is_even_on A
proof
let A be symmetrical Subset of REAL;
A is symmetrical Subset of COMPLEX by NUMBERS:11,XBOOLE_1:1;
hence thesis by Th21,Th66;
end;
theorem
for A being symmetrical Subset of REAL holds sin" is_odd_on A
proof
let A be symmetrical Subset of REAL;
A is symmetrical Subset of COMPLEX by NUMBERS:11,XBOOLE_1:1;
hence thesis by Th18,Th65;
end;
theorem
for A being symmetrical Subset of REAL holds cos" is_even_on A
proof
let A be symmetrical Subset of REAL;
A is symmetrical Subset of COMPLEX by NUMBERS:11,XBOOLE_1:1;
hence thesis by Th19,Th66;
end;
theorem
for A being symmetrical Subset of REAL holds -sin is_odd_on A
proof
let A be symmetrical Subset of REAL;
A is symmetrical Subset of COMPLEX by NUMBERS:11,XBOOLE_1:1;
hence thesis by Th16,Th65;
end;
theorem
for A being symmetrical Subset of REAL holds -cos is_even_on A
proof
let A be symmetrical Subset of REAL;
A is symmetrical Subset of COMPLEX by NUMBERS:11,XBOOLE_1:1;
hence thesis by Th17,Th66;
end;
theorem
for A being symmetrical Subset of REAL holds sin^2 is_even_on A
proof
let A be symmetrical Subset of REAL;
A is symmetrical Subset of COMPLEX & sin is_odd_on A by Th65,NUMBERS:11
,XBOOLE_1:1;
hence thesis by Th22;
end;
theorem
for A being symmetrical Subset of REAL holds cos^2 is_even_on A
proof
let A be symmetrical Subset of REAL;
A is symmetrical Subset of COMPLEX & cos is_even_on A by Th66,NUMBERS:11
,XBOOLE_1:1;
hence thesis by Th23;
end;
reserve B for symmetrical Subset of REAL;
theorem Th81:
B c= dom (sec) implies sec is_even_on B
proof
assume
A1: B c= dom (sec);
then
A2: dom(sec|B) = B by RELAT_1:62;
A3: for x st x in B holds sec.(-x) = sec.x
proof
let x;
assume
A4: x in B;
then -x in B by Def1;
then sec.(-x)=(cos.(-x))" by A1,RFUNCT_1:def 2
.=(cos.x)" by SIN_COS:30
.= sec.x by A1,A4,RFUNCT_1:def 2;
hence thesis;
end;
for x st x in dom(sec|B) & -x in dom(sec|B) holds sec|B.(-x)=sec|B.x
proof
let x;
assume that
A5: x in dom(sec|B) and
A6: -x in dom(sec|B);
sec|B.(-x)=sec|B/.(-x) by A6,PARTFUN1:def 6
.=sec/.(-x) by A1,A2,A6,PARTFUN2:17
.=sec.(-x) by A1,A6,PARTFUN1:def 6
.=sec.x by A3,A5
.=sec/.x by A1,A5,PARTFUN1:def 6
.=sec|B/.x by A1,A2,A5,PARTFUN2:17
.=sec|B.x by A5,PARTFUN1:def 6;
hence thesis;
end;
then sec|B is with_symmetrical_domain quasi_even by A2;
hence thesis by A1;
end;
theorem
(for x being Real st x in B holds cos.x<>0) implies sec is_even_on B
proof
assume
A1: for x being Real st x in B holds cos.x<>0;
B c= dom (sec)
proof
let x be Real;
assume
A2: x in B;
then cos.x<>0 by A1;
then not cos.x in {0} by TARSKI:def 1;
then not x in cos"{0} by FUNCT_1:def 7;
then x in dom cos \ cos"{0} by A2,SIN_COS:24,XBOOLE_0:def 5;
hence thesis by RFUNCT_1:def 2;
end;
hence thesis by Th81;
end;
theorem Th83:
B c= dom (cosec) implies cosec is_odd_on B
proof
assume
A1: B c= dom (cosec);
then
A2: dom(cosec|B) = B by RELAT_1:62;
A3: for x st x in B holds cosec.(-x) = -cosec.x
proof
let x;
assume
A4: x in B;
then -x in B by Def1;
then cosec.(-x)=(sin.(-x))" by A1,RFUNCT_1:def 2
.=(-sin.x)" by SIN_COS:30
.=-(sin.x)" by XCMPLX_1:222
.=-cosec.x by A1,A4,RFUNCT_1:def 2;
hence thesis;
end;
for x st x in dom(cosec|B) & -x in dom(cosec|B) holds cosec|B.(-x)=-
cosec|B.x
proof
let x;
assume that
A5: x in dom(cosec|B) and
A6: -x in dom(cosec|B);
cosec|B.(-x)=cosec|B/.(-x) by A6,PARTFUN1:def 6
.=cosec/.(-x) by A1,A2,A6,PARTFUN2:17
.=cosec.(-x) by A1,A6,PARTFUN1:def 6
.=-cosec.x by A3,A5
.=-cosec/.x by A1,A5,PARTFUN1:def 6
.=-cosec|B/.x by A1,A2,A5,PARTFUN2:17
.=-cosec|B.x by A5,PARTFUN1:def 6;
hence thesis;
end;
then cosec|B is with_symmetrical_domain quasi_odd by A2;
hence thesis by A1;
end;
theorem
(for x being Real st x in B holds sin.x<>0) implies cosec is_odd_on B
proof
assume
A1: for x being Real st x in B holds sin.x<>0;
B c= dom cosec
proof
let x be Real;
assume
A2: x in B;
then sin.x<>0 by A1;
then not sin.x in {0} by TARSKI:def 1;
then not x in sin"{0} by FUNCT_1:def 7;
then x in dom sin \ sin"{0} by A2,SIN_COS:24,XBOOLE_0:def 5;
hence thesis by RFUNCT_1:def 2;
end;
hence thesis by Th83;
end;