P. 347 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 34601-34700   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	probvalrnd 34601	The value of a probability is a real number. (Contributed by Thierry Arnoux, 2-Feb-2017.)
⊢ (𝜑 → 𝑃 ∈ Prob)    &   ⊢ (𝜑 → 𝐴 ∈ dom 𝑃)    ⇒   ⊢ (𝜑 → (𝑃‘𝐴) ∈ ℝ)
Theorem	probtotrnd 34602	The probability of the universe set is finite. (Contributed by Thierry Arnoux, 2-Feb-2017.)
⊢ (𝜑 → 𝑃 ∈ Prob)    ⇒   ⊢ (𝜑 → (𝑃‘∪ dom 𝑃) ∈ ℝ)
Theorem	totprobd 34603*	Law of total probability, deduction form. (Contributed by Thierry Arnoux, 25-Dec-2016.)
⊢ (𝜑 → 𝑃 ∈ Prob)    &   ⊢ (𝜑 → 𝐴 ∈ dom 𝑃)    &   ⊢ (𝜑 → 𝐵 ∈ 𝒫 dom 𝑃)    &   ⊢ (𝜑 → ∪ 𝐵 = ∪ dom 𝑃)    &   ⊢ (𝜑 → 𝐵 ≼ ω)    &   ⊢ (𝜑 → Disj 𝑏 ∈ 𝐵 𝑏)    ⇒   ⊢ (𝜑 → (𝑃‘𝐴) = Σ*𝑏 ∈ 𝐵(𝑃‘(𝑏 ∩ 𝐴)))
Theorem	totprob 34604*	Law of total probability. (Contributed by Thierry Arnoux, 25-Dec-2016.)
⊢ ((𝑃 ∈ Prob ∧ 𝐴 ∈ dom 𝑃 ∧ (∪ 𝐵 = ∪ dom 𝑃 ∧ 𝐵 ∈ 𝒫 dom 𝑃 ∧ (𝐵 ≼ ω ∧ Disj 𝑏 ∈ 𝐵 𝑏))) → (𝑃‘𝐴) = Σ*𝑏 ∈ 𝐵(𝑃‘(𝑏 ∩ 𝐴)))
Theorem	probfinmeasb 34605	Build a probability measure from a finite measure. (Contributed by Thierry Arnoux, 31-Jan-2017.)
⊢ ((𝑀 ∈ (measures‘𝑆) ∧ (𝑀‘∪ 𝑆) ∈ ℝ+) → (𝑀 ∘f/c /𝑒 (𝑀‘∪ 𝑆)) ∈ Prob)
Theorem	probfinmeasbALTV 34606*	Alternate version of probfinmeasb 34605. (Contributed by Thierry Arnoux, 17-Dec-2016.) (New usage is discouraged.)
⊢ ((𝑀 ∈ (measures‘𝑆) ∧ (𝑀‘∪ 𝑆) ∈ ℝ+) → (𝑥 ∈ 𝑆 ↦ ((𝑀‘𝑥) /𝑒 (𝑀‘∪ 𝑆))) ∈ Prob)
Theorem	probmeasb 34607*	Build a probability from a measure and a set with finite measure. (Contributed by Thierry Arnoux, 25-Dec-2016.)
⊢ ((𝑀 ∈ (measures‘𝑆) ∧ 𝐴 ∈ 𝑆 ∧ (𝑀‘𝐴) ∈ ℝ+) → (𝑥 ∈ 𝑆 ↦ ((𝑀‘(𝑥 ∩ 𝐴)) / (𝑀‘𝐴))) ∈ Prob)
21.3.23.2  Conditional Probabilities
Syntax	ccprob 34608	Extends class notation with the conditional probability builder.
class cprob
Definition	df-cndprob 34609*	Define the conditional probability. (Contributed by Thierry Arnoux, 14-Sep-2016.) (Revised by Thierry Arnoux, 21-Jan-2017.)
⊢ cprob = (𝑝 ∈ Prob ↦ (𝑎 ∈ dom 𝑝, 𝑏 ∈ dom 𝑝 ↦ ((𝑝‘(𝑎 ∩ 𝑏)) / (𝑝‘𝑏))))
Theorem	cndprobval 34610	The value of the conditional probability , i.e. the probability for the event 𝐴, given 𝐵, under the probability law 𝑃. (Contributed by Thierry Arnoux, 21-Jan-2017.)
⊢ ((𝑃 ∈ Prob ∧ 𝐴 ∈ dom 𝑃 ∧ 𝐵 ∈ dom 𝑃) → ((cprob‘𝑃)‘⟨𝐴, 𝐵⟩) = ((𝑃‘(𝐴 ∩ 𝐵)) / (𝑃‘𝐵)))
Theorem	cndprobin 34611	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 34612	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 34613	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 34614	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 34615*	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 34616	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 34617	Extend class notation with the class of real-valued random variables.
class rRndVar
Definition	df-rrv 34618	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 34619	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 34620*	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 34621	A real-valued random variable is a function. (Contributed by Thierry Arnoux, 25-Jan-2017.)
⊢ (𝜑 → 𝑃 ∈ Prob)    &   ⊢ (𝜑 → 𝑋 ∈ (rRndVar‘𝑃))    ⇒   ⊢ (𝜑 → 𝑋:∪ dom 𝑃⟶ℝ)
Theorem	rrvfn 34622	A real-valued random variable is a function over the universe. (Contributed by Thierry Arnoux, 25-Jan-2017.)
⊢ (𝜑 → 𝑃 ∈ Prob)    &   ⊢ (𝜑 → 𝑋 ∈ (rRndVar‘𝑃))    ⇒   ⊢ (𝜑 → 𝑋 Fn ∪ dom 𝑃)
Theorem	rrvdm 34623	The domain of a random variable is the universe. (Contributed by Thierry Arnoux, 25-Jan-2017.)
⊢ (𝜑 → 𝑃 ∈ Prob)    &   ⊢ (𝜑 → 𝑋 ∈ (rRndVar‘𝑃))    ⇒   ⊢ (𝜑 → dom 𝑋 = ∪ dom 𝑃)
Theorem	rrvrnss 34624	The range of a random variable as a subset of ℝ. (Contributed by Thierry Arnoux, 6-Feb-2017.)
⊢ (𝜑 → 𝑃 ∈ Prob)    &   ⊢ (𝜑 → 𝑋 ∈ (rRndVar‘𝑃))    ⇒   ⊢ (𝜑 → ran 𝑋 ⊆ ℝ)
Theorem	rrvf2 34625	A real-valued random variable is a function. (Contributed by Thierry Arnoux, 25-Jan-2017.)
⊢ (𝜑 → 𝑃 ∈ Prob)    &   ⊢ (𝜑 → 𝑋 ∈ (rRndVar‘𝑃))    ⇒   ⊢ (𝜑 → 𝑋:dom 𝑋⟶ℝ)
Theorem	rrvdmss 34626	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 34627*	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 34628*	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 34629	The sum of two random variables is a random variable. (Contributed by Thierry Arnoux, 4-Jun-2017.)
⊢ (𝜑 → 𝑃 ∈ Prob)    &   ⊢ (𝜑 → 𝑋 ∈ (rRndVar‘𝑃))    &   ⊢ (𝜑 → 𝑌 ∈ (rRndVar‘𝑃))    ⇒   ⊢ (𝜑 → (𝑋 ∘f + 𝑌) ∈ (rRndVar‘𝑃))
Theorem	rrvmulc 34630	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 34631	An indexed sum of random variables is a random variable. (Contributed by Thierry Arnoux, 22-May-2017.)
⊢ (𝜑 → 𝑃 ∈ Prob)    &   ⊢ (𝜑 → 𝑋:ℕ⟶(rRndVar‘𝑃))    &   ⊢ ((𝜑 ∧ 𝑁 ∈ ℕ) → 𝑆 = (seq1( ∘f + , 𝑋)‘𝑁))    ⇒   ⊢ ((𝜑 ∧ 𝑁 ∈ ℕ) → 𝑆 ∈ (rRndVar‘𝑃))
Theorem	boolesineq 34632*	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 34633	Extend class notation to include the preimage set mapping operator.
class ∘RV/𝑐𝑅
Definition	df-orvc 34634*	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 5809- elementhood: {𝑋 ∈ 𝐴} as (𝑋∘RV/𝑐 E 𝐴) cf. epel 5535- 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 34635*	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 34636*	Another way to express the value of the preimage mapping operator. (Contributed by Thierry Arnoux, 19-Jan-2017.)
⊢ (𝜑 → Fun 𝑋)    &   ⊢ (𝜑 → 𝑋 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑊)    ⇒   ⊢ (𝜑 → (𝑋∘RV/𝑐𝑅𝐴) = {𝑧 ∈ dom 𝑋 ∣ (𝑋‘𝑧)𝑅𝐴})
Theorem	elorvc 34637*	Elementhood of a preimage. (Contributed by Thierry Arnoux, 21-Jan-2017.)
⊢ (𝜑 → Fun 𝑋)    &   ⊢ (𝜑 → 𝑋 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑊)    ⇒   ⊢ ((𝜑 ∧ 𝑧 ∈ dom 𝑋) → (𝑧 ∈ (𝑋∘RV/𝑐𝑅𝐴) ↔ (𝑋‘𝑧)𝑅𝐴))
Theorem	orvcval4 34638*	The value of the preimage mapping operator can be restricted to preimages in the base set of the topology. Cf. orvcval 34635. (Contributed by Thierry Arnoux, 21-Jan-2017.)
⊢ (𝜑 → 𝑆 ∈ ∪ ran sigAlgebra)    &   ⊢ (𝜑 → 𝐽 ∈ Top)    &   ⊢ (𝜑 → 𝑋 ∈ (𝑆MblFnM(sigaGen‘𝐽)))    &   ⊢ (𝜑 → 𝐴 ∈ 𝑉)    ⇒   ⊢ (𝜑 → (𝑋∘RV/𝑐𝑅𝐴) = (◡𝑋 “ {𝑦 ∈ ∪ 𝐽 ∣ 𝑦𝑅𝐴}))
Theorem	orvcoel 34639*	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 34640*	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 34641*	Elementhood of a preimage for a real-valued random variable. (Contributed by Thierry Arnoux, 21-Jan-2017.)
⊢ (𝜑 → 𝑃 ∈ Prob)    &   ⊢ (𝜑 → 𝑋 ∈ (rRndVar‘𝑃))    &   ⊢ (𝜑 → 𝐴 ∈ 𝑉)    ⇒   ⊢ ((𝜑 ∧ 𝑧 ∈ ∪ dom 𝑃) → (𝑧 ∈ (𝑋∘RV/𝑐𝑅𝐴) ↔ (𝑋‘𝑧)𝑅𝐴))
Theorem	orrvcval4 34642*	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 34643*	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 34644*	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 34645	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 34646	Preimage maps produced by the membership relation. (Contributed by Thierry Arnoux, 6-Feb-2017.)
⊢ (𝜑 → 𝑃 ∈ Prob)    &   ⊢ (𝜑 → 𝑋 ∈ (rRndVar‘𝑃))    &   ⊢ (𝜑 → 𝐴 ∈ 𝔅ℝ)    ⇒   ⊢ (𝜑 → (𝑋∘RV/𝑐 E 𝐴) = (◡𝑋 “ 𝐴))
Theorem	orvcelel 34647	Preimage maps produced by the membership relation are measurable sets. (Contributed by Thierry Arnoux, 5-Feb-2017.)
⊢ (𝜑 → 𝑃 ∈ Prob)    &   ⊢ (𝜑 → 𝑋 ∈ (rRndVar‘𝑃))    &   ⊢ (𝜑 → 𝐴 ∈ 𝔅ℝ)    ⇒   ⊢ (𝜑 → (𝑋∘RV/𝑐 E 𝐴) ∈ dom 𝑃)
Theorem	dstrvval 34648*	The value of the distribution of a random variable. (Contributed by Thierry Arnoux, 9-Feb-2017.)
⊢ (𝜑 → 𝑃 ∈ Prob)    &   ⊢ (𝜑 → 𝑋 ∈ (rRndVar‘𝑃))    &   ⊢ (𝜑 → 𝐷 = (𝑎 ∈ 𝔅ℝ ↦ (𝑃‘(𝑋∘RV/𝑐 E 𝑎))))    &   ⊢ (𝜑 → 𝐴 ∈ 𝔅ℝ)    ⇒   ⊢ (𝜑 → (𝐷‘𝐴) = (𝑃‘(◡𝑋 “ 𝐴)))
Theorem	dstrvprob 34649*	The distribution of a random variable is a probability law. (TODO: could be shortened using dstrvval 34648). (Contributed by Thierry Arnoux, 10-Feb-2017.)
⊢ (𝜑 → 𝑃 ∈ Prob)    &   ⊢ (𝜑 → 𝑋 ∈ (rRndVar‘𝑃))    &   ⊢ (𝜑 → 𝐷 = (𝑎 ∈ 𝔅ℝ ↦ (𝑃‘(𝑋∘RV/𝑐 E 𝑎))))    ⇒   ⊢ (𝜑 → 𝐷 ∈ Prob)
21.3.23.6  Cumulative Distribution Functions
Theorem	orvclteel 34650	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 34651	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 34652*	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 34653	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 34654*	A cumulative distribution function is nondecreasing. (Contributed by Thierry Arnoux, 11-Feb-2017.)
⊢ (𝜑 → 𝑃 ∈ Prob)    &   ⊢ (𝜑 → 𝑋 ∈ (rRndVar‘𝑃))    &   ⊢ (𝜑 → 𝐹 = (𝑥 ∈ ℝ ↦ (𝑃‘(𝑋∘RV/𝑐 ≤ 𝑥))))    &   ⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → 𝐴 ≤ 𝐵)    ⇒   ⊢ (𝜑 → (𝐹‘𝐴) ≤ (𝐹‘𝐵))
Theorem	dstfrvclim1 34655*	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 34656	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 34657	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 34658	The space of our coin-flip probability. (Contributed by Thierry Arnoux, 15-Jan-2017.)
⊢ 𝐻 ∈ V    &   ⊢ 𝑇 ∈ V    &   ⊢ 𝐻 ≠ 𝑇    &   ⊢ 𝑃 = ((♯ ↾ 𝒫 {𝐻, 𝑇}) ∘f/c / 2)    &   ⊢ 𝑋 = {⟨𝐻, 1⟩, ⟨𝑇, 0⟩}    ⇒   ⊢ dom 𝑃 = 𝒫 {𝐻, 𝑇}
Theorem	coinflipuniv 34659	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 34660	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 34661	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 34662	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 34663*	𝑂 is a set. (Contributed by Thierry Arnoux, 7-Dec-2016.)
⊢ 𝑀 ∈ ℕ    &   ⊢ 𝑁 ∈ ℕ    &   ⊢ 𝑂 = {𝑐 ∈ 𝒫 (1...(𝑀 + 𝑁)) ∣ (♯‘𝑐) = 𝑀}    ⇒   ⊢ 𝑂 ∈ V
Theorem	ballotlem1 34664*	The size of the universe is a binomial coefficient. (Contributed by Thierry Arnoux, 23-Nov-2016.)
⊢ 𝑀 ∈ ℕ    &   ⊢ 𝑁 ∈ ℕ    &   ⊢ 𝑂 = {𝑐 ∈ 𝒫 (1...(𝑀 + 𝑁)) ∣ (♯‘𝑐) = 𝑀}    ⇒   ⊢ (♯‘𝑂) = ((𝑀 + 𝑁)C𝑀)
Theorem	ballotlemelo 34665*	Elementhood in 𝑂. (Contributed by Thierry Arnoux, 17-Apr-2017.)
⊢ 𝑀 ∈ ℕ    &   ⊢ 𝑁 ∈ ℕ    &   ⊢ 𝑂 = {𝑐 ∈ 𝒫 (1...(𝑀 + 𝑁)) ∣ (♯‘𝑐) = 𝑀}    ⇒   ⊢ (𝐶 ∈ 𝑂 ↔ (𝐶 ⊆ (1...(𝑀 + 𝑁)) ∧ (♯‘𝐶) = 𝑀))
Theorem	ballotlem2 34666*	The probability that the first vote picked in a count is a B. (Contributed by Thierry Arnoux, 23-Nov-2016.)
⊢ 𝑀 ∈ ℕ    &   ⊢ 𝑁 ∈ ℕ    &   ⊢ 𝑂 = {𝑐 ∈ 𝒫 (1...(𝑀 + 𝑁)) ∣ (♯‘𝑐) = 𝑀}    &   ⊢ 𝑃 = (𝑥 ∈ 𝒫 𝑂 ↦ ((♯‘𝑥) / (♯‘𝑂)))    ⇒   ⊢ (𝑃‘{𝑐 ∈ 𝑂 ∣ ¬ 1 ∈ 𝑐}) = (𝑁 / (𝑀 + 𝑁))
Theorem	ballotlemfval 34667*	The value of 𝐹. (Contributed by Thierry Arnoux, 23-Nov-2016.)
⊢ 𝑀 ∈ ℕ    &   ⊢ 𝑁 ∈ ℕ    &   ⊢ 𝑂 = {𝑐 ∈ 𝒫 (1...(𝑀 + 𝑁)) ∣ (♯‘𝑐) = 𝑀}    &   ⊢ 𝑃 = (𝑥 ∈ 𝒫 𝑂 ↦ ((♯‘𝑥) / (♯‘𝑂)))    &   ⊢ 𝐹 = (𝑐 ∈ 𝑂 ↦ (𝑖 ∈ ℤ ↦ ((♯‘((1...𝑖) ∩ 𝑐)) − (♯‘((1...𝑖) ∖ 𝑐)))))    &   ⊢ (𝜑 → 𝐶 ∈ 𝑂)    &   ⊢ (𝜑 → 𝐽 ∈ ℤ)    ⇒   ⊢ (𝜑 → ((𝐹‘𝐶)‘𝐽) = ((♯‘((1...𝐽) ∩ 𝐶)) − (♯‘((1...𝐽) ∖ 𝐶))))
Theorem	ballotlemfelz 34668*	(𝐹‘𝐶) has values in ℤ. (Contributed by Thierry Arnoux, 23-Nov-2016.)
⊢ 𝑀 ∈ ℕ    &   ⊢ 𝑁 ∈ ℕ    &   ⊢ 𝑂 = {𝑐 ∈ 𝒫 (1...(𝑀 + 𝑁)) ∣ (♯‘𝑐) = 𝑀}    &   ⊢ 𝑃 = (𝑥 ∈ 𝒫 𝑂 ↦ ((♯‘𝑥) / (♯‘𝑂)))    &   ⊢ 𝐹 = (𝑐 ∈ 𝑂 ↦ (𝑖 ∈ ℤ ↦ ((♯‘((1...𝑖) ∩ 𝑐)) − (♯‘((1...𝑖) ∖ 𝑐)))))    &   ⊢ (𝜑 → 𝐶 ∈ 𝑂)    &   ⊢ (𝜑 → 𝐽 ∈ ℤ)    ⇒   ⊢ (𝜑 → ((𝐹‘𝐶)‘𝐽) ∈ ℤ)
Theorem	ballotlemfp1 34669*	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 34670*	𝐹 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 34671*	𝐹 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 34672*	(𝐹‘𝐶) finishes counting at (𝑀 − 𝑁). (Contributed by Thierry Arnoux, 25-Nov-2016.)
⊢ 𝑀 ∈ ℕ    &   ⊢ 𝑁 ∈ ℕ    &   ⊢ 𝑂 = {𝑐 ∈ 𝒫 (1...(𝑀 + 𝑁)) ∣ (♯‘𝑐) = 𝑀}    &   ⊢ 𝑃 = (𝑥 ∈ 𝒫 𝑂 ↦ ((♯‘𝑥) / (♯‘𝑂)))    &   ⊢ 𝐹 = (𝑐 ∈ 𝑂 ↦ (𝑖 ∈ ℤ ↦ ((♯‘((1...𝑖) ∩ 𝑐)) − (♯‘((1...𝑖) ∖ 𝑐)))))    ⇒   ⊢ (𝐶 ∈ 𝑂 → ((𝐹‘𝐶)‘(𝑀 + 𝑁)) = (𝑀 − 𝑁))
Theorem	ballotlemfval0 34673*	(𝐹‘𝐶) always starts counting at 0 . (Contributed by Thierry Arnoux, 25-Nov-2016.)
⊢ 𝑀 ∈ ℕ    &   ⊢ 𝑁 ∈ ℕ    &   ⊢ 𝑂 = {𝑐 ∈ 𝒫 (1...(𝑀 + 𝑁)) ∣ (♯‘𝑐) = 𝑀}    &   ⊢ 𝑃 = (𝑥 ∈ 𝒫 𝑂 ↦ ((♯‘𝑥) / (♯‘𝑂)))    &   ⊢ 𝐹 = (𝑐 ∈ 𝑂 ↦ (𝑖 ∈ ℤ ↦ ((♯‘((1...𝑖) ∩ 𝑐)) − (♯‘((1...𝑖) ∖ 𝑐)))))    ⇒   ⊢ (𝐶 ∈ 𝑂 → ((𝐹‘𝐶)‘0) = 0)
Theorem	ballotleme 34674*	Elements of 𝐸. (Contributed by Thierry Arnoux, 14-Dec-2016.)
⊢ 𝑀 ∈ ℕ    &   ⊢ 𝑁 ∈ ℕ    &   ⊢ 𝑂 = {𝑐 ∈ 𝒫 (1...(𝑀 + 𝑁)) ∣ (♯‘𝑐) = 𝑀}    &   ⊢ 𝑃 = (𝑥 ∈ 𝒫 𝑂 ↦ ((♯‘𝑥) / (♯‘𝑂)))    &   ⊢ 𝐹 = (𝑐 ∈ 𝑂 ↦ (𝑖 ∈ ℤ ↦ ((♯‘((1...𝑖) ∩ 𝑐)) − (♯‘((1...𝑖) ∖ 𝑐)))))    &   ⊢ 𝐸 = {𝑐 ∈ 𝑂 ∣ ∀𝑖 ∈ (1...(𝑀 + 𝑁))0 < ((𝐹‘𝑐)‘𝑖)}    ⇒   ⊢ (𝐶 ∈ 𝐸 ↔ (𝐶 ∈ 𝑂 ∧ ∀𝑖 ∈ (1...(𝑀 + 𝑁))0 < ((𝐹‘𝐶)‘𝑖)))
Theorem	ballotlemodife 34675*	Elements of (𝑂 ∖ 𝐸). (Contributed by Thierry Arnoux, 7-Dec-2016.)
⊢ 𝑀 ∈ ℕ    &   ⊢ 𝑁 ∈ ℕ    &   ⊢ 𝑂 = {𝑐 ∈ 𝒫 (1...(𝑀 + 𝑁)) ∣ (♯‘𝑐) = 𝑀}    &   ⊢ 𝑃 = (𝑥 ∈ 𝒫 𝑂 ↦ ((♯‘𝑥) / (♯‘𝑂)))    &   ⊢ 𝐹 = (𝑐 ∈ 𝑂 ↦ (𝑖 ∈ ℤ ↦ ((♯‘((1...𝑖) ∩ 𝑐)) − (♯‘((1...𝑖) ∖ 𝑐)))))    &   ⊢ 𝐸 = {𝑐 ∈ 𝑂 ∣ ∀𝑖 ∈ (1...(𝑀 + 𝑁))0 < ((𝐹‘𝑐)‘𝑖)}    ⇒   ⊢ (𝐶 ∈ (𝑂 ∖ 𝐸) ↔ (𝐶 ∈ 𝑂 ∧ ∃𝑖 ∈ (1...(𝑀 + 𝑁))((𝐹‘𝐶)‘𝑖) ≤ 0))
Theorem	ballotlem4 34676*	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 34677*	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 34678*	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 34679*	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 34680*	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 34681*	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 34682*	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 34683*	(𝐼‘𝐶) 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 34684*	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 34685*	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 34686*	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 34687*	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 34688*	𝑆 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 34689*	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 34690*	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 34691*	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 34692*	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 34693*	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 34694*	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 34695*	Value of 𝑅. (Contributed by Thierry Arnoux, 14-Apr-2017.)
⊢ 𝑀 ∈ ℕ    &   ⊢ 𝑁 ∈ ℕ    &   ⊢ 𝑂 = {𝑐 ∈ 𝒫 (1...(𝑀 + 𝑁)) ∣ (♯‘𝑐) = 𝑀}    &   ⊢ 𝑃 = (𝑥 ∈ 𝒫 𝑂 ↦ ((♯‘𝑥) / (♯‘𝑂)))    &   ⊢ 𝐹 = (𝑐 ∈ 𝑂 ↦ (𝑖 ∈ ℤ ↦ ((♯‘((1...𝑖) ∩ 𝑐)) − (♯‘((1...𝑖) ∖ 𝑐)))))    &   ⊢ 𝐸 = {𝑐 ∈ 𝑂 ∣ ∀𝑖 ∈ (1...(𝑀 + 𝑁))0 < ((𝐹‘𝑐)‘𝑖)}    &   ⊢ 𝑁 < 𝑀    &   ⊢ 𝐼 = (𝑐 ∈ (𝑂 ∖ 𝐸) ↦ inf({𝑘 ∈ (1...(𝑀 + 𝑁)) ∣ ((𝐹‘𝑐)‘𝑘) = 0}, ℝ, < ))    &   ⊢ 𝑆 = (𝑐 ∈ (𝑂 ∖ 𝐸) ↦ (𝑖 ∈ (1...(𝑀 + 𝑁)) ↦ if(𝑖 ≤ (𝐼‘𝑐), (((𝐼‘𝑐) + 1) − 𝑖), 𝑖)))    &   ⊢ 𝑅 = (𝑐 ∈ (𝑂 ∖ 𝐸) ↦ ((𝑆‘𝑐) “ 𝑐))    ⇒   ⊢ (𝐶 ∈ (𝑂 ∖ 𝐸) → (𝑅‘𝐶) = ((𝑆‘𝐶) “ 𝐶))
Theorem	ballotlemscr 34696*	The image of (𝑅‘𝐶) by (𝑆‘𝐶). (Contributed by Thierry Arnoux, 21-Apr-2017.)
⊢ 𝑀 ∈ ℕ    &   ⊢ 𝑁 ∈ ℕ    &   ⊢ 𝑂 = {𝑐 ∈ 𝒫 (1...(𝑀 + 𝑁)) ∣ (♯‘𝑐) = 𝑀}    &   ⊢ 𝑃 = (𝑥 ∈ 𝒫 𝑂 ↦ ((♯‘𝑥) / (♯‘𝑂)))    &   ⊢ 𝐹 = (𝑐 ∈ 𝑂 ↦ (𝑖 ∈ ℤ ↦ ((♯‘((1...𝑖) ∩ 𝑐)) − (♯‘((1...𝑖) ∖ 𝑐)))))    &   ⊢ 𝐸 = {𝑐 ∈ 𝑂 ∣ ∀𝑖 ∈ (1...(𝑀 + 𝑁))0 < ((𝐹‘𝑐)‘𝑖)}    &   ⊢ 𝑁 < 𝑀    &   ⊢ 𝐼 = (𝑐 ∈ (𝑂 ∖ 𝐸) ↦ inf({𝑘 ∈ (1...(𝑀 + 𝑁)) ∣ ((𝐹‘𝑐)‘𝑘) = 0}, ℝ, < ))    &   ⊢ 𝑆 = (𝑐 ∈ (𝑂 ∖ 𝐸) ↦ (𝑖 ∈ (1...(𝑀 + 𝑁)) ↦ if(𝑖 ≤ (𝐼‘𝑐), (((𝐼‘𝑐) + 1) − 𝑖), 𝑖)))    &   ⊢ 𝑅 = (𝑐 ∈ (𝑂 ∖ 𝐸) ↦ ((𝑆‘𝑐) “ 𝑐))    ⇒   ⊢ (𝐶 ∈ (𝑂 ∖ 𝐸) → ((𝑆‘𝐶) “ (𝑅‘𝐶)) = 𝐶)
Theorem	ballotlemrv 34697*	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 34698*	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 34699*	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 34700*	Range of 𝑅 is included in 𝑂. (Contributed by Thierry Arnoux, 17-Apr-2017.)
⊢ 𝑀 ∈ ℕ    &   ⊢ 𝑁 ∈ ℕ    &   ⊢ 𝑂 = {𝑐 ∈ 𝒫 (1...(𝑀 + 𝑁)) ∣ (♯‘𝑐) = 𝑀}    &   ⊢ 𝑃 = (𝑥 ∈ 𝒫 𝑂 ↦ ((♯‘𝑥) / (♯‘𝑂)))    &   ⊢ 𝐹 = (𝑐 ∈ 𝑂 ↦ (𝑖 ∈ ℤ ↦ ((♯‘((1...𝑖) ∩ 𝑐)) − (♯‘((1...𝑖) ∖ 𝑐)))))    &   ⊢ 𝐸 = {𝑐 ∈ 𝑂 ∣ ∀𝑖 ∈ (1...(𝑀 + 𝑁))0 < ((𝐹‘𝑐)‘𝑖)}    &   ⊢ 𝑁 < 𝑀    &   ⊢ 𝐼 = (𝑐 ∈ (𝑂 ∖ 𝐸) ↦ inf({𝑘 ∈ (1...(𝑀 + 𝑁)) ∣ ((𝐹‘𝑐)‘𝑘) = 0}, ℝ, < ))    &   ⊢ 𝑆 = (𝑐 ∈ (𝑂 ∖ 𝐸) ↦ (𝑖 ∈ (1...(𝑀 + 𝑁)) ↦ if(𝑖 ≤ (𝐼‘𝑐), (((𝐼‘𝑐) + 1) − 𝑖), 𝑖)))    &   ⊢ 𝑅 = (𝑐 ∈ (𝑂 ∖ 𝐸) ↦ ((𝑆‘𝑐) “ 𝑐))    ⇒   ⊢ (𝐶 ∈ (𝑂 ∖ 𝐸) → (𝑅‘𝐶) ∈ 𝑂)