:: by Rafa{\l} Ziobro

::

:: Received October 18, 2016

:: Copyright (c) 2016-2018 Association of Mizar Users

registration
end;

registration
end;

registration

correctness

existence

ex b_{1} being Complex st b_{1} is real ;

by COMPLEX1:def 1;

correctness

existence

not for b_{1} being Complex holds b_{1} is real ;

end;
existence

ex b

by COMPLEX1:def 1;

correctness

existence

not for b

proof end;

registration
end;

registration

coherence

for b_{1} being Relation st b_{1} is REAL -valued holds

b_{1} is COMPLEX -valued
by NUMBERS:11;

coherence

for b_{1} being Relation st b_{1} is RAT -valued holds

b_{1} is REAL -valued
by NUMBERS:12;

coherence

for b_{1} being Relation st b_{1} is RAT -valued holds

b_{1} is COMPLEX -valued
by NUMBERS:13;

coherence

for b_{1} being Relation st b_{1} is INT -valued holds

b_{1} is RAT -valued
;

coherence

for b_{1} being Relation st b_{1} is INT -valued holds

b_{1} is REAL -valued
by NUMBERS:15;

coherence

for b_{1} being Relation st b_{1} is INT -valued holds

b_{1} is COMPLEX -valued
by NUMBERS:16;

coherence

for b_{1} being Relation st b_{1} is NAT -valued holds

b_{1} is INT -valued
;

coherence

for b_{1} being Relation st b_{1} is NAT -valued holds

b_{1} is RAT -valued
;

coherence

for b_{1} being Relation st b_{1} is NAT -valued holds

b_{1} is REAL -valued
by NUMBERS:19;

coherence

for b_{1} being Relation st b_{1} is NAT -valued holds

b_{1} is COMPLEX -valued
by NUMBERS:20;

coherence

for b_{1} being Relation st b_{1} is real-valued holds

b_{1} is REAL -valued

for b_{1} being Relation st b_{1} is complex-valued holds

b_{1} is COMPLEX -valued

end;
for b

b

coherence

for b

b

coherence

for b

b

coherence

for b

b

coherence

for b

b

coherence

for b

b

coherence

for b

b

coherence

for b

b

coherence

for b

b

coherence

for b

b

coherence

for b

b

proof end;

coherence for b

b

proof end;

registration
end;

registration

let a be object ;

let f be FinSequence;

reducibility

(<*a*> ^ f) . 1 = a by FINSEQ_1:41;

reducibility

(f ^ <*a*>) . (1 + (len f)) = a by FINSEQ_1:42;

end;
let f be FinSequence;

reducibility

(<*a*> ^ f) . 1 = a by FINSEQ_1:41;

reducibility

(f ^ <*a*>) . (1 + (len f)) = a by FINSEQ_1:42;

registration
end;

registration

let f, g be FinSequence;

reducibility

(f ^ g) | (dom f) = f by FINSEQ_1:21;

reducibility

(f ^ g) | (len f) = f

end;
reducibility

(f ^ g) | (dom f) = f by FINSEQ_1:21;

reducibility

(f ^ g) | (len f) = f

proof end;

registration

let f be FinSequence;

reducibility

f . 0 = 0

f | (len f) = f

f /^ (len f) is empty

end;
reducibility

f . 0 = 0

proof end;

reducibility f | (len f) = f

proof end;

coherence f /^ (len f) is empty

proof end;

registration

let n be Nat;

reducibility

card (Seg n) = n by FINSEQ_1:57;

reducibility

card (Segm n) = n by ORDINAL1:def 17;

end;
reducibility

card (Seg n) = n by FINSEQ_1:57;

reducibility

card (Segm n) = n by ORDINAL1:def 17;

registration

let n be Nat;

reducibility

len (id (Seg n)) = n

len (idseq n) = n

end;
reducibility

len (id (Seg n)) = n

proof end;

reducibility len (idseq n) = n

proof end;

registration

let m, n be Nat;

reducibility

(idseq (m + n)) . m = m

