# Metamath Proof Explorer

## Theorem ballotlemfc0

Description: F takes value 0 between negative and positive values. (Contributed by Thierry Arnoux, 24-Nov-2016)

Ref Expression
Hypotheses ballotth.m ${⊢}{M}\in ℕ$
ballotth.n ${⊢}{N}\in ℕ$
ballotth.o ${⊢}{O}=\left\{{c}\in 𝒫\left(1\dots {M}+{N}\right)|\left|{c}\right|={M}\right\}$
ballotth.p ${⊢}{P}=\left({x}\in 𝒫{O}⟼\frac{\left|{x}\right|}{\left|{O}\right|}\right)$
ballotth.f ${⊢}{F}=\left({c}\in {O}⟼\left({i}\in ℤ⟼\left|\left(1\dots {i}\right)\cap {c}\right|-\left|\left(1\dots {i}\right)\setminus {c}\right|\right)\right)$
ballotlemfp1.c ${⊢}{\phi }\to {C}\in {O}$
ballotlemfp1.j ${⊢}{\phi }\to {J}\in ℕ$
ballotlemfc0.3 ${⊢}{\phi }\to \exists {i}\in \left(1\dots {J}\right)\phantom{\rule{.4em}{0ex}}{F}\left({C}\right)\left({i}\right)\le 0$
ballotlemfc0.4 ${⊢}{\phi }\to 0<{F}\left({C}\right)\left({J}\right)$
Assertion ballotlemfc0 ${⊢}{\phi }\to \exists {k}\in \left(1\dots {J}\right)\phantom{\rule{.4em}{0ex}}{F}\left({C}\right)\left({k}\right)=0$

### Proof

