Metamath Proof Explorer

Theorem ballotth

Description: 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)

Ref Expression
Hypotheses ballotth.m ⊢M∈ℕ
ballotth.n ⊢N∈ℕ
ballotth.o ⊢O=c∈𝒫1…M+N|c=M
ballotth.p ⊢P=x∈𝒫O⟼xO
ballotth.f ⊢F=c∈O⟼i∈ℤ⟼1…i∩c−1…i∖c
ballotth.e ⊢E=c∈O|∀i∈1…M+N0<F⁡c⁡i
ballotth.mgtn ⊢N<M
ballotth.i ⊢I=c∈O∖E⟼supk∈1…M+N|F⁡c⁡k=0ℝ<
ballotth.s ⊢S=c∈O∖E⟼i∈1…M+N⟼ifi≤I⁡cI⁡c+1-ii
ballotth.r ⊢R=c∈O∖E⟼S⁡cc
Assertion ballotth ⊢P⁡E=M−NM+N

Proof

Step Hyp Ref Expression
1 ballotth.m ⊢M∈ℕ
2 ballotth.n ⊢N∈ℕ
3 ballotth.o ⊢O=c∈𝒫1…M+N|c=M
4 ballotth.p ⊢P=x∈𝒫O⟼xO
5 ballotth.f ⊢F=c∈O⟼i∈ℤ⟼1…i∩c−1…i∖c
6 ballotth.e ⊢E=c∈O|∀i∈1…M+N0<F⁡c⁡i
7 ballotth.mgtn ⊢N<M
8 ballotth.i ⊢I=c∈O∖E⟼supk∈1…M+N|F⁡c⁡k=0ℝ<
9 ballotth.s ⊢S=c∈O∖E⟼i∈1…M+N⟼ifi≤I⁡cI⁡c+1-ii
10 ballotth.r ⊢R=c∈O∖E⟼S⁡cc
11 ssrab2 ⊢c∈O|∀i∈1…M+N0<F⁡c⁡i⊆O
12 6 11 eqsstri ⊢E⊆O
13 fzfi ⊢1…M+N∈Fin
14 pwfi ⊢1…M+N∈Fin↔𝒫1…M+N∈Fin
15 13 14 mpbi ⊢𝒫1…M+N∈Fin
16 ssrab2 ⊢c∈𝒫1…M+N|c=M⊆𝒫1…M+N
17 3 16 eqsstri ⊢O⊆𝒫1…M+N
18 ssfi ⊢𝒫1…M+N∈Fin∧O⊆𝒫1…M+N→O∈Fin
19 15 17 18 mp2an ⊢O∈Fin
20 ssfi ⊢O∈Fin∧E⊆O→E∈Fin
21 19 12 20 mp2an ⊢E∈Fin
22 21 elexi ⊢E∈V
23 22 elpw ⊢E∈𝒫O↔E⊆O
24 fveq2 ⊢x=E→x=E
25 24 oveq1d ⊢x=E→xO=EO
26 ovex ⊢EO∈V
27 25 4 26 fvmpt ⊢E∈𝒫O→P⁡E=EO
28 23 27 sylbir ⊢E⊆O→P⁡E=EO
29 12 28 ax-mp ⊢P⁡E=EO
30 hashssdif ⊢O∈Fin∧E⊆O→O∖E=O−E
31 19 12 30 mp2an ⊢O∖E=O−E
32 31 eqcomi ⊢O−E=O∖E
33 hashcl ⊢O∈Fin→O∈ℕ0
34 19 33 ax-mp ⊢O∈ℕ0
35 34 nn0cni ⊢O∈ℂ
36 hashcl ⊢E∈Fin→E∈ℕ0
37 21 36 ax-mp ⊢E∈ℕ0
38 37 nn0cni ⊢E∈ℂ
39 difss ⊢O∖E⊆O
40 ssfi ⊢O∈Fin∧O∖E⊆O→O∖E∈Fin
41 19 39 40 mp2an ⊢O∖E∈Fin
42 hashcl ⊢O∖E∈Fin→O∖E∈ℕ0
43 41 42 ax-mp ⊢O∖E∈ℕ0
44 43 nn0cni ⊢O∖E∈ℂ
45 35 38 44 subsub23i ⊢O−E=O∖E↔O−O∖E=E
46 32 45 mpbi ⊢O−O∖E=E
47 46 oveq1i ⊢O−O∖EO=EO
48 29 47 eqtr4i ⊢P⁡E=O−O∖EO
49 1 2 3 ballotlem1 ⊢O=(M+NM)
50 1 nnnn0i ⊢M∈ℕ0
51 nnaddcl ⊢M∈ℕ∧N∈ℕ→M+N∈ℕ
52 1 2 51 mp2an ⊢M+N∈ℕ
53 52 nnnn0i ⊢M+N∈ℕ0
54 1 nnrei ⊢M∈ℝ
55 2 nnnn0i ⊢N∈ℕ0
56 54 55 nn0addge1i ⊢M≤M+N
57 elfz2nn0 ⊢M∈0…M+N↔M∈ℕ0∧M+N∈ℕ0∧M≤M+N
58 50 53 56 57 mpbir3an ⊢M∈0…M+N
59 bccl2 ⊢M∈0…M+N→(M+NM)∈ℕ
60 58 59 ax-mp ⊢(M+NM)∈ℕ
61 60 nnne0i ⊢(M+NM)≠0
62 49 61 eqnetri ⊢O≠0
63 35 62 pm3.2i ⊢O∈ℂ∧O≠0
64 divsubdir ⊢O∈ℂ∧O∖E∈ℂ∧O∈ℂ∧O≠0→O−O∖EO=OO−O∖EO
65 35 44 63 64 mp3an ⊢O−O∖EO=OO−O∖EO
66 35 62 dividi ⊢OO=1
67 66 oveq1i ⊢OO−O∖EO=1−O∖EO
68 48 65 67 3eqtri ⊢P⁡E=1−O∖EO
69 1 2 3 4 5 6 7 8 9 10 ballotlem8 ⊢c∈O∖E|1∈c=c∈O∖E|¬1∈c
70 69 oveq1i ⊢c∈O∖E|1∈c+c∈O∖E|¬1∈c=c∈O∖E|¬1∈c+c∈O∖E|¬1∈c
71 70 oveq1i ⊢c∈O∖E|1∈c+c∈O∖E|¬1∈cO=c∈O∖E|¬1∈c+c∈O∖E|¬1∈cO
72 rabxm ⊢O∖E=c∈O∖E|1∈c∪c∈O∖E|¬1∈c
73 72 fveq2i ⊢O∖E=c∈O∖E|1∈c∪c∈O∖E|¬1∈c
74 ssrab2 ⊢c∈O∖E|1∈c⊆O∖E
75 74 39 sstri ⊢c∈O∖E|1∈c⊆O
76 75 17 sstri ⊢c∈O∖E|1∈c⊆𝒫1…M+N
77 ssfi ⊢𝒫1…M+N∈Fin∧c∈O∖E|1∈c⊆𝒫1…M+N→c∈O∖E|1∈c∈Fin
78 15 76 77 mp2an ⊢c∈O∖E|1∈c∈Fin
79 ssrab2 ⊢c∈O∖E|¬1∈c⊆O∖E
80 79 39 sstri ⊢c∈O∖E|¬1∈c⊆O
81 80 17 sstri ⊢c∈O∖E|¬1∈c⊆𝒫1…M+N
82 ssfi ⊢𝒫1…M+N∈Fin∧c∈O∖E|¬1∈c⊆𝒫1…M+N→c∈O∖E|¬1∈c∈Fin
83 15 81 82 mp2an ⊢c∈O∖E|¬1∈c∈Fin
84 rabnc ⊢c∈O∖E|1∈c∩c∈O∖E|¬1∈c=∅
85 hashun ⊢c∈O∖E|1∈c∈Fin∧c∈O∖E|¬1∈c∈Fin∧c∈O∖E|1∈c∩c∈O∖E|¬1∈c=∅→c∈O∖E|1∈c∪c∈O∖E|¬1∈c=c∈O∖E|1∈c+c∈O∖E|¬1∈c
86 78 83 84 85 mp3an ⊢c∈O∖E|1∈c∪c∈O∖E|¬1∈c=c∈O∖E|1∈c+c∈O∖E|¬1∈c
87 73 86 eqtri ⊢O∖E=c∈O∖E|1∈c+c∈O∖E|¬1∈c
88 87 oveq1i ⊢O∖EO=c∈O∖E|1∈c+c∈O∖E|¬1∈cO
89 ssrab2 ⊢c∈O|¬1∈c⊆O
90 19 elexi ⊢O∈V
91 90 elpw2 ⊢c∈O|¬1∈c∈𝒫O↔c∈O|¬1∈c⊆O
92 89 91 mpbir ⊢c∈O|¬1∈c∈𝒫O
93 fveq2 ⊢x=c∈O|¬1∈c→x=c∈O|¬1∈c
94 93 oveq1d ⊢x=c∈O|¬1∈c→xO=c∈O|¬1∈cO
95 ovex ⊢c∈O|¬1∈cO∈V
96 94 4 95 fvmpt ⊢c∈O|¬1∈c∈𝒫O→P⁡c∈O|¬1∈c=c∈O|¬1∈cO
97 92 96 ax-mp ⊢P⁡c∈O|¬1∈c=c∈O|¬1∈cO
98 1 2 3 4 ballotlem2 ⊢P⁡c∈O|¬1∈c=NM+N
99 nfrab1 ⊢Ⅎ_cc∈O|¬1∈c
100 nfrab1 ⊢Ⅎ_cc∈O∖E|¬1∈c
101 99 100 dfss2f ⊢c∈O|¬1∈c⊆c∈O∖E|¬1∈c↔∀cc∈c∈O|¬1∈c→c∈c∈O∖E|¬1∈c
102 1 2 3 4 5 6 ballotlem4 ⊢c∈O→¬1∈c→¬c∈E
103 102 imdistani ⊢c∈O∧¬1∈c→c∈O∧¬c∈E
104 rabid ⊢c∈c∈O|¬1∈c↔c∈O∧¬1∈c
105 eldif ⊢c∈O∖E↔c∈O∧¬c∈E
106 103 104 105 3imtr4i ⊢c∈c∈O|¬1∈c→c∈O∖E
107 104 simprbi ⊢c∈c∈O|¬1∈c→¬1∈c
108 rabid ⊢c∈c∈O∖E|¬1∈c↔c∈O∖E∧¬1∈c
109 106 107 108 sylanbrc ⊢c∈c∈O|¬1∈c→c∈c∈O∖E|¬1∈c
110 101 109 mpgbir ⊢c∈O|¬1∈c⊆c∈O∖E|¬1∈c
111 rabss2 ⊢O∖E⊆O→c∈O∖E|¬1∈c⊆c∈O|¬1∈c
112 39 111 ax-mp ⊢c∈O∖E|¬1∈c⊆c∈O|¬1∈c
113 110 112 eqssi ⊢c∈O|¬1∈c=c∈O∖E|¬1∈c
114 113 fveq2i ⊢c∈O|¬1∈c=c∈O∖E|¬1∈c
115 114 oveq1i ⊢c∈O|¬1∈cO=c∈O∖E|¬1∈cO
116 97 98 115 3eqtr3i ⊢NM+N=c∈O∖E|¬1∈cO
117 116 oveq2i ⊢2⁢NM+N=2⁢c∈O∖E|¬1∈cO
118 2cn ⊢2∈ℂ
119 hashcl ⊢c∈O∖E|¬1∈c∈Fin→c∈O∖E|¬1∈c∈ℕ0
120 83 119 ax-mp ⊢c∈O∖E|¬1∈c∈ℕ0
121 120 nn0cni ⊢c∈O∖E|¬1∈c∈ℂ
122 118 121 35 62 divassi ⊢2⁢c∈O∖E|¬1∈cO=2⁢c∈O∖E|¬1∈cO
123 121 2timesi ⊢2⁢c∈O∖E|¬1∈c=c∈O∖E|¬1∈c+c∈O∖E|¬1∈c
124 123 oveq1i ⊢2⁢c∈O∖E|¬1∈cO=c∈O∖E|¬1∈c+c∈O∖E|¬1∈cO
125 117 122 124 3eqtr2i ⊢2⁢NM+N=c∈O∖E|¬1∈c+c∈O∖E|¬1∈cO
126 71 88 125 3eqtr4ri ⊢2⁢NM+N=O∖EO
127 126 oveq2i ⊢1−2⁢NM+N=1−O∖EO
128 52 nncni ⊢M+N∈ℂ
129 2 nncni ⊢N∈ℂ
130 118 129 mulcli ⊢2⋅ N∈ℂ
131 52 nnne0i ⊢M+N≠0
132 128 131 pm3.2i ⊢M+N∈ℂ∧M+N≠0
133 divsubdir ⊢M+N∈ℂ∧2⋅ N∈ℂ∧M+N∈ℂ∧M+N≠0→M+N-2⋅ NM+N=M+NM+N−2⋅ NM+N
134 128 130 132 133 mp3an ⊢M+N-2⋅ NM+N=M+NM+N−2⋅ NM+N
135 129 2timesi ⊢2⋅ N=N+N
136 135 oveq2i ⊢M+N-2⋅ N=M+N-N+N
137 1 nncni ⊢M∈ℂ
138 137 129 129 129 addsub4i ⊢M+N-N+N=M−N+N-N
139 129 subidi ⊢N−N=0
140 139 oveq2i ⊢M−N+N-N=M-N+0
141 137 129 subcli ⊢M−N∈ℂ
142 141 addridi ⊢M-N+0=M−N
143 138 140 142 3eqtri ⊢M+N-N+N=M−N
144 136 143 eqtri ⊢M+N-2⋅ N=M−N
145 144 oveq1i ⊢M+N-2⋅ NM+N=M−NM+N
146 128 131 dividi ⊢M+NM+N=1
147 118 129 128 131 divassi ⊢2⋅ NM+N=2⁢NM+N
148 146 147 oveq12i ⊢M+NM+N−2⋅ NM+N=1−2⁢NM+N
149 134 145 148 3eqtr3ri ⊢1−2⁢NM+N=M−NM+N
150 68 127 149 3eqtr2i ⊢P⁡E=M−NM+N