Metamath Proof Explorer

Theorem ballotlem1c

Description: If the first vote is for A, the vote on the first tie is for B. (Contributed by Thierry Arnoux, 4-Apr-2017)

Ref Expression
Hypotheses ballotth.m ⊢ M ∈ ℕ
ballotth.n ⊢ N ∈ ℕ
ballotth.o ⊢ O = c ∈ 𝒫 1 … M + N | c = M
ballotth.p ⊢ P = x ∈ 𝒫 O ⟼ x O
ballotth.f ⊢ F = c ∈ O ⟼ i ∈ ℤ ⟼ 1 … i ∩ c − 1 … i ∖ c
ballotth.e ⊢ E = c ∈ O | ∀ i ∈ 1 … M + N 0 < F ⁡ c ⁡ i
ballotth.mgtn ⊢ N < M
ballotth.i ⊢ I = c ∈ O ∖ E ⟼ sup k ∈ 1 … M + N | F ⁡ c ⁡ k = 0 ℝ <
Assertion ballotlem1c ⊢ C ∈ O ∖ E ∧ 1 ∈ C → ¬ I ⁡ C ∈ C

Proof

Step Hyp Ref Expression
1 ballotth.m ⊢ M ∈ ℕ
2 ballotth.n ⊢ N ∈ ℕ
3 ballotth.o ⊢ O = c ∈ 𝒫 1 … M + N | c = M
4 ballotth.p ⊢ P = x ∈ 𝒫 O ⟼ x O
5 ballotth.f ⊢ F = c ∈ O ⟼ i ∈ ℤ ⟼ 1 … i ∩ c − 1 … i ∖ c
6 ballotth.e ⊢ E = c ∈ O | ∀ i ∈ 1 … M + N 0 < F ⁡ c ⁡ i
7 ballotth.mgtn ⊢ N < M
8 ballotth.i ⊢ I = c ∈ O ∖ E ⟼ sup k ∈ 1 … M + N | F ⁡ c ⁡ k = 0 ℝ <
9 eldifi ⊢ C ∈ O ∖ E → C ∈ O
10 9 ad2antrr ⊢ C ∈ O ∖ E ∧ 1 ∈ C ∧ I ⁡ C ∈ C → C ∈ O
11 1 2 3 4 5 6 7 8 ballotlemiex ⊢ C ∈ O ∖ E → I ⁡ C ∈ 1 … M + N ∧ F ⁡ C ⁡ I ⁡ C = 0
12 11 simpld ⊢ C ∈ O ∖ E → I ⁡ C ∈ 1 … M + N
13 elfznn ⊢ I ⁡ C ∈ 1 … M + N → I ⁡ C ∈ ℕ
14 12 13 syl ⊢ C ∈ O ∖ E → I ⁡ C ∈ ℕ
15 14 adantr ⊢ C ∈ O ∖ E ∧ 1 ∈ C → I ⁡ C ∈ ℕ
16 1 2 3 4 5 6 7 8 ballotlemii ⊢ C ∈ O ∖ E ∧ 1 ∈ C → I ⁡ C ≠ 1
17 eluz2b3 ⊢ I ⁡ C ∈ ℤ ≥ 2 ↔ I ⁡ C ∈ ℕ ∧ I ⁡ C ≠ 1
18 15 16 17 sylanbrc ⊢ C ∈ O ∖ E ∧ 1 ∈ C → I ⁡ C ∈ ℤ ≥ 2
19 uz2m1nn ⊢ I ⁡ C ∈ ℤ ≥ 2 → I ⁡ C − 1 ∈ ℕ
20 18 19 syl ⊢ C ∈ O ∖ E ∧ 1 ∈ C → I ⁡ C − 1 ∈ ℕ
21 20 adantr ⊢ C ∈ O ∖ E ∧ 1 ∈ C ∧ I ⁡ C ∈ C → I ⁡ C − 1 ∈ ℕ
22 elnnuz ⊢ I ⁡ C − 1 ∈ ℕ ↔ I ⁡ C − 1 ∈ ℤ ≥ 1
23 22 biimpi ⊢ I ⁡ C − 1 ∈ ℕ → I ⁡ C − 1 ∈ ℤ ≥ 1
24 eluzfz1 ⊢ I ⁡ C − 1 ∈ ℤ ≥ 1 → 1 ∈ 1 … I ⁡ C − 1
25 20 23 24 3syl ⊢ C ∈ O ∖ E ∧ 1 ∈ C → 1 ∈ 1 … I ⁡ C − 1
26 25 adantr ⊢ C ∈ O ∖ E ∧ 1 ∈ C ∧ I ⁡ C ∈ C → 1 ∈ 1 … I ⁡ C − 1
27 0le1 ⊢ 0 ≤ 1
28 1e0p1 ⊢ 1 = 0 + 1
29 27 28 breqtri ⊢ 0 ≤ 0 + 1
30 1nn ⊢ 1 ∈ ℕ
31 30 a1i ⊢ C ∈ O ∖ E → 1 ∈ ℕ
32 1 2 3 4 5 9 31 ballotlemfp1 ⊢ C ∈ O ∖ E → ¬ 1 ∈ C → F ⁡ C ⁡ 1 = F ⁡ C ⁡ 1 − 1 − 1 ∧ 1 ∈ C → F ⁡ C ⁡ 1 = F ⁡ C ⁡ 1 − 1 + 1
33 32 simprd ⊢ C ∈ O ∖ E → 1 ∈ C → F ⁡ C ⁡ 1 = F ⁡ C ⁡ 1 − 1 + 1
34 33 imp ⊢ C ∈ O ∖ E ∧ 1 ∈ C → F ⁡ C ⁡ 1 = F ⁡ C ⁡ 1 − 1 + 1
35 1m1e0 ⊢ 1 − 1 = 0
36 35 fveq2i ⊢ F ⁡ C ⁡ 1 − 1 = F ⁡ C ⁡ 0
37 36 oveq1i ⊢ F ⁡ C ⁡ 1 − 1 + 1 = F ⁡ C ⁡ 0 + 1
38 37 a1i ⊢ C ∈ O ∖ E ∧ 1 ∈ C → F ⁡ C ⁡ 1 − 1 + 1 = F ⁡ C ⁡ 0 + 1
39 1 2 3 4 5 ballotlemfval0 ⊢ C ∈ O → F ⁡ C ⁡ 0 = 0
40 9 39 syl ⊢ C ∈ O ∖ E → F ⁡ C ⁡ 0 = 0
41 40 adantr ⊢ C ∈ O ∖ E ∧ 1 ∈ C → F ⁡ C ⁡ 0 = 0
42 41 oveq1d ⊢ C ∈ O ∖ E ∧ 1 ∈ C → F ⁡ C ⁡ 0 + 1 = 0 + 1
43 34 38 42 3eqtrrd ⊢ C ∈ O ∖ E ∧ 1 ∈ C → 0 + 1 = F ⁡ C ⁡ 1
44 29 43 breqtrid ⊢ C ∈ O ∖ E ∧ 1 ∈ C → 0 ≤ F ⁡ C ⁡ 1
45 44 adantr ⊢ C ∈ O ∖ E ∧ 1 ∈ C ∧ I ⁡ C ∈ C → 0 ≤ F ⁡ C ⁡ 1
46 fveq2 ⊢ i = 1 → F ⁡ C ⁡ i = F ⁡ C ⁡ 1
47 46 breq2d ⊢ i = 1 → 0 ≤ F ⁡ C ⁡ i ↔ 0 ≤ F ⁡ C ⁡ 1
48 47 rspcev ⊢ 1 ∈ 1 … I ⁡ C − 1 ∧ 0 ≤ F ⁡ C ⁡ 1 → ∃ i ∈ 1 … I ⁡ C − 1 0 ≤ F ⁡ C ⁡ i
49 26 45 48 syl2anc ⊢ C ∈ O ∖ E ∧ 1 ∈ C ∧ I ⁡ C ∈ C → ∃ i ∈ 1 … I ⁡ C − 1 0 ≤ F ⁡ C ⁡ i
50 df-neg ⊢ − 1 = 0 − 1
51 1 2 3 4 5 9 14 ballotlemfp1 ⊢ C ∈ O ∖ E → ¬ I ⁡ C ∈ C → F ⁡ C ⁡ I ⁡ C = F ⁡ C ⁡ I ⁡ C − 1 − 1 ∧ I ⁡ C ∈ C → F ⁡ C ⁡ I ⁡ C = F ⁡ C ⁡ I ⁡ C − 1 + 1
52 51 simprd ⊢ C ∈ O ∖ E → I ⁡ C ∈ C → F ⁡ C ⁡ I ⁡ C = F ⁡ C ⁡ I ⁡ C − 1 + 1
53 52 imp ⊢ C ∈ O ∖ E ∧ I ⁡ C ∈ C → F ⁡ C ⁡ I ⁡ C = F ⁡ C ⁡ I ⁡ C − 1 + 1
54 11 simprd ⊢ C ∈ O ∖ E → F ⁡ C ⁡ I ⁡ C = 0
55 54 adantr ⊢ C ∈ O ∖ E ∧ I ⁡ C ∈ C → F ⁡ C ⁡ I ⁡ C = 0
56 53 55 eqtr3d ⊢ C ∈ O ∖ E ∧ I ⁡ C ∈ C → F ⁡ C ⁡ I ⁡ C − 1 + 1 = 0
57 0cnd ⊢ C ∈ O ∖ E ∧ I ⁡ C ∈ C → 0 ∈ ℂ
58 1cnd ⊢ C ∈ O ∖ E ∧ I ⁡ C ∈ C → 1 ∈ ℂ
59 9 adantr ⊢ C ∈ O ∖ E ∧ I ⁡ C ∈ C → C ∈ O
60 14 nnzd ⊢ C ∈ O ∖ E → I ⁡ C ∈ ℤ
61 60 adantr ⊢ C ∈ O ∖ E ∧ I ⁡ C ∈ C → I ⁡ C ∈ ℤ
62 1zzd ⊢ C ∈ O ∖ E ∧ I ⁡ C ∈ C → 1 ∈ ℤ
63 61 62 zsubcld ⊢ C ∈ O ∖ E ∧ I ⁡ C ∈ C → I ⁡ C − 1 ∈ ℤ
64 1 2 3 4 5 59 63 ballotlemfelz ⊢ C ∈ O ∖ E ∧ I ⁡ C ∈ C → F ⁡ C ⁡ I ⁡ C − 1 ∈ ℤ
65 64 zcnd ⊢ C ∈ O ∖ E ∧ I ⁡ C ∈ C → F ⁡ C ⁡ I ⁡ C − 1 ∈ ℂ
66 57 58 65 subadd2d ⊢ C ∈ O ∖ E ∧ I ⁡ C ∈ C → 0 − 1 = F ⁡ C ⁡ I ⁡ C − 1 ↔ F ⁡ C ⁡ I ⁡ C − 1 + 1 = 0
67 56 66 mpbird ⊢ C ∈ O ∖ E ∧ I ⁡ C ∈ C → 0 − 1 = F ⁡ C ⁡ I ⁡ C − 1
68 50 67 eqtrid ⊢ C ∈ O ∖ E ∧ I ⁡ C ∈ C → − 1 = F ⁡ C ⁡ I ⁡ C − 1
69 neg1lt0 ⊢ − 1 < 0
70 68 69 eqbrtrrdi ⊢ C ∈ O ∖ E ∧ I ⁡ C ∈ C → F ⁡ C ⁡ I ⁡ C − 1 < 0
71 70 adantlr ⊢ C ∈ O ∖ E ∧ 1 ∈ C ∧ I ⁡ C ∈ C → F ⁡ C ⁡ I ⁡ C − 1 < 0
72 1 2 3 4 5 10 21 49 71 ballotlemfcc ⊢ C ∈ O ∖ E ∧ 1 ∈ C ∧ I ⁡ C ∈ C → ∃ k ∈ 1 … I ⁡ C − 1 F ⁡ C ⁡ k = 0
73 1 2 3 4 5 6 7 8 ballotlemimin ⊢ C ∈ O ∖ E → ¬ ∃ k ∈ 1 … I ⁡ C − 1 F ⁡ C ⁡ k = 0
74 73 ad2antrr ⊢ C ∈ O ∖ E ∧ 1 ∈ C ∧ I ⁡ C ∈ C → ¬ ∃ k ∈ 1 … I ⁡ C − 1 F ⁡ C ⁡ k = 0
75 72 74 pm2.65da ⊢ C ∈ O ∖ E ∧ 1 ∈ C → ¬ I ⁡ C ∈ C