Metamath Proof Explorer

Theorem ballotlemi1

Description: The first tie cannot be reached at the first pick. (Contributed by Thierry Arnoux, 12-Mar-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 ballotlemi1 ⊢ C ∈ O ∖ E ∧ ¬ 1 ∈ C → I ⁡ C ≠ 1

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 0re ⊢ 0 ∈ ℝ
10 1re ⊢ 1 ∈ ℝ
11 9 10 resubcli ⊢ 0 − 1 ∈ ℝ
12 0lt1 ⊢ 0 < 1
13 ltsub23 ⊢ 0 ∈ ℝ ∧ 1 ∈ ℝ ∧ 0 ∈ ℝ → 0 − 1 < 0 ↔ 0 − 0 < 1
14 9 10 9 13 mp3an ⊢ 0 − 1 < 0 ↔ 0 − 0 < 1
15 0m0e0 ⊢ 0 − 0 = 0
16 15 breq1i ⊢ 0 − 0 < 1 ↔ 0 < 1
17 14 16 bitr2i ⊢ 0 < 1 ↔ 0 − 1 < 0
18 12 17 mpbi ⊢ 0 − 1 < 0
19 11 18 gtneii ⊢ 0 ≠ 0 − 1
20 19 nesymi ⊢ ¬ 0 − 1 = 0
21 eldifi ⊢ C ∈ O ∖ E → C ∈ O
22 1nn ⊢ 1 ∈ ℕ
23 22 a1i ⊢ C ∈ O ∖ E → 1 ∈ ℕ
24 1 2 3 4 5 21 23 ballotlemfp1 ⊢ C ∈ O ∖ E → ¬ 1 ∈ C → F ⁡ C ⁡ 1 = F ⁡ C ⁡ 1 − 1 − 1 ∧ 1 ∈ C → F ⁡ C ⁡ 1 = F ⁡ C ⁡ 1 − 1 + 1
25 24 simpld ⊢ C ∈ O ∖ E → ¬ 1 ∈ C → F ⁡ C ⁡ 1 = F ⁡ C ⁡ 1 − 1 − 1
26 25 imp ⊢ C ∈ O ∖ E ∧ ¬ 1 ∈ C → F ⁡ C ⁡ 1 = F ⁡ C ⁡ 1 − 1 − 1
27 1m1e0 ⊢ 1 − 1 = 0
28 27 fveq2i ⊢ F ⁡ C ⁡ 1 − 1 = F ⁡ C ⁡ 0
29 28 oveq1i ⊢ F ⁡ C ⁡ 1 − 1 − 1 = F ⁡ C ⁡ 0 − 1
30 29 a1i ⊢ C ∈ O ∖ E ∧ ¬ 1 ∈ C → F ⁡ C ⁡ 1 − 1 − 1 = F ⁡ C ⁡ 0 − 1
31 1 2 3 4 5 ballotlemfval0 ⊢ C ∈ O → F ⁡ C ⁡ 0 = 0
32 21 31 syl ⊢ C ∈ O ∖ E → F ⁡ C ⁡ 0 = 0
33 32 adantr ⊢ C ∈ O ∖ E ∧ ¬ 1 ∈ C → F ⁡ C ⁡ 0 = 0
34 33 oveq1d ⊢ C ∈ O ∖ E ∧ ¬ 1 ∈ C → F ⁡ C ⁡ 0 − 1 = 0 − 1
35 26 30 34 3eqtrrd ⊢ C ∈ O ∖ E ∧ ¬ 1 ∈ C → 0 − 1 = F ⁡ C ⁡ 1
36 35 eqeq1d ⊢ C ∈ O ∖ E ∧ ¬ 1 ∈ C → 0 − 1 = 0 ↔ F ⁡ C ⁡ 1 = 0
37 20 36 mtbii ⊢ C ∈ O ∖ E ∧ ¬ 1 ∈ C → ¬ F ⁡ C ⁡ 1 = 0
38 1 2 3 4 5 6 7 8 ballotlemiex ⊢ C ∈ O ∖ E → I ⁡ C ∈ 1 … M + N ∧ F ⁡ C ⁡ I ⁡ C = 0
39 38 simprd ⊢ C ∈ O ∖ E → F ⁡ C ⁡ I ⁡ C = 0
40 39 ad2antrr ⊢ C ∈ O ∖ E ∧ ¬ 1 ∈ C ∧ I ⁡ C = 1 → F ⁡ C ⁡ I ⁡ C = 0
41 fveqeq2 ⊢ I ⁡ C = 1 → F ⁡ C ⁡ I ⁡ C = 0 ↔ F ⁡ C ⁡ 1 = 0
42 41 adantl ⊢ C ∈ O ∖ E ∧ ¬ 1 ∈ C ∧ I ⁡ C = 1 → F ⁡ C ⁡ I ⁡ C = 0 ↔ F ⁡ C ⁡ 1 = 0
43 40 42 mpbid ⊢ C ∈ O ∖ E ∧ ¬ 1 ∈ C ∧ I ⁡ C = 1 → F ⁡ C ⁡ 1 = 0
44 37 43 mtand ⊢ C ∈ O ∖ E ∧ ¬ 1 ∈ C → ¬ I ⁡ C = 1
45 44 neqned ⊢ C ∈ O ∖ E ∧ ¬ 1 ∈ C → I ⁡ C ≠ 1