Metamath Proof Explorer

Theorem ballotlem1ri

Description: When the vote on the first tie is for A, the first vote is also for A on the reverse counting. (Contributed by Thierry Arnoux, 18-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 ℝ <
ballotth.s ⊢ S = c ∈ O ∖ E ⟼ i ∈ 1 … M + N ⟼ if i ≤ I ⁡ c I ⁡ c + 1 - i i
ballotth.r ⊢ R = c ∈ O ∖ E ⟼ S ⁡ c c
Assertion ballotlem1ri ⊢ C ∈ O ∖ E → 1 ∈ R ⁡ 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 ballotth.s ⊢ S = c ∈ O ∖ E ⟼ i ∈ 1 … M + N ⟼ if i ≤ I ⁡ c I ⁡ c + 1 - i i
10 ballotth.r ⊢ R = c ∈ O ∖ E ⟼ S ⁡ c c
11 nnaddcl ⊢ M ∈ ℕ ∧ N ∈ ℕ → M + N ∈ ℕ
12 1 2 11 mp2an ⊢ M + N ∈ ℕ
13 nnuz ⊢ ℕ = ℤ ≥ 1
14 12 13 eleqtri ⊢ M + N ∈ ℤ ≥ 1
15 eluzfz1 ⊢ M + N ∈ ℤ ≥ 1 → 1 ∈ 1 … M + N
16 14 15 mp1i ⊢ C ∈ O ∖ E → 1 ∈ 1 … M + N
17 1 2 3 4 5 6 7 8 ballotlemiex ⊢ C ∈ O ∖ E → I ⁡ C ∈ 1 … M + N ∧ F ⁡ C ⁡ I ⁡ C = 0
18 17 simpld ⊢ C ∈ O ∖ E → I ⁡ C ∈ 1 … M + N
19 elfzle1 ⊢ I ⁡ C ∈ 1 … M + N → 1 ≤ I ⁡ C
20 18 19 syl ⊢ C ∈ O ∖ E → 1 ≤ I ⁡ C
21 1 2 3 4 5 6 7 8 9 10 ballotlemrv1 ⊢ C ∈ O ∖ E ∧ 1 ∈ 1 … M + N ∧ 1 ≤ I ⁡ C → 1 ∈ R ⁡ C ↔ I ⁡ C + 1 - 1 ∈ C
22 16 20 21 mpd3an23 ⊢ C ∈ O ∖ E → 1 ∈ R ⁡ C ↔ I ⁡ C + 1 - 1 ∈ C
23 elfzelz ⊢ I ⁡ C ∈ 1 … M + N → I ⁡ C ∈ ℤ
24 18 23 syl ⊢ C ∈ O ∖ E → I ⁡ C ∈ ℤ
25 24 zcnd ⊢ C ∈ O ∖ E → I ⁡ C ∈ ℂ
26 1cnd ⊢ C ∈ O ∖ E → 1 ∈ ℂ
27 25 26 pncand ⊢ C ∈ O ∖ E → I ⁡ C + 1 - 1 = I ⁡ C
28 27 eleq1d ⊢ C ∈ O ∖ E → I ⁡ C + 1 - 1 ∈ C ↔ I ⁡ C ∈ C
29 22 28 bitrd ⊢ C ∈ O ∖ E → 1 ∈ R ⁡ C ↔ I ⁡ C ∈ C