:: On Subnomials
:: by Rafa{\l} Ziobro
::
:: Received October 18, 2016
:: Copyright (c) 2016-2021 Association of Mizar Users


registration
let a be positive Real;
let n be Nat;
cluster a |^ n -> positive ;
coherence
a |^ n is positive
by PREPOWER:6;
end;

registration
let a be non negative Real;
let n be Nat;
cluster a |^ n -> non negative ;
coherence
not a |^ n is negative
proof end;
end;

registration
let a be non negative Real;
reduce sqrt (a |^ 2) to a;
reducibility
sqrt (a |^ 2) = a
proof end;
end;

registration
cluster complex real for object ;
correctness
existence
ex b1 being Complex st b1 is real
;
by COMPLEX1:def 1;
cluster complex non real for object ;
correctness
existence
not for b1 being Complex holds b1 is real
;
proof end;
end;

registration
let a be non real Complex;
cluster Im a -> non zero ;
coherence
not Im a is zero
proof end;
end;

registration
let a be Real;
reduce Re a to a;
reducibility
Re a = a
by COMPLEX1:def 1;
end;

theorem :: NEWTON04:1
for a being non zero Real
for a1 being Complex st a * a1 is Real holds
a1 is Real
proof end;

registration
cluster Relation-like REAL -valued -> COMPLEX -valued for set ;
coherence
for b1 being Relation st b1 is REAL -valued holds
b1 is COMPLEX -valued
by NUMBERS:11;
cluster Relation-like RAT -valued -> REAL -valued for set ;
coherence
for b1 being Relation st b1 is RAT -valued holds
b1 is REAL -valued
by NUMBERS:12;
cluster Relation-like RAT -valued -> COMPLEX -valued for set ;
coherence
for b1 being Relation st b1 is RAT -valued holds
b1 is COMPLEX -valued
by NUMBERS:13;
cluster Relation-like INT -valued -> RAT -valued for set ;
coherence
for b1 being Relation st b1 is INT -valued holds
b1 is RAT -valued
;
cluster Relation-like INT -valued -> REAL -valued for set ;
coherence
for b1 being Relation st b1 is INT -valued holds
b1 is REAL -valued
by NUMBERS:15;
cluster Relation-like INT -valued -> COMPLEX -valued for set ;
coherence
for b1 being Relation st b1 is INT -valued holds
b1 is COMPLEX -valued
by NUMBERS:16;
cluster Relation-like NAT -valued -> INT -valued for set ;
coherence
for b1 being Relation st b1 is NAT -valued holds
b1 is INT -valued
;
cluster Relation-like NAT -valued -> RAT -valued for set ;
coherence
for b1 being Relation st b1 is NAT -valued holds
b1 is RAT -valued
;
cluster Relation-like NAT -valued -> REAL -valued for set ;
coherence
for b1 being Relation st b1 is NAT -valued holds
b1 is REAL -valued
by NUMBERS:19;
cluster Relation-like NAT -valued -> COMPLEX -valued for set ;
coherence
for b1 being Relation st b1 is NAT -valued holds
b1 is COMPLEX -valued
by NUMBERS:20;
cluster Relation-like real-valued -> REAL -valued for set ;
coherence
for b1 being Relation st b1 is real-valued holds
b1 is REAL -valued
proof end;
cluster Relation-like complex-valued -> COMPLEX -valued for set ;
coherence
for b1 being Relation st b1 is complex-valued holds
b1 is COMPLEX -valued
proof end;
end;

registration
let a be object ;
reduce 1 * (len <*a*>) to 1;
reducibility
1 * (len <*a*>) = 1
by FINSEQ_1:40;
end;

registration
let a be object ;
let f be FinSequence;
reduce (<*a*> ^ f) . 1 to a;
reducibility
(<*a*> ^ f) . 1 = a
by FINSEQ_1:41;
reduce (f ^ <*a*>) . (1 + (len f)) to a;
reducibility
(f ^ <*a*>) . (1 + (len f)) = a
by FINSEQ_1:42;
end;

registration
let x be Complex;
reduce Sum <*x*> to x;
reducibility
Sum <*x*> = x
by RVSUM_2:30;
end;

registration
let f, g be FinSequence;
reduce (f ^ g) | (dom f) to f;
reducibility
(f ^ g) | (dom f) = f
by FINSEQ_1:21;
reduce (f ^ g) | (len f) to f;
reducibility
(f ^ g) | (len f) = f
proof end;
end;

theorem Th0: :: NEWTON04:2
for f being FinSequence ex D being non empty set st f is FinSequence of D
proof end;

registration
let f be FinSequence;
reduce f . 0 to 0 ;
reducibility
f . 0 = 0
proof end;
reduce f | (len f) to f;
reducibility
f | (len f) = f
proof end;
cluster f /^ (len f) -> empty ;
coherence
f /^ (len f) is empty
by RFINSEQ:27;
end;

registration
let n be Nat;
reduce card (Seg n) to n;
reducibility
card (Seg n) = n
by FINSEQ_1:57;
reduce card (Segm n) to n;
reducibility
card (Segm n) = n
by ORDINAL1:def 17;
end;

registration
let n be Nat;
reduce len (id (Seg n)) to n;
reducibility
len (id (Seg n)) = n
proof end;
reduce len (idseq n) to n;
reducibility
len (idseq n) = n
proof end;
end;

registration
let m, n be Nat;
reduce (idseq (m + n)) . m to m;
reducibility
(idseq (m + n)) . m = m
proof end;
reduce (Rev (idseq (m + (n + 1)))) . (m + 1) to n + 1;
reducibility
(Rev (idseq (m + (n + 1)))) . (m + 1) = n + 1
proof end;
end;

definition
let a, b be Nat;
:: original: min
redefine func min (a,b) -> Nat;
coherence
min (a,b) is Nat
by XXREAL_0:def 9;
:: original: max
redefine func max (a,b) -> Nat;
coherence
max (a,b) is Nat
by XXREAL_0:def 10;
end;

registration
let f be FinSequence;
let n be Nat;
reduce f | ((len f) + n) to f;
reducibility
f | ((len f) + n) = f
by FINSEQ_1:58, NAT_1:12;
reduce f | (Seg (max ((len f),n))) to f;
reducibility
f | (Seg (max ((len f),n))) = f
proof end;
cluster f /^ ((len f) + n) -> empty ;
coherence
f /^ ((len f) + n) is empty
proof end;
cluster (f /^ (len f)) . n -> zero ;
coherence
(f /^ (len f)) . n is zero
;
end;

theorem :: NEWTON04:3
for n being Element of NAT
for D being set
for f being FinSequence of D st n in dom f holds
len (f | n) = n
proof end;

theorem :: NEWTON04:4
for n being Element of NAT
for D being set
for f being FinSequence of D st n >= len f holds
len (f | n) = len f
proof end;

registration
let f be FinSequence;
let n be non zero Nat;
cluster f . ((len f) + n) -> zero ;
coherence
f . ((len f) + n) is zero
proof end;
end;

registration
let f be FinSequence of REAL ;
let i, j be Nat;
reduce (f | i) | (i + j) to f | i;
reducibility
(f | i) | (i + j) = f | i
proof end;
end;

registration
let a be Nat;
reduce Sum (a |-> 0) to 0 ;
reducibility
Sum (a |-> 0) = 0
by RVSUM_1:81;
cluster Sum (a |-> 0) -> zero ;
coherence
Sum (a |-> 0) is zero
;
end;

registration
let a be Nat;
let b be object ;
reduce len (a |-> b) to a;
reducibility
len (a |-> b) = a
by CARD_1:def 7;
end;

registration
let a be non zero Nat;
let b be object ;
cluster a |-> b -> non empty ;
coherence
not a |-> b is empty
;
cluster a |-> b -> constant ;
coherence
a |-> b is constant
proof end;
reduce the_value_of (a |-> b) to b;
reducibility
the_value_of (a |-> b) = b
proof end;
end;

registration
let f be constant FinSequence;
reduce Rev f to f;
reducibility
Rev f = f
proof end;
end;

registration
let a be Nat;
let b be non zero Nat;
let x be object ;
reduce ((a + b) |-> x) . b to x;
reducibility
((a + b) |-> x) . b = x
proof end;
cluster (a |-> x) . (a + b) -> zero ;
coherence
(a |-> x) . (a + b) is zero
proof end;
end;

registration
let a be object ;
let n be Nat;
reduce Rev (n |-> a) to n |-> a;
reducibility
Rev (n |-> a) = n |-> a
proof end;
end;

registration
let n be Nat;
reduce n choose (0 * 1) to 1;
reducibility
n choose (0 * 1) = 1
by NEWTON:19;
reduce n choose (n * 1) to 1;
reducibility
n choose (n * 1) = 1
by NEWTON:21;
end;

registration
let f be nonnegative-yielding FinSequence of REAL ;
let i be Nat;
cluster f . i -> non negative ;
coherence
not f . i is negative
proof end;
end;

registration
cluster Relation-like empty Function-like FinSequence-like -> nonpositive-yielding for set ;
coherence
for b1 being FinSequence st b1 is empty holds
b1 is nonpositive-yielding
proof end;
end;

registration
let f be nonpositive-yielding FinSequence of REAL ;
let i be Nat;
cluster f . i -> non positive ;
coherence
not f . i is positive
proof end;
end;

registration
let f be nonnegative-yielding FinSequence of REAL ;
let i, j be Nat;
cluster (f | j) . i -> non negative ;
coherence
not (f | j) . i is negative
proof end;
cluster (f /^ j) . i -> non negative ;
coherence
not (f /^ j) . i is negative
proof end;
end;

registration
let f be empty real-valued FinSequence;
cluster Product f -> non negative ;
coherence
not Product f is negative
by RVSUM_1:94;
end;

registration
let f be nonnegative-yielding FinSequence of REAL ;
cluster Sum f -> non negative ;
coherence
not Sum f is negative
proof end;
cluster Product f -> non negative ;
coherence
not Product f is negative
proof end;
end;

