:: Binary Operations on Numbers
:: by Library Committee
::
:: Received June 21, 2004
:: Copyright (c) 2004-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 XBOOLE_0, SUBSET_1, FUNCT_1, BINOP_1, XCMPLX_0, NUMBERS, XREAL_0,
RAT_1, INT_1, ZFMISC_1, ARYTM_1, RELAT_1, ARYTM_3, CARD_1, SETWISEO,
BINOP_2, NAT_1, VALUED_0, FUNCT_7, REAL_1;
notations XBOOLE_0, ZFMISC_1, SUBSET_1, FUNCT_1, FUNCT_2, BINOP_1, SETWISEO,
ORDINAL1, XCMPLX_0, XREAL_0, NAT_1, INT_1, NUMBERS, RAT_1, VALUED_0;
constructors BINOP_1, SETWISEO, XCMPLX_0, RAT_1, RELSET_1, VALUED_0, NUMBERS;
registrations ORDINAL1, NUMBERS, XCMPLX_0, XREAL_0, NAT_1, INT_1, RAT_1,
RELSET_1, VALUED_0;
requirements BOOLE, SUBSET, ARITHM, NUMERALS;
begin
scheme :: BINOP_2:sch 1
FuncDefUniq{C, D()->non empty set, F(Element of C())->object}:
for f1,f2 being Function of C(),D() st
(for x being Element of C() holds f1.x = F(x)) & (for x
being Element of C() holds f2.x = F(x)) holds f1 = f2;
scheme :: BINOP_2:sch 2
BinOpDefuniq{A()->non empty set, O(Element of A(),Element of A())->object}:
for o1,o2 being BinOp of A() st (for a,b being Element of A() holds
o1.(a,b) = O(a,b)) &
(for a,b being Element of A() holds o2.(a,b) = O(a,b)) holds o1 = o2;
scheme :: BINOP_2:sch 3
CFuncDefUniq{F(object)->object}:
for f1,f2 being Function of COMPLEX,COMPLEX st
(for x being Complex holds f1.x = F(x)) & (for x
being Complex holds f2.x = F(x)) holds f1 = f2;
scheme :: BINOP_2:sch 4
RFuncDefUniq{F(Real)->object}: for f1,f2 being
Function of REAL,REAL st
(for x being Real holds f1.x = F(x)) & (for x
being Real holds f2.x = F(x)) holds f1 = f2;
registration
cluster -> rational for Element of RAT;
end;
scheme :: BINOP_2:sch 5
WFuncDefUniq{F(Rational)->object}: for f1,f2 being
Function of RAT,RAT st
(for x being Rational holds f1.x = F(x)) & (for x
being Rational holds f2.x = F(x)) holds f1 = f2;
scheme :: BINOP_2:sch 6
IFuncDefUniq{F(Integer)->object}: for f1,f2 being
Function of INT,INT st
(for x being Integer holds f1.x = F(x)) & (for x
being Integer holds f2.x = F(x)) holds f1 = f2;
scheme :: BINOP_2:sch 7
NFuncDefUniq{F(Nat)->object}: for f1,f2 being sequence of NAT st
(for x being Nat holds f1.x = F(x)) & (for x
being Nat holds f2.x = F(x)) holds f1 = f2;
scheme :: BINOP_2:sch 8
CBinOpDefuniq{O(Complex,Complex)->object}:
for o1,o2 being BinOp of COMPLEX st
(for a,b being Complex holds o1.(a,b) = O(a,b)) &
(for a,b being Complex holds o2.(a,b) = O(a,b)) holds o1 = o2;
scheme :: BINOP_2:sch 9
RBinOpDefuniq{O(Real,Real)->object}:
for o1,o2 being BinOp of REAL st
(for a,b being Real holds o1.(a,b) = O(a,b)) &
(for a,b being Real holds o2.(a,b) = O(a,b)) holds o1 = o2;
scheme :: BINOP_2:sch 10
WBinOpDefuniq{O(Rational,Rational)->object}:
for o1,o2 being BinOp of RAT st
(for a,b being Rational holds o1.(a,b) = O(a,b)) &
(for a,b being Rational holds o2.(a,b) = O(a,b)) holds o1 = o2;
scheme :: BINOP_2:sch 11
IBinOpDefuniq{O(Integer,Integer)->object}:
for o1,o2 being BinOp of INT st
(for a,b being Integer holds o1.(a,b) = O(a,b)) &
(for a,b being Integer holds o2.(a,b) = O(a,b)) holds o1 = o2;
scheme :: BINOP_2:sch 12
NBinOpDefuniq{O(Nat,Nat)->object}:
for o1,o2 being BinOp of NAT st
(for a,b being Nat holds o1.(a,b) = O(a,b)) &
(for a,b being Nat holds o2.(a,b) = O(a,b)) holds o1 = o2;
scheme :: BINOP_2:sch 13
CLambda2D{F(Complex,Complex) -> Complex}:
ex f being Function of [:COMPLEX,COMPLEX:],COMPLEX st
for x,y being Complex holds f.(x,y)=F(x,y);
scheme :: BINOP_2:sch 14
RLambda2D{F(Real,Real) -> Real}:
ex f being Function of [:REAL,REAL:],REAL st
for x,y being Real holds f.(x,y)=F(x,y);
scheme :: BINOP_2:sch 15
WLambda2D{F(Rational,Rational) -> Rational}:
ex f being Function of [:RAT,RAT:],RAT st
for x,y being Rational holds f.(x,y)=F(x,y);
scheme :: BINOP_2:sch 16
ILambda2D{F(Integer,Integer) -> Integer}:
ex f being Function of [:INT,INT:],INT st
for x,y being Integer holds f.(x,y)=F(x,y);
scheme :: BINOP_2:sch 17
NLambda2D{F(Nat,Nat) -> Nat}:
ex f being Function of [:NAT,NAT:],NAT st
for x,y being Nat holds f.(x,y)=F(x,y);
scheme :: BINOP_2:sch 18
CLambdaD{F(Complex) -> Complex }: ex f
being Function of COMPLEX,COMPLEX st
for x being Complex holds f.x = F(x);
scheme :: BINOP_2:sch 19
RLambdaD{F(Real) -> Real }: ex f
being Function of REAL,REAL st
for x being Real holds f.x = F(x);
scheme :: BINOP_2:sch 20
WLambdaD{F(Rational) -> Rational }: ex f
being Function of RAT,RAT st
for x being Rational holds f.x = F(x);
scheme :: BINOP_2:sch 21
ILambdaD{F(Integer) -> Integer }: ex f
being Function of INT,INT st
for x being Integer holds f.x = F(x);
scheme :: BINOP_2:sch 22
NLambdaD{F(Nat) -> Nat }: ex f
being sequence of NAT st
for x being Nat holds f.x = F(x);
reserve c,c1,c2 for Complex;
reserve r,r1,r2 for Real;
reserve w,w1,w2 for Rational;
reserve i,i1,i2 for Integer;
reserve n1,n2 for Nat;
:: definition
:: let n1,n2;
:: redefine func n1+n2 -> Element of NAT;
:: coherence by ORDINAL1:def 12;
:: redefine func n1*n2 -> Element of NAT;
:: coherence by ORDINAL1:def 12;
:: end;
definition
func compcomplex -> UnOp of COMPLEX means
:: BINOP_2:def 1
for c holds it.c = -c;
func invcomplex -> UnOp of COMPLEX means
:: BINOP_2:def 2
for c holds it.c = c";
func addcomplex -> BinOp of COMPLEX means
:: BINOP_2:def 3
for c1,c2 holds it.(c1,c2) = c1 + c2;
func diffcomplex -> BinOp of COMPLEX means
:: BINOP_2:def 4
for c1,c2 holds it.(c1,c2) = c1 - c2;
func multcomplex -> BinOp of COMPLEX means
:: BINOP_2:def 5
for c1,c2 holds it.(c1,c2) = c1 * c2;
func divcomplex -> BinOp of COMPLEX means
:: BINOP_2:def 6
for c1,c2 holds it.(c1,c2) = c1 / c2;
end;
definition
func compreal -> UnOp of REAL means
:: BINOP_2:def 7
for r holds it.r = -r;
func invreal -> UnOp of REAL means
:: BINOP_2:def 8
for r holds it.r = r";
func addreal -> BinOp of REAL means
:: BINOP_2:def 9
for r1,r2 holds it.(r1,r2) = r1 + r2;
func diffreal -> BinOp of REAL means
:: BINOP_2:def 10
for r1,r2 holds it.(r1,r2) = r1 - r2;
func multreal -> BinOp of REAL means
:: BINOP_2:def 11
for r1,r2 holds it.(r1,r2) = r1 * r2;
func divreal -> BinOp of REAL means
:: BINOP_2:def 12
for r1,r2 holds it.(r1,r2) = r1 / r2;
end;
definition
func comprat -> UnOp of RAT means
:: BINOP_2:def 13
for w holds it.w = -w;
func invrat -> UnOp of RAT means
:: BINOP_2:def 14
for w holds it.w = w";
func addrat -> BinOp of RAT means
:: BINOP_2:def 15
for w1,w2 holds it.(w1,w2) = w1 + w2;
func diffrat -> BinOp of RAT means
:: BINOP_2:def 16
for w1,w2 holds it.(w1,w2) = w1 - w2;
func multrat -> BinOp of RAT means
:: BINOP_2:def 17
for w1,w2 holds it.(w1,w2) = w1 * w2;
func divrat -> BinOp of RAT means
:: BINOP_2:def 18
for w1,w2 holds it.(w1,w2) = w1 / w2;
end;
definition
func compint -> UnOp of INT means
:: BINOP_2:def 19
for i holds it.i = -i;
func addint -> BinOp of INT means
:: BINOP_2:def 20
for i1,i2 holds it.(i1,i2) = i1 + i2;
func diffint -> BinOp of INT means
:: BINOP_2:def 21
for i1,i2 holds it.(i1,i2) = i1 - i2;
func multint -> BinOp of INT means
:: BINOP_2:def 22
for i1,i2 holds it.(i1,i2) = i1 * i2;
end;
definition
func addnat -> BinOp of NAT means
:: BINOP_2:def 23
for n1,n2 holds it.(n1,n2) = n1 + n2;
func multnat -> BinOp of NAT means
:: BINOP_2:def 24
for n1,n2 holds it.(n1,n2) = n1 * n2;
end;
registration
cluster addcomplex -> commutative associative;
cluster multcomplex -> commutative associative;
cluster addreal -> commutative associative;
cluster multreal -> commutative associative;
cluster addrat -> commutative associative;
cluster multrat -> commutative associative;
cluster addint -> commutative associative;
cluster multint -> commutative associative;
cluster addnat -> commutative associative;
cluster multnat -> commutative associative;
end;
registration
cluster addcomplex -> having_a_unity;
cluster addreal -> having_a_unity;
cluster addrat -> having_a_unity;
cluster addint -> having_a_unity;
cluster addnat -> having_a_unity;
cluster multcomplex -> having_a_unity;
cluster multreal -> having_a_unity;
cluster multrat -> having_a_unity;
cluster multint -> having_a_unity;
cluster multnat -> having_a_unity;
end;
theorem :: BINOP_2:1
the_unity_wrt addcomplex = 0;
theorem :: BINOP_2:2
the_unity_wrt addreal = 0;
theorem :: BINOP_2:3
the_unity_wrt addrat = 0;
theorem :: BINOP_2:4
the_unity_wrt addint = 0;
theorem :: BINOP_2:5
the_unity_wrt addnat = 0;
theorem :: BINOP_2:6
the_unity_wrt multcomplex = 1;
theorem :: BINOP_2:7
the_unity_wrt multreal = 1;
theorem :: BINOP_2:8
the_unity_wrt multrat = 1;
theorem :: BINOP_2:9
the_unity_wrt multint = 1;
theorem :: BINOP_2:10
the_unity_wrt multnat = 1;
registration
let f be real-valued Function;
let a,b be object;
cluster f.(a,b) -> real;
end;