Mathbox for Thierry Arnoux < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  ballotlemsv Structured version   Visualization version   GIF version

Theorem ballotlemsv 30902
 Description: Value of 𝑆 evaluated at 𝐽 for a given counting 𝐶. (Contributed by Thierry Arnoux, 12-Apr-2017.)
Hypotheses
Ref Expression
ballotth.m 𝑀 ∈ ℕ
ballotth.n 𝑁 ∈ ℕ
ballotth.o 𝑂 = {𝑐 ∈ 𝒫 (1...(𝑀 + 𝑁)) ∣ (♯‘𝑐) = 𝑀}
ballotth.p 𝑃 = (𝑥 ∈ 𝒫 𝑂 ↦ ((♯‘𝑥) / (♯‘𝑂)))
ballotth.f 𝐹 = (𝑐𝑂 ↦ (𝑖 ∈ ℤ ↦ ((♯‘((1...𝑖) ∩ 𝑐)) − (♯‘((1...𝑖) ∖ 𝑐)))))
ballotth.e 𝐸 = {𝑐𝑂 ∣ ∀𝑖 ∈ (1...(𝑀 + 𝑁))0 < ((𝐹𝑐)‘𝑖)}
ballotth.mgtn 𝑁 < 𝑀
ballotth.i 𝐼 = (𝑐 ∈ (𝑂𝐸) ↦ inf({𝑘 ∈ (1...(𝑀 + 𝑁)) ∣ ((𝐹𝑐)‘𝑘) = 0}, ℝ, < ))
ballotth.s 𝑆 = (𝑐 ∈ (𝑂𝐸) ↦ (𝑖 ∈ (1...(𝑀 + 𝑁)) ↦ if(𝑖 ≤ (𝐼𝑐), (((𝐼𝑐) + 1) − 𝑖), 𝑖)))
Assertion
Ref Expression
ballotlemsv ((𝐶 ∈ (𝑂𝐸) ∧ 𝐽 ∈ (1...(𝑀 + 𝑁))) → ((𝑆𝐶)‘𝐽) = if(𝐽 ≤ (𝐼𝐶), (((𝐼𝐶) + 1) − 𝐽), 𝐽))
Distinct variable groups:   𝑀,𝑐   𝑁,𝑐   𝑂,𝑐   𝑖,𝑀   𝑖,𝑁   𝑖,𝑂   𝑘,𝑀   𝑘,𝑁   𝑘,𝑂   𝑖,𝑐,𝐹,𝑘   𝐶,𝑖,𝑘   𝑖,𝐸,𝑘   𝐶,𝑘   𝑘,𝐼,𝑐   𝐸,𝑐   𝑖,𝐼,𝑐
Allowed substitution hints:   𝐶(𝑥,𝑐)   𝑃(𝑥,𝑖,𝑘,𝑐)   𝑆(𝑥,𝑖,𝑘,𝑐)   𝐸(𝑥)   𝐹(𝑥)   𝐼(𝑥)   𝐽(𝑥,𝑖,𝑘,𝑐)   𝑀(𝑥)   𝑁(𝑥)   𝑂(𝑥)

