:: 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 b₁ being Complex st b₁ is real ;
by COMPLEX1:def 1;

cluster complex non real for object ;

correctness
existence
not for b₁ being Complex holds b₁ 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 b₁ being Relation st b₁ is REAL -valued holds
b₁ is COMPLEX -valued by NUMBERS:11;

cluster Relation-like RAT -valued -> REAL -valued for set ;

coherence
for b₁ being Relation st b₁ is RAT -valued holds
b₁ is REAL -valued by NUMBERS:12;

cluster Relation-like RAT -valued -> COMPLEX -valued for set ;

coherence
for b₁ being Relation st b₁ is RAT -valued holds
b₁ is COMPLEX -valued by NUMBERS:13;

cluster Relation-like INT -valued -> RAT -valued for set ;

coherence
for b₁ being Relation st b₁ is INT -valued holds
b₁ is RAT -valued ;

cluster Relation-like INT -valued -> REAL -valued for set ;

coherence
for b₁ being Relation st b₁ is INT -valued holds
b₁ is REAL -valued by NUMBERS:15;

cluster Relation-like INT -valued -> COMPLEX -valued for set ;

coherence
for b₁ being Relation st b₁ is INT -valued holds
b₁ is COMPLEX -valued by NUMBERS:16;

cluster Relation-like NAT -valued -> INT -valued for set ;

coherence
for b₁ being Relation st b₁ is NAT -valued holds
b₁ is INT -valued ;

cluster Relation-like NAT -valued -> RAT -valued for set ;

coherence
for b₁ being Relation st b₁ is NAT -valued holds
b₁ is RAT -valued ;

cluster Relation-like NAT -valued -> REAL -valued for set ;

coherence
for b₁ being Relation st b₁ is NAT -valued holds
b₁ is REAL -valued by NUMBERS:19;

cluster Relation-like NAT -valued -> COMPLEX -valued for set ;

coherence
for b₁ being Relation st b₁ is NAT -valued holds
b₁ is COMPLEX -valued by NUMBERS:20;

cluster Relation-like real-valued -> REAL -valued for set ;

coherence
for b₁ being Relation st b₁ is real-valued holds
b₁ is REAL -valued

proof end;

cluster Relation-like complex-valued -> COMPLEX -valued for set ;

coherence
for b₁ being Relation st b₁ is complex-valued holds
b₁ 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 b₁ being FinSequence st b₁ is empty holds
b₁ 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 b₁ being FinSequence of D st b₁ is empty

proof end;

cluster empty -> nonnegative-yielding for FinSequence of D;

coherence
for b₁ being FinSequence of D st b₁ is empty holds
b₁ is nonnegative-yielding ;

end;

registration

cluster Relation-like INT -valued Function-like FinSequence-like nonnegative-yielding -> NAT -valued for set ;

coherence
for b₁ being FinSequence st b₁ is nonnegative-yielding & b₁ is INT -valued holds
b₁ is NAT -valued

proof end;

cluster nonnegative-yielding -> NAT -valued for FinSequence of INT ;

coherence
for b₁ being FinSequence of INT st b₁ is nonnegative-yielding holds
b₁ 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 b₃ -valued FinSequence st len r = i + j holds
ex p, q being b₃ -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 b₁ being FinSequence of REAL holds
( b₁ = (a,b) Subnomial n iff ( len b₁ = n + 1 & ( for i, l, m being Nat st i in dom b₁ & m = i - 1 & l = n - m holds
b₁ . 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 b₄ being FinSequence of REAL holds
( b₄ = (a,b) Subnomial n iff ( len b₄ = n + 1 & ( for i, l, m being Nat st i in dom b₄ & m = i - 1 & l = n - m holds
b₄ . 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 b₁ -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;