registration
let f be nonpositive-yielding FinSequence of REAL ;
cluster Sum f -> non positive ;
coherence
not Sum f is positive
proof end;
end;

registration
let a be object ;
let f be nonnegative-yielding FinSequence of REAL ;
cluster f . a -> non negative ;
coherence
not f . a is negative
proof end;
end;

registration
let a be object ;
let f be nonpositive-yielding FinSequence of REAL ;
cluster f . a -> non positive ;
coherence
not f . a is positive
proof end;
end;

registration
let D be set ;
let f, g be D -valued FinSequence;
cluster f ^ g -> D -valued ;
correctness
coherence
f ^ g is D -valued
;
proof end;
end;

registration
let f be FinSequence of REAL ;
let n be Nat;
cluster (f | n) /^ n -> empty ;
coherence
(f | n) /^ n is empty
;
cluster f /^ (max ((len f),n)) -> empty ;
coherence
f /^ (max ((len f),n)) is empty
proof end;
end;

registration
let D be set ;
cluster Relation-like omega -defined D -valued empty Function-like V32() FinSequence-like FinSubsequence-like for FinSequence of D;
existence
ex b1 being FinSequence of D st b1 is empty
proof end;
cluster empty -> nonnegative-yielding for FinSequence of D;
coherence
for b1 being FinSequence of D st b1 is empty holds
b1 is nonnegative-yielding
;
end;

registration
cluster Relation-like INT -valued Function-like FinSequence-like nonnegative-yielding -> NAT -valued for set ;
coherence
for b1 being FinSequence st b1 is nonnegative-yielding & b1 is INT -valued holds
b1 is NAT -valued
proof end;
cluster nonnegative-yielding -> NAT -valued for FinSequence of INT ;
coherence
for b1 being FinSequence of INT st b1 is nonnegative-yielding holds
b1 is NAT -valued
;
end;

registration
let f be COMPLEX -valued FinSequence;
reduce f + 0 to f;
reducibility
f + 0 = f
proof end;
reduce f - 0 to f;
reducibility
f - 0 = f
proof end;
end;

registration
let x be object ;
reduce <*x*> . 1 to x;
reducibility
<*x*> . 1 = x
by FINSEQ_1:def 8;
end;

theorem :: NEWTON04:5
for f being FinSequence
for P being Permutation of (dom f) holds P is Permutation of (dom (Rev f))
proof end;

theorem MATRIX94: :: NEWTON04:6
for n being Nat holds Rev (idseq n) is Permutation of (Seg n)
proof end;

theorem :: NEWTON04:7
for f being FinSequence holds idseq (len f) is Permutation of (dom f)
proof end;

theorem RFP: :: NEWTON04:8
for f being FinSequence holds Rev (idseq (len f)) is Permutation of (dom (Rev f))
proof end;

::stolen from EUCLID_7:def 2
theorem DR: :: NEWTON04:9
for f being Function
for h being Permutation of (dom f) holds dom (f * h) = dom f
proof end;