Proof of Theorem ballotlemsv
Dummy variable 𝑗 is distinct from all other variables.
StepHypRef Expression
1 ballotth.m . . . . 5 𝑀 ∈ ℕ
2 ballotth.n . . . . 5 𝑁 ∈ ℕ
3 ballotth.o . . . . 5 𝑂 = {𝑐 ∈ 𝒫 (1...(𝑀 + 𝑁)) ∣ (♯‘𝑐) = 𝑀}
4 ballotth.p . . . . 5 𝑃 = (𝑥 ∈ 𝒫 𝑂 ↦ ((♯‘𝑥) / (♯‘𝑂)))
5 ballotth.f . . . . 5 𝐹 = (𝑐𝑂 ↦ (𝑖 ∈ ℤ ↦ ((♯‘((1...𝑖) ∩ 𝑐)) − (♯‘((1...𝑖) ∖ 𝑐)))))
6 ballotth.e . . . . 5 𝐸 = {𝑐𝑂 ∣ ∀𝑖 ∈ (1...(𝑀 + 𝑁))0 < ((𝐹𝑐)‘𝑖)}
7 ballotth.mgtn . . . . 5 𝑁 < 𝑀
8 ballotth.i . . . . 5 𝐼 = (𝑐 ∈ (𝑂𝐸) ↦ inf({𝑘 ∈ (1...(𝑀 + 𝑁)) ∣ ((𝐹𝑐)‘𝑘) = 0}, ℝ, < ))
9 ballotth.s . . . . 5 𝑆 = (𝑐 ∈ (𝑂𝐸) ↦ (𝑖 ∈ (1...(𝑀 + 𝑁)) ↦ if(𝑖 ≤ (𝐼𝑐), (((𝐼𝑐) + 1) − 𝑖), 𝑖)))
101, 2, 3, 4, 5, 6, 7, 8, 9ballotlemsval 30901 . . . 4 (𝐶 ∈ (𝑂𝐸) → (𝑆𝐶) = (𝑖 ∈ (1...(𝑀 + 𝑁)) ↦ if(𝑖 ≤ (𝐼𝐶), (((𝐼𝐶) + 1) − 𝑖), 𝑖)))
11 breq1 4808 . . . . . 6 (𝑖 = 𝑗 → (𝑖 ≤ (𝐼𝐶) ↔ 𝑗 ≤ (𝐼𝐶)))
12 oveq2 6823 . . . . . 6 (𝑖 = 𝑗 → (((𝐼𝐶) + 1) − 𝑖) = (((𝐼𝐶) + 1) − 𝑗))
13 id 22 . . . . . 6 (𝑖 = 𝑗𝑖 = 𝑗)
1411, 12, 13ifbieq12d 4258 . . . . 5 (𝑖 = 𝑗 → if(𝑖 ≤ (𝐼𝐶), (((𝐼𝐶) + 1) − 𝑖), 𝑖) = if(𝑗 ≤ (𝐼𝐶), (((𝐼𝐶) + 1) − 𝑗), 𝑗))
1514cbvmptv 4903 . . . 4 (𝑖 ∈ (1...(𝑀 + 𝑁)) ↦ if(𝑖 ≤ (𝐼𝐶), (((𝐼𝐶) + 1) − 𝑖), 𝑖)) = (𝑗 ∈ (1...(𝑀 + 𝑁)) ↦ if(𝑗 ≤ (𝐼𝐶), (((𝐼𝐶) + 1) − 𝑗), 𝑗))
1610, 15syl6eq 2811 . . 3 (𝐶 ∈ (𝑂𝐸) → (𝑆𝐶) = (𝑗 ∈ (1...(𝑀 + 𝑁)) ↦ if(𝑗 ≤ (𝐼𝐶), (((𝐼𝐶) + 1) − 𝑗), 𝑗)))
1716adantr 472 . 2 ((𝐶 ∈ (𝑂𝐸) ∧ 𝐽 ∈ (1...(𝑀 + 𝑁))) → (𝑆𝐶) = (𝑗 ∈ (1...(𝑀 + 𝑁)) ↦ if(𝑗 ≤ (𝐼𝐶), (((𝐼𝐶) + 1) − 𝑗), 𝑗)))
18 simpr 479 . . . . 5 ((𝐶 ∈ (𝑂𝐸) ∧ 𝑗 = 𝐽) → 𝑗 = 𝐽)
1918breq1d 4815 . . . 4 ((𝐶 ∈ (𝑂𝐸) ∧ 𝑗 = 𝐽) → (𝑗 ≤ (𝐼𝐶) ↔ 𝐽 ≤ (𝐼𝐶)))
2018oveq2d 6831 . . . 4 ((𝐶 ∈ (𝑂𝐸) ∧ 𝑗 = 𝐽) → (((𝐼𝐶) + 1) − 𝑗) = (((𝐼𝐶) + 1) − 𝐽))
2119, 20, 18ifbieq12d 4258 . . 3 ((𝐶 ∈ (𝑂𝐸) ∧ 𝑗 = 𝐽) → if(𝑗 ≤ (𝐼𝐶), (((𝐼𝐶) + 1) − 𝑗), 𝑗) = if(𝐽 ≤ (𝐼𝐶), (((𝐼𝐶) + 1) − 𝐽), 𝐽))
2221adantlr 753 . 2 (((𝐶 ∈ (𝑂𝐸) ∧ 𝐽 ∈ (1...(𝑀 + 𝑁))) ∧ 𝑗 = 𝐽) → if(𝑗 ≤ (𝐼𝐶), (((𝐼𝐶) + 1) − 𝑗), 𝑗) = if(𝐽 ≤ (𝐼𝐶), (((𝐼𝐶) + 1) − 𝐽), 𝐽))
23 simpr 479 . 2 ((𝐶 ∈ (𝑂𝐸) ∧ 𝐽 ∈ (1...(𝑀 + 𝑁))) → 𝐽 ∈ (1...(𝑀 + 𝑁)))
24 ovexd 6845 . . 3 (((𝐶 ∈ (𝑂𝐸) ∧ 𝐽 ∈ (1...(𝑀 + 𝑁))) ∧ 𝐽 ≤ (𝐼𝐶)) → (((𝐼𝐶) + 1) − 𝐽) ∈ V)
25 elex 3353 . . . 4 (𝐽 ∈ (1...(𝑀 + 𝑁)) → 𝐽 ∈ V)
2625ad2antlr 765 . . 3 (((𝐶 ∈ (𝑂𝐸) ∧ 𝐽 ∈ (1...(𝑀 + 𝑁))) ∧ ¬ 𝐽 ≤ (𝐼𝐶)) → 𝐽 ∈ V)
2724, 26ifclda 4265 . 2 ((𝐶 ∈ (𝑂𝐸) ∧ 𝐽 ∈ (1...(𝑀 + 𝑁))) → if(𝐽 ≤ (𝐼𝐶), (((𝐼𝐶) + 1) − 𝐽), 𝐽) ∈ V)
2817, 22, 23, 27fvmptd 6452 1 ((𝐶 ∈ (𝑂𝐸) ∧ 𝐽 ∈ (1...(𝑀 + 𝑁))) → ((𝑆𝐶)‘𝐽) = if(𝐽 ≤ (𝐼𝐶), (((𝐼𝐶) + 1) − 𝐽), 𝐽))
 Colors of variables: wff setvar class Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 383   = wceq 1632   ∈ wcel 2140  ∀wral 3051  {crab 3055  Vcvv 3341   ∖ cdif 3713   ∩ cin 3715  ifcif 4231  𝒫 cpw 4303   class class class wbr 4805   ↦ cmpt 4882  ‘cfv 6050  (class class class)co 6815  infcinf 8515  ℝcr 10148  0cc0 10149  1c1 10150   + caddc 10152   < clt 10287   ≤ cle 10288   − cmin 10479   / cdiv 10897  ℕcn 11233  ℤcz 11590  ...cfz 12540  ♯chash 13332 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1871  ax-4 1886  ax-5 1989  ax-6 2055  ax-7 2091  ax-9 2149  ax-10 2169  ax-11 2184  ax-12 2197  ax-13 2392  ax-ext 2741  ax-rep 4924  ax-sep 4934  ax-nul 4942  ax-pr 5056 This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3an 1074  df-tru 1635  df-ex 1854  df-nf 1859  df-sb 2048  df-eu 2612  df-mo 2613  df-clab 2748  df-cleq 2754  df-clel 2757  df-nfc 2892  df-ne 2934  df-ral 3056  df-rex 3057  df-reu 3058  df-rab 3060  df-v 3343  df-sbc 3578  df-csb 3676  df-dif 3719  df-un 3721  df-in 3723  df-ss 3730  df-nul 4060  df-if 4232  df-sn 4323  df-pr 4325  df-op 4329  df-uni 4590  df-iun 4675  df-br 4806  df-opab 4866  df-mpt 4883  df-id 5175  df-xp 5273  df-rel 5274  df-cnv 5275  df-co 5276  df-dm 5277  df-rn 5278  df-res 5279  df-ima 5280  df-iota 6013  df-fun 6052  df-fn 6053  df-f 6054  df-f1 6055  df-fo 6056  df-f1o 6057  df-fv 6058  df-ov 6818 This theorem is referenced by:  ballotlemsgt1  30903  ballotlemsdom  30904  ballotlemsel1i  30905  ballotlemsf1o  30906  ballotlemsi  30907  ballotlemsima  30908  ballotlemrv  30912
 Copyright terms: Public domain W3C validator