Metamath Proof Explorer

Theorem ballotlemi

Description: Value of I for a given counting C . (Contributed by Thierry Arnoux, 1-Dec-2016) (Revised by AV, 6-Oct-2020)

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 ℝ <
Assertion ballotlemi ⊢ C ∈ O ∖ E → I ⁡ C = sup k ∈ 1 … M + N | F ⁡ C ⁡ k = 0 ℝ <

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 fveq2 ⊢ d = C → F ⁡ d = F ⁡ C
10 9 fveq1d ⊢ d = C → F ⁡ d ⁡ k = F ⁡ C ⁡ k
11 10 eqeq1d ⊢ d = C → F ⁡ d ⁡ k = 0 ↔ F ⁡ C ⁡ k = 0
12 11 rabbidv ⊢ d = C → k ∈ 1 … M + N | F ⁡ d ⁡ k = 0 = k ∈ 1 … M + N | F ⁡ C ⁡ k = 0
13 12 infeq1d ⊢ d = C → sup k ∈ 1 … M + N | F ⁡ d ⁡ k = 0 ℝ < = sup k ∈ 1 … M + N | F ⁡ C ⁡ k = 0 ℝ <
14 fveq2 ⊢ c = d → F ⁡ c = F ⁡ d
15 14 fveq1d ⊢ c = d → F ⁡ c ⁡ k = F ⁡ d ⁡ k
16 15 eqeq1d ⊢ c = d → F ⁡ c ⁡ k = 0 ↔ F ⁡ d ⁡ k = 0
17 16 rabbidv ⊢ c = d → k ∈ 1 … M + N | F ⁡ c ⁡ k = 0 = k ∈ 1 … M + N | F ⁡ d ⁡ k = 0
18 17 infeq1d ⊢ c = d → sup k ∈ 1 … M + N | F ⁡ c ⁡ k = 0 ℝ < = sup k ∈ 1 … M + N | F ⁡ d ⁡ k = 0 ℝ <
19 18 cbvmptv ⊢ c ∈ O ∖ E ⟼ sup k ∈ 1 … M + N | F ⁡ c ⁡ k = 0 ℝ < = d ∈ O ∖ E ⟼ sup k ∈ 1 … M + N | F ⁡ d ⁡ k = 0 ℝ <
20 8 19 eqtri ⊢ I = d ∈ O ∖ E ⟼ sup k ∈ 1 … M + N | F ⁡ d ⁡ k = 0 ℝ <
21 ltso ⊢ < Or ℝ
22 21 infex ⊢ sup k ∈ 1 … M + N | F ⁡ C ⁡ k = 0 ℝ < ∈ V
23 13 20 22 fvmpt ⊢ C ∈ O ∖ E → I ⁡ C = sup k ∈ 1 … M + N | F ⁡ C ⁡ k = 0 ℝ <