Metamath Proof Explorer

Theorem ballotlemsi

Description: The image by S of the first tie pick is the first pick. (Contributed by Thierry Arnoux, 14-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
Assertion ballotlemsi ⊢ C ∈ O ∖ E → S ⁡ 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 ballotth.s ⊢ S = c ∈ O ∖ E ⟼ i ∈ 1 … M + N ⟼ if i ≤ I ⁡ c I ⁡ c + 1 - i i
10 1 2 3 4 5 6 7 8 ballotlemiex ⊢ C ∈ O ∖ E → I ⁡ C ∈ 1 … M + N ∧ F ⁡ C ⁡ I ⁡ C = 0
11 10 simpld ⊢ C ∈ O ∖ E → I ⁡ C ∈ 1 … M + N
12 1 2 3 4 5 6 7 8 9 ballotlemsv ⊢ C ∈ O ∖ E ∧ I ⁡ C ∈ 1 … M + N → S ⁡ C ⁡ I ⁡ C = if I ⁡ C ≤ I ⁡ C I ⁡ C + 1 - I ⁡ C I ⁡ C
13 11 12 mpdan ⊢ C ∈ O ∖ E → S ⁡ C ⁡ I ⁡ C = if I ⁡ C ≤ I ⁡ C I ⁡ C + 1 - I ⁡ C I ⁡ C
14 elfzelz ⊢ I ⁡ C ∈ 1 … M + N → I ⁡ C ∈ ℤ
15 14 zred ⊢ I ⁡ C ∈ 1 … M + N → I ⁡ C ∈ ℝ
16 11 15 syl ⊢ C ∈ O ∖ E → I ⁡ C ∈ ℝ
17 16 leidd ⊢ C ∈ O ∖ E → I ⁡ C ≤ I ⁡ C
18 17 iftrued ⊢ C ∈ O ∖ E → if I ⁡ C ≤ I ⁡ C I ⁡ C + 1 - I ⁡ C I ⁡ C = I ⁡ C + 1 - I ⁡ C
19 16 recnd ⊢ C ∈ O ∖ E → I ⁡ C ∈ ℂ
20 1cnd ⊢ C ∈ O ∖ E → 1 ∈ ℂ
21 19 20 pncan2d ⊢ C ∈ O ∖ E → I ⁡ C + 1 - I ⁡ C = 1
22 13 18 21 3eqtrd ⊢ C ∈ O ∖ E → S ⁡ C ⁡ I ⁡ C = 1