:: {E}uler's {P}artition {T}heorem
:: by Karol P\kak
::
:: Received March 26, 2015
:: Copyright (c) 2015-2016 Association of Mizar Users

environ

vocabularies HIDDEN, 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 HIDDEN, 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;
definitions TARSKI, FUNCT_1, FLEXARY1;
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;
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;
constructors HIDDEN, XXREAL_2, ABIAN, RFINSEQ2, CLASSES1, MONOID_0, NAT_D, FOMODEL2, RELSET_1, FIB_NUM2, FINSOP_1, NEWTON, POWER, JORDAN1H, FLEXARY1;
requirements HIDDEN, NUMERALS, SUBSET, BOOLE, ARITHM, REAL;
equalities FINSEQ_1, FINSEQ_2, XCMPLX_0, FLEXARY1;
expansions FINSEQ_1, TARSKI, XBOOLE_0, FUNCT_1;


registration
let r be ext-real number ;
cluster <*r*> -> ext-real-valued ;
coherence
<*r*> is ext-real-valued
proof end;
cluster <*r*> -> increasing decreasing non-decreasing non-increasing ;
coherence
( <*r*> is decreasing & <*r*> is increasing & <*r*> is non-decreasing & <*r*> is non-increasing )
;
end;

theorem Th1: :: EULRPART:1
for f, g being ext-real-valued non-decreasing FinSequence st f . (len f) <= g . 1 holds
f ^ g is non-decreasing
proof end;

definition
let R be Relation;
attr R is odd-valued means :Def1: :: EULRPART:def 1
rng R c= OddNAT ;
end;

:: deftheorem Def1 defines odd-valued EULRPART:def 1 :
for R being Relation holds
( R is odd-valued iff rng R c= OddNAT );

theorem Th2: :: EULRPART:2
for n being Nat holds
( n in OddNAT iff n is odd )
proof end;

registration
cluster Relation-like odd-valued -> non-zero natural-valued for set ;
coherence
for b1 being Relation st b1 is odd-valued holds
( b1 is non-zero & b1 is natural-valued )
proof end;
end;

definition
let F be Function;
redefine attr F is odd-valued means :Def2: :: EULRPART:def 2
for x being object st x in dom F holds
F . x is odd Nat;
compatibility
( F is odd-valued iff for x being object st x in dom F holds
F . x is odd Nat )
proof end;
end;

:: deftheorem Def2 defines odd-valued EULRPART:def 2 :
for F being Function holds
( F is odd-valued iff for x being object st x in dom F holds
F . x is odd Nat );

registration
cluster empty Relation-like -> odd-valued for set ;
coherence
for b1 being Relation st b1 is empty holds
b1 is odd-valued
proof end;
let i be odd Nat;
cluster <*i*> -> odd-valued ;
coherence
<*i*> is odd-valued
proof end;
end;

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

registration
cluster Relation-like OddNAT -valued -> odd-valued for set ;
coherence
for b1 being Relation st b1 is OddNAT -valued holds
b1 is odd-valued
by RELAT_1:def 19;
end;

definition
let n be Nat;
mode a_partition of n -> non-zero natural-valued non-decreasing FinSequence means :Def3: :: EULRPART:def 3
Sum it = n;
existence
ex b1 being non-zero natural-valued non-decreasing FinSequence st Sum b1 = n
proof end;
end;

:: deftheorem Def3 defines a_partition EULRPART:def 3 :
for n being Nat
for b2 being non-zero natural-valued non-decreasing FinSequence holds
( b2 is a_partition of n iff Sum b2 = n );

theorem :: EULRPART:3
{} is a_partition of 0 by RVSUM_1:72, Def3;

registration
let n be Nat;
cluster Relation-like omega -defined RAT -valued non-zero Function-like finite FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued natural-valued non-decreasing V294() odd-valued for a_partition of n;
existence
ex b1 being a_partition of n st b1 is odd-valued
proof end;
cluster Relation-like omega -defined RAT -valued non-zero Function-like one-to-one finite FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued natural-valued non-decreasing V294() for a_partition of n;
existence
ex b1 being a_partition of n st b1 is one-to-one
proof end;
end;

registration
let n be Nat;
let a1 be set ;
a_partition of a1 ex b1 being set st
for b2 being a_partition of n holds b2 in b1
proof end;
end;

definition
let f be odd-valued FinSequence;
mode odd_organization of f -> valued_reorganization of f means :Def4: :: EULRPART:def 4
for n being Nat holds (2 * n) - 1 = f . (it _ (n,1)) & ... & (2 * n) - 1 = f . (it _ (n,(len (it . n))));
existence
ex b1 being valued_reorganization of f st
for n being Nat holds (2 * n) - 1 = f . (b1 _ (n,1)) & ... & (2 * n) - 1 = f . (b1 _ (n,(len (b1 . n))))
proof end;
end;

