P. 306 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 30501-30600   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	bayesth 30501	Bayes Theorem. (Contributed by Thierry Arnoux, 20-Dec-2016.) (Revised by Thierry Arnoux, 21-Jan-2017.)
|- ( ( ( P e. Prob /\ A e. dom P /\ B e. dom P ) /\ ( P ` A ) =/= 0 /\ ( P ` B ) =/= 0 ) -> ( (cprob ` P ) ` <. A , B >. ) = ( ( ( (cprob ` P ) ` <. B , A >. ) x. ( P ` A ) ) / ( P ` B ) ) )
20.3.21.3  Real Valued Random Variables
Syntax	crrv 30502	Extend class notation with the class of real valued random variables.
class rRndVar
Definition	df-rrv 30503	In its generic definition, a random variable is a measurable function from a probability space to a Borel set. Here, we specifically target real-valued random variables, i.e. measurable function from a probability space to the Borel sigma-algebra on the set of real numbers. (Contributed by Thierry Arnoux, 20-Sep-2016.) (Revised by Thierry Arnoux, 25-Jan-2017.)
|- rRndVar = ( p e. Prob |-> ( dom pMblFnM𝔅ℝ ) )
Theorem	rrvmbfm 30504	A real-valued random variable is a measurable function from its sample space to the Borel sigma-algebra. (Contributed by Thierry Arnoux, 25-Jan-2017.)
|- ( ph -> P e. Prob )   =>    |- ( ph -> ( X e. (rRndVar ` P ) <-> X e. ( dom PMblFnM𝔅ℝ ) ) )
Theorem	isrrvv 30505*	Elementhood to the set of real-valued random variables with respect to the probability P. (Contributed by Thierry Arnoux, 25-Jan-2017.)
|- ( ph -> P e. Prob )   =>    |- ( ph -> ( X e. (rRndVar ` P ) <-> ( X : U. dom P --> RR /\ A. y e. 𝔅ℝ ( `' X " y ) e. dom P ) ) )
Theorem	rrvvf 30506	A real-valued random variable is a function. (Contributed by Thierry Arnoux, 25-Jan-2017.)
|- ( ph -> P e. Prob )   &    |- ( ph -> X e. (rRndVar ` P ) )   =>    |- ( ph -> X : U. dom P --> RR )
Theorem	rrvfn 30507	A real-valued random variable is a function over the universe. (Contributed by Thierry Arnoux, 25-Jan-2017.)
|- ( ph -> P e. Prob )   &    |- ( ph -> X e. (rRndVar ` P ) )   =>    |- ( ph -> X Fn U. dom P )
Theorem	rrvdm 30508	The domain of a random variable is the universe. (Contributed by Thierry Arnoux, 25-Jan-2017.)
|- ( ph -> P e. Prob )   &    |- ( ph -> X e. (rRndVar ` P ) )   =>    |- ( ph -> dom X = U. dom P )
Theorem	rrvrnss 30509	The range of a random variable as a subset of RR. (Contributed by Thierry Arnoux, 6-Feb-2017.)
|- ( ph -> P e. Prob )   &    |- ( ph -> X e. (rRndVar ` P ) )   =>    |- ( ph -> ran X C_ RR )
Theorem	rrvf2 30510	A real-valued random variable is a function. (Contributed by Thierry Arnoux, 25-Jan-2017.)
|- ( ph -> P e. Prob )   &    |- ( ph -> X e. (rRndVar ` P ) )   =>    |- ( ph -> X : dom X --> RR )
Theorem	rrvdmss 30511	The domain of a random variable. This is useful to shorten proofs. (Contributed by Thierry Arnoux, 25-Jan-2017.)
|- ( ph -> P e. Prob )   &    |- ( ph -> X e. (rRndVar ` P ) )   =>    |- ( ph -> U. dom P C_ dom X )
Theorem	rrvfinvima 30512*	For a real-value random variable X, any open interval in RR is the image of a measurable set. (Contributed by Thierry Arnoux, 25-Jan-2017.)
|- ( ph -> P e. Prob )   &    |- ( ph -> X e. (rRndVar ` P ) )   =>    |- ( ph -> A. y e. 𝔅ℝ ( `' X " y ) e. dom P )
Theorem	0rrv 30513*	The constant function equal to zero is a random variable. (Contributed by Thierry Arnoux, 16-Jan-2017.) (Revised by Thierry Arnoux, 30-Jan-2017.)
|- ( ph -> P e. Prob )   =>    |- ( ph -> ( x e. U. dom P |-> 0 ) e. (rRndVar ` P ) )
Theorem	rrvadd 30514	The sum of two random variables is a random variable. (Contributed by Thierry Arnoux, 4-Jun-2017.)
|- ( ph -> P e. Prob )   &    |- ( ph -> X e. (rRndVar ` P ) )   &    |- ( ph -> Y e. (rRndVar ` P ) )   =>    |- ( ph -> ( X oF + Y ) e. (rRndVar ` P ) )
Theorem	rrvmulc 30515	A random variable multiplied by a constant is a random variable. (Contributed by Thierry Arnoux, 17-Jan-2017.) (Revised by Thierry Arnoux, 22-May-2017.)
|- ( ph -> P e. Prob )   &    |- ( ph -> X e. (rRndVar ` P ) )   &    |- ( ph -> C e. RR )   =>    |- ( ph -> ( X∘𝑓/𝑐 x. C ) e. (rRndVar ` P ) )
Theorem	rrvsum 30516	An indexed sum of random variables is a random variable. (Contributed by Thierry Arnoux, 22-May-2017.)
|- ( ph -> P e. Prob )   &    |- ( ph -> X : NN --> (rRndVar ` P ) )   &    |- ( ( ph /\ N e. NN ) -> S = ( seq 1 ( oF + , X ) ` N ) )   =>    |- ( ( ph /\ N e. NN ) -> S e. (rRndVar ` P ) )
20.3.21.4  Preimage set mapping operator
Syntax	corvc 30517	Extend class notation to include the preimage set mapping operator.
class ∘RV/𝑐 R
Definition	df-orvc 30518*	Define the preimage set mapping operator. In probability theory, the notation P ( X = A ) denotes the probability that a random variable X takes the value A. We introduce here an operator which enables to write this in Metamath as ( P ` ( X∘RV/𝑐 _I A ) ), and keep a similar notation. Because with this notation ( X∘RV/𝑐 _I A ) is a set, we can also apply it to conditional probabilities, like in ( P ` ( X∘RV/𝑐 _I A ) | ( Y∘RV/𝑐 _I B ) ) ). The oRVC operator transforms a relation R into an operation taking a random variable X and a constant C, and returning the preimage through X of the equivalence class of C. The most commonly used relations are: - equality: { X = A } as ( X∘RV/𝑐 _I A ) cf. ideq 5274- elementhood: { X e. A } as ( X∘RV/𝑐 _E A ) cf. epel 5032- less-than: { X <_ A } as ( X∘RV/𝑐 <_ A ) Even though it is primarily designed to be used within probability theory and with random variables, this operator is defined on generic functions, and could be used in other fields, e.g. for continuous functions. (Contributed by Thierry Arnoux, 15-Jan-2017.)
|- ∘RV/𝑐 R = ( x e. { x | Fun x } , a e. _V |-> ( `' x " { y | y R a } ) )
Theorem	orvcval 30519*	Value of the preimage mapping operator applied on a given random variable and constant. (Contributed by Thierry Arnoux, 19-Jan-2017.)
|- ( ph -> Fun X )   &    |- ( ph -> X e. V )   &    |- ( ph -> A e. W )   =>    |- ( ph -> ( X∘RV/𝑐 R A ) = ( `' X " { y | y R A } ) )
Theorem	orvcval2 30520*	Another way to express the value of the preimage mapping operator. (Contributed by Thierry Arnoux, 19-Jan-2017.)
|- ( ph -> Fun X )   &    |- ( ph -> X e. V )   &    |- ( ph -> A e. W )   =>    |- ( ph -> ( X∘RV/𝑐 R A ) = { z e. dom X | ( X ` z ) R A } )
Theorem	elorvc 30521*	Elementhood of a preimage. (Contributed by Thierry Arnoux, 21-Jan-2017.)
|- ( ph -> Fun X )   &    |- ( ph -> X e. V )   &    |- ( ph -> A e. W )   =>    |- ( ( ph /\ z e. dom X ) -> ( z e. ( X∘RV/𝑐 R A ) <-> ( X ` z ) R A ) )
Theorem	orvcval4 30522*	The value of the preimage mapping operator can be restricted to preimages in the base set of the topology. Cf. orvcval 30519. (Contributed by Thierry Arnoux, 21-Jan-2017.)
|- ( ph -> S e. U. ran sigAlgebra )   &    |- ( ph -> J e. Top )   &    |- ( ph -> X e. ( SMblFnM (sigaGen ` J ) ) )   &    |- ( ph -> A e. V )   =>    |- ( ph -> ( X∘RV/𝑐 R A ) = ( `' X " { y e. U. J | y R A } ) )
Theorem	orvcoel 30523*	If the relation produces open sets, preimage maps by a measurable function are measurable sets. (Contributed by Thierry Arnoux, 21-Jan-2017.)
|- ( ph -> S e. U. ran sigAlgebra )   &    |- ( ph -> J e. Top )   &    |- ( ph -> X e. ( SMblFnM (sigaGen ` J ) ) )   &    |- ( ph -> A e. V )   &    |- ( ph -> { y e. U. J | y R A } e. J )   =>    |- ( ph -> ( X∘RV/𝑐 R A ) e. S )
Theorem	orvccel 30524*	If the relation produces closed sets, preimage maps by a measurable function are measurable sets. (Contributed by Thierry Arnoux, 21-Jan-2017.)
|- ( ph -> S e. U. ran sigAlgebra )   &    |- ( ph -> J e. Top )   &    |- ( ph -> X e. ( SMblFnM (sigaGen ` J ) ) )   &    |- ( ph -> A e. V )   &    |- ( ph -> { y e. U. J | y R A } e. ( Clsd ` J ) )   =>    |- ( ph -> ( X∘RV/𝑐 R A ) e. S )
Theorem	elorrvc 30525*	Elementhood of a preimage for a real-valued random variable. (Contributed by Thierry Arnoux, 21-Jan-2017.)
|- ( ph -> P e. Prob )   &    |- ( ph -> X e. (rRndVar ` P ) )   &    |- ( ph -> A e. V )   =>    |- ( ( ph /\ z e. U. dom P ) -> ( z e. ( X∘RV/𝑐 R A ) <-> ( X ` z ) R A ) )
Theorem	orrvcval4 30526*	The value of the preimage mapping operator can be restricted to preimages of subsets of RR. (Contributed by Thierry Arnoux, 21-Jan-2017.)
|- ( ph -> P e. Prob )   &    |- ( ph -> X e. (rRndVar ` P ) )   &    |- ( ph -> A e. V )   =>    |- ( ph -> ( X∘RV/𝑐 R A ) = ( `' X " { y e. RR | y R A } ) )
Theorem	orrvcoel 30527*	If the relation produces open sets, preimage maps of a random variable are measurable sets. (Contributed by Thierry Arnoux, 21-Jan-2017.)
|- ( ph -> P e. Prob )   &    |- ( ph -> X e. (rRndVar ` P ) )   &    |- ( ph -> A e. V )   &    |- ( ph -> { y e. RR | y R A } e. ( topGen ` ran (,) ) )   =>    |- ( ph -> ( X∘RV/𝑐 R A ) e. dom P )
Theorem	orrvccel 30528*	If the relation produces closed sets, preimage maps are measurable sets. (Contributed by Thierry Arnoux, 21-Jan-2017.)
|- ( ph -> P e. Prob )   &    |- ( ph -> X e. (rRndVar ` P ) )   &    |- ( ph -> A e. V )   &    |- ( ph -> { y e. RR | y R A } e. ( Clsd ` ( topGen ` ran (,) ) ) )   =>    |- ( ph -> ( X∘RV/𝑐 R A ) e. dom P )
Theorem	orvcgteel 30529	Preimage maps produced by the "greater than or equal" relation are measurable sets. (Contributed by Thierry Arnoux, 5-Feb-2017.)
|- ( ph -> P e. Prob )   &    |- ( ph -> X e. (rRndVar ` P ) )   &    |- ( ph -> A e. RR )   =>    |- ( ph -> ( X∘RV/𝑐 `' <_ A ) e. dom P )
20.3.21.5  Distribution Functions
Theorem	orvcelval 30530	Preimage maps produced by the membership relation. (Contributed by Thierry Arnoux, 6-Feb-2017.)
|- ( ph -> P e. Prob )   &    |- ( ph -> X e. (rRndVar ` P ) )   &    |- ( ph -> A e. 𝔅ℝ )   =>    |- ( ph -> ( X∘RV/𝑐 _E A ) = ( `' X " A ) )
Theorem	orvcelel 30531	Preimage maps produced by the membership relation are measurable sets. (Contributed by Thierry Arnoux, 5-Feb-2017.)
|- ( ph -> P e. Prob )   &    |- ( ph -> X e. (rRndVar ` P ) )   &    |- ( ph -> A e. 𝔅ℝ )   =>    |- ( ph -> ( X∘RV/𝑐 _E A ) e. dom P )
Theorem	dstrvval 30532*	The value of the distribution of a random variable. (Contributed by Thierry Arnoux, 9-Feb-2017.)
|- ( ph -> P e. Prob )   &    |- ( ph -> X e. (rRndVar ` P ) )   &    |- ( ph -> D = ( a e. 𝔅ℝ |-> ( P ` ( X∘RV/𝑐 _E a ) ) ) )   &    |- ( ph -> A e. 𝔅ℝ )   =>    |- ( ph -> ( D ` A ) = ( P ` ( `' X " A ) ) )
Theorem	dstrvprob 30533*	The distribution of a random variable is a probability law. (TODO: could be shortened using dstrvval 30532) (Contributed by Thierry Arnoux, 10-Feb-2017.)
|- ( ph -> P e. Prob )   &    |- ( ph -> X e. (rRndVar ` P ) )   &    |- ( ph -> D = ( a e. 𝔅ℝ |-> ( P ` ( X∘RV/𝑐 _E a ) ) ) )   =>    |- ( ph -> D e. Prob )
20.3.21.6  Cumulative Distribution Functions
Theorem	orvclteel 30534	Preimage maps produced by the "lower than or equal" relation are measurable sets. (Contributed by Thierry Arnoux, 4-Feb-2017.)
|- ( ph -> P e. Prob )   &    |- ( ph -> X e. (rRndVar ` P ) )   &    |- ( ph -> A e. RR )   =>    |- ( ph -> ( X∘RV/𝑐 <_ A ) e. dom P )
Theorem	dstfrvel 30535	Elementhood of preimage maps produced by the "lower than or equal" relation. (Contributed by Thierry Arnoux, 13-Feb-2017.)
|- ( ph -> P e. Prob )   &    |- ( ph -> X e. (rRndVar ` P ) )   &    |- ( ph -> A e. RR )   &    |- ( ph -> B e. U. dom P )   &    |- ( ph -> ( X ` B ) <_ A )   =>    |- ( ph -> B e. ( X∘RV/𝑐 <_ A ) )
Theorem	dstfrvunirn 30536*	The limit of all preimage maps by the "lower than or equal" relation is the universe. (Contributed by Thierry Arnoux, 12-Feb-2017.)
|- ( ph -> P e. Prob )   &    |- ( ph -> X e. (rRndVar ` P ) )   =>    |- ( ph -> U. ran ( n e. NN |-> ( X∘RV/𝑐 <_ n ) ) = U. dom P )
Theorem	orvclteinc 30537	Preimage maps produced by the "lower than or equal" relation are increasing. (Contributed by Thierry Arnoux, 11-Feb-2017.)
|- ( ph -> P e. Prob )   &    |- ( ph -> X e. (rRndVar ` P ) )   &    |- ( ph -> A e. RR )   &    |- ( ph -> B e. RR )   &    |- ( ph -> A <_ B )   =>    |- ( ph -> ( X∘RV/𝑐 <_ A ) C_ ( X∘RV/𝑐 <_ B ) )
Theorem	dstfrvinc 30538*	A cumulative distribution function is non-decreasing. (Contributed by Thierry Arnoux, 11-Feb-2017.)
|- ( ph -> P e. Prob )   &    |- ( ph -> X e. (rRndVar ` P ) )   &    |- ( ph -> F = ( x e. RR |-> ( P ` ( X∘RV/𝑐 <_ x ) ) ) )   &    |- ( ph -> A e. RR )   &    |- ( ph -> B e. RR )   &    |- ( ph -> A <_ B )   =>    |- ( ph -> ( F ` A ) <_ ( F ` B ) )
Theorem	dstfrvclim1 30539*	The limit of the cumulative distribution function is one. (Contributed by Thierry Arnoux, 12-Feb-2017.) (Revised by Thierry Arnoux, 11-Jul-2017.)
|- ( ph -> P e. Prob )   &    |- ( ph -> X e. (rRndVar ` P ) )   &    |- ( ph -> F = ( x e. RR |-> ( P ` ( X∘RV/𝑐 <_ x ) ) ) )   =>    |- ( ph -> F ~~> 1 )
20.3.21.7  Probabilities - example
Theorem	coinfliplem 30540	Division in the extended real numbers can be used for the coin-flip example. (Contributed by Thierry Arnoux, 15-Jan-2017.)
|- H e. _V   &    |- T e. _V   &    |- H =/= T   &    |- P = ( ( # |` ~P { H , T } )∘𝑓/𝑐 / 2 )   &    |- X = { <. H , 1 >. , <. T , 0 >. }   =>    |- P = ( ( # |` ~P { H , T } )∘𝑓/𝑐 /𝑒 2 )
Theorem	coinflipprob 30541	The P we defined for coin-flip is a probability law. (Contributed by Thierry Arnoux, 15-Jan-2017.)
|- H e. _V   &    |- T e. _V   &    |- H =/= T   &    |- P = ( ( # |` ~P { H , T } )∘𝑓/𝑐 / 2 )   &    |- X = { <. H , 1 >. , <. T , 0 >. }   =>    |- P e. Prob
Theorem	coinflipspace 30542	The space of our coin-flip probability. (Contributed by Thierry Arnoux, 15-Jan-2017.)
|- H e. _V   &    |- T e. _V   &    |- H =/= T   &    |- P = ( ( # |` ~P { H , T } )∘𝑓/𝑐 / 2 )   &    |- X = { <. H , 1 >. , <. T , 0 >. }   =>    |- dom P = ~P { H , T }
Theorem	coinflipuniv 30543	The universe of our coin-flip probability is { H , T }. (Contributed by Thierry Arnoux, 15-Jan-2017.)
|- H e. _V   &    |- T e. _V   &    |- H =/= T   &    |- P = ( ( # |` ~P { H , T } )∘𝑓/𝑐 / 2 )   &    |- X = { <. H , 1 >. , <. T , 0 >. }   =>    |- U. dom P = { H , T }
Theorem	coinfliprv 30544	The X we defined for coin-flip is a random variable. (Contributed by Thierry Arnoux, 12-Jan-2017.)
|- H e. _V   &    |- T e. _V   &    |- H =/= T   &    |- P = ( ( # |` ~P { H , T } )∘𝑓/𝑐 / 2 )   &    |- X = { <. H , 1 >. , <. T , 0 >. }   =>    |- X e. (rRndVar ` P )
Theorem	coinflippv 30545	The probability of heads is one-half. (Contributed by Thierry Arnoux, 15-Jan-2017.)
|- H e. _V   &    |- T e. _V   &    |- H =/= T   &    |- P = ( ( # |` ~P { H , T } )∘𝑓/𝑐 / 2 )   &    |- X = { <. H , 1 >. , <. T , 0 >. }   =>    |- ( P ` { H } ) = ( 1 / 2 )
Theorem	coinflippvt 30546	The probability of tails is one-half. (Contributed by Thierry Arnoux, 5-Feb-2017.)
|- H e. _V   &    |- T e. _V   &    |- H =/= T   &    |- P = ( ( # |` ~P { H , T } )∘𝑓/𝑐 / 2 )   &    |- X = { <. H , 1 >. , <. T , 0 >. }   =>    |- ( P ` { T } ) = ( 1 / 2 )
20.3.21.8  Bertrand's Ballot Problem
Theorem	ballotlemoex 30547*	O is a set. (Contributed by Thierry Arnoux, 7-Dec-2016.)
|- M e. NN   &    |- N e. NN   &    |- O = { c e. ~P ( 1 ... ( M + N ) ) | ( # ` c ) = M }   =>    |- O e. _V
Theorem	ballotlem1 30548*	The size of the universe is a binomial coefficient. (Contributed by Thierry Arnoux, 23-Nov-2016.)
|- M e. NN   &    |- N e. NN   &    |- O = { c e. ~P ( 1 ... ( M + N ) ) | ( # ` c ) = M }   =>    |- ( # ` O ) = ( ( M + N ) _C M )
Theorem	ballotlemelo 30549*	Elementhood in O. (Contributed by Thierry Arnoux, 17-Apr-2017.)
|- M e. NN   &    |- N e. NN   &    |- O = { c e. ~P ( 1 ... ( M + N ) ) | ( # ` c ) = M }   =>    |- ( C e. O <-> ( C C_ ( 1 ... ( M + N ) ) /\ ( # ` C ) = M ) )
Theorem	ballotlem2 30550*	The probability that the first vote picked in a count is a B. (Contributed by Thierry Arnoux, 23-Nov-2016.)
|- M e. NN   &    |- N e. NN   &    |- O = { c e. ~P ( 1 ... ( M + N ) ) | ( # ` c ) = M }   &    |- P = ( x e. ~P O |-> ( ( # ` x ) / ( # ` O ) ) )   =>    |- ( P ` { c e. O | -. 1 e. c } ) = ( N / ( M + N ) )
Theorem	ballotlemfval 30551*	The value of F. (Contributed by Thierry Arnoux, 23-Nov-2016.)
|- M e. NN   &    |- N e. NN   &    |- O = { c e. ~P ( 1 ... ( M + N ) ) | ( # ` c ) = M }   &    |- P = ( x e. ~P O |-> ( ( # ` x ) / ( # ` O ) ) )   &    |- F = ( c e. O |-> ( i e. ZZ |-> ( ( # ` ( ( 1 ... i ) i^i c ) ) - ( # ` ( ( 1 ... i ) \ c ) ) ) ) )   &    |- ( ph -> C e. O )   &    |- ( ph -> J e. ZZ )   =>    |- ( ph -> ( ( F ` C ) ` J ) = ( ( # ` ( ( 1 ... J ) i^i C ) ) - ( # ` ( ( 1 ... J ) \ C ) ) ) )
Theorem	ballotlemfelz 30552*	( F ` C ) has values in ZZ. (Contributed by Thierry Arnoux, 23-Nov-2016.)
|- M e. NN   &    |- N e. NN   &    |- O = { c e. ~P ( 1 ... ( M + N ) ) | ( # ` c ) = M }   &    |- P = ( x e. ~P O |-> ( ( # ` x ) / ( # ` O ) ) )   &    |- F = ( c e. O |-> ( i e. ZZ |-> ( ( # ` ( ( 1 ... i ) i^i c ) ) - ( # ` ( ( 1 ... i ) \ c ) ) ) ) )   &    |- ( ph -> C e. O )   &    |- ( ph -> J e. ZZ )   =>    |- ( ph -> ( ( F ` C ) ` J ) e. ZZ )
Theorem	ballotlemfp1 30553*	If the J th ballot is for A, ( F ` C ) goes up 1. If the J th ballot is for B, ( F ` C ) goes down 1. (Contributed by Thierry Arnoux, 24-Nov-2016.)
|- M e. NN   &    |- N e. NN   &    |- O = { c e. ~P ( 1 ... ( M + N ) ) | ( # ` c ) = M }   &    |- P = ( x e. ~P O |-> ( ( # ` x ) / ( # ` O ) ) )   &    |- F = ( c e. O |-> ( i e. ZZ |-> ( ( # ` ( ( 1 ... i ) i^i c ) ) - ( # ` ( ( 1 ... i ) \ c ) ) ) ) )   &    |- ( ph -> C e. O )   &    |- ( ph -> J e. NN )   =>    |- ( ph -> ( ( -. J e. C -> ( ( F ` C ) ` J ) = ( ( ( F ` C ) ` ( J - 1 ) ) - 1 ) ) /\ ( J e. C -> ( ( F ` C ) ` J ) = ( ( ( F ` C ) ` ( J - 1 ) ) + 1 ) ) ) )
Theorem	ballotlemfc0 30554*	F takes value 0 between negative and positive values. (Contributed by Thierry Arnoux, 24-Nov-2016.)
|- M e. NN   &    |- N e. NN   &    |- O = { c e. ~P ( 1 ... ( M + N ) ) | ( # ` c ) = M }   &    |- P = ( x e. ~P O |-> ( ( # ` x ) / ( # ` O ) ) )   &    |- F = ( c e. O |-> ( i e. ZZ |-> ( ( # ` ( ( 1 ... i ) i^i c ) ) - ( # ` ( ( 1 ... i ) \ c ) ) ) ) )   &    |- ( ph -> C e. O )   &    |- ( ph -> J e. NN )   &    |- ( ph -> E. i e. ( 1 ... J ) ( ( F ` C ) ` i ) <_ 0 )   &    |- ( ph -> 0 < ( ( F ` C ) ` J ) )   =>    |- ( ph -> E. k e. ( 1 ... J ) ( ( F ` C ) ` k ) = 0 )
Theorem	ballotlemfcc 30555*	F takes value 0 between positive and negative values. (Contributed by Thierry Arnoux, 2-Apr-2017.)
|- M e. NN   &    |- N e. NN   &    |- O = { c e. ~P ( 1 ... ( M + N ) ) | ( # ` c ) = M }   &    |- P = ( x e. ~P O |-> ( ( # ` x ) / ( # ` O ) ) )   &    |- F = ( c e. O |-> ( i e. ZZ |-> ( ( # ` ( ( 1 ... i ) i^i c ) ) - ( # ` ( ( 1 ... i ) \ c ) ) ) ) )   &    |- ( ph -> C e. O )   &    |- ( ph -> J e. NN )   &    |- ( ph -> E. i e. ( 1 ... J ) 0 <_ ( ( F ` C ) ` i ) )   &    |- ( ph -> ( ( F ` C ) ` J ) < 0 )   =>    |- ( ph -> E. k e. ( 1 ... J ) ( ( F ` C ) ` k ) = 0 )
Theorem	ballotlemfmpn 30556*	( F ` C ) finishes counting at ( M - N ). (Contributed by Thierry Arnoux, 25-Nov-2016.)
|- M e. NN   &    |- N e. NN   &    |- O = { c e. ~P ( 1 ... ( M + N ) ) | ( # ` c ) = M }   &    |- P = ( x e. ~P O |-> ( ( # ` x ) / ( # ` O ) ) )   &    |- F = ( c e. O |-> ( i e. ZZ |-> ( ( # ` ( ( 1 ... i ) i^i c ) ) - ( # ` ( ( 1 ... i ) \ c ) ) ) ) )   =>    |- ( C e. O -> ( ( F ` C ) ` ( M + N ) ) = ( M - N ) )
Theorem	ballotlemfval0 30557*	( F ` C ) always starts counting at 0 . (Contributed by Thierry Arnoux, 25-Nov-2016.)
|- M e. NN   &    |- N e. NN   &    |- O = { c e. ~P ( 1 ... ( M + N ) ) | ( # ` c ) = M }   &    |- P = ( x e. ~P O |-> ( ( # ` x ) / ( # ` O ) ) )   &    |- F = ( c e. O |-> ( i e. ZZ |-> ( ( # ` ( ( 1 ... i ) i^i c ) ) - ( # ` ( ( 1 ... i ) \ c ) ) ) ) )   =>    |- ( C e. O -> ( ( F ` C ) ` 0 ) = 0 )
Theorem	ballotleme 30558*	Elements of E. (Contributed by Thierry Arnoux, 14-Dec-2016.)
|- M e. NN   &    |- N e. NN   &    |- O = { c e. ~P ( 1 ... ( M + N ) ) | ( # ` c ) = M }   &    |- P = ( x e. ~P O |-> ( ( # ` x ) / ( # ` O ) ) )   &    |- F = ( c e. O |-> ( i e. ZZ |-> ( ( # ` ( ( 1 ... i ) i^i c ) ) - ( # ` ( ( 1 ... i ) \ c ) ) ) ) )   &    |- E = { c e. O | A. i e. ( 1 ... ( M + N ) ) 0 < ( ( F ` c ) ` i ) }   =>    |- ( C e. E <-> ( C e. O /\ A. i e. ( 1 ... ( M + N ) ) 0 < ( ( F ` C ) ` i ) ) )
Theorem	ballotlemodife 30559*	Elements of ( O \ E ). (Contributed by Thierry Arnoux, 7-Dec-2016.)
|- M e. NN   &    |- N e. NN   &    |- O = { c e. ~P ( 1 ... ( M + N ) ) | ( # ` c ) = M }   &    |- P = ( x e. ~P O |-> ( ( # ` x ) / ( # ` O ) ) )   &    |- F = ( c e. O |-> ( i e. ZZ |-> ( ( # ` ( ( 1 ... i ) i^i c ) ) - ( # ` ( ( 1 ... i ) \ c ) ) ) ) )   &    |- E = { c e. O | A. i e. ( 1 ... ( M + N ) ) 0 < ( ( F ` c ) ` i ) }   =>    |- ( C e. ( O \ E ) <-> ( C e. O /\ E. i e. ( 1 ... ( M + N ) ) ( ( F ` C ) ` i ) <_ 0 ) )
Theorem	ballotlem4 30560*	If the first pick is a vote for B, A is not ahead throughout the count. (Contributed by Thierry Arnoux, 25-Nov-2016.)
|- M e. NN   &    |- N e. NN   &    |- O = { c e. ~P ( 1 ... ( M + N ) ) | ( # ` c ) = M }   &    |- P = ( x e. ~P O |-> ( ( # ` x ) / ( # ` O ) ) )   &    |- F = ( c e. O |-> ( i e. ZZ |-> ( ( # ` ( ( 1 ... i ) i^i c ) ) - ( # ` ( ( 1 ... i ) \ c ) ) ) ) )   &    |- E = { c e. O | A. i e. ( 1 ... ( M + N ) ) 0 < ( ( F ` c ) ` i ) }   =>    |- ( C e. O -> ( -. 1 e. C -> -. C e. E ) )
Theorem	ballotlem5 30561*	If A is not ahead throughout, there is a k where votes are tied. (Contributed by Thierry Arnoux, 1-Dec-2016.)
|- M e. NN   &    |- N e. NN   &    |- O = { c e. ~P ( 1 ... ( M + N ) ) | ( # ` c ) = M }   &    |- P = ( x e. ~P O |-> ( ( # ` x ) / ( # ` O ) ) )   &    |- F = ( c e. O |-> ( i e. ZZ |-> ( ( # ` ( ( 1 ... i ) i^i c ) ) - ( # ` ( ( 1 ... i ) \ c ) ) ) ) )   &    |- E = { c e. O | A. i e. ( 1 ... ( M + N ) ) 0 < ( ( F ` c ) ` i ) }   &    |- N < M   =>    |- ( C e. ( O \ E ) -> E. k e. ( 1 ... ( M + N ) ) ( ( F ` C ) ` k ) = 0 )
Theorem	ballotlemi 30562*	Value of I for a given counting C. (Contributed by Thierry Arnoux, 1-Dec-2016.) (Revised by AV, 6-Oct-2020.)
|- M e. NN   &    |- N e. NN   &    |- O = { c e. ~P ( 1 ... ( M + N ) ) | ( # ` c ) = M }   &    |- P = ( x e. ~P O |-> ( ( # ` x ) / ( # ` O ) ) )   &    |- F = ( c e. O |-> ( i e. ZZ |-> ( ( # ` ( ( 1 ... i ) i^i c ) ) - ( # ` ( ( 1 ... i ) \ c ) ) ) ) )   &    |- E = { c e. O | A. i e. ( 1 ... ( M + N ) ) 0 < ( ( F ` c ) ` i ) }   &    |- N < M   &    |- I = ( c e. ( O \ E ) |-> inf ( { k e. ( 1 ... ( M + N ) ) | ( ( F ` c ) ` k ) = 0 } , RR , < ) )   =>    |- ( C e. ( O \ E ) -> ( I ` C ) = inf ( { k e. ( 1 ... ( M + N ) ) | ( ( F ` C ) ` k ) = 0 } , RR , < ) )
Theorem	ballotlemiex 30563*	Properties of ( I ` C ). (Contributed by Thierry Arnoux, 12-Dec-2016.) (Revised by AV, 6-Oct-2020.)
|- M e. NN   &    |- N e. NN   &    |- O = { c e. ~P ( 1 ... ( M + N ) ) | ( # ` c ) = M }   &    |- P = ( x e. ~P O |-> ( ( # ` x ) / ( # ` O ) ) )   &    |- F = ( c e. O |-> ( i e. ZZ |-> ( ( # ` ( ( 1 ... i ) i^i c ) ) - ( # ` ( ( 1 ... i ) \ c ) ) ) ) )   &    |- E = { c e. O | A. i e. ( 1 ... ( M + N ) ) 0 < ( ( F ` c ) ` i ) }   &    |- N < M   &    |- I = ( c e. ( O \ E ) |-> inf ( { k e. ( 1 ... ( M + N ) ) | ( ( F ` c ) ` k ) = 0 } , RR , < ) )   =>    |- ( C e. ( O \ E ) -> ( ( I ` C ) e. ( 1 ... ( M + N ) ) /\ ( ( F ` C ) ` ( I ` C ) ) = 0 ) )
Theorem	ballotlemi1 30564*	The first tie cannot be reached at the first pick. (Contributed by Thierry Arnoux, 12-Mar-2017.)
|- M e. NN   &    |- N e. NN   &    |- O = { c e. ~P ( 1 ... ( M + N ) ) | ( # ` c ) = M }   &    |- P = ( x e. ~P O |-> ( ( # ` x ) / ( # ` O ) ) )   &    |- F = ( c e. O |-> ( i e. ZZ |-> ( ( # ` ( ( 1 ... i ) i^i c ) ) - ( # ` ( ( 1 ... i ) \ c ) ) ) ) )   &    |- E = { c e. O | A. i e. ( 1 ... ( M + N ) ) 0 < ( ( F ` c ) ` i ) }   &    |- N < M   &    |- I = ( c e. ( O \ E ) |-> inf ( { k e. ( 1 ... ( M + N ) ) | ( ( F ` c ) ` k ) = 0 } , RR , < ) )   =>    |- ( ( C e. ( O \ E ) /\ -. 1 e. C ) -> ( I ` C ) =/= 1 )
Theorem	ballotlemii 30565*	The first tie cannot be reached at the first pick. (Contributed by Thierry Arnoux, 4-Apr-2017.)
|- M e. NN   &    |- N e. NN   &    |- O = { c e. ~P ( 1 ... ( M + N ) ) | ( # ` c ) = M }   &    |- P = ( x e. ~P O |-> ( ( # ` x ) / ( # ` O ) ) )   &    |- F = ( c e. O |-> ( i e. ZZ |-> ( ( # ` ( ( 1 ... i ) i^i c ) ) - ( # ` ( ( 1 ... i ) \ c ) ) ) ) )   &    |- E = { c e. O | A. i e. ( 1 ... ( M + N ) ) 0 < ( ( F ` c ) ` i ) }   &    |- N < M   &    |- I = ( c e. ( O \ E ) |-> inf ( { k e. ( 1 ... ( M + N ) ) | ( ( F ` c ) ` k ) = 0 } , RR , < ) )   =>    |- ( ( C e. ( O \ E ) /\ 1 e. C ) -> ( I ` C ) =/= 1 )
Theorem	ballotlemsup 30566*	The set of zeroes of F satisfies the conditions to have a supremum. (Contributed by Thierry Arnoux, 1-Dec-2016.) (Revised by AV, 6-Oct-2020.)
|- M e. NN   &    |- N e. NN   &    |- O = { c e. ~P ( 1 ... ( M + N ) ) | ( # ` c ) = M }   &    |- P = ( x e. ~P O |-> ( ( # ` x ) / ( # ` O ) ) )   &    |- F = ( c e. O |-> ( i e. ZZ |-> ( ( # ` ( ( 1 ... i ) i^i c ) ) - ( # ` ( ( 1 ... i ) \ c ) ) ) ) )   &    |- E = { c e. O | A. i e. ( 1 ... ( M + N ) ) 0 < ( ( F ` c ) ` i ) }   &    |- N < M   &    |- I = ( c e. ( O \ E ) |-> inf ( { k e. ( 1 ... ( M + N ) ) | ( ( F ` c ) ` k ) = 0 } , RR , < ) )   =>    |- ( C e. ( O \ E ) -> E. z e. RR ( A. w e. { k e. ( 1 ... ( M + N ) ) | ( ( F ` C ) ` k ) = 0 } -. w < z /\ A. w e. RR ( z < w -> E. y e. { k e. ( 1 ... ( M + N ) ) | ( ( F ` C ) ` k ) = 0 } y < w ) ) )
Theorem	ballotlemimin 30567*	( I ` C ) is the first tie. (Contributed by Thierry Arnoux, 1-Dec-2016.) (Revised by AV, 6-Oct-2020.)
|- M e. NN   &    |- N e. NN   &    |- O = { c e. ~P ( 1 ... ( M + N ) ) | ( # ` c ) = M }   &    |- P = ( x e. ~P O |-> ( ( # ` x ) / ( # ` O ) ) )   &    |- F = ( c e. O |-> ( i e. ZZ |-> ( ( # ` ( ( 1 ... i ) i^i c ) ) - ( # ` ( ( 1 ... i ) \ c ) ) ) ) )   &    |- E = { c e. O | A. i e. ( 1 ... ( M + N ) ) 0 < ( ( F ` c ) ` i ) }   &    |- N < M   &    |- I = ( c e. ( O \ E ) |-> inf ( { k e. ( 1 ... ( M + N ) ) | ( ( F ` c ) ` k ) = 0 } , RR , < ) )   =>    |- ( C e. ( O \ E ) -> -. E. k e. ( 1 ... ( ( I ` C ) - 1 ) ) ( ( F ` C ) ` k ) = 0 )
Theorem	ballotlemic 30568*	If the first vote is for B, the vote on the first tie is for A. (Contributed by Thierry Arnoux, 1-Dec-2016.)
|- M e. NN   &    |- N e. NN   &    |- O = { c e. ~P ( 1 ... ( M + N ) ) | ( # ` c ) = M }   &    |- P = ( x e. ~P O |-> ( ( # ` x ) / ( # ` O ) ) )   &    |- F = ( c e. O |-> ( i e. ZZ |-> ( ( # ` ( ( 1 ... i ) i^i c ) ) - ( # ` ( ( 1 ... i ) \ c ) ) ) ) )   &    |- E = { c e. O | A. i e. ( 1 ... ( M + N ) ) 0 < ( ( F ` c ) ` i ) }   &    |- N < M   &    |- I = ( c e. ( O \ E ) |-> inf ( { k e. ( 1 ... ( M + N ) ) | ( ( F ` c ) ` k ) = 0 } , RR , < ) )   =>    |- ( ( C e. ( O \ E ) /\ -. 1 e. C ) -> ( I ` C ) e. C )
Theorem	ballotlem1c 30569*	If the first vote is for A, the vote on the first tie is for B. (Contributed by Thierry Arnoux, 4-Apr-2017.)
|- M e. NN   &    |- N e. NN   &    |- O = { c e. ~P ( 1 ... ( M + N ) ) | ( # ` c ) = M }   &    |- P = ( x e. ~P O |-> ( ( # ` x ) / ( # ` O ) ) )   &    |- F = ( c e. O |-> ( i e. ZZ |-> ( ( # ` ( ( 1 ... i ) i^i c ) ) - ( # ` ( ( 1 ... i ) \ c ) ) ) ) )   &    |- E = { c e. O | A. i e. ( 1 ... ( M + N ) ) 0 < ( ( F ` c ) ` i ) }   &    |- N < M   &    |- I = ( c e. ( O \ E ) |-> inf ( { k e. ( 1 ... ( M + N ) ) | ( ( F ` c ) ` k ) = 0 } , RR , < ) )   =>    |- ( ( C e. ( O \ E ) /\ 1 e. C ) -> -. ( I ` C ) e. C )
Theorem	ballotlemsval 30570*	Value of S. (Contributed by Thierry Arnoux, 12-Apr-2017.)
|- M e. NN   &    |- N e. NN   &    |- O = { c e. ~P ( 1 ... ( M + N ) ) | ( # ` c ) = M }   &    |- P = ( x e. ~P O |-> ( ( # ` x ) / ( # ` O ) ) )   &    |- F = ( c e. O |-> ( i e. ZZ |-> ( ( # ` ( ( 1 ... i ) i^i c ) ) - ( # ` ( ( 1 ... i ) \ c ) ) ) ) )   &    |- E = { c e. O | A. i e. ( 1 ... ( M + N ) ) 0 < ( ( F ` c ) ` i ) }   &    |- N < M   &    |- I = ( c e. ( O \ E ) |-> inf ( { k e. ( 1 ... ( M + N ) ) | ( ( F ` c ) ` k ) = 0 } , RR , < ) )   &    |- S = ( c e. ( O \ E ) |-> ( i e. ( 1 ... ( M + N ) ) |-> if ( i <_ ( I ` c ) , ( ( ( I ` c ) + 1 ) - i ) , i ) ) )   =>    |- ( C e. ( O \ E ) -> ( S ` C ) = ( i e. ( 1 ... ( M + N ) ) |-> if ( i <_ ( I ` C ) , ( ( ( I ` C ) + 1 ) - i ) , i ) ) )
Theorem	ballotlemsv 30571*	Value of S evaluated at J for a given counting C. (Contributed by Thierry Arnoux, 12-Apr-2017.)
|- M e. NN   &    |- N e. NN   &    |- O = { c e. ~P ( 1 ... ( M + N ) ) | ( # ` c ) = M }   &    |- P = ( x e. ~P O |-> ( ( # ` x ) / ( # ` O ) ) )   &    |- F = ( c e. O |-> ( i e. ZZ |-> ( ( # ` ( ( 1 ... i ) i^i c ) ) - ( # ` ( ( 1 ... i ) \ c ) ) ) ) )   &    |- E = { c e. O | A. i e. ( 1 ... ( M + N ) ) 0 < ( ( F ` c ) ` i ) }   &    |- N < M   &    |- I = ( c e. ( O \ E ) |-> inf ( { k e. ( 1 ... ( M + N ) ) | ( ( F ` c ) ` k ) = 0 } , RR , < ) )   &    |- S = ( c e. ( O \ E ) |-> ( i e. ( 1 ... ( M + N ) ) |-> if ( i <_ ( I ` c ) , ( ( ( I ` c ) + 1 ) - i ) , i ) ) )   =>    |- ( ( C e. ( O \ E ) /\ J e. ( 1 ... ( M + N ) ) ) -> ( ( S ` C ) ` J ) = if ( J <_ ( I ` C ) , ( ( ( I ` C ) + 1 ) - J ) , J ) )
Theorem	ballotlemsgt1 30572*	S maps values less than ( I ` C ) to values greater than 1. (Contributed by Thierry Arnoux, 28-Apr-2017.)
|- M e. NN   &    |- N e. NN   &    |- O = { c e. ~P ( 1 ... ( M + N ) ) | ( # ` c ) = M }   &    |- P = ( x e. ~P O |-> ( ( # ` x ) / ( # ` O ) ) )   &    |- F = ( c e. O |-> ( i e. ZZ |-> ( ( # ` ( ( 1 ... i ) i^i c ) ) - ( # ` ( ( 1 ... i ) \ c ) ) ) ) )   &    |- E = { c e. O | A. i e. ( 1 ... ( M + N ) ) 0 < ( ( F ` c ) ` i ) }   &    |- N < M   &    |- I = ( c e. ( O \ E ) |-> inf ( { k e. ( 1 ... ( M + N ) ) | ( ( F ` c ) ` k ) = 0 } , RR , < ) )   &    |- S = ( c e. ( O \ E ) |-> ( i e. ( 1 ... ( M + N ) ) |-> if ( i <_ ( I ` c ) , ( ( ( I ` c ) + 1 ) - i ) , i ) ) )   =>    |- ( ( C e. ( O \ E ) /\ J e. ( 1 ... ( M + N ) ) /\ J < ( I ` C ) ) -> 1 < ( ( S ` C ) ` J ) )
Theorem	ballotlemsdom 30573*	Domain of S for a given counting C. (Contributed by Thierry Arnoux, 12-Apr-2017.)
|- M e. NN   &    |- N e. NN   &    |- O = { c e. ~P ( 1 ... ( M + N ) ) | ( # ` c ) = M }   &    |- P = ( x e. ~P O |-> ( ( # ` x ) / ( # ` O ) ) )   &    |- F = ( c e. O |-> ( i e. ZZ |-> ( ( # ` ( ( 1 ... i ) i^i c ) ) - ( # ` ( ( 1 ... i ) \ c ) ) ) ) )   &    |- E = { c e. O | A. i e. ( 1 ... ( M + N ) ) 0 < ( ( F ` c ) ` i ) }   &    |- N < M   &    |- I = ( c e. ( O \ E ) |-> inf ( { k e. ( 1 ... ( M + N ) ) | ( ( F ` c ) ` k ) = 0 } , RR , < ) )   &    |- S = ( c e. ( O \ E ) |-> ( i e. ( 1 ... ( M + N ) ) |-> if ( i <_ ( I ` c ) , ( ( ( I ` c ) + 1 ) - i ) , i ) ) )   =>    |- ( ( C e. ( O \ E ) /\ J e. ( 1 ... ( M + N ) ) ) -> ( ( S ` C ) ` J ) e. ( 1 ... ( M + N ) ) )
Theorem	ballotlemsel1i 30574*	The range ( 1 ... ( I ` C ) ) is invariant under ( S ` C ). (Contributed by Thierry Arnoux, 28-Apr-2017.)
|- M e. NN   &    |- N e. NN   &    |- O = { c e. ~P ( 1 ... ( M + N ) ) | ( # ` c ) = M }   &    |- P = ( x e. ~P O |-> ( ( # ` x ) / ( # ` O ) ) )   &    |- F = ( c e. O |-> ( i e. ZZ |-> ( ( # ` ( ( 1 ... i ) i^i c ) ) - ( # ` ( ( 1 ... i ) \ c ) ) ) ) )   &    |- E = { c e. O | A. i e. ( 1 ... ( M + N ) ) 0 < ( ( F ` c ) ` i ) }   &    |- N < M   &    |- I = ( c e. ( O \ E ) |-> inf ( { k e. ( 1 ... ( M + N ) ) | ( ( F ` c ) ` k ) = 0 } , RR , < ) )   &    |- S = ( c e. ( O \ E ) |-> ( i e. ( 1 ... ( M + N ) ) |-> if ( i <_ ( I ` c ) , ( ( ( I ` c ) + 1 ) - i ) , i ) ) )   =>    |- ( ( C e. ( O \ E ) /\ J e. ( 1 ... ( I ` C ) ) ) -> ( ( S ` C ) ` J ) e. ( 1 ... ( I ` C ) ) )
Theorem	ballotlemsf1o 30575*	The defined S is a bijection, and an involution. (Contributed by Thierry Arnoux, 14-Apr-2017.)
|- M e. NN   &    |- N e. NN   &    |- O = { c e. ~P ( 1 ... ( M + N ) ) | ( # ` c ) = M }   &    |- P = ( x e. ~P O |-> ( ( # ` x ) / ( # ` O ) ) )   &    |- F = ( c e. O |-> ( i e. ZZ |-> ( ( # ` ( ( 1 ... i ) i^i c ) ) - ( # ` ( ( 1 ... i ) \ c ) ) ) ) )   &    |- E = { c e. O | A. i e. ( 1 ... ( M + N ) ) 0 < ( ( F ` c ) ` i ) }   &    |- N < M   &    |- I = ( c e. ( O \ E ) |-> inf ( { k e. ( 1 ... ( M + N ) ) | ( ( F ` c ) ` k ) = 0 } , RR , < ) )   &    |- S = ( c e. ( O \ E ) |-> ( i e. ( 1 ... ( M + N ) ) |-> if ( i <_ ( I ` c ) , ( ( ( I ` c ) + 1 ) - i ) , i ) ) )   =>    |- ( C e. ( O \ E ) -> ( ( S ` C ) : ( 1 ... ( M + N ) ) -1-1-onto-> ( 1 ... ( M + N ) ) /\ `' ( S ` C ) = ( S ` C ) ) )
Theorem	ballotlemsi 30576*	The image by S of the first tie pick is the first pick. (Contributed by Thierry Arnoux, 14-Apr-2017.)
|- M e. NN   &    |- N e. NN   &    |- O = { c e. ~P ( 1 ... ( M + N ) ) | ( # ` c ) = M }   &    |- P = ( x e. ~P O |-> ( ( # ` x ) / ( # ` O ) ) )   &    |- F = ( c e. O |-> ( i e. ZZ |-> ( ( # ` ( ( 1 ... i ) i^i c ) ) - ( # ` ( ( 1 ... i ) \ c ) ) ) ) )   &    |- E = { c e. O | A. i e. ( 1 ... ( M + N ) ) 0 < ( ( F ` c ) ` i ) }   &    |- N < M   &    |- I = ( c e. ( O \ E ) |-> inf ( { k e. ( 1 ... ( M + N ) ) | ( ( F ` c ) ` k ) = 0 } , RR , < ) )   &    |- S = ( c e. ( O \ E ) |-> ( i e. ( 1 ... ( M + N ) ) |-> if ( i <_ ( I ` c ) , ( ( ( I ` c ) + 1 ) - i ) , i ) ) )   =>    |- ( C e. ( O \ E ) -> ( ( S ` C ) ` ( I ` C ) ) = 1 )
Theorem	ballotlemsima 30577*	The image by S of an interval before the first pick. (Contributed by Thierry Arnoux, 5-May-2017.)
|- M e. NN   &    |- N e. NN   &    |- O = { c e. ~P ( 1 ... ( M + N ) ) | ( # ` c ) = M }   &    |- P = ( x e. ~P O |-> ( ( # ` x ) / ( # ` O ) ) )   &    |- F = ( c e. O |-> ( i e. ZZ |-> ( ( # ` ( ( 1 ... i ) i^i c ) ) - ( # ` ( ( 1 ... i ) \ c ) ) ) ) )   &    |- E = { c e. O | A. i e. ( 1 ... ( M + N ) ) 0 < ( ( F ` c ) ` i ) }   &    |- N < M   &    |- I = ( c e. ( O \ E ) |-> inf ( { k e. ( 1 ... ( M + N ) ) | ( ( F ` c ) ` k ) = 0 } , RR , < ) )   &    |- S = ( c e. ( O \ E ) |-> ( i e. ( 1 ... ( M + N ) ) |-> if ( i <_ ( I ` c ) , ( ( ( I ` c ) + 1 ) - i ) , i ) ) )   =>    |- ( ( C e. ( O \ E ) /\ J e. ( 1 ... ( I ` C ) ) ) -> ( ( S ` C ) " ( 1 ... J ) ) = ( ( ( S ` C ) ` J ) ... ( I ` C ) ) )
Theorem	ballotlemieq 30578*	If two countings share the same first tie, they also have the same swap function. (Contributed by Thierry Arnoux, 18-Apr-2017.)
|- M e. NN   &    |- N e. NN   &    |- O = { c e. ~P ( 1 ... ( M + N ) ) | ( # ` c ) = M }   &    |- P = ( x e. ~P O |-> ( ( # ` x ) / ( # ` O ) ) )   &    |- F = ( c e. O |-> ( i e. ZZ |-> ( ( # ` ( ( 1 ... i ) i^i c ) ) - ( # ` ( ( 1 ... i ) \ c ) ) ) ) )   &    |- E = { c e. O | A. i e. ( 1 ... ( M + N ) ) 0 < ( ( F ` c ) ` i ) }   &    |- N < M   &    |- I = ( c e. ( O \ E ) |-> inf ( { k e. ( 1 ... ( M + N ) ) | ( ( F ` c ) ` k ) = 0 } , RR , < ) )   &    |- S = ( c e. ( O \ E ) |-> ( i e. ( 1 ... ( M + N ) ) |-> if ( i <_ ( I ` c ) , ( ( ( I ` c ) + 1 ) - i ) , i ) ) )   =>    |- ( ( C e. ( O \ E ) /\ D e. ( O \ E ) /\ ( I ` C ) = ( I ` D ) ) -> ( S ` C ) = ( S ` D ) )
Theorem	ballotlemrval 30579*	Value of R. (Contributed by Thierry Arnoux, 14-Apr-2017.)
|- M e. NN   &    |- N e. NN   &    |- O = { c e. ~P ( 1 ... ( M + N ) ) | ( # ` c ) = M }   &    |- P = ( x e. ~P O |-> ( ( # ` x ) / ( # ` O ) ) )   &    |- F = ( c e. O |-> ( i e. ZZ |-> ( ( # ` ( ( 1 ... i ) i^i c ) ) - ( # ` ( ( 1 ... i ) \ c ) ) ) ) )   &    |- E = { c e. O | A. i e. ( 1 ... ( M + N ) ) 0 < ( ( F ` c ) ` i ) }   &    |- N < M   &    |- I = ( c e. ( O \ E ) |-> inf ( { k e. ( 1 ... ( M + N ) ) | ( ( F ` c ) ` k ) = 0 } , RR , < ) )   &    |- S = ( c e. ( O \ E ) |-> ( i e. ( 1 ... ( M + N ) ) |-> if ( i <_ ( I ` c ) , ( ( ( I ` c ) + 1 ) - i ) , i ) ) )   &    |- R = ( c e. ( O \ E ) |-> ( ( S ` c ) " c ) )   =>    |- ( C e. ( O \ E ) -> ( R ` C ) = ( ( S ` C ) " C ) )
Theorem	ballotlemscr 30580*	The image of ( R ` C ) by ( S ` C ). (Contributed by Thierry Arnoux, 21-Apr-2017.)
|- M e. NN   &    |- N e. NN   &    |- O = { c e. ~P ( 1 ... ( M + N ) ) | ( # ` c ) = M }   &    |- P = ( x e. ~P O |-> ( ( # ` x ) / ( # ` O ) ) )   &    |- F = ( c e. O |-> ( i e. ZZ |-> ( ( # ` ( ( 1 ... i ) i^i c ) ) - ( # ` ( ( 1 ... i ) \ c ) ) ) ) )   &    |- E = { c e. O | A. i e. ( 1 ... ( M + N ) ) 0 < ( ( F ` c ) ` i ) }   &    |- N < M   &    |- I = ( c e. ( O \ E ) |-> inf ( { k e. ( 1 ... ( M + N ) ) | ( ( F ` c ) ` k ) = 0 } , RR , < ) )   &    |- S = ( c e. ( O \ E ) |-> ( i e. ( 1 ... ( M + N ) ) |-> if ( i <_ ( I ` c ) , ( ( ( I ` c ) + 1 ) - i ) , i ) ) )   &    |- R = ( c e. ( O \ E ) |-> ( ( S ` c ) " c ) )   =>    |- ( C e. ( O \ E ) -> ( ( S ` C ) " ( R ` C ) ) = C )
Theorem	ballotlemrv 30581*	Value of R evaluated at J. (Contributed by Thierry Arnoux, 17-Apr-2017.)
|- M e. NN   &    |- N e. NN   &    |- O = { c e. ~P ( 1 ... ( M + N ) ) | ( # ` c ) = M }   &    |- P = ( x e. ~P O |-> ( ( # ` x ) / ( # ` O ) ) )   &    |- F = ( c e. O |-> ( i e. ZZ |-> ( ( # ` ( ( 1 ... i ) i^i c ) ) - ( # ` ( ( 1 ... i ) \ c ) ) ) ) )   &    |- E = { c e. O | A. i e. ( 1 ... ( M + N ) ) 0 < ( ( F ` c ) ` i ) }   &    |- N < M   &    |- I = ( c e. ( O \ E ) |-> inf ( { k e. ( 1 ... ( M + N ) ) | ( ( F ` c ) ` k ) = 0 } , RR , < ) )   &    |- S = ( c e. ( O \ E ) |-> ( i e. ( 1 ... ( M + N ) ) |-> if ( i <_ ( I ` c ) , ( ( ( I ` c ) + 1 ) - i ) , i ) ) )   &    |- R = ( c e. ( O \ E ) |-> ( ( S ` c ) " c ) )   =>    |- ( ( C e. ( O \ E ) /\ J e. ( 1 ... ( M + N ) ) ) -> ( J e. ( R ` C ) <-> if ( J <_ ( I ` C ) , ( ( ( I ` C ) + 1 ) - J ) , J ) e. C ) )
Theorem	ballotlemrv1 30582*	Value of R before the tie. (Contributed by Thierry Arnoux, 11-Apr-2017.)
|- M e. NN   &    |- N e. NN   &    |- O = { c e. ~P ( 1 ... ( M + N ) ) | ( # ` c ) = M }   &    |- P = ( x e. ~P O |-> ( ( # ` x ) / ( # ` O ) ) )   &    |- F = ( c e. O |-> ( i e. ZZ |-> ( ( # ` ( ( 1 ... i ) i^i c ) ) - ( # ` ( ( 1 ... i ) \ c ) ) ) ) )   &    |- E = { c e. O | A. i e. ( 1 ... ( M + N ) ) 0 < ( ( F ` c ) ` i ) }   &    |- N < M   &    |- I = ( c e. ( O \ E ) |-> inf ( { k e. ( 1 ... ( M + N ) ) | ( ( F ` c ) ` k ) = 0 } , RR , < ) )   &    |- S = ( c e. ( O \ E ) |-> ( i e. ( 1 ... ( M + N ) ) |-> if ( i <_ ( I ` c ) , ( ( ( I ` c ) + 1 ) - i ) , i ) ) )   &    |- R = ( c e. ( O \ E ) |-> ( ( S ` c ) " c ) )   =>    |- ( ( C e. ( O \ E ) /\ J e. ( 1 ... ( M + N ) ) /\ J <_ ( I ` C ) ) -> ( J e. ( R ` C ) <-> ( ( ( I ` C ) + 1 ) - J ) e. C ) )
Theorem	ballotlemrv2 30583*	Value of R after the tie. (Contributed by Thierry Arnoux, 11-Apr-2017.)
|- M e. NN   &    |- N e. NN   &    |- O = { c e. ~P ( 1 ... ( M + N ) ) | ( # ` c ) = M }   &    |- P = ( x e. ~P O |-> ( ( # ` x ) / ( # ` O ) ) )   &    |- F = ( c e. O |-> ( i e. ZZ |-> ( ( # ` ( ( 1 ... i ) i^i c ) ) - ( # ` ( ( 1 ... i ) \ c ) ) ) ) )   &    |- E = { c e. O | A. i e. ( 1 ... ( M + N ) ) 0 < ( ( F ` c ) ` i ) }   &    |- N < M   &    |- I = ( c e. ( O \ E ) |-> inf ( { k e. ( 1 ... ( M + N ) ) | ( ( F ` c ) ` k ) = 0 } , RR , < ) )   &    |- S = ( c e. ( O \ E ) |-> ( i e. ( 1 ... ( M + N ) ) |-> if ( i <_ ( I ` c ) , ( ( ( I ` c ) + 1 ) - i ) , i ) ) )   &    |- R = ( c e. ( O \ E ) |-> ( ( S ` c ) " c ) )   =>    |- ( ( C e. ( O \ E ) /\ J e. ( 1 ... ( M + N ) ) /\ ( I ` C ) < J ) -> ( J e. ( R ` C ) <-> J e. C ) )
Theorem	ballotlemro 30584*	Range of R is included in O. (Contributed by Thierry Arnoux, 17-Apr-2017.)
|- M e. NN   &    |- N e. NN   &    |- O = { c e. ~P ( 1 ... ( M + N ) ) | ( # ` c ) = M }   &    |- P = ( x e. ~P O |-> ( ( # ` x ) / ( # ` O ) ) )   &    |- F = ( c e. O |-> ( i e. ZZ |-> ( ( # ` ( ( 1 ... i ) i^i c ) ) - ( # ` ( ( 1 ... i ) \ c ) ) ) ) )   &    |- E = { c e. O | A. i e. ( 1 ... ( M + N ) ) 0 < ( ( F ` c ) ` i ) }   &    |- N < M   &    |- I = ( c e. ( O \ E ) |-> inf ( { k e. ( 1 ... ( M + N ) ) | ( ( F ` c ) ` k ) = 0 } , RR , < ) )   &    |- S = ( c e. ( O \ E ) |-> ( i e. ( 1 ... ( M + N ) ) |-> if ( i <_ ( I ` c ) , ( ( ( I ` c ) + 1 ) - i ) , i ) ) )   &    |- R = ( c e. ( O \ E ) |-> ( ( S ` c ) " c ) )   =>    |- ( C e. ( O \ E ) -> ( R ` C ) e. O )
Theorem	ballotlemgval 30585*	Expand the value of .^. (Contributed by Thierry Arnoux, 21-Apr-2017.)
|- M e. NN   &    |- N e. NN   &    |- O = { c e. ~P ( 1 ... ( M + N ) ) | ( # ` c ) = M }   &    |- P = ( x e. ~P O |-> ( ( # ` x ) / ( # ` O ) ) )   &    |- F = ( c e. O |-> ( i e. ZZ |-> ( ( # ` ( ( 1 ... i ) i^i c ) ) - ( # ` ( ( 1 ... i ) \ c ) ) ) ) )   &    |- E = { c e. O | A. i e. ( 1 ... ( M + N ) ) 0 < ( ( F ` c ) ` i ) }   &    |- N < M   &    |- I = ( c e. ( O \ E ) |-> inf ( { k e. ( 1 ... ( M + N ) ) | ( ( F ` c ) ` k ) = 0 } , RR , < ) )   &    |- S = ( c e. ( O \ E ) |-> ( i e. ( 1 ... ( M + N ) ) |-> if ( i <_ ( I ` c ) , ( ( ( I ` c ) + 1 ) - i ) , i ) ) )   &    |- R = ( c e. ( O \ E ) |-> ( ( S ` c ) " c ) )   &    |- .^ = ( u e. Fin , v e. Fin |-> ( ( # ` ( v i^i u ) ) - ( # ` ( v \ u ) ) ) )   =>    |- ( ( U e. Fin /\ V e. Fin ) -> ( U .^ V ) = ( ( # ` ( V i^i U ) ) - ( # ` ( V \ U ) ) ) )
Theorem	ballotlemgun 30586*	A property of the defined .^ operator. (Contributed by Thierry Arnoux, 26-Apr-2017.)
|- M e. NN   &    |- N e. NN   &    |- O = { c e. ~P ( 1 ... ( M + N ) ) | ( # ` c ) = M }   &    |- P = ( x e. ~P O |-> ( ( # ` x ) / ( # ` O ) ) )   &    |- F = ( c e. O |-> ( i e. ZZ |-> ( ( # ` ( ( 1 ... i ) i^i c ) ) - ( # ` ( ( 1 ... i ) \ c ) ) ) ) )   &    |- E = { c e. O | A. i e. ( 1 ... ( M + N ) ) 0 < ( ( F ` c ) ` i ) }   &    |- N < M   &    |- I = ( c e. ( O \ E ) |-> inf ( { k e. ( 1 ... ( M + N ) ) | ( ( F ` c ) ` k ) = 0 } , RR , < ) )   &    |- S = ( c e. ( O \ E ) |-> ( i e. ( 1 ... ( M + N ) ) |-> if ( i <_ ( I ` c ) , ( ( ( I ` c ) + 1 ) - i ) , i ) ) )   &    |- R = ( c e. ( O \ E ) |-> ( ( S ` c ) " c ) )   &    |- .^ = ( u e. Fin , v e. Fin |-> ( ( # ` ( v i^i u ) ) - ( # ` ( v \ u ) ) ) )   &    |- ( ph -> U e. Fin )   &    |- ( ph -> V e. Fin )   &    |- ( ph -> W e. Fin )   &    |- ( ph -> ( V i^i W ) = (/) )   =>    |- ( ph -> ( U .^ ( V u. W ) ) = ( ( U .^ V ) + ( U .^ W ) ) )
Theorem	ballotlemfg 30587*	Express the value of ( F ` C ) in terms of .^. (Contributed by Thierry Arnoux, 21-Apr-2017.)
|- M e. NN   &    |- N e. NN   &    |- O = { c e. ~P ( 1 ... ( M + N ) ) | ( # ` c ) = M }   &    |- P = ( x e. ~P O |-> ( ( # ` x ) / ( # ` O ) ) )   &    |- F = ( c e. O |-> ( i e. ZZ |-> ( ( # ` ( ( 1 ... i ) i^i c ) ) - ( # ` ( ( 1 ... i ) \ c ) ) ) ) )   &    |- E = { c e. O | A. i e. ( 1 ... ( M + N ) ) 0 < ( ( F ` c ) ` i ) }   &    |- N < M   &    |- I = ( c e. ( O \ E ) |-> inf ( { k e. ( 1 ... ( M + N ) ) | ( ( F ` c ) ` k ) = 0 } , RR , < ) )   &    |- S = ( c e. ( O \ E ) |-> ( i e. ( 1 ... ( M + N ) ) |-> if ( i <_ ( I ` c ) , ( ( ( I ` c ) + 1 ) - i ) , i ) ) )   &    |- R = ( c e. ( O \ E ) |-> ( ( S ` c ) " c ) )   &    |- .^ = ( u e. Fin , v e. Fin |-> ( ( # ` ( v i^i u ) ) - ( # ` ( v \ u ) ) ) )   =>    |- ( ( C e. ( O \ E ) /\ J e. ( 0 ... ( M + N ) ) ) -> ( ( F ` C ) ` J ) = ( C .^ ( 1 ... J ) ) )
Theorem	ballotlemfrc 30588*	Express the value of ( F ` ( R ` C ) ) in terms of the newly defined .^. (Contributed by Thierry Arnoux, 21-Apr-2017.)
|- M e. NN   &    |- N e. NN   &    |- O = { c e. ~P ( 1 ... ( M + N ) ) | ( # ` c ) = M }   &    |- P = ( x e. ~P O |-> ( ( # ` x ) / ( # ` O ) ) )   &    |- F = ( c e. O |-> ( i e. ZZ |-> ( ( # ` ( ( 1 ... i ) i^i c ) ) - ( # ` ( ( 1 ... i ) \ c ) ) ) ) )   &    |- E = { c e. O | A. i e. ( 1 ... ( M + N ) ) 0 < ( ( F ` c ) ` i ) }   &    |- N < M   &    |- I = ( c e. ( O \ E ) |-> inf ( { k e. ( 1 ... ( M + N ) ) | ( ( F ` c ) ` k ) = 0 } , RR , < ) )   &    |- S = ( c e. ( O \ E ) |-> ( i e. ( 1 ... ( M + N ) ) |-> if ( i <_ ( I ` c ) , ( ( ( I ` c ) + 1 ) - i ) , i ) ) )   &    |- R = ( c e. ( O \ E ) |-> ( ( S ` c ) " c ) )   &    |- .^ = ( u e. Fin , v e. Fin |-> ( ( # ` ( v i^i u ) ) - ( # ` ( v \ u ) ) ) )   =>    |- ( ( C e. ( O \ E ) /\ J e. ( 1 ... ( I ` C ) ) ) -> ( ( F ` ( R ` C ) ) ` J ) = ( C .^ ( ( ( S ` C ) ` J ) ... ( I ` C ) ) ) )
Theorem	ballotlemfrci 30589*	Reverse counting preserves a tie at the first tie. (Contributed by Thierry Arnoux, 21-Apr-2017.)
|- M e. NN   &    |- N e. NN   &    |- O = { c e. ~P ( 1 ... ( M + N ) ) | ( # ` c ) = M }   &    |- P = ( x e. ~P O |-> ( ( # ` x ) / ( # ` O ) ) )   &    |- F = ( c e. O |-> ( i e. ZZ |-> ( ( # ` ( ( 1 ... i ) i^i c ) ) - ( # ` ( ( 1 ... i ) \ c ) ) ) ) )   &    |- E = { c e. O | A. i e. ( 1 ... ( M + N ) ) 0 < ( ( F ` c ) ` i ) }   &    |- N < M   &    |- I = ( c e. ( O \ E ) |-> inf ( { k e. ( 1 ... ( M + N ) ) | ( ( F ` c ) ` k ) = 0 } , RR , < ) )   &    |- S = ( c e. ( O \ E ) |-> ( i e. ( 1 ... ( M + N ) ) |-> if ( i <_ ( I ` c ) , ( ( ( I ` c ) + 1 ) - i ) , i ) ) )   &    |- R = ( c e. ( O \ E ) |-> ( ( S ` c ) " c ) )   &    |- .^ = ( u e. Fin , v e. Fin |-> ( ( # ` ( v i^i u ) ) - ( # ` ( v \ u ) ) ) )   =>    |- ( C e. ( O \ E ) -> ( ( F ` ( R ` C ) ) ` ( I ` C ) ) = 0 )
Theorem	ballotlemfrceq 30590*	Value of F for a reverse counting ( R ` C ). (Contributed by Thierry Arnoux, 27-Apr-2017.)
|- M e. NN   &    |- N e. NN   &    |- O = { c e. ~P ( 1 ... ( M + N ) ) | ( # ` c ) = M }   &    |- P = ( x e. ~P O |-> ( ( # ` x ) / ( # ` O ) ) )   &    |- F = ( c e. O |-> ( i e. ZZ |-> ( ( # ` ( ( 1 ... i ) i^i c ) ) - ( # ` ( ( 1 ... i ) \ c ) ) ) ) )   &    |- E = { c e. O | A. i e. ( 1 ... ( M + N ) ) 0 < ( ( F ` c ) ` i ) }   &    |- N < M   &    |- I = ( c e. ( O \ E ) |-> inf ( { k e. ( 1 ... ( M + N ) ) | ( ( F ` c ) ` k ) = 0 } , RR , < ) )   &    |- S = ( c e. ( O \ E ) |-> ( i e. ( 1 ... ( M + N ) ) |-> if ( i <_ ( I ` c ) , ( ( ( I ` c ) + 1 ) - i ) , i ) ) )   &    |- R = ( c e. ( O \ E ) |-> ( ( S ` c ) " c ) )   &    |- .^ = ( u e. Fin , v e. Fin |-> ( ( # ` ( v i^i u ) ) - ( # ` ( v \ u ) ) ) )   =>    |- ( ( C e. ( O \ E ) /\ J e. ( 1 ... ( I ` C ) ) ) -> ( ( F ` C ) ` ( ( ( S ` C ) ` J ) - 1 ) ) = -u ( ( F ` ( R ` C ) ) ` J ) )
Theorem	ballotlemfrcn0 30591*	Value of F for a reversed counting ( R ` C ), before the first tie, cannot be zero . (Contributed by Thierry Arnoux, 25-Apr-2017.) (Revised by AV, 6-Oct-2020.)
|- M e. NN   &    |- N e. NN   &    |- O = { c e. ~P ( 1 ... ( M + N ) ) | ( # ` c ) = M }   &    |- P = ( x e. ~P O |-> ( ( # ` x ) / ( # ` O ) ) )   &    |- F = ( c e. O |-> ( i e. ZZ |-> ( ( # ` ( ( 1 ... i ) i^i c ) ) - ( # ` ( ( 1 ... i ) \ c ) ) ) ) )   &    |- E = { c e. O | A. i e. ( 1 ... ( M + N ) ) 0 < ( ( F ` c ) ` i ) }   &    |- N < M   &    |- I = ( c e. ( O \ E ) |-> inf ( { k e. ( 1 ... ( M + N ) ) | ( ( F ` c ) ` k ) = 0 } , RR , < ) )   &    |- S = ( c e. ( O \ E ) |-> ( i e. ( 1 ... ( M + N ) ) |-> if ( i <_ ( I ` c ) , ( ( ( I ` c ) + 1 ) - i ) , i ) ) )   &    |- R = ( c e. ( O \ E ) |-> ( ( S ` c ) " c ) )   =>    |- ( ( C e. ( O \ E ) /\ J e. ( 1 ... ( M + N ) ) /\ J < ( I ` C ) ) -> ( ( F ` ( R ` C ) ) ` J ) =/= 0 )
Theorem	ballotlemrc 30592*	Range of R. (Contributed by Thierry Arnoux, 19-Apr-2017.)
|- M e. NN   &    |- N e. NN   &    |- O = { c e. ~P ( 1 ... ( M + N ) ) | ( # ` c ) = M }   &    |- P = ( x e. ~P O |-> ( ( # ` x ) / ( # ` O ) ) )   &    |- F = ( c e. O |-> ( i e. ZZ |-> ( ( # ` ( ( 1 ... i ) i^i c ) ) - ( # ` ( ( 1 ... i ) \ c ) ) ) ) )   &    |- E = { c e. O | A. i e. ( 1 ... ( M + N ) ) 0 < ( ( F ` c ) ` i ) }   &    |- N < M   &    |- I = ( c e. ( O \ E ) |-> inf ( { k e. ( 1 ... ( M + N ) ) | ( ( F ` c ) ` k ) = 0 } , RR , < ) )   &    |- S = ( c e. ( O \ E ) |-> ( i e. ( 1 ... ( M + N ) ) |-> if ( i <_ ( I ` c ) , ( ( ( I ` c ) + 1 ) - i ) , i ) ) )   &    |- R = ( c e. ( O \ E ) |-> ( ( S ` c ) " c ) )   =>    |- ( C e. ( O \ E ) -> ( R ` C ) e. ( O \ E ) )
Theorem	ballotlemirc 30593*	Applying R does not change first ties. (Contributed by Thierry Arnoux, 19-Apr-2017.) (Revised by AV, 6-Oct-2020.)
|- M e. NN   &    |- N e. NN   &    |- O = { c e. ~P ( 1 ... ( M + N ) ) | ( # ` c ) = M }   &    |- P = ( x e. ~P O |-> ( ( # ` x ) / ( # ` O ) ) )   &    |- F = ( c e. O |-> ( i e. ZZ |-> ( ( # ` ( ( 1 ... i ) i^i c ) ) - ( # ` ( ( 1 ... i ) \ c ) ) ) ) )   &    |- E = { c e. O | A. i e. ( 1 ... ( M + N ) ) 0 < ( ( F ` c ) ` i ) }   &    |- N < M   &    |- I = ( c e. ( O \ E ) |-> inf ( { k e. ( 1 ... ( M + N ) ) | ( ( F ` c ) ` k ) = 0 } , RR , < ) )   &    |- S = ( c e. ( O \ E ) |-> ( i e. ( 1 ... ( M + N ) ) |-> if ( i <_ ( I ` c ) , ( ( ( I ` c ) + 1 ) - i ) , i ) ) )   &    |- R = ( c e. ( O \ E ) |-> ( ( S ` c ) " c ) )   =>    |- ( C e. ( O \ E ) -> ( I ` ( R ` C ) ) = ( I ` C ) )
Theorem	ballotlemrinv0 30594*	Lemma for ballotlemrinv 30595. (Contributed by Thierry Arnoux, 18-Apr-2017.)
|- M e. NN   &    |- N e. NN   &    |- O = { c e. ~P ( 1 ... ( M + N ) ) | ( # ` c ) = M }   &    |- P = ( x e. ~P O |-> ( ( # ` x ) / ( # ` O ) ) )   &    |- F = ( c e. O |-> ( i e. ZZ |-> ( ( # ` ( ( 1 ... i ) i^i c ) ) - ( # ` ( ( 1 ... i ) \ c ) ) ) ) )   &    |- E = { c e. O | A. i e. ( 1 ... ( M + N ) ) 0 < ( ( F ` c ) ` i ) }   &    |- N < M   &    |- I = ( c e. ( O \ E ) |-> inf ( { k e. ( 1 ... ( M + N ) ) | ( ( F ` c ) ` k ) = 0 } , RR , < ) )   &    |- S = ( c e. ( O \ E ) |-> ( i e. ( 1 ... ( M + N ) ) |-> if ( i <_ ( I ` c ) , ( ( ( I ` c ) + 1 ) - i ) , i ) ) )   &    |- R = ( c e. ( O \ E ) |-> ( ( S ` c ) " c ) )   =>    |- ( ( C e. ( O \ E ) /\ D = ( ( S ` C ) " C ) ) -> ( D e. ( O \ E ) /\ C = ( ( S ` D ) " D ) ) )
Theorem	ballotlemrinv 30595*	R is its own inverse : it is an involution. (Contributed by Thierry Arnoux, 10-Apr-2017.)
|- M e. NN   &    |- N e. NN   &    |- O = { c e. ~P ( 1 ... ( M + N ) ) | ( # ` c ) = M }   &    |- P = ( x e. ~P O |-> ( ( # ` x ) / ( # ` O ) ) )   &    |- F = ( c e. O |-> ( i e. ZZ |-> ( ( # ` ( ( 1 ... i ) i^i c ) ) - ( # ` ( ( 1 ... i ) \ c ) ) ) ) )   &    |- E = { c e. O | A. i e. ( 1 ... ( M + N ) ) 0 < ( ( F ` c ) ` i ) }   &    |- N < M   &    |- I = ( c e. ( O \ E ) |-> inf ( { k e. ( 1 ... ( M + N ) ) | ( ( F ` c ) ` k ) = 0 } , RR , < ) )   &    |- S = ( c e. ( O \ E ) |-> ( i e. ( 1 ... ( M + N ) ) |-> if ( i <_ ( I ` c ) , ( ( ( I ` c ) + 1 ) - i ) , i ) ) )   &    |- R = ( c e. ( O \ E ) |-> ( ( S ` c ) " c ) )   =>    |- `' R = R
Theorem	ballotlem1ri 30596*	When the vote on the first tie is for A, the first vote is also for A on the reverse counting. (Contributed by Thierry Arnoux, 18-Apr-2017.)
|- M e. NN   &    |- N e. NN   &    |- O = { c e. ~P ( 1 ... ( M + N ) ) | ( # ` c ) = M }   &    |- P = ( x e. ~P O |-> ( ( # ` x ) / ( # ` O ) ) )   &    |- F = ( c e. O |-> ( i e. ZZ |-> ( ( # ` ( ( 1 ... i ) i^i c ) ) - ( # ` ( ( 1 ... i ) \ c ) ) ) ) )   &    |- E = { c e. O | A. i e. ( 1 ... ( M + N ) ) 0 < ( ( F ` c ) ` i ) }   &    |- N < M   &    |- I = ( c e. ( O \ E ) |-> inf ( { k e. ( 1 ... ( M + N ) ) | ( ( F ` c ) ` k ) = 0 } , RR , < ) )   &    |- S = ( c e. ( O \ E ) |-> ( i e. ( 1 ... ( M + N ) ) |-> if ( i <_ ( I ` c ) , ( ( ( I ` c ) + 1 ) - i ) , i ) ) )   &    |- R = ( c e. ( O \ E ) |-> ( ( S ` c ) " c ) )   =>    |- ( C e. ( O \ E ) -> ( 1 e. ( R ` C ) <-> ( I ` C ) e. C ) )
Theorem	ballotlem7 30597*	R is a bijection between two subsets of ( O \ E ): one where a vote for A is picked first, and one where a vote for B is picked first. (Contributed by Thierry Arnoux, 12-Dec-2016.)
|- M e. NN   &    |- N e. NN   &    |- O = { c e. ~P ( 1 ... ( M + N ) ) | ( # ` c ) = M }   &    |- P = ( x e. ~P O |-> ( ( # ` x ) / ( # ` O ) ) )   &    |- F = ( c e. O |-> ( i e. ZZ |-> ( ( # ` ( ( 1 ... i ) i^i c ) ) - ( # ` ( ( 1 ... i ) \ c ) ) ) ) )   &    |- E = { c e. O | A. i e. ( 1 ... ( M + N ) ) 0 < ( ( F ` c ) ` i ) }   &    |- N < M   &    |- I = ( c e. ( O \ E ) |-> inf ( { k e. ( 1 ... ( M + N ) ) | ( ( F ` c ) ` k ) = 0 } , RR , < ) )   &    |- S = ( c e. ( O \ E ) |-> ( i e. ( 1 ... ( M + N ) ) |-> if ( i <_ ( I ` c ) , ( ( ( I ` c ) + 1 ) - i ) , i ) ) )   &    |- R = ( c e. ( O \ E ) |-> ( ( S ` c ) " c ) )   =>    |- ( R |` { c e. ( O \ E ) | 1 e. c } ) : { c e. ( O \ E ) | 1 e. c } -1-1-onto-> { c e. ( O \ E ) | -. 1 e. c }
Theorem	ballotlem8 30598*	There are as many countings with ties starting with a ballot for A as there are starting with a ballot for B. (Contributed by Thierry Arnoux, 7-Dec-2016.)
|- M e. NN   &    |- N e. NN   &    |- O = { c e. ~P ( 1 ... ( M + N ) ) | ( # ` c ) = M }   &    |- P = ( x e. ~P O |-> ( ( # ` x ) / ( # ` O ) ) )   &    |- F = ( c e. O |-> ( i e. ZZ |-> ( ( # ` ( ( 1 ... i ) i^i c ) ) - ( # ` ( ( 1 ... i ) \ c ) ) ) ) )   &    |- E = { c e. O | A. i e. ( 1 ... ( M + N ) ) 0 < ( ( F ` c ) ` i ) }   &    |- N < M   &    |- I = ( c e. ( O \ E ) |-> inf ( { k e. ( 1 ... ( M + N ) ) | ( ( F ` c ) ` k ) = 0 } , RR , < ) )   &    |- S = ( c e. ( O \ E ) |-> ( i e. ( 1 ... ( M + N ) ) |-> if ( i <_ ( I ` c ) , ( ( ( I ` c ) + 1 ) - i ) , i ) ) )   &    |- R = ( c e. ( O \ E ) |-> ( ( S ` c ) " c ) )   =>    |- ( # ` { c e. ( O \ E ) | 1 e. c } ) = ( # ` { c e. ( O \ E ) | -. 1 e. c } )
Theorem	ballotth 30599*	Bertrand's ballot problem : the probability that A is ahead throughout the counting. This is Metamath 100 proof #30. (Contributed by Thierry Arnoux, 7-Dec-2016.)
|- M e. NN   &    |- N e. NN   &    |- O = { c e. ~P ( 1 ... ( M + N ) ) | ( # ` c ) = M }   &    |- P = ( x e. ~P O |-> ( ( # ` x ) / ( # ` O ) ) )   &    |- F = ( c e. O |-> ( i e. ZZ |-> ( ( # ` ( ( 1 ... i ) i^i c ) ) - ( # ` ( ( 1 ... i ) \ c ) ) ) ) )   &    |- E = { c e. O | A. i e. ( 1 ... ( M + N ) ) 0 < ( ( F ` c ) ` i ) }   &    |- N < M   &    |- I = ( c e. ( O \ E ) |-> inf ( { k e. ( 1 ... ( M + N ) ) | ( ( F ` c ) ` k ) = 0 } , RR , < ) )   &    |- S = ( c e. ( O \ E ) |-> ( i e. ( 1 ... ( M + N ) ) |-> if ( i <_ ( I ` c ) , ( ( ( I ` c ) + 1 ) - i ) , i ) ) )   &    |- R = ( c e. ( O \ E ) |-> ( ( S ` c ) " c ) )   =>    |- ( P ` E ) = ( ( M - N ) / ( M + N ) )
20.3.22  Signum (sgn or sign) function - misc. additions
Theorem	sgncl 30600	Closure of the signum. (Contributed by Thierry Arnoux, 28-Sep-2018.)
|- ( A e. RR* -> (sgn ` A ) e. { -u 1 , 0 , 1 } )