Metamath Proof Explorer

Theorem ballotlemiex

Description: Properties of ( IC ) . (Contributed by Thierry Arnoux, 12-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 ⟼ inf k ∈ 1 … M + N | F ⁡ c ⁡ k = 0 ℝ <
Assertion ballotlemiex ⊢ C ∈ O ∖ E → I ⁡ C ∈ 1 … M + N ∧ F ⁡ C ⁡ I ⁡ C = 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 ⟼ inf k ∈ 1 … M + N | F ⁡ c ⁡ k = 0 ℝ <
9 1 2 3 4 5 6 7 8 ballotlemi ⊢ C ∈ O ∖ E → I ⁡ C = inf k ∈ 1 … M + N | F ⁡ C ⁡ k = 0 ℝ <
10 ltso ⊢ < Or ℝ
11 10 a1i ⊢ C ∈ O ∖ E → < Or ℝ
12 fzfi ⊢ 1 … M + N ∈ Fin
13 ssrab2 ⊢ k ∈ 1 … M + N | F ⁡ C ⁡ k = 0 ⊆ 1 … M + N
14 ssfi ⊢ 1 … M + N ∈ Fin ∧ k ∈ 1 … M + N | F ⁡ C ⁡ k = 0 ⊆ 1 … M + N → k ∈ 1 … M + N | F ⁡ C ⁡ k = 0 ∈ Fin
15 12 13 14 mp2an ⊢ k ∈ 1 … M + N | F ⁡ C ⁡ k = 0 ∈ Fin
16 15 a1i ⊢ C ∈ O ∖ E → k ∈ 1 … M + N | F ⁡ C ⁡ k = 0 ∈ Fin
17 1 2 3 4 5 6 7 ballotlem5 ⊢ C ∈ O ∖ E → ∃ k ∈ 1 … M + N F ⁡ C ⁡ k = 0
18 rabn0 ⊢ k ∈ 1 … M + N | F ⁡ C ⁡ k = 0 ≠ ∅ ↔ ∃ k ∈ 1 … M + N F ⁡ C ⁡ k = 0
19 17 18 sylibr ⊢ C ∈ O ∖ E → k ∈ 1 … M + N | F ⁡ C ⁡ k = 0 ≠ ∅
20 fzssuz ⊢ 1 … M + N ⊆ ℤ ≥ 1
21 uzssz ⊢ ℤ ≥ 1 ⊆ ℤ
22 20 21 sstri ⊢ 1 … M + N ⊆ ℤ
23 zssre ⊢ ℤ ⊆ ℝ
24 22 23 sstri ⊢ 1 … M + N ⊆ ℝ
25 13 24 sstri ⊢ k ∈ 1 … M + N | F ⁡ C ⁡ k = 0 ⊆ ℝ
26 25 a1i ⊢ C ∈ O ∖ E → k ∈ 1 … M + N | F ⁡ C ⁡ k = 0 ⊆ ℝ
27 fiinfcl ⊢ < Or ℝ ∧ k ∈ 1 … M + N | F ⁡ C ⁡ k = 0 ∈ Fin ∧ k ∈ 1 … M + N | F ⁡ C ⁡ k = 0 ≠ ∅ ∧ k ∈ 1 … M + N | F ⁡ C ⁡ k = 0 ⊆ ℝ → inf k ∈ 1 … M + N | F ⁡ C ⁡ k = 0 ℝ < ∈ k ∈ 1 … M + N | F ⁡ C ⁡ k = 0
28 11 16 19 26 27 syl13anc ⊢ C ∈ O ∖ E → inf k ∈ 1 … M + N | F ⁡ C ⁡ k = 0 ℝ < ∈ k ∈ 1 … M + N | F ⁡ C ⁡ k = 0
29 9 28 eqeltrd ⊢ C ∈ O ∖ E → I ⁡ C ∈ k ∈ 1 … M + N | F ⁡ C ⁡ k = 0
30 fveqeq2 ⊢ k = I ⁡ C → F ⁡ C ⁡ k = 0 ↔ F ⁡ C ⁡ I ⁡ C = 0
31 30 elrab ⊢ I ⁡ C ∈ k ∈ 1 … M + N | F ⁡ C ⁡ k = 0 ↔ I ⁡ C ∈ 1 … M + N ∧ F ⁡ C ⁡ I ⁡ C = 0
32 29 31 sylib ⊢ C ∈ O ∖ E → I ⁡ C ∈ 1 … M + N ∧ F ⁡ C ⁡ I ⁡ C = 0