:: On Subnomials
:: by Rafa{\l} Ziobro
::
:: Received October 18, 2016
:: Copyright (c) 2016-2026 Association of Mizar Users
:: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.
environ
vocabularies FINSEQ_2, ABIAN, INT_1, ARYTM_3, XXREAL_0, CARD_1, ARYTM_1,
COMPLEX1, REAL_1, XCMPLX_0, ORDINAL4, NEWTON, CARD_3, SUBSET_1, TARSKI,
RFINSEQ, REALSET1, PARTFUN1, PARTFUN3, FUNCOP_1, FUNCT_2, NEWTON04,
NUMBERS, NAT_1, FINSEQ_1, RELAT_1, FUNCT_1, XREAL_0, ORDINAL1, VALUED_0,
XBOOLE_0, VALUED_1, FOMODEL0, RFINSEQ2, SQUARE_1, FINSEQ_5, CLASSES1;
notations SQUARE_1, CARD_1, COMPLEX1, FUNCOP_1, FUNCT_2, FINSEQ_2, TARSKI,
XXREAL_0, ABIAN, INT_1, NEWTON, PARTFUN1, RFINSEQ, FINSEQ_5, PARTFUN3,
XBOOLE_0, ORDINAL1, XCMPLX_0, XREAL_0, NUMBERS, RELAT_1, FUNCT_1,
RVSUM_1, FINSEQ_1, SUBSET_1, VALUED_0, VALUED_1, FOMODEL0, RFINSEQ2,
CLASSES1;
constructors SQUARE_1, NAT_D, NEWTON, RFINSEQ, WSIERP_1, RECDEF_1, RELSET_1,
PARTFUN3, CLASSES1, RVSUM_2, SEQ_4, MATRIX_5, FINSEQ_5, ABIAN, REAL_1,
FOMODEL0, RFINSEQ2;
registrations ORDINAL1, XXREAL_0, XREAL_0, INT_1, NEWTON, WSIERP_1, NAT_6,
FUNCT_1, CARD_1, RVSUM_1, RELAT_1, INT_6, PARTFUN3, TIETZE_2, FINSEQ_2,
NEWTON02, PREPOWER, RVSUM_3, MEMBERED, COMPLEX1, MATRIX_9, FUNCT_2,
FINSEQ_5, ABIAN, RELSET_1, NUMBERS, NAT_1, FINSEQ_1, XBOOLE_0, XCMPLX_0,
VALUED_0, VALUED_1, FOMODEL0;
requirements REAL, NUMERALS, BOOLE, SUBSET, ARITHM;
definitions RELAT_1, PARTFUN3;
equalities FINSEQ_1, COMPLEX1;
expansions INT_1, FINSEQ_1;
theorems RVSUM_3, CARD_1, XCMPLX_0, NUMBERS, RVSUM_2, NUMPOLY1,
INT_2, NAT_1, ABSVALUE, INT_1, PREPOWER, NEWTON, XCMPLX_1, XREAL_1,
XXREAL_0, WSIERP_1, XREAL_0, COMPLEX1, FINSEQ_1, TARSKI, RFINSEQ,
FINSEQ_2, RVSUM_1, FINSEQ_3, FINSEQ_5, ORDINAL1, PARTFUN1, NEWTON02,
PARTFUN3, COMPLSP2, FUNCT_1, VALUED_1, XBOOLE_1, INTEGRA5,
RFINSEQ2, FINSEQ_6, FINSEQ_7, RFUNCT_1, RELAT_1, TAYLOR_2, INT_4,
FUNCOP_1, FUNCT_2, SQUARE_1, NAT_4, VALUED_2;
begin
reserve a,b,i,j,k,l,m,n for Nat;
registration
let a be positive Real, n be Nat;
cluster a|^n -> positive;
coherence by PREPOWER:6;
end;
registration
let a be non negative Real, n be Nat;
cluster a|^n -> non negative;
coherence
proof
a=0 or a>0;
hence thesis;
end;
end;
registration
let a be non negative Real;
reduce sqrt(a|^2) to a;
reducibility
proof
a|^2 = a^2 by NEWTON:81;
hence thesis by SQUARE_1:22;
end;
end;
registration
cluster real for Complex;
correctness by COMPLEX1:def 1;
cluster non real for Complex;
correctness
proof
not <i> is real by COMPLEX1:18;
hence thesis;
end;
end;
registration
let a be non real Complex;
cluster Im a -> non zero;
coherence
proof
a <> Re a + 0*<i>;
hence thesis by COMPLEX1:13;
end;
end;
registration
let a be Real;
reduce Re a to a;
reducibility by COMPLEX1:def 1;
end;
theorem
for a be non zero Real, a1 be Complex st a*a1 is Real holds a1 is Real
proof
let a be non zero Real, a1 be Complex;
Im(a1*a) = Re a1 * Im a + Re a * Im a1 by COMPLEX1:9
.= Re a1 * 0 + a * Im a1;
hence thesis;
end;
registration
let a be object;
reduce 1*len <*a*> to 1;
reducibility by FINSEQ_1:40;
end;
registration
let a be object, f be FinSequence;
reduce (<*a*>^f).1 to a;
reducibility by FINSEQ_1:41;
reduce (f^<*a*>).(1+len f) to a;
reducibility by FINSEQ_1:42;
end;
registration
let x be Complex;
reduce Sum <*x*> to x;
reducibility by RVSUM_2:30;
end;
registration
let f,g be FinSequence;
reduce (f^g)|(dom f) to f;
reducibility by FINSEQ_1:21;
reduce (f^g)|(len f) to f;
reducibility
proof
(f^g)|(dom f) = (f^g)|(Seg len f) by FINSEQ_1:def 3;
hence thesis;
end;
end;
theorem Th0:
for f be FinSequence holds ex D be non empty set st f is FinSequence of D
proof
let f be FinSequence;
f is FinSequence of rng f \/ {1} by XBOOLE_1:7,FINSEQ_1:def 4;
hence thesis;
end;
registration :: f|(dom f) -- RELAT_1
let f be FinSequence;
reduce f.0 to 0;
reducibility
proof
not 0 in dom f by FINSEQ_3:24;
hence thesis by FUNCT_1:def 2;
end;
reduce f|(len f) to f;
reducibility
proof
f = f^{};
hence thesis;
end;
cluster f/^(len f) -> empty;
coherence by RFINSEQ:27;
end;
registration
let n be Nat;
reduce card (Seg n) to n;
reducibility by FINSEQ_1:57;
reduce card (Segm n) to n;
reducibility by ORDINAL1:def 17;
end;
registration
let n be Nat;
reduce len (id Seg n) to n;
reducibility
proof ::FINSEQ_2:28 etc.
n in NAT & dom (id Seg n) = Seg n by ORDINAL1:def 12;
hence len (id Seg n) = n by FINSEQ_1:def 3;
end;
reduce len idseq n to n;
reducibility
proof
len idseq n = len id Seg n by FINSEQ_2:def 1;
hence thesis;
end;
end;
registration
let m,n be Nat;
reduce (idseq(m+n)).m to m;
reducibility
proof
per cases;
suppose m = 0;
hence thesis;
end;
suppose m > 0; then
m+n >= m+0 & m >= 1 by NAT_1:14,XREAL_1:6; then
m in Seg (m+n);
hence thesis by FINSEQ_2:49;
end;
end;
reduce Rev (idseq(m+(n+1))).(m+1) to n+1;
reducibility
proof
set l = m+1,k = m+n+1;
A0: m+n+1 = len (idseq (m+n+1)) &
len (idseq (m+n+1)) = len (Rev (idseq (m+n+1))) by FINSEQ_5:def 3;
1 <= m+1 & (m+1) <= (m+1)+n by NAT_1:11;then
l in dom Rev(idseq k) by A0,FINSEQ_3:25; then
Rev (idseq k).l = (idseq k).(k-l+1) by A0,FINSEQ_5:def 3
.= (idseq(m+(n+1))).(n+1);
hence thesis;
end;
end;
definition
let a,b be Nat;
redefine func min(a,b) -> Nat; :: redefines min (XXREAL_0, definition)
coherence by XXREAL_0:def 9;
redefine func max(a,b) -> Nat; :: redefines max (XXREAL_0, definition)
coherence by XXREAL_0:def 10;
end;
registration
let f be FinSequence, n be Nat;
reduce f|((len f)+n) to f;
reducibility by FINSEQ_1:58,NAT_1:12;
reduce f|(Seg (max((len f),n))) to f;
reducibility
proof
set l=max((len f),n)-len f;
f|(Seg ((len f) + l)) = f|((len f)+l);
hence thesis;
end;
cluster f/^((len f)+n) -> empty;
coherence
proof
0 + len f <= n + len f by XREAL_1:6;
hence thesis by FINSEQ_5:32;
end;
cluster (f/^(len f)).n -> zero;
coherence;
end;
theorem
for n be Nat, D be set, f be D-valued FinSequence st
n in dom f holds len(f|n) = n
proof
let n be Nat, D be set, f be D-valued FinSequence;
assume n in dom f; then
n <= len f by FINSEQ_3:25;
hence thesis by FINSEQ_1:59;
end;
theorem
for n be Nat, D be set, f be D-valued FinSequence st
n >= len f holds len(f|n) = len f
proof
let n be Nat, D be set, f be D-valued FinSequence;
assume n >= len f; then
reconsider k = n - len f as Element of NAT by NAT_1:21;
len (f|n) = len (f|(len f + k));
hence thesis;
end;
registration
let f be FinSequence, n be non zero Nat;
cluster f.((len f)+n) -> zero;
coherence
proof
len f + n > len f + 0 by XREAL_1:6; then
not (len f)+n in dom f by FINSEQ_3:25;
hence thesis by FUNCT_1:def 2;
end;
end;
registration
let f be real-valued FinSequence, i,j be Nat;
reduce ((f|i)|(i+j)) to f|i;
reducibility
proof
len (f|i) = min(len f, i) by FINSEQ_2:21; then
i+j >= len (f|i) by XXREAL_0:17,NAT_1:12; then
reconsider k = i+j - len (f|i) as Element of NAT by NAT_1:21;
((f|i)|(i+j)) = ((f|i)|(len(f|i)+k));
hence thesis;
end;
end;
registration
let a be Nat;
reduce Sum (a |-> 0) to 0;
reducibility by RVSUM_1:81;
cluster Sum (a|->0) -> zero;
coherence;
end;
registration
let a be Nat, b be object;
reduce len (a |-> b) to a;
reducibility by CARD_1:def 7;
end;
registration
let a be non zero Nat, b be object;
cluster (a |-> b) -> non empty;
coherence;
cluster (a |-> b) -> constant;
coherence
proof
Seg a --> b is constant;
hence thesis by FINSEQ_2:def 2;
end;
reduce the_value_of (a |-> b) to b;
reducibility
proof
reconsider b as set by TARSKI:1;
the_value_of (Seg a --> b) = b by FUNCOP_1:79;
hence thesis by FINSEQ_2:def 2;
end;
end;
registration
let f be constant FinSequence;
reduce Rev f to f;
reducibility
proof
A1: dom Rev f = dom f by FINSEQ_5:57;
for i be object st i in dom f holds
(Rev f).i = f.i
proof
let i be object such that
B1: i in dom f;
B2: i in dom Rev f by B1,FINSEQ_5:57;
reconsider i as Nat by B1;
set n = len f;
B3: n >= i >= 1 by B1,FINSEQ_3:25; then
reconsider k = n - i as Element of NAT by NAT_1:21;
k+i >= k+1 & 1 + k >= 1 + 0 by B3,XREAL_1:6; then
k+1 in dom f by FINSEQ_3:25; then
f.(k+1) = f.i by B1,FUNCT_1:def 10;
hence thesis by B2,FINSEQ_5:def 3;
end;
hence thesis by A1,FUNCT_1:2;
end;
end;
registration
let a be Nat,b be non zero Nat, x be object;
reduce ((a+b)|-> x).b to x;
reducibility
proof
a+b >= 0+b by XREAL_1:6; then
b >= 1 & b <= (a+b) by NAT_1:14; then
b in Seg (a+b);
hence thesis by FINSEQ_2:57;
end;
cluster (a |-> x).(a+b) -> zero;
coherence
proof
a+b > a+0 by XREAL_1:6; then
a+b > len (a |-> x);
hence thesis;
end;
end;
registration
let a be object, n be Nat;
reduce Rev (n|-> a) to n|-> a;
reducibility
proof
n = 0 or n > 0; then
(n|->a) is empty or (n|->a) is constant;
hence thesis;
end;
end;
registration
let n be Nat;
reduce n choose (0*1) to 1;
reducibility by NEWTON:19;
reduce n choose (n*1) to 1;
reducibility by NEWTON:21;
end;
registration
let f be nonnegative-yielding real-valued FinSequence, i be Nat;
cluster f.i -> non negative;
coherence
proof
per cases;
suppose i in dom f; then
f.i in rng f by FUNCT_1:def 3;
hence thesis by PARTFUN3:def 4;
end;
suppose
not i in dom f;
hence thesis by FUNCT_1:def 2;
end;
end;
end;
registration :: see TIETZE_2
cluster empty -> nonpositive-yielding for FinSequence;
coherence
proof
let f be FinSequence;
assume f is empty; then
for r be Real st r in rng f holds r <= 0;
hence thesis by PARTFUN3:def 3;
end;
end;
registration
let f be nonpositive-yielding real-valued FinSequence, i be Nat;
cluster f.i -> non positive;
coherence
proof
per cases;
suppose i in dom f; then
f.i in rng f by FUNCT_1:3;
hence thesis by PARTFUN3:def 3;
end;
suppose
not i in dom f;
hence thesis by FUNCT_1:def 2;
end;
end;
end;
registration
let f be nonnegative-yielding real-valued FinSequence, i,j be Nat;
cluster (f|j).i -> non negative;
coherence
proof
len (f|j) = min (j, len f) by FINSEQ_2:21; then
A0: j >= len (f|j) by XXREAL_0:17;
per cases;
suppose
Q0: j in dom f;
per cases;
suppose
i in dom (f|j); then
len (f|j) >= i >= 1 by FINSEQ_3:25; then
A2: 1 <= i & i <= j by A0,XXREAL_0:2;
reconsider f as FinSequence of REAL by FINSEQ_1:102;
(f|j).i = f.i by Q0,A2,NEWTON02:107;
hence thesis;
end;
suppose
not i in dom (f|j);
hence thesis by FUNCT_1:def 2;
end;
end;
suppose not j in dom f; then
j > len f or j < 1 by FINSEQ_3:25; then
f|j = f or j = 0 by FINSEQ_1:58,NAT_1:14;
hence thesis;
end;
end;
cluster (f/^j).i -> non negative;
coherence
proof
rng (f/^j) c= rng f by FINSEQ_5:33; then
for x be Real holds x in rng (f/^j) implies x >= 0 by PARTFUN3:def 4; then
(f/^j) is nonnegative-yielding by PARTFUN3:def 4;
hence thesis;
end;
end;
registration
let f be empty real-valued FinSequence;
cluster Product f -> non negative;
coherence;
end;
registration
let f be nonnegative-yielding real-valued FinSequence;
cluster Sum f -> non negative;
coherence
proof
for i be Nat st i in dom f holds f.i >= 0;
hence thesis by RVSUM_1:84;
end;
cluster Product f -> non negative;
coherence
proof
reconsider g = f as FinSequence of REAL by FINSEQ_1:102;
per cases;
suppose g is positive-yielding; then
for x be Real st x in rng g holds x > 0 by PARTFUN3:def 1; then
for k be Element of NAT st k in dom g holds g.k > 0 by FUNCT_1:3;
hence thesis by NAT_4:42;
end;
suppose
B1: not g is positive-yielding;
ex i be object st i in dom g & g.i = 0
proof
consider r be Real such that
C1: r in rng g & r <= 0 by B1,PARTFUN3:def 1;
r = 0 by PARTFUN3:def 4,C1;
hence thesis by C1,FUNCT_1:def 3;
end;
hence thesis by RVSUM_1:103;
end;
end;
end;
registration
let f be nonpositive-yielding real-valued FinSequence;
cluster Sum f -> non positive;
coherence
proof
Sum (-f) >= Sum ((len f) |-> 0); then
-(Sum f) + (Sum f) >= 0 + (Sum f) by RVSUM_1:88;
hence thesis;
end;
end;
registration
let a be object,f be nonnegative-yielding real-valued FinSequence;
cluster f.a -> non negative;
coherence
proof
a in dom f or not a in dom f;
hence thesis by FUNCT_1:def 2;
end;
end;
registration
let a be object, f be nonpositive-yielding real-valued FinSequence;
cluster f.a -> non positive;
coherence
proof
a in dom f or not a in dom f;
hence thesis by FUNCT_1:def 2;
end;
end;
registration
let D be set;
let f,g be D-valued FinSequence;
cluster f^g -> D-valued;
correctness;
end;
registration
let f be real-valued FinSequence, n be Nat;
cluster (f|n)/^n -> empty;
coherence
proof
f is FinSequence of REAL by FINSEQ_1:102;
hence thesis;
end;
cluster f/^(max((len f),n)) -> empty;
coherence
proof
(f|(max((len f),n)))/^(max((len f),n)) is empty;
hence thesis;
end;
end;
registration
let D be set;
cluster empty for FinSequence of D;
existence
proof
<*>D = {};
hence thesis;
end;
cluster empty -> nonnegative-yielding for D-valued FinSequence;
coherence;
end;
registration
cluster nonnegative-yielding INT-valued -> NAT-valued for FinSequence;
coherence
proof
let f be FinSequence;
assume
A1: f is nonnegative-yielding INT-valued;
then reconsider f as FinSequence of INT by NEWTON02:103;
reconsider f as FinSequence of REAL by FINSEQ_2:24,NUMBERS:15;
for i be Nat st i in dom f holds f.i in NAT by A1,INT_1:3;
hence thesis by FINSEQ_2:12;
end;
cluster nonnegative-yielding -> NAT-valued for INT-valued FinSequence;
coherence;
end;
registration
let f be complex-valued Function;
reduce f+0 to f;
reducibility
proof
A1: dom (f+0) = dom f & for c be object st c in dom (f+0) holds
(f+0).c = f.c+0 by VALUED_1:def 2;
for c be object st c in dom (f+0) holds (f+0).c = f.c
proof
let c be object such that
B1: c in dom (f+0);
(f+0).c = f.c+0 by VALUED_1:def 2,B1 .= f.c;
hence thesis;
end;
hence thesis by A1,FUNCT_1:2;
end;
reduce f-0 to f;
reducibility
proof
f-0 = -0 + f by VALUED_1:def 3;
hence thesis;
end;
end;
theorem
for f be FinSequence, P be Permutation of (dom f) holds
P is Permutation of (dom (Rev f))
proof
let f be FinSequence, P be Permutation of (dom f);
len f = len (Rev f) by FINSEQ_5:def 3; then
dom f = dom (Rev f) by FINSEQ_3:29;
hence thesis;
end;
theorem MATRIX94:
Rev idseq n is Permutation of (Seg n)
proof
reconsider f = idseq n as one-to-one FinSequence-like Function of
Seg n, Seg n by FINSEQ_2:55;
A1: dom Rev (idseq n) = dom (idseq n) by FINSEQ_5:57
.= dom (id (Seg n)) by FINSEQ_2:def 1
.= Seg n;
A2: rng idseq n = rng (id (Seg n)) by FINSEQ_2:def 1
.= Seg n; then
rng Rev f c= Seg n by FINSEQ_5:57; then
reconsider
g = Rev f as FinSequence-like Function of Seg n, Seg n by A1,FUNCT_2:2;
rng f = rng Rev f by FINSEQ_5:57; then
g is onto by A2,FUNCT_2:def 3;
hence thesis;
end;
theorem
for f be FinSequence holds
idseq (len f) is Permutation of (dom f)
proof
let f be FinSequence;
Seg (len f) = dom f by FINSEQ_1:def 3;
hence thesis by FINSEQ_2:55;
end;
theorem RFP:
for f be FinSequence holds
Rev (idseq (len f)) is Permutation of dom (Rev f)
proof
let f be FinSequence;
dom (Rev f) = dom f by FINSEQ_5:57
.= Seg(len f) by FINSEQ_1:def 3;
hence thesis by MATRIX94;
end;
::stolen from EUCLID_7:def 2
theorem DR:
for f be Function, h be Permutation of dom f holds
dom (f*h) = dom f
proof
let f be Function, h be Permutation of dom f;
dom (f*h) = h"(dom f) by RELAT_1:147
.= h"(rng h) by FUNCT_2:def 3
.= dom h by RELAT_1:134
.= dom f by FUNCT_2:52;
hence thesis;
end;
registration
let f be FinSequence, h be Permutation of (dom f);
cluster f*h -> FinSequence-like;
coherence
proof
dom (f*h) = dom f by DR
.= Seg len f by FINSEQ_1:def 3;
hence thesis;
end;
cluster f*h -> dom f-defined;
coherence;
end;
theorem REV:
for f be FinSequence holds f = (Rev f)*(Rev (idseq len f))
proof
let f be FinSequence;
reconsider P = (Rev (idseq (len f))) as Permutation of dom (Rev f) by RFP;
reconsider g = (Rev f)*P as FinSequence;
A1: dom f = dom (Rev f) by FINSEQ_5:57
.= dom ((Rev f)*P) by DR;
for x be object st x in dom f holds f.x = g.x
proof
set n=len f;
let x be object such that
B1: x in dom f;
reconsider x as Nat by B1;
B2: 1 <= x <= n by B1,FINSEQ_3:25; then
reconsider m = x-1 as Nat;
reconsider k = n - x as Element of NAT by B2,NAT_1:21;
set l = k+1;
1+0 <= l <= k+x by B2,XREAL_1:6; then
l in dom f by FINSEQ_3:25; then
B3: l in dom Rev f by FINSEQ_5:57;
g.x = (Rev f).(Rev (idseq (m+l)).(m+1)) by A1,B1,FUNCT_1:12
.= f.(n-l+1) by B3,FINSEQ_5:def 3
.= f.x;
hence thesis;
end;
hence thesis by A1,FUNCT_1:2;
end;
theorem FFE:
for f be FinSequence holds f,(Rev f) are_fiberwise_equipotent
proof
let f be FinSequence;
A1: f = (Rev f)*(Rev (idseq len f)) by REV;
(Rev (idseq len f)) is Permutation of dom (Rev f) by RFP;
hence thesis by A1, RFINSEQ:4;
end;
theorem
for D be non empty set, r be D-valued FinSequence st len r = i+j
ex p,q be D-valued FinSequence st len p = i & len q = j & r = p^q
proof
let D be non empty set, r be D-valued FinSequence such that
A1: len r = i+j;
reconsider r1 = r as FinSequence of D by NEWTON02:103;
ex p1,q1 be FinSequence of D st
len p1 = i & len q1 = j & r1 = p1^q1 by A1,FINSEQ_2:23;
hence thesis;
end;
theorem
for f be nonnegative-yielding real-valued FinSequence holds
Sum f >= Sum (f|j)
proof
let f be nonnegative-yielding real-valued FinSequence;
A1: (f|j)^(f/^j) = f by RFINSEQ:8;
for i be Nat st i in dom (f/^j) holds (f/^j).i >= 0;
then Sum (f|j) + Sum (f/^j) >= Sum (f|j) + 0 by RVSUM_1:84,XREAL_1:6;
hence thesis by A1,RVSUM_1:75;
end;
theorem FXX:
for f be complex-valued Function, x1,x2 be Complex holds
f+x1+x2 = f+(x1+x2)
proof
let f be complex-valued Function, x1,x2 be Complex;
reconsider X = dom f as set;
A1: dom (f+x1+x2) = dom (f+x1) &
for c be object st c in dom (f+x1+x2) holds
(f+x1+x2).c = (f+x1).c+x2 by VALUED_1:def 2;
A2: dom (f+x1) = dom f & for c be object st c in dom (f+x1) holds
(f+x1).c = f.c+x1 by VALUED_1:def 2;
A3: dom (f+(x1+x2)) = dom f & for c be object st c in dom (f+(x1+x2))
holds (f+(x1+x2)).c = f.c + (x1+x2) by VALUED_1:def 2;
for c be object st c in X holds (f+x1+x2).c = (f+(x1+x2)).c
proof
let c be object such that
B1: c in X;
(f+x1+x2).c = (f+x1).c+x2 by A1,A2,B1
.= (f.c + x1)+ x2 by A2,B1
.= f.c + (x1+x2)
.= (f+(x1+x2)).c by A3,B1;
hence thesis;
end;
hence thesis by A1,A2,A3,FUNCT_1:2;
end;
registration
let f be complex-valued Function, x be Complex;
reduce f+x-x to f;
reducibility
proof
f+x-x = f+x+-x by VALUED_1:def 3
.= f+(x+-x) by FXX
.= f + 0;
hence thesis;
end;
reduce f-x+x to f;
reducibility
proof
f-x+x = f+(-x)+x by VALUED_1:def 3
.= f+(-x+x) by FXX
.= f + 0;
hence thesis;
end;
end;
registration
let x,y be Real;
reduce max (min(x,y),max(x,y)) to max(x,y);
reducibility
proof
max(x,y) >= x >= min(x,y) by XXREAL_0:17,25;
hence thesis by XXREAL_0:def 10,XXREAL_0:2;
end;
reduce min (min(x,y),max(x,y)) to min(x,y);
reducibility
proof
max(x,y) >= x >= min(x,y) by XXREAL_0:17,25;
hence thesis by XXREAL_0:def 9,XXREAL_0:2;
end;
end;
registration
let x,y be Real, z be non negative Real;
reduce min (min(x,y),y+z) to min (x,y);
reducibility
proof
y+z >= y+0 by XREAL_1:6; then
min (y,y+z) = y by XXREAL_0:def 9;
hence thesis by XXREAL_0:33;
end;
reduce max (max(x,y),y-z) to max (x,y);
reducibility
proof
y-z <= y-0 by XREAL_1:10; then
max (y-z,y) = y by XXREAL_0:def 10;
hence thesis by XXREAL_0:34;
end;
end;
registration
let f be FinSequence, i,j be Nat;
reduce ((f|i)|(i+j)) to f|i;
reducibility
proof
len (f|i) = min (len f, i) by FINSEQ_2:21; then
i+j >= len (f|i) by XXREAL_0:17,NAT_1:12;then
reconsider k = i+j - len (f|i) as Element of NAT by NAT_1:21;
((f|i)|(i+j)) = ((f|i)|(len(f|i)+k));
hence thesis;
end;
end;
registration
let f be nonnegative-yielding real-valued FinSequence, n be Nat;
cluster f|n -> nonnegative-yielding;
coherence
proof
let r be Real;
assume r in rng (f|n); then
ex i be object st i in dom (f|n) & (f|n).i = r by FUNCT_1:def 3;
hence thesis;
end;
cluster f/^n -> nonnegative-yielding;
coherence
proof
let r be Real;
assume r in rng (f/^n); then
ex i be object st i in dom (f/^n) & (f/^n).i = r by FUNCT_1:def 3;
hence thesis;
end;
end;
registration
let f be real-valued FinSequence;
cluster f - (min f) -> nonnegative-yielding;
coherence
proof
for r be Real st r in rng (f - (min f)) holds r >= 0
proof
let r be Real such that
A1: r in rng (f-(min f));
consider x be object such that
A2: x in dom (f - (min f)) & r = (f - (min f)).x by A1,FUNCT_1:def 3;
A3: dom (f - (min f)) = dom f & for i be object st i in dom f holds
(f-(min f)).i = f.i - min f by VALUED_1:3;
reconsider x as Nat by A2;
1 <= x <= len f by A2,A3,FINSEQ_3:25; then
f.x - (min f) >= (min f) - (min f) by XREAL_1:9,RFINSEQ2:2;
hence thesis by A2,A3;
end;
hence thesis by PARTFUN3:def 4;
end;
cluster f - (max f) -> nonpositive-yielding;
coherence
proof
for r be Real st r in rng (f - (max f)) holds r <= 0
proof
let r be Real such that
A1: r in rng (f-(max f));
consider x be object such that
A2: x in dom (f - (max f)) & r = (f - (max f)).x by A1,FUNCT_1:def 3;
A3: dom (f - (max f)) = dom f & for i be object st i in dom f holds
(f-(max f)).i = f.i - max f by VALUED_1:3;
reconsider x as Nat by A2;
1 <= x <= len f by A2,A3,FINSEQ_3:25; then
f.x - (max f) <= (max f) - (max f) by XREAL_1:9,RFINSEQ2:1;
hence thesis by A2,A3;
end;
hence thesis by PARTFUN3:def 3;
end;
end;
registration
let f be FinSequence;
cluster Rev f -> (len f)-element;
coherence
proof
len (Rev f) = len f by FINSEQ_5:def 3; then
(Rev f) null f is (len f)-element;
hence thesis;
end;
end;
registration
let D be non empty set;
let f be D-valued FinSequence;
cluster Rev f -> D-valued;
coherence;
end;
registration
let a be Complex, f be complex-valued FinSequence;
cluster a(#)f -> (len f)-element;
coherence
proof
dom (a(#)f) = dom f by VALUED_1:def 5; then
len (a(#)f) = len f by FINSEQ_3:29; then
(a(#)f) null f is (len f)-element;
hence thesis;
end;
end;
registration
let a,b be Real, n be Nat;
reduce len ((a,b) In_Power (n+1-1)) to n+1;
reducibility by NEWTON:def 4;
cluster (a,b) In_Power n -> (n+1)-element;
coherence
proof
(a,b) In_Power (n+1-1) null n is (n+1)-element;
hence thesis;
end;
end;
registration
let n be Nat;
reduce len (Newton_Coeff (n+1-1)) to n+1;
reducibility by NEWTON:def 5;
cluster Newton_Coeff n -> nonnegative-yielding;
coherence
proof
for r be Real st r in rng (Newton_Coeff n) holds r >= 0;
hence thesis by PARTFUN3:def 4;
end;
cluster Newton_Coeff n -> (n+1)-element;
coherence
proof
Newton_Coeff (n+1-1) null n is (n+1)-element;
hence thesis;
end;
end;
registration
let n be non zero Nat;
reduce (Newton_Coeff n).2 to n;
reducibility
proof
n+1 >= 1+1 & 1+1 >= 1+0 by XREAL_1:6,NAT_1:14; then
len (Newton_Coeff n) >= 1+1 >= 1 by NEWTON:def 5; then
2 in dom (Newton_Coeff n) by FINSEQ_3:25; then
(Newton_Coeff n).2 = n choose (2-1) by NEWTON:def 5;
hence thesis by NEWTON:23,NAT_1:14;
end;
reduce (Newton_Coeff n).n to n;
reducibility
proof
n+1 >= n+0 & n >= 1 by NAT_1:14,XREAL_1:6; then
len (Newton_Coeff n) >= n >= 1 by NEWTON:def 5; then
n in dom (Newton_Coeff n) by FINSEQ_3:25; then
(Newton_Coeff n).n = n choose (n-1) by NEWTON:def 5;
hence thesis by NEWTON:24,NAT_1:14;
end;
end;
theorem F123:
for f1,f2,f3 be complex-valued Function holds
(f1 (#) f2) (#) f3 = f1 (#) (f2 (#) f3)
proof
let f1,f2,f3 be complex-valued Function;
A1: dom ((f1 (#) f2) (#) f3) = dom (f1 (#) f2) /\ dom f3 by VALUED_1:def 4
.= dom f1 /\ dom f2 /\ dom f3 by VALUED_1:def 4;
A2: dom (f1 (#) (f2 (#) f3)) = dom f1 /\ dom (f2 (#) f3) by VALUED_1:def 4
.= dom f1 /\ (dom f2 /\ dom f3) by VALUED_1:def 4; then
A3: dom ((f1 (#) f2) (#) f3) = dom (f1 (#) (f2 (#) f3)) by A1,XBOOLE_1:16;
for x be object st x in dom ((f1 (#) f2) (#) f3) holds
((f1 (#) f2) (#) f3).x = (f1 (#) (f2 (#) f3)).x
proof
let x be object such that
B1: x in dom ((f1 (#) f2) (#) f3);
x in dom (f1 (#) (f2 (#) f3)) by B1,A1,A2,XBOOLE_1:16; then
B2a: x in (dom (f1 (#) f2) /\ dom f3) &
x in (dom f1 /\ dom (f2 (#) f3)) by VALUED_1:def 4, B1;
B3: ((f1 (#) f2) (#) f3).x = (f1 (#) f2).x * f3.x by VALUED_1:def 4,B1
.= (f1.x * f2.x) * f3.x by B2a,VALUED_1:def 4;
(f1 (#) (f2 (#) f3)).x = f1.x * (f2 (#) f3).x by A3,B1,VALUED_1:def 4
.= f1.x * (f2.x * f3.x) by B2a,VALUED_1:def 4;
hence thesis by B3;
end;
hence thesis by A1,A2,XBOOLE_1:16,FUNCT_1:2;
end;
theorem
for f,g be complex-valued Function, i be object holds (f(#)g).i = f.i*g.i
by VALUED_1:5;
theorem
for x,y be Real holds max(x,y) - min(x,y)= |.x-y.|
proof
let x,y be Real;
per cases;
suppose
x >= y; then
min (x,y)= y & max(x,y) = x by XXREAL_0:def 9, def 10;
hence thesis by ABSVALUE:def 1;
end;
suppose
A1: x < y; then
A2: min (x,y) = x & max (x,y) = y by XXREAL_0:def 9, def 10;
x - y < x - x by A1,XREAL_1:10; then
|.x-y.| = -(x-y) by ABSVALUE:def 1;
hence thesis by A2;
end;
end;
theorem
for x,y be Real holds min(x,y)*max(x,y) = x*y &
min(x,y) + max(x,y) = x+y
proof
let x,y be Real;
per cases;
suppose x >= y; then
min (x,y)= y & max(x,y) = x by XXREAL_0:def 9, def 10;
hence thesis;
end;
suppose x < y; then
min (x,y) = x & max (x,y) = y by XXREAL_0:def 9, def 10;
hence thesis;
end;
end;
theorem SF:
for f be nonnegative-yielding real-valued FinSequence holds
Sum f >= Sum (f|j)
proof
let f be nonnegative-yielding real-valued FinSequence;
A1: (f|j)^(f/^j) = f by RFINSEQ:8;
Sum (f|j) + Sum (f/^j) >= Sum (f|j) + 0 by XREAL_1:6;
hence thesis by A1,RVSUM_1:75;
end;
theorem :: POLYNOM3:18:
for f be nonnegative-yielding real-valued FinSequence holds
i >= j implies Sum (f|i) >= Sum (f|j)
proof
let f be nonnegative-yielding real-valued FinSequence;
assume i >= j; then
Sum (f|i|j) = Sum (f|j) by FINSEQ_1:82;
hence thesis by SF;
end;
theorem SN:
for f be nonnegative-yielding real-valued FinSequence holds Sum f >= f.n :: POLYNOM5:4
proof
let f be nonnegative-yielding real-valued FinSequence;
per cases;
suppose not n in dom f;
hence thesis by FUNCT_1:def 2;
end;
suppose
n in dom f; then
A0a: len f >= n >= 1 by FINSEQ_3:25; then
reconsider k = n - 1 as Nat;
k+1 > k+0 by XREAL_1:6; then
len f > k by A0a,XXREAL_0:2; then
A1: f|(k+1) = f|k^ <*f.(k+1)*> by FINSEQ_5:83;
A2: Sum f = Sum (((f|k)^<*f.(k+1)*>)^(f/^n)) by A1,RFINSEQ:8
.= Sum ((f|k)^<*f.(k+1)*>) + Sum (f/^n) by RVSUM_1:75
.= Sum(f|k) + f.(k+1) + Sum (f/^n) by RVSUM_1:74;
f.(k+1) + (Sum(f|k) + Sum (f/^n)) >= f.(k+1) + 0 by XREAL_1:6;
hence thesis by A2;
end;
end;
theorem DLS:
for f,g,h be complex-valued FinSequence st dom h = dom f /\ dom g holds
len h = min (len f,len g)
proof
let f,g,h be complex-valued FinSequence such that
A1: dom h = dom f /\ dom g;
per cases;
suppose
B1: len f >= len g; then
dom f /\ dom g = dom g by FINSEQ_3:30,XBOOLE_1:28; then
len h = len g by A1,FINSEQ_3:29;
hence thesis by B1,XXREAL_0:def 9;
end;
suppose
B1: len f < len g; then
dom f /\ dom g = dom f by FINSEQ_3:30,XBOOLE_1:28; then
len h = len f by A1,FINSEQ_3:29;
hence thesis by B1,XXREAL_0:def 9;
end;
end;
theorem FLS:
for f,g be complex-valued FinSequence holds len (f + g) = min (len f,len g)
proof
let f,g be complex-valued FinSequence;
reconsider h = f+g as FinSequence of COMPLEX by NEWTON02:103;
dom h = dom f /\ dom g by VALUED_1:def 1;
hence thesis by DLS;
end;
theorem
for f,g be complex-valued FinSequence holds len (f (#) g) = min (len f,len g)
proof
let f,g be complex-valued FinSequence;
reconsider h = f(#)g as FinSequence of COMPLEX by NEWTON02:103;
dom h = dom f /\ dom g by VALUED_1:def 4;
hence thesis by DLS;
end;
theorem
for f,g be complex-valued FinSequence holds len (f - g) = min (len f, len g)
proof
let f,g be complex-valued FinSequence;
reconsider h = -g as FinSequence of COMPLEX by NEWTON02:103;
h = (-1)(#)g by VALUED_1:def 6; then
dom h = dom g by VALUED_1:def 5; then
A1: len h = len g by FINSEQ_3:29;
f-g = f+h by VALUED_1:def 9;
hence thesis by FLS,A1;
end;
theorem FS:
for f,g be nonnegative-yielding real-valued FinSequence holds
(f(#)g).n <= (Sum f)*g.n
proof
let f,g being nonnegative-yielding real-valued FinSequence;
per cases;
suppose n in dom (f(#)g); then
(f(#)g).n = f.n * g.n by VALUED_1:def 4;
hence thesis by SN,XREAL_1:64;
end;
suppose
not n in dom (f(#)g);
hence thesis by FUNCT_1:def 2;
end;
end;
theorem
for r be Real, n be non zero Nat
ex f be FinSequence of REAL st len f = n & Sum f = r
proof
let r be Real, n be non zero Nat;
reconsider k = n-1 as Nat;
0 in REAL by XREAL_0:def 1; then
reconsider g = k|-> 0 as FinSequence of REAL by FINSEQ_2:63;
reconsider h = g^<*r*> as FinSequence of REAL by RVSUM_1:145;
A1: len (g^<*r*>) = (len g)+1 by FINSEQ_2:16
.= k + 1;
Sum (g^<*r*>) = Sum(k|-> 0) + r by RVSUM_1:74
.= 0 + r; then
Sum h = r & len h = k+1 by A1;
hence thesis;
end;
LmFG: for f,g be real-valued FinSequence st (for x be Nat holds f.x >= g.x)
holds Sum (f|min(len f,len g)) >= Sum (g|min(len f,len g))
proof
let f,g be real-valued FinSequence such that
A0: for x be Nat holds f.x >= g.x;
reconsider f,g as FinSequence of REAL by FINSEQ_1:102;
set i = min(len f,len g);
set h=f|i,j=g|i;
per cases;
suppose
f is empty or g is empty; then
min (len f, len g) = 0 by XXREAL_0:def 9;
hence thesis;
end;
suppose f is non empty & g is non empty; then
len f >= 1 & len g >= 1 by FINSEQ_1:20; then
min(len f,len g) >= 1 by XXREAL_0:def 9; then
A3: i in dom f & i in dom g by XXREAL_0:17,FINSEQ_3:25; then
A4: len h = i & len j = i by NEWTON02:110;
for k be Element of NAT st k in dom j holds j.k <= h.k
proof
let k be Element of NAT;
assume k in dom j;
then i >= k >= 1 by A4,FINSEQ_3:25;
then (f|i).k = f.k & (g|i).k = g.k by A3,NEWTON02:107;
hence thesis by A0;
end;
hence thesis by A4,INTEGRA5:3;
end;
end;
theorem SL:
for f be complex-valued FinSequence, x be Complex holds
f + x = f + ((len f) |-> x)
proof
let f be complex-valued FinSequence, x be Complex;
reconsider g = ((len f) |-> x) as FinSequence of COMPLEX by NEWTON02:103;
A0: dom (f+x) = dom f by VALUED_1:def 2;
A2: len (f+g) = min (len f, len ((len f)|-> x)) by FLS
.= len f;
for i be Nat st i in dom (f+x) holds (f+x).i = (f+g).i
proof
let i be Nat such that
B1: i in dom (f+x);
B2: i in dom f by B1,VALUED_1:def 2;
reconsider i as non zero Nat by B1,FINSEQ_3:25;
len f >= i by B2,FINSEQ_3:25; then
reconsider k = len f - i as Element of NAT by NAT_1:21;
i in dom (f+g) by A2,B2,FINSEQ_3:29; then
(f+g).i = f.i + ((k+i)|-> x).i by VALUED_1:def 1
.= f.i + x;
hence thesis by B1,VALUED_1:def 2;
end;
hence thesis by A0,FINSEQ_3:29,A2,FINSEQ_2:9;
end;
theorem SFX:
for f be complex-valued FinSequence, x be Complex holds
Sum (f+x) = Sum f + x*(len f)
proof
let f be complex-valued FinSequence, x be Complex;
reconsider x as Element of COMPLEX by XCMPLX_0:def 2;
set k=len f, g = ((len f)|->x);
(f null {}) is k-element; then
reconsider f as k-element complex-valued FinSequence;
reconsider h = f+x as FinSequence of COMPLEX by RVSUM_1:146;
dom f = dom (f+x) by VALUED_1:def 2; then
len f = len (f+x) by FINSEQ_3:29; then
h null {} is k-element; then
reconsider h as k-element FinSequence of COMPLEX;
Sum (f+x) = Sum (f + g) by SL
.= Sum f + Sum ((len f) |-> x) by RVSUM_2:40
.= Sum f + (len f)*x by RVSUM_2:36;
hence thesis;
end;
theorem
for f be complex-valued FinSequence, x be Complex holds
Sum (f-x) = Sum f - x*(len f)
proof
let f be complex-valued FinSequence, x be Complex;
reconsider f as FinSequence of COMPLEX by RVSUM_1:146;
Sum (f+-x) = Sum f + (-x)*(len f) by SFX;
hence thesis by VALUED_1:def 3;
end;
theorem
for f be real-valued FinSequence,
g be nonnegative-yielding real-valued FinSequence st
(for x be Nat holds f.x >= g.x) holds f is nonnegative-yielding
proof
let f be real-valued FinSequence,
g be nonnegative-yielding real-valued FinSequence
such that
A1: for x be Nat holds f.x >= g.x;
for r be Real st r in rng f holds r >= 0
proof
let r be Real such that
B0: r in rng f;
consider k be object such that
B1: k in dom f & r = f.k by B0,FUNCT_1:def 3;
reconsider k as Nat by B1;
g.k >= 0;
hence thesis by B1,A1;
end;
hence thesis by PARTFUN3:def 4;
end;
theorem NYS:
for f,g be real-valued FinSequence st (for x be Nat holds f.x >= g.x) holds
Sum f >= Sum g
proof
let f,g be real-valued FinSequence such that
A0: for x be Nat holds f.x >= g.x;
reconsider f,g as FinSequence of REAL by FINSEQ_1:102;
per cases;
suppose
len f <= len g; then
len f = min(len f,len g) by XXREAL_0:def 9; then
B1: Sum (f|(len f)) >= Sum (g|(len f)) by A0,LmFG;
for r be Real st r in rng (g/^(len f)) holds r <= 0
proof
let r be Real such that
C1: r in rng (g/^(len f));
consider k being object such that
C2: k in dom (g/^(len f)) & r = (g/^(len f)).k by C1,FUNCT_1:def 3;
reconsider k as non zero Nat by C2,FINSEQ_3:25;
C4: (len f)+k in dom g by C2,FINSEQ_5:26;
r = (g/^(len f))/.k by C2,PARTFUN1:def 6
.= g/.((len f)+k) by C2,FINSEQ_5:27
.= g.((len f)+k) by PARTFUN1:def 6,C4; then
r <= f.((len f) + k) by A0;
hence thesis;
end; then
reconsider h = g/^(len f) as nonpositive-yielding FinSequence of REAL
by PARTFUN3:def 3;
C5: Sum g = Sum ((g|(len f))^(g/^(len f))) by RFINSEQ:8
.= Sum (g|(len f)) + Sum (g/^(len f)) by RVSUM_1:75;
Sum h <= 0; then
Sum (g|(len f)) + 0 >= Sum (g|(len f)) + Sum(g/^(len f)) by XREAL_1:6;
hence thesis by B1,C5,XXREAL_0:2;
end;
suppose
len f > len g; then
len g = min(len f,len g) by XXREAL_0:def 9; then
B1: Sum (f|(len g)) >= Sum (g|(len g)) by A0,LmFG;
for r be Real st r in rng (f/^(len g)) holds r >= 0
proof
let r be Real such that
C1: r in rng (f/^(len g));
consider k being object such that
C2: k in dom (f/^(len g)) & r = (f/^(len g)).k by C1,FUNCT_1:def 3;
reconsider k as non zero Nat by C2,FINSEQ_3:25;
C4: (len g)+k in dom f by C2,FINSEQ_5:26;
r = (f/^(len g))/.k by C2,PARTFUN1:def 6
.= f/.((len g)+k) by C2,FINSEQ_5:27
.= f.((len g)+k) by PARTFUN1:def 6,C4; then
r >= g.((len g) + k) by A0;
hence thesis;
end; then
reconsider h = f/^(len g) as nonnegative-yielding FinSequence of REAL
by PARTFUN3:def 4;
C5: Sum f = Sum ((f|(len g))^(f/^(len g))) by RFINSEQ:8
.= Sum (f|(len g)) + Sum (f/^(len g)) by RVSUM_1:75;
Sum h >= 0; then
Sum (f|(len g)) + 0 <= Sum (f|(len g)) + Sum(f/^(len g)) by XREAL_1:6;
hence thesis by B1,C5,XXREAL_0:2;
end;
end;
theorem S1:
for f be complex-valued FinSequence holds Sum (f|(1 qua Nat)) = f.(1 qua Nat)
proof
let f be complex-valued FinSequence;
per cases;
suppose not f is empty; then
f | 1 = <*f.1*> by FINSEQ_5:20;
hence thesis;
end;
suppose
B1: f is empty; then
Sum (f| 1) = 0
.= f.1 by B1;
hence thesis;
end;
end;
theorem S2:
for f be complex-valued FinSequence, n be Nat holds Sum ((f/^n)| 1) = f.(n+1)
proof
let f be complex-valued FinSequence, n be Nat;
per cases;
suppose
A1: 1 in dom (f/^n);
A0: f is FinSequence of COMPLEX by FINSEQ_1:107;
thus Sum ((f/^n)| 1) = (f/^n).1 by S1
.= f.(n+1) by A1,A0,FINSEQ_7:4;
end;
suppose
not 1 in dom (f/^n); then
A1: f/^n is empty by FINSEQ_5:6; then
0 = len (f/^n)
.= (len f) -'n by RFINSEQ:29; then
len f = n or 0 + n >= ((len f)-n) +n by XREAL_0:def 2,XREAL_1:6; then
len f + 0 < n + 1 by XREAL_1:8; then
A2: not (n+1) in dom f by FINSEQ_3:25;
thus Sum ((f/^n)| 1) = 0 by A1
.= f.(n+1) by A2,FUNCT_1:def 2;
end;
end;
theorem FINSEQ681:
for f be FinSequence, a,b be Nat holds (f/^a)/^b = f/^(a+b)
proof
let f be FinSequence, a,b be Nat;
ex D be non empty set st
f is FinSequence of D by Th0;
hence thesis by FINSEQ_6:81;
end;
theorem ::POLYNOM4:1
for f be complex-valued FinSequence holds
f = (f|i)^((f/^i)|(1 qua Nat))^(f/^(i+1))
proof
let f be complex-valued FinSequence;
f = (f|i)^(f/^i) by RFINSEQ:8
.= (f|i)^(((f/^i)| 1)^((f/^i)/^1)) by RFINSEQ:8
.= (f|i)^((f/^i)| 1)^((f/^i)/^1) by FINSEQ_1:32
.= (f|i)^((f/^i)| 1)^(f/^(i+1)) by FINSEQ681;
hence thesis;
end;
theorem SUM:
for f be complex-valued FinSequence holds
Sum f = Sum (f|i) + f.(i+1) + Sum (f/^(i+1))
proof
let f be complex-valued FinSequence;
set f1 = f|i, f2 = f/^i, k = 1,f4 = f2/^k;
Sum f = Sum (f1^f2) by RFINSEQ:8
.= Sum (f|i) + Sum f2 by RVSUM_2:32
.= Sum (f|i) + Sum ((f2|k)^(f2/^k)) by RFINSEQ:8
.= Sum (f|i) + (Sum (f2|k) + Sum (f2/^k)) by RVSUM_2:32
.= Sum (f|i) + (Sum (f2|k) + Sum (f/^(i+k))) by FINSEQ681
.= Sum (f|i) + Sum (f2|k) + Sum (f/^(i+k));
hence thesis by S2;
end;
theorem FINSEQ74:
for f be FinSequence, i be non zero Nat holds f.(n+i) = (f/^n).i
proof
let f be FinSequence, i be non zero Nat;
consider D be non empty set such that
A0: f is FinSequence of D by Th0;
reconsider f as FinSequence of D by A0;
per cases;
suppose
B1: not i in dom (f/^n);
B2: (f/^n).i = 0 by B1,FUNCT_1:def 2;
n+i > len f
proof
i >= 1 by NAT_1:14; then
i > len (f/^n) by B1, FINSEQ_3:25; then
C1: i > len f -' n by RFINSEQ:29;
per cases;
suppose
D1: len f < n;
n+i >= n+0 by XREAL_1:6;
hence thesis by D1,XXREAL_0:2;
end;
suppose
len f >= n; then
len f - n >= n - n by XREAL_1:9; then
len f -' n = len f - n by XREAL_0:def 2; then
i+n > (len f - n)+n by C1,XREAL_1:6;
hence thesis;
end;
end; then
not n+i in dom f by FINSEQ_3:25;
hence thesis by B2,FUNCT_1:def 2;
end;
suppose
i in dom (f/^n);
hence thesis by FINSEQ_7:4;
end;
end;
theorem NYS1:
for f,g be real-valued FinSequence st
(for x be Nat holds f.x >= g.x & ex i st f.(i+1) > g.(i+1)) holds
Sum f > Sum g
proof
let f,g be real-valued FinSequence such that
A1: for x be Nat holds f.x >= g.x & ex i be Nat st f.(i+1) > g.(i+1);
consider i be Nat such that
A2: f.(i+1) > g.(i+1) by A1;
A5: Sum f = Sum (f|i) + f.(i+1) + Sum (f/^(i+1)) by SUM;
A6: Sum g = Sum (g|i) + g.(i+1) + Sum (g/^(i+1)) by SUM;
for x be Nat holds (f|i).x >= (g|i).x & (f/^(i+1)).x >= (g/^(i+1)).x
proof
let x be Nat;
B0: i >= x implies (f|i).x = f.x & (g|i).x = g.x by FINSEQ_3:112;
len (f|i) <= i & len (g|i) <= i by FINSEQ_5:17; then
i < x implies len (f|i) < x & len (g|i) < x by XXREAL_0:2; then
i < x implies not x in dom (f|i) & not x in dom (g|i)
by FINSEQ_3:25; then
B2: i < x implies (f|i).x = 0 & 0 = (g|i).x by FUNCT_1:def 2;
x <> 0 implies (f.((i+1)+x) = (f/^(i+1)).x &
g.((i+1)+x) = (g/^(i+1)).x) by FINSEQ74;
hence thesis by A1,B0,B2;
end; then
Sum (f|i) >= Sum (g|i) & Sum(f/^(i+1)) >= Sum (g/^(i+1)) by NYS; then
Sum (f|i) + Sum (f/^(i+1)) >= Sum (g|i) + Sum (g/^(i+1))
by XREAL_1:7; then
A7: Sum (f|i) + Sum (f/^(i+1)) + f.(i+1) >=
Sum (g|i) + Sum (g/^(i+1))+f.(i+1) by XREAL_1:6;
Sum (g|i) + Sum (g/^(i+1))+ f.(i+1) >
Sum (g|i) + Sum (g/^(i+1))+ g.(i+1) by A2,XREAL_1:6;
hence thesis by A5,A6,A7,XXREAL_0:2;
end;
theorem
for f,g being nonnegative-yielding real-valued FinSequence holds
(Sum f)*(Sum g) >= Sum(f(#)g)
proof
let f,g being nonnegative-yielding real-valued FinSequence;
now let i be Nat;
(Sum f)*g.i = ((Sum f)(#)g).i by VALUED_1:6;
hence (f(#)g).i <= ((Sum f)*g).i by FS;
end; then
Sum (f(#)g) <= Sum((Sum f)*g) by NYS;
hence thesis by RVSUM_1:87;
end;
theorem
for a be Complex, f be complex-valued FinSequence holds
((len f)|->a)(#)f = a(#)f
proof
let a be Complex, f be complex-valued FinSequence;
len ((len f)|->a) = len f; then
dom ((len f)|->a) = dom f by FINSEQ_3:29; then
A1: (dom ((len f)|->a)) /\ (dom f) = dom (a(#)f) by VALUED_1:def 5; then
A2: dom (((len f)|->a)(#)f) = dom (a(#)f) by VALUED_1:def 4;
for x be object st x in dom (((len f)|->a)(#)f) holds
(((len f)|->a)(#)f).x = (a(#)f).x
proof let x be object such that
B1: x in dom (((len f)|-> a)(#)f);
reconsider x as non zero Nat by B1,FINSEQ_3:25;
len ((len f)|->a) >= x >= 1 by A1,A2,B1,FINSEQ_3:25; then
ex k be Nat st len f = x+k by NAT_1:10; then
reconsider k = len f - x as Nat;
(((len f)|->a)(#)f).x = ((x+k)|-> a).x*(f.x) by B1,VALUED_1:def 4
.= (a(#)f).x by A2,B1,VALUED_1:def 5;
hence thesis;
end;
hence thesis by A2,FUNCT_1:2;
end;
theorem AMP:
for a,b be Complex holds
a(#)<*b*> = <*a*b*>
proof
let a,b be Complex;
A1: dom <*(a*b)*> = Seg 1 & dom <*b*> = Seg 1 by FINSEQ_1:def 8;
for x be object st x in Seg 1 holds <*a*b*>.x = a*<*b*>.x
proof
let x be object;
assume x in Seg 1;
then x = 1 by FINSEQ_1:2,TARSKI:def 1;
hence thesis;
end;
hence thesis by A1,VALUED_1:def 5;
end;
theorem ADP:
for a be Complex, f,g be complex-valued FinSequence holds
a(#)(f^g) = (a(#)f)^(a(#)g)
proof
let a be Complex, f,g be complex-valued FinSequence;
A0: dom (a(#)(f^g)) = dom (f^g) & dom (a(#)f) = dom f &
dom (a(#)g) = dom g by VALUED_1:def 5; then
A1: len (a(#)(f^g)) = len (f^g) & len (a(#)f) = len f &
len (a(#)g) = len g by FINSEQ_3:29; then
len (a(#)(f^g)) = len (a(#)f) + len (a(#)g) by FINSEQ_1:22
.= len ((a(#)f)^(a(#)g)) by FINSEQ_1:22; then
A2: dom (a(#)(f^g)) = dom ((a(#)f)^(a(#)g)) by FINSEQ_3:29;
for x be object st x in dom (a(#)(f^g)) holds
(a(#)(f^g)).x = ((a(#)f)^(a(#)g)).x
proof
let x be object such that
B1: x in dom (a(#)(f^g));
per cases;
suppose
C1: x in dom f; then
C2: x in dom (a(#)f) by VALUED_1:def 5; then
((a(#)f)^(a(#)g)).x = (a(#)f).x by FINSEQ_1:def 7
.= a*f.x by C2,VALUED_1:def 5
.= a*(f^g).x by C1,FINSEQ_1:def 7
.= (a(#)(f^g)).x by B1,VALUED_1:def 5;
hence thesis;
end;
suppose
C0: not x in dom f;
x in (dom (f^g)) by VALUED_1:def 5,B1; then
consider n be Nat such that
C2: n in dom g & x = len f + n by C0,FINSEQ_1:25;
((a(#)f)^(a(#)g)).((len f)+n) = (a(#)g).n by A0,A1,C2,FINSEQ_1:def 7
.= a*g.n by A0,C2,VALUED_1:def 5
.= a*(f^g).(len f + n) by C2,FINSEQ_1:def 7
.= (a(#)(f^g)).x by C2,B1,VALUED_1:def 5;
hence thesis by C2;
end;
end;
hence thesis by A2,FUNCT_1:2;
end;
theorem CREV:
for a be Complex, f,g be complex-valued FinSequence
st g = Rev f holds Rev (a(#)f) = a(#)g
proof
let a be Complex, f,g be complex-valued FinSequence such that
A1: g = Rev f;
set h = (a(#)f),h1 = a(#)g,h2=Rev h;
A2: dom h1 = dom g & dom h = dom f by VALUED_1:def 5;
A4: dom Rev (h) = dom h & dom (Rev f) = dom f by FINSEQ_5:57; then
A5: len h1 = len h2 & len h2 = len f & len f = len h &
len g = len f by A1,A2,FINSEQ_3:29;
reconsider h1 as (len f)-element complex-valued FinSequence by A5;
for x be object st x in dom h1 holds h1.x = h2.x
proof
let x be object such that
B1: x in dom h1;
reconsider x as Nat by B1;
B3: 1 <= x <= len f by B1,A1,A2,A4,FINSEQ_3:25; then
reconsider k = (len f)-x as Element of NAT by NAT_1:21;
set l=k+1;
B4: 0+1 <= k+1 & k+1 <= k+x by B3,XREAL_1:6;
(Rev h).x = h.((len h)-x+1) by B1,A1,A2,A4,FINSEQ_5:def 3
.= (a(#)f).l by A2,FINSEQ_3:29
.= a*(Rev (Rev f)).l by A2,B4,FINSEQ_3:25,VALUED_1:def 5
.= a*(g.((len g)-l+1)) by A1,A4,B4,FINSEQ_3:25,FINSEQ_5:def 3
.= a*(g.x) by A5;
hence thesis by B1,VALUED_1:def 5;
end;
hence thesis by A1,A2,A4,FUNCT_1:2;
end;
:: Dwumian > Niedomian :)
definition :: see Newton:def 4,def 5
let a,b be Real;
let n be natural Number;
func (a,b) Subnomial n -> FinSequence of REAL equals
((a,b) In_Power n) /" (Newton_Coeff n);
correctness by NEWTON02:103;
end;
theorem DOMN:
for a,b be Real, n be Nat holds
len ((a,b) In_Power n) = len (Newton_Coeff n) &
len ((a,b) Subnomial n) = len (Newton_Coeff n) &
len ((a,b) In_Power n) = len ((a,b) Subnomial n) &
dom ((a,b) In_Power n) = dom (Newton_Coeff n) &
dom ((a,b) Subnomial n) = dom (Newton_Coeff n) &
dom ((a,b) In_Power n) = dom ((a,b) Subnomial n)
proof
let a,b be Real, n be Nat;
len (a,b) In_Power (n+1-1) = len (Newton_Coeff n); then
A2: dom ((a,b) In_Power n) = dom (Newton_Coeff n) by FINSEQ_3:29;
dom (((a,b) In_Power n) /" (Newton_Coeff n)) =
dom ((a,b) In_Power n) /\ dom (Newton_Coeff n) by VALUED_1:16;
hence thesis by A2,FINSEQ_3:29;
end;
registration
let a,b be Real, n be Nat;
reduce len ((a,b) Subnomial (n+1-1)) to n+1;
reducibility
proof
len ((a,b) Subnomial (n+1-1)) = len (Newton_Coeff (n+1-1)) by DOMN;
hence thesis;
end;
cluster (a,b) Subnomial n -> (n+1)-element;
coherence
proof
(a,b) Subnomial (n+1-1) null n is (n+1)-element;
hence thesis;
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
proof
per cases;
suppose
A0: m in dom ((a,b) In_Power n); then
consider k such that
A1: m = 1+k by NAT_1:10,FINSEQ_3:25;
len ((a,b) In_Power n) = n+1 by NEWTON:def 4; then
n >= k by A0,FINSEQ_3:25,A1,XREAL_1:6; then
consider l such that
A2: n = k+l by NAT_1:10;
k = m - 1 & l = n - k by A1,A2; then
((a,b) In_Power n).m = (n choose k)*a|^l*b|^k by A0,NEWTON:def 4;
hence thesis;
end;
suppose
not m in dom ((a,b) In_Power n);
hence thesis by FUNCT_1:def 2;
end;
end;
end;
registration
let a,b be Integer;
let n be Nat;
cluster (a,b) In_Power n -> INT-valued;
coherence
proof
for k st k in dom (a,b) In_Power n holds
((a,b) In_Power n).k in INT by INT_1:def 2;
hence thesis by FINSEQ_2:12;
end;
end;
theorem NIS:
for a,b be Integer, k be Nat st k in dom (Newton_Coeff n) holds
(Newton_Coeff n).k divides ((a,b) In_Power n).k
proof
let a,b be Integer, k be Nat such that
A0: k in dom (Newton_Coeff n);
A0a: k >= 1 by A0,FINSEQ_3:25; then
reconsider m = k - 1 as Nat;
A1: n+1 = len ((a,b) In_Power n) by NEWTON:def 4;
len (Newton_Coeff n) = n+1 by NEWTON:def 5; then
A1a: n+1 >= m+1 by A0,FINSEQ_3:25; then
consider l such that
A2: n = m + l by XREAL_1:6,NAT_1:10;
A3: (Newton_Coeff n).k = (n choose m) by A0,NEWTON:def 5;
A4: k in dom ((a,b) In_Power n) by A0a,A1,A1a,FINSEQ_3:25;
l = n - m by A2; then
((a,b) In_Power n).k = (n choose m)*a|^l*b|^m by A4,NEWTON:def 4
.= (Newton_Coeff n).k*(a|^l*b|^m) by A3;
hence thesis;
end;
registration
let l,k be Nat;
cluster (l+k) choose k -> positive;
coherence
proof
reconsider n = l+k as Nat;
l = n-k & n >= k by NAT_1:11; then
n choose k = (n!)/((k!)*(l!)) by NEWTON:def 3;
hence thesis;
end;
end;
registration
let l be Nat, k be non zero Nat;
cluster l choose (l+k) -> zero;
coherence
proof
l+0 < l+k by XREAL_1:6;
hence thesis by NEWTON:def 3;
end;
cluster (Newton_Coeff l).(l+k+1) -> zero;
coherence
proof
len (Newton_Coeff l) = l+1 & (l+1)+0 < (l+1)+k by XREAL_1:6,NEWTON:def 5;
hence thesis;
end;
end;
registration
let l be Nat, k be Nat;
cluster (Newton_Coeff (l+k)).(k+1) -> positive;
coherence
proof
(k+1)+l >= (k+1)+0 & k+1 >= 0 + 1 by XREAL_1:6; then
len (Newton_Coeff (l+k)) >= k+1 & k+1 >= 1 by NEWTON:def 5; then
k+1 in dom (Newton_Coeff (l+k)) by FINSEQ_3:25; then
(Newton_Coeff (l+k)).(k+1) = (l+k) choose (k+1-1) by NEWTON:def 5;
hence thesis;
end;
end;
theorem D1:
for k,l be Nat holds
k in dom (Newton_Coeff l) implies (Newton_Coeff l).k is non zero
proof
let k,l be Nat;
assume
k in dom (Newton_Coeff l); then
A1: len (Newton_Coeff l) = l+1 &
len (Newton_Coeff l) >= k & k >= 1 by FINSEQ_3:25,NEWTON:def 5; then
reconsider i = k-1 as Nat;
consider m be Nat such that
A2: (l+1) = k + m by A1,NAT_1:10;
(Newton_Coeff (m+i)).(i+1) is non zero;
hence thesis by A2;
end;
registration
let a,b be Integer;
let m,n be Nat;
cluster ((a,b) Subnomial n).m -> integer;
coherence
proof
per cases;
suppose
A0: m in dom (Newton_Coeff n); then
(Newton_Coeff n).m divides ((a,b) In_Power n).m by NIS; then
consider x be Integer such that
A2: ((a,b) In_Power n).m = ((Newton_Coeff n).m)*x;
(Newton_Coeff n).m <> 0 by A0,D1; then
x = ((a,b) In_Power n).m /(Newton_Coeff n).m by A2,XCMPLX_1:89;
hence thesis by VALUED_1:17;
end;
suppose
not m in dom (Newton_Coeff n); then
(Newton_Coeff n).m = 0 by FUNCT_1:def 2; then
0 = ((a,b) In_Power n).m /(Newton_Coeff n).m by XCMPLX_1:49;
hence thesis by VALUED_1:17;
end;
end;
end;
registration
let a,b be Integer;
let n be Nat;
cluster (a,b) Subnomial n -> INT-valued;
coherence
proof
for k st k in dom (a,b) Subnomial n holds
((a,b) Subnomial n).k in INT by INT_1:def 2;
hence thesis by FINSEQ_2:12;
end;
end;
LmS1: for a,b be Real, n be Nat holds
for 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
let a,b be Real, n be Nat;
let i,l,m be Nat such that
A1: i in dom (a,b) Subnomial n & m = i - 1 & l = n-m;
dom (Newton_Coeff n) = dom ((a,b) Subnomial n) &
dom (Newton_Coeff n) = dom ((a,b) In_Power n) by DOMN; then
A2: ((a,b) In_Power n).i = ((n choose m)* a|^l * b|^m) &
(Newton_Coeff n).i = (n choose m) by A1,NEWTON:def 4,NEWTON:def 5;
((a,b) Subnomial n).i = (((m+l) choose m)* (a|^l * b|^m))/((m+l) choose m)
by A1,A2,VALUED_1:17
.= (a|^l * b|^m) by XCMPLX_1:89;
hence thesis;
end;
definition
let a,b be Real, n be Nat;
redefine func (a,b) Subnomial n -> FinSequence of REAL means :Def2: :: redefines Subnomial (NEWTON04, definition)
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
proof
let f be FinSequence of REAL;
L1: len ((a,b) Subnomial n) = len ((a,b) Subnomial (n+1-1))
.= n+1;
L2: len f = len ((a,b) Subnomial n) iff dom f = dom ((a,b) Subnomial n)
by FINSEQ_3:29;
(len f = len (a,b) Subnomial n &
for i,l,m be Nat st i in dom ((a,b) Subnomial n) & m = i-1 & l = n-m
holds
f.i = a|^l*b|^m) implies f = ((a,b) Subnomial n)
proof
assume
A3: (len f = len (a,b) Subnomial n &
for i,l,m be Nat st i in dom ((a,b) Subnomial n) & m = i-1 & l = n-m
holds f.i = a|^l*b|^m);
A4: (dom f = dom (a,b) Subnomial n &
for i,l,m be Nat st i in dom ((a,b) Subnomial n) & m = i-1 & l = n-m
holds f.i = a|^l*b|^m) by A3,FINSEQ_3:29;
for i be Nat st i in dom ((a,b) Subnomial n)
holds f.i = ((a,b) Subnomial n).i
proof
let i be Nat such that
B2: i in dom ((a,b) Subnomial n);
reconsider m = i-1 as Nat by B2,FINSEQ_3:26;
len ((a,b) Subnomial (n+1-1)) = n+1; then
(n+1)-(m+1) is Element of NAT by FINSEQ_3:26,B2; then
reconsider l = n-m as Nat;
f.i = a|^l*b|^m by A3,B2;
hence thesis by LmS1,B2;
end;
hence thesis by A4,FINSEQ_1:13;
end;
hence thesis by L1,L2,LmS1;
end;
coherence;
end;
registration
let a,b be positive Real, k,l be Nat;
cluster ((a,b)Subnomial (k+l)).(k+1) -> positive;
coherence
proof
1+0 <= 1+k & (k+1)+0 <= (k+1)+l by XREAL_1:6; then
1 <= k+1 <= len((a,b) Subnomial (k+l+1-1)); then
k = (k+1) - 1 & l = (k+l) - k &
(k+1) in dom ((a,b) Subnomial (k+l)) by FINSEQ_3:25; then
((a,b)Subnomial (k+l)).(k+1) = a|^l * b|^k by Def2;
hence thesis;
end;
end;
registration
let a,b be positive Real, n be Nat;
cluster Sum((a,b)Subnomial n) -> positive;
coherence
proof
A1: for i be Nat st i in dom ((a,b) Subnomial n) holds
0 <= ((a,b) Subnomial n).i
proof
let i be Nat such that
B1: i in dom ((a,b) Subnomial n);
B2: 1 <= i <= len((a,b) Subnomial (n+1-1)) by B1,FINSEQ_3:25; then
reconsider s = (n+1) - i as Element of NAT by NAT_1:21;
reconsider l = i - 1 as Nat by B2;
((a,b) Subnomial (l+s)).(l+1) > 0;
hence thesis;
end;
len ((a,b) Subnomial (n+1-1)) >= 1 by NAT_1:14; then
1 in dom ((a,b) Subnomial (n+1-1)) & 0 < ((a,b) Subnomial (0+n)).(0+1)
by FINSEQ_3:25;
hence thesis by A1,RVSUM_1:85;
end;
end;
registration
let k be Nat, n be non zero Nat;
cluster ((0,0) In_Power n).k -> zero;
coherence
proof
per cases;
suppose
A1: k in dom (0,0) In_Power n; then
A2: 1 <= k <= len ((0,0) In_Power (n+1-1)) by FINSEQ_3:25; then
reconsider m = k-1 as Nat;
ex l be Nat st (n+1) = (m+1) + l by A2,NAT_1:10; then
reconsider l = n - m as Nat;
m = 0 implies l >= 1 by NAT_1:14; then
A3: m < 1 implies 0|^l = 0 by NAT_1:14,NEWTON:11;
A4: m >= 1 implies 0|^m = 0 by NEWTON:11;
((0,0) In_Power (n+1-1)).k = (n choose m)*0|^(l)*0|^(m)
by A1,NEWTON:def 4;
hence thesis by A3,A4;
end;
suppose not k in dom (0,0) In_Power n;
hence thesis by FUNCT_1:def 2;
end;
end;
cluster ((0,0) Subnomial n).k -> zero;
coherence
proof
((0,0) Subnomial n).k = (((0,0) In_Power n).k) / (Newton_Coeff n).k
by VALUED_1:17;
hence thesis;
end;
end;
registration
let n be non zero Nat;
cluster ((0,0) In_Power n) -> empty-yielding;
coherence
proof
for x be set st x in rng((0,0) In_Power n) holds x = {}
proof
let x be set;
assume x in rng ((0,0) In_Power n);
then ex k be object st
k in dom ((0,0) In_Power n) & ((0,0) In_Power n).k = x
by FUNCT_1:def 3;
hence thesis;
end;
hence thesis by RELAT_1:149;
end;
cluster ((0,0) Subnomial n) -> empty-yielding;
coherence
proof
for x be set st x in rng((0,0) Subnomial n) holds x = {}
proof
let x be set;
assume x in rng ((0,0) Subnomial n);then
ex k be object st k in dom ((0,0) Subnomial n) &
((0,0) Subnomial n).k = x by FUNCT_1:def 3;
hence thesis;
end;
hence thesis by RELAT_1:149;
end;
end;
registration
let f be empty-yielding complex-valued FinSequence;
cluster Sum f -> zero;
coherence
proof
f = len f |-> 0;
hence thesis;
end;
end;
registration
let n be Nat;
reduce (Newton_Coeff n).1 to 1;
correctness
proof
(Newton_Coeff n).1 = ((1,1) In_Power n).1 by NEWTON:31
.= 1|^n by NEWTON:28;
hence thesis;
end;
reduce (Newton_Coeff n).(n+1) to 1;
reducibility
proof
(Newton_Coeff n).(n+1) = ((1,1) In_Power n).(n+1) by NEWTON:31
.= 1|^n by NEWTON:29;
hence thesis;
end;
end;
theorem NS:
for a,b be Real, n be Nat holds
(((a,b) In_Power n).1 = ((a,b) Subnomial n).1) &
(((a,b) In_Power n).(n+1) = ((a,b) Subnomial n).(n+1))
proof
let a,b be Real, n be Nat;
A1: ((a,b) Subnomial n).1 = ((a,b) In_Power n).1/(Newton_Coeff n).1
by VALUED_1:17;
((a,b) Subnomial n).(n+1) = ((a,b) In_Power n).(n+1)/(Newton_Coeff n).(n+1)
by VALUED_1:17;
hence thesis by A1;
end;
theorem RS:
for a,b be Real holds
(a,b) Subnomial (n+1) = (a*((a,b)Subnomial n))^<*b|^(n+1)*>
proof
let a,b be Real;
A0: (a,b)Subnomial n is FinSequence of COMPLEX by RVSUM_1:146;
A0a: len ((a,b) Subnomial n) = len (a*(a,b) Subnomial n) by COMPLSP2:3;
A2: len ((a,b) Subnomial ((n+1)+1-1)) = (n+1) + 1 &
len ((a,b) Subnomial (n+1-1)) = n+1; then
A3: len ((a,b) Subnomial (n+1))
= len ((a,b) Subnomial n) + len <*b|^(n+1)*> by FINSEQ_1:39
.= len (a*((a,b)Subnomial n )) + len <*b|^(n+1)*> by COMPLSP2:3
.= len (a*((a,b)Subnomial n)^<*b|^(n+1)*>) by FINSEQ_1:22;
for k be Nat st 1 <= k <= len ((a,b) Subnomial (n+1)) holds
((a,b) Subnomial (n+1)).k = (a*((a,b)Subnomial n)^<*b|^(n+1)*>).k
proof
let k be Nat such that
B0: 1 <= k <= len ((a,b) Subnomial (n+1));
reconsider m = k-1 as Nat by B0;
per cases;
suppose
C1: k in dom ((a,b) Subnomial n); then
C2: 1 <= k <= len ((a,b) Subnomial n) by FINSEQ_3:25; then
m+1 <= n+1 by Def2; then
reconsider l = n-m as Element of NAT by XREAL_1:6,NAT_1:21;
C3: l+1 = (n+1) - m;
k in dom ((a,b) Subnomial (n+1)) by B0,FINSEQ_3:25; then
((a,b) Subnomial (n+1)).k = a|^(l+1)*b|^m by Def2,C3
.= a*a|^l*b|^m by NEWTON:6
.= a*(a|^l*b|^m)
.= a*((a,b) Subnomial n).k by C1,Def2
.= (a*(a,b) Subnomial n).k by A0,COMPLSP2:16
.= ((a*(a,b) Subnomial n)^<*b|^(n+1)*>).k by A0a,C2,FINSEQ_1:64;
hence thesis;
end;
suppose
not k in dom ((a,b) Subnomial n); then
not k <= n+1 by B0,A2,FINSEQ_3:25; then
k >= (n+1)+1 by INT_1:7; then
C1: k = (n+1)+1 by B0,A2,XXREAL_0:1;
len (a*(a,b) Subnomial n) = n+1 by A2,NEWTON:2; then
((a*(a,b) Subnomial n)^<*b|^(n+1)*>).((n+1)+1)
= ((a,b) In_Power (n+1)).((n+1)+1) by NEWTON:29;
hence thesis by NS,C1;
end;
end;
hence thesis by A3;
end;
theorem LS:
for a,b be Real holds
(a,b) Subnomial (n+1) = <*a|^(n+1)*>^(b*((a,b)Subnomial n))
proof
let a,b be Real;
A2: len ((a,b) Subnomial ((n+1)+1-1)) = (n+1) + 1 &
len ((a,b) Subnomial (n+1-1)) = n+1; then
A3: len ((a,b) Subnomial (n+1))
= len <*a|^(n+1)*> + len ((a,b) Subnomial n) by FINSEQ_1:39
.= len <*a|^(n+1)*> + len (b*((a,b)Subnomial n )) by NEWTON:2
.= len (<*a|^(n+1)*>^(b*((a,b)Subnomial n))) by FINSEQ_1:22;
for k be Nat st 1 <= k <= len ((a,b) Subnomial (n+1)) holds
((a,b) Subnomial (n+1)).k = (<*a|^(n+1)*>^(b*((a,b)Subnomial n))).k
proof
let k be Nat such that
B0: 1 <= k <= len ((a,b) Subnomial (n+1));
per cases by B0,XXREAL_0:1;
suppose
k > 1; then
k >= 1+1 by NAT_1:13; then
reconsider m = k-2 as Element of NAT by NAT_1:21;
C2: n+2 >= m+2 by A2,B0; then
reconsider l = n - m as Element of NAT by XREAL_1:6,NAT_1:21;
C3: l = (n+1) - (m+1);
m <= n by C2,XREAL_1:6; then
C3a: 0+1 <= m+1 <= n+1 by XREAL_1:6; then
C4: m+1 in dom (a,b) Subnomial n by A2,FINSEQ_3:25;
C5: m = (m+1)-1 & l = n - m;
C6: 1 <= m+1 <= len (b*((a,b)Subnomial n)) by C3a,A2,NEWTON:2;
m + 1 = k - 1 & k in dom ((a,b) Subnomial (n+1)) by B0,FINSEQ_3:25; then
((a,b) Subnomial (n+1)).k = a|^l*b|^(m+1) by Def2,C3
.= a|^l*(b*b|^m) by NEWTON:6
.= b*(a|^l*b|^m)
.= b*((a,b) Subnomial n).(m+1) by C4,C5,Def2
.= (b*(a,b) Subnomial n).(m+1) by RVSUM_1:45
.=(<*a|^(n+1)*>^(b*((a,b)Subnomial n))).(len (<*a|^(n+1)*>)+(m+1))
by C6,FINSEQ_1:65
.=(<*a|^(n+1)*>^(b*((a,b)Subnomial n))).((m+1)+1) by FINSEQ_1:39;
hence thesis;
end;
suppose
C1: k = 1;
(<*a|^(n+1)*>^(b*(a,b) Subnomial n)).1
= ((a,b) In_Power (n+1)).1 by NEWTON:28;
hence thesis by NS,C1;
end;
end;
hence thesis by A3;
end;
theorem SumS:
for a,b be Real, n be Nat holds
a|^(n+1) - b|^(n+1) = (a-b)*Sum((a,b)Subnomial n)
proof
let a,b be Real, n be Nat;
A1: Sum ((a,b) Subnomial (n+1)) = Sum ((a*((a,b)Subnomial n))^<*b|^(n+1)*>)
by RS
.= Sum(a*((a,b)Subnomial n)) + b|^(n+1) by RVSUM_2:31
.= a*Sum((a,b) Subnomial n) + b|^(n+1) by RVSUM_2:38;
Sum ((a,b) Subnomial (n+1)) = Sum (<*a|^(n+1)*>^(b*((a,b)Subnomial n))) by LS
.= a|^(n+1) + Sum(b*((a,b)Subnomial n)) by RVSUM_2:33
.= b*Sum((a,b) Subnomial n) + a|^(n+1) by RVSUM_2:38;
hence thesis by A1;
end;
theorem
for a be Real, n be non zero Nat holds
a|^n = Sum ((a,0) Subnomial n)
proof
let a be Real, n be non zero Nat;
per cases;
suppose a is zero;
hence thesis;
end;
suppose A2:a is non zero;
a|^(n+1) - 0|^(n+1) = (a-0)*Sum ((a,0) Subnomial n) by SumS; then
a*a|^n = a*Sum ((a,0) Subnomial n) by NEWTON:6;
hence thesis by A2,XCMPLX_1:5;
end;
end;
theorem
for a be Real, n be Nat holds
a|^(n+1) = Sum((a,1) Subnomial n)*(a-1) + 1
proof
let a be Real, n be Nat;
a|^(n+1) - 1|^(n+1) = (a-1)*Sum ((a,1) Subnomial n) by SumS;
hence thesis;
end;
theorem STT:
for a,b,c,d be Real, n be Nat, x be object st
x in dom ((a*b,c*d) Subnomial n) holds
((a*b,c*d) Subnomial n).x = ((a,d) Subnomial n).x * ((b,c) Subnomial n).x
proof
let a,b,c,d be Real, n be Nat, x be object such that
B1: x in dom ((a*b,c*d) Subnomial n);
len ((a*b,c*d) Subnomial (n+1-1)) = len ((a,d) Subnomial (n+1-1)) &
len ((a*b,c*d) Subnomial (n+1-1)) = len ((b,c) Subnomial (n+1-1)); then
A0: dom ((a*b,c*d) Subnomial n) = dom ((a,d) Subnomial n) &
dom ((a*b,c*d) Subnomial n) = dom ((b,c) Subnomial n) by FINSEQ_3:29;
reconsider x as positive Nat by B1,FINSEQ_3:25;
set m = x-1;
len ((a*b,c*d) Subnomial (n+1-1)) >= x by B1,FINSEQ_3:25; then
consider k be Nat such that
B2: n+1 = x + k by NAT_1:10;
B3: n = m + k & k = n - m by B2; then
((a*b,c*d) Subnomial (m+k)).(m+1) = (a*b)|^k * (c*d)|^m by B1,Def2
.= a|^k * b|^k * (c*d)|^m by NEWTON:7
.= a|^k * b|^k * (c|^m * d|^m) by NEWTON:7
.= (a|^k * d|^m)*(b|^k * c|^m)
.= ((a,d) Subnomial (m+k)).(m+1)*(b|^k * c|^m) by A0,B1,B3,Def2
.= ((a,d) Subnomial (m+k)).(m+1)*((b,c)Subnomial (m+k)).(m+1)
by A0,B1,B3,Def2;
hence thesis by B2;
end;
theorem ST:
for a,b,c,d be Real, n be Nat holds
(a*b,c*d) Subnomial n = ((a,d) Subnomial n) (#) ((b,c) Subnomial n)
proof
let a,b,c,d be Real, n be Nat;
len ((a*b,c*d) Subnomial (n+1-1)) = len ((a,d) Subnomial (n+1-1)) &
len ((a*b,c*d) Subnomial (n+1-1)) = len ((b,c) Subnomial (n+1-1)); then
dom ((a*b,c*d) Subnomial n) = dom ((a,d) Subnomial n) &
dom ((a*b,c*d) Subnomial n) = dom ((b,c) Subnomial n) by FINSEQ_3:29; then
A1: dom ((a*b,c*d) Subnomial n) = dom ((a,d) Subnomial n) /\
dom ((b,c) Subnomial n);
for x be object st x in dom ((a*b,c*d) Subnomial n) holds
((a*b,c*d) Subnomial n).x = ((a,d) Subnomial n).x *
((b,c) Subnomial n).x by STT;
hence thesis by A1,VALUED_1:def 4;
end;
theorem DAB:
for a,b be Real, n be Nat holds
(a,b) Subnomial n = ((a,1) Subnomial n) (#) ((1,b) Subnomial n)
proof
let a,b be Real, n be Nat;
(a*1,b*1) Subnomial n = ((a,1) Subnomial n) (#) ((1,b) Subnomial n) by ST;
hence thesis;
end;
theorem INS:
for a,b be Real, n be Nat holds
(a,b) In_Power n = (Newton_Coeff n) (#) ((a,b) Subnomial n)
proof
let a,b be Real, n be Nat;
A0a: dom ((a,b) In_Power n) = dom (Newton_Coeff n) by DOMN; then
A0: dom ((a,b) In_Power n) =
dom (Newton_Coeff n) /\ dom ((a,b) In_Power n); then
A1: dom ((a,b) In_Power n) = dom ((a,b) Subnomial n) by VALUED_1:16;
for c be object st c in dom ((a,b) In_Power n) holds
((a,b) In_Power n).c = (Newton_Coeff n).c * ((a,b) Subnomial n).c
proof
let c be object such that
B1: c in dom ((a,b) In_Power n);
reconsider c as positive Nat by B1,FINSEQ_3:25;
set m = c-1;
c <= len (Newton_Coeff (n+1-1)) by B1,A0a,FINSEQ_3:25; then
consider k be Nat such that
B2: n+1 = c + k by NAT_1:10;
B3: n = m + k & k = n - m by B2;
(Newton_Coeff (m+k)).(m+1) * ((a,b) Subnomial (m+k)).(m+1)
= ((m+k) choose m)* ((a,b) Subnomial (m+k)).(m+1)
by B2,B1,A0a,NEWTON:def 5
.= ((m+k) choose m)*((a|^k)*(b|^m)) by B1,A1,B3,Def2
.= ((m+k) choose m)*(a|^k)*(b|^m)
.= ((a,b) In_Power (m+k)).(m+1) by NEWTON:def 4,B1,B3;
hence thesis by B2;
end;
hence thesis by A0,A1,VALUED_1:def 4;
end;
theorem
for a,b be Real, n be Nat holds
(a,b) In_Power n = ((a,1) In_Power n) (#) ((1,b) Subnomial n) &
(a,b) In_Power n = ((a,1) Subnomial n) (#) ((1,b) In_Power n)
proof
let a,b be Real, n be Nat;
A1: (a,b) In_Power n = (Newton_Coeff n) (#) ((a,b) Subnomial n) by INS
.= (Newton_Coeff n) (#) (((a,1) Subnomial n) (#) ((1,b) Subnomial n))
by DAB;
(Newton_Coeff n) (#) ((a,1) Subnomial n) = ((a,1) In_Power n) &
(Newton_Coeff n) (#) ((1,b) Subnomial n) = ((1,b) In_Power n) by INS;
hence thesis by A1,F123;
end;
theorem
for a,b,c,d be Real, n be Nat holds
(a*b,c*d) In_Power n =
(Newton_Coeff n) (#) ((a,c) Subnomial n) (#) ((b,d) Subnomial n)
proof
let a,b,c,d be Real, n be Nat;
(a*b,c*d) In_Power n = (Newton_Coeff n) (#) ((a*b,c*d) Subnomial n) by INS
.= (Newton_Coeff n) (#) (((a,c) Subnomial n) (#) ((b,d) Subnomial n))
by ST;
hence thesis by RFUNCT_1:9;
end;
theorem CONST:
for a be Real, n,i be Nat st i in dom ((a,a)Subnomial n) holds
((a,a)Subnomial n).i = a|^n
proof
let a be Real, n,i be Nat such that
A1: i in dom ((a,a)Subnomial n);
A2: 1 <= i <= len ((a,a) Subnomial (n+1-1)) by A1,FINSEQ_3:25; then
reconsider k = i-1 as Nat;
n+1 >= k+1 by A2; then
reconsider l = n-k as Element of NAT by XREAL_1:6,NAT_1:21;
a|^k*a|^l = a|^(k+l) by NEWTON:8;
hence thesis by A1,Def2;
end;
theorem CONST1:
for n be Nat, a be Real holds ((a,a)Subnomial n) = ((n+1)|-> a|^n)
proof
let n be Nat, a be Real;
A1: for j be Nat holds ((a,a)Subnomial n).j = ((n+1)|-> a|^n).j
proof
let j be Nat;
j <> 0 implies ((a,a)Subnomial n).j = ((n+1)|-> a|^n).j
proof
assume j <> 0; then
reconsider i = j-1 as Nat;
per cases;
suppose
ex k be Nat st n = i+k; then
reconsider k = n-i as Nat;
set l = i+1;
0+1 <= i+1 & (i+1)+0 <= (i+1)+k by XREAL_1:6; then
1 <= i+1 <= len ((a,a) Subnomial (n+1-1)); then
i+1 in dom ((a,a)Subnomial (i+k)) by FINSEQ_3:25; then
((a,a)Subnomial (i+k)).(i+1) = a|^n &
((k+(i+1))|-> a|^n).(i+1) = a|^n by CONST;
hence thesis;
end;
suppose
not ex k be Nat st n = i + k; then
i+1 > n+1 by XREAL_1:6,NAT_1:10; then
i+1 > len ((a,a)Subnomial n) & i+1 > len ((n+1)|-> a|^n) = n+1
by Def2; then
not (i+1) in dom ((a,a)Subnomial n) &
not (i+1) in dom ((n+1)|-> a|^n) by FINSEQ_3:25; then
((a,a)Subnomial n).(i+1) = 0 & ((n+1)|-> a|^n).(i+1) = 0
by FUNCT_1:def 2;
hence thesis;
end;
end;
hence thesis;
end;
len ((a,a)Subnomial (n+1-1)) = len ((n+1)|-> a|^n);
hence thesis by A1;
end;
theorem PRA:
for n be Nat, a be Real holds Product((a,a)Subnomial n) = a|^(n*(n+1))
proof
let n be Nat, a be Real;
set f = (n+1) |-> (a|^n),h = the_value_of f,i = len f;
Product((a,a)Subnomial n) = Product f by CONST1
.= h|^ i by RVSUM_3:8
.= a|^(n*(n+1)) by NEWTON:9;
hence thesis;
end;
theorem PRN:
for n be Nat, f,g be n-element complex-valued FinSequence holds
Product (f(#)g)= (Product f) * (Product g) by RVSUM_2:48;
theorem SAB:
for a,b be Real, n be Nat holds
(a,b) Subnomial n = Rev ((b,a) Subnomial n)
proof
let a,b be Real, n be Nat;
A1: dom (a,b) Subnomial n = dom (Newton_Coeff n) & dom (b,a) Subnomial n =
dom (Newton_Coeff n) by DOMN; then
A2: dom ((a,b) Subnomial n) = dom (Rev ((b,a) Subnomial n))
by FINSEQ_5:57;
for i be object st i in dom ((a,b)Subnomial n) holds
((a,b)Subnomial n).i = (Rev((b,a)Subnomial n)).i
proof
let i be object such that
B1: i in dom ((a,b)Subnomial n);
reconsider i as Nat by B1;
reconsider m = i-1 as Nat by B1,FINSEQ_3:26;
len((a,b)Subnomial(n+1-1)) - (m+1) is Element of NAT
by B1,FINSEQ_3:26; then
reconsider l = n-m as Nat;
set k = l+1;
B2: i in dom Rev((b,a) Subnomial (n+1-1)) by A1,FINSEQ_5:57,B1;
k+i = (len((b,a) Subnomial (n+1-1)))+1
.= (len (Rev((b,a) Subnomial (n+1-1))))+1 by FINSEQ_5:def 3; then
B3: k in dom Rev(Rev((b,a) Subnomial (n+1-1))) by B2,FINSEQ_5:59;
B4: l = k-1;
B5: m = n-l;
((a,b)Subnomial n).i = a|^l * b|^m by B1,Def2
.= ((b,a)Subnomial n).(len ((b,a)Subnomial (n+1-1))-i+1)
by B3,B4,B5,Def2
.= Rev((b,a)Subnomial n).i by FINSEQ_5:58,A1,B1;
hence thesis;
end;
hence thesis by A2,FUNCT_1:2;
end;
registration
let n be Nat, i be Nat;
reduce ((1,1)Subnomial (n+i)).(i+1) to 1;
reducibility
proof
A1: 1+0 <= 1+i & (i+1)+0 <= (i+1)+n by XREAL_1:6;
len ((1,1)Subnomial ((n+i)+1-1)) = n+i+1; then
i+1 in dom ((1,1)Subnomial (n + i)) by A1,FINSEQ_3:25; then
((1,1) Subnomial (n+i)).(i+1) = 1|^(n+i) by CONST;
hence thesis;
end;
end;
registration
let n be Nat,i be non zero Nat;
reduce ((1,-1) Subnomial (2*i+n)).(2*i) to -1;
reducibility
proof
A1: len ((1,-1) Subnomial ((2*i+n)+1-1)) = 2*i+n+1;
i+i >= 1+0 & 2*i+(n+1) >= 2*i + 0 by XREAL_1:6,NAT_1:14; then
A2: 2*i in dom ((1,-1) Subnomial (2*i+n)) by A1,FINSEQ_3:25;
reconsider k = 2*i - 1 as odd Nat;
n+1 = (2*i+n) - k; then
((1,-1) Subnomial (n+2*i)).(2*i) = 1|^(n+1) * (-1)|^k by A2,Def2
.= 1*(-1);
hence thesis;
end;
end;
registration
let n be Nat, i be odd Nat;
reduce ((1,-1) Subnomial (n+i)).i to 1;
reducibility
proof
A1: len ((1,-1) Subnomial ((n+i)+1-1)) = n+i+1;
i >= 1 & i+(n+1) >= i + 0 by XREAL_1:6,NAT_1:14; then
A2: i in dom ((1,-1) Subnomial (i+n)) by A1,FINSEQ_3:25;
reconsider k = i - 1 as even Nat;
n+1 = (i+n) - k; then
((1,-1) Subnomial (n+i)).(i) = 1|^(n+1) * (-1)|^k by A2,Def2
.= 1*1;
hence thesis;
end;
end;
registration
let a be Real, n be Nat;
cluster n|->a -> constant;
coherence
proof
for i,j be object st i in dom (n|->a) & j in dom (n|->a) holds
(n|->a).i = (n|->a).j
proof
let i, j be object such that
A1: i in dom (n|->a) & j in dom (n|->a);
reconsider i as Nat by A1;
reconsider j as Nat by A1;
dom(n |-> a) = Seg (len (n|->a)) by FINSEQ_1:def 3; then
(n|->a).i = a & (n|->a).j = a by A1,FINSEQ_2:57;
hence thesis;
end;
hence thesis by FUNCT_1:def 10;
end;
cluster ((a,a)Subnomial n) -> constant;
coherence
proof
((a,a) Subnomial n) = ((n+1)|->a|^n) by CONST1;
hence thesis;
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
proof
per cases;
suppose
A1: k in dom ((a,b) In_Power n); then
k >= 1 by FINSEQ_3:25; then
reconsider l = k - 1 as Nat;
len ((a,b) In_Power n) >= l+1 by FINSEQ_3:25,A1; then
n+1 >= l+1 by NEWTON:def 4; then
reconsider m = n - l as Element of NAT by XREAL_1:6,NAT_1:21;
((a,b) In_Power n).k = (n choose l)*a|^m*b|^l by A1,NEWTON:def 4;
hence thesis;
end;
suppose not k in dom ((a,b) In_Power n);
hence thesis by FUNCT_1:def 2;
end;
end;
cluster ((a,b) Subnomial n).k -> non negative;
coherence
proof
((a,b) Subnomial n).k = ((a,b) In_Power n).k / (Newton_Coeff n).k
by VALUED_1:17;
hence thesis;
end;
end;
theorem SAA:
for a be Real, n be Nat holds
Sum ((a,a)Subnomial n) = (n+1)*a|^n
proof
let a be Real, n be Nat;
A1: n+1 = len ((a,a)Subnomial (n+1-1));
n+1 >= 0+1 by XREAL_1:6; then
A2: n+1 in dom ((a,a)Subnomial n) by A1,FINSEQ_3:25;
n+1 is set & n+1 in dom ((a,a)Subnomial n) &
((a,a) Subnomial n).(n+1) = a|^n by A2,CONST; then
the_value_of ((a,a) Subnomial n) = a|^n by FUNCT_1:def 12;
hence thesis by A1,RVSUM_3:7;
end;
theorem ES:
for a be Real, n be even Nat holds
Sum ((a,-a) Subnomial n) = a|^n
proof
let a be Real, n be even Nat;
per cases;
suppose
A1: a is zero;
per cases;
suppose
B1: n = 0;
Sum ((a,-a)Subnomial n) = (0+1)*a|^n by A1,B1,SAA;
hence thesis;
end;
suppose
B1: n > 0;
(a,-a) Subnomial n = len ((0,0) Subnomial (n+1-1))|-> 0 by B1,A1;
hence thesis by A1,B1,NAT_1:14,NEWTON:11;
end;
end;
suppose
A1: not a is zero;
(a-(-a))*Sum ((a,-a) Subnomial n) = a|^(n+1)-((-1)*a)|^(n+1) by SumS
.= a|^(n+1)-(-1)|^(n+1)*a|^(n+1) by NEWTON:7
.= 2*a|^(n+1)
.= 2*(a*a|^n) by NEWTON:6
.= (2*a)*a|^n;
hence thesis by A1,XCMPLX_1:5;
end;
end;
registration
let n be even Nat;
reduce Sum((1,-1) Subnomial n) to 1;
reducibility
proof
Sum((1,-1) Subnomial n) = 1|^n by ES;
hence thesis;
end;
end;
registration
let a be Real, n be odd Nat;
cluster Sum((a,-a) Subnomial n) -> zero;
coherence
proof
per cases;
suppose a is zero; then
(a,-a) Subnomial n = len ((0,0) Subnomial (n+1-1))|-> 0;
hence thesis;
end;
suppose
not a is zero; then
A1: 2*a <> 0;
(a-(-a))*Sum((a,-a)Subnomial n) = a|^(n+1)-((-1)*a)|^(n+1) by SumS
.= a|^(n+1) - ((-1)|^(n+1)*a|^(n+1)) by NEWTON:7
.= a|^(n+1) - 1*a|^(n+1);
hence thesis by A1;
end;
end;
end;
registration
let n be Nat;
reduce Sum ((1,1)Subnomial (n+1-1)) to n+1;
reducibility
proof
Sum ((1,1)Subnomial n) = (n+1)*1|^n by SAA;
hence thesis;
end;
end;
registration
let n be Nat;
cluster Sum (Newton_Coeff n) -> non zero;
coherence
proof
set f = Newton_Coeff n;
0 in REAL by XREAL_0:def 1; then
reconsider g = (n |-> 0) as FinSequence of REAL by FINSEQ_2:63;
A1: for x be Nat holds f.x >= (n |-> 0).x;
f.(0+1) > g.(0+1); then
Sum f > Sum (n |-> 0) by A1,NYS1;
hence thesis;
end;
end;
registration
let a,b be non negative Real, n be Nat;
cluster (a,b) Subnomial n -> nonnegative-yielding;
coherence
proof
for r be Real st r in rng ((a,b) Subnomial n) holds r >= 0
proof
let r be Real such that
B1: r in rng ((a,b) Subnomial n);
ex k be object st
k in dom((a,b) Subnomial n) & r = ((a,b) Subnomial n).k
by B1,FUNCT_1:def 3;
hence thesis;
end;
hence thesis by PARTFUN3:def 4;
end;
cluster (a,b) In_Power n -> nonnegative-yielding;
coherence
proof
for r be Real st r in rng ((a,b) In_Power n) holds r >= 0
proof
let r be Real such that
B1: r in rng ((a,b) In_Power n);
ex k be object st
k in dom((a,b) In_Power n) & r = ((a,b) In_Power n).k
by B1,FUNCT_1:def 3;
hence thesis;
end;
hence thesis by PARTFUN3:def 4;
end;
cluster Sum ((a,b) Subnomial n) -> non negative;
coherence;
cluster Sum ((a,b) In_Power n) -> non negative;
coherence;
end;
theorem SFE:
for a,b be Real holds
((a,b)Subnomial n), ((b,a) Subnomial n) are_fiberwise_equipotent
proof
let a,b be Real;
((a,b)Subnomial n), Rev((a,b)Subnomial n) are_fiberwise_equipotent by FFE;
hence thesis by SAB;
end;
theorem
for a,b be Real holds
Product (a,b) Subnomial n = Product (b,a) Subnomial n by SFE,RVSUM_3:4;
theorem
for a be non negative Real holds
Product ((a,1) Subnomial n) = a|^((n+1) choose 2)
proof
let a be non negative Real;
set l = a|^(n choose 2),f = ((a,1) Subnomial n),g = ((1,a) Subnomial n);
A1: ((n+1) choose 2)*2 = (n*(n+1))/2*2 by NUMPOLY1:72
.= n*(n+1);
A2: (a|^((n+1) choose 2))|^2 = a|^(((n+1) choose 2)*2) by NEWTON:9
.= Product ((a*1,a*1) Subnomial n) by A1,PRA
.= Product (f(#)g) by ST
.= (Product f)*(Product g) by PRN
.= (Product f)*(Product f)
by SFE,RVSUM_3:4
.= (Product f)|^2 by NEWTON:81;
a|^((n+1) choose 2) = sqrt((Product f)|^2) by A2
.= Product f;
hence thesis;
end;
theorem ES:
(n!)*(k!) <= (n+k)!
proof
set s = (n+k) choose n,l = n+k;
k = l-n & n+k >= n+0 by XREAL_1:6; then
A2: s*((n!)*(k!)) = (n+k)!/((n!)*(k!))*((n!)*(k!)) by NEWTON:def 3
.= (n+k)! by XCMPLX_1:87;
s*((n!)*(k!)) >= 1*((n!)*(k!)) by XREAL_1:64,NAT_1:14;
hence thesis by A2;
end;
theorem NCK:
(n+k) choose k = 1 iff n = 0 or k = 0
proof
A1: n <> 0 & k <> 0 implies (n+k) choose k <> 1
proof
assume n <> 0 & k <> 0; then
reconsider m = n-1,l=k-1 as Nat;
(m+k) choose k >= 1 & (n+l) choose l >= 1 by NAT_1:14; then
B2: ((k+m) choose k) + ((l+n) choose l) >= 1 + 1 by XREAL_1:7;
((m+k)+1) choose (l+1) = ((m+k) choose k) + ((n+l) choose l)
by NEWTON:22;
hence thesis by B2;
end;
n = 0 or k = 0 implies (n+k) choose (k*1) = 1;
hence thesis by A1;
end;
theorem EZ:
(n!)*(k!) = (n+k)! iff (n = 0 or k = 0)
proof
n = (n+k) - k & n+k >= 0+k by XREAL_1:6; then
((n+k) choose (k*1))*((n!)*(k!)) = (n+k)!/((n!)*(k!))*((n!)*(k!))
by NEWTON:def 3
.= (n+k)! by XCMPLX_1:87;
hence thesis by NCK,XCMPLX_1:7;
end;
registration
let n,k be non zero Nat;
cluster (n+k)!-(n!)*(k!) -> positive;
coherence
proof
(n!)*(k!) <= (n+k)! by ES; then
(n!)*(k!) < (n+k)! by EZ,XXREAL_0:1; then
(n!)*(k!)-(n!)*(k!) < (n+k)!-(n!)*(k!) by XREAL_1:9; then
(n+k)!-(n!)*(k!) > 0;
hence thesis;
end;
end;
theorem
for a be Real holds
Sum ((a,a) Subnomial n) = Sum((1,1) Subnomial n)*Sum ((a,0)In_Power n)
proof
let a be Real;
Sum((1,1) Subnomial n)*Sum ((a,0)In_Power (n+1-1)) = (n+1)*(a+0)|^n
by NEWTON:30;
hence thesis by SAA;
end;
theorem
for a,b,c be Real holds Sum ((a+b,c) In_Power n) = Sum((a,b+c) In_Power n)
proof
let a,b,c be Real;
Sum (((a+b),c) In_Power n) = (a+b+c)|^n by NEWTON:30
.= (a+(b+c))|^n
.= Sum ((a,b+c) In_Power n) by NEWTON:30;
hence thesis;
end;
theorem NCI:
(Newton_Coeff n).(i+1) = n choose i
proof
per cases;
suppose
B1: i+1 in dom Newton_Coeff n; then
1 <= i+1 <= len (Newton_Coeff n) by FINSEQ_3:25; then
1 <= i+1 <= n+1 by NEWTON:def 5; then
reconsider k = (n+1)-(i+1) as Element of NAT by NAT_1: 21;
n = i+k & i=(i+1)-1;
hence thesis by B1,NEWTON:def 5;
end;
suppose
B1: not (i+1) in dom Newton_Coeff n; then
not 1 <= i+1 <= len (Newton_Coeff n) by FINSEQ_3:25; then
not 0+1 <= i+1 <= n+1 by NEWTON:def 5; then
not 0 <= i <= n by XREAL_1:6; then
(n choose i) = 0 by NEWTON:def 3;
hence thesis by B1,FUNCT_1:def 2;
end;
end;
theorem
2*n choose n = (2*n)!/((n!)|^2)
proof
A1:n = (2*n) - n;
n+n >= n+0 by XREAL_1:6; then
2*n choose n = ((2*n)!) /((n!)*(n!)) by A1,NEWTON:def 3;
hence thesis by NEWTON:81;
end;
theorem
(Newton_Coeff (2*n+1)).(n+1) = (Newton_Coeff (2*n+1)).(n+2)
proof
reconsider k = 2*n+1 as Nat;
A0: (n+1) + n >= (n+1) + 0 & n+(n+1) >= n + 0 by XREAL_1:6;
A2: len (Newton_Coeff (2*n+1)) = (2*n + 1)+1 by NEWTON:def 5;
1+(n+1) >= 1+0 & (n+2)+n >= (n+2)+0 by XREAL_1:6; then
A4: n+2 in dom (Newton_Coeff (2*n+1)) & n+1 = (n+2)-1 by A2,FINSEQ_3:25;
(2*n+1) - n = n+1; then
reconsider l = k - n as Nat;
(Newton_Coeff (2*n+1)).(n+1) = (2*n+1) choose n by NCI
.= k choose l by A0,NEWTON:20
.= (Newton_Coeff (2*n+1)).(n+2) by A4,NEWTON:def 5;
hence thesis;
end;
theorem
for a be non zero Integer st 1 <= k <= n holds
a divides ((a,b) Subnomial n).k
proof
let a be non zero Integer;
A0: len ((a,b) Subnomial n) = n+1 by Def2;
assume
A1: 1<= k <= n; then
reconsider m = k-1 as Nat;
(k-1)+1 > (k-1)+0 by XREAL_1:6; then
consider l be Nat such that
A2: n = m+l by A1,XXREAL_0:2,NAT_1:10;
m+l >= m+1 by A1,A2; then
l >= 1 by XREAL_1:6; then
reconsider s = l-1 as Nat;
A4: l = n - m by A2;
k+0 <= n+1 by XREAL_1:7,A1; then
k in dom ((a,b) Subnomial n) by A0,A1,FINSEQ_3:25; then
((a,b) Subnomial n).k = a|^(s+1)*b|^m by Def2,A4
.= a*a|^s*b|^m by NEWTON:6
.= a*(a|^s*b|^m);
hence thesis;
end;
theorem DIS:
for a,b be Integer holds
a*b divides ((a,b)In_Power n).i - ((a,b) Subnomial n).i
proof
let a,b be Integer;
per cases;
suppose
A1: i in dom ((a,b)In_Power (n+1-1)); then
A1a: i in dom ((a,b)Subnomial (n+1-1)) by DOMN; then
A1b: 1 <= i <= len ((a,b)Subnomial (n+1-1)) by FINSEQ_3:25; then
A1c: 1-1 <= i-1 <= n by XREAL_1:9;
reconsider m = i - 1 as Nat by A1b;
n - m >= m - m by A1c,XREAL_1:9; then
reconsider l = n - m as Nat by INT_1:3;
A2: ((a,b)In_Power n).i = (n choose m)*a|^l*b|^m by A1,NEWTON:def 4;
A3: ((a,b)In_Power n).i - ((a,b) Subnomial n).i =
(n choose m)*a|^l*b|^m - a|^l*b|^m by A1a,Def2,A2
.= ((n choose m)-1)*(a|^l*b|^m);
per cases;
suppose
m = 0 or m = n; then
(n choose m) = 1 by NEWTON:19,21;
hence thesis by A3,INT_2:12;
end;
suppose
m > 0 & m <> n; then
0 < m < n by A1c,XXREAL_0:1; then
m > 0 & n-m > m-m by XREAL_1:9; then
a divides a|^l & b divides b|^m by NEWTON02:14; then
a*b divides a|^l*b|^m by NEWTON02:2;
hence thesis by A3,INT_2:2;
end;
end;
suppose
A1: not i in dom ((a,b)In_Power (n+1-1)); then
not i in dom ((a,b)Subnomial (n+1-1)) by DOMN; then
((a,b)In_Power n).i = 0 & ((a,b) Subnomial n).i = 0 by A1,FUNCT_1:def 2;
hence thesis by INT_2:12;
end;
end;
theorem INT436:
for f be INT-valued FinSequence, a be Integer st
(for n be Nat st n in dom f holds a divides f.n) holds
a divides Sum f
proof
let f be INT-valued FinSequence, a be Integer such that
A1: for n be Nat st n in dom f holds a divides f.n;
reconsider f1 = f as FinSequence of REAL by NEWTON02:103;
f1.(min_p f1) in INT by INT_1:def 2; then
reconsider k = min f1 as Integer by RFINSEQ2:def 4;
reconsider f2 = f as FinSequence of COMPLEX by NEWTON02:103;
reconsider g = f2 - k as FinSequence of INT by NEWTON02:103;
reconsider g as FinSequence of NAT by NEWTON02:103;
|.a.| in INT & |.a.|>=0 by INT_1:def 2; then
reconsider l = |.a.| as Nat;
A1a: a divides k
proof
per cases;
suppose
B1: (min_p f1) in dom f1;
reconsider x = min_p f1 as Nat;
a divides f.x by B1,A1;
hence thesis by RFINSEQ2:def 4;
end;
suppose not min_p f1 in dom f1; then
0 = f1.(min_p f1) by FUNCT_1:def 2
.= k by RFINSEQ2:def 4;
hence thesis by INT_2:12;
end;
end;
m in dom g implies l divides g.m
proof
assume
B1: m in dom g;
B2: m in dom (f2+-k) by B1,VALUED_1:def 3; then
m in dom f by VALUED_1:def 2; then
a divides f.m & a divides -k by A1,A1a,INT_2:10; then
a divides f.m + -k by WSIERP_1:4; then
a divides (f+-k).m by B2,VALUED_1:def 2; then
a divides (f-k).m by VALUED_1:def 3;
hence thesis by WSIERP_1:13;
end; then
A2: a divides Sum g by INT_4:36,WSIERP_1:13;
A3: a divides k*(len g) by A1a,INT_2:2;
reconsider g as FinSequence of COMPLEX by NEWTON02:103;
Sum (g+k) = Sum g + k*(len g) by SFX;
hence thesis by A2,A3,WSIERP_1:4;
end;
theorem
for a,b be Integer holds
a*b*(a-b) divides (a-b)*(a+b)|^n -(a|^(n+1)-b|^(n+1))
proof
let a,b be Integer;
A0: len ((a,b)In_Power (n+1-1)) = n+1 & len ((a,b)Subnomial (n+1-1)) = n+1;
reconsider R1 = ((a,b)In_Power n) as Element of (n+1)-tuples_on REAL
by A0,FINSEQ_2:92;
reconsider R2 = ((a,b)Subnomial n) as Element of (n+1)-tuples_on REAL
by A0,FINSEQ_2:92;
A1: Sum (((a,b)In_Power n) - ((a,b) Subnomial n)) = Sum (R1-R2)
.= Sum((a,b)In_Power n) - Sum ((a,b) Subnomial n) by RVSUM_1:90;
reconsider f = (((a,b)In_Power n) - ((a,b) Subnomial n)) as
INT-valued FinSequence;
for i be Nat st i in dom f holds
(a*b) divides (((a,b)In_Power n) - ((a,b) Subnomial n)).i
proof
let i be Nat such that
B1: i in dom f;
a*b divides (((a,b)In_Power n).i - ((a,b) Subnomial n).i) by DIS;
hence thesis by B1,VALUED_1:13;
end; then
A2: (a*b) divides Sum (((a,b)In_Power n) - ((a,b) Subnomial n)) by INT436;
(a-b)*(a+b)|^n -(a|^(n+1)-b|^(n+1)) =
(a-b)*(a+b)|^n - (a-b)*Sum((a,b) Subnomial n) by SumS
.= (a-b)*Sum((a,b)In_Power n) - (a-b)*Sum((a,b) Subnomial n) by NEWTON:30
.= (a-b)*(Sum((a,b)In_Power n) - Sum((a,b) Subnomial n));
hence thesis by A1,A2,NEWTON02:2;
end;
theorem ILS:
for a,b be non negative Real holds
((a,b) In_Power n).i >= ((a,b) Subnomial n).i
proof
let a,b be non negative Real;
per cases;
suppose i in dom (Newton_Coeff n); then
(Newton_Coeff n).i <> 0 by D1; then
(Newton_Coeff n).i * ((a,b) Subnomial n).i >= 1*((a,b)Subnomial n).i
by NAT_1:14,XREAL_1:64; then
((Newton_Coeff n)(#)((a,b) Subnomial n)).i >= ((a,b) Subnomial n).i
by VALUED_1:5;
hence thesis by INS;
end;
suppose not i in dom (Newton_Coeff n); then
not i in dom ((a,b)In_Power n) /\ dom (Newton_Coeff n); then
not i in dom ((a,b) Subnomial n) by VALUED_1:16;
hence thesis by FUNCT_1:def 2;
end;
end;
theorem SST:
for a,b be non negative Real holds
(a+b)|^n >= Sum((a,b) Subnomial n)
proof
let a,b be non negative Real;
for i be Nat holds ((a,b) In_Power n).i >= ((a,b) Subnomial n).i
by ILS; then
Sum((a,b) In_Power n) >= Sum((a,b) Subnomial n) by NYS;
hence thesis by NEWTON:30;
end;
theorem SLT:
for a,b be non negative Real, n be non zero Nat holds
a|^n + b|^n <= Sum((a,b) Subnomial n)
proof
let a,b be non negative Real, n be non zero Nat;
reconsider f = (a,b) Subnomial n
as nonnegative-yielding FinSequence of REAL;
len f = n+1 by Def2; then
A1: Sum f = Sum((f|n)/^1) + f.1 + f.(n+1) by NEWTON02:115;
A2: ((a,b) Subnomial n).1 = ((a,b) In_Power n).1 by NS
.= a|^n by NEWTON:28;
A3: ((a,b) Subnomial n).(n+1) = ((a,b) In_Power n).(n+1) by NS
.= b|^n by NEWTON:29;
Sum((f|n)/^1) + (a|^n + b|^n) >= 0 + (a|^n + b|^n) by XREAL_1:6;
hence thesis by A1,A2,A3;
end;
PLT: for a,b be non negative Real, n be non zero Nat holds
a*((a+b)+b)|^n >= (a+b)|^(n+1) - b|^(n+1) >= a*((a+b)|^n + b|^n)
proof
let a,b be non negative Real, n be non zero Nat;
((a+b)-b)*Sum(((a+b),b) Subnomial n) = (a+b)|^(n+1) - b|^(n+1) by SumS;
hence thesis by SST,SLT,XREAL_1:64;
end;
theorem
for a,b be non negative Real, n be non zero Nat holds
a*(a+2*b)|^n + b|^(n+1) >= (a+b)|^(n+1)
proof
let a,b be non negative Real, n be non zero Nat;
a*((a+b)+b)|^n + b|^(n+1) >= ((a+b)|^(n+1) - b|^(n+1)) + b|^(n+1)
by PLT,XREAL_1:6;
hence thesis;
end;
theorem
for a,b be non negative Real, n be non zero Nat holds
a*(a+b)|^n + (a+b)*b|^n <= (a+b)|^(n+1)
proof
let a,b be non negative Real, n be non zero Nat;
a*((a+b)|^n + b|^n) + b*b|^n <= ((a+b)|^(n+1) - b|^(n+1)) + b*b|^n
by PLT,XREAL_1:6; then
a*(a+b)|^n + (a+b)*b|^n <= (a+b)|^(n+1)- b|^(n+1) + b|^(n+1) by NEWTON:6;
hence thesis;
end;
theorem SSI:
for a,b be positive Real, n be non zero Nat holds
Sum ((a,b) Subnomial (n+1)) < Sum ((a,b) In_Power (n+1))
proof
let a,b be positive Real, n be non zero Nat;
A1: for i be Nat holds
((a,b) Subnomial (n+1)).i <= ((a,b) In_Power (n+1)).i by ILS;
reconsider h = ((a,b)Subnomial (n+1))
as nonnegative-yielding FinSequence of REAL;
reconsider g = ((a,b)In_Power (n+1))
as nonnegative-yielding FinSequence of REAL;
1+0 < 1+n by XREAL_1:6; then
1*((a,b) Subnomial (n+1)).(n+1) <
(Newton_Coeff (n+1)).(n+1)*((a,b) Subnomial (n+1)).(n+1)
by XREAL_1:68; then
((a,b) Subnomial (n+1)).(n+1) <
((Newton_Coeff (n+1))(#)((a,b) Subnomial (n+1))).(n+1)
by VALUED_1:5; then
((a,b) Subnomial (n+1)).(n+1) < ((a,b) In_Power (n+1)).(n+1) by INS;
hence thesis by A1,NYS1;
end;
theorem
for a,b be positive Real, n be non zero Nat holds
Sum ((a+b,0)Subnomial (n+1)) > Sum ((a,b)Subnomial (n+1))
proof
let a,b be positive Real, n be non zero Nat;
(a+b - 0)*Sum (((a+b),0)Subnomial (n+1)) =
(a+b)|^((n+1)+1) - 0|^((n+1)+1) by SumS; then
(a+b)*Sum (((a+b),0)Subnomial (n+1)) = (a+b)*(a+b)|^(n+1) by NEWTON:6; then
Sum (((a+b),0)Subnomial (n+1)) = (a+b)|^(n+1) by XCMPLX_1:5; then
Sum (((a+b),0)Subnomial (n+1)) = Sum ((a,b) In_Power (n+1)) by NEWTON:30;
hence thesis by SSI;
end;
theorem
for a,b be Real, n,i be Nat holds
((a,b) Subnomial n).i <= ((|.a.|,|.b.|)Subnomial n).i
proof
let a,b be Real, n,i be Nat;
reconsider f = ((|.a.|,|.b.|) Subnomial n)
as nonnegative-yielding FinSequence of REAL;
per cases;
suppose not i in dom ((a,b) Subnomial n);
hence thesis by FUNCT_1:def 2;
end;
suppose
A0: i in dom ((a,b) Subnomial n); then
A1: 1 <= i <= len ((a,b) Subnomial (n+1-1)) by FINSEQ_3:25; then
reconsider l = i-1 as Nat;
ex k be Nat st n+1 = (l+1) + k by A1,NAT_1:10; then
reconsider k = (n+1) - (l+1) as Nat;
A2: k = n - l & l = i - 1;
A3: |.a.||^k = |.a|^k.| & |.b.||^l = |.b|^l.| by TAYLOR_2:1;
A4: dom ((a,b) Subnomial n) = dom (Newton_Coeff n) by DOMN
.= dom ((|.a.|,|.b.|)Subnomial n) by DOMN;
|.(a|^k)*(b|^l).| >= (a|^k)*(b|^l) by ABSVALUE:4; then
(|.a|^k.|) * (|.b|^l.|) >= a|^k*b|^l by COMPLEX1:65; then
(|.a.||^k)*(|.b.||^l) >= ((a,b) Subnomial (l+k)).(l+1) by A0,A2,A3,LmS1;
hence thesis by A0,A2,A4,LmS1;
end;
end;
theorem
for a be Real, n be Nat, i be odd Nat holds
((a,-a) Subnomial (n+i)).i = a|^(n+i)
proof
let a be Real, n be Nat, i be odd Nat;
A1: len ((a,a) Subnomial ((n+i)+1-1)) = n+i+1 &
len ((a,-a) Subnomial ((n+i)+1-1)) = n+i+1;
i >= 1 & i+(n+1) >= i + 0 by XREAL_1:6,NAT_1:14; then
A2: i in dom ((a,a) Subnomial (i+n)) &
i in dom ((a,-a) Subnomial (i+n)) by A1,FINSEQ_3:25; then
((a*1,(-1)*a) Subnomial (n+i)).i =
((a,a) Subnomial (n+i)).i*((1,-1) Subnomial (n+i)).i by STT
.= a|^(n+i) by A2,CONST;
hence thesis;
end;
theorem
for a be Real, n be Nat, i be non zero Nat holds
((a,-a) Subnomial (n+2*i)).(2*i) = -a|^(n+2*i)
proof
let a be Real, n be Nat, i be non zero Nat;
A1: len ((a,a) Subnomial ((n+2*i)+1-1)) = n+2*i+1 &
len ((a,-a) Subnomial ((n+2*i)+1-1)) = n+2*i+1;
2*i >= 1 & 2*i+(n+1) >= 2*i + 0 by XREAL_1:6,NAT_1:14; then
A2: 2*i in dom ((a,a) Subnomial (2*i+n)) &
2*i in dom ((a,-a) Subnomial (2*i+n)) by A1,FINSEQ_3:25; then
((a*1,(-1)*a) Subnomial (n+2*i)).(2*i) =
((a,a) Subnomial (n+2*i)).(2*i)*((1,-1) Subnomial (n+2*i)).(2*i) by STT
.= a|^(n+2*i)*(-1) by A2,CONST;
hence thesis;
end;
theorem SAN:
for a,b be Real, n be Nat holds
(a,b) Subnomial (n+1) = <*a|^(n+1)*>^(b*(a,b) Subnomial n)
proof
let a,b be Real, n be Nat;
A0: dom ((a,b)Subnomial n) = dom (b*((a,b)Subnomial n)) by VALUED_1:def 5;
A1: dom (a,b)Subnomial (n+1) = dom (<*a|^(n+1)*>^(b*(a,b) Subnomial n))
proof
len (a,b)Subnomial ((n+1)+1-1) = 1 + len ((a,b) Subnomial (n+1-1))
.= 1*(len <*a|^(n+1)*>) + len ((a,b)Subnomial n)
.= (len <*a|^(n+1)*>) + len (b*((a,b)Subnomial n)) by A0,FINSEQ_3:29
.= len (<*a|^(n+1)*>^(b*(a,b) Subnomial n)) by FINSEQ_1:22;
hence thesis by FINSEQ_3:29;
end;
for i be object st i in dom (a,b) Subnomial (n+1) holds
((a,b) Subnomial (n+1)).i = (<*a|^(n+1)*>^(b*(a,b) Subnomial n)).i
proof
let i be object such that
B1: i in dom (a,b)Subnomial (n+1);
reconsider i as non zero Nat by B1,FINSEQ_3:25;
B2: 1 <= i <= len ((a,b)Subnomial ((n+1)+1-1)) by B1,FINSEQ_3:25;
reconsider j = i - 1 as Nat;
B3: j+1 <= (n+1)+1 by B2; then
ex k be Nat st n+1 = j+k by XREAL_1:6,NAT_1:10; then
reconsider k = n+1-j as Nat;
set m = n+1;
per cases;
suppose
C1: j = 0; then
C2: len ((a,b)Subnomial (m+1-1)) - 1 = m & j = 1 - 1 & m - j = m;
1+0 <= 1+m by XREAL_1:6; then
1 <= len ((a,b) Subnomial (m+1-1)); then
1 in dom ((a,b) Subnomial m) by FINSEQ_3:25; then
((a,b) Subnomial m).1 = a|^(n+1)*(1*b|^0) by C2,Def2
.= (<*a|^(n+1)*>^(b*(a,b) Subnomial n)).1;
hence thesis by C1;
end;
suppose
C0: j > 0; then
len ((a,b)Subnomial (n+1-1)) >= j >= 0 + 1
by B3,XREAL_1:6,NAT_1:13; then
C1: j in dom ((a,b) Subnomial (n+1-1)) by FINSEQ_3:25; then
C2: j in dom (b*(a,b) Subnomial (n+1-1)) by VALUED_1:def 5; then
C3: len (b*(a,b)Subnomial (n+1-1)) >= j >= 1 by FINSEQ_3:25;
reconsider x = j-1 as Nat by C0;
C5: n = x+k & k = n-x;
1*len <*a|^(n+1)*> = 1; then
(<*a|^(n+1)*>^(b*(a,b) Subnomial n)).(1+j) = (b*(a,b) Subnomial n).j
by C3, FINSEQ_1:65
.= b*(((a,b)Subnomial (n+1-1)).j) by C2,VALUED_1:def 5
.= b*(a|^k*b|^x) by C1,C5,Def2
.= a|^k*(b*b|^x)
.= a|^k*b|^(x+1) by NEWTON:6
.= ((a,b) Subnomial ((n+1)+1-1)).i by B1,Def2;
hence thesis;
end;
end;
hence thesis by A1,FUNCT_1:2;
end;
theorem
for a,b be Real, n be Nat holds
(a,b) Subnomial (n+2) = <*a|^(n+2)*>^(a*b*(a,b) Subnomial n)^<*b|^(n+2)*>
proof
let a,b be Real, n be Nat;
reconsider f = (b,a) Subnomial n as complex-valued FinSequence;
A0: Rev ((b,a) Subnomial (n+1)) = Rev (<*b|^(n+1)*>^(a*(b,a) Subnomial n))
by SAN
.= (Rev(a*(b,a) Subnomial n))^(Rev<*b|^(n+1)*>) by FINSEQ_5:64
.= (a*(Rev(b,a) Subnomial n))^(Rev<*b|^(n+1)*>) by CREV
.= (a*((a,b)Subnomial n))^<*b|^(n+1)*> by SAB;
(a,b) Subnomial (n+1+1) = <*a|^(n+2)*>^(b*(a,b) Subnomial (n+1)) by SAN
.= <*a|^(n+2)*>^(b*Rev((b,a) Subnomial (n+1))) by SAB
.= <*a|^(n+2)*>^((b*(a*(a,b)Subnomial n))^(b*<*b|^(n+1)*>)) by A0,ADP
.= <*a|^(n+2)*>^(b*(a*(a,b)Subnomial n))^(b*<*b|^(n+1)*>) by FINSEQ_1:32
.= <*a|^(n+2)*>^(b*(a*(a,b)Subnomial n))^(<*b*b|^(n+1)*>) by AMP
.= <*a|^(n+2)*>^(b*(a*(a,b)Subnomial n))^(<*b|^((n+1)+1)*>) by NEWTON:6
.= <*a|^(n+2)*>^(b*a*(a,b)Subnomial n)^(<*b|^((n+1)+1)*>) by VALUED_2:16;
hence thesis;
end;