P. 292 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 29101-29200   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	omsmeasOLD 29101	The restriction of a constructed outer measure to Catatheodory measurable sets is a measure. This theorem allows to construct measures from pre-measures with the required characteristics, as for the Lebesgue measure. (Contributed by Thierry Arnoux, 17-May-2020.) Obsolete version of omsmeas 29100 as of 4-Oct-2020. (New usage is discouraged.) (Proof modification is discouraged.)
|- M = (toOMeas ` R )   &    |- S = (toCaraSiga ` M )   &    |- ( ph -> Q e. V )   &    |- ( ph -> R : Q --> ( 0 [,] +oo ) )   &    |- ( ph -> (/) e. dom R )   &    |- ( ph -> ( R ` (/) ) = 0 )   =>    |- ( ph -> ( M |` S ) e. (measures ` S ) )
Theorem	pmeasmono 29102*	This theorem's hypotheses define a pre-measure. A pre-measure is monotone. (Contributed by Thierry Arnoux, 19-Jul-2020.)
|- ( ph -> P : R --> ( 0 [,] +oo ) )   &    |- ( ph -> ( P ` (/) ) = 0 )   &    |- ( ( ph /\ ( x ~<_ om /\ x C_ R /\ Disj y e. x y ) ) -> ( P ` U. x ) = Σ* y e. x ( P ` y ) )   &    |- ( ph -> A e. R )   &    |- ( ph -> B e. R )   &    |- ( ph -> ( B \ A ) e. R )   &    |- ( ph -> A C_ B )   =>    |- ( ph -> ( P ` A ) <_ ( P ` B ) )
Theorem	pmeasadd 29103*	A premeasure on a ring of sets is additive on disjoint countable collections. This is called sigma-additivity. (Contributed by Thierry Arnoux, 19-Jul-2020.)
|- ( ph -> P : R --> ( 0 [,] +oo ) )   &    |- ( ph -> ( P ` (/) ) = 0 )   &    |- ( ( ph /\ ( x ~<_ om /\ x C_ R /\ Disj y e. x y ) ) -> ( P ` U. x ) = Σ* y e. x ( P ` y ) )   &    |- Q = { s e. ~P ~P O | ( (/) e. s /\ A. x e. s A. y e. s ( ( x u. y ) e. s /\ ( x \ y ) e. s ) ) }   &    |- ( ph -> R e. Q )   &    |- ( ph -> A ~<_ om )   &    |- ( ( ph /\ k e. A ) -> B e. R )   &    |- ( ph -> Disj k e. A B )   =>    |- ( ph -> ( P ` U_ k e. A B ) = Σ* k e. A ( P ` B ) )
21.3.16  Integration
21.3.16.1  Lebesgue integral - misc additions
Theorem	itgeq12dv 29104*	Equality theorem for an integral. (Contributed by Thierry Arnoux, 14-Feb-2017.)
|- ( ph -> A = B )   &    |- ( ( ph /\ x e. A ) -> C = D )   =>    |- ( ph -> S. A C _d x = S. B D _d x )
21.3.16.2  Bochner integral
Syntax	citgm 29105	Extend class notation with the (measure) Bochner integral.
class itgm
Syntax	csitm 29106	Extend class notation with the integral metric for simple functions.
class sitm
Syntax	csitg 29107	Extend class notation with the integral of simple functions.
class sitg
Definition	df-sitg 29108*	Define the integral of simple functions from a measurable space dom m to a generic space w equipped with the right scalar product. w will later be required to be a Banach space. These simple functions are required to take finitely many different values: this is expressed by ran g e. Fin in the definition. Moreover, for each x, the pre-image ( `' g " { x } ) is requested to be measurable, of finite measure. In this definition, (sigaGen ` ( TopOpen ` w ) ) is the Borel sigma-algebra on w, and the functions g range over the measurable functions over that Borel algebra. Definition 2.4.1 of [Bogachev] p. 118. (Contributed by Thierry Arnoux, 21-Oct-2017.)
|- sitg = ( w e. _V , m e. U. ran measures |-> ( f e. { g e. ( dom mMblFnM (sigaGen ` ( TopOpen ` w ) ) ) | ( ran g e. Fin /\ A. x e. ( ran g \ { ( 0g ` w ) } ) ( m ` ( `' g " { x } ) ) e. ( 0 [,) +oo ) ) } |-> ( w gsumg ( x e. ( ran f \ { ( 0g ` w ) } ) |-> ( ( (RRHom ` (Scalar ` w ) ) ` ( m ` ( `' f " { x } ) ) ) ( .s ` w ) x ) ) ) ) )
Definition	df-sitm 29109*	Define the integral metric for simple functions, as the integral of the distances between the function values. Since distances take nonnegative values in RR*, the range structure for this integral is ( RR*s ↾s ( 0 [,] +oo ) ). See definition 2.3.1 of [Bogachev] p. 116. (Contributed by Thierry Arnoux, 22-Oct-2017.)
|- sitm = ( w e. _V , m e. U. ran measures |-> ( f e. dom ( wsitg m ) , g e. dom ( wsitg m ) |-> ( ( ( RR*s ↾s ( 0 [,] +oo ) )sitg m ) ` ( f oF ( dist ` w ) g ) ) ) )
Theorem	sitgval 29110*	Value of the simple function integral builder for a given space W and measure M. (Contributed by Thierry Arnoux, 30-Jan-2018.)
|- B = ( Base ` W )   &    |- J = ( TopOpen ` W )   &    |- S = (sigaGen ` J )   &    |- .0. = ( 0g ` W )   &    |- .x. = ( .s ` W )   &    |- H = (RRHom ` (Scalar ` W ) )   &    |- ( ph -> W e. V )   &    |- ( ph -> M e. U. ran measures )   =>    |- ( ph -> ( Wsitg M ) = ( f e. { g e. ( dom MMblFnM S ) | ( ran g e. Fin /\ A. x e. ( ran g \ { .0. } ) ( M ` ( `' g " { x } ) ) e. ( 0 [,) +oo ) ) } |-> ( W gsumg ( x e. ( ran f \ { .0. } ) |-> ( ( H ` ( M ` ( `' f " { x } ) ) ) .x. x ) ) ) ) )
Theorem	issibf 29111*	The predicate " F is a simple function" relative to the Bochner integral. (Contributed by Thierry Arnoux, 19-Feb-2018.)
|- B = ( Base ` W )   &    |- J = ( TopOpen ` W )   &    |- S = (sigaGen ` J )   &    |- .0. = ( 0g ` W )   &    |- .x. = ( .s ` W )   &    |- H = (RRHom ` (Scalar ` W ) )   &    |- ( ph -> W e. V )   &    |- ( ph -> M e. U. ran measures )   =>    |- ( ph -> ( F e. dom ( Wsitg M ) <-> ( F e. ( dom MMblFnM S ) /\ ran F e. Fin /\ A. x e. ( ran F \ { .0. } ) ( M ` ( `' F " { x } ) ) e. ( 0 [,) +oo ) ) ) )
Theorem	sibf0 29112	The constant zero function is a simple function. (Contributed by Thierry Arnoux, 4-Mar-2018.)
|- B = ( Base ` W )   &    |- J = ( TopOpen ` W )   &    |- S = (sigaGen ` J )   &    |- .0. = ( 0g ` W )   &    |- .x. = ( .s ` W )   &    |- H = (RRHom ` (Scalar ` W ) )   &    |- ( ph -> W e. V )   &    |- ( ph -> M e. U. ran measures )   &    |- ( ph -> W e. TopSp )   &    |- ( ph -> W e. Mnd )   =>    |- ( ph -> ( U. dom M X. { .0. } ) e. dom ( Wsitg M ) )
Theorem	sibfmbl 29113	A simple function is measurable. (Contributed by Thierry Arnoux, 19-Feb-2018.)
|- B = ( Base ` W )   &    |- J = ( TopOpen ` W )   &    |- S = (sigaGen ` J )   &    |- .0. = ( 0g ` W )   &    |- .x. = ( .s ` W )   &    |- H = (RRHom ` (Scalar ` W ) )   &    |- ( ph -> W e. V )   &    |- ( ph -> M e. U. ran measures )   &    |- ( ph -> F e. dom ( Wsitg M ) )   =>    |- ( ph -> F e. ( dom MMblFnM S ) )
Theorem	sibff 29114	A simple function is a function. (Contributed by Thierry Arnoux, 19-Feb-2018.)
|- B = ( Base ` W )   &    |- J = ( TopOpen ` W )   &    |- S = (sigaGen ` J )   &    |- .0. = ( 0g ` W )   &    |- .x. = ( .s ` W )   &    |- H = (RRHom ` (Scalar ` W ) )   &    |- ( ph -> W e. V )   &    |- ( ph -> M e. U. ran measures )   &    |- ( ph -> F e. dom ( Wsitg M ) )   =>    |- ( ph -> F : U. dom M --> U. J )
Theorem	sibfrn 29115	A simple function has finite range. (Contributed by Thierry Arnoux, 19-Feb-2018.)
|- B = ( Base ` W )   &    |- J = ( TopOpen ` W )   &    |- S = (sigaGen ` J )   &    |- .0. = ( 0g ` W )   &    |- .x. = ( .s ` W )   &    |- H = (RRHom ` (Scalar ` W ) )   &    |- ( ph -> W e. V )   &    |- ( ph -> M e. U. ran measures )   &    |- ( ph -> F e. dom ( Wsitg M ) )   =>    |- ( ph -> ran F e. Fin )
Theorem	sibfima 29116	Any preimage of a singleton by a simple function is measurable. (Contributed by Thierry Arnoux, 19-Feb-2018.)
|- B = ( Base ` W )   &    |- J = ( TopOpen ` W )   &    |- S = (sigaGen ` J )   &    |- .0. = ( 0g ` W )   &    |- .x. = ( .s ` W )   &    |- H = (RRHom ` (Scalar ` W ) )   &    |- ( ph -> W e. V )   &    |- ( ph -> M e. U. ran measures )   &    |- ( ph -> F e. dom ( Wsitg M ) )   =>    |- ( ( ph /\ A e. ( ran F \ { .0. } ) ) -> ( M ` ( `' F " { A } ) ) e. ( 0 [,) +oo ) )
Theorem	sibfinima 29117	The measure of the intersection of any two preimages by simple functions is a real number. (Contributed by Thierry Arnoux, 21-Mar-2018.)
|- B = ( Base ` W )   &    |- J = ( TopOpen ` W )   &    |- S = (sigaGen ` J )   &    |- .0. = ( 0g ` W )   &    |- .x. = ( .s ` W )   &    |- H = (RRHom ` (Scalar ` W ) )   &    |- ( ph -> W e. V )   &    |- ( ph -> M e. U. ran measures )   &    |- ( ph -> F e. dom ( Wsitg M ) )   &    |- ( ph -> G e. dom ( Wsitg M ) )   &    |- ( ph -> W e. TopSp )   &    |- ( ph -> J e. Fre )   =>    |- ( ( ( ph /\ X e. ran F /\ Y e. ran G ) /\ ( X =/= .0. \/ Y =/= .0. ) ) -> ( M ` ( ( `' F " { X } ) i^i ( `' G " { Y } ) ) ) e. ( 0 [,) +oo ) )
Theorem	sibfof 29118	Applying function operations on simple functions results in simple functions with regard to the destination space, provided the operation fulfills a simple condition. (Contributed by Thierry Arnoux, 12-Mar-2018.)
|- B = ( Base ` W )   &    |- J = ( TopOpen ` W )   &    |- S = (sigaGen ` J )   &    |- .0. = ( 0g ` W )   &    |- .x. = ( .s ` W )   &    |- H = (RRHom ` (Scalar ` W ) )   &    |- ( ph -> W e. V )   &    |- ( ph -> M e. U. ran measures )   &    |- ( ph -> F e. dom ( Wsitg M ) )   &    |- C = ( Base ` K )   &    |- ( ph -> W e. TopSp )   &    |- ( ph -> .+ : ( B X. B ) --> C )   &    |- ( ph -> G e. dom ( Wsitg M ) )   &    |- ( ph -> K e. TopSp )   &    |- ( ph -> J e. Fre )   &    |- ( ph -> ( .0. .+ .0. ) = ( 0g ` K ) )   =>    |- ( ph -> ( F oF .+ G ) e. dom ( Ksitg M ) )
Theorem	sitgfval 29119*	Value of the Bochner integral for a simple function F. (Contributed by Thierry Arnoux, 30-Jan-2018.)
|- B = ( Base ` W )   &    |- J = ( TopOpen ` W )   &    |- S = (sigaGen ` J )   &    |- .0. = ( 0g ` W )   &    |- .x. = ( .s ` W )   &    |- H = (RRHom ` (Scalar ` W ) )   &    |- ( ph -> W e. V )   &    |- ( ph -> M e. U. ran measures )   &    |- ( ph -> F e. dom ( Wsitg M ) )   =>    |- ( ph -> ( ( Wsitg M ) ` F ) = ( W gsumg ( x e. ( ran F \ { .0. } ) |-> ( ( H ` ( M ` ( `' F " { x } ) ) ) .x. x ) ) ) )
Theorem	sitgclg 29120*	Closure of the Bochner integral on simple functions, generic version. See sitgclbn 29121 for the version for Banach spaces. (Contributed by Thierry Arnoux, 24-Feb-2018.) (Proof shortened by AV, 12-Dec-2019.)
|- B = ( Base ` W )   &    |- J = ( TopOpen ` W )   &    |- S = (sigaGen ` J )   &    |- .0. = ( 0g ` W )   &    |- .x. = ( .s ` W )   &    |- H = (RRHom ` (Scalar ` W ) )   &    |- ( ph -> W e. V )   &    |- ( ph -> M e. U. ran measures )   &    |- ( ph -> F e. dom ( Wsitg M ) )   &    |- G = (Scalar ` W )   &    |- D = ( ( dist ` G ) |` ( ( Base ` G ) X. ( Base ` G ) ) )   &    |- ( ph -> W e. TopSp )   &    |- ( ph -> W e. CMnd )   &    |- ( ph -> (Scalar ` W ) e. ℝExt )   &    |- ( ( ph /\ m e. ( H " ( 0 [,) +oo ) ) /\ x e. B ) -> ( m .x. x ) e. B )   =>    |- ( ph -> ( ( Wsitg M ) ` F ) e. B )
Theorem	sitgclbn 29121	Closure of the Bochner integral on a simple function. This version is specific to Banach spaces, with additional conditions on its scalar field. (Contributed by Thierry Arnoux, 24-Feb-2018.)
|- B = ( Base ` W )   &    |- J = ( TopOpen ` W )   &    |- S = (sigaGen ` J )   &    |- .0. = ( 0g ` W )   &    |- .x. = ( .s ` W )   &    |- H = (RRHom ` (Scalar ` W ) )   &    |- ( ph -> W e. V )   &    |- ( ph -> M e. U. ran measures )   &    |- ( ph -> F e. dom ( Wsitg M ) )   &    |- ( ph -> W e. Ban )   &    |- ( ph -> (Scalar ` W ) e. ℝExt )   =>    |- ( ph -> ( ( Wsitg M ) ` F ) e. B )
Theorem	sitgclcn 29122	Closure of the Bochner integral on a simple function. This version is specific to Banach spaces on the complex numbers. (Contributed by Thierry Arnoux, 24-Feb-2018.)
|- B = ( Base ` W )   &    |- J = ( TopOpen ` W )   &    |- S = (sigaGen ` J )   &    |- .0. = ( 0g ` W )   &    |- .x. = ( .s ` W )   &    |- H = (RRHom ` (Scalar ` W ) )   &    |- ( ph -> W e. V )   &    |- ( ph -> M e. U. ran measures )   &    |- ( ph -> F e. dom ( Wsitg M ) )   &    |- ( ph -> W e. Ban )   &    |- ( ph -> (Scalar ` W ) = ℂfld )   =>    |- ( ph -> ( ( Wsitg M ) ` F ) e. B )
Theorem	sitgclre 29123	Closure of the Bochner integral on a simple function. This version is specific to Banach spaces on the real numbers. (Contributed by Thierry Arnoux, 24-Feb-2018.)
|- B = ( Base ` W )   &    |- J = ( TopOpen ` W )   &    |- S = (sigaGen ` J )   &    |- .0. = ( 0g ` W )   &    |- .x. = ( .s ` W )   &    |- H = (RRHom ` (Scalar ` W ) )   &    |- ( ph -> W e. V )   &    |- ( ph -> M e. U. ran measures )   &    |- ( ph -> F e. dom ( Wsitg M ) )   &    |- ( ph -> W e. Ban )   &    |- ( ph -> (Scalar ` W ) = RRfld )   =>    |- ( ph -> ( ( Wsitg M ) ` F ) e. B )
Theorem	sitg0 29124	The integral of the constant zero function is zero. (Contributed by Thierry Arnoux, 13-Mar-2018.)
|- B = ( Base ` W )   &    |- J = ( TopOpen ` W )   &    |- S = (sigaGen ` J )   &    |- .0. = ( 0g ` W )   &    |- .x. = ( .s ` W )   &    |- H = (RRHom ` (Scalar ` W ) )   &    |- ( ph -> W e. V )   &    |- ( ph -> M e. U. ran measures )   &    |- ( ph -> W e. TopSp )   &    |- ( ph -> W e. Mnd )   =>    |- ( ph -> ( ( Wsitg M ) ` ( U. dom M X. { .0. } ) ) = .0. )
Theorem	sitgf 29125*	The integral for simple functions is itself a function. (Contributed by Thierry Arnoux, 13-Feb-2018.)
|- B = ( Base ` W )   &    |- J = ( TopOpen ` W )   &    |- S = (sigaGen ` J )   &    |- .0. = ( 0g ` W )   &    |- .x. = ( .s ` W )   &    |- H = (RRHom ` (Scalar ` W ) )   &    |- ( ph -> W e. V )   &    |- ( ph -> M e. U. ran measures )   &    |- ( ( ph /\ f e. dom ( Wsitg M ) ) -> ( ( Wsitg M ) ` f ) e. B )   =>    |- ( ph -> ( Wsitg M ) : dom ( Wsitg M ) --> B )
Theorem	sitgaddlemb 29126	Lemma for * sitgadd . (Contributed by Thierry Arnoux, 10-Mar-2019.)
|- B = ( Base ` W )   &    |- J = ( TopOpen ` W )   &    |- S = (sigaGen ` J )   &    |- .0. = ( 0g ` W )   &    |- .x. = ( .s ` W )   &    |- H = (RRHom ` (Scalar ` W ) )   &    |- ( ph -> W e. V )   &    |- ( ph -> M e. U. ran measures )   &    |- ( ph -> W e. TopSp )   &    |- ( ph -> ( W ↾v ( H " ( 0 [,) +oo ) ) ) e. SLMod )   &    |- ( ph -> J e. Fre )   &    |- ( ph -> F e. dom ( Wsitg M ) )   &    |- ( ph -> G e. dom ( Wsitg M ) )   &    |- ( ph -> (Scalar ` W ) e. ℝExt )   &    |- .+ = ( +g ` W )   =>    |- ( ( ph /\ p e. ( ( ran F X. ran G ) \ { <. .0. , .0. >. } ) ) -> ( ( H ` ( M ` ( ( `' F " { ( 1st ` p ) } ) i^i ( `' G " { ( 2nd ` p ) } ) ) ) ) .x. ( 2nd ` p ) ) e. B )
Theorem	sitmval 29127*	Value of the simple function integral metric for a given space W and measure M. (Contributed by Thierry Arnoux, 30-Jan-2018.)
|- D = ( dist ` W )   &    |- ( ph -> W e. V )   &    |- ( ph -> M e. U. ran measures )   =>    |- ( ph -> ( Wsitm M ) = ( f e. dom ( Wsitg M ) , g e. dom ( Wsitg M ) |-> ( ( ( RR*s ↾s ( 0 [,] +oo ) )sitg M ) ` ( f oF D g ) ) ) )
Theorem	sitmfval 29128	Value of the integral distance between two simple functions. (Contributed by Thierry Arnoux, 30-Jan-2018.)
|- D = ( dist ` W )   &    |- ( ph -> W e. V )   &    |- ( ph -> M e. U. ran measures )   &    |- ( ph -> F e. dom ( Wsitg M ) )   &    |- ( ph -> G e. dom ( Wsitg M ) )   =>    |- ( ph -> ( F ( Wsitm M ) G ) = ( ( ( RR*s ↾s ( 0 [,] +oo ) )sitg M ) ` ( F oF D G ) ) )
Theorem	sitmcl 29129	Closure of the integral distance between two simple functions, for an extended metric space. (Contributed by Thierry Arnoux, 13-Feb-2018.)
|- ( ph -> W e. Mnd )   &    |- ( ph -> W e. *MetSp )   &    |- ( ph -> M e. U. ran measures )   &    |- ( ph -> F e. dom ( Wsitg M ) )   &    |- ( ph -> G e. dom ( Wsitg M ) )   =>    |- ( ph -> ( F ( Wsitm M ) G ) e. ( 0 [,] +oo ) )
Theorem	sitmf 29130	The integral metric as a function. (Contributed by Thierry Arnoux, 13-Mar-2018.)
|- ( ph -> W e. Mnd )   &    |- ( ph -> W e. *MetSp )   &    |- ( ph -> M e. U. ran measures )   =>    |- ( ph -> ( Wsitm M ) : ( dom ( Wsitg M ) X. dom ( Wsitg M ) ) --> ( 0 [,] +oo ) )
Definition	df-itgm 29131*	Define the Bochner integral as the extension by continuity of the Bochnel integral for simple functions. Bogachev first defines 'fundamental in the mean' sequences, in definition 2.3.1 of [Bogachev] p. 116, and notes that those are actually Cauchy sequences for the pseudometric ( wsitm m ). He then defines the Bochner integral in chapter 2.4.4 in [Bogachev] p. 118. The definition of the Lebesgue integral, df-itg 22516. (Contributed by Thierry Arnoux, 13-Feb-2018.)
|- itgm = ( w e. _V , m e. U. ran measures |-> ( ( (metUnif ` ( wsitm m ) )CnExt (UnifSt ` w ) ) ` ( wsitg m ) ) )
21.3.17  Euler's partition theorem
Theorem	oddpwdc 29132*	Lemma for eulerpart 29160. The function F that decomposes a number into its "odd" and "even" parts, which is to say the largest power of two and largest odd divisor of a number, is a bijection from pairs of a nonnegative integer and an odd number to positive integers. (Contributed by Thierry Arnoux, 15-Aug-2017.)
|- J = { z e. NN | -. 2 || z }   &    |- F = ( x e. J , y e. NN0 |-> ( ( 2 ^ y ) x. x ) )   =>    |- F : ( J X. NN0 ) -1-1-onto-> NN
Theorem	oddpwdcv 29133*	Lemma for eulerpart 29160: value of the F function. (Contributed by Thierry Arnoux, 9-Sep-2017.)
|- J = { z e. NN | -. 2 || z }   &    |- F = ( x e. J , y e. NN0 |-> ( ( 2 ^ y ) x. x ) )   =>    |- ( W e. ( J X. NN0 ) -> ( F ` W ) = ( ( 2 ^ ( 2nd ` W ) ) x. ( 1st ` W ) ) )
Theorem	eulerpartlemsv1 29134*	Lemma for eulerpart 29160. Value of the sum of a partition A. (Contributed by Thierry Arnoux, 26-Aug-2018.)
|- R = { f | ( `' f " NN ) e. Fin }   &    |- S = ( f e. ( ( NN0 ^m NN ) i^i R ) |-> sum_ k e. NN ( ( f ` k ) x. k ) )   =>    |- ( A e. ( ( NN0 ^m NN ) i^i R ) -> ( S ` A ) = sum_ k e. NN ( ( A ` k ) x. k ) )
Theorem	eulerpartlemelr 29135*	Lemma for eulerpart 29160. (Contributed by Thierry Arnoux, 8-Aug-2018.)
|- R = { f | ( `' f " NN ) e. Fin }   &    |- S = ( f e. ( ( NN0 ^m NN ) i^i R ) |-> sum_ k e. NN ( ( f ` k ) x. k ) )   =>    |- ( A e. ( ( NN0 ^m NN ) i^i R ) -> ( A : NN --> NN0 /\ ( `' A " NN ) e. Fin ) )
Theorem	eulerpartlemsv2 29136*	Lemma for eulerpart 29160. Value of the sum of a finite partition A (Contributed by Thierry Arnoux, 19-Aug-2018.)
|- R = { f | ( `' f " NN ) e. Fin }   &    |- S = ( f e. ( ( NN0 ^m NN ) i^i R ) |-> sum_ k e. NN ( ( f ` k ) x. k ) )   =>    |- ( A e. ( ( NN0 ^m NN ) i^i R ) -> ( S ` A ) = sum_ k e. ( `' A " NN ) ( ( A ` k ) x. k ) )
Theorem	eulerpartlemsf 29137*	Lemma for eulerpart 29160. (Contributed by Thierry Arnoux, 8-Aug-2018.)
|- R = { f | ( `' f " NN ) e. Fin }   &    |- S = ( f e. ( ( NN0 ^m NN ) i^i R ) |-> sum_ k e. NN ( ( f ` k ) x. k ) )   =>    |- S : ( ( NN0 ^m NN ) i^i R ) --> NN0
Theorem	eulerpartlems 29138*	Lemma for eulerpart 29160. (Contributed by Thierry Arnoux, 6-Aug-2018.) (Revised by Thierry Arnoux, 1-Sep-2019.)
|- R = { f | ( `' f " NN ) e. Fin }   &    |- S = ( f e. ( ( NN0 ^m NN ) i^i R ) |-> sum_ k e. NN ( ( f ` k ) x. k ) )   =>    |- ( ( A e. ( ( NN0 ^m NN ) i^i R ) /\ t e. ( ZZ>= ` ( ( S ` A ) + 1 ) ) ) -> ( A ` t ) = 0 )
Theorem	eulerpartlemsv3 29139*	Lemma for eulerpart 29160. Value of the sum of a finite partition A (Contributed by Thierry Arnoux, 19-Aug-2018.)
|- R = { f | ( `' f " NN ) e. Fin }   &    |- S = ( f e. ( ( NN0 ^m NN ) i^i R ) |-> sum_ k e. NN ( ( f ` k ) x. k ) )   =>    |- ( A e. ( ( NN0 ^m NN ) i^i R ) -> ( S ` A ) = sum_ k e. ( 1 ... ( S ` A ) ) ( ( A ` k ) x. k ) )
Theorem	eulerpartlemgc 29140*	Lemma for eulerpart 29160. (Contributed by Thierry Arnoux, 9-Aug-2018.)
|- R = { f | ( `' f " NN ) e. Fin }   &    |- S = ( f e. ( ( NN0 ^m NN ) i^i R ) |-> sum_ k e. NN ( ( f ` k ) x. k ) )   =>    |- ( ( A e. ( ( NN0 ^m NN ) i^i R ) /\ ( t e. NN /\ n e. (bits ` ( A ` t ) ) ) ) -> ( ( 2 ^ n ) x. t ) <_ ( S ` A ) )
Theorem	eulerpartleme 29141*	Lemma for eulerpart 29160. (Contributed by Mario Carneiro, 26-Jan-2015.)
|- P = { f e. ( NN0 ^m NN ) | ( ( `' f " NN ) e. Fin /\ sum_ k e. NN ( ( f ` k ) x. k ) = N ) }   =>    |- ( A e. P <-> ( A : NN --> NN0 /\ ( `' A " NN ) e. Fin /\ sum_ k e. NN ( ( A ` k ) x. k ) = N ) )
Theorem	eulerpartlemv 29142*	Lemma for eulerpart 29160. (Contributed by Thierry Arnoux, 19-Aug-2018.)
|- P = { f e. ( NN0 ^m NN ) | ( ( `' f " NN ) e. Fin /\ sum_ k e. NN ( ( f ` k ) x. k ) = N ) }   =>    |- ( A e. P <-> ( A : NN --> NN0 /\ ( `' A " NN ) e. Fin /\ sum_ k e. ( `' A " NN ) ( ( A ` k ) x. k ) = N ) )
Theorem	eulerpartlemo 29143*	Lemma for eulerpart 29160: O is the set of odd partitions of N. (Contributed by Thierry Arnoux, 10-Aug-2017.)
|- P = { f e. ( NN0 ^m NN ) | ( ( `' f " NN ) e. Fin /\ sum_ k e. NN ( ( f ` k ) x. k ) = N ) }   &    |- O = { g e. P | A. n e. ( `' g " NN ) -. 2 || n }   &    |- D = { g e. P | A. n e. NN ( g ` n ) <_ 1 }   =>    |- ( A e. O <-> ( A e. P /\ A. n e. ( `' A " NN ) -. 2 || n ) )
Theorem	eulerpartlemd 29144*	Lemma for eulerpart 29160: D is the set of distinct part. of N. (Contributed by Thierry Arnoux, 11-Aug-2017.)
|- P = { f e. ( NN0 ^m NN ) | ( ( `' f " NN ) e. Fin /\ sum_ k e. NN ( ( f ` k ) x. k ) = N ) }   &    |- O = { g e. P | A. n e. ( `' g " NN ) -. 2 || n }   &    |- D = { g e. P | A. n e. NN ( g ` n ) <_ 1 }   =>    |- ( A e. D <-> ( A e. P /\ ( A " NN ) C_ { 0 , 1 } ) )
Theorem	eulerpartlem1 29145*	Lemma for eulerpart 29160. (Contributed by Thierry Arnoux, 27-Aug-2017.) (Revised by Thierry Arnoux, 1-Sep-2019.)
|- P = { f e. ( NN0 ^m NN ) | ( ( `' f " NN ) e. Fin /\ sum_ k e. NN ( ( f ` k ) x. k ) = N ) }   &    |- O = { g e. P | A. n e. ( `' g " NN ) -. 2 || n }   &    |- D = { g e. P | A. n e. NN ( g ` n ) <_ 1 }   &    |- J = { z e. NN | -. 2 || z }   &    |- F = ( x e. J , y e. NN0 |-> ( ( 2 ^ y ) x. x ) )   &    |- H = { r e. ( ( ~P NN0 i^i Fin ) ^m J ) | ( r supp (/) ) e. Fin }   &    |- M = ( r e. H |-> { <. x , y >. | ( x e. J /\ y e. ( r ` x ) ) } )   =>    |- M : H -1-1-onto-> ( ~P ( J X. NN0 ) i^i Fin )
Theorem	eulerpartlemb 29146*	Lemma for eulerpart 29160. The set of all partitions of N is finite. (Contributed by Mario Carneiro, 26-Jan-2015.)
|- P = { f e. ( NN0 ^m NN ) | ( ( `' f " NN ) e. Fin /\ sum_ k e. NN ( ( f ` k ) x. k ) = N ) }   &    |- O = { g e. P | A. n e. ( `' g " NN ) -. 2 || n }   &    |- D = { g e. P | A. n e. NN ( g ` n ) <_ 1 }   &    |- J = { z e. NN | -. 2 || z }   &    |- F = ( x e. J , y e. NN0 |-> ( ( 2 ^ y ) x. x ) )   &    |- H = { r e. ( ( ~P NN0 i^i Fin ) ^m J ) | ( r supp (/) ) e. Fin }   &    |- M = ( r e. H |-> { <. x , y >. | ( x e. J /\ y e. ( r ` x ) ) } )   =>    |- P e. Fin
Theorem	eulerpartlemt0 29147*	Lemma for eulerpart 29160. (Contributed by Thierry Arnoux, 19-Sep-2017.)
|- P = { f e. ( NN0 ^m NN ) | ( ( `' f " NN ) e. Fin /\ sum_ k e. NN ( ( f ` k ) x. k ) = N ) }   &    |- O = { g e. P | A. n e. ( `' g " NN ) -. 2 || n }   &    |- D = { g e. P | A. n e. NN ( g ` n ) <_ 1 }   &    |- J = { z e. NN | -. 2 || z }   &    |- F = ( x e. J , y e. NN0 |-> ( ( 2 ^ y ) x. x ) )   &    |- H = { r e. ( ( ~P NN0 i^i Fin ) ^m J ) | ( r supp (/) ) e. Fin }   &    |- M = ( r e. H |-> { <. x , y >. | ( x e. J /\ y e. ( r ` x ) ) } )   &    |- R = { f | ( `' f " NN ) e. Fin }   &    |- T = { f e. ( NN0 ^m NN ) | ( `' f " NN ) C_ J }   =>    |- ( A e. ( T i^i R ) <-> ( A e. ( NN0 ^m NN ) /\ ( `' A " NN ) e. Fin /\ ( `' A " NN ) C_ J ) )
Theorem	eulerpartlemf 29148*	Lemma for eulerpart 29160: Odd partitions are zero for even numbers. (Contributed by Thierry Arnoux, 9-Sep-2017.)
|- P = { f e. ( NN0 ^m NN ) | ( ( `' f " NN ) e. Fin /\ sum_ k e. NN ( ( f ` k ) x. k ) = N ) }   &    |- O = { g e. P | A. n e. ( `' g " NN ) -. 2 || n }   &    |- D = { g e. P | A. n e. NN ( g ` n ) <_ 1 }   &    |- J = { z e. NN | -. 2 || z }   &    |- F = ( x e. J , y e. NN0 |-> ( ( 2 ^ y ) x. x ) )   &    |- H = { r e. ( ( ~P NN0 i^i Fin ) ^m J ) | ( r supp (/) ) e. Fin }   &    |- M = ( r e. H |-> { <. x , y >. | ( x e. J /\ y e. ( r ` x ) ) } )   &    |- R = { f | ( `' f " NN ) e. Fin }   &    |- T = { f e. ( NN0 ^m NN ) | ( `' f " NN ) C_ J }   =>    |- ( ( A e. ( T i^i R ) /\ t e. ( NN \ J ) ) -> ( A ` t ) = 0 )
Theorem	eulerpartlemt 29149*	Lemma for eulerpart 29160. (Contributed by Thierry Arnoux, 19-Sep-2017.)
|- P = { f e. ( NN0 ^m NN ) | ( ( `' f " NN ) e. Fin /\ sum_ k e. NN ( ( f ` k ) x. k ) = N ) }   &    |- O = { g e. P | A. n e. ( `' g " NN ) -. 2 || n }   &    |- D = { g e. P | A. n e. NN ( g ` n ) <_ 1 }   &    |- J = { z e. NN | -. 2 || z }   &    |- F = ( x e. J , y e. NN0 |-> ( ( 2 ^ y ) x. x ) )   &    |- H = { r e. ( ( ~P NN0 i^i Fin ) ^m J ) | ( r supp (/) ) e. Fin }   &    |- M = ( r e. H |-> { <. x , y >. | ( x e. J /\ y e. ( r ` x ) ) } )   &    |- R = { f | ( `' f " NN ) e. Fin }   &    |- T = { f e. ( NN0 ^m NN ) | ( `' f " NN ) C_ J }   =>    |- ( ( NN0 ^m J ) i^i R ) = ran ( m e. ( T i^i R ) |-> ( m |` J ) )
Theorem	eulerpartgbij 29150*	Lemma for eulerpart 29160: The G function is a bijection. (Contributed by Thierry Arnoux, 27-Aug-2017.) (Revised by Thierry Arnoux, 1-Sep-2019.)
|- P = { f e. ( NN0 ^m NN ) | ( ( `' f " NN ) e. Fin /\ sum_ k e. NN ( ( f ` k ) x. k ) = N ) }   &    |- O = { g e. P | A. n e. ( `' g " NN ) -. 2 || n }   &    |- D = { g e. P | A. n e. NN ( g ` n ) <_ 1 }   &    |- J = { z e. NN | -. 2 || z }   &    |- F = ( x e. J , y e. NN0 |-> ( ( 2 ^ y ) x. x ) )   &    |- H = { r e. ( ( ~P NN0 i^i Fin ) ^m J ) | ( r supp (/) ) e. Fin }   &    |- M = ( r e. H |-> { <. x , y >. | ( x e. J /\ y e. ( r ` x ) ) } )   &    |- R = { f | ( `' f " NN ) e. Fin }   &    |- T = { f e. ( NN0 ^m NN ) | ( `' f " NN ) C_ J }   &    |- G = ( o e. ( T i^i R ) |-> ( (𝟭 ` NN ) ` ( F " ( M ` (bits o. ( o |` J ) ) ) ) ) )   =>    |- G : ( T i^i R ) -1-1-onto-> ( ( { 0 , 1 } ^m NN ) i^i R )
Theorem	eulerpartlemgv 29151*	Lemma for eulerpart 29160: value of the function G. (Contributed by Thierry Arnoux, 13-Nov-2017.)
|- P = { f e. ( NN0 ^m NN ) | ( ( `' f " NN ) e. Fin /\ sum_ k e. NN ( ( f ` k ) x. k ) = N ) }   &    |- O = { g e. P | A. n e. ( `' g " NN ) -. 2 || n }   &    |- D = { g e. P | A. n e. NN ( g ` n ) <_ 1 }   &    |- J = { z e. NN | -. 2 || z }   &    |- F = ( x e. J , y e. NN0 |-> ( ( 2 ^ y ) x. x ) )   &    |- H = { r e. ( ( ~P NN0 i^i Fin ) ^m J ) | ( r supp (/) ) e. Fin }   &    |- M = ( r e. H |-> { <. x , y >. | ( x e. J /\ y e. ( r ` x ) ) } )   &    |- R = { f | ( `' f " NN ) e. Fin }   &    |- T = { f e. ( NN0 ^m NN ) | ( `' f " NN ) C_ J }   &    |- G = ( o e. ( T i^i R ) |-> ( (𝟭 ` NN ) ` ( F " ( M ` (bits o. ( o |` J ) ) ) ) ) )   =>    |- ( A e. ( T i^i R ) -> ( G ` A ) = ( (𝟭 ` NN ) ` ( F " ( M ` (bits o. ( A |` J ) ) ) ) ) )
Theorem	eulerpartlemr 29152*	Lemma for eulerpart 29160. (Contributed by Thierry Arnoux, 13-Nov-2017.)
|- P = { f e. ( NN0 ^m NN ) | ( ( `' f " NN ) e. Fin /\ sum_ k e. NN ( ( f ` k ) x. k ) = N ) }   &    |- O = { g e. P | A. n e. ( `' g " NN ) -. 2 || n }   &    |- D = { g e. P | A. n e. NN ( g ` n ) <_ 1 }   &    |- J = { z e. NN | -. 2 || z }   &    |- F = ( x e. J , y e. NN0 |-> ( ( 2 ^ y ) x. x ) )   &    |- H = { r e. ( ( ~P NN0 i^i Fin ) ^m J ) | ( r supp (/) ) e. Fin }   &    |- M = ( r e. H |-> { <. x , y >. | ( x e. J /\ y e. ( r ` x ) ) } )   &    |- R = { f | ( `' f " NN ) e. Fin }   &    |- T = { f e. ( NN0 ^m NN ) | ( `' f " NN ) C_ J }   &    |- G = ( o e. ( T i^i R ) |-> ( (𝟭 ` NN ) ` ( F " ( M ` (bits o. ( o |` J ) ) ) ) ) )   =>    |- O = ( ( T i^i R ) i^i P )
Theorem	eulerpartlemmf 29153*	Lemma for eulerpart 29160. (Contributed by Thierry Arnoux, 30-Aug-2018.) (Revised by Thierry Arnoux, 1-Sep-2019.)
|- P = { f e. ( NN0 ^m NN ) | ( ( `' f " NN ) e. Fin /\ sum_ k e. NN ( ( f ` k ) x. k ) = N ) }   &    |- O = { g e. P | A. n e. ( `' g " NN ) -. 2 || n }   &    |- D = { g e. P | A. n e. NN ( g ` n ) <_ 1 }   &    |- J = { z e. NN | -. 2 || z }   &    |- F = ( x e. J , y e. NN0 |-> ( ( 2 ^ y ) x. x ) )   &    |- H = { r e. ( ( ~P NN0 i^i Fin ) ^m J ) | ( r supp (/) ) e. Fin }   &    |- M = ( r e. H |-> { <. x , y >. | ( x e. J /\ y e. ( r ` x ) ) } )   &    |- R = { f | ( `' f " NN ) e. Fin }   &    |- T = { f e. ( NN0 ^m NN ) | ( `' f " NN ) C_ J }   &    |- G = ( o e. ( T i^i R ) |-> ( (𝟭 ` NN ) ` ( F " ( M ` (bits o. ( o |` J ) ) ) ) ) )   =>    |- ( A e. ( T i^i R ) -> (bits o. ( A |` J ) ) e. H )
Theorem	eulerpartlemgvv 29154*	Lemma for eulerpart 29160: value of the function G evaluated. (Contributed by Thierry Arnoux, 10-Aug-2018.)
|- P = { f e. ( NN0 ^m NN ) | ( ( `' f " NN ) e. Fin /\ sum_ k e. NN ( ( f ` k ) x. k ) = N ) }   &    |- O = { g e. P | A. n e. ( `' g " NN ) -. 2 || n }   &    |- D = { g e. P | A. n e. NN ( g ` n ) <_ 1 }   &    |- J = { z e. NN | -. 2 || z }   &    |- F = ( x e. J , y e. NN0 |-> ( ( 2 ^ y ) x. x ) )   &    |- H = { r e. ( ( ~P NN0 i^i Fin ) ^m J ) | ( r supp (/) ) e. Fin }   &    |- M = ( r e. H |-> { <. x , y >. | ( x e. J /\ y e. ( r ` x ) ) } )   &    |- R = { f | ( `' f " NN ) e. Fin }   &    |- T = { f e. ( NN0 ^m NN ) | ( `' f " NN ) C_ J }   &    |- G = ( o e. ( T i^i R ) |-> ( (𝟭 ` NN ) ` ( F " ( M ` (bits o. ( o |` J ) ) ) ) ) )   =>    |- ( ( A e. ( T i^i R ) /\ B e. NN ) -> ( ( G ` A ) ` B ) = if ( E. t e. NN E. n e. (bits ` ( A ` t ) ) ( ( 2 ^ n ) x. t ) = B , 1 , 0 ) )
Theorem	eulerpartlemgu 29155*	Lemma for eulerpart 29160: Rewriting the U set for an odd partition Note that interestingly, this proof reuses marypha2lem2 7896. (Contributed by Thierry Arnoux, 10-Aug-2018.)
|- P = { f e. ( NN0 ^m NN ) | ( ( `' f " NN ) e. Fin /\ sum_ k e. NN ( ( f ` k ) x. k ) = N ) }   &    |- O = { g e. P | A. n e. ( `' g " NN ) -. 2 || n }   &    |- D = { g e. P | A. n e. NN ( g ` n ) <_ 1 }   &    |- J = { z e. NN | -. 2 || z }   &    |- F = ( x e. J , y e. NN0 |-> ( ( 2 ^ y ) x. x ) )   &    |- H = { r e. ( ( ~P NN0 i^i Fin ) ^m J ) | ( r supp (/) ) e. Fin }   &    |- M = ( r e. H |-> { <. x , y >. | ( x e. J /\ y e. ( r ` x ) ) } )   &    |- R = { f | ( `' f " NN ) e. Fin }   &    |- T = { f e. ( NN0 ^m NN ) | ( `' f " NN ) C_ J }   &    |- G = ( o e. ( T i^i R ) |-> ( (𝟭 ` NN ) ` ( F " ( M ` (bits o. ( o |` J ) ) ) ) ) )   &    |- U = U_ t e. ( ( `' A " NN ) i^i J ) ( { t } X. (bits ` ( A ` t ) ) )   =>    |- ( A e. ( T i^i R ) -> U = { <. t , n >. | ( t e. ( ( `' A " NN ) i^i J ) /\ n e. ( (bits o. A ) ` t ) ) } )
Theorem	eulerpartlemgh 29156*	Lemma for eulerpart 29160: The F function is a bijection on the U subsets. (Contributed by Thierry Arnoux, 15-Aug-2018.)
|- P = { f e. ( NN0 ^m NN ) | ( ( `' f " NN ) e. Fin /\ sum_ k e. NN ( ( f ` k ) x. k ) = N ) }   &    |- O = { g e. P | A. n e. ( `' g " NN ) -. 2 || n }   &    |- D = { g e. P | A. n e. NN ( g ` n ) <_ 1 }   &    |- J = { z e. NN | -. 2 || z }   &    |- F = ( x e. J , y e. NN0 |-> ( ( 2 ^ y ) x. x ) )   &    |- H = { r e. ( ( ~P NN0 i^i Fin ) ^m J ) | ( r supp (/) ) e. Fin }   &    |- M = ( r e. H |-> { <. x , y >. | ( x e. J /\ y e. ( r ` x ) ) } )   &    |- R = { f | ( `' f " NN ) e. Fin }   &    |- T = { f e. ( NN0 ^m NN ) | ( `' f " NN ) C_ J }   &    |- G = ( o e. ( T i^i R ) |-> ( (𝟭 ` NN ) ` ( F " ( M ` (bits o. ( o |` J ) ) ) ) ) )   &    |- U = U_ t e. ( ( `' A " NN ) i^i J ) ( { t } X. (bits ` ( A ` t ) ) )   =>    |- ( A e. ( T i^i R ) -> ( F |` U ) : U -1-1-onto-> { m e. NN | E. t e. NN E. n e. (bits ` ( A ` t ) ) ( ( 2 ^ n ) x. t ) = m } )
Theorem	eulerpartlemgf 29157*	Lemma for eulerpart 29160: Images under G have finite support. (Contributed by Thierry Arnoux, 29-Aug-2018.)
|- P = { f e. ( NN0 ^m NN ) | ( ( `' f " NN ) e. Fin /\ sum_ k e. NN ( ( f ` k ) x. k ) = N ) }   &    |- O = { g e. P | A. n e. ( `' g " NN ) -. 2 || n }   &    |- D = { g e. P | A. n e. NN ( g ` n ) <_ 1 }   &    |- J = { z e. NN | -. 2 || z }   &    |- F = ( x e. J , y e. NN0 |-> ( ( 2 ^ y ) x. x ) )   &    |- H = { r e. ( ( ~P NN0 i^i Fin ) ^m J ) | ( r supp (/) ) e. Fin }   &    |- M = ( r e. H |-> { <. x , y >. | ( x e. J /\ y e. ( r ` x ) ) } )   &    |- R = { f | ( `' f " NN ) e. Fin }   &    |- T = { f e. ( NN0 ^m NN ) | ( `' f " NN ) C_ J }   &    |- G = ( o e. ( T i^i R ) |-> ( (𝟭 ` NN ) ` ( F " ( M ` (bits o. ( o |` J ) ) ) ) ) )   =>    |- ( A e. ( T i^i R ) -> ( `' ( G ` A ) " NN ) e. Fin )
Theorem	eulerpartlemgs2 29158*	Lemma for eulerpart 29160: The G function also preserves partition sums. (Contributed by Thierry Arnoux, 10-Sep-2017.)
|- P = { f e. ( NN0 ^m NN ) | ( ( `' f " NN ) e. Fin /\ sum_ k e. NN ( ( f ` k ) x. k ) = N ) }   &    |- O = { g e. P | A. n e. ( `' g " NN ) -. 2 || n }   &    |- D = { g e. P | A. n e. NN ( g ` n ) <_ 1 }   &    |- J = { z e. NN | -. 2 || z }   &    |- F = ( x e. J , y e. NN0 |-> ( ( 2 ^ y ) x. x ) )   &    |- H = { r e. ( ( ~P NN0 i^i Fin ) ^m J ) | ( r supp (/) ) e. Fin }   &    |- M = ( r e. H |-> { <. x , y >. | ( x e. J /\ y e. ( r ` x ) ) } )   &    |- R = { f | ( `' f " NN ) e. Fin }   &    |- T = { f e. ( NN0 ^m NN ) | ( `' f " NN ) C_ J }   &    |- G = ( o e. ( T i^i R ) |-> ( (𝟭 ` NN ) ` ( F " ( M ` (bits o. ( o |` J ) ) ) ) ) )   &    |- S = ( f e. ( ( NN0 ^m NN ) i^i R ) |-> sum_ k e. NN ( ( f ` k ) x. k ) )   =>    |- ( A e. ( T i^i R ) -> ( S ` ( G ` A ) ) = ( S ` A ) )
Theorem	eulerpartlemn 29159*	Lemma for eulerpart 29160. (Contributed by Thierry Arnoux, 30-Aug-2018.)
|- P = { f e. ( NN0 ^m NN ) | ( ( `' f " NN ) e. Fin /\ sum_ k e. NN ( ( f ` k ) x. k ) = N ) }   &    |- O = { g e. P | A. n e. ( `' g " NN ) -. 2 || n }   &    |- D = { g e. P | A. n e. NN ( g ` n ) <_ 1 }   &    |- J = { z e. NN | -. 2 || z }   &    |- F = ( x e. J , y e. NN0 |-> ( ( 2 ^ y ) x. x ) )   &    |- H = { r e. ( ( ~P NN0 i^i Fin ) ^m J ) | ( r supp (/) ) e. Fin }   &    |- M = ( r e. H |-> { <. x , y >. | ( x e. J /\ y e. ( r ` x ) ) } )   &    |- R = { f | ( `' f " NN ) e. Fin }   &    |- T = { f e. ( NN0 ^m NN ) | ( `' f " NN ) C_ J }   &    |- G = ( o e. ( T i^i R ) |-> ( (𝟭 ` NN ) ` ( F " ( M ` (bits o. ( o |` J ) ) ) ) ) )   &    |- S = ( f e. ( ( NN0 ^m NN ) i^i R ) |-> sum_ k e. NN ( ( f ` k ) x. k ) )   =>    |- ( G |` O ) : O -1-1-onto-> D
Theorem	eulerpart 29160*	Euler's theorem on partitions, also known as a special case of Glaisher's theorem. Let P be the set of all partitions of N, represented as multisets of positive integers, which is to say functions from NN to NN0 where the value of the function represents the number of repetitions of an individual element, and the sum of all the elements with repetition equals N. Then the set O of all partitions that only consist of odd numbers and the set D of all partitions which have no repeated elements have the same cardinality. This is Metamath 100 proof #45. (Contributed by Thierry Arnoux, 14-Aug-2018.) (Revised by Thierry Arnoux, 1-Sep-2019.)
|- P = { f e. ( NN0 ^m NN ) | ( ( `' f " NN ) e. Fin /\ sum_ k e. NN ( ( f ` k ) x. k ) = N ) }   &    |- O = { g e. P | A. n e. ( `' g " NN ) -. 2 || n }   &    |- D = { g e. P | A. n e. NN ( g ` n ) <_ 1 }   =>    |- ( # ` O ) = ( # ` D )
21.3.18  Sequences defined by strong recursion
Syntax	csseq 29161	Sequences defined by strong recursion.
class seqstr
Definition	df-sseq 29162*	Define a builder for sequences by strong recursion, i.e. by computing the value of the n-th element of the sequence from all preceding elements and not just the previous one. (Contributed by Thierry Arnoux, 21-Apr-2019.)
|- seqstr = ( m e. _V , f e. _V |-> ( m u. ( lastS o. seq ( # ` m ) ( ( x e. _V , y e. _V |-> ( x ++ <" ( f ` x ) "> ) ) , ( NN0 X. { ( m ++ <" ( f ` m ) "> ) } ) ) ) ) )
Theorem	subiwrd 29163	Lemma for sseqp1 29173. (Contributed by Thierry Arnoux, 25-Apr-2019.)
|- ( ph -> S e. _V )   &    |- ( ph -> F : NN0 --> S )   &    |- ( ph -> N e. NN0 )   =>    |- ( ph -> ( F |` ( 0..^ N ) ) e. Word S )
Theorem	subiwrdlen 29164	Length of a subword of an infinite word. (Contributed by Thierry Arnoux, 25-Apr-2019.)
|- ( ph -> S e. _V )   &    |- ( ph -> F : NN0 --> S )   &    |- ( ph -> N e. NN0 )   =>    |- ( ph -> ( # ` ( F |` ( 0..^ N ) ) ) = N )
Theorem	iwrdsplit 29165	Lemma for sseqp1 29173. (Contributed by Thierry Arnoux, 25-Apr-2019.)
|- ( ph -> S e. _V )   &    |- ( ph -> F : NN0 --> S )   &    |- ( ph -> N e. NN0 )   =>    |- ( ph -> ( F |` ( 0..^ ( N + 1 ) ) ) = ( ( F |` ( 0..^ N ) ) ++ <" ( F ` N ) "> ) )
Theorem	sseqval 29166*	Value of the strong sequence builder function. The set W represents here the words of length greater than or equal to the lenght of the initial sequence M. (Contributed by Thierry Arnoux, 21-Apr-2019.)
|- ( ph -> S e. _V )   &    |- ( ph -> M e. Word S )   &    |- W = (Word S i^i ( `' # " ( ZZ>= ` ( # ` M ) ) ) )   &    |- ( ph -> F : W --> S )   =>    |- ( ph -> ( Mseqstr F ) = ( M u. ( lastS o. seq ( # ` M ) ( ( x e. _V , y e. _V |-> ( x ++ <" ( F ` x ) "> ) ) , ( NN0 X. { ( M ++ <" ( F ` M ) "> ) } ) ) ) ) )
Theorem	sseqfv1 29167	Value of the strong sequence builder function at one of its initial values. (Contributed by Thierry Arnoux, 21-Apr-2019.)
|- ( ph -> S e. _V )   &    |- ( ph -> M e. Word S )   &    |- W = (Word S i^i ( `' # " ( ZZ>= ` ( # ` M ) ) ) )   &    |- ( ph -> F : W --> S )   &    |- ( ph -> N e. ( 0..^ ( # ` M ) ) )   =>    |- ( ph -> ( ( Mseqstr F ) ` N ) = ( M ` N ) )
Theorem	sseqfn 29168	A strong recursive sequence is a function over the nonnegative integers. (Contributed by Thierry Arnoux, 23-Apr-2019.)
|- ( ph -> S e. _V )   &    |- ( ph -> M e. Word S )   &    |- W = (Word S i^i ( `' # " ( ZZ>= ` ( # ` M ) ) ) )   &    |- ( ph -> F : W --> S )   =>    |- ( ph -> ( Mseqstr F ) Fn NN0 )
Theorem	sseqmw 29169	Lemma for sseqf 29170 amd sseqp1 29173. (Contributed by Thierry Arnoux, 25-Apr-2019.)
|- ( ph -> S e. _V )   &    |- ( ph -> M e. Word S )   &    |- W = (Word S i^i ( `' # " ( ZZ>= ` ( # ` M ) ) ) )   &    |- ( ph -> F : W --> S )   =>    |- ( ph -> M e. W )
Theorem	sseqf 29170	A strong recursive sequence is a function over the nonnegative integers. (Contributed by Thierry Arnoux, 23-Apr-2019.)
|- ( ph -> S e. _V )   &    |- ( ph -> M e. Word S )   &    |- W = (Word S i^i ( `' # " ( ZZ>= ` ( # ` M ) ) ) )   &    |- ( ph -> F : W --> S )   =>    |- ( ph -> ( Mseqstr F ) : NN0 --> S )
Theorem	sseqfres 29171	The first elements in the strong recursive sequence are the sequence initializer. (Contributed by Thierry Arnoux, 23-Apr-2019.)
|- ( ph -> S e. _V )   &    |- ( ph -> M e. Word S )   &    |- W = (Word S i^i ( `' # " ( ZZ>= ` ( # ` M ) ) ) )   &    |- ( ph -> F : W --> S )   =>    |- ( ph -> ( ( Mseqstr F ) |` ( 0..^ ( # ` M ) ) ) = M )
Theorem	sseqfv2 29172*	Value of the strong sequence builder function. (Contributed by Thierry Arnoux, 21-Apr-2019.)
|- ( ph -> S e. _V )   &    |- ( ph -> M e. Word S )   &    |- W = (Word S i^i ( `' # " ( ZZ>= ` ( # ` M ) ) ) )   &    |- ( ph -> F : W --> S )   &    |- ( ph -> N e. ( ZZ>= ` ( # ` M ) ) )   =>    |- ( ph -> ( ( Mseqstr F ) ` N ) = ( lastS ` ( seq ( # ` M ) ( ( x e. _V , y e. _V |-> ( x ++ <" ( F ` x ) "> ) ) , ( NN0 X. { ( M ++ <" ( F ` M ) "> ) } ) ) ` N ) ) )
Theorem	sseqp1 29173	Value of the strong sequence builder function at a successor. (Contributed by Thierry Arnoux, 24-Apr-2019.)
|- ( ph -> S e. _V )   &    |- ( ph -> M e. Word S )   &    |- W = (Word S i^i ( `' # " ( ZZ>= ` ( # ` M ) ) ) )   &    |- ( ph -> F : W --> S )   &    |- ( ph -> N e. ( ZZ>= ` ( # ` M ) ) )   =>    |- ( ph -> ( ( Mseqstr F ) ` N ) = ( F ` ( ( Mseqstr F ) |` ( 0..^ N ) ) ) )
21.3.19  Fibonacci Numbers
Syntax	cfib 29174	The Fibonacci sequence.
class Fibci
Definition	df-fib 29175	Define the Fibonacci sequence, where that each element is the sum of the two preceding ones, starting from 0 and 1. (Contributed by Thierry Arnoux, 25-Apr-2019.)
|- Fibci = ( <" 0 1 ">seqstr ( w e. (Word NN0 i^i ( `' # " ( ZZ>= ` 2 ) ) ) |-> ( ( w ` ( ( # ` w ) - 2 ) ) + ( w ` ( ( # ` w ) - 1 ) ) ) ) )
Theorem	fiblem 29176	Lemma for fib0 29177, fib1 29178 and fibp1 29179. (Contributed by Thierry Arnoux, 25-Apr-2019.)
|- ( w e. (Word NN0 i^i ( `' # " ( ZZ>= ` 2 ) ) ) |-> ( ( w ` ( ( # ` w ) - 2 ) ) + ( w ` ( ( # ` w ) - 1 ) ) ) ) : (Word NN0 i^i ( `' # " ( ZZ>= ` ( # ` <" 0 1 "> ) ) ) ) --> NN0
Theorem	fib0 29177	Value of the Fibonacci sequence at index 0. (Contributed by Thierry Arnoux, 25-Apr-2019.)
|- (Fibci ` 0 ) = 0
Theorem	fib1 29178	Value of the Fibonacci sequence at index 1. (Contributed by Thierry Arnoux, 25-Apr-2019.)
|- (Fibci ` 1 ) = 1
Theorem	fibp1 29179	Value of the Fibonacci sequence at higher indices. (Contributed by Thierry Arnoux, 25-Apr-2019.)
|- ( N e. NN -> (Fibci ` ( N + 1 ) ) = ( (Fibci ` ( N - 1 ) ) + (Fibci ` N ) ) )
Theorem	fib2 29180	Value of the Fibonacci sequence at index 2. (Contributed by Thierry Arnoux, 25-Apr-2019.)
|- (Fibci ` 2 ) = 1
Theorem	fib3 29181	Value of the Fibonacci sequence at index 3. (Contributed by Thierry Arnoux, 25-Apr-2019.)
|- (Fibci ` 3 ) = 2
Theorem	fib4 29182	Value of the Fibonacci sequence at index 4. (Contributed by Thierry Arnoux, 25-Apr-2019.)
|- (Fibci ` 4 ) = 3
Theorem	fib5 29183	Value of the Fibonacci sequence at index 5. (Contributed by Thierry Arnoux, 25-Apr-2019.)
|- (Fibci ` 5 ) = 5
Theorem	fib6 29184	Value of the Fibonacci sequence at index 6. (Contributed by Thierry Arnoux, 25-Apr-2019.)
|- (Fibci ` 6 ) = 8
21.3.20  Probability
21.3.20.1  Probability Theory
Syntax	cprb 29185	Extend class notation to include the class of probability measures.
class Prob
Definition	df-prob 29186	Define the class of probability measures as the set of measures with total measure 1. (Contributed by Thierry Arnoux, 14-Sep-2016.)
|- Prob = { p e. U. ran measures | ( p ` U. dom p ) = 1 }
Theorem	elprob 29187	The property of being a probability measure. (Contributed by Thierry Arnoux, 8-Dec-2016.)
|- ( P e. Prob <-> ( P e. U. ran measures /\ ( P ` U. dom P ) = 1 ) )
Theorem	domprobmeas 29188	A probability measure is a measure on its domain. (Contributed by Thierry Arnoux, 23-Dec-2016.)
|- ( P e. Prob -> P e. (measures ` dom P ) )
Theorem	domprobsiga 29189	The domain of a probability measure is a sigma-algebra. (Contributed by Thierry Arnoux, 23-Dec-2016.)
|- ( P e. Prob -> dom P e. U. ran sigAlgebra )
Theorem	probtot 29190	The probability of the universe set is 1. Second axiom of Kolmogorov. (Contributed by Thierry Arnoux, 8-Dec-2016.)
|- ( P e. Prob -> ( P ` U. dom P ) = 1 )
Theorem	prob01 29191	A probability is an element of [ 0 , 1 ]. First axiom of Kolmogorov. (Contributed by Thierry Arnoux, 25-Dec-2016.)
|- ( ( P e. Prob /\ A e. dom P ) -> ( P ` A ) e. ( 0 [,] 1 ) )
Theorem	probnul 29192	The probability of the empty event set is 0. (Contributed by Thierry Arnoux, 25-Dec-2016.)
|- ( P e. Prob -> ( P ` (/) ) = 0 )
Theorem	unveldomd 29193	The universe is an element of the domain of the probability, the universe (entire probability space) being U. dom P in our construction. (Contributed by Thierry Arnoux, 22-Jan-2017.)
|- ( ph -> P e. Prob )   =>    |- ( ph -> U. dom P e. dom P )
Theorem	unveldom 29194	The universe is an element of the domain of the probability, the universe (entire probability space) being U. dom P in our construction. (Contributed by Thierry Arnoux, 22-Jan-2017.)
|- ( P e. Prob -> U. dom P e. dom P )
Theorem	nuleldmp 29195	The empty set is an element of the domain of the probability. (Contributed by Thierry Arnoux, 22-Jan-2017.)
|- ( P e. Prob -> (/) e. dom P )
Theorem	probcun 29196*	The probability of the union of a countable disjoint set of events is the sum of their probabilities. (Third axiom of Kolmogorov) Here, the sum_ construct cannot be used as it can handle infinite indexing set only if they are subsets of ZZ, which is not the case here. (Contributed by Thierry Arnoux, 25-Dec-2016.)
|- ( ( P e. Prob /\ A e. ~P dom P /\ ( A ~<_ om /\ Disj x e. A x ) ) -> ( P ` U. A ) = Σ* x e. A ( P ` x ) )
Theorem	probun 29197	The probability of the union two incompatible events is the sum of their probabilities. (Contributed by Thierry Arnoux, 25-Dec-2016.)
|- ( ( P e. Prob /\ A e. dom P /\ B e. dom P ) -> ( ( A i^i B ) = (/) -> ( P ` ( A u. B ) ) = ( ( P ` A ) + ( P ` B ) ) ) )
Theorem	probdif 29198	The probability of the difference of two event sets. (Contributed by Thierry Arnoux, 12-Dec-2016.)
|- ( ( P e. Prob /\ A e. dom P /\ B e. dom P ) -> ( P ` ( A \ B ) ) = ( ( P ` A ) - ( P ` ( A i^i B ) ) ) )
Theorem	probinc 29199	A probability law is increasing with regard to event set inclusion. (Contributed by Thierry Arnoux, 10-Feb-2017.)
|- ( ( ( P e. Prob /\ A e. dom P /\ B e. dom P ) /\ A C_ B ) -> ( P ` A ) <_ ( P ` B ) )
Theorem	probdsb 29200	The probability of the complement of a set. That is, the probability that the event A does not occur. (Contributed by Thierry Arnoux, 15-Dec-2016.)
|- ( ( P e. Prob /\ A e. dom P ) -> ( P ` ( U. dom P \ A ) ) = ( 1 - ( P ` A ) ) )