:: 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);