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

Theorem ballotlem2 30678
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.
StepHypRef Expression
1 ssrab2 3720 . . . . 5 {𝑐𝑂 ∣ ¬ 1 ∈ 𝑐} ⊆ 𝑂
2 ballotth.m . . . . . . 7 𝑀 ∈ ℕ
3 ballotth.n . . . . . . 7 𝑁 ∈ ℕ
4 ballotth.o . . . . . . 7 𝑂 = {𝑐 ∈ 𝒫 (1...(𝑀 + 𝑁)) ∣ (#‘𝑐) = 𝑀}
52, 3, 4ballotlemoex 30675 . . . . . 6 𝑂 ∈ V
65elpw2 4858 . . . . 5 ({𝑐𝑂 ∣ ¬ 1 ∈ 𝑐} ∈ 𝒫 𝑂 ↔ {𝑐𝑂 ∣ ¬ 1 ∈ 𝑐} ⊆ 𝑂)
71, 6mpbir 221 . . . 4 {𝑐𝑂 ∣ ¬ 1 ∈ 𝑐} ∈ 𝒫 𝑂
8 fveq2 6229 . . . . . 6 (𝑥 = {𝑐𝑂 ∣ ¬ 1 ∈ 𝑐} → (#‘𝑥) = (#‘{𝑐𝑂 ∣ ¬ 1 ∈ 𝑐}))
98oveq1d 6705 . . . . 5 (𝑥 = {𝑐𝑂 ∣ ¬ 1 ∈ 𝑐} → ((#‘𝑥) / (#‘𝑂)) = ((#‘{𝑐𝑂 ∣ ¬ 1 ∈ 𝑐}) / (#‘𝑂)))
10 ballotth.p . . . . 5 𝑃 = (𝑥 ∈ 𝒫 𝑂 ↦ ((#‘𝑥) / (#‘𝑂)))
11 ovex 6718 . . . . 5 ((#‘{𝑐𝑂 ∣ ¬ 1 ∈ 𝑐}) / (#‘𝑂)) ∈ V
129, 10, 11fvmpt 6321 . . . 4 ({𝑐𝑂 ∣ ¬ 1 ∈ 𝑐} ∈ 𝒫 𝑂 → (𝑃‘{𝑐𝑂 ∣ ¬ 1 ∈ 𝑐}) = ((#‘{𝑐𝑂 ∣ ¬ 1 ∈ 𝑐}) / (#‘𝑂)))
137, 12ax-mp 5 . . 3 (𝑃‘{𝑐𝑂 ∣ ¬ 1 ∈ 𝑐}) = ((#‘{𝑐𝑂 ∣ ¬ 1 ∈ 𝑐}) / (#‘𝑂))
14 an32 856 . . . . . . . . 9 (((𝑐 ∈ 𝒫 (1...(𝑀 + 𝑁)) ∧ ¬ 1 ∈ 𝑐) ∧ (#‘𝑐) = 𝑀) ↔ ((𝑐 ∈ 𝒫 (1...(𝑀 + 𝑁)) ∧ (#‘𝑐) = 𝑀) ∧ ¬ 1 ∈ 𝑐))
15 2eluzge1 11772 . . . . . . . . . . . . . . 15 2 ∈ (ℤ‘1)
16 fzss1 12418 . . . . . . . . . . . . . . 15 (2 ∈ (ℤ‘1) → (2...(𝑀 + 𝑁)) ⊆ (1...(𝑀 + 𝑁)))
1715, 16ax-mp 5 . . . . . . . . . . . . . 14 (2...(𝑀 + 𝑁)) ⊆ (1...(𝑀 + 𝑁))
18 sspwb 4947 . . . . . . . . . . . . . 14 ((2...(𝑀 + 𝑁)) ⊆ (1...(𝑀 + 𝑁)) ↔ 𝒫 (2...(𝑀 + 𝑁)) ⊆ 𝒫 (1...(𝑀 + 𝑁)))
1917, 18mpbi 220 . . . . . . . . . . . . 13 𝒫 (2...(𝑀 + 𝑁)) ⊆ 𝒫 (1...(𝑀 + 𝑁))
2019sseli 3632 . . . . . . . . . . . 12 (𝑐 ∈ 𝒫 (2...(𝑀 + 𝑁)) → 𝑐 ∈ 𝒫 (1...(𝑀 + 𝑁)))
21 1lt2 11232 . . . . . . . . . . . . . . . . 17 1 < 2
22 1re 10077 . . . . . . . . . . . . . . . . . 18 1 ∈ ℝ
23 2re 11128 . . . . . . . . . . . . . . . . . 18 2 ∈ ℝ
2422, 23ltnlei 10196 . . . . . . . . . . . . . . . . 17 (1 < 2 ↔ ¬ 2 ≤ 1)
2521, 24mpbi 220 . . . . . . . . . . . . . . . 16 ¬ 2 ≤ 1
26 elfzle1 12382 . . . . . . . . . . . . . . . 16 (1 ∈ (2...(𝑀 + 𝑁)) → 2 ≤ 1)
2725, 26mto 188 . . . . . . . . . . . . . . 15 ¬ 1 ∈ (2...(𝑀 + 𝑁))
28 elelpwi 4204 . . . . . . . . . . . . . . 15 ((1 ∈ 𝑐𝑐 ∈ 𝒫 (2...(𝑀 + 𝑁))) → 1 ∈ (2...(𝑀 + 𝑁)))
2927, 28mto 188 . . . . . . . . . . . . . 14 ¬ (1 ∈ 𝑐𝑐 ∈ 𝒫 (2...(𝑀 + 𝑁)))
30 ancom 465 . . . . . . . . . . . . . 14 ((1 ∈ 𝑐𝑐 ∈ 𝒫 (2...(𝑀 + 𝑁))) ↔ (𝑐 ∈ 𝒫 (2...(𝑀 + 𝑁)) ∧ 1 ∈ 𝑐))
3129, 30mtbi 311 . . . . . . . . . . . . 13 ¬ (𝑐 ∈ 𝒫 (2...(𝑀 + 𝑁)) ∧ 1 ∈ 𝑐)
3231imnani 438 . . . . . . . . . . . 12 (𝑐 ∈ 𝒫 (2...(𝑀 + 𝑁)) → ¬ 1 ∈ 𝑐)
3320, 32jca 553 . . . . . . . . . . 11 (𝑐 ∈ 𝒫 (2...(𝑀 + 𝑁)) → (𝑐 ∈ 𝒫 (1...(𝑀 + 𝑁)) ∧ ¬ 1 ∈ 𝑐))
34 ssin 3868 . . . . . . . . . . . . 13 ((𝑐 ⊆ (1...(𝑀 + 𝑁)) ∧ 𝑐 ⊆ {𝑖 ∣ ¬ 𝑖 = 1}) ↔ 𝑐 ⊆ ((1...(𝑀 + 𝑁)) ∩ {𝑖 ∣ ¬ 𝑖 = 1}))
35 1le2 11279 . . . . . . . . . . . . . . . . . . . . . 22 1 ≤ 2
36 1p1e2 11172 . . . . . . . . . . . . . . . . . . . . . . 23 (1 + 1) = 2
37 nnge1 11084 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑀 ∈ ℕ → 1 ≤ 𝑀)
382, 37ax-mp 5 . . . . . . . . . . . . . . . . . . . . . . . 24 1 ≤ 𝑀
39 nnge1 11084 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑁 ∈ ℕ → 1 ≤ 𝑁)
403, 39ax-mp 5 . . . . . . . . . . . . . . . . . . . . . . . 24 1 ≤ 𝑁
412nnrei 11067 . . . . . . . . . . . . . . . . . . . . . . . . 25 𝑀 ∈ ℝ
423nnrei 11067 . . . . . . . . . . . . . . . . . . . . . . . . 25 𝑁 ∈ ℝ
4322, 22, 41, 42le2addi 10629 . . . . . . . . . . . . . . . . . . . . . . . 24 ((1 ≤ 𝑀 ∧ 1 ≤ 𝑁) → (1 + 1) ≤ (𝑀 + 𝑁))
4438, 40, 43mp2an 708 . . . . . . . . . . . . . . . . . . . . . . 23 (1 + 1) ≤ (𝑀 + 𝑁)
4536, 44eqbrtrri 4708 . . . . . . . . . . . . . . . . . . . . . 22 2 ≤ (𝑀 + 𝑁)
4641, 42readdcli 10091 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑀 + 𝑁) ∈ ℝ
4722, 23, 46letri 10204 . . . . . . . . . . . . . . . . . . . . . 22 ((1 ≤ 2 ∧ 2 ≤ (𝑀 + 𝑁)) → 1 ≤ (𝑀 + 𝑁))
4835, 45, 47mp2an 708 . . . . . . . . . . . . . . . . . . . . 21 1 ≤ (𝑀 + 𝑁)
49 1z 11445 . . . . . . . . . . . . . . . . . . . . . 22 1 ∈ ℤ
50 nnaddcl 11080 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) → (𝑀 + 𝑁) ∈ ℕ)
512, 3, 50mp2an 708 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑀 + 𝑁) ∈ ℕ
5251nnzi 11439 . . . . . . . . . . . . . . . . . . . . . 22 (𝑀 + 𝑁) ∈ ℤ
53 eluz 11739 . . . . . . . . . . . . . . . . . . . . . 22 ((1 ∈ ℤ ∧ (𝑀 + 𝑁) ∈ ℤ) → ((𝑀 + 𝑁) ∈ (ℤ‘1) ↔ 1 ≤ (𝑀 + 𝑁)))
5449, 52, 53mp2an 708 . . . . . . . . . . . . . . . . . . . . 21 ((𝑀 + 𝑁) ∈ (ℤ‘1) ↔ 1 ≤ (𝑀 + 𝑁))
5548, 54mpbir 221 . . . . . . . . . . . . . . . . . . . 20 (𝑀 + 𝑁) ∈ (ℤ‘1)
56 elfzp12 12457 . . . . . . . . . . . . . . . . . . . 20 ((𝑀 + 𝑁) ∈ (ℤ‘1) → (𝑖 ∈ (1...(𝑀 + 𝑁)) ↔ (𝑖 = 1 ∨ 𝑖 ∈ ((1 + 1)...(𝑀 + 𝑁)))))
5755, 56ax-mp 5 . . . . . . . . . . . . . . . . . . 19 (𝑖 ∈ (1...(𝑀 + 𝑁)) ↔ (𝑖 = 1 ∨ 𝑖 ∈ ((1 + 1)...(𝑀 + 𝑁))))
5857biimpi 206 . . . . . . . . . . . . . . . . . 18 (𝑖 ∈ (1...(𝑀 + 𝑁)) → (𝑖 = 1 ∨ 𝑖 ∈ ((1 + 1)...(𝑀 + 𝑁))))
5958orcanai 972 . . . . . . . . . . . . . . . . 17 ((𝑖 ∈ (1...(𝑀 + 𝑁)) ∧ ¬ 𝑖 = 1) → 𝑖 ∈ ((1 + 1)...(𝑀 + 𝑁)))
6036oveq1i 6700 . . . . . . . . . . . . . . . . 17 ((1 + 1)...(𝑀 + 𝑁)) = (2...(𝑀 + 𝑁))
6159, 60syl6eleq 2740 . . . . . . . . . . . . . . . 16 ((𝑖 ∈ (1...(𝑀 + 𝑁)) ∧ ¬ 𝑖 = 1) → 𝑖 ∈ (2...(𝑀 + 𝑁)))
6261ss2abi 3707 . . . . . . . . . . . . . . 15 {𝑖 ∣ (𝑖 ∈ (1...(𝑀 + 𝑁)) ∧ ¬ 𝑖 = 1)} ⊆ {𝑖𝑖 ∈ (2...(𝑀 + 𝑁))}
63 inab 3928 . . . . . . . . . . . . . . . 16 ({𝑖𝑖 ∈ (1...(𝑀 + 𝑁))} ∩ {𝑖 ∣ ¬ 𝑖 = 1}) = {𝑖 ∣ (𝑖 ∈ (1...(𝑀 + 𝑁)) ∧ ¬ 𝑖 = 1)}
64 abid2 2774 . . . . . . . . . . . . . . . . 17 {𝑖𝑖 ∈ (1...(𝑀 + 𝑁))} = (1...(𝑀 + 𝑁))
6564ineq1i 3843 . . . . . . . . . . . . . . . 16 ({𝑖𝑖 ∈ (1...(𝑀 + 𝑁))} ∩ {𝑖 ∣ ¬ 𝑖 = 1}) = ((1...(𝑀 + 𝑁)) ∩ {𝑖 ∣ ¬ 𝑖 = 1})
6663, 65eqtr3i 2675 . . . . . . . . . . . . . . 15 {𝑖 ∣ (𝑖 ∈ (1...(𝑀 + 𝑁)) ∧ ¬ 𝑖 = 1)} = ((1...(𝑀 + 𝑁)) ∩ {𝑖 ∣ ¬ 𝑖 = 1})
67 abid2 2774 . . . . . . . . . . . . . . 15 {𝑖𝑖 ∈ (2...(𝑀 + 𝑁))} = (2...(𝑀 + 𝑁))
6862, 66, 673sstr3i 3676 . . . . . . . . . . . . . 14 ((1...(𝑀 + 𝑁)) ∩ {𝑖 ∣ ¬ 𝑖 = 1}) ⊆ (2...(𝑀 + 𝑁))
69 sstr 3644 . . . . . . . . . . . . . 14 ((𝑐 ⊆ ((1...(𝑀 + 𝑁)) ∩ {𝑖 ∣ ¬ 𝑖 = 1}) ∧ ((1...(𝑀 + 𝑁)) ∩ {𝑖 ∣ ¬ 𝑖 = 1}) ⊆ (2...(𝑀 + 𝑁))) → 𝑐 ⊆ (2...(𝑀 + 𝑁)))
7068, 69mpan2 707 . . . . . . . . . . . . 13 (𝑐 ⊆ ((1...(𝑀 + 𝑁)) ∩ {𝑖 ∣ ¬ 𝑖 = 1}) → 𝑐 ⊆ (2...(𝑀 + 𝑁)))
7134, 70sylbi 207 . . . . . . . . . . . 12 ((𝑐 ⊆ (1...(𝑀 + 𝑁)) ∧ 𝑐 ⊆ {𝑖 ∣ ¬ 𝑖 = 1}) → 𝑐 ⊆ (2...(𝑀 + 𝑁)))
72 selpw 4198 . . . . . . . . . . . . 13 (𝑐 ∈ 𝒫 (1...(𝑀 + 𝑁)) ↔ 𝑐 ⊆ (1...(𝑀 + 𝑁)))
73 ssab 3705 . . . . . . . . . . . . . 14 (𝑐 ⊆ {𝑖 ∣ ¬ 𝑖 = 1} ↔ ∀𝑖(𝑖𝑐 → ¬ 𝑖 = 1))
74 df-ex 1745 . . . . . . . . . . . . . . . . 17 (∃𝑖(𝑖 = 1 ∧ 𝑖𝑐) ↔ ¬ ∀𝑖 ¬ (𝑖 = 1 ∧ 𝑖𝑐))
7574bicomi 214 . . . . . . . . . . . . . . . 16 (¬ ∀𝑖 ¬ (𝑖 = 1 ∧ 𝑖𝑐) ↔ ∃𝑖(𝑖 = 1 ∧ 𝑖𝑐))
7675con1bii 345 . . . . . . . . . . . . . . 15 (¬ ∃𝑖(𝑖 = 1 ∧ 𝑖𝑐) ↔ ∀𝑖 ¬ (𝑖 = 1 ∧ 𝑖𝑐))
77 df-clel 2647 . . . . . . . . . . . . . . . 16 (1 ∈ 𝑐 ↔ ∃𝑖(𝑖 = 1 ∧ 𝑖𝑐))
7877notbii 309 . . . . . . . . . . . . . . 15 (¬ 1 ∈ 𝑐 ↔ ¬ ∃𝑖(𝑖 = 1 ∧ 𝑖𝑐))
79 imnang 1809 . . . . . . . . . . . . . . . 16 (∀𝑖(𝑖𝑐 → ¬ 𝑖 = 1) ↔ ∀𝑖 ¬ (𝑖𝑐𝑖 = 1))
80 ancom 465 . . . . . . . . . . . . . . . . . 18 ((𝑖 = 1 ∧ 𝑖𝑐) ↔ (𝑖𝑐𝑖 = 1))
8180notbii 309 . . . . . . . . . . . . . . . . 17 (¬ (𝑖 = 1 ∧ 𝑖𝑐) ↔ ¬ (𝑖𝑐𝑖 = 1))
8281albii 1787 . . . . . . . . . . . . . . . 16 (∀𝑖 ¬ (𝑖 = 1 ∧ 𝑖𝑐) ↔ ∀𝑖 ¬ (𝑖𝑐𝑖 = 1))
8379, 82bitr4i 267 . . . . . . . . . . . . . . 15 (∀𝑖(𝑖𝑐 → ¬ 𝑖 = 1) ↔ ∀𝑖 ¬ (𝑖 = 1 ∧ 𝑖𝑐))
8476, 78, 833bitr4ri 293 . . . . . . . . . . . . . 14 (∀𝑖(𝑖𝑐 → ¬ 𝑖 = 1) ↔ ¬ 1 ∈ 𝑐)
8573, 84bitr2i 265 . . . . . . . . . . . . 13 (¬ 1 ∈ 𝑐𝑐 ⊆ {𝑖 ∣ ¬ 𝑖 = 1})
8672, 85anbi12i 733 . . . . . . . . . . . 12 ((𝑐 ∈ 𝒫 (1...(𝑀 + 𝑁)) ∧ ¬ 1 ∈ 𝑐) ↔ (𝑐 ⊆ (1...(𝑀 + 𝑁)) ∧ 𝑐 ⊆ {𝑖 ∣ ¬ 𝑖 = 1}))
87 selpw 4198 . . . . . . . . . . . 12 (𝑐 ∈ 𝒫 (2...(𝑀 + 𝑁)) ↔ 𝑐 ⊆ (2...(𝑀 + 𝑁)))
8871, 86, 873imtr4i 281 . . . . . . . . . . 11 ((𝑐 ∈ 𝒫 (1...(𝑀 + 𝑁)) ∧ ¬ 1 ∈ 𝑐) → 𝑐 ∈ 𝒫 (2...(𝑀 + 𝑁)))
8933, 88impbii 199 . . . . . . . . . 10 (𝑐 ∈ 𝒫 (2...(𝑀 + 𝑁)) ↔ (𝑐 ∈ 𝒫 (1...(𝑀 + 𝑁)) ∧ ¬ 1 ∈ 𝑐))
9089anbi1i 731 . . . . . . . . 9 ((𝑐 ∈ 𝒫 (2...(𝑀 + 𝑁)) ∧ (#‘𝑐) = 𝑀) ↔ ((𝑐 ∈ 𝒫 (1...(𝑀 + 𝑁)) ∧ ¬ 1 ∈ 𝑐) ∧ (#‘𝑐) = 𝑀))
914rabeq2i 3228 . . . . . . . . . 10 (𝑐𝑂 ↔ (𝑐 ∈ 𝒫 (1...(𝑀 + 𝑁)) ∧ (#‘𝑐) = 𝑀))
9291anbi1i 731 . . . . . . . . 9 ((𝑐𝑂 ∧ ¬ 1 ∈ 𝑐) ↔ ((𝑐 ∈ 𝒫 (1...(𝑀 + 𝑁)) ∧ (#‘𝑐) = 𝑀) ∧ ¬ 1 ∈ 𝑐))
9314, 90, 923bitr4i 292 . . . . . . . 8 ((𝑐 ∈ 𝒫 (2...(𝑀 + 𝑁)) ∧ (#‘𝑐) = 𝑀) ↔ (𝑐𝑂 ∧ ¬ 1 ∈ 𝑐))
9493abbii 2768 . . . . . . 7 {𝑐 ∣ (𝑐 ∈ 𝒫 (2...(𝑀 + 𝑁)) ∧ (#‘𝑐) = 𝑀)} = {𝑐 ∣ (𝑐𝑂 ∧ ¬ 1 ∈ 𝑐)}
95 df-rab 2950 . . . . . . 7 {𝑐 ∈ 𝒫 (2...(𝑀 + 𝑁)) ∣ (#‘𝑐) = 𝑀} = {𝑐 ∣ (𝑐 ∈ 𝒫 (2...(𝑀 + 𝑁)) ∧ (#‘𝑐) = 𝑀)}
96 df-rab 2950 . . . . . . 7 {𝑐𝑂 ∣ ¬ 1 ∈ 𝑐} = {𝑐 ∣ (𝑐𝑂 ∧ ¬ 1 ∈ 𝑐)}
9794, 95, 963eqtr4i 2683 . . . . . 6 {𝑐 ∈ 𝒫 (2...(𝑀 + 𝑁)) ∣ (#‘𝑐) = 𝑀} = {𝑐𝑂 ∣ ¬ 1 ∈ 𝑐}
9897fveq2i 6232 . . . . 5 (#‘{𝑐 ∈ 𝒫 (2...(𝑀 + 𝑁)) ∣ (#‘𝑐) = 𝑀}) = (#‘{𝑐𝑂 ∣ ¬ 1 ∈ 𝑐})
99 fzfi 12811 . . . . . . 7 (2...(𝑀 + 𝑁)) ∈ Fin
1002nnzi 11439 . . . . . . 7 𝑀 ∈ ℤ
101 hashbc 13275 . . . . . . 7 (((2...(𝑀 + 𝑁)) ∈ Fin ∧ 𝑀 ∈ ℤ) → ((#‘(2...(𝑀 + 𝑁)))C𝑀) = (#‘{𝑐 ∈ 𝒫 (2...(𝑀 + 𝑁)) ∣ (#‘𝑐) = 𝑀}))
10299, 100, 101mp2an 708 . . . . . 6 ((#‘(2...(𝑀 + 𝑁)))C𝑀) = (#‘{𝑐 ∈ 𝒫 (2...(𝑀 + 𝑁)) ∣ (#‘𝑐) = 𝑀})
103 2z 11447 . . . . . . . . . . . 12 2 ∈ ℤ
104103eluz1i 11733 . . . . . . . . . . 11 ((𝑀 + 𝑁) ∈ (ℤ‘2) ↔ ((𝑀 + 𝑁) ∈ ℤ ∧ 2 ≤ (𝑀 + 𝑁)))
10552, 45, 104mpbir2an 975 . . . . . . . . . 10 (𝑀 + 𝑁) ∈ (ℤ‘2)
106 hashfz 13252 . . . . . . . . . 10 ((𝑀 + 𝑁) ∈ (ℤ‘2) → (#‘(2...(𝑀 + 𝑁))) = (((𝑀 + 𝑁) − 2) + 1))
107105, 106ax-mp 5 . . . . . . . . 9 (#‘(2...(𝑀 + 𝑁))) = (((𝑀 + 𝑁) − 2) + 1)
1082nncni 11068 . . . . . . . . . . 11 𝑀 ∈ ℂ
1093nncni 11068 . . . . . . . . . . 11 𝑁 ∈ ℂ
110108, 109addcli 10082 . . . . . . . . . 10 (𝑀 + 𝑁) ∈ ℂ
111 2cn 11129 . . . . . . . . . 10 2 ∈ ℂ
112 ax-1cn 10032 . . . . . . . . . 10 1 ∈ ℂ
113 subadd23 10331 . . . . . . . . . 10 (((𝑀 + 𝑁) ∈ ℂ ∧ 2 ∈ ℂ ∧ 1 ∈ ℂ) → (((𝑀 + 𝑁) − 2) + 1) = ((𝑀 + 𝑁) + (1 − 2)))
114110, 111, 112, 113mp3an 1464 . . . . . . . . 9 (((𝑀 + 𝑁) − 2) + 1) = ((𝑀 + 𝑁) + (1 − 2))
115111, 112negsubdi2i 10405 . . . . . . . . . . 11 -(2 − 1) = (1 − 2)
116 2m1e1 11173 . . . . . . . . . . . 12 (2 − 1) = 1
117116negeqi 10312 . . . . . . . . . . 11 -(2 − 1) = -1
118115, 117eqtr3i 2675 . . . . . . . . . 10 (1 − 2) = -1
119118oveq2i 6701 . . . . . . . . 9 ((𝑀 + 𝑁) + (1 − 2)) = ((𝑀 + 𝑁) + -1)
120107, 114, 1193eqtri 2677 . . . . . . . 8 (#‘(2...(𝑀 + 𝑁))) = ((𝑀 + 𝑁) + -1)
121110, 112negsubi 10397 . . . . . . . 8 ((𝑀 + 𝑁) + -1) = ((𝑀 + 𝑁) − 1)
122120, 121eqtri 2673 . . . . . . 7 (#‘(2...(𝑀 + 𝑁))) = ((𝑀 + 𝑁) − 1)
123122oveq1i 6700 . . . . . 6 ((#‘(2...(𝑀 + 𝑁)))C𝑀) = (((𝑀 + 𝑁) − 1)C𝑀)
124102, 123eqtr3i 2675 . . . . 5 (#‘{𝑐 ∈ 𝒫 (2...(𝑀 + 𝑁)) ∣ (#‘𝑐) = 𝑀}) = (((𝑀 + 𝑁) − 1)C𝑀)
12598, 124eqtr3i 2675 . . . 4 (#‘{𝑐𝑂 ∣ ¬ 1 ∈ 𝑐}) = (((𝑀 + 𝑁) − 1)C𝑀)
1262, 3, 4ballotlem1 30676 . . . 4 (#‘𝑂) = ((𝑀 + 𝑁)C𝑀)
127125, 126oveq12i 6702 . . 3 ((#‘{𝑐𝑂 ∣ ¬ 1 ∈ 𝑐}) / (#‘𝑂)) = ((((𝑀 + 𝑁) − 1)C𝑀) / ((𝑀 + 𝑁)C𝑀))
12813, 127eqtri 2673 . 2 (𝑃‘{𝑐𝑂 ∣ ¬ 1 ∈ 𝑐}) = ((((𝑀 + 𝑁) − 1)C𝑀) / ((𝑀 + 𝑁)C𝑀))
129 0le1 10589 . . . . 5 0 ≤ 1
130 0re 10078 . . . . . 6 0 ∈ ℝ
131130, 22, 41letri 10204 . . . . 5 ((0 ≤ 1 ∧ 1 ≤ 𝑀) → 0 ≤ 𝑀)
132129, 38, 131mp2an 708 . . . 4 0 ≤ 𝑀
1333nngt0i 11092 . . . . . 6 0 < 𝑁
13442, 133elrpii 11873 . . . . 5 𝑁 ∈ ℝ+
135 ltaddrp 11905 . . . . 5 ((𝑀 ∈ ℝ ∧ 𝑁 ∈ ℝ+) → 𝑀 < (𝑀 + 𝑁))
13641, 134, 135mp2an 708 . . . 4 𝑀 < (𝑀 + 𝑁)
137 0z 11426 . . . . 5 0 ∈ ℤ
138 elfzm11 12449 . . . . 5 ((0 ∈ ℤ ∧ (𝑀 + 𝑁) ∈ ℤ) → (𝑀 ∈ (0...((𝑀 + 𝑁) − 1)) ↔ (𝑀 ∈ ℤ ∧ 0 ≤ 𝑀𝑀 < (𝑀 + 𝑁))))
139137, 52, 138mp2an 708 . . . 4 (𝑀 ∈ (0...((𝑀 + 𝑁) − 1)) ↔ (𝑀 ∈ ℤ ∧ 0 ≤ 𝑀𝑀 < (𝑀 + 𝑁)))
140100, 132, 136, 139mpbir3an 1263 . . 3 𝑀 ∈ (0...((𝑀 + 𝑁) − 1))
141 bcm1n 29682 . . 3 ((𝑀 ∈ (0...((𝑀 + 𝑁) − 1)) ∧ (𝑀 + 𝑁) ∈ ℕ) → ((((𝑀 + 𝑁) − 1)C𝑀) / ((𝑀 + 𝑁)C𝑀)) = (((𝑀 + 𝑁) − 𝑀) / (𝑀 + 𝑁)))
142140, 51, 141mp2an 708 . 2 ((((𝑀 + 𝑁) − 1)C𝑀) / ((𝑀 + 𝑁)C𝑀)) = (((𝑀 + 𝑁) − 𝑀) / (𝑀 + 𝑁))
143 pncan2 10326 . . . 4 ((𝑀 ∈ ℂ ∧ 𝑁 ∈ ℂ) → ((𝑀 + 𝑁) − 𝑀) = 𝑁)
144108, 109, 143mp2an 708 . . 3 ((𝑀 + 𝑁) − 𝑀) = 𝑁
145144oveq1i 6700 . 2 (((𝑀 + 𝑁) − 𝑀) / (𝑀 + 𝑁)) = (𝑁 / (𝑀 + 𝑁))
146128, 142, 1453eqtri 2677 1 (𝑃‘{𝑐𝑂 ∣ ¬ 1 ∈ 𝑐}) = (𝑁 / (𝑀 + 𝑁))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 196  wo 382  wa 383  w3a 1054  wal 1521   = wceq 1523  wex 1744  wcel 2030  {cab 2637  {crab 2945  cin 3606  wss 3607  𝒫 cpw 4191   class class class wbr 4685  cmpt 4762  cfv 5926  (class class class)co 6690  Fincfn 7997  cc 9972  cr 9973  0cc0 9974  1c1 9975   + caddc 9977   < clt 10112  cle 10113  cmin 10304  -cneg 10305   / cdiv 10722  cn 11058  2c2 11108  cz 11415  cuz 11725  +crp 11870  ...cfz 12364  Ccbc 13129  #chash 13157
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-8 2032  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631  ax-rep 4804  ax-sep 4814  ax-nul 4822  ax-pow 4873  ax-pr 4936  ax-un 6991  ax-cnex 10030  ax-resscn 10031  ax-1cn 10032  ax-icn 10033  ax-addcl 10034  ax-addrcl 10035  ax-mulcl 10036  ax-mulrcl 10037  ax-mulcom 10038  ax-addass 10039  ax-mulass 10040  ax-distr 10041  ax-i2m1 10042  ax-1ne0 10043  ax-1rid 10044  ax-rnegex 10045  ax-rrecex 10046  ax-cnre 10047  ax-pre-lttri 10048  ax-pre-lttrn 10049  ax-pre-ltadd 10050  ax-pre-mulgt0 10051
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3or 1055  df-3an 1056  df-tru 1526  df-ex 1745  df-nf 1750  df-sb 1938  df-eu 2502  df-mo 2503  df-clab 2638  df-cleq 2644  df-clel 2647  df-nfc 2782  df-ne 2824  df-nel 2927  df-ral 2946  df-rex 2947  df-reu 2948  df-rmo 2949  df-rab 2950  df-v 3233  df-sbc 3469  df-csb 3567  df-dif 3610  df-un 3612  df-in 3614  df-ss 3621  df-pss 3623  df-nul 3949  df-if 4120  df-pw 4193  df-sn 4211  df-pr 4213  df-tp 4215  df-op 4217  df-uni 4469  df-int 4508  df-iun 4554  df-br 4686  df-opab 4746  df-mpt 4763  df-tr 4786  df-id 5053  df-eprel 5058  df-po 5064  df-so 5065  df-fr 5102  df-we 5104  df-xp 5149  df-rel 5150  df-cnv 5151  df-co 5152  df-dm 5153  df-rn 5154  df-res 5155  df-ima 5156  df-pred 5718  df-ord 5764  df-on 5765  df-lim 5766  df-suc 5767  df-iota 5889  df-fun 5928  df-fn 5929  df-f 5930  df-f1 5931  df-fo 5932  df-f1o 5933  df-fv 5934  df-riota 6651  df-ov 6693  df-oprab 6694  df-mpt2 6695  df-om 7108  df-1st 7210  df-2nd 7211  df-wrecs 7452  df-recs 7513  df-rdg 7551  df-1o 7605  df-2o 7606  df-oadd 7609  df-er 7787  df-map 7901  df-en 7998  df-dom 7999  df-sdom 8000  df-fin 8001  df-card 8803  df-cda 9028  df-pnf 10114  df-mnf 10115  df-xr 10116  df-ltxr 10117  df-le 10118  df-sub 10306  df-neg 10307  df-div 10723  df-nn 11059  df-2 11117  df-n0 11331  df-z 11416  df-uz 11726  df-rp 11871  df-fz 12365  df-seq 12842  df-fac 13101  df-bc 13130  df-hash 13158
This theorem is referenced by:  ballotth  30727
  Copyright terms: Public domain W3C validator