registration
let f be FinSequence;
let h be Permutation of (dom f);
cluster h (#) f -> FinSequence-like ;
coherence
f * h is FinSequence-like
proof end;
cluster h (#) f -> dom f -defined ;
coherence
f * h is dom f -defined
;
end;

theorem REV: :: NEWTON04:10
for f being FinSequence holds f = (Rev f) * (Rev (idseq (len f)))
proof end;

theorem FFE: :: NEWTON04:11
for f being FinSequence holds f, Rev f are_fiberwise_equipotent
proof end;

theorem :: NEWTON04:12
for i, j being Nat
for D being non empty set
for r being b3 -valued FinSequence st len r = i + j holds
ex p, q being b3 -valued FinSequence st
( len p = i & len q = j & r = p ^ q )
proof end;

theorem :: NEWTON04:13
for j being Nat
for f being nonnegative-yielding FinSequence of REAL holds Sum f >= Sum (f | j)
proof end;

theorem FXX: :: NEWTON04:14
for f being COMPLEX -valued FinSequence
for x1, x2 being Complex holds (f + x1) + x2 = f + (x1 + x2)
proof end;

registration
let f be COMPLEX -valued FinSequence;
let x be Complex;
reduce (f + x) - x to f;
reducibility
(f + x) - x = f
proof end;
reduce (f - x) + x to f;
reducibility
(f - x) + x = f
proof end;
end;

registration
let x, y be Real;
reduce max ((min (x,y)),(max (x,y))) to max (x,y);
reducibility
max ((min (x,y)),(max (x,y))) = max (x,y)
proof end;
reduce min ((min (x,y)),(max (x,y))) to min (x,y);
reducibility
min ((min (x,y)),(max (x,y))) = min (x,y)
proof end;
end;

registration
let x, y be Real;
let z be non negative Real;
reduce min ((min (x,y)),(y + z)) to min (x,y);
reducibility
min ((min (x,y)),(y + z)) = min (x,y)
proof end;
reduce max ((max (x,y)),(y - z)) to max (x,y);
reducibility
max ((max (x,y)),(y - z)) = max (x,y)
proof end;
end;

registration
let f be FinSequence;
let i, j be Nat;
reduce (f | i) | (i + j) to f | i;
reducibility
(f | i) | (i + j) = f | i
proof end;
end;

registration
let f be nonnegative-yielding FinSequence of REAL ;
let n be Nat;
cluster f | n -> nonnegative-yielding ;
coherence
f | n is nonnegative-yielding
proof end;
cluster f /^ n -> nonnegative-yielding ;
coherence
f /^ n is nonnegative-yielding
proof end;
end;

registration
let f be FinSequence of REAL ;
cluster f - (min f) -> nonnegative-yielding ;
coherence
f - (min f) is nonnegative-yielding
proof end;
cluster f - (max f) -> nonpositive-yielding ;
coherence
f - (max f) is nonpositive-yielding
proof end;
end;

registration
let f be FinSequence;
cluster Rev f -> len f -element ;
coherence
Rev f is len f -element
proof end;
end;

registration
let D be non empty set ;
let f be D -valued FinSequence;
cluster Rev f -> D -valued ;
coherence
Rev f is D -valued
proof end;
end;

registration
let a be Complex;
let f be complex-valued FinSequence;
cluster a * f -> len f -element ;
coherence
a (#) f is len f -element
proof end;
end;

registration
let a, b be Real;
let n be Nat;
reduce len ((a,b) In_Power ((n + 1) - 1)) to n + 1;
reducibility
len ((a,b) In_Power ((n + 1) - 1)) = n + 1
by NEWTON:def 4;
cluster (a,b) In_Power n -> n + 1 -element ;
coherence
(a,b) In_Power n is n + 1 -element
proof end;
end;

registration
let n be Nat;
reduce len (Newton_Coeff ((n + 1) - 1)) to n + 1;
reducibility
len (Newton_Coeff ((n + 1) - 1)) = n + 1
by NEWTON:def 5;
cluster Newton_Coeff n -> nonnegative-yielding ;
coherence
Newton_Coeff n is nonnegative-yielding
proof end;
cluster Newton_Coeff n -> n + 1 -element ;
coherence
Newton_Coeff n is n + 1 -element
proof end;
end;

registration
let n be non zero Nat;
reduce (Newton_Coeff n) . 2 to n;
reducibility
(Newton_Coeff n) . 2 = n
proof end;
reduce (Newton_Coeff n) . n to n;
reducibility
(Newton_Coeff n) . n = n
proof end;
end;

theorem F123: :: NEWTON04:15
for f1, f2, f3 being complex-valued Function holds (f1 (#) f2) (#) f3 = f1 (#) (f2 (#) f3)
proof end;

theorem :: NEWTON04:16
for f, g being FinSequence of COMPLEX
for i being object holds (f (#) g) . i = (f . i) * (g . i)
proof end;

theorem :: NEWTON04:17
for x, y being Real holds (max (x,y)) - (min (x,y)) = |.(x - y).|
proof end;

theorem :: NEWTON04:18
for x, y being Real holds
( (min (x,y)) * (max (x,y)) = x * y & (min (x,y)) + (max (x,y)) = x + y )
proof end;

theorem SF: :: NEWTON04:19
for j being Nat
for f being nonnegative-yielding FinSequence of REAL holds Sum f >= Sum (f | j)
proof end;

theorem :: NEWTON04:20
for i, j being Nat
for f being nonnegative-yielding FinSequence of REAL st i >= j holds
Sum (f | i) >= Sum (f | j)
proof end;

theorem SN: :: NEWTON04:21
for n being Nat
for f being nonnegative-yielding FinSequence of REAL holds Sum f >= f . n
proof end;

theorem DLS: :: NEWTON04:22
for f, g, h being FinSequence of COMPLEX st dom h = (dom f) /\ (dom g) holds
len h = min ((len f),(len g))
proof end;

theorem FLS: :: NEWTON04:23
for f, g being FinSequence of COMPLEX holds len (f + g) = min ((len f),(len g))
proof end;

theorem :: NEWTON04:24
for f, g being FinSequence of COMPLEX holds len (f (#) g) = min ((len f),(len g))
proof end;

theorem :: NEWTON04:25
for f, g being FinSequence of COMPLEX holds len (f - g) = min ((len f),(len g))
proof end;

theorem FS: :: NEWTON04:26
for n being Nat
for f, g being nonnegative-yielding FinSequence of REAL holds (f (#) g) . n <= (Sum f) * (g . n)
proof end;

theorem :: NEWTON04:27
for r being Real
for n being non zero Nat ex f being FinSequence of REAL st
( len f = n & Sum f = r )
proof end;

LmFG: for f, g being FinSequence of REAL st ( for x being Nat holds f . x >= g . x ) holds
Sum (f | (min ((len f),(len g)))) >= Sum (g | (min ((len f),(len g))))

proof end;

theorem SL: :: NEWTON04:28
for f being FinSequence of COMPLEX
for x being Complex holds f + x = f + ((len f) |-> x)
proof end;

theorem SFX: :: NEWTON04:29
for f being FinSequence of COMPLEX
for x being Complex holds Sum (f + x) = (Sum f) + (x * (len f))
proof end;

theorem :: NEWTON04:30
for f being complex-valued FinSequence
for x being Complex holds Sum (f - x) = (Sum f) - (x * (len f))
proof end;

theorem :: NEWTON04:31
for f being FinSequence of REAL
for g being nonnegative-yielding FinSequence of REAL st ( for x being Nat holds f . x >= g . x ) holds
f is nonnegative-yielding
proof end;

theorem NYS: :: NEWTON04:32
for f, g being FinSequence of REAL st ( for x being Nat holds f . x >= g . x ) holds
Sum f >= Sum g
proof end;

theorem S1: :: NEWTON04:33
for f being FinSequence of COMPLEX holds Sum (f | 1) = f . 1
proof end;

theorem S2: :: NEWTON04:34
for f being FinSequence of COMPLEX
for n being Nat holds Sum ((f /^ n) | 1) = f . (n + 1)
proof end;

theorem FINSEQ681: :: NEWTON04:35
for f being FinSequence
for a, b being Nat holds (f /^ a) /^ b = f /^ (a + b)
proof end;

theorem :: NEWTON04:36
for i being Nat
for f being FinSequence of COMPLEX holds f = ((f | i) ^ ((f /^ i) | 1)) ^ (f /^ (i + 1))
proof end;

theorem SUM: :: NEWTON04:37
for i being Nat
for f being FinSequence of COMPLEX holds Sum f = ((Sum (f | i)) + (f . (i + 1))) + (Sum (f /^ (i + 1)))
proof end;

theorem FINSEQ74: :: NEWTON04:38
for n being Nat
for f being FinSequence
for i being non zero Nat holds f . (n + i) = (f /^ n) . i
proof end;

theorem NYS1: :: NEWTON04:39
for f, g being FinSequence of REAL st ( for x being Nat holds
( f . x >= g . x & ex i being Nat st f . (i + 1) > g . (i + 1) ) ) holds
Sum f > Sum g
proof end;

theorem :: NEWTON04:40
for f, g being nonnegative-yielding FinSequence of REAL holds (Sum f) * (Sum g) >= Sum (f (#) g)
proof end;

theorem :: NEWTON04:41
for a being Complex
for f being complex-valued FinSequence holds ((len f) |-> a) (#) f = a (#) f
proof end;

theorem AMP: :: NEWTON04:42
for a, b being Complex holds a (#) <*b*> = <*(a * b)*>
proof end;

theorem ADP: :: NEWTON04:43
for a being Complex
for f, g being complex-valued FinSequence holds a (#) (f ^ g) = (a (#) f) ^ (a (#) g)
proof end;

theorem CREV: :: NEWTON04:44
for a being Complex
for f, g being complex-valued FinSequence st g = Rev f holds
Rev (a (#) f) = a (#) g
proof end;

:: Dwumian > Niedomian :)
definition
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);
correctness
coherence
((a,b) In_Power n) /" (Newton_Coeff n) is FinSequence of REAL
;
by NEWTON02:103;
end;

:: deftheorem defines Subnomial NEWTON04:def 1 :
for a, b being Real
for n being natural Number holds (a,b) Subnomial n = ((a,b) In_Power n) /" (Newton_Coeff n);

theorem DOMN: :: NEWTON04:45
for a, b being Real
for n being 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) )
proof end;

registration
let a, b be Real;
let n be Nat;
reduce len ((a,b) Subnomial ((n + 1) - 1)) to n + 1;
reducibility
len ((a,b) Subnomial ((n + 1) - 1)) = n + 1
proof end;
cluster (a,b) Subnomial n -> n + 1 -element ;
coherence
(a,b) Subnomial n is n + 1 -element
proof end;
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 ;
coherence
((a,b) In_Power n) . m is integer
proof end;
end;

registration
let a, b be Integer;
let n be Nat;
cluster (a,b) In_Power n -> INT -valued ;
coherence
(a,b) In_Power n is INT -valued
proof end;
end;

theorem NIS: :: NEWTON04:46
for n being Nat
for a, b being Integer
for k being Nat st k in dom (Newton_Coeff n) holds
(Newton_Coeff n) . k divides ((a,b) In_Power n) . k
proof end;

registration
let l, k be Nat;
cluster (l + k) choose k -> positive ;
coherence
(l + k) choose k is positive
proof end;
end;

registration
let l be Nat;
let k be non zero Nat;
cluster l choose (l + k) -> zero ;
coherence
l choose (l + k) is zero
proof end;
cluster (Newton_Coeff l) . ((l + k) + 1) -> zero ;
coherence
(Newton_Coeff l) . ((l + k) + 1) is zero
proof end;
end;

registration
let l, k be Nat;
cluster (Newton_Coeff (l + k)) . (k + 1) -> positive ;
coherence
(Newton_Coeff (l + k)) . (k + 1) is positive
proof end;
end;

theorem D1: :: NEWTON04:47
for k, l being Nat st k in dom (Newton_Coeff l) holds
not (Newton_Coeff l) . k is zero
proof end;

registration
let a, b be Integer;
let m, n be Nat;
cluster ((a,b) Subnomial n) . m -> integer ;
coherence
((a,b) Subnomial n) . m is integer
proof end;
end;

registration
let a, b be Integer;
let n be Nat;
cluster (a,b) Subnomial n -> INT -valued ;
coherence
(a,b) Subnomial n is INT -valued
proof end;
end;

LmS1: for a, b being Real
for n, i, l, m being Nat st i in dom ((a,b) Subnomial n) & m = i - 1 & l = n - m holds
((a,b) Subnomial n) . i = (a |^ l) * (b |^ m)

proof end;

definition
let a, b be Real;
let n be Nat;
:: original: Subnomial
redefine func (a,b) Subnomial n -> FinSequence of REAL means :Def2: :: 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) ) );
compatibility
for b1 being FinSequence of REAL holds
( b1 = (a,b) Subnomial n iff ( len b1 = n + 1 & ( for i, l, m being Nat st i in dom b1 & m = i - 1 & l = n - m holds
b1 . i = (a |^ l) * (b |^ m) ) ) )
proof end;
coherence
(a,b) Subnomial n is FinSequence of REAL
;
end;

:: deftheorem Def2 defines Subnomial NEWTON04:def 2 :
for a, b being Real
for n being Nat
for b4 being FinSequence of REAL holds
( b4 = (a,b) Subnomial n iff ( len b4 = n + 1 & ( for i, l, m being Nat st i in dom b4 & m = i - 1 & l = n - m holds
b4 . i = (a |^ l) * (b |^ m) ) ) );

registration
let a, b be positive Real;
let k, l be Nat;
cluster ((a,b) Subnomial (k + l)) . (k + 1) -> positive ;
coherence
((a,b) Subnomial (k + l)) . (k + 1) is positive
proof end;
end;

registration
let a, b be positive Real;
let n be Nat;
cluster Sum ((a,b) Subnomial n) -> positive ;
coherence
Sum ((a,b) Subnomial n) is positive
proof end;
end;

registration
let k be Nat;
let n be non zero Nat;
cluster ((0,0) In_Power n) . k -> zero ;
coherence
((0,0) In_Power n) . k is zero
proof end;
cluster ((0,0) Subnomial n) . k -> zero ;
coherence
((0,0) Subnomial n) . k is zero
proof end;
end;

registration
let n be non zero Nat;
cluster (0,0) In_Power n -> empty-yielding ;
coherence
(0,0) In_Power n is empty-yielding
proof end;
cluster (0,0) Subnomial n -> empty-yielding ;
coherence
(0,0) Subnomial n is empty-yielding
proof end;
end;

registration
let f be empty-yielding FinSequence of COMPLEX ;
cluster Sum f -> zero ;
coherence
Sum f is zero
proof end;
end;

registration
let n be Nat;
reduce (Newton_Coeff n) . 1 to 1;
correctness
reducibility
(Newton_Coeff n) . 1 = 1
;
proof end;
reduce (Newton_Coeff n) . (n + 1) to 1;
reducibility
(Newton_Coeff n) . (n + 1) = 1
proof end;
end;

theorem NS: :: NEWTON04:48
for a, b being Real
for n being 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) )
proof end;

theorem RS: :: NEWTON04:49
for n being Nat
for a, b being Real holds (a,b) Subnomial (n + 1) = (a * ((a,b) Subnomial n)) ^ <*(b |^ (n + 1))*>
proof end;

theorem LS: :: NEWTON04:50
for n being Nat
for a, b being Real holds (a,b) Subnomial (n + 1) = <*(a |^ (n + 1))*> ^ (b * ((a,b) Subnomial n))
proof end;

theorem SumS: :: NEWTON04:51
for a, b being Real
for n being Nat holds (a |^ (n + 1)) - (b |^ (n + 1)) = (a - b) * (Sum ((a,b) Subnomial n))
proof end;

theorem :: NEWTON04:52
for a being Real
for n being non zero Nat holds a |^ n = Sum ((a,0) Subnomial n)
proof end;

theorem :: NEWTON04:53
for a being Real
for n being Nat holds a |^ (n + 1) = ((Sum ((a,1) Subnomial n)) * (a - 1)) + 1
proof end;

theorem STT: :: NEWTON04:54
for a, b, c, d being Real
for n being Nat
for x being 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)
proof end;

theorem ST: :: NEWTON04:55
for a, b, c, d being Real
for n being Nat holds ((a * b),(c * d)) Subnomial n = ((a,d) Subnomial n) (#) ((b,c) Subnomial n)
proof end;

theorem DAB: :: NEWTON04:56
for a, b being Real
for n being Nat holds (a,b) Subnomial n = ((a,1) Subnomial n) (#) ((1,b) Subnomial n)
proof end;

theorem INS: :: NEWTON04:57
for a, b being Real
for n being Nat holds (a,b) In_Power n = (Newton_Coeff n) (#) ((a,b) Subnomial n)
proof end;

theorem :: NEWTON04:58
for a, b being Real
for n being 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) )
proof end;

theorem :: NEWTON04:59
for a, b, c, d being Real
for n being Nat holds ((a * b),(c * d)) In_Power n = ((Newton_Coeff n) (#) ((a,c) Subnomial n)) (#) ((b,d) Subnomial n)
proof end;

theorem CONST: :: NEWTON04:60
for a being Real
for n, i being Nat st i in dom ((a,a) Subnomial n) holds
((a,a) Subnomial n) . i = a |^ n
proof end;

theorem CONST1: :: NEWTON04:61
for n being Nat
for a being Real holds (a,a) Subnomial n = (n + 1) |-> (a |^ n)
proof end;

theorem PRA: :: NEWTON04:62
for n being Nat
for a being Real holds Product ((a,a) Subnomial n) = a |^ (n * (n + 1))
proof end;

theorem PRN: :: NEWTON04:63
for n being Nat
for f, g being b1 -element complex-valued FinSequence holds Product (f (#) g) = (Product f) * (Product g)
proof end;

theorem SAB: :: NEWTON04:64
for a, b being Real
for n being Nat holds (a,b) Subnomial n = Rev ((b,a) Subnomial n)
proof end;

registration
let n, i be Nat;
reduce ((1,1) Subnomial (n + i)) . (i + 1) to 1;
reducibility
((1,1) Subnomial (n + i)) . (i + 1) = 1
proof end;
end;

registration
let n be Nat;
let i be non zero Nat;
reduce ((1,(- 1)) Subnomial ((2 * i) + n)) . (2 * i) to - 1;
reducibility
((1,(- 1)) Subnomial ((2 * i) + n)) . (2 * i) = - 1
proof end;
end;

registration
let n be Nat;
let i be odd Nat;
reduce ((1,(- 1)) Subnomial (n + i)) . i to 1;
reducibility
((1,(- 1)) Subnomial (n + i)) . i = 1
proof end;
end;

registration
let a be Real;
let n be Nat;
cluster n |-> a -> constant ;
coherence
n |-> a is constant
proof end;
cluster (a,a) Subnomial n -> constant ;
coherence
(a,a) Subnomial n is constant
proof end;
end;

registration
let a, b be non negative Real;
let n, k be Nat;
cluster ((a,b) In_Power n) . k -> non negative ;
coherence
not ((a,b) In_Power n) . k is negative
proof end;
cluster ((a,b) Subnomial n) . k -> non negative ;
coherence
not ((a,b) Subnomial n) . k is negative
proof end;
end;

theorem SAA: :: NEWTON04:65
for a being Real
for n being Nat holds Sum ((a,a) Subnomial n) = (n + 1) * (a |^ n)
proof end;

theorem ES: :: NEWTON04:66
for a being Real
for n being even Nat holds Sum ((a,(- a)) Subnomial n) = a |^ n
proof end;

registration
let n be even Nat;
reduce Sum ((1,(- 1)) Subnomial n) to 1;
reducibility
Sum ((1,(- 1)) Subnomial n) = 1
proof end;
end;

registration
let a be Real;
let n be odd Nat;
cluster Sum ((a,(- a)) Subnomial n) -> zero ;
coherence
Sum ((a,(- a)) Subnomial n) is zero
proof end;
end;

registration
let n be Nat;
reduce Sum ((1,1) Subnomial ((n + 1) - 1)) to n + 1;
reducibility
Sum ((1,1) Subnomial ((n + 1) - 1)) = n + 1
proof end;
end;

registration
let n be Nat;
cluster Sum (Newton_Coeff n) -> non zero ;
coherence
not Sum (Newton_Coeff n) is zero
proof end;
end;

registration
let a, b be non negative Real;
let n be Nat;
cluster (a,b) Subnomial n -> nonnegative-yielding ;
coherence
(a,b) Subnomial n is nonnegative-yielding
proof end;
cluster (a,b) In_Power n -> nonnegative-yielding ;
coherence
(a,b) In_Power n is nonnegative-yielding
proof end;
cluster Sum ((a,b) Subnomial n) -> non negative ;
coherence
not Sum ((a,b) Subnomial n) is negative
;
cluster Sum ((a,b) In_Power n) -> non negative ;
coherence
not Sum ((a,b) In_Power n) is negative
;
end;

theorem SFE: :: NEWTON04:67
for n being Nat
for a, b being Real holds (a,b) Subnomial n,(b,a) Subnomial n are_fiberwise_equipotent
proof end;

theorem :: NEWTON04:68
for n being Nat
for a, b being Real holds Product ((a,b) Subnomial n) = Product ((b,a) Subnomial n) by SFE, RVSUM_3:4;

theorem :: NEWTON04:69
for n being Nat
for a being non negative Real holds Product ((a,1) Subnomial n) = a |^ ((n + 1) choose 2)
proof end;

theorem ES: :: NEWTON04:70
for k, n being Nat holds (n !) * (k !) <= (n + k) !
proof end;

theorem NCK: :: NEWTON04:71
for k, n being Nat holds
( (n + k) choose k = 1 iff ( n = 0 or k = 0 ) )
proof end;

theorem EZ: :: NEWTON04:72
for k, n being Nat holds
( (n !) * (k !) = (n + k) ! iff ( n = 0 or k = 0 ) )
proof end;

registration
let n, k be non zero Nat;
cluster ((n + k) !) - ((n !) * (k !)) -> positive ;
coherence
((n + k) !) - ((n !) * (k !)) is positive
proof end;
end;

theorem :: NEWTON04:73
for n being Nat
for a being Real holds Sum ((a,a) Subnomial n) = (Sum ((1,1) Subnomial n)) * (Sum ((a,0) In_Power n))
proof end;

theorem :: NEWTON04:74
for n being Nat
for a, b, c being Real holds Sum (((a + b),c) In_Power n) = Sum ((a,(b + c)) In_Power n)
proof end;

theorem NCI: :: NEWTON04:75
for i, n being Nat holds (Newton_Coeff n) . (i + 1) = n choose i
proof end;

theorem :: NEWTON04:76
for n being Nat holds (2 * n) choose n = ((2 * n) !) / ((n !) |^ 2)
proof end;

theorem :: NEWTON04:77
for n being Nat holds (Newton_Coeff ((2 * n) + 1)) . (n + 1) = (Newton_Coeff ((2 * n) + 1)) . (n + 2)
proof end;

theorem :: NEWTON04:78
for b, k, n being Nat
for a being non zero Integer st 1 <= k & k <= n holds
a divides ((a,b) Subnomial n) . k
proof end;

theorem DIS: :: NEWTON04:79
for i, n being Nat
for a, b being Integer holds a * b divides (((a,b) In_Power n) . i) - (((a,b) Subnomial n) . i)
proof end;

theorem INT436: :: NEWTON04:80
for f being INT -valued FinSequence
for a being Integer st ( for n being Nat st n in dom f holds
a divides f . n ) holds
a divides Sum f
proof end;

theorem :: NEWTON04:81
for n being Nat
for a, b being Integer holds (a * b) * (a - b) divides ((a - b) * ((a + b) |^ n)) - ((a |^ (n + 1)) - (b |^ (n + 1)))
proof end;

theorem ILS: :: NEWTON04:82
for i, n being Nat
for a, b being non negative Real holds ((a,b) In_Power n) . i >= ((a,b) Subnomial n) . i
proof end;

theorem SST: :: NEWTON04:83
for n being Nat
for a, b being non negative Real holds (a + b) |^ n >= Sum ((a,b) Subnomial n)
proof end;

theorem SLT: :: NEWTON04:84
for a, b being non negative Real
for n being non zero Nat holds (a |^ n) + (b |^ n) <= Sum ((a,b) Subnomial n)
proof end;

PLT: for a, b being non negative Real
for n being non zero Nat holds
( a * (((a + b) + b) |^ n) >= ((a + b) |^ (n + 1)) - (b |^ (n + 1)) & ((a + b) |^ (n + 1)) - (b |^ (n + 1)) >= a * (((a + b) |^ n) + (b |^ n)) )

proof end;

theorem :: NEWTON04:85
for a, b being non negative Real
for n being non zero Nat holds (a * ((a + (2 * b)) |^ n)) + (b |^ (n + 1)) >= (a + b) |^ (n + 1)
proof end;

theorem :: NEWTON04:86
for a, b being non negative Real
for n being non zero Nat holds (a * ((a + b) |^ n)) + ((a + b) * (b |^ n)) <= (a + b) |^ (n + 1)
proof end;

theorem SSI: :: NEWTON04:87
for a, b being positive Real
for n being non zero Nat holds Sum ((a,b) Subnomial (n + 1)) < Sum ((a,b) In_Power (n + 1))
proof end;

theorem :: NEWTON04:88
for a, b being positive Real
for n being non zero Nat holds Sum (((a + b),0) Subnomial (n + 1)) > Sum ((a,b) Subnomial (n + 1))
proof end;

theorem :: NEWTON04:89
for a, b being Real
for n, i being Nat holds ((a,b) Subnomial n) . i <= ((|.a.|,|.b.|) Subnomial n) . i
proof end;

theorem :: NEWTON04:90
for a being Real
for n being Nat
for i being odd Nat holds ((a,(- a)) Subnomial (n + i)) . i = a |^ (n + i)
proof end;

theorem :: NEWTON04:91
for a being Real
for n being Nat
for i being non zero Nat holds ((a,(- a)) Subnomial (n + (2 * i))) . (2 * i) = - (a |^ (n + (2 * i)))
proof end;

theorem SAN: :: NEWTON04:92
for a, b being Real
for n being Nat holds (a,b) Subnomial (n + 1) = <*(a |^ (n + 1))*> ^ (b * ((a,b) Subnomial n))
proof end;

theorem :: NEWTON04:93
for a, b being Real
for n being Nat holds (a,b) Subnomial (n + 2) = (<*(a |^ (n + 2))*> ^ ((a * b) * ((a,b) Subnomial n))) ^ <*(b |^ (n + 2))*>
proof end;