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 ⟼ x O
ballotth.f ⊢ F = c ∈ O ⟼ i ∈ ℤ ⟼ 1 … i ∩ c − 1 … i ∖ c
ballotth.e ⊢ E = c ∈ O | ∀ i ∈ 1 … M + N 0 < F ⁡ c ⁡ i
ballotth.mgtn ⊢ N < M
ballotth.i ⊢ I = c ∈ O ∖ E ⟼ sup k ∈ 1 … M + N | F ⁡ c ⁡ k = 0 ℝ <
ballotth.s ⊢ S = c ∈ O ∖ E ⟼ i ∈ 1 … M + N ⟼ if i ≤ I ⁡ c I ⁡ c + 1 - i i
ballotth.r ⊢ R = c ∈ O ∖ E ⟼ S ⁡ c c
Assertion ballotth ⊢ P ⁡ E = M − N M + 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 ⟼ x O
5 ballotth.f ⊢ F = c ∈ O ⟼ i ∈ ℤ ⟼ 1 … i ∩ c − 1 … i ∖ c
6 ballotth.e ⊢ E = c ∈ O | ∀ i ∈ 1 … M + N 0 < F ⁡ c ⁡ i
7 ballotth.mgtn ⊢ N < M
8 ballotth.i ⊢ I = c ∈ O ∖ E ⟼ sup k ∈ 1 … M + N | F ⁡ c ⁡ k = 0 ℝ <
9 ballotth.s ⊢ S = c ∈ O ∖ E ⟼ i ∈ 1 … M + N ⟼ if i ≤ I ⁡ c I ⁡ c + 1 - i i
10 ballotth.r ⊢ R = c ∈ O ∖ E ⟼ S ⁡ c c
11 ssrab2 ⊢ c ∈ O | ∀ i ∈ 1 … M + N 0 < 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 → x O = E O
26 ovex ⊢ E O ∈ V
27 25 4 26 fvmpt ⊢ E ∈ 𝒫 O → P ⁡ E = E O
28 23 27 sylbir ⊢ E ⊆ O → P ⁡ E = E O
29 12 28 ax-mp ⊢ P ⁡ E = E O
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 ∖ E O = E O
48 29 47 eqtr4i ⊢ P ⁡ E = O − O ∖ E O
49 1 2 3 ballotlem1 ⊢ O = ( M + N M)
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 + N M) ∈ ℕ
60 58 59 ax-mp ⊢ ( M + N M) ∈ ℕ
61 60 nnne0i ⊢ ( M + N M) ≠ 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 ∖ E O = O O − O ∖ E O
65 35 44 63 64 mp3an ⊢ O − O ∖ E O = O O − O ∖ E O
66 35 62 dividi ⊢ O O = 1
67 66 oveq1i ⊢ O O − O ∖ E O = 1 − O ∖ E O
68 48 65 67 3eqtri ⊢ P ⁡ E = 1 − O ∖ E O
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 ∈ c O = c ∈ O ∖ E | ¬ 1 ∈ c + c ∈ O ∖ E | ¬ 1 ∈ c O
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 ∖ E O = c ∈ O ∖ E | 1 ∈ c + c ∈ O ∖ E | ¬ 1 ∈ c O
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 → x O = c ∈ O | ¬ 1 ∈ c O
95 ovex ⊢ c ∈ O | ¬ 1 ∈ c O ∈ V
96 94 4 95 fvmpt ⊢ c ∈ O | ¬ 1 ∈ c ∈ 𝒫 O → P ⁡ c ∈ O | ¬ 1 ∈ c = c ∈ O | ¬ 1 ∈ c O
97 92 96 ax-mp ⊢ P ⁡ c ∈ O | ¬ 1 ∈ c = c ∈ O | ¬ 1 ∈ c O
98 1 2 3 4 ballotlem2 ⊢ P ⁡ c ∈ O | ¬ 1 ∈ c = N M + N
99 nfrab1 ⊢ Ⅎ _ c c ∈ O | ¬ 1 ∈ c
100 nfrab1 ⊢ Ⅎ _ c c ∈ O ∖ E | ¬ 1 ∈ c
101 99 100 dfss2f ⊢ c ∈ O | ¬ 1 ∈ c ⊆ c ∈ O ∖ E | ¬ 1 ∈ c ↔ ∀ c c ∈ 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 ∈ c O = c ∈ O ∖ E | ¬ 1 ∈ c O
116 97 98 115 3eqtr3i ⊢ N M + N = c ∈ O ∖ E | ¬ 1 ∈ c O
117 116 oveq2i ⊢ 2 ⁢ N M + N = 2 ⁢ c ∈ O ∖ E | ¬ 1 ∈ c O
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 ∈ c O = 2 ⁢ c ∈ O ∖ E | ¬ 1 ∈ c O
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 ∈ c O = c ∈ O ∖ E | ¬ 1 ∈ c + c ∈ O ∖ E | ¬ 1 ∈ c O
125 117 122 124 3eqtr2i ⊢ 2 ⁢ N M + N = c ∈ O ∖ E | ¬ 1 ∈ c + c ∈ O ∖ E | ¬ 1 ∈ c O
126 71 88 125 3eqtr4ri ⊢ 2 ⁢ N M + N = O ∖ E O
127 126 oveq2i ⊢ 1 − 2 ⁢ N M + N = 1 − O ∖ E O
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 ⋅ N M + N = M + N M + N − 2 ⋅ N M + N
134 128 130 132 133 mp3an ⊢ M + N - 2 ⋅ N M + N = M + N M + N − 2 ⋅ N M + 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 addid1i ⊢ 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 ⋅ N M + N = M − N M + N
146 128 131 dividi ⊢ M + N M + N = 1
147 118 129 128 131 divassi ⊢ 2 ⋅ N M + N = 2 ⁢ N M + N
148 146 147 oveq12i ⊢ M + N M + N − 2 ⋅ N M + N = 1 − 2 ⁢ N M + N
149 134 145 148 3eqtr3ri ⊢ 1 − 2 ⁢ N M + N = M − N M + N
150 68 127 149 3eqtr2i ⊢ P ⁡ E = M − N M + N