P. 305 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 30401-30500   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	sibfinima 30401	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 30402	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 30403*	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 30404*	Closure of the Bochner integral on simple functions, generic version. See sitgclbn 30405 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 30405	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 30406	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 30407	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 30408	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 30409*	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 30410	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 30411*	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 30412	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 30413	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 30414	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 30415*	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 23392. (Contributed by Thierry Arnoux, 13-Feb-2018.)
|- itgm = ( w e. _V , m e. U. ran measures |-> ( ( (metUnif ` ( wsitm m ) )CnExt (UnifSt ` w ) ) ` ( wsitg m ) ) )
20.3.18  Euler's partition theorem
Theorem	oddpwdc 30416*	Lemma for eulerpart 30444. 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 30417*	Lemma for eulerpart 30444: 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 30418*	Lemma for eulerpart 30444. 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 30419*	Lemma for eulerpart 30444. (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 30420*	Lemma for eulerpart 30444. 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 30421*	Lemma for eulerpart 30444. (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 30422*	Lemma for eulerpart 30444. (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 30423*	Lemma for eulerpart 30444. 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 30424*	Lemma for eulerpart 30444. (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 30425*	Lemma for eulerpart 30444. (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 30426*	Lemma for eulerpart 30444. (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 30427*	Lemma for eulerpart 30444: 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 30428*	Lemma for eulerpart 30444: 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 30429*	Lemma for eulerpart 30444. (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 30430*	Lemma for eulerpart 30444. 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 30431*	Lemma for eulerpart 30444. (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 30432*	Lemma for eulerpart 30444: 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 30433*	Lemma for eulerpart 30444. (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 30434*	Lemma for eulerpart 30444: 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 30435*	Lemma for eulerpart 30444: 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 30436*	Lemma for eulerpart 30444. (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 30437*	Lemma for eulerpart 30444. (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 30438*	Lemma for eulerpart 30444: 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 30439*	Lemma for eulerpart 30444: Rewriting the U set for an odd partition Note that interestingly, this proof reuses marypha2lem2 8342. (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 30440*	Lemma for eulerpart 30444: 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 30441*	Lemma for eulerpart 30444: 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 30442*	Lemma for eulerpart 30444: 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 30443*	Lemma for eulerpart 30444. (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 30444*	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 )
20.3.19  Sequences defined by strong recursion
Syntax	csseq 30445	Sequences defined by strong recursion.
class seqstr
Definition	df-sseq 30446*	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 30447	Lemma for sseqp1 30457. (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 30448	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 30449	Lemma for sseqp1 30457. (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 30450*	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 30451	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 30452	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 30453	Lemma for sseqf 30454 amd sseqp1 30457. (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 30454	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 30455	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 30456*	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 30457	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 ) ) ) )
20.3.20  Fibonacci Numbers
Syntax	cfib 30458	The Fibonacci sequence.
class Fibci
Definition	df-fib 30459	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 30460	Lemma for fib0 30461, fib1 30462 and fibp1 30463. (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 30461	Value of the Fibonacci sequence at index 0. (Contributed by Thierry Arnoux, 25-Apr-2019.)
|- (Fibci ` 0 ) = 0
Theorem	fib1 30462	Value of the Fibonacci sequence at index 1. (Contributed by Thierry Arnoux, 25-Apr-2019.)
|- (Fibci ` 1 ) = 1
Theorem	fibp1 30463	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 30464	Value of the Fibonacci sequence at index 2. (Contributed by Thierry Arnoux, 25-Apr-2019.)
|- (Fibci ` 2 ) = 1
Theorem	fib3 30465	Value of the Fibonacci sequence at index 3. (Contributed by Thierry Arnoux, 25-Apr-2019.)
|- (Fibci ` 3 ) = 2
Theorem	fib4 30466	Value of the Fibonacci sequence at index 4. (Contributed by Thierry Arnoux, 25-Apr-2019.)
|- (Fibci ` 4 ) = 3
Theorem	fib5 30467	Value of the Fibonacci sequence at index 5. (Contributed by Thierry Arnoux, 25-Apr-2019.)
|- (Fibci ` 5 ) = 5
Theorem	fib6 30468	Value of the Fibonacci sequence at index 6. (Contributed by Thierry Arnoux, 25-Apr-2019.)
|- (Fibci ` 6 ) = 8
20.3.21  Probability
20.3.21.1  Probability Theory
Syntax	cprb 30469	Extend class notation to include the class of probability measures.
class Prob
Definition	df-prob 30470	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 30471	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 30472	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 30473	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 30474	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 30475	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 30476	The probability of the empty event set is 0. (Contributed by Thierry Arnoux, 25-Dec-2016.)
|- ( P e. Prob -> ( P ` (/) ) = 0 )
Theorem	unveldomd 30477	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 30478	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 30479	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 30480*	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 30481	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 30482	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 30483	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 30484	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 ) ) )
Theorem	probmeasd 30485	A probability measure is a measure. (Contributed by Thierry Arnoux, 2-Feb-2017.)
|- ( ph -> P e. Prob )   =>    |- ( ph -> P e. U. ran measures )
Theorem	probvalrnd 30486	The value of a probability is a real number. (Contributed by Thierry Arnoux, 2-Feb-2017.)
|- ( ph -> P e. Prob )   &    |- ( ph -> A e. dom P )   =>    |- ( ph -> ( P ` A ) e. RR )
Theorem	probtotrnd 30487	The probability of the universe set is finite. (Contributed by Thierry Arnoux, 2-Feb-2017.)
|- ( ph -> P e. Prob )   =>    |- ( ph -> ( P ` U. dom P ) e. RR )
Theorem	totprobd 30488*	Law of total probability, deduction form. (Contributed by Thierry Arnoux, 25-Dec-2016.)
|- ( ph -> P e. Prob )   &    |- ( ph -> A e. dom P )   &    |- ( ph -> B e. ~P dom P )   &    |- ( ph -> U. B = U. dom P )   &    |- ( ph -> B ~<_ om )   &    |- ( ph -> Disj b e. B b )   =>    |- ( ph -> ( P ` A ) = Σ* b e. B ( P ` ( b i^i A ) ) )
Theorem	totprob 30489*	Law of total probability. (Contributed by Thierry Arnoux, 25-Dec-2016.)
|- ( ( P e. Prob /\ A e. dom P /\ ( U. B = U. dom P /\ B e. ~P dom P /\ ( B ~<_ om /\ Disj b e. B b ) ) ) -> ( P ` A ) = Σ* b e. B ( P ` ( b i^i A ) ) )
Theorem	probfinmeasbOLD 30490*	Build a probability measure from a finite measure. (Contributed by Thierry Arnoux, 17-Dec-2016.) (New usage is discouraged.) (Proof modification is discouraged.)
|- ( ( M e. (measures ` S ) /\ ( M ` U. S ) e. RR+ ) -> ( x e. S |-> ( ( M ` x ) /𝑒 ( M ` U. S ) ) ) e. Prob )
Theorem	probfinmeasb 30491	Build a probability measure from a finite measure. (Contributed by Thierry Arnoux, 31-Jan-2017.)
|- ( ( M e. (measures ` S ) /\ ( M ` U. S ) e. RR+ ) -> ( M∘𝑓/𝑐 /𝑒 ( M ` U. S ) ) e. Prob )
Theorem	probmeasb 30492*	Build a probability from a measure and a set with finite measure. (Contributed by Thierry Arnoux, 25-Dec-2016.)
|- ( ( M e. (measures ` S ) /\ A e. S /\ ( M ` A ) e. RR+ ) -> ( x e. S |-> ( ( M ` ( x i^i A ) ) / ( M ` A ) ) ) e. Prob )
20.3.21.2  Conditional Probabilities
Syntax	ccprob 30493	Extends class notation with the conditional probability builder.
class cprob
Definition	df-cndprob 30494*	Define the conditional probability. (Contributed by Thierry Arnoux, 14-Sep-2016.) (Revised by Thierry Arnoux, 21-Jan-2017.)
|- cprob = ( p e. Prob |-> ( a e. dom p , b e. dom p |-> ( ( p ` ( a i^i b ) ) / ( p ` b ) ) ) )
Theorem	cndprobval 30495	The value of the conditional probability , i.e. the probability for the event A, given B, under the probability law P. (Contributed by Thierry Arnoux, 21-Jan-2017.)
|- ( ( P e. Prob /\ A e. dom P /\ B e. dom P ) -> ( (cprob ` P ) ` <. A , B >. ) = ( ( P ` ( A i^i B ) ) / ( P ` B ) ) )
Theorem	cndprobin 30496	An identity linking conditional probability and intersection. (Contributed by Thierry Arnoux, 13-Dec-2016.) (Revised by Thierry Arnoux, 21-Jan-2017.)
|- ( ( ( P e. Prob /\ A e. dom P /\ B e. dom P ) /\ ( P ` B ) =/= 0 ) -> ( ( (cprob ` P ) ` <. A , B >. ) x. ( P ` B ) ) = ( P ` ( A i^i B ) ) )
Theorem	cndprob01 30497	The conditional probability has values in [ 0 , 1 ]. (Contributed by Thierry Arnoux, 13-Dec-2016.) (Revised by Thierry Arnoux, 21-Jan-2017.)
|- ( ( ( P e. Prob /\ A e. dom P /\ B e. dom P ) /\ ( P ` B ) =/= 0 ) -> ( (cprob ` P ) ` <. A , B >. ) e. ( 0 [,] 1 ) )
Theorem	cndprobtot 30498	The conditional probability given a certain event is one. (Contributed by Thierry Arnoux, 20-Dec-2016.) (Revised by Thierry Arnoux, 21-Jan-2017.)
|- ( ( P e. Prob /\ A e. dom P /\ ( P ` A ) =/= 0 ) -> ( (cprob ` P ) ` <. U. dom P , A >. ) = 1 )
Theorem	cndprobnul 30499	The conditional probability given empty event is zero. (Contributed by Thierry Arnoux, 20-Dec-2016.) (Revised by Thierry Arnoux, 21-Jan-2017.)
|- ( ( P e. Prob /\ A e. dom P /\ ( P ` A ) =/= 0 ) -> ( (cprob ` P ) ` <. (/) , A >. ) = 0 )
Theorem	cndprobprob 30500*	The conditional probability defines a probability law. (Contributed by Thierry Arnoux, 23-Dec-2016.) (Revised by Thierry Arnoux, 21-Jan-2017.)
|- ( ( P e. Prob /\ B e. dom P /\ ( P ` B ) =/= 0 ) -> ( a e. dom P |-> ( (cprob ` P ) ` <. a , B >. ) ) e. Prob )