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 34491

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 34488	. . . . 5 ⊢ 𝑂 ∈ V
5		ssrab2 4080	. . . . 5 ⊢ {𝑐 ∈ 𝑂 ∣ ¬ 1 ∈ 𝑐} ⊆ 𝑂
6	4, 5	elpwi2 5335	. . . 4 ⊢ {𝑐 ∈ 𝑂 ∣ ¬ 1 ∈ 𝑐} ∈ 𝒫 𝑂
7		fveq2 6906	. . . . . 6 ⊢ (𝑥 = {𝑐 ∈ 𝑂 ∣ ¬ 1 ∈ 𝑐} → (♯‘𝑥) = (♯‘{𝑐 ∈ 𝑂 ∣ ¬ 1 ∈ 𝑐}))
8	7	oveq1d 7446	. . . . 5 ⊢ (𝑥 = {𝑐 ∈ 𝑂 ∣ ¬ 1 ∈ 𝑐} → ((♯‘𝑥) / (♯‘𝑂)) = ((♯‘{𝑐 ∈ 𝑂 ∣ ¬ 1 ∈ 𝑐}) / (♯‘𝑂)))
9		ballotth.p	. . . . 5 ⊢ 𝑃 = (𝑥 ∈ 𝒫 𝑂 ↦ ((♯‘𝑥) / (♯‘𝑂)))
10		ovex 7464	. . . . 5 ⊢ ((♯‘{𝑐 ∈ 𝑂 ∣ ¬ 1 ∈ 𝑐}) / (♯‘𝑂)) ∈ V
11	8, 9, 10	fvmpt 7016	. . . 4 ⊢ ({𝑐 ∈ 𝑂 ∣ ¬ 1 ∈ 𝑐} ∈ 𝒫 𝑂 → (𝑃‘{𝑐 ∈ 𝑂 ∣ ¬ 1 ∈ 𝑐}) = ((♯‘{𝑐 ∈ 𝑂 ∣ ¬ 1 ∈ 𝑐}) / (♯‘𝑂)))
12	6, 11	ax-mp 5	. . 3 ⊢ (𝑃‘{𝑐 ∈ 𝑂 ∣ ¬ 1 ∈ 𝑐}) = ((♯‘{𝑐 ∈ 𝑂 ∣ ¬ 1 ∈ 𝑐}) / (♯‘𝑂))
13		an32 646	. . . . . . . 8 ⊢ (((𝑐 ∈ 𝒫 (1...(𝑀 + 𝑁)) ∧ ¬ 1 ∈ 𝑐) ∧ (♯‘𝑐) = 𝑀) ↔ ((𝑐 ∈ 𝒫 (1...(𝑀 + 𝑁)) ∧ (♯‘𝑐) = 𝑀) ∧ ¬ 1 ∈ 𝑐))
14		2eluzge1 12936	. . . . . . . . . . . . . 14 ⊢ 2 ∈ (ℤ_≥‘1)
15		fzss1 13603	. . . . . . . . . . . . . 14 ⊢ (2 ∈ (ℤ_≥‘1) → (2...(𝑀 + 𝑁)) ⊆ (1...(𝑀 + 𝑁)))
16	14, 15	ax-mp 5	. . . . . . . . . . . . 13 ⊢ (2...(𝑀 + 𝑁)) ⊆ (1...(𝑀 + 𝑁))
17	16	sspwi 4612	. . . . . . . . . . . 12 ⊢ 𝒫 (2...(𝑀 + 𝑁)) ⊆ 𝒫 (1...(𝑀 + 𝑁))
18	17	sseli 3979	. . . . . . . . . . 11 ⊢ (𝑐 ∈ 𝒫 (2...(𝑀 + 𝑁)) → 𝑐 ∈ 𝒫 (1...(𝑀 + 𝑁)))
19		1lt2 12437	. . . . . . . . . . . . . . . 16 ⊢ 1 < 2
20		1re 11261	. . . . . . . . . . . . . . . . 17 ⊢ 1 ∈ ℝ
21		2re 12340	. . . . . . . . . . . . . . . . 17 ⊢ 2 ∈ ℝ
22	20, 21	ltnlei 11382	. . . . . . . . . . . . . . . 16 ⊢ (1 < 2 ↔ ¬ 2 ≤ 1)
23	19, 22	mpbi 230	. . . . . . . . . . . . . . 15 ⊢ ¬ 2 ≤ 1
24		elfzle1 13567	. . . . . . . . . . . . . . 15 ⊢ (1 ∈ (2...(𝑀 + 𝑁)) → 2 ≤ 1)
25	23, 24	mto 197	. . . . . . . . . . . . . 14 ⊢ ¬ 1 ∈ (2...(𝑀 + 𝑁))
26		elelpwi 4610	. . . . . . . . . . . . . 14 ⊢ ((1 ∈ 𝑐 ∧ 𝑐 ∈ 𝒫 (2...(𝑀 + 𝑁))) → 1 ∈ (2...(𝑀 + 𝑁)))
27	25, 26	mto 197	. . . . . . . . . . . . 13 ⊢ ¬ (1 ∈ 𝑐 ∧ 𝑐 ∈ 𝒫 (2...(𝑀 + 𝑁)))
28		ancom 460	. . . . . . . . . . . . 13 ⊢ ((1 ∈ 𝑐 ∧ 𝑐 ∈ 𝒫 (2...(𝑀 + 𝑁))) ↔ (𝑐 ∈ 𝒫 (2...(𝑀 + 𝑁)) ∧ 1 ∈ 𝑐))
29	27, 28	mtbi 322	. . . . . . . . . . . 12 ⊢ ¬ (𝑐 ∈ 𝒫 (2...(𝑀 + 𝑁)) ∧ 1 ∈ 𝑐)
30	29	imnani 400	. . . . . . . . . . 11 ⊢ (𝑐 ∈ 𝒫 (2...(𝑀 + 𝑁)) → ¬ 1 ∈ 𝑐)
31	18, 30	jca 511	. . . . . . . . . 10 ⊢ (𝑐 ∈ 𝒫 (2...(𝑀 + 𝑁)) → (𝑐 ∈ 𝒫 (1...(𝑀 + 𝑁)) ∧ ¬ 1 ∈ 𝑐))
32		ssin 4239	. . . . . . . . . . . 12 ⊢ ((𝑐 ⊆ (1...(𝑀 + 𝑁)) ∧ 𝑐 ⊆ {𝑖 ∣ ¬ 𝑖 = 1}) ↔ 𝑐 ⊆ ((1...(𝑀 + 𝑁)) ∩ {𝑖 ∣ ¬ 𝑖 = 1}))
33		1le2 12475	. . . . . . . . . . . . . . . . . . . . 21 ⊢ 1 ≤ 2
34		1p1e2 12391	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (1 + 1) = 2
35		nnge1 12294	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑀 ∈ ℕ → 1 ≤ 𝑀)
36	1, 35	ax-mp 5	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ 1 ≤ 𝑀
37		nnge1 12294	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑁 ∈ ℕ → 1 ≤ 𝑁)
38	2, 37	ax-mp 5	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ 1 ≤ 𝑁
39	1	nnrei 12275	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ 𝑀 ∈ ℝ
40	2	nnrei 12275	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ 𝑁 ∈ ℝ
41	20, 20, 39, 40	le2addi 11826	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((1 ≤ 𝑀 ∧ 1 ≤ 𝑁) → (1 + 1) ≤ (𝑀 + 𝑁))
42	36, 38, 41	mp2an 692	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (1 + 1) ≤ (𝑀 + 𝑁)
43	34, 42	eqbrtrri 5166	. . . . . . . . . . . . . . . . . . . . 21 ⊢ 2 ≤ (𝑀 + 𝑁)
44	39, 40	readdcli 11276	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑀 + 𝑁) ∈ ℝ
45	20, 21, 44	letri 11390	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((1 ≤ 2 ∧ 2 ≤ (𝑀 + 𝑁)) → 1 ≤ (𝑀 + 𝑁))
46	33, 43, 45	mp2an 692	. . . . . . . . . . . . . . . . . . . 20 ⊢ 1 ≤ (𝑀 + 𝑁)
47		1z 12647	. . . . . . . . . . . . . . . . . . . . 21 ⊢ 1 ∈ ℤ
48		nnaddcl 12289	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) → (𝑀 + 𝑁) ∈ ℕ)
49	1, 2, 48	mp2an 692	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑀 + 𝑁) ∈ ℕ
50	49	nnzi 12641	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑀 + 𝑁) ∈ ℤ
51		eluz 12892	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((1 ∈ ℤ ∧ (𝑀 + 𝑁) ∈ ℤ) → ((𝑀 + 𝑁) ∈ (ℤ_≥‘1) ↔ 1 ≤ (𝑀 + 𝑁)))
52	47, 50, 51	mp2an 692	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑀 + 𝑁) ∈ (ℤ_≥‘1) ↔ 1 ≤ (𝑀 + 𝑁))
53	46, 52	mpbir 231	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑀 + 𝑁) ∈ (ℤ_≥‘1)
54		elfzp12 13643	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑀 + 𝑁) ∈ (ℤ_≥‘1) → (𝑖 ∈ (1...(𝑀 + 𝑁)) ↔ (𝑖 = 1 ∨ 𝑖 ∈ ((1 + 1)...(𝑀 + 𝑁)))))
55	53, 54	ax-mp 5	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑖 ∈ (1...(𝑀 + 𝑁)) ↔ (𝑖 = 1 ∨ 𝑖 ∈ ((1 + 1)...(𝑀 + 𝑁))))
56	55	biimpi 216	. . . . . . . . . . . . . . . . 17 ⊢ (𝑖 ∈ (1...(𝑀 + 𝑁)) → (𝑖 = 1 ∨ 𝑖 ∈ ((1 + 1)...(𝑀 + 𝑁))))
57	56	orcanai 1005	. . . . . . . . . . . . . . . 16 ⊢ ((𝑖 ∈ (1...(𝑀 + 𝑁)) ∧ ¬ 𝑖 = 1) → 𝑖 ∈ ((1 + 1)...(𝑀 + 𝑁)))
58	34	oveq1i 7441	. . . . . . . . . . . . . . . 16 ⊢ ((1 + 1)...(𝑀 + 𝑁)) = (2...(𝑀 + 𝑁))
59	57, 58	eleqtrdi 2851	. . . . . . . . . . . . . . 15 ⊢ ((𝑖 ∈ (1...(𝑀 + 𝑁)) ∧ ¬ 𝑖 = 1) → 𝑖 ∈ (2...(𝑀 + 𝑁)))
60	59	ss2abi 4067	. . . . . . . . . . . . . 14 ⊢ {𝑖 ∣ (𝑖 ∈ (1...(𝑀 + 𝑁)) ∧ ¬ 𝑖 = 1)} ⊆ {𝑖 ∣ 𝑖 ∈ (2...(𝑀 + 𝑁))}
61		inab 4309	. . . . . . . . . . . . . . 15 ⊢ ({𝑖 ∣ 𝑖 ∈ (1...(𝑀 + 𝑁))} ∩ {𝑖 ∣ ¬ 𝑖 = 1}) = {𝑖 ∣ (𝑖 ∈ (1...(𝑀 + 𝑁)) ∧ ¬ 𝑖 = 1)}
62		abid2 2879	. . . . . . . . . . . . . . . 16 ⊢ {𝑖 ∣ 𝑖 ∈ (1...(𝑀 + 𝑁))} = (1...(𝑀 + 𝑁))
63	62	ineq1i 4216	. . . . . . . . . . . . . . 15 ⊢ ({𝑖 ∣ 𝑖 ∈ (1...(𝑀 + 𝑁))} ∩ {𝑖 ∣ ¬ 𝑖 = 1}) = ((1...(𝑀 + 𝑁)) ∩ {𝑖 ∣ ¬ 𝑖 = 1})
64	61, 63	eqtr3i 2767	. . . . . . . . . . . . . 14 ⊢ {𝑖 ∣ (𝑖 ∈ (1...(𝑀 + 𝑁)) ∧ ¬ 𝑖 = 1)} = ((1...(𝑀 + 𝑁)) ∩ {𝑖 ∣ ¬ 𝑖 = 1})
65		abid2 2879	. . . . . . . . . . . . . 14 ⊢ {𝑖 ∣ 𝑖 ∈ (2...(𝑀 + 𝑁))} = (2...(𝑀 + 𝑁))
66	60, 64, 65	3sstr3i 4034	. . . . . . . . . . . . 13 ⊢ ((1...(𝑀 + 𝑁)) ∩ {𝑖 ∣ ¬ 𝑖 = 1}) ⊆ (2...(𝑀 + 𝑁))
67		sstr 3992	. . . . . . . . . . . . 13 ⊢ ((𝑐 ⊆ ((1...(𝑀 + 𝑁)) ∩ {𝑖 ∣ ¬ 𝑖 = 1}) ∧ ((1...(𝑀 + 𝑁)) ∩ {𝑖 ∣ ¬ 𝑖 = 1}) ⊆ (2...(𝑀 + 𝑁))) → 𝑐 ⊆ (2...(𝑀 + 𝑁)))
68	66, 67	mpan2 691	. . . . . . . . . . . 12 ⊢ (𝑐 ⊆ ((1...(𝑀 + 𝑁)) ∩ {𝑖 ∣ ¬ 𝑖 = 1}) → 𝑐 ⊆ (2...(𝑀 + 𝑁)))
69	32, 68	sylbi 217	. . . . . . . . . . 11 ⊢ ((𝑐 ⊆ (1...(𝑀 + 𝑁)) ∧ 𝑐 ⊆ {𝑖 ∣ ¬ 𝑖 = 1}) → 𝑐 ⊆ (2...(𝑀 + 𝑁)))
70		velpw 4605	. . . . . . . . . . . 12 ⊢ (𝑐 ∈ 𝒫 (1...(𝑀 + 𝑁)) ↔ 𝑐 ⊆ (1...(𝑀 + 𝑁)))
71		ssab 4064	. . . . . . . . . . . . 13 ⊢ (𝑐 ⊆ {𝑖 ∣ ¬ 𝑖 = 1} ↔ ∀𝑖(𝑖 ∈ 𝑐 → ¬ 𝑖 = 1))
72		df-ex 1780	. . . . . . . . . . . . . . . 16 ⊢ (∃𝑖(𝑖 = 1 ∧ 𝑖 ∈ 𝑐) ↔ ¬ ∀𝑖 ¬ (𝑖 = 1 ∧ 𝑖 ∈ 𝑐))
73	72	bicomi 224	. . . . . . . . . . . . . . 15 ⊢ (¬ ∀𝑖 ¬ (𝑖 = 1 ∧ 𝑖 ∈ 𝑐) ↔ ∃𝑖(𝑖 = 1 ∧ 𝑖 ∈ 𝑐))
74	73	con1bii 356	. . . . . . . . . . . . . 14 ⊢ (¬ ∃𝑖(𝑖 = 1 ∧ 𝑖 ∈ 𝑐) ↔ ∀𝑖 ¬ (𝑖 = 1 ∧ 𝑖 ∈ 𝑐))
75		dfclel 2817	. . . . . . . . . . . . . . 15 ⊢ (1 ∈ 𝑐 ↔ ∃𝑖(𝑖 = 1 ∧ 𝑖 ∈ 𝑐))
76	75	notbii 320	. . . . . . . . . . . . . 14 ⊢ (¬ 1 ∈ 𝑐 ↔ ¬ ∃𝑖(𝑖 = 1 ∧ 𝑖 ∈ 𝑐))
77		imnang 1842	. . . . . . . . . . . . . . 15 ⊢ (∀𝑖(𝑖 ∈ 𝑐 → ¬ 𝑖 = 1) ↔ ∀𝑖 ¬ (𝑖 ∈ 𝑐 ∧ 𝑖 = 1))
78		ancom 460	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑖 = 1 ∧ 𝑖 ∈ 𝑐) ↔ (𝑖 ∈ 𝑐 ∧ 𝑖 = 1))
79	78	notbii 320	. . . . . . . . . . . . . . . 16 ⊢ (¬ (𝑖 = 1 ∧ 𝑖 ∈ 𝑐) ↔ ¬ (𝑖 ∈ 𝑐 ∧ 𝑖 = 1))
80	79	albii 1819	. . . . . . . . . . . . . . 15 ⊢ (∀𝑖 ¬ (𝑖 = 1 ∧ 𝑖 ∈ 𝑐) ↔ ∀𝑖 ¬ (𝑖 ∈ 𝑐 ∧ 𝑖 = 1))
81	77, 80	bitr4i 278	. . . . . . . . . . . . . 14 ⊢ (∀𝑖(𝑖 ∈ 𝑐 → ¬ 𝑖 = 1) ↔ ∀𝑖 ¬ (𝑖 = 1 ∧ 𝑖 ∈ 𝑐))
82	74, 76, 81	3bitr4ri 304	. . . . . . . . . . . . 13 ⊢ (∀𝑖(𝑖 ∈ 𝑐 → ¬ 𝑖 = 1) ↔ ¬ 1 ∈ 𝑐)
83	71, 82	bitr2i 276	. . . . . . . . . . . 12 ⊢ (¬ 1 ∈ 𝑐 ↔ 𝑐 ⊆ {𝑖 ∣ ¬ 𝑖 = 1})
84	70, 83	anbi12i 628	. . . . . . . . . . 11 ⊢ ((𝑐 ∈ 𝒫 (1...(𝑀 + 𝑁)) ∧ ¬ 1 ∈ 𝑐) ↔ (𝑐 ⊆ (1...(𝑀 + 𝑁)) ∧ 𝑐 ⊆ {𝑖 ∣ ¬ 𝑖 = 1}))
85		velpw 4605	. . . . . . . . . . 11 ⊢ (𝑐 ∈ 𝒫 (2...(𝑀 + 𝑁)) ↔ 𝑐 ⊆ (2...(𝑀 + 𝑁)))
86	69, 84, 85	3imtr4i 292	. . . . . . . . . 10 ⊢ ((𝑐 ∈ 𝒫 (1...(𝑀 + 𝑁)) ∧ ¬ 1 ∈ 𝑐) → 𝑐 ∈ 𝒫 (2...(𝑀 + 𝑁)))
87	31, 86	impbii 209	. . . . . . . . 9 ⊢ (𝑐 ∈ 𝒫 (2...(𝑀 + 𝑁)) ↔ (𝑐 ∈ 𝒫 (1...(𝑀 + 𝑁)) ∧ ¬ 1 ∈ 𝑐))
88	87	anbi1i 624	. . . . . . . 8 ⊢ ((𝑐 ∈ 𝒫 (2...(𝑀 + 𝑁)) ∧ (♯‘𝑐) = 𝑀) ↔ ((𝑐 ∈ 𝒫 (1...(𝑀 + 𝑁)) ∧ ¬ 1 ∈ 𝑐) ∧ (♯‘𝑐) = 𝑀))
89	3	reqabi 3460	. . . . . . . . 9 ⊢ (𝑐 ∈ 𝑂 ↔ (𝑐 ∈ 𝒫 (1...(𝑀 + 𝑁)) ∧ (♯‘𝑐) = 𝑀))
90	89	anbi1i 624	. . . . . . . 8 ⊢ ((𝑐 ∈ 𝑂 ∧ ¬ 1 ∈ 𝑐) ↔ ((𝑐 ∈ 𝒫 (1...(𝑀 + 𝑁)) ∧ (♯‘𝑐) = 𝑀) ∧ ¬ 1 ∈ 𝑐))
91	13, 88, 90	3bitr4i 303	. . . . . . 7 ⊢ ((𝑐 ∈ 𝒫 (2...(𝑀 + 𝑁)) ∧ (♯‘𝑐) = 𝑀) ↔ (𝑐 ∈ 𝑂 ∧ ¬ 1 ∈ 𝑐))
92	91	rabbia2 3439	. . . . . 6 ⊢ {𝑐 ∈ 𝒫 (2...(𝑀 + 𝑁)) ∣ (♯‘𝑐) = 𝑀} = {𝑐 ∈ 𝑂 ∣ ¬ 1 ∈ 𝑐}
93	92	fveq2i 6909	. . . . 5 ⊢ (♯‘{𝑐 ∈ 𝒫 (2...(𝑀 + 𝑁)) ∣ (♯‘𝑐) = 𝑀}) = (♯‘{𝑐 ∈ 𝑂 ∣ ¬ 1 ∈ 𝑐})
94		fzfi 14013	. . . . . . 7 ⊢ (2...(𝑀 + 𝑁)) ∈ Fin
95	1	nnzi 12641	. . . . . . 7 ⊢ 𝑀 ∈ ℤ
96		hashbc 14492	. . . . . . 7 ⊢ (((2...(𝑀 + 𝑁)) ∈ Fin ∧ 𝑀 ∈ ℤ) → ((♯‘(2...(𝑀 + 𝑁)))C𝑀) = (♯‘{𝑐 ∈ 𝒫 (2...(𝑀 + 𝑁)) ∣ (♯‘𝑐) = 𝑀}))
97	94, 95, 96	mp2an 692	. . . . . 6 ⊢ ((♯‘(2...(𝑀 + 𝑁)))C𝑀) = (♯‘{𝑐 ∈ 𝒫 (2...(𝑀 + 𝑁)) ∣ (♯‘𝑐) = 𝑀})
98		2z 12649	. . . . . . . . . . . 12 ⊢ 2 ∈ ℤ
99	98	eluz1i 12886	. . . . . . . . . . 11 ⊢ ((𝑀 + 𝑁) ∈ (ℤ_≥‘2) ↔ ((𝑀 + 𝑁) ∈ ℤ ∧ 2 ≤ (𝑀 + 𝑁)))
100	50, 43, 99	mpbir2an 711	. . . . . . . . . 10 ⊢ (𝑀 + 𝑁) ∈ (ℤ_≥‘2)
101		hashfz 14466	. . . . . . . . . 10 ⊢ ((𝑀 + 𝑁) ∈ (ℤ_≥‘2) → (♯‘(2...(𝑀 + 𝑁))) = (((𝑀 + 𝑁) − 2) + 1))
102	100, 101	ax-mp 5	. . . . . . . . 9 ⊢ (♯‘(2...(𝑀 + 𝑁))) = (((𝑀 + 𝑁) − 2) + 1)
103	1	nncni 12276	. . . . . . . . . . 11 ⊢ 𝑀 ∈ ℂ
104	2	nncni 12276	. . . . . . . . . . 11 ⊢ 𝑁 ∈ ℂ
105	103, 104	addcli 11267	. . . . . . . . . 10 ⊢ (𝑀 + 𝑁) ∈ ℂ
106		2cn 12341	. . . . . . . . . 10 ⊢ 2 ∈ ℂ
107		ax-1cn 11213	. . . . . . . . . 10 ⊢ 1 ∈ ℂ
108		subadd23 11520	. . . . . . . . . 10 ⊢ (((𝑀 + 𝑁) ∈ ℂ ∧ 2 ∈ ℂ ∧ 1 ∈ ℂ) → (((𝑀 + 𝑁) − 2) + 1) = ((𝑀 + 𝑁) + (1 − 2)))
109	105, 106, 107, 108	mp3an 1463	. . . . . . . . 9 ⊢ (((𝑀 + 𝑁) − 2) + 1) = ((𝑀 + 𝑁) + (1 − 2))
110	106, 107	negsubdi2i 11595	. . . . . . . . . . 11 ⊢ -(2 − 1) = (1 − 2)
111		2m1e1 12392	. . . . . . . . . . . 12 ⊢ (2 − 1) = 1
112	111	negeqi 11501	. . . . . . . . . . 11 ⊢ -(2 − 1) = -1
113	110, 112	eqtr3i 2767	. . . . . . . . . 10 ⊢ (1 − 2) = -1
114	113	oveq2i 7442	. . . . . . . . 9 ⊢ ((𝑀 + 𝑁) + (1 − 2)) = ((𝑀 + 𝑁) + -1)
115	102, 109, 114	3eqtri 2769	. . . . . . . 8 ⊢ (♯‘(2...(𝑀 + 𝑁))) = ((𝑀 + 𝑁) + -1)
116	105, 107	negsubi 11587	. . . . . . . 8 ⊢ ((𝑀 + 𝑁) + -1) = ((𝑀 + 𝑁) − 1)
117	115, 116	eqtri 2765	. . . . . . 7 ⊢ (♯‘(2...(𝑀 + 𝑁))) = ((𝑀 + 𝑁) − 1)
118	117	oveq1i 7441	. . . . . 6 ⊢ ((♯‘(2...(𝑀 + 𝑁)))C𝑀) = (((𝑀 + 𝑁) − 1)C𝑀)
119	97, 118	eqtr3i 2767	. . . . 5 ⊢ (♯‘{𝑐 ∈ 𝒫 (2...(𝑀 + 𝑁)) ∣ (♯‘𝑐) = 𝑀}) = (((𝑀 + 𝑁) − 1)C𝑀)
120	93, 119	eqtr3i 2767	. . . 4 ⊢ (♯‘{𝑐 ∈ 𝑂 ∣ ¬ 1 ∈ 𝑐}) = (((𝑀 + 𝑁) − 1)C𝑀)
121	1, 2, 3	ballotlem1 34489	. . . 4 ⊢ (♯‘𝑂) = ((𝑀 + 𝑁)C𝑀)
122	120, 121	oveq12i 7443	. . 3 ⊢ ((♯‘{𝑐 ∈ 𝑂 ∣ ¬ 1 ∈ 𝑐}) / (♯‘𝑂)) = ((((𝑀 + 𝑁) − 1)C𝑀) / ((𝑀 + 𝑁)C𝑀))
123	12, 122	eqtri 2765	. 2 ⊢ (𝑃‘{𝑐 ∈ 𝑂 ∣ ¬ 1 ∈ 𝑐}) = ((((𝑀 + 𝑁) − 1)C𝑀) / ((𝑀 + 𝑁)C𝑀))
124		0le1 11786	. . . . 5 ⊢ 0 ≤ 1
125		0re 11263	. . . . . 6 ⊢ 0 ∈ ℝ
126	125, 20, 39	letri 11390	. . . . 5 ⊢ ((0 ≤ 1 ∧ 1 ≤ 𝑀) → 0 ≤ 𝑀)
127	124, 36, 126	mp2an 692	. . . 4 ⊢ 0 ≤ 𝑀
128	2	nngt0i 12305	. . . . . 6 ⊢ 0 < 𝑁
129	40, 128	elrpii 13037	. . . . 5 ⊢ 𝑁 ∈ ℝ⁺
130		ltaddrp 13072	. . . . 5 ⊢ ((𝑀 ∈ ℝ ∧ 𝑁 ∈ ℝ⁺) → 𝑀 < (𝑀 + 𝑁))
131	39, 129, 130	mp2an 692	. . . 4 ⊢ 𝑀 < (𝑀 + 𝑁)
132		0z 12624	. . . . 5 ⊢ 0 ∈ ℤ
133		elfzm11 13635	. . . . 5 ⊢ ((0 ∈ ℤ ∧ (𝑀 + 𝑁) ∈ ℤ) → (𝑀 ∈ (0...((𝑀 + 𝑁) − 1)) ↔ (𝑀 ∈ ℤ ∧ 0 ≤ 𝑀 ∧ 𝑀 < (𝑀 + 𝑁))))
134	132, 50, 133	mp2an 692	. . . 4 ⊢ (𝑀 ∈ (0...((𝑀 + 𝑁) − 1)) ↔ (𝑀 ∈ ℤ ∧ 0 ≤ 𝑀 ∧ 𝑀 < (𝑀 + 𝑁)))
135	95, 127, 131, 134	mpbir3an 1342	. . 3 ⊢ 𝑀 ∈ (0...((𝑀 + 𝑁) − 1))
136		bcm1n 32797	. . 3 ⊢ ((𝑀 ∈ (0...((𝑀 + 𝑁) − 1)) ∧ (𝑀 + 𝑁) ∈ ℕ) → ((((𝑀 + 𝑁) − 1)C𝑀) / ((𝑀 + 𝑁)C𝑀)) = (((𝑀 + 𝑁) − 𝑀) / (𝑀 + 𝑁)))
137	135, 49, 136	mp2an 692	. 2 ⊢ ((((𝑀 + 𝑁) − 1)C𝑀) / ((𝑀 + 𝑁)C𝑀)) = (((𝑀 + 𝑁) − 𝑀) / (𝑀 + 𝑁))
138		pncan2 11515	. . . 4 ⊢ ((𝑀 ∈ ℂ ∧ 𝑁 ∈ ℂ) → ((𝑀 + 𝑁) − 𝑀) = 𝑁)
139	103, 104, 138	mp2an 692	. . 3 ⊢ ((𝑀 + 𝑁) − 𝑀) = 𝑁
140	139	oveq1i 7441	. 2 ⊢ (((𝑀 + 𝑁) − 𝑀) / (𝑀 + 𝑁)) = (𝑁 / (𝑀 + 𝑁))
141	123, 137, 140	3eqtri 2769	1 ⊢ (𝑃‘{𝑐 ∈ 𝑂 ∣ ¬ 1 ∈ 𝑐}) = (𝑁 / (𝑀 + 𝑁))

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ↔ wb 206 ∧ wa 395 ∨ wo 848 ∧ w3a 1087 ∀wal 1538 = wceq 1540 ∃wex 1779 ∈ wcel 2108 {cab 2714 {crab 3436 Vcvv 3480 ∩ cin 3950 ⊆ wss 3951 𝒫 cpw 4600 class class class wbr 5143 ↦ cmpt 5225 ‘cfv 6561 (class class class)co 7431 Fincfn 8985 ℂcc 11153 ℝcr 11154 0cc0 11155 1c1 11156 + caddc 11158 < clt 11295 ≤ cle 11296 − cmin 11492 -cneg 11493 / cdiv 11920 ℕcn 12266 2c2 12321 ℤcz 12613 ℤ_≥cuz 12878 ℝ⁺crp 13034 ...cfz 13547 Ccbc 14341 ♯chash 14369

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 1910 ax-6 1967 ax-7 2007 ax-8 2110 ax-9 2118 ax-10 2141 ax-11 2157 ax-12 2177 ax-ext 2708 ax-sep 5296 ax-nul 5306 ax-pow 5365 ax-pr 5432 ax-un 7755 ax-cnex 11211 ax-resscn 11212 ax-1cn 11213 ax-icn 11214 ax-addcl 11215 ax-addrcl 11216 ax-mulcl 11217 ax-mulrcl 11218 ax-mulcom 11219 ax-addass 11220 ax-mulass 11221 ax-distr 11222 ax-i2m1 11223 ax-1ne0 11224 ax-1rid 11225 ax-rnegex 11226 ax-rrecex 11227 ax-cnre 11228 ax-pre-lttri 11229 ax-pre-lttrn 11230 ax-pre-ltadd 11231 ax-pre-mulgt0 11232

This theorem depends on definitions: df-bi 207 df-an 396 df-or 849 df-3or 1088 df-3an 1089 df-tru 1543 df-fal 1553 df-ex 1780 df-nf 1784 df-sb 2065 df-mo 2540 df-eu 2569 df-clab 2715 df-cleq 2729 df-clel 2816 df-nfc 2892 df-ne 2941 df-nel 3047 df-ral 3062 df-rex 3071 df-rmo 3380 df-reu 3381 df-rab 3437 df-v 3482 df-sbc 3789 df-csb 3900 df-dif 3954 df-un 3956 df-in 3958 df-ss 3968 df-pss 3971 df-nul 4334 df-if 4526 df-pw 4602 df-sn 4627 df-pr 4629 df-op 4633 df-uni 4908 df-int 4947 df-iun 4993 df-br 5144 df-opab 5206 df-mpt 5226 df-tr 5260 df-id 5578 df-eprel 5584 df-po 5592 df-so 5593 df-fr 5637 df-we 5639 df-xp 5691 df-rel 5692 df-cnv 5693 df-co 5694 df-dm 5695 df-rn 5696 df-res 5697 df-ima 5698 df-pred 6321 df-ord 6387 df-on 6388 df-lim 6389 df-suc 6390 df-iota 6514 df-fun 6563 df-fn 6564 df-f 6565 df-f1 6566 df-fo 6567 df-f1o 6568 df-fv 6569 df-riota 7388 df-ov 7434 df-oprab 7435 df-mpo 7436 df-om 7888 df-1st 8014 df-2nd 8015 df-frecs 8306 df-wrecs 8337 df-recs 8411 df-rdg 8450 df-1o 8506 df-oadd 8510 df-er 8745 df-en 8986 df-dom 8987 df-sdom 8988 df-fin 8989 df-dju 9941 df-card 9979 df-pnf 11297 df-mnf 11298 df-xr 11299 df-ltxr 11300 df-le 11301 df-sub 11494 df-neg 11495 df-div 11921 df-nn 12267 df-2 12329 df-n0 12527 df-z 12614 df-uz 12879 df-rp 13035 df-fz 13548 df-seq 14043 df-fac 14313 df-bc 14342 df-hash 14370

This theorem is referenced by: ballotth 34540

W3C validator