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 34823

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 34820	. . . . 5 ⊢ 𝑂 ∈ V
5		ssrab2 4042	. . . . 5 ⊢ {𝑐 ∈ 𝑂 ∣ ¬ 1 ∈ 𝑐} ⊆ 𝑂
6	4, 5	elpwi2 5306	. . . 4 ⊢ {𝑐 ∈ 𝑂 ∣ ¬ 1 ∈ 𝑐} ∈ 𝒫 𝑂
7		fveq2 6882	. . . . . 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 6990	. . . 4 ⊢ ({𝑐 ∈ 𝑂 ∣ ¬ 1 ∈ 𝑐} ∈ 𝒫 𝑂 → (𝑃‘{𝑐 ∈ 𝑂 ∣ ¬ 1 ∈ 𝑐}) = ((♯‘{𝑐 ∈ 𝑂 ∣ ¬ 1 ∈ 𝑐}) / (♯‘𝑂)))
12	6, 11	ax-mp 5	. . 3 ⊢ (𝑃‘{𝑐 ∈ 𝑂 ∣ ¬ 1 ∈ 𝑐}) = ((♯‘{𝑐 ∈ 𝑂 ∣ ¬ 1 ∈ 𝑐}) / (♯‘𝑂))
13		an32 658	. . . . . . . 8 ⊢ (((𝑐 ∈ 𝒫 (1...(𝑀 + 𝑁)) ∧ ¬ 1 ∈ 𝑐) ∧ (♯‘𝑐) = 𝑀) ↔ ((𝑐 ∈ 𝒫 (1...(𝑀 + 𝑁)) ∧ (♯‘𝑐) = 𝑀) ∧ ¬ 1 ∈ 𝑐))
14		2eluzge1 12905	. . . . . . . . . . . . . 14 ⊢ 2 ∈ (ℤ_≥‘1)
15		fzss1 13590	. . . . . . . . . . . . . 14 ⊢ (2 ∈ (ℤ_≥‘1) → (2...(𝑀 + 𝑁)) ⊆ (1...(𝑀 + 𝑁)))
16	14, 15	ax-mp 5	. . . . . . . . . . . . 13 ⊢ (2...(𝑀 + 𝑁)) ⊆ (1...(𝑀 + 𝑁))
17	16	sspwi 4579	. . . . . . . . . . . 12 ⊢ 𝒫 (2...(𝑀 + 𝑁)) ⊆ 𝒫 (1...(𝑀 + 𝑁))
18	17	sseli 3941	. . . . . . . . . . 11 ⊢ (𝑐 ∈ 𝒫 (2...(𝑀 + 𝑁)) → 𝑐 ∈ 𝒫 (1...(𝑀 + 𝑁)))
19		1lt2 12412	. . . . . . . . . . . . . . . 16 ⊢ 1 < 2
20		1re 11207	. . . . . . . . . . . . . . . . 17 ⊢ 1 ∈ ℝ
21		2re 12314	. . . . . . . . . . . . . . . . 17 ⊢ 2 ∈ ℝ
22	20, 21	ltnlei 11330	. . . . . . . . . . . . . . . 16 ⊢ (1 < 2 ↔ ¬ 2 ≤ 1)
23	19, 22	mpbi 233	. . . . . . . . . . . . . . 15 ⊢ ¬ 2 ≤ 1
24		elfzle1 13554	. . . . . . . . . . . . . . 15 ⊢ (1 ∈ (2...(𝑀 + 𝑁)) → 2 ≤ 1)
25	23, 24	mto 200	. . . . . . . . . . . . . 14 ⊢ ¬ 1 ∈ (2...(𝑀 + 𝑁))
26		elelpwi 4577	. . . . . . . . . . . . . 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 4199	. . . . . . . . . . . 12 ⊢ ((𝑐 ⊆ (1...(𝑀 + 𝑁)) ∧ 𝑐 ⊆ {𝑖 ∣ ¬ 𝑖 = 1}) ↔ 𝑐 ⊆ ((1...(𝑀 + 𝑁)) ∩ {𝑖 ∣ ¬ 𝑖 = 1}))
33		1le2 12451	. . . . . . . . . . . . . . . . . . . . 21 ⊢ 1 ≤ 2
34		1p1e2 12363	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (1 + 1) = 2
35		nnge1 12263	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑀 ∈ ℕ → 1 ≤ 𝑀)
36	1, 35	ax-mp 5	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ 1 ≤ 𝑀
37		nnge1 12263	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑁 ∈ ℕ → 1 ≤ 𝑁)
38	2, 37	ax-mp 5	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ 1 ≤ 𝑁
39	1	nnrei 12241	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ 𝑀 ∈ ℝ
40	2	nnrei 12241	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ 𝑁 ∈ ℝ
41	20, 20, 39, 40	le2addi 11776	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((1 ≤ 𝑀 ∧ 1 ≤ 𝑁) → (1 + 1) ≤ (𝑀 + 𝑁))
42	36, 38, 41	mp2an 704	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (1 + 1) ≤ (𝑀 + 𝑁)
43	34, 42	eqbrtrri 5138	. . . . . . . . . . . . . . . . . . . . 21 ⊢ 2 ≤ (𝑀 + 𝑁)
44	39, 40	readdcli 11223	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑀 + 𝑁) ∈ ℝ
45	20, 21, 44	letri 11338	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((1 ≤ 2 ∧ 2 ≤ (𝑀 + 𝑁)) → 1 ≤ (𝑀 + 𝑁))
46	33, 43, 45	mp2an 704	. . . . . . . . . . . . . . . . . . . 20 ⊢ 1 ≤ (𝑀 + 𝑁)
47		1z 12623	. . . . . . . . . . . . . . . . . . . . 21 ⊢ 1 ∈ ℤ
48		nnaddcl 12255	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) → (𝑀 + 𝑁) ∈ ℕ)
49	1, 2, 48	mp2an 704	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑀 + 𝑁) ∈ ℕ
50	49	nnzi 12617	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑀 + 𝑁) ∈ ℤ
51		eluz 12875	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((1 ∈ ℤ ∧ (𝑀 + 𝑁) ∈ ℤ) → ((𝑀 + 𝑁) ∈ (ℤ_≥‘1) ↔ 1 ≤ (𝑀 + 𝑁)))
52	47, 50, 51	mp2an 704	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑀 + 𝑁) ∈ (ℤ_≥‘1) ↔ 1 ≤ (𝑀 + 𝑁))
53	46, 52	mpbir 234	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑀 + 𝑁) ∈ (ℤ_≥‘1)
54		elfzp12 13630	. . . . . . . . . . . . . . . . . . 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 7421	. . . . . . . . . . . . . . . 16 ⊢ ((1 + 1)...(𝑀 + 𝑁)) = (2...(𝑀 + 𝑁))
59	57, 58	eleqtrdi 2879	. . . . . . . . . . . . . . 15 ⊢ ((𝑖 ∈ (1...(𝑀 + 𝑁)) ∧ ¬ 𝑖 = 1) → 𝑖 ∈ (2...(𝑀 + 𝑁)))
60	59	ss2abi 4028	. . . . . . . . . . . . . 14 ⊢ {𝑖 ∣ (𝑖 ∈ (1...(𝑀 + 𝑁)) ∧ ¬ 𝑖 = 1)} ⊆ {𝑖 ∣ 𝑖 ∈ (2...(𝑀 + 𝑁))}
61		inab 4270	. . . . . . . . . . . . . . 15 ⊢ ({𝑖 ∣ 𝑖 ∈ (1...(𝑀 + 𝑁))} ∩ {𝑖 ∣ ¬ 𝑖 = 1}) = {𝑖 ∣ (𝑖 ∈ (1...(𝑀 + 𝑁)) ∧ ¬ 𝑖 = 1)}
62		abid2 2906	. . . . . . . . . . . . . . . 16 ⊢ {𝑖 ∣ 𝑖 ∈ (1...(𝑀 + 𝑁))} = (1...(𝑀 + 𝑁))
63	62	ineq1i 4177	. . . . . . . . . . . . . . 15 ⊢ ({𝑖 ∣ 𝑖 ∈ (1...(𝑀 + 𝑁))} ∩ {𝑖 ∣ ¬ 𝑖 = 1}) = ((1...(𝑀 + 𝑁)) ∩ {𝑖 ∣ ¬ 𝑖 = 1})
64	61, 63	eqtr3i 2794	. . . . . . . . . . . . . 14 ⊢ {𝑖 ∣ (𝑖 ∈ (1...(𝑀 + 𝑁)) ∧ ¬ 𝑖 = 1)} = ((1...(𝑀 + 𝑁)) ∩ {𝑖 ∣ ¬ 𝑖 = 1})
65		abid2 2906	. . . . . . . . . . . . . 14 ⊢ {𝑖 ∣ 𝑖 ∈ (2...(𝑀 + 𝑁))} = (2...(𝑀 + 𝑁))
66	60, 64, 65	3sstr3i 3995	. . . . . . . . . . . . 13 ⊢ ((1...(𝑀 + 𝑁)) ∩ {𝑖 ∣ ¬ 𝑖 = 1}) ⊆ (2...(𝑀 + 𝑁))
67		sstr 3953	. . . . . . . . . . . . 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 4572	. . . . . . . . . . . 12 ⊢ (𝑐 ∈ 𝒫 (1...(𝑀 + 𝑁)) ↔ 𝑐 ⊆ (1...(𝑀 + 𝑁)))
71		ssab 4025	. . . . . . . . . . . . 13 ⊢ (𝑐 ⊆ {𝑖 ∣ ¬ 𝑖 = 1} ↔ ∀𝑖(𝑖 ∈ 𝑐 → ¬ 𝑖 = 1))
72		df-ex 1807	. . . . . . . . . . . . . . . 16 ⊢ (∃𝑖(𝑖 = 1 ∧ 𝑖 ∈ 𝑐) ↔ ¬ ∀𝑖 ¬ (𝑖 = 1 ∧ 𝑖 ∈ 𝑐))
73	72	bicomi 227	. . . . . . . . . . . . . . 15 ⊢ (¬ ∀𝑖 ¬ (𝑖 = 1 ∧ 𝑖 ∈ 𝑐) ↔ ∃𝑖(𝑖 = 1 ∧ 𝑖 ∈ 𝑐))
74	73	con1bii 359	. . . . . . . . . . . . . 14 ⊢ (¬ ∃𝑖(𝑖 = 1 ∧ 𝑖 ∈ 𝑐) ↔ ∀𝑖 ¬ (𝑖 = 1 ∧ 𝑖 ∈ 𝑐))
75		dfclel 2845	. . . . . . . . . . . . . . 15 ⊢ (1 ∈ 𝑐 ↔ ∃𝑖(𝑖 = 1 ∧ 𝑖 ∈ 𝑐))
76	75	notbii 323	. . . . . . . . . . . . . 14 ⊢ (¬ 1 ∈ 𝑐 ↔ ¬ ∃𝑖(𝑖 = 1 ∧ 𝑖 ∈ 𝑐))
77		imnang 1869	. . . . . . . . . . . . . . 15 ⊢ (∀𝑖(𝑖 ∈ 𝑐 → ¬ 𝑖 = 1) ↔ ∀𝑖 ¬ (𝑖 ∈ 𝑐 ∧ 𝑖 = 1))
78		ancom 465	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑖 = 1 ∧ 𝑖 ∈ 𝑐) ↔ (𝑖 ∈ 𝑐 ∧ 𝑖 = 1))
79	78	notbii 323	. . . . . . . . . . . . . . . 16 ⊢ (¬ (𝑖 = 1 ∧ 𝑖 ∈ 𝑐) ↔ ¬ (𝑖 ∈ 𝑐 ∧ 𝑖 = 1))
80	79	albii 1846	. . . . . . . . . . . . . . 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 4572	. . . . . . . . . . 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 3446	. . . . . . . . 9 ⊢ (𝑐 ∈ 𝑂 ↔ (𝑐 ∈ 𝒫 (1...(𝑀 + 𝑁)) ∧ (♯‘𝑐) = 𝑀))
90	89	anbi1i 635	. . . . . . . 8 ⊢ ((𝑐 ∈ 𝑂 ∧ ¬ 1 ∈ 𝑐) ↔ ((𝑐 ∈ 𝒫 (1...(𝑀 + 𝑁)) ∧ (♯‘𝑐) = 𝑀) ∧ ¬ 1 ∈ 𝑐))
91	13, 88, 90	3bitr4i 306	. . . . . . 7 ⊢ ((𝑐 ∈ 𝒫 (2...(𝑀 + 𝑁)) ∧ (♯‘𝑐) = 𝑀) ↔ (𝑐 ∈ 𝑂 ∧ ¬ 1 ∈ 𝑐))
92	91	rabbia2 3426	. . . . . 6 ⊢ {𝑐 ∈ 𝒫 (2...(𝑀 + 𝑁)) ∣ (♯‘𝑐) = 𝑀} = {𝑐 ∈ 𝑂 ∣ ¬ 1 ∈ 𝑐}
93	92	fveq2i 6885	. . . . 5 ⊢ (♯‘{𝑐 ∈ 𝒫 (2...(𝑀 + 𝑁)) ∣ (♯‘𝑐) = 𝑀}) = (♯‘{𝑐 ∈ 𝑂 ∣ ¬ 1 ∈ 𝑐})
94		fzfi 14007	. . . . . . 7 ⊢ (2...(𝑀 + 𝑁)) ∈ Fin
95	1	nnzi 12617	. . . . . . 7 ⊢ 𝑀 ∈ ℤ
96		hashbc 14489	. . . . . . 7 ⊢ (((2...(𝑀 + 𝑁)) ∈ Fin ∧ 𝑀 ∈ ℤ) → ((♯‘(2...(𝑀 + 𝑁)))C𝑀) = (♯‘{𝑐 ∈ 𝒫 (2...(𝑀 + 𝑁)) ∣ (♯‘𝑐) = 𝑀}))
97	94, 95, 96	mp2an 704	. . . . . 6 ⊢ ((♯‘(2...(𝑀 + 𝑁)))C𝑀) = (♯‘{𝑐 ∈ 𝒫 (2...(𝑀 + 𝑁)) ∣ (♯‘𝑐) = 𝑀})
98		2z 12625	. . . . . . . . . . . 12 ⊢ 2 ∈ ℤ
99	98	eluz1i 12869	. . . . . . . . . . 11 ⊢ ((𝑀 + 𝑁) ∈ (ℤ_≥‘2) ↔ ((𝑀 + 𝑁) ∈ ℤ ∧ 2 ≤ (𝑀 + 𝑁)))
100	50, 43, 99	mpbir2an 723	. . . . . . . . . 10 ⊢ (𝑀 + 𝑁) ∈ (ℤ_≥‘2)
101		hashfz 14463	. . . . . . . . . 10 ⊢ ((𝑀 + 𝑁) ∈ (ℤ_≥‘2) → (♯‘(2...(𝑀 + 𝑁))) = (((𝑀 + 𝑁) − 2) + 1))
102	100, 101	ax-mp 5	. . . . . . . . 9 ⊢ (♯‘(2...(𝑀 + 𝑁))) = (((𝑀 + 𝑁) − 2) + 1)
103	1	nncni 12242	. . . . . . . . . . 11 ⊢ 𝑀 ∈ ℂ
104	2	nncni 12242	. . . . . . . . . . 11 ⊢ 𝑁 ∈ ℂ
105	103, 104	addcli 11214	. . . . . . . . . 10 ⊢ (𝑀 + 𝑁) ∈ ℂ
106		2cn 12315	. . . . . . . . . 10 ⊢ 2 ∈ ℂ
107		ax-1cn 11157	. . . . . . . . . 10 ⊢ 1 ∈ ℂ
108		subadd23 11468	. . . . . . . . . 10 ⊢ (((𝑀 + 𝑁) ∈ ℂ ∧ 2 ∈ ℂ ∧ 1 ∈ ℂ) → (((𝑀 + 𝑁) − 2) + 1) = ((𝑀 + 𝑁) + (1 − 2)))
109	105, 106, 107, 108	mp3an 1487	. . . . . . . . 9 ⊢ (((𝑀 + 𝑁) − 2) + 1) = ((𝑀 + 𝑁) + (1 − 2))
110	106, 107	negsubdi2i 11543	. . . . . . . . . . 11 ⊢ -(2 − 1) = (1 − 2)
111		2m1e1 12364	. . . . . . . . . . . 12 ⊢ (2 − 1) = 1
112	111	negeqi 11449	. . . . . . . . . . 11 ⊢ -(2 − 1) = -1
113	110, 112	eqtr3i 2794	. . . . . . . . . 10 ⊢ (1 − 2) = -1
114	113	oveq2i 7422	. . . . . . . . 9 ⊢ ((𝑀 + 𝑁) + (1 − 2)) = ((𝑀 + 𝑁) + -1)
115	102, 109, 114	3eqtri 2796	. . . . . . . 8 ⊢ (♯‘(2...(𝑀 + 𝑁))) = ((𝑀 + 𝑁) + -1)
116	105, 107	negsubi 11535	. . . . . . . 8 ⊢ ((𝑀 + 𝑁) + -1) = ((𝑀 + 𝑁) − 1)
117	115, 116	eqtri 2792	. . . . . . 7 ⊢ (♯‘(2...(𝑀 + 𝑁))) = ((𝑀 + 𝑁) − 1)
118	117	oveq1i 7421	. . . . . 6 ⊢ ((♯‘(2...(𝑀 + 𝑁)))C𝑀) = (((𝑀 + 𝑁) − 1)C𝑀)
119	97, 118	eqtr3i 2794	. . . . 5 ⊢ (♯‘{𝑐 ∈ 𝒫 (2...(𝑀 + 𝑁)) ∣ (♯‘𝑐) = 𝑀}) = (((𝑀 + 𝑁) − 1)C𝑀)
120	93, 119	eqtr3i 2794	. . . 4 ⊢ (♯‘{𝑐 ∈ 𝑂 ∣ ¬ 1 ∈ 𝑐}) = (((𝑀 + 𝑁) − 1)C𝑀)
121	1, 2, 3	ballotlem1 34821	. . . 4 ⊢ (♯‘𝑂) = ((𝑀 + 𝑁)C𝑀)
122	120, 121	oveq12i 7423	. . 3 ⊢ ((♯‘{𝑐 ∈ 𝑂 ∣ ¬ 1 ∈ 𝑐}) / (♯‘𝑂)) = ((((𝑀 + 𝑁) − 1)C𝑀) / ((𝑀 + 𝑁)C𝑀))
123	12, 122	eqtri 2792	. 2 ⊢ (𝑃‘{𝑐 ∈ 𝑂 ∣ ¬ 1 ∈ 𝑐}) = ((((𝑀 + 𝑁) − 1)C𝑀) / ((𝑀 + 𝑁)C𝑀))
124		0le1 11736	. . . . 5 ⊢ 0 ≤ 1
125		0re 11209	. . . . . 6 ⊢ 0 ∈ ℝ
126	125, 20, 39	letri 11338	. . . . 5 ⊢ ((0 ≤ 1 ∧ 1 ≤ 𝑀) → 0 ≤ 𝑀)
127	124, 36, 126	mp2an 704	. . . 4 ⊢ 0 ≤ 𝑀
128	2	nngt0i 12274	. . . . . 6 ⊢ 0 < 𝑁
129	40, 128	elrpii 13018	. . . . 5 ⊢ 𝑁 ∈ ℝ⁺
130		ltaddrp 13054	. . . . 5 ⊢ ((𝑀 ∈ ℝ ∧ 𝑁 ∈ ℝ⁺) → 𝑀 < (𝑀 + 𝑁))
131	39, 129, 130	mp2an 704	. . . 4 ⊢ 𝑀 < (𝑀 + 𝑁)
132		0z 12601	. . . . 5 ⊢ 0 ∈ ℤ
133		elfzm11 13622	. . . . 5 ⊢ ((0 ∈ ℤ ∧ (𝑀 + 𝑁) ∈ ℤ) → (𝑀 ∈ (0...((𝑀 + 𝑁) − 1)) ↔ (𝑀 ∈ ℤ ∧ 0 ≤ 𝑀 ∧ 𝑀 < (𝑀 + 𝑁))))
134	132, 50, 133	mp2an 704	. . . 4 ⊢ (𝑀 ∈ (0...((𝑀 + 𝑁) − 1)) ↔ (𝑀 ∈ ℤ ∧ 0 ≤ 𝑀 ∧ 𝑀 < (𝑀 + 𝑁)))
135	95, 127, 131, 134	mpbir3an 1358	. . 3 ⊢ 𝑀 ∈ (0...((𝑀 + 𝑁) − 1))
136		bcm1n 33080	. . 3 ⊢ ((𝑀 ∈ (0...((𝑀 + 𝑁) − 1)) ∧ (𝑀 + 𝑁) ∈ ℕ) → ((((𝑀 + 𝑁) − 1)C𝑀) / ((𝑀 + 𝑁)C𝑀)) = (((𝑀 + 𝑁) − 𝑀) / (𝑀 + 𝑁)))
137	135, 49, 136	mp2an 704	. 2 ⊢ ((((𝑀 + 𝑁) − 1)C𝑀) / ((𝑀 + 𝑁)C𝑀)) = (((𝑀 + 𝑁) − 𝑀) / (𝑀 + 𝑁))
138		pncan2 11463	. . . 4 ⊢ ((𝑀 ∈ ℂ ∧ 𝑁 ∈ ℂ) → ((𝑀 + 𝑁) − 𝑀) = 𝑁)
139	103, 104, 138	mp2an 704	. . 3 ⊢ ((𝑀 + 𝑁) − 𝑀) = 𝑁
140	139	oveq1i 7421	. 2 ⊢ (((𝑀 + 𝑁) − 𝑀) / (𝑀 + 𝑁)) = (𝑁 / (𝑀 + 𝑁))
141	123, 137, 140	3eqtri 2796	1 ⊢ (𝑃‘{𝑐 ∈ 𝑂 ∣ ¬ 1 ∈ 𝑐}) = (𝑁 / (𝑀 + 𝑁))

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ↔ wb 209 ∧ wa 400 ∨ wo 860 ∧ w3a 1101 ∀wal 1565 = wceq 1567 ∃wex 1806 ∈ wcel 2149 {cab 2747 {crab 3423 Vcvv 3463 ∩ cin 3912 ⊆ wss 3913 𝒫 cpw 4567 class class class wbr 5113 ↦ cmpt 5196 ‘cfv 6537 (class class class)co 7411 Fincfn 8942 ℂcc 11097 ℝcr 11098 0cc0 11099 1c1 11100 + caddc 11102 < clt 11242 ≤ cle 11243 − cmin 11440 -cneg 11441 / cdiv 11870 ℕcn 12232 2c2 12294 ℤcz 12590 ℤ_≥cuz 12861 ℝ⁺crp 13015 ...cfz 13534 Ccbc 14337 ♯chash 14365

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1822 ax-4 1836 ax-5 1937 ax-6 1994 ax-7 2035 ax-8 2151 ax-9 2159 ax-10 2182 ax-11 2198 ax-12 2219 ax-ext 2741 ax-sep 5261 ax-nul 5271 ax-pow 5337 ax-pr 5405 ax-un 7733 ax-cnex 11155 ax-resscn 11156 ax-1cn 11157 ax-icn 11158 ax-addcl 11159 ax-addrcl 11160 ax-mulcl 11161 ax-mulrcl 11162 ax-mulcom 11163 ax-addass 11164 ax-mulass 11165 ax-distr 11166 ax-i2m1 11167 ax-1ne0 11168 ax-1rid 11169 ax-rnegex 11170 ax-rrecex 11171 ax-cnre 11172 ax-pre-lttri 11173 ax-pre-lttrn 11174 ax-pre-ltadd 11175 ax-pre-mulgt0 11176

This theorem depends on definitions: df-bi 210 df-an 401 df-or 861 df-3or 1102 df-3an 1103 df-tru 1570 df-fal 1580 df-ex 1807 df-nf 1811 df-sb 2098 df-mo 2573 df-eu 2603 df-clab 2748 df-cleq 2761 df-clel 2844 df-nfc 2918 df-ne 2965 df-nel 3071 df-ral 3086 df-rex 3096 df-rmo 3376 df-reu 3377 df-rab 3424 df-v 3465 df-sbc 3754 df-csb 3862 df-dif 3916 df-un 3918 df-in 3920 df-ss 3930 df-pss 3933 df-nul 4295 df-if 4493 df-pw 4569 df-sn 4595 df-pr 4597 df-op 4601 df-uni 4877 df-int 4917 df-iun 4962 df-br 5114 df-opab 5178 df-mpt 5197 df-tr 5223 df-id 5557 df-eprel 5562 df-po 5570 df-so 5571 df-fr 5615 df-we 5617 df-xp 5668 df-rel 5669 df-cnv 5670 df-co 5671 df-dm 5672 df-rn 5673 df-res 5674 df-ima 5675 df-pred 6303 df-ord 6364 df-on 6365 df-lim 6366 df-suc 6367 df-iota 6493 df-fun 6539 df-fn 6540 df-f 6541 df-f1 6542 df-fo 6543 df-f1o 6544 df-fv 6545 df-riota 7368 df-ov 7414 df-oprab 7415 df-mpo 7416 df-om 7862 df-1st 7985 df-2nd 7986 df-frecs 8277 df-wrecs 8308 df-recs 8357 df-rdg 8396 df-1o 8452 df-oadd 8456 df-er 8693 df-en 8943 df-dom 8944 df-sdom 8945 df-fin 8946 df-dju 9886 df-card 9924 df-pnf 11244 df-mnf 11245 df-xr 11246 df-ltxr 11247 df-le 11248 df-sub 11442 df-neg 11443 df-div 11871 df-nn 12233 df-2 12302 df-n0 12504 df-z 12591 df-uz 12862 df-rp 13016 df-fz 13535 df-seq 14037 df-fac 14309 df-bc 14338 df-hash 14366

This theorem is referenced by: ballotth 34872

W3C validator