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 34879

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 34876	. . . . 5 ⊢ 𝑂 ∈ V
5		ssrab2 4034	. . . . 5 ⊢ {𝑐 ∈ 𝑂 ∣ ¬ 1 ∈ 𝑐} ⊆ 𝑂
6	4, 5	elpwi2 5306	. . . 4 ⊢ {𝑐 ∈ 𝑂 ∣ ¬ 1 ∈ 𝑐} ∈ 𝒫 𝑂
7		fveq2 6881	. . . . . 6 ⊢ (𝑥 = {𝑐 ∈ 𝑂 ∣ ¬ 1 ∈ 𝑐} → (♯‘𝑥) = (♯‘{𝑐 ∈ 𝑂 ∣ ¬ 1 ∈ 𝑐}))
8	7	oveq1d 7425	. . . . 5 ⊢ (𝑥 = {𝑐 ∈ 𝑂 ∣ ¬ 1 ∈ 𝑐} → ((♯‘𝑥) / (♯‘𝑂)) = ((♯‘{𝑐 ∈ 𝑂 ∣ ¬ 1 ∈ 𝑐}) / (♯‘𝑂)))
9		ballotth.p	. . . . 5 ⊢ 𝑃 = (𝑥 ∈ 𝒫 𝑂 ↦ ((♯‘𝑥) / (♯‘𝑂)))
10		ovex 7443	. . . . 5 ⊢ ((♯‘{𝑐 ∈ 𝑂 ∣ ¬ 1 ∈ 𝑐}) / (♯‘𝑂)) ∈ V
11	8, 9, 10	fvmpt 6989	. . . 4 ⊢ ({𝑐 ∈ 𝑂 ∣ ¬ 1 ∈ 𝑐} ∈ 𝒫 𝑂 → (𝑃‘{𝑐 ∈ 𝑂 ∣ ¬ 1 ∈ 𝑐}) = ((♯‘{𝑐 ∈ 𝑂 ∣ ¬ 1 ∈ 𝑐}) / (♯‘𝑂)))
12	6, 11	ax-mp 5	. . 3 ⊢ (𝑃‘{𝑐 ∈ 𝑂 ∣ ¬ 1 ∈ 𝑐}) = ((♯‘{𝑐 ∈ 𝑂 ∣ ¬ 1 ∈ 𝑐}) / (♯‘𝑂))
13		an32 658	. . . . . . . 8 ⊢ (((𝑐 ∈ 𝒫 (1...(𝑀 + 𝑁)) ∧ ¬ 1 ∈ 𝑐) ∧ (♯‘𝑐) = 𝑀) ↔ ((𝑐 ∈ 𝒫 (1...(𝑀 + 𝑁)) ∧ (♯‘𝑐) = 𝑀) ∧ ¬ 1 ∈ 𝑐))
14		2eluzge1 12901	. . . . . . . . . . . . . 14 ⊢ 2 ∈ (ℤ_≥‘1)
15		fzss1 13587	. . . . . . . . . . . . . 14 ⊢ (2 ∈ (ℤ_≥‘1) → (2...(𝑀 + 𝑁)) ⊆ (1...(𝑀 + 𝑁)))
16	14, 15	ax-mp 5	. . . . . . . . . . . . 13 ⊢ (2...(𝑀 + 𝑁)) ⊆ (1...(𝑀 + 𝑁))
17	16	sspwi 4574	. . . . . . . . . . . 12 ⊢ 𝒫 (2...(𝑀 + 𝑁)) ⊆ 𝒫 (1...(𝑀 + 𝑁))
18	17	sseli 3933	. . . . . . . . . . 11 ⊢ (𝑐 ∈ 𝒫 (2...(𝑀 + 𝑁)) → 𝑐 ∈ 𝒫 (1...(𝑀 + 𝑁)))
19		1lt2 12408	. . . . . . . . . . . . . . . 16 ⊢ 1 < 2
20		1re 11203	. . . . . . . . . . . . . . . . 17 ⊢ 1 ∈ ℝ
21		2re 12310	. . . . . . . . . . . . . . . . 17 ⊢ 2 ∈ ℝ
22	20, 21	ltnlei 11326	. . . . . . . . . . . . . . . 16 ⊢ (1 < 2 ↔ ¬ 2 ≤ 1)
23	19, 22	mpbi 233	. . . . . . . . . . . . . . 15 ⊢ ¬ 2 ≤ 1
24		elfzle1 13550	. . . . . . . . . . . . . . 15 ⊢ (1 ∈ (2...(𝑀 + 𝑁)) → 2 ≤ 1)
25	23, 24	mto 200	. . . . . . . . . . . . . 14 ⊢ ¬ 1 ∈ (2...(𝑀 + 𝑁))
26		elelpwi 4572	. . . . . . . . . . . . . 14 ⊢ ((1 ∈ 𝑐 ∧ 𝑐 ∈ 𝒫 (2...(𝑀 + 𝑁))) → 1 ∈ (2...(𝑀 + 𝑁)))
27	25, 26	mto 200	. . . . . . . . . . . . 13 ⊢ ¬ (1 ∈ 𝑐 ∧ 𝑐 ∈ 𝒫 (2...(𝑀 + 𝑁)))
28		ancom 465	. . . . . . . . . . . . 13 ⊢ ((1 ∈ 𝑐 ∧ 𝑐 ∈ 𝒫 (2...(𝑀 + 𝑁))) ↔ (𝑐 ∈ 𝒫 (2...(𝑀 + 𝑁)) ∧ 1 ∈ 𝑐))
29	27, 28	mtbi 325	. . . . . . . . . . . 12 ⊢ ¬ (𝑐 ∈ 𝒫 (2...(𝑀 + 𝑁)) ∧ 1 ∈ 𝑐)
30	29	imnani 405	. . . . . . . . . . 11 ⊢ (𝑐 ∈ 𝒫 (2...(𝑀 + 𝑁)) → ¬ 1 ∈ 𝑐)
31	18, 30	jca 520	. . . . . . . . . 10 ⊢ (𝑐 ∈ 𝒫 (2...(𝑀 + 𝑁)) → (𝑐 ∈ 𝒫 (1...(𝑀 + 𝑁)) ∧ ¬ 1 ∈ 𝑐))
32		ssin 4191	. . . . . . . . . . . 12 ⊢ ((𝑐 ⊆ (1...(𝑀 + 𝑁)) ∧ 𝑐 ⊆ {𝑖 ∣ ¬ 𝑖 = 1}) ↔ 𝑐 ⊆ ((1...(𝑀 + 𝑁)) ∩ {𝑖 ∣ ¬ 𝑖 = 1}))
33		1le2 12447	. . . . . . . . . . . . . . . . . . . . 21 ⊢ 1 ≤ 2
34		1p1e2 12359	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (1 + 1) = 2
35		nnge1 12259	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑀 ∈ ℕ → 1 ≤ 𝑀)
36	1, 35	ax-mp 5	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ 1 ≤ 𝑀
37		nnge1 12259	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑁 ∈ ℕ → 1 ≤ 𝑁)
38	2, 37	ax-mp 5	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ 1 ≤ 𝑁
39	1	nnrei 12237	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ 𝑀 ∈ ℝ
40	2	nnrei 12237	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ 𝑁 ∈ ℝ
41	20, 20, 39, 40	le2addi 11772	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((1 ≤ 𝑀 ∧ 1 ≤ 𝑁) → (1 + 1) ≤ (𝑀 + 𝑁))
42	36, 38, 41	mp2an 704	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (1 + 1) ≤ (𝑀 + 𝑁)
43	34, 42	eqbrtrri 5134	. . . . . . . . . . . . . . . . . . . . 21 ⊢ 2 ≤ (𝑀 + 𝑁)
44	39, 40	readdcli 11219	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑀 + 𝑁) ∈ ℝ
45	20, 21, 44	letri 11334	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((1 ≤ 2 ∧ 2 ≤ (𝑀 + 𝑁)) → 1 ≤ (𝑀 + 𝑁))
46	33, 43, 45	mp2an 704	. . . . . . . . . . . . . . . . . . . 20 ⊢ 1 ≤ (𝑀 + 𝑁)
47		1z 12619	. . . . . . . . . . . . . . . . . . . . 21 ⊢ 1 ∈ ℤ
48		nnaddcl 12251	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) → (𝑀 + 𝑁) ∈ ℕ)
49	1, 2, 48	mp2an 704	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑀 + 𝑁) ∈ ℕ
50	49	nnzi 12613	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑀 + 𝑁) ∈ ℤ
51		eluz 12871	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((1 ∈ ℤ ∧ (𝑀 + 𝑁) ∈ ℤ) → ((𝑀 + 𝑁) ∈ (ℤ_≥‘1) ↔ 1 ≤ (𝑀 + 𝑁)))
52	47, 50, 51	mp2an 704	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑀 + 𝑁) ∈ (ℤ_≥‘1) ↔ 1 ≤ (𝑀 + 𝑁))
53	46, 52	mpbir 234	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑀 + 𝑁) ∈ (ℤ_≥‘1)
54		elfzp12 13627	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑀 + 𝑁) ∈ (ℤ_≥‘1) → (𝑖 ∈ (1...(𝑀 + 𝑁)) ↔ (𝑖 = 1 ∨ 𝑖 ∈ ((1 + 1)...(𝑀 + 𝑁)))))
55	53, 54	ax-mp 5	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑖 ∈ (1...(𝑀 + 𝑁)) ↔ (𝑖 = 1 ∨ 𝑖 ∈ ((1 + 1)...(𝑀 + 𝑁))))
56	55	biimpi 219	. . . . . . . . . . . . . . . . 17 ⊢ (𝑖 ∈ (1...(𝑀 + 𝑁)) → (𝑖 = 1 ∨ 𝑖 ∈ ((1 + 1)...(𝑀 + 𝑁))))
57	56	orcanai 1018	. . . . . . . . . . . . . . . 16 ⊢ ((𝑖 ∈ (1...(𝑀 + 𝑁)) ∧ ¬ 𝑖 = 1) → 𝑖 ∈ ((1 + 1)...(𝑀 + 𝑁)))
58	34	oveq1i 7420	. . . . . . . . . . . . . . . 16 ⊢ ((1 + 1)...(𝑀 + 𝑁)) = (2...(𝑀 + 𝑁))
59	57, 58	eleqtrdi 2873	. . . . . . . . . . . . . . 15 ⊢ ((𝑖 ∈ (1...(𝑀 + 𝑁)) ∧ ¬ 𝑖 = 1) → 𝑖 ∈ (2...(𝑀 + 𝑁)))
60	59	ss2abi 4020	. . . . . . . . . . . . . 14 ⊢ {𝑖 ∣ (𝑖 ∈ (1...(𝑀 + 𝑁)) ∧ ¬ 𝑖 = 1)} ⊆ {𝑖 ∣ 𝑖 ∈ (2...(𝑀 + 𝑁))}
61		inab 4262	. . . . . . . . . . . . . . 15 ⊢ ({𝑖 ∣ 𝑖 ∈ (1...(𝑀 + 𝑁))} ∩ {𝑖 ∣ ¬ 𝑖 = 1}) = {𝑖 ∣ (𝑖 ∈ (1...(𝑀 + 𝑁)) ∧ ¬ 𝑖 = 1)}
62		abid2 2900	. . . . . . . . . . . . . . . 16 ⊢ {𝑖 ∣ 𝑖 ∈ (1...(𝑀 + 𝑁))} = (1...(𝑀 + 𝑁))
63	62	ineq1i 4169	. . . . . . . . . . . . . . 15 ⊢ ({𝑖 ∣ 𝑖 ∈ (1...(𝑀 + 𝑁))} ∩ {𝑖 ∣ ¬ 𝑖 = 1}) = ((1...(𝑀 + 𝑁)) ∩ {𝑖 ∣ ¬ 𝑖 = 1})
64	61, 63	eqtr3i 2788	. . . . . . . . . . . . . 14 ⊢ {𝑖 ∣ (𝑖 ∈ (1...(𝑀 + 𝑁)) ∧ ¬ 𝑖 = 1)} = ((1...(𝑀 + 𝑁)) ∩ {𝑖 ∣ ¬ 𝑖 = 1})
65		abid2 2900	. . . . . . . . . . . . . 14 ⊢ {𝑖 ∣ 𝑖 ∈ (2...(𝑀 + 𝑁))} = (2...(𝑀 + 𝑁))
66	60, 64, 65	3sstr3i 3987	. . . . . . . . . . . . 13 ⊢ ((1...(𝑀 + 𝑁)) ∩ {𝑖 ∣ ¬ 𝑖 = 1}) ⊆ (2...(𝑀 + 𝑁))
67		sstr 3945	. . . . . . . . . . . . 13 ⊢ ((𝑐 ⊆ ((1...(𝑀 + 𝑁)) ∩ {𝑖 ∣ ¬ 𝑖 = 1}) ∧ ((1...(𝑀 + 𝑁)) ∩ {𝑖 ∣ ¬ 𝑖 = 1}) ⊆ (2...(𝑀 + 𝑁))) → 𝑐 ⊆ (2...(𝑀 + 𝑁)))
68	66, 67	mpan2 703	. . . . . . . . . . . 12 ⊢ (𝑐 ⊆ ((1...(𝑀 + 𝑁)) ∩ {𝑖 ∣ ¬ 𝑖 = 1}) → 𝑐 ⊆ (2...(𝑀 + 𝑁)))
69	32, 68	sylbi 220	. . . . . . . . . . 11 ⊢ ((𝑐 ⊆ (1...(𝑀 + 𝑁)) ∧ 𝑐 ⊆ {𝑖 ∣ ¬ 𝑖 = 1}) → 𝑐 ⊆ (2...(𝑀 + 𝑁)))
70		velpw 4567	. . . . . . . . . . . 12 ⊢ (𝑐 ∈ 𝒫 (1...(𝑀 + 𝑁)) ↔ 𝑐 ⊆ (1...(𝑀 + 𝑁)))
71		ssab 4017	. . . . . . . . . . . . 13 ⊢ (𝑐 ⊆ {𝑖 ∣ ¬ 𝑖 = 1} ↔ ∀𝑖(𝑖 ∈ 𝑐 → ¬ 𝑖 = 1))
72		df-ex 1810	. . . . . . . . . . . . . . . 16 ⊢ (∃𝑖(𝑖 = 1 ∧ 𝑖 ∈ 𝑐) ↔ ¬ ∀𝑖 ¬ (𝑖 = 1 ∧ 𝑖 ∈ 𝑐))
73	72	bicomi 227	. . . . . . . . . . . . . . 15 ⊢ (¬ ∀𝑖 ¬ (𝑖 = 1 ∧ 𝑖 ∈ 𝑐) ↔ ∃𝑖(𝑖 = 1 ∧ 𝑖 ∈ 𝑐))
74	73	con1bii 359	. . . . . . . . . . . . . 14 ⊢ (¬ ∃𝑖(𝑖 = 1 ∧ 𝑖 ∈ 𝑐) ↔ ∀𝑖 ¬ (𝑖 = 1 ∧ 𝑖 ∈ 𝑐))
75		dfclel 2839	. . . . . . . . . . . . . . 15 ⊢ (1 ∈ 𝑐 ↔ ∃𝑖(𝑖 = 1 ∧ 𝑖 ∈ 𝑐))
76	75	notbii 323	. . . . . . . . . . . . . 14 ⊢ (¬ 1 ∈ 𝑐 ↔ ¬ ∃𝑖(𝑖 = 1 ∧ 𝑖 ∈ 𝑐))
77		imnang 1872	. . . . . . . . . . . . . . 15 ⊢ (∀𝑖(𝑖 ∈ 𝑐 → ¬ 𝑖 = 1) ↔ ∀𝑖 ¬ (𝑖 ∈ 𝑐 ∧ 𝑖 = 1))
78		ancom 465	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑖 = 1 ∧ 𝑖 ∈ 𝑐) ↔ (𝑖 ∈ 𝑐 ∧ 𝑖 = 1))
79	78	notbii 323	. . . . . . . . . . . . . . . 16 ⊢ (¬ (𝑖 = 1 ∧ 𝑖 ∈ 𝑐) ↔ ¬ (𝑖 ∈ 𝑐 ∧ 𝑖 = 1))
80	79	albii 1849	. . . . . . . . . . . . . . 15 ⊢ (∀𝑖 ¬ (𝑖 = 1 ∧ 𝑖 ∈ 𝑐) ↔ ∀𝑖 ¬ (𝑖 ∈ 𝑐 ∧ 𝑖 = 1))
81	77, 80	bitr4i 281	. . . . . . . . . . . . . 14 ⊢ (∀𝑖(𝑖 ∈ 𝑐 → ¬ 𝑖 = 1) ↔ ∀𝑖 ¬ (𝑖 = 1 ∧ 𝑖 ∈ 𝑐))
82	74, 76, 81	3bitr4ri 307	. . . . . . . . . . . . 13 ⊢ (∀𝑖(𝑖 ∈ 𝑐 → ¬ 𝑖 = 1) ↔ ¬ 1 ∈ 𝑐)
83	71, 82	bitr2i 279	. . . . . . . . . . . 12 ⊢ (¬ 1 ∈ 𝑐 ↔ 𝑐 ⊆ {𝑖 ∣ ¬ 𝑖 = 1})
84	70, 83	anbi12i 639	. . . . . . . . . . 11 ⊢ ((𝑐 ∈ 𝒫 (1...(𝑀 + 𝑁)) ∧ ¬ 1 ∈ 𝑐) ↔ (𝑐 ⊆ (1...(𝑀 + 𝑁)) ∧ 𝑐 ⊆ {𝑖 ∣ ¬ 𝑖 = 1}))
85		velpw 4567	. . . . . . . . . . 11 ⊢ (𝑐 ∈ 𝒫 (2...(𝑀 + 𝑁)) ↔ 𝑐 ⊆ (2...(𝑀 + 𝑁)))
86	69, 84, 85	3imtr4i 295	. . . . . . . . . 10 ⊢ ((𝑐 ∈ 𝒫 (1...(𝑀 + 𝑁)) ∧ ¬ 1 ∈ 𝑐) → 𝑐 ∈ 𝒫 (2...(𝑀 + 𝑁)))
87	31, 86	impbii 212	. . . . . . . . 9 ⊢ (𝑐 ∈ 𝒫 (2...(𝑀 + 𝑁)) ↔ (𝑐 ∈ 𝒫 (1...(𝑀 + 𝑁)) ∧ ¬ 1 ∈ 𝑐))
88	87	anbi1i 635	. . . . . . . 8 ⊢ ((𝑐 ∈ 𝒫 (2...(𝑀 + 𝑁)) ∧ (♯‘𝑐) = 𝑀) ↔ ((𝑐 ∈ 𝒫 (1...(𝑀 + 𝑁)) ∧ ¬ 1 ∈ 𝑐) ∧ (♯‘𝑐) = 𝑀))
89	3	reqabi 3439	. . . . . . . . 9 ⊢ (𝑐 ∈ 𝑂 ↔ (𝑐 ∈ 𝒫 (1...(𝑀 + 𝑁)) ∧ (♯‘𝑐) = 𝑀))
90	89	anbi1i 635	. . . . . . . 8 ⊢ ((𝑐 ∈ 𝑂 ∧ ¬ 1 ∈ 𝑐) ↔ ((𝑐 ∈ 𝒫 (1...(𝑀 + 𝑁)) ∧ (♯‘𝑐) = 𝑀) ∧ ¬ 1 ∈ 𝑐))
91	13, 88, 90	3bitr4i 306	. . . . . . 7 ⊢ ((𝑐 ∈ 𝒫 (2...(𝑀 + 𝑁)) ∧ (♯‘𝑐) = 𝑀) ↔ (𝑐 ∈ 𝑂 ∧ ¬ 1 ∈ 𝑐))
92	91	rabbia2 3419	. . . . . 6 ⊢ {𝑐 ∈ 𝒫 (2...(𝑀 + 𝑁)) ∣ (♯‘𝑐) = 𝑀} = {𝑐 ∈ 𝑂 ∣ ¬ 1 ∈ 𝑐}
93	92	fveq2i 6884	. . . . 5 ⊢ (♯‘{𝑐 ∈ 𝒫 (2...(𝑀 + 𝑁)) ∣ (♯‘𝑐) = 𝑀}) = (♯‘{𝑐 ∈ 𝑂 ∣ ¬ 1 ∈ 𝑐})
94		fzfi 14004	. . . . . . 7 ⊢ (2...(𝑀 + 𝑁)) ∈ Fin
95	1	nnzi 12613	. . . . . . 7 ⊢ 𝑀 ∈ ℤ
96		hashbc 14486	. . . . . . 7 ⊢ (((2...(𝑀 + 𝑁)) ∈ Fin ∧ 𝑀 ∈ ℤ) → ((♯‘(2...(𝑀 + 𝑁)))C𝑀) = (♯‘{𝑐 ∈ 𝒫 (2...(𝑀 + 𝑁)) ∣ (♯‘𝑐) = 𝑀}))
97	94, 95, 96	mp2an 704	. . . . . 6 ⊢ ((♯‘(2...(𝑀 + 𝑁)))C𝑀) = (♯‘{𝑐 ∈ 𝒫 (2...(𝑀 + 𝑁)) ∣ (♯‘𝑐) = 𝑀})
98		2z 12621	. . . . . . . . . . . 12 ⊢ 2 ∈ ℤ
99	98	eluz1i 12865	. . . . . . . . . . 11 ⊢ ((𝑀 + 𝑁) ∈ (ℤ_≥‘2) ↔ ((𝑀 + 𝑁) ∈ ℤ ∧ 2 ≤ (𝑀 + 𝑁)))
100	50, 43, 99	mpbir2an 723	. . . . . . . . . 10 ⊢ (𝑀 + 𝑁) ∈ (ℤ_≥‘2)
101		hashfz 14460	. . . . . . . . . 10 ⊢ ((𝑀 + 𝑁) ∈ (ℤ_≥‘2) → (♯‘(2...(𝑀 + 𝑁))) = (((𝑀 + 𝑁) − 2) + 1))
102	100, 101	ax-mp 5	. . . . . . . . 9 ⊢ (♯‘(2...(𝑀 + 𝑁))) = (((𝑀 + 𝑁) − 2) + 1)
103	1	nncni 12238	. . . . . . . . . . 11 ⊢ 𝑀 ∈ ℂ
104	2	nncni 12238	. . . . . . . . . . 11 ⊢ 𝑁 ∈ ℂ
105	103, 104	addcli 11210	. . . . . . . . . 10 ⊢ (𝑀 + 𝑁) ∈ ℂ
106		2cn 12311	. . . . . . . . . 10 ⊢ 2 ∈ ℂ
107		ax-1cn 11153	. . . . . . . . . 10 ⊢ 1 ∈ ℂ
108		subadd23 11464	. . . . . . . . . 10 ⊢ (((𝑀 + 𝑁) ∈ ℂ ∧ 2 ∈ ℂ ∧ 1 ∈ ℂ) → (((𝑀 + 𝑁) − 2) + 1) = ((𝑀 + 𝑁) + (1 − 2)))
109	105, 106, 107, 108	mp3an 1490	. . . . . . . . 9 ⊢ (((𝑀 + 𝑁) − 2) + 1) = ((𝑀 + 𝑁) + (1 − 2))
110	106, 107	negsubdi2i 11539	. . . . . . . . . . 11 ⊢ -(2 − 1) = (1 − 2)
111		2m1e1 12360	. . . . . . . . . . . 12 ⊢ (2 − 1) = 1
112	111	negeqi 11445	. . . . . . . . . . 11 ⊢ -(2 − 1) = -1
113	110, 112	eqtr3i 2788	. . . . . . . . . 10 ⊢ (1 − 2) = -1
114	113	oveq2i 7421	. . . . . . . . 9 ⊢ ((𝑀 + 𝑁) + (1 − 2)) = ((𝑀 + 𝑁) + -1)
115	102, 109, 114	3eqtri 2790	. . . . . . . 8 ⊢ (♯‘(2...(𝑀 + 𝑁))) = ((𝑀 + 𝑁) + -1)
116	105, 107	negsubi 11531	. . . . . . . 8 ⊢ ((𝑀 + 𝑁) + -1) = ((𝑀 + 𝑁) − 1)
117	115, 116	eqtri 2786	. . . . . . 7 ⊢ (♯‘(2...(𝑀 + 𝑁))) = ((𝑀 + 𝑁) − 1)
118	117	oveq1i 7420	. . . . . 6 ⊢ ((♯‘(2...(𝑀 + 𝑁)))C𝑀) = (((𝑀 + 𝑁) − 1)C𝑀)
119	97, 118	eqtr3i 2788	. . . . 5 ⊢ (♯‘{𝑐 ∈ 𝒫 (2...(𝑀 + 𝑁)) ∣ (♯‘𝑐) = 𝑀}) = (((𝑀 + 𝑁) − 1)C𝑀)
120	93, 119	eqtr3i 2788	. . . 4 ⊢ (♯‘{𝑐 ∈ 𝑂 ∣ ¬ 1 ∈ 𝑐}) = (((𝑀 + 𝑁) − 1)C𝑀)
121	1, 2, 3	ballotlem1 34877	. . . 4 ⊢ (♯‘𝑂) = ((𝑀 + 𝑁)C𝑀)
122	120, 121	oveq12i 7422	. . 3 ⊢ ((♯‘{𝑐 ∈ 𝑂 ∣ ¬ 1 ∈ 𝑐}) / (♯‘𝑂)) = ((((𝑀 + 𝑁) − 1)C𝑀) / ((𝑀 + 𝑁)C𝑀))
123	12, 122	eqtri 2786	. 2 ⊢ (𝑃‘{𝑐 ∈ 𝑂 ∣ ¬ 1 ∈ 𝑐}) = ((((𝑀 + 𝑁) − 1)C𝑀) / ((𝑀 + 𝑁)C𝑀))
124		0le1 11732	. . . . 5 ⊢ 0 ≤ 1
125		0re 11205	. . . . . 6 ⊢ 0 ∈ ℝ
126	125, 20, 39	letri 11334	. . . . 5 ⊢ ((0 ≤ 1 ∧ 1 ≤ 𝑀) → 0 ≤ 𝑀)
127	124, 36, 126	mp2an 704	. . . 4 ⊢ 0 ≤ 𝑀
128	2	nngt0i 12270	. . . . . 6 ⊢ 0 < 𝑁
129	40, 128	elrpii 13014	. . . . 5 ⊢ 𝑁 ∈ ℝ⁺
130		ltaddrp 13050	. . . . 5 ⊢ ((𝑀 ∈ ℝ ∧ 𝑁 ∈ ℝ⁺) → 𝑀 < (𝑀 + 𝑁))
131	39, 129, 130	mp2an 704	. . . 4 ⊢ 𝑀 < (𝑀 + 𝑁)
132		0z 12597	. . . . 5 ⊢ 0 ∈ ℤ
133		elfzm11 13619	. . . . 5 ⊢ ((0 ∈ ℤ ∧ (𝑀 + 𝑁) ∈ ℤ) → (𝑀 ∈ (0...((𝑀 + 𝑁) − 1)) ↔ (𝑀 ∈ ℤ ∧ 0 ≤ 𝑀 ∧ 𝑀 < (𝑀 + 𝑁))))
134	132, 50, 133	mp2an 704	. . . 4 ⊢ (𝑀 ∈ (0...((𝑀 + 𝑁) − 1)) ↔ (𝑀 ∈ ℤ ∧ 0 ≤ 𝑀 ∧ 𝑀 < (𝑀 + 𝑁)))
135	95, 127, 131, 134	mpbir3an 1360	. . 3 ⊢ 𝑀 ∈ (0...((𝑀 + 𝑁) − 1))
136		bcm1n 33140	. . 3 ⊢ ((𝑀 ∈ (0...((𝑀 + 𝑁) − 1)) ∧ (𝑀 + 𝑁) ∈ ℕ) → ((((𝑀 + 𝑁) − 1)C𝑀) / ((𝑀 + 𝑁)C𝑀)) = (((𝑀 + 𝑁) − 𝑀) / (𝑀 + 𝑁)))
137	135, 49, 136	mp2an 704	. 2 ⊢ ((((𝑀 + 𝑁) − 1)C𝑀) / ((𝑀 + 𝑁)C𝑀)) = (((𝑀 + 𝑁) − 𝑀) / (𝑀 + 𝑁))
138		pncan2 11459	. . . 4 ⊢ ((𝑀 ∈ ℂ ∧ 𝑁 ∈ ℂ) → ((𝑀 + 𝑁) − 𝑀) = 𝑁)
139	103, 104, 138	mp2an 704	. . 3 ⊢ ((𝑀 + 𝑁) − 𝑀) = 𝑁
140	139	oveq1i 7420	. 2 ⊢ (((𝑀 + 𝑁) − 𝑀) / (𝑀 + 𝑁)) = (𝑁 / (𝑀 + 𝑁))
141	123, 137, 140	3eqtri 2790	1 ⊢ (𝑃‘{𝑐 ∈ 𝑂 ∣ ¬ 1 ∈ 𝑐}) = (𝑁 / (𝑀 + 𝑁))

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ↔ wb 209 ∧ wa 400 ∨ wo 860 ∧ w3a 1103 ∀wal 1568 = wceq 1570 ∃wex 1809 ∈ wcel 2143 {cab 2741 {crab 3416 Vcvv 3455 ∩ cin 3904 ⊆ wss 3905 𝒫 cpw 4562 class class class wbr 5109 ↦ cmpt 5192 ‘cfv 6536 (class class class)co 7410 Fincfn 8939 ℂcc 11093 ℝcr 11094 0cc0 11095 1c1 11096 + caddc 11098 < clt 11238 ≤ cle 11239 − cmin 11436 -cneg 11437 / cdiv 11866 ℕcn 12228 2c2 12290 ℤcz 12586 ℤ_≥cuz 12857 ℝ⁺crp 13011 ...cfz 13530 Ccbc 14334 ♯chash 14362

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1825 ax-4 1839 ax-5 1940 ax-6 1997 ax-7 2038 ax-8 2145 ax-9 2153 ax-10 2176 ax-11 2192 ax-12 2213 ax-ext 2735 ax-sep 5257 ax-nul 5269 ax-pow 5336 ax-pr 5404 ax-un 7732 ax-cnex 11151 ax-resscn 11152 ax-1cn 11153 ax-icn 11154 ax-addcl 11155 ax-addrcl 11156 ax-mulcl 11157 ax-mulrcl 11158 ax-mulcom 11159 ax-addass 11160 ax-mulass 11161 ax-distr 11162 ax-i2m1 11163 ax-1ne0 11164 ax-1rid 11165 ax-rnegex 11166 ax-rrecex 11167 ax-cnre 11168 ax-pre-lttri 11169 ax-pre-lttrn 11170 ax-pre-ltadd 11171 ax-pre-mulgt0 11172

This theorem depends on definitions: df-bi 210 df-an 401 df-or 861 df-3or 1104 df-3an 1105 df-tru 1573 df-fal 1583 df-ex 1810 df-nf 1814 df-sb 2097 df-mo 2567 df-eu 2597 df-clab 2742 df-cleq 2755 df-clel 2838 df-nfc 2912 df-ne 2959 df-nel 3065 df-ral 3080 df-rex 3090 df-rmo 3369 df-reu 3370 df-rab 3417 df-v 3457 df-sbc 3745 df-csb 3854 df-dif 3908 df-un 3910 df-in 3912 df-ss 3922 df-pss 3925 df-nul 4287 df-if 4488 df-pw 4564 df-sn 4590 df-pr 4592 df-op 4596 df-uni 4873 df-int 4913 df-iun 4958 df-br 5110 df-opab 5174 df-mpt 5193 df-tr 5219 df-id 5556 df-eprel 5561 df-po 5569 df-so 5570 df-fr 5614 df-we 5616 df-xp 5667 df-rel 5668 df-cnv 5669 df-co 5670 df-dm 5671 df-rn 5672 df-res 5673 df-ima 5674 df-pred 6302 df-ord 6363 df-on 6364 df-lim 6365 df-suc 6366 df-iota 6492 df-fun 6538 df-fn 6539 df-f 6540 df-f1 6541 df-fo 6542 df-f1o 6543 df-fv 6544 df-riota 7367 df-ov 7413 df-oprab 7414 df-mpo 7415 df-om 7859 df-1st 7982 df-2nd 7983 df-frecs 8274 df-wrecs 8305 df-recs 8354 df-rdg 8393 df-1o 8449 df-oadd 8453 df-er 8690 df-en 8940 df-dom 8941 df-sdom 8942 df-fin 8943 df-dju 9883 df-card 9921 df-pnf 11240 df-mnf 11241 df-xr 11242 df-ltxr 11243 df-le 11244 df-sub 11438 df-neg 11439 df-div 11867 df-nn 12229 df-2 12298 df-n0 12500 df-z 12587 df-uz 12858 df-rp 13012 df-fz 13531 df-seq 14034 df-fac 14306 df-bc 14335 df-hash 14363

This theorem is referenced by: ballotth 34928

W3C validator