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 ⟼ inf 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 ⟼ inf 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 fveq2 ⊢ i = 1 → F ⁡ C ⁡ i = F ⁡ C ⁡ 1
23 22 breq2d ⊢ i = 1 → 0 ≤ F ⁡ C ⁡ i ↔ 0 ≤ F ⁡ C ⁡ 1
24 elnnuz ⊢ I ⁡ C − 1 ∈ ℕ ↔ I ⁡ C − 1 ∈ ℤ ≥ 1
25 24 biimpi ⊢ I ⁡ C − 1 ∈ ℕ → I ⁡ C − 1 ∈ ℤ ≥ 1
26 eluzfz1 ⊢ I ⁡ C − 1 ∈ ℤ ≥ 1 → 1 ∈ 1 … I ⁡ C − 1
27 20 25 26 3syl ⊢ C ∈ O ∖ E ∧ 1 ∈ C → 1 ∈ 1 … I ⁡ C − 1
28 27 adantr ⊢ C ∈ O ∖ E ∧ 1 ∈ C ∧ I ⁡ C ∈ C → 1 ∈ 1 … I ⁡ C − 1
29 0le1 ⊢ 0 ≤ 1
30 1e0p1 ⊢ 1 = 0 + 1
31 29 30 breqtri ⊢ 0 ≤ 0 + 1
32 1nn ⊢ 1 ∈ ℕ
33 32 a1i ⊢ C ∈ O ∖ E → 1 ∈ ℕ
34 1 2 3 4 5 9 33 ballotlemfp1 ⊢ C ∈ O ∖ E → ¬ 1 ∈ C → F ⁡ C ⁡ 1 = F ⁡ C ⁡ 1 − 1 − 1 ∧ 1 ∈ C → F ⁡ C ⁡ 1 = F ⁡ C ⁡ 1 − 1 + 1
35 34 simprd ⊢ C ∈ O ∖ E → 1 ∈ C → F ⁡ C ⁡ 1 = F ⁡ C ⁡ 1 − 1 + 1
36 35 imp ⊢ C ∈ O ∖ E ∧ 1 ∈ C → F ⁡ C ⁡ 1 = F ⁡ C ⁡ 1 − 1 + 1
37 1m1e0 ⊢ 1 − 1 = 0
38 37 fveq2i ⊢ F ⁡ C ⁡ 1 − 1 = F ⁡ C ⁡ 0
39 38 oveq1i ⊢ F ⁡ C ⁡ 1 − 1 + 1 = F ⁡ C ⁡ 0 + 1
40 39 a1i ⊢ C ∈ O ∖ E ∧ 1 ∈ C → F ⁡ C ⁡ 1 − 1 + 1 = F ⁡ C ⁡ 0 + 1
41 1 2 3 4 5 ballotlemfval0 ⊢ C ∈ O → F ⁡ C ⁡ 0 = 0
42 9 41 syl ⊢ C ∈ O ∖ E → F ⁡ C ⁡ 0 = 0
43 42 adantr ⊢ C ∈ O ∖ E ∧ 1 ∈ C → F ⁡ C ⁡ 0 = 0
44 43 oveq1d ⊢ C ∈ O ∖ E ∧ 1 ∈ C → F ⁡ C ⁡ 0 + 1 = 0 + 1
45 36 40 44 3eqtrrd ⊢ C ∈ O ∖ E ∧ 1 ∈ C → 0 + 1 = F ⁡ C ⁡ 1
46 31 45 breqtrid ⊢ C ∈ O ∖ E ∧ 1 ∈ C → 0 ≤ F ⁡ C ⁡ 1
47 46 adantr ⊢ C ∈ O ∖ E ∧ 1 ∈ C ∧ I ⁡ C ∈ C → 0 ≤ F ⁡ C ⁡ 1
48 23 28 47 rspcedvdw ⊢ C ∈ O ∖ E ∧ 1 ∈ C ∧ I ⁡ C ∈ C → ∃ i ∈ 1 … I ⁡ C − 1 0 ≤ F ⁡ C ⁡ i
49 df-neg ⊢ − 1 = 0 − 1
50 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
51 50 simprd ⊢ C ∈ O ∖ E → I ⁡ C ∈ C → F ⁡ C ⁡ I ⁡ C = F ⁡ C ⁡ I ⁡ C − 1 + 1
52 51 imp ⊢ C ∈ O ∖ E ∧ I ⁡ C ∈ C → F ⁡ C ⁡ I ⁡ C = F ⁡ C ⁡ I ⁡ C − 1 + 1
53 11 simprd ⊢ C ∈ O ∖ E → F ⁡ C ⁡ I ⁡ C = 0
54 53 adantr ⊢ C ∈ O ∖ E ∧ I ⁡ C ∈ C → F ⁡ C ⁡ I ⁡ C = 0
55 52 54 eqtr3d ⊢ C ∈ O ∖ E ∧ I ⁡ C ∈ C → F ⁡ C ⁡ I ⁡ C − 1 + 1 = 0
56 0cnd ⊢ C ∈ O ∖ E ∧ I ⁡ C ∈ C → 0 ∈ ℂ
57 1cnd ⊢ C ∈ O ∖ E ∧ I ⁡ C ∈ C → 1 ∈ ℂ
58 9 adantr ⊢ C ∈ O ∖ E ∧ I ⁡ C ∈ C → C ∈ O
59 14 nnzd ⊢ C ∈ O ∖ E → I ⁡ C ∈ ℤ
60 59 adantr ⊢ C ∈ O ∖ E ∧ I ⁡ C ∈ C → I ⁡ C ∈ ℤ
61 1zzd ⊢ C ∈ O ∖ E ∧ I ⁡ C ∈ C → 1 ∈ ℤ
62 60 61 zsubcld ⊢ C ∈ O ∖ E ∧ I ⁡ C ∈ C → I ⁡ C − 1 ∈ ℤ
63 1 2 3 4 5 58 62 ballotlemfelz ⊢ C ∈ O ∖ E ∧ I ⁡ C ∈ C → F ⁡ C ⁡ I ⁡ C − 1 ∈ ℤ
64 63 zcnd ⊢ C ∈ O ∖ E ∧ I ⁡ C ∈ C → F ⁡ C ⁡ I ⁡ C − 1 ∈ ℂ
65 56 57 64 subadd2d ⊢ C ∈ O ∖ E ∧ I ⁡ C ∈ C → 0 − 1 = F ⁡ C ⁡ I ⁡ C − 1 ↔ F ⁡ C ⁡ I ⁡ C − 1 + 1 = 0
66 55 65 mpbird ⊢ C ∈ O ∖ E ∧ I ⁡ C ∈ C → 0 − 1 = F ⁡ C ⁡ I ⁡ C − 1
67 49 66 eqtrid ⊢ C ∈ O ∖ E ∧ I ⁡ C ∈ C → − 1 = F ⁡ C ⁡ I ⁡ C − 1
68 neg1lt0 ⊢ − 1 < 0
69 67 68 eqbrtrrdi ⊢ C ∈ O ∖ E ∧ I ⁡ C ∈ C → F ⁡ C ⁡ I ⁡ C − 1 < 0
70 69 adantlr ⊢ C ∈ O ∖ E ∧ 1 ∈ C ∧ I ⁡ C ∈ C → F ⁡ C ⁡ I ⁡ C − 1 < 0
71 1 2 3 4 5 10 21 48 70 ballotlemfcc ⊢ C ∈ O ∖ E ∧ 1 ∈ C ∧ I ⁡ C ∈ C → ∃ k ∈ 1 … I ⁡ C − 1 F ⁡ C ⁡ k = 0
72 1 2 3 4 5 6 7 8 ballotlemimin ⊢ C ∈ O ∖ E → ¬ ∃ k ∈ 1 … I ⁡ C − 1 F ⁡ C ⁡ k = 0
73 72 ad2antrr ⊢ C ∈ O ∖ E ∧ 1 ∈ C ∧ I ⁡ C ∈ C → ¬ ∃ k ∈ 1 … I ⁡ C − 1 F ⁡ C ⁡ k = 0
74 71 73 pm2.65da ⊢ C ∈ O ∖ E ∧ 1 ∈ C → ¬ I ⁡ C ∈ C