:: {E}uler's {P}artition {T}heorem
:: by Karol P\kak
::
:: Received March 26, 2015
:: Copyright (c) 2015-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 NUMBERS, ORDINAL1, SUBSET_1, CARD_1, ARYTM_3, TARSKI, RELAT_1,
XXREAL_0, ARYTM_1, XBOOLE_0, FINSET_1, FUNCT_1, NAT_1, ZFMISC_1,
FINSEQ_1, VALUED_0, VALUED_1, CARD_3, RFINSEQ2, NEWTON, EQREL_1,
FIB_NUM2, ORDINAL4, ORDINAL2, GOBRD13, ABIAN, FINSEQ_2, CLASSES1,
MCART_1, FINSOP_1, POWER, RFUNCT_3, MONOID_0, FLEXARY1, EULRPART;
notations TARSKI, XBOOLE_0, XTUPLE_0, SUBSET_1, ORDINAL1, CARD_1, NUMBERS,
XCMPLX_0, RELAT_1, FUNCT_1, RELSET_1, MONOID_0, FUNCT_2, XXREAL_0, NAT_1,
FINSEQ_2, FINSEQ_1, VALUED_0, VALUED_1, FINSET_1, RVSUM_1, CLASSES1,
XXREAL_2, ABIAN, RFINSEQ2, FIB_NUM2, FUNCT_3, NAT_D, MATRIX_0, NEWTON,
POWER, FINSOP_1, RFUNCT_3, JORDAN1H, FLEXARY1;
constructors XXREAL_2, ABIAN, RFINSEQ2, CLASSES1, MONOID_0, NAT_D, FOMODEL2,
RELSET_1, FIB_NUM2, FINSOP_1, NEWTON, POWER, JORDAN1H, FLEXARY1;
registrations ORDINAL1, XREAL_0, FUNCT_1, FINSEQ_1, FINSEQ_2, VALUED_0,
VALUED_1, PRE_POLY, NAT_1, INT_6, RVSUM_1, XCMPLX_0, MEMBERED, VALUED_2,
FOMODEL0, XBOOLE_0, RELAT_1, FUNCT_2, CARD_1, RELSET_1, XXREAL_2,
EUCLID_9, FINSET_1, XXREAL_0, NUMBERS, INT_1, AOFA_A00, XTUPLE_0, NEWTON,
ABIAN, POWER, RFINSEQ, AFINSQ_2, FLEXARY1;
requirements NUMERALS, SUBSET, BOOLE, ARITHM, REAL;
definitions TARSKI, FUNCT_1, FLEXARY1;
equalities FINSEQ_1, FINSEQ_2, XCMPLX_0, FLEXARY1;
expansions FINSEQ_1, TARSKI, XBOOLE_0, FUNCT_1;
theorems ABIAN, CARD_1, CARD_2, CARD_4, CLASSES1, FIB_NUM2, FINSEQ_1,
FINSEQ_2, FINSEQ_3, FOMODEL2, FUNCOP_1, FUNCT_1, FUNCT_2, INTEGRA3,
MATRPROB, NAGATA_2, NAT_1, NAT_D, NEWTON, NUMBERS, ORDINAL1, RELAT_1,
RFINSEQ, RFINSEQ2, RFUNCT_3, RVSUM_1, STIRL2_1, SUBSET_1, TARSKI,
VALUED_0, VALUED_1, XBOOLE_0, XBOOLE_1, XCMPLX_1, XREAL_1, XXREAL_0,
XXREAL_2, ZFMISC_1, FLEXARY1;
schemes FINSEQ_1, FINSEQ_2, FUNCT_2, NAT_1, FLEXARY1;
begin :: Preliminaries
reserve x,y for object,
i,j,k,m,n for Nat;
registration
let r be ext-real number;
cluster <*r*> -> decreasing increasing non-decreasing non-increasing;
coherence;
end;
theorem Th1:
for f,g be non-decreasing ext-real-valued FinSequence st
f.len f <= g.1 holds f^g is non-decreasing
proof
let f,g be non-decreasing ext-real-valued FinSequence such that
A1:f.len f <= g.1;
set fg=f^g;
for e1,e2 be ExtReal st e1 in dom fg & e2 in dom fg & e1 <= e2 holds
fg.e1 <= fg.e2
proof
let e1,e2 be ExtReal such that A2:e1 in dom fg & e2 in dom fg & e1 <= e2;
per cases;
suppose A3:e1 in dom f & e2 in dom f;
then fg.e1=f.e1 & fg.e2=f.e2 by FINSEQ_1:def 7;
hence thesis by A2,A3,VALUED_0:def 15;
end;
suppose A4:e1 in dom f & not e2 in dom f;
then consider i such that
A5:i in dom g & e2=len f+ i by A2,FINSEQ_1:25;
A6:1 <= e1 & e1 <= len f & 1 <= i & i <= len g by A4,A5,FINSEQ_3:25;
then 1 <= len f & 1 <= len g by XXREAL_0:2;
then len f in dom f & 1 in dom g by FINSEQ_3:25;
then A7:f.e1 <= f.len f & g.1 <= g.i by VALUED_0:def 15,A4,A5,A6;
then A8: f.e1 <= g.1 by A1,XXREAL_0:2;
fg.e1 = f.e1 & fg.e2 = g.i by A5,A4,FINSEQ_1:def 7;
hence thesis by A8,A7,XXREAL_0:2;
end;
suppose not e1 in dom f & e2 in dom f;
then not (1<= e1 & e1 <= len f) & e2 <= len f & 1<= e1 by A2,FINSEQ_3:25;
hence thesis by XXREAL_0:2,A2;
end;
suppose A9:not e1 in dom f & not e2 in dom f;
then consider i such that
A10:i in dom g & e1=len f+ i by A2,FINSEQ_1:25;
consider j such that
A11:j in dom g & e2=len f+ j by A2,FINSEQ_1:25,A9;
fg.e1= g.i & fg.e2 = g.j by A10,A11,FINSEQ_1:def 7;
hence thesis by A10,A2,A11,XREAL_1:6,VALUED_0:def 15;
end;
end;
hence thesis by VALUED_0:def 15;
end;
definition
let R be Relation;
attr R is odd-valued means :Def1:
rng R c= OddNAT;
end;
theorem Th2:
n in OddNAT iff n is odd
proof
thus n in OddNAT implies n is odd
proof
assume n in OddNAT;
then ex i be Element of NAT st
n=2*i+1 by FIB_NUM2:def 4;
hence thesis;
end;
assume n is odd;
then consider i such that
A1:n=2*i+1 by ABIAN:9;
i in NAT by ORDINAL1:def 12;
hence thesis by A1,FIB_NUM2:def 4;
end;
registration
cluster odd-valued -> non-zero natural-valued for Relation;
coherence
proof
let R be Relation;
assume A1: R is odd-valued;
OddNAT c= NAT;
then A2: rng R c= NAT by A1;
not 0 in rng R
proof
assume 0 in rng R;
then 0 is odd by A1,Th2;
hence thesis;
end;
hence thesis by ORDINAL1:def 15,A2,VALUED_0:def 6;
end;
end;
definition
let F be Function;
redefine attr F is odd-valued means :Def2: :: redefines odd-valued (EULRPART, definition)
for x st x in dom F holds F.x is odd Nat;
compatibility
proof
thus F is odd-valued implies for x st x in dom F holds F.x is odd Nat
proof
assume A1: F is odd-valued;
let x;
assume x in dom F;
then F.x in rng F by FUNCT_1:def 3;
then F.x in OddNAT by A1;
then ex k be Element of NAT st
F.x = 2*k+1 by FIB_NUM2:def 4;
hence thesis;
end;
assume A2: for x st x in dom F holds F.x is odd Nat;
rng F c= OddNAT
proof
let y;
assume y in rng F;
then consider x such that
A3: x in dom F & F.x=y by FUNCT_1:def 3;
F.x is odd Nat by A2,A3;
then consider i such that
A4: F.x = 2*i+1 by ABIAN:9;
i in NAT by ORDINAL1:def 12;
hence thesis by FIB_NUM2:def 4,A3,A4;
end;
hence thesis;
end;
end;
registration
cluster empty -> odd-valued for Relation;
coherence
proof
let R be Relation;
assume R is empty;
then rng R c= OddNAT;
hence thesis;
end;
let i be odd Nat;
cluster <*i*> -> odd-valued;
coherence
proof
{i} c= OddNAT by Th2,ZFMISC_1:31;
hence thesis by FINSEQ_1:38;
end;
end;
registration
let f,g be odd-valued FinSequence;
cluster f^g -> odd-valued;
coherence
proof
A1:rng f c= OddNAT & rng g c= OddNAT by Def1;
rng (f^g) = (rng f) \/ (rng g) by FINSEQ_1:31;
hence thesis by A1,XBOOLE_1:8;
end;
end;
registration
cluster OddNAT-valued -> odd-valued for Relation;
coherence by RELAT_1:def 19;
end;
definition
let n be Nat;
mode a_partition of n -> non-zero non-decreasing natural-valued FinSequence
means :Def3:
Sum it = n;
existence
proof
per cases;
suppose n<>0;
then not 0 in rng <*n*>;
then A1:<*n*> is non-zero by ORDINAL1:def 15;
Sum <*n*> = n by RVSUM_1:73;
hence thesis by A1;
end;
suppose n=0;
hence thesis by RVSUM_1:72;
end;
end;
end;
theorem
{} is a_partition of 0 by RVSUM_1:72,Def3;
registration
let n be Nat;
cluster odd-valued for a_partition of n;
existence
proof
per cases;
suppose n=0;
then reconsider N={} as a_partition of n by RVSUM_1:72,Def3;
N is odd-valued;
hence thesis;
end;
suppose A1: n is odd;
Sum <*n*>=n by RVSUM_1:73;
then <*n*> is a_partition of n by Def3,A1;
hence thesis by A1;
end;
suppose A2:n is even & n<>0;
then consider i such that
A3:n=2*i by ABIAN:def 2;
i<>0 by A2,A3;
then reconsider i1=i-1 as Nat;
A4: i1*2+1+1 = n by A3;
A5:1=1+2*0;
reconsider N1=<*1*>,N2=<*i1*2+1*> as
non-decreasing natural-valued FinSequence;
len N1=1 by FINSEQ_1:39;
then N1.len N1=1 & N2.1=i1*2+1;
then A6:N1^N2 is non-decreasing by NAT_1:11,Th1;
rng <*1,i1*2+1*> = {1,i1*2+1} by FINSEQ_2:127;
then A7:<*1,i1*2+1*> is non-zero;
N1^N2 = <*1,i1*2+1*>;
then Sum (N1^N2)=n by RVSUM_1:77,A4;
then reconsider N=N1^N2 as a_partition of n by A7,A6,Def3;
N is odd-valued by A5;
hence thesis;
end;
end;
cluster one-to-one for a_partition of n;
existence
proof
per cases;
suppose n=0;
then reconsider N={} as a_partition of n by RVSUM_1:72,Def3;
N is one-to-one;
hence thesis;
end;
suppose n<>0;
then not 0 in rng <*n*>;
then A8:<*n*> is non-zero by ORDINAL1:def 15;
Sum <*n*> = n by RVSUM_1:73;
then reconsider N=<*n*> as a_partition of n by A8,Def3;
N is one-to-one;
hence thesis;
end;
end;
end;
registration
let n be Nat;
sethood of a_partition of n
proof
take N=NAT*;
let p be a_partition of n;
rng p c= NAT by VALUED_0:def 6;
then p is FinSequence of NAT by FINSEQ_1:def 4;
hence thesis by FINSEQ_1:def 11;
end;
end;
definition
let f be odd-valued FinSequence;
mode odd_organization of f -> valued_reorganization of f means :Def4:
2*n-1 = f.it_(n,1) & ... & 2*n-1 = f.it_(n,len (it.n));
existence
proof
A1: rng f c= NAT by VALUED_0:def 6;
{1} c= NAT by ZFMISC_1:31;
then reconsider D=(rng f)\/{1} as finite non empty Subset of NAT by
A1,XBOOLE_1:8;
set m=max D;
deffunc G(Nat)=2*$1-'1;
consider g be FinSequence of NAT such that
A2:
len g = m+1 & for j st j in dom g holds g.j = G(j) from FINSEQ_2:sch 1;
reconsider g as non empty FinSequence of NAT by A2;
rng f c= rng g
proof
let y;
assume A3:y in rng f; then consider x such that
A4:x in dom f & f.x=y by FUNCT_1:def 3;
reconsider n=y as odd Nat by A4,Def2;
consider i such that
A5:2*i+1 =n by ABIAN:9;
n in D by A3,XBOOLE_0:def 3;
then A6:n <= m by XXREAL_2:def 8;
m <= m+(m+1) & m+(m+1) = 2*m+1 by NAT_1:11;
then 2*i+1 <=2*m+1 by A6,A5,XXREAL_0:2;
then 2*i <= 2*m by XREAL_1:6;
then i <=m by XREAL_1:68;
then A7:1<= i+1 & i+1 <= m+1 by XREAL_1:6,NAT_1:11;
then A8:i+1 in dom g by A2,FINSEQ_3:25;
A9: g.(i+1) = 2*(i+1)-'1 by A7,A2,FINSEQ_3:25;
2*1 <= 2*(i+1)by NAT_1:11,XREAL_1:64;
then g.(i+1) = 2*(i+1)-1 by XXREAL_0:2,A9,XREAL_1:233;
hence thesis by A5,A8,FUNCT_1:def 3;
end;
then consider o be len g-element DoubleReorganization of dom f such that
A10: o.n is increasing &
(g.n = f.o_(n,1) &...& g.n = f.o_(n,len (o.n))) by FLEXARY1:39;
o is valued_reorganization of f
proof
thus for n ex x st
x = f.o_(n,1) & ... & x = f.o_(n,len (o.n))
proof
let n;
g.n = f.o_(n,1) &...& g.n = f.o_(n,len (o.n)) by A10;
hence thesis;
end;
let n1,n2,i1,i2 be Nat such that
A11: i1 in dom (o.n1) & i2 in dom (o.n2) &
f.o_(n1,i1) = f.o_(n2,i2);
A12:g.n1 = f.o_(n1,1) &...& g.n1 = f.o_(n1,len (o.n1)) by A10;
1 <= i1 & i1 <= len (o.n1) by A11,FINSEQ_3:25;
then A13:g.n1 = f.o_(n1,i1) by A12;
A14:g.n2 = f.o_(n2,1) &...& g.n2 = f.o_(n2,len (o.n2)) by A10;
1 <= i2 & i2 <= len (o.n2) by A11,FINSEQ_3:25;
then A15:g.n1=g.n2 by A14,A11,A13;
len o = len g by CARD_1:def 7;
then A16:dom o=dom g by FINSEQ_3:29;
A17:n1 in dom g
proof
assume not n1 in dom g;
then o.n1={} by A16,FUNCT_1:def 2;
hence thesis by A11;
end;
then A18:g.n1=G(n1) by A2;
A19:n2 in dom g
proof
assume not n2 in dom g;
then o.n2={} by A16,FUNCT_1:def 2;
hence thesis by A11;
end;
then A20: G(n1)=G(n2) by A2,A18,A15;
2*1 <= 2*n1 by A17,FINSEQ_3:25,XREAL_1:64;
then A21: 2*n1-'1 = 2*n1-1 by XXREAL_0:2,XREAL_1:233;
2*1 <= 2*n2 by A19,FINSEQ_3:25,XREAL_1:64;
then 2*n2-'1 = 2*n2-1 by XXREAL_0:2,XREAL_1:233;
hence n1=n2 by A20,A21;
end;
then reconsider o as valued_reorganization of f;
take o;
for n holds
2*n-1 = f.o_(n,1) & ... & 2*n-1 = f.o_(n,len (o.n))
proof
let n;
let i such that A22:1 <= i & i <= len (o.n);
A23: g.n = f.o_(n,1) &...& g.n = f.o_(n,len (o.n)) by A10;
len o = len g by CARD_1:def 7;
then A24:dom o=dom g by FINSEQ_3:29;
o.n <>{} by A22;
then n in dom o by FUNCT_1:def 2;
then A25:1 <= n & n <= len o & g.n = G(n) by A24,A2,FINSEQ_3:25;
then 2*1 <= 2*n by XREAL_1:64;
then 2*n-'1 = 2*n-1 by XXREAL_0:2,XREAL_1:233;
hence thesis by A23,A22,A25;
end;
hence thesis;
end;
end;
theorem Th4:
for f be odd-valued FinSequence
for o be DoubleReorganization of dom f st
for n holds 2*n-1 = f.o_(n,1) & ... & 2*n-1 = f.o_(n,len (o.n))
holds o is odd_organization of f
proof
let f be odd-valued FinSequence;
let o be DoubleReorganization of dom f such that A1:
for n holds 2*n-1 = f.o_(n,1) & ... & 2*n-1 = f.o_(n,len (o.n));
A2: for n ex x st
x = f.o_(n,1) & ... & x = f.o_(n,len (o.n))
proof
let n;
take x=2*n-1;
thus thesis by A1;
end;
for n1,n2,i1,i2 be Nat st
i1 in dom (o.n1) & i2 in dom (o.n2) &
f.o_(n1,i1) = f.o_(n2,i2)
holds n1 = n2
proof
let n1,n2,i1,i2 be Nat such that
A3: i1 in dom (o.n1) & i2 in dom (o.n2) &
f.o_(n1,i1) = f.o_(n2,i2);
A4:2*n1-1 = f.o_(n1,1) & ... & 2*n1-1 = f.o_(n1,len (o.n1)) by A1;
1<= i1 & i1 <= len (o.n1) by A3,FINSEQ_3:25;
then A5: f.o_(n1,i1) = 2*n1-1 by A4;
A6:2*n2-1 = f.o_(n2,1) & ... & 2*n2-1 = f.o_(n2,len (o.n2)) by A1;
1<= i2 & i2 <= len (o.n2) by A3,FINSEQ_3:25;
then 2*n2-1 = 2*n1-1 by A6,A5,A3;
hence thesis;
end;
then o is valued_reorganization of f by A2,FLEXARY1:def 9;
hence thesis by A1,Def4;
end;
theorem Th5:
for f be odd-valued FinSequence,
g be complex-valued FinSequence
for o1,o2 be DoubleReorganization of dom g st
o1 is odd_organization of f &
o2 is odd_organization of f
holds
Sum (g*.o1).i =Sum (g*.o2).i
proof
let f be odd-valued FinSequence,
g be complex-valued FinSequence;
A1:for o1,o2 be DoubleReorganization of dom g st
o1 is odd_organization of f &
o2 is odd_organization of f
holds
rng (f*.o1.n) c= rng (f*.o2.n)
proof
let o1,o2 be DoubleReorganization of dom g such that
A2:o1 is odd_organization of f &
o2 is odd_organization of f;
reconsider O1=o1 as odd_organization of f by A2;
let y be object;
assume A3:y in rng (f*.o1.n);
then A4: rng (f*.o1.n) = {f.o1_(n,1)} & 1 in dom (o1.n) by FLEXARY1:49,A2;
A5:n in dom o1
proof
assume not n in dom o1;
then o1.n={} by FUNCT_1:def 2;
hence thesis by A3,FLEXARY1:49,A2;
end;
then o1.n.1 in Values o1 by FLEXARY1:1,A4;
then o1.n.1 in dom f by FLEXARY1:def 7,A2;
then o1.n.1 in Values o2 by FLEXARY1:def 7,A2;
then consider j,w be object such that
A6:j in dom o2 & w in dom (o2.j) & o2.j.w = o1.n.1 by FLEXARY1:1;
reconsider j,w as Nat by A6;
A7: (f*.o1).n = f*(o1.n) by A5,FOMODEL2:def 6;
len ((f*.O1).n) = len (o1.n) by CARD_1:def 7;
then A8: dom ((f*.o1).n) = dom (o1.n) by FINSEQ_3:29;
A9:2*n-1 = f.o1_(n,1) & ... & 2*n-1 = f.o1_(n,len (o1.n)) by A2,Def4;
A10: 1 <= len (o1.n) by A4,FINSEQ_3:25;
A11:2*j-1 = f.o2_(j,1) & ... & 2*j-1 = f.o2_(j,len (o2.j)) by A2,Def4;
1<= w & w <= len (o2.j) by A6,FINSEQ_3:25;
then 2*j-1 = f.o2_(j,w) by A11;
then A12: 2*j-1 = 2*n-1 by A6, A10,A9;
then A13:y = f.o2_(n,w) by A4,A3,TARSKI:def 1,A6;
A14:(f*.o2)_(n,w) = f.o2_(n,w) by FLEXARY1:42;
A15:o2.n.w in dom f by A8,A4,A7,FUNCT_1:11,A6, A12;
(f*.o2).n = f*(o2.n) by A12,A6,FOMODEL2:def 6;
then w in dom ((f*.o2).n) by A15, A6, A12,FUNCT_1:11;
hence thesis by FUNCT_1:def 3,A13,A14;
end;
let o1,o2 be DoubleReorganization of dom g such that
A16:o1 is odd_organization of f &
o2 is odd_organization of f;
rng (f*.o1.i) = rng (f*.o2.i) by A1,A16;
hence thesis by A16,FLEXARY1:51;
end;
theorem Th6:
for p be a_partition of n
ex O be odd-valued FinSequence,
a be natural-valued FinSequence st
len O = len p = len a & p = O (#) 2|^a &
( p.1 = O.1 * (2|^a.1) & ... & p.len p = O.len p * (2|^a.len p))
proof
let p be a_partition of n;
defpred P[object,object] means
for i,j st p.$1=(2|^i)*(2*j+1) holds $2=[2*j+1,i];
A1:dom p = Seg len p by FINSEQ_1:def 3;
A2:for k st k in Seg len p ex x st P[k,x]
proof
let k;
assume k in Seg len p;
then p.k in rng p by FUNCT_1:def 3,A1;
then consider n,m be Nat such that
A3:p.k=(2|^n)*(2*m+1) by NAGATA_2:1;
take x=[2*m+1,n];
let i,j;
assume p.k=(2|^i)*(2*j+1);
then i=n & j=m by A3,CARD_4:4;
hence thesis;
end;
consider Oa be FinSequence such that
A4:dom Oa = Seg len p &
for k st k in Seg len p holds P[k,Oa.k] from FINSEQ_1:sch 1(A2);
deffunc P1(object)=(Oa.$1)`1;
consider O be FinSequence such that
A5:len O = len p & for k st k in dom O holds O.k=P1(k) from FINSEQ_1:sch 2;
A6:dom O=dom p by FINSEQ_3:29,A5;
for x st x in dom O holds O.x is odd Nat
proof
let x;
assume A7:x in dom O;
then p.x in rng p by FUNCT_1:def 3,A6;
then consider n,m be Nat such that
A8:p.x=(2|^n)*(2*m+1) by NAGATA_2:1;
Oa.x = [2*m+1,n] by A7,A1,A8,A6,A4;
then P1(x) = 2*m+1;
hence thesis by A7,A5;
end;
then reconsider O as odd-valued FinSequence by Def2;
deffunc P2(object)=(Oa.$1)`2;
consider A be FinSequence such that
A9:len A = len p & for k st k in dom A holds A.k=P2(k) from FINSEQ_1:sch 2;
A10:dom A=dom p by FINSEQ_3:29,A9;
for x st x in dom A holds A.x is natural
proof
let x;
assume A11:x in dom A;
then p.x in rng p by FUNCT_1:def 3,A10;
then consider n,m be Nat such that
A12: p.x=(2|^n)*(2*m+1) by NAGATA_2:1;
Oa.x = [2*m+1,n] by A11,A1,A12,A10,A4;
then P2(x) = n;
hence thesis by A11,A9;
end;
then reconsider A as natural-valued FinSequence by VALUED_0:def 12;
take O,A;
thus len O = len p =len A by A5,A9;
set OA=O (#) 2|^A;
dom (2|^A) = dom A by FLEXARY1:def 4;
then A13:dom O /\ dom (2|^A) = dom p by A10,A6;
A14: p.1 = O.1 * (2|^A.1) & ... & p.len p = O.len p * (2|^A.len p)
proof
let i;
assume A15: 1<= i & i <= len p;
then i in dom p by FINSEQ_3:25;
then p.i in rng p by FUNCT_1:def 3;
then consider n,m be Nat such that
A16:p.i=(2|^n)*(2*m+1) by NAGATA_2:1;
Oa.i = [2*m+1,n] & [2*m+1,n]`1 = 2*m+1 & [2*m+1,n]`2 = n
by A15,FINSEQ_3:25,A1,A16,A4;
then O.i = 2*m+1 & A.i = n by A15,FINSEQ_3:25,A5,A9;
hence thesis by A16;
end;
for i st i in dom p holds p.i = OA.i
proof
let i;
assume A17:i in dom p;
then 1 <= i & i <= len p by FINSEQ_3:25;
then A18: p.i = O.i * ( 2|^A.i) by A14;
(2|^A).i = 2 to_power (A.i) by A17,A10,FLEXARY1:def 4;
hence thesis by VALUED_1:5,A18;
end;
hence thesis by A13,VALUED_1:def 4,A14;
end;
theorem Th7:
for D be finite set
for f be Function of D,NAT
ex h be FinSequence of D st
for d be Element of D holds
card Coim(h,d) = f.d
proof
defpred P[Nat] means
for D be finite set st card D=$1
for f be Function of D,NAT
ex h be FinSequence of D st
for d be Element of D holds
card Coim(h,d) = f.d;
A1:P[0]
proof
let D be finite set such that A2:card D=0;
let f be Function of D,NAT;
take h=<*>D;
let d be Element of D;
A3: Coim(h,d)=h"{d} by RELAT_1:def 17;
not d in dom f by A2;
hence thesis by FUNCT_1:def 2,A3;
end;
A4:P[i] implies P[i+1]
proof
assume A5:P[i];
set i1=i+1;
let D be finite set such that A6:card D=i1;
let f be Function of D,NAT;
D is non empty by A6;
then consider d be object such that
A7:d in D;
set Dd=D\{d};
A8:card Dd = i by A6,A7,STIRL2_1:55;
reconsider fd=f|Dd as Function of Dd,NAT;
consider h be FinSequence of Dd such that
A9:for x be Element of Dd holds
card Coim(h,x) = fd.x by A5,A8;
A10:rng h c= Dd;
Dd c= D;
then rng h c= D;
then reconsider h as FinSequence of D by FINSEQ_1:def 4;
reconsider g=f.d |-> d as FinSequence of D by A7,FINSEQ_2:63;
take hg=h^g;
let x be Element of D;
Coim(hg,x) = hg"{x} & Coim(h,x) = h"{x} & Coim(g,x) = g"{x}
by RELAT_1:def 17;
then A11:card Coim(hg,x) = card (h"{x})+ card (g"{x}) by FINSEQ_3:57;
per cases;
suppose A12:x<>d;
then x in Dd by A7,ZFMISC_1:56;
then A13: card Coim(h,x) = fd.x & fd.x = f.x by A9,FUNCT_1:49;
not d in {x} by A12,TARSKI:def 1;
then g"{x}={} by FUNCOP_1:16;
hence thesis by RELAT_1:def 17,A11,A13;
end;
suppose A14:x=d;
then not x in rng h by ZFMISC_1:56,A10;
then A15:h"{x} = {} by FUNCT_1:72;
d in {x} by A14,TARSKI:def 1;
then g"{x}=Seg (f.d) by FUNCOP_1:14;
hence thesis by FINSEQ_1:57,A15,A11,A14;
end;
end;
let D be finite set;
P[i] from NAT_1:sch 2(A1,A4);
then P[card D];
hence thesis;
end;
Lm1:
for f1,f2,g1,g2 be complex-valued FinSequence st
len f1 = len g1 & len f2 <= len g2 holds
(f1^f2) (#) (g1^g2) = (f1(#)g1)^(f2(#)g2)
proof
let f1,f2,g1,g2 be complex-valued FinSequence such that
A1:len f1 = len g1
and
A2:len f2 <= len g2;
A3:dom f1 = Seg len f1 & dom f2 = Seg len f2 & dom g1 = Seg len g1 &
dom g2 = Seg len g2 by FINSEQ_1:def 3;
A4:dom (f1^f2) = Seg len (f1^f2) & dom (g1^g2) = Seg len (g1^g2)
by FINSEQ_1:def 3;
A5:len (f1^f2) = len f1 + len f2 & len (g1^g2) = len g1 + len g2
by FINSEQ_1:22;
then dom (f1^f2)/\dom (g1^g2) = dom (f1^f2)
by A1,A2,XREAL_1:6,A4,FINSEQ_1:7;
then dom ((f1^f2)(#)(g1^g2)) = dom (f1^f2) by VALUED_1:def 4;
then A6:len ((f1^f2)(#)(g1^g2))= len (f1^f2) by FINSEQ_3:29;
dom f1/\dom g1 = dom f1 by A1,A3;
then A7: dom (f1(#)g1) = dom f1 by VALUED_1:def 4;
then A8:len (f1(#)g1) = len f1 by FINSEQ_3:29;
A9: dom f2/\dom g2 = dom f2 by A2,A3,FINSEQ_1:7;
then A10: dom (f2(#)g2) = dom f2 by VALUED_1:def 4;
then A11: len (f2(#)g2) = len f2 by FINSEQ_3:29;
for i st 1<= i & i <= len (f1^f2) holds
((f1^f2) (#) (g1^g2)).i = ((f1(#)g1)^(f2(#)g2)).i
proof
let i;
assume 1<= i & i <= len (f1^f2);
then A12:i in dom (f1^f2) by FINSEQ_3:25;
per cases;
suppose A13: i in dom f1;
then A14:(f1^f2).i = f1.i & (g1^g2).i = g1.i by A1,A3,FINSEQ_1:def 7;
((f1(#)g1)^(f2(#)g2)).i = (f1(#)g1).i by A13,A7, FINSEQ_1:def 7
.= (f1.i) * (g1.i) by VALUED_1:5;
hence thesis by A14,VALUED_1:5;
end;
suppose not i in dom f1;
then consider j such that
A15:j in dom f2 & i=len f1+j by A12,FINSEQ_1:25;
A16:(f1^f2).i = f2.j & (g1^g2).i = g2.j by A9,A15,A1,FINSEQ_1:def 7;
((f1(#)g1)^(f2(#)g2)).i = (f2(#)g2).j by A15,A8,A10,FINSEQ_1:def 7
.= (f2.j) * (g2.j) by VALUED_1:5;
hence thesis by VALUED_1:5,A16;
end;
end;
hence thesis by A5,A6,A8,A11,FINSEQ_1:22;
end;
theorem Th8:
for f1,f2,g1,g2 be complex-valued FinSequence st len f1 = len g1 holds
(f1^f2) (#) (g1^g2) = (f1(#)g1)^(f2(#)g2)
proof
let f1,f2,g1,g2 be complex-valued FinSequence such that
A1:len f1 = len g1;
len f2 <= len g2 or len f2 >= len g2;
hence thesis by A1,Lm1;
end;
Lm2: for f be complex-valued FinSequence holds
((id dom f) (#)f).i = i*f.i
proof
let f be complex-valued FinSequence;
per cases;
suppose i in dom f;
then (id dom f).i = i by FUNCT_1:17;
hence thesis by VALUED_1:5;
end;
suppose not i in dom f;
then A1: f.i = 0 by FUNCT_1:def 2;
((id dom f) (#)f).i = (id dom f).i * f.i by VALUED_1:5;
hence thesis by A1;
end;
end;
theorem Th9:
for f,h be natural-valued FinSequence st
for i holds card Coim(h,i) = f.i
holds Sum h = 1 * f.1 + 2 * f.2 + ((id dom f)(#)f,3) +...
proof
defpred P[Nat] means
for f,h be natural-valued FinSequence st len f = $1 &
for i holds card Coim(h,i) = f.i
holds Sum h = ((id dom f) (#)f,1) +...;
A1:P[0]
proof
let f,h be natural-valued FinSequence such that
A2:len f = 0
and
A3:for i holds card Coim(h,i) = f.i;
set L=(len h) |->0;
now let i such that A4:1 <= i & i <= len h;
A5:i in dom h by A4,FINSEQ_3:25;
f={} by A2;
then f.(h.i)=0;
then card Coim(h,h.i) =0 by A3;
then Coim(h,h.i)={};
then h"{h.i} = {} by RELAT_1:def 17;
then not h.i in rng h by FUNCT_1:72;
hence h.i = L.i by A5,FUNCT_1:def 3;
end;
then A6: h = (len h) |->0 by CARD_1:def 7;
A7: f={} by A2;
then reconsider E= (id dom f) (#)f as complex-valued FinSequence;
((id dom f) (#)f,1) +... = E.1 + (E,1+1) +... by FLEXARY1:20
.= Sum E by FLEXARY1:22
.=0 by A7,RVSUM_1:72;
hence thesis by A6,RVSUM_1:81;
end;
A8:P[i] implies P[i+1]
proof
assume A9:P[i];
set i1=i+1;
let f,h be natural-valued FinSequence such that
A10:len f = i1
and
A11:for i holds card Coim(h,i) = f.i;
A12:id dom f = idseq i1 by FINSEQ_1:def 3,A10;
set fi=f|i;
A13: f = fi^ <*f.i1*> by A10,FINSEQ_3:55;
A14:i < i1 by NAT_1:13;
then A15:len fi = i by A10,FINSEQ_1:59;
then A16: id dom fi = idseq i by FINSEQ_1:def 3;
A17: idseq i1 = (idseq i)^ <*i1*> by FINSEQ_2:51;
len fi = len (idseq i) by CARD_1:def 7,A15;
then A18: (id dom f) (#) f = ((idseq i) (#)fi)^(<*i1*>(#)<*f.i1*>)
by Th8,A12,A13,A17;
A19: Seg 1 /\Seg 1 = Seg 1;
dom <*i1*> = Seg 1 & dom <*f.i1*> = Seg 1 by FINSEQ_1:38;
then dom (<*i1*>(#)<*f.i1*>) = Seg 1 by VALUED_1:def 4,A19;
then A20: len (<*i1*>(#)<*f.i1*>) = 1 by FINSEQ_1:def 3;
<*i1*>.1=i1 & <*f.i1*>.1 = f.i1;
then (<*i1*>(#)<*f.i1*>).1 = i1 * (f.i1) by VALUED_1:5;
then A21: <*i1*>(#)<*f.i1*> = <*i1 * (f.i1)*> by A20,FINSEQ_1:40;
A22:((id dom f) (#) f,1)+... = Sum ((idseq i1)(#)f) by A12,FLEXARY1:21;
per cases;
suppose A23: f.i1 =0;
then A24: ((id dom f) (#) f,1)+... = (Sum ((idseq i) (#)fi)) + 0
by A21,A12,A18,A22,RVSUM_1:74;
for j holds card Coim(h,j) = fi.j
proof
let j;
per cases;
suppose j in dom fi;
then fi.j=f.j & f.j = card Coim(h,j) by A11,FUNCT_1:47;
hence thesis;
end;
suppose A25: j = i1;
then not j in dom fi by A14,A15,FINSEQ_3:25;
then fi.j=0 & f.j = card Coim(h,j) by A11,FUNCT_1:def 2;
hence thesis by A23,A25;
end;
suppose A26: j <> i1 & not j in dom fi;
then A27:fi.j = 0 by FUNCT_1:def 2;
j < 1 or j >i by A26,A15,FINSEQ_3:25;
then j < 1 or j >= i1 by NAT_1:13;
then j < 1 or j > i1 by A26,XXREAL_0:1;
then not j in dom f by A10,FINSEQ_3:25;
then f.j=0 by FUNCT_1:def 2;
hence thesis by A11,A27;
end;
end;
then Sum h = ((idseq i)(#)fi,1)+... by A9,A16,A15
.= Sum ((idseq i) (#)fi) by FLEXARY1:21;
hence thesis by A24;
end;
suppose f.i1 <>0;
then card Coim(h,i1)<>0 by A11;
then Coim(h,i1) <>{};
then consider xx be object such that
A28:xx in Coim(h,i1) by XBOOLE_0:def 1;
A29:xx in Coim(h,i1) & Coim(h,i1) = h"{i1} by A28,RELAT_1:def 17;
then reconsider D=dom h as non empty set by FUNCT_1:def 7;
A30: rng h c= REAL;
then reconsider H=h as Function of D,REAL by FUNCT_2:2;
reconsider h1=H as FinSequence of REAL by A30,FINSEQ_1:def 4;
set X = h"{i1},Y=D\X;
dom (H| (Y\/X)) is finite;
then A31: FinS(H,Y \/ X), FinS(H,Y) ^ FinS(H,X) are_fiberwise_equipotent
by RFUNCT_3:76,XBOOLE_1:79;
A32: D = X \/ Y by RELAT_1:132,XBOOLE_1:45;
H|D = H;
then H,FinS(H,X \/ Y) are_fiberwise_equipotent by A32,RFUNCT_3:def 13;
then A33: Sum h1 = Sum (FinS(H,Y) ^ FinS(H,X))
by A31,CLASSES1:76,RFINSEQ:9
.= Sum FinS(H,Y) + Sum FinS(H,X) by RVSUM_1:75;
A34:dom (H|X) = X & dom (H|Y) = Y by RELAT_1:132,RELAT_1:62;
rng (H|X) c= {i1}
proof
let y be object;
assume y in rng (H|X);
then consider x be object such that
A35:x in X & (H|X).x=y by A34,FUNCT_1:def 3;
(H|X).x=H.x by A35,FUNCT_1:49;
hence thesis by A35,FUNCT_1:def 7;
end;
then FinS(H,X) = (card X) |->i1 by A29,A34,ZFMISC_1:33,RFUNCT_3:75;
then A36: FinS(H,X) = (f.i1) |->i1 by A29,A11;
A37: H|Y, FinS(H,Y) are_fiberwise_equipotent by A34,RFUNCT_3:def 13;
then rng (H|Y) = rng FinS(H,Y) by CLASSES1:75;
then rng FinS(H,Y) c= NAT by VALUED_0:def 6;
then reconsider F=FinS(H,Y) as natural-valued FinSequence
by VALUED_0:def 6;
for j holds card Coim(F,j) = fi.j
proof
let j;
set hY=h|Y;
A38: card Coim(F,j) = card Coim(hY,j) by A37,CLASSES1:def 10;
A39: hY"{j} = Coim(hY,j) & h"{j} = Coim(h,j) by RELAT_1:def 17;
A40: hY"{j} = Y /\ h"{j} by FUNCT_1:70
.= (h"{j}/\D) \h"{i1} by XBOOLE_1:49
.= h"{j} \h"{i1} by RELAT_1:132,XBOOLE_1:28
.= h"({j}\{i1}) by FUNCT_1:69;
A41: card Coim(h,j) = f.j by A11;
per cases;
suppose A42:j in dom fi;
then j<>i1 by A15,FINSEQ_3:25,A14;
then card Coim(F,j) = card Coim(h,j) by ZFMISC_1:14,A38,A39,A40;
hence thesis by A41,A42,FUNCT_1:47;
end;
suppose A43:j = i1;
then A44:not j in dom fi by A14,A15,FINSEQ_3:25;
card Coim(F,j) = card (h"{}) by A43,A38,A39,A40;
hence thesis by A44,FUNCT_1:def 2;
end;
suppose A45:not j in dom fi & j<>i1;
then A46:fi.j = 0 by FUNCT_1:def 2;
j < 1 or j >i by A45,A15,FINSEQ_3:25;
then j < 1 or j >= i1 by NAT_1:13;
then j < 1 or j > i1 by A45,XXREAL_0:1;
then A47:not j in dom f by A10,FINSEQ_3:25;
card Coim(F,j) = card Coim(h,j) by A45,ZFMISC_1:14,A38,A39,A40;
hence thesis by A46,A47,FUNCT_1:def 2,A41;
end;
end;
then A48: Sum F = ((idseq i)(#)fi,1)+... by A9,A15,A16
.= Sum ((idseq i) (#)fi) by FLEXARY1:21;
((id dom f) (#) f,1)+... = (Sum ((idseq i) (#)fi)) + (i1 * (f.i1))
by A21,A12,A18,A22,RVSUM_1:74;
hence thesis by A33,A48,A36,RVSUM_1:80;
end;
end;
A49:P[i] from NAT_1:sch 2(A1,A8);
let f,h be natural-valued FinSequence such that A50:
for i holds card Coim(h,i) = f.i;
set I=(idseq len f) (#)f;
A51:id dom f = idseq len f by FINSEQ_1:def 3;
then A52: I.1 = 1*f.1 by Lm2;
A53: I.2 = 2*f.2 by Lm2,A51;
Sum h = (I,1) +... by A49,A51,A50
.= I.1 + (I,1+1)+... by FLEXARY1:20
.= I.1 +(I.2 +(I,2+1)+...) by FLEXARY1:20;
hence thesis by A52,A53,A51;
end;
theorem Th10:
for g be natural-valued FinSequence
for sort be DoubleReorganization of dom g
ex h be (2*len sort)-element FinSequence of NAT st
for j holds h.(2*j) = 0 &
h.(2*j-1) = g. sort_(j,1) + (g*.sort.j,2)+...
proof
let g be natural-valued FinSequence;
let sort be DoubleReorganization of dom g;
defpred P[object,object] means
($1 = 2*j-1 implies
$2 = g. sort_(j,1) + (g*.sort.j,2)+...) &
($1 = 2*j implies $2 = 0);
set S=Seg (2* len sort);
A1: for k st k in S ex x st P[k,x]
proof
let k;
assume k in Seg (2*len sort);
per cases;
suppose A2:k is even;
set j=the Nat;
take x = 0;
thus thesis by A2;
end;
suppose k is odd;
then consider j such that
A4: k=2*j+1 by ABIAN:9;
set j1=j+1;
take x= g. sort_(j1,1) + (g*.sort.j1,2)+...;
let i;
thus thesis by A4;
end;
end;
consider f be FinSequence such that
A5:dom f = S & for i st i in S holds P[i,f.i] from FINSEQ_1:sch 1(A1);
A6:rng f c= NAT
proof
let y;
assume y in rng f;
then consider x such that
A7:x in dom f & f.x=y by FUNCT_1:def 3;
reconsider x as Nat by A7;
per cases;
suppose x is even;
then ex i st x=2*i by ABIAN:def 2;
then f.x=0 by A5,A7;
hence thesis by A7;
end;
suppose x is odd;
then consider i such that
A8: x = 2*i+1 by ABIAN:9;
2*(i+1) - 1 = x by A8;
then f.x= g. sort_(i+1,1) + (g*.sort.(i+1),2)+... by A7,A5;
hence thesis by A7,ORDINAL1:def 12;
end;
end;
A9: len f = (2*len sort) by A5,FINSEQ_1:def 3;
then reconsider f as (2*len sort)-element FinSequence of NAT
by A6,FINSEQ_1:def 4,CARD_1:def 7;
take f;
let i;
thus f.(2*i) = 0
proof
2*i in dom f or not 2*i in dom f;
hence thesis by A5,FUNCT_1:def 2;
end;
thus f.(2*i-1) = g. sort_(i,1) + (g*.sort.i,2)+...
proof
per cases by FINSEQ_3:25;
suppose 2*i-1 in dom f;
hence thesis by A5;
end;
suppose A10:2*i-1 > len f;
then A11:not 2*i-1 in dom f by FINSEQ_3:25;
2*i-1 +1 > len f by A10,NAT_1:13;
then i > len sort by A9,XREAL_1:64;
then A12: not i in dom sort by FINSEQ_3:25;
then sort.i = {} by FUNCT_1:def 2;
then not sort_(i,1) in dom g by FINSEQ_3:25;
then A13: g. sort_(i,1)={} by FUNCT_1:def 2;
dom (g*.sort)= dom sort by FOMODEL2:def 6;
then g*.sort.i = {} by A12,FUNCT_1:def 2;
then g. sort_(i,1) + (g*.sort.i,2)+... = 0 by FLEXARY1:15,A13;
hence thesis by A11,FUNCT_1:def 2;
end;
suppose A14: 2*i-1 < 1;
then A15: not 2*i-1 in dom f by FINSEQ_3:25;
2*i-1+1 < 1+1 by A14,XREAL_1:6;
then 2*i < 2*1;
then A16:not i in dom sort by XREAL_1:64,FINSEQ_3:25;
then sort.i = 0 by FUNCT_1:def 2;
then not sort_(i,1) in dom g by FUNCT_1:def 2,FINSEQ_3:25;
then A17:g. sort_(i,1)=0 by FUNCT_1:def 2;
dom (g*.sort)= dom sort by FOMODEL2:def 6;
then g*.sort.i = {} by A16,FUNCT_1:def 2;
then g.sort_(i,1) + (g*.sort.i,2)+... = 0 by FLEXARY1:15,A17;
hence thesis by A15,FUNCT_1:def 2;
end;
end;
end;
Lm3:for mu be natural-valued FinSequence st
for j holds mu.(2*j) = 0
ex h be odd-valued FinSequence st
h is non-decreasing &
for j holds card Coim(h,j) = mu.j
proof
let mu be natural-valued FinSequence such that
A1:for j holds mu.(2*j) = 0;
set S=Seg len mu;
A2:rng mu c= NAT by VALUED_0:def 6;
A3:dom mu = S by FINSEQ_1:def 3;
then mu is Function of S,NAT by A2,FUNCT_2:2;
then consider h be FinSequence of S such that
A4: for d be Element of S holds
card Coim(h,d) = mu.d by Th7;
A5: rng h c= S by FINSEQ_1:def 4;
A6: rng h c= OddNAT
proof
let y be object;
assume A7:y in rng h;
then A8: card Coim(h,y) = mu.y by A4,A5;
Coim(h,y) = h"{y} by RELAT_1:def 17;
then A9: Coim(h,y)<>{} by A7,FUNCT_1:72;
consider x such that
A10:x in dom h & h.x=y by A7,FUNCT_1:def 3;
reconsider y as Nat by A10;
y is odd
proof
assume y is even;
then ex j st y=2*j by ABIAN:def 2;
hence thesis by A1,A9,A8;
end;
hence thesis by Th2;
end;
then reconsider h as odd-valued FinSequence by Def1;
rng h c= REAL;
then reconsider h as FinSequence of REAL by FINSEQ_1:def 4;
set s= sort_a h;
rng h=rng s by RFINSEQ2:def 6,CLASSES1:75;
then reconsider s as odd-valued FinSequence by A6,Def1;
take s;
thus s is non-decreasing;
let i;
per cases;
suppose i in S;
then mu.i=card Coim(h,i) by A4;
hence thesis by RFINSEQ2:def 6,CLASSES1:def 10;
end;
suppose A11: not i in S;
then A12:mu.i = 0 & not i in rng h by A5,A3,FUNCT_1:def 2;
h"{i}= {} by A11,A5,FUNCT_1:72;
then Coim(h,i) = {} by RELAT_1:def 17;
then card Coim(h,i)=0;
hence thesis by CLASSES1:def 10,RFINSEQ2:def 6,A12;
end;
end;
begin :: Euler Transformation
theorem Th11:
for d be one-to-one a_partition of n
ex e be odd-valued a_partition of n st
for j be Nat, O1 be odd-valued FinSequence,
a1 be natural-valued FinSequence st
len O1 = len d = len a1 & d = O1 (#) 2|^a1
for sort be DoubleReorganization of dom d
st
(1 = O1.sort_(1,1) & ... & 1 = O1.sort_(1,len (sort.1))) &
(3 = O1.sort_(2,1) & ... & 3 = O1.sort_(2,len (sort.2))) &
(5 = O1.sort_(3,1) & ... & 5 = O1.sort_(3,len (sort.3))) &
for i holds
2*i-1 = O1.sort_(i,1) & ... & 2*i-1 = O1.sort_(i,len (sort.i))
holds
card Coim(e,1) = (2|^a1). sort_(1,1) + ((2|^a1)*.sort.1,2)+... &
card Coim(e,3) = (2|^a1). sort_(2,1) + ((2|^a1)*.sort.2,2)+... &
card Coim(e,5) = (2|^a1). sort_(3,1) + ((2|^a1)*.sort.3,2)+... &
card Coim(e,j*2-1) = (2|^a1). sort_(j,1) + ((2|^a1)*.sort.j,2)+...
proof
let d be one-to-one a_partition of n;
consider O be odd-valued FinSequence,
a be natural-valued FinSequence such that
A1:len O = len d = len a & d = O (#) 2|^a and
d.1 = O.1 * (2|^a.1) & ... & d.len d = O.len d * (2|^a.len d) by Th6;
len (2|^a)=len O by A1,CARD_1:def 7;
then reconsider sort = the odd_organization of O as
DoubleReorganization of dom (2|^a) by FINSEQ_3:29;
consider mu be (2*len sort)-element FinSequence of NAT such that
A2: for j holds mu.(2*j) = 0 &
mu.(2*j-1) = (2|^a). sort_(j,1) + ((2|^a)*.sort.j,2)+... by Th10;
set alpha = a*(sort.1),beta = a*(sort.2),gamma = a*(sort.3);
A3:n = ((2|^alpha).1 + (2|^alpha,2)+...) * 1 +
((2|^beta).1 + (2|^beta,2)+...) * 3 +
((2|^gamma).1 + (2|^gamma,2)+...) * 5 +
((id dom mu)(#)mu,7)+...
proof
reconsider o1=sort as DoubleReorganization of dom d by A1,FINSEQ_3:29;
A4:dom (d*.o1) = dom o1 & dom ((2|^a)*.sort)=dom sort
by FOMODEL2:def 6;
A5:for j holds Sum (d*.o1.j) = (2*j-1) *mu.(2*j-1)
proof
let j;
A6: mu.(2*j-1) = (2|^a).sort_(j,1) + ((2|^a)*.sort.j,2)+... by A2;
per cases;
suppose j in dom o1;
set jj=2*j-1;
A7:d*.o1.j = d*(o1.j) by FLEXARY1:41;
A8:(2|^a)*.sort.j = (2|^a)*(sort.j) by FLEXARY1:41;
A9:len (d*.o1.j) = len (o1.j) by CARD_1:def 7;
A10:len ((2|^a)*.sort.j) = len (sort.j) by CARD_1:def 7;
for n st 1<=n & n <= len (sort.j) holds
d*.o1.j.n = (jj * ((2|^a)*.sort.j)).n
proof
let n;
assume A11:1<=n & n <= len (sort.j);
A12: 2*j-1 = O.o1_(j,1) &...& 2*j-1 = O.o1_(j,len (o1.j)) by Def4;
thus d*.o1.j.n = d.o1_(j,n) by A11,A9,FINSEQ_3:25,A7,FUNCT_1:12
.= O.o1_(j,n) * (2|^a).o1_(j,n) by A1,VALUED_1:5
.=jj*(2|^a).o1_(j,n) by A12,A11
.= jj* (((2|^a)*.sort.j).n) by A11,A10,FINSEQ_3:25,A8,FUNCT_1:12
.= (jj * ((2|^a)*.sort.j)).n by VALUED_1:6;
end;
then A13: d*.o1.j = jj * ((2|^a)*.sort.j) by A9,CARD_1:def 7;
((2|^a)*.sort.j).1=((2|^a)*.sort)_(j,1);
then (2|^a).sort_(j,1) = ((2|^a)*.sort.j).1 by FLEXARY1:42;
then Sum ((2|^a)*.sort.j)
= (2|^a).sort_(j,1) + ((2|^a)*.sort.j,2)+... by FLEXARY1:22
.= mu.jj by A2;
hence thesis by A13,RVSUM_1:87;
end;
suppose A14: not j in dom sort;
then sort.j = {} by FUNCT_1:def 2;
then A15: not sort.j.1 in dom (2|^a) by FINSEQ_3:25;
not j in dom ((2|^a)*.sort) by A14,FOMODEL2:def 6;
then (2|^a)*.sort.j={} by FUNCT_1:def 2;
then ((2|^a)*.sort.j,2)+... = 0 by FLEXARY1:15;
then mu.(2*j-1) = 0 by A6, A15,FUNCT_1:def 2;
hence thesis by A14,A4,FUNCT_1:def 2,RVSUM_1:72;
end;
end;
set I=idseq len mu;
A16: I=id dom mu by FINSEQ_1:def 3;
A17:1-'1=0 & 2-'1 = 2-1 by XREAL_1:233,232;
A18:for j holds (Sum (d*.o1),4+j*1)+...+(Sum (d*.o1),4+j*1+(1-'1)) =
(I(#)mu,7+j*2)+...+(I(#)mu,7+j*2+(2-'1))
proof
let j;
set S=Sum (d*.o1);
A19: (S,4+j*1)+...+(S,4+j*1+(1-'1)) = S.(4+j) by A17,FLEXARY1:11
.= Sum (d*.o1.(4+j)) by FLEXARY1:def 8
.= (2*(4+j)-1) *mu.(2*(4+j)-1) by A5
.= (2*j+7) *mu.(2*j+7);
A20: (I(#)mu,7+j*2)+...+(I(#)mu,7+j*2+(2-'1)) =
(I(#)mu).(7+j*2)+
(I(#)mu,7+j*2+1)+...+(I(#)mu,7+j*2+1) by NAT_1:11,FLEXARY1:13,A17
.= (I(#)mu).(7+j*2)+(I(#)mu).(7+j*2+1) by FLEXARY1:11;
(7+j*2+1)=2*(j+4);
then mu.(7+j*2+1) = 0 by A2;
then (I(#)mu).(7+j*2+1) = (7+j*2+1)*0 by A16,Lm2;
hence thesis by A19,A20,A16,Lm2;
end;
A21:(Sum (d*.o1),4) +... = (I(#)mu,7) +... from FLEXARY1:sch 1(A18);
A22:2*1-1=1;
then A23: 1*mu.1 = Sum (d*.o1.1) by A5
.= (Sum (d*.o1)).1 by FLEXARY1:def 8;
A24: 2*2-1=3;
then A25: 3*mu.3 = Sum (d*.o1.2) by A5
.= (Sum (d*.o1)).2 by FLEXARY1:def 8;
A26:2*3-1=5;
then A27: 5*mu.5 = Sum (d*.o1.3) by A5
.= (Sum (d*.o1)).3 by FLEXARY1:def 8;
for j holds (2|^a).sort_(j,1) = (2|^(a *(sort.j))).1 &
((2|^a)*.sort).j = 2|^(a *(sort.j))
proof
let j;
A28:(2|^a).sort_(j,1) = ((2|^a)*.sort)_(j,1) by FLEXARY1:42;
((2|^a)*.sort).j = (2|^a)*(sort.j) by FLEXARY1:41
.= 2|^(a*(sort.j)) by FLEXARY1:25;
hence thesis by A28;
end;
then A29:(2|^a).sort_(1,1) = (2|^alpha).1 &
(2|^a).sort_(2,1) = (2|^beta).1 &
(2|^a).sort_(3,1) = (2|^gamma).1 &
(2|^a)*.sort.1 = 2|^alpha &
(2|^a)*.sort.2 = 2|^beta &
(2|^a)*.sort.3 = 2|^gamma;
thus n = Sum d by Def3
.= Sum Sum (d*.o1) by FLEXARY1:47
.= 1*mu.1 + (Sum (d*.o1),2)+... by FLEXARY1:22,A23
.= 1*mu.1 + (3*mu.3 +(Sum (d*.o1),2+1) +...) by A25,FLEXARY1:20
.= 1*mu.1 + 3*mu.3 +(Sum (d*.o1),3) +...
.= 1*mu.1 + 3*mu.3 + (5*mu.5 +(Sum (d*.o1),3+1) +...)
by FLEXARY1:20,A27
.= 1*mu.1 + 3*mu.3 + 5*mu.5 +((id dom mu)(#)mu,7) +... by A16,A21
.= 1*((2|^a).sort_(1,1) + ((2|^a)*.sort.1,2)+...)
+ 3*mu.3 + 5*mu.5 +((id dom mu)(#)mu,7) +... by A2,A22
.= 1*((2|^a).sort_(1,1) + ((2|^a)*.sort.1,2)+...)
+ 3 * ((2|^a).sort_(2,1) + ((2|^a)*.sort.2,2)+...)
+ 5 *mu.5
+ ((id dom mu)(#)mu,7) +... by A2,A24
.= ((2|^alpha).1 + (2|^alpha,2)+...) * 1 +
((2|^beta).1 + (2|^beta,2)+...) * 3 +
((2|^gamma).1 + (2|^gamma,2)+...) * 5 +
((id dom mu)(#)mu,7)+... by A2,A26,A29;
end;
A30:n = mu.1 * 1 + mu.3 * 3 + mu.5 * 5 + ((id dom mu)(#)mu,7) +...
proof
for j holds (2|^a). sort_(j,1) = (2|^(a *(sort.j))).1 &
((2|^a)*.sort).j = 2|^(a *(sort.j))
proof
let j;
A31:(2|^a). sort_(j,1) = ((2|^a)*.sort)_(j,1) by FLEXARY1:42;
((2|^a)*.sort).j = (2|^a)*(sort.j) by FLEXARY1:41
.= 2|^(a*(sort.j)) by FLEXARY1:25;
hence thesis by A31;
end;
then A32:(2|^a). sort_(1,1) = (2|^alpha).1 &
(2|^a). sort_(2,1) = (2|^beta).1 &
(2|^a). sort_(3,1) = (2|^gamma).1 &
(2|^a)*.sort.1 = 2|^alpha &
(2|^a)*.sort.2 = 2|^beta &
(2|^a)*.sort.3 = 2|^gamma;
A33: (2|^a). sort_(1,1) + ((2|^a)*.sort.1,2)+... = mu.(2*1-1) by A2;
A34: (2|^a). sort_(2,1) + ((2|^a)*.sort.2,2)+... = mu.(2*2-1) by A2;
(2|^a). sort_(3,1) + ((2|^a)*.sort.3,2)+... = mu.(2*3-1) by A2;
hence thesis by A33,A34,A3,A32;
end;
consider h be odd-valued FinSequence such that
A35:h is non-decreasing &
for i holds card Coim(h,i) = mu.i by Lm3,A2;
A36:n = card Coim(h,1) * 1 + card Coim(h,3) * 3 +
card Coim(h,5) * 5 + ((id dom mu)(#)mu,7) +...
proof
A37: mu.1= card Coim(h,1) by A35;
mu.3 = card Coim(h,3) by A35;
hence thesis by A35,A37,A30;
end;
n = Sum h
proof
set I=idseq len mu;
A38: I=id dom mu by FINSEQ_1:def 3;
then (I(#)mu).3 = 3*mu.3 by Lm2;
then A39: (I(#)mu,3)+... = 3*mu.3+(I(#)mu,3+1)+... by FLEXARY1:20
.= 3* card Coim(h,3)+(I(#)mu,3+1)+... by A35;
A40:(I(#)mu).4 = 4*mu.4 & 4=2*2 by A38,Lm2;
then mu.4=0 by A2;
then A41: (I(#)mu,4)+... = 0+(I(#)mu,4+1)+... by A40,FLEXARY1:20;
(I(#)mu).5 = 5*mu.5 by A38,Lm2;
then A42: (I(#)mu,5)+... = 5*mu.5+(I(#)mu,5+1)+... by FLEXARY1:20
.= 5* card Coim(h,5)+(I(#)mu,5+1)+... by A35;
A43:(I(#)mu).6 = 6*mu.6 & 6=3*2 by A38,Lm2;
then mu.6=0 by A2;
then A44: (I(#)mu,6)+... = 0+(I(#)mu,6+1)+... by A43,FLEXARY1:20;
2*1=2;
then mu.2 = 0 by A2;
then 2 * mu.2 = 0;
hence Sum h = 1 * mu.1 + 0 + ((id dom mu)(#)mu,3)+... by Th9,A35
.= 1* card Coim(h,1) + ((id dom mu)(#)mu,3)+... by A35
.= n by A36,A39,A41,A38,A42,A44;
end;
then reconsider h as odd-valued a_partition of n by A35,Def3;
take h;
let j;
let O1 be odd-valued FinSequence,
a1 be natural-valued FinSequence
such that
A45:len O1 = len d = len a1 & d = O1 (#) 2|^a1;
let sort1 be DoubleReorganization of dom d such that
A46: (1 = O1.sort1_(1,1) & ... & 1 = O1.sort1_(1,len (sort1.1))) &
(3 = O1.sort1_(2,1) & ... & 3 = O1.sort1_(2,len (sort1.2))) &
(5 = O1.sort1_(3,1) & ... & 5 = O1.sort1_(3,len (sort1.3))) &
for i holds
2*i-1 = O1.sort1_(i,1) & ... & 2*i-1 = O1.sort1_(i,len (sort1.i));
for j st 1<= j & j <= len d holds O.j = O1.j & a.j=a1.j
proof
let j such that A48:1<=j & j<= len d;
A49: O1.j *((2|^a1).j) = (O1 (#) 2|^a1).j by VALUED_1:5
.= O.j * (2|^a).j by VALUED_1:5,A1,A45;
j in dom a by A48,FINSEQ_3:25,A1;
then A50: (2|^a).j = 2 to_power (a.j) by FLEXARY1:def 4
.= 2 |^ (a.j);
j in dom a1 by A48,FINSEQ_3:25,A45;
then A51: (2|^a1).j = 2 to_power (a1.j) by FLEXARY1:def 4
.= 2 |^ (a1.j);
j in dom O by A48,FINSEQ_3:25,A1;
then O.j is odd Nat by Def2;
then consider i1 be Nat such that
A52:O.j = 2*i1+1 by ABIAN:9;
j in dom O1 by A48,FINSEQ_3:25,A45;
then O1.j is odd Nat by Def2;
then ex i2 be Nat st O1.j = 2*i2+1 by ABIAN:9;
hence thesis by A50,A51,A52,A49,CARD_4:4;
end;
then A53:O=O1 & a=a1 by A45,A1;
A54:for j holds
card Coim(h,j*2-1) = (2|^a1). sort1_(j,1) +
((2|^a1)*.sort1.j,2)+...
proof
let j;
A55:(2|^a).sort_(j,1) = ((2|^a)*.sort)_(j,1) by FLEXARY1:42;
A56:len (2|^a)=len a by CARD_1:def 7;
then A57:dom O=dom d & dom d = dom a & dom (2|^a) = dom a
by A1,FINSEQ_3:29;
card Coim(h,j*2-1) = mu.(2*j-1)
proof
per cases;
suppose A58: j=0;
then A59:not (2*j-1) in dom mu;
not 2*j-1 in rng h by A58;
then h"{2*j-1}={} by FUNCT_1:72;
then Coim(h,j*2-1) = {} by RELAT_1:def 17;
hence thesis by A59,FUNCT_1:def 2;
end;
suppose j>0;
hence thesis by A35;
end;
end;
then A60: card Coim(h,j*2-1)
= ((2|^a)*.sort.j).1 + ((2|^a)*.sort.j,2)+... by A2,A55
.= Sum ((2|^a)*.sort.j) by FLEXARY1:22;
reconsider S=sort1 as DoubleReorganization of dom (2|^a)
by A56,A1,FINSEQ_3:29;
(2|^a1). sort1_(j,1) = ((2|^a1)*.sort1)_(j,1) by FLEXARY1:42;
then A61: (2|^a1). sort1_(j,1) + ((2|^a1)*.sort1.j,2)+...
= Sum ((2|^a)*.S.j) by A53,FLEXARY1:22;
A62:sort1 is odd_organization of O by A57,Th4,A46,A53;
thus card Coim(h,j*2-1) = Sum ((2|^a)*.sort).j by FLEXARY1:def 8,A60
.=Sum ((2|^a)*.S).j by A62,Th5
.= (2|^a1). sort1_(j,1) + ((2|^a1)*.sort1.j,2)+... by
FLEXARY1:def 8,A61;
end;
2*1-1=1 & 2*2-1 = 3 & 2*3-1 = 5;
hence thesis by A54;
end;
definition
let n be Nat;
let p be one-to-one a_partition of n;
func Euler_transformation p -> odd-valued a_partition of n means :Def5:
for O be odd-valued FinSequence,
a be natural-valued FinSequence
st
len O = len p = len a & p = O (#) 2|^a
for sort be DoubleReorganization of dom p
st
(1 = O.sort_(1,1) & ... & 1 = O.sort_(1,len (sort.1))) &
(3 = O.sort_(2,1) & ... & 3 = O.sort_(2,len (sort.2))) &
(5 = O.sort_(3,1) & ... & 5 = O.sort_(3,len (sort.3))) &
for i holds
2*i-1 = O.sort_(i,1) & ... & 2*i-1 = O.sort_(i,len (sort.i))
holds
card Coim(it,1) = (2|^a). sort_(1,1) + ((2|^a)*.sort.1,2)+... &
card Coim(it,3) = (2|^a). sort_(2,1) + ((2|^a)*.sort.2,2)+... &
card Coim(it,5) = (2|^a). sort_(3,1) + ((2|^a)*.sort.3,2)+... &
card Coim(it,j*2-1) = (2|^a). sort_(j,1) + ((2|^a)*.sort.j,2)+...;
existence by Th11;
uniqueness
proof
let E1,E2 be odd-valued a_partition of n such that
A1:for O be odd-valued FinSequence,
a be natural-valued FinSequence st
len O = len p = len a & p = O (#) 2|^a
for sort be DoubleReorganization of dom p st
(1 = O.sort_(1,1) & ... & 1 = O.sort_(1,len (sort.1))) &
(3 = O.sort_(2,1) & ... & 3 = O.sort_(2,len (sort.2))) &
(5 = O.sort_(3,1) & ... & 5 = O.sort_(3,len (sort.3))) &
for i holds
2*i-1 = O.sort_(i,1) & ... & 2*i-1 = O.sort_(i,len (sort.i))
holds
card Coim(E1,1) = (2|^a). sort_(1,1) + ((2|^a)*.sort.1,2)+... &
card Coim(E1,3) = (2|^a). sort_(2,1) + ((2|^a)*.sort.2,2)+... &
card Coim(E1,5) = (2|^a). sort_(3,1) + ((2|^a)*.sort.3,2)+... &
card Coim(E1,j*2-1) = (2|^a). sort_(j,1) + ((2|^a)*.sort.j,2)+...
and
A2:for O be odd-valued FinSequence,
a be natural-valued FinSequence st
len O = len p = len a & p = O (#) 2|^a
for sort be DoubleReorganization of dom p st
(1 = O.sort_(1,1) & ... & 1 = O.sort_(1,len (sort.1))) &
(3 = O.sort_(2,1) & ... & 3 = O.sort_(2,len (sort.2))) &
(5 = O.sort_(3,1) & ... & 5 = O.sort_(3,len (sort.3))) &
for i holds
2*i-1 = O.sort_(i,1) & ... & 2*i-1 = O.sort_(i,len (sort.i))
holds
card Coim(E2,1) = (2|^a). sort_(1,1) + ((2|^a)*.sort.1,2)+... &
card Coim(E2,3) = (2|^a). sort_(2,1) + ((2|^a)*.sort.2,2)+... &
card Coim(E2,5) = (2|^a). sort_(3,1) + ((2|^a)*.sort.3,2)+... &
card Coim(E2,j*2-1) = (2|^a). sort_(j,1) + ((2|^a)*.sort.j,2)+...;
consider O be odd-valued FinSequence,
a be natural-valued FinSequence such that
A3:len O = len p = len a & p = O (#) 2|^a and
p.1 = O.1 * (2|^a.1) & ... & p.len p = O.len p * (2|^a.len p) by Th6;
reconsider sort = the odd_organization of O as DoubleReorganization of dom p
by A3,FINSEQ_3:29;
A4: 2*1-1=1;
A5: 2*2-1=3;
2*3-1=5;
then A6: (1 = O.sort_(1,1) & ... & 1 = O.sort_(1,len (sort.1))) &
(3 = O.sort_(2,1) & ... & 3 = O.sort_(2,len (sort.2))) &
(5 = O.sort_(3,1) & ... & 5 = O.sort_(3,len (sort.3))) &
for i holds
2*i-1 = O.sort_(i,1) & ... & 2*i-1 = O.sort_(i,len (sort.i))
by A4,Def4,A5;
A7: for x be object holds card Coim(E1,x) = card Coim(E2,x)
proof
let x be object;
per cases;
suppose A8:not x in OddNAT;
rng E1 c= OddNAT & rng E2 c= OddNAT by Def1;
then E1"{x}={} & E2"{x}={} by A8,FUNCT_1:72;
then Coim(E1,x)={} & Coim(E2,x)={} by RELAT_1:def 17;
hence thesis;
end;
suppose x in OddNAT;
then consider i be Element of NAT such that
A9: x=2*i+1 by FIB_NUM2:def 4;
set i1=i+1;
card Coim(E1,i1*2-1) = (2|^a). sort_(i1,1) + ((2|^a)*.sort.i1,2)
+... by A1,A3,A6
.= card Coim(E2,i1*2-1) by A6,A3,A2;
hence thesis by A9;
end;
end;
thus E1=E2 by RFINSEQ2:19,A7,CLASSES1:def 10;
end;
end;
theorem Th12:
for n be Nat,
p be one-to-one a_partition of n,
e be odd-valued a_partition of n holds
e = Euler_transformation p iff
for O be odd-valued FinSequence,
a be natural-valued FinSequence,
sort be odd_organization of O
st
len O = len p = len a & p = O (#) 2|^a
for j holds card Coim(e,j*2-1) = ((2|^a)*.sort.j,1)+...
proof
let n be Nat,
p be one-to-one a_partition of n,
e be odd-valued a_partition of n;
thus e = Euler_transformation p implies
for O be odd-valued FinSequence,
a be natural-valued FinSequence,
sort be odd_organization of O
st
len O = len p = len a & p = O (#) 2|^a
for j holds
card Coim(e,j*2-1) = ((2|^a)*.sort.j,1)+...
proof
assume A1:e = Euler_transformation p;
let O be odd-valued FinSequence,
a be natural-valued FinSequence,
sort be odd_organization of O such that
A2:len O = len p = len a & p = O (#) 2|^a;
let j;
len (2|^a)=len a by CARD_1:def 7;
then A3:dom O=dom p & dom p = dom a & dom (2|^a) = dom a
by A2,FINSEQ_3:29;
reconsider S = sort as DoubleReorganization of dom p by A2, FINSEQ_3:29;
A4: 2*1-1=1;
A5: 2*2-1=3;
2*3-1=5;
then A6: (1 = O.S_(1,1) & ... & 1 = O.S_(1,len (S.1))) &
(3 = O.S_(2,1) & ... & 3 = O.S_(2,len (S.2))) &
(5 = O.S_(3,1) & ... & 5 = O.S_(3,len (S.3))) &
for i holds
2*i-1 = O.S_(i,1) & ... & 2*i-1 = O.S_(i,len (S.i)) by A4,Def4,A5;
(2|^a). sort_(j,1) = (2|^a)*.sort_(j,1) by FLEXARY1:42;
then card Coim(e,j*2-1)
= ((2|^a)*.sort).j.1 + ((2|^a)*.sort.j,1+1)+... by A6,A2,A1,Def5
.= ((2|^a)*.S.j,1)+... by FLEXARY1:20,A3;
hence thesis;
end;
assume A7:for O be odd-valued FinSequence,
a be natural-valued FinSequence,
sort be odd_organization of O st
len O = len p = len a & p = O (#) 2|^a
for j holds
card Coim(e,j*2-1) = ((2|^a)*.sort.j,1)+...;
for j
for O be odd-valued FinSequence,
a be natural-valued FinSequence st
len O = len p = len a & p = O (#) 2|^a
for sort be DoubleReorganization of dom p st
(1 = O.sort_(1,1) & ... & 1 = O.sort_(1,len (sort.1))) &
(3 = O.sort_(2,1) & ... & 3 = O.sort_(2,len (sort.2))) &
(5 = O.sort_(3,1) & ... & 5 = O.sort_(3,len (sort.3))) &
for i holds
2*i-1 = O.sort_(i,1) & ... & 2*i-1 = O.sort_(i,len (sort.i))
holds
card Coim(e,1)=(2|^a).sort_(1,1) + ((2|^a)*.sort.1,2)+...&
card Coim(e,3) = (2|^a).sort_(2,1) + ((2|^a)*.sort.2,2)+...&
card Coim(e,5) = (2|^a). sort_(3,1) + ((2|^a)*.sort.3,2)+...&
card Coim(e,j*2-1)
= (2|^a). sort_(j,1) + ((2|^a)*.sort.j,2)+...
proof
let j; let O be odd-valued FinSequence,
a be natural-valued FinSequence;
assume A8:len O = len p = len a & p = O (#) 2|^a;
let sort be DoubleReorganization of dom p;
assume
A9:(1 = O.sort_(1,1) & ... & 1 = O.sort_(1,len (sort.1))) &
(3 = O.sort_(2,1) & ... & 3 = O.sort_(2,len (sort.2))) &
(5 = O.sort_(3,1) & ... & 5 = O.sort_(3,len (sort.3))) &
for i holds
2*i-1 = O.sort_(i,1) & ... & 2*i-1 = O.sort_(i,len (sort.i));
A10:for j holds card Coim(e,j*2-1) = (2|^a). sort_(j,1) +
((2|^a)*.sort.j,2)+...
proof
let j;
len (2|^a)=len a by CARD_1:def 7;
then A11:dom O=dom p & dom p = dom a & dom (2|^a) = dom a
by A8,FINSEQ_3:29;
reconsider S = sort as DoubleReorganization of dom p;
A12: sort is odd_organization of O by A11,A9,Th4;
(2|^a). sort_(j,1) = (2|^a)*.sort_(j,1) by FLEXARY1:42; then
((2|^a)*.S.j,1)+...= (2|^a). sort_(j,1) + ((2|^a)*.sort.j,1+1)
+... by A11,FLEXARY1:20;
hence thesis by A12,A7,A8;
end;
1*2-1=1 & 2*2-1=3 & 3*2-1 = 5;
hence thesis by A10;
end;
hence thesis by Def5;
end;
registration
cluster one-to-one non-decreasing -> increasing for real-valued Function;
coherence
proof
let f be real-valued Function;
assume A1:f is one-to-one non-decreasing;
for e1,e2 be ExtReal st e1 in dom f & e2 in dom f & e1 < e2 holds
f.e1 < f.e2
proof
let e1,e2 be ExtReal such that A2:e1 in dom f & e2 in dom f & e1 < e2;
f.e1 <= f.e2 by A1,A2,VALUED_0:def 15;
hence thesis by XXREAL_0:1,A2,A1;
end;
hence thesis by VALUED_0:def 13;
end;
end;
theorem Th13:
for O be odd-valued FinSequence,
a be natural-valued FinSequence,
s be odd_organization of O st
len O = len a & O (#) 2|^a is one-to-one
holds a*.s.i is one-to-one
proof
let O be odd-valued FinSequence,
a be natural-valued FinSequence,
s be odd_organization of O;
set p=O (#) (2|^a);
assume A1:len O = len a & p is one-to-one;
then reconsider S=s as DoubleReorganization of dom a by FINSEQ_3:29;
A2:(a*.S).i = a*(S.i) by FLEXARY1:41;
thus (a*.s).i is one-to-one
proof
assume not (a*.s).i is one-to-one;
then consider x1,x2 be object such that
A3: x1 in dom ((a*.S).i)& x2 in dom ((a*.S).i)&
(a*.S).i.x1=(a*.S).i.x2 & x1<>x2;
reconsider x1,x2 as Nat by A3;
set s1=s_(i,x1),s2=s_(i,x2);
A4:x1 in dom (s.i) & s1 in dom a & a.s1 = (a*.S).i.x1
by A2,A3,FUNCT_1:11,12;
A5:x2 in dom (S.i) & s2 in dom a & a.s2 = (a*.S).i.x2
by A2,A3,FUNCT_1:11,12;
A6:2*i-1 = O.s_(i,1) & ... & 2*i-1 = O.s_(i,len (s.i)) by Def4;
1<= x1 & x1 <= len (s.i) by A4,FINSEQ_3:25;
then A7: 2*i-1 = O.s1 by A6;
1<= x2 & x2 <= len (s.i) by A5,FINSEQ_3:25;
then A8: 2*i-1 = O.s2 by A6;
O is (len O)-element by CARD_1:def 7;
then A9:len p = len a by A1,CARD_1:def 7;
A10:1<= s.i.x1 & s.i.x1 <= len a by A4,FINSEQ_3:25;
1<= s.i.x2 & s.i.x2 <= len a by A5,FINSEQ_3:25;
then A11:s2 in dom p & s1 in dom p by A9,A10,FINSEQ_3:25;
A12:p.s1 = (O.s1) * ((2|^a).s1) by VALUED_1:5;
A13:(2|^a).s1 = 2 to_power (a.s1) by A4,FLEXARY1:def 4;
p.s2 = (O.s2) * ((2|^a).s2) by VALUED_1:5;
then p.s2 = p.s1 by A5,FLEXARY1:def 4,A13,A12,A7,A8,A4,A3;
then s2 = s1 by A11,A1;
hence thesis by A4,A5,FUNCT_1:def 4,A3;
end;
end;
Lm4:
for p1,p2 be one-to-one a_partition of n st
Euler_transformation p1 = Euler_transformation p2
holds rng p1 c= rng p2
proof
let p1,p2 be one-to-one a_partition of n;
assume A1:Euler_transformation p1 = Euler_transformation p2;
consider O1 be odd-valued FinSequence,
a1 be natural-valued FinSequence such that
A2: len O1 = len p1 = len a1 & p1 = O1 (#) 2|^a1 and
A3: p1.1 = O1.1 * (2|^a1.1) & ... &
p1.len p1 = O1.len p1 * (2|^a1.len p1) by Th6;
set s1= the odd_organization of O1;
reconsider S1=s1 as DoubleReorganization of dom a1 by FINSEQ_3:29,A2;
consider O2 be odd-valued FinSequence,
a2 be natural-valued FinSequence such that
A4: len O2 = len p2 = len a2 & p2 = O2 (#) 2|^a2 and
A5: p2.1 = O2.1 * (2|^a2.1) & ... &
p2.len p2 = O2.len p2 * (2|^a2.len p2) by Th6;
set s2= the odd_organization of O2;
reconsider S2=s2 as DoubleReorganization of dom a2 by FINSEQ_3:29,A4;
A6: for j holds rng (a1*.s1.j) = rng (a2*.s2.j)
proof
let j;
A7:card Coim(Euler_transformation p1,j*2-1)
= ((2|^a1)*.s1.j,1)+... by A2,Th12
.= ((2|^a1)*(s1.j),1)+... by FLEXARY1:41
.= (2|^(a1*(s1.j)),1)+... by FLEXARY1:25
.= (2|^(a1*(S1.j))).1+ (2|^(a1*(S1.j)),1+1)+... by FLEXARY1:20;
A8:(a2*.S2).j = a2*(S2.j) by FLEXARY1:41;
then A9: a2*(S2.j) is one-to-one natural-valued by A4,Th13;
(a1*.S1).j = a1*(S1.j) by FLEXARY1:41;
then A10:a1*(S1.j) is one-to-one natural-valued by A2,Th13;
card Coim(Euler_transformation p2,j*2-1)
= ((2|^a2)*.s2.j,1)+... by A4,Th12
.= ((2|^a2)*(s2.j),1)+... by FLEXARY1:41
.= (2|^(a2*(s2.j)),1)+... by FLEXARY1:25
.= (2|^(a2*(S2.j))).1+ (2|^(a2*(S2.j)),1+1)+... by FLEXARY1:20;
then rng (a2*(S2.j)) = rng(a1*(S1.j))
by A7,A1,FLEXARY1:30,A9,A10;
hence thesis by A8,FLEXARY1:41;
end;
let y be object;
assume y in rng p1;
then consider x be object such that
A11:x in dom p1 & p1.x=y by FUNCT_1:def 3;
reconsider x as Nat by A11;
1 <= x & x <= len p1 by A11,FINSEQ_3:25;
then A12:p1.x = O1.x * (2|^a1.x) by A3;
dom p1 = dom O1 by A2,FINSEQ_3:29;
then x in Values s1 by FLEXARY1:def 7,A11;
then consider i,j be object such that
A13: i in dom s1 & j in dom (s1.i) & x = s1.i.j by FLEXARY1:1;
reconsider i,j as Nat by A13;
len ((a1*.S1).i) = len (S1.i) by CARD_1:def 7;
then A14: dom ((a1*.S1).i) = dom (S1.i) by FINSEQ_3:29;
then ((a1*.S1).i).j in rng (a1*.s1.i) by A13,FUNCT_1:def 3;
then ((a1*.S1).i).j in rng (a2*.s2.i) by A6;
then consider z be object such that
A15:z in dom (a2*.S2.i) & (a2*.S2.i).z = ((a1*.S1).i).j by FUNCT_1:def 3;
reconsider z as Nat by A15;
set Z=S2.i.z;
A16:(a1*.S1).i = a1 * (S1.i) by FLEXARY1:41;
A17:(a2*.S2.i) = a2* (S2.i) by FLEXARY1:41;
A18:len ((a2*.S2).i) = len (S2.i) by CARD_1:def 7;
A19:(a2*.S2.i).z = a2.Z & Z in dom a2 by A17,A15,FUNCT_1:11,12;
then A20: Z in dom p2 by FINSEQ_3:29,A4;
1<= Z & Z <= len p2 by A19,A4,FINSEQ_3:25;
then A21:p2.Z = O2.Z * (2|^a2.Z) by A5;
A22:p2.Z in rng p2 by A20,FUNCT_1:def 3;
A23:1<= j & j <= len (s1.i) by A13,FINSEQ_3:25;
2*i-1 = O1.s1_(i,1) & ... & 2*i-1 = O1.s1_(i,len (s1.i)) by Def4;
then A24:O1.s1_(i,j) = 2*i-1 by A23;
A25:1<= z & z <= len (s2.i) by FINSEQ_3:25, A18,A15;
2*i-1 = O2.s2_(i,1) & ... & 2*i-1 = O2.s2_(i,len (s2.i)) by Def4;
then O2.s2_(i,z) = 2*i-1 by A25;
hence thesis by A24,A13,A22,A21,A15,A16,A14,FUNCT_1:12,A19,A12,A11;
end;
theorem Th14:
for p1,p2 be one-to-one a_partition of n st
Euler_transformation p1 = Euler_transformation p2
holds p1 = p2
proof
let p1,p2 be one-to-one a_partition of n;
assume
Euler_transformation p1 = Euler_transformation p2;
then A1:rng p1 = rng p2 by Lm4;
then p1 is FinSequence of REAL & p2 is FinSequence of REAL
by FINSEQ_1:def 4;
hence thesis by INTEGRA3:6,A1;
end;
theorem Th15:
for e be odd-valued a_partition of n
ex p be one-to-one a_partition of n st
e = Euler_transformation p
proof
let e be odd-valued a_partition of n;
A1:Sum e=n by Def3;
deffunc h(object) = card Coim(e,$1);
consider H be FinSequence such that
A2:len H=n & for k st k in dom H holds H.k=h(k) from FINSEQ_1:sch 2;
rng H c= NAT
proof
let y be object;
assume y in rng H;
then consider x be object such that
A3:x in dom H & H.x=y by FUNCT_1:def 3;
reconsider x as Nat by A3;
H.x = card Coim(e,x) by A3,A2;
hence thesis by A3;
end;
then reconsider H as natural-valued FinSequence by VALUED_0:def 6;
A4:dom H = Seg len H by FINSEQ_1:def 3;
A5:Sum e = Sum ((idseq n) (#)H)
proof
A6:for i st i in dom e holds 0 <= e.i;
for i holds card Coim(e,i) = H.i
proof
let i;
per cases by FINSEQ_3:25;
suppose i in dom H;
hence thesis by A2;
end;
suppose i < 1;
then A8: not i in rng e & not i in dom H by NAT_1:14,FINSEQ_3:25;
then H.i = 0 & e"{i}={} by FUNCT_1:def 2,72;
then Coim(e,i)={} by RELAT_1:def 17;
hence thesis by A8,FUNCT_1:def 2;
end;
suppose A9: i > len H;
then A10: not i in dom H by FINSEQ_3:25;
Coim(e,i)={}
proof
assume Coim(e,i)<>{};
then e"{i}<>{} by RELAT_1:def 17;
then i in rng e by FUNCT_1:72;
then consider x be object such that
A11: x in dom e & e.x=i by FUNCT_1:def 3;
reconsider x as Nat by A11;
i <= Sum e by A11,A6,MATRPROB:5;
hence thesis by Def3,A9,A2;
end;
hence thesis by A10,FUNCT_1:def 2;
end;
end;
hence Sum e = 1 * H.1 + 2 * H.2 + ((id dom H)(#)H,3) +... by Th9
.=1 * H.1 + ((id dom H) (#)H).2+ ((id dom H)(#)H,3) +... by Lm2
.=((id dom H)(#)H).1+((id dom H)(#)H).2+((id dom H)(#)H,3)+...
by Lm2
.=((id dom H)(#)H).1+(((id dom H)(#)H).2+
((id dom H)(#)H,2+1)+...)
.=((id dom H)(#)H).1+((id dom H)(#)H,2) +... by FLEXARY1:20
.=Sum ((idseq n) (#)H) by A4,A2,FLEXARY1:22;
end;
defpred F[Nat,object] means
ex f be increasing natural-valued FinSequence st
H.$1 = (2|^f).1+(2|^f,2)+... & $2 = $1*(2|^f);
ex p be FinSequence of NAT* st
dom p = Seg len H &
for k st k in Seg len H holds F[k,p.k]
proof
A12:for k st k in Seg len H ex x be object st F[k,x]
proof
let k;
assume k in Seg len H;
consider f be increasing natural-valued FinSequence such that
A13: H.k = (2|^f).1+(2|^f,2)+... by FLEXARY1:31;
take G=k * (2|^f);
thus thesis by A13;
end;
consider p be FinSequence such that
A14:dom p = Seg len H &
for k st k in Seg len H holds F[k,p.k] from FINSEQ_1:sch 1(A12);
rng p c= NAT*
proof
let y be object;
assume y in rng p;
then consider x be object such that
A15:x in dom p & p.x=y by FUNCT_1:def 3;
reconsider x as Nat by A15;
consider f be increasing natural-valued FinSequence such that
A16:H.x = (2|^f).1+(2|^f,2)+... &
p.x = x*(2|^f) by A15,A14;
rng (x*(2|^f)) c= NAT by VALUED_0:def 6;
then x*(2|^f) is FinSequence of NAT by FINSEQ_1:def 4;
hence thesis by FINSEQ_1:def 11,A15,A16;
end;
then p is FinSequence of NAT* by FINSEQ_1:def 4;
hence thesis by A14;
end;
then consider p be FinSequence of NAT* such that
A17: dom p = Seg len H & for k st k in Seg len H holds F[k,p.k];
A18:for k st p.k<>{} holds k is odd
proof
let k;
assume A19: p.k<>{};
then A20:k in dom p by FUNCT_1:def 2;
then consider f be increasing natural-valued FinSequence such that
A21:H.k = (2|^f).1+(2|^f,2)+... &
p.k = k*(2|^f) by A17;
consider j be object such that
A22:j in dom (p.k) by A19,XBOOLE_0:def 1;
reconsider j as Nat by A22;
A23:dom (p.k) = dom (2|^f) by A21,VALUED_1:def 5;
then j in dom f by A22,FLEXARY1:def 4;
then (2|^f).j = 2 to_power (f.j) by FLEXARY1: def 4
.= 2|^ (f.j);
then A24:(2|^f).j >0 by NEWTON:83;
for i st i in dom (2|^f) holds 0 <= (2|^f).i;
then A25:Sum (2|^f) >0 by A22,A24,A23,RVSUM_1:85;
A26:rng e c= OddNAT by Def1;
H.k = card Coim(e,k) by A20,A4,A17,A2;
then Coim(e,k) <> {} by FLEXARY1:22,A25,A21;
then e"{k} <>{} by RELAT_1:def 17;
then k in OddNAT by FUNCT_1:72,A26;
hence thesis by Th2;
end;
A27:H is n-element complex-valued by A2,CARD_1:def 7;
len p = n by A17,A2,FINSEQ_1:def 3;
then A28:len (Sum p)=n by CARD_1:def 7;
now let i;
assume 1 <= i & i <= n;
then i in Seg len H by A2;
then consider f be increasing natural-valued FinSequence such that
A29:H.i = (2|^f).1+(2|^f,2)+... &
p.i = i*(2|^f) by A17;
thus (Sum p).i = Sum (i*(2|^f)) by A29,FLEXARY1:def 8
.= i*Sum (2|^f) by RVSUM_1:87
.= i*H.i by A29,FLEXARY1:22
.= ((idseq n) (#)H).i by A4,A2,Lm2;
end;
then A30:Sum p = ((idseq n) (#)H) by CARD_1:def 7,A27,A28;
set NC=NAT-concatenation,np=NC "**" p;
NAT* c= COMPLEX* by NUMBERS:20,FINSEQ_1:62;
then reconsider p1=p as FinSequence of COMPLEX* by FINSEQ_2:24;
rng np c=REAL;
then reconsider np as FinSequence of REAL by FINSEQ_1:def 4;
set sp=sort_a np;
Sum (COMPLEX-concatenation "**" p1) = Sum np by FLEXARY1:5;
then A31:Sum np =n by FLEXARY1:48,A30,A5,A1;
A32:Sum sp=n by RFINSEQ2:def 6,RFINSEQ:9,A31;
A33:rng sp = rng np by RFINSEQ2:def 6,CLASSES1:75;
A34:rng np = Values p by FLEXARY1:4;
sp is one-to-one a_partition of n
proof
not 0 in rng sp
proof
assume 0 in rng sp;
then consider x,y be object such that
A35: x in dom p & y in dom (p.x) & 0=p.x.y by A33,A34,FLEXARY1:1;
reconsider x,y as Nat by A35;
consider f be increasing natural-valued FinSequence such that
A36:H.x = (2|^f).1+(2|^f,2)+... & p.x = x*(2|^f) by A35,A17;
A37: 1 <= x by A35,FINSEQ_3:25;
A38: (x*(2|^f)).y = x* ((2|^f).y) by RVSUM_1:45;
y in dom (2|^f) by A35, A36,VALUED_1:def 5;
then y in dom f by FLEXARY1:def 4;
then (2|^f).y = 2 to_power (f.y) by FLEXARY1:def 4
.= 2|^ (f.y);
then (2|^f).y >0 by NEWTON:83;
hence thesis by A35,A36,A37,A38;
end;
then A39:sp is non-zero by ORDINAL1:def 15;
A40:Sum sp=n by RFINSEQ2:def 6,RFINSEQ:9,A31;
A41:sp is natural-valued by A34,A33,VALUED_0:def 6;
sp is one-to-one
proof
now
let x1,x2 be set such that A42:x1 in dom sp & x2 in dom sp
& sp.x1=sp.x2;
sp.x1 in {sp.x1} by TARSKI:def 1;
then A43:x1 in sp"{sp.x1} & x2 in sp"{sp.x1} by FUNCT_1:def 7,A42;
assume x1<>x2;
then not sp"{sp.x1} is trivial by A43,SUBSET_1:def 7;
then A44: card (sp"{sp.x1}) >= 2 by NAT_D:60;
card Coim(sp,sp.x1) = card Coim(np,sp.x1)
by CLASSES1:def 10,RFINSEQ2:def 6;
then card Coim(np,sp.x1) >= 2 by A44,RELAT_1:def 17;
then A45:card (np"{sp.x1}) >= 2 by RELAT_1:def 17;
then not np"{sp.x1} is trivial by NAT_D:60;
then consider d1,d2 be Element of np"{sp.x1} such that
A46: d1<>d2 by SUBSET_1:def 7;
np"{sp.x1} is non empty by A45;
then A47:d1 in dom np & np.d1 in {sp.x1} & d2 in dom np &
np.d2 in {sp.x1} by FUNCT_1:def 7;
then A48:np.d1=sp.x1 & np.d2=sp.x1 by TARSKI:def 1;
consider n1,k1 be Nat such that
A49:n1+1 in dom p & k1 in dom (p.(n1+1)) &
d1 = k1 + len (NC "**" (p|n1)) by FLEXARY1:6,A47;
set n2=n1+1;
A50: np.d1 = p.n2.k1 by FLEXARY1:8,A49;
consider f be increasing natural-valued FinSequence such that
A51:H.n2 = (2|^f).1+(2|^f,2)+... &
p.n2 = n2*(2|^f) by A49,A17;
A52: p.n2.k1 = n2* ((2|^f).k1) by A51,RVSUM_1:45;
k1 in dom (2|^f) by A49, A51,VALUED_1:def 5;
then A53:k1 in dom f by FLEXARY1:def 4;
then A54:(2|^f).k1 = 2 to_power (f.k1) by FLEXARY1:def 4
.= 2|^ (f.k1);
consider n3,k3 be Nat such that
A55:n3+1 in dom p & k3 in dom (p.(n3+1)) &
d2 = k3 + len (NC "**" (p|n3)) by FLEXARY1:6,A47;
set n4=n3+1;
consider g be increasing natural-valued FinSequence such that
A56:H.n4 = (2|^g).1+(2|^g,2)+... &
p.n4 = n4*(2|^g) by A55,A17;
k3 in dom (2|^g) by A55, A56,VALUED_1:def 5;
then A57:k3 in dom g by FLEXARY1:def 4;
then A58:(2|^g).k3 = 2 to_power (g.k3) by FLEXARY1:def 4
.= 2|^ (g.k3);
A59: p.n4 <>{} & p.n2 <>{} by A55,A49;
then consider c2 be Nat such that
A60:n2=2*c2+1 by A18,ABIAN:9;
consider c4 be Nat such that
A61:n4=2*c4+1 by A59,A18,ABIAN:9;
p.n2.k1 = p.n4.k3 by A48,A50,FLEXARY1:8,A55;
then A62: n2 * (2|^ (f.k1)) = n4 * 2|^ (g.k3) by A56,RVSUM_1:45,
A58,A52,A54;
then A63:c2=c4 & f.k1 = g.k3 by A60,A61,CARD_4:4;
n4=n2 by A62,A60,A61,CARD_4:4;
then A64:f=g by A51,A56,FLEXARY1:27;
f is one-to-one;
hence thesis by A57,A53,A64,A63,A49,A55,A60,A61,A46;
end;
hence thesis;
end;
hence thesis by Def3,A39,A41,A40;
end;
then reconsider sp as one-to-one a_partition of n;
take sp;
for O be odd-valued FinSequence,
a be natural-valued FinSequence,
sort be odd_organization of O st
len O = len sp = len a & sp = O (#) 2|^a
for j holds card Coim(e,j*2-1) = ((2|^a)*.sort.j,1)+...
proof
let O be odd-valued FinSequence,
a be natural-valued FinSequence,
sort be odd_organization of O such that
A65: len O = len sp = len a & sp = O (#) 2|^a;
let j;
A66:dom a= dom sp = dom O & dom a = dom (2|^a)
by FLEXARY1:def 4,FINSEQ_3:29,A65;
then reconsider S=sort as DoubleReorganization of dom (2|^a);
A67: 2*j-1 = O.sort_(j,1) & ...& 2*j-1 = O.sort_(j,len (sort.j)) by Def4;
per cases;
suppose A68: j < 1;
then j = 0 by NAT_1:14;
then not 2*j-1 in rng e;
then e"{2*j-1} ={} by FUNCT_1:72;
then A69:Coim(e,2*j-1)={} by RELAT_1:def 17;
not j in dom ((2|^a)*.S) by FINSEQ_3:25, A68;
then Sum ((2|^a)*.S.j) = 0 by FUNCT_1:def 2,RVSUM_1:72;
hence card Coim(e,j*2-1) = ((2|^a)*.sort.j,1)+... by FLEXARY1:21,A69;
end;
suppose A70: j*2-1 > n;
A71:Coim(e,j*2-1)={}
proof
assume Coim(e,j*2-1)<>{};
then e"{j*2-1} <>0 by RELAT_1:def 17;
then 2*j-1 in rng e by FUNCT_1:72;
then consider w be object such that
A72:w in dom e & e.w=2*j-1 by FUNCT_1:def 3;
for i st i in dom e holds 0 <= e.i;
hence thesis by A72,MATRPROB:5,A1,A70;
end;
(2|^a)*.S.j ={}
proof
set L=len (S.j),SjL=S.j.L;
assume A74: (2|^a)*.S.j<>{};
len ((2|^a)*.S.j) = L by CARD_1:def 7;
then A75: L >=1 by A74,NAT_1:14;
then A76:2*j-1 = O.sort_(j,L) by A67;
S.j<>{} by A74;
then A77:j in dom S by FUNCT_1:def 2;
L in dom (S.j) by A75,FINSEQ_3:25;
then A78: SjL in Values S by FLEXARY1:1,A77;
then A79:SjL in dom O by FLEXARY1:def 7;
then A80:sp.SjL = O.SjL * (2|^a).SjL by VALUED_1:def 4,A66,A65;
A81: (2|^a).SjL = 2 to_power (a.SjL) by FLEXARY1:def 4,A66,A79;
A82:for i st i in dom sp holds 0 <= sp.i;
2 |^ (a.SjL)>0 by NEWTON:83;
then 2 |^ (a.SjL) >=1 by NAT_1:14;
then A83: sp.SjL >= 1*(2*j-1) by A76,A80, A81,XREAL_1:66;
SjL in dom sp by A78,FLEXARY1:def 7,A66;
then sp.SjL <= n by A82,MATRPROB:5,A32;
hence thesis by A83,A70,XXREAL_0:2;
end;
hence card Coim(e,j*2-1) = ((2|^a)*.sort.j,1)+...
by RVSUM_1:72,FLEXARY1:21,A71;
end;
suppose A84:j >=1 & j*2-1 <=n;
set J=j*2-1;
2*j >= 2*1 by A84,XREAL_1:64;
then A85:J >= 2-1 by XREAL_1:9;
then consider f be increasing natural-valued FinSequence such that
A86: H.J = (2|^f).1+(2|^f,2)+... &
p.J = J*(2|^f) by A84,FINSEQ_3:25,A2,A17,A4;
reconsider j1=j-1 as Nat by A84;
A87:J=2*j1+1;
for x be object holds card Coim((2|^a)*.sort.j,x) = card Coim(2|^f,x)
proof
let y be object;
set AS=(2|^a)*.sort.j;
A90:(2|^a)*.S.j = (2|^a)*(S.j) by FLEXARY1:41;
A91:a*.sort.j is one-to-one by Th13,A65;
A92:y in rng AS implies y in rng (2|^f)
proof
assume y in rng AS;
then consider x be object such that
A93:x in dom ((2|^a)*.S.j) & ((2|^a)*.S.j).x=y by FUNCT_1:def 3;
reconsider x as Nat by A93;
set Sjx=S.j.x;
A94:x in dom (S.j) & Sjx in dom (2|^a) by A90,A93,FUNCT_1:11;
then A95: 1<= x & x <= len (S.j) by FINSEQ_3:25;
J = O.sort_(j,1) &...& J=O.sort_(j,len (sort.j)) by Def4;
then A96: J = O.sort_(j,x) by A95;
Sjx in dom a by A94,FLEXARY1:def 4;
then A97:(2|^a).Sjx = 2 to_power (a.Sjx) by FLEXARY1:def 4;
sp.Sjx in Values p by A66,A94,FUNCT_1:def 3,A33,A34;
then consider u,w be object such that
A98:u in dom p & w in dom (p.u) & sp.Sjx=p.u.w by FLEXARY1:1;
reconsider u,w as Nat by A98;
p.u <>{} by A98;
then consider s be Nat such that
A99:u=2*s+1 by A18,ABIAN:9;
consider fu be increasing natural-valued FinSequence such that
A100:H.u = (2|^fu).1+(2|^fu,2)+... &
p.u = u*(2|^fu) by A17,A98;
A101: p.u.w = u*(2|^fu).w by A100,RVSUM_1:45;
w in dom (2|^fu) by A100,A98,VALUED_1:def 5;
then w in dom fu by FLEXARY1:def 4;
then A102: (2|^fu).w = 2 to_power (fu.w) by FLEXARY1: def 4;
then A103: J*(2 |^ (a.Sjx)) = (2*s+1)*(2|^(fu.w))
by A98,A101,A99,A65,VALUED_1:5,A97, A96;
then A104: j1=s & a.Sjx = fu.w by CARD_4:4,A87;
A105: u*(2|^fu) = J*(2|^f) by A103,CARD_4:4,A87,A100,A86,A99;
then A106:w in dom (2|^f) by A98,A100,VALUED_1:def 5;
u*((2|^fu).w) = J*((2|^f).w) by A105,A100,A101,RVSUM_1:45;
then A107:(2|^fu).w = (2|^f).w by A104,A99,XCMPLX_1:5;
y = (2|^fu).w by A102,A104, A90,A93,FUNCT_1:12,A97;
hence thesis by A106,A107,FUNCT_1:def 3;
end;
A108: y in rng (2|^f) implies y in rng AS
proof
assume y in rng (2|^f);
then consider x be object such that
A109: x in dom (2|^f) & (2|^f).x=y by FUNCT_1:def 3;
reconsider x as Nat by A109;
x in dom f by A109,FLEXARY1:def 4;
then A110:(2|^f).x = 2 to_power (f.x) by FLEXARY1:def 4;
A111:x in dom (p.J) by A86,A109,VALUED_1:def 5;
set pJx=p.J.x;
J in dom p by A85,A84,A2,A17;
then pJx in rng sp by FLEXARY1:1,A111,A33,A34;
then consider w be object such that
A112: w in dom sp & sp.w = pJx by FUNCT_1:def 3;
reconsider w as Nat by A112;
A113:sp.w = O.w * (2|^a).w by A65,VALUED_1:5;
Values sort = dom O by FLEXARY1:def 7;
then consider r,t be object such that
A114: r in dom S & t in dom (S.r) & S.r.t = w by FLEXARY1:1,A112,A66;
reconsider r,t as Nat by A114;
1 <= r by A114,FINSEQ_3:25;
then reconsider r1=r-1 as Nat;
set R=2*r-1;
A115:R= O.sort_(r,1) &...& R=O.sort_(r,len (sort.r)) by Def4;
1<= t & t <= len (S.r) by A114,FINSEQ_3:25;
then A116: R=O.sort_(r,t) by A115;
A117:(2|^a).w = 2 to_power (a.w) by A112,A66,FLEXARY1:def 4;
then J*(2|^(f.x)) = (2*r1+1)*(2|^(a.w))
by A110,A113,A86,RVSUM_1:45,A112, A116,A114;
then A118: j1=r1 & f.x = a.w by CARD_4:4,A87;
then A119: t in dom ((2|^a)*(S.j)) by A112,A66,A114,FUNCT_1:11;
then ((2|^a)*(S.j)).t = (2|^f).x
by A114,A118,FUNCT_1:12,A110,A117;
hence thesis by A109,A119,A90,FUNCT_1:def 3;
end;
per cases;
suppose A120: Coim(AS,y)={};
Coim(2|^f,y)={}
proof
assume Coim(2|^f,y)<>{};
then (2|^f)"{y}<>{} by RELAT_1:def 17;
then AS"{y}<>{} by FUNCT_1:72,A108;
hence thesis by RELAT_1:def 17,A120;
end;
hence thesis by A120;
end;
suppose Coim(AS,y)<>{};
then A121: AS"{y}<>{} by RELAT_1:def 17;
then A122:y in rng AS by FUNCT_1:72;
A123:2+0=2;
(2|^a)*.S.j = 2|^(a*(S.j)) by FLEXARY1:25,A90
.= 2|^(a*.S.j) by FLEXARY1:41;
then ex x st AS"{y}={x} by A91,A123,A122,FUNCT_1:74;
then A124:card Coim (AS,y) = 1 by CARD_2:42,RELAT_1:def 17;
ex x st (2|^f)"{y}={x} by A121,FUNCT_1:72,A92,A123,FUNCT_1:74;
hence thesis by CARD_2:42,A124,RELAT_1:def 17;
end;
end;
then Sum ((2|^a)*.S.j) = Sum (2|^f) by CLASSES1:def 10,RFINSEQ:9
.= (2|^f).1+(2|^f,2)+... by FLEXARY1:22
.= card Coim(e,J)
by A85,A84,FINSEQ_3:25,A2,A86;
hence thesis by FLEXARY1:21;
end;
end;
hence thesis by Th12;
end;
begin :: Main Theorem
::$N Euler's partition theorem
::$L https://en.wikipedia.org/wiki/Partition_(number_theory) Euler's partition theorem
theorem
card the set of all p where p is odd-valued a_partition of n
=
card the set of all p where p is one-to-one a_partition of n
proof
set OddVall = the set of all p where p is odd-valued a_partition of n;
set OneToOne = the set of all p where p is one-to-one a_partition of n;
A1:the odd-valued a_partition of n in OddVall;
ex E be Function of OneToOne, OddVall st
for p be one-to-one a_partition of n holds E.p = Euler_transformation p
proof
defpred P[object,object] means
for p be one-to-one a_partition of n st p=$1 holds
$2=Euler_transformation p;
A2:for x be object st x in OneToOne ex y be object st y in OddVall & P[x,y]
proof
let x be object;
assume x in OneToOne;
then ex q be one-to-one a_partition of n st x=q & not contradiction;
then reconsider x as one-to-one a_partition of n;
take Euler_transformation x;
thus thesis;
end;
consider f be Function of OneToOne, OddVall such that
A3: for x be object st x in OneToOne holds P[x,f.x]
from FUNCT_2:sch 1(A2);
take f;
let p be one-to-one a_partition of n;
p in OneToOne;
hence thesis by A3;
end;
then consider E be Function of OneToOne, OddVall such that
A4:for p be one-to-one a_partition of n
holds E.p=Euler_transformation p;
A5:dom E = OneToOne by A1,FUNCT_2:def 1;
OddVall c= rng E
proof
let p be object;
assume p in OddVall;
then ex o be odd-valued a_partition of n st o=p & not contradiction;
then reconsider p as odd-valued a_partition of n;
consider q be one-to-one a_partition of n such that
A6: p = Euler_transformation q by Th15;
q in dom E & p=E.q by A6, A4,A5;
hence thesis by FUNCT_1:def 3;
end;
then A7: rng E = OddVall;
E is one-to-one
proof
let p1,p2 be object;
assume A8:p1 in dom E & p2 in dom E & E.p1=E.p2;
then
(ex o be one-to-one a_partition of n st o=p1 & not contradiction) &
ex o be one-to-one a_partition of n st o=p2 & not contradiction by A5;
then reconsider p1,p2 as one-to-one a_partition of n;
E.p1 = Euler_transformation p1 & E.p2 = Euler_transformation p2 by A4;
hence thesis by Th14,A8;
end;
hence thesis by A5,A7,CARD_1:70;
end;