P. 345 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 34401-34500   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	cndprobin 34401	An identity linking conditional probability and intersection. (Contributed by Thierry Arnoux, 13-Dec-2016.) (Revised by Thierry Arnoux, 21-Jan-2017.)
⊢ (((𝑃 ∈ Prob ∧ 𝐴 ∈ dom 𝑃 ∧ 𝐵 ∈ dom 𝑃) ∧ (𝑃‘𝐵) ≠ 0) → (((cprob‘𝑃)‘⟨𝐴, 𝐵⟩) · (𝑃‘𝐵)) = (𝑃‘(𝐴 ∩ 𝐵)))
Theorem	cndprob01 34402	The conditional probability has values in [0, 1]. (Contributed by Thierry Arnoux, 13-Dec-2016.) (Revised by Thierry Arnoux, 21-Jan-2017.)
⊢ (((𝑃 ∈ Prob ∧ 𝐴 ∈ dom 𝑃 ∧ 𝐵 ∈ dom 𝑃) ∧ (𝑃‘𝐵) ≠ 0) → ((cprob‘𝑃)‘⟨𝐴, 𝐵⟩) ∈ (0[,]1))
Theorem	cndprobtot 34403	The conditional probability given a certain event is one. (Contributed by Thierry Arnoux, 20-Dec-2016.) (Revised by Thierry Arnoux, 21-Jan-2017.)
⊢ ((𝑃 ∈ Prob ∧ 𝐴 ∈ dom 𝑃 ∧ (𝑃‘𝐴) ≠ 0) → ((cprob‘𝑃)‘⟨∪ dom 𝑃, 𝐴⟩) = 1)
Theorem	cndprobnul 34404	The conditional probability given empty event is zero. (Contributed by Thierry Arnoux, 20-Dec-2016.) (Revised by Thierry Arnoux, 21-Jan-2017.)
⊢ ((𝑃 ∈ Prob ∧ 𝐴 ∈ dom 𝑃 ∧ (𝑃‘𝐴) ≠ 0) → ((cprob‘𝑃)‘⟨∅, 𝐴⟩) = 0)
Theorem	cndprobprob 34405*	The conditional probability defines a probability law. (Contributed by Thierry Arnoux, 23-Dec-2016.) (Revised by Thierry Arnoux, 21-Jan-2017.)
⊢ ((𝑃 ∈ Prob ∧ 𝐵 ∈ dom 𝑃 ∧ (𝑃‘𝐵) ≠ 0) → (𝑎 ∈ dom 𝑃 ↦ ((cprob‘𝑃)‘⟨𝑎, 𝐵⟩)) ∈ Prob)
Theorem	bayesth 34406	Bayes Theorem. (Contributed by Thierry Arnoux, 20-Dec-2016.) (Revised by Thierry Arnoux, 21-Jan-2017.)
⊢ (((𝑃 ∈ Prob ∧ 𝐴 ∈ dom 𝑃 ∧ 𝐵 ∈ dom 𝑃) ∧ (𝑃‘𝐴) ≠ 0 ∧ (𝑃‘𝐵) ≠ 0) → ((cprob‘𝑃)‘⟨𝐴, 𝐵⟩) = ((((cprob‘𝑃)‘⟨𝐵, 𝐴⟩) · (𝑃‘𝐴)) / (𝑃‘𝐵)))
21.3.23.3  Real-valued Random Variables
Syntax	crrv 34407	Extend class notation with the class of real-valued random variables.
class rRndVar
Definition	df-rrv 34408	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 = (𝑝 ∈ Prob ↦ (dom 𝑝MblFnM𝔅ℝ))
Theorem	rrvmbfm 34409	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.)
⊢ (𝜑 → 𝑃 ∈ Prob)    ⇒   ⊢ (𝜑 → (𝑋 ∈ (rRndVar‘𝑃) ↔ 𝑋 ∈ (dom 𝑃MblFnM𝔅ℝ)))
Theorem	isrrvv 34410*	Elementhood to the set of real-valued random variables with respect to the probability 𝑃. (Contributed by Thierry Arnoux, 25-Jan-2017.)
⊢ (𝜑 → 𝑃 ∈ Prob)    ⇒   ⊢ (𝜑 → (𝑋 ∈ (rRndVar‘𝑃) ↔ (𝑋:∪ dom 𝑃⟶ℝ ∧ ∀𝑦 ∈ 𝔅ℝ (◡𝑋 “ 𝑦) ∈ dom 𝑃)))
Theorem	rrvvf 34411	A real-valued random variable is a function. (Contributed by Thierry Arnoux, 25-Jan-2017.)
⊢ (𝜑 → 𝑃 ∈ Prob)    &   ⊢ (𝜑 → 𝑋 ∈ (rRndVar‘𝑃))    ⇒   ⊢ (𝜑 → 𝑋:∪ dom 𝑃⟶ℝ)
Theorem	rrvfn 34412	A real-valued random variable is a function over the universe. (Contributed by Thierry Arnoux, 25-Jan-2017.)
⊢ (𝜑 → 𝑃 ∈ Prob)    &   ⊢ (𝜑 → 𝑋 ∈ (rRndVar‘𝑃))    ⇒   ⊢ (𝜑 → 𝑋 Fn ∪ dom 𝑃)
Theorem	rrvdm 34413	The domain of a random variable is the universe. (Contributed by Thierry Arnoux, 25-Jan-2017.)
⊢ (𝜑 → 𝑃 ∈ Prob)    &   ⊢ (𝜑 → 𝑋 ∈ (rRndVar‘𝑃))    ⇒   ⊢ (𝜑 → dom 𝑋 = ∪ dom 𝑃)
Theorem	rrvrnss 34414	The range of a random variable as a subset of ℝ. (Contributed by Thierry Arnoux, 6-Feb-2017.)
⊢ (𝜑 → 𝑃 ∈ Prob)    &   ⊢ (𝜑 → 𝑋 ∈ (rRndVar‘𝑃))    ⇒   ⊢ (𝜑 → ran 𝑋 ⊆ ℝ)
Theorem	rrvf2 34415	A real-valued random variable is a function. (Contributed by Thierry Arnoux, 25-Jan-2017.)
⊢ (𝜑 → 𝑃 ∈ Prob)    &   ⊢ (𝜑 → 𝑋 ∈ (rRndVar‘𝑃))    ⇒   ⊢ (𝜑 → 𝑋:dom 𝑋⟶ℝ)
Theorem	rrvdmss 34416	The domain of a random variable. This is useful to shorten proofs. (Contributed by Thierry Arnoux, 25-Jan-2017.)
⊢ (𝜑 → 𝑃 ∈ Prob)    &   ⊢ (𝜑 → 𝑋 ∈ (rRndVar‘𝑃))    ⇒   ⊢ (𝜑 → ∪ dom 𝑃 ⊆ dom 𝑋)
Theorem	rrvfinvima 34417*	For a real-value random variable 𝑋, any open interval in ℝ is the image of a measurable set. (Contributed by Thierry Arnoux, 25-Jan-2017.)
⊢ (𝜑 → 𝑃 ∈ Prob)    &   ⊢ (𝜑 → 𝑋 ∈ (rRndVar‘𝑃))    ⇒   ⊢ (𝜑 → ∀𝑦 ∈ 𝔅ℝ (◡𝑋 “ 𝑦) ∈ dom 𝑃)
Theorem	0rrv 34418*	The constant function equal to zero is a random variable. (Contributed by Thierry Arnoux, 16-Jan-2017.) (Revised by Thierry Arnoux, 30-Jan-2017.)
⊢ (𝜑 → 𝑃 ∈ Prob)    ⇒   ⊢ (𝜑 → (𝑥 ∈ ∪ dom 𝑃 ↦ 0) ∈ (rRndVar‘𝑃))
Theorem	rrvadd 34419	The sum of two random variables is a random variable. (Contributed by Thierry Arnoux, 4-Jun-2017.)
⊢ (𝜑 → 𝑃 ∈ Prob)    &   ⊢ (𝜑 → 𝑋 ∈ (rRndVar‘𝑃))    &   ⊢ (𝜑 → 𝑌 ∈ (rRndVar‘𝑃))    ⇒   ⊢ (𝜑 → (𝑋 ∘f + 𝑌) ∈ (rRndVar‘𝑃))
Theorem	rrvmulc 34420	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.)
⊢ (𝜑 → 𝑃 ∈ Prob)    &   ⊢ (𝜑 → 𝑋 ∈ (rRndVar‘𝑃))    &   ⊢ (𝜑 → 𝐶 ∈ ℝ)    ⇒   ⊢ (𝜑 → (𝑋 ∘f/c · 𝐶) ∈ (rRndVar‘𝑃))
Theorem	rrvsum 34421	An indexed sum of random variables is a random variable. (Contributed by Thierry Arnoux, 22-May-2017.)
⊢ (𝜑 → 𝑃 ∈ Prob)    &   ⊢ (𝜑 → 𝑋:ℕ⟶(rRndVar‘𝑃))    &   ⊢ ((𝜑 ∧ 𝑁 ∈ ℕ) → 𝑆 = (seq1( ∘f + , 𝑋)‘𝑁))    ⇒   ⊢ ((𝜑 ∧ 𝑁 ∈ ℕ) → 𝑆 ∈ (rRndVar‘𝑃))
Theorem	boolesineq 34422*	Boole's inequality (union bound). For any finite or countable collection of events, the probability of their union is at most the sum of their probabilities. (Suggested by DeepSeek R1.) (Contributed by Ender Ting, 30-Apr-2025.)
⊢ ((𝑃 ∈ Prob ∧ 𝐴:ℕ⟶dom 𝑃) → (𝑃‘∪ 𝑛 ∈ ℕ (𝐴‘𝑛)) ≤ Σ*𝑛 ∈ ℕ(𝑃‘(𝐴‘𝑛)))
21.3.23.4  Preimage set mapping operator
Syntax	corvc 34423	Extend class notation to include the preimage set mapping operator.
class ∘RV/𝑐𝑅
Definition	df-orvc 34424*	Define the preimage set mapping operator. In probability theory, the notation 𝑃(𝑋 = 𝐴) denotes the probability that a random variable 𝑋 takes the value 𝐴. We introduce here an operator which enables to write this in Metamath as (𝑃‘(𝑋∘RV/𝑐 I 𝐴)), and keep a similar notation. Because with this notation (𝑋∘RV/𝑐 I 𝐴) is a set, we can also apply it to conditional probabilities, like in (𝑃‘(𝑋∘RV/𝑐 I 𝐴) ∣ (𝑌∘RV/𝑐 I 𝐵))). The oRVC operator transforms a relation 𝑅 into an operation taking a random variable 𝑋 and a constant 𝐶, and returning the preimage through 𝑋 of the equivalence class of 𝐶. The most commonly used relations are: - equality: {𝑋 = 𝐴} as (𝑋∘RV/𝑐 I 𝐴) cf. ideq 5799- elementhood: {𝑋 ∈ 𝐴} as (𝑋∘RV/𝑐 E 𝐴) cf. epel 5526- less-than: {𝑋 ≤ 𝐴} as (𝑋∘RV/𝑐 ≤ 𝐴) 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/𝑐𝑅 = (𝑥 ∈ {𝑥 ∣ Fun 𝑥}, 𝑎 ∈ V ↦ (◡𝑥 “ {𝑦 ∣ 𝑦𝑅𝑎}))
Theorem	orvcval 34425*	Value of the preimage mapping operator applied on a given random variable and constant. (Contributed by Thierry Arnoux, 19-Jan-2017.)
⊢ (𝜑 → Fun 𝑋)    &   ⊢ (𝜑 → 𝑋 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑊)    ⇒   ⊢ (𝜑 → (𝑋∘RV/𝑐𝑅𝐴) = (◡𝑋 “ {𝑦 ∣ 𝑦𝑅𝐴}))
Theorem	orvcval2 34426*	Another way to express the value of the preimage mapping operator. (Contributed by Thierry Arnoux, 19-Jan-2017.)
⊢ (𝜑 → Fun 𝑋)    &   ⊢ (𝜑 → 𝑋 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑊)    ⇒   ⊢ (𝜑 → (𝑋∘RV/𝑐𝑅𝐴) = {𝑧 ∈ dom 𝑋 ∣ (𝑋‘𝑧)𝑅𝐴})
Theorem	elorvc 34427*	Elementhood of a preimage. (Contributed by Thierry Arnoux, 21-Jan-2017.)
⊢ (𝜑 → Fun 𝑋)    &   ⊢ (𝜑 → 𝑋 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑊)    ⇒   ⊢ ((𝜑 ∧ 𝑧 ∈ dom 𝑋) → (𝑧 ∈ (𝑋∘RV/𝑐𝑅𝐴) ↔ (𝑋‘𝑧)𝑅𝐴))
Theorem	orvcval4 34428*	The value of the preimage mapping operator can be restricted to preimages in the base set of the topology. Cf. orvcval 34425. (Contributed by Thierry Arnoux, 21-Jan-2017.)
⊢ (𝜑 → 𝑆 ∈ ∪ ran sigAlgebra)    &   ⊢ (𝜑 → 𝐽 ∈ Top)    &   ⊢ (𝜑 → 𝑋 ∈ (𝑆MblFnM(sigaGen‘𝐽)))    &   ⊢ (𝜑 → 𝐴 ∈ 𝑉)    ⇒   ⊢ (𝜑 → (𝑋∘RV/𝑐𝑅𝐴) = (◡𝑋 “ {𝑦 ∈ ∪ 𝐽 ∣ 𝑦𝑅𝐴}))
Theorem	orvcoel 34429*	If the relation produces open sets, preimage maps by a measurable function are measurable sets. (Contributed by Thierry Arnoux, 21-Jan-2017.)
⊢ (𝜑 → 𝑆 ∈ ∪ ran sigAlgebra)    &   ⊢ (𝜑 → 𝐽 ∈ Top)    &   ⊢ (𝜑 → 𝑋 ∈ (𝑆MblFnM(sigaGen‘𝐽)))    &   ⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ (𝜑 → {𝑦 ∈ ∪ 𝐽 ∣ 𝑦𝑅𝐴} ∈ 𝐽)    ⇒   ⊢ (𝜑 → (𝑋∘RV/𝑐𝑅𝐴) ∈ 𝑆)
Theorem	orvccel 34430*	If the relation produces closed sets, preimage maps by a measurable function are measurable sets. (Contributed by Thierry Arnoux, 21-Jan-2017.)
⊢ (𝜑 → 𝑆 ∈ ∪ ran sigAlgebra)    &   ⊢ (𝜑 → 𝐽 ∈ Top)    &   ⊢ (𝜑 → 𝑋 ∈ (𝑆MblFnM(sigaGen‘𝐽)))    &   ⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ (𝜑 → {𝑦 ∈ ∪ 𝐽 ∣ 𝑦𝑅𝐴} ∈ (Clsd‘𝐽))    ⇒   ⊢ (𝜑 → (𝑋∘RV/𝑐𝑅𝐴) ∈ 𝑆)
Theorem	elorrvc 34431*	Elementhood of a preimage for a real-valued random variable. (Contributed by Thierry Arnoux, 21-Jan-2017.)
⊢ (𝜑 → 𝑃 ∈ Prob)    &   ⊢ (𝜑 → 𝑋 ∈ (rRndVar‘𝑃))    &   ⊢ (𝜑 → 𝐴 ∈ 𝑉)    ⇒   ⊢ ((𝜑 ∧ 𝑧 ∈ ∪ dom 𝑃) → (𝑧 ∈ (𝑋∘RV/𝑐𝑅𝐴) ↔ (𝑋‘𝑧)𝑅𝐴))
Theorem	orrvcval4 34432*	The value of the preimage mapping operator can be restricted to preimages of subsets of ℝ. (Contributed by Thierry Arnoux, 21-Jan-2017.)
⊢ (𝜑 → 𝑃 ∈ Prob)    &   ⊢ (𝜑 → 𝑋 ∈ (rRndVar‘𝑃))    &   ⊢ (𝜑 → 𝐴 ∈ 𝑉)    ⇒   ⊢ (𝜑 → (𝑋∘RV/𝑐𝑅𝐴) = (◡𝑋 “ {𝑦 ∈ ℝ ∣ 𝑦𝑅𝐴}))
Theorem	orrvcoel 34433*	If the relation produces open sets, preimage maps of a random variable are measurable sets. (Contributed by Thierry Arnoux, 21-Jan-2017.)
⊢ (𝜑 → 𝑃 ∈ Prob)    &   ⊢ (𝜑 → 𝑋 ∈ (rRndVar‘𝑃))    &   ⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ (𝜑 → {𝑦 ∈ ℝ ∣ 𝑦𝑅𝐴} ∈ (topGen‘ran (,)))    ⇒   ⊢ (𝜑 → (𝑋∘RV/𝑐𝑅𝐴) ∈ dom 𝑃)
Theorem	orrvccel 34434*	If the relation produces closed sets, preimage maps are measurable sets. (Contributed by Thierry Arnoux, 21-Jan-2017.)
⊢ (𝜑 → 𝑃 ∈ Prob)    &   ⊢ (𝜑 → 𝑋 ∈ (rRndVar‘𝑃))    &   ⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ (𝜑 → {𝑦 ∈ ℝ ∣ 𝑦𝑅𝐴} ∈ (Clsd‘(topGen‘ran (,))))    ⇒   ⊢ (𝜑 → (𝑋∘RV/𝑐𝑅𝐴) ∈ dom 𝑃)
Theorem	orvcgteel 34435	Preimage maps produced by the "greater than or equal to" relation are measurable sets. (Contributed by Thierry Arnoux, 5-Feb-2017.)
⊢ (𝜑 → 𝑃 ∈ Prob)    &   ⊢ (𝜑 → 𝑋 ∈ (rRndVar‘𝑃))    &   ⊢ (𝜑 → 𝐴 ∈ ℝ)    ⇒   ⊢ (𝜑 → (𝑋∘RV/𝑐◡ ≤ 𝐴) ∈ dom 𝑃)
21.3.23.5  Distribution Functions
Theorem	orvcelval 34436	Preimage maps produced by the membership relation. (Contributed by Thierry Arnoux, 6-Feb-2017.)
⊢ (𝜑 → 𝑃 ∈ Prob)    &   ⊢ (𝜑 → 𝑋 ∈ (rRndVar‘𝑃))    &   ⊢ (𝜑 → 𝐴 ∈ 𝔅ℝ)    ⇒   ⊢ (𝜑 → (𝑋∘RV/𝑐 E 𝐴) = (◡𝑋 “ 𝐴))
Theorem	orvcelel 34437	Preimage maps produced by the membership relation are measurable sets. (Contributed by Thierry Arnoux, 5-Feb-2017.)
⊢ (𝜑 → 𝑃 ∈ Prob)    &   ⊢ (𝜑 → 𝑋 ∈ (rRndVar‘𝑃))    &   ⊢ (𝜑 → 𝐴 ∈ 𝔅ℝ)    ⇒   ⊢ (𝜑 → (𝑋∘RV/𝑐 E 𝐴) ∈ dom 𝑃)
Theorem	dstrvval 34438*	The value of the distribution of a random variable. (Contributed by Thierry Arnoux, 9-Feb-2017.)
⊢ (𝜑 → 𝑃 ∈ Prob)    &   ⊢ (𝜑 → 𝑋 ∈ (rRndVar‘𝑃))    &   ⊢ (𝜑 → 𝐷 = (𝑎 ∈ 𝔅ℝ ↦ (𝑃‘(𝑋∘RV/𝑐 E 𝑎))))    &   ⊢ (𝜑 → 𝐴 ∈ 𝔅ℝ)    ⇒   ⊢ (𝜑 → (𝐷‘𝐴) = (𝑃‘(◡𝑋 “ 𝐴)))
Theorem	dstrvprob 34439*	The distribution of a random variable is a probability law. (TODO: could be shortened using dstrvval 34438). (Contributed by Thierry Arnoux, 10-Feb-2017.)
⊢ (𝜑 → 𝑃 ∈ Prob)    &   ⊢ (𝜑 → 𝑋 ∈ (rRndVar‘𝑃))    &   ⊢ (𝜑 → 𝐷 = (𝑎 ∈ 𝔅ℝ ↦ (𝑃‘(𝑋∘RV/𝑐 E 𝑎))))    ⇒   ⊢ (𝜑 → 𝐷 ∈ Prob)
21.3.23.6  Cumulative Distribution Functions
Theorem	orvclteel 34440	Preimage maps produced by the "less than or equal to" relation are measurable sets. (Contributed by Thierry Arnoux, 4-Feb-2017.)
⊢ (𝜑 → 𝑃 ∈ Prob)    &   ⊢ (𝜑 → 𝑋 ∈ (rRndVar‘𝑃))    &   ⊢ (𝜑 → 𝐴 ∈ ℝ)    ⇒   ⊢ (𝜑 → (𝑋∘RV/𝑐 ≤ 𝐴) ∈ dom 𝑃)
Theorem	dstfrvel 34441	Elementhood of preimage maps produced by the "less than or equal to" relation. (Contributed by Thierry Arnoux, 13-Feb-2017.)
⊢ (𝜑 → 𝑃 ∈ Prob)    &   ⊢ (𝜑 → 𝑋 ∈ (rRndVar‘𝑃))    &   ⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ∪ dom 𝑃)    &   ⊢ (𝜑 → (𝑋‘𝐵) ≤ 𝐴)    ⇒   ⊢ (𝜑 → 𝐵 ∈ (𝑋∘RV/𝑐 ≤ 𝐴))
Theorem	dstfrvunirn 34442*	The limit of all preimage maps by the "less than or equal to" relation is the universe. (Contributed by Thierry Arnoux, 12-Feb-2017.)
⊢ (𝜑 → 𝑃 ∈ Prob)    &   ⊢ (𝜑 → 𝑋 ∈ (rRndVar‘𝑃))    ⇒   ⊢ (𝜑 → ∪ ran (𝑛 ∈ ℕ ↦ (𝑋∘RV/𝑐 ≤ 𝑛)) = ∪ dom 𝑃)
Theorem	orvclteinc 34443	Preimage maps produced by the "less than or equal to" relation are increasing. (Contributed by Thierry Arnoux, 11-Feb-2017.)
⊢ (𝜑 → 𝑃 ∈ Prob)    &   ⊢ (𝜑 → 𝑋 ∈ (rRndVar‘𝑃))    &   ⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → 𝐴 ≤ 𝐵)    ⇒   ⊢ (𝜑 → (𝑋∘RV/𝑐 ≤ 𝐴) ⊆ (𝑋∘RV/𝑐 ≤ 𝐵))
Theorem	dstfrvinc 34444*	A cumulative distribution function is nondecreasing. (Contributed by Thierry Arnoux, 11-Feb-2017.)
⊢ (𝜑 → 𝑃 ∈ Prob)    &   ⊢ (𝜑 → 𝑋 ∈ (rRndVar‘𝑃))    &   ⊢ (𝜑 → 𝐹 = (𝑥 ∈ ℝ ↦ (𝑃‘(𝑋∘RV/𝑐 ≤ 𝑥))))    &   ⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → 𝐴 ≤ 𝐵)    ⇒   ⊢ (𝜑 → (𝐹‘𝐴) ≤ (𝐹‘𝐵))
Theorem	dstfrvclim1 34445*	The limit of the cumulative distribution function is one. (Contributed by Thierry Arnoux, 12-Feb-2017.) (Revised by Thierry Arnoux, 11-Jul-2017.)
⊢ (𝜑 → 𝑃 ∈ Prob)    &   ⊢ (𝜑 → 𝑋 ∈ (rRndVar‘𝑃))    &   ⊢ (𝜑 → 𝐹 = (𝑥 ∈ ℝ ↦ (𝑃‘(𝑋∘RV/𝑐 ≤ 𝑥))))    ⇒   ⊢ (𝜑 → 𝐹 ⇝ 1)
21.3.23.7  Probabilities - example
Theorem	coinfliplem 34446	Division in the extended real numbers can be used for the coin-flip example. (Contributed by Thierry Arnoux, 15-Jan-2017.)
⊢ 𝐻 ∈ V    &   ⊢ 𝑇 ∈ V    &   ⊢ 𝐻 ≠ 𝑇    &   ⊢ 𝑃 = ((♯ ↾ 𝒫 {𝐻, 𝑇}) ∘f/c / 2)    &   ⊢ 𝑋 = {⟨𝐻, 1⟩, ⟨𝑇, 0⟩}    ⇒   ⊢ 𝑃 = ((♯ ↾ 𝒫 {𝐻, 𝑇}) ∘f/c /𝑒 2)
Theorem	coinflipprob 34447	The 𝑃 we defined for coin-flip is a probability law. (Contributed by Thierry Arnoux, 15-Jan-2017.)
⊢ 𝐻 ∈ V    &   ⊢ 𝑇 ∈ V    &   ⊢ 𝐻 ≠ 𝑇    &   ⊢ 𝑃 = ((♯ ↾ 𝒫 {𝐻, 𝑇}) ∘f/c / 2)    &   ⊢ 𝑋 = {⟨𝐻, 1⟩, ⟨𝑇, 0⟩}    ⇒   ⊢ 𝑃 ∈ Prob
Theorem	coinflipspace 34448	The space of our coin-flip probability. (Contributed by Thierry Arnoux, 15-Jan-2017.)
⊢ 𝐻 ∈ V    &   ⊢ 𝑇 ∈ V    &   ⊢ 𝐻 ≠ 𝑇    &   ⊢ 𝑃 = ((♯ ↾ 𝒫 {𝐻, 𝑇}) ∘f/c / 2)    &   ⊢ 𝑋 = {⟨𝐻, 1⟩, ⟨𝑇, 0⟩}    ⇒   ⊢ dom 𝑃 = 𝒫 {𝐻, 𝑇}
Theorem	coinflipuniv 34449	The universe of our coin-flip probability is {𝐻, 𝑇}. (Contributed by Thierry Arnoux, 15-Jan-2017.)
⊢ 𝐻 ∈ V    &   ⊢ 𝑇 ∈ V    &   ⊢ 𝐻 ≠ 𝑇    &   ⊢ 𝑃 = ((♯ ↾ 𝒫 {𝐻, 𝑇}) ∘f/c / 2)    &   ⊢ 𝑋 = {⟨𝐻, 1⟩, ⟨𝑇, 0⟩}    ⇒   ⊢ ∪ dom 𝑃 = {𝐻, 𝑇}
Theorem	coinfliprv 34450	The 𝑋 we defined for coin-flip is a random variable. (Contributed by Thierry Arnoux, 12-Jan-2017.)
⊢ 𝐻 ∈ V    &   ⊢ 𝑇 ∈ V    &   ⊢ 𝐻 ≠ 𝑇    &   ⊢ 𝑃 = ((♯ ↾ 𝒫 {𝐻, 𝑇}) ∘f/c / 2)    &   ⊢ 𝑋 = {⟨𝐻, 1⟩, ⟨𝑇, 0⟩}    ⇒   ⊢ 𝑋 ∈ (rRndVar‘𝑃)
Theorem	coinflippv 34451	The probability of heads is one-half. (Contributed by Thierry Arnoux, 15-Jan-2017.)
⊢ 𝐻 ∈ V    &   ⊢ 𝑇 ∈ V    &   ⊢ 𝐻 ≠ 𝑇    &   ⊢ 𝑃 = ((♯ ↾ 𝒫 {𝐻, 𝑇}) ∘f/c / 2)    &   ⊢ 𝑋 = {⟨𝐻, 1⟩, ⟨𝑇, 0⟩}    ⇒   ⊢ (𝑃‘{𝐻}) = (1 / 2)
Theorem	coinflippvt 34452	The probability of tails is one-half. (Contributed by Thierry Arnoux, 5-Feb-2017.)
⊢ 𝐻 ∈ V    &   ⊢ 𝑇 ∈ V    &   ⊢ 𝐻 ≠ 𝑇    &   ⊢ 𝑃 = ((♯ ↾ 𝒫 {𝐻, 𝑇}) ∘f/c / 2)    &   ⊢ 𝑋 = {⟨𝐻, 1⟩, ⟨𝑇, 0⟩}    ⇒   ⊢ (𝑃‘{𝑇}) = (1 / 2)
21.3.23.8  Bertrand's Ballot Problem
Theorem	ballotlemoex 34453*	𝑂 is a set. (Contributed by Thierry Arnoux, 7-Dec-2016.)
⊢ 𝑀 ∈ ℕ    &   ⊢ 𝑁 ∈ ℕ    &   ⊢ 𝑂 = {𝑐 ∈ 𝒫 (1...(𝑀 + 𝑁)) ∣ (♯‘𝑐) = 𝑀}    ⇒   ⊢ 𝑂 ∈ V
Theorem	ballotlem1 34454*	The size of the universe is a binomial coefficient. (Contributed by Thierry Arnoux, 23-Nov-2016.)
⊢ 𝑀 ∈ ℕ    &   ⊢ 𝑁 ∈ ℕ    &   ⊢ 𝑂 = {𝑐 ∈ 𝒫 (1...(𝑀 + 𝑁)) ∣ (♯‘𝑐) = 𝑀}    ⇒   ⊢ (♯‘𝑂) = ((𝑀 + 𝑁)C𝑀)
Theorem	ballotlemelo 34455*	Elementhood in 𝑂. (Contributed by Thierry Arnoux, 17-Apr-2017.)
⊢ 𝑀 ∈ ℕ    &   ⊢ 𝑁 ∈ ℕ    &   ⊢ 𝑂 = {𝑐 ∈ 𝒫 (1...(𝑀 + 𝑁)) ∣ (♯‘𝑐) = 𝑀}    ⇒   ⊢ (𝐶 ∈ 𝑂 ↔ (𝐶 ⊆ (1...(𝑀 + 𝑁)) ∧ (♯‘𝐶) = 𝑀))
Theorem	ballotlem2 34456*	The probability that the first vote picked in a count is a B. (Contributed by Thierry Arnoux, 23-Nov-2016.)
⊢ 𝑀 ∈ ℕ    &   ⊢ 𝑁 ∈ ℕ    &   ⊢ 𝑂 = {𝑐 ∈ 𝒫 (1...(𝑀 + 𝑁)) ∣ (♯‘𝑐) = 𝑀}    &   ⊢ 𝑃 = (𝑥 ∈ 𝒫 𝑂 ↦ ((♯‘𝑥) / (♯‘𝑂)))    ⇒   ⊢ (𝑃‘{𝑐 ∈ 𝑂 ∣ ¬ 1 ∈ 𝑐}) = (𝑁 / (𝑀 + 𝑁))
Theorem	ballotlemfval 34457*	The value of 𝐹. (Contributed by Thierry Arnoux, 23-Nov-2016.)
⊢ 𝑀 ∈ ℕ    &   ⊢ 𝑁 ∈ ℕ    &   ⊢ 𝑂 = {𝑐 ∈ 𝒫 (1...(𝑀 + 𝑁)) ∣ (♯‘𝑐) = 𝑀}    &   ⊢ 𝑃 = (𝑥 ∈ 𝒫 𝑂 ↦ ((♯‘𝑥) / (♯‘𝑂)))    &   ⊢ 𝐹 = (𝑐 ∈ 𝑂 ↦ (𝑖 ∈ ℤ ↦ ((♯‘((1...𝑖) ∩ 𝑐)) − (♯‘((1...𝑖) ∖ 𝑐)))))    &   ⊢ (𝜑 → 𝐶 ∈ 𝑂)    &   ⊢ (𝜑 → 𝐽 ∈ ℤ)    ⇒   ⊢ (𝜑 → ((𝐹‘𝐶)‘𝐽) = ((♯‘((1...𝐽) ∩ 𝐶)) − (♯‘((1...𝐽) ∖ 𝐶))))
Theorem	ballotlemfelz 34458*	(𝐹‘𝐶) has values in ℤ. (Contributed by Thierry Arnoux, 23-Nov-2016.)
⊢ 𝑀 ∈ ℕ    &   ⊢ 𝑁 ∈ ℕ    &   ⊢ 𝑂 = {𝑐 ∈ 𝒫 (1...(𝑀 + 𝑁)) ∣ (♯‘𝑐) = 𝑀}    &   ⊢ 𝑃 = (𝑥 ∈ 𝒫 𝑂 ↦ ((♯‘𝑥) / (♯‘𝑂)))    &   ⊢ 𝐹 = (𝑐 ∈ 𝑂 ↦ (𝑖 ∈ ℤ ↦ ((♯‘((1...𝑖) ∩ 𝑐)) − (♯‘((1...𝑖) ∖ 𝑐)))))    &   ⊢ (𝜑 → 𝐶 ∈ 𝑂)    &   ⊢ (𝜑 → 𝐽 ∈ ℤ)    ⇒   ⊢ (𝜑 → ((𝐹‘𝐶)‘𝐽) ∈ ℤ)
Theorem	ballotlemfp1 34459*	If the 𝐽 th ballot is for A, (𝐹‘𝐶) goes up 1. If the 𝐽 th ballot is for B, (𝐹‘𝐶) goes down 1. (Contributed by Thierry Arnoux, 24-Nov-2016.)
⊢ 𝑀 ∈ ℕ    &   ⊢ 𝑁 ∈ ℕ    &   ⊢ 𝑂 = {𝑐 ∈ 𝒫 (1...(𝑀 + 𝑁)) ∣ (♯‘𝑐) = 𝑀}    &   ⊢ 𝑃 = (𝑥 ∈ 𝒫 𝑂 ↦ ((♯‘𝑥) / (♯‘𝑂)))    &   ⊢ 𝐹 = (𝑐 ∈ 𝑂 ↦ (𝑖 ∈ ℤ ↦ ((♯‘((1...𝑖) ∩ 𝑐)) − (♯‘((1...𝑖) ∖ 𝑐)))))    &   ⊢ (𝜑 → 𝐶 ∈ 𝑂)    &   ⊢ (𝜑 → 𝐽 ∈ ℕ)    ⇒   ⊢ (𝜑 → ((¬ 𝐽 ∈ 𝐶 → ((𝐹‘𝐶)‘𝐽) = (((𝐹‘𝐶)‘(𝐽 − 1)) − 1)) ∧ (𝐽 ∈ 𝐶 → ((𝐹‘𝐶)‘𝐽) = (((𝐹‘𝐶)‘(𝐽 − 1)) + 1))))
Theorem	ballotlemfc0 34460*	𝐹 takes value 0 between negative and positive values. (Contributed by Thierry Arnoux, 24-Nov-2016.)
⊢ 𝑀 ∈ ℕ    &   ⊢ 𝑁 ∈ ℕ    &   ⊢ 𝑂 = {𝑐 ∈ 𝒫 (1...(𝑀 + 𝑁)) ∣ (♯‘𝑐) = 𝑀}    &   ⊢ 𝑃 = (𝑥 ∈ 𝒫 𝑂 ↦ ((♯‘𝑥) / (♯‘𝑂)))    &   ⊢ 𝐹 = (𝑐 ∈ 𝑂 ↦ (𝑖 ∈ ℤ ↦ ((♯‘((1...𝑖) ∩ 𝑐)) − (♯‘((1...𝑖) ∖ 𝑐)))))    &   ⊢ (𝜑 → 𝐶 ∈ 𝑂)    &   ⊢ (𝜑 → 𝐽 ∈ ℕ)    &   ⊢ (𝜑 → ∃𝑖 ∈ (1...𝐽)((𝐹‘𝐶)‘𝑖) ≤ 0)    &   ⊢ (𝜑 → 0 < ((𝐹‘𝐶)‘𝐽))    ⇒   ⊢ (𝜑 → ∃𝑘 ∈ (1...𝐽)((𝐹‘𝐶)‘𝑘) = 0)
Theorem	ballotlemfcc 34461*	𝐹 takes value 0 between positive and negative values. (Contributed by Thierry Arnoux, 2-Apr-2017.)
⊢ 𝑀 ∈ ℕ    &   ⊢ 𝑁 ∈ ℕ    &   ⊢ 𝑂 = {𝑐 ∈ 𝒫 (1...(𝑀 + 𝑁)) ∣ (♯‘𝑐) = 𝑀}    &   ⊢ 𝑃 = (𝑥 ∈ 𝒫 𝑂 ↦ ((♯‘𝑥) / (♯‘𝑂)))    &   ⊢ 𝐹 = (𝑐 ∈ 𝑂 ↦ (𝑖 ∈ ℤ ↦ ((♯‘((1...𝑖) ∩ 𝑐)) − (♯‘((1...𝑖) ∖ 𝑐)))))    &   ⊢ (𝜑 → 𝐶 ∈ 𝑂)    &   ⊢ (𝜑 → 𝐽 ∈ ℕ)    &   ⊢ (𝜑 → ∃𝑖 ∈ (1...𝐽)0 ≤ ((𝐹‘𝐶)‘𝑖))    &   ⊢ (𝜑 → ((𝐹‘𝐶)‘𝐽) < 0)    ⇒   ⊢ (𝜑 → ∃𝑘 ∈ (1...𝐽)((𝐹‘𝐶)‘𝑘) = 0)
Theorem	ballotlemfmpn 34462*	(𝐹‘𝐶) finishes counting at (𝑀 − 𝑁). (Contributed by Thierry Arnoux, 25-Nov-2016.)
⊢ 𝑀 ∈ ℕ    &   ⊢ 𝑁 ∈ ℕ    &   ⊢ 𝑂 = {𝑐 ∈ 𝒫 (1...(𝑀 + 𝑁)) ∣ (♯‘𝑐) = 𝑀}    &   ⊢ 𝑃 = (𝑥 ∈ 𝒫 𝑂 ↦ ((♯‘𝑥) / (♯‘𝑂)))    &   ⊢ 𝐹 = (𝑐 ∈ 𝑂 ↦ (𝑖 ∈ ℤ ↦ ((♯‘((1...𝑖) ∩ 𝑐)) − (♯‘((1...𝑖) ∖ 𝑐)))))    ⇒   ⊢ (𝐶 ∈ 𝑂 → ((𝐹‘𝐶)‘(𝑀 + 𝑁)) = (𝑀 − 𝑁))
Theorem	ballotlemfval0 34463*	(𝐹‘𝐶) always starts counting at 0 . (Contributed by Thierry Arnoux, 25-Nov-2016.)
⊢ 𝑀 ∈ ℕ    &   ⊢ 𝑁 ∈ ℕ    &   ⊢ 𝑂 = {𝑐 ∈ 𝒫 (1...(𝑀 + 𝑁)) ∣ (♯‘𝑐) = 𝑀}    &   ⊢ 𝑃 = (𝑥 ∈ 𝒫 𝑂 ↦ ((♯‘𝑥) / (♯‘𝑂)))    &   ⊢ 𝐹 = (𝑐 ∈ 𝑂 ↦ (𝑖 ∈ ℤ ↦ ((♯‘((1...𝑖) ∩ 𝑐)) − (♯‘((1...𝑖) ∖ 𝑐)))))    ⇒   ⊢ (𝐶 ∈ 𝑂 → ((𝐹‘𝐶)‘0) = 0)
Theorem	ballotleme 34464*	Elements of 𝐸. (Contributed by Thierry Arnoux, 14-Dec-2016.)
⊢ 𝑀 ∈ ℕ    &   ⊢ 𝑁 ∈ ℕ    &   ⊢ 𝑂 = {𝑐 ∈ 𝒫 (1...(𝑀 + 𝑁)) ∣ (♯‘𝑐) = 𝑀}    &   ⊢ 𝑃 = (𝑥 ∈ 𝒫 𝑂 ↦ ((♯‘𝑥) / (♯‘𝑂)))    &   ⊢ 𝐹 = (𝑐 ∈ 𝑂 ↦ (𝑖 ∈ ℤ ↦ ((♯‘((1...𝑖) ∩ 𝑐)) − (♯‘((1...𝑖) ∖ 𝑐)))))    &   ⊢ 𝐸 = {𝑐 ∈ 𝑂 ∣ ∀𝑖 ∈ (1...(𝑀 + 𝑁))0 < ((𝐹‘𝑐)‘𝑖)}    ⇒   ⊢ (𝐶 ∈ 𝐸 ↔ (𝐶 ∈ 𝑂 ∧ ∀𝑖 ∈ (1...(𝑀 + 𝑁))0 < ((𝐹‘𝐶)‘𝑖)))
Theorem	ballotlemodife 34465*	Elements of (𝑂 ∖ 𝐸). (Contributed by Thierry Arnoux, 7-Dec-2016.)
⊢ 𝑀 ∈ ℕ    &   ⊢ 𝑁 ∈ ℕ    &   ⊢ 𝑂 = {𝑐 ∈ 𝒫 (1...(𝑀 + 𝑁)) ∣ (♯‘𝑐) = 𝑀}    &   ⊢ 𝑃 = (𝑥 ∈ 𝒫 𝑂 ↦ ((♯‘𝑥) / (♯‘𝑂)))    &   ⊢ 𝐹 = (𝑐 ∈ 𝑂 ↦ (𝑖 ∈ ℤ ↦ ((♯‘((1...𝑖) ∩ 𝑐)) − (♯‘((1...𝑖) ∖ 𝑐)))))    &   ⊢ 𝐸 = {𝑐 ∈ 𝑂 ∣ ∀𝑖 ∈ (1...(𝑀 + 𝑁))0 < ((𝐹‘𝑐)‘𝑖)}    ⇒   ⊢ (𝐶 ∈ (𝑂 ∖ 𝐸) ↔ (𝐶 ∈ 𝑂 ∧ ∃𝑖 ∈ (1...(𝑀 + 𝑁))((𝐹‘𝐶)‘𝑖) ≤ 0))
Theorem	ballotlem4 34466*	If the first pick is a vote for B, A is not ahead throughout the count. (Contributed by Thierry Arnoux, 25-Nov-2016.)
⊢ 𝑀 ∈ ℕ    &   ⊢ 𝑁 ∈ ℕ    &   ⊢ 𝑂 = {𝑐 ∈ 𝒫 (1...(𝑀 + 𝑁)) ∣ (♯‘𝑐) = 𝑀}    &   ⊢ 𝑃 = (𝑥 ∈ 𝒫 𝑂 ↦ ((♯‘𝑥) / (♯‘𝑂)))    &   ⊢ 𝐹 = (𝑐 ∈ 𝑂 ↦ (𝑖 ∈ ℤ ↦ ((♯‘((1...𝑖) ∩ 𝑐)) − (♯‘((1...𝑖) ∖ 𝑐)))))    &   ⊢ 𝐸 = {𝑐 ∈ 𝑂 ∣ ∀𝑖 ∈ (1...(𝑀 + 𝑁))0 < ((𝐹‘𝑐)‘𝑖)}    ⇒   ⊢ (𝐶 ∈ 𝑂 → (¬ 1 ∈ 𝐶 → ¬ 𝐶 ∈ 𝐸))
Theorem	ballotlem5 34467*	If A is not ahead throughout, there is a 𝑘 where votes are tied. (Contributed by Thierry Arnoux, 1-Dec-2016.)
⊢ 𝑀 ∈ ℕ    &   ⊢ 𝑁 ∈ ℕ    &   ⊢ 𝑂 = {𝑐 ∈ 𝒫 (1...(𝑀 + 𝑁)) ∣ (♯‘𝑐) = 𝑀}    &   ⊢ 𝑃 = (𝑥 ∈ 𝒫 𝑂 ↦ ((♯‘𝑥) / (♯‘𝑂)))    &   ⊢ 𝐹 = (𝑐 ∈ 𝑂 ↦ (𝑖 ∈ ℤ ↦ ((♯‘((1...𝑖) ∩ 𝑐)) − (♯‘((1...𝑖) ∖ 𝑐)))))    &   ⊢ 𝐸 = {𝑐 ∈ 𝑂 ∣ ∀𝑖 ∈ (1...(𝑀 + 𝑁))0 < ((𝐹‘𝑐)‘𝑖)}    &   ⊢ 𝑁 < 𝑀    ⇒   ⊢ (𝐶 ∈ (𝑂 ∖ 𝐸) → ∃𝑘 ∈ (1...(𝑀 + 𝑁))((𝐹‘𝐶)‘𝑘) = 0)
Theorem	ballotlemi 34468*	Value of 𝐼 for a given counting 𝐶. (Contributed by Thierry Arnoux, 1-Dec-2016.) (Revised by AV, 6-Oct-2020.)
⊢ 𝑀 ∈ ℕ    &   ⊢ 𝑁 ∈ ℕ    &   ⊢ 𝑂 = {𝑐 ∈ 𝒫 (1...(𝑀 + 𝑁)) ∣ (♯‘𝑐) = 𝑀}    &   ⊢ 𝑃 = (𝑥 ∈ 𝒫 𝑂 ↦ ((♯‘𝑥) / (♯‘𝑂)))    &   ⊢ 𝐹 = (𝑐 ∈ 𝑂 ↦ (𝑖 ∈ ℤ ↦ ((♯‘((1...𝑖) ∩ 𝑐)) − (♯‘((1...𝑖) ∖ 𝑐)))))    &   ⊢ 𝐸 = {𝑐 ∈ 𝑂 ∣ ∀𝑖 ∈ (1...(𝑀 + 𝑁))0 < ((𝐹‘𝑐)‘𝑖)}    &   ⊢ 𝑁 < 𝑀    &   ⊢ 𝐼 = (𝑐 ∈ (𝑂 ∖ 𝐸) ↦ inf({𝑘 ∈ (1...(𝑀 + 𝑁)) ∣ ((𝐹‘𝑐)‘𝑘) = 0}, ℝ, < ))    ⇒   ⊢ (𝐶 ∈ (𝑂 ∖ 𝐸) → (𝐼‘𝐶) = inf({𝑘 ∈ (1...(𝑀 + 𝑁)) ∣ ((𝐹‘𝐶)‘𝑘) = 0}, ℝ, < ))
Theorem	ballotlemiex 34469*	Properties of (𝐼‘𝐶). (Contributed by Thierry Arnoux, 12-Dec-2016.) (Revised by AV, 6-Oct-2020.)
⊢ 𝑀 ∈ ℕ    &   ⊢ 𝑁 ∈ ℕ    &   ⊢ 𝑂 = {𝑐 ∈ 𝒫 (1...(𝑀 + 𝑁)) ∣ (♯‘𝑐) = 𝑀}    &   ⊢ 𝑃 = (𝑥 ∈ 𝒫 𝑂 ↦ ((♯‘𝑥) / (♯‘𝑂)))    &   ⊢ 𝐹 = (𝑐 ∈ 𝑂 ↦ (𝑖 ∈ ℤ ↦ ((♯‘((1...𝑖) ∩ 𝑐)) − (♯‘((1...𝑖) ∖ 𝑐)))))    &   ⊢ 𝐸 = {𝑐 ∈ 𝑂 ∣ ∀𝑖 ∈ (1...(𝑀 + 𝑁))0 < ((𝐹‘𝑐)‘𝑖)}    &   ⊢ 𝑁 < 𝑀    &   ⊢ 𝐼 = (𝑐 ∈ (𝑂 ∖ 𝐸) ↦ inf({𝑘 ∈ (1...(𝑀 + 𝑁)) ∣ ((𝐹‘𝑐)‘𝑘) = 0}, ℝ, < ))    ⇒   ⊢ (𝐶 ∈ (𝑂 ∖ 𝐸) → ((𝐼‘𝐶) ∈ (1...(𝑀 + 𝑁)) ∧ ((𝐹‘𝐶)‘(𝐼‘𝐶)) = 0))
Theorem	ballotlemi1 34470*	The first tie cannot be reached at the first pick. (Contributed by Thierry Arnoux, 12-Mar-2017.)
⊢ 𝑀 ∈ ℕ    &   ⊢ 𝑁 ∈ ℕ    &   ⊢ 𝑂 = {𝑐 ∈ 𝒫 (1...(𝑀 + 𝑁)) ∣ (♯‘𝑐) = 𝑀}    &   ⊢ 𝑃 = (𝑥 ∈ 𝒫 𝑂 ↦ ((♯‘𝑥) / (♯‘𝑂)))    &   ⊢ 𝐹 = (𝑐 ∈ 𝑂 ↦ (𝑖 ∈ ℤ ↦ ((♯‘((1...𝑖) ∩ 𝑐)) − (♯‘((1...𝑖) ∖ 𝑐)))))    &   ⊢ 𝐸 = {𝑐 ∈ 𝑂 ∣ ∀𝑖 ∈ (1...(𝑀 + 𝑁))0 < ((𝐹‘𝑐)‘𝑖)}    &   ⊢ 𝑁 < 𝑀    &   ⊢ 𝐼 = (𝑐 ∈ (𝑂 ∖ 𝐸) ↦ inf({𝑘 ∈ (1...(𝑀 + 𝑁)) ∣ ((𝐹‘𝑐)‘𝑘) = 0}, ℝ, < ))    ⇒   ⊢ ((𝐶 ∈ (𝑂 ∖ 𝐸) ∧ ¬ 1 ∈ 𝐶) → (𝐼‘𝐶) ≠ 1)
Theorem	ballotlemii 34471*	The first tie cannot be reached at the first pick. (Contributed by Thierry Arnoux, 4-Apr-2017.)
⊢ 𝑀 ∈ ℕ    &   ⊢ 𝑁 ∈ ℕ    &   ⊢ 𝑂 = {𝑐 ∈ 𝒫 (1...(𝑀 + 𝑁)) ∣ (♯‘𝑐) = 𝑀}    &   ⊢ 𝑃 = (𝑥 ∈ 𝒫 𝑂 ↦ ((♯‘𝑥) / (♯‘𝑂)))    &   ⊢ 𝐹 = (𝑐 ∈ 𝑂 ↦ (𝑖 ∈ ℤ ↦ ((♯‘((1...𝑖) ∩ 𝑐)) − (♯‘((1...𝑖) ∖ 𝑐)))))    &   ⊢ 𝐸 = {𝑐 ∈ 𝑂 ∣ ∀𝑖 ∈ (1...(𝑀 + 𝑁))0 < ((𝐹‘𝑐)‘𝑖)}    &   ⊢ 𝑁 < 𝑀    &   ⊢ 𝐼 = (𝑐 ∈ (𝑂 ∖ 𝐸) ↦ inf({𝑘 ∈ (1...(𝑀 + 𝑁)) ∣ ((𝐹‘𝑐)‘𝑘) = 0}, ℝ, < ))    ⇒   ⊢ ((𝐶 ∈ (𝑂 ∖ 𝐸) ∧ 1 ∈ 𝐶) → (𝐼‘𝐶) ≠ 1)
Theorem	ballotlemsup 34472*	The set of zeroes of 𝐹 satisfies the conditions to have a supremum. (Contributed by Thierry Arnoux, 1-Dec-2016.) (Revised by AV, 6-Oct-2020.)
⊢ 𝑀 ∈ ℕ    &   ⊢ 𝑁 ∈ ℕ    &   ⊢ 𝑂 = {𝑐 ∈ 𝒫 (1...(𝑀 + 𝑁)) ∣ (♯‘𝑐) = 𝑀}    &   ⊢ 𝑃 = (𝑥 ∈ 𝒫 𝑂 ↦ ((♯‘𝑥) / (♯‘𝑂)))    &   ⊢ 𝐹 = (𝑐 ∈ 𝑂 ↦ (𝑖 ∈ ℤ ↦ ((♯‘((1...𝑖) ∩ 𝑐)) − (♯‘((1...𝑖) ∖ 𝑐)))))    &   ⊢ 𝐸 = {𝑐 ∈ 𝑂 ∣ ∀𝑖 ∈ (1...(𝑀 + 𝑁))0 < ((𝐹‘𝑐)‘𝑖)}    &   ⊢ 𝑁 < 𝑀    &   ⊢ 𝐼 = (𝑐 ∈ (𝑂 ∖ 𝐸) ↦ inf({𝑘 ∈ (1...(𝑀 + 𝑁)) ∣ ((𝐹‘𝑐)‘𝑘) = 0}, ℝ, < ))    ⇒   ⊢ (𝐶 ∈ (𝑂 ∖ 𝐸) → ∃𝑧 ∈ ℝ (∀𝑤 ∈ {𝑘 ∈ (1...(𝑀 + 𝑁)) ∣ ((𝐹‘𝐶)‘𝑘) = 0} ¬ 𝑤 < 𝑧 ∧ ∀𝑤 ∈ ℝ (𝑧 < 𝑤 → ∃𝑦 ∈ {𝑘 ∈ (1...(𝑀 + 𝑁)) ∣ ((𝐹‘𝐶)‘𝑘) = 0}𝑦 < 𝑤)))
Theorem	ballotlemimin 34473*	(𝐼‘𝐶) is the first tie. (Contributed by Thierry Arnoux, 1-Dec-2016.) (Revised by AV, 6-Oct-2020.)
⊢ 𝑀 ∈ ℕ    &   ⊢ 𝑁 ∈ ℕ    &   ⊢ 𝑂 = {𝑐 ∈ 𝒫 (1...(𝑀 + 𝑁)) ∣ (♯‘𝑐) = 𝑀}    &   ⊢ 𝑃 = (𝑥 ∈ 𝒫 𝑂 ↦ ((♯‘𝑥) / (♯‘𝑂)))    &   ⊢ 𝐹 = (𝑐 ∈ 𝑂 ↦ (𝑖 ∈ ℤ ↦ ((♯‘((1...𝑖) ∩ 𝑐)) − (♯‘((1...𝑖) ∖ 𝑐)))))    &   ⊢ 𝐸 = {𝑐 ∈ 𝑂 ∣ ∀𝑖 ∈ (1...(𝑀 + 𝑁))0 < ((𝐹‘𝑐)‘𝑖)}    &   ⊢ 𝑁 < 𝑀    &   ⊢ 𝐼 = (𝑐 ∈ (𝑂 ∖ 𝐸) ↦ inf({𝑘 ∈ (1...(𝑀 + 𝑁)) ∣ ((𝐹‘𝑐)‘𝑘) = 0}, ℝ, < ))    ⇒   ⊢ (𝐶 ∈ (𝑂 ∖ 𝐸) → ¬ ∃𝑘 ∈ (1...((𝐼‘𝐶) − 1))((𝐹‘𝐶)‘𝑘) = 0)
Theorem	ballotlemic 34474*	If the first vote is for B, the vote on the first tie is for A. (Contributed by Thierry Arnoux, 1-Dec-2016.)
⊢ 𝑀 ∈ ℕ    &   ⊢ 𝑁 ∈ ℕ    &   ⊢ 𝑂 = {𝑐 ∈ 𝒫 (1...(𝑀 + 𝑁)) ∣ (♯‘𝑐) = 𝑀}    &   ⊢ 𝑃 = (𝑥 ∈ 𝒫 𝑂 ↦ ((♯‘𝑥) / (♯‘𝑂)))    &   ⊢ 𝐹 = (𝑐 ∈ 𝑂 ↦ (𝑖 ∈ ℤ ↦ ((♯‘((1...𝑖) ∩ 𝑐)) − (♯‘((1...𝑖) ∖ 𝑐)))))    &   ⊢ 𝐸 = {𝑐 ∈ 𝑂 ∣ ∀𝑖 ∈ (1...(𝑀 + 𝑁))0 < ((𝐹‘𝑐)‘𝑖)}    &   ⊢ 𝑁 < 𝑀    &   ⊢ 𝐼 = (𝑐 ∈ (𝑂 ∖ 𝐸) ↦ inf({𝑘 ∈ (1...(𝑀 + 𝑁)) ∣ ((𝐹‘𝑐)‘𝑘) = 0}, ℝ, < ))    ⇒   ⊢ ((𝐶 ∈ (𝑂 ∖ 𝐸) ∧ ¬ 1 ∈ 𝐶) → (𝐼‘𝐶) ∈ 𝐶)
Theorem	ballotlem1c 34475*	If the first vote is for A, the vote on the first tie is for B. (Contributed by Thierry Arnoux, 4-Apr-2017.)
⊢ 𝑀 ∈ ℕ    &   ⊢ 𝑁 ∈ ℕ    &   ⊢ 𝑂 = {𝑐 ∈ 𝒫 (1...(𝑀 + 𝑁)) ∣ (♯‘𝑐) = 𝑀}    &   ⊢ 𝑃 = (𝑥 ∈ 𝒫 𝑂 ↦ ((♯‘𝑥) / (♯‘𝑂)))    &   ⊢ 𝐹 = (𝑐 ∈ 𝑂 ↦ (𝑖 ∈ ℤ ↦ ((♯‘((1...𝑖) ∩ 𝑐)) − (♯‘((1...𝑖) ∖ 𝑐)))))    &   ⊢ 𝐸 = {𝑐 ∈ 𝑂 ∣ ∀𝑖 ∈ (1...(𝑀 + 𝑁))0 < ((𝐹‘𝑐)‘𝑖)}    &   ⊢ 𝑁 < 𝑀    &   ⊢ 𝐼 = (𝑐 ∈ (𝑂 ∖ 𝐸) ↦ inf({𝑘 ∈ (1...(𝑀 + 𝑁)) ∣ ((𝐹‘𝑐)‘𝑘) = 0}, ℝ, < ))    ⇒   ⊢ ((𝐶 ∈ (𝑂 ∖ 𝐸) ∧ 1 ∈ 𝐶) → ¬ (𝐼‘𝐶) ∈ 𝐶)
Theorem	ballotlemsval 34476*	Value of 𝑆. (Contributed by Thierry Arnoux, 12-Apr-2017.)
⊢ 𝑀 ∈ ℕ    &   ⊢ 𝑁 ∈ ℕ    &   ⊢ 𝑂 = {𝑐 ∈ 𝒫 (1...(𝑀 + 𝑁)) ∣ (♯‘𝑐) = 𝑀}    &   ⊢ 𝑃 = (𝑥 ∈ 𝒫 𝑂 ↦ ((♯‘𝑥) / (♯‘𝑂)))    &   ⊢ 𝐹 = (𝑐 ∈ 𝑂 ↦ (𝑖 ∈ ℤ ↦ ((♯‘((1...𝑖) ∩ 𝑐)) − (♯‘((1...𝑖) ∖ 𝑐)))))    &   ⊢ 𝐸 = {𝑐 ∈ 𝑂 ∣ ∀𝑖 ∈ (1...(𝑀 + 𝑁))0 < ((𝐹‘𝑐)‘𝑖)}    &   ⊢ 𝑁 < 𝑀    &   ⊢ 𝐼 = (𝑐 ∈ (𝑂 ∖ 𝐸) ↦ inf({𝑘 ∈ (1...(𝑀 + 𝑁)) ∣ ((𝐹‘𝑐)‘𝑘) = 0}, ℝ, < ))    &   ⊢ 𝑆 = (𝑐 ∈ (𝑂 ∖ 𝐸) ↦ (𝑖 ∈ (1...(𝑀 + 𝑁)) ↦ if(𝑖 ≤ (𝐼‘𝑐), (((𝐼‘𝑐) + 1) − 𝑖), 𝑖)))    ⇒   ⊢ (𝐶 ∈ (𝑂 ∖ 𝐸) → (𝑆‘𝐶) = (𝑖 ∈ (1...(𝑀 + 𝑁)) ↦ if(𝑖 ≤ (𝐼‘𝐶), (((𝐼‘𝐶) + 1) − 𝑖), 𝑖)))
Theorem	ballotlemsv 34477*	Value of 𝑆 evaluated at 𝐽 for a given counting 𝐶. (Contributed by Thierry Arnoux, 12-Apr-2017.)
⊢ 𝑀 ∈ ℕ    &   ⊢ 𝑁 ∈ ℕ    &   ⊢ 𝑂 = {𝑐 ∈ 𝒫 (1...(𝑀 + 𝑁)) ∣ (♯‘𝑐) = 𝑀}    &   ⊢ 𝑃 = (𝑥 ∈ 𝒫 𝑂 ↦ ((♯‘𝑥) / (♯‘𝑂)))    &   ⊢ 𝐹 = (𝑐 ∈ 𝑂 ↦ (𝑖 ∈ ℤ ↦ ((♯‘((1...𝑖) ∩ 𝑐)) − (♯‘((1...𝑖) ∖ 𝑐)))))    &   ⊢ 𝐸 = {𝑐 ∈ 𝑂 ∣ ∀𝑖 ∈ (1...(𝑀 + 𝑁))0 < ((𝐹‘𝑐)‘𝑖)}    &   ⊢ 𝑁 < 𝑀    &   ⊢ 𝐼 = (𝑐 ∈ (𝑂 ∖ 𝐸) ↦ inf({𝑘 ∈ (1...(𝑀 + 𝑁)) ∣ ((𝐹‘𝑐)‘𝑘) = 0}, ℝ, < ))    &   ⊢ 𝑆 = (𝑐 ∈ (𝑂 ∖ 𝐸) ↦ (𝑖 ∈ (1...(𝑀 + 𝑁)) ↦ if(𝑖 ≤ (𝐼‘𝑐), (((𝐼‘𝑐) + 1) − 𝑖), 𝑖)))    ⇒   ⊢ ((𝐶 ∈ (𝑂 ∖ 𝐸) ∧ 𝐽 ∈ (1...(𝑀 + 𝑁))) → ((𝑆‘𝐶)‘𝐽) = if(𝐽 ≤ (𝐼‘𝐶), (((𝐼‘𝐶) + 1) − 𝐽), 𝐽))
Theorem	ballotlemsgt1 34478*	𝑆 maps values less than (𝐼‘𝐶) to values greater than 1. (Contributed by Thierry Arnoux, 28-Apr-2017.)
⊢ 𝑀 ∈ ℕ    &   ⊢ 𝑁 ∈ ℕ    &   ⊢ 𝑂 = {𝑐 ∈ 𝒫 (1...(𝑀 + 𝑁)) ∣ (♯‘𝑐) = 𝑀}    &   ⊢ 𝑃 = (𝑥 ∈ 𝒫 𝑂 ↦ ((♯‘𝑥) / (♯‘𝑂)))    &   ⊢ 𝐹 = (𝑐 ∈ 𝑂 ↦ (𝑖 ∈ ℤ ↦ ((♯‘((1...𝑖) ∩ 𝑐)) − (♯‘((1...𝑖) ∖ 𝑐)))))    &   ⊢ 𝐸 = {𝑐 ∈ 𝑂 ∣ ∀𝑖 ∈ (1...(𝑀 + 𝑁))0 < ((𝐹‘𝑐)‘𝑖)}    &   ⊢ 𝑁 < 𝑀    &   ⊢ 𝐼 = (𝑐 ∈ (𝑂 ∖ 𝐸) ↦ inf({𝑘 ∈ (1...(𝑀 + 𝑁)) ∣ ((𝐹‘𝑐)‘𝑘) = 0}, ℝ, < ))    &   ⊢ 𝑆 = (𝑐 ∈ (𝑂 ∖ 𝐸) ↦ (𝑖 ∈ (1...(𝑀 + 𝑁)) ↦ if(𝑖 ≤ (𝐼‘𝑐), (((𝐼‘𝑐) + 1) − 𝑖), 𝑖)))    ⇒   ⊢ ((𝐶 ∈ (𝑂 ∖ 𝐸) ∧ 𝐽 ∈ (1...(𝑀 + 𝑁)) ∧ 𝐽 < (𝐼‘𝐶)) → 1 < ((𝑆‘𝐶)‘𝐽))
Theorem	ballotlemsdom 34479*	Domain of 𝑆 for a given counting 𝐶. (Contributed by Thierry Arnoux, 12-Apr-2017.)
⊢ 𝑀 ∈ ℕ    &   ⊢ 𝑁 ∈ ℕ    &   ⊢ 𝑂 = {𝑐 ∈ 𝒫 (1...(𝑀 + 𝑁)) ∣ (♯‘𝑐) = 𝑀}    &   ⊢ 𝑃 = (𝑥 ∈ 𝒫 𝑂 ↦ ((♯‘𝑥) / (♯‘𝑂)))    &   ⊢ 𝐹 = (𝑐 ∈ 𝑂 ↦ (𝑖 ∈ ℤ ↦ ((♯‘((1...𝑖) ∩ 𝑐)) − (♯‘((1...𝑖) ∖ 𝑐)))))    &   ⊢ 𝐸 = {𝑐 ∈ 𝑂 ∣ ∀𝑖 ∈ (1...(𝑀 + 𝑁))0 < ((𝐹‘𝑐)‘𝑖)}    &   ⊢ 𝑁 < 𝑀    &   ⊢ 𝐼 = (𝑐 ∈ (𝑂 ∖ 𝐸) ↦ inf({𝑘 ∈ (1...(𝑀 + 𝑁)) ∣ ((𝐹‘𝑐)‘𝑘) = 0}, ℝ, < ))    &   ⊢ 𝑆 = (𝑐 ∈ (𝑂 ∖ 𝐸) ↦ (𝑖 ∈ (1...(𝑀 + 𝑁)) ↦ if(𝑖 ≤ (𝐼‘𝑐), (((𝐼‘𝑐) + 1) − 𝑖), 𝑖)))    ⇒   ⊢ ((𝐶 ∈ (𝑂 ∖ 𝐸) ∧ 𝐽 ∈ (1...(𝑀 + 𝑁))) → ((𝑆‘𝐶)‘𝐽) ∈ (1...(𝑀 + 𝑁)))
Theorem	ballotlemsel1i 34480*	The range (1...(𝐼‘𝐶)) is invariant under (𝑆‘𝐶). (Contributed by Thierry Arnoux, 28-Apr-2017.)
⊢ 𝑀 ∈ ℕ    &   ⊢ 𝑁 ∈ ℕ    &   ⊢ 𝑂 = {𝑐 ∈ 𝒫 (1...(𝑀 + 𝑁)) ∣ (♯‘𝑐) = 𝑀}    &   ⊢ 𝑃 = (𝑥 ∈ 𝒫 𝑂 ↦ ((♯‘𝑥) / (♯‘𝑂)))    &   ⊢ 𝐹 = (𝑐 ∈ 𝑂 ↦ (𝑖 ∈ ℤ ↦ ((♯‘((1...𝑖) ∩ 𝑐)) − (♯‘((1...𝑖) ∖ 𝑐)))))    &   ⊢ 𝐸 = {𝑐 ∈ 𝑂 ∣ ∀𝑖 ∈ (1...(𝑀 + 𝑁))0 < ((𝐹‘𝑐)‘𝑖)}    &   ⊢ 𝑁 < 𝑀    &   ⊢ 𝐼 = (𝑐 ∈ (𝑂 ∖ 𝐸) ↦ inf({𝑘 ∈ (1...(𝑀 + 𝑁)) ∣ ((𝐹‘𝑐)‘𝑘) = 0}, ℝ, < ))    &   ⊢ 𝑆 = (𝑐 ∈ (𝑂 ∖ 𝐸) ↦ (𝑖 ∈ (1...(𝑀 + 𝑁)) ↦ if(𝑖 ≤ (𝐼‘𝑐), (((𝐼‘𝑐) + 1) − 𝑖), 𝑖)))    ⇒   ⊢ ((𝐶 ∈ (𝑂 ∖ 𝐸) ∧ 𝐽 ∈ (1...(𝐼‘𝐶))) → ((𝑆‘𝐶)‘𝐽) ∈ (1...(𝐼‘𝐶)))
Theorem	ballotlemsf1o 34481*	The defined 𝑆 is a bijection, and an involution. (Contributed by Thierry Arnoux, 14-Apr-2017.)
⊢ 𝑀 ∈ ℕ    &   ⊢ 𝑁 ∈ ℕ    &   ⊢ 𝑂 = {𝑐 ∈ 𝒫 (1...(𝑀 + 𝑁)) ∣ (♯‘𝑐) = 𝑀}    &   ⊢ 𝑃 = (𝑥 ∈ 𝒫 𝑂 ↦ ((♯‘𝑥) / (♯‘𝑂)))    &   ⊢ 𝐹 = (𝑐 ∈ 𝑂 ↦ (𝑖 ∈ ℤ ↦ ((♯‘((1...𝑖) ∩ 𝑐)) − (♯‘((1...𝑖) ∖ 𝑐)))))    &   ⊢ 𝐸 = {𝑐 ∈ 𝑂 ∣ ∀𝑖 ∈ (1...(𝑀 + 𝑁))0 < ((𝐹‘𝑐)‘𝑖)}    &   ⊢ 𝑁 < 𝑀    &   ⊢ 𝐼 = (𝑐 ∈ (𝑂 ∖ 𝐸) ↦ inf({𝑘 ∈ (1...(𝑀 + 𝑁)) ∣ ((𝐹‘𝑐)‘𝑘) = 0}, ℝ, < ))    &   ⊢ 𝑆 = (𝑐 ∈ (𝑂 ∖ 𝐸) ↦ (𝑖 ∈ (1...(𝑀 + 𝑁)) ↦ if(𝑖 ≤ (𝐼‘𝑐), (((𝐼‘𝑐) + 1) − 𝑖), 𝑖)))    ⇒   ⊢ (𝐶 ∈ (𝑂 ∖ 𝐸) → ((𝑆‘𝐶):(1...(𝑀 + 𝑁))–1-1-onto→(1...(𝑀 + 𝑁)) ∧ ◡(𝑆‘𝐶) = (𝑆‘𝐶)))
Theorem	ballotlemsi 34482*	The image by 𝑆 of the first tie pick is the first pick. (Contributed by Thierry Arnoux, 14-Apr-2017.)
⊢ 𝑀 ∈ ℕ    &   ⊢ 𝑁 ∈ ℕ    &   ⊢ 𝑂 = {𝑐 ∈ 𝒫 (1...(𝑀 + 𝑁)) ∣ (♯‘𝑐) = 𝑀}    &   ⊢ 𝑃 = (𝑥 ∈ 𝒫 𝑂 ↦ ((♯‘𝑥) / (♯‘𝑂)))    &   ⊢ 𝐹 = (𝑐 ∈ 𝑂 ↦ (𝑖 ∈ ℤ ↦ ((♯‘((1...𝑖) ∩ 𝑐)) − (♯‘((1...𝑖) ∖ 𝑐)))))    &   ⊢ 𝐸 = {𝑐 ∈ 𝑂 ∣ ∀𝑖 ∈ (1...(𝑀 + 𝑁))0 < ((𝐹‘𝑐)‘𝑖)}    &   ⊢ 𝑁 < 𝑀    &   ⊢ 𝐼 = (𝑐 ∈ (𝑂 ∖ 𝐸) ↦ inf({𝑘 ∈ (1...(𝑀 + 𝑁)) ∣ ((𝐹‘𝑐)‘𝑘) = 0}, ℝ, < ))    &   ⊢ 𝑆 = (𝑐 ∈ (𝑂 ∖ 𝐸) ↦ (𝑖 ∈ (1...(𝑀 + 𝑁)) ↦ if(𝑖 ≤ (𝐼‘𝑐), (((𝐼‘𝑐) + 1) − 𝑖), 𝑖)))    ⇒   ⊢ (𝐶 ∈ (𝑂 ∖ 𝐸) → ((𝑆‘𝐶)‘(𝐼‘𝐶)) = 1)
Theorem	ballotlemsima 34483*	The image by 𝑆 of an interval before the first pick. (Contributed by Thierry Arnoux, 5-May-2017.)
⊢ 𝑀 ∈ ℕ    &   ⊢ 𝑁 ∈ ℕ    &   ⊢ 𝑂 = {𝑐 ∈ 𝒫 (1...(𝑀 + 𝑁)) ∣ (♯‘𝑐) = 𝑀}    &   ⊢ 𝑃 = (𝑥 ∈ 𝒫 𝑂 ↦ ((♯‘𝑥) / (♯‘𝑂)))    &   ⊢ 𝐹 = (𝑐 ∈ 𝑂 ↦ (𝑖 ∈ ℤ ↦ ((♯‘((1...𝑖) ∩ 𝑐)) − (♯‘((1...𝑖) ∖ 𝑐)))))    &   ⊢ 𝐸 = {𝑐 ∈ 𝑂 ∣ ∀𝑖 ∈ (1...(𝑀 + 𝑁))0 < ((𝐹‘𝑐)‘𝑖)}    &   ⊢ 𝑁 < 𝑀    &   ⊢ 𝐼 = (𝑐 ∈ (𝑂 ∖ 𝐸) ↦ inf({𝑘 ∈ (1...(𝑀 + 𝑁)) ∣ ((𝐹‘𝑐)‘𝑘) = 0}, ℝ, < ))    &   ⊢ 𝑆 = (𝑐 ∈ (𝑂 ∖ 𝐸) ↦ (𝑖 ∈ (1...(𝑀 + 𝑁)) ↦ if(𝑖 ≤ (𝐼‘𝑐), (((𝐼‘𝑐) + 1) − 𝑖), 𝑖)))    ⇒   ⊢ ((𝐶 ∈ (𝑂 ∖ 𝐸) ∧ 𝐽 ∈ (1...(𝐼‘𝐶))) → ((𝑆‘𝐶) “ (1...𝐽)) = (((𝑆‘𝐶)‘𝐽)...(𝐼‘𝐶)))
Theorem	ballotlemieq 34484*	If two countings share the same first tie, they also have the same swap function. (Contributed by Thierry Arnoux, 18-Apr-2017.)
⊢ 𝑀 ∈ ℕ    &   ⊢ 𝑁 ∈ ℕ    &   ⊢ 𝑂 = {𝑐 ∈ 𝒫 (1...(𝑀 + 𝑁)) ∣ (♯‘𝑐) = 𝑀}    &   ⊢ 𝑃 = (𝑥 ∈ 𝒫 𝑂 ↦ ((♯‘𝑥) / (♯‘𝑂)))    &   ⊢ 𝐹 = (𝑐 ∈ 𝑂 ↦ (𝑖 ∈ ℤ ↦ ((♯‘((1...𝑖) ∩ 𝑐)) − (♯‘((1...𝑖) ∖ 𝑐)))))    &   ⊢ 𝐸 = {𝑐 ∈ 𝑂 ∣ ∀𝑖 ∈ (1...(𝑀 + 𝑁))0 < ((𝐹‘𝑐)‘𝑖)}    &   ⊢ 𝑁 < 𝑀    &   ⊢ 𝐼 = (𝑐 ∈ (𝑂 ∖ 𝐸) ↦ inf({𝑘 ∈ (1...(𝑀 + 𝑁)) ∣ ((𝐹‘𝑐)‘𝑘) = 0}, ℝ, < ))    &   ⊢ 𝑆 = (𝑐 ∈ (𝑂 ∖ 𝐸) ↦ (𝑖 ∈ (1...(𝑀 + 𝑁)) ↦ if(𝑖 ≤ (𝐼‘𝑐), (((𝐼‘𝑐) + 1) − 𝑖), 𝑖)))    ⇒   ⊢ ((𝐶 ∈ (𝑂 ∖ 𝐸) ∧ 𝐷 ∈ (𝑂 ∖ 𝐸) ∧ (𝐼‘𝐶) = (𝐼‘𝐷)) → (𝑆‘𝐶) = (𝑆‘𝐷))
Theorem	ballotlemrval 34485*	Value of 𝑅. (Contributed by Thierry Arnoux, 14-Apr-2017.)
⊢ 𝑀 ∈ ℕ    &   ⊢ 𝑁 ∈ ℕ    &   ⊢ 𝑂 = {𝑐 ∈ 𝒫 (1...(𝑀 + 𝑁)) ∣ (♯‘𝑐) = 𝑀}    &   ⊢ 𝑃 = (𝑥 ∈ 𝒫 𝑂 ↦ ((♯‘𝑥) / (♯‘𝑂)))    &   ⊢ 𝐹 = (𝑐 ∈ 𝑂 ↦ (𝑖 ∈ ℤ ↦ ((♯‘((1...𝑖) ∩ 𝑐)) − (♯‘((1...𝑖) ∖ 𝑐)))))    &   ⊢ 𝐸 = {𝑐 ∈ 𝑂 ∣ ∀𝑖 ∈ (1...(𝑀 + 𝑁))0 < ((𝐹‘𝑐)‘𝑖)}    &   ⊢ 𝑁 < 𝑀    &   ⊢ 𝐼 = (𝑐 ∈ (𝑂 ∖ 𝐸) ↦ inf({𝑘 ∈ (1...(𝑀 + 𝑁)) ∣ ((𝐹‘𝑐)‘𝑘) = 0}, ℝ, < ))    &   ⊢ 𝑆 = (𝑐 ∈ (𝑂 ∖ 𝐸) ↦ (𝑖 ∈ (1...(𝑀 + 𝑁)) ↦ if(𝑖 ≤ (𝐼‘𝑐), (((𝐼‘𝑐) + 1) − 𝑖), 𝑖)))    &   ⊢ 𝑅 = (𝑐 ∈ (𝑂 ∖ 𝐸) ↦ ((𝑆‘𝑐) “ 𝑐))    ⇒   ⊢ (𝐶 ∈ (𝑂 ∖ 𝐸) → (𝑅‘𝐶) = ((𝑆‘𝐶) “ 𝐶))
Theorem	ballotlemscr 34486*	The image of (𝑅‘𝐶) by (𝑆‘𝐶). (Contributed by Thierry Arnoux, 21-Apr-2017.)
⊢ 𝑀 ∈ ℕ    &   ⊢ 𝑁 ∈ ℕ    &   ⊢ 𝑂 = {𝑐 ∈ 𝒫 (1...(𝑀 + 𝑁)) ∣ (♯‘𝑐) = 𝑀}    &   ⊢ 𝑃 = (𝑥 ∈ 𝒫 𝑂 ↦ ((♯‘𝑥) / (♯‘𝑂)))    &   ⊢ 𝐹 = (𝑐 ∈ 𝑂 ↦ (𝑖 ∈ ℤ ↦ ((♯‘((1...𝑖) ∩ 𝑐)) − (♯‘((1...𝑖) ∖ 𝑐)))))    &   ⊢ 𝐸 = {𝑐 ∈ 𝑂 ∣ ∀𝑖 ∈ (1...(𝑀 + 𝑁))0 < ((𝐹‘𝑐)‘𝑖)}    &   ⊢ 𝑁 < 𝑀    &   ⊢ 𝐼 = (𝑐 ∈ (𝑂 ∖ 𝐸) ↦ inf({𝑘 ∈ (1...(𝑀 + 𝑁)) ∣ ((𝐹‘𝑐)‘𝑘) = 0}, ℝ, < ))    &   ⊢ 𝑆 = (𝑐 ∈ (𝑂 ∖ 𝐸) ↦ (𝑖 ∈ (1...(𝑀 + 𝑁)) ↦ if(𝑖 ≤ (𝐼‘𝑐), (((𝐼‘𝑐) + 1) − 𝑖), 𝑖)))    &   ⊢ 𝑅 = (𝑐 ∈ (𝑂 ∖ 𝐸) ↦ ((𝑆‘𝑐) “ 𝑐))    ⇒   ⊢ (𝐶 ∈ (𝑂 ∖ 𝐸) → ((𝑆‘𝐶) “ (𝑅‘𝐶)) = 𝐶)
Theorem	ballotlemrv 34487*	Value of 𝑅 evaluated at 𝐽. (Contributed by Thierry Arnoux, 17-Apr-2017.)
⊢ 𝑀 ∈ ℕ    &   ⊢ 𝑁 ∈ ℕ    &   ⊢ 𝑂 = {𝑐 ∈ 𝒫 (1...(𝑀 + 𝑁)) ∣ (♯‘𝑐) = 𝑀}    &   ⊢ 𝑃 = (𝑥 ∈ 𝒫 𝑂 ↦ ((♯‘𝑥) / (♯‘𝑂)))    &   ⊢ 𝐹 = (𝑐 ∈ 𝑂 ↦ (𝑖 ∈ ℤ ↦ ((♯‘((1...𝑖) ∩ 𝑐)) − (♯‘((1...𝑖) ∖ 𝑐)))))    &   ⊢ 𝐸 = {𝑐 ∈ 𝑂 ∣ ∀𝑖 ∈ (1...(𝑀 + 𝑁))0 < ((𝐹‘𝑐)‘𝑖)}    &   ⊢ 𝑁 < 𝑀    &   ⊢ 𝐼 = (𝑐 ∈ (𝑂 ∖ 𝐸) ↦ inf({𝑘 ∈ (1...(𝑀 + 𝑁)) ∣ ((𝐹‘𝑐)‘𝑘) = 0}, ℝ, < ))    &   ⊢ 𝑆 = (𝑐 ∈ (𝑂 ∖ 𝐸) ↦ (𝑖 ∈ (1...(𝑀 + 𝑁)) ↦ if(𝑖 ≤ (𝐼‘𝑐), (((𝐼‘𝑐) + 1) − 𝑖), 𝑖)))    &   ⊢ 𝑅 = (𝑐 ∈ (𝑂 ∖ 𝐸) ↦ ((𝑆‘𝑐) “ 𝑐))    ⇒   ⊢ ((𝐶 ∈ (𝑂 ∖ 𝐸) ∧ 𝐽 ∈ (1...(𝑀 + 𝑁))) → (𝐽 ∈ (𝑅‘𝐶) ↔ if(𝐽 ≤ (𝐼‘𝐶), (((𝐼‘𝐶) + 1) − 𝐽), 𝐽) ∈ 𝐶))
Theorem	ballotlemrv1 34488*	Value of 𝑅 before the tie. (Contributed by Thierry Arnoux, 11-Apr-2017.)
⊢ 𝑀 ∈ ℕ    &   ⊢ 𝑁 ∈ ℕ    &   ⊢ 𝑂 = {𝑐 ∈ 𝒫 (1...(𝑀 + 𝑁)) ∣ (♯‘𝑐) = 𝑀}    &   ⊢ 𝑃 = (𝑥 ∈ 𝒫 𝑂 ↦ ((♯‘𝑥) / (♯‘𝑂)))    &   ⊢ 𝐹 = (𝑐 ∈ 𝑂 ↦ (𝑖 ∈ ℤ ↦ ((♯‘((1...𝑖) ∩ 𝑐)) − (♯‘((1...𝑖) ∖ 𝑐)))))    &   ⊢ 𝐸 = {𝑐 ∈ 𝑂 ∣ ∀𝑖 ∈ (1...(𝑀 + 𝑁))0 < ((𝐹‘𝑐)‘𝑖)}    &   ⊢ 𝑁 < 𝑀    &   ⊢ 𝐼 = (𝑐 ∈ (𝑂 ∖ 𝐸) ↦ inf({𝑘 ∈ (1...(𝑀 + 𝑁)) ∣ ((𝐹‘𝑐)‘𝑘) = 0}, ℝ, < ))    &   ⊢ 𝑆 = (𝑐 ∈ (𝑂 ∖ 𝐸) ↦ (𝑖 ∈ (1...(𝑀 + 𝑁)) ↦ if(𝑖 ≤ (𝐼‘𝑐), (((𝐼‘𝑐) + 1) − 𝑖), 𝑖)))    &   ⊢ 𝑅 = (𝑐 ∈ (𝑂 ∖ 𝐸) ↦ ((𝑆‘𝑐) “ 𝑐))    ⇒   ⊢ ((𝐶 ∈ (𝑂 ∖ 𝐸) ∧ 𝐽 ∈ (1...(𝑀 + 𝑁)) ∧ 𝐽 ≤ (𝐼‘𝐶)) → (𝐽 ∈ (𝑅‘𝐶) ↔ (((𝐼‘𝐶) + 1) − 𝐽) ∈ 𝐶))
Theorem	ballotlemrv2 34489*	Value of 𝑅 after the tie. (Contributed by Thierry Arnoux, 11-Apr-2017.)
⊢ 𝑀 ∈ ℕ    &   ⊢ 𝑁 ∈ ℕ    &   ⊢ 𝑂 = {𝑐 ∈ 𝒫 (1...(𝑀 + 𝑁)) ∣ (♯‘𝑐) = 𝑀}    &   ⊢ 𝑃 = (𝑥 ∈ 𝒫 𝑂 ↦ ((♯‘𝑥) / (♯‘𝑂)))    &   ⊢ 𝐹 = (𝑐 ∈ 𝑂 ↦ (𝑖 ∈ ℤ ↦ ((♯‘((1...𝑖) ∩ 𝑐)) − (♯‘((1...𝑖) ∖ 𝑐)))))    &   ⊢ 𝐸 = {𝑐 ∈ 𝑂 ∣ ∀𝑖 ∈ (1...(𝑀 + 𝑁))0 < ((𝐹‘𝑐)‘𝑖)}    &   ⊢ 𝑁 < 𝑀    &   ⊢ 𝐼 = (𝑐 ∈ (𝑂 ∖ 𝐸) ↦ inf({𝑘 ∈ (1...(𝑀 + 𝑁)) ∣ ((𝐹‘𝑐)‘𝑘) = 0}, ℝ, < ))    &   ⊢ 𝑆 = (𝑐 ∈ (𝑂 ∖ 𝐸) ↦ (𝑖 ∈ (1...(𝑀 + 𝑁)) ↦ if(𝑖 ≤ (𝐼‘𝑐), (((𝐼‘𝑐) + 1) − 𝑖), 𝑖)))    &   ⊢ 𝑅 = (𝑐 ∈ (𝑂 ∖ 𝐸) ↦ ((𝑆‘𝑐) “ 𝑐))    ⇒   ⊢ ((𝐶 ∈ (𝑂 ∖ 𝐸) ∧ 𝐽 ∈ (1...(𝑀 + 𝑁)) ∧ (𝐼‘𝐶) < 𝐽) → (𝐽 ∈ (𝑅‘𝐶) ↔ 𝐽 ∈ 𝐶))
Theorem	ballotlemro 34490*	Range of 𝑅 is included in 𝑂. (Contributed by Thierry Arnoux, 17-Apr-2017.)
⊢ 𝑀 ∈ ℕ    &   ⊢ 𝑁 ∈ ℕ    &   ⊢ 𝑂 = {𝑐 ∈ 𝒫 (1...(𝑀 + 𝑁)) ∣ (♯‘𝑐) = 𝑀}    &   ⊢ 𝑃 = (𝑥 ∈ 𝒫 𝑂 ↦ ((♯‘𝑥) / (♯‘𝑂)))    &   ⊢ 𝐹 = (𝑐 ∈ 𝑂 ↦ (𝑖 ∈ ℤ ↦ ((♯‘((1...𝑖) ∩ 𝑐)) − (♯‘((1...𝑖) ∖ 𝑐)))))    &   ⊢ 𝐸 = {𝑐 ∈ 𝑂 ∣ ∀𝑖 ∈ (1...(𝑀 + 𝑁))0 < ((𝐹‘𝑐)‘𝑖)}    &   ⊢ 𝑁 < 𝑀    &   ⊢ 𝐼 = (𝑐 ∈ (𝑂 ∖ 𝐸) ↦ inf({𝑘 ∈ (1...(𝑀 + 𝑁)) ∣ ((𝐹‘𝑐)‘𝑘) = 0}, ℝ, < ))    &   ⊢ 𝑆 = (𝑐 ∈ (𝑂 ∖ 𝐸) ↦ (𝑖 ∈ (1...(𝑀 + 𝑁)) ↦ if(𝑖 ≤ (𝐼‘𝑐), (((𝐼‘𝑐) + 1) − 𝑖), 𝑖)))    &   ⊢ 𝑅 = (𝑐 ∈ (𝑂 ∖ 𝐸) ↦ ((𝑆‘𝑐) “ 𝑐))    ⇒   ⊢ (𝐶 ∈ (𝑂 ∖ 𝐸) → (𝑅‘𝐶) ∈ 𝑂)
Theorem	ballotlemgval 34491*	Expand the value of ↑. (Contributed by Thierry Arnoux, 21-Apr-2017.)
⊢ 𝑀 ∈ ℕ    &   ⊢ 𝑁 ∈ ℕ    &   ⊢ 𝑂 = {𝑐 ∈ 𝒫 (1...(𝑀 + 𝑁)) ∣ (♯‘𝑐) = 𝑀}    &   ⊢ 𝑃 = (𝑥 ∈ 𝒫 𝑂 ↦ ((♯‘𝑥) / (♯‘𝑂)))    &   ⊢ 𝐹 = (𝑐 ∈ 𝑂 ↦ (𝑖 ∈ ℤ ↦ ((♯‘((1...𝑖) ∩ 𝑐)) − (♯‘((1...𝑖) ∖ 𝑐)))))    &   ⊢ 𝐸 = {𝑐 ∈ 𝑂 ∣ ∀𝑖 ∈ (1...(𝑀 + 𝑁))0 < ((𝐹‘𝑐)‘𝑖)}    &   ⊢ 𝑁 < 𝑀    &   ⊢ 𝐼 = (𝑐 ∈ (𝑂 ∖ 𝐸) ↦ inf({𝑘 ∈ (1...(𝑀 + 𝑁)) ∣ ((𝐹‘𝑐)‘𝑘) = 0}, ℝ, < ))    &   ⊢ 𝑆 = (𝑐 ∈ (𝑂 ∖ 𝐸) ↦ (𝑖 ∈ (1...(𝑀 + 𝑁)) ↦ if(𝑖 ≤ (𝐼‘𝑐), (((𝐼‘𝑐) + 1) − 𝑖), 𝑖)))    &   ⊢ 𝑅 = (𝑐 ∈ (𝑂 ∖ 𝐸) ↦ ((𝑆‘𝑐) “ 𝑐))    &   ⊢ ↑ = (𝑢 ∈ Fin, 𝑣 ∈ Fin ↦ ((♯‘(𝑣 ∩ 𝑢)) − (♯‘(𝑣 ∖ 𝑢))))    ⇒   ⊢ ((𝑈 ∈ Fin ∧ 𝑉 ∈ Fin) → (𝑈 ↑ 𝑉) = ((♯‘(𝑉 ∩ 𝑈)) − (♯‘(𝑉 ∖ 𝑈))))
Theorem	ballotlemgun 34492*	A property of the defined ↑ operator. (Contributed by Thierry Arnoux, 26-Apr-2017.)
⊢ 𝑀 ∈ ℕ    &   ⊢ 𝑁 ∈ ℕ    &   ⊢ 𝑂 = {𝑐 ∈ 𝒫 (1...(𝑀 + 𝑁)) ∣ (♯‘𝑐) = 𝑀}    &   ⊢ 𝑃 = (𝑥 ∈ 𝒫 𝑂 ↦ ((♯‘𝑥) / (♯‘𝑂)))    &   ⊢ 𝐹 = (𝑐 ∈ 𝑂 ↦ (𝑖 ∈ ℤ ↦ ((♯‘((1...𝑖) ∩ 𝑐)) − (♯‘((1...𝑖) ∖ 𝑐)))))    &   ⊢ 𝐸 = {𝑐 ∈ 𝑂 ∣ ∀𝑖 ∈ (1...(𝑀 + 𝑁))0 < ((𝐹‘𝑐)‘𝑖)}    &   ⊢ 𝑁 < 𝑀    &   ⊢ 𝐼 = (𝑐 ∈ (𝑂 ∖ 𝐸) ↦ inf({𝑘 ∈ (1...(𝑀 + 𝑁)) ∣ ((𝐹‘𝑐)‘𝑘) = 0}, ℝ, < ))    &   ⊢ 𝑆 = (𝑐 ∈ (𝑂 ∖ 𝐸) ↦ (𝑖 ∈ (1...(𝑀 + 𝑁)) ↦ if(𝑖 ≤ (𝐼‘𝑐), (((𝐼‘𝑐) + 1) − 𝑖), 𝑖)))    &   ⊢ 𝑅 = (𝑐 ∈ (𝑂 ∖ 𝐸) ↦ ((𝑆‘𝑐) “ 𝑐))    &   ⊢ ↑ = (𝑢 ∈ Fin, 𝑣 ∈ Fin ↦ ((♯‘(𝑣 ∩ 𝑢)) − (♯‘(𝑣 ∖ 𝑢))))    &   ⊢ (𝜑 → 𝑈 ∈ Fin)    &   ⊢ (𝜑 → 𝑉 ∈ Fin)    &   ⊢ (𝜑 → 𝑊 ∈ Fin)    &   ⊢ (𝜑 → (𝑉 ∩ 𝑊) = ∅)    ⇒   ⊢ (𝜑 → (𝑈 ↑ (𝑉 ∪ 𝑊)) = ((𝑈 ↑ 𝑉) + (𝑈 ↑ 𝑊)))
Theorem	ballotlemfg 34493*	Express the value of (𝐹‘𝐶) in terms of ↑. (Contributed by Thierry Arnoux, 21-Apr-2017.)
⊢ 𝑀 ∈ ℕ    &   ⊢ 𝑁 ∈ ℕ    &   ⊢ 𝑂 = {𝑐 ∈ 𝒫 (1...(𝑀 + 𝑁)) ∣ (♯‘𝑐) = 𝑀}    &   ⊢ 𝑃 = (𝑥 ∈ 𝒫 𝑂 ↦ ((♯‘𝑥) / (♯‘𝑂)))    &   ⊢ 𝐹 = (𝑐 ∈ 𝑂 ↦ (𝑖 ∈ ℤ ↦ ((♯‘((1...𝑖) ∩ 𝑐)) − (♯‘((1...𝑖) ∖ 𝑐)))))    &   ⊢ 𝐸 = {𝑐 ∈ 𝑂 ∣ ∀𝑖 ∈ (1...(𝑀 + 𝑁))0 < ((𝐹‘𝑐)‘𝑖)}    &   ⊢ 𝑁 < 𝑀    &   ⊢ 𝐼 = (𝑐 ∈ (𝑂 ∖ 𝐸) ↦ inf({𝑘 ∈ (1...(𝑀 + 𝑁)) ∣ ((𝐹‘𝑐)‘𝑘) = 0}, ℝ, < ))    &   ⊢ 𝑆 = (𝑐 ∈ (𝑂 ∖ 𝐸) ↦ (𝑖 ∈ (1...(𝑀 + 𝑁)) ↦ if(𝑖 ≤ (𝐼‘𝑐), (((𝐼‘𝑐) + 1) − 𝑖), 𝑖)))    &   ⊢ 𝑅 = (𝑐 ∈ (𝑂 ∖ 𝐸) ↦ ((𝑆‘𝑐) “ 𝑐))    &   ⊢ ↑ = (𝑢 ∈ Fin, 𝑣 ∈ Fin ↦ ((♯‘(𝑣 ∩ 𝑢)) − (♯‘(𝑣 ∖ 𝑢))))    ⇒   ⊢ ((𝐶 ∈ (𝑂 ∖ 𝐸) ∧ 𝐽 ∈ (0...(𝑀 + 𝑁))) → ((𝐹‘𝐶)‘𝐽) = (𝐶 ↑ (1...𝐽)))
Theorem	ballotlemfrc 34494*	Express the value of (𝐹‘(𝑅‘𝐶)) in terms of the newly defined ↑. (Contributed by Thierry Arnoux, 21-Apr-2017.)
⊢ 𝑀 ∈ ℕ    &   ⊢ 𝑁 ∈ ℕ    &   ⊢ 𝑂 = {𝑐 ∈ 𝒫 (1...(𝑀 + 𝑁)) ∣ (♯‘𝑐) = 𝑀}    &   ⊢ 𝑃 = (𝑥 ∈ 𝒫 𝑂 ↦ ((♯‘𝑥) / (♯‘𝑂)))    &   ⊢ 𝐹 = (𝑐 ∈ 𝑂 ↦ (𝑖 ∈ ℤ ↦ ((♯‘((1...𝑖) ∩ 𝑐)) − (♯‘((1...𝑖) ∖ 𝑐)))))    &   ⊢ 𝐸 = {𝑐 ∈ 𝑂 ∣ ∀𝑖 ∈ (1...(𝑀 + 𝑁))0 < ((𝐹‘𝑐)‘𝑖)}    &   ⊢ 𝑁 < 𝑀    &   ⊢ 𝐼 = (𝑐 ∈ (𝑂 ∖ 𝐸) ↦ inf({𝑘 ∈ (1...(𝑀 + 𝑁)) ∣ ((𝐹‘𝑐)‘𝑘) = 0}, ℝ, < ))    &   ⊢ 𝑆 = (𝑐 ∈ (𝑂 ∖ 𝐸) ↦ (𝑖 ∈ (1...(𝑀 + 𝑁)) ↦ if(𝑖 ≤ (𝐼‘𝑐), (((𝐼‘𝑐) + 1) − 𝑖), 𝑖)))    &   ⊢ 𝑅 = (𝑐 ∈ (𝑂 ∖ 𝐸) ↦ ((𝑆‘𝑐) “ 𝑐))    &   ⊢ ↑ = (𝑢 ∈ Fin, 𝑣 ∈ Fin ↦ ((♯‘(𝑣 ∩ 𝑢)) − (♯‘(𝑣 ∖ 𝑢))))    ⇒   ⊢ ((𝐶 ∈ (𝑂 ∖ 𝐸) ∧ 𝐽 ∈ (1...(𝐼‘𝐶))) → ((𝐹‘(𝑅‘𝐶))‘𝐽) = (𝐶 ↑ (((𝑆‘𝐶)‘𝐽)...(𝐼‘𝐶))))
Theorem	ballotlemfrci 34495*	Reverse counting preserves a tie at the first tie. (Contributed by Thierry Arnoux, 21-Apr-2017.)
⊢ 𝑀 ∈ ℕ    &   ⊢ 𝑁 ∈ ℕ    &   ⊢ 𝑂 = {𝑐 ∈ 𝒫 (1...(𝑀 + 𝑁)) ∣ (♯‘𝑐) = 𝑀}    &   ⊢ 𝑃 = (𝑥 ∈ 𝒫 𝑂 ↦ ((♯‘𝑥) / (♯‘𝑂)))    &   ⊢ 𝐹 = (𝑐 ∈ 𝑂 ↦ (𝑖 ∈ ℤ ↦ ((♯‘((1...𝑖) ∩ 𝑐)) − (♯‘((1...𝑖) ∖ 𝑐)))))    &   ⊢ 𝐸 = {𝑐 ∈ 𝑂 ∣ ∀𝑖 ∈ (1...(𝑀 + 𝑁))0 < ((𝐹‘𝑐)‘𝑖)}    &   ⊢ 𝑁 < 𝑀    &   ⊢ 𝐼 = (𝑐 ∈ (𝑂 ∖ 𝐸) ↦ inf({𝑘 ∈ (1...(𝑀 + 𝑁)) ∣ ((𝐹‘𝑐)‘𝑘) = 0}, ℝ, < ))    &   ⊢ 𝑆 = (𝑐 ∈ (𝑂 ∖ 𝐸) ↦ (𝑖 ∈ (1...(𝑀 + 𝑁)) ↦ if(𝑖 ≤ (𝐼‘𝑐), (((𝐼‘𝑐) + 1) − 𝑖), 𝑖)))    &   ⊢ 𝑅 = (𝑐 ∈ (𝑂 ∖ 𝐸) ↦ ((𝑆‘𝑐) “ 𝑐))    &   ⊢ ↑ = (𝑢 ∈ Fin, 𝑣 ∈ Fin ↦ ((♯‘(𝑣 ∩ 𝑢)) − (♯‘(𝑣 ∖ 𝑢))))    ⇒   ⊢ (𝐶 ∈ (𝑂 ∖ 𝐸) → ((𝐹‘(𝑅‘𝐶))‘(𝐼‘𝐶)) = 0)
Theorem	ballotlemfrceq 34496*	Value of 𝐹 for a reverse counting (𝑅‘𝐶). (Contributed by Thierry Arnoux, 27-Apr-2017.)
⊢ 𝑀 ∈ ℕ    &   ⊢ 𝑁 ∈ ℕ    &   ⊢ 𝑂 = {𝑐 ∈ 𝒫 (1...(𝑀 + 𝑁)) ∣ (♯‘𝑐) = 𝑀}    &   ⊢ 𝑃 = (𝑥 ∈ 𝒫 𝑂 ↦ ((♯‘𝑥) / (♯‘𝑂)))    &   ⊢ 𝐹 = (𝑐 ∈ 𝑂 ↦ (𝑖 ∈ ℤ ↦ ((♯‘((1...𝑖) ∩ 𝑐)) − (♯‘((1...𝑖) ∖ 𝑐)))))    &   ⊢ 𝐸 = {𝑐 ∈ 𝑂 ∣ ∀𝑖 ∈ (1...(𝑀 + 𝑁))0 < ((𝐹‘𝑐)‘𝑖)}    &   ⊢ 𝑁 < 𝑀    &   ⊢ 𝐼 = (𝑐 ∈ (𝑂 ∖ 𝐸) ↦ inf({𝑘 ∈ (1...(𝑀 + 𝑁)) ∣ ((𝐹‘𝑐)‘𝑘) = 0}, ℝ, < ))    &   ⊢ 𝑆 = (𝑐 ∈ (𝑂 ∖ 𝐸) ↦ (𝑖 ∈ (1...(𝑀 + 𝑁)) ↦ if(𝑖 ≤ (𝐼‘𝑐), (((𝐼‘𝑐) + 1) − 𝑖), 𝑖)))    &   ⊢ 𝑅 = (𝑐 ∈ (𝑂 ∖ 𝐸) ↦ ((𝑆‘𝑐) “ 𝑐))    &   ⊢ ↑ = (𝑢 ∈ Fin, 𝑣 ∈ Fin ↦ ((♯‘(𝑣 ∩ 𝑢)) − (♯‘(𝑣 ∖ 𝑢))))    ⇒   ⊢ ((𝐶 ∈ (𝑂 ∖ 𝐸) ∧ 𝐽 ∈ (1...(𝐼‘𝐶))) → ((𝐹‘𝐶)‘(((𝑆‘𝐶)‘𝐽) − 1)) = -((𝐹‘(𝑅‘𝐶))‘𝐽))
Theorem	ballotlemfrcn0 34497*	Value of 𝐹 for a reversed counting (𝑅‘𝐶), before the first tie, cannot be zero. (Contributed by Thierry Arnoux, 25-Apr-2017.) (Revised by AV, 6-Oct-2020.)
⊢ 𝑀 ∈ ℕ    &   ⊢ 𝑁 ∈ ℕ    &   ⊢ 𝑂 = {𝑐 ∈ 𝒫 (1...(𝑀 + 𝑁)) ∣ (♯‘𝑐) = 𝑀}    &   ⊢ 𝑃 = (𝑥 ∈ 𝒫 𝑂 ↦ ((♯‘𝑥) / (♯‘𝑂)))    &   ⊢ 𝐹 = (𝑐 ∈ 𝑂 ↦ (𝑖 ∈ ℤ ↦ ((♯‘((1...𝑖) ∩ 𝑐)) − (♯‘((1...𝑖) ∖ 𝑐)))))    &   ⊢ 𝐸 = {𝑐 ∈ 𝑂 ∣ ∀𝑖 ∈ (1...(𝑀 + 𝑁))0 < ((𝐹‘𝑐)‘𝑖)}    &   ⊢ 𝑁 < 𝑀    &   ⊢ 𝐼 = (𝑐 ∈ (𝑂 ∖ 𝐸) ↦ inf({𝑘 ∈ (1...(𝑀 + 𝑁)) ∣ ((𝐹‘𝑐)‘𝑘) = 0}, ℝ, < ))    &   ⊢ 𝑆 = (𝑐 ∈ (𝑂 ∖ 𝐸) ↦ (𝑖 ∈ (1...(𝑀 + 𝑁)) ↦ if(𝑖 ≤ (𝐼‘𝑐), (((𝐼‘𝑐) + 1) − 𝑖), 𝑖)))    &   ⊢ 𝑅 = (𝑐 ∈ (𝑂 ∖ 𝐸) ↦ ((𝑆‘𝑐) “ 𝑐))    ⇒   ⊢ ((𝐶 ∈ (𝑂 ∖ 𝐸) ∧ 𝐽 ∈ (1...(𝑀 + 𝑁)) ∧ 𝐽 < (𝐼‘𝐶)) → ((𝐹‘(𝑅‘𝐶))‘𝐽) ≠ 0)
Theorem	ballotlemrc 34498*	Range of 𝑅. (Contributed by Thierry Arnoux, 19-Apr-2017.)
⊢ 𝑀 ∈ ℕ    &   ⊢ 𝑁 ∈ ℕ    &   ⊢ 𝑂 = {𝑐 ∈ 𝒫 (1...(𝑀 + 𝑁)) ∣ (♯‘𝑐) = 𝑀}    &   ⊢ 𝑃 = (𝑥 ∈ 𝒫 𝑂 ↦ ((♯‘𝑥) / (♯‘𝑂)))    &   ⊢ 𝐹 = (𝑐 ∈ 𝑂 ↦ (𝑖 ∈ ℤ ↦ ((♯‘((1...𝑖) ∩ 𝑐)) − (♯‘((1...𝑖) ∖ 𝑐)))))    &   ⊢ 𝐸 = {𝑐 ∈ 𝑂 ∣ ∀𝑖 ∈ (1...(𝑀 + 𝑁))0 < ((𝐹‘𝑐)‘𝑖)}    &   ⊢ 𝑁 < 𝑀    &   ⊢ 𝐼 = (𝑐 ∈ (𝑂 ∖ 𝐸) ↦ inf({𝑘 ∈ (1...(𝑀 + 𝑁)) ∣ ((𝐹‘𝑐)‘𝑘) = 0}, ℝ, < ))    &   ⊢ 𝑆 = (𝑐 ∈ (𝑂 ∖ 𝐸) ↦ (𝑖 ∈ (1...(𝑀 + 𝑁)) ↦ if(𝑖 ≤ (𝐼‘𝑐), (((𝐼‘𝑐) + 1) − 𝑖), 𝑖)))    &   ⊢ 𝑅 = (𝑐 ∈ (𝑂 ∖ 𝐸) ↦ ((𝑆‘𝑐) “ 𝑐))    ⇒   ⊢ (𝐶 ∈ (𝑂 ∖ 𝐸) → (𝑅‘𝐶) ∈ (𝑂 ∖ 𝐸))
Theorem	ballotlemirc 34499*	Applying 𝑅 does not change first ties. (Contributed by Thierry Arnoux, 19-Apr-2017.) (Revised by AV, 6-Oct-2020.)
⊢ 𝑀 ∈ ℕ    &   ⊢ 𝑁 ∈ ℕ    &   ⊢ 𝑂 = {𝑐 ∈ 𝒫 (1...(𝑀 + 𝑁)) ∣ (♯‘𝑐) = 𝑀}    &   ⊢ 𝑃 = (𝑥 ∈ 𝒫 𝑂 ↦ ((♯‘𝑥) / (♯‘𝑂)))    &   ⊢ 𝐹 = (𝑐 ∈ 𝑂 ↦ (𝑖 ∈ ℤ ↦ ((♯‘((1...𝑖) ∩ 𝑐)) − (♯‘((1...𝑖) ∖ 𝑐)))))    &   ⊢ 𝐸 = {𝑐 ∈ 𝑂 ∣ ∀𝑖 ∈ (1...(𝑀 + 𝑁))0 < ((𝐹‘𝑐)‘𝑖)}    &   ⊢ 𝑁 < 𝑀    &   ⊢ 𝐼 = (𝑐 ∈ (𝑂 ∖ 𝐸) ↦ inf({𝑘 ∈ (1...(𝑀 + 𝑁)) ∣ ((𝐹‘𝑐)‘𝑘) = 0}, ℝ, < ))    &   ⊢ 𝑆 = (𝑐 ∈ (𝑂 ∖ 𝐸) ↦ (𝑖 ∈ (1...(𝑀 + 𝑁)) ↦ if(𝑖 ≤ (𝐼‘𝑐), (((𝐼‘𝑐) + 1) − 𝑖), 𝑖)))    &   ⊢ 𝑅 = (𝑐 ∈ (𝑂 ∖ 𝐸) ↦ ((𝑆‘𝑐) “ 𝑐))    ⇒   ⊢ (𝐶 ∈ (𝑂 ∖ 𝐸) → (𝐼‘(𝑅‘𝐶)) = (𝐼‘𝐶))
Theorem	ballotlemrinv0 34500*	Lemma for ballotlemrinv 34501. (Contributed by Thierry Arnoux, 18-Apr-2017.)
⊢ 𝑀 ∈ ℕ    &   ⊢ 𝑁 ∈ ℕ    &   ⊢ 𝑂 = {𝑐 ∈ 𝒫 (1...(𝑀 + 𝑁)) ∣ (♯‘𝑐) = 𝑀}    &   ⊢ 𝑃 = (𝑥 ∈ 𝒫 𝑂 ↦ ((♯‘𝑥) / (♯‘𝑂)))    &   ⊢ 𝐹 = (𝑐 ∈ 𝑂 ↦ (𝑖 ∈ ℤ ↦ ((♯‘((1...𝑖) ∩ 𝑐)) − (♯‘((1...𝑖) ∖ 𝑐)))))    &   ⊢ 𝐸 = {𝑐 ∈ 𝑂 ∣ ∀𝑖 ∈ (1...(𝑀 + 𝑁))0 < ((𝐹‘𝑐)‘𝑖)}    &   ⊢ 𝑁 < 𝑀    &   ⊢ 𝐼 = (𝑐 ∈ (𝑂 ∖ 𝐸) ↦ inf({𝑘 ∈ (1...(𝑀 + 𝑁)) ∣ ((𝐹‘𝑐)‘𝑘) = 0}, ℝ, < ))    &   ⊢ 𝑆 = (𝑐 ∈ (𝑂 ∖ 𝐸) ↦ (𝑖 ∈ (1...(𝑀 + 𝑁)) ↦ if(𝑖 ≤ (𝐼‘𝑐), (((𝐼‘𝑐) + 1) − 𝑖), 𝑖)))    &   ⊢ 𝑅 = (𝑐 ∈ (𝑂 ∖ 𝐸) ↦ ((𝑆‘𝑐) “ 𝑐))    ⇒   ⊢ ((𝐶 ∈ (𝑂 ∖ 𝐸) ∧ 𝐷 = ((𝑆‘𝐶) “ 𝐶)) → (𝐷 ∈ (𝑂 ∖ 𝐸) ∧ 𝐶 = ((𝑆‘𝐷) “ 𝐷)))