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 31746

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 31743	. . . . 5 ⊢ 𝑂 ∈ V
5		ssrab2 4055	. . . . 5 ⊢ {𝑐 ∈ 𝑂 ∣ ¬ 1 ∈ 𝑐} ⊆ 𝑂
6	4, 5	elpwi2 5248	. . . 4 ⊢ {𝑐 ∈ 𝑂 ∣ ¬ 1 ∈ 𝑐} ∈ 𝒫 𝑂
7		fveq2 6669	. . . . . 6 ⊢ (𝑥 = {𝑐 ∈ 𝑂 ∣ ¬ 1 ∈ 𝑐} → (♯‘𝑥) = (♯‘{𝑐 ∈ 𝑂 ∣ ¬ 1 ∈ 𝑐}))
8	7	oveq1d 7170	. . . . 5 ⊢ (𝑥 = {𝑐 ∈ 𝑂 ∣ ¬ 1 ∈ 𝑐} → ((♯‘𝑥) / (♯‘𝑂)) = ((♯‘{𝑐 ∈ 𝑂 ∣ ¬ 1 ∈ 𝑐}) / (♯‘𝑂)))
9		ballotth.p	. . . . 5 ⊢ 𝑃 = (𝑥 ∈ 𝒫 𝑂 ↦ ((♯‘𝑥) / (♯‘𝑂)))
10		ovex 7188	. . . . 5 ⊢ ((♯‘{𝑐 ∈ 𝑂 ∣ ¬ 1 ∈ 𝑐}) / (♯‘𝑂)) ∈ V
11	8, 9, 10	fvmpt 6767	. . . 4 ⊢ ({𝑐 ∈ 𝑂 ∣ ¬ 1 ∈ 𝑐} ∈ 𝒫 𝑂 → (𝑃‘{𝑐 ∈ 𝑂 ∣ ¬ 1 ∈ 𝑐}) = ((♯‘{𝑐 ∈ 𝑂 ∣ ¬ 1 ∈ 𝑐}) / (♯‘𝑂)))
12	6, 11	ax-mp 5	. . 3 ⊢ (𝑃‘{𝑐 ∈ 𝑂 ∣ ¬ 1 ∈ 𝑐}) = ((♯‘{𝑐 ∈ 𝑂 ∣ ¬ 1 ∈ 𝑐}) / (♯‘𝑂))
13		an32 644	. . . . . . . 8 ⊢ (((𝑐 ∈ 𝒫 (1...(𝑀 + 𝑁)) ∧ ¬ 1 ∈ 𝑐) ∧ (♯‘𝑐) = 𝑀) ↔ ((𝑐 ∈ 𝒫 (1...(𝑀 + 𝑁)) ∧ (♯‘𝑐) = 𝑀) ∧ ¬ 1 ∈ 𝑐))
14		2eluzge1 12293	. . . . . . . . . . . . . 14 ⊢ 2 ∈ (ℤ_≥‘1)
15		fzss1 12945	. . . . . . . . . . . . . 14 ⊢ (2 ∈ (ℤ_≥‘1) → (2...(𝑀 + 𝑁)) ⊆ (1...(𝑀 + 𝑁)))
16	14, 15	ax-mp 5	. . . . . . . . . . . . 13 ⊢ (2...(𝑀 + 𝑁)) ⊆ (1...(𝑀 + 𝑁))
17	16	sspwi 4552	. . . . . . . . . . . 12 ⊢ 𝒫 (2...(𝑀 + 𝑁)) ⊆ 𝒫 (1...(𝑀 + 𝑁))
18	17	sseli 3962	. . . . . . . . . . 11 ⊢ (𝑐 ∈ 𝒫 (2...(𝑀 + 𝑁)) → 𝑐 ∈ 𝒫 (1...(𝑀 + 𝑁)))
19		1lt2 11807	. . . . . . . . . . . . . . . 16 ⊢ 1 < 2
20		1re 10640	. . . . . . . . . . . . . . . . 17 ⊢ 1 ∈ ℝ
21		2re 11710	. . . . . . . . . . . . . . . . 17 ⊢ 2 ∈ ℝ
22	20, 21	ltnlei 10760	. . . . . . . . . . . . . . . 16 ⊢ (1 < 2 ↔ ¬ 2 ≤ 1)
23	19, 22	mpbi 232	. . . . . . . . . . . . . . 15 ⊢ ¬ 2 ≤ 1
24		elfzle1 12909	. . . . . . . . . . . . . . 15 ⊢ (1 ∈ (2...(𝑀 + 𝑁)) → 2 ≤ 1)
25	23, 24	mto 199	. . . . . . . . . . . . . 14 ⊢ ¬ 1 ∈ (2...(𝑀 + 𝑁))
26		elelpwi 4550	. . . . . . . . . . . . . 14 ⊢ ((1 ∈ 𝑐 ∧ 𝑐 ∈ 𝒫 (2...(𝑀 + 𝑁))) → 1 ∈ (2...(𝑀 + 𝑁)))
27	25, 26	mto 199	. . . . . . . . . . . . 13 ⊢ ¬ (1 ∈ 𝑐 ∧ 𝑐 ∈ 𝒫 (2...(𝑀 + 𝑁)))
28		ancom 463	. . . . . . . . . . . . 13 ⊢ ((1 ∈ 𝑐 ∧ 𝑐 ∈ 𝒫 (2...(𝑀 + 𝑁))) ↔ (𝑐 ∈ 𝒫 (2...(𝑀 + 𝑁)) ∧ 1 ∈ 𝑐))
29	27, 28	mtbi 324	. . . . . . . . . . . 12 ⊢ ¬ (𝑐 ∈ 𝒫 (2...(𝑀 + 𝑁)) ∧ 1 ∈ 𝑐)
30	29	imnani 403	. . . . . . . . . . 11 ⊢ (𝑐 ∈ 𝒫 (2...(𝑀 + 𝑁)) → ¬ 1 ∈ 𝑐)
31	18, 30	jca 514	. . . . . . . . . 10 ⊢ (𝑐 ∈ 𝒫 (2...(𝑀 + 𝑁)) → (𝑐 ∈ 𝒫 (1...(𝑀 + 𝑁)) ∧ ¬ 1 ∈ 𝑐))
32		ssin 4206	. . . . . . . . . . . 12 ⊢ ((𝑐 ⊆ (1...(𝑀 + 𝑁)) ∧ 𝑐 ⊆ {𝑖 ∣ ¬ 𝑖 = 1}) ↔ 𝑐 ⊆ ((1...(𝑀 + 𝑁)) ∩ {𝑖 ∣ ¬ 𝑖 = 1}))
33		1le2 11845	. . . . . . . . . . . . . . . . . . . . 21 ⊢ 1 ≤ 2
34		1p1e2 11761	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (1 + 1) = 2
35		nnge1 11664	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑀 ∈ ℕ → 1 ≤ 𝑀)
36	1, 35	ax-mp 5	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ 1 ≤ 𝑀
37		nnge1 11664	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑁 ∈ ℕ → 1 ≤ 𝑁)
38	2, 37	ax-mp 5	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ 1 ≤ 𝑁
39	1	nnrei 11646	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ 𝑀 ∈ ℝ
40	2	nnrei 11646	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ 𝑁 ∈ ℝ
41	20, 20, 39, 40	le2addi 11202	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((1 ≤ 𝑀 ∧ 1 ≤ 𝑁) → (1 + 1) ≤ (𝑀 + 𝑁))
42	36, 38, 41	mp2an 690	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (1 + 1) ≤ (𝑀 + 𝑁)
43	34, 42	eqbrtrri 5088	. . . . . . . . . . . . . . . . . . . . 21 ⊢ 2 ≤ (𝑀 + 𝑁)
44	39, 40	readdcli 10655	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑀 + 𝑁) ∈ ℝ
45	20, 21, 44	letri 10768	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((1 ≤ 2 ∧ 2 ≤ (𝑀 + 𝑁)) → 1 ≤ (𝑀 + 𝑁))
46	33, 43, 45	mp2an 690	. . . . . . . . . . . . . . . . . . . 20 ⊢ 1 ≤ (𝑀 + 𝑁)
47		1z 12011	. . . . . . . . . . . . . . . . . . . . 21 ⊢ 1 ∈ ℤ
48		nnaddcl 11659	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) → (𝑀 + 𝑁) ∈ ℕ)
49	1, 2, 48	mp2an 690	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑀 + 𝑁) ∈ ℕ
50	49	nnzi 12005	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑀 + 𝑁) ∈ ℤ
51		eluz 12256	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((1 ∈ ℤ ∧ (𝑀 + 𝑁) ∈ ℤ) → ((𝑀 + 𝑁) ∈ (ℤ_≥‘1) ↔ 1 ≤ (𝑀 + 𝑁)))
52	47, 50, 51	mp2an 690	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑀 + 𝑁) ∈ (ℤ_≥‘1) ↔ 1 ≤ (𝑀 + 𝑁))
53	46, 52	mpbir 233	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑀 + 𝑁) ∈ (ℤ_≥‘1)
54		elfzp12 12985	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑀 + 𝑁) ∈ (ℤ_≥‘1) → (𝑖 ∈ (1...(𝑀 + 𝑁)) ↔ (𝑖 = 1 ∨ 𝑖 ∈ ((1 + 1)...(𝑀 + 𝑁)))))
55	53, 54	ax-mp 5	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑖 ∈ (1...(𝑀 + 𝑁)) ↔ (𝑖 = 1 ∨ 𝑖 ∈ ((1 + 1)...(𝑀 + 𝑁))))
56	55	biimpi 218	. . . . . . . . . . . . . . . . 17 ⊢ (𝑖 ∈ (1...(𝑀 + 𝑁)) → (𝑖 = 1 ∨ 𝑖 ∈ ((1 + 1)...(𝑀 + 𝑁))))
57	56	orcanai 999	. . . . . . . . . . . . . . . 16 ⊢ ((𝑖 ∈ (1...(𝑀 + 𝑁)) ∧ ¬ 𝑖 = 1) → 𝑖 ∈ ((1 + 1)...(𝑀 + 𝑁)))
58	34	oveq1i 7165	. . . . . . . . . . . . . . . 16 ⊢ ((1 + 1)...(𝑀 + 𝑁)) = (2...(𝑀 + 𝑁))
59	57, 58	eleqtrdi 2923	. . . . . . . . . . . . . . 15 ⊢ ((𝑖 ∈ (1...(𝑀 + 𝑁)) ∧ ¬ 𝑖 = 1) → 𝑖 ∈ (2...(𝑀 + 𝑁)))
60	59	ss2abi 4042	. . . . . . . . . . . . . 14 ⊢ {𝑖 ∣ (𝑖 ∈ (1...(𝑀 + 𝑁)) ∧ ¬ 𝑖 = 1)} ⊆ {𝑖 ∣ 𝑖 ∈ (2...(𝑀 + 𝑁))}
61		inab 4270	. . . . . . . . . . . . . . 15 ⊢ ({𝑖 ∣ 𝑖 ∈ (1...(𝑀 + 𝑁))} ∩ {𝑖 ∣ ¬ 𝑖 = 1}) = {𝑖 ∣ (𝑖 ∈ (1...(𝑀 + 𝑁)) ∧ ¬ 𝑖 = 1)}
62		abid2 2957	. . . . . . . . . . . . . . . 16 ⊢ {𝑖 ∣ 𝑖 ∈ (1...(𝑀 + 𝑁))} = (1...(𝑀 + 𝑁))
63	62	ineq1i 4184	. . . . . . . . . . . . . . 15 ⊢ ({𝑖 ∣ 𝑖 ∈ (1...(𝑀 + 𝑁))} ∩ {𝑖 ∣ ¬ 𝑖 = 1}) = ((1...(𝑀 + 𝑁)) ∩ {𝑖 ∣ ¬ 𝑖 = 1})
64	61, 63	eqtr3i 2846	. . . . . . . . . . . . . 14 ⊢ {𝑖 ∣ (𝑖 ∈ (1...(𝑀 + 𝑁)) ∧ ¬ 𝑖 = 1)} = ((1...(𝑀 + 𝑁)) ∩ {𝑖 ∣ ¬ 𝑖 = 1})
65		abid2 2957	. . . . . . . . . . . . . 14 ⊢ {𝑖 ∣ 𝑖 ∈ (2...(𝑀 + 𝑁))} = (2...(𝑀 + 𝑁))
66	60, 64, 65	3sstr3i 4008	. . . . . . . . . . . . 13 ⊢ ((1...(𝑀 + 𝑁)) ∩ {𝑖 ∣ ¬ 𝑖 = 1}) ⊆ (2...(𝑀 + 𝑁))
67		sstr 3974	. . . . . . . . . . . . 13 ⊢ ((𝑐 ⊆ ((1...(𝑀 + 𝑁)) ∩ {𝑖 ∣ ¬ 𝑖 = 1}) ∧ ((1...(𝑀 + 𝑁)) ∩ {𝑖 ∣ ¬ 𝑖 = 1}) ⊆ (2...(𝑀 + 𝑁))) → 𝑐 ⊆ (2...(𝑀 + 𝑁)))
68	66, 67	mpan2 689	. . . . . . . . . . . 12 ⊢ (𝑐 ⊆ ((1...(𝑀 + 𝑁)) ∩ {𝑖 ∣ ¬ 𝑖 = 1}) → 𝑐 ⊆ (2...(𝑀 + 𝑁)))
69	32, 68	sylbi 219	. . . . . . . . . . 11 ⊢ ((𝑐 ⊆ (1...(𝑀 + 𝑁)) ∧ 𝑐 ⊆ {𝑖 ∣ ¬ 𝑖 = 1}) → 𝑐 ⊆ (2...(𝑀 + 𝑁)))
70		velpw 4543	. . . . . . . . . . . 12 ⊢ (𝑐 ∈ 𝒫 (1...(𝑀 + 𝑁)) ↔ 𝑐 ⊆ (1...(𝑀 + 𝑁)))
71		ssab 4040	. . . . . . . . . . . . 13 ⊢ (𝑐 ⊆ {𝑖 ∣ ¬ 𝑖 = 1} ↔ ∀𝑖(𝑖 ∈ 𝑐 → ¬ 𝑖 = 1))
72		df-ex 1777	. . . . . . . . . . . . . . . 16 ⊢ (∃𝑖(𝑖 = 1 ∧ 𝑖 ∈ 𝑐) ↔ ¬ ∀𝑖 ¬ (𝑖 = 1 ∧ 𝑖 ∈ 𝑐))
73	72	bicomi 226	. . . . . . . . . . . . . . 15 ⊢ (¬ ∀𝑖 ¬ (𝑖 = 1 ∧ 𝑖 ∈ 𝑐) ↔ ∃𝑖(𝑖 = 1 ∧ 𝑖 ∈ 𝑐))
74	73	con1bii 359	. . . . . . . . . . . . . 14 ⊢ (¬ ∃𝑖(𝑖 = 1 ∧ 𝑖 ∈ 𝑐) ↔ ∀𝑖 ¬ (𝑖 = 1 ∧ 𝑖 ∈ 𝑐))
75		dfclel 2894	. . . . . . . . . . . . . . 15 ⊢ (1 ∈ 𝑐 ↔ ∃𝑖(𝑖 = 1 ∧ 𝑖 ∈ 𝑐))
76	75	notbii 322	. . . . . . . . . . . . . 14 ⊢ (¬ 1 ∈ 𝑐 ↔ ¬ ∃𝑖(𝑖 = 1 ∧ 𝑖 ∈ 𝑐))
77		imnang 1838	. . . . . . . . . . . . . . 15 ⊢ (∀𝑖(𝑖 ∈ 𝑐 → ¬ 𝑖 = 1) ↔ ∀𝑖 ¬ (𝑖 ∈ 𝑐 ∧ 𝑖 = 1))
78		ancom 463	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑖 = 1 ∧ 𝑖 ∈ 𝑐) ↔ (𝑖 ∈ 𝑐 ∧ 𝑖 = 1))
79	78	notbii 322	. . . . . . . . . . . . . . . 16 ⊢ (¬ (𝑖 = 1 ∧ 𝑖 ∈ 𝑐) ↔ ¬ (𝑖 ∈ 𝑐 ∧ 𝑖 = 1))
80	79	albii 1816	. . . . . . . . . . . . . . 15 ⊢ (∀𝑖 ¬ (𝑖 = 1 ∧ 𝑖 ∈ 𝑐) ↔ ∀𝑖 ¬ (𝑖 ∈ 𝑐 ∧ 𝑖 = 1))
81	77, 80	bitr4i 280	. . . . . . . . . . . . . 14 ⊢ (∀𝑖(𝑖 ∈ 𝑐 → ¬ 𝑖 = 1) ↔ ∀𝑖 ¬ (𝑖 = 1 ∧ 𝑖 ∈ 𝑐))
82	74, 76, 81	3bitr4ri 306	. . . . . . . . . . . . 13 ⊢ (∀𝑖(𝑖 ∈ 𝑐 → ¬ 𝑖 = 1) ↔ ¬ 1 ∈ 𝑐)
83	71, 82	bitr2i 278	. . . . . . . . . . . 12 ⊢ (¬ 1 ∈ 𝑐 ↔ 𝑐 ⊆ {𝑖 ∣ ¬ 𝑖 = 1})
84	70, 83	anbi12i 628	. . . . . . . . . . 11 ⊢ ((𝑐 ∈ 𝒫 (1...(𝑀 + 𝑁)) ∧ ¬ 1 ∈ 𝑐) ↔ (𝑐 ⊆ (1...(𝑀 + 𝑁)) ∧ 𝑐 ⊆ {𝑖 ∣ ¬ 𝑖 = 1}))
85		velpw 4543	. . . . . . . . . . 11 ⊢ (𝑐 ∈ 𝒫 (2...(𝑀 + 𝑁)) ↔ 𝑐 ⊆ (2...(𝑀 + 𝑁)))
86	69, 84, 85	3imtr4i 294	. . . . . . . . . 10 ⊢ ((𝑐 ∈ 𝒫 (1...(𝑀 + 𝑁)) ∧ ¬ 1 ∈ 𝑐) → 𝑐 ∈ 𝒫 (2...(𝑀 + 𝑁)))
87	31, 86	impbii 211	. . . . . . . . 9 ⊢ (𝑐 ∈ 𝒫 (2...(𝑀 + 𝑁)) ↔ (𝑐 ∈ 𝒫 (1...(𝑀 + 𝑁)) ∧ ¬ 1 ∈ 𝑐))
88	87	anbi1i 625	. . . . . . . 8 ⊢ ((𝑐 ∈ 𝒫 (2...(𝑀 + 𝑁)) ∧ (♯‘𝑐) = 𝑀) ↔ ((𝑐 ∈ 𝒫 (1...(𝑀 + 𝑁)) ∧ ¬ 1 ∈ 𝑐) ∧ (♯‘𝑐) = 𝑀))
89	3	rabeq2i 3487	. . . . . . . . 9 ⊢ (𝑐 ∈ 𝑂 ↔ (𝑐 ∈ 𝒫 (1...(𝑀 + 𝑁)) ∧ (♯‘𝑐) = 𝑀))
90	89	anbi1i 625	. . . . . . . 8 ⊢ ((𝑐 ∈ 𝑂 ∧ ¬ 1 ∈ 𝑐) ↔ ((𝑐 ∈ 𝒫 (1...(𝑀 + 𝑁)) ∧ (♯‘𝑐) = 𝑀) ∧ ¬ 1 ∈ 𝑐))
91	13, 88, 90	3bitr4i 305	. . . . . . 7 ⊢ ((𝑐 ∈ 𝒫 (2...(𝑀 + 𝑁)) ∧ (♯‘𝑐) = 𝑀) ↔ (𝑐 ∈ 𝑂 ∧ ¬ 1 ∈ 𝑐))
92	91	rabbia2 3477	. . . . . 6 ⊢ {𝑐 ∈ 𝒫 (2...(𝑀 + 𝑁)) ∣ (♯‘𝑐) = 𝑀} = {𝑐 ∈ 𝑂 ∣ ¬ 1 ∈ 𝑐}
93	92	fveq2i 6672	. . . . 5 ⊢ (♯‘{𝑐 ∈ 𝒫 (2...(𝑀 + 𝑁)) ∣ (♯‘𝑐) = 𝑀}) = (♯‘{𝑐 ∈ 𝑂 ∣ ¬ 1 ∈ 𝑐})
94		fzfi 13339	. . . . . . 7 ⊢ (2...(𝑀 + 𝑁)) ∈ Fin
95	1	nnzi 12005	. . . . . . 7 ⊢ 𝑀 ∈ ℤ
96		hashbc 13810	. . . . . . 7 ⊢ (((2...(𝑀 + 𝑁)) ∈ Fin ∧ 𝑀 ∈ ℤ) → ((♯‘(2...(𝑀 + 𝑁)))C𝑀) = (♯‘{𝑐 ∈ 𝒫 (2...(𝑀 + 𝑁)) ∣ (♯‘𝑐) = 𝑀}))
97	94, 95, 96	mp2an 690	. . . . . 6 ⊢ ((♯‘(2...(𝑀 + 𝑁)))C𝑀) = (♯‘{𝑐 ∈ 𝒫 (2...(𝑀 + 𝑁)) ∣ (♯‘𝑐) = 𝑀})
98		2z 12013	. . . . . . . . . . . 12 ⊢ 2 ∈ ℤ
99	98	eluz1i 12250	. . . . . . . . . . 11 ⊢ ((𝑀 + 𝑁) ∈ (ℤ_≥‘2) ↔ ((𝑀 + 𝑁) ∈ ℤ ∧ 2 ≤ (𝑀 + 𝑁)))
100	50, 43, 99	mpbir2an 709	. . . . . . . . . 10 ⊢ (𝑀 + 𝑁) ∈ (ℤ_≥‘2)
101		hashfz 13787	. . . . . . . . . 10 ⊢ ((𝑀 + 𝑁) ∈ (ℤ_≥‘2) → (♯‘(2...(𝑀 + 𝑁))) = (((𝑀 + 𝑁) − 2) + 1))
102	100, 101	ax-mp 5	. . . . . . . . 9 ⊢ (♯‘(2...(𝑀 + 𝑁))) = (((𝑀 + 𝑁) − 2) + 1)
103	1	nncni 11647	. . . . . . . . . . 11 ⊢ 𝑀 ∈ ℂ
104	2	nncni 11647	. . . . . . . . . . 11 ⊢ 𝑁 ∈ ℂ
105	103, 104	addcli 10646	. . . . . . . . . 10 ⊢ (𝑀 + 𝑁) ∈ ℂ
106		2cn 11711	. . . . . . . . . 10 ⊢ 2 ∈ ℂ
107		ax-1cn 10594	. . . . . . . . . 10 ⊢ 1 ∈ ℂ
108		subadd23 10897	. . . . . . . . . 10 ⊢ (((𝑀 + 𝑁) ∈ ℂ ∧ 2 ∈ ℂ ∧ 1 ∈ ℂ) → (((𝑀 + 𝑁) − 2) + 1) = ((𝑀 + 𝑁) + (1 − 2)))
109	105, 106, 107, 108	mp3an 1457	. . . . . . . . 9 ⊢ (((𝑀 + 𝑁) − 2) + 1) = ((𝑀 + 𝑁) + (1 − 2))
110	106, 107	negsubdi2i 10971	. . . . . . . . . . 11 ⊢ -(2 − 1) = (1 − 2)
111		2m1e1 11762	. . . . . . . . . . . 12 ⊢ (2 − 1) = 1
112	111	negeqi 10878	. . . . . . . . . . 11 ⊢ -(2 − 1) = -1
113	110, 112	eqtr3i 2846	. . . . . . . . . 10 ⊢ (1 − 2) = -1
114	113	oveq2i 7166	. . . . . . . . 9 ⊢ ((𝑀 + 𝑁) + (1 − 2)) = ((𝑀 + 𝑁) + -1)
115	102, 109, 114	3eqtri 2848	. . . . . . . 8 ⊢ (♯‘(2...(𝑀 + 𝑁))) = ((𝑀 + 𝑁) + -1)
116	105, 107	negsubi 10963	. . . . . . . 8 ⊢ ((𝑀 + 𝑁) + -1) = ((𝑀 + 𝑁) − 1)
117	115, 116	eqtri 2844	. . . . . . 7 ⊢ (♯‘(2...(𝑀 + 𝑁))) = ((𝑀 + 𝑁) − 1)
118	117	oveq1i 7165	. . . . . 6 ⊢ ((♯‘(2...(𝑀 + 𝑁)))C𝑀) = (((𝑀 + 𝑁) − 1)C𝑀)
119	97, 118	eqtr3i 2846	. . . . 5 ⊢ (♯‘{𝑐 ∈ 𝒫 (2...(𝑀 + 𝑁)) ∣ (♯‘𝑐) = 𝑀}) = (((𝑀 + 𝑁) − 1)C𝑀)
120	93, 119	eqtr3i 2846	. . . 4 ⊢ (♯‘{𝑐 ∈ 𝑂 ∣ ¬ 1 ∈ 𝑐}) = (((𝑀 + 𝑁) − 1)C𝑀)
121	1, 2, 3	ballotlem1 31744	. . . 4 ⊢ (♯‘𝑂) = ((𝑀 + 𝑁)C𝑀)
122	120, 121	oveq12i 7167	. . 3 ⊢ ((♯‘{𝑐 ∈ 𝑂 ∣ ¬ 1 ∈ 𝑐}) / (♯‘𝑂)) = ((((𝑀 + 𝑁) − 1)C𝑀) / ((𝑀 + 𝑁)C𝑀))
123	12, 122	eqtri 2844	. 2 ⊢ (𝑃‘{𝑐 ∈ 𝑂 ∣ ¬ 1 ∈ 𝑐}) = ((((𝑀 + 𝑁) − 1)C𝑀) / ((𝑀 + 𝑁)C𝑀))
124		0le1 11162	. . . . 5 ⊢ 0 ≤ 1
125		0re 10642	. . . . . 6 ⊢ 0 ∈ ℝ
126	125, 20, 39	letri 10768	. . . . 5 ⊢ ((0 ≤ 1 ∧ 1 ≤ 𝑀) → 0 ≤ 𝑀)
127	124, 36, 126	mp2an 690	. . . 4 ⊢ 0 ≤ 𝑀
128	2	nngt0i 11675	. . . . . 6 ⊢ 0 < 𝑁
129	40, 128	elrpii 12391	. . . . 5 ⊢ 𝑁 ∈ ℝ⁺
130		ltaddrp 12425	. . . . 5 ⊢ ((𝑀 ∈ ℝ ∧ 𝑁 ∈ ℝ⁺) → 𝑀 < (𝑀 + 𝑁))
131	39, 129, 130	mp2an 690	. . . 4 ⊢ 𝑀 < (𝑀 + 𝑁)
132		0z 11991	. . . . 5 ⊢ 0 ∈ ℤ
133		elfzm11 12977	. . . . 5 ⊢ ((0 ∈ ℤ ∧ (𝑀 + 𝑁) ∈ ℤ) → (𝑀 ∈ (0...((𝑀 + 𝑁) − 1)) ↔ (𝑀 ∈ ℤ ∧ 0 ≤ 𝑀 ∧ 𝑀 < (𝑀 + 𝑁))))
134	132, 50, 133	mp2an 690	. . . 4 ⊢ (𝑀 ∈ (0...((𝑀 + 𝑁) − 1)) ↔ (𝑀 ∈ ℤ ∧ 0 ≤ 𝑀 ∧ 𝑀 < (𝑀 + 𝑁)))
135	95, 127, 131, 134	mpbir3an 1337	. . 3 ⊢ 𝑀 ∈ (0...((𝑀 + 𝑁) − 1))
136		bcm1n 30517	. . 3 ⊢ ((𝑀 ∈ (0...((𝑀 + 𝑁) − 1)) ∧ (𝑀 + 𝑁) ∈ ℕ) → ((((𝑀 + 𝑁) − 1)C𝑀) / ((𝑀 + 𝑁)C𝑀)) = (((𝑀 + 𝑁) − 𝑀) / (𝑀 + 𝑁)))
137	135, 49, 136	mp2an 690	. 2 ⊢ ((((𝑀 + 𝑁) − 1)C𝑀) / ((𝑀 + 𝑁)C𝑀)) = (((𝑀 + 𝑁) − 𝑀) / (𝑀 + 𝑁))
138		pncan2 10892	. . . 4 ⊢ ((𝑀 ∈ ℂ ∧ 𝑁 ∈ ℂ) → ((𝑀 + 𝑁) − 𝑀) = 𝑁)
139	103, 104, 138	mp2an 690	. . 3 ⊢ ((𝑀 + 𝑁) − 𝑀) = 𝑁
140	139	oveq1i 7165	. 2 ⊢ (((𝑀 + 𝑁) − 𝑀) / (𝑀 + 𝑁)) = (𝑁 / (𝑀 + 𝑁))
141	123, 137, 140	3eqtri 2848	1 ⊢ (𝑃‘{𝑐 ∈ 𝑂 ∣ ¬ 1 ∈ 𝑐}) = (𝑁 / (𝑀 + 𝑁))

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ↔ wb 208 ∧ wa 398 ∨ wo 843 ∧ w3a 1083 ∀wal 1531 = wceq 1533 ∃wex 1776 ∈ wcel 2110 {cab 2799 {crab 3142 Vcvv 3494 ∩ cin 3934 ⊆ wss 3935 𝒫 cpw 4538 class class class wbr 5065 ↦ cmpt 5145 ‘cfv 6354 (class class class)co 7155 Fincfn 8508 ℂcc 10534 ℝcr 10535 0cc0 10536 1c1 10537 + caddc 10539 < clt 10674 ≤ cle 10675 − cmin 10869 -cneg 10870 / cdiv 11296 ℕcn 11637 2c2 11691 ℤcz 11980 ℤ_≥cuz 12242 ℝ⁺crp 12388 ...cfz 12891 Ccbc 13661 ♯chash 13689

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1792 ax-4 1806 ax-5 1907 ax-6 1966 ax-7 2011 ax-8 2112 ax-9 2120 ax-10 2141 ax-11 2157 ax-12 2173 ax-ext 2793 ax-rep 5189 ax-sep 5202 ax-nul 5209 ax-pow 5265 ax-pr 5329 ax-un 7460 ax-cnex 10592 ax-resscn 10593 ax-1cn 10594 ax-icn 10595 ax-addcl 10596 ax-addrcl 10597 ax-mulcl 10598 ax-mulrcl 10599 ax-mulcom 10600 ax-addass 10601 ax-mulass 10602 ax-distr 10603 ax-i2m1 10604 ax-1ne0 10605 ax-1rid 10606 ax-rnegex 10607 ax-rrecex 10608 ax-cnre 10609 ax-pre-lttri 10610 ax-pre-lttrn 10611 ax-pre-ltadd 10612 ax-pre-mulgt0 10613

This theorem depends on definitions: df-bi 209 df-an 399 df-or 844 df-3or 1084 df-3an 1085 df-tru 1536 df-ex 1777 df-nf 1781 df-sb 2066 df-mo 2618 df-eu 2650 df-clab 2800 df-cleq 2814 df-clel 2893 df-nfc 2963 df-ne 3017 df-nel 3124 df-ral 3143 df-rex 3144 df-reu 3145 df-rmo 3146 df-rab 3147 df-v 3496 df-sbc 3772 df-csb 3883 df-dif 3938 df-un 3940 df-in 3942 df-ss 3951 df-pss 3953 df-nul 4291 df-if 4467 df-pw 4540 df-sn 4567 df-pr 4569 df-tp 4571 df-op 4573 df-uni 4838 df-int 4876 df-iun 4920 df-br 5066 df-opab 5128 df-mpt 5146 df-tr 5172 df-id 5459 df-eprel 5464 df-po 5473 df-so 5474 df-fr 5513 df-we 5515 df-xp 5560 df-rel 5561 df-cnv 5562 df-co 5563 df-dm 5564 df-rn 5565 df-res 5566 df-ima 5567 df-pred 6147 df-ord 6193 df-on 6194 df-lim 6195 df-suc 6196 df-iota 6313 df-fun 6356 df-fn 6357 df-f 6358 df-f1 6359 df-fo 6360 df-f1o 6361 df-fv 6362 df-riota 7113 df-ov 7158 df-oprab 7159 df-mpo 7160 df-om 7580 df-1st 7688 df-2nd 7689 df-wrecs 7946 df-recs 8007 df-rdg 8045 df-1o 8101 df-2o 8102 df-oadd 8105 df-er 8288 df-map 8407 df-en 8509 df-dom 8510 df-sdom 8511 df-fin 8512 df-dju 9329 df-card 9367 df-pnf 10676 df-mnf 10677 df-xr 10678 df-ltxr 10679 df-le 10680 df-sub 10871 df-neg 10872 df-div 11297 df-nn 11638 df-2 11699 df-n0 11897 df-z 11981 df-uz 12243 df-rp 12389 df-fz 12892 df-seq 13369 df-fac 13633 df-bc 13662 df-hash 13690

This theorem is referenced by: ballotth 31795

W3C validator