:: Binary Operations on Numbers
:: by Library Committee
::
:: Received June 21, 2004
:: Copyright (c) 2004-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 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;
definitions BINOP_1;
equalities BINOP_1;
expansions BINOP_1;
theorems BINOP_1, FUNCT_2, XCMPLX_0, XREAL_0, INT_1, RAT_1, SETWISEO, NUMBERS,
ORDINAL1;
schemes BINOP_1, FUNCT_2;
begin
scheme
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 proof
let f1,f2 be Function of C(),D() such that
A1: for x being Element of C() holds f1.x = F(x) and
A2: for x being Element of C() holds f2.x = F(x);
now
let x be Element of C();
thus f1.x = F(x) by A1
.= f2.x by A2;
end;
hence thesis by FUNCT_2:63;
end;
scheme
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
proof
let o1,o2 be BinOp of A() such that
A1: for a,b being Element of A() holds o1.(a,b) = O(a,b) and
A2: for a,b being Element of A() holds o2.(a,b) = O(a,b);
now
let a,b be Element of A();
thus o1.(a,b) = O(a,b) by A1
.= o2.(a,b) by A2;
end;
hence thesis;
end;
scheme
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 proof
let f1,f2 be Function of COMPLEX,COMPLEX such that
A1: for x being Complex holds f1.x = F(x) and
A2: for x being Complex holds f2.x = F(x);
now
let x be Element of COMPLEX;
thus f1.x = F(x) by A1
.= f2.x by A2;
end;
hence thesis by FUNCT_2:63;
end;
scheme
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 proof
let f1,f2 be Function of REAL,REAL such that
A1: for x being Real holds f1.x = F(x) and
A2: for x being Real holds f2.x = F(x);
now
let x be Element of REAL;
thus f1.x = F(x) by A1
.= f2.x by A2;
end;
hence thesis by FUNCT_2:63;
end;
registration
cluster -> rational for Element of RAT;
coherence by RAT_1:def 2;
end;
scheme
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 proof
let f1,f2 be Function of RAT,RAT such that
A1: for x being Rational holds f1.x = F(x) and
A2: for x being Rational holds f2.x = F(x);
now
let x be Element of RAT;
thus f1.x = F(x) by A1
.= f2.x by A2;
end;
hence thesis by FUNCT_2:63;
end;
scheme
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 proof
let f1,f2 be Function of INT,INT such that
A1: for x being Integer holds f1.x = F(x) and
A2: for x being Integer holds f2.x = F(x);
now
let x be Element of INT;
thus f1.x = F(x) by A1
.= f2.x by A2;
end;
hence thesis by FUNCT_2:63;
end;
scheme
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 proof
let f1,f2 be sequence of NAT such that
A1: for x being Nat holds f1.x = F(x) and
A2: for x being Nat holds f2.x = F(x);
now
let x be Element of NAT;
thus f1.x = F(x) by A1
.= f2.x by A2;
end;
hence thesis by FUNCT_2:63;
end;
scheme
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
proof
let o1,o2 be BinOp of COMPLEX such that
A1: for a,b being Complex holds o1.(a,b) = O(a,b) and
A2: for a,b being Complex holds o2.(a,b) = O(a,b);
now
let a,b be Element of COMPLEX;
thus o1.(a,b) = O(a,b) by A1
.= o2.(a,b) by A2;
end;
hence thesis;
end;
scheme
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
proof
let o1,o2 be BinOp of REAL such that
A1: for a,b being Real holds o1.(a,b) = O(a,b) and
A2: for a,b being Real holds o2.(a,b) = O(a,b);
now
let a,b be Element of REAL;
thus o1.(a,b) = O(a,b) by A1
.= o2.(a,b) by A2;
end;
hence thesis;
end;
scheme
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
proof
let o1,o2 be BinOp of RAT such that
A1: for a,b being Rational holds o1.(a,b) = O(a,b) and
A2: for a,b being Rational holds o2.(a,b) = O(a,b);
now
let a,b be Element of RAT;
thus o1.(a,b) = O(a,b) by A1
.= o2.(a,b) by A2;
end;
hence thesis;
end;
scheme
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
proof
let o1,o2 be BinOp of INT such that
A1: for a,b being Integer holds o1.(a,b) = O(a,b) and
A2: for a,b being Integer holds o2.(a,b) = O(a,b);
now
let a,b be Element of INT;
thus o1.(a,b) = O(a,b) by A1
.= o2.(a,b) by A2;
end;
hence thesis;
end;
scheme
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
proof
let o1,o2 be BinOp of NAT such that
A1: for a,b being Nat holds o1.(a,b) = O(a,b) and
A2: for a,b being Nat holds o2.(a,b) = O(a,b);
now
let a,b be Element of NAT;
thus o1.(a,b) = O(a,b) by A1
.= o2.(a,b) by A2;
end;
hence thesis;
end;
scheme
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)
proof
defpred P[Complex,Complex,set] means $3 = F($1,$2);
A1: for x,y being Element of COMPLEX ex z being Element of COMPLEX st P[x,y,z]
proof let x,y being Element of COMPLEX;
reconsider z = F(x,y) as Element of COMPLEX by XCMPLX_0:def 2;
take z;
thus P[x,y,z];
end;
consider f being Function of [:COMPLEX,COMPLEX:],COMPLEX such that
A2: for x,y being Element of COMPLEX
holds P[x,y,f.(x,y)] from BINOP_1:sch 3(A1);
take f; let x,y be Complex;
reconsider x,y as Element of COMPLEX by XCMPLX_0:def 2;
P[x,y,f.(x,y)] by A2;
then f.(x,y)=F(x,y);
hence thesis;
end;
scheme
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)
proof
defpred P[Real,Real,set] means $3 = F($1,$2);
A1: for x,y being Element of REAL ex z being Element of REAL st P[x,y,z]
proof let x,y being Element of REAL;
reconsider z = F(x,y) as Element of REAL by XREAL_0:def 1;
take z;
thus P[x,y,z];
end;
consider f being Function of [:REAL,REAL:],REAL such that
A2: for x,y being Element of REAL holds P[x,y,f.(x,y)] from BINOP_1:sch 3(A1
);
take f; let x,y be Real;
reconsider x,y as Element of REAL by XREAL_0:def 1;
P[x,y,f.(x,y)] by A2;
then f.(x,y)=F(x,y);
hence thesis;
end;
scheme
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)
proof
defpred P[Rational,Rational,set] means $3 = F($1,$2);
A1: for x,y being Element of RAT ex z being Element of RAT st P[x,y,z]
proof let x,y being Element of RAT;
reconsider z = F(x,y) as Element of RAT by RAT_1:def 2;
take z;
thus P[x,y,z];
end;
consider f being Function of [:RAT,RAT:],RAT such that
A2: for x,y being Element of RAT holds P[x,y,f.(x,y)] from BINOP_1:sch 3(A1);
take f; let x,y be Rational;
reconsider x,y as Element of RAT by RAT_1:def 2;
P[x,y,f.(x,y)] by A2;
then f.(x,y)=F(x,y);
hence thesis;
end;
scheme
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)
proof
defpred P[Integer,Integer,set] means $3 = F($1,$2);
A1: for x,y being Element of INT ex z being Element of INT st P[x,y,z]
proof let x,y being Element of INT;
reconsider z = F(x,y) as Element of INT by INT_1:def 2;
take z;
thus P[x,y,z];
end;
consider f being Function of [:INT,INT:],INT such that
A2: for x,y being Element of INT holds P[x,y,f.(x,y)] from BINOP_1:sch 3(A1);
take f; let x,y be Integer;
reconsider x,y as Element of INT by INT_1:def 2;
P[x,y,f.(x,y)] by A2;
then f.(x,y)=F(x,y);
hence thesis;
end;
scheme
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)
proof
defpred P[Nat,Nat,set] means $3 = F($1,$2);
A1: for x,y being Element of NAT ex z being Element of NAT st P[x,y,z]
proof let x,y being Element of NAT;
reconsider z = F(x,y) as Element of NAT by ORDINAL1:def 12;
take z;
thus P[x,y,z];
end;
consider f being Function of [:NAT,NAT:],NAT such that
A2: for x,y being Element of NAT holds P[x,y,f.(x,y)] from BINOP_1:sch 3(A1);
take f; let x,y be Nat;
reconsider x,y as Element of NAT by ORDINAL1:def 12;
P[x,y,f.(x,y)] by A2;
then f.(x,y)=F(x,y);
hence thesis;
end;
scheme
CLambdaD{F(Complex) -> Complex }: ex f
being Function of COMPLEX,COMPLEX st
for x being Complex holds f.x = F(x)
proof
defpred P[Element of COMPLEX,set] means $2 = F($1);
A1: for x being Element of COMPLEX ex y being Element of COMPLEX st P[x,y]
proof let x being Element of COMPLEX;
reconsider y = F(x) as Element of COMPLEX by XCMPLX_0:def 2;
take y;
thus P[x,y];
end;
consider f being Function of COMPLEX,COMPLEX such that
A2: for x being Element of COMPLEX holds P[x,f.x] from FUNCT_2:sch 3(A1);
take f; let c be Complex;
reconsider c as Element of COMPLEX by XCMPLX_0:def 2;
P[c,f.c] by A2;
hence thesis;
end;
scheme
RLambdaD{F(Real) -> Real }: ex f
being Function of REAL,REAL st
for x being Real holds f.x = F(x)
proof
defpred P[Element of REAL,set] means $2 = F($1);
A1: for x being Element of REAL ex y being Element of REAL st P[x,y]
proof let x being Element of REAL;
reconsider y = F(x) as Element of REAL by XREAL_0:def 1;
take y;
thus P[x,y];
end;
consider f being Function of REAL,REAL such that
A2: for x being Element of REAL holds P[x,f.x] from FUNCT_2:sch 3(A1);
take f; let c be Real;
reconsider c as Element of REAL by XREAL_0:def 1;
P[c,f.c] by A2;
hence thesis;
end;
scheme
WLambdaD{F(Rational) -> Rational }: ex f
being Function of RAT,RAT st
for x being Rational holds f.x = F(x)
proof
defpred P[Element of RAT,set] means $2 = F($1);
A1: for x being Element of RAT ex y being Element of RAT st P[x,y]
proof let x being Element of RAT;
reconsider y = F(x) as Element of RAT by RAT_1:def 2;
take y;
thus P[x,y];
end;
consider f being Function of RAT,RAT such that
A2: for x being Element of RAT holds P[x,f.x] from FUNCT_2:sch 3(A1);
take f; let c be Rational;
reconsider c as Element of RAT by RAT_1:def 2;
P[c,f.c] by A2;
hence thesis;
end;
scheme
ILambdaD{F(Integer) -> Integer }: ex f
being Function of INT,INT st
for x being Integer holds f.x = F(x)
proof
defpred P[Element of INT,set] means $2 = F($1);
A1: for x being Element of INT ex y being Element of INT st P[x,y]
proof let x being Element of INT;
reconsider y = F(x) as Element of INT by INT_1:def 2;
take y;
thus P[x,y];
end;
consider f being Function of INT,INT such that
A2: for x being Element of INT holds P[x,f.x] from FUNCT_2:sch 3(A1);
take f; let c be Integer;
reconsider c as Element of INT by INT_1:def 2;
P[c,f.c] by A2;
hence thesis;
end;
scheme
NLambdaD{F(Nat) -> Nat }: ex f
being sequence of NAT st
for x being Nat holds f.x = F(x)
proof
defpred P[Element of NAT,set] means $2 = F($1);
A1: for x being Element of NAT ex y being Element of NAT st P[x,y]
proof let x being Element of NAT;
reconsider y = F(x) as Element of NAT by ORDINAL1:def 12;
take y;
thus P[x,y];
end;
consider f being sequence of NAT such that
A2: for x being Element of NAT holds P[x,f.x] from FUNCT_2:sch 3(A1);
take f; let c be Nat;
reconsider c as Element of NAT by ORDINAL1:def 12;
P[c,f.c] by A2;
hence thesis;
end;
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
for c holds it.c = -c;
existence from CLambdaD;
uniqueness from CFuncDefUniq;
func invcomplex -> UnOp of COMPLEX means
for c holds it.c = c";
existence from CLambdaD;
uniqueness from CFuncDefUniq;
func addcomplex -> BinOp of COMPLEX means
:Def3:
for c1,c2 holds it.(c1,c2) = c1 + c2;
existence from CLambda2D;
uniqueness from CBinOpDefuniq;
func diffcomplex -> BinOp of COMPLEX means
for c1,c2 holds it.(c1,c2) = c1 - c2;
existence from CLambda2D;
uniqueness from CBinOpDefuniq;
func multcomplex -> BinOp of COMPLEX means
:Def5:
for c1,c2 holds it.(c1,c2) = c1 * c2;
existence from CLambda2D;
uniqueness from CBinOpDefuniq;
func divcomplex -> BinOp of COMPLEX means
for c1,c2 holds it.(c1,c2) = c1 / c2;
existence from CLambda2D;
uniqueness from CBinOpDefuniq;
end;
definition
func compreal -> UnOp of REAL means
for r holds it.r = -r;
existence from RLambdaD;
uniqueness from RFuncDefUniq;
func invreal -> UnOp of REAL means
for r holds it.r = r";
existence from RLambdaD;
uniqueness from RFuncDefUniq;
func addreal -> BinOp of REAL means
:Def9:
for r1,r2 holds it.(r1,r2) = r1 + r2;
existence from RLambda2D;
uniqueness from RBinOpDefuniq;
func diffreal -> BinOp of REAL means
for r1,r2 holds it.(r1,r2) = r1 - r2;
existence from RLambda2D;
uniqueness from RBinOpDefuniq;
func multreal -> BinOp of REAL means
:Def11:
for r1,r2 holds it.(r1,r2) = r1 * r2;
existence from RLambda2D;
uniqueness from RBinOpDefuniq;
func divreal -> BinOp of REAL means
for r1,r2 holds it.(r1,r2) = r1 / r2;
existence from RLambda2D;
uniqueness from RBinOpDefuniq;
end;
definition
func comprat -> UnOp of RAT means
for w holds it.w = -w;
existence from WLambdaD;
uniqueness from WFuncDefUniq;
func invrat -> UnOp of RAT means
for w holds it.w = w";
existence from WLambdaD;
uniqueness from WFuncDefUniq;
func addrat -> BinOp of RAT means
:Def15:
for w1,w2 holds it.(w1,w2) = w1 + w2;
existence from WLambda2D;
uniqueness from WBinOpDefuniq;
func diffrat -> BinOp of RAT means
for w1,w2 holds it.(w1,w2) = w1 - w2;
existence from WLambda2D;
uniqueness from WBinOpDefuniq;
func multrat -> BinOp of RAT means
:Def17:
for w1,w2 holds it.(w1,w2) = w1 * w2;
existence from WLambda2D;
uniqueness from WBinOpDefuniq;
func divrat -> BinOp of RAT means
for w1,w2 holds it.(w1,w2) = w1 / w2;
existence from WLambda2D;
uniqueness from WBinOpDefuniq;
end;
definition
func compint -> UnOp of INT means
for i holds it.i = -i;
existence from ILambdaD;
uniqueness from IFuncDefUniq;
func addint -> BinOp of INT means
:Def20:
for i1,i2 holds it.(i1,i2) = i1 + i2;
existence from ILambda2D;
uniqueness from IBinOpDefuniq;
func diffint -> BinOp of INT means
for i1,i2 holds it.(i1,i2) = i1 - i2;
existence from ILambda2D;
uniqueness from IBinOpDefuniq;
func multint -> BinOp of INT means
:Def22:
for i1,i2 holds it.(i1,i2) = i1 * i2;
existence from ILambda2D;
uniqueness from IBinOpDefuniq;
end;
definition
func addnat -> BinOp of NAT means
:Def23:
for n1,n2 holds it.(n1,n2) = n1 + n2;
existence from NLambda2D;
uniqueness from NBinOpDefuniq;
func multnat -> BinOp of NAT means
:Def24:
for n1,n2 holds it.(n1,n2) = n1 * n2;
existence from NLambda2D;
uniqueness from NBinOpDefuniq;
end;
registration
cluster addcomplex -> commutative associative;
coherence
proof
thus addcomplex is commutative
proof
let c1,c2 be Element of COMPLEX;
thus addcomplex.(c1,c2) = c1 + c2 by Def3
.= addcomplex.(c2,c1) by Def3;
end;
let c1,c2,c3 be Element of COMPLEX;
thus addcomplex.(c1,addcomplex.(c2,c3)) = c1 + addcomplex.(c2,c3) by Def3
.= c1 + (c2 + c3) by Def3
.= c1 + c2 + c3
.= addcomplex.(c1,c2) + c3 by Def3
.= addcomplex.(addcomplex.(c1,c2),c3) by Def3;
end;
cluster multcomplex -> commutative associative;
coherence
proof
thus multcomplex is commutative
proof
let c1,c2 be Element of COMPLEX;
thus multcomplex.(c1,c2) = c1 * c2 by Def5
.= multcomplex.(c2,c1) by Def5;
end;
let c1,c2,c3 be Element of COMPLEX;
thus multcomplex.(c1,multcomplex.(c2,c3)) = c1 * multcomplex.(c2,c3) by
Def5
.= c1 * (c2 * c3) by Def5
.= c1 * c2 * c3
.= multcomplex.(c1,c2) * c3 by Def5
.= multcomplex.(multcomplex.(c1,c2),c3) by Def5;
end;
cluster addreal -> commutative associative;
coherence
proof
thus addreal is commutative
proof
let r1,r2 be Element of REAL;
thus addreal.(r1,r2) = r1 + r2 by Def9
.= addreal.(r2,r1) by Def9;
end;
let r1,r2,r3 be Element of REAL;
thus addreal.(r1,addreal.(r2,r3)) = r1 + addreal.(r2,r3) by Def9
.= r1 + (r2 + r3) by Def9
.= r1 + r2 + r3
.= addreal.(r1,r2) + r3 by Def9
.= addreal.(addreal.(r1,r2),r3) by Def9;
end;
cluster multreal -> commutative associative;
coherence
proof
thus multreal is commutative
proof
let r1,r2 be Element of REAL;
thus multreal.(r1,r2) = r1 * r2 by Def11
.= multreal.(r2,r1) by Def11;
end;
let r1,r2,r3 be Element of REAL;
thus multreal.(r1,multreal.(r2,r3)) = r1 * multreal.(r2,r3) by Def11
.= r1 * (r2 * r3) by Def11
.= r1 * r2 * r3
.= multreal.(r1,r2) * r3 by Def11
.= multreal.(multreal.(r1,r2),r3) by Def11;
end;
cluster addrat -> commutative associative;
coherence
proof
thus addrat is commutative
proof
let w1,w2 be Element of RAT;
thus addrat.(w1,w2) = w1 + w2 by Def15
.= addrat.(w2,w1) by Def15;
end;
let w1,w2,w3 be Element of RAT;
thus addrat.(w1,addrat.(w2,w3)) = w1 + addrat.(w2,w3) by Def15
.= w1 + (w2 + w3) by Def15
.= w1 + w2 + w3
.= addrat.(w1,w2) + w3 by Def15
.= addrat.(addrat.(w1,w2),w3) by Def15;
end;
cluster multrat -> commutative associative;
coherence
proof
thus multrat is commutative
proof
let w1,w2 be Element of RAT;
thus multrat.(w1,w2) = w1 * w2 by Def17
.= multrat.(w2,w1) by Def17;
end;
let w1,w2,w3 be Element of RAT;
thus multrat.(w1,multrat.(w2,w3)) = w1 * multrat.(w2,w3) by Def17
.= w1 * (w2 * w3) by Def17
.= w1 * w2 * w3
.= multrat.(w1,w2) * w3 by Def17
.= multrat.(multrat.(w1,w2),w3) by Def17;
end;
cluster addint -> commutative associative;
coherence
proof
thus addint is commutative
proof
let i1,i2 be Element of INT;
thus addint.(i1,i2) = i1 + i2 by Def20
.= addint.(i2,i1) by Def20;
end;
let i1,i2,i3 be Element of INT;
thus addint.(i1,addint.(i2,i3)) = i1 + addint.(i2,i3) by Def20
.= i1 + (i2 + i3) by Def20
.= i1 + i2 + i3
.= addint.(i1,i2) + i3 by Def20
.= addint.(addint.(i1,i2),i3) by Def20;
end;
cluster multint -> commutative associative;
coherence
proof
thus multint is commutative
proof
let i1,i2 be Element of INT;
thus multint.(i1,i2) = i1 * i2 by Def22
.= multint.(i2,i1) by Def22;
end;
let i1,i2,i3 be Element of INT;
thus multint.(i1,multint.(i2,i3)) = i1 * multint.(i2,i3) by Def22
.= i1 * (i2 * i3) by Def22
.= i1 * i2 * i3
.= multint.(i1,i2) * i3 by Def22
.= multint.(multint.(i1,i2),i3) by Def22;
end;
cluster addnat -> commutative associative;
coherence
proof
thus addnat is commutative
proof
let n1,n2 be Element of NAT;
thus addnat.(n1,n2) = n1 + n2 by Def23
.= addnat.(n2,n1) by Def23;
end;
let n1,n2,n3 be Element of NAT;
thus addnat.(n1,addnat.(n2,n3)) = n1 + addnat.(n2,n3) by Def23
.= n1 + (n2 + n3) by Def23
.= n1 + n2 + n3
.= addnat.(n1,n2) + n3 by Def23
.= addnat.(addnat.(n1,n2),n3) by Def23;
end;
cluster multnat -> commutative associative;
coherence
proof
thus multnat is commutative
proof
let n1,n2 be Element of NAT;
thus multnat.(n1,n2) = n1 * n2 by Def24
.= multnat.(n2,n1) by Def24;
end;
let n1,n2,n3 be Element of NAT;
thus multnat.(n1,multnat.(n2,n3)) = n1 * multnat.(n2,n3) by Def24
.= n1 * (n2 * n3) by Def24
.= n1 * n2 * n3
.= multnat.(n1,n2) * n3 by Def24
.= multnat.(multnat.(n1,n2),n3) by Def24;
end;
end;
Lm1: 0 in NAT;
Lm2: 0 is_a_unity_wrt addcomplex
proof
thus for c being Element of COMPLEX holds addcomplex.(0,c) = c
proof
let c be Element of COMPLEX;
thus addcomplex.(0,c) = 0 + c by Def3
.= c;
end;
let c be Element of COMPLEX;
thus addcomplex.(c,0) = c + 0 by Def3
.= c;
end;
Lm3: In(0,REAL) is_a_unity_wrt addreal
proof
thus for r being Element of REAL holds addreal.(In(0,REAL),r) = r
proof
let r be Element of REAL;
thus addreal.(In(0,REAL),r) = 0 + r by Def9
.= r;
end;
let r be Element of REAL;
thus addreal.(r,In(0,REAL)) = r + 0 by Def9
.= r;
end;
Lm4: 0 is_a_unity_wrt addrat
proof
thus for w being Element of RAT holds addrat.(0,w) = w
proof
let w be Element of RAT;
thus addrat.(0,w) = 0 + w by Def15
.= w;
end;
let w be Element of RAT;
thus addrat.(w,0) = w + 0 by Def15
.= w;
end;
Lm5: 0 is_a_unity_wrt addint
proof
thus for i being Element of INT holds addint.(0,i) = i
proof
let i be Element of INT;
thus addint.(0,i) = 0 + i by Def20
.= i;
end;
let i be Element of INT;
thus addint.(i,0) = i + 0 by Def20
.= i;
end;
Lm6: 0 is_a_unity_wrt addnat
proof
thus for n being Element of NAT holds addnat.(0,n) = n
proof
let n be Element of NAT;
thus addnat.(0,n) = 0 + n by Def23
.= n;
end;
let n be Element of NAT;
thus addnat.(n,0) = n + 0 by Def23
.= n;
end;
Lm7: 1 in NAT;
Lm8: 1 is_a_unity_wrt multcomplex
proof
thus for c being Element of COMPLEX holds multcomplex.(1,c) = c
proof
let c be Element of COMPLEX;
thus multcomplex.(1,c) = 1 * c by Def5
.= c;
end;
let c be Element of COMPLEX;
thus multcomplex.(c,1) = c * 1 by Def5
.= c;
end;
Lm9: 1 is_a_unity_wrt multreal
proof
1 in NAT;
then reconsider j = 1 as Element of REAL by NUMBERS:19;
thus for r being Element of REAL holds multreal.(1,r) = r
proof
let r be Element of REAL;
thus multreal.(1,r) = 1 * r by Def11
.= r;
end;
let r be Element of REAL;
thus multreal.(r,1) = r * 1 by Def11
.= r;
end;
Lm10: 1 is_a_unity_wrt multrat
proof
thus for w being Element of RAT holds multrat.(1,w) = w
proof
let w be Element of RAT;
thus multrat.(1,w) = 1 * w by Def17
.= w;
end;
let w be Element of RAT;
thus multrat.(w,1) = w * 1 by Def17
.= w;
end;
Lm11: 1 is_a_unity_wrt multint
proof
thus for i being Element of INT holds multint.(1,i) = i
proof
let i be Element of INT;
thus multint.(1,i) = 1 * i by Def22
.= i;
end;
let i be Element of INT;
thus multint.(i,1) = i * 1 by Def22
.= i;
end;
Lm12: 1 is_a_unity_wrt multnat
proof
thus for n being Element of NAT holds multnat.(1,n) = n
proof
let n be Element of NAT;
thus multnat.(1,n) = 1 * n by Def24
.= n;
end;
let n be Element of NAT;
thus multnat.(n,1) = n * 1 by Def24
.= n;
end;
registration
cluster addcomplex -> having_a_unity;
coherence by Lm1,NUMBERS:20,Lm2,SETWISEO:def 2;
cluster addreal -> having_a_unity;
coherence by Lm3,SETWISEO:def 2;
cluster addrat -> having_a_unity;
coherence by Lm1,NUMBERS:18,Lm4,SETWISEO:def 2;
cluster addint -> having_a_unity;
coherence by Lm1,NUMBERS:17,Lm5,SETWISEO:def 2;
cluster addnat -> having_a_unity;
coherence by Lm6,SETWISEO:def 2;
cluster multcomplex -> having_a_unity;
coherence by Lm7,NUMBERS:20,Lm8,SETWISEO:def 2;
cluster multreal -> having_a_unity;
coherence by Lm7,NUMBERS:19,Lm9,SETWISEO:def 2;
cluster multrat -> having_a_unity;
coherence by Lm7,NUMBERS:18,Lm10,SETWISEO:def 2;
cluster multint -> having_a_unity;
coherence by Lm7,NUMBERS:17,Lm11,SETWISEO:def 2;
cluster multnat -> having_a_unity;
coherence by Lm12,SETWISEO:def 2;
end;
theorem
the_unity_wrt addcomplex = 0 by Lm1,NUMBERS:20,Lm2,BINOP_1:def 8;
theorem
the_unity_wrt addreal = 0 by Lm3,BINOP_1:def 8;
theorem
the_unity_wrt addrat = 0 by Lm1,NUMBERS:18,Lm4,BINOP_1:def 8;
theorem
the_unity_wrt addint = 0 by Lm1,NUMBERS:17,Lm5,BINOP_1:def 8;
theorem
the_unity_wrt addnat = 0 by Lm6,BINOP_1:def 8;
theorem
the_unity_wrt multcomplex = 1 by Lm7,NUMBERS:20,Lm8,BINOP_1:def 8;
theorem
the_unity_wrt multreal = 1 by Lm7,NUMBERS:19,Lm9,BINOP_1:def 8;
theorem
the_unity_wrt multrat = 1 by Lm7,NUMBERS:18,Lm10,BINOP_1:def 8;
theorem
the_unity_wrt multint = 1 by Lm7,NUMBERS:17,Lm11,BINOP_1:def 8;
theorem
the_unity_wrt multnat = 1 by Lm12,BINOP_1:def 8;
registration
let f be real-valued Function;
let a,b be object;
cluster f.(a,b) -> real;
coherence;
end;