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 = \{c \in 𝒫 (1 \dots M + N) \| \|c\| = M\}$
	ballotth.p	$⊢ P = (x \in 𝒫 O ⟼ \frac{\|x\|}{\|O\|})$
	ballotth.f	$⊢ F = (c \in O ⟼ (i \in ℤ ⟼ \|(1 \dots i) \cap c\| - \|(1 \dots i) ∖ c\|))$
	ballotlemfp1.c	$⊢ φ \to C \in O$
	ballotlemfp1.j	$⊢ φ \to J \in ℕ$
	ballotlemfc0.3	$⊢ φ \to \exists i \in (1 \dots J) F (C) (i) \leq 0$
	ballotlemfc0.4	$⊢ φ \to 0 < F (C) (J)$
Assertion	ballotlemfc0	$⊢ φ \to \exists k \in (1 \dots J) F (C) (k) = 0$

Proof

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

Metamath Proof Explorer

Theorem ballotlemfc0

Proof