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	68	rexeqdv	$⊢ (φ \land J = 1) \to (\exists i \in (1 \dots J) F (C) (i) \leq 0 \leftrightarrow \exists i \in \{J\} F (C) (i) \leq 0)$
70	61 69	mpbid	$⊢ (φ \land J = 1) \to \exists i \in \{J\} F (C) (i) \leq 0$
71		fveq2	$⊢ i = J \to F (C) (i) = F (C) (J)$
72	71	breq1d	$⊢ i = J \to (F (C) (i) \leq 0 \leftrightarrow F (C) (J) \leq 0)$
73	72	rexsng	$⊢ J \in ℕ \to (\exists i \in \{J\} F (C) (i) \leq 0 \leftrightarrow F (C) (J) \leq 0)$
74	7 73	syl	$⊢ φ \to (\exists i \in \{J\} F (C) (i) \leq 0 \leftrightarrow F (C) (J) \leq 0)$
75	74	adantr	$⊢ (φ \land J = 1) \to (\exists i \in \{J\} F (C) (i) \leq 0 \leftrightarrow F (C) (J) \leq 0)$
76	70 75	mpbid	$⊢ (φ \land J = 1) \to F (C) (J) \leq 0$
77	9	adantr	$⊢ (φ \land J = 1) \to 0 < F (C) (J)$
78		0red	$⊢ φ \to 0 \in ℝ$
79	1 2 3 4 5 6 64	ballotlemfelz	$⊢ φ \to F (C) (J) \in ℤ$
80	79	zred	$⊢ φ \to F (C) (J) \in ℝ$
81	78 80	ltnled	$⊢ φ \to (0 < F (C) (J) \leftrightarrow \neg F (C) (J) \leq 0)$
82	81	adantr	$⊢ (φ \land J = 1) \to (0 < F (C) (J) \leftrightarrow \neg F (C) (J) \leq 0)$
83	77 82	mpbid	$⊢ (φ \land J = 1) \to \neg F (C) (J) \leq 0$
84	76 83	pm2.65da	$⊢ φ \to \neg J = 1$
85		biortn	$⊢ \neg J = 1 \to (J - 1 \in ℕ \leftrightarrow (\neg \neg J = 1 \lor J - 1 \in ℕ))$
86	84 85	syl	$⊢ φ \to (J - 1 \in ℕ \leftrightarrow (\neg \neg J = 1 \lor J - 1 \in ℕ))$
87		notnotb	$⊢ J = 1 \leftrightarrow \neg \neg J = 1$
88	87	orbi1i	$⊢ (J = 1 \lor J - 1 \in ℕ) \leftrightarrow (\neg \neg J = 1 \lor J - 1 \in ℕ)$
89	86 88	bitr4di	$⊢ φ \to (J - 1 \in ℕ \leftrightarrow (J = 1 \lor J - 1 \in ℕ))$
90	60 89	mpbird	$⊢ φ \to J - 1 \in ℕ$
91		elnnuz	$⊢ J - 1 \in ℕ \leftrightarrow J - 1 \in ℤ_{\geq 1}$
92	90 91	sylib	$⊢ φ \to J - 1 \in ℤ_{\geq 1}$
93		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))$
94	92 93	syl	$⊢ φ \to (k \in (1 \dots J - 1 + 1) \leftrightarrow (k \in (1 \dots J - 1) \lor k = J - 1 + 1))$
95	7	nncnd	$⊢ φ \to J \in ℂ$
96		1cnd	$⊢ φ \to 1 \in ℂ$
97	95 96	npcand	$⊢ φ \to J - 1 + 1 = J$
98	97	oveq2d	$⊢ φ \to (1 \dots J - 1 + 1) = (1 \dots J)$
99	98	eleq2d	$⊢ φ \to (k \in (1 \dots J - 1 + 1) \leftrightarrow k \in (1 \dots J))$
100	97	eqeq2d	$⊢ φ \to (k = J - 1 + 1 \leftrightarrow k = J)$
101	100	orbi2d	$⊢ φ \to ((k \in (1 \dots J - 1) \lor k = J - 1 + 1) \leftrightarrow (k \in (1 \dots J - 1) \lor k = J))$
102	94 99 101	3bitr3d	$⊢ φ \to (k \in (1 \dots J) \leftrightarrow (k \in (1 \dots J - 1) \lor k = J))$
103		orcom	$⊢ (k \in (1 \dots J - 1) \lor k = J) \leftrightarrow (k = J \lor k \in (1 \dots J - 1))$
104	102 103	bitrdi	$⊢ φ \to (k \in (1 \dots J) \leftrightarrow (k = J \lor k \in (1 \dots J - 1)))$
105	104	biimpd	$⊢ φ \to (k \in (1 \dots J) \to (k = J \lor k \in (1 \dots J - 1)))$
106		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)))$
107	105 106	sylibr	$⊢ φ \to ((k \in (1 \dots J) \land \neg k = J) \to k \in (1 \dots J - 1))$
108	90	nnzd	$⊢ φ \to J - 1 \in ℤ$
109		1z	$⊢ 1 \in ℤ$
110	108 109	jctil	$⊢ φ \to (1 \in ℤ \land J - 1 \in ℤ)$
111		elfzelz	$⊢ k \in (1 \dots J - 1) \to k \in ℤ$
112	111 109	jctir	$⊢ k \in (1 \dots J - 1) \to (k \in ℤ \land 1 \in ℤ)$
113		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))$
114	110 112 113	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))$
115	114	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)$
116	115	3anidm23	$⊢ (φ \land k \in (1 \dots J - 1)) \to k + 1 \in (1 + 1 \dots J - 1 + 1)$
117		1p1e2	$⊢ 1 + 1 = 2$
118	117	a1i	$⊢ φ \to 1 + 1 = 2$
119	118 97	oveq12d	$⊢ φ \to (1 + 1 \dots J - 1 + 1) = (2 \dots J)$
120	119	eleq2d	$⊢ φ \to (k + 1 \in (1 + 1 \dots J - 1 + 1) \leftrightarrow k + 1 \in (2 \dots J))$
121		2eluzge1	$⊢ 2 \in ℤ_{\geq 1}$
122		fzss1	$⊢ 2 \in ℤ_{\geq 1} \to (2 \dots J) \subseteq (1 \dots J)$
123	121 122	ax-mp	$⊢ (2 \dots J) \subseteq (1 \dots J)$
124	123	sseli	$⊢ k + 1 \in (2 \dots J) \to k + 1 \in (1 \dots J)$
125	120 124	syl6bi	$⊢ φ \to (k + 1 \in (1 + 1 \dots J - 1 + 1) \to k + 1 \in (1 \dots J))$
126	125	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))$
127	116 126	mpd	$⊢ (φ \land k \in (1 \dots J - 1)) \to k + 1 \in (1 \dots J)$
128	127	ex	$⊢ φ \to (k \in (1 \dots J - 1) \to k + 1 \in (1 \dots J))$
129	107 128	syld	$⊢ φ \to ((k \in (1 \dots J) \land \neg k = J) \to k + 1 \in (1 \dots J))$
130	58 129	sylan2d	$⊢ φ \to ((k \in (1 \dots J) \land F (C) (k) \leq 0) \to k + 1 \in (1 \dots J))$
131	130	imp	$⊢ (φ \land (k \in (1 \dots J) \land F (C) (k) \leq 0)) \to k + 1 \in (1 \dots J)$
132	131	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)$
133		fveq2	$⊢ i = k + 1 \to F (C) (i) = F (C) (k + 1)$
134	133	breq1d	$⊢ i = k + 1 \to (F (C) (i) \leq 0 \leftrightarrow F (C) (k + 1) \leq 0)$
135	134	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)$
136		breq1	$⊢ j = k + 1 \to (j \leq k \leftrightarrow k + 1 \leq k)$
137	136	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$
138	135 137	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$
139	138	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)$
140	139	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)$
141	29 132 140	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)$
142	28 141	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$
143		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$
144	132	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)$
145		simpll	$⊢ ((φ \land (k \in (1 \dots J) \land F (C) (k) \leq 0)) \land \neg k + 1 \in C) \to φ$
146	131	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)$
147	42	sseld	$⊢ 1 \in ℤ_{\geq 0} \to (k + 1 \in (1 \dots J) \to k + 1 \in (0 \dots J))$
148	41 146 147	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)$
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 F (C) (k) \leq 0)) \land \neg k + 1 \in C) \to F (C) (k + 1) \in ℝ$
155		0red	$⊢ ((φ \land (k \in (1 \dots J) \land F (C) (k) \leq 0)) \land \neg k + 1 \in C) \to 0 \in ℝ$
156		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$
157	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)$
158	157 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)$
159	130	imdistani	$⊢ (φ \land (k \in (1 \dots J) \land F (C) (k) \leq 0)) \to (φ \land k + 1 \in (1 \dots J))$
160	6	adantr	$⊢ (φ \land k + 1 \in (1 \dots J)) \to C \in O$
161		elfznn	$⊢ k + 1 \in (1 \dots J) \to k + 1 \in ℕ$
162	161	adantl	$⊢ (φ \land k + 1 \in (1 \dots J)) \to k + 1 \in ℕ$
163	1 2 3 4 5 160 162	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))$
164	163	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)$
165	164	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$
166	159 165	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$
167		elfzelz	$⊢ k \in (1 \dots J) \to k \in ℤ$
168	167	zcnd	$⊢ k \in (1 \dots J) \to k \in ℂ$
169		1cnd	$⊢ k \in (1 \dots J) \to 1 \in ℂ$
170	168 169	pncand	$⊢ k \in (1 \dots J) \to k + 1 - 1 = k$
171	170	fveq2d	$⊢ k \in (1 \dots J) \to F (C) (k + 1 - 1) = F (C) (k)$
172	171	oveq1d	$⊢ k \in (1 \dots J) \to F (C) (k + 1 - 1) - 1 = F (C) (k) - 1$
173	172	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)$
174	157 173	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)$
175	166 174	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$
176		0z	$⊢ 0 \in ℤ$
177		zlem1lt	$⊢ (F (C) (k) \in ℤ \land 0 \in ℤ) \to (F (C) (k) \leq 0 \leftrightarrow F (C) (k) - 1 < 0)$
178	49 176 177	sylancl	$⊢ (φ \land k \in (0 \dots J)) \to (F (C) (k) \leq 0 \leftrightarrow F (C) (k) - 1 < 0)$
179	178	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)$
180		breq1	$⊢ F (C) (k + 1) = F (C) (k) - 1 \to (F (C) (k + 1) < 0 \leftrightarrow F (C) (k) - 1 < 0)$
181	180	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)$
182	179 181	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)$
183	145 158 175 182	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)$
184	156 183	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$
185	154 155 184	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$
186	185	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$
187	143 144 186 138	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$
188	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$
189	187 188	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$
190	163	simprd	$⊢ (φ \land k + 1 \in (1 \dots J)) \to (k + 1 \in C \to F (C) (k + 1) = F (C) (k + 1 - 1) + 1)$
191	190	imp	$⊢ ((φ \land k + 1 \in (1 \dots J)) \land k + 1 \in C) \to F (C) (k + 1) = F (C) (k + 1 - 1) + 1$
192	159 191	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$
193	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)$
194	171	oveq1d	$⊢ k \in (1 \dots J) \to F (C) (k + 1 - 1) + 1 = F (C) (k) + 1$
195	194	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)$
196	193 195	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)$
197	192 196	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$
198	197	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$
199	189 198	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$
200		breq1	$⊢ F (C) (k + 1) = F (C) (k) + 1 \to (F (C) (k + 1) \leq 0 \leftrightarrow F (C) (k) + 1 \leq 0)$
201	200	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)$
202	199 201	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)$
203	142 202	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$
204	15 44	syl	$⊢ (φ \land (k \in (1 \dots J) \land F (C) (k) \leq 0)) \to k \in (0 \dots J)$
205	204 49	syldan	$⊢ (φ \land (k \in (1 \dots J) \land F (C) (k) \leq 0)) \to F (C) (k) \in ℤ$
206	205	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 ℤ$
207		zleltp1	$⊢ (0 \in ℤ \land F (C) (k) \in ℤ) \to (0 \leq F (C) (k) \leftrightarrow 0 < F (C) (k) + 1)$
208	176 207	mpan	$⊢ F (C) (k) \in ℤ \to (0 \leq F (C) (k) \leftrightarrow 0 < F (C) (k) + 1)$
209		0red	$⊢ F (C) (k) \in ℤ \to 0 \in ℝ$
210		zre	$⊢ F (C) (k) \in ℤ \to F (C) (k) \in ℝ$
211		1red	$⊢ F (C) (k) \in ℤ \to 1 \in ℝ$
212	210 211	readdcld	$⊢ F (C) (k) \in ℤ \to F (C) (k) + 1 \in ℝ$
213	209 212	ltnled	$⊢ F (C) (k) \in ℤ \to (0 < F (C) (k) + 1 \leftrightarrow \neg F (C) (k) + 1 \leq 0)$
214	208 213	bitrd	$⊢ F (C) (k) \in ℤ \to (0 \leq F (C) (k) \leftrightarrow \neg F (C) (k) + 1 \leq 0)$
215	206 214	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)$
216	203 215	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)$
217	206	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 ℝ$
218		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 ℝ$
219	217 218	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)))$
220	14 216 219	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$
221	13 220	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$
222		ssrab2	$⊢ \{i \in (1 \dots J) \| F (C) (i) \leq 0\} \subseteq (1 \dots J)$
223	222 21	sstri	$⊢ \{i \in (1 \dots J) \| F (C) (i) \leq 0\} \subseteq ℝ$
224	223	a1i	$⊢ φ \to \{i \in (1 \dots J) \| F (C) (i) \leq 0\} \subseteq ℝ$
225		fzfi	$⊢ (1 \dots J) \in Fin$
226		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$
227	225 222 226	mp2an	$⊢ \{i \in (1 \dots J) \| F (C) (i) \leq 0\} \in Fin$
228	227	a1i	$⊢ φ \to \{i \in (1 \dots J) \| F (C) (i) \leq 0\} \in Fin$
229		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$
230	8 229	sylibr	$⊢ φ \to \{i \in (1 \dots J) \| F (C) (i) \leq 0\} \neq \emptyset$
231		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$
232	224 228 230 231	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$
233	221 232	reximddv	$⊢ φ \to \exists k \in \{i \in (1 \dots J) \| F (C) (i) \leq 0\} F (C) (k) = 0$
234		elrabi	$⊢ k \in \{i \in (1 \dots J) \| F (C) (i) \leq 0\} \to k \in (1 \dots J)$
235	234	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)$
236	235	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$
237	233 236	syl	$⊢ φ \to \exists k \in (1 \dots J) F (C) (k) = 0$

Metamath Proof Explorer

Theorem ballotlemfc0

Proof