Metamath Proof Explorer

Theorem ballotlemrc

Description: Range of R . (Contributed by Thierry Arnoux, 19-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 ballotlemrc ⊢ C ∈ O ∖ E → R ⁡ C ∈ O ∖ E

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 1 2 3 4 5 6 7 8 9 10 ballotlemro ⊢ C ∈ O ∖ E → R ⁡ C ∈ O
12 1 2 3 4 5 6 7 8 ballotlemiex ⊢ C ∈ O ∖ E → I ⁡ C ∈ 1 … M + N ∧ F ⁡ C ⁡ I ⁡ C = 0
13 12 simpld ⊢ C ∈ O ∖ E → I ⁡ C ∈ 1 … M + N
14 eqid ⊢ u ∈ Fin , v ∈ Fin ⟼ v ∩ u − v ∖ u = u ∈ Fin , v ∈ Fin ⟼ v ∩ u − v ∖ u
15 1 2 3 4 5 6 7 8 9 10 14 ballotlemfrci ⊢ C ∈ O ∖ E → F ⁡ R ⁡ C ⁡ I ⁡ C = 0
16 0le0 ⊢ 0 ≤ 0
17 15 16 eqbrtrdi ⊢ C ∈ O ∖ E → F ⁡ R ⁡ C ⁡ I ⁡ C ≤ 0
18 fveq2 ⊢ i = I ⁡ C → F ⁡ R ⁡ C ⁡ i = F ⁡ R ⁡ C ⁡ I ⁡ C
19 18 breq1d ⊢ i = I ⁡ C → F ⁡ R ⁡ C ⁡ i ≤ 0 ↔ F ⁡ R ⁡ C ⁡ I ⁡ C ≤ 0
20 19 rspcev ⊢ I ⁡ C ∈ 1 … M + N ∧ F ⁡ R ⁡ C ⁡ I ⁡ C ≤ 0 → ∃ i ∈ 1 … M + N F ⁡ R ⁡ C ⁡ i ≤ 0
21 13 17 20 syl2anc ⊢ C ∈ O ∖ E → ∃ i ∈ 1 … M + N F ⁡ R ⁡ C ⁡ i ≤ 0
22 1 2 3 4 5 6 ballotlemodife ⊢ R ⁡ C ∈ O ∖ E ↔ R ⁡ C ∈ O ∧ ∃ i ∈ 1 … M + N F ⁡ R ⁡ C ⁡ i ≤ 0
23 11 21 22 sylanbrc ⊢ C ∈ O ∖ E → R ⁡ C ∈ O ∖ E