Metamath Proof Explorer

Theorem ballotlem2

Description: The probability that the first vote picked in a count is a B. (Contributed by Thierry Arnoux, 23-Nov-2016)

Ref Expression
Hypotheses ballotth.m ⊢ 𝑀 ∈ ℕ
ballotth.n ⊢ 𝑁 ∈ ℕ
ballotth.o ⊢ 𝑂 = { 𝑐 ∈ 𝒫 ( 1 ... ( 𝑀 + 𝑁 ) ) ∣ ( ♯ ‘ 𝑐 ) = 𝑀 }
ballotth.p ⊢ 𝑃 = ( 𝑥 ∈ 𝒫 𝑂 ↦ ( ( ♯ ‘ 𝑥 ) / ( ♯ ‘ 𝑂 ) ) )
Assertion ballotlem2 ( 𝑃 ‘ { 𝑐 ∈ 𝑂 ∣ ¬ 1 ∈ 𝑐 } ) = ( 𝑁 / ( 𝑀 + 𝑁 ) )

Proof

Step Hyp Ref Expression
1 ballotth.m ⊢ 𝑀 ∈ ℕ
2 ballotth.n ⊢ 𝑁 ∈ ℕ
3 ballotth.o ⊢ 𝑂 = { 𝑐 ∈ 𝒫 ( 1 ... ( 𝑀 + 𝑁 ) ) ∣ ( ♯ ‘ 𝑐 ) = 𝑀 }
4 ballotth.p ⊢ 𝑃 = ( 𝑥 ∈ 𝒫 𝑂 ↦ ( ( ♯ ‘ 𝑥 ) / ( ♯ ‘ 𝑂 ) ) )
5 1 2 3 ballotlemoex ⊢ 𝑂 ∈ V
6 ssrab2 ⊢ { 𝑐 ∈ 𝑂 ∣ ¬ 1 ∈ 𝑐 } ⊆ 𝑂
7 5 6 elpwi2 ⊢ { 𝑐 ∈ 𝑂 ∣ ¬ 1 ∈ 𝑐 } ∈ 𝒫 𝑂
8 fveq2 ⊢ ( 𝑥 = { 𝑐 ∈ 𝑂 ∣ ¬ 1 ∈ 𝑐 } → ( ♯ ‘ 𝑥 ) = ( ♯ ‘ { 𝑐 ∈ 𝑂 ∣ ¬ 1 ∈ 𝑐 } ) )
9 8 oveq1d ⊢ ( 𝑥 = { 𝑐 ∈ 𝑂 ∣ ¬ 1 ∈ 𝑐 } → ( ( ♯ ‘ 𝑥 ) / ( ♯ ‘ 𝑂 ) ) = ( ( ♯ ‘ { 𝑐 ∈ 𝑂 ∣ ¬ 1 ∈ 𝑐 } ) / ( ♯ ‘ 𝑂 ) ) )
10 ovex ⊢ ( ( ♯ ‘ { 𝑐 ∈ 𝑂 ∣ ¬ 1 ∈ 𝑐 } ) / ( ♯ ‘ 𝑂 ) ) ∈ V
11 9 4 10 fvmpt ⊢ ( { 𝑐 ∈ 𝑂 ∣ ¬ 1 ∈ 𝑐 } ∈ 𝒫 𝑂 → ( 𝑃 ‘ { 𝑐 ∈ 𝑂 ∣ ¬ 1 ∈ 𝑐 } ) = ( ( ♯ ‘ { 𝑐 ∈ 𝑂 ∣ ¬ 1 ∈ 𝑐 } ) / ( ♯ ‘ 𝑂 ) ) )
12 7 11 ax-mp ⊢ ( 𝑃 ‘ { 𝑐 ∈ 𝑂 ∣ ¬ 1 ∈ 𝑐 } ) = ( ( ♯ ‘ { 𝑐 ∈ 𝑂 ∣ ¬ 1 ∈ 𝑐 } ) / ( ♯ ‘ 𝑂 ) )
13 an32 ⊢ ( ( ( 𝑐 ∈ 𝒫 ( 1 ... ( 𝑀 + 𝑁 ) ) ∧ ¬ 1 ∈ 𝑐 ) ∧ ( ♯ ‘ 𝑐 ) = 𝑀 ) ↔ ( ( 𝑐 ∈ 𝒫 ( 1 ... ( 𝑀 + 𝑁 ) ) ∧ ( ♯ ‘ 𝑐 ) = 𝑀 ) ∧ ¬ 1 ∈ 𝑐 ) )
14 2eluzge1 ⊢ 2 ∈ ( ℤ≥ ‘ 1 )
15 fzss1 ⊢ ( 2 ∈ ( ℤ≥ ‘ 1 ) → ( 2 ... ( 𝑀 + 𝑁 ) ) ⊆ ( 1 ... ( 𝑀 + 𝑁 ) ) )
16 14 15 ax-mp ⊢ ( 2 ... ( 𝑀 + 𝑁 ) ) ⊆ ( 1 ... ( 𝑀 + 𝑁 ) )
17 16 sspwi ⊢ 𝒫 ( 2 ... ( 𝑀 + 𝑁 ) ) ⊆ 𝒫 ( 1 ... ( 𝑀 + 𝑁 ) )
18 17 sseli ⊢ ( 𝑐 ∈ 𝒫 ( 2 ... ( 𝑀 + 𝑁 ) ) → 𝑐 ∈ 𝒫 ( 1 ... ( 𝑀 + 𝑁 ) ) )
19 1lt2 ⊢ 1 < 2
20 1re ⊢ 1 ∈ ℝ
21 2re ⊢ 2 ∈ ℝ
22 20 21 ltnlei ⊢ ( 1 < 2 ↔ ¬ 2 ≤ 1 )
23 19 22 mpbi ⊢ ¬ 2 ≤ 1
24 elfzle1 ⊢ ( 1 ∈ ( 2 ... ( 𝑀 + 𝑁 ) ) → 2 ≤ 1 )
25 23 24 mto ⊢ ¬ 1 ∈ ( 2 ... ( 𝑀 + 𝑁 ) )
26 elelpwi ⊢ ( ( 1 ∈ 𝑐 ∧ 𝑐 ∈ 𝒫 ( 2 ... ( 𝑀 + 𝑁 ) ) ) → 1 ∈ ( 2 ... ( 𝑀 + 𝑁 ) ) )
27 25 26 mto ⊢ ¬ ( 1 ∈ 𝑐 ∧ 𝑐 ∈ 𝒫 ( 2 ... ( 𝑀 + 𝑁 ) ) )
28 ancom ⊢ ( ( 1 ∈ 𝑐 ∧ 𝑐 ∈ 𝒫 ( 2 ... ( 𝑀 + 𝑁 ) ) ) ↔ ( 𝑐 ∈ 𝒫 ( 2 ... ( 𝑀 + 𝑁 ) ) ∧ 1 ∈ 𝑐 ) )
29 27 28 mtbi ⊢ ¬ ( 𝑐 ∈ 𝒫 ( 2 ... ( 𝑀 + 𝑁 ) ) ∧ 1 ∈ 𝑐 )
30 29 imnani ⊢ ( 𝑐 ∈ 𝒫 ( 2 ... ( 𝑀 + 𝑁 ) ) → ¬ 1 ∈ 𝑐 )
31 18 30 jca ⊢ ( 𝑐 ∈ 𝒫 ( 2 ... ( 𝑀 + 𝑁 ) ) → ( 𝑐 ∈ 𝒫 ( 1 ... ( 𝑀 + 𝑁 ) ) ∧ ¬ 1 ∈ 𝑐 ) )
32 ssin ⊢ ( ( 𝑐 ⊆ ( 1 ... ( 𝑀 + 𝑁 ) ) ∧ 𝑐 ⊆ { 𝑖 ∣ ¬ 𝑖 = 1 } ) ↔ 𝑐 ⊆ ( ( 1 ... ( 𝑀 + 𝑁 ) ) ∩ { 𝑖 ∣ ¬ 𝑖 = 1 } ) )
33 1le2 ⊢ 1 ≤ 2
34 1p1e2 ⊢ ( 1 + 1 ) = 2
35 nnge1 ⊢ ( 𝑀 ∈ ℕ → 1 ≤ 𝑀 )
36 1 35 ax-mp ⊢ 1 ≤ 𝑀
37 nnge1 ⊢ ( 𝑁 ∈ ℕ → 1 ≤ 𝑁 )
38 2 37 ax-mp ⊢ 1 ≤ 𝑁
39 1 nnrei ⊢ 𝑀 ∈ ℝ
40 2 nnrei ⊢ 𝑁 ∈ ℝ
41 20 20 39 40 le2addi ⊢ ( ( 1 ≤ 𝑀 ∧ 1 ≤ 𝑁 ) → ( 1 + 1 ) ≤ ( 𝑀 + 𝑁 ) )
42 36 38 41 mp2an ⊢ ( 1 + 1 ) ≤ ( 𝑀 + 𝑁 )
43 34 42 eqbrtrri ⊢ 2 ≤ ( 𝑀 + 𝑁 )
44 39 40 readdcli ⊢ ( 𝑀 + 𝑁 ) ∈ ℝ
45 20 21 44 letri ⊢ ( ( 1 ≤ 2 ∧ 2 ≤ ( 𝑀 + 𝑁 ) ) → 1 ≤ ( 𝑀 + 𝑁 ) )
46 33 43 45 mp2an ⊢ 1 ≤ ( 𝑀 + 𝑁 )
47 1z ⊢ 1 ∈ ℤ
48 nnaddcl ⊢ ( ( 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ) → ( 𝑀 + 𝑁 ) ∈ ℕ )
49 1 2 48 mp2an ⊢ ( 𝑀 + 𝑁 ) ∈ ℕ
50 49 nnzi ⊢ ( 𝑀 + 𝑁 ) ∈ ℤ
51 eluz ⊢ ( ( 1 ∈ ℤ ∧ ( 𝑀 + 𝑁 ) ∈ ℤ ) → ( ( 𝑀 + 𝑁 ) ∈ ( ℤ≥ ‘ 1 ) ↔ 1 ≤ ( 𝑀 + 𝑁 ) ) )
52 47 50 51 mp2an ⊢ ( ( 𝑀 + 𝑁 ) ∈ ( ℤ≥ ‘ 1 ) ↔ 1 ≤ ( 𝑀 + 𝑁 ) )
53 46 52 mpbir ⊢ ( 𝑀 + 𝑁 ) ∈ ( ℤ≥ ‘ 1 )
54 elfzp12 ⊢ ( ( 𝑀 + 𝑁 ) ∈ ( ℤ≥ ‘ 1 ) → ( 𝑖 ∈ ( 1 ... ( 𝑀 + 𝑁 ) ) ↔ ( 𝑖 = 1 ∨ 𝑖 ∈ ( ( 1 + 1 ) ... ( 𝑀 + 𝑁 ) ) ) ) )
55 53 54 ax-mp ⊢ ( 𝑖 ∈ ( 1 ... ( 𝑀 + 𝑁 ) ) ↔ ( 𝑖 = 1 ∨ 𝑖 ∈ ( ( 1 + 1 ) ... ( 𝑀 + 𝑁 ) ) ) )
56 55 biimpi ⊢ ( 𝑖 ∈ ( 1 ... ( 𝑀 + 𝑁 ) ) → ( 𝑖 = 1 ∨ 𝑖 ∈ ( ( 1 + 1 ) ... ( 𝑀 + 𝑁 ) ) ) )
57 56 orcanai ⊢ ( ( 𝑖 ∈ ( 1 ... ( 𝑀 + 𝑁 ) ) ∧ ¬ 𝑖 = 1 ) → 𝑖 ∈ ( ( 1 + 1 ) ... ( 𝑀 + 𝑁 ) ) )
58 34 oveq1i ⊢ ( ( 1 + 1 ) ... ( 𝑀 + 𝑁 ) ) = ( 2 ... ( 𝑀 + 𝑁 ) )
59 57 58 eleqtrdi ⊢ ( ( 𝑖 ∈ ( 1 ... ( 𝑀 + 𝑁 ) ) ∧ ¬ 𝑖 = 1 ) → 𝑖 ∈ ( 2 ... ( 𝑀 + 𝑁 ) ) )
60 59 ss2abi ⊢ { 𝑖 ∣ ( 𝑖 ∈ ( 1 ... ( 𝑀 + 𝑁 ) ) ∧ ¬ 𝑖 = 1 ) } ⊆ { 𝑖 ∣ 𝑖 ∈ ( 2 ... ( 𝑀 + 𝑁 ) ) }
61 inab ⊢ ( { 𝑖 ∣ 𝑖 ∈ ( 1 ... ( 𝑀 + 𝑁 ) ) } ∩ { 𝑖 ∣ ¬ 𝑖 = 1 } ) = { 𝑖 ∣ ( 𝑖 ∈ ( 1 ... ( 𝑀 + 𝑁 ) ) ∧ ¬ 𝑖 = 1 ) }
62 abid2 ⊢ { 𝑖 ∣ 𝑖 ∈ ( 1 ... ( 𝑀 + 𝑁 ) ) } = ( 1 ... ( 𝑀 + 𝑁 ) )
63 62 ineq1i ⊢ ( { 𝑖 ∣ 𝑖 ∈ ( 1 ... ( 𝑀 + 𝑁 ) ) } ∩ { 𝑖 ∣ ¬ 𝑖 = 1 } ) = ( ( 1 ... ( 𝑀 + 𝑁 ) ) ∩ { 𝑖 ∣ ¬ 𝑖 = 1 } )
64 61 63 eqtr3i ⊢ { 𝑖 ∣ ( 𝑖 ∈ ( 1 ... ( 𝑀 + 𝑁 ) ) ∧ ¬ 𝑖 = 1 ) } = ( ( 1 ... ( 𝑀 + 𝑁 ) ) ∩ { 𝑖 ∣ ¬ 𝑖 = 1 } )
65 abid2 ⊢ { 𝑖 ∣ 𝑖 ∈ ( 2 ... ( 𝑀 + 𝑁 ) ) } = ( 2 ... ( 𝑀 + 𝑁 ) )
66 60 64 65 3sstr3i ⊢ ( ( 1 ... ( 𝑀 + 𝑁 ) ) ∩ { 𝑖 ∣ ¬ 𝑖 = 1 } ) ⊆ ( 2 ... ( 𝑀 + 𝑁 ) )
67 sstr ⊢ ( ( 𝑐 ⊆ ( ( 1 ... ( 𝑀 + 𝑁 ) ) ∩ { 𝑖 ∣ ¬ 𝑖 = 1 } ) ∧ ( ( 1 ... ( 𝑀 + 𝑁 ) ) ∩ { 𝑖 ∣ ¬ 𝑖 = 1 } ) ⊆ ( 2 ... ( 𝑀 + 𝑁 ) ) ) → 𝑐 ⊆ ( 2 ... ( 𝑀 + 𝑁 ) ) )
68 66 67 mpan2 ⊢ ( 𝑐 ⊆ ( ( 1 ... ( 𝑀 + 𝑁 ) ) ∩ { 𝑖 ∣ ¬ 𝑖 = 1 } ) → 𝑐 ⊆ ( 2 ... ( 𝑀 + 𝑁 ) ) )
69 32 68 sylbi ⊢ ( ( 𝑐 ⊆ ( 1 ... ( 𝑀 + 𝑁 ) ) ∧ 𝑐 ⊆ { 𝑖 ∣ ¬ 𝑖 = 1 } ) → 𝑐 ⊆ ( 2 ... ( 𝑀 + 𝑁 ) ) )
70 velpw ⊢ ( 𝑐 ∈ 𝒫 ( 1 ... ( 𝑀 + 𝑁 ) ) ↔ 𝑐 ⊆ ( 1 ... ( 𝑀 + 𝑁 ) ) )
71 ssab ⊢ ( 𝑐 ⊆ { 𝑖 ∣ ¬ 𝑖 = 1 } ↔ ∀ 𝑖 ( 𝑖 ∈ 𝑐 → ¬ 𝑖 = 1 ) )
72 df-ex ⊢ ( ∃ 𝑖 ( 𝑖 = 1 ∧ 𝑖 ∈ 𝑐 ) ↔ ¬ ∀ 𝑖 ¬ ( 𝑖 = 1 ∧ 𝑖 ∈ 𝑐 ) )
73 72 bicomi ⊢ ( ¬ ∀ 𝑖 ¬ ( 𝑖 = 1 ∧ 𝑖 ∈ 𝑐 ) ↔ ∃ 𝑖 ( 𝑖 = 1 ∧ 𝑖 ∈ 𝑐 ) )
74 73 con1bii ⊢ ( ¬ ∃ 𝑖 ( 𝑖 = 1 ∧ 𝑖 ∈ 𝑐 ) ↔ ∀ 𝑖 ¬ ( 𝑖 = 1 ∧ 𝑖 ∈ 𝑐 ) )
75 dfclel ⊢ ( 1 ∈ 𝑐 ↔ ∃ 𝑖 ( 𝑖 = 1 ∧ 𝑖 ∈ 𝑐 ) )
76 75 notbii ⊢ ( ¬ 1 ∈ 𝑐 ↔ ¬ ∃ 𝑖 ( 𝑖 = 1 ∧ 𝑖 ∈ 𝑐 ) )
77 imnang ⊢ ( ∀ 𝑖 ( 𝑖 ∈ 𝑐 → ¬ 𝑖 = 1 ) ↔ ∀ 𝑖 ¬ ( 𝑖 ∈ 𝑐 ∧ 𝑖 = 1 ) )
78 ancom ⊢ ( ( 𝑖 = 1 ∧ 𝑖 ∈ 𝑐 ) ↔ ( 𝑖 ∈ 𝑐 ∧ 𝑖 = 1 ) )
79 78 notbii ⊢ ( ¬ ( 𝑖 = 1 ∧ 𝑖 ∈ 𝑐 ) ↔ ¬ ( 𝑖 ∈ 𝑐 ∧ 𝑖 = 1 ) )
80 79 albii ⊢ ( ∀ 𝑖 ¬ ( 𝑖 = 1 ∧ 𝑖 ∈ 𝑐 ) ↔ ∀ 𝑖 ¬ ( 𝑖 ∈ 𝑐 ∧ 𝑖 = 1 ) )
81 77 80 bitr4i ⊢ ( ∀ 𝑖 ( 𝑖 ∈ 𝑐 → ¬ 𝑖 = 1 ) ↔ ∀ 𝑖 ¬ ( 𝑖 = 1 ∧ 𝑖 ∈ 𝑐 ) )
82 74 76 81 3bitr4ri ⊢ ( ∀ 𝑖 ( 𝑖 ∈ 𝑐 → ¬ 𝑖 = 1 ) ↔ ¬ 1 ∈ 𝑐 )
83 71 82 bitr2i ⊢ ( ¬ 1 ∈ 𝑐 ↔ 𝑐 ⊆ { 𝑖 ∣ ¬ 𝑖 = 1 } )
84 70 83 anbi12i ⊢ ( ( 𝑐 ∈ 𝒫 ( 1 ... ( 𝑀 + 𝑁 ) ) ∧ ¬ 1 ∈ 𝑐 ) ↔ ( 𝑐 ⊆ ( 1 ... ( 𝑀 + 𝑁 ) ) ∧ 𝑐 ⊆ { 𝑖 ∣ ¬ 𝑖 = 1 } ) )
85 velpw ⊢ ( 𝑐 ∈ 𝒫 ( 2 ... ( 𝑀 + 𝑁 ) ) ↔ 𝑐 ⊆ ( 2 ... ( 𝑀 + 𝑁 ) ) )
86 69 84 85 3imtr4i ⊢ ( ( 𝑐 ∈ 𝒫 ( 1 ... ( 𝑀 + 𝑁 ) ) ∧ ¬ 1 ∈ 𝑐 ) → 𝑐 ∈ 𝒫 ( 2 ... ( 𝑀 + 𝑁 ) ) )
87 31 86 impbii ⊢ ( 𝑐 ∈ 𝒫 ( 2 ... ( 𝑀 + 𝑁 ) ) ↔ ( 𝑐 ∈ 𝒫 ( 1 ... ( 𝑀 + 𝑁 ) ) ∧ ¬ 1 ∈ 𝑐 ) )
88 87 anbi1i ⊢ ( ( 𝑐 ∈ 𝒫 ( 2 ... ( 𝑀 + 𝑁 ) ) ∧ ( ♯ ‘ 𝑐 ) = 𝑀 ) ↔ ( ( 𝑐 ∈ 𝒫 ( 1 ... ( 𝑀 + 𝑁 ) ) ∧ ¬ 1 ∈ 𝑐 ) ∧ ( ♯ ‘ 𝑐 ) = 𝑀 ) )
89 3 rabeq2i ⊢ ( 𝑐 ∈ 𝑂 ↔ ( 𝑐 ∈ 𝒫 ( 1 ... ( 𝑀 + 𝑁 ) ) ∧ ( ♯ ‘ 𝑐 ) = 𝑀 ) )
90 89 anbi1i ⊢ ( ( 𝑐 ∈ 𝑂 ∧ ¬ 1 ∈ 𝑐 ) ↔ ( ( 𝑐 ∈ 𝒫 ( 1 ... ( 𝑀 + 𝑁 ) ) ∧ ( ♯ ‘ 𝑐 ) = 𝑀 ) ∧ ¬ 1 ∈ 𝑐 ) )
91 13 88 90 3bitr4i ⊢ ( ( 𝑐 ∈ 𝒫 ( 2 ... ( 𝑀 + 𝑁 ) ) ∧ ( ♯ ‘ 𝑐 ) = 𝑀 ) ↔ ( 𝑐 ∈ 𝑂 ∧ ¬ 1 ∈ 𝑐 ) )
92 91 rabbia2 ⊢ { 𝑐 ∈ 𝒫 ( 2 ... ( 𝑀 + 𝑁 ) ) ∣ ( ♯ ‘ 𝑐 ) = 𝑀 } = { 𝑐 ∈ 𝑂 ∣ ¬ 1 ∈ 𝑐 }
93 92 fveq2i ⊢ ( ♯ ‘ { 𝑐 ∈ 𝒫 ( 2 ... ( 𝑀 + 𝑁 ) ) ∣ ( ♯ ‘ 𝑐 ) = 𝑀 } ) = ( ♯ ‘ { 𝑐 ∈ 𝑂 ∣ ¬ 1 ∈ 𝑐 } )
94 fzfi ⊢ ( 2 ... ( 𝑀 + 𝑁 ) ) ∈ Fin
95 1 nnzi ⊢ 𝑀 ∈ ℤ
96 hashbc ⊢ ( ( ( 2 ... ( 𝑀 + 𝑁 ) ) ∈ Fin ∧ 𝑀 ∈ ℤ ) → ( ( ♯ ‘ ( 2 ... ( 𝑀 + 𝑁 ) ) ) C 𝑀 ) = ( ♯ ‘ { 𝑐 ∈ 𝒫 ( 2 ... ( 𝑀 + 𝑁 ) ) ∣ ( ♯ ‘ 𝑐 ) = 𝑀 } ) )
97 94 95 96 mp2an ⊢ ( ( ♯ ‘ ( 2 ... ( 𝑀 + 𝑁 ) ) ) C 𝑀 ) = ( ♯ ‘ { 𝑐 ∈ 𝒫 ( 2 ... ( 𝑀 + 𝑁 ) ) ∣ ( ♯ ‘ 𝑐 ) = 𝑀 } )
98 2z ⊢ 2 ∈ ℤ
99 98 eluz1i ⊢ ( ( 𝑀 + 𝑁 ) ∈ ( ℤ≥ ‘ 2 ) ↔ ( ( 𝑀 + 𝑁 ) ∈ ℤ ∧ 2 ≤ ( 𝑀 + 𝑁 ) ) )
100 50 43 99 mpbir2an ⊢ ( 𝑀 + 𝑁 ) ∈ ( ℤ≥ ‘ 2 )
101 hashfz ⊢ ( ( 𝑀 + 𝑁 ) ∈ ( ℤ≥ ‘ 2 ) → ( ♯ ‘ ( 2 ... ( 𝑀 + 𝑁 ) ) ) = ( ( ( 𝑀 + 𝑁 ) − 2 ) + 1 ) )
102 100 101 ax-mp ⊢ ( ♯ ‘ ( 2 ... ( 𝑀 + 𝑁 ) ) ) = ( ( ( 𝑀 + 𝑁 ) − 2 ) + 1 )
103 1 nncni ⊢ 𝑀 ∈ ℂ
104 2 nncni ⊢ 𝑁 ∈ ℂ
105 103 104 addcli ⊢ ( 𝑀 + 𝑁 ) ∈ ℂ
106 2cn ⊢ 2 ∈ ℂ
107 ax-1cn ⊢ 1 ∈ ℂ
108 subadd23 ⊢ ( ( ( 𝑀 + 𝑁 ) ∈ ℂ ∧ 2 ∈ ℂ ∧ 1 ∈ ℂ ) → ( ( ( 𝑀 + 𝑁 ) − 2 ) + 1 ) = ( ( 𝑀 + 𝑁 ) + ( 1 − 2 ) ) )
109 105 106 107 108 mp3an ⊢ ( ( ( 𝑀 + 𝑁 ) − 2 ) + 1 ) = ( ( 𝑀 + 𝑁 ) + ( 1 − 2 ) )
110 106 107 negsubdi2i ⊢ - ( 2 − 1 ) = ( 1 − 2 )
111 2m1e1 ⊢ ( 2 − 1 ) = 1
112 111 negeqi ⊢ - ( 2 − 1 ) = - 1
113 110 112 eqtr3i ⊢ ( 1 − 2 ) = - 1
114 113 oveq2i ⊢ ( ( 𝑀 + 𝑁 ) + ( 1 − 2 ) ) = ( ( 𝑀 + 𝑁 ) + - 1 )
115 102 109 114 3eqtri ⊢ ( ♯ ‘ ( 2 ... ( 𝑀 + 𝑁 ) ) ) = ( ( 𝑀 + 𝑁 ) + - 1 )
116 105 107 negsubi ⊢ ( ( 𝑀 + 𝑁 ) + - 1 ) = ( ( 𝑀 + 𝑁 ) − 1 )
117 115 116 eqtri ⊢ ( ♯ ‘ ( 2 ... ( 𝑀 + 𝑁 ) ) ) = ( ( 𝑀 + 𝑁 ) − 1 )
118 117 oveq1i ⊢ ( ( ♯ ‘ ( 2 ... ( 𝑀 + 𝑁 ) ) ) C 𝑀 ) = ( ( ( 𝑀 + 𝑁 ) − 1 ) C 𝑀 )
119 97 118 eqtr3i ⊢ ( ♯ ‘ { 𝑐 ∈ 𝒫 ( 2 ... ( 𝑀 + 𝑁 ) ) ∣ ( ♯ ‘ 𝑐 ) = 𝑀 } ) = ( ( ( 𝑀 + 𝑁 ) − 1 ) C 𝑀 )
120 93 119 eqtr3i ⊢ ( ♯ ‘ { 𝑐 ∈ 𝑂 ∣ ¬ 1 ∈ 𝑐 } ) = ( ( ( 𝑀 + 𝑁 ) − 1 ) C 𝑀 )
121 1 2 3 ballotlem1 ⊢ ( ♯ ‘ 𝑂 ) = ( ( 𝑀 + 𝑁 ) C 𝑀 )
122 120 121 oveq12i ⊢ ( ( ♯ ‘ { 𝑐 ∈ 𝑂 ∣ ¬ 1 ∈ 𝑐 } ) / ( ♯ ‘ 𝑂 ) ) = ( ( ( ( 𝑀 + 𝑁 ) − 1 ) C 𝑀 ) / ( ( 𝑀 + 𝑁 ) C 𝑀 ) )
123 12 122 eqtri ⊢ ( 𝑃 ‘ { 𝑐 ∈ 𝑂 ∣ ¬ 1 ∈ 𝑐 } ) = ( ( ( ( 𝑀 + 𝑁 ) − 1 ) C 𝑀 ) / ( ( 𝑀 + 𝑁 ) C 𝑀 ) )
124 0le1 ⊢ 0 ≤ 1
125 0re ⊢ 0 ∈ ℝ
126 125 20 39 letri ⊢ ( ( 0 ≤ 1 ∧ 1 ≤ 𝑀 ) → 0 ≤ 𝑀 )
127 124 36 126 mp2an ⊢ 0 ≤ 𝑀
128 2 nngt0i ⊢ 0 < 𝑁
129 40 128 elrpii ⊢ 𝑁 ∈ ℝ+
130 ltaddrp ⊢ ( ( 𝑀 ∈ ℝ ∧ 𝑁 ∈ ℝ+ ) → 𝑀 < ( 𝑀 + 𝑁 ) )
131 39 129 130 mp2an ⊢ 𝑀 < ( 𝑀 + 𝑁 )
132 0z ⊢ 0 ∈ ℤ
133 elfzm11 ⊢ ( ( 0 ∈ ℤ ∧ ( 𝑀 + 𝑁 ) ∈ ℤ ) → ( 𝑀 ∈ ( 0 ... ( ( 𝑀 + 𝑁 ) − 1 ) ) ↔ ( 𝑀 ∈ ℤ ∧ 0 ≤ 𝑀 ∧ 𝑀 < ( 𝑀 + 𝑁 ) ) ) )
134 132 50 133 mp2an ⊢ ( 𝑀 ∈ ( 0 ... ( ( 𝑀 + 𝑁 ) − 1 ) ) ↔ ( 𝑀 ∈ ℤ ∧ 0 ≤ 𝑀 ∧ 𝑀 < ( 𝑀 + 𝑁 ) ) )
135 95 127 131 134 mpbir3an ⊢ 𝑀 ∈ ( 0 ... ( ( 𝑀 + 𝑁 ) − 1 ) )
136 bcm1n ⊢ ( ( 𝑀 ∈ ( 0 ... ( ( 𝑀 + 𝑁 ) − 1 ) ) ∧ ( 𝑀 + 𝑁 ) ∈ ℕ ) → ( ( ( ( 𝑀 + 𝑁 ) − 1 ) C 𝑀 ) / ( ( 𝑀 + 𝑁 ) C 𝑀 ) ) = ( ( ( 𝑀 + 𝑁 ) − 𝑀 ) / ( 𝑀 + 𝑁 ) ) )
137 135 49 136 mp2an ⊢ ( ( ( ( 𝑀 + 𝑁 ) − 1 ) C 𝑀 ) / ( ( 𝑀 + 𝑁 ) C 𝑀 ) ) = ( ( ( 𝑀 + 𝑁 ) − 𝑀 ) / ( 𝑀 + 𝑁 ) )
138 pncan2 ⊢ ( ( 𝑀 ∈ ℂ ∧ 𝑁 ∈ ℂ ) → ( ( 𝑀 + 𝑁 ) − 𝑀 ) = 𝑁 )
139 103 104 138 mp2an ⊢ ( ( 𝑀 + 𝑁 ) − 𝑀 ) = 𝑁
140 139 oveq1i ⊢ ( ( ( 𝑀 + 𝑁 ) − 𝑀 ) / ( 𝑀 + 𝑁 ) ) = ( 𝑁 / ( 𝑀 + 𝑁 ) )
141 123 137 140 3eqtri ⊢ ( 𝑃 ‘ { 𝑐 ∈ 𝑂 ∣ ¬ 1 ∈ 𝑐 } ) = ( 𝑁 / ( 𝑀 + 𝑁 ) )