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 e. NN
ballotth.n 
|- N e. NN
ballotth.o 
|- O = { c e. ~P ( 1 ... ( M + N ) ) | ( # ` c ) = M }
ballotth.p 
|- P = ( x e. ~P O |-> ( ( # ` x ) / ( # ` O ) ) )
Assertion ballotlem2 
|- ( P ` { c e. O | -. 1 e. c } ) = ( N / ( M + N ) )

Proof

Step Hyp Ref Expression
1 ballotth.m 
 |-  M e. NN
2 ballotth.n 
 |-  N e. NN
3 ballotth.o 
 |-  O = { c e. ~P ( 1 ... ( M + N ) ) | ( # ` c ) = M }
4 ballotth.p 
 |-  P = ( x e. ~P O |-> ( ( # ` x ) / ( # ` O ) ) )
5 1 2 3 ballotlemoex 
 |-  O e. _V
6 ssrab2 
 |-  { c e. O | -. 1 e. c } C_ O
7 5 6 elpwi2 
 |-  { c e. O | -. 1 e. c } e. ~P O
8 fveq2 
 |-  ( x = { c e. O | -. 1 e. c } -> ( # ` x ) = ( # ` { c e. O | -. 1 e. c } ) )
9 8 oveq1d 
 |-  ( x = { c e. O | -. 1 e. c } -> ( ( # ` x ) / ( # ` O ) ) = ( ( # ` { c e. O | -. 1 e. c } ) / ( # ` O ) ) )
10 ovex 
 |-  ( ( # ` { c e. O | -. 1 e. c } ) / ( # ` O ) ) e. _V
11 9 4 10 fvmpt 
 |-  ( { c e. O | -. 1 e. c } e. ~P O -> ( P ` { c e. O | -. 1 e. c } ) = ( ( # ` { c e. O | -. 1 e. c } ) / ( # ` O ) ) )
12 7 11 ax-mp 
 |-  ( P ` { c e. O | -. 1 e. c } ) = ( ( # ` { c e. O | -. 1 e. c } ) / ( # ` O ) )
13 an32 
 |-  ( ( ( c e. ~P ( 1 ... ( M + N ) ) /\ -. 1 e. c ) /\ ( # ` c ) = M ) <-> ( ( c e. ~P ( 1 ... ( M + N ) ) /\ ( # ` c ) = M ) /\ -. 1 e. c ) )
14 2eluzge1 
 |-  2 e. ( ZZ>= ` 1 )
15 fzss1 
 |-  ( 2 e. ( ZZ>= ` 1 ) -> ( 2 ... ( M + N ) ) C_ ( 1 ... ( M + N ) ) )
16 14 15 ax-mp 
 |-  ( 2 ... ( M + N ) ) C_ ( 1 ... ( M + N ) )
17 16 sspwi 
 |-  ~P ( 2 ... ( M + N ) ) C_ ~P ( 1 ... ( M + N ) )
18 17 sseli 
 |-  ( c e. ~P ( 2 ... ( M + N ) ) -> c e. ~P ( 1 ... ( M + N ) ) )
19 1lt2 
 |-  1 < 2
20 1re 
 |-  1 e. RR
21 2re 
 |-  2 e. RR
22 20 21 ltnlei 
 |-  ( 1 < 2 <-> -. 2 <_ 1 )
23 19 22 mpbi 
 |-  -. 2 <_ 1
24 elfzle1 
 |-  ( 1 e. ( 2 ... ( M + N ) ) -> 2 <_ 1 )
25 23 24 mto 
 |-  -. 1 e. ( 2 ... ( M + N ) )
26 elelpwi 
 |-  ( ( 1 e. c /\ c e. ~P ( 2 ... ( M + N ) ) ) -> 1 e. ( 2 ... ( M + N ) ) )
27 25 26 mto 
 |-  -. ( 1 e. c /\ c e. ~P ( 2 ... ( M + N ) ) )
28 ancom 
 |-  ( ( 1 e. c /\ c e. ~P ( 2 ... ( M + N ) ) ) <-> ( c e. ~P ( 2 ... ( M + N ) ) /\ 1 e. c ) )
29 27 28 mtbi 
 |-  -. ( c e. ~P ( 2 ... ( M + N ) ) /\ 1 e. c )
30 29 imnani 
 |-  ( c e. ~P ( 2 ... ( M + N ) ) -> -. 1 e. c )
31 18 30 jca 
 |-  ( c e. ~P ( 2 ... ( M + N ) ) -> ( c e. ~P ( 1 ... ( M + N ) ) /\ -. 1 e. c ) )
32 ssin 
 |-  ( ( c C_ ( 1 ... ( M + N ) ) /\ c C_ { i | -. i = 1 } ) <-> c C_ ( ( 1 ... ( M + N ) ) i^i { i | -. i = 1 } ) )
33 1le2 
 |-  1 <_ 2
34 1p1e2 
 |-  ( 1 + 1 ) = 2
35 nnge1 
 |-  ( M e. NN -> 1 <_ M )
36 1 35 ax-mp 
 |-  1 <_ M
37 nnge1 
 |-  ( N e. NN -> 1 <_ N )
38 2 37 ax-mp 
 |-  1 <_ N
39 1 nnrei 
 |-  M e. RR
40 2 nnrei 
 |-  N e. RR
41 20 20 39 40 le2addi 
 |-  ( ( 1 <_ M /\ 1 <_ N ) -> ( 1 + 1 ) <_ ( M + N ) )
42 36 38 41 mp2an 
 |-  ( 1 + 1 ) <_ ( M + N )
43 34 42 eqbrtrri 
 |-  2 <_ ( M + N )
44 39 40 readdcli 
 |-  ( M + N ) e. RR
45 20 21 44 letri 
 |-  ( ( 1 <_ 2 /\ 2 <_ ( M + N ) ) -> 1 <_ ( M + N ) )
46 33 43 45 mp2an 
 |-  1 <_ ( M + N )
47 1z 
 |-  1 e. ZZ
48 nnaddcl 
 |-  ( ( M e. NN /\ N e. NN ) -> ( M + N ) e. NN )
49 1 2 48 mp2an 
 |-  ( M + N ) e. NN
50 49 nnzi 
 |-  ( M + N ) e. ZZ
51 eluz 
 |-  ( ( 1 e. ZZ /\ ( M + N ) e. ZZ ) -> ( ( M + N ) e. ( ZZ>= ` 1 ) <-> 1 <_ ( M + N ) ) )
52 47 50 51 mp2an 
 |-  ( ( M + N ) e. ( ZZ>= ` 1 ) <-> 1 <_ ( M + N ) )
53 46 52 mpbir 
 |-  ( M + N ) e. ( ZZ>= ` 1 )
54 elfzp12 
 |-  ( ( M + N ) e. ( ZZ>= ` 1 ) -> ( i e. ( 1 ... ( M + N ) ) <-> ( i = 1 \/ i e. ( ( 1 + 1 ) ... ( M + N ) ) ) ) )
55 53 54 ax-mp 
 |-  ( i e. ( 1 ... ( M + N ) ) <-> ( i = 1 \/ i e. ( ( 1 + 1 ) ... ( M + N ) ) ) )
56 55 biimpi 
 |-  ( i e. ( 1 ... ( M + N ) ) -> ( i = 1 \/ i e. ( ( 1 + 1 ) ... ( M + N ) ) ) )
57 56 orcanai 
 |-  ( ( i e. ( 1 ... ( M + N ) ) /\ -. i = 1 ) -> i e. ( ( 1 + 1 ) ... ( M + N ) ) )
58 34 oveq1i 
 |-  ( ( 1 + 1 ) ... ( M + N ) ) = ( 2 ... ( M + N ) )
59 57 58 eleqtrdi 
 |-  ( ( i e. ( 1 ... ( M + N ) ) /\ -. i = 1 ) -> i e. ( 2 ... ( M + N ) ) )
60 59 ss2abi 
 |-  { i | ( i e. ( 1 ... ( M + N ) ) /\ -. i = 1 ) } C_ { i | i e. ( 2 ... ( M + N ) ) }
61 inab 
 |-  ( { i | i e. ( 1 ... ( M + N ) ) } i^i { i | -. i = 1 } ) = { i | ( i e. ( 1 ... ( M + N ) ) /\ -. i = 1 ) }
62 abid2 
 |-  { i | i e. ( 1 ... ( M + N ) ) } = ( 1 ... ( M + N ) )
63 62 ineq1i 
 |-  ( { i | i e. ( 1 ... ( M + N ) ) } i^i { i | -. i = 1 } ) = ( ( 1 ... ( M + N ) ) i^i { i | -. i = 1 } )
64 61 63 eqtr3i 
 |-  { i | ( i e. ( 1 ... ( M + N ) ) /\ -. i = 1 ) } = ( ( 1 ... ( M + N ) ) i^i { i | -. i = 1 } )
65 abid2 
 |-  { i | i e. ( 2 ... ( M + N ) ) } = ( 2 ... ( M + N ) )
66 60 64 65 3sstr3i 
 |-  ( ( 1 ... ( M + N ) ) i^i { i | -. i = 1 } ) C_ ( 2 ... ( M + N ) )
67 sstr 
 |-  ( ( c C_ ( ( 1 ... ( M + N ) ) i^i { i | -. i = 1 } ) /\ ( ( 1 ... ( M + N ) ) i^i { i | -. i = 1 } ) C_ ( 2 ... ( M + N ) ) ) -> c C_ ( 2 ... ( M + N ) ) )
68 66 67 mpan2 
 |-  ( c C_ ( ( 1 ... ( M + N ) ) i^i { i | -. i = 1 } ) -> c C_ ( 2 ... ( M + N ) ) )
69 32 68 sylbi 
 |-  ( ( c C_ ( 1 ... ( M + N ) ) /\ c C_ { i | -. i = 1 } ) -> c C_ ( 2 ... ( M + N ) ) )
70 velpw 
 |-  ( c e. ~P ( 1 ... ( M + N ) ) <-> c C_ ( 1 ... ( M + N ) ) )
71 ssab 
 |-  ( c C_ { i | -. i = 1 } <-> A. i ( i e. c -> -. i = 1 ) )
72 df-ex 
 |-  ( E. i ( i = 1 /\ i e. c ) <-> -. A. i -. ( i = 1 /\ i e. c ) )
73 72 bicomi 
 |-  ( -. A. i -. ( i = 1 /\ i e. c ) <-> E. i ( i = 1 /\ i e. c ) )
74 73 con1bii 
 |-  ( -. E. i ( i = 1 /\ i e. c ) <-> A. i -. ( i = 1 /\ i e. c ) )
75 dfclel 
 |-  ( 1 e. c <-> E. i ( i = 1 /\ i e. c ) )
76 75 notbii 
 |-  ( -. 1 e. c <-> -. E. i ( i = 1 /\ i e. c ) )
77 imnang 
 |-  ( A. i ( i e. c -> -. i = 1 ) <-> A. i -. ( i e. c /\ i = 1 ) )
78 ancom 
 |-  ( ( i = 1 /\ i e. c ) <-> ( i e. c /\ i = 1 ) )
79 78 notbii 
 |-  ( -. ( i = 1 /\ i e. c ) <-> -. ( i e. c /\ i = 1 ) )
80 79 albii 
 |-  ( A. i -. ( i = 1 /\ i e. c ) <-> A. i -. ( i e. c /\ i = 1 ) )
81 77 80 bitr4i 
 |-  ( A. i ( i e. c -> -. i = 1 ) <-> A. i -. ( i = 1 /\ i e. c ) )
82 74 76 81 3bitr4ri 
 |-  ( A. i ( i e. c -> -. i = 1 ) <-> -. 1 e. c )
83 71 82 bitr2i 
 |-  ( -. 1 e. c <-> c C_ { i | -. i = 1 } )
84 70 83 anbi12i 
 |-  ( ( c e. ~P ( 1 ... ( M + N ) ) /\ -. 1 e. c ) <-> ( c C_ ( 1 ... ( M + N ) ) /\ c C_ { i | -. i = 1 } ) )
85 velpw 
 |-  ( c e. ~P ( 2 ... ( M + N ) ) <-> c C_ ( 2 ... ( M + N ) ) )
86 69 84 85 3imtr4i 
 |-  ( ( c e. ~P ( 1 ... ( M + N ) ) /\ -. 1 e. c ) -> c e. ~P ( 2 ... ( M + N ) ) )
87 31 86 impbii 
 |-  ( c e. ~P ( 2 ... ( M + N ) ) <-> ( c e. ~P ( 1 ... ( M + N ) ) /\ -. 1 e. c ) )
88 87 anbi1i 
 |-  ( ( c e. ~P ( 2 ... ( M + N ) ) /\ ( # ` c ) = M ) <-> ( ( c e. ~P ( 1 ... ( M + N ) ) /\ -. 1 e. c ) /\ ( # ` c ) = M ) )
89 3 rabeq2i 
 |-  ( c e. O <-> ( c e. ~P ( 1 ... ( M + N ) ) /\ ( # ` c ) = M ) )
90 89 anbi1i 
 |-  ( ( c e. O /\ -. 1 e. c ) <-> ( ( c e. ~P ( 1 ... ( M + N ) ) /\ ( # ` c ) = M ) /\ -. 1 e. c ) )
91 13 88 90 3bitr4i 
 |-  ( ( c e. ~P ( 2 ... ( M + N ) ) /\ ( # ` c ) = M ) <-> ( c e. O /\ -. 1 e. c ) )
92 91 rabbia2 
 |-  { c e. ~P ( 2 ... ( M + N ) ) | ( # ` c ) = M } = { c e. O | -. 1 e. c }
93 92 fveq2i 
 |-  ( # ` { c e. ~P ( 2 ... ( M + N ) ) | ( # ` c ) = M } ) = ( # ` { c e. O | -. 1 e. c } )
94 fzfi 
 |-  ( 2 ... ( M + N ) ) e. Fin
95 1 nnzi 
 |-  M e. ZZ
96 hashbc 
 |-  ( ( ( 2 ... ( M + N ) ) e. Fin /\ M e. ZZ ) -> ( ( # ` ( 2 ... ( M + N ) ) ) _C M ) = ( # ` { c e. ~P ( 2 ... ( M + N ) ) | ( # ` c ) = M } ) )
97 94 95 96 mp2an 
 |-  ( ( # ` ( 2 ... ( M + N ) ) ) _C M ) = ( # ` { c e. ~P ( 2 ... ( M + N ) ) | ( # ` c ) = M } )
98 2z 
 |-  2 e. ZZ
99 98 eluz1i 
 |-  ( ( M + N ) e. ( ZZ>= ` 2 ) <-> ( ( M + N ) e. ZZ /\ 2 <_ ( M + N ) ) )
100 50 43 99 mpbir2an 
 |-  ( M + N ) e. ( ZZ>= ` 2 )
101 hashfz 
 |-  ( ( M + N ) e. ( ZZ>= ` 2 ) -> ( # ` ( 2 ... ( M + N ) ) ) = ( ( ( M + N ) - 2 ) + 1 ) )
102 100 101 ax-mp 
 |-  ( # ` ( 2 ... ( M + N ) ) ) = ( ( ( M + N ) - 2 ) + 1 )
103 1 nncni 
 |-  M e. CC
104 2 nncni 
 |-  N e. CC
105 103 104 addcli 
 |-  ( M + N ) e. CC
106 2cn 
 |-  2 e. CC
107 ax-1cn 
 |-  1 e. CC
108 subadd23 
 |-  ( ( ( M + N ) e. CC /\ 2 e. CC /\ 1 e. CC ) -> ( ( ( M + N ) - 2 ) + 1 ) = ( ( M + N ) + ( 1 - 2 ) ) )
109 105 106 107 108 mp3an 
 |-  ( ( ( M + N ) - 2 ) + 1 ) = ( ( M + N ) + ( 1 - 2 ) )
110 106 107 negsubdi2i 
 |-  -u ( 2 - 1 ) = ( 1 - 2 )
111 2m1e1 
 |-  ( 2 - 1 ) = 1
112 111 negeqi 
 |-  -u ( 2 - 1 ) = -u 1
113 110 112 eqtr3i 
 |-  ( 1 - 2 ) = -u 1
114 113 oveq2i 
 |-  ( ( M + N ) + ( 1 - 2 ) ) = ( ( M + N ) + -u 1 )
115 102 109 114 3eqtri 
 |-  ( # ` ( 2 ... ( M + N ) ) ) = ( ( M + N ) + -u 1 )
116 105 107 negsubi 
 |-  ( ( M + N ) + -u 1 ) = ( ( M + N ) - 1 )
117 115 116 eqtri 
 |-  ( # ` ( 2 ... ( M + N ) ) ) = ( ( M + N ) - 1 )
118 117 oveq1i 
 |-  ( ( # ` ( 2 ... ( M + N ) ) ) _C M ) = ( ( ( M + N ) - 1 ) _C M )
119 97 118 eqtr3i 
 |-  ( # ` { c e. ~P ( 2 ... ( M + N ) ) | ( # ` c ) = M } ) = ( ( ( M + N ) - 1 ) _C M )
120 93 119 eqtr3i 
 |-  ( # ` { c e. O | -. 1 e. c } ) = ( ( ( M + N ) - 1 ) _C M )
121 1 2 3 ballotlem1 
 |-  ( # ` O ) = ( ( M + N ) _C M )
122 120 121 oveq12i 
 |-  ( ( # ` { c e. O | -. 1 e. c } ) / ( # ` O ) ) = ( ( ( ( M + N ) - 1 ) _C M ) / ( ( M + N ) _C M ) )
123 12 122 eqtri 
 |-  ( P ` { c e. O | -. 1 e. c } ) = ( ( ( ( M + N ) - 1 ) _C M ) / ( ( M + N ) _C M ) )
124 0le1 
 |-  0 <_ 1
125 0re 
 |-  0 e. RR
126 125 20 39 letri 
 |-  ( ( 0 <_ 1 /\ 1 <_ M ) -> 0 <_ M )
127 124 36 126 mp2an 
 |-  0 <_ M
128 2 nngt0i 
 |-  0 < N
129 40 128 elrpii 
 |-  N e. RR+
130 ltaddrp 
 |-  ( ( M e. RR /\ N e. RR+ ) -> M < ( M + N ) )
131 39 129 130 mp2an 
 |-  M < ( M + N )
132 0z 
 |-  0 e. ZZ
133 elfzm11 
 |-  ( ( 0 e. ZZ /\ ( M + N ) e. ZZ ) -> ( M e. ( 0 ... ( ( M + N ) - 1 ) ) <-> ( M e. ZZ /\ 0 <_ M /\ M < ( M + N ) ) ) )
134 132 50 133 mp2an 
 |-  ( M e. ( 0 ... ( ( M + N ) - 1 ) ) <-> ( M e. ZZ /\ 0 <_ M /\ M < ( M + N ) ) )
135 95 127 131 134 mpbir3an 
 |-  M e. ( 0 ... ( ( M + N ) - 1 ) )
136 bcm1n 
 |-  ( ( M e. ( 0 ... ( ( M + N ) - 1 ) ) /\ ( M + N ) e. NN ) -> ( ( ( ( M + N ) - 1 ) _C M ) / ( ( M + N ) _C M ) ) = ( ( ( M + N ) - M ) / ( M + N ) ) )
137 135 49 136 mp2an 
 |-  ( ( ( ( M + N ) - 1 ) _C M ) / ( ( M + N ) _C M ) ) = ( ( ( M + N ) - M ) / ( M + N ) )
138 pncan2 
 |-  ( ( M e. CC /\ N e. CC ) -> ( ( M + N ) - M ) = N )
139 103 104 138 mp2an 
 |-  ( ( M + N ) - M ) = N
140 139 oveq1i 
 |-  ( ( ( M + N ) - M ) / ( M + N ) ) = ( N / ( M + N ) )
141 123 137 140 3eqtri 
 |-  ( P ` { c e. O | -. 1 e. c } ) = ( N / ( M + N ) )