Metamath Proof Explorer

Theorem ballotlemii

Description: The first tie cannot be reached at the first pick. (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 ballotlemii ⊢ 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 1e0p1 ⊢ 1 = 0 + 1
10 ax-1ne0 ⊢ 1 ≠ 0
11 9 10 eqnetrri ⊢ 0 + 1 ≠ 0
12 11 neii ⊢ ¬ 0 + 1 = 0
13 eldifi ⊢ C ∈ O ∖ E → C ∈ O
14 1nn ⊢ 1 ∈ ℕ
15 14 a1i ⊢ C ∈ O ∖ E → 1 ∈ ℕ
16 1 2 3 4 5 13 15 ballotlemfp1 ⊢ C ∈ O ∖ E → ¬ 1 ∈ C → F ⁡ C ⁡ 1 = F ⁡ C ⁡ 1 − 1 − 1 ∧ 1 ∈ C → F ⁡ C ⁡ 1 = F ⁡ C ⁡ 1 − 1 + 1
17 16 simprd ⊢ C ∈ O ∖ E → 1 ∈ C → F ⁡ C ⁡ 1 = F ⁡ C ⁡ 1 − 1 + 1
18 17 imp ⊢ C ∈ O ∖ E ∧ 1 ∈ C → F ⁡ C ⁡ 1 = F ⁡ C ⁡ 1 − 1 + 1
19 1m1e0 ⊢ 1 − 1 = 0
20 19 fveq2i ⊢ F ⁡ C ⁡ 1 − 1 = F ⁡ C ⁡ 0
21 20 oveq1i ⊢ F ⁡ C ⁡ 1 − 1 + 1 = F ⁡ C ⁡ 0 + 1
22 21 a1i ⊢ C ∈ O ∖ E ∧ 1 ∈ C → F ⁡ C ⁡ 1 − 1 + 1 = F ⁡ C ⁡ 0 + 1
23 1 2 3 4 5 ballotlemfval0 ⊢ C ∈ O → F ⁡ C ⁡ 0 = 0
24 13 23 syl ⊢ C ∈ O ∖ E → F ⁡ C ⁡ 0 = 0
25 24 adantr ⊢ C ∈ O ∖ E ∧ 1 ∈ C → F ⁡ C ⁡ 0 = 0
26 25 oveq1d ⊢ C ∈ O ∖ E ∧ 1 ∈ C → F ⁡ C ⁡ 0 + 1 = 0 + 1
27 18 22 26 3eqtrrd ⊢ C ∈ O ∖ E ∧ 1 ∈ C → 0 + 1 = F ⁡ C ⁡ 1
28 27 eqeq1d ⊢ C ∈ O ∖ E ∧ 1 ∈ C → 0 + 1 = 0 ↔ F ⁡ C ⁡ 1 = 0
29 12 28 mtbii ⊢ C ∈ O ∖ E ∧ 1 ∈ C → ¬ F ⁡ C ⁡ 1 = 0
30 1 2 3 4 5 6 7 8 ballotlemiex ⊢ C ∈ O ∖ E → I ⁡ C ∈ 1 … M + N ∧ F ⁡ C ⁡ I ⁡ C = 0
31 30 simprd ⊢ C ∈ O ∖ E → F ⁡ C ⁡ I ⁡ C = 0
32 31 ad2antrr ⊢ C ∈ O ∖ E ∧ 1 ∈ C ∧ I ⁡ C = 1 → F ⁡ C ⁡ I ⁡ C = 0
33 fveqeq2 ⊢ I ⁡ C = 1 → F ⁡ C ⁡ I ⁡ C = 0 ↔ F ⁡ C ⁡ 1 = 0
34 33 adantl ⊢ C ∈ O ∖ E ∧ 1 ∈ C ∧ I ⁡ C = 1 → F ⁡ C ⁡ I ⁡ C = 0 ↔ F ⁡ C ⁡ 1 = 0
35 32 34 mpbid ⊢ C ∈ O ∖ E ∧ 1 ∈ C ∧ I ⁡ C = 1 → F ⁡ C ⁡ 1 = 0
36 29 35 mtand ⊢ C ∈ O ∖ E ∧ 1 ∈ C → ¬ I ⁡ C = 1
37 36 neqned ⊢ C ∈ O ∖ E ∧ 1 ∈ C → I ⁡ C ≠ 1