(Rev (idseq (m + (n + 1)))) . (m + 1) = n + 1

end;
reducibility

(idseq (m + n)) . m = m

proof end;

reducibility (Rev (idseq (m + (n + 1)))) . (m + 1) = n + 1

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

registration

let f be FinSequence;

let n be Nat;

reducibility

f | ((len f) + n) = f by FINSEQ_1:58, NAT_1:12;

reducibility

f | (Seg (max ((len f),n))) = f

f /^ ((len f) + n) is empty

(f /^ (len f)) . n is zero ;

end;
let n be Nat;

reducibility

f | ((len f) + n) = f by FINSEQ_1:58, NAT_1:12;

reducibility

f | (Seg (max ((len f),n))) = f

proof end;

coherence f /^ ((len f) + n) is empty

proof end;

coherence (f /^ (len f)) . n is zero ;

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

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

for D being set

for f being FinSequence of D st n >= len f holds

len (f | n) = len f

proof end;

registration
end;

registration
end;

registration
end;

registration

let a be non zero Nat;

let b be object ;

coherence

not a |-> b is empty ;

coherence

a |-> b is constant

the_value_of (a |-> b) = b

end;
let b be object ;

coherence

not a |-> b is empty ;

coherence

a |-> b is constant

proof end;

reducibility the_value_of (a |-> b) = b

proof end;

registration
end;

registration

let a be Nat;

let b be non zero Nat;

let x be object ;

reducibility

((a + b) |-> x) . b = x

(a |-> x) . (a + b) is zero

end;
let b be non zero Nat;

let x be object ;

reducibility

((a + b) |-> x) . b = x

proof end;

coherence (a |-> x) . (a + b) is zero

proof end;

registration

let n be Nat;

reducibility

n choose (0 * 1) = 1 by NEWTON:19;

reducibility

n choose (n * 1) = 1 by NEWTON:21;

end;
reducibility

n choose (0 * 1) = 1 by NEWTON:19;

reducibility

n choose (n * 1) = 1 by NEWTON:21;

registration

let f be nonnegative-yielding FinSequence of REAL ;

let i be Nat;

coherence

not f . i is negative

end;
let i be Nat;

coherence

not f . i is negative

proof end;

registration

coherence

for b_{1} being FinSequence st b_{1} is empty holds

b_{1} is nonpositive-yielding

end;
for b

b

proof end;

registration

let f be nonpositive-yielding FinSequence of REAL ;

let i be Nat;

coherence

not f . i is positive

end;
let i be Nat;

coherence

not f . i is positive

proof end;

registration

let f be nonnegative-yielding FinSequence of REAL ;

let i, j be Nat;

coherence

not (f | j) . i is negative

not (f /^ j) . i is negative

end;
let i, j be Nat;

coherence

not (f | j) . i is negative

proof end;

coherence not (f /^ j) . i is negative

proof end;

registration
end;

registration

let f be nonnegative-yielding FinSequence of REAL ;

coherence

not Sum f is negative

not Product f is negative

end;
coherence

not Sum f is negative

proof end;

coherence not Product f is negative

proof end;

registration
end;

registration

let a be object ;

let f be nonnegative-yielding FinSequence of REAL ;

coherence

not f . a is negative

end;
let f be nonnegative-yielding FinSequence of REAL ;

coherence

not f . a is negative

proof end;

registration

let a be object ;

let f be nonpositive-yielding FinSequence of REAL ;

coherence

not f . a is positive

end;
let f be nonpositive-yielding FinSequence of REAL ;

coherence

not f . a is positive

proof end;

registration

let D be set ;

let f, g be D -valued FinSequence;

correctness

coherence

f ^ g is D -valued ;

end;
let f, g be D -valued FinSequence;

correctness

coherence

f ^ g is D -valued ;

proof end;

registration

let f be FinSequence of REAL ;

let n be Nat;

coherence

(f | n) /^ n is empty ;

coherence

f /^ (max ((len f),n)) is empty

end;
let n be Nat;

coherence

(f | n) /^ n is empty ;

coherence

