Metamath Proof Explorer

Theorem ballotlemodife

Description: Elements of ( O \ E ) . (Contributed by Thierry Arnoux, 7-Dec-2016)

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
Assertion ballotlemodife ⊢ C ∈ O ∖ E ↔ C ∈ O ∧ ∃ i ∈ 1 … M + N F ⁡ C ⁡ i ≤ 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 eldif ⊢ C ∈ O ∖ E ↔ C ∈ O ∧ ¬ C ∈ E
8 df-or ⊢ C ∈ O ∧ ¬ C ∈ O ∨ C ∈ O ∧ ¬ ∀ i ∈ 1 … M + N 0 < F ⁡ C ⁡ i ↔ ¬ C ∈ O ∧ ¬ C ∈ O → C ∈ O ∧ ¬ ∀ i ∈ 1 … M + N 0 < F ⁡ C ⁡ i
9 pm3.24 ⊢ ¬ C ∈ O ∧ ¬ C ∈ O
10 9 a1bi ⊢ C ∈ O ∧ ¬ ∀ i ∈ 1 … M + N 0 < F ⁡ C ⁡ i ↔ ¬ C ∈ O ∧ ¬ C ∈ O → C ∈ O ∧ ¬ ∀ i ∈ 1 … M + N 0 < F ⁡ C ⁡ i
11 8 10 bitr4i ⊢ C ∈ O ∧ ¬ C ∈ O ∨ C ∈ O ∧ ¬ ∀ i ∈ 1 … M + N 0 < F ⁡ C ⁡ i ↔ C ∈ O ∧ ¬ ∀ i ∈ 1 … M + N 0 < F ⁡ C ⁡ i
12 1 2 3 4 5 6 ballotleme ⊢ C ∈ E ↔ C ∈ O ∧ ∀ i ∈ 1 … M + N 0 < F ⁡ C ⁡ i
13 12 notbii ⊢ ¬ C ∈ E ↔ ¬ C ∈ O ∧ ∀ i ∈ 1 … M + N 0 < F ⁡ C ⁡ i
14 13 anbi2i ⊢ C ∈ O ∧ ¬ C ∈ E ↔ C ∈ O ∧ ¬ C ∈ O ∧ ∀ i ∈ 1 … M + N 0 < F ⁡ C ⁡ i
15 ianor ⊢ ¬ C ∈ O ∧ ∀ i ∈ 1 … M + N 0 < F ⁡ C ⁡ i ↔ ¬ C ∈ O ∨ ¬ ∀ i ∈ 1 … M + N 0 < F ⁡ C ⁡ i
16 15 anbi2i ⊢ C ∈ O ∧ ¬ C ∈ O ∧ ∀ i ∈ 1 … M + N 0 < F ⁡ C ⁡ i ↔ C ∈ O ∧ ¬ C ∈ O ∨ ¬ ∀ i ∈ 1 … M + N 0 < F ⁡ C ⁡ i
17 andi ⊢ C ∈ O ∧ ¬ C ∈ O ∨ ¬ ∀ i ∈ 1 … M + N 0 < F ⁡ C ⁡ i ↔ C ∈ O ∧ ¬ C ∈ O ∨ C ∈ O ∧ ¬ ∀ i ∈ 1 … M + N 0 < F ⁡ C ⁡ i
18 14 16 17 3bitri ⊢ C ∈ O ∧ ¬ C ∈ E ↔ C ∈ O ∧ ¬ C ∈ O ∨ C ∈ O ∧ ¬ ∀ i ∈ 1 … M + N 0 < F ⁡ C ⁡ i
19 fz1ssfz0 ⊢ 1 … M + N ⊆ 0 … M + N
20 19 a1i ⊢ C ∈ O → 1 … M + N ⊆ 0 … M + N
21 20 sseld ⊢ C ∈ O → i ∈ 1 … M + N → i ∈ 0 … M + N
22 21 imdistani ⊢ C ∈ O ∧ i ∈ 1 … M + N → C ∈ O ∧ i ∈ 0 … M + N
23 simpl ⊢ C ∈ O ∧ j ∈ 0 … M + N → C ∈ O
24 elfzelz ⊢ j ∈ 0 … M + N → j ∈ ℤ
25 24 adantl ⊢ C ∈ O ∧ j ∈ 0 … M + N → j ∈ ℤ
26 1 2 3 4 5 23 25 ballotlemfelz ⊢ C ∈ O ∧ j ∈ 0 … M + N → F ⁡ C ⁡ j ∈ ℤ
27 26 zred ⊢ C ∈ O ∧ j ∈ 0 … M + N → F ⁡ C ⁡ j ∈ ℝ
28 27 sbimi ⊢ i j C ∈ O ∧ j ∈ 0 … M + N → i j F ⁡ C ⁡ j ∈ ℝ
29 sban ⊢ i j C ∈ O ∧ j ∈ 0 … M + N ↔ i j C ∈ O ∧ i j j ∈ 0 … M + N
30 sbv ⊢ i j C ∈ O ↔ C ∈ O
31 clelsb3 ⊢ i j j ∈ 0 … M + N ↔ i ∈ 0 … M + N
32 30 31 anbi12i ⊢ i j C ∈ O ∧ i j j ∈ 0 … M + N ↔ C ∈ O ∧ i ∈ 0 … M + N
33 29 32 bitri ⊢ i j C ∈ O ∧ j ∈ 0 … M + N ↔ C ∈ O ∧ i ∈ 0 … M + N
34 nfv ⊢ Ⅎ j F ⁡ C ⁡ i ∈ ℝ
35 fveq2 ⊢ j = i → F ⁡ C ⁡ j = F ⁡ C ⁡ i
36 35 eleq1d ⊢ j = i → F ⁡ C ⁡ j ∈ ℝ ↔ F ⁡ C ⁡ i ∈ ℝ
37 34 36 sbiev ⊢ i j F ⁡ C ⁡ j ∈ ℝ ↔ F ⁡ C ⁡ i ∈ ℝ
38 28 33 37 3imtr3i ⊢ C ∈ O ∧ i ∈ 0 … M + N → F ⁡ C ⁡ i ∈ ℝ
39 22 38 syl ⊢ C ∈ O ∧ i ∈ 1 … M + N → F ⁡ C ⁡ i ∈ ℝ
40 0red ⊢ C ∈ O ∧ i ∈ 1 … M + N → 0 ∈ ℝ
41 39 40 lenltd ⊢ C ∈ O ∧ i ∈ 1 … M + N → F ⁡ C ⁡ i ≤ 0 ↔ ¬ 0 < F ⁡ C ⁡ i
42 41 rexbidva ⊢ C ∈ O → ∃ i ∈ 1 … M + N F ⁡ C ⁡ i ≤ 0 ↔ ∃ i ∈ 1 … M + N ¬ 0 < F ⁡ C ⁡ i
43 rexnal ⊢ ∃ i ∈ 1 … M + N ¬ 0 < F ⁡ C ⁡ i ↔ ¬ ∀ i ∈ 1 … M + N 0 < F ⁡ C ⁡ i
44 42 43 bitrdi ⊢ C ∈ O → ∃ i ∈ 1 … M + N F ⁡ C ⁡ i ≤ 0 ↔ ¬ ∀ i ∈ 1 … M + N 0 < F ⁡ C ⁡ i
45 44 pm5.32i ⊢ C ∈ O ∧ ∃ i ∈ 1 … M + N F ⁡ C ⁡ i ≤ 0 ↔ C ∈ O ∧ ¬ ∀ i ∈ 1 … M + N 0 < F ⁡ C ⁡ i
46 11 18 45 3bitr4i ⊢ C ∈ O ∧ ¬ C ∈ E ↔ C ∈ O ∧ ∃ i ∈ 1 … M + N F ⁡ C ⁡ i ≤ 0
47 7 46 bitri ⊢ C ∈ O ∖ E ↔ C ∈ O ∧ ∃ i ∈ 1 … M + N F ⁡ C ⁡ i ≤ 0