Metamath Proof Explorer

Theorem ballotlemrv2

Description: Value of R after the tie. (Contributed by Thierry Arnoux, 11-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 ℝ <
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 ballotlemrv2 ⊢ C ∈ O ∖ E ∧ J ∈ 1 … M + N ∧ I ⁡ C < J → J ∈ R ⁡ C ↔ J ∈ 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 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 1 2 3 4 5 6 7 8 9 10 ballotlemrv ⊢ C ∈ O ∖ E ∧ J ∈ 1 … M + N → J ∈ R ⁡ C ↔ if J ≤ I ⁡ C I ⁡ C + 1 - J J ∈ C
12 11 3adant3 ⊢ C ∈ O ∖ E ∧ J ∈ 1 … M + N ∧ I ⁡ C < J → J ∈ R ⁡ C ↔ if J ≤ I ⁡ C I ⁡ C + 1 - J J ∈ C
13 fzssuz ⊢ 1 … M + N ⊆ ℤ ≥ 1
14 uzssz ⊢ ℤ ≥ 1 ⊆ ℤ
15 13 14 sstri ⊢ 1 … M + N ⊆ ℤ
16 1 2 3 4 5 6 7 8 ballotlemiex ⊢ C ∈ O ∖ E → I ⁡ C ∈ 1 … M + N ∧ F ⁡ C ⁡ I ⁡ C = 0
17 16 simpld ⊢ C ∈ O ∖ E → I ⁡ C ∈ 1 … M + N
18 15 17 sselid ⊢ C ∈ O ∖ E → I ⁡ C ∈ ℤ
19 18 adantr ⊢ C ∈ O ∖ E ∧ J ∈ 1 … M + N → I ⁡ C ∈ ℤ
20 19 zred ⊢ C ∈ O ∖ E ∧ J ∈ 1 … M + N → I ⁡ C ∈ ℝ
21 simpr ⊢ C ∈ O ∖ E ∧ J ∈ 1 … M + N → J ∈ 1 … M + N
22 15 21 sselid ⊢ C ∈ O ∖ E ∧ J ∈ 1 … M + N → J ∈ ℤ
23 22 zred ⊢ C ∈ O ∖ E ∧ J ∈ 1 … M + N → J ∈ ℝ
24 20 23 ltnled ⊢ C ∈ O ∖ E ∧ J ∈ 1 … M + N → I ⁡ C < J ↔ ¬ J ≤ I ⁡ C
25 24 biimp3a ⊢ C ∈ O ∖ E ∧ J ∈ 1 … M + N ∧ I ⁡ C < J → ¬ J ≤ I ⁡ C
26 25 iffalsed ⊢ C ∈ O ∖ E ∧ J ∈ 1 … M + N ∧ I ⁡ C < J → if J ≤ I ⁡ C I ⁡ C + 1 - J J = J
27 26 eleq1d ⊢ C ∈ O ∖ E ∧ J ∈ 1 … M + N ∧ I ⁡ C < J → if J ≤ I ⁡ C I ⁡ C + 1 - J J ∈ C ↔ J ∈ C
28 12 27 bitrd ⊢ C ∈ O ∖ E ∧ J ∈ 1 … M + N ∧ I ⁡ C < J → J ∈ R ⁡ C ↔ J ∈ C