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 \in ℕ$
	ballotth.n	$⊢ N \in ℕ$
	ballotth.o	$⊢ O = \{c \in 𝒫 (1 \dots M + N) \| \|c\| = M\}$
	ballotth.p	$⊢ P = (x \in 𝒫 O ⟼ \frac{\|x\|}{\|O\|})$
Assertion	ballotlem2	$⊢ P (\{c \in O \| \neg 1 \in c\}) = \frac{N}{M + N}$

Proof

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

Metamath Proof Explorer

Theorem ballotlem2

Proof