:: On Subnomials :: by Rafa{\l} Ziobro :: :: Received October 18, 2016 :: Copyright (c) 2016-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 FINSEQ_2, ABIAN, INT_1, ARYTM_3, XXREAL_0, CARD_1, ARYTM_1, COMPLEX1, REAL_1, XCMPLX_0, ORDINAL4, NEWTON, CARD_3, SUBSET_1, TARSKI, RFINSEQ, REALSET1, PARTFUN1, PARTFUN3, FUNCOP_1, FUNCT_2, NEWTON04, NUMBERS, NAT_1, FINSEQ_1, RELAT_1, FUNCT_1, XREAL_0, ORDINAL1, VALUED_0, XBOOLE_0, VALUED_1, FOMODEL0, RFINSEQ2, SQUARE_1, FINSEQ_5, CLASSES1; notations SQUARE_1, CARD_1, COMPLEX1, FUNCOP_1, FUNCT_2, FINSEQ_2, TARSKI, XXREAL_0, ABIAN, INT_1, NEWTON, PARTFUN1, RFINSEQ, FINSEQ_5, PARTFUN3, XBOOLE_0, ORDINAL1, XCMPLX_0, XREAL_0, NUMBERS, RELAT_1, FUNCT_1, RVSUM_1, FINSEQ_1, SUBSET_1, VALUED_0, VALUED_1, FOMODEL0, RFINSEQ2, CLASSES1; constructors SQUARE_1, NAT_D, NEWTON, RFINSEQ, WSIERP_1, RECDEF_1, RELSET_1, PARTFUN3, CLASSES1, RVSUM_2, SEQ_4, MATRIX_5, FINSEQ_5, ABIAN, REAL_1, FOMODEL0, RFINSEQ2; registrations ORDINAL1, XXREAL_0, XREAL_0, INT_1, NEWTON, WSIERP_1, NAT_6, FUNCT_1, CARD_1, RVSUM_1, RELAT_1, INT_6, PARTFUN3, TIETZE_2, FINSEQ_2, NEWTON02, PREPOWER, RVSUM_3, MEMBERED, COMPLEX1, MATRIX_9, FUNCT_2, FINSEQ_5, ABIAN, RELSET_1, NUMBERS, NAT_1, FINSEQ_1, XBOOLE_0, XCMPLX_0, VALUED_0, VALUED_1, FOMODEL0; requirements REAL, NUMERALS, BOOLE, SUBSET, ARITHM; begin reserve a,b,i,j,k,l,m,n for Nat; registration let a be positive Real, n be Nat; cluster a|^n -> positive; end; registration let a be non negative Real, n be Nat; cluster a|^n -> non negative; end; registration let a be non negative Real; reduce sqrt(a|^2) to a; end; registration cluster real for Complex; cluster non real for Complex; end; registration let a be non real Complex; cluster Im a -> non zero; end; registration let a be Real; reduce Re a to a; end; theorem :: NEWTON04:1 for a be non zero Real, a1 be Complex st a*a1 is Real holds a1 is Real; registration cluster REAL-valued -> COMPLEX-valued for Relation; cluster RAT-valued -> REAL-valued for Relation; cluster RAT-valued -> COMPLEX-valued for Relation; cluster INT-valued -> RAT-valued for Relation; cluster INT-valued -> REAL-valued for Relation; cluster INT-valued -> COMPLEX-valued for Relation; cluster NAT-valued -> INT-valued for Relation; cluster NAT-valued -> RAT-valued for Relation; cluster NAT-valued -> REAL-valued for Relation; cluster NAT-valued -> COMPLEX-valued for Relation; cluster real-valued -> REAL-valued for Relation; cluster complex-valued -> COMPLEX-valued for Relation; end; registration let a be object; reduce 1*len <*a*> to 1; end; registration let a be object, f be FinSequence; reduce (<*a*>^f).1 to a; reduce (f^<*a*>).(1+len f) to a; end; registration let x be Complex; reduce Sum <*x*> to x; end; registration let f,g be FinSequence; reduce (f^g)|(dom f) to f; reduce (f^g)|(len f) to f; end; theorem :: NEWTON04:2 for f be FinSequence holds ex D be non empty set st f is FinSequence of D; registration :: f|(dom f) -- RELAT_1 let f be FinSequence; reduce f.0 to 0; reduce f|(len f) to f; cluster f/^(len f) -> empty; end; registration let n be Nat; reduce card (Seg n) to n; reduce card (Segm n) to n; end; registration let n be Nat; reduce len (id Seg n) to n; reduce len idseq n to n; end; registration let m,n be Nat; reduce (idseq(m+n)).m to m; reduce Rev (idseq(m+(n+1))).(m+1) to n+1; end; definition let a,b be Nat; redefine func min(a,b) -> Nat; redefine func max(a,b) -> Nat; end; registration let f be FinSequence, n be Nat; reduce f|((len f)+n) to f; reduce f|(Seg (max((len f),n))) to f; cluster f/^((len f)+n) -> empty; cluster (f/^(len f)).n -> zero; end; theorem :: NEWTON04:3 for n be Element of NAT, D be set, f be FinSequence of D st n in dom f holds len(f|n) = n; theorem :: NEWTON04:4 for n be Element of NAT, D be set, f be FinSequence of D st n >= len f holds len(f|n) = len f; registration let f be FinSequence, n be non zero Nat; cluster f.((len f)+n) -> zero; end; registration let f be FinSequence of REAL, i,j be Nat; reduce ((f|i)|(i+j)) to f|i; end; registration let a be Nat; reduce Sum (a |-> 0) to 0; cluster Sum (a|->0) -> zero; end; registration let a be Nat, b be object; reduce len (a |-> b) to a; end; registration let a be non zero Nat, b be object; cluster (a |-> b) -> non empty; cluster (a |-> b) -> constant; reduce the_value_of (a |-> b) to b; end; registration let f be constant FinSequence; reduce Rev f to f; end; registration let a be Nat,b be non zero Nat, x be object; reduce ((a+b)|-> x).b to x; cluster (a |-> x).(a+b) -> zero; end; registration let a be object, n be Nat; reduce Rev (n|-> a) to n|-> a; end; registration let n be Nat; reduce n choose (0*1) to 1; reduce n choose (n*1) to 1; end; registration let f be nonnegative-yielding FinSequence of REAL, i be Nat; cluster f.i -> non negative; end; registration :: see TIETZE_2 cluster empty -> nonpositive-yielding for FinSequence; end; registration let f be nonpositive-yielding FinSequence of REAL, i be Nat; cluster f.i -> non positive; end; registration let f be nonnegative-yielding FinSequence of REAL, i,j be Nat; cluster (f|j).i -> non negative; cluster (f/^j).i -> non negative; end; registration let f be empty real-valued FinSequence; cluster Product f -> non negative; end; registration let f be nonnegative-yielding FinSequence of REAL; cluster Sum f -> non negative; cluster Product f -> non negative; end; registration let f be nonpositive-yielding FinSequence of REAL; cluster Sum f -> non positive; end; registration let a be object,f be nonnegative-yielding FinSequence of REAL; cluster f.a -> non negative; end; registration let a be object, f be nonpositive-yielding FinSequence of REAL; cluster f.a -> non positive; end; registration let D be set; let f,g be D-valued FinSequence; cluster f^g -> D-valued; end; registration let f be FinSequence of REAL, n be Nat; cluster (f|n)/^n -> empty; cluster f/^(max((len f),n)) -> empty; end; registration let D be set; cluster empty for FinSequence of D; cluster empty -> nonnegative-yielding for FinSequence of D; end; registration cluster nonnegative-yielding INT-valued -> NAT-valued for FinSequence; cluster nonnegative-yielding -> NAT-valued for FinSequence of INT; end; registration let f be COMPLEX-valued FinSequence; reduce f+0 to f; reduce f-0 to f; end; registration let x be object; reduce <*x*>.1 to x; end; theorem :: NEWTON04:5 for f be FinSequence, P be Permutation of (dom f) holds P is Permutation of (dom (Rev f)); theorem :: NEWTON04:6 Rev idseq n is Permutation of (Seg n); theorem :: NEWTON04:7 for f be FinSequence holds idseq (len f) is Permutation of (dom f); theorem :: NEWTON04:8 for f be FinSequence holds Rev (idseq (len f)) is Permutation of dom (Rev f); ::stolen from EUCLID_7:def 2 theorem :: NEWTON04:9 for f be Function, h be Permutation of dom f holds dom (f*h) = dom f; registration let f be FinSequence, h be Permutation of (dom f); cluster f*h -> FinSequence-like; cluster f*h -> dom f-defined; end; theorem :: NEWTON04:10 for f be FinSequence holds f = (Rev f)*(Rev (idseq len f)); theorem :: NEWTON04:11 for f be FinSequence holds f,(Rev f) are_fiberwise_equipotent; theorem :: NEWTON04:12 for D be non empty set, r be D-valued FinSequence st len r = i+j ex p,q be D-valued FinSequence st len p = i & len q = j & r = p^q; theorem :: NEWTON04:13 for f be nonnegative-yielding FinSequence of REAL holds Sum f >= Sum (f|j); theorem :: NEWTON04:14 for f be COMPLEX-valued FinSequence, x1,x2 be Complex holds f+x1+x2 = f+(x1+x2); registration let f be COMPLEX-valued FinSequence, x be Complex; reduce f+x-x to f; reduce f-x+x to f; end; registration let x,y be Real; reduce max (min(x,y),max(x,y)) to max(x,y); reduce min (min(x,y),max(x,y)) to min(x,y); end; registration let x,y be Real, z be non negative Real; reduce min (min(x,y),y+z) to min (x,y); reduce max (max(x,y),y-z) to max (x,y); end; registration let f be FinSequence, i,j be Nat; reduce ((f|i)|(i+j)) to f|i; end; registration let f be nonnegative-yielding FinSequence of REAL, n be Nat; cluster f|n -> nonnegative-yielding; cluster f/^n -> nonnegative-yielding; end; registration let f be FinSequence of REAL; cluster f - (min f) -> nonnegative-yielding; cluster f - (max f) -> nonpositive-yielding; end; registration let f be FinSequence; cluster Rev f -> (len f)-element; end; registration let D be non empty set; let f be D-valued FinSequence; cluster Rev f -> D-valued; end; registration let a be Complex, f be complex-valued FinSequence; cluster a(#)f -> (len f)-element; end; registration let a,b be Real, n be Nat; reduce len ((a,b) In_Power (n+1-1)) to n+1; cluster (a,b) In_Power n -> (n+1)-element; end; registration let n be Nat; reduce len (Newton_Coeff (n+1-1)) to n+1; cluster Newton_Coeff n -> nonnegative-yielding; cluster Newton_Coeff n -> (n+1)-element; end; registration let n be non zero Nat; reduce (Newton_Coeff n).2 to n; reduce (Newton_Coeff n).n to n; end; theorem :: NEWTON04:15 for f1,f2,f3 be complex-valued Function holds (f1 (#) f2) (#) f3 = f1 (#) (f2 (#) f3); theorem :: NEWTON04:16 for f,g be FinSequence of COMPLEX, i be object holds (f (#) g).i = f.i*g.i; theorem :: NEWTON04:17 for x,y be Real holds max(x,y) - min(x,y)= |.x-y.|; theorem :: NEWTON04:18 for x,y be Real holds min(x,y)*max(x,y) = x*y & min(x,y) + max(x,y) = x+y; theorem :: NEWTON04:19 for f be nonnegative-yielding FinSequence of REAL holds Sum f >= Sum (f|j); theorem :: NEWTON04:20 :: POLYNOM3:18: for f be nonnegative-yielding FinSequence of REAL holds i >= j implies Sum (f|i) >= Sum (f|j); theorem :: NEWTON04:21 for f be nonnegative-yielding FinSequence of REAL holds Sum f >= f.n; theorem :: NEWTON04:22 for f,g,h be FinSequence of COMPLEX st dom h = dom f /\ dom g holds len h = min (len f,len g); theorem :: NEWTON04:23 for f,g be FinSequence of COMPLEX holds len (f + g) = min (len f, len g); theorem :: NEWTON04:24 for f,g be FinSequence of COMPLEX holds len (f (#) g) = min (len f, len g); theorem :: NEWTON04:25 for f,g be FinSequence of COMPLEX holds len (f - g) = min (len f, len g); theorem :: NEWTON04:26 for f,g be nonnegative-yielding FinSequence of REAL holds (f(#)g).n <= (Sum f)*g.n; theorem :: NEWTON04:27 for r be Real, n be non zero Nat holds ex f be FinSequence of REAL st len f = n & Sum f = r; theorem :: NEWTON04:28 for f be FinSequence of COMPLEX, x be Complex holds f + x = f + ((len f) |-> x); theorem :: NEWTON04:29 for f be FinSequence of COMPLEX, x be Complex holds Sum (f+x) = Sum f + x*(len f); theorem :: NEWTON04:30 for f be complex-valued FinSequence, x be Complex holds Sum (f-x) = Sum f - x*(len f); theorem :: NEWTON04:31 for f be FinSequence of REAL, g be nonnegative-yielding FinSequence of REAL st (for x be Nat holds f.x >= g.x) holds f is nonnegative-yielding; theorem :: NEWTON04:32 for f,g be FinSequence of REAL st (for x be Nat holds f.x >= g.x) holds Sum f >= Sum g; theorem :: NEWTON04:33 for f be FinSequence of COMPLEX holds Sum (f|(1 qua Nat)) = f.(1 qua Nat); theorem :: NEWTON04:34 for f be FinSequence of COMPLEX, n be Nat holds Sum ((f/^n)| 1) = f.(n+1); theorem :: NEWTON04:35 for f be FinSequence, a,b be Nat holds (f/^a)/^b = f/^(a+b); theorem :: NEWTON04:36 ::POLYNOM4:1 for f be FinSequence of COMPLEX holds f = (f|i)^((f/^i)|(1 qua Nat))^(f/^(i+1)); theorem :: NEWTON04:37 for f be FinSequence of COMPLEX holds Sum f = Sum (f|i) + f.(i+1) + Sum (f/^(i+1)); theorem :: NEWTON04:38 for f be FinSequence, i be non zero Nat holds f.(n+i) = (f/^n).i; theorem :: NEWTON04:39 for f,g be FinSequence of REAL st (for x be Nat holds f.x >= g.x & ex i st f.(i+1) > g.(i+1)) holds Sum f > Sum g; theorem :: NEWTON04:40 for f,g being nonnegative-yielding FinSequence of REAL holds (Sum f)*(Sum g) >= Sum(f(#)g); theorem :: NEWTON04:41 for a be Complex, f be complex-valued FinSequence holds ((len f)|->a)(#)f = a(#)f; theorem :: NEWTON04:42 for a,b be Complex holds a(#)<*b*> = <*a*b*>; theorem :: NEWTON04:43 for a be Complex, f,g be complex-valued FinSequence holds a(#)(f^g) = (a(#)f)^(a(#)g); theorem :: NEWTON04:44 for a be Complex, f,g be complex-valued FinSequence st g = Rev f holds Rev (a(#)f) = a(#)g; :: Dwumian > Niedomian :) definition :: see Newton:def 4,def 5 let a,b be Real; let n be natural Number; func (a,b) Subnomial n -> FinSequence of REAL equals :: NEWTON04:def 1 ((a,b) In_Power n) /" (Newton_Coeff n); end; theorem :: NEWTON04:45 for a,b be Real, n be Nat holds len ((a,b) In_Power n) = len (Newton_Coeff n) & len ((a,b) Subnomial n) = len (Newton_Coeff n) & len ((a,b) In_Power n) = len ((a,b) Subnomial n) & dom ((a,b) In_Power n) = dom (Newton_Coeff n) & dom ((a,b) Subnomial n) = dom (Newton_Coeff n) & dom ((a,b) In_Power n) = dom ((a,b) Subnomial n); registration let a,b be Real, n be Nat; reduce len ((a,b) Subnomial (n+1-1)) to n+1; cluster (a,b) Subnomial n -> (n+1)-element; end; :: see NEWTON02 for Nat registration registration let a,b be Integer; let n,m be Nat; cluster ((a,b) In_Power n).m -> integer; end; registration let a,b be Integer; let n be Nat; cluster (a,b) In_Power n -> INT-valued; end; theorem :: NEWTON04:46 for a,b be Integer, k be Nat st k in dom (Newton_Coeff n) holds (Newton_Coeff n).k divides ((a,b) In_Power n).k; registration let l,k be Nat; cluster (l+k) choose k -> positive; end; registration let l be Nat, k be non zero Nat; cluster l choose (l+k) -> zero; cluster (Newton_Coeff l).(l+k+1) -> zero; end; registration let l be Nat, k be Nat; cluster (Newton_Coeff (l+k)).(k+1) -> positive; end; theorem :: NEWTON04:47 for k,l be Nat holds k in dom (Newton_Coeff l) implies (Newton_Coeff l).k is non zero; registration let a,b be Integer; let m,n be Nat; cluster ((a,b) Subnomial n).m -> integer; end; registration let a,b be Integer; let n be Nat; cluster (a,b) Subnomial n -> INT-valued; end; definition let a,b be Real, n be Nat; redefine func (a,b) Subnomial n -> FinSequence of REAL means :: NEWTON04:def 2 len it = n+1 & for i,l,m being Nat st i in dom it & m = i - 1 & l = n-m holds it.i = a|^l * b|^m; end; registration let a,b be positive Real, k,l be Nat; cluster ((a,b)Subnomial (k+l)).(k+1) -> positive; end; registration let a,b be positive Real, n be Nat; cluster Sum((a,b)Subnomial n) -> positive; end; registration let k be Nat, n be non zero Nat; cluster ((0,0) In_Power n).k -> zero; cluster ((0,0) Subnomial n).k -> zero; end; registration let n be non zero Nat; cluster ((0,0) In_Power n) -> empty-yielding; cluster ((0,0) Subnomial n) -> empty-yielding; end; registration let f be empty-yielding FinSequence of COMPLEX; cluster Sum f -> zero; end; registration let n be Nat; reduce (Newton_Coeff n).1 to 1; reduce (Newton_Coeff n).(n+1) to 1; end; theorem :: NEWTON04:48 for a,b be Real, n be Nat holds (((a,b) In_Power n).1 = ((a,b) Subnomial n).1) & (((a,b) In_Power n).(n+1) = ((a,b) Subnomial n).(n+1)); theorem :: NEWTON04:49 for a,b be Real holds (a,b) Subnomial (n+1) = (a*((a,b)Subnomial n))^<*b|^(n+1)*>; theorem :: NEWTON04:50 for a,b be Real holds (a,b) Subnomial (n+1) = <*a|^(n+1)*>^(b*((a,b)Subnomial n)); theorem :: NEWTON04:51 for a,b be Real, n be Nat holds a|^(n+1) - b|^(n+1) = (a-b)*Sum((a,b)Subnomial n); theorem :: NEWTON04:52 for a be Real, n be non zero Nat holds a|^n = Sum ((a,0) Subnomial n); theorem :: NEWTON04:53 for a be Real, n be Nat holds a|^(n+1) = Sum((a,1) Subnomial n)*(a-1) + 1; theorem :: NEWTON04:54 for a,b,c,d be Real, n be Nat, x be object st x in dom ((a*b,c*d) Subnomial n) holds ((a*b,c*d) Subnomial n).x = ((a,d) Subnomial n).x * ((b,c) Subnomial n).x; theorem :: NEWTON04:55 for a,b,c,d be Real, n be Nat holds (a*b,c*d) Subnomial n = ((a,d) Subnomial n) (#) ((b,c) Subnomial n); theorem :: NEWTON04:56 for a,b be Real, n be Nat holds (a,b) Subnomial n = ((a,1) Subnomial n) (#) ((1,b) Subnomial n); theorem :: NEWTON04:57 for a,b be Real, n be Nat holds (a,b) In_Power n = (Newton_Coeff n) (#) ((a,b) Subnomial n); theorem :: NEWTON04:58 for a,b be Real, n be Nat holds (a,b) In_Power n = ((a,1) In_Power n) (#) ((1,b) Subnomial n) & (a,b) In_Power n = ((a,1) Subnomial n) (#) ((1,b) In_Power n); theorem :: NEWTON04:59 for a,b,c,d be Real, n be Nat holds (a*b,c*d) In_Power n = (Newton_Coeff n) (#) ((a,c) Subnomial n) (#) ((b,d) Subnomial n); theorem :: NEWTON04:60 for a be Real, n,i be Nat st i in dom ((a,a)Subnomial n) holds ((a,a)Subnomial n).i = a|^n; theorem :: NEWTON04:61 for n be Nat, a be Real holds ((a,a)Subnomial n) = ((n+1)|-> a|^n); theorem :: NEWTON04:62 for n be Nat, a be Real holds Product((a,a)Subnomial n) = a|^(n*(n+1)); theorem :: NEWTON04:63 for n be Nat, f,g be n-element complex-valued FinSequence holds Product (f(#)g)= (Product f) * (Product g); theorem :: NEWTON04:64 for a,b be Real, n be Nat holds (a,b) Subnomial n = Rev ((b,a) Subnomial n); registration let n be Nat, i be Nat; reduce ((1,1)Subnomial (n+i)).(i+1) to 1; end; registration let n be Nat,i be non zero Nat; reduce ((1,-1) Subnomial (2*i+n)).(2*i) to -1; end; registration let n be Nat, i be odd Nat; reduce ((1,-1) Subnomial (n+i)).i to 1; end; registration let a be Real, n be Nat; cluster n|->a -> constant; cluster ((a,a)Subnomial n) -> constant; end; registration let a,b be non negative Real; let n,k be Nat; cluster ((a,b) In_Power n).k -> non negative; cluster ((a,b) Subnomial n).k -> non negative; end; theorem :: NEWTON04:65 for a be Real, n be Nat holds Sum ((a,a)Subnomial n) = (n+1)*a|^n; theorem :: NEWTON04:66 for a be Real, n be even Nat holds Sum ((a,-a) Subnomial n) = a|^n; registration let n be even Nat; reduce Sum((1,-1) Subnomial n) to 1; end; registration let a be Real, n be odd Nat; cluster Sum((a,-a) Subnomial n) -> zero; end; registration let n be Nat; reduce Sum ((1,1)Subnomial (n+1-1)) to n+1; end; registration let n be Nat; cluster Sum (Newton_Coeff n) -> non zero; end; registration let a,b be non negative Real, n be Nat; cluster (a,b) Subnomial n -> nonnegative-yielding; cluster (a,b) In_Power n -> nonnegative-yielding; cluster Sum ((a,b) Subnomial n) -> non negative; cluster Sum ((a,b) In_Power n) -> non negative; end; theorem :: NEWTON04:67 for a,b be Real holds ((a,b)Subnomial n), ((b,a) Subnomial n) are_fiberwise_equipotent; theorem :: NEWTON04:68 for a,b be Real holds Product (a,b) Subnomial n = Product (b,a) Subnomial n; theorem :: NEWTON04:69 for a be non negative Real holds Product ((a,1) Subnomial n) = a|^((n+1) choose 2); theorem :: NEWTON04:70 (n!)*(k!) <= (n+k)!; theorem :: NEWTON04:71 (n+k) choose k = 1 iff n = 0 or k = 0; theorem :: NEWTON04:72 (n!)*(k!) = (n+k)! iff (n = 0 or k = 0); registration let n,k be non zero Nat; cluster (n+k)!-(n!)*(k!) -> positive; end; theorem :: NEWTON04:73 for a be Real holds Sum ((a,a) Subnomial n) = Sum((1,1) Subnomial n)*Sum ((a,0)In_Power n); theorem :: NEWTON04:74 for a,b,c be Real holds Sum ((a+b,c) In_Power n) = Sum((a,b+c) In_Power n); theorem :: NEWTON04:75 (Newton_Coeff n).(i+1) = n choose i; theorem :: NEWTON04:76 2*n choose n = (2*n)!/((n!)|^2); theorem :: NEWTON04:77 (Newton_Coeff (2*n+1)).(n+1) = (Newton_Coeff (2*n+1)).(n+2); theorem :: NEWTON04:78 for a be non zero Integer st 1 <= k <= n holds a divides ((a,b) Subnomial n).k; theorem :: NEWTON04:79 for a,b be Integer holds a*b divides ((a,b)In_Power n).i - ((a,b) Subnomial n).i; theorem :: NEWTON04:80 for f be INT-valued FinSequence, a be Integer st (for n be Nat st n in dom f holds a divides f.n) holds a divides Sum f; theorem :: NEWTON04:81 for a,b be Integer holds a*b*(a-b) divides (a-b)*(a+b)|^n -(a|^(n+1)-b|^(n+1)); theorem :: NEWTON04:82 for a,b be non negative Real holds ((a,b) In_Power n).i >= ((a,b) Subnomial n).i; theorem :: NEWTON04:83 for a,b be non negative Real holds (a+b)|^n >= Sum((a,b) Subnomial n); theorem :: NEWTON04:84 for a,b be non negative Real, n be non zero Nat holds a|^n + b|^n <= Sum((a,b) Subnomial n); theorem :: NEWTON04:85 for a,b be non negative Real, n be non zero Nat holds a*(a+2*b)|^n + b|^(n+1) >= (a+b)|^(n+1); theorem :: NEWTON04:86 for a,b be non negative Real, n be non zero Nat holds a*(a+b)|^n + (a+b)*b|^n <= (a+b)|^(n+1); theorem :: NEWTON04:87 for a,b be positive Real, n be non zero Nat holds Sum ((a,b) Subnomial (n+1)) < Sum ((a,b) In_Power (n+1)); theorem :: NEWTON04:88 for a,b be positive Real, n be non zero Nat holds Sum ((a+b,0)Subnomial (n+1)) > Sum ((a,b)Subnomial (n+1)); theorem :: NEWTON04:89 for a,b be Real, n,i be Nat holds ((a,b) Subnomial n).i <= ((|.a.|,|.b.|)Subnomial n).i; theorem :: NEWTON04:90 for a be Real, n be Nat, i be odd Nat holds ((a,-a) Subnomial (n+i)).i = a|^(n+i); theorem :: NEWTON04:91 for a be Real, n be Nat, i be non zero Nat holds ((a,-a) Subnomial (n+2*i)).(2*i) = -a|^(n+2*i); theorem :: NEWTON04:92 for a,b be Real, n be Nat holds (a,b) Subnomial (n+1) = <*a|^(n+1)*>^(b*(a,b) Subnomial n); theorem :: NEWTON04:93 for a,b be Real, n be Nat holds (a,b) Subnomial (n+2) = <*a|^(n+2)*>^(a*b*(a,b) Subnomial n)^<*b|^(n+2)*>;