Home | Metamath
Proof Explorer Theorem List (p. 318 of 450) | < Previous Next > |
Bad symbols? Try the
GIF version. |
||
Mirrors > Metamath Home Page > MPE Home Page > Theorem List Contents > Recent Proofs This page: Page List |
Color key: | Metamath Proof Explorer
(1-28695) |
Hilbert Space Explorer
(28696-30218) |
Users' Mathboxes
(30219-44955) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | isrrvv 31701* | 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 31702 | A real-valued random variable is a function. (Contributed by Thierry Arnoux, 25-Jan-2017.) |
⊢ (𝜑 → 𝑃 ∈ Prob) & ⊢ (𝜑 → 𝑋 ∈ (rRndVar‘𝑃)) ⇒ ⊢ (𝜑 → 𝑋:∪ dom 𝑃⟶ℝ) | ||
Theorem | rrvfn 31703 | A real-valued random variable is a function over the universe. (Contributed by Thierry Arnoux, 25-Jan-2017.) |
⊢ (𝜑 → 𝑃 ∈ Prob) & ⊢ (𝜑 → 𝑋 ∈ (rRndVar‘𝑃)) ⇒ ⊢ (𝜑 → 𝑋 Fn ∪ dom 𝑃) | ||
Theorem | rrvdm 31704 | The domain of a random variable is the universe. (Contributed by Thierry Arnoux, 25-Jan-2017.) |
⊢ (𝜑 → 𝑃 ∈ Prob) & ⊢ (𝜑 → 𝑋 ∈ (rRndVar‘𝑃)) ⇒ ⊢ (𝜑 → dom 𝑋 = ∪ dom 𝑃) | ||
Theorem | rrvrnss 31705 | The range of a random variable as a subset of ℝ. (Contributed by Thierry Arnoux, 6-Feb-2017.) |
⊢ (𝜑 → 𝑃 ∈ Prob) & ⊢ (𝜑 → 𝑋 ∈ (rRndVar‘𝑃)) ⇒ ⊢ (𝜑 → ran 𝑋 ⊆ ℝ) | ||
Theorem | rrvf2 31706 | A real-valued random variable is a function. (Contributed by Thierry Arnoux, 25-Jan-2017.) |
⊢ (𝜑 → 𝑃 ∈ Prob) & ⊢ (𝜑 → 𝑋 ∈ (rRndVar‘𝑃)) ⇒ ⊢ (𝜑 → 𝑋:dom 𝑋⟶ℝ) | ||
Theorem | rrvdmss 31707 | 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 31708* | 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 31709* | 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 31710 | The sum of two random variables is a random variable. (Contributed by Thierry Arnoux, 4-Jun-2017.) |
⊢ (𝜑 → 𝑃 ∈ Prob) & ⊢ (𝜑 → 𝑋 ∈ (rRndVar‘𝑃)) & ⊢ (𝜑 → 𝑌 ∈ (rRndVar‘𝑃)) ⇒ ⊢ (𝜑 → (𝑋 ∘f + 𝑌) ∈ (rRndVar‘𝑃)) | ||
Theorem | rrvmulc 31711 | 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 31712 | An indexed sum of random variables is a random variable. (Contributed by Thierry Arnoux, 22-May-2017.) |
⊢ (𝜑 → 𝑃 ∈ Prob) & ⊢ (𝜑 → 𝑋:ℕ⟶(rRndVar‘𝑃)) & ⊢ ((𝜑 ∧ 𝑁 ∈ ℕ) → 𝑆 = (seq1( ∘f + , 𝑋)‘𝑁)) ⇒ ⊢ ((𝜑 ∧ 𝑁 ∈ ℕ) → 𝑆 ∈ (rRndVar‘𝑃)) | ||
Syntax | corvc 31713 | Extend class notation to include the preimage set mapping operator. |
class ∘RV/𝑐𝑅 | ||
Definition | df-orvc 31714* |
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 5723- elementhood: {𝑋 ∈ 𝐴} as (𝑋∘RV/𝑐 E 𝐴) cf. epel 5469- 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 31715* | 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 31716* | Another way to express the value of the preimage mapping operator. (Contributed by Thierry Arnoux, 19-Jan-2017.) |
⊢ (𝜑 → Fun 𝑋) & ⊢ (𝜑 → 𝑋 ∈ 𝑉) & ⊢ (𝜑 → 𝐴 ∈ 𝑊) ⇒ ⊢ (𝜑 → (𝑋∘RV/𝑐𝑅𝐴) = {𝑧 ∈ dom 𝑋 ∣ (𝑋‘𝑧)𝑅𝐴}) | ||
Theorem | elorvc 31717* | Elementhood of a preimage. (Contributed by Thierry Arnoux, 21-Jan-2017.) |
⊢ (𝜑 → Fun 𝑋) & ⊢ (𝜑 → 𝑋 ∈ 𝑉) & ⊢ (𝜑 → 𝐴 ∈ 𝑊) ⇒ ⊢ ((𝜑 ∧ 𝑧 ∈ dom 𝑋) → (𝑧 ∈ (𝑋∘RV/𝑐𝑅𝐴) ↔ (𝑋‘𝑧)𝑅𝐴)) | ||
Theorem | orvcval4 31718* | The value of the preimage mapping operator can be restricted to preimages in the base set of the topology. Cf. orvcval 31715. (Contributed by Thierry Arnoux, 21-Jan-2017.) |
⊢ (𝜑 → 𝑆 ∈ ∪ ran sigAlgebra) & ⊢ (𝜑 → 𝐽 ∈ Top) & ⊢ (𝜑 → 𝑋 ∈ (𝑆MblFnM(sigaGen‘𝐽))) & ⊢ (𝜑 → 𝐴 ∈ 𝑉) ⇒ ⊢ (𝜑 → (𝑋∘RV/𝑐𝑅𝐴) = (◡𝑋 “ {𝑦 ∈ ∪ 𝐽 ∣ 𝑦𝑅𝐴})) | ||
Theorem | orvcoel 31719* | 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 31720* | 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 31721* | Elementhood of a preimage for a real-valued random variable. (Contributed by Thierry Arnoux, 21-Jan-2017.) |
⊢ (𝜑 → 𝑃 ∈ Prob) & ⊢ (𝜑 → 𝑋 ∈ (rRndVar‘𝑃)) & ⊢ (𝜑 → 𝐴 ∈ 𝑉) ⇒ ⊢ ((𝜑 ∧ 𝑧 ∈ ∪ dom 𝑃) → (𝑧 ∈ (𝑋∘RV/𝑐𝑅𝐴) ↔ (𝑋‘𝑧)𝑅𝐴)) | ||
Theorem | orrvcval4 31722* | The value of the preimage mapping operator can be restricted to preimages of subsets of RR. (Contributed by Thierry Arnoux, 21-Jan-2017.) |
⊢ (𝜑 → 𝑃 ∈ Prob) & ⊢ (𝜑 → 𝑋 ∈ (rRndVar‘𝑃)) & ⊢ (𝜑 → 𝐴 ∈ 𝑉) ⇒ ⊢ (𝜑 → (𝑋∘RV/𝑐𝑅𝐴) = (◡𝑋 “ {𝑦 ∈ ℝ ∣ 𝑦𝑅𝐴})) | ||
Theorem | orrvcoel 31723* | 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 31724* | 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 31725 | 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 𝑃) | ||
Theorem | orvcelval 31726 | Preimage maps produced by the membership relation. (Contributed by Thierry Arnoux, 6-Feb-2017.) |
⊢ (𝜑 → 𝑃 ∈ Prob) & ⊢ (𝜑 → 𝑋 ∈ (rRndVar‘𝑃)) & ⊢ (𝜑 → 𝐴 ∈ 𝔅ℝ) ⇒ ⊢ (𝜑 → (𝑋∘RV/𝑐 E 𝐴) = (◡𝑋 “ 𝐴)) | ||
Theorem | orvcelel 31727 | Preimage maps produced by the membership relation are measurable sets. (Contributed by Thierry Arnoux, 5-Feb-2017.) |
⊢ (𝜑 → 𝑃 ∈ Prob) & ⊢ (𝜑 → 𝑋 ∈ (rRndVar‘𝑃)) & ⊢ (𝜑 → 𝐴 ∈ 𝔅ℝ) ⇒ ⊢ (𝜑 → (𝑋∘RV/𝑐 E 𝐴) ∈ dom 𝑃) | ||
Theorem | dstrvval 31728* | The value of the distribution of a random variable. (Contributed by Thierry Arnoux, 9-Feb-2017.) |
⊢ (𝜑 → 𝑃 ∈ Prob) & ⊢ (𝜑 → 𝑋 ∈ (rRndVar‘𝑃)) & ⊢ (𝜑 → 𝐷 = (𝑎 ∈ 𝔅ℝ ↦ (𝑃‘(𝑋∘RV/𝑐 E 𝑎)))) & ⊢ (𝜑 → 𝐴 ∈ 𝔅ℝ) ⇒ ⊢ (𝜑 → (𝐷‘𝐴) = (𝑃‘(◡𝑋 “ 𝐴))) | ||
Theorem | dstrvprob 31729* | The distribution of a random variable is a probability law. (TODO: could be shortened using dstrvval 31728) (Contributed by Thierry Arnoux, 10-Feb-2017.) |
⊢ (𝜑 → 𝑃 ∈ Prob) & ⊢ (𝜑 → 𝑋 ∈ (rRndVar‘𝑃)) & ⊢ (𝜑 → 𝐷 = (𝑎 ∈ 𝔅ℝ ↦ (𝑃‘(𝑋∘RV/𝑐 E 𝑎)))) ⇒ ⊢ (𝜑 → 𝐷 ∈ Prob) | ||
Theorem | orvclteel 31730 | 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 31731 | 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 31732* | 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 31733 | 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 31734* | A cumulative distribution function is nondecreasing. (Contributed by Thierry Arnoux, 11-Feb-2017.) |
⊢ (𝜑 → 𝑃 ∈ Prob) & ⊢ (𝜑 → 𝑋 ∈ (rRndVar‘𝑃)) & ⊢ (𝜑 → 𝐹 = (𝑥 ∈ ℝ ↦ (𝑃‘(𝑋∘RV/𝑐 ≤ 𝑥)))) & ⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 𝐴 ≤ 𝐵) ⇒ ⊢ (𝜑 → (𝐹‘𝐴) ≤ (𝐹‘𝐵)) | ||
Theorem | dstfrvclim1 31735* | 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) | ||
Theorem | coinfliplem 31736 | 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 31737 | 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 31738 | The space of our coin-flip probability. (Contributed by Thierry Arnoux, 15-Jan-2017.) |
⊢ 𝐻 ∈ V & ⊢ 𝑇 ∈ V & ⊢ 𝐻 ≠ 𝑇 & ⊢ 𝑃 = ((♯ ↾ 𝒫 {𝐻, 𝑇}) ∘f/c / 2) & ⊢ 𝑋 = {〈𝐻, 1〉, 〈𝑇, 0〉} ⇒ ⊢ dom 𝑃 = 𝒫 {𝐻, 𝑇} | ||
Theorem | coinflipuniv 31739 | 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 31740 | 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 31741 | 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 31742 | The probability of tails is one-half. (Contributed by Thierry Arnoux, 5-Feb-2017.) |
⊢ 𝐻 ∈ V & ⊢ 𝑇 ∈ V & ⊢ 𝐻 ≠ 𝑇 & ⊢ 𝑃 = ((♯ ↾ 𝒫 {𝐻, 𝑇}) ∘f/c / 2) & ⊢ 𝑋 = {〈𝐻, 1〉, 〈𝑇, 0〉} ⇒ ⊢ (𝑃‘{𝑇}) = (1 / 2) | ||
Theorem | ballotlemoex 31743* | 𝑂 is a set. (Contributed by Thierry Arnoux, 7-Dec-2016.) |
⊢ 𝑀 ∈ ℕ & ⊢ 𝑁 ∈ ℕ & ⊢ 𝑂 = {𝑐 ∈ 𝒫 (1...(𝑀 + 𝑁)) ∣ (♯‘𝑐) = 𝑀} ⇒ ⊢ 𝑂 ∈ V | ||
Theorem | ballotlem1 31744* | The size of the universe is a binomial coefficient. (Contributed by Thierry Arnoux, 23-Nov-2016.) |
⊢ 𝑀 ∈ ℕ & ⊢ 𝑁 ∈ ℕ & ⊢ 𝑂 = {𝑐 ∈ 𝒫 (1...(𝑀 + 𝑁)) ∣ (♯‘𝑐) = 𝑀} ⇒ ⊢ (♯‘𝑂) = ((𝑀 + 𝑁)C𝑀) | ||
Theorem | ballotlemelo 31745* | Elementhood in 𝑂. (Contributed by Thierry Arnoux, 17-Apr-2017.) |
⊢ 𝑀 ∈ ℕ & ⊢ 𝑁 ∈ ℕ & ⊢ 𝑂 = {𝑐 ∈ 𝒫 (1...(𝑀 + 𝑁)) ∣ (♯‘𝑐) = 𝑀} ⇒ ⊢ (𝐶 ∈ 𝑂 ↔ (𝐶 ⊆ (1...(𝑀 + 𝑁)) ∧ (♯‘𝐶) = 𝑀)) | ||
Theorem | ballotlem2 31746* | The probability that the first vote picked in a count is a B. (Contributed by Thierry Arnoux, 23-Nov-2016.) |
⊢ 𝑀 ∈ ℕ & ⊢ 𝑁 ∈ ℕ & ⊢ 𝑂 = {𝑐 ∈ 𝒫 (1...(𝑀 + 𝑁)) ∣ (♯‘𝑐) = 𝑀} & ⊢ 𝑃 = (𝑥 ∈ 𝒫 𝑂 ↦ ((♯‘𝑥) / (♯‘𝑂))) ⇒ ⊢ (𝑃‘{𝑐 ∈ 𝑂 ∣ ¬ 1 ∈ 𝑐}) = (𝑁 / (𝑀 + 𝑁)) | ||
Theorem | ballotlemfval 31747* | The value of F. (Contributed by Thierry Arnoux, 23-Nov-2016.) |
⊢ 𝑀 ∈ ℕ & ⊢ 𝑁 ∈ ℕ & ⊢ 𝑂 = {𝑐 ∈ 𝒫 (1...(𝑀 + 𝑁)) ∣ (♯‘𝑐) = 𝑀} & ⊢ 𝑃 = (𝑥 ∈ 𝒫 𝑂 ↦ ((♯‘𝑥) / (♯‘𝑂))) & ⊢ 𝐹 = (𝑐 ∈ 𝑂 ↦ (𝑖 ∈ ℤ ↦ ((♯‘((1...𝑖) ∩ 𝑐)) − (♯‘((1...𝑖) ∖ 𝑐))))) & ⊢ (𝜑 → 𝐶 ∈ 𝑂) & ⊢ (𝜑 → 𝐽 ∈ ℤ) ⇒ ⊢ (𝜑 → ((𝐹‘𝐶)‘𝐽) = ((♯‘((1...𝐽) ∩ 𝐶)) − (♯‘((1...𝐽) ∖ 𝐶)))) | ||
Theorem | ballotlemfelz 31748* | (𝐹‘𝐶) has values in ℤ. (Contributed by Thierry Arnoux, 23-Nov-2016.) |
⊢ 𝑀 ∈ ℕ & ⊢ 𝑁 ∈ ℕ & ⊢ 𝑂 = {𝑐 ∈ 𝒫 (1...(𝑀 + 𝑁)) ∣ (♯‘𝑐) = 𝑀} & ⊢ 𝑃 = (𝑥 ∈ 𝒫 𝑂 ↦ ((♯‘𝑥) / (♯‘𝑂))) & ⊢ 𝐹 = (𝑐 ∈ 𝑂 ↦ (𝑖 ∈ ℤ ↦ ((♯‘((1...𝑖) ∩ 𝑐)) − (♯‘((1...𝑖) ∖ 𝑐))))) & ⊢ (𝜑 → 𝐶 ∈ 𝑂) & ⊢ (𝜑 → 𝐽 ∈ ℤ) ⇒ ⊢ (𝜑 → ((𝐹‘𝐶)‘𝐽) ∈ ℤ) | ||
Theorem | ballotlemfp1 31749* | 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 31750* | 𝐹 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 31751* | 𝐹 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 31752* | (𝐹‘𝐶) finishes counting at (𝑀 − 𝑁). (Contributed by Thierry Arnoux, 25-Nov-2016.) |
⊢ 𝑀 ∈ ℕ & ⊢ 𝑁 ∈ ℕ & ⊢ 𝑂 = {𝑐 ∈ 𝒫 (1...(𝑀 + 𝑁)) ∣ (♯‘𝑐) = 𝑀} & ⊢ 𝑃 = (𝑥 ∈ 𝒫 𝑂 ↦ ((♯‘𝑥) / (♯‘𝑂))) & ⊢ 𝐹 = (𝑐 ∈ 𝑂 ↦ (𝑖 ∈ ℤ ↦ ((♯‘((1...𝑖) ∩ 𝑐)) − (♯‘((1...𝑖) ∖ 𝑐))))) ⇒ ⊢ (𝐶 ∈ 𝑂 → ((𝐹‘𝐶)‘(𝑀 + 𝑁)) = (𝑀 − 𝑁)) | ||
Theorem | ballotlemfval0 31753* | (𝐹‘𝐶) always starts counting at 0 . (Contributed by Thierry Arnoux, 25-Nov-2016.) |
⊢ 𝑀 ∈ ℕ & ⊢ 𝑁 ∈ ℕ & ⊢ 𝑂 = {𝑐 ∈ 𝒫 (1...(𝑀 + 𝑁)) ∣ (♯‘𝑐) = 𝑀} & ⊢ 𝑃 = (𝑥 ∈ 𝒫 𝑂 ↦ ((♯‘𝑥) / (♯‘𝑂))) & ⊢ 𝐹 = (𝑐 ∈ 𝑂 ↦ (𝑖 ∈ ℤ ↦ ((♯‘((1...𝑖) ∩ 𝑐)) − (♯‘((1...𝑖) ∖ 𝑐))))) ⇒ ⊢ (𝐶 ∈ 𝑂 → ((𝐹‘𝐶)‘0) = 0) | ||
Theorem | ballotleme 31754* | Elements of 𝐸. (Contributed by Thierry Arnoux, 14-Dec-2016.) |
⊢ 𝑀 ∈ ℕ & ⊢ 𝑁 ∈ ℕ & ⊢ 𝑂 = {𝑐 ∈ 𝒫 (1...(𝑀 + 𝑁)) ∣ (♯‘𝑐) = 𝑀} & ⊢ 𝑃 = (𝑥 ∈ 𝒫 𝑂 ↦ ((♯‘𝑥) / (♯‘𝑂))) & ⊢ 𝐹 = (𝑐 ∈ 𝑂 ↦ (𝑖 ∈ ℤ ↦ ((♯‘((1...𝑖) ∩ 𝑐)) − (♯‘((1...𝑖) ∖ 𝑐))))) & ⊢ 𝐸 = {𝑐 ∈ 𝑂 ∣ ∀𝑖 ∈ (1...(𝑀 + 𝑁))0 < ((𝐹‘𝑐)‘𝑖)} ⇒ ⊢ (𝐶 ∈ 𝐸 ↔ (𝐶 ∈ 𝑂 ∧ ∀𝑖 ∈ (1...(𝑀 + 𝑁))0 < ((𝐹‘𝐶)‘𝑖))) | ||
Theorem | ballotlemodife 31755* | Elements of (𝑂 ∖ 𝐸). (Contributed by Thierry Arnoux, 7-Dec-2016.) |
⊢ 𝑀 ∈ ℕ & ⊢ 𝑁 ∈ ℕ & ⊢ 𝑂 = {𝑐 ∈ 𝒫 (1...(𝑀 + 𝑁)) ∣ (♯‘𝑐) = 𝑀} & ⊢ 𝑃 = (𝑥 ∈ 𝒫 𝑂 ↦ ((♯‘𝑥) / (♯‘𝑂))) & ⊢ 𝐹 = (𝑐 ∈ 𝑂 ↦ (𝑖 ∈ ℤ ↦ ((♯‘((1...𝑖) ∩ 𝑐)) − (♯‘((1...𝑖) ∖ 𝑐))))) & ⊢ 𝐸 = {𝑐 ∈ 𝑂 ∣ ∀𝑖 ∈ (1...(𝑀 + 𝑁))0 < ((𝐹‘𝑐)‘𝑖)} ⇒ ⊢ (𝐶 ∈ (𝑂 ∖ 𝐸) ↔ (𝐶 ∈ 𝑂 ∧ ∃𝑖 ∈ (1...(𝑀 + 𝑁))((𝐹‘𝐶)‘𝑖) ≤ 0)) | ||
Theorem | ballotlem4 31756* | 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 31757* | 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 31758* | 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 31759* | 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 31760* | 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 31761* | 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 31762* | 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 31763* | (𝐼‘𝐶) 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 31764* | 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 31765* | 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 31766* | 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 31767* | 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 31768* | 𝑆 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 31769* | 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 31770* | 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 31771* | 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 31772* | 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 31773* | 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 31774* | 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 31775* | Value of 𝑅. (Contributed by Thierry Arnoux, 14-Apr-2017.) |
⊢ 𝑀 ∈ ℕ & ⊢ 𝑁 ∈ ℕ & ⊢ 𝑂 = {𝑐 ∈ 𝒫 (1...(𝑀 + 𝑁)) ∣ (♯‘𝑐) = 𝑀} & ⊢ 𝑃 = (𝑥 ∈ 𝒫 𝑂 ↦ ((♯‘𝑥) / (♯‘𝑂))) & ⊢ 𝐹 = (𝑐 ∈ 𝑂 ↦ (𝑖 ∈ ℤ ↦ ((♯‘((1...𝑖) ∩ 𝑐)) − (♯‘((1...𝑖) ∖ 𝑐))))) & ⊢ 𝐸 = {𝑐 ∈ 𝑂 ∣ ∀𝑖 ∈ (1...(𝑀 + 𝑁))0 < ((𝐹‘𝑐)‘𝑖)} & ⊢ 𝑁 < 𝑀 & ⊢ 𝐼 = (𝑐 ∈ (𝑂 ∖ 𝐸) ↦ inf({𝑘 ∈ (1...(𝑀 + 𝑁)) ∣ ((𝐹‘𝑐)‘𝑘) = 0}, ℝ, < )) & ⊢ 𝑆 = (𝑐 ∈ (𝑂 ∖ 𝐸) ↦ (𝑖 ∈ (1...(𝑀 + 𝑁)) ↦ if(𝑖 ≤ (𝐼‘𝑐), (((𝐼‘𝑐) + 1) − 𝑖), 𝑖))) & ⊢ 𝑅 = (𝑐 ∈ (𝑂 ∖ 𝐸) ↦ ((𝑆‘𝑐) “ 𝑐)) ⇒ ⊢ (𝐶 ∈ (𝑂 ∖ 𝐸) → (𝑅‘𝐶) = ((𝑆‘𝐶) “ 𝐶)) | ||
Theorem | ballotlemscr 31776* | The image of (𝑅‘𝐶) by (𝑆‘𝐶). (Contributed by Thierry Arnoux, 21-Apr-2017.) |
⊢ 𝑀 ∈ ℕ & ⊢ 𝑁 ∈ ℕ & ⊢ 𝑂 = {𝑐 ∈ 𝒫 (1...(𝑀 + 𝑁)) ∣ (♯‘𝑐) = 𝑀} & ⊢ 𝑃 = (𝑥 ∈ 𝒫 𝑂 ↦ ((♯‘𝑥) / (♯‘𝑂))) & ⊢ 𝐹 = (𝑐 ∈ 𝑂 ↦ (𝑖 ∈ ℤ ↦ ((♯‘((1...𝑖) ∩ 𝑐)) − (♯‘((1...𝑖) ∖ 𝑐))))) & ⊢ 𝐸 = {𝑐 ∈ 𝑂 ∣ ∀𝑖 ∈ (1...(𝑀 + 𝑁))0 < ((𝐹‘𝑐)‘𝑖)} & ⊢ 𝑁 < 𝑀 & ⊢ 𝐼 = (𝑐 ∈ (𝑂 ∖ 𝐸) ↦ inf({𝑘 ∈ (1...(𝑀 + 𝑁)) ∣ ((𝐹‘𝑐)‘𝑘) = 0}, ℝ, < )) & ⊢ 𝑆 = (𝑐 ∈ (𝑂 ∖ 𝐸) ↦ (𝑖 ∈ (1...(𝑀 + 𝑁)) ↦ if(𝑖 ≤ (𝐼‘𝑐), (((𝐼‘𝑐) + 1) − 𝑖), 𝑖))) & ⊢ 𝑅 = (𝑐 ∈ (𝑂 ∖ 𝐸) ↦ ((𝑆‘𝑐) “ 𝑐)) ⇒ ⊢ (𝐶 ∈ (𝑂 ∖ 𝐸) → ((𝑆‘𝐶) “ (𝑅‘𝐶)) = 𝐶) | ||
Theorem | ballotlemrv 31777* | 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 31778* | 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 31779* | 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 31780* | 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 31781* | 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 31782* | 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 31783* | 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 31784* | 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 31785* | 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 31786* | 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 31787* | 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 31788* | Range of 𝑅. (Contributed by Thierry Arnoux, 19-Apr-2017.) |
⊢ 𝑀 ∈ ℕ & ⊢ 𝑁 ∈ ℕ & ⊢ 𝑂 = {𝑐 ∈ 𝒫 (1...(𝑀 + 𝑁)) ∣ (♯‘𝑐) = 𝑀} & ⊢ 𝑃 = (𝑥 ∈ 𝒫 𝑂 ↦ ((♯‘𝑥) / (♯‘𝑂))) & ⊢ 𝐹 = (𝑐 ∈ 𝑂 ↦ (𝑖 ∈ ℤ ↦ ((♯‘((1...𝑖) ∩ 𝑐)) − (♯‘((1...𝑖) ∖ 𝑐))))) & ⊢ 𝐸 = {𝑐 ∈ 𝑂 ∣ ∀𝑖 ∈ (1...(𝑀 + 𝑁))0 < ((𝐹‘𝑐)‘𝑖)} & ⊢ 𝑁 < 𝑀 & ⊢ 𝐼 = (𝑐 ∈ (𝑂 ∖ 𝐸) ↦ inf({𝑘 ∈ (1...(𝑀 + 𝑁)) ∣ ((𝐹‘𝑐)‘𝑘) = 0}, ℝ, < )) & ⊢ 𝑆 = (𝑐 ∈ (𝑂 ∖ 𝐸) ↦ (𝑖 ∈ (1...(𝑀 + 𝑁)) ↦ if(𝑖 ≤ (𝐼‘𝑐), (((𝐼‘𝑐) + 1) − 𝑖), 𝑖))) & ⊢ 𝑅 = (𝑐 ∈ (𝑂 ∖ 𝐸) ↦ ((𝑆‘𝑐) “ 𝑐)) ⇒ ⊢ (𝐶 ∈ (𝑂 ∖ 𝐸) → (𝑅‘𝐶) ∈ (𝑂 ∖ 𝐸)) | ||
Theorem | ballotlemirc 31789* | 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 31790* | Lemma for ballotlemrinv 31791. (Contributed by Thierry Arnoux, 18-Apr-2017.) |
⊢ 𝑀 ∈ ℕ & ⊢ 𝑁 ∈ ℕ & ⊢ 𝑂 = {𝑐 ∈ 𝒫 (1...(𝑀 + 𝑁)) ∣ (♯‘𝑐) = 𝑀} & ⊢ 𝑃 = (𝑥 ∈ 𝒫 𝑂 ↦ ((♯‘𝑥) / (♯‘𝑂))) & ⊢ 𝐹 = (𝑐 ∈ 𝑂 ↦ (𝑖 ∈ ℤ ↦ ((♯‘((1...𝑖) ∩ 𝑐)) − (♯‘((1...𝑖) ∖ 𝑐))))) & ⊢ 𝐸 = {𝑐 ∈ 𝑂 ∣ ∀𝑖 ∈ (1...(𝑀 + 𝑁))0 < ((𝐹‘𝑐)‘𝑖)} & ⊢ 𝑁 < 𝑀 & ⊢ 𝐼 = (𝑐 ∈ (𝑂 ∖ 𝐸) ↦ inf({𝑘 ∈ (1...(𝑀 + 𝑁)) ∣ ((𝐹‘𝑐)‘𝑘) = 0}, ℝ, < )) & ⊢ 𝑆 = (𝑐 ∈ (𝑂 ∖ 𝐸) ↦ (𝑖 ∈ (1...(𝑀 + 𝑁)) ↦ if(𝑖 ≤ (𝐼‘𝑐), (((𝐼‘𝑐) + 1) − 𝑖), 𝑖))) & ⊢ 𝑅 = (𝑐 ∈ (𝑂 ∖ 𝐸) ↦ ((𝑆‘𝑐) “ 𝑐)) ⇒ ⊢ ((𝐶 ∈ (𝑂 ∖ 𝐸) ∧ 𝐷 = ((𝑆‘𝐶) “ 𝐶)) → (𝐷 ∈ (𝑂 ∖ 𝐸) ∧ 𝐶 = ((𝑆‘𝐷) “ 𝐷))) | ||
Theorem | ballotlemrinv 31791* | 𝑅 is its own inverse : it is an involution. (Contributed by Thierry Arnoux, 10-Apr-2017.) |
⊢ 𝑀 ∈ ℕ & ⊢ 𝑁 ∈ ℕ & ⊢ 𝑂 = {𝑐 ∈ 𝒫 (1...(𝑀 + 𝑁)) ∣ (♯‘𝑐) = 𝑀} & ⊢ 𝑃 = (𝑥 ∈ 𝒫 𝑂 ↦ ((♯‘𝑥) / (♯‘𝑂))) & ⊢ 𝐹 = (𝑐 ∈ 𝑂 ↦ (𝑖 ∈ ℤ ↦ ((♯‘((1...𝑖) ∩ 𝑐)) − (♯‘((1...𝑖) ∖ 𝑐))))) & ⊢ 𝐸 = {𝑐 ∈ 𝑂 ∣ ∀𝑖 ∈ (1...(𝑀 + 𝑁))0 < ((𝐹‘𝑐)‘𝑖)} & ⊢ 𝑁 < 𝑀 & ⊢ 𝐼 = (𝑐 ∈ (𝑂 ∖ 𝐸) ↦ inf({𝑘 ∈ (1...(𝑀 + 𝑁)) ∣ ((𝐹‘𝑐)‘𝑘) = 0}, ℝ, < )) & ⊢ 𝑆 = (𝑐 ∈ (𝑂 ∖ 𝐸) ↦ (𝑖 ∈ (1...(𝑀 + 𝑁)) ↦ if(𝑖 ≤ (𝐼‘𝑐), (((𝐼‘𝑐) + 1) − 𝑖), 𝑖))) & ⊢ 𝑅 = (𝑐 ∈ (𝑂 ∖ 𝐸) ↦ ((𝑆‘𝑐) “ 𝑐)) ⇒ ⊢ ◡𝑅 = 𝑅 | ||
Theorem | ballotlem1ri 31792* | 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.) |
⊢ 𝑀 ∈ ℕ & ⊢ 𝑁 ∈ ℕ & ⊢ 𝑂 = {𝑐 ∈ 𝒫 (1...(𝑀 + 𝑁)) ∣ (♯‘𝑐) = 𝑀} & ⊢ 𝑃 = (𝑥 ∈ 𝒫 𝑂 ↦ ((♯‘𝑥) / (♯‘𝑂))) & ⊢ 𝐹 = (𝑐 ∈ 𝑂 ↦ (𝑖 ∈ ℤ ↦ ((♯‘((1...𝑖) ∩ 𝑐)) − (♯‘((1...𝑖) ∖ 𝑐))))) & ⊢ 𝐸 = {𝑐 ∈ 𝑂 ∣ ∀𝑖 ∈ (1...(𝑀 + 𝑁))0 < ((𝐹‘𝑐)‘𝑖)} & ⊢ 𝑁 < 𝑀 & ⊢ 𝐼 = (𝑐 ∈ (𝑂 ∖ 𝐸) ↦ inf({𝑘 ∈ (1...(𝑀 + 𝑁)) ∣ ((𝐹‘𝑐)‘𝑘) = 0}, ℝ, < )) & ⊢ 𝑆 = (𝑐 ∈ (𝑂 ∖ 𝐸) ↦ (𝑖 ∈ (1...(𝑀 + 𝑁)) ↦ if(𝑖 ≤ (𝐼‘𝑐), (((𝐼‘𝑐) + 1) − 𝑖), 𝑖))) & ⊢ 𝑅 = (𝑐 ∈ (𝑂 ∖ 𝐸) ↦ ((𝑆‘𝑐) “ 𝑐)) ⇒ ⊢ (𝐶 ∈ (𝑂 ∖ 𝐸) → (1 ∈ (𝑅‘𝐶) ↔ (𝐼‘𝐶) ∈ 𝐶)) | ||
Theorem | ballotlem7 31793* | 𝑅 is a bijection between two subsets of (𝑂 ∖ 𝐸): 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.) |
⊢ 𝑀 ∈ ℕ & ⊢ 𝑁 ∈ ℕ & ⊢ 𝑂 = {𝑐 ∈ 𝒫 (1...(𝑀 + 𝑁)) ∣ (♯‘𝑐) = 𝑀} & ⊢ 𝑃 = (𝑥 ∈ 𝒫 𝑂 ↦ ((♯‘𝑥) / (♯‘𝑂))) & ⊢ 𝐹 = (𝑐 ∈ 𝑂 ↦ (𝑖 ∈ ℤ ↦ ((♯‘((1...𝑖) ∩ 𝑐)) − (♯‘((1...𝑖) ∖ 𝑐))))) & ⊢ 𝐸 = {𝑐 ∈ 𝑂 ∣ ∀𝑖 ∈ (1...(𝑀 + 𝑁))0 < ((𝐹‘𝑐)‘𝑖)} & ⊢ 𝑁 < 𝑀 & ⊢ 𝐼 = (𝑐 ∈ (𝑂 ∖ 𝐸) ↦ inf({𝑘 ∈ (1...(𝑀 + 𝑁)) ∣ ((𝐹‘𝑐)‘𝑘) = 0}, ℝ, < )) & ⊢ 𝑆 = (𝑐 ∈ (𝑂 ∖ 𝐸) ↦ (𝑖 ∈ (1...(𝑀 + 𝑁)) ↦ if(𝑖 ≤ (𝐼‘𝑐), (((𝐼‘𝑐) + 1) − 𝑖), 𝑖))) & ⊢ 𝑅 = (𝑐 ∈ (𝑂 ∖ 𝐸) ↦ ((𝑆‘𝑐) “ 𝑐)) ⇒ ⊢ (𝑅 ↾ {𝑐 ∈ (𝑂 ∖ 𝐸) ∣ 1 ∈ 𝑐}):{𝑐 ∈ (𝑂 ∖ 𝐸) ∣ 1 ∈ 𝑐}–1-1-onto→{𝑐 ∈ (𝑂 ∖ 𝐸) ∣ ¬ 1 ∈ 𝑐} | ||
Theorem | ballotlem8 31794* | 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.) |
⊢ 𝑀 ∈ ℕ & ⊢ 𝑁 ∈ ℕ & ⊢ 𝑂 = {𝑐 ∈ 𝒫 (1...(𝑀 + 𝑁)) ∣ (♯‘𝑐) = 𝑀} & ⊢ 𝑃 = (𝑥 ∈ 𝒫 𝑂 ↦ ((♯‘𝑥) / (♯‘𝑂))) & ⊢ 𝐹 = (𝑐 ∈ 𝑂 ↦ (𝑖 ∈ ℤ ↦ ((♯‘((1...𝑖) ∩ 𝑐)) − (♯‘((1...𝑖) ∖ 𝑐))))) & ⊢ 𝐸 = {𝑐 ∈ 𝑂 ∣ ∀𝑖 ∈ (1...(𝑀 + 𝑁))0 < ((𝐹‘𝑐)‘𝑖)} & ⊢ 𝑁 < 𝑀 & ⊢ 𝐼 = (𝑐 ∈ (𝑂 ∖ 𝐸) ↦ inf({𝑘 ∈ (1...(𝑀 + 𝑁)) ∣ ((𝐹‘𝑐)‘𝑘) = 0}, ℝ, < )) & ⊢ 𝑆 = (𝑐 ∈ (𝑂 ∖ 𝐸) ↦ (𝑖 ∈ (1...(𝑀 + 𝑁)) ↦ if(𝑖 ≤ (𝐼‘𝑐), (((𝐼‘𝑐) + 1) − 𝑖), 𝑖))) & ⊢ 𝑅 = (𝑐 ∈ (𝑂 ∖ 𝐸) ↦ ((𝑆‘𝑐) “ 𝑐)) ⇒ ⊢ (♯‘{𝑐 ∈ (𝑂 ∖ 𝐸) ∣ 1 ∈ 𝑐}) = (♯‘{𝑐 ∈ (𝑂 ∖ 𝐸) ∣ ¬ 1 ∈ 𝑐}) | ||
Theorem | ballotth 31795* | Bertrand's ballot problem : the probability that A is ahead throughout the counting. The proof formalized here is a proof "by reflection", as opposed to other known proofs "by induction" or "by permutation". This is Metamath 100 proof #30. (Contributed by Thierry Arnoux, 7-Dec-2016.) |
⊢ 𝑀 ∈ ℕ & ⊢ 𝑁 ∈ ℕ & ⊢ 𝑂 = {𝑐 ∈ 𝒫 (1...(𝑀 + 𝑁)) ∣ (♯‘𝑐) = 𝑀} & ⊢ 𝑃 = (𝑥 ∈ 𝒫 𝑂 ↦ ((♯‘𝑥) / (♯‘𝑂))) & ⊢ 𝐹 = (𝑐 ∈ 𝑂 ↦ (𝑖 ∈ ℤ ↦ ((♯‘((1...𝑖) ∩ 𝑐)) − (♯‘((1...𝑖) ∖ 𝑐))))) & ⊢ 𝐸 = {𝑐 ∈ 𝑂 ∣ ∀𝑖 ∈ (1...(𝑀 + 𝑁))0 < ((𝐹‘𝑐)‘𝑖)} & ⊢ 𝑁 < 𝑀 & ⊢ 𝐼 = (𝑐 ∈ (𝑂 ∖ 𝐸) ↦ inf({𝑘 ∈ (1...(𝑀 + 𝑁)) ∣ ((𝐹‘𝑐)‘𝑘) = 0}, ℝ, < )) & ⊢ 𝑆 = (𝑐 ∈ (𝑂 ∖ 𝐸) ↦ (𝑖 ∈ (1...(𝑀 + 𝑁)) ↦ if(𝑖 ≤ (𝐼‘𝑐), (((𝐼‘𝑐) + 1) − 𝑖), 𝑖))) & ⊢ 𝑅 = (𝑐 ∈ (𝑂 ∖ 𝐸) ↦ ((𝑆‘𝑐) “ 𝑐)) ⇒ ⊢ (𝑃‘𝐸) = ((𝑀 − 𝑁) / (𝑀 + 𝑁)) | ||
Theorem | sgncl 31796 | Closure of the signum. (Contributed by Thierry Arnoux, 28-Sep-2018.) |
⊢ (𝐴 ∈ ℝ* → (sgn‘𝐴) ∈ {-1, 0, 1}) | ||
Theorem | sgnclre 31797 | Closure of the signum. (Contributed by Thierry Arnoux, 28-Sep-2018.) |
⊢ (𝐴 ∈ ℝ → (sgn‘𝐴) ∈ ℝ) | ||
Theorem | sgnneg 31798 | Negation of the signum. (Contributed by Thierry Arnoux, 1-Oct-2018.) |
⊢ (𝐴 ∈ ℝ → (sgn‘-𝐴) = -(sgn‘𝐴)) | ||
Theorem | sgn3da 31799 | A conditional containing a signum is true if it is true in all three possible cases. (Contributed by Thierry Arnoux, 1-Oct-2018.) |
⊢ (𝜑 → 𝐴 ∈ ℝ*) & ⊢ ((sgn‘𝐴) = 0 → (𝜓 ↔ 𝜒)) & ⊢ ((sgn‘𝐴) = 1 → (𝜓 ↔ 𝜃)) & ⊢ ((sgn‘𝐴) = -1 → (𝜓 ↔ 𝜏)) & ⊢ ((𝜑 ∧ 𝐴 = 0) → 𝜒) & ⊢ ((𝜑 ∧ 0 < 𝐴) → 𝜃) & ⊢ ((𝜑 ∧ 𝐴 < 0) → 𝜏) ⇒ ⊢ (𝜑 → 𝜓) | ||
Theorem | sgnmul 31800 | Signum of a product. (Contributed by Thierry Arnoux, 2-Oct-2018.) |
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (sgn‘(𝐴 · 𝐵)) = ((sgn‘𝐴) · (sgn‘𝐵))) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |