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	67	rexeqdv	$⊢ (φ \land J = 1) \to (\exists i \in (1 \dots J) 0 \leq F (C) (i) \leftrightarrow \exists i \in \{J\} 0 \leq F (C) (i))$
69	60 68	mpbid	$⊢ (φ \land J = 1) \to \exists i \in \{J\} 0 \leq F (C) (i)$
70		fveq2	$⊢ i = J \to F (C) (i) = F (C) (J)$
71	70	breq2d	$⊢ i = J \to (0 \leq F (C) (i) \leftrightarrow 0 \leq F (C) (J))$
72	71	rexsng	$⊢ J \in ℕ \to (\exists i \in \{J\} 0 \leq F (C) (i) \leftrightarrow 0 \leq F (C) (J))$
73	7 72	syl	$⊢ φ \to (\exists i \in \{J\} 0 \leq F (C) (i) \leftrightarrow 0 \leq F (C) (J))$
74	73	adantr	$⊢ (φ \land J = 1) \to (\exists i \in \{J\} 0 \leq F (C) (i) \leftrightarrow 0 \leq F (C) (J))$
75	69 74	mpbid	$⊢ (φ \land J = 1) \to 0 \leq F (C) (J)$
76	9	adantr	$⊢ (φ \land J = 1) \to F (C) (J) < 0$
77	1 2 3 4 5 6 63	ballotlemfelz	$⊢ φ \to F (C) (J) \in ℤ$
78	77	zred	$⊢ φ \to F (C) (J) \in ℝ$
79		0red	$⊢ φ \to 0 \in ℝ$
80	78 79	ltnled	$⊢ φ \to (F (C) (J) < 0 \leftrightarrow \neg 0 \leq F (C) (J))$
81	80	adantr	$⊢ (φ \land J = 1) \to (F (C) (J) < 0 \leftrightarrow \neg 0 \leq F (C) (J))$
82	76 81	mpbid	$⊢ (φ \land J = 1) \to \neg 0 \leq F (C) (J)$
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	59 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	syl6bb	$⊢ φ \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	syl6bi	$⊢ φ \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	57 128	sylan2d	$⊢ φ \to ((k \in (1 \dots J) \land 0 \leq F (C) (k)) \to k + 1 \in (1 \dots J))$
130	129	imp	$⊢ (φ \land (k \in (1 \dots J) \land 0 \leq F (C) (k))) \to k + 1 \in (1 \dots J)$
131	130	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)$
132		fveq2	$⊢ i = k + 1 \to F (C) (i) = F (C) (k + 1)$
133	132	breq2d	$⊢ i = k + 1 \to (0 \leq F (C) (i) \leftrightarrow 0 \leq F (C) (k + 1))$
134	133	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))$
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) \| 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$
137	134 136	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$
138	137	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)$
139	138	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))$
140	28 131 139	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))$
141	27 140	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)$
142		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$
143	131	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)$
144		0red	$⊢ ((φ \land (k \in (1 \dots J) \land 0 \leq F (C) (k))) \land k + 1 \in C) \to 0 \in ℝ$
145		simpll	$⊢ ((φ \land (k \in (1 \dots J) \land 0 \leq F (C) (k))) \land k + 1 \in C) \to φ$
146	130	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)$
147	41	sseld	$⊢ 1 \in ℤ_{\geq 0} \to (k + 1 \in (1 \dots J) \to k + 1 \in (0 \dots J))$
148	40 146 147	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)$
149	6	adantr	$⊢ (φ \land k + 1 \in (0 \dots J)) \to C \in O$
150		elfzelz	$⊢ k + 1 \in (0 \dots J) \to k + 1 \in ℤ$
151	150	adantl	$⊢ (φ \land k + 1 \in (0 \dots J)) \to k + 1 \in ℤ$
152	1 2 3 4 5 149 151	ballotlemfelz	$⊢ (φ \land k + 1 \in (0 \dots J)) \to F (C) (k + 1) \in ℤ$
153	152	zred	$⊢ (φ \land k + 1 \in (0 \dots J)) \to F (C) (k + 1) \in ℝ$
154	145 148 153	syl2anc	$⊢ ((φ \land (k \in (1 \dots J) \land 0 \leq F (C) (k))) \land k + 1 \in C) \to F (C) (k + 1) \in ℝ$
155		simplrr	$⊢ ((φ \land (k \in (1 \dots J) \land 0 \leq F (C) (k))) \land k + 1 \in C) \to 0 \leq F (C) (k)$
156	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)$
157	156 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)$
158	129	imdistani	$⊢ (φ \land (k \in (1 \dots J) \land 0 \leq F (C) (k))) \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	simprd	$⊢ (φ \land k + 1 \in (1 \dots J)) \to (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 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 0 \leq F (C) (k))) \land 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 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)$
174	165 173	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$
175		0z	$⊢ 0 \in ℤ$
176		zleltp1	$⊢ (0 \in ℤ \land F (C) (k) \in ℤ) \to (0 \leq F (C) (k) \leftrightarrow 0 < F (C) (k) + 1)$
177	175 47 176	sylancr	$⊢ (φ \land k \in (0 \dots J)) \to (0 \leq F (C) (k) \leftrightarrow 0 < F (C) (k) + 1)$
178	177	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)$
179		breq2	$⊢ F (C) (k + 1) = F (C) (k) + 1 \to (0 < F (C) (k + 1) \leftrightarrow 0 < F (C) (k) + 1)$
180	179	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)$
181	178 180	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))$
182	145 157 174 181	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))$
183	155 182	mpbid	$⊢ ((φ \land (k \in (1 \dots J) \land 0 \leq F (C) (k))) \land k + 1 \in C) \to 0 < F (C) (k + 1)$
184	144 154 183	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)$
185	184	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)$
186	142 143 185 137	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$
187	27 186	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$
188	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)$
189	188	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$
190	158 189	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$
191	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)$
192	170	oveq1d	$⊢ k \in (1 \dots J) \to F (C) (k + 1 - 1) - 1 = F (C) (k) - 1$
193	192	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)$
194	191 193	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)$
195	190 194	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$
196	195	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$
197	187 196	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$
198		breq2	$⊢ F (C) (k + 1) = F (C) (k) - 1 \to (0 \leq F (C) (k + 1) \leftrightarrow 0 \leq F (C) (k) - 1)$
199	198	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)$
200	197 199	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)$
201	141 200	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$
202	14 43	syl	$⊢ (φ \land (k \in (1 \dots J) \land 0 \leq F (C) (k))) \to k \in (0 \dots J)$
203	202 47	syldan	$⊢ (φ \land (k \in (1 \dots J) \land 0 \leq F (C) (k))) \to F (C) (k) \in ℤ$
204	203	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 ℤ$
205		zlem1lt	$⊢ (F (C) (k) \in ℤ \land 0 \in ℤ) \to (F (C) (k) \leq 0 \leftrightarrow F (C) (k) - 1 < 0)$
206	175 205	mpan2	$⊢ F (C) (k) \in ℤ \to (F (C) (k) \leq 0 \leftrightarrow F (C) (k) - 1 < 0)$
207		zre	$⊢ F (C) (k) \in ℤ \to F (C) (k) \in ℝ$
208		1red	$⊢ F (C) (k) \in ℤ \to 1 \in ℝ$
209	207 208	resubcld	$⊢ F (C) (k) \in ℤ \to F (C) (k) - 1 \in ℝ$
210		0red	$⊢ F (C) (k) \in ℤ \to 0 \in ℝ$
211	209 210	ltnled	$⊢ F (C) (k) \in ℤ \to (F (C) (k) - 1 < 0 \leftrightarrow \neg 0 \leq F (C) (k) - 1)$
212	206 211	bitrd	$⊢ F (C) (k) \in ℤ \to (F (C) (k) \leq 0 \leftrightarrow \neg 0 \leq F (C) (k) - 1)$
213	204 212	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)$
214	201 213	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$
215		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)$
216	204	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 ℝ$
217		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 ℝ$
218	216 217	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)))$
219	214 215 218	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$
220	13 219	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$
221		ssrab2	$⊢ \{i \in (1 \dots J) \| 0 \leq F (C) (i)\} \subseteq (1 \dots J)$
222	221 20	sstri	$⊢ \{i \in (1 \dots J) \| 0 \leq F (C) (i)\} \subseteq ℝ$
223	222	a1i	$⊢ φ \to \{i \in (1 \dots J) \| 0 \leq F (C) (i)\} \subseteq ℝ$
224		fzfi	$⊢ (1 \dots J) \in Fin$
225		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$
226	224 221 225	mp2an	$⊢ \{i \in (1 \dots J) \| 0 \leq F (C) (i)\} \in Fin$
227	226	a1i	$⊢ φ \to \{i \in (1 \dots J) \| 0 \leq F (C) (i)\} \in Fin$
228		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)$
229	8 228	sylibr	$⊢ φ \to \{i \in (1 \dots J) \| 0 \leq F (C) (i)\} \neq \emptyset$
230		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$
231	223 227 229 230	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$
232	220 231	reximddv	$⊢ φ \to \exists k \in \{i \in (1 \dots J) \| 0 \leq F (C) (i)\} F (C) (k) = 0$
233		elrabi	$⊢ k \in \{i \in (1 \dots J) \| 0 \leq F (C) (i)\} \to k \in (1 \dots J)$
234	233	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)$
235	234	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$
236	232 235	syl	$⊢ φ \to \exists k \in (1 \dots J) F (C) (k) = 0$

Metamath Proof Explorer

Theorem ballotlemfcc

Proof