:: Binary Operations on Numbers :: by Library Committee :: :: Received June 21, 2004 :: Copyright (c) 2004-2021 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;