ballotlemfcc

Description: F takes value 0 between positive and negative values. (Contributed by Thierry Arnoux, 2-Apr-2017)

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

Metamath Proof Explorer

Theorem ballotlemfcc

Proof