ballotth - Mathbox for Thierry Arnoux

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

Theorem ballotth 30599

Description: Bertrand's ballot problem : the probability that A is ahead throughout the counting. This is Metamath 100 proof #30. (Contributed by Thierry Arnoux, 7-Dec-2016.)

**Hypotheses**
Ref	Expression
ballotth.m	⊢ 𝑀 ∈ ℕ
ballotth.n	⊢ 𝑁 ∈ ℕ
ballotth.o	⊢ 𝑂 = {𝑐 ∈ 𝒫 (1...(𝑀 + 𝑁)) ∣ (#‘𝑐) = 𝑀}
ballotth.p	⊢ 𝑃 = (𝑥 ∈ 𝒫 𝑂 ↦ ((#‘𝑥) / (#‘𝑂)))
ballotth.f	⊢ 𝐹 = (𝑐 ∈ 𝑂 ↦ (𝑖 ∈ ℤ ↦ ((#‘((1...𝑖) ∩ 𝑐)) − (#‘((1...𝑖) ∖ 𝑐)))))
ballotth.e	⊢ 𝐸 = {𝑐 ∈ 𝑂 ∣ ∀𝑖 ∈ (1...(𝑀 + 𝑁))0 < ((𝐹‘𝑐)‘𝑖)}
ballotth.mgtn	⊢ 𝑁 < 𝑀
ballotth.i	⊢ 𝐼 = (𝑐 ∈ (𝑂 ∖ 𝐸) ↦ inf({𝑘 ∈ (1...(𝑀 + 𝑁)) ∣ ((𝐹‘𝑐)‘𝑘) = 0}, ℝ, < ))
ballotth.s	⊢ 𝑆 = (𝑐 ∈ (𝑂 ∖ 𝐸) ↦ (𝑖 ∈ (1...(𝑀 + 𝑁)) ↦ if(𝑖 ≤ (𝐼‘𝑐), (((𝐼‘𝑐) + 1) − 𝑖), 𝑖)))
ballotth.r	⊢ 𝑅 = (𝑐 ∈ (𝑂 ∖ 𝐸) ↦ ((𝑆‘𝑐) “ 𝑐))

**Assertion**
Ref	Expression
ballotth	⊢ (𝑃‘𝐸) = ((𝑀 − 𝑁) / (𝑀 + 𝑁))

Distinct variable groups: 𝑀,𝑐 𝑁,𝑐 𝑂,𝑐 𝑖,𝑀 𝑖,𝑁 𝑖,𝑂 𝑘,𝑀 𝑘,𝑁 𝑘,𝑂 𝑖,𝑐,𝐹,𝑘 𝑖,𝐸,𝑘 𝑘,𝐼,𝑐 𝐸,𝑐 𝑖,𝐼,𝑐 𝑆,𝑘,𝑖,𝑐 𝑅,𝑖,𝑘 𝑥,𝑐,𝐹 𝑥,𝑀 𝑥,𝑁,𝑘,𝑖 𝑥,𝐸 𝑥,𝑂 Allowed substitution hints: 𝑃(𝑥,𝑖,𝑘,𝑐) 𝑅(𝑥,𝑐) 𝑆(𝑥) 𝐼(𝑥)

**Proof of Theorem ballotth**
Step	Hyp	Ref	Expression
1		ballotth.e	. . . . . 6 ⊢ 𝐸 = {𝑐 ∈ 𝑂 ∣ ∀𝑖 ∈ (1...(𝑀 + 𝑁))0 < ((𝐹‘𝑐)‘𝑖)}
2		ssrab2 3687	. . . . . 6 ⊢ {𝑐 ∈ 𝑂 ∣ ∀𝑖 ∈ (1...(𝑀 + 𝑁))0 < ((𝐹‘𝑐)‘𝑖)} ⊆ 𝑂
3	1, 2	eqsstri 3635	. . . . 5 ⊢ 𝐸 ⊆ 𝑂
4		fzfi 12771	. . . . . . . . . . 11 ⊢ (1...(𝑀 + 𝑁)) ∈ Fin
5		pwfi 8261	. . . . . . . . . . 11 ⊢ ((1...(𝑀 + 𝑁)) ∈ Fin ↔ 𝒫 (1...(𝑀 + 𝑁)) ∈ Fin)
6	4, 5	mpbi 220	. . . . . . . . . 10 ⊢ 𝒫 (1...(𝑀 + 𝑁)) ∈ Fin
7		ballotth.o	. . . . . . . . . . 11 ⊢ 𝑂 = {𝑐 ∈ 𝒫 (1...(𝑀 + 𝑁)) ∣ (#‘𝑐) = 𝑀}
8		ssrab2 3687	. . . . . . . . . . 11 ⊢ {𝑐 ∈ 𝒫 (1...(𝑀 + 𝑁)) ∣ (#‘𝑐) = 𝑀} ⊆ 𝒫 (1...(𝑀 + 𝑁))
9	7, 8	eqsstri 3635	. . . . . . . . . 10 ⊢ 𝑂 ⊆ 𝒫 (1...(𝑀 + 𝑁))
10		ssfi 8180	. . . . . . . . . 10 ⊢ ((𝒫 (1...(𝑀 + 𝑁)) ∈ Fin ∧ 𝑂 ⊆ 𝒫 (1...(𝑀 + 𝑁))) → 𝑂 ∈ Fin)
11	6, 9, 10	mp2an 708	. . . . . . . . 9 ⊢ 𝑂 ∈ Fin
12		ssfi 8180	. . . . . . . . 9 ⊢ ((𝑂 ∈ Fin ∧ 𝐸 ⊆ 𝑂) → 𝐸 ∈ Fin)
13	11, 3, 12	mp2an 708	. . . . . . . 8 ⊢ 𝐸 ∈ Fin
14	13	elexi 3213	. . . . . . 7 ⊢ 𝐸 ∈ V
15	14	elpw 4164	. . . . . 6 ⊢ (𝐸 ∈ 𝒫 𝑂 ↔ 𝐸 ⊆ 𝑂)
16		fveq2 6191	. . . . . . . 8 ⊢ (𝑥 = 𝐸 → (#‘𝑥) = (#‘𝐸))
17	16	oveq1d 6665	. . . . . . 7 ⊢ (𝑥 = 𝐸 → ((#‘𝑥) / (#‘𝑂)) = ((#‘𝐸) / (#‘𝑂)))
18		ballotth.p	. . . . . . 7 ⊢ 𝑃 = (𝑥 ∈ 𝒫 𝑂 ↦ ((#‘𝑥) / (#‘𝑂)))
19		ovex 6678	. . . . . . 7 ⊢ ((#‘𝐸) / (#‘𝑂)) ∈ V
20	17, 18, 19	fvmpt 6282	. . . . . 6 ⊢ (𝐸 ∈ 𝒫 𝑂 → (𝑃‘𝐸) = ((#‘𝐸) / (#‘𝑂)))
21	15, 20	sylbir 225	. . . . 5 ⊢ (𝐸 ⊆ 𝑂 → (𝑃‘𝐸) = ((#‘𝐸) / (#‘𝑂)))
22	3, 21	ax-mp 5	. . . 4 ⊢ (𝑃‘𝐸) = ((#‘𝐸) / (#‘𝑂))
23		hashssdif 13200	. . . . . . . 8 ⊢ ((𝑂 ∈ Fin ∧ 𝐸 ⊆ 𝑂) → (#‘(𝑂 ∖ 𝐸)) = ((#‘𝑂) − (#‘𝐸)))
24	11, 3, 23	mp2an 708	. . . . . . 7 ⊢ (#‘(𝑂 ∖ 𝐸)) = ((#‘𝑂) − (#‘𝐸))
25	24	eqcomi 2631	. . . . . 6 ⊢ ((#‘𝑂) − (#‘𝐸)) = (#‘(𝑂 ∖ 𝐸))
26		hashcl 13147	. . . . . . . . 9 ⊢ (𝑂 ∈ Fin → (#‘𝑂) ∈ ℕ₀)
27	11, 26	ax-mp 5	. . . . . . . 8 ⊢ (#‘𝑂) ∈ ℕ₀
28	27	nn0cni 11304	. . . . . . 7 ⊢ (#‘𝑂) ∈ ℂ
29		hashcl 13147	. . . . . . . . 9 ⊢ (𝐸 ∈ Fin → (#‘𝐸) ∈ ℕ₀)
30	13, 29	ax-mp 5	. . . . . . . 8 ⊢ (#‘𝐸) ∈ ℕ₀
31	30	nn0cni 11304	. . . . . . 7 ⊢ (#‘𝐸) ∈ ℂ
32		difss 3737	. . . . . . . . . 10 ⊢ (𝑂 ∖ 𝐸) ⊆ 𝑂
33		ssfi 8180	. . . . . . . . . 10 ⊢ ((𝑂 ∈ Fin ∧ (𝑂 ∖ 𝐸) ⊆ 𝑂) → (𝑂 ∖ 𝐸) ∈ Fin)
34	11, 32, 33	mp2an 708	. . . . . . . . 9 ⊢ (𝑂 ∖ 𝐸) ∈ Fin
35		hashcl 13147	. . . . . . . . 9 ⊢ ((𝑂 ∖ 𝐸) ∈ Fin → (#‘(𝑂 ∖ 𝐸)) ∈ ℕ₀)
36	34, 35	ax-mp 5	. . . . . . . 8 ⊢ (#‘(𝑂 ∖ 𝐸)) ∈ ℕ₀
37	36	nn0cni 11304	. . . . . . 7 ⊢ (#‘(𝑂 ∖ 𝐸)) ∈ ℂ
38	28, 31, 37	subsub23i 10371	. . . . . 6 ⊢ (((#‘𝑂) − (#‘𝐸)) = (#‘(𝑂 ∖ 𝐸)) ↔ ((#‘𝑂) − (#‘(𝑂 ∖ 𝐸))) = (#‘𝐸))
39	25, 38	mpbi 220	. . . . 5 ⊢ ((#‘𝑂) − (#‘(𝑂 ∖ 𝐸))) = (#‘𝐸)
40	39	oveq1i 6660	. . . 4 ⊢ (((#‘𝑂) − (#‘(𝑂 ∖ 𝐸))) / (#‘𝑂)) = ((#‘𝐸) / (#‘𝑂))
41	22, 40	eqtr4i 2647	. . 3 ⊢ (𝑃‘𝐸) = (((#‘𝑂) − (#‘(𝑂 ∖ 𝐸))) / (#‘𝑂))
42		ballotth.m	. . . . . . 7 ⊢ 𝑀 ∈ ℕ
43		ballotth.n	. . . . . . 7 ⊢ 𝑁 ∈ ℕ
44	42, 43, 7	ballotlem1 30548	. . . . . 6 ⊢ (#‘𝑂) = ((𝑀 + 𝑁)C𝑀)
45	42	nnnn0i 11300	. . . . . . . . 9 ⊢ 𝑀 ∈ ℕ₀
46		nnaddcl 11042	. . . . . . . . . . 11 ⊢ ((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) → (𝑀 + 𝑁) ∈ ℕ)
47	42, 43, 46	mp2an 708	. . . . . . . . . 10 ⊢ (𝑀 + 𝑁) ∈ ℕ
48	47	nnnn0i 11300	. . . . . . . . 9 ⊢ (𝑀 + 𝑁) ∈ ℕ₀
49	42	nnrei 11029	. . . . . . . . . 10 ⊢ 𝑀 ∈ ℝ
50	43	nnnn0i 11300	. . . . . . . . . 10 ⊢ 𝑁 ∈ ℕ₀
51	49, 50	nn0addge1i 11341	. . . . . . . . 9 ⊢ 𝑀 ≤ (𝑀 + 𝑁)
52		elfz2nn0 12431	. . . . . . . . 9 ⊢ (𝑀 ∈ (0...(𝑀 + 𝑁)) ↔ (𝑀 ∈ ℕ₀ ∧ (𝑀 + 𝑁) ∈ ℕ₀ ∧ 𝑀 ≤ (𝑀 + 𝑁)))
53	45, 48, 51, 52	mpbir3an 1244	. . . . . . . 8 ⊢ 𝑀 ∈ (0...(𝑀 + 𝑁))
54		bccl2 13110	. . . . . . . 8 ⊢ (𝑀 ∈ (0...(𝑀 + 𝑁)) → ((𝑀 + 𝑁)C𝑀) ∈ ℕ)
55	53, 54	ax-mp 5	. . . . . . 7 ⊢ ((𝑀 + 𝑁)C𝑀) ∈ ℕ
56	55	nnne0i 11055	. . . . . 6 ⊢ ((𝑀 + 𝑁)C𝑀) ≠ 0
57	44, 56	eqnetri 2864	. . . . 5 ⊢ (#‘𝑂) ≠ 0
58	28, 57	pm3.2i 471	. . . 4 ⊢ ((#‘𝑂) ∈ ℂ ∧ (#‘𝑂) ≠ 0)
59		divsubdir 10721	. . . 4 ⊢ (((#‘𝑂) ∈ ℂ ∧ (#‘(𝑂 ∖ 𝐸)) ∈ ℂ ∧ ((#‘𝑂) ∈ ℂ ∧ (#‘𝑂) ≠ 0)) → (((#‘𝑂) − (#‘(𝑂 ∖ 𝐸))) / (#‘𝑂)) = (((#‘𝑂) / (#‘𝑂)) − ((#‘(𝑂 ∖ 𝐸)) / (#‘𝑂))))
60	28, 37, 58, 59	mp3an 1424	. . 3 ⊢ (((#‘𝑂) − (#‘(𝑂 ∖ 𝐸))) / (#‘𝑂)) = (((#‘𝑂) / (#‘𝑂)) − ((#‘(𝑂 ∖ 𝐸)) / (#‘𝑂)))
61	28, 57	dividi 10758	. . . 4 ⊢ ((#‘𝑂) / (#‘𝑂)) = 1
62	61	oveq1i 6660	. . 3 ⊢ (((#‘𝑂) / (#‘𝑂)) − ((#‘(𝑂 ∖ 𝐸)) / (#‘𝑂))) = (1 − ((#‘(𝑂 ∖ 𝐸)) / (#‘𝑂)))
63	41, 60, 62	3eqtri 2648	. 2 ⊢ (𝑃‘𝐸) = (1 − ((#‘(𝑂 ∖ 𝐸)) / (#‘𝑂)))
64		ballotth.f	. . . . . . 7 ⊢ 𝐹 = (𝑐 ∈ 𝑂 ↦ (𝑖 ∈ ℤ ↦ ((#‘((1...𝑖) ∩ 𝑐)) − (#‘((1...𝑖) ∖ 𝑐)))))
65		ballotth.mgtn	. . . . . . 7 ⊢ 𝑁 < 𝑀
66		ballotth.i	. . . . . . 7 ⊢ 𝐼 = (𝑐 ∈ (𝑂 ∖ 𝐸) ↦ inf({𝑘 ∈ (1...(𝑀 + 𝑁)) ∣ ((𝐹‘𝑐)‘𝑘) = 0}, ℝ, < ))
67		ballotth.s	. . . . . . 7 ⊢ 𝑆 = (𝑐 ∈ (𝑂 ∖ 𝐸) ↦ (𝑖 ∈ (1...(𝑀 + 𝑁)) ↦ if(𝑖 ≤ (𝐼‘𝑐), (((𝐼‘𝑐) + 1) − 𝑖), 𝑖)))
68		ballotth.r	. . . . . . 7 ⊢ 𝑅 = (𝑐 ∈ (𝑂 ∖ 𝐸) ↦ ((𝑆‘𝑐) “ 𝑐))
69	42, 43, 7, 18, 64, 1, 65, 66, 67, 68	ballotlem8 30598	. . . . . 6 ⊢ (#‘{𝑐 ∈ (𝑂 ∖ 𝐸) ∣ 1 ∈ 𝑐}) = (#‘{𝑐 ∈ (𝑂 ∖ 𝐸) ∣ ¬ 1 ∈ 𝑐})
70	69	oveq1i 6660	. . . . 5 ⊢ ((#‘{𝑐 ∈ (𝑂 ∖ 𝐸) ∣ 1 ∈ 𝑐}) + (#‘{𝑐 ∈ (𝑂 ∖ 𝐸) ∣ ¬ 1 ∈ 𝑐})) = ((#‘{𝑐 ∈ (𝑂 ∖ 𝐸) ∣ ¬ 1 ∈ 𝑐}) + (#‘{𝑐 ∈ (𝑂 ∖ 𝐸) ∣ ¬ 1 ∈ 𝑐}))
71	70	oveq1i 6660	. . . 4 ⊢ (((#‘{𝑐 ∈ (𝑂 ∖ 𝐸) ∣ 1 ∈ 𝑐}) + (#‘{𝑐 ∈ (𝑂 ∖ 𝐸) ∣ ¬ 1 ∈ 𝑐})) / (#‘𝑂)) = (((#‘{𝑐 ∈ (𝑂 ∖ 𝐸) ∣ ¬ 1 ∈ 𝑐}) + (#‘{𝑐 ∈ (𝑂 ∖ 𝐸) ∣ ¬ 1 ∈ 𝑐})) / (#‘𝑂))
72		rabxm 3961	. . . . . . 7 ⊢ (𝑂 ∖ 𝐸) = ({𝑐 ∈ (𝑂 ∖ 𝐸) ∣ 1 ∈ 𝑐} ∪ {𝑐 ∈ (𝑂 ∖ 𝐸) ∣ ¬ 1 ∈ 𝑐})
73	72	fveq2i 6194	. . . . . 6 ⊢ (#‘(𝑂 ∖ 𝐸)) = (#‘({𝑐 ∈ (𝑂 ∖ 𝐸) ∣ 1 ∈ 𝑐} ∪ {𝑐 ∈ (𝑂 ∖ 𝐸) ∣ ¬ 1 ∈ 𝑐}))
74		ssrab2 3687	. . . . . . . . . 10 ⊢ {𝑐 ∈ (𝑂 ∖ 𝐸) ∣ 1 ∈ 𝑐} ⊆ (𝑂 ∖ 𝐸)
75	74, 32	sstri 3612	. . . . . . . . 9 ⊢ {𝑐 ∈ (𝑂 ∖ 𝐸) ∣ 1 ∈ 𝑐} ⊆ 𝑂
76	75, 9	sstri 3612	. . . . . . . 8 ⊢ {𝑐 ∈ (𝑂 ∖ 𝐸) ∣ 1 ∈ 𝑐} ⊆ 𝒫 (1...(𝑀 + 𝑁))
77		ssfi 8180	. . . . . . . 8 ⊢ ((𝒫 (1...(𝑀 + 𝑁)) ∈ Fin ∧ {𝑐 ∈ (𝑂 ∖ 𝐸) ∣ 1 ∈ 𝑐} ⊆ 𝒫 (1...(𝑀 + 𝑁))) → {𝑐 ∈ (𝑂 ∖ 𝐸) ∣ 1 ∈ 𝑐} ∈ Fin)
78	6, 76, 77	mp2an 708	. . . . . . 7 ⊢ {𝑐 ∈ (𝑂 ∖ 𝐸) ∣ 1 ∈ 𝑐} ∈ Fin
79		ssrab2 3687	. . . . . . . . . 10 ⊢ {𝑐 ∈ (𝑂 ∖ 𝐸) ∣ ¬ 1 ∈ 𝑐} ⊆ (𝑂 ∖ 𝐸)
80	79, 32	sstri 3612	. . . . . . . . 9 ⊢ {𝑐 ∈ (𝑂 ∖ 𝐸) ∣ ¬ 1 ∈ 𝑐} ⊆ 𝑂
81	80, 9	sstri 3612	. . . . . . . 8 ⊢ {𝑐 ∈ (𝑂 ∖ 𝐸) ∣ ¬ 1 ∈ 𝑐} ⊆ 𝒫 (1...(𝑀 + 𝑁))
82		ssfi 8180	. . . . . . . 8 ⊢ ((𝒫 (1...(𝑀 + 𝑁)) ∈ Fin ∧ {𝑐 ∈ (𝑂 ∖ 𝐸) ∣ ¬ 1 ∈ 𝑐} ⊆ 𝒫 (1...(𝑀 + 𝑁))) → {𝑐 ∈ (𝑂 ∖ 𝐸) ∣ ¬ 1 ∈ 𝑐} ∈ Fin)
83	6, 81, 82	mp2an 708	. . . . . . 7 ⊢ {𝑐 ∈ (𝑂 ∖ 𝐸) ∣ ¬ 1 ∈ 𝑐} ∈ Fin
84		rabnc 3962	. . . . . . 7 ⊢ ({𝑐 ∈ (𝑂 ∖ 𝐸) ∣ 1 ∈ 𝑐} ∩ {𝑐 ∈ (𝑂 ∖ 𝐸) ∣ ¬ 1 ∈ 𝑐}) = ∅
85		hashun 13171	. . . . . . 7 ⊢ (({𝑐 ∈ (𝑂 ∖ 𝐸) ∣ 1 ∈ 𝑐} ∈ Fin ∧ {𝑐 ∈ (𝑂 ∖ 𝐸) ∣ ¬ 1 ∈ 𝑐} ∈ Fin ∧ ({𝑐 ∈ (𝑂 ∖ 𝐸) ∣ 1 ∈ 𝑐} ∩ {𝑐 ∈ (𝑂 ∖ 𝐸) ∣ ¬ 1 ∈ 𝑐}) = ∅) → (#‘({𝑐 ∈ (𝑂 ∖ 𝐸) ∣ 1 ∈ 𝑐} ∪ {𝑐 ∈ (𝑂 ∖ 𝐸) ∣ ¬ 1 ∈ 𝑐})) = ((#‘{𝑐 ∈ (𝑂 ∖ 𝐸) ∣ 1 ∈ 𝑐}) + (#‘{𝑐 ∈ (𝑂 ∖ 𝐸) ∣ ¬ 1 ∈ 𝑐})))
86	78, 83, 84, 85	mp3an 1424	. . . . . 6 ⊢ (#‘({𝑐 ∈ (𝑂 ∖ 𝐸) ∣ 1 ∈ 𝑐} ∪ {𝑐 ∈ (𝑂 ∖ 𝐸) ∣ ¬ 1 ∈ 𝑐})) = ((#‘{𝑐 ∈ (𝑂 ∖ 𝐸) ∣ 1 ∈ 𝑐}) + (#‘{𝑐 ∈ (𝑂 ∖ 𝐸) ∣ ¬ 1 ∈ 𝑐}))
87	73, 86	eqtri 2644	. . . . 5 ⊢ (#‘(𝑂 ∖ 𝐸)) = ((#‘{𝑐 ∈ (𝑂 ∖ 𝐸) ∣ 1 ∈ 𝑐}) + (#‘{𝑐 ∈ (𝑂 ∖ 𝐸) ∣ ¬ 1 ∈ 𝑐}))
88	87	oveq1i 6660	. . . 4 ⊢ ((#‘(𝑂 ∖ 𝐸)) / (#‘𝑂)) = (((#‘{𝑐 ∈ (𝑂 ∖ 𝐸) ∣ 1 ∈ 𝑐}) + (#‘{𝑐 ∈ (𝑂 ∖ 𝐸) ∣ ¬ 1 ∈ 𝑐})) / (#‘𝑂))
89		ssrab2 3687	. . . . . . . . 9 ⊢ {𝑐 ∈ 𝑂 ∣ ¬ 1 ∈ 𝑐} ⊆ 𝑂
90	11	elexi 3213	. . . . . . . . . 10 ⊢ 𝑂 ∈ V
91	90	elpw2 4828	. . . . . . . . 9 ⊢ ({𝑐 ∈ 𝑂 ∣ ¬ 1 ∈ 𝑐} ∈ 𝒫 𝑂 ↔ {𝑐 ∈ 𝑂 ∣ ¬ 1 ∈ 𝑐} ⊆ 𝑂)
92	89, 91	mpbir 221	. . . . . . . 8 ⊢ {𝑐 ∈ 𝑂 ∣ ¬ 1 ∈ 𝑐} ∈ 𝒫 𝑂
93		fveq2 6191	. . . . . . . . . 10 ⊢ (𝑥 = {𝑐 ∈ 𝑂 ∣ ¬ 1 ∈ 𝑐} → (#‘𝑥) = (#‘{𝑐 ∈ 𝑂 ∣ ¬ 1 ∈ 𝑐}))
94	93	oveq1d 6665	. . . . . . . . 9 ⊢ (𝑥 = {𝑐 ∈ 𝑂 ∣ ¬ 1 ∈ 𝑐} → ((#‘𝑥) / (#‘𝑂)) = ((#‘{𝑐 ∈ 𝑂 ∣ ¬ 1 ∈ 𝑐}) / (#‘𝑂)))
95		ovex 6678	. . . . . . . . 9 ⊢ ((#‘{𝑐 ∈ 𝑂 ∣ ¬ 1 ∈ 𝑐}) / (#‘𝑂)) ∈ V
96	94, 18, 95	fvmpt 6282	. . . . . . . 8 ⊢ ({𝑐 ∈ 𝑂 ∣ ¬ 1 ∈ 𝑐} ∈ 𝒫 𝑂 → (𝑃‘{𝑐 ∈ 𝑂 ∣ ¬ 1 ∈ 𝑐}) = ((#‘{𝑐 ∈ 𝑂 ∣ ¬ 1 ∈ 𝑐}) / (#‘𝑂)))
97	92, 96	ax-mp 5	. . . . . . 7 ⊢ (𝑃‘{𝑐 ∈ 𝑂 ∣ ¬ 1 ∈ 𝑐}) = ((#‘{𝑐 ∈ 𝑂 ∣ ¬ 1 ∈ 𝑐}) / (#‘𝑂))
98	42, 43, 7, 18	ballotlem2 30550	. . . . . . 7 ⊢ (𝑃‘{𝑐 ∈ 𝑂 ∣ ¬ 1 ∈ 𝑐}) = (𝑁 / (𝑀 + 𝑁))
99		nfrab1 3122	. . . . . . . . . . . 12 ⊢ Ⅎ𝑐{𝑐 ∈ 𝑂 ∣ ¬ 1 ∈ 𝑐}
100		nfrab1 3122	. . . . . . . . . . . 12 ⊢ Ⅎ𝑐{𝑐 ∈ (𝑂 ∖ 𝐸) ∣ ¬ 1 ∈ 𝑐}
101	99, 100	dfss2f 3594	. . . . . . . . . . 11 ⊢ ({𝑐 ∈ 𝑂 ∣ ¬ 1 ∈ 𝑐} ⊆ {𝑐 ∈ (𝑂 ∖ 𝐸) ∣ ¬ 1 ∈ 𝑐} ↔ ∀𝑐(𝑐 ∈ {𝑐 ∈ 𝑂 ∣ ¬ 1 ∈ 𝑐} → 𝑐 ∈ {𝑐 ∈ (𝑂 ∖ 𝐸) ∣ ¬ 1 ∈ 𝑐}))
102	42, 43, 7, 18, 64, 1	ballotlem4 30560	. . . . . . . . . . . . . 14 ⊢ (𝑐 ∈ 𝑂 → (¬ 1 ∈ 𝑐 → ¬ 𝑐 ∈ 𝐸))
103	102	imdistani 726	. . . . . . . . . . . . 13 ⊢ ((𝑐 ∈ 𝑂 ∧ ¬ 1 ∈ 𝑐) → (𝑐 ∈ 𝑂 ∧ ¬ 𝑐 ∈ 𝐸))
104		rabid 3116	. . . . . . . . . . . . 13 ⊢ (𝑐 ∈ {𝑐 ∈ 𝑂 ∣ ¬ 1 ∈ 𝑐} ↔ (𝑐 ∈ 𝑂 ∧ ¬ 1 ∈ 𝑐))
105		eldif 3584	. . . . . . . . . . . . 13 ⊢ (𝑐 ∈ (𝑂 ∖ 𝐸) ↔ (𝑐 ∈ 𝑂 ∧ ¬ 𝑐 ∈ 𝐸))
106	103, 104, 105	3imtr4i 281	. . . . . . . . . . . 12 ⊢ (𝑐 ∈ {𝑐 ∈ 𝑂 ∣ ¬ 1 ∈ 𝑐} → 𝑐 ∈ (𝑂 ∖ 𝐸))
107	104	simprbi 480	. . . . . . . . . . . 12 ⊢ (𝑐 ∈ {𝑐 ∈ 𝑂 ∣ ¬ 1 ∈ 𝑐} → ¬ 1 ∈ 𝑐)
108		rabid 3116	. . . . . . . . . . . 12 ⊢ (𝑐 ∈ {𝑐 ∈ (𝑂 ∖ 𝐸) ∣ ¬ 1 ∈ 𝑐} ↔ (𝑐 ∈ (𝑂 ∖ 𝐸) ∧ ¬ 1 ∈ 𝑐))
109	106, 107, 108	sylanbrc 698	. . . . . . . . . . 11 ⊢ (𝑐 ∈ {𝑐 ∈ 𝑂 ∣ ¬ 1 ∈ 𝑐} → 𝑐 ∈ {𝑐 ∈ (𝑂 ∖ 𝐸) ∣ ¬ 1 ∈ 𝑐})
110	101, 109	mpgbir 1726	. . . . . . . . . 10 ⊢ {𝑐 ∈ 𝑂 ∣ ¬ 1 ∈ 𝑐} ⊆ {𝑐 ∈ (𝑂 ∖ 𝐸) ∣ ¬ 1 ∈ 𝑐}
111		rabss2 3685	. . . . . . . . . . 11 ⊢ ((𝑂 ∖ 𝐸) ⊆ 𝑂 → {𝑐 ∈ (𝑂 ∖ 𝐸) ∣ ¬ 1 ∈ 𝑐} ⊆ {𝑐 ∈ 𝑂 ∣ ¬ 1 ∈ 𝑐})
112	32, 111	ax-mp 5	. . . . . . . . . 10 ⊢ {𝑐 ∈ (𝑂 ∖ 𝐸) ∣ ¬ 1 ∈ 𝑐} ⊆ {𝑐 ∈ 𝑂 ∣ ¬ 1 ∈ 𝑐}
113	110, 112	eqssi 3619	. . . . . . . . 9 ⊢ {𝑐 ∈ 𝑂 ∣ ¬ 1 ∈ 𝑐} = {𝑐 ∈ (𝑂 ∖ 𝐸) ∣ ¬ 1 ∈ 𝑐}
114	113	fveq2i 6194	. . . . . . . 8 ⊢ (#‘{𝑐 ∈ 𝑂 ∣ ¬ 1 ∈ 𝑐}) = (#‘{𝑐 ∈ (𝑂 ∖ 𝐸) ∣ ¬ 1 ∈ 𝑐})
115	114	oveq1i 6660	. . . . . . 7 ⊢ ((#‘{𝑐 ∈ 𝑂 ∣ ¬ 1 ∈ 𝑐}) / (#‘𝑂)) = ((#‘{𝑐 ∈ (𝑂 ∖ 𝐸) ∣ ¬ 1 ∈ 𝑐}) / (#‘𝑂))
116	97, 98, 115	3eqtr3i 2652	. . . . . 6 ⊢ (𝑁 / (𝑀 + 𝑁)) = ((#‘{𝑐 ∈ (𝑂 ∖ 𝐸) ∣ ¬ 1 ∈ 𝑐}) / (#‘𝑂))
117	116	oveq2i 6661	. . . . 5 ⊢ (2 · (𝑁 / (𝑀 + 𝑁))) = (2 · ((#‘{𝑐 ∈ (𝑂 ∖ 𝐸) ∣ ¬ 1 ∈ 𝑐}) / (#‘𝑂)))
118		2cn 11091	. . . . . 6 ⊢ 2 ∈ ℂ
119		hashcl 13147	. . . . . . . 8 ⊢ ({𝑐 ∈ (𝑂 ∖ 𝐸) ∣ ¬ 1 ∈ 𝑐} ∈ Fin → (#‘{𝑐 ∈ (𝑂 ∖ 𝐸) ∣ ¬ 1 ∈ 𝑐}) ∈ ℕ₀)
120	83, 119	ax-mp 5	. . . . . . 7 ⊢ (#‘{𝑐 ∈ (𝑂 ∖ 𝐸) ∣ ¬ 1 ∈ 𝑐}) ∈ ℕ₀
121	120	nn0cni 11304	. . . . . 6 ⊢ (#‘{𝑐 ∈ (𝑂 ∖ 𝐸) ∣ ¬ 1 ∈ 𝑐}) ∈ ℂ
122	118, 121, 28, 57	divassi 10781	. . . . 5 ⊢ ((2 · (#‘{𝑐 ∈ (𝑂 ∖ 𝐸) ∣ ¬ 1 ∈ 𝑐})) / (#‘𝑂)) = (2 · ((#‘{𝑐 ∈ (𝑂 ∖ 𝐸) ∣ ¬ 1 ∈ 𝑐}) / (#‘𝑂)))
123	121	2timesi 11147	. . . . . 6 ⊢ (2 · (#‘{𝑐 ∈ (𝑂 ∖ 𝐸) ∣ ¬ 1 ∈ 𝑐})) = ((#‘{𝑐 ∈ (𝑂 ∖ 𝐸) ∣ ¬ 1 ∈ 𝑐}) + (#‘{𝑐 ∈ (𝑂 ∖ 𝐸) ∣ ¬ 1 ∈ 𝑐}))
124	123	oveq1i 6660	. . . . 5 ⊢ ((2 · (#‘{𝑐 ∈ (𝑂 ∖ 𝐸) ∣ ¬ 1 ∈ 𝑐})) / (#‘𝑂)) = (((#‘{𝑐 ∈ (𝑂 ∖ 𝐸) ∣ ¬ 1 ∈ 𝑐}) + (#‘{𝑐 ∈ (𝑂 ∖ 𝐸) ∣ ¬ 1 ∈ 𝑐})) / (#‘𝑂))
125	117, 122, 124	3eqtr2i 2650	. . . 4 ⊢ (2 · (𝑁 / (𝑀 + 𝑁))) = (((#‘{𝑐 ∈ (𝑂 ∖ 𝐸) ∣ ¬ 1 ∈ 𝑐}) + (#‘{𝑐 ∈ (𝑂 ∖ 𝐸) ∣ ¬ 1 ∈ 𝑐})) / (#‘𝑂))
126	71, 88, 125	3eqtr4ri 2655	. . 3 ⊢ (2 · (𝑁 / (𝑀 + 𝑁))) = ((#‘(𝑂 ∖ 𝐸)) / (#‘𝑂))
127	126	oveq2i 6661	. 2 ⊢ (1 − (2 · (𝑁 / (𝑀 + 𝑁)))) = (1 − ((#‘(𝑂 ∖ 𝐸)) / (#‘𝑂)))
128	47	nncni 11030	. . . 4 ⊢ (𝑀 + 𝑁) ∈ ℂ
129	43	nncni 11030	. . . . 5 ⊢ 𝑁 ∈ ℂ
130	118, 129	mulcli 10045	. . . 4 ⊢ (2 · 𝑁) ∈ ℂ
131	47	nnne0i 11055	. . . . 5 ⊢ (𝑀 + 𝑁) ≠ 0
132	128, 131	pm3.2i 471	. . . 4 ⊢ ((𝑀 + 𝑁) ∈ ℂ ∧ (𝑀 + 𝑁) ≠ 0)
133		divsubdir 10721	. . . 4 ⊢ (((𝑀 + 𝑁) ∈ ℂ ∧ (2 · 𝑁) ∈ ℂ ∧ ((𝑀 + 𝑁) ∈ ℂ ∧ (𝑀 + 𝑁) ≠ 0)) → (((𝑀 + 𝑁) − (2 · 𝑁)) / (𝑀 + 𝑁)) = (((𝑀 + 𝑁) / (𝑀 + 𝑁)) − ((2 · 𝑁) / (𝑀 + 𝑁))))
134	128, 130, 132, 133	mp3an 1424	. . 3 ⊢ (((𝑀 + 𝑁) − (2 · 𝑁)) / (𝑀 + 𝑁)) = (((𝑀 + 𝑁) / (𝑀 + 𝑁)) − ((2 · 𝑁) / (𝑀 + 𝑁)))
135	129	2timesi 11147	. . . . . 6 ⊢ (2 · 𝑁) = (𝑁 + 𝑁)
136	135	oveq2i 6661	. . . . 5 ⊢ ((𝑀 + 𝑁) − (2 · 𝑁)) = ((𝑀 + 𝑁) − (𝑁 + 𝑁))
137	42	nncni 11030	. . . . . . 7 ⊢ 𝑀 ∈ ℂ
138	137, 129, 129, 129	addsub4i 10377	. . . . . 6 ⊢ ((𝑀 + 𝑁) − (𝑁 + 𝑁)) = ((𝑀 − 𝑁) + (𝑁 − 𝑁))
139	129	subidi 10352	. . . . . . 7 ⊢ (𝑁 − 𝑁) = 0
140	139	oveq2i 6661	. . . . . 6 ⊢ ((𝑀 − 𝑁) + (𝑁 − 𝑁)) = ((𝑀 − 𝑁) + 0)
141	137, 129	subcli 10357	. . . . . . 7 ⊢ (𝑀 − 𝑁) ∈ ℂ
142	141	addid1i 10223	. . . . . 6 ⊢ ((𝑀 − 𝑁) + 0) = (𝑀 − 𝑁)
143	138, 140, 142	3eqtri 2648	. . . . 5 ⊢ ((𝑀 + 𝑁) − (𝑁 + 𝑁)) = (𝑀 − 𝑁)
144	136, 143	eqtri 2644	. . . 4 ⊢ ((𝑀 + 𝑁) − (2 · 𝑁)) = (𝑀 − 𝑁)
145	144	oveq1i 6660	. . 3 ⊢ (((𝑀 + 𝑁) − (2 · 𝑁)) / (𝑀 + 𝑁)) = ((𝑀 − 𝑁) / (𝑀 + 𝑁))
146	128, 131	dividi 10758	. . . 4 ⊢ ((𝑀 + 𝑁) / (𝑀 + 𝑁)) = 1
147	118, 129, 128, 131	divassi 10781	. . . 4 ⊢ ((2 · 𝑁) / (𝑀 + 𝑁)) = (2 · (𝑁 / (𝑀 + 𝑁)))
148	146, 147	oveq12i 6662	. . 3 ⊢ (((𝑀 + 𝑁) / (𝑀 + 𝑁)) − ((2 · 𝑁) / (𝑀 + 𝑁))) = (1 − (2 · (𝑁 / (𝑀 + 𝑁))))
149	134, 145, 148	3eqtr3ri 2653	. 2 ⊢ (1 − (2 · (𝑁 / (𝑀 + 𝑁)))) = ((𝑀 − 𝑁) / (𝑀 + 𝑁))
150	63, 127, 149	3eqtr2i 2650	1 ⊢ (𝑃‘𝐸) = ((𝑀 − 𝑁) / (𝑀 + 𝑁))

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ∧ wa 384 = wceq 1483 ∈ wcel 1990 ≠ wne 2794 ∀wral 2912 {crab 2916 ∖ cdif 3571 ∪ cun 3572 ∩ cin 3573 ⊆ wss 3574 ∅c0 3915 ifcif 4086 𝒫 cpw 4158 class class class wbr 4653 ↦ cmpt 4729 “ cima 5117 ‘cfv 5888 (class class class)co 6650 Fincfn 7955 infcinf 8347 ℂcc 9934 ℝcr 9935 0cc0 9936 1c1 9937 + caddc 9939 · cmul 9941 < clt 10074 ≤ cle 10075 − cmin 10266 / cdiv 10684 ℕcn 11020 2c2 11070 ℕ₀cn0 11292 ℤcz 11377 ...cfz 12326 Ccbc 13089 #chash 13117

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1722 ax-4 1737 ax-5 1839 ax-6 1888 ax-7 1935 ax-8 1992 ax-9 1999 ax-10 2019 ax-11 2034 ax-12 2047 ax-13 2246 ax-ext 2602 ax-rep 4771 ax-sep 4781 ax-nul 4789 ax-pow 4843 ax-pr 4906 ax-un 6949 ax-cnex 9992 ax-resscn 9993 ax-1cn 9994 ax-icn 9995 ax-addcl 9996 ax-addrcl 9997 ax-mulcl 9998 ax-mulrcl 9999 ax-mulcom 10000 ax-addass 10001 ax-mulass 10002 ax-distr 10003 ax-i2m1 10004 ax-1ne0 10005 ax-1rid 10006 ax-rnegex 10007 ax-rrecex 10008 ax-cnre 10009 ax-pre-lttri 10010 ax-pre-lttrn 10011 ax-pre-ltadd 10012 ax-pre-mulgt0 10013

This theorem depends on definitions: df-bi 197 df-or 385 df-an 386 df-3or 1038 df-3an 1039 df-tru 1486 df-ex 1705 df-nf 1710 df-sb 1881 df-eu 2474 df-mo 2475 df-clab 2609 df-cleq 2615 df-clel 2618 df-nfc 2753 df-ne 2795 df-nel 2898 df-ral 2917 df-rex 2918 df-reu 2919 df-rmo 2920 df-rab 2921 df-v 3202 df-sbc 3436 df-csb 3534 df-dif 3577 df-un 3579 df-in 3581 df-ss 3588 df-pss 3590 df-nul 3916 df-if 4087 df-pw 4160 df-sn 4178 df-pr 4180 df-tp 4182 df-op 4184 df-uni 4437 df-int 4476 df-iun 4522 df-br 4654 df-opab 4713 df-mpt 4730 df-tr 4753 df-id 5024 df-eprel 5029 df-po 5035 df-so 5036 df-fr 5073 df-we 5075 df-xp 5120 df-rel 5121 df-cnv 5122 df-co 5123 df-dm 5124 df-rn 5125 df-res 5126 df-ima 5127 df-pred 5680 df-ord 5726 df-on 5727 df-lim 5728 df-suc 5729 df-iota 5851 df-fun 5890 df-fn 5891 df-f 5892 df-f1 5893 df-fo 5894 df-f1o 5895 df-fv 5896 df-riota 6611 df-ov 6653 df-oprab 6654 df-mpt2 6655 df-om 7066 df-1st 7168 df-2nd 7169 df-wrecs 7407 df-recs 7468 df-rdg 7506 df-1o 7560 df-2o 7561 df-oadd 7564 df-er 7742 df-map 7859 df-en 7956 df-dom 7957 df-sdom 7958 df-fin 7959 df-sup 8348 df-inf 8349 df-card 8765 df-cda 8990 df-pnf 10076 df-mnf 10077 df-xr 10078 df-ltxr 10079 df-le 10080 df-sub 10268 df-neg 10269 df-div 10685 df-nn 11021 df-2 11079 df-n0 11293 df-z 11378 df-uz 11688 df-rp 11833 df-fz 12327 df-seq 12802 df-fac 13061 df-bc 13090 df-hash 13118

This theorem is referenced by: (None)

W3C validator