Step Hyp Ref Expression
1 ballotth.m ${⊢}{M}\in ℕ$
2 ballotth.n ${⊢}{N}\in ℕ$
3 ballotth.o ${⊢}{O}=\left\{{c}\in 𝒫\left(1\dots {M}+{N}\right)|\left|{c}\right|={M}\right\}$
4 ballotth.p ${⊢}{P}=\left({x}\in 𝒫{O}⟼\frac{\left|{x}\right|}{\left|{O}\right|}\right)$
5 ballotth.f ${⊢}{F}=\left({c}\in {O}⟼\left({i}\in ℤ⟼\left|\left(1\dots {i}\right)\cap {c}\right|-\left|\left(1\dots {i}\right)\setminus {c}\right|\right)\right)$
6 ballotlemfp1.c ${⊢}{\phi }\to {C}\in {O}$
7 ballotlemfp1.j ${⊢}{\phi }\to {J}\in ℕ$
8 ballotlemfc0.3 ${⊢}{\phi }\to \exists {i}\in \left(1\dots {J}\right)\phantom{\rule{.4em}{0ex}}{F}\left({C}\right)\left({i}\right)\le 0$
9 ballotlemfc0.4 ${⊢}{\phi }\to 0<{F}\left({C}\right)\left({J}\right)$
10 fveq2 ${⊢}{i}={k}\to {F}\left({C}\right)\left({i}\right)={F}\left({C}\right)\left({k}\right)$
11 10 breq1d ${⊢}{i}={k}\to \left({F}\left({C}\right)\left({i}\right)\le 0↔{F}\left({C}\right)\left({k}\right)\le 0\right)$
12 11 elrab ${⊢}{k}\in \left\{{i}\in \left(1\dots {J}\right)|{F}\left({C}\right)\left({i}\right)\le 0\right\}↔\left({k}\in \left(1\dots {J}\right)\wedge {F}\left({C}\right)\left({k}\right)\le 0\right)$
13 12 anbi1i ${⊢}\left({k}\in \left\{{i}\in \left(1\dots {J}\right)|{F}\left({C}\right)\left({i}\right)\le 0\right\}\wedge \forall {j}\in \left\{{i}\in \left(1\dots {J}\right)|{F}\left({C}\right)\left({i}\right)\le 0\right\}\phantom{\rule{.4em}{0ex}}{j}\le {k}\right)↔\left(\left({k}\in \left(1\dots {J}\right)\wedge {F}\left({C}\right)\left({k}\right)\le 0\right)\wedge \forall {j}\in \left\{{i}\in \left(1\dots {J}\right)|{F}\left({C}\right)\left({i}\right)\le 0\right\}\phantom{\rule{.4em}{0ex}}{j}\le {k}\right)$
14 simprlr ${⊢}\left({\phi }\wedge \left(\left({k}\in \left(1\dots {J}\right)\wedge {F}\left({C}\right)\left({k}\right)\le 0\right)\wedge \forall {j}\in \left\{{i}\in \left(1\dots {J}\right)|{F}\left({C}\right)\left({i}\right)\le 0\right\}\phantom{\rule{.4em}{0ex}}{j}\le {k}\right)\right)\to {F}\left({C}\right)\left({k}\right)\le 0$
15 simprl ${⊢}\left({\phi }\wedge \left({k}\in \left(1\dots {J}\right)\wedge {F}\left({C}\right)\left({k}\right)\le 0\right)\right)\to {k}\in \left(1\dots {J}\right)$
16 15 adantrr ${⊢}\left({\phi }\wedge \left(\left({k}\in \left(1\dots {J}\right)\wedge {F}\left({C}\right)\left({k}\right)\le 0\right)\wedge \forall {j}\in \left\{{i}\in \left(1\dots {J}\right)|{F}\left({C}\right)\left({i}\right)\le 0\right\}\phantom{\rule{.4em}{0ex}}{j}\le {k}\right)\right)\to {k}\in \left(1\dots {J}\right)$
17 fzssuz ${⊢}\left(1\dots {J}\right)\subseteq {ℤ}_{\ge 1}$
18 uzssz ${⊢}{ℤ}_{\ge 1}\subseteq ℤ$
19 17 18 sstri ${⊢}\left(1\dots {J}\right)\subseteq ℤ$
20 zssre ${⊢}ℤ\subseteq ℝ$
21 19 20 sstri ${⊢}\left(1\dots {J}\right)\subseteq ℝ$
22 21 sseli ${⊢}{k}\in \left(1\dots {J}\right)\to {k}\in ℝ$
23 22 ltp1d ${⊢}{k}\in \left(1\dots {J}\right)\to {k}<{k}+1$
24 1red ${⊢}{k}\in \left(1\dots {J}\right)\to 1\in ℝ$
25 22 24 readdcld ${⊢}{k}\in \left(1\dots {J}\right)\to {k}+1\in ℝ$
26 22 25 ltnled ${⊢}{k}\in \left(1\dots {J}\right)\to \left({k}<{k}+1↔¬{k}+1\le {k}\right)$
27 23 26 mpbid ${⊢}{k}\in \left(1\dots {J}\right)\to ¬{k}+1\le {k}$
28 16 27 syl ${⊢}\left({\phi }\wedge \left(\left({k}\in \left(1\dots {J}\right)\wedge {F}\left({C}\right)\left({k}\right)\le 0\right)\wedge \forall {j}\in \left\{{i}\in \left(1\dots {J}\right)|{F}\left({C}\right)\left({i}\right)\le 0\right\}\phantom{\rule{.4em}{0ex}}{j}\le {k}\right)\right)\to ¬{k}+1\le {k}$
29 simprr ${⊢}\left({\phi }\wedge \left(\left({k}\in \left(1\dots {J}\right)\wedge {F}\left({C}\right)\left({k}\right)\le 0\right)\wedge \forall {j}\in \left\{{i}\in \left(1\dots {J}\right)|{F}\left({C}\right)\left({i}\right)\le 0\right\}\phantom{\rule{.4em}{0ex}}{j}\le {k}\right)\right)\to \forall {j}\in \left\{{i}\in \left(1\dots {J}\right)|{F}\left({C}\right)\left({i}\right)\le 0\right\}\phantom{\rule{.4em}{0ex}}{j}\le {k}$
30 9 adantr ${⊢}\left({\phi }\wedge {k}={J}\right)\to 0<{F}\left({C}\right)\left({J}\right)$
31 simpr ${⊢}\left({\phi }\wedge {k}={J}\right)\to {k}={J}$
32 31 fveq2d ${⊢}\left({\phi }\wedge {k}={J}\right)\to {F}\left({C}\right)\left({k}\right)={F}\left({C}\right)\left({J}\right)$
33 32 breq2d ${⊢}\left({\phi }\wedge {k}={J}\right)\to \left(0<{F}\left({C}\right)\left({k}\right)↔0<{F}\left({C}\right)\left({J}\right)\right)$
34 elnnuz ${⊢}{J}\in ℕ↔{J}\in {ℤ}_{\ge 1}$
35 7 34 sylib ${⊢}{\phi }\to {J}\in {ℤ}_{\ge 1}$
36 eluzfz2 ${⊢}{J}\in {ℤ}_{\ge 1}\to {J}\in \left(1\dots {J}\right)$
37 35 36 syl ${⊢}{\phi }\to {J}\in \left(1\dots {J}\right)$
38 eleq1 ${⊢}{k}={J}\to \left({k}\in \left(1\dots {J}\right)↔{J}\in \left(1\dots {J}\right)\right)$
39 37 38 syl5ibrcom ${⊢}{\phi }\to \left({k}={J}\to {k}\in \left(1\dots {J}\right)\right)$
40 39 anc2li ${⊢}{\phi }\to \left({k}={J}\to \left({\phi }\wedge {k}\in \left(1\dots {J}\right)\right)\right)$
41 1eluzge0 ${⊢}1\in {ℤ}_{\ge 0}$
42 fzss1 ${⊢}1\in {ℤ}_{\ge 0}\to \left(1\dots {J}\right)\subseteq \left(0\dots {J}\right)$
43 42 sseld ${⊢}1\in {ℤ}_{\ge 0}\to \left({k}\in \left(1\dots {J}\right)\to {k}\in \left(0\dots {J}\right)\right)$
44 41 43 ax-mp ${⊢}{k}\in \left(1\dots {J}\right)\to {k}\in \left(0\dots {J}\right)$
45 0red ${⊢}\left({\phi }\wedge {k}\in \left(0\dots {J}\right)\right)\to 0\in ℝ$
46 6 adantr ${⊢}\left({\phi }\wedge {k}\in \left(0\dots {J}\right)\right)\to {C}\in {O}$
47 elfzelz ${⊢}{k}\in \left(0\dots {J}\right)\to {k}\in ℤ$
48 47 adantl ${⊢}\left({\phi }\wedge {k}\in \left(0\dots {J}\right)\right)\to {k}\in ℤ$
49 1 2 3 4 5 46 48 ballotlemfelz ${⊢}\left({\phi }\wedge {k}\in \left(0\dots {J}\right)\right)\to {F}\left({C}\right)\left({k}\right)\in ℤ$
50 49 zred ${⊢}\left({\phi }\wedge {k}\in \left(0\dots {J}\right)\right)\to {F}\left({C}\right)\left({k}\right)\in ℝ$
51 45 50 ltnled ${⊢}\left({\phi }\wedge {k}\in \left(0\dots {J}\right)\right)\to \left(0<{F}\left({C}\right)\left({k}\right)↔¬{F}\left({C}\right)\left({k}\right)\le 0\right)$
52 44 51 sylan2 ${⊢}\left({\phi }\wedge {k}\in \left(1\dots {J}\right)\right)\to \left(0<{F}\left({C}\right)\left({k}\right)↔¬{F}\left({C}\right)\left({k}\right)\le 0\right)$
53 40 52 syl6 ${⊢}{\phi }\to \left({k}={J}\to \left(0<{F}\left({C}\right)\left({k}\right)↔¬{F}\left({C}\right)\left({k}\right)\le 0\right)\right)$
54 53 imp ${⊢}\left({\phi }\wedge {k}={J}\right)\to \left(0<{F}\left({C}\right)\left({k}\right)↔¬{F}\left({C}\right)\left({k}\right)\le 0\right)$
55 33 54 bitr3d ${⊢}\left({\phi }\wedge {k}={J}\right)\to \left(0<{F}\left({C}\right)\left({J}\right)↔¬{F}\left({C}\right)\left({k}\right)\le 0\right)$
56 30 55 mpbid ${⊢}\left({\phi }\wedge {k}={J}\right)\to ¬{F}\left({C}\right)\left({k}\right)\le 0$
57 56 ex ${⊢}{\phi }\to \left({k}={J}\to ¬{F}\left({C}\right)\left({k}\right)\le 0\right)$
58 57 con2d ${⊢}{\phi }\to \left({F}\left({C}\right)\left({k}\right)\le 0\to ¬{k}={J}\right)$
59 nn1m1nn ${⊢}{J}\in ℕ\to \left({J}=1\vee {J}-1\in ℕ\right)$
60 7 59 syl ${⊢}{\phi }\to \left({J}=1\vee {J}-1\in ℕ\right)$
61 8 adantr ${⊢}\left({\phi }\wedge {J}=1\right)\to \exists {i}\in \left(1\dots {J}\right)\phantom{\rule{.4em}{0ex}}{F}\left({C}\right)\left({i}\right)\le 0$
62 oveq1 ${⊢}{J}=1\to \left({J}\dots {J}\right)=\left(1\dots {J}\right)$
63 62 adantl ${⊢}\left({\phi }\wedge {J}=1\right)\to \left({J}\dots {J}\right)=\left(1\dots {J}\right)$
64 7 nnzd ${⊢}{\phi }\to {J}\in ℤ$
65 fzsn ${⊢}{J}\in ℤ\to \left({J}\dots {J}\right)=\left\{{J}\right\}$
66 64 65 syl ${⊢}{\phi }\to \left({J}\dots {J}\right)=\left\{{J}\right\}$
67 66 adantr ${⊢}\left({\phi }\wedge {J}=1\right)\to \left({J}\dots {J}\right)=\left\{{J}\right\}$
68 63 67 eqtr3d ${⊢}\left({\phi }\wedge {J}=1\right)\to \left(1\dots {J}\right)=\left\{{J}\right\}$
69 68 rexeqdv ${⊢}\left({\phi }\wedge {J}=1\right)\to \left(\exists {i}\in \left(1\dots {J}\right)\phantom{\rule{.4em}{0ex}}{F}\left({C}\right)\left({i}\right)\le 0↔\exists {i}\in \left\{{J}\right\}\phantom{\rule{.4em}{0ex}}{F}\left({C}\right)\left({i}\right)\le 0\right)$
70 61 69 mpbid ${⊢}\left({\phi }\wedge {J}=1\right)\to \exists {i}\in \left\{{J}\right\}\phantom{\rule{.4em}{0ex}}{F}\left({C}\right)\left({i}\right)\le 0$
71 fveq2 ${⊢}{i}={J}\to {F}\left({C}\right)\left({i}\right)={F}\left({C}\right)\left({J}\right)$
72 71 breq1d ${⊢}{i}={J}\to \left({F}\left({C}\right)\left({i}\right)\le 0↔{F}\left({C}\right)\left({J}\right)\le 0\right)$
73 72 rexsng ${⊢}{J}\in ℕ\to \left(\exists {i}\in \left\{{J}\right\}\phantom{\rule{.4em}{0ex}}{F}\left({C}\right)\left({i}\right)\le 0↔{F}\left({C}\right)\left({J}\right)\le 0\right)$
74 7 73 syl ${⊢}{\phi }\to \left(\exists {i}\in \left\{{J}\right\}\phantom{\rule{.4em}{0ex}}{F}\left({C}\right)\left({i}\right)\le 0↔{F}\left({C}\right)\left({J}\right)\le 0\right)$
75 74 adantr ${⊢}\left({\phi }\wedge {J}=1\right)\to \left(\exists {i}\in \left\{{J}\right\}\phantom{\rule{.4em}{0ex}}{F}\left({C}\right)\left({i}\right)\le 0↔{F}\left({C}\right)\left({J}\right)\le 0\right)$
76 70 75 mpbid ${⊢}\left({\phi }\wedge {J}=1\right)\to {F}\left({C}\right)\left({J}\right)\le 0$
77 9 adantr ${⊢}\left({\phi }\wedge {J}=1\right)\to 0<{F}\left({C}\right)\left({J}\right)$
78 0red ${⊢}{\phi }\to 0\in ℝ$
79 1 2 3 4 5 6 64 ballotlemfelz ${⊢}{\phi }\to {F}\left({C}\right)\left({J}\right)\in ℤ$
80 79 zred ${⊢}{\phi }\to {F}\left({C}\right)\left({J}\right)\in ℝ$
81 78 80 ltnled ${⊢}{\phi }\to \left(0<{F}\left({C}\right)\left({J}\right)↔¬{F}\left({C}\right)\left({J}\right)\le 0\right)$
82 81 adantr ${⊢}\left({\phi }\wedge {J}=1\right)\to \left(0<{F}\left({C}\right)\left({J}\right)↔¬{F}\left({C}\right)\left({J}\right)\le 0\right)$
83 77 82 mpbid ${⊢}\left({\phi }\wedge {J}=1\right)\to ¬{F}\left({C}\right)\left({J}\right)\le 0$
84 76 83 pm2.65da ${⊢}{\phi }\to ¬{J}=1$
85 biortn ${⊢}¬{J}=1\to \left({J}-1\in ℕ↔\left(¬¬{J}=1\vee {J}-1\in ℕ\right)\right)$
86 84 85 syl ${⊢}{\phi }\to \left({J}-1\in ℕ↔\left(¬¬{J}=1\vee {J}-1\in ℕ\right)\right)$
87 notnotb ${⊢}{J}=1↔¬¬{J}=1$
88 87 orbi1i ${⊢}\left({J}=1\vee {J}-1\in ℕ\right)↔\left(¬¬{J}=1\vee {J}-1\in ℕ\right)$
89 86 88 syl6bbr ${⊢}{\phi }\to \left({J}-1\in ℕ↔\left({J}=1\vee {J}-1\in ℕ\right)\right)$
90 60 89 mpbird ${⊢}{\phi }\to {J}-1\in ℕ$
91 elnnuz ${⊢}{J}-1\in ℕ↔{J}-1\in {ℤ}_{\ge 1}$
92 90 91 sylib ${⊢}{\phi }\to {J}-1\in {ℤ}_{\ge 1}$
93 elfzp1 ${⊢}{J}-1\in {ℤ}_{\ge 1}\to \left({k}\in \left(1\dots {J}-1+1\right)↔\left({k}\in \left(1\dots {J}-1\right)\vee {k}={J}-1+1\right)\right)$
94 92 93 syl ${⊢}{\phi }\to \left({k}\in \left(1\dots {J}-1+1\right)↔\left({k}\in \left(1\dots {J}-1\right)\vee {k}={J}-1+1\right)\right)$
95 7 nncnd ${⊢}{\phi }\to {J}\in ℂ$
96 1cnd ${⊢}{\phi }\to 1\in ℂ$
97 95 96 npcand ${⊢}{\phi }\to {J}-1+1={J}$
98 97 oveq2d ${⊢}{\phi }\to \left(1\dots {J}-1+1\right)=\left(1\dots {J}\right)$
99 98 eleq2d ${⊢}{\phi }\to \left({k}\in \left(1\dots {J}-1+1\right)↔{k}\in \left(1\dots {J}\right)\right)$
100 97 eqeq2d ${⊢}{\phi }\to \left({k}={J}-1+1↔{k}={J}\right)$
101 100 orbi2d ${⊢}{\phi }\to \left(\left({k}\in \left(1\dots {J}-1\right)\vee {k}={J}-1+1\right)↔\left({k}\in \left(1\dots {J}-1\right)\vee {k}={J}\right)\right)$
102 94 99 101 3bitr3d ${⊢}{\phi }\to \left({k}\in \left(1\dots {J}\right)↔\left({k}\in \left(1\dots {J}-1\right)\vee {k}={J}\right)\right)$
103 orcom ${⊢}\left({k}\in \left(1\dots {J}-1\right)\vee {k}={J}\right)↔\left({k}={J}\vee {k}\in \left(1\dots {J}-1\right)\right)$
104 102 103 syl6bb ${⊢}{\phi }\to \left({k}\in \left(1\dots {J}\right)↔\left({k}={J}\vee {k}\in \left(1\dots {J}-1\right)\right)\right)$
105 104 biimpd ${⊢}{\phi }\to \left({k}\in \left(1\dots {J}\right)\to \left({k}={J}\vee {k}\in \left(1\dots {J}-1\right)\right)\right)$
106 pm5.6 ${⊢}\left(\left({k}\in \left(1\dots {J}\right)\wedge ¬{k}={J}\right)\to {k}\in \left(1\dots {J}-1\right)\right)↔\left({k}\in \left(1\dots {J}\right)\to \left({k}={J}\vee {k}\in \left(1\dots {J}-1\right)\right)\right)$
107 105 106 sylibr ${⊢}{\phi }\to \left(\left({k}\in \left(1\dots {J}\right)\wedge ¬{k}={J}\right)\to {k}\in \left(1\dots {J}-1\right)\right)$
108 90 nnzd ${⊢}{\phi }\to {J}-1\in ℤ$
109 1z ${⊢}1\in ℤ$
110 108 109 jctil ${⊢}{\phi }\to \left(1\in ℤ\wedge {J}-1\in ℤ\right)$
111 elfzelz ${⊢}{k}\in \left(1\dots {J}-1\right)\to {k}\in ℤ$
112 111 109 jctir ${⊢}{k}\in \left(1\dots {J}-1\right)\to \left({k}\in ℤ\wedge 1\in ℤ\right)$
113 fzaddel ${⊢}\left(\left(1\in ℤ\wedge {J}-1\in ℤ\right)\wedge \left({k}\in ℤ\wedge 1\in ℤ\right)\right)\to \left({k}\in \left(1\dots {J}-1\right)↔{k}+1\in \left(1+1\dots {J}-1+1\right)\right)$
114 110 112 113 syl2an ${⊢}\left({\phi }\wedge {k}\in \left(1\dots {J}-1\right)\right)\to \left({k}\in \left(1\dots {J}-1\right)↔{k}+1\in \left(1+1\dots {J}-1+1\right)\right)$
115 114 biimp3a ${⊢}\left({\phi }\wedge {k}\in \left(1\dots {J}-1\right)\wedge {k}\in \left(1\dots {J}-1\right)\right)\to {k}+1\in \left(1+1\dots {J}-1+1\right)$
116 115 3anidm23 ${⊢}\left({\phi }\wedge {k}\in \left(1\dots {J}-1\right)\right)\to {k}+1\in \left(1+1\dots {J}-1+1\right)$
117 1p1e2 ${⊢}1+1=2$
118 117 a1i ${⊢}{\phi }\to 1+1=2$
119 118 97 oveq12d ${⊢}{\phi }\to \left(1+1\dots {J}-1+1\right)=\left(2\dots {J}\right)$
120 119 eleq2d ${⊢}{\phi }\to \left({k}+1\in \left(1+1\dots {J}-1+1\right)↔{k}+1\in \left(2\dots {J}\right)\right)$
121 2eluzge1 ${⊢}2\in {ℤ}_{\ge 1}$
122 fzss1 ${⊢}2\in {ℤ}_{\ge 1}\to \left(2\dots {J}\right)\subseteq \left(1\dots {J}\right)$
123 121 122 ax-mp ${⊢}\left(2\dots {J}\right)\subseteq \left(1\dots {J}\right)$
124 123 sseli ${⊢}{k}+1\in \left(2\dots {J}\right)\to {k}+1\in \left(1\dots {J}\right)$
125 120 124 syl6bi ${⊢}{\phi }\to \left({k}+1\in \left(1+1\dots {J}-1+1\right)\to {k}+1\in \left(1\dots {J}\right)\right)$
126 125 adantr ${⊢}\left({\phi }\wedge {k}\in \left(1\dots {J}-1\right)\right)\to \left({k}+1\in \left(1+1\dots {J}-1+1\right)\to {k}+1\in \left(1\dots {J}\right)\right)$
127 116 126 mpd ${⊢}\left({\phi }\wedge {k}\in \left(1\dots {J}-1\right)\right)\to {k}+1\in \left(1\dots {J}\right)$
128 127 ex ${⊢}{\phi }\to \left({k}\in \left(1\dots {J}-1\right)\to {k}+1\in \left(1\dots {J}\right)\right)$
129 107 128 syld ${⊢}{\phi }\to \left(\left({k}\in \left(1\dots {J}\right)\wedge ¬{k}={J}\right)\to {k}+1\in \left(1\dots {J}\right)\right)$
130 58 129 sylan2d ${⊢}{\phi }\to \left(\left({k}\in \left(1\dots {J}\right)\wedge {F}\left({C}\right)\left({k}\right)\le 0\right)\to {k}+1\in \left(1\dots {J}\right)\right)$
131 130 imp ${⊢}\left({\phi }\wedge \left({k}\in \left(1\dots {J}\right)\wedge {F}\left({C}\right)\left({k}\right)\le 0\right)\right)\to {k}+1\in \left(1\dots {J}\right)$
132 131 adantrr ${⊢}\left({\phi }\wedge \left(\left({k}\in \left(1\dots {J}\right)\wedge {F}\left({C}\right)\left({k}\right)\le 0\right)\wedge \forall {j}\in \left\{{i}\in \left(1\dots {J}\right)|{F}\left({C}\right)\left({i}\right)\le 0\right\}\phantom{\rule{.4em}{0ex}}{j}\le {k}\right)\right)\to {k}+1\in \left(1\dots {J}\right)$
133 fveq2 ${⊢}{i}={k}+1\to {F}\left({C}\right)\left({i}\right)={F}\left({C}\right)\left({k}+1\right)$
134 133 breq1d ${⊢}{i}={k}+1\to \left({F}\left({C}\right)\left({i}\right)\le 0↔{F}\left({C}\right)\left({k}+1\right)\le 0\right)$
135 134 elrab ${⊢}{k}+1\in \left\{{i}\in \left(1\dots {J}\right)|{F}\left({C}\right)\left({i}\right)\le 0\right\}↔\left({k}+1\in \left(1\dots {J}\right)\wedge {F}\left({C}\right)\left({k}+1\right)\le 0\right)$
136 breq1 ${⊢}{j}={k}+1\to \left({j}\le {k}↔{k}+1\le {k}\right)$
137 136 rspccva ${⊢}\left(\forall {j}\in \left\{{i}\in \left(1\dots {J}\right)|{F}\left({C}\right)\left({i}\right)\le 0\right\}\phantom{\rule{.4em}{0ex}}{j}\le {k}\wedge {k}+1\in \left\{{i}\in \left(1\dots {J}\right)|{F}\left({C}\right)\left({i}\right)\le 0\right\}\right)\to {k}+1\le {k}$
138 135 137 sylan2br ${⊢}\left(\forall {j}\in \left\{{i}\in \left(1\dots {J}\right)|{F}\left({C}\right)\left({i}\right)\le 0\right\}\phantom{\rule{.4em}{0ex}}{j}\le {k}\wedge \left({k}+1\in \left(1\dots {J}\right)\wedge {F}\left({C}\right)\left({k}+1\right)\le 0\right)\right)\to {k}+1\le {k}$
139 138 expr ${⊢}\left(\forall {j}\in \left\{{i}\in \left(1\dots {J}\right)|{F}\left({C}\right)\left({i}\right)\le 0\right\}\phantom{\rule{.4em}{0ex}}{j}\le {k}\wedge {k}+1\in \left(1\dots {J}\right)\right)\to \left({F}\left({C}\right)\left({k}+1\right)\le 0\to {k}+1\le {k}\right)$
140 139 con3d ${⊢}\left(\forall {j}\in \left\{{i}\in \left(1\dots {J}\right)|{F}\left({C}\right)\left({i}\right)\le 0\right\}\phantom{\rule{.4em}{0ex}}{j}\le {k}\wedge {k}+1\in \left(1\dots {J}\right)\right)\to \left(¬{k}+1\le {k}\to ¬{F}\left({C}\right)\left({k}+1\right)\le 0\right)$
141 29 132 140 syl2anc ${⊢}\left({\phi }\wedge \left(\left({k}\in \left(1\dots {J}\right)\wedge {F}\left({C}\right)\left({k}\right)\le 0\right)\wedge \forall {j}\in \left\{{i}\in \left(1\dots {J}\right)|{F}\left({C}\right)\left({i}\right)\le 0\right\}\phantom{\rule{.4em}{0ex}}{j}\le {k}\right)\right)\to \left(¬{k}+1\le {k}\to ¬{F}\left({C}\right)\left({k}+1\right)\le 0\right)$
142 28 141 mpd ${⊢}\left({\phi }\wedge \left(\left({k}\in \left(1\dots {J}\right)\wedge {F}\left({C}\right)\left({k}\right)\le 0\right)\wedge \forall {j}\in \left\{{i}\in \left(1\dots {J}\right)|{F}\left({C}\right)\left({i}\right)\le 0\right\}\phantom{\rule{.4em}{0ex}}{j}\le {k}\right)\right)\to ¬{F}\left({C}\right)\left({k}+1\right)\le 0$
143 simplrr ${⊢}\left(\left({\phi }\wedge \left(\left({k}\in \left(1\dots {J}\right)\wedge {F}\left({C}\right)\left({k}\right)\le 0\right)\wedge \forall {j}\in \left\{{i}\in \left(1\dots {J}\right)|{F}\left({C}\right)\left({i}\right)\le 0\right\}\phantom{\rule{.4em}{0ex}}{j}\le {k}\right)\right)\wedge ¬{k}+1\in {C}\right)\to \forall {j}\in \left\{{i}\in \left(1\dots {J}\right)|{F}\left({C}\right)\left({i}\right)\le 0\right\}\phantom{\rule{.4em}{0ex}}{j}\le {k}$
144 132 adantr ${⊢}\left(\left({\phi }\wedge \left(\left({k}\in \left(1\dots {J}\right)\wedge {F}\left({C}\right)\left({k}\right)\le 0\right)\wedge \forall {j}\in \left\{{i}\in \left(1\dots {J}\right)|{F}\left({C}\right)\left({i}\right)\le 0\right\}\phantom{\rule{.4em}{0ex}}{j}\le {k}\right)\right)\wedge ¬{k}+1\in {C}\right)\to {k}+1\in \left(1\dots {J}\right)$
145 simpll ${⊢}\left(\left({\phi }\wedge \left({k}\in \left(1\dots {J}\right)\wedge {F}\left({C}\right)\left({k}\right)\le 0\right)\right)\wedge ¬{k}+1\in {C}\right)\to {\phi }$
146 131 adantr ${⊢}\left(\left({\phi }\wedge \left({k}\in \left(1\dots {J}\right)\wedge {F}\left({C}\right)\left({k}\right)\le 0\right)\right)\wedge ¬{k}+1\in {C}\right)\to {k}+1\in \left(1\dots {J}\right)$
147 42 sseld ${⊢}1\in {ℤ}_{\ge 0}\to \left({k}+1\in \left(1\dots {J}\right)\to {k}+1\in \left(0\dots {J}\right)\right)$
148 41 146 147 mpsyl ${⊢}\left(\left({\phi }\wedge \left({k}\in \left(1\dots {J}\right)\wedge {F}\left({C}\right)\left({k}\right)\le 0\right)\right)\wedge ¬{k}+1\in {C}\right)\to {k}+1\in \left(0\dots {J}\right)$
149 6 adantr ${⊢}\left({\phi }\wedge {k}+1\in \left(0\dots {J}\right)\right)\to {C}\in {O}$
150 elfzelz ${⊢}{k}+1\in \left(0\dots {J}\right)\to {k}+1\in ℤ$
151 150 adantl ${⊢}\left({\phi }\wedge {k}+1\in \left(0\dots {J}\right)\right)\to {k}+1\in ℤ$
152 1 2 3 4 5 149 151 ballotlemfelz ${⊢}\left({\phi }\wedge {k}+1\in \left(0\dots {J}\right)\right)\to {F}\left({C}\right)\left({k}+1\right)\in ℤ$
153 152 zred ${⊢}\left({\phi }\wedge {k}+1\in \left(0\dots {J}\right)\right)\to {F}\left({C}\right)\left({k}+1\right)\in ℝ$
154 145 148 153 syl2anc ${⊢}\left(\left({\phi }\wedge \left({k}\in \left(1\dots {J}\right)\wedge {F}\left({C}\right)\left({k}\right)\le 0\right)\right)\wedge ¬{k}+1\in {C}\right)\to {F}\left({C}\right)\left({k}+1\right)\in ℝ$
155 0red ${⊢}\left(\left({\phi }\wedge \left({k}\in \left(1\dots {J}\right)\wedge {F}\left({C}\right)\left({k}\right)\le 0\right)\right)\wedge ¬{k}+1\in {C}\right)\to 0\in ℝ$
156 simplrr ${⊢}\left(\left({\phi }\wedge \left({k}\in \left(1\dots {J}\right)\wedge {F}\left({C}\right)\left({k}\right)\le 0\right)\right)\wedge ¬{k}+1\in {C}\right)\to {F}\left({C}\right)\left({k}\right)\le 0$
157 15 adantr ${⊢}\left(\left({\phi }\wedge \left({k}\in \left(1\dots {J}\right)\wedge {F}\left({C}\right)\left({k}\right)\le 0\right)\right)\wedge ¬{k}+1\in {C}\right)\to {k}\in \left(1\dots {J}\right)$
158 157 44 syl ${⊢}\left(\left({\phi }\wedge \left({k}\in \left(1\dots {J}\right)\wedge {F}\left({C}\right)\left({k}\right)\le 0\right)\right)\wedge ¬{k}+1\in {C}\right)\to {k}\in \left(0\dots {J}\right)$
159 130 imdistani ${⊢}\left({\phi }\wedge \left({k}\in \left(1\dots {J}\right)\wedge {F}\left({C}\right)\left({k}\right)\le 0\right)\right)\to \left({\phi }\wedge {k}+1\in \left(1\dots {J}\right)\right)$
160 6 adantr ${⊢}\left({\phi }\wedge {k}+1\in \left(1\dots {J}\right)\right)\to {C}\in {O}$
161 elfznn ${⊢}{k}+1\in \left(1\dots {J}\right)\to {k}+1\in ℕ$
162 161 adantl ${⊢}\left({\phi }\wedge {k}+1\in \left(1\dots {J}\right)\right)\to {k}+1\in ℕ$
163 1 2 3 4 5 160 162 ballotlemfp1 ${⊢}\left({\phi }\wedge {k}+1\in \left(1\dots {J}\right)\right)\to \left(\left(¬{k}+1\in {C}\to {F}\left({C}\right)\left({k}+1\right)={F}\left({C}\right)\left({k}+1-1\right)-1\right)\wedge \left({k}+1\in {C}\to {F}\left({C}\right)\left({k}+1\right)={F}\left({C}\right)\left({k}+1-1\right)+1\right)\right)$
164 163 simpld ${⊢}\left({\phi }\wedge {k}+1\in \left(1\dots {J}\right)\right)\to \left(¬{k}+1\in {C}\to {F}\left({C}\right)\left({k}+1\right)={F}\left({C}\right)\left({k}+1-1\right)-1\right)$
165 164 imp ${⊢}\left(\left({\phi }\wedge {k}+1\in \left(1\dots {J}\right)\right)\wedge ¬{k}+1\in {C}\right)\to {F}\left({C}\right)\left({k}+1\right)={F}\left({C}\right)\left({k}+1-1\right)-1$
166 159 165 sylan ${⊢}\left(\left({\phi }\wedge \left({k}\in \left(1\dots {J}\right)\wedge {F}\left({C}\right)\left({k}\right)\le 0\right)\right)\wedge ¬{k}+1\in {C}\right)\to {F}\left({C}\right)\left({k}+1\right)={F}\left({C}\right)\left({k}+1-1\right)-1$
167 elfzelz ${⊢}{k}\in \left(1\dots {J}\right)\to {k}\in ℤ$
168 167 zcnd ${⊢}{k}\in \left(1\dots {J}\right)\to {k}\in ℂ$
169 1cnd ${⊢}{k}\in \left(1\dots {J}\right)\to 1\in ℂ$
170 168 169 pncand ${⊢}{k}\in \left(1\dots {J}\right)\to {k}+1-1={k}$
171 170 fveq2d ${⊢}{k}\in \left(1\dots {J}\right)\to {F}\left({C}\right)\left({k}+1-1\right)={F}\left({C}\right)\left({k}\right)$
172 171 oveq1d ${⊢}{k}\in \left(1\dots {J}\right)\to {F}\left({C}\right)\left({k}+1-1\right)-1={F}\left({C}\right)\left({k}\right)-1$
173 172 eqeq2d ${⊢}{k}\in \left(1\dots {J}\right)\to \left({F}\left({C}\right)\left({k}+1\right)={F}\left({C}\right)\left({k}+1-1\right)-1↔{F}\left({C}\right)\left({k}+1\right)={F}\left({C}\right)\left({k}\right)-1\right)$
174 157 173 syl ${⊢}\left(\left({\phi }\wedge \left({k}\in \left(1\dots {J}\right)\wedge {F}\left({C}\right)\left({k}\right)\le 0\right)\right)\wedge ¬{k}+1\in {C}\right)\to \left({F}\left({C}\right)\left({k}+1\right)={F}\left({C}\right)\left({k}+1-1\right)-1↔{F}\left({C}\right)\left({k}+1\right)={F}\left({C}\right)\left({k}\right)-1\right)$
175 166 174 mpbid ${⊢}\left(\left({\phi }\wedge \left({k}\in \left(1\dots {J}\right)\wedge {F}\left({C}\right)\left({k}\right)\le 0\right)\right)\wedge ¬{k}+1\in {C}\right)\to {F}\left({C}\right)\left({k}+1\right)={F}\left({C}\right)\left({k}\right)-1$
176 0z ${⊢}0\in ℤ$
177 zlem1lt ${⊢}\left({F}\left({C}\right)\left({k}\right)\in ℤ\wedge 0\in ℤ\right)\to \left({F}\left({C}\right)\left({k}\right)\le 0↔{F}\left({C}\right)\left({k}\right)-1<0\right)$
178 49 176 177 sylancl ${⊢}\left({\phi }\wedge {k}\in \left(0\dots {J}\right)\right)\to \left({F}\left({C}\right)\left({k}\right)\le 0↔{F}\left({C}\right)\left({k}\right)-1<0\right)$
179 178 adantr ${⊢}\left(\left({\phi }\wedge {k}\in \left(0\dots {J}\right)\right)\wedge {F}\left({C}\right)\left({k}+1\right)={F}\left({C}\right)\left({k}\right)-1\right)\to \left({F}\left({C}\right)\left({k}\right)\le 0↔{F}\left({C}\right)\left({k}\right)-1<0\right)$
180 breq1 ${⊢}{F}\left({C}\right)\left({k}+1\right)={F}\left({C}\right)\left({k}\right)-1\to \left({F}\left({C}\right)\left({k}+1\right)<0↔{F}\left({C}\right)\left({k}\right)-1<0\right)$
181 180 adantl ${⊢}\left(\left({\phi }\wedge {k}\in \left(0\dots {J}\right)\right)\wedge {F}\left({C}\right)\left({k}+1\right)={F}\left({C}\right)\left({k}\right)-1\right)\to \left({F}\left({C}\right)\left({k}+1\right)<0↔{F}\left({C}\right)\left({k}\right)-1<0\right)$
182 179 181 bitr4d ${⊢}\left(\left({\phi }\wedge {k}\in \left(0\dots {J}\right)\right)\wedge {F}\left({C}\right)\left({k}+1\right)={F}\left({C}\right)\left({k}\right)-1\right)\to \left({F}\left({C}\right)\left({k}\right)\le 0↔{F}\left({C}\right)\left({k}+1\right)<0\right)$
183 145 158 175 182 syl21anc ${⊢}\left(\left({\phi }\wedge \left({k}\in \left(1\dots {J}\right)\wedge {F}\left({C}\right)\left({k}\right)\le 0\right)\right)\wedge ¬{k}+1\in {C}\right)\to \left({F}\left({C}\right)\left({k}\right)\le 0↔{F}\left({C}\right)\left({k}+1\right)<0\right)$
184 156 183 mpbid ${⊢}\left(\left({\phi }\wedge \left({k}\in \left(1\dots {J}\right)\wedge {F}\left({C}\right)\left({k}\right)\le 0\right)\right)\wedge ¬{k}+1\in {C}\right)\to {F}\left({C}\right)\left({k}+1\right)<0$
185 154 155 184 ltled ${⊢}\left(\left({\phi }\wedge \left({k}\in \left(1\dots {J}\right)\wedge {F}\left({C}\right)\left({k}\right)\le 0\right)\right)\wedge ¬{k}+1\in {C}\right)\to {F}\left({C}\right)\left({k}+1\right)\le 0$
186 185 adantlrr ${⊢}\left(\left({\phi }\wedge \left(\left({k}\in \left(1\dots {J}\right)\wedge {F}\left({C}\right)\left({k}\right)\le 0\right)\wedge \forall {j}\in \left\{{i}\in \left(1\dots {J}\right)|{F}\left({C}\right)\left({i}\right)\le 0\right\}\phantom{\rule{.4em}{0ex}}{j}\le {k}\right)\right)\wedge ¬{k}+1\in {C}\right)\to {F}\left({C}\right)\left({k}+1\right)\le 0$
187 143 144 186 138 syl12anc ${⊢}\left(\left({\phi }\wedge \left(\left({k}\in \left(1\dots {J}\right)\wedge {F}\left({C}\right)\left({k}\right)\le 0\right)\wedge \forall {j}\in \left\{{i}\in \left(1\dots {J}\right)|{F}\left({C}\right)\left({i}\right)\le 0\right\}\phantom{\rule{.4em}{0ex}}{j}\le {k}\right)\right)\wedge ¬{k}+1\in {C}\right)\to {k}+1\le {k}$
188 28 adantr ${⊢}\left(\left({\phi }\wedge \left(\left({k}\in \left(1\dots {J}\right)\wedge {F}\left({C}\right)\left({k}\right)\le 0\right)\wedge \forall {j}\in \left\{{i}\in \left(1\dots {J}\right)|{F}\left({C}\right)\left({i}\right)\le 0\right\}\phantom{\rule{.4em}{0ex}}{j}\le {k}\right)\right)\wedge ¬{k}+1\in {C}\right)\to ¬{k}+1\le {k}$
189 187 188 condan ${⊢}\left({\phi }\wedge \left(\left({k}\in \left(1\dots {J}\right)\wedge {F}\left({C}\right)\left({k}\right)\le 0\right)\wedge \forall {j}\in \left\{{i}\in \left(1\dots {J}\right)|{F}\left({C}\right)\left({i}\right)\le 0\right\}\phantom{\rule{.4em}{0ex}}{j}\le {k}\right)\right)\to {k}+1\in {C}$
190 163 simprd ${⊢}\left({\phi }\wedge {k}+1\in \left(1\dots {J}\right)\right)\to \left({k}+1\in {C}\to {F}\left({C}\right)\left({k}+1\right)={F}\left({C}\right)\left({k}+1-1\right)+1\right)$
191 190 imp ${⊢}\left(\left({\phi }\wedge {k}+1\in \left(1\dots {J}\right)\right)\wedge {k}+1\in {C}\right)\to {F}\left({C}\right)\left({k}+1\right)={F}\left({C}\right)\left({k}+1-1\right)+1$
192 159 191 sylan ${⊢}\left(\left({\phi }\wedge \left({k}\in \left(1\dots {J}\right)\wedge {F}\left({C}\right)\left({k}\right)\le 0\right)\right)\wedge {k}+1\in {C}\right)\to {F}\left({C}\right)\left({k}+1\right)={F}\left({C}\right)\left({k}+1-1\right)+1$
193 15 adantr ${⊢}\left(\left({\phi }\wedge \left({k}\in \left(1\dots {J}\right)\wedge {F}\left({C}\right)\left({k}\right)\le 0\right)\right)\wedge {k}+1\in {C}\right)\to {k}\in \left(1\dots {J}\right)$
194 171 oveq1d ${⊢}{k}\in \left(1\dots {J}\right)\to {F}\left({C}\right)\left({k}+1-1\right)+1={F}\left({C}\right)\left({k}\right)+1$
195 194 eqeq2d ${⊢}{k}\in \left(1\dots {J}\right)\to \left({F}\left({C}\right)\left({k}+1\right)={F}\left({C}\right)\left({k}+1-1\right)+1↔{F}\left({C}\right)\left({k}+1\right)={F}\left({C}\right)\left({k}\right)+1\right)$
196 193 195 syl ${⊢}\left(\left({\phi }\wedge \left({k}\in \left(1\dots {J}\right)\wedge {F}\left({C}\right)\left({k}\right)\le 0\right)\right)\wedge {k}+1\in {C}\right)\to \left({F}\left({C}\right)\left({k}+1\right)={F}\left({C}\right)\left({k}+1-1\right)+1↔{F}\left({C}\right)\left({k}+1\right)={F}\left({C}\right)\left({k}\right)+1\right)$
197 192 196 mpbid ${⊢}\left(\left({\phi }\wedge \left({k}\in \left(1\dots {J}\right)\wedge {F}\left({C}\right)\left({k}\right)\le 0\right)\right)\wedge {k}+1\in {C}\right)\to {F}\left({C}\right)\left({k}+1\right)={F}\left({C}\right)\left({k}\right)+1$
198 197 adantlrr ${⊢}\left(\left({\phi }\wedge \left(\left({k}\in \left(1\dots {J}\right)\wedge {F}\left({C}\right)\left({k}\right)\le 0\right)\wedge \forall {j}\in \left\{{i}\in \left(1\dots {J}\right)|{F}\left({C}\right)\left({i}\right)\le 0\right\}\phantom{\rule{.4em}{0ex}}{j}\le {k}\right)\right)\wedge {k}+1\in {C}\right)\to {F}\left({C}\right)\left({k}+1\right)={F}\left({C}\right)\left({k}\right)+1$
199 189 198 mpdan ${⊢}\left({\phi }\wedge \left(\left({k}\in \left(1\dots {J}\right)\wedge {F}\left({C}\right)\left({k}\right)\le 0\right)\wedge \forall {j}\in \left\{{i}\in \left(1\dots {J}\right)|{F}\left({C}\right)\left({i}\right)\le 0\right\}\phantom{\rule{.4em}{0ex}}{j}\le {k}\right)\right)\to {F}\left({C}\right)\left({k}+1\right)={F}\left({C}\right)\left({k}\right)+1$
200 breq1 ${⊢}{F}\left({C}\right)\left({k}+1\right)={F}\left({C}\right)\left({k}\right)+1\to \left({F}\left({C}\right)\left({k}+1\right)\le 0↔{F}\left({C}\right)\left({k}\right)+1\le 0\right)$
201 200 notbid ${⊢}{F}\left({C}\right)\left({k}+1\right)={F}\left({C}\right)\left({k}\right)+1\to \left(¬{F}\left({C}\right)\left({k}+1\right)\le 0↔¬{F}\left({C}\right)\left({k}\right)+1\le 0\right)$
202 199 201 syl ${⊢}\left({\phi }\wedge \left(\left({k}\in \left(1\dots {J}\right)\wedge {F}\left({C}\right)\left({k}\right)\le 0\right)\wedge \forall {j}\in \left\{{i}\in \left(1\dots {J}\right)|{F}\left({C}\right)\left({i}\right)\le 0\right\}\phantom{\rule{.4em}{0ex}}{j}\le {k}\right)\right)\to \left(¬{F}\left({C}\right)\left({k}+1\right)\le 0↔¬{F}\left({C}\right)\left({k}\right)+1\le 0\right)$
203 142 202 mpbid ${⊢}\left({\phi }\wedge \left(\left({k}\in \left(1\dots {J}\right)\wedge {F}\left({C}\right)\left({k}\right)\le 0\right)\wedge \forall {j}\in \left\{{i}\in \left(1\dots {J}\right)|{F}\left({C}\right)\left({i}\right)\le 0\right\}\phantom{\rule{.4em}{0ex}}{j}\le {k}\right)\right)\to ¬{F}\left({C}\right)\left({k}\right)+1\le 0$
204 15 44 syl ${⊢}\left({\phi }\wedge \left({k}\in \left(1\dots {J}\right)\wedge {F}\left({C}\right)\left({k}\right)\le 0\right)\right)\to {k}\in \left(0\dots {J}\right)$
205 204 49 syldan ${⊢}\left({\phi }\wedge \left({k}\in \left(1\dots {J}\right)\wedge {F}\left({C}\right)\left({k}\right)\le 0\right)\right)\to {F}\left({C}\right)\left({k}\right)\in ℤ$
206 205 adantrr ${⊢}\left({\phi }\wedge \left(\left({k}\in \left(1\dots {J}\right)\wedge {F}\left({C}\right)\left({k}\right)\le 0\right)\wedge \forall {j}\in \left\{{i}\in \left(1\dots {J}\right)|{F}\left({C}\right)\left({i}\right)\le 0\right\}\phantom{\rule{.4em}{0ex}}{j}\le {k}\right)\right)\to {F}\left({C}\right)\left({k}\right)\in ℤ$
207 zleltp1 ${⊢}\left(0\in ℤ\wedge {F}\left({C}\right)\left({k}\right)\in ℤ\right)\to \left(0\le {F}\left({C}\right)\left({k}\right)↔0<{F}\left({C}\right)\left({k}\right)+1\right)$
208 176 207 mpan ${⊢}{F}\left({C}\right)\left({k}\right)\in ℤ\to \left(0\le {F}\left({C}\right)\left({k}\right)↔0<{F}\left({C}\right)\left({k}\right)+1\right)$
209 0red ${⊢}{F}\left({C}\right)\left({k}\right)\in ℤ\to 0\in ℝ$
210 zre ${⊢}{F}\left({C}\right)\left({k}\right)\in ℤ\to {F}\left({C}\right)\left({k}\right)\in ℝ$
211 1red ${⊢}{F}\left({C}\right)\left({k}\right)\in ℤ\to 1\in ℝ$
212 210 211 readdcld ${⊢}{F}\left({C}\right)\left({k}\right)\in ℤ\to {F}\left({C}\right)\left({k}\right)+1\in ℝ$
213 209 212 ltnled ${⊢}{F}\left({C}\right)\left({k}\right)\in ℤ\to \left(0<{F}\left({C}\right)\left({k}\right)+1↔¬{F}\left({C}\right)\left({k}\right)+1\le 0\right)$
214 208 213 bitrd ${⊢}{F}\left({C}\right)\left({k}\right)\in ℤ\to \left(0\le {F}\left({C}\right)\left({k}\right)↔¬{F}\left({C}\right)\left({k}\right)+1\le 0\right)$
215 206 214 syl ${⊢}\left({\phi }\wedge \left(\left({k}\in \left(1\dots {J}\right)\wedge {F}\left({C}\right)\left({k}\right)\le 0\right)\wedge \forall {j}\in \left\{{i}\in \left(1\dots {J}\right)|{F}\left({C}\right)\left({i}\right)\le 0\right\}\phantom{\rule{.4em}{0ex}}{j}\le {k}\right)\right)\to \left(0\le {F}\left({C}\right)\left({k}\right)↔¬{F}\left({C}\right)\left({k}\right)+1\le 0\right)$
216 203 215 mpbird ${⊢}\left({\phi }\wedge \left(\left({k}\in \left(1\dots {J}\right)\wedge {F}\left({C}\right)\left({k}\right)\le 0\right)\wedge \forall {j}\in \left\{{i}\in \left(1\dots {J}\right)|{F}\left({C}\right)\left({i}\right)\le 0\right\}\phantom{\rule{.4em}{0ex}}{j}\le {k}\right)\right)\to 0\le {F}\left({C}\right)\left({k}\right)$
217 206 zred ${⊢}\left({\phi }\wedge \left(\left({k}\in \left(1\dots {J}\right)\wedge {F}\left({C}\right)\left({k}\right)\le 0\right)\wedge \forall {j}\in \left\{{i}\in \left(1\dots {J}\right)|{F}\left({C}\right)\left({i}\right)\le 0\right\}\phantom{\rule{.4em}{0ex}}{j}\le {k}\right)\right)\to {F}\left({C}\right)\left({k}\right)\in ℝ$
218 0red ${⊢}\left({\phi }\wedge \left(\left({k}\in \left(1\dots {J}\right)\wedge {F}\left({C}\right)\left({k}\right)\le 0\right)\wedge \forall {j}\in \left\{{i}\in \left(1\dots {J}\right)|{F}\left({C}\right)\left({i}\right)\le 0\right\}\phantom{\rule{.4em}{0ex}}{j}\le {k}\right)\right)\to 0\in ℝ$
219 217 218 letri3d ${⊢}\left({\phi }\wedge \left(\left({k}\in \left(1\dots {J}\right)\wedge {F}\left({C}\right)\left({k}\right)\le 0\right)\wedge \forall {j}\in \left\{{i}\in \left(1\dots {J}\right)|{F}\left({C}\right)\left({i}\right)\le 0\right\}\phantom{\rule{.4em}{0ex}}{j}\le {k}\right)\right)\to \left({F}\left({C}\right)\left({k}\right)=0↔\left({F}\left({C}\right)\left({k}\right)\le 0\wedge 0\le {F}\left({C}\right)\left({k}\right)\right)\right)$
220 14 216 219 mpbir2and ${⊢}\left({\phi }\wedge \left(\left({k}\in \left(1\dots {J}\right)\wedge {F}\left({C}\right)\left({k}\right)\le 0\right)\wedge \forall {j}\in \left\{{i}\in \left(1\dots {J}\right)|{F}\left({C}\right)\left({i}\right)\le 0\right\}\phantom{\rule{.4em}{0ex}}{j}\le {k}\right)\right)\to {F}\left({C}\right)\left({k}\right)=0$
221 13 220 sylan2b ${⊢}\left({\phi }\wedge \left({k}\in \left\{{i}\in \left(1\dots {J}\right)|{F}\left({C}\right)\left({i}\right)\le 0\right\}\wedge \forall {j}\in \left\{{i}\in \left(1\dots {J}\right)|{F}\left({C}\right)\left({i}\right)\le 0\right\}\phantom{\rule{.4em}{0ex}}{j}\le {k}\right)\right)\to {F}\left({C}\right)\left({k}\right)=0$
222 ssrab2 ${⊢}\left\{{i}\in \left(1\dots {J}\right)|{F}\left({C}\right)\left({i}\right)\le 0\right\}\subseteq \left(1\dots {J}\right)$
223 222 21 sstri ${⊢}\left\{{i}\in \left(1\dots {J}\right)|{F}\left({C}\right)\left({i}\right)\le 0\right\}\subseteq ℝ$
224 223 a1i ${⊢}{\phi }\to \left\{{i}\in \left(1\dots {J}\right)|{F}\left({C}\right)\left({i}\right)\le 0\right\}\subseteq ℝ$
225 fzfi ${⊢}\left(1\dots {J}\right)\in \mathrm{Fin}$
226 ssfi ${⊢}\left(\left(1\dots {J}\right)\in \mathrm{Fin}\wedge \left\{{i}\in \left(1\dots {J}\right)|{F}\left({C}\right)\left({i}\right)\le 0\right\}\subseteq \left(1\dots {J}\right)\right)\to \left\{{i}\in \left(1\dots {J}\right)|{F}\left({C}\right)\left({i}\right)\le 0\right\}\in \mathrm{Fin}$
227 225 222 226 mp2an ${⊢}\left\{{i}\in \left(1\dots {J}\right)|{F}\left({C}\right)\left({i}\right)\le 0\right\}\in \mathrm{Fin}$
228 227 a1i ${⊢}{\phi }\to \left\{{i}\in \left(1\dots {J}\right)|{F}\left({C}\right)\left({i}\right)\le 0\right\}\in \mathrm{Fin}$
229 rabn0 ${⊢}\left\{{i}\in \left(1\dots {J}\right)|{F}\left({C}\right)\left({i}\right)\le 0\right\}\ne \varnothing ↔\exists {i}\in \left(1\dots {J}\right)\phantom{\rule{.4em}{0ex}}{F}\left({C}\right)\left({i}\right)\le 0$
230 8 229 sylibr ${⊢}{\phi }\to \left\{{i}\in \left(1\dots {J}\right)|{F}\left({C}\right)\left({i}\right)\le 0\right\}\ne \varnothing$
231 fimaxre ${⊢}\left(\left\{{i}\in \left(1\dots {J}\right)|{F}\left({C}\right)\left({i}\right)\le 0\right\}\subseteq ℝ\wedge \left\{{i}\in \left(1\dots {J}\right)|{F}\left({C}\right)\left({i}\right)\le 0\right\}\in \mathrm{Fin}\wedge \left\{{i}\in \left(1\dots {J}\right)|{F}\left({C}\right)\left({i}\right)\le 0\right\}\ne \varnothing \right)\to \exists {k}\in \left\{{i}\in \left(1\dots {J}\right)|{F}\left({C}\right)\left({i}\right)\le 0\right\}\phantom{\rule{.4em}{0ex}}\forall {j}\in \left\{{i}\in \left(1\dots {J}\right)|{F}\left({C}\right)\left({i}\right)\le 0\right\}\phantom{\rule{.4em}{0ex}}{j}\le {k}$
232 224 228 230 231 syl3anc ${⊢}{\phi }\to \exists {k}\in \left\{{i}\in \left(1\dots {J}\right)|{F}\left({C}\right)\left({i}\right)\le 0\right\}\phantom{\rule{.4em}{0ex}}\forall {j}\in \left\{{i}\in \left(1\dots {J}\right)|{F}\left({C}\right)\left({i}\right)\le 0\right\}\phantom{\rule{.4em}{0ex}}{j}\le {k}$
233 221 232 reximddv ${⊢}{\phi }\to \exists {k}\in \left\{{i}\in \left(1\dots {J}\right)|{F}\left({C}\right)\left({i}\right)\le 0\right\}\phantom{\rule{.4em}{0ex}}{F}\left({C}\right)\left({k}\right)=0$
234 elrabi ${⊢}{k}\in \left\{{i}\in \left(1\dots {J}\right)|{F}\left({C}\right)\left({i}\right)\le 0\right\}\to {k}\in \left(1\dots {J}\right)$
235 234 anim1i ${⊢}\left({k}\in \left\{{i}\in \left(1\dots {J}\right)|{F}\left({C}\right)\left({i}\right)\le 0\right\}\wedge {F}\left({C}\right)\left({k}\right)=0\right)\to \left({k}\in \left(1\dots {J}\right)\wedge {F}\left({C}\right)\left({k}\right)=0\right)$
236 235 reximi2 ${⊢}\exists {k}\in \left\{{i}\in \left(1\dots {J}\right)|{F}\left({C}\right)\left({i}\right)\le 0\right\}\phantom{\rule{.4em}{0ex}}{F}\left({C}\right)\left({k}\right)=0\to \exists {k}\in \left(1\dots {J}\right)\phantom{\rule{.4em}{0ex}}{F}\left({C}\right)\left({k}\right)=0$
237 233 236 syl ${⊢}{\phi }\to \exists {k}\in \left(1\dots {J}\right)\phantom{\rule{.4em}{0ex}}{F}\left({C}\right)\left({k}\right)=0$