Users' Mathboxes Mathbox for Thierry Arnoux < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  ballotlem2 Unicode version

Theorem ballotlem2 26574
Description: The probability that the first vote picked in a count is a B (Contributed by Thierry Arnoux, 23-Nov-2016.)
Hypotheses
Ref Expression
ballotth.m
ballotth.n
ballotth.o
ballotth.p
Assertion
Ref Expression
ballotlem2
Distinct variable groups:   M,   N,   O, ,

Proof of Theorem ballotlem2
Dummy variable is distinct from all other variables.
StepHypRef Expression
1 ssrab2 3414 . . . . 5
2 ballotth.m . . . . . . 7
3 ballotth.n . . . . . . 7
4 ballotth.o . . . . . . 7
52, 3, 4ballotlemoex 26571 . . . . . 6
65elpw2 4428 . . . . 5
71, 6mpbir 203 . . . 4
8 fveq2 5661 . . . . . 6
98oveq1d 6076 . . . . 5
10 ballotth.p . . . . 5
11 ovex 6086 . . . . 5
129, 10, 11fvmpt 5744 . . . 4
137, 12ax-mp 5 . . 3
14 1le2 10481 . . . . . . . . . . . . . . . 16
15 1z 10621 . . . . . . . . . . . . . . . . 17
16 2z 10623 . . . . . . . . . . . . . . . . 17
17 eluz 10819 . . . . . . . . . . . . . . . . 17
1815, 16, 17mp2an 657 . . . . . . . . . . . . . . . 16
1914, 18mpbir 203 . . . . . . . . . . . . . . 15
20 fzss1 11441 . . . . . . . . . . . . . . 15
2119, 20ax-mp 5 . . . . . . . . . . . . . 14
22 sspwb 4513 . . . . . . . . . . . . . 14
2321, 22mpbi 202 . . . . . . . . . . . . 13
2423sseli 3329 . . . . . . . . . . . 12
25 1lt2 10434 . . . . . . . . . . . . . . . . 17
26 1re 9331 . . . . . . . . . . . . . . . . . 18
27 2re 10337 . . . . . . . . . . . . . . . . . 18
2826, 27ltnlei 9441 . . . . . . . . . . . . . . . . 17
2925, 28mpbi 202 . . . . . . . . . . . . . . . 16
30 elfzle1 11398 . . . . . . . . . . . . . . . 16
3129, 30mto 170 . . . . . . . . . . . . . . 15
32 elelpwi 3848 . . . . . . . . . . . . . . 15
3331, 32mto 170 . . . . . . . . . . . . . 14
34 ancom 441 . . . . . . . . . . . . . 14
3533, 34mtbi 292 . . . . . . . . . . . . 13
3635imnani 416 . . . . . . . . . . . 12
3724, 36jca 522 . . . . . . . . . . 11
38 ssin 3549 . . . . . . . . . . . . 13
39 1p1e2 10381 . . . . . . . . . . . . . . . . . . . . . . 23
40 nnge1 10294 . . . . . . . . . . . . . . . . . . . . . . . . 25
412, 40ax-mp 5 . . . . . . . . . . . . . . . . . . . . . . . 24
42 nnge1 10294 . . . . . . . . . . . . . . . . . . . . . . . . 25
433, 42ax-mp 5 . . . . . . . . . . . . . . . . . . . . . . . 24
442nnrei 10277 . . . . . . . . . . . . . . . . . . . . . . . . 25
453nnrei 10277 . . . . . . . . . . . . . . . . . . . . . . . . 25
4626, 26, 44, 45le2addi 9849 . . . . . . . . . . . . . . . . . . . . . . . 24
4741, 43, 46mp2an 657 . . . . . . . . . . . . . . . . . . . . . . 23
4839, 47eqbrtrri 4288 . . . . . . . . . . . . . . . . . . . . . 22
4944, 45readdcli 9345 . . . . . . . . . . . . . . . . . . . . . . 23
5026, 27, 49letri 9449 . . . . . . . . . . . . . . . . . . . . . 22
5114, 48, 50mp2an 657 . . . . . . . . . . . . . . . . . . . . 21
52 nnaddcl 10290 . . . . . . . . . . . . . . . . . . . . . . . 24
532, 3, 52mp2an 657 . . . . . . . . . . . . . . . . . . . . . . 23
5453nnzi 10615 . . . . . . . . . . . . . . . . . . . . . 22
55 eluz 10819 . . . . . . . . . . . . . . . . . . . . . 22
5615, 54, 55mp2an 657 . . . . . . . . . . . . . . . . . . . . 21
5751, 56mpbir 203 . . . . . . . . . . . . . . . . . . . 20
58 elfzp12 11480 . . . . . . . . . . . . . . . . . . . 20
5957, 58ax-mp 5 . . . . . . . . . . . . . . . . . . 19
6059biimpi 188 . . . . . . . . . . . . . . . . . 18
6160orcanai 889 . . . . . . . . . . . . . . . . 17
6239oveq1i 6071 . . . . . . . . . . . . . . . . 17
6361, 62syl6eleq 2512 . . . . . . . . . . . . . . . 16
6463ss2abi 3401 . . . . . . . . . . . . . . 15
65 inab 3595 . . . . . . . . . . . . . . . 16
66 abid2 2539 . . . . . . . . . . . . . . . . 17
6766ineq1i 3525 . . . . . . . . . . . . . . . 16
6865, 67eqtr3i 2444 . . . . . . . . . . . . . . 15
69 abid2 2539 . . . . . . . . . . . . . . 15
7064, 68, 693sstr3i 3371 . . . . . . . . . . . . . 14
71 sstr 3341 . . . . . . . . . . . . . 14
7270, 71mpan2 656 . . . . . . . . . . . . 13
7338, 72sylbi 189 . . . . . . . . . . . 12
74 selpw 3844 . . . . . . . . . . . . 13
75 ssab 3399 . . . . . . . . . . . . . 14
76 df-ex 1582 . . . . . . . . . . . . . . . . 17
7776bicomi 196 . . . . . . . . . . . . . . . 16
7877con1bii 324 . . . . . . . . . . . . . . 15
79 df-clel 2418 . . . . . . . . . . . . . . . 16
8079notbii 290 . . . . . . . . . . . . . . 15
81 imnan 415 . . . . . . . . . . . . . . . . 17
8281albii 1605 . . . . . . . . . . . . . . . 16
83 ancom 441 . . . . . . . . . . . . . . . . . 18
8483notbii 290 . . . . . . . . . . . . . . . . 17
8584albii 1605 . . . . . . . . . . . . . . . 16
8682, 85bitr4i 246 . . . . . . . . . . . . . . 15
8778, 80, 863bitr4ri 272 . . . . . . . . . . . . . 14
8875, 87bitr2i 244 . . . . . . . . . . . . 13
8974, 88anbi12i 682 . . . . . . . . . . . 12
90 selpw 3844 . . . . . . . . . . . 12
9173, 89, 903imtr4i 260 . . . . . . . . . . 11
9237, 91impbii 182 . . . . . . . . . 10
9392anbi1i 680 . . . . . . . . 9
944rabeq2i 2948 . . . . . . . . . . 11
9594anbi1i 680 . . . . . . . . . 10
96 an32 781 . . . . . . . . . 10
9795, 96bitr4i 246 . . . . . . . . 9
9893, 97bitr4i 246 . . . . . . . 8
9998abbii 2534 . . . . . . 7
100 df-rab 2703 . . . . . . 7
101 df-rab 2703 . . . . . . 7
10299, 100, 1013eqtr4i 2452 . . . . . 6
103102fveq2i 5664 . . . . 5
104 fzfi 11735 . . . . . . 7
1052nnzi 10615 . . . . . . 7
106 hashbc 12147 . . . . . . 7
107104, 105, 106mp2an 657 . . . . . 6
10816eluz1i 10813 . . . . . . . . . . 11
10954, 48, 108mpbir2an 896 . . . . . . . . . 10
110 hashfz 12129 . . . . . . . . . 10
111109, 110ax-mp 5 . . . . . . . . 9
1122nncni 10278 . . . . . . . . . . 11
1133nncni 10278 . . . . . . . . . . 11
114112, 113addcli 9336 . . . . . . . . . 10
115 2cn 10338 . . . . . . . . . 10
116 ax-1cn 9286 . . . . . . . . . 10
117 subadd23 9568 . . . . . . . . . 10
118114, 115, 116, 117mp3an 1299 . . . . . . . . 9
119115, 116negsubdi2i 9640 . . . . . . . . . . 11
120 2m1e1 10382 . . . . . . . . . . . 12
121120negeqi 9549 . . . . . . . . . . 11
122119, 121eqtr3i 2444 . . . . . . . . . 10
123122oveq2i 6072 . . . . . . . . 9
124111, 118, 1233eqtri 2446 . . . . . . . 8
125114, 116negsubi 9632 . . . . . . . 8
126124, 125eqtri 2442 . . . . . . 7
127126oveq1i 6071 . . . . . 6
128107, 127eqtr3i 2444 . . . . 5
129103, 128eqtr3i 2444 . . . 4
1302, 3, 4ballotlem1 26572 . . . 4
131129, 130oveq12i 6073 . . 3
13213, 131eqtri 2442 . 2
133 0le1 9809 . . . . . 6
134 0re 9332 . . . . . . 7
135134, 26, 44letri 9449 . . . . . 6
136133, 41, 135mp2an 657 . . . . 5
1373nngt0i 10301 . . . . . . 7
13845, 137elrpii 10939 . . . . . 6
139 ltaddrp 10968 . . . . . 6
14044, 138, 139mp2an 657 . . . . 5
141105, 136, 1403pm3.2i 1151 . . . 4
142 0z 10602 . . . . 5
143 elfzm11 11469 . . . . 5
144142, 54, 143mp2an 657 . . . 4
145141, 144mpbir 203 . . 3
146 bcm1n 25757 . . 3
147145, 53, 146mp2an 657 . 2
148 pncan2 9563 . . . 4
149112, 113, 148mp2an 657 . . 3
150149oveq1i 6071 . 2
151132, 147, 1503eqtri 2446 1
Colors of variables: wff setvar class
Syntax hints:  -.wn 3  ->wi 4  <->wb 178  \/wo 361  /\wa 362  /\w3a 950  A.wal 1580  E.wex 1581  =wceq 1687  e.wcel 1749  {cab 2408  {crab 2698  i^icin 3304  C_wss 3305  ~Pcpw 3837   class class class wbr 4267  e.cmpt 4325  `cfv 5390  (class class class)co 6061   cfn 7269   cc 9226   cr 9227  0cc0 9228  1c1 9229   caddc 9231   clt 9364   cle 9365   cmin 9541  -ucneg 9542   cdiv 9939   cn 10268  2c2 10317   cz 10591   cuz 10806   crp 10936   cfz 11381   cbc 12019   chash 12044
This theorem is referenced by:  ballotth  26623
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1586  ax-4 1597  ax-5 1661  ax-6 1701  ax-7 1721  ax-8 1751  ax-9 1753  ax-10 1768  ax-11 1773  ax-12 1785  ax-13 1934  ax-ext 2403  ax-rep 4378  ax-sep 4388  ax-nul 4396  ax-pow 4442  ax-pr 4503  ax-un 6342  ax-cnex 9284  ax-resscn 9285  ax-1cn 9286  ax-icn 9287  ax-addcl 9288  ax-addrcl 9289  ax-mulcl 9290  ax-mulrcl 9291  ax-mulcom 9292  ax-addass 9293  ax-mulass 9294  ax-distr 9295  ax-i2m1 9296  ax-1ne0 9297  ax-1rid 9298  ax-rnegex 9299  ax-rrecex 9300  ax-cnre 9301  ax-pre-lttri 9302  ax-pre-lttrn 9303  ax-pre-ltadd 9304  ax-pre-mulgt0 9305
This theorem depends on definitions:  df-bi 179  df-or 363  df-an 364  df-3or 951  df-3an 952  df-tru 1355  df-ex 1582  df-nf 1585  df-sb 1694  df-eu 2248  df-mo 2249  df-clab 2409  df-cleq 2415  df-clel 2418  df-nfc 2547  df-ne 2587  df-nel 2588  df-ral 2699  df-rex 2700  df-reu 2701  df-rmo 2702  df-rab 2703  df-v 2953  df-sbc 3165  df-csb 3266  df-dif 3308  df-un 3310  df-in 3312  df-ss 3319  df-pss 3321  df-nul 3615  df-if 3769  df-pw 3839  df-sn 3859  df-pr 3860  df-tp 3861  df-op 3862  df-uni 4067  df-int 4104  df-iun 4148  df-br 4268  df-opab 4326  df-mpt 4327  df-tr 4361  df-eprel 4603  df-id 4607  df-po 4612  df-so 4613  df-fr 4650  df-we 4652  df-ord 4693  df-on 4694  df-lim 4695  df-suc 4696  df-xp 4817  df-rel 4818  df-cnv 4819  df-co 4820  df-dm 4821  df-rn 4822  df-res 4823  df-ima 4824  df-iota 5353  df-fun 5392  df-fn 5393  df-f 5394  df-f1 5395  df-fo 5396  df-f1o 5397  df-fv 5398  df-riota 6020  df-ov 6064  df-oprab 6065  df-mpt2 6066  df-om 6447  df-1st 6546  df-2nd 6547  df-recs 6791  df-rdg 6825  df-1o 6881  df-2o 6882  df-oadd 6885  df-er 7062  df-map 7177  df-en 7270  df-dom 7271  df-sdom 7272  df-fin 7273  df-card 8056  df-cda 8284  df-pnf 9366  df-mnf 9367  df-xr 9368  df-ltxr 9369  df-le 9370  df-sub 9543  df-neg 9544  df-div 9940  df-nn 10269  df-2 10326  df-n0 10526  df-z 10592  df-uz 10807  df-rp 10937  df-fz 11382  df-seq 11748  df-fac 11993  df-bc 12020  df-hash 12045
  Copyright terms: Public domain W3C validator