:: deftheorem Def4 defines odd_organization EULRPART:def 4 :
for f being odd-valued FinSequence
for b2 being valued_reorganization of f holds
( b2 is odd_organization of f iff for n being Nat holds (2 * n) - 1 = f . (b2 _ (n,1)) & ... & (2 * n) - 1 = f . (b2 _ (n,(len (b2 . n)))) );

theorem Th4: :: EULRPART:4
for f being odd-valued FinSequence
for o being DoubleReorganization of dom f st ( for n being Nat 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 end;

theorem Th5: :: EULRPART:5
for i being Nat
for f being odd-valued FinSequence
for g being complex-valued FinSequence
for o1, o2 being 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 end;

theorem Th6: :: EULRPART:6
for n being Nat
for p being a_partition of n ex O being odd-valued FinSequence ex a being natural-valued FinSequence st
( len O = len p & 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 end;

theorem Th7: :: EULRPART:7
for D being finite set
for f being Function of D,NAT ex h being FinSequence of D st
for d being Element of D holds card (Coim (h,d)) = f . d
proof end;

Lm1: for f1, f2, g1, g2 being complex-valued FinSequence st len f1 = len g1 & len f2 <= len g2 holds
(f1 ^ f2) (#) (g1 ^ g2) = (f1 (#) g1) ^ (f2 (#) g2)

proof end;

theorem Th8: :: EULRPART:8
for f1, f2, g1, g2 being complex-valued FinSequence st len f1 = len g1 holds
(f1 ^ f2) (#) (g1 ^ g2) = (f1 (#) g1) ^ (f2 (#) g2)
proof end;

Lm2: for i being Nat
for f being complex-valued FinSequence holds ((id (dom f)) (#) f) . i = i * (f . i)

proof end;

theorem Th9: :: EULRPART:9
for f, h being natural-valued FinSequence st ( for i being Nat holds card (Coim (h,i)) = f . i ) holds
Sum h = ((1 * (f . 1)) + (2 * (f . 2))) + ((((id (dom f)) (#) f),3) +...)
proof end;

theorem Th10: :: EULRPART:10
for g being natural-valued FinSequence
for sort being DoubleReorganization of dom g ex h being 2 * (len b2) -element FinSequence of NAT st
for j being Nat holds
( h . (2 * j) = 0 & h . ((2 * j) - 1) = (g . (sort _ (j,1))) + ((((g *. sort) . j),2) +...) )
proof end;

Lm3: for mu being natural-valued FinSequence st ( for j being Nat holds mu . (2 * j) = 0 ) holds
ex h being odd-valued FinSequence st
( h is non-decreasing & ( for j being Nat holds card (Coim (h,j)) = mu . j ) )

proof end;

theorem Th11: :: EULRPART:11
for n being Nat
for d being one-to-one a_partition of n ex e being odd-valued a_partition of n st
for j being Nat
for O1 being odd-valued FinSequence
for a1 being natural-valued FinSequence st len O1 = len d & len d = len a1 & d = O1 (#) (2 |^ a1) holds
for sort being 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 being Nat 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 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: :: EULRPART:def 5
for j being Nat
for O being odd-valued FinSequence
for a being natural-valued FinSequence st len O = len p & len p = len a & p = O (#) (2 |^ a) holds
for sort being 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 being Nat 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
ex b1 being odd-valued a_partition of n st
for j being Nat
for O being odd-valued FinSequence
for a being natural-valued FinSequence st len O = len p & len p = len a & p = O (#) (2 |^ a) holds
for sort being 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 being Nat holds (2 * i) - 1 = O . (sort _ (i,1)) & ... & (2 * i) - 1 = O . (sort _ (i,(len (sort . i)))) ) holds
( card (Coim (b1,1)) = ((2 |^ a) . (sort _ (1,1))) + (((((2 |^ a) *. sort) . 1),2) +...) & card (Coim (b1,3)) = ((2 |^ a) . (sort _ (2,1))) + (((((2 |^ a) *. sort) . 2),2) +...) & card (Coim (b1,5)) = ((2 |^ a) . (sort _ (3,1))) + (((((2 |^ a) *. sort) . 3),2) +...) & card (Coim (b1,((j * 2) - 1))) = ((2 |^ a) . (sort _ (j,1))) + (((((2 |^ a) *. sort) . j),2) +...) )
by Th11;
uniqueness
for b1, b2 being odd-valued a_partition of n st ( for j being Nat
for O being odd-valued FinSequence
for a being natural-valued FinSequence st len O = len p & len p = len a & p = O (#) (2 |^ a) holds
for sort being 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 being Nat holds (2 * i) - 1 = O . (sort _ (i,1)) & ... & (2 * i) - 1 = O . (sort _ (i,(len (sort . i)))) ) holds
( card (Coim (b1,1)) = ((2 |^ a) . (sort _ (1,1))) + (((((2 |^ a) *. sort) . 1),2) +...) & card (Coim (b1,3)) = ((2 |^ a) . (sort _ (2,1))) + (((((2 |^ a) *. sort) . 2),2) +...) & card (Coim (b1,5)) = ((2 |^ a) . (sort _ (3,1))) + (((((2 |^ a) *. sort) . 3),2) +...) & card (Coim (b1,((j * 2) - 1))) = ((2 |^ a) . (sort _ (j,1))) + (((((2 |^ a) *. sort) . j),2) +...) ) ) & ( for j being Nat
for O being odd-valued FinSequence
for a being natural-valued FinSequence st len O = len p & len p = len a & p = O (#) (2 |^ a) holds
for sort being 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 being Nat holds (2 * i) - 1 = O . (sort _ (i,1)) & ... & (2 * i) - 1 = O . (sort _ (i,(len (sort . i)))) ) holds
( card (Coim (b2,1)) = ((2 |^ a) . (sort _ (1,1))) + (((((2 |^ a) *. sort) . 1),2) +...) & card (Coim (b2,3)) = ((2 |^ a) . (sort _ (2,1))) + (((((2 |^ a) *. sort) . 2),2) +...) & card (Coim (b2,5)) = ((2 |^ a) . (sort _ (3,1))) + (((((2 |^ a) *. sort) . 3),2) +...) & card (Coim (b2,((j * 2) - 1))) = ((2 |^ a) . (sort _ (j,1))) + (((((2 |^ a) *. sort) . j),2) +...) ) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def5 defines Euler_transformation EULRPART:def 5 :
for n being Nat
for p being one-to-one a_partition of n
for b3 being odd-valued a_partition of n holds
( b3 = Euler_transformation p iff for j being Nat
for O being odd-valued FinSequence
for a being natural-valued FinSequence st len O = len p & len p = len a & p = O (#) (2 |^ a) holds
for sort being 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 being Nat holds (2 * i) - 1 = O . (sort _ (i,1)) & ... & (2 * i) - 1 = O . (sort _ (i,(len (sort . i)))) ) holds
( card (Coim (b3,1)) = ((2 |^ a) . (sort _ (1,1))) + (((((2 |^ a) *. sort) . 1),2) +...) & card (Coim (b3,3)) = ((2 |^ a) . (sort _ (2,1))) + (((((2 |^ a) *. sort) . 2),2) +...) & card (Coim (b3,5)) = ((2 |^ a) . (sort _ (3,1))) + (((((2 |^ a) *. sort) . 3),2) +...) & card (Coim (b3,((j * 2) - 1))) = ((2 |^ a) . (sort _ (j,1))) + (((((2 |^ a) *. sort) . j),2) +...) ) );

theorem Th12: :: EULRPART:12
for n being Nat
for p being one-to-one a_partition of n
for e being odd-valued a_partition of n holds
( e = Euler_transformation p iff for O being odd-valued FinSequence
for a being natural-valued FinSequence
for sort being odd_organization of O st len O = len p & len p = len a & p = O (#) (2 |^ a) holds
for j being Nat holds card (Coim (e,((j * 2) - 1))) = ((((2 |^ a) *. sort) . j),1) +... )
proof end;

registration
cluster Relation-like Function-like one-to-one real-valued non-decreasing -> real-valued increasing for set ;
coherence
for b1 being real-valued Function st b1 is one-to-one & b1 is non-decreasing holds
b1 is increasing
proof end;
end;

theorem Th13: :: EULRPART:13
for i being Nat
for O being odd-valued FinSequence
for a being natural-valued FinSequence
for s being 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 end;

Lm4: for n being Nat
for p1, p2 being one-to-one a_partition of n st Euler_transformation p1 = Euler_transformation p2 holds
rng p1 c= rng p2

proof end;

theorem Th14: :: EULRPART:14
for n being Nat
for p1, p2 being one-to-one a_partition of n st Euler_transformation p1 = Euler_transformation p2 holds
p1 = p2
proof end;

theorem Th15: :: EULRPART:15
for n being Nat
for e being odd-valued a_partition of n ex p being one-to-one a_partition of n st e = Euler_transformation p
proof end;

:: WP: Euler's partition theorem
theorem :: EULRPART:16
for n being Nat holds card { p where p is odd-valued a_partition of n : verum } = card { p where p is one-to-one a_partition of n : verum }
proof end;