P. 292 of Theorem List - Metamath Proof Explorer

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

Type	Label	Description
Statement
Theorem	rrvmbfm 29101	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 29102*	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 29103	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 29104	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 29105	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 29106	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 29107	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 29108	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 29109*	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 29110*	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 29111	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 29112	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 29113	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 ) )
21.3.20.4  Preimage set mapping operator
Syntax	corvc 29114	Extend class notation to include the preimage set mapping operator.
class ∘RV/𝑐 R
Definition	df-orvc 29115*	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 5007- elementhood: { X e. A } as ( X∘RV/𝑐 _E A ) cf. epel 4768- 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 29116*	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 29117*	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 29118*	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 29119*	The value of the preimage mapping operator can be restricted to preimages in the base set of the topology. Cf. orvcval 29116 (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 29120*	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 29121*	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 29122*	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 29123*	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 29124*	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 29125*	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 29126	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 )
21.3.20.5  Distribution Functions
Theorem	orvcelval 29127	Preimage maps produced by the "elementhood" 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 29128	Preimage maps produced by the "elementhood" 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 29129*	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 29130*	The distribution of a random variable is a probability law (TODO: could be shortened using dstrvval 29129) (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 )
21.3.20.6  Cumulative Distribution Functions
Theorem	orvclteel 29131	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 29132	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 29133*	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 29134	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 29135*	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 29136*	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 )
21.3.20.7  Probabilities - example
Theorem	coinfliplem 29137	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 29138	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 29139	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 29140	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 29141	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 29142	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 29143	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 )
21.3.20.8  Bertrand's Ballot Problem
Theorem	ballotlemoex 29144*	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 29145*	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 29146*	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 29147*	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 29148*	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 29149*	( 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 29150*	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 29151*	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 29152*	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 29153*	( 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 29154*	( 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 29155*	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 29156*	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 29157*	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 29158*	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 29159*	Value of I for a given counting C. (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 ) |-> sup ( { k e. ( 1 ... ( M + N ) ) | ( ( F ` c ) ` k ) = 0 } , RR , `' < ) )   =>    |- ( C e. ( O \ E ) -> ( I ` C ) = sup ( { k e. ( 1 ... ( M + N ) ) | ( ( F ` C ) ` k ) = 0 } , RR , `' < ) )
Theorem	ballotlemiex 29160*	Properties of ( I ` C ). (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 ) |-> sup ( { 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 29161*	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 ) |-> sup ( { k e. ( 1 ... ( M + N ) ) | ( ( F ` c ) ` k ) = 0 } , RR , `' < ) )   =>    |- ( ( C e. ( O \ E ) /\ -. 1 e. C ) -> ( I ` C ) =/= 1 )
Theorem	ballotlemii 29162*	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 ) |-> sup ( { k e. ( 1 ... ( M + N ) ) | ( ( F ` c ) ` k ) = 0 } , RR , `' < ) )   =>    |- ( ( C e. ( O \ E ) /\ 1 e. C ) -> ( I ` C ) =/= 1 )
Theorem	ballotlemsup 29163*	The set of zeroes of F satisfies the conditions to have a supremum (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 ) |-> sup ( { 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 } -. z `' < w /\ A. w e. RR ( w `' < z -> E. y e. { k e. ( 1 ... ( M + N ) ) | ( ( F ` C ) ` k ) = 0 } w `' < y ) ) )
Theorem	ballotlemimin 29164*	( I ` C ) is the first tie. (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 ) |-> sup ( { 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 29165*	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 ) |-> sup ( { k e. ( 1 ... ( M + N ) ) | ( ( F ` c ) ` k ) = 0 } , RR , `' < ) )   =>    |- ( ( C e. ( O \ E ) /\ -. 1 e. C ) -> ( I ` C ) e. C )
Theorem	ballotlem1c 29166*	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 ) |-> sup ( { k e. ( 1 ... ( M + N ) ) | ( ( F ` c ) ` k ) = 0 } , RR , `' < ) )   =>    |- ( ( C e. ( O \ E ) /\ 1 e. C ) -> -. ( I ` C ) e. C )
Theorem	ballotlemsval 29167*	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 ) |-> sup ( { 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 29168*	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 ) |-> sup ( { 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 29169*	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 ) |-> sup ( { 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 29170*	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 ) |-> sup ( { 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 29171*	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 ) |-> sup ( { 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 29172*	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 ) |-> sup ( { 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 29173*	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 ) |-> sup ( { 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 29174*	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 ) |-> sup ( { 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 29175*	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 ) |-> sup ( { 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 29176*	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 ) |-> sup ( { 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 29177*	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 ) |-> sup ( { 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 29178*	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 ) |-> sup ( { 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 29179*	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 ) |-> sup ( { 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 29180*	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 ) |-> sup ( { 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 29181*	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 ) |-> sup ( { 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 29182*	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 ) |-> sup ( { 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 29183*	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 ) |-> sup ( { 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 29184*	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 ) |-> sup ( { 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 29185*	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 ) |-> sup ( { 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 29186*	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 ) |-> sup ( { 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 29187*	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 ) |-> sup ( { 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 29188*	Value of F for a reversed counting ( R ` C ), before the first tie, cannot be zero . (Contributed by Thierry Arnoux, 25-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 ) |-> sup ( { 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 29189*	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 ) |-> sup ( { 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 29190*	Applying R does not change first ties. (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 ) |-> sup ( { 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 29191*	Lemma for ballotlemrinv 29192. (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 ) |-> sup ( { 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 29192*	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 ) |-> sup ( { 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 29193*	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 ) |-> sup ( { 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 29194*	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 ) |-> sup ( { 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 29195*	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 ) |-> sup ( { 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 29196*	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 ) |-> sup ( { 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 ) )
21.3.21  Signum (sgn or sign) function - misc. additions
Theorem	sgncl 29197	Closure of the signum. (Contributed by Thierry Arnoux, 28-Sep-2018.)
|- ( A e. RR* -> (sgn ` A ) e. { -u 1 , 0 , 1 } )
Theorem	sgnclre 29198	Closure of the signum. (Contributed by Thierry Arnoux, 28-Sep-2018.)
|- ( A e. RR -> (sgn ` A ) e. RR )
Theorem	sgnneg 29199	Negation of the signum. (Contributed by Thierry Arnoux, 1-Oct-2018.)
|- ( A e. RR -> (sgn ` -u A ) = -u (sgn ` A ) )
Theorem	sgn3da 29200	A conditional containing a signum is true if it is true in all three possible cases. (Contributed by Thierry Arnoux, 1-Oct-2018.)
|- ( ph -> A e. RR* )   &    |- ( (sgn ` A ) = 0 -> ( ps <-> ch ) )   &    |- ( (sgn ` A ) = 1 -> ( ps <-> th ) )   &    |- ( (sgn ` A ) = -u 1 -> ( ps <-> ta ) )   &    |- ( ( ph /\ A = 0 ) -> ch )   &    |- ( ( ph /\ 0 < A ) -> th )   &    |- ( ( ph /\ A < 0 ) -> ta )   =>    |- ( ph -> ps )