Metamath Proof Explorer


Theorem ballotlem2

Description: The probability that the first vote picked in a count is a B. (Contributed by Thierry Arnoux, 23-Nov-2016)

Ref Expression
Hypotheses ballotth.m M
ballotth.n N
ballotth.o O=c𝒫1M+N|c=M
ballotth.p P=x𝒫OxO
Assertion ballotlem2 PcO|¬1c=NM+N

Proof

Step Hyp Ref Expression
1 ballotth.m M
2 ballotth.n N
3 ballotth.o O=c𝒫1M+N|c=M
4 ballotth.p P=x𝒫OxO
5 1 2 3 ballotlemoex OV
6 ssrab2 cO|¬1cO
7 5 6 elpwi2 cO|¬1c𝒫O
8 fveq2 x=cO|¬1cx=cO|¬1c
9 8 oveq1d x=cO|¬1cxO=cO|¬1cO
10 ovex cO|¬1cOV
11 9 4 10 fvmpt cO|¬1c𝒫OPcO|¬1c=cO|¬1cO
12 7 11 ax-mp PcO|¬1c=cO|¬1cO
13 an32 c𝒫1M+N¬1cc=Mc𝒫1M+Nc=M¬1c
14 2eluzge1 21
15 fzss1 212M+N1M+N
16 14 15 ax-mp 2M+N1M+N
17 16 sspwi 𝒫2M+N𝒫1M+N
18 17 sseli c𝒫2M+Nc𝒫1M+N
19 1lt2 1<2
20 1re 1
21 2re 2
22 20 21 ltnlei 1<2¬21
23 19 22 mpbi ¬21
24 elfzle1 12M+N21
25 23 24 mto ¬12M+N
26 elelpwi 1cc𝒫2M+N12M+N
27 25 26 mto ¬1cc𝒫2M+N
28 ancom 1cc𝒫2M+Nc𝒫2M+N1c
29 27 28 mtbi ¬c𝒫2M+N1c
30 29 imnani c𝒫2M+N¬1c
31 18 30 jca c𝒫2M+Nc𝒫1M+N¬1c
32 ssin c1M+Nci|¬i=1c1M+Ni|¬i=1
33 1le2 12
34 1p1e2 1+1=2
35 nnge1 M1M
36 1 35 ax-mp 1M
37 nnge1 N1N
38 2 37 ax-mp 1N
39 1 nnrei M
40 2 nnrei N
41 20 20 39 40 le2addi 1M1N1+1M+N
42 36 38 41 mp2an 1+1M+N
43 34 42 eqbrtrri 2M+N
44 39 40 readdcli M+N
45 20 21 44 letri 122M+N1M+N
46 33 43 45 mp2an 1M+N
47 1z 1
48 nnaddcl MNM+N
49 1 2 48 mp2an M+N
50 49 nnzi M+N
51 eluz 1M+NM+N11M+N
52 47 50 51 mp2an M+N11M+N
53 46 52 mpbir M+N1
54 elfzp12 M+N1i1M+Ni=1i1+1M+N
55 53 54 ax-mp i1M+Ni=1i1+1M+N
56 55 biimpi i1M+Ni=1i1+1M+N
57 56 orcanai i1M+N¬i=1i1+1M+N
58 34 oveq1i 1+1M+N=2M+N
59 57 58 eleqtrdi i1M+N¬i=1i2M+N
60 59 ss2abi i|i1M+N¬i=1i|i2M+N
61 inab i|i1M+Ni|¬i=1=i|i1M+N¬i=1
62 abid2 i|i1M+N=1M+N
63 62 ineq1i i|i1M+Ni|¬i=1=1M+Ni|¬i=1
64 61 63 eqtr3i i|i1M+N¬i=1=1M+Ni|¬i=1
65 abid2 i|i2M+N=2M+N
66 60 64 65 3sstr3i 1M+Ni|¬i=12M+N
67 sstr c1M+Ni|¬i=11M+Ni|¬i=12M+Nc2M+N
68 66 67 mpan2 c1M+Ni|¬i=1c2M+N
69 32 68 sylbi c1M+Nci|¬i=1c2M+N
70 velpw c𝒫1M+Nc1M+N
71 ssab ci|¬i=1iic¬i=1
72 df-ex ii=1ic¬i¬i=1ic
73 72 bicomi ¬i¬i=1icii=1ic
74 73 con1bii ¬ii=1ici¬i=1ic
75 dfclel 1cii=1ic
76 75 notbii ¬1c¬ii=1ic
77 imnang iic¬i=1i¬ici=1
78 ancom i=1icici=1
79 78 notbii ¬i=1ic¬ici=1
80 79 albii i¬i=1ici¬ici=1
81 77 80 bitr4i iic¬i=1i¬i=1ic
82 74 76 81 3bitr4ri iic¬i=1¬1c
83 71 82 bitr2i ¬1cci|¬i=1
84 70 83 anbi12i c𝒫1M+N¬1cc1M+Nci|¬i=1
85 velpw c𝒫2M+Nc2M+N
86 69 84 85 3imtr4i c𝒫1M+N¬1cc𝒫2M+N
87 31 86 impbii c𝒫2M+Nc𝒫1M+N¬1c
88 87 anbi1i c𝒫2M+Nc=Mc𝒫1M+N¬1cc=M
89 3 rabeq2i cOc𝒫1M+Nc=M
90 89 anbi1i cO¬1cc𝒫1M+Nc=M¬1c
91 13 88 90 3bitr4i c𝒫2M+Nc=McO¬1c
92 91 rabbia2 c𝒫2M+N|c=M=cO|¬1c
93 92 fveq2i c𝒫2M+N|c=M=cO|¬1c
94 fzfi 2M+NFin
95 1 nnzi M
96 hashbc 2M+NFinM(2M+NM)=c𝒫2M+N|c=M
97 94 95 96 mp2an (2M+NM)=c𝒫2M+N|c=M
98 2z 2
99 98 eluz1i M+N2M+N2M+N
100 50 43 99 mpbir2an M+N2
101 hashfz M+N22M+N=M+N-2+1
102 100 101 ax-mp 2M+N=M+N-2+1
103 1 nncni M
104 2 nncni N
105 103 104 addcli M+N
106 2cn 2
107 ax-1cn 1
108 subadd23 M+N21M+N-2+1=M+N+12
109 105 106 107 108 mp3an M+N-2+1=M+N+12
110 106 107 negsubdi2i 21=12
111 2m1e1 21=1
112 111 negeqi 21=1
113 110 112 eqtr3i 12=1
114 113 oveq2i M+N+12=M+N+-1
115 102 109 114 3eqtri 2M+N=M+N+-1
116 105 107 negsubi M+N+-1=M+N-1
117 115 116 eqtri 2M+N=M+N-1
118 117 oveq1i (2M+NM)=(M+N-1M)
119 97 118 eqtr3i c𝒫2M+N|c=M=(M+N-1M)
120 93 119 eqtr3i cO|¬1c=(M+N-1M)
121 1 2 3 ballotlem1 O=(M+NM)
122 120 121 oveq12i cO|¬1cO=(M+N-1M)(M+NM)
123 12 122 eqtri PcO|¬1c=(M+N-1M)(M+NM)
124 0le1 01
125 0re 0
126 125 20 39 letri 011M0M
127 124 36 126 mp2an 0M
128 2 nngt0i 0<N
129 40 128 elrpii N+
130 ltaddrp MN+M<M+N
131 39 129 130 mp2an M<M+N
132 0z 0
133 elfzm11 0M+NM0M+N-1M0MM<M+N
134 132 50 133 mp2an M0M+N-1M0MM<M+N
135 95 127 131 134 mpbir3an M0M+N-1
136 bcm1n M0M+N-1M+N(M+N-1M)(M+NM)=M+N-MM+N
137 135 49 136 mp2an (M+N-1M)(M+NM)=M+N-MM+N
138 pncan2 MNM+N-M=N
139 103 104 138 mp2an M+N-M=N
140 139 oveq1i M+N-MM+N=NM+N
141 123 137 140 3eqtri PcO|¬1c=NM+N