:: The Binomial Theorem for Algebraic Structures
:: by Christoph Schwarzweller
::
:: Received November 20, 2000
:: Copyright (c) 2000-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 NUMBERS, RLVECT_1, ALGSTR_0, XBOOLE_0, SUBSET_1, ARYTM_3,
ALGSTR_1, BINOP_1, LATTICES, GROUP_1, VECTSP_2, VECTSP_1, SUPINF_2,
RELAT_1, FUNCT_1, ZFMISC_1, CARD_1, FUNCT_2, MCART_1, CARD_3, FINSEQ_1,
STRUCT_0, XXREAL_0, PARTFUN1, NAT_1, NEWTON, ARYTM_1, ORDINAL4, FINSEQ_2,
BINOM;
notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, ORDINAL1, NUMBERS, XCMPLX_0,
STRUCT_0, ALGSTR_0, PARTFUN1, FUNCT_1, FUNCT_2, FINSEQ_1, RELSET_1,
BINOP_1, NAT_1, ALGSTR_1, FINSEQ_2, VECTSP_1, VECTSP_2, GROUP_1, NEWTON,
RLVECT_1, XTUPLE_0, MCART_1, POLYNOM1, XXREAL_0;
constructors BINOP_1, REAL_1, NEWTON, ALGSTR_1, MONOID_0, POLYNOM1, RELSET_1,
FVSUM_1, XTUPLE_0;
registrations XBOOLE_0, ORDINAL1, RELSET_1, XXREAL_0, XREAL_0, NAT_1,
FINSEQ_2, STRUCT_0, VECTSP_1, ALGSTR_1, MONOID_0, INT_1, ALGSTR_0,
CARD_1, FINSEQ_1, XTUPLE_0;
requirements NUMERALS, SUBSET, REAL, BOOLE, ARITHM;
begin :: Preliminaries
registration
cluster Abelian right_add-cancelable -> left_add-cancelable for non empty
addLoopStr;
cluster Abelian left_add-cancelable -> right_add-cancelable for non empty
addLoopStr;
end;
registration
cluster right_zeroed right_complementable add-associative ->
right_add-cancelable for non empty addLoopStr;
end;
registration
cluster Abelian add-associative left_zeroed right_zeroed commutative
associative add-cancelable distributive unital for
non empty doubleLoopStr;
end;
theorem :: BINOM:1
for R being right_zeroed left_add-cancelable left-distributive
non empty doubleLoopStr, a being Element of R holds 0.R * a = 0.R;
theorem :: BINOM:2
for R being left_zeroed right_add-cancelable right-distributive
non empty doubleLoopStr, a being Element of R holds a * 0.R = 0.R;
begin :: On Finite Sequences
theorem :: BINOM:3
for L being left_zeroed non empty addLoopStr, a being Element
of L holds Sum <* a *> = a;
theorem :: BINOM:4
for R being left_zeroed right_add-cancelable right-distributive non
empty doubleLoopStr, a being Element of R, p being FinSequence of the carrier
of R holds Sum(a * p) = a * Sum p;
theorem :: BINOM:5
for R being right_zeroed left_add-cancelable left-distributive
non empty doubleLoopStr, a being Element of R, p being FinSequence of the
carrier of R holds Sum(p * a) = Sum p * a;
theorem :: BINOM:6
for R being commutative non empty multMagma, a being Element of R,
p being FinSequence of the carrier of R holds p * a = a * p;
definition
let R be non empty addLoopStr, p,q be FinSequence of the carrier of R;
func p + q -> FinSequence of the carrier of R means
:: BINOM:def 1
dom it = dom p &
for i being Nat st 1 <= i & i <= len it holds it/.i = p/.i + q/.i;
end;
theorem :: BINOM:7
for R being Abelian right_zeroed add-associative non empty
addLoopStr, p,q being FinSequence of the carrier of R st dom p = dom q holds
Sum(p + q) = Sum p + Sum q;
begin :: On Powers in Rings
definition
let R be unital non empty multMagma, a be Element of R, n be Nat;
func a|^n -> Element of R equals
:: BINOM:def 2
power(R).(a,n);
end;
theorem :: BINOM:8
for R being unital non empty multMagma, a being Element of R
holds a|^0 = 1_R & a|^1 = a;
theorem :: BINOM:9
for R being unital associative commutative non empty multMagma,
a,b being Element of R, n being Nat holds
(a * b)|^n = (a|^n) * (b|^n);
theorem :: BINOM:10
for R being unital associative non empty multMagma,
a being Element of R, n,m being Nat holds
a|^(n+m) = (a|^n) * (a|^m);
theorem :: BINOM:11
for R being unital associative non empty multMagma, a being Element
of R, n,m being Nat holds (a|^n)|^m = a|^(n * m);
begin :: On Natural Products in Rings
definition
let R be non empty addLoopStr;
func Nat-mult-left(R) -> Function of [:NAT,the carrier of R:],the carrier of
R means
:: BINOM:def 3
for a being Element of R holds it.(0,a) = 0.R &
for n being Nat holds it.(n+1,a) = a + it.(n,a);
func Nat-mult-right(R) -> Function of [:the carrier of R,NAT:],the carrier
of R means
:: BINOM:def 4
for a being Element of R holds it.(a,0) = 0.R & for n being
Element of NAT holds it.(a,n+1) = it.(a,n) + a;
end;
definition
let R be non empty addLoopStr, a be Element of R, n be Nat;
func n * a -> Element of R equals
:: BINOM:def 5
(Nat-mult-left(R)).(n,a);
func a * n -> Element of R equals
:: BINOM:def 6
(Nat-mult-right(R)).(a,n);
end;
theorem :: BINOM:12
for R being non empty addLoopStr, a being Element of R holds 0 * a =
0.R & a * 0 = 0.R;
theorem :: BINOM:13
for R being right_zeroed non empty addLoopStr, a being Element
of R holds 1 * a = a;
theorem :: BINOM:14
for R being left_zeroed non empty addLoopStr, a being Element
of R holds a * 1 = a;
theorem :: BINOM:15
for R being left_zeroed add-associative non empty addLoopStr,
a being Element of R, n,m being Nat
holds (n + m) * a = n * a + m * a;
theorem :: BINOM:16
for R being right_zeroed add-associative non empty addLoopStr,
a being Element of R, n,m being Element of NAT holds a * (n + m) = a * n + a *
m;
theorem :: BINOM:17
for R being left_zeroed right_zeroed add-associative non empty
addLoopStr, a being Element of R, n being Element of NAT holds n * a = a * n;
theorem :: BINOM:18
for R being Abelian non empty addLoopStr, a being Element of R, n
being Element of NAT holds n * a = a * n;
theorem :: BINOM:19
for R being left_zeroed right_zeroed left_add-cancelable
add-associative left-distributive non empty doubleLoopStr, a,b being Element
of R, n being Element of NAT holds (n * a) * b = n * (a * b);
theorem :: BINOM:20
for R being left_zeroed right_zeroed right_add-cancelable
add-associative distributive non empty doubleLoopStr, a,b being Element of R,
n being Element of NAT holds b * (n * a) = (b * a) * n;
theorem :: BINOM:21
for R being left_zeroed right_zeroed add-associative
add-cancelable distributive non empty doubleLoopStr, a,b being Element of R,
n being Element of NAT holds (a * n) * b = a * (n * b);
begin :: The Binomial Theorem
definition
let R be unital non empty doubleLoopStr, a,b be Element of R, n be Nat;
func (a,b) In_Power n -> FinSequence of the carrier of R means
:: BINOM:def 7
len it = n + 1 & for i,l,m being Nat st i in dom it & m = i - 1 & l = n - m
holds it/.i = (n choose m) * a|^l * b|^m;
end;
theorem :: BINOM:22
for R being right_zeroed unital non empty doubleLoopStr, a,b
being Element of R holds (a,b) In_Power 0 = <*1_R*>;
theorem :: BINOM:23
for R being right_zeroed unital non empty doubleLoopStr, a,b
being Element of R, n being Nat holds ((a,b) In_Power n).1 = a|^n;
theorem :: BINOM:24
for R being right_zeroed unital non empty doubleLoopStr, a,b
being Element of R, n being Nat holds ((a,b) In_Power n).(n+1) = b|^ n;
::$N Binomial Theorem
theorem :: BINOM:25
for R being Abelian add-associative left_zeroed right_zeroed
commutative associative add-cancelable distributive unital non empty
doubleLoopStr, a,b being Element of R, n being Element of NAT holds (a+b)|^n =
Sum((a,b) In_Power n);
theorem :: BINOM:26
for C,D be non empty set, b be Element of D, F be Function of [:C,D:],D
ex g being Function of [:NAT,C:],D st for a being Element of C holds
g.(0,a) = b & for n being Nat holds g.(n+1,a) = F.(a,g.(n,a));
theorem :: BINOM:27
for C,D be non empty set, b be Element of D, F be Function of [:D,C:],D
ex g being Function of [:C,NAT:],D st for a being Element of C holds
g.(a,0) = b & for n being Element of NAT holds g.(a,n+1) = F.(g.(a,n),a);