Metamath Proof Explorer

Theorem ballotlemsval

Description: Value of S . (Contributed by Thierry Arnoux, 12-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
Assertion ballotlemsval ⊢ C ∈ O ∖ E → S ⁡ C = i ∈ 1 … M + N ⟼ if i ≤ I ⁡ C I ⁡ C + 1 - i i

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 simpl ⊢ d = C ∧ i ∈ 1 … M + N → d = C
11 10 fveq2d ⊢ d = C ∧ i ∈ 1 … M + N → I ⁡ d = I ⁡ C
12 11 breq2d ⊢ d = C ∧ i ∈ 1 … M + N → i ≤ I ⁡ d ↔ i ≤ I ⁡ C
13 11 oveq1d ⊢ d = C ∧ i ∈ 1 … M + N → I ⁡ d + 1 = I ⁡ C + 1
14 13 oveq1d ⊢ d = C ∧ i ∈ 1 … M + N → I ⁡ d + 1 - i = I ⁡ C + 1 - i
15 12 14 ifbieq1d ⊢ d = C ∧ i ∈ 1 … M + N → if i ≤ I ⁡ d I ⁡ d + 1 - i i = if i ≤ I ⁡ C I ⁡ C + 1 - i i
16 15 mpteq2dva ⊢ d = C → i ∈ 1 … M + N ⟼ if i ≤ I ⁡ d I ⁡ d + 1 - i i = i ∈ 1 … M + N ⟼ if i ≤ I ⁡ C I ⁡ C + 1 - i i
17 simpl ⊢ c = d ∧ i ∈ 1 … M + N → c = d
18 17 fveq2d ⊢ c = d ∧ i ∈ 1 … M + N → I ⁡ c = I ⁡ d
19 18 breq2d ⊢ c = d ∧ i ∈ 1 … M + N → i ≤ I ⁡ c ↔ i ≤ I ⁡ d
20 18 oveq1d ⊢ c = d ∧ i ∈ 1 … M + N → I ⁡ c + 1 = I ⁡ d + 1
21 20 oveq1d ⊢ c = d ∧ i ∈ 1 … M + N → I ⁡ c + 1 - i = I ⁡ d + 1 - i
22 19 21 ifbieq1d ⊢ c = d ∧ i ∈ 1 … M + N → if i ≤ I ⁡ c I ⁡ c + 1 - i i = if i ≤ I ⁡ d I ⁡ d + 1 - i i
23 22 mpteq2dva ⊢ c = d → i ∈ 1 … M + N ⟼ if i ≤ I ⁡ c I ⁡ c + 1 - i i = i ∈ 1 … M + N ⟼ if i ≤ I ⁡ d I ⁡ d + 1 - i i
24 23 cbvmptv ⊢ c ∈ O ∖ E ⟼ i ∈ 1 … M + N ⟼ if i ≤ I ⁡ c I ⁡ c + 1 - i i = d ∈ O ∖ E ⟼ i ∈ 1 … M + N ⟼ if i ≤ I ⁡ d I ⁡ d + 1 - i i
25 9 24 eqtri ⊢ S = d ∈ O ∖ E ⟼ i ∈ 1 … M + N ⟼ if i ≤ I ⁡ d I ⁡ d + 1 - i i
26 ovex ⊢ 1 … M + N ∈ V
27 26 mptex ⊢ i ∈ 1 … M + N ⟼ if i ≤ I ⁡ C I ⁡ C + 1 - i i ∈ V
28 16 25 27 fvmpt ⊢ C ∈ O ∖ E → S ⁡ C = i ∈ 1 … M + N ⟼ if i ≤ I ⁡ C I ⁡ C + 1 - i i