f /^ (max ((len f),n)) is empty

proof end;

registration

let D be set ;

ex b_{1} being FinSequence of D st b_{1} is empty

for b_{1} being FinSequence of D st b_{1} is empty holds

b_{1} is nonnegative-yielding
;

end;
cluster Relation-like omega -defined D -valued empty Function-like V32() FinSequence-like FinSubsequence-like for of ;

existence ex b

proof end;

coherence for b

b

registration

for b_{1} being FinSequence st b_{1} is nonnegative-yielding & b_{1} is INT -valued holds

b_{1} is NAT -valued

for b_{1} being FinSequence of INT st b_{1} is nonnegative-yielding holds

b_{1} is NAT -valued
;

end;

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

coherence for b

b

proof end;

coherence for b

b

registration

let f be COMPLEX -valued FinSequence;

reducibility

f + 0 = f

f - 0 = f

end;
reducibility

f + 0 = f

proof end;

reducibility f - 0 = f

proof end;

registration
end;

::stolen from EUCLID_7:def 2

registration

let f be FinSequence;

let h be Permutation of (dom f);

coherence

f * h is FinSequence-like

f * h is dom f -defined ;

end;
let h be Permutation of (dom f);

coherence

f * h is FinSequence-like

proof end;

coherence f * h is dom f -defined ;

theorem :: NEWTON04:12

for i, j being Nat

for D being non empty set

for r being b_{3} -valued FinSequence st len r = i + j holds

ex p, q being b_{3} -valued FinSequence st

( len p = i & len q = j & r = p ^ q )

for D being non empty set

for r being b

ex p, q being b

( len p = i & len q = j & r = p ^ q )

proof end;

theorem FXX: :: NEWTON04:14

for f being COMPLEX -valued FinSequence

for x1, x2 being Complex holds (f + x1) + x2 = f + (x1 + x2)

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;

reducibility

(f + x) - x = f

(f - x) + x = f

end;
let x be Complex;

reducibility

(f + x) - x = f

proof end;

reducibility (f - x) + x = f

proof end;

registration

let x, y be Real;

reducibility

max ((min (x,y)),(max (x,y))) = max (x,y)

min ((min (x,y)),(max (x,y))) = min (x,y)

end;
reducibility

max ((min (x,y)),(max (x,y))) = max (x,y)

proof end;

reducibility min ((min (x,y)),(max (x,y))) = min (x,y)

proof end;

registration

let x, y be Real;

let z be non negative Real;

reducibility

min ((min (x,y)),(y + z)) = min (x,y)

max ((max (x,y)),(y - z)) = max (x,y)

end;
let z be non negative Real;

reducibility

min ((min (x,y)),(y + z)) = min (x,y)

proof end;

reducibility max ((max (x,y)),(y - z)) = max (x,y)

proof end;

registration
end;

registration

let f be nonnegative-yielding FinSequence of REAL ;

let n be Nat;

coherence

f | n is nonnegative-yielding

f /^ n is nonnegative-yielding

end;
let n be Nat;

coherence

f | n is nonnegative-yielding

proof end;

coherence f /^ n is nonnegative-yielding

proof end;

registration

let f be FinSequence of REAL ;

coherence

f - (min f) is nonnegative-yielding

f - (max f) is nonpositive-yielding

end;
coherence

f - (min f) is nonnegative-yielding

proof end;

coherence f - (max f) is nonpositive-yielding

proof end;

registration
end;

registration

let a be Complex;

let f be complex-valued FinSequence;

coherence

a (#) f is len f -element

end;
let f be complex-valued FinSequence;

coherence

a (#) f is len f -element

proof end;

registration

let a, b be Real;

let n be Nat;

reducibility

len ((a,b) In_Power ((n + 1) - 1)) = n + 1 by NEWTON:def 4;

coherence

(a,b) In_Power n is n + 1 -element

end;
let n be Nat;

reducibility

len ((a,b) In_Power ((n + 1) - 1)) = n + 1 by NEWTON:def 4;

coherence

(a,b) In_Power n is n + 1 -element

proof end;

registration

let n be Nat;

reducibility

len (Newton_Coeff ((n + 1) - 1)) = n + 1 by NEWTON:def 5;

coherence

Newton_Coeff n is nonnegative-yielding

Newton_Coeff n is n + 1 -element

end;
reducibility

len (Newton_Coeff ((n + 1) - 1)) = n + 1 by NEWTON:def 5;

coherence

Newton_Coeff n is nonnegative-yielding

proof end;

coherence Newton_Coeff n is n + 1 -element

proof end;

registration

let n be non zero Nat;

reducibility

(Newton_Coeff n) . 2 = n

(Newton_Coeff n) . n = n

end;
reducibility

(Newton_Coeff n) . 2 = n

proof end;

reducibility (Newton_Coeff n) . n = n

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)

for f being nonnegative-yielding FinSequence of REAL st i >= j holds

Sum (f | i) >= Sum (f | j)

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

len h = 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)

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 )

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 :: NEWTON04:30

for f being complex-valued FinSequence

for x being Complex holds Sum (f - x) = (Sum f) - (x * (len f))

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

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 :: NEWTON04:36

for i being Nat

for f being FinSequence of COMPLEX holds f = ((f | i) ^ ((f /^ i) | 1)) ^ (f /^ (i + 1))

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

for f being FinSequence of COMPLEX holds Sum f = ((Sum (f | i)) + (f . (i + 1))) + (Sum (f /^ (i + 1)))

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

( f . x >= g . x & ex i being Nat st f . (i + 1) > g . (i + 1) ) ) holds

Sum f > Sum g

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)

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

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 ;

coherence

((a,b) In_Power n) /" (Newton_Coeff n) is FinSequence of REAL ;

by NEWTON02:103;

end;
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 ((a,b) In_Power n) /" (Newton_Coeff n);

coherence

((a,b) In_Power n) /" (Newton_Coeff n) is FinSequence of REAL ;

by NEWTON02:103;

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

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

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;

reducibility

len ((a,b) Subnomial ((n + 1) - 1)) = n + 1

(a,b) Subnomial n is n + 1 -element

end;
let n be Nat;

reducibility

len ((a,b) Subnomial ((n + 1) - 1)) = n + 1

proof end;

coherence (a,b) Subnomial n is n + 1 -element

proof end;

:: see NEWTON02 for Nat registration

registration
end;

registration
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

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 be Nat;

let k be non zero Nat;

coherence

l choose (l + k) is zero

(Newton_Coeff l) . ((l + k) + 1) is zero

end;
let k be non zero Nat;

coherence

l choose (l + k) is zero

proof end;

coherence (Newton_Coeff l) . ((l + k) + 1) is zero

proof end;

registration
end;

registration
end;

registration
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;

for b_{1} being FinSequence of REAL holds

( b_{1} = (a,b) Subnomial n iff ( len b_{1} = n + 1 & ( for i, l, m being Nat st i in dom b_{1} & m = i - 1 & l = n - m holds

b_{1} . i = (a |^ l) * (b |^ m) ) ) )

(a,b) Subnomial n is FinSequence of REAL ;

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

for b

( b

b

proof end;

coherence (a,b) Subnomial n is FinSequence of REAL ;

:: deftheorem Def2 defines Subnomial NEWTON04:def 2 :

for a, b being Real

for n being Nat

for b_{4} being FinSequence of REAL holds

( b_{4} = (a,b) Subnomial n iff ( len b_{4} = n + 1 & ( for i, l, m being Nat st i in dom b_{4} & m = i - 1 & l = n - m holds

b_{4} . i = (a |^ l) * (b |^ m) ) ) );

for a, b being Real

for n being Nat

for b

( b

b

registration

let a, b be positive Real;

let k, l be Nat;

coherence

((a,b) Subnomial (k + l)) . (k + 1) is positive

end;
let k, l be Nat;

coherence

((a,b) Subnomial (k + l)) . (k + 1) is positive

proof end;

registration
end;

registration

let k be Nat;

let n be non zero Nat;

coherence

((0,0) In_Power n) . k is zero

((0,0) Subnomial n) . k is zero

end;
let n be non zero Nat;

coherence

((0,0) In_Power n) . k is zero

proof end;

coherence ((0,0) Subnomial n) . k is zero

proof end;

registration

let n be non zero Nat;

coherence

(0,0) In_Power n is empty-yielding

(0,0) Subnomial n is empty-yielding

end;
coherence

(0,0) In_Power n is empty-yielding

proof end;

coherence (0,0) Subnomial n is empty-yielding

proof end;

registration
end;

registration

let n be Nat;

correctness

reducibility

(Newton_Coeff n) . 1 = 1;

(Newton_Coeff n) . (n + 1) = 1

end;
correctness

reducibility

(Newton_Coeff n) . 1 = 1;

proof end;

reducibility (Newton_Coeff n) . (n + 1) = 1

proof 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) )

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))*>

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

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

for n being Nat holds (a |^ (n + 1)) - (b |^ (n + 1)) = (a - b) * (Sum ((a,b) Subnomial n))

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)

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)

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)

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)

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

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)

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

for n, i being Nat st i in dom ((a,a) Subnomial n) holds

((a,a) Subnomial n) . i = a |^ n

proof end;

theorem PRN: :: NEWTON04:63

for n being Nat

for f, g being b_{1} -element complex-valued FinSequence holds Product (f (#) g) = (Product f) * (Product g)

for f, g being b

proof end;

registration

let n be Nat;

let i be non zero Nat;

reducibility

((1,(- 1)) Subnomial ((2 * i) + n)) . (2 * i) = - 1

end;
let i be non zero Nat;

reducibility

((1,(- 1)) Subnomial ((2 * i) + n)) . (2 * i) = - 1

proof end;

registration
end;

registration

let a be Real;

let n be Nat;

coherence

n |-> a is constant

(a,a) Subnomial n is constant

end;
let n be Nat;

coherence

n |-> a is constant

proof end;

coherence (a,a) Subnomial n is constant

proof end;

registration

let a, b be non negative Real;

let n, k be Nat;

coherence

not ((a,b) In_Power n) . k is negative

not ((a,b) Subnomial n) . k is negative

end;
let n, k be Nat;

coherence

not ((a,b) In_Power n) . k is negative

proof end;

coherence not ((a,b) Subnomial n) . k is negative

proof end;

registration
end;

registration

let a, b be non negative Real;

let n be Nat;

coherence

(a,b) Subnomial n is nonnegative-yielding

(a,b) In_Power n is nonnegative-yielding

not Sum ((a,b) Subnomial n) is negative ;

coherence

not Sum ((a,b) In_Power n) is negative ;

end;
let n be Nat;

coherence

(a,b) Subnomial n is nonnegative-yielding

proof end;

coherence (a,b) In_Power n is nonnegative-yielding

proof end;

coherence not Sum ((a,b) Subnomial n) is negative ;

coherence

not Sum ((a,b) In_Power n) is negative ;

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

for a, b being Real holds (a,b) Subnomial n,(b,a) Subnomial n are_fiberwise_equipotent

proof end;

theorem :: NEWTON04:68

theorem :: NEWTON04:69

for n being Nat

for a being non negative Real holds Product ((a,1) Subnomial n) = a |^ ((n + 1) choose 2)

for a being non negative Real holds Product ((a,1) Subnomial n) = a |^ ((n + 1) choose 2)

proof end;

registration
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))

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)

for a, b, c being Real holds Sum (((a + b),c) In_Power n) = Sum ((a,(b + c)) In_Power n)

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

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)

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

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

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

for a, b being non negative Real holds ((a,b) In_Power n) . i >= ((a,b) Subnomial n) . i

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)

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)

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)

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

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

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

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)

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

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

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))*>

for n being Nat holds (a,b) Subnomial (n + 2) = (<*(a |^ (n + 2))*> ^ ((a * b) * ((a,b) Subnomial n))) ^ <*(b |^ (n + 2))*>

proof end;