ballotlem2 - Mathbox for Thierry Arnoux

	Mathbox for Thierry Arnoux		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > Mathboxes > ballotlem2		Structured version Visualization version GIF version

Theorem ballotlem2 33785

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

**Hypotheses**
Ref	Expression
ballotth.m	⊢ 𝑀 ∈ ℕ
ballotth.n	⊢ 𝑁 ∈ ℕ
ballotth.o	⊢ 𝑂 = {𝑐 ∈ 𝒫 (1...(𝑀 + 𝑁)) ∣ (♯‘𝑐) = 𝑀}
ballotth.p	⊢ 𝑃 = (𝑥 ∈ 𝒫 𝑂 ↦ ((♯‘𝑥) / (♯‘𝑂)))

**Assertion**
Ref	Expression
ballotlem2	⊢ (𝑃‘{𝑐 ∈ 𝑂 ∣ ¬ 1 ∈ 𝑐}) = (𝑁 / (𝑀 + 𝑁))

Distinct variable groups: 𝑀,𝑐 𝑁,𝑐 𝑂,𝑐,𝑥 Allowed substitution hints: 𝑃(𝑥,𝑐) 𝑀(𝑥) 𝑁(𝑥)

Proof of Theorem ballotlem2 Dummy variable 𝑖 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		ballotth.m	. . . . . 6 ⊢ 𝑀 ∈ ℕ
2		ballotth.n	. . . . . 6 ⊢ 𝑁 ∈ ℕ
3		ballotth.o	. . . . . 6 ⊢ 𝑂 = {𝑐 ∈ 𝒫 (1...(𝑀 + 𝑁)) ∣ (♯‘𝑐) = 𝑀}
4	1, 2, 3	ballotlemoex 33782	. . . . 5 ⊢ 𝑂 ∈ V
5		ssrab2 4076	. . . . 5 ⊢ {𝑐 ∈ 𝑂 ∣ ¬ 1 ∈ 𝑐} ⊆ 𝑂
6	4, 5	elpwi2 5345	. . . 4 ⊢ {𝑐 ∈ 𝑂 ∣ ¬ 1 ∈ 𝑐} ∈ 𝒫 𝑂
7		fveq2 6890	. . . . . 6 ⊢ (𝑥 = {𝑐 ∈ 𝑂 ∣ ¬ 1 ∈ 𝑐} → (♯‘𝑥) = (♯‘{𝑐 ∈ 𝑂 ∣ ¬ 1 ∈ 𝑐}))
8	7	oveq1d 7426	. . . . 5 ⊢ (𝑥 = {𝑐 ∈ 𝑂 ∣ ¬ 1 ∈ 𝑐} → ((♯‘𝑥) / (♯‘𝑂)) = ((♯‘{𝑐 ∈ 𝑂 ∣ ¬ 1 ∈ 𝑐}) / (♯‘𝑂)))
9		ballotth.p	. . . . 5 ⊢ 𝑃 = (𝑥 ∈ 𝒫 𝑂 ↦ ((♯‘𝑥) / (♯‘𝑂)))
10		ovex 7444	. . . . 5 ⊢ ((♯‘{𝑐 ∈ 𝑂 ∣ ¬ 1 ∈ 𝑐}) / (♯‘𝑂)) ∈ V
11	8, 9, 10	fvmpt 6997	. . . 4 ⊢ ({𝑐 ∈ 𝑂 ∣ ¬ 1 ∈ 𝑐} ∈ 𝒫 𝑂 → (𝑃‘{𝑐 ∈ 𝑂 ∣ ¬ 1 ∈ 𝑐}) = ((♯‘{𝑐 ∈ 𝑂 ∣ ¬ 1 ∈ 𝑐}) / (♯‘𝑂)))
12	6, 11	ax-mp 5	. . 3 ⊢ (𝑃‘{𝑐 ∈ 𝑂 ∣ ¬ 1 ∈ 𝑐}) = ((♯‘{𝑐 ∈ 𝑂 ∣ ¬ 1 ∈ 𝑐}) / (♯‘𝑂))
13		an32 642	. . . . . . . 8 ⊢ (((𝑐 ∈ 𝒫 (1...(𝑀 + 𝑁)) ∧ ¬ 1 ∈ 𝑐) ∧ (♯‘𝑐) = 𝑀) ↔ ((𝑐 ∈ 𝒫 (1...(𝑀 + 𝑁)) ∧ (♯‘𝑐) = 𝑀) ∧ ¬ 1 ∈ 𝑐))
14		2eluzge1 12882	. . . . . . . . . . . . . 14 ⊢ 2 ∈ (ℤ_≥‘1)
15		fzss1 13544	. . . . . . . . . . . . . 14 ⊢ (2 ∈ (ℤ_≥‘1) → (2...(𝑀 + 𝑁)) ⊆ (1...(𝑀 + 𝑁)))
16	14, 15	ax-mp 5	. . . . . . . . . . . . 13 ⊢ (2...(𝑀 + 𝑁)) ⊆ (1...(𝑀 + 𝑁))
17	16	sspwi 4613	. . . . . . . . . . . 12 ⊢ 𝒫 (2...(𝑀 + 𝑁)) ⊆ 𝒫 (1...(𝑀 + 𝑁))
18	17	sseli 3977	. . . . . . . . . . 11 ⊢ (𝑐 ∈ 𝒫 (2...(𝑀 + 𝑁)) → 𝑐 ∈ 𝒫 (1...(𝑀 + 𝑁)))
19		1lt2 12387	. . . . . . . . . . . . . . . 16 ⊢ 1 < 2
20		1re 11218	. . . . . . . . . . . . . . . . 17 ⊢ 1 ∈ ℝ
21		2re 12290	. . . . . . . . . . . . . . . . 17 ⊢ 2 ∈ ℝ
22	20, 21	ltnlei 11339	. . . . . . . . . . . . . . . 16 ⊢ (1 < 2 ↔ ¬ 2 ≤ 1)
23	19, 22	mpbi 229	. . . . . . . . . . . . . . 15 ⊢ ¬ 2 ≤ 1
24		elfzle1 13508	. . . . . . . . . . . . . . 15 ⊢ (1 ∈ (2...(𝑀 + 𝑁)) → 2 ≤ 1)
25	23, 24	mto 196	. . . . . . . . . . . . . 14 ⊢ ¬ 1 ∈ (2...(𝑀 + 𝑁))
26		elelpwi 4611	. . . . . . . . . . . . . 14 ⊢ ((1 ∈ 𝑐 ∧ 𝑐 ∈ 𝒫 (2...(𝑀 + 𝑁))) → 1 ∈ (2...(𝑀 + 𝑁)))
27	25, 26	mto 196	. . . . . . . . . . . . 13 ⊢ ¬ (1 ∈ 𝑐 ∧ 𝑐 ∈ 𝒫 (2...(𝑀 + 𝑁)))
28		ancom 459	. . . . . . . . . . . . 13 ⊢ ((1 ∈ 𝑐 ∧ 𝑐 ∈ 𝒫 (2...(𝑀 + 𝑁))) ↔ (𝑐 ∈ 𝒫 (2...(𝑀 + 𝑁)) ∧ 1 ∈ 𝑐))
29	27, 28	mtbi 321	. . . . . . . . . . . 12 ⊢ ¬ (𝑐 ∈ 𝒫 (2...(𝑀 + 𝑁)) ∧ 1 ∈ 𝑐)
30	29	imnani 399	. . . . . . . . . . 11 ⊢ (𝑐 ∈ 𝒫 (2...(𝑀 + 𝑁)) → ¬ 1 ∈ 𝑐)
31	18, 30	jca 510	. . . . . . . . . 10 ⊢ (𝑐 ∈ 𝒫 (2...(𝑀 + 𝑁)) → (𝑐 ∈ 𝒫 (1...(𝑀 + 𝑁)) ∧ ¬ 1 ∈ 𝑐))
32		ssin 4229	. . . . . . . . . . . 12 ⊢ ((𝑐 ⊆ (1...(𝑀 + 𝑁)) ∧ 𝑐 ⊆ {𝑖 ∣ ¬ 𝑖 = 1}) ↔ 𝑐 ⊆ ((1...(𝑀 + 𝑁)) ∩ {𝑖 ∣ ¬ 𝑖 = 1}))
33		1le2 12425	. . . . . . . . . . . . . . . . . . . . 21 ⊢ 1 ≤ 2
34		1p1e2 12341	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (1 + 1) = 2
35		nnge1 12244	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑀 ∈ ℕ → 1 ≤ 𝑀)
36	1, 35	ax-mp 5	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ 1 ≤ 𝑀
37		nnge1 12244	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑁 ∈ ℕ → 1 ≤ 𝑁)
38	2, 37	ax-mp 5	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ 1 ≤ 𝑁
39	1	nnrei 12225	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ 𝑀 ∈ ℝ
40	2	nnrei 12225	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ 𝑁 ∈ ℝ
41	20, 20, 39, 40	le2addi 11781	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((1 ≤ 𝑀 ∧ 1 ≤ 𝑁) → (1 + 1) ≤ (𝑀 + 𝑁))
42	36, 38, 41	mp2an 688	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (1 + 1) ≤ (𝑀 + 𝑁)
43	34, 42	eqbrtrri 5170	. . . . . . . . . . . . . . . . . . . . 21 ⊢ 2 ≤ (𝑀 + 𝑁)
44	39, 40	readdcli 11233	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑀 + 𝑁) ∈ ℝ
45	20, 21, 44	letri 11347	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((1 ≤ 2 ∧ 2 ≤ (𝑀 + 𝑁)) → 1 ≤ (𝑀 + 𝑁))
46	33, 43, 45	mp2an 688	. . . . . . . . . . . . . . . . . . . 20 ⊢ 1 ≤ (𝑀 + 𝑁)
47		1z 12596	. . . . . . . . . . . . . . . . . . . . 21 ⊢ 1 ∈ ℤ
48		nnaddcl 12239	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) → (𝑀 + 𝑁) ∈ ℕ)
49	1, 2, 48	mp2an 688	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑀 + 𝑁) ∈ ℕ
50	49	nnzi 12590	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑀 + 𝑁) ∈ ℤ
51		eluz 12840	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((1 ∈ ℤ ∧ (𝑀 + 𝑁) ∈ ℤ) → ((𝑀 + 𝑁) ∈ (ℤ_≥‘1) ↔ 1 ≤ (𝑀 + 𝑁)))
52	47, 50, 51	mp2an 688	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑀 + 𝑁) ∈ (ℤ_≥‘1) ↔ 1 ≤ (𝑀 + 𝑁))
53	46, 52	mpbir 230	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑀 + 𝑁) ∈ (ℤ_≥‘1)
54		elfzp12 13584	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑀 + 𝑁) ∈ (ℤ_≥‘1) → (𝑖 ∈ (1...(𝑀 + 𝑁)) ↔ (𝑖 = 1 ∨ 𝑖 ∈ ((1 + 1)...(𝑀 + 𝑁)))))
55	53, 54	ax-mp 5	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑖 ∈ (1...(𝑀 + 𝑁)) ↔ (𝑖 = 1 ∨ 𝑖 ∈ ((1 + 1)...(𝑀 + 𝑁))))
56	55	biimpi 215	. . . . . . . . . . . . . . . . 17 ⊢ (𝑖 ∈ (1...(𝑀 + 𝑁)) → (𝑖 = 1 ∨ 𝑖 ∈ ((1 + 1)...(𝑀 + 𝑁))))
57	56	orcanai 999	. . . . . . . . . . . . . . . 16 ⊢ ((𝑖 ∈ (1...(𝑀 + 𝑁)) ∧ ¬ 𝑖 = 1) → 𝑖 ∈ ((1 + 1)...(𝑀 + 𝑁)))
58	34	oveq1i 7421	. . . . . . . . . . . . . . . 16 ⊢ ((1 + 1)...(𝑀 + 𝑁)) = (2...(𝑀 + 𝑁))
59	57, 58	eleqtrdi 2841	. . . . . . . . . . . . . . 15 ⊢ ((𝑖 ∈ (1...(𝑀 + 𝑁)) ∧ ¬ 𝑖 = 1) → 𝑖 ∈ (2...(𝑀 + 𝑁)))
60	59	ss2abi 4062	. . . . . . . . . . . . . 14 ⊢ {𝑖 ∣ (𝑖 ∈ (1...(𝑀 + 𝑁)) ∧ ¬ 𝑖 = 1)} ⊆ {𝑖 ∣ 𝑖 ∈ (2...(𝑀 + 𝑁))}
61		inab 4298	. . . . . . . . . . . . . . 15 ⊢ ({𝑖 ∣ 𝑖 ∈ (1...(𝑀 + 𝑁))} ∩ {𝑖 ∣ ¬ 𝑖 = 1}) = {𝑖 ∣ (𝑖 ∈ (1...(𝑀 + 𝑁)) ∧ ¬ 𝑖 = 1)}
62		abid2 2869	. . . . . . . . . . . . . . . 16 ⊢ {𝑖 ∣ 𝑖 ∈ (1...(𝑀 + 𝑁))} = (1...(𝑀 + 𝑁))
63	62	ineq1i 4207	. . . . . . . . . . . . . . 15 ⊢ ({𝑖 ∣ 𝑖 ∈ (1...(𝑀 + 𝑁))} ∩ {𝑖 ∣ ¬ 𝑖 = 1}) = ((1...(𝑀 + 𝑁)) ∩ {𝑖 ∣ ¬ 𝑖 = 1})
64	61, 63	eqtr3i 2760	. . . . . . . . . . . . . 14 ⊢ {𝑖 ∣ (𝑖 ∈ (1...(𝑀 + 𝑁)) ∧ ¬ 𝑖 = 1)} = ((1...(𝑀 + 𝑁)) ∩ {𝑖 ∣ ¬ 𝑖 = 1})
65		abid2 2869	. . . . . . . . . . . . . 14 ⊢ {𝑖 ∣ 𝑖 ∈ (2...(𝑀 + 𝑁))} = (2...(𝑀 + 𝑁))
66	60, 64, 65	3sstr3i 4023	. . . . . . . . . . . . 13 ⊢ ((1...(𝑀 + 𝑁)) ∩ {𝑖 ∣ ¬ 𝑖 = 1}) ⊆ (2...(𝑀 + 𝑁))
67		sstr 3989	. . . . . . . . . . . . 13 ⊢ ((𝑐 ⊆ ((1...(𝑀 + 𝑁)) ∩ {𝑖 ∣ ¬ 𝑖 = 1}) ∧ ((1...(𝑀 + 𝑁)) ∩ {𝑖 ∣ ¬ 𝑖 = 1}) ⊆ (2...(𝑀 + 𝑁))) → 𝑐 ⊆ (2...(𝑀 + 𝑁)))
68	66, 67	mpan2 687	. . . . . . . . . . . 12 ⊢ (𝑐 ⊆ ((1...(𝑀 + 𝑁)) ∩ {𝑖 ∣ ¬ 𝑖 = 1}) → 𝑐 ⊆ (2...(𝑀 + 𝑁)))
69	32, 68	sylbi 216	. . . . . . . . . . 11 ⊢ ((𝑐 ⊆ (1...(𝑀 + 𝑁)) ∧ 𝑐 ⊆ {𝑖 ∣ ¬ 𝑖 = 1}) → 𝑐 ⊆ (2...(𝑀 + 𝑁)))
70		velpw 4606	. . . . . . . . . . . 12 ⊢ (𝑐 ∈ 𝒫 (1...(𝑀 + 𝑁)) ↔ 𝑐 ⊆ (1...(𝑀 + 𝑁)))
71		ssab 4057	. . . . . . . . . . . . 13 ⊢ (𝑐 ⊆ {𝑖 ∣ ¬ 𝑖 = 1} ↔ ∀𝑖(𝑖 ∈ 𝑐 → ¬ 𝑖 = 1))
72		df-ex 1780	. . . . . . . . . . . . . . . 16 ⊢ (∃𝑖(𝑖 = 1 ∧ 𝑖 ∈ 𝑐) ↔ ¬ ∀𝑖 ¬ (𝑖 = 1 ∧ 𝑖 ∈ 𝑐))
73	72	bicomi 223	. . . . . . . . . . . . . . 15 ⊢ (¬ ∀𝑖 ¬ (𝑖 = 1 ∧ 𝑖 ∈ 𝑐) ↔ ∃𝑖(𝑖 = 1 ∧ 𝑖 ∈ 𝑐))
74	73	con1bii 355	. . . . . . . . . . . . . 14 ⊢ (¬ ∃𝑖(𝑖 = 1 ∧ 𝑖 ∈ 𝑐) ↔ ∀𝑖 ¬ (𝑖 = 1 ∧ 𝑖 ∈ 𝑐))
75		dfclel 2809	. . . . . . . . . . . . . . 15 ⊢ (1 ∈ 𝑐 ↔ ∃𝑖(𝑖 = 1 ∧ 𝑖 ∈ 𝑐))
76	75	notbii 319	. . . . . . . . . . . . . 14 ⊢ (¬ 1 ∈ 𝑐 ↔ ¬ ∃𝑖(𝑖 = 1 ∧ 𝑖 ∈ 𝑐))
77		imnang 1842	. . . . . . . . . . . . . . 15 ⊢ (∀𝑖(𝑖 ∈ 𝑐 → ¬ 𝑖 = 1) ↔ ∀𝑖 ¬ (𝑖 ∈ 𝑐 ∧ 𝑖 = 1))
78		ancom 459	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑖 = 1 ∧ 𝑖 ∈ 𝑐) ↔ (𝑖 ∈ 𝑐 ∧ 𝑖 = 1))
79	78	notbii 319	. . . . . . . . . . . . . . . 16 ⊢ (¬ (𝑖 = 1 ∧ 𝑖 ∈ 𝑐) ↔ ¬ (𝑖 ∈ 𝑐 ∧ 𝑖 = 1))
80	79	albii 1819	. . . . . . . . . . . . . . 15 ⊢ (∀𝑖 ¬ (𝑖 = 1 ∧ 𝑖 ∈ 𝑐) ↔ ∀𝑖 ¬ (𝑖 ∈ 𝑐 ∧ 𝑖 = 1))
81	77, 80	bitr4i 277	. . . . . . . . . . . . . 14 ⊢ (∀𝑖(𝑖 ∈ 𝑐 → ¬ 𝑖 = 1) ↔ ∀𝑖 ¬ (𝑖 = 1 ∧ 𝑖 ∈ 𝑐))
82	74, 76, 81	3bitr4ri 303	. . . . . . . . . . . . 13 ⊢ (∀𝑖(𝑖 ∈ 𝑐 → ¬ 𝑖 = 1) ↔ ¬ 1 ∈ 𝑐)
83	71, 82	bitr2i 275	. . . . . . . . . . . 12 ⊢ (¬ 1 ∈ 𝑐 ↔ 𝑐 ⊆ {𝑖 ∣ ¬ 𝑖 = 1})
84	70, 83	anbi12i 625	. . . . . . . . . . 11 ⊢ ((𝑐 ∈ 𝒫 (1...(𝑀 + 𝑁)) ∧ ¬ 1 ∈ 𝑐) ↔ (𝑐 ⊆ (1...(𝑀 + 𝑁)) ∧ 𝑐 ⊆ {𝑖 ∣ ¬ 𝑖 = 1}))
85		velpw 4606	. . . . . . . . . . 11 ⊢ (𝑐 ∈ 𝒫 (2...(𝑀 + 𝑁)) ↔ 𝑐 ⊆ (2...(𝑀 + 𝑁)))
86	69, 84, 85	3imtr4i 291	. . . . . . . . . 10 ⊢ ((𝑐 ∈ 𝒫 (1...(𝑀 + 𝑁)) ∧ ¬ 1 ∈ 𝑐) → 𝑐 ∈ 𝒫 (2...(𝑀 + 𝑁)))
87	31, 86	impbii 208	. . . . . . . . 9 ⊢ (𝑐 ∈ 𝒫 (2...(𝑀 + 𝑁)) ↔ (𝑐 ∈ 𝒫 (1...(𝑀 + 𝑁)) ∧ ¬ 1 ∈ 𝑐))
88	87	anbi1i 622	. . . . . . . 8 ⊢ ((𝑐 ∈ 𝒫 (2...(𝑀 + 𝑁)) ∧ (♯‘𝑐) = 𝑀) ↔ ((𝑐 ∈ 𝒫 (1...(𝑀 + 𝑁)) ∧ ¬ 1 ∈ 𝑐) ∧ (♯‘𝑐) = 𝑀))
89	3	reqabi 3452	. . . . . . . . 9 ⊢ (𝑐 ∈ 𝑂 ↔ (𝑐 ∈ 𝒫 (1...(𝑀 + 𝑁)) ∧ (♯‘𝑐) = 𝑀))
90	89	anbi1i 622	. . . . . . . 8 ⊢ ((𝑐 ∈ 𝑂 ∧ ¬ 1 ∈ 𝑐) ↔ ((𝑐 ∈ 𝒫 (1...(𝑀 + 𝑁)) ∧ (♯‘𝑐) = 𝑀) ∧ ¬ 1 ∈ 𝑐))
91	13, 88, 90	3bitr4i 302	. . . . . . 7 ⊢ ((𝑐 ∈ 𝒫 (2...(𝑀 + 𝑁)) ∧ (♯‘𝑐) = 𝑀) ↔ (𝑐 ∈ 𝑂 ∧ ¬ 1 ∈ 𝑐))
92	91	rabbia2 3433	. . . . . 6 ⊢ {𝑐 ∈ 𝒫 (2...(𝑀 + 𝑁)) ∣ (♯‘𝑐) = 𝑀} = {𝑐 ∈ 𝑂 ∣ ¬ 1 ∈ 𝑐}
93	92	fveq2i 6893	. . . . 5 ⊢ (♯‘{𝑐 ∈ 𝒫 (2...(𝑀 + 𝑁)) ∣ (♯‘𝑐) = 𝑀}) = (♯‘{𝑐 ∈ 𝑂 ∣ ¬ 1 ∈ 𝑐})
94		fzfi 13941	. . . . . . 7 ⊢ (2...(𝑀 + 𝑁)) ∈ Fin
95	1	nnzi 12590	. . . . . . 7 ⊢ 𝑀 ∈ ℤ
96		hashbc 14416	. . . . . . 7 ⊢ (((2...(𝑀 + 𝑁)) ∈ Fin ∧ 𝑀 ∈ ℤ) → ((♯‘(2...(𝑀 + 𝑁)))C𝑀) = (♯‘{𝑐 ∈ 𝒫 (2...(𝑀 + 𝑁)) ∣ (♯‘𝑐) = 𝑀}))
97	94, 95, 96	mp2an 688	. . . . . 6 ⊢ ((♯‘(2...(𝑀 + 𝑁)))C𝑀) = (♯‘{𝑐 ∈ 𝒫 (2...(𝑀 + 𝑁)) ∣ (♯‘𝑐) = 𝑀})
98		2z 12598	. . . . . . . . . . . 12 ⊢ 2 ∈ ℤ
99	98	eluz1i 12834	. . . . . . . . . . 11 ⊢ ((𝑀 + 𝑁) ∈ (ℤ_≥‘2) ↔ ((𝑀 + 𝑁) ∈ ℤ ∧ 2 ≤ (𝑀 + 𝑁)))
100	50, 43, 99	mpbir2an 707	. . . . . . . . . 10 ⊢ (𝑀 + 𝑁) ∈ (ℤ_≥‘2)
101		hashfz 14391	. . . . . . . . . 10 ⊢ ((𝑀 + 𝑁) ∈ (ℤ_≥‘2) → (♯‘(2...(𝑀 + 𝑁))) = (((𝑀 + 𝑁) − 2) + 1))
102	100, 101	ax-mp 5	. . . . . . . . 9 ⊢ (♯‘(2...(𝑀 + 𝑁))) = (((𝑀 + 𝑁) − 2) + 1)
103	1	nncni 12226	. . . . . . . . . . 11 ⊢ 𝑀 ∈ ℂ
104	2	nncni 12226	. . . . . . . . . . 11 ⊢ 𝑁 ∈ ℂ
105	103, 104	addcli 11224	. . . . . . . . . 10 ⊢ (𝑀 + 𝑁) ∈ ℂ
106		2cn 12291	. . . . . . . . . 10 ⊢ 2 ∈ ℂ
107		ax-1cn 11170	. . . . . . . . . 10 ⊢ 1 ∈ ℂ
108		subadd23 11476	. . . . . . . . . 10 ⊢ (((𝑀 + 𝑁) ∈ ℂ ∧ 2 ∈ ℂ ∧ 1 ∈ ℂ) → (((𝑀 + 𝑁) − 2) + 1) = ((𝑀 + 𝑁) + (1 − 2)))
109	105, 106, 107, 108	mp3an 1459	. . . . . . . . 9 ⊢ (((𝑀 + 𝑁) − 2) + 1) = ((𝑀 + 𝑁) + (1 − 2))
110	106, 107	negsubdi2i 11550	. . . . . . . . . . 11 ⊢ -(2 − 1) = (1 − 2)
111		2m1e1 12342	. . . . . . . . . . . 12 ⊢ (2 − 1) = 1
112	111	negeqi 11457	. . . . . . . . . . 11 ⊢ -(2 − 1) = -1
113	110, 112	eqtr3i 2760	. . . . . . . . . 10 ⊢ (1 − 2) = -1
114	113	oveq2i 7422	. . . . . . . . 9 ⊢ ((𝑀 + 𝑁) + (1 − 2)) = ((𝑀 + 𝑁) + -1)
115	102, 109, 114	3eqtri 2762	. . . . . . . 8 ⊢ (♯‘(2...(𝑀 + 𝑁))) = ((𝑀 + 𝑁) + -1)
116	105, 107	negsubi 11542	. . . . . . . 8 ⊢ ((𝑀 + 𝑁) + -1) = ((𝑀 + 𝑁) − 1)
117	115, 116	eqtri 2758	. . . . . . 7 ⊢ (♯‘(2...(𝑀 + 𝑁))) = ((𝑀 + 𝑁) − 1)
118	117	oveq1i 7421	. . . . . 6 ⊢ ((♯‘(2...(𝑀 + 𝑁)))C𝑀) = (((𝑀 + 𝑁) − 1)C𝑀)
119	97, 118	eqtr3i 2760	. . . . 5 ⊢ (♯‘{𝑐 ∈ 𝒫 (2...(𝑀 + 𝑁)) ∣ (♯‘𝑐) = 𝑀}) = (((𝑀 + 𝑁) − 1)C𝑀)
120	93, 119	eqtr3i 2760	. . . 4 ⊢ (♯‘{𝑐 ∈ 𝑂 ∣ ¬ 1 ∈ 𝑐}) = (((𝑀 + 𝑁) − 1)C𝑀)
121	1, 2, 3	ballotlem1 33783	. . . 4 ⊢ (♯‘𝑂) = ((𝑀 + 𝑁)C𝑀)
122	120, 121	oveq12i 7423	. . 3 ⊢ ((♯‘{𝑐 ∈ 𝑂 ∣ ¬ 1 ∈ 𝑐}) / (♯‘𝑂)) = ((((𝑀 + 𝑁) − 1)C𝑀) / ((𝑀 + 𝑁)C𝑀))
123	12, 122	eqtri 2758	. 2 ⊢ (𝑃‘{𝑐 ∈ 𝑂 ∣ ¬ 1 ∈ 𝑐}) = ((((𝑀 + 𝑁) − 1)C𝑀) / ((𝑀 + 𝑁)C𝑀))
124		0le1 11741	. . . . 5 ⊢ 0 ≤ 1
125		0re 11220	. . . . . 6 ⊢ 0 ∈ ℝ
126	125, 20, 39	letri 11347	. . . . 5 ⊢ ((0 ≤ 1 ∧ 1 ≤ 𝑀) → 0 ≤ 𝑀)
127	124, 36, 126	mp2an 688	. . . 4 ⊢ 0 ≤ 𝑀
128	2	nngt0i 12255	. . . . . 6 ⊢ 0 < 𝑁
129	40, 128	elrpii 12981	. . . . 5 ⊢ 𝑁 ∈ ℝ⁺
130		ltaddrp 13015	. . . . 5 ⊢ ((𝑀 ∈ ℝ ∧ 𝑁 ∈ ℝ⁺) → 𝑀 < (𝑀 + 𝑁))
131	39, 129, 130	mp2an 688	. . . 4 ⊢ 𝑀 < (𝑀 + 𝑁)
132		0z 12573	. . . . 5 ⊢ 0 ∈ ℤ
133		elfzm11 13576	. . . . 5 ⊢ ((0 ∈ ℤ ∧ (𝑀 + 𝑁) ∈ ℤ) → (𝑀 ∈ (0...((𝑀 + 𝑁) − 1)) ↔ (𝑀 ∈ ℤ ∧ 0 ≤ 𝑀 ∧ 𝑀 < (𝑀 + 𝑁))))
134	132, 50, 133	mp2an 688	. . . 4 ⊢ (𝑀 ∈ (0...((𝑀 + 𝑁) − 1)) ↔ (𝑀 ∈ ℤ ∧ 0 ≤ 𝑀 ∧ 𝑀 < (𝑀 + 𝑁)))
135	95, 127, 131, 134	mpbir3an 1339	. . 3 ⊢ 𝑀 ∈ (0...((𝑀 + 𝑁) − 1))
136		bcm1n 32273	. . 3 ⊢ ((𝑀 ∈ (0...((𝑀 + 𝑁) − 1)) ∧ (𝑀 + 𝑁) ∈ ℕ) → ((((𝑀 + 𝑁) − 1)C𝑀) / ((𝑀 + 𝑁)C𝑀)) = (((𝑀 + 𝑁) − 𝑀) / (𝑀 + 𝑁)))
137	135, 49, 136	mp2an 688	. 2 ⊢ ((((𝑀 + 𝑁) − 1)C𝑀) / ((𝑀 + 𝑁)C𝑀)) = (((𝑀 + 𝑁) − 𝑀) / (𝑀 + 𝑁))
138		pncan2 11471	. . . 4 ⊢ ((𝑀 ∈ ℂ ∧ 𝑁 ∈ ℂ) → ((𝑀 + 𝑁) − 𝑀) = 𝑁)
139	103, 104, 138	mp2an 688	. . 3 ⊢ ((𝑀 + 𝑁) − 𝑀) = 𝑁
140	139	oveq1i 7421	. 2 ⊢ (((𝑀 + 𝑁) − 𝑀) / (𝑀 + 𝑁)) = (𝑁 / (𝑀 + 𝑁))
141	123, 137, 140	3eqtri 2762	1 ⊢ (𝑃‘{𝑐 ∈ 𝑂 ∣ ¬ 1 ∈ 𝑐}) = (𝑁 / (𝑀 + 𝑁))

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ↔ wb 205 ∧ wa 394 ∨ wo 843 ∧ w3a 1085 ∀wal 1537 = wceq 1539 ∃wex 1779 ∈ wcel 2104 {cab 2707 {crab 3430 Vcvv 3472 ∩ cin 3946 ⊆ wss 3947 𝒫 cpw 4601 class class class wbr 5147 ↦ cmpt 5230 ‘cfv 6542 (class class class)co 7411 Fincfn 8941 ℂcc 11110 ℝcr 11111 0cc0 11112 1c1 11113 + caddc 11115 < clt 11252 ≤ cle 11253 − cmin 11448 -cneg 11449 / cdiv 11875 ℕcn 12216 2c2 12271 ℤcz 12562 ℤ_≥cuz 12826 ℝ⁺crp 12978 ...cfz 13488 Ccbc 14266 ♯chash 14294

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1911 ax-6 1969 ax-7 2009 ax-8 2106 ax-9 2114 ax-10 2135 ax-11 2152 ax-12 2169 ax-ext 2701 ax-sep 5298 ax-nul 5305 ax-pow 5362 ax-pr 5426 ax-un 7727 ax-cnex 11168 ax-resscn 11169 ax-1cn 11170 ax-icn 11171 ax-addcl 11172 ax-addrcl 11173 ax-mulcl 11174 ax-mulrcl 11175 ax-mulcom 11176 ax-addass 11177 ax-mulass 11178 ax-distr 11179 ax-i2m1 11180 ax-1ne0 11181 ax-1rid 11182 ax-rnegex 11183 ax-rrecex 11184 ax-cnre 11185 ax-pre-lttri 11186 ax-pre-lttrn 11187 ax-pre-ltadd 11188 ax-pre-mulgt0 11189

This theorem depends on definitions: df-bi 206 df-an 395 df-or 844 df-3or 1086 df-3an 1087 df-tru 1542 df-fal 1552 df-ex 1780 df-nf 1784 df-sb 2066 df-mo 2532 df-eu 2561 df-clab 2708 df-cleq 2722 df-clel 2808 df-nfc 2883 df-ne 2939 df-nel 3045 df-ral 3060 df-rex 3069 df-rmo 3374 df-reu 3375 df-rab 3431 df-v 3474 df-sbc 3777 df-csb 3893 df-dif 3950 df-un 3952 df-in 3954 df-ss 3964 df-pss 3966 df-nul 4322 df-if 4528 df-pw 4603 df-sn 4628 df-pr 4630 df-op 4634 df-uni 4908 df-int 4950 df-iun 4998 df-br 5148 df-opab 5210 df-mpt 5231 df-tr 5265 df-id 5573 df-eprel 5579 df-po 5587 df-so 5588 df-fr 5630 df-we 5632 df-xp 5681 df-rel 5682 df-cnv 5683 df-co 5684 df-dm 5685 df-rn 5686 df-res 5687 df-ima 5688 df-pred 6299 df-ord 6366 df-on 6367 df-lim 6368 df-suc 6369 df-iota 6494 df-fun 6544 df-fn 6545 df-f 6546 df-f1 6547 df-fo 6548 df-f1o 6549 df-fv 6550 df-riota 7367 df-ov 7414 df-oprab 7415 df-mpo 7416 df-om 7858 df-1st 7977 df-2nd 7978 df-frecs 8268 df-wrecs 8299 df-recs 8373 df-rdg 8412 df-1o 8468 df-oadd 8472 df-er 8705 df-en 8942 df-dom 8943 df-sdom 8944 df-fin 8945 df-dju 9898 df-card 9936 df-pnf 11254 df-mnf 11255 df-xr 11256 df-ltxr 11257 df-le 11258 df-sub 11450 df-neg 11451 df-div 11876 df-nn 12217 df-2 12279 df-n0 12477 df-z 12563 df-uz 12827 df-rp 12979 df-fz 13489 df-seq 13971 df-fac 14238 df-bc 14267 df-hash 14295

This theorem is referenced by: ballotth 33834

W3C validator