ballotlemfc0 - Mathbox for Thierry Arnoux

	Mathbox for Thierry Arnoux		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > Mathboxes > ballotlemfc0		Structured version Visualization version GIF version

Theorem ballotlemfc0 29881

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

**Hypotheses**
Ref	Expression
ballotth.m	⊢ 𝑀 ∈ ℕ
ballotth.n	⊢ 𝑁 ∈ ℕ
ballotth.o	⊢ 𝑂 = {𝑐 ∈ 𝒫 (1...(𝑀 + 𝑁)) ∣ (#‘𝑐) = 𝑀}
ballotth.p	⊢ 𝑃 = (𝑥 ∈ 𝒫 𝑂 ↦ ((#‘𝑥) / (#‘𝑂)))
ballotth.f	⊢ 𝐹 = (𝑐 ∈ 𝑂 ↦ (𝑖 ∈ ℤ ↦ ((#‘((1...𝑖) ∩ 𝑐)) − (#‘((1...𝑖) ∖ 𝑐)))))
ballotlemfp1.c	⊢ (𝜑 → 𝐶 ∈ 𝑂)
ballotlemfp1.j	⊢ (𝜑 → 𝐽 ∈ ℕ)
ballotlemfc0.3	⊢ (𝜑 → ∃𝑖 ∈ (1...𝐽)((𝐹‘𝐶)‘𝑖) ≤ 0)
ballotlemfc0.4	⊢ (𝜑 → 0 < ((𝐹‘𝐶)‘𝐽))

**Assertion**
Ref	Expression
ballotlemfc0	⊢ (𝜑 → ∃𝑘 ∈ (1...𝐽)((𝐹‘𝐶)‘𝑘) = 0)

Distinct variable groups: 𝑀,𝑐 𝑁,𝑐 𝑂,𝑐 𝑖,𝑀 𝑖,𝑁 𝑖,𝑂 𝑘,𝑀 𝑘,𝑁 𝑘,𝑂 𝑖,𝑐,𝐹 𝑘,𝐹 𝐶,𝑖 𝑖,𝐽 𝜑,𝑖,𝑘 𝑘,𝐽 𝐶,𝑘 𝜑,𝑘 Allowed substitution hints: 𝜑(𝑥,𝑐) 𝐶(𝑥,𝑐) 𝑃(𝑥,𝑖,𝑘,𝑐) 𝐹(𝑥) 𝐽(𝑥,𝑐) 𝑀(𝑥) 𝑁(𝑥) 𝑂(𝑥)

Proof of Theorem ballotlemfc0 Dummy variable 𝑗 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		fveq2 6103	. . . . . . 7 ⊢ (𝑖 = 𝑘 → ((𝐹‘𝐶)‘𝑖) = ((𝐹‘𝐶)‘𝑘))
2	1	breq1d 4593	. . . . . 6 ⊢ (𝑖 = 𝑘 → (((𝐹‘𝐶)‘𝑖) ≤ 0 ↔ ((𝐹‘𝐶)‘𝑘) ≤ 0))
3	2	elrab 3331	. . . . 5 ⊢ (𝑘 ∈ {𝑖 ∈ (1...𝐽) ∣ ((𝐹‘𝐶)‘𝑖) ≤ 0} ↔ (𝑘 ∈ (1...𝐽) ∧ ((𝐹‘𝐶)‘𝑘) ≤ 0))
4	3	anbi1i 727	. . . 4 ⊢ ((𝑘 ∈ {𝑖 ∈ (1...𝐽) ∣ ((𝐹‘𝐶)‘𝑖) ≤ 0} ∧ ∀𝑗 ∈ {𝑖 ∈ (1...𝐽) ∣ ((𝐹‘𝐶)‘𝑖) ≤ 0}𝑗 ≤ 𝑘) ↔ ((𝑘 ∈ (1...𝐽) ∧ ((𝐹‘𝐶)‘𝑘) ≤ 0) ∧ ∀𝑗 ∈ {𝑖 ∈ (1...𝐽) ∣ ((𝐹‘𝐶)‘𝑖) ≤ 0}𝑗 ≤ 𝑘))
5		simprlr 799	. . . . 5 ⊢ ((𝜑 ∧ ((𝑘 ∈ (1...𝐽) ∧ ((𝐹‘𝐶)‘𝑘) ≤ 0) ∧ ∀𝑗 ∈ {𝑖 ∈ (1...𝐽) ∣ ((𝐹‘𝐶)‘𝑖) ≤ 0}𝑗 ≤ 𝑘)) → ((𝐹‘𝐶)‘𝑘) ≤ 0)
6		simprl 790	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑘 ∈ (1...𝐽) ∧ ((𝐹‘𝐶)‘𝑘) ≤ 0)) → 𝑘 ∈ (1...𝐽))
7	6	adantrr 749	. . . . . . . . 9 ⊢ ((𝜑 ∧ ((𝑘 ∈ (1...𝐽) ∧ ((𝐹‘𝐶)‘𝑘) ≤ 0) ∧ ∀𝑗 ∈ {𝑖 ∈ (1...𝐽) ∣ ((𝐹‘𝐶)‘𝑖) ≤ 0}𝑗 ≤ 𝑘)) → 𝑘 ∈ (1...𝐽))
8		fzssuz 12253	. . . . . . . . . . . . . 14 ⊢ (1...𝐽) ⊆ (ℤ_≥‘1)
9		uzssz 11583	. . . . . . . . . . . . . 14 ⊢ (ℤ_≥‘1) ⊆ ℤ
10	8, 9	sstri 3577	. . . . . . . . . . . . 13 ⊢ (1...𝐽) ⊆ ℤ
11		zssre 11261	. . . . . . . . . . . . 13 ⊢ ℤ ⊆ ℝ
12	10, 11	sstri 3577	. . . . . . . . . . . 12 ⊢ (1...𝐽) ⊆ ℝ
13	12	sseli 3564	. . . . . . . . . . 11 ⊢ (𝑘 ∈ (1...𝐽) → 𝑘 ∈ ℝ)
14	13	ltp1d 10833	. . . . . . . . . 10 ⊢ (𝑘 ∈ (1...𝐽) → 𝑘 < (𝑘 + 1))
15		1red 9934	. . . . . . . . . . . 12 ⊢ (𝑘 ∈ (1...𝐽) → 1 ∈ ℝ)
16	13, 15	readdcld 9948	. . . . . . . . . . 11 ⊢ (𝑘 ∈ (1...𝐽) → (𝑘 + 1) ∈ ℝ)
17	13, 16	ltnled 10063	. . . . . . . . . 10 ⊢ (𝑘 ∈ (1...𝐽) → (𝑘 < (𝑘 + 1) ↔ ¬ (𝑘 + 1) ≤ 𝑘))
18	14, 17	mpbid 221	. . . . . . . . 9 ⊢ (𝑘 ∈ (1...𝐽) → ¬ (𝑘 + 1) ≤ 𝑘)
19	7, 18	syl 17	. . . . . . . 8 ⊢ ((𝜑 ∧ ((𝑘 ∈ (1...𝐽) ∧ ((𝐹‘𝐶)‘𝑘) ≤ 0) ∧ ∀𝑗 ∈ {𝑖 ∈ (1...𝐽) ∣ ((𝐹‘𝐶)‘𝑖) ≤ 0}𝑗 ≤ 𝑘)) → ¬ (𝑘 + 1) ≤ 𝑘)
20		simprr 792	. . . . . . . . 9 ⊢ ((𝜑 ∧ ((𝑘 ∈ (1...𝐽) ∧ ((𝐹‘𝐶)‘𝑘) ≤ 0) ∧ ∀𝑗 ∈ {𝑖 ∈ (1...𝐽) ∣ ((𝐹‘𝐶)‘𝑖) ≤ 0}𝑗 ≤ 𝑘)) → ∀𝑗 ∈ {𝑖 ∈ (1...𝐽) ∣ ((𝐹‘𝐶)‘𝑖) ≤ 0}𝑗 ≤ 𝑘)
21		ballotlemfc0.4	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → 0 < ((𝐹‘𝐶)‘𝐽))
22	21	adantr 480	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑘 = 𝐽) → 0 < ((𝐹‘𝐶)‘𝐽))
23		simpr 476	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑘 = 𝐽) → 𝑘 = 𝐽)
24	23	fveq2d 6107	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑘 = 𝐽) → ((𝐹‘𝐶)‘𝑘) = ((𝐹‘𝐶)‘𝐽))
25	24	breq2d 4595	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑘 = 𝐽) → (0 < ((𝐹‘𝐶)‘𝑘) ↔ 0 < ((𝐹‘𝐶)‘𝐽)))
26		ballotlemfp1.j	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜑 → 𝐽 ∈ ℕ)
27		elnnuz 11600	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝐽 ∈ ℕ ↔ 𝐽 ∈ (ℤ_≥‘1))
28	26, 27	sylib 207	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → 𝐽 ∈ (ℤ_≥‘1))
29		eluzfz2 12220	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝐽 ∈ (ℤ_≥‘1) → 𝐽 ∈ (1...𝐽))
30	28, 29	syl 17	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → 𝐽 ∈ (1...𝐽))
31		eleq1 2676	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑘 = 𝐽 → (𝑘 ∈ (1...𝐽) ↔ 𝐽 ∈ (1...𝐽)))
32	30, 31	syl5ibrcom 236	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → (𝑘 = 𝐽 → 𝑘 ∈ (1...𝐽)))
33	32	anc2li 578	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (𝑘 = 𝐽 → (𝜑 ∧ 𝑘 ∈ (1...𝐽))))
34		1eluzge0 11608	. . . . . . . . . . . . . . . . . . . 20 ⊢ 1 ∈ (ℤ_≥‘0)
35		fzss1 12251	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (1 ∈ (ℤ_≥‘0) → (1...𝐽) ⊆ (0...𝐽))
36	35	sseld 3567	. . . . . . . . . . . . . . . . . . . 20 ⊢ (1 ∈ (ℤ_≥‘0) → (𝑘 ∈ (1...𝐽) → 𝑘 ∈ (0...𝐽)))
37	34, 36	ax-mp 5	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑘 ∈ (1...𝐽) → 𝑘 ∈ (0...𝐽))
38		0red 9920	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝐽)) → 0 ∈ ℝ)
39		ballotth.m	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ 𝑀 ∈ ℕ
40		ballotth.n	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ 𝑁 ∈ ℕ
41		ballotth.o	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ 𝑂 = {𝑐 ∈ 𝒫 (1...(𝑀 + 𝑁)) ∣ (#‘𝑐) = 𝑀}
42		ballotth.p	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ 𝑃 = (𝑥 ∈ 𝒫 𝑂 ↦ ((#‘𝑥) / (#‘𝑂)))
43		ballotth.f	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ 𝐹 = (𝑐 ∈ 𝑂 ↦ (𝑖 ∈ ℤ ↦ ((#‘((1...𝑖) ∩ 𝑐)) − (#‘((1...𝑖) ∖ 𝑐)))))
44		ballotlemfp1.c	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝜑 → 𝐶 ∈ 𝑂)
45	44	adantr 480	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝐽)) → 𝐶 ∈ 𝑂)
46		elfzelz 12213	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑘 ∈ (0...𝐽) → 𝑘 ∈ ℤ)
47	46	adantl 481	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝐽)) → 𝑘 ∈ ℤ)
48	39, 40, 41, 42, 43, 45, 47	ballotlemfelz 29879	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝐽)) → ((𝐹‘𝐶)‘𝑘) ∈ ℤ)
49	48	zred 11358	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝐽)) → ((𝐹‘𝐶)‘𝑘) ∈ ℝ)
50	38, 49	ltnled 10063	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝐽)) → (0 < ((𝐹‘𝐶)‘𝑘) ↔ ¬ ((𝐹‘𝐶)‘𝑘) ≤ 0))
51	37, 50	sylan2 490	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑘 ∈ (1...𝐽)) → (0 < ((𝐹‘𝐶)‘𝑘) ↔ ¬ ((𝐹‘𝐶)‘𝑘) ≤ 0))
52	33, 51	syl6 34	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (𝑘 = 𝐽 → (0 < ((𝐹‘𝐶)‘𝑘) ↔ ¬ ((𝐹‘𝐶)‘𝑘) ≤ 0)))
53	52	imp 444	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑘 = 𝐽) → (0 < ((𝐹‘𝐶)‘𝑘) ↔ ¬ ((𝐹‘𝐶)‘𝑘) ≤ 0))
54	25, 53	bitr3d 269	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑘 = 𝐽) → (0 < ((𝐹‘𝐶)‘𝐽) ↔ ¬ ((𝐹‘𝐶)‘𝑘) ≤ 0))
55	22, 54	mpbid 221	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑘 = 𝐽) → ¬ ((𝐹‘𝐶)‘𝑘) ≤ 0)
56	55	ex 449	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝑘 = 𝐽 → ¬ ((𝐹‘𝐶)‘𝑘) ≤ 0))
57	56	con2d 128	. . . . . . . . . . . 12 ⊢ (𝜑 → (((𝐹‘𝐶)‘𝑘) ≤ 0 → ¬ 𝑘 = 𝐽))
58		nn1m1nn 10917	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝐽 ∈ ℕ → (𝐽 = 1 ∨ (𝐽 − 1) ∈ ℕ))
59	26, 58	syl 17	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → (𝐽 = 1 ∨ (𝐽 − 1) ∈ ℕ))
60		ballotlemfc0.3	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝜑 → ∃𝑖 ∈ (1...𝐽)((𝐹‘𝐶)‘𝑖) ≤ 0)
61	60	adantr 480	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝜑 ∧ 𝐽 = 1) → ∃𝑖 ∈ (1...𝐽)((𝐹‘𝐶)‘𝑖) ≤ 0)
62		oveq1 6556	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝐽 = 1 → (𝐽...𝐽) = (1...𝐽))
63	62	adantl 481	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝜑 ∧ 𝐽 = 1) → (𝐽...𝐽) = (1...𝐽))
64	26	nnzd 11357	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝜑 → 𝐽 ∈ ℤ)
65		fzsn 12254	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝐽 ∈ ℤ → (𝐽...𝐽) = {𝐽})
66	64, 65	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝜑 → (𝐽...𝐽) = {𝐽})
67	66	adantr 480	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝜑 ∧ 𝐽 = 1) → (𝐽...𝐽) = {𝐽})
68	63, 67	eqtr3d 2646	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝜑 ∧ 𝐽 = 1) → (1...𝐽) = {𝐽})
69	68	rexeqdv 3122	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝜑 ∧ 𝐽 = 1) → (∃𝑖 ∈ (1...𝐽)((𝐹‘𝐶)‘𝑖) ≤ 0 ↔ ∃𝑖 ∈ {𝐽} ((𝐹‘𝐶)‘𝑖) ≤ 0))
70	61, 69	mpbid 221	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝜑 ∧ 𝐽 = 1) → ∃𝑖 ∈ {𝐽} ((𝐹‘𝐶)‘𝑖) ≤ 0)
71		fveq2 6103	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝑖 = 𝐽 → ((𝐹‘𝐶)‘𝑖) = ((𝐹‘𝐶)‘𝐽))
72	71	breq1d 4593	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑖 = 𝐽 → (((𝐹‘𝐶)‘𝑖) ≤ 0 ↔ ((𝐹‘𝐶)‘𝐽) ≤ 0))
73	72	rexsng 4166	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝐽 ∈ ℕ → (∃𝑖 ∈ {𝐽} ((𝐹‘𝐶)‘𝑖) ≤ 0 ↔ ((𝐹‘𝐶)‘𝐽) ≤ 0))
74	26, 73	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝜑 → (∃𝑖 ∈ {𝐽} ((𝐹‘𝐶)‘𝑖) ≤ 0 ↔ ((𝐹‘𝐶)‘𝐽) ≤ 0))
75	74	adantr 480	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝜑 ∧ 𝐽 = 1) → (∃𝑖 ∈ {𝐽} ((𝐹‘𝐶)‘𝑖) ≤ 0 ↔ ((𝐹‘𝐶)‘𝐽) ≤ 0))
76	70, 75	mpbid 221	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ 𝐽 = 1) → ((𝐹‘𝐶)‘𝐽) ≤ 0)
77	21	adantr 480	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝜑 ∧ 𝐽 = 1) → 0 < ((𝐹‘𝐶)‘𝐽))
78		0red 9920	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝜑 → 0 ∈ ℝ)
79	39, 40, 41, 42, 43, 44, 64	ballotlemfelz 29879	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝜑 → ((𝐹‘𝐶)‘𝐽) ∈ ℤ)
80	79	zred 11358	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝜑 → ((𝐹‘𝐶)‘𝐽) ∈ ℝ)
81	78, 80	ltnled 10063	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝜑 → (0 < ((𝐹‘𝐶)‘𝐽) ↔ ¬ ((𝐹‘𝐶)‘𝐽) ≤ 0))
82	81	adantr 480	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝜑 ∧ 𝐽 = 1) → (0 < ((𝐹‘𝐶)‘𝐽) ↔ ¬ ((𝐹‘𝐶)‘𝐽) ≤ 0))
83	77, 82	mpbid 221	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ 𝐽 = 1) → ¬ ((𝐹‘𝐶)‘𝐽) ≤ 0)
84	76, 83	pm2.65da 598	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜑 → ¬ 𝐽 = 1)
85		biortn 420	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (¬ 𝐽 = 1 → ((𝐽 − 1) ∈ ℕ ↔ (¬ ¬ 𝐽 = 1 ∨ (𝐽 − 1) ∈ ℕ)))
86	84, 85	syl 17	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → ((𝐽 − 1) ∈ ℕ ↔ (¬ ¬ 𝐽 = 1 ∨ (𝐽 − 1) ∈ ℕ)))
87		notnotb 303	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝐽 = 1 ↔ ¬ ¬ 𝐽 = 1)
88	87	orbi1i 541	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝐽 = 1 ∨ (𝐽 − 1) ∈ ℕ) ↔ (¬ ¬ 𝐽 = 1 ∨ (𝐽 − 1) ∈ ℕ))
89	86, 88	syl6bbr 277	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → ((𝐽 − 1) ∈ ℕ ↔ (𝐽 = 1 ∨ (𝐽 − 1) ∈ ℕ)))
90	59, 89	mpbird 246	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → (𝐽 − 1) ∈ ℕ)
91		elnnuz 11600	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝐽 − 1) ∈ ℕ ↔ (𝐽 − 1) ∈ (ℤ_≥‘1))
92	90, 91	sylib 207	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (𝐽 − 1) ∈ (ℤ_≥‘1))
93		elfzp1 12261	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝐽 − 1) ∈ (ℤ_≥‘1) → (𝑘 ∈ (1...((𝐽 − 1) + 1)) ↔ (𝑘 ∈ (1...(𝐽 − 1)) ∨ 𝑘 = ((𝐽 − 1) + 1))))
94	92, 93	syl 17	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (𝑘 ∈ (1...((𝐽 − 1) + 1)) ↔ (𝑘 ∈ (1...(𝐽 − 1)) ∨ 𝑘 = ((𝐽 − 1) + 1))))
95	26	nncnd 10913	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → 𝐽 ∈ ℂ)
96		1cnd 9935	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → 1 ∈ ℂ)
97	95, 96	npcand 10275	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → ((𝐽 − 1) + 1) = 𝐽)
98	97	oveq2d 6565	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (1...((𝐽 − 1) + 1)) = (1...𝐽))
99	98	eleq2d 2673	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (𝑘 ∈ (1...((𝐽 − 1) + 1)) ↔ 𝑘 ∈ (1...𝐽)))
100	97	eqeq2d 2620	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (𝑘 = ((𝐽 − 1) + 1) ↔ 𝑘 = 𝐽))
101	100	orbi2d 734	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → ((𝑘 ∈ (1...(𝐽 − 1)) ∨ 𝑘 = ((𝐽 − 1) + 1)) ↔ (𝑘 ∈ (1...(𝐽 − 1)) ∨ 𝑘 = 𝐽)))
102	94, 99, 101	3bitr3d 297	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (𝑘 ∈ (1...𝐽) ↔ (𝑘 ∈ (1...(𝐽 − 1)) ∨ 𝑘 = 𝐽)))
103		orcom 401	. . . . . . . . . . . . . . . 16 ⊢ ((𝑘 ∈ (1...(𝐽 − 1)) ∨ 𝑘 = 𝐽) ↔ (𝑘 = 𝐽 ∨ 𝑘 ∈ (1...(𝐽 − 1))))
104	102, 103	syl6bb 275	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝑘 ∈ (1...𝐽) ↔ (𝑘 = 𝐽 ∨ 𝑘 ∈ (1...(𝐽 − 1)))))
105	104	biimpd 218	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝑘 ∈ (1...𝐽) → (𝑘 = 𝐽 ∨ 𝑘 ∈ (1...(𝐽 − 1)))))
106		pm5.6 949	. . . . . . . . . . . . . 14 ⊢ (((𝑘 ∈ (1...𝐽) ∧ ¬ 𝑘 = 𝐽) → 𝑘 ∈ (1...(𝐽 − 1))) ↔ (𝑘 ∈ (1...𝐽) → (𝑘 = 𝐽 ∨ 𝑘 ∈ (1...(𝐽 − 1)))))
107	105, 106	sylibr 223	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((𝑘 ∈ (1...𝐽) ∧ ¬ 𝑘 = 𝐽) → 𝑘 ∈ (1...(𝐽 − 1))))
108	90	nnzd 11357	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → (𝐽 − 1) ∈ ℤ)
109		1z 11284	. . . . . . . . . . . . . . . . . . 19 ⊢ 1 ∈ ℤ
110	108, 109	jctil 558	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (1 ∈ ℤ ∧ (𝐽 − 1) ∈ ℤ))
111		elfzelz 12213	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑘 ∈ (1...(𝐽 − 1)) → 𝑘 ∈ ℤ)
112	111, 109	jctir 559	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑘 ∈ (1...(𝐽 − 1)) → (𝑘 ∈ ℤ ∧ 1 ∈ ℤ))
113		fzaddel 12246	. . . . . . . . . . . . . . . . . 18 ⊢ (((1 ∈ ℤ ∧ (𝐽 − 1) ∈ ℤ) ∧ (𝑘 ∈ ℤ ∧ 1 ∈ ℤ)) → (𝑘 ∈ (1...(𝐽 − 1)) ↔ (𝑘 + 1) ∈ ((1 + 1)...((𝐽 − 1) + 1))))
114	110, 112, 113	syl2an 493	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑘 ∈ (1...(𝐽 − 1))) → (𝑘 ∈ (1...(𝐽 − 1)) ↔ (𝑘 + 1) ∈ ((1 + 1)...((𝐽 − 1) + 1))))
115	114	biimp3a 1424	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑘 ∈ (1...(𝐽 − 1)) ∧ 𝑘 ∈ (1...(𝐽 − 1))) → (𝑘 + 1) ∈ ((1 + 1)...((𝐽 − 1) + 1)))
116	115	3anidm23 1377	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑘 ∈ (1...(𝐽 − 1))) → (𝑘 + 1) ∈ ((1 + 1)...((𝐽 − 1) + 1)))
117		1p1e2 11011	. . . . . . . . . . . . . . . . . . . 20 ⊢ (1 + 1) = 2
118	117	a1i 11	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → (1 + 1) = 2)
119	118, 97	oveq12d 6567	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → ((1 + 1)...((𝐽 − 1) + 1)) = (2...𝐽))
120	119	eleq2d 2673	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → ((𝑘 + 1) ∈ ((1 + 1)...((𝐽 − 1) + 1)) ↔ (𝑘 + 1) ∈ (2...𝐽)))
121		2eluzge1 11610	. . . . . . . . . . . . . . . . . . 19 ⊢ 2 ∈ (ℤ_≥‘1)
122		fzss1 12251	. . . . . . . . . . . . . . . . . . 19 ⊢ (2 ∈ (ℤ_≥‘1) → (2...𝐽) ⊆ (1...𝐽))
123	121, 122	ax-mp 5	. . . . . . . . . . . . . . . . . 18 ⊢ (2...𝐽) ⊆ (1...𝐽)
124	123	sseli 3564	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑘 + 1) ∈ (2...𝐽) → (𝑘 + 1) ∈ (1...𝐽))
125	120, 124	syl6bi 242	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ((𝑘 + 1) ∈ ((1 + 1)...((𝐽 − 1) + 1)) → (𝑘 + 1) ∈ (1...𝐽)))
126	125	adantr 480	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑘 ∈ (1...(𝐽 − 1))) → ((𝑘 + 1) ∈ ((1 + 1)...((𝐽 − 1) + 1)) → (𝑘 + 1) ∈ (1...𝐽)))
127	116, 126	mpd 15	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑘 ∈ (1...(𝐽 − 1))) → (𝑘 + 1) ∈ (1...𝐽))
128	127	ex 449	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝑘 ∈ (1...(𝐽 − 1)) → (𝑘 + 1) ∈ (1...𝐽)))
129	107, 128	syld 46	. . . . . . . . . . . 12 ⊢ (𝜑 → ((𝑘 ∈ (1...𝐽) ∧ ¬ 𝑘 = 𝐽) → (𝑘 + 1) ∈ (1...𝐽)))
130	57, 129	sylan2d 498	. . . . . . . . . . 11 ⊢ (𝜑 → ((𝑘 ∈ (1...𝐽) ∧ ((𝐹‘𝐶)‘𝑘) ≤ 0) → (𝑘 + 1) ∈ (1...𝐽)))
131	130	imp 444	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑘 ∈ (1...𝐽) ∧ ((𝐹‘𝐶)‘𝑘) ≤ 0)) → (𝑘 + 1) ∈ (1...𝐽))
132	131	adantrr 749	. . . . . . . . 9 ⊢ ((𝜑 ∧ ((𝑘 ∈ (1...𝐽) ∧ ((𝐹‘𝐶)‘𝑘) ≤ 0) ∧ ∀𝑗 ∈ {𝑖 ∈ (1...𝐽) ∣ ((𝐹‘𝐶)‘𝑖) ≤ 0}𝑗 ≤ 𝑘)) → (𝑘 + 1) ∈ (1...𝐽))
133		fveq2 6103	. . . . . . . . . . . . . 14 ⊢ (𝑖 = (𝑘 + 1) → ((𝐹‘𝐶)‘𝑖) = ((𝐹‘𝐶)‘(𝑘 + 1)))
134	133	breq1d 4593	. . . . . . . . . . . . 13 ⊢ (𝑖 = (𝑘 + 1) → (((𝐹‘𝐶)‘𝑖) ≤ 0 ↔ ((𝐹‘𝐶)‘(𝑘 + 1)) ≤ 0))
135	134	elrab 3331	. . . . . . . . . . . 12 ⊢ ((𝑘 + 1) ∈ {𝑖 ∈ (1...𝐽) ∣ ((𝐹‘𝐶)‘𝑖) ≤ 0} ↔ ((𝑘 + 1) ∈ (1...𝐽) ∧ ((𝐹‘𝐶)‘(𝑘 + 1)) ≤ 0))
136		breq1 4586	. . . . . . . . . . . . 13 ⊢ (𝑗 = (𝑘 + 1) → (𝑗 ≤ 𝑘 ↔ (𝑘 + 1) ≤ 𝑘))
137	136	rspccva 3281	. . . . . . . . . . . 12 ⊢ ((∀𝑗 ∈ {𝑖 ∈ (1...𝐽) ∣ ((𝐹‘𝐶)‘𝑖) ≤ 0}𝑗 ≤ 𝑘 ∧ (𝑘 + 1) ∈ {𝑖 ∈ (1...𝐽) ∣ ((𝐹‘𝐶)‘𝑖) ≤ 0}) → (𝑘 + 1) ≤ 𝑘)
138	135, 137	sylan2br 492	. . . . . . . . . . 11 ⊢ ((∀𝑗 ∈ {𝑖 ∈ (1...𝐽) ∣ ((𝐹‘𝐶)‘𝑖) ≤ 0}𝑗 ≤ 𝑘 ∧ ((𝑘 + 1) ∈ (1...𝐽) ∧ ((𝐹‘𝐶)‘(𝑘 + 1)) ≤ 0)) → (𝑘 + 1) ≤ 𝑘)
139	138	expr 641	. . . . . . . . . 10 ⊢ ((∀𝑗 ∈ {𝑖 ∈ (1...𝐽) ∣ ((𝐹‘𝐶)‘𝑖) ≤ 0}𝑗 ≤ 𝑘 ∧ (𝑘 + 1) ∈ (1...𝐽)) → (((𝐹‘𝐶)‘(𝑘 + 1)) ≤ 0 → (𝑘 + 1) ≤ 𝑘))
140	139	con3d 147	. . . . . . . . 9 ⊢ ((∀𝑗 ∈ {𝑖 ∈ (1...𝐽) ∣ ((𝐹‘𝐶)‘𝑖) ≤ 0}𝑗 ≤ 𝑘 ∧ (𝑘 + 1) ∈ (1...𝐽)) → (¬ (𝑘 + 1) ≤ 𝑘 → ¬ ((𝐹‘𝐶)‘(𝑘 + 1)) ≤ 0))
141	20, 132, 140	syl2anc 691	. . . . . . . 8 ⊢ ((𝜑 ∧ ((𝑘 ∈ (1...𝐽) ∧ ((𝐹‘𝐶)‘𝑘) ≤ 0) ∧ ∀𝑗 ∈ {𝑖 ∈ (1...𝐽) ∣ ((𝐹‘𝐶)‘𝑖) ≤ 0}𝑗 ≤ 𝑘)) → (¬ (𝑘 + 1) ≤ 𝑘 → ¬ ((𝐹‘𝐶)‘(𝑘 + 1)) ≤ 0))
142	19, 141	mpd 15	. . . . . . 7 ⊢ ((𝜑 ∧ ((𝑘 ∈ (1...𝐽) ∧ ((𝐹‘𝐶)‘𝑘) ≤ 0) ∧ ∀𝑗 ∈ {𝑖 ∈ (1...𝐽) ∣ ((𝐹‘𝐶)‘𝑖) ≤ 0}𝑗 ≤ 𝑘)) → ¬ ((𝐹‘𝐶)‘(𝑘 + 1)) ≤ 0)
143		simplrr 797	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ ((𝑘 ∈ (1...𝐽) ∧ ((𝐹‘𝐶)‘𝑘) ≤ 0) ∧ ∀𝑗 ∈ {𝑖 ∈ (1...𝐽) ∣ ((𝐹‘𝐶)‘𝑖) ≤ 0}𝑗 ≤ 𝑘)) ∧ ¬ (𝑘 + 1) ∈ 𝐶) → ∀𝑗 ∈ {𝑖 ∈ (1...𝐽) ∣ ((𝐹‘𝐶)‘𝑖) ≤ 0}𝑗 ≤ 𝑘)
144	132	adantr 480	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ ((𝑘 ∈ (1...𝐽) ∧ ((𝐹‘𝐶)‘𝑘) ≤ 0) ∧ ∀𝑗 ∈ {𝑖 ∈ (1...𝐽) ∣ ((𝐹‘𝐶)‘𝑖) ≤ 0}𝑗 ≤ 𝑘)) ∧ ¬ (𝑘 + 1) ∈ 𝐶) → (𝑘 + 1) ∈ (1...𝐽))
145		simpll 786	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (𝑘 ∈ (1...𝐽) ∧ ((𝐹‘𝐶)‘𝑘) ≤ 0)) ∧ ¬ (𝑘 + 1) ∈ 𝐶) → 𝜑)
146	131	adantr 480	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ (𝑘 ∈ (1...𝐽) ∧ ((𝐹‘𝐶)‘𝑘) ≤ 0)) ∧ ¬ (𝑘 + 1) ∈ 𝐶) → (𝑘 + 1) ∈ (1...𝐽))
147	35	sseld 3567	. . . . . . . . . . . . . . 15 ⊢ (1 ∈ (ℤ_≥‘0) → ((𝑘 + 1) ∈ (1...𝐽) → (𝑘 + 1) ∈ (0...𝐽)))
148	34, 146, 147	mpsyl 66	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (𝑘 ∈ (1...𝐽) ∧ ((𝐹‘𝐶)‘𝑘) ≤ 0)) ∧ ¬ (𝑘 + 1) ∈ 𝐶) → (𝑘 + 1) ∈ (0...𝐽))
149	44	adantr 480	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ (𝑘 + 1) ∈ (0...𝐽)) → 𝐶 ∈ 𝑂)
150		elfzelz 12213	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑘 + 1) ∈ (0...𝐽) → (𝑘 + 1) ∈ ℤ)
151	150	adantl 481	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ (𝑘 + 1) ∈ (0...𝐽)) → (𝑘 + 1) ∈ ℤ)
152	39, 40, 41, 42, 43, 149, 151	ballotlemfelz 29879	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ (𝑘 + 1) ∈ (0...𝐽)) → ((𝐹‘𝐶)‘(𝑘 + 1)) ∈ ℤ)
153	152	zred 11358	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑘 + 1) ∈ (0...𝐽)) → ((𝐹‘𝐶)‘(𝑘 + 1)) ∈ ℝ)
154	145, 148, 153	syl2anc 691	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑘 ∈ (1...𝐽) ∧ ((𝐹‘𝐶)‘𝑘) ≤ 0)) ∧ ¬ (𝑘 + 1) ∈ 𝐶) → ((𝐹‘𝐶)‘(𝑘 + 1)) ∈ ℝ)
155		0red 9920	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑘 ∈ (1...𝐽) ∧ ((𝐹‘𝐶)‘𝑘) ≤ 0)) ∧ ¬ (𝑘 + 1) ∈ 𝐶) → 0 ∈ ℝ)
156		simplrr 797	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (𝑘 ∈ (1...𝐽) ∧ ((𝐹‘𝐶)‘𝑘) ≤ 0)) ∧ ¬ (𝑘 + 1) ∈ 𝐶) → ((𝐹‘𝐶)‘𝑘) ≤ 0)
157	6	adantr 480	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ (𝑘 ∈ (1...𝐽) ∧ ((𝐹‘𝐶)‘𝑘) ≤ 0)) ∧ ¬ (𝑘 + 1) ∈ 𝐶) → 𝑘 ∈ (1...𝐽))
158	157, 37	syl 17	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ (𝑘 ∈ (1...𝐽) ∧ ((𝐹‘𝐶)‘𝑘) ≤ 0)) ∧ ¬ (𝑘 + 1) ∈ 𝐶) → 𝑘 ∈ (0...𝐽))
159	130	imdistani 722	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ (𝑘 ∈ (1...𝐽) ∧ ((𝐹‘𝐶)‘𝑘) ≤ 0)) → (𝜑 ∧ (𝑘 + 1) ∈ (1...𝐽)))
160	44	adantr 480	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ (𝑘 + 1) ∈ (1...𝐽)) → 𝐶 ∈ 𝑂)
161		elfznn 12241	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑘 + 1) ∈ (1...𝐽) → (𝑘 + 1) ∈ ℕ)
162	161	adantl 481	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ (𝑘 + 1) ∈ (1...𝐽)) → (𝑘 + 1) ∈ ℕ)
163	39, 40, 41, 42, 43, 160, 162	ballotlemfp1 29880	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ (𝑘 + 1) ∈ (1...𝐽)) → ((¬ (𝑘 + 1) ∈ 𝐶 → ((𝐹‘𝐶)‘(𝑘 + 1)) = (((𝐹‘𝐶)‘((𝑘 + 1) − 1)) − 1)) ∧ ((𝑘 + 1) ∈ 𝐶 → ((𝐹‘𝐶)‘(𝑘 + 1)) = (((𝐹‘𝐶)‘((𝑘 + 1) − 1)) + 1))))
164	163	simpld 474	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ (𝑘 + 1) ∈ (1...𝐽)) → (¬ (𝑘 + 1) ∈ 𝐶 → ((𝐹‘𝐶)‘(𝑘 + 1)) = (((𝐹‘𝐶)‘((𝑘 + 1) − 1)) − 1)))
165	164	imp 444	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ (𝑘 + 1) ∈ (1...𝐽)) ∧ ¬ (𝑘 + 1) ∈ 𝐶) → ((𝐹‘𝐶)‘(𝑘 + 1)) = (((𝐹‘𝐶)‘((𝑘 + 1) − 1)) − 1))
166	159, 165	sylan 487	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ (𝑘 ∈ (1...𝐽) ∧ ((𝐹‘𝐶)‘𝑘) ≤ 0)) ∧ ¬ (𝑘 + 1) ∈ 𝐶) → ((𝐹‘𝐶)‘(𝑘 + 1)) = (((𝐹‘𝐶)‘((𝑘 + 1) − 1)) − 1))
167		elfzelz 12213	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑘 ∈ (1...𝐽) → 𝑘 ∈ ℤ)
168	167	zcnd 11359	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑘 ∈ (1...𝐽) → 𝑘 ∈ ℂ)
169		1cnd 9935	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑘 ∈ (1...𝐽) → 1 ∈ ℂ)
170	168, 169	pncand 10272	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑘 ∈ (1...𝐽) → ((𝑘 + 1) − 1) = 𝑘)
171	170	fveq2d 6107	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑘 ∈ (1...𝐽) → ((𝐹‘𝐶)‘((𝑘 + 1) − 1)) = ((𝐹‘𝐶)‘𝑘))
172	171	oveq1d 6564	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑘 ∈ (1...𝐽) → (((𝐹‘𝐶)‘((𝑘 + 1) − 1)) − 1) = (((𝐹‘𝐶)‘𝑘) − 1))
173	172	eqeq2d 2620	. . . . . . . . . . . . . . . . 17 ⊢ (𝑘 ∈ (1...𝐽) → (((𝐹‘𝐶)‘(𝑘 + 1)) = (((𝐹‘𝐶)‘((𝑘 + 1) − 1)) − 1) ↔ ((𝐹‘𝐶)‘(𝑘 + 1)) = (((𝐹‘𝐶)‘𝑘) − 1)))
174	157, 173	syl 17	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ (𝑘 ∈ (1...𝐽) ∧ ((𝐹‘𝐶)‘𝑘) ≤ 0)) ∧ ¬ (𝑘 + 1) ∈ 𝐶) → (((𝐹‘𝐶)‘(𝑘 + 1)) = (((𝐹‘𝐶)‘((𝑘 + 1) − 1)) − 1) ↔ ((𝐹‘𝐶)‘(𝑘 + 1)) = (((𝐹‘𝐶)‘𝑘) − 1)))
175	166, 174	mpbid 221	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ (𝑘 ∈ (1...𝐽) ∧ ((𝐹‘𝐶)‘𝑘) ≤ 0)) ∧ ¬ (𝑘 + 1) ∈ 𝐶) → ((𝐹‘𝐶)‘(𝑘 + 1)) = (((𝐹‘𝐶)‘𝑘) − 1))
176		0z 11265	. . . . . . . . . . . . . . . . . 18 ⊢ 0 ∈ ℤ
177		zlem1lt 11306	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝐹‘𝐶)‘𝑘) ∈ ℤ ∧ 0 ∈ ℤ) → (((𝐹‘𝐶)‘𝑘) ≤ 0 ↔ (((𝐹‘𝐶)‘𝑘) − 1) < 0))
178	48, 176, 177	sylancl 693	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝐽)) → (((𝐹‘𝐶)‘𝑘) ≤ 0 ↔ (((𝐹‘𝐶)‘𝑘) − 1) < 0))
179	178	adantr 480	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑘 ∈ (0...𝐽)) ∧ ((𝐹‘𝐶)‘(𝑘 + 1)) = (((𝐹‘𝐶)‘𝑘) − 1)) → (((𝐹‘𝐶)‘𝑘) ≤ 0 ↔ (((𝐹‘𝐶)‘𝑘) − 1) < 0))
180		breq1 4586	. . . . . . . . . . . . . . . . 17 ⊢ (((𝐹‘𝐶)‘(𝑘 + 1)) = (((𝐹‘𝐶)‘𝑘) − 1) → (((𝐹‘𝐶)‘(𝑘 + 1)) < 0 ↔ (((𝐹‘𝐶)‘𝑘) − 1) < 0))
181	180	adantl 481	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑘 ∈ (0...𝐽)) ∧ ((𝐹‘𝐶)‘(𝑘 + 1)) = (((𝐹‘𝐶)‘𝑘) − 1)) → (((𝐹‘𝐶)‘(𝑘 + 1)) < 0 ↔ (((𝐹‘𝐶)‘𝑘) − 1) < 0))
182	179, 181	bitr4d 270	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑘 ∈ (0...𝐽)) ∧ ((𝐹‘𝐶)‘(𝑘 + 1)) = (((𝐹‘𝐶)‘𝑘) − 1)) → (((𝐹‘𝐶)‘𝑘) ≤ 0 ↔ ((𝐹‘𝐶)‘(𝑘 + 1)) < 0))
183	145, 158, 175, 182	syl21anc 1317	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (𝑘 ∈ (1...𝐽) ∧ ((𝐹‘𝐶)‘𝑘) ≤ 0)) ∧ ¬ (𝑘 + 1) ∈ 𝐶) → (((𝐹‘𝐶)‘𝑘) ≤ 0 ↔ ((𝐹‘𝐶)‘(𝑘 + 1)) < 0))
184	156, 183	mpbid 221	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑘 ∈ (1...𝐽) ∧ ((𝐹‘𝐶)‘𝑘) ≤ 0)) ∧ ¬ (𝑘 + 1) ∈ 𝐶) → ((𝐹‘𝐶)‘(𝑘 + 1)) < 0)
185	154, 155, 184	ltled 10064	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝑘 ∈ (1...𝐽) ∧ ((𝐹‘𝐶)‘𝑘) ≤ 0)) ∧ ¬ (𝑘 + 1) ∈ 𝐶) → ((𝐹‘𝐶)‘(𝑘 + 1)) ≤ 0)
186	185	adantlrr 753	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ ((𝑘 ∈ (1...𝐽) ∧ ((𝐹‘𝐶)‘𝑘) ≤ 0) ∧ ∀𝑗 ∈ {𝑖 ∈ (1...𝐽) ∣ ((𝐹‘𝐶)‘𝑖) ≤ 0}𝑗 ≤ 𝑘)) ∧ ¬ (𝑘 + 1) ∈ 𝐶) → ((𝐹‘𝐶)‘(𝑘 + 1)) ≤ 0)
187	143, 144, 186, 138	syl12anc 1316	. . . . . . . . . 10 ⊢ (((𝜑 ∧ ((𝑘 ∈ (1...𝐽) ∧ ((𝐹‘𝐶)‘𝑘) ≤ 0) ∧ ∀𝑗 ∈ {𝑖 ∈ (1...𝐽) ∣ ((𝐹‘𝐶)‘𝑖) ≤ 0}𝑗 ≤ 𝑘)) ∧ ¬ (𝑘 + 1) ∈ 𝐶) → (𝑘 + 1) ≤ 𝑘)
188	19	adantr 480	. . . . . . . . . 10 ⊢ (((𝜑 ∧ ((𝑘 ∈ (1...𝐽) ∧ ((𝐹‘𝐶)‘𝑘) ≤ 0) ∧ ∀𝑗 ∈ {𝑖 ∈ (1...𝐽) ∣ ((𝐹‘𝐶)‘𝑖) ≤ 0}𝑗 ≤ 𝑘)) ∧ ¬ (𝑘 + 1) ∈ 𝐶) → ¬ (𝑘 + 1) ≤ 𝑘)
189	187, 188	condan 831	. . . . . . . . 9 ⊢ ((𝜑 ∧ ((𝑘 ∈ (1...𝐽) ∧ ((𝐹‘𝐶)‘𝑘) ≤ 0) ∧ ∀𝑗 ∈ {𝑖 ∈ (1...𝐽) ∣ ((𝐹‘𝐶)‘𝑖) ≤ 0}𝑗 ≤ 𝑘)) → (𝑘 + 1) ∈ 𝐶)
190	163	simprd 478	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑘 + 1) ∈ (1...𝐽)) → ((𝑘 + 1) ∈ 𝐶 → ((𝐹‘𝐶)‘(𝑘 + 1)) = (((𝐹‘𝐶)‘((𝑘 + 1) − 1)) + 1)))
191	190	imp 444	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝑘 + 1) ∈ (1...𝐽)) ∧ (𝑘 + 1) ∈ 𝐶) → ((𝐹‘𝐶)‘(𝑘 + 1)) = (((𝐹‘𝐶)‘((𝑘 + 1) − 1)) + 1))
192	159, 191	sylan 487	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝑘 ∈ (1...𝐽) ∧ ((𝐹‘𝐶)‘𝑘) ≤ 0)) ∧ (𝑘 + 1) ∈ 𝐶) → ((𝐹‘𝐶)‘(𝑘 + 1)) = (((𝐹‘𝐶)‘((𝑘 + 1) − 1)) + 1))
193	6	adantr 480	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝑘 ∈ (1...𝐽) ∧ ((𝐹‘𝐶)‘𝑘) ≤ 0)) ∧ (𝑘 + 1) ∈ 𝐶) → 𝑘 ∈ (1...𝐽))
194	171	oveq1d 6564	. . . . . . . . . . . . 13 ⊢ (𝑘 ∈ (1...𝐽) → (((𝐹‘𝐶)‘((𝑘 + 1) − 1)) + 1) = (((𝐹‘𝐶)‘𝑘) + 1))
195	194	eqeq2d 2620	. . . . . . . . . . . 12 ⊢ (𝑘 ∈ (1...𝐽) → (((𝐹‘𝐶)‘(𝑘 + 1)) = (((𝐹‘𝐶)‘((𝑘 + 1) − 1)) + 1) ↔ ((𝐹‘𝐶)‘(𝑘 + 1)) = (((𝐹‘𝐶)‘𝑘) + 1)))
196	193, 195	syl 17	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝑘 ∈ (1...𝐽) ∧ ((𝐹‘𝐶)‘𝑘) ≤ 0)) ∧ (𝑘 + 1) ∈ 𝐶) → (((𝐹‘𝐶)‘(𝑘 + 1)) = (((𝐹‘𝐶)‘((𝑘 + 1) − 1)) + 1) ↔ ((𝐹‘𝐶)‘(𝑘 + 1)) = (((𝐹‘𝐶)‘𝑘) + 1)))
197	192, 196	mpbid 221	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝑘 ∈ (1...𝐽) ∧ ((𝐹‘𝐶)‘𝑘) ≤ 0)) ∧ (𝑘 + 1) ∈ 𝐶) → ((𝐹‘𝐶)‘(𝑘 + 1)) = (((𝐹‘𝐶)‘𝑘) + 1))
198	197	adantlrr 753	. . . . . . . . 9 ⊢ (((𝜑 ∧ ((𝑘 ∈ (1...𝐽) ∧ ((𝐹‘𝐶)‘𝑘) ≤ 0) ∧ ∀𝑗 ∈ {𝑖 ∈ (1...𝐽) ∣ ((𝐹‘𝐶)‘𝑖) ≤ 0}𝑗 ≤ 𝑘)) ∧ (𝑘 + 1) ∈ 𝐶) → ((𝐹‘𝐶)‘(𝑘 + 1)) = (((𝐹‘𝐶)‘𝑘) + 1))
199	189, 198	mpdan 699	. . . . . . . 8 ⊢ ((𝜑 ∧ ((𝑘 ∈ (1...𝐽) ∧ ((𝐹‘𝐶)‘𝑘) ≤ 0) ∧ ∀𝑗 ∈ {𝑖 ∈ (1...𝐽) ∣ ((𝐹‘𝐶)‘𝑖) ≤ 0}𝑗 ≤ 𝑘)) → ((𝐹‘𝐶)‘(𝑘 + 1)) = (((𝐹‘𝐶)‘𝑘) + 1))
200		breq1 4586	. . . . . . . . 9 ⊢ (((𝐹‘𝐶)‘(𝑘 + 1)) = (((𝐹‘𝐶)‘𝑘) + 1) → (((𝐹‘𝐶)‘(𝑘 + 1)) ≤ 0 ↔ (((𝐹‘𝐶)‘𝑘) + 1) ≤ 0))
201	200	notbid 307	. . . . . . . 8 ⊢ (((𝐹‘𝐶)‘(𝑘 + 1)) = (((𝐹‘𝐶)‘𝑘) + 1) → (¬ ((𝐹‘𝐶)‘(𝑘 + 1)) ≤ 0 ↔ ¬ (((𝐹‘𝐶)‘𝑘) + 1) ≤ 0))
202	199, 201	syl 17	. . . . . . 7 ⊢ ((𝜑 ∧ ((𝑘 ∈ (1...𝐽) ∧ ((𝐹‘𝐶)‘𝑘) ≤ 0) ∧ ∀𝑗 ∈ {𝑖 ∈ (1...𝐽) ∣ ((𝐹‘𝐶)‘𝑖) ≤ 0}𝑗 ≤ 𝑘)) → (¬ ((𝐹‘𝐶)‘(𝑘 + 1)) ≤ 0 ↔ ¬ (((𝐹‘𝐶)‘𝑘) + 1) ≤ 0))
203	142, 202	mpbid 221	. . . . . 6 ⊢ ((𝜑 ∧ ((𝑘 ∈ (1...𝐽) ∧ ((𝐹‘𝐶)‘𝑘) ≤ 0) ∧ ∀𝑗 ∈ {𝑖 ∈ (1...𝐽) ∣ ((𝐹‘𝐶)‘𝑖) ≤ 0}𝑗 ≤ 𝑘)) → ¬ (((𝐹‘𝐶)‘𝑘) + 1) ≤ 0)
204	6, 37	syl 17	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑘 ∈ (1...𝐽) ∧ ((𝐹‘𝐶)‘𝑘) ≤ 0)) → 𝑘 ∈ (0...𝐽))
205	204, 48	syldan 486	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑘 ∈ (1...𝐽) ∧ ((𝐹‘𝐶)‘𝑘) ≤ 0)) → ((𝐹‘𝐶)‘𝑘) ∈ ℤ)
206	205	adantrr 749	. . . . . . 7 ⊢ ((𝜑 ∧ ((𝑘 ∈ (1...𝐽) ∧ ((𝐹‘𝐶)‘𝑘) ≤ 0) ∧ ∀𝑗 ∈ {𝑖 ∈ (1...𝐽) ∣ ((𝐹‘𝐶)‘𝑖) ≤ 0}𝑗 ≤ 𝑘)) → ((𝐹‘𝐶)‘𝑘) ∈ ℤ)
207		zleltp1 11305	. . . . . . . . 9 ⊢ ((0 ∈ ℤ ∧ ((𝐹‘𝐶)‘𝑘) ∈ ℤ) → (0 ≤ ((𝐹‘𝐶)‘𝑘) ↔ 0 < (((𝐹‘𝐶)‘𝑘) + 1)))
208	176, 207	mpan 702	. . . . . . . 8 ⊢ (((𝐹‘𝐶)‘𝑘) ∈ ℤ → (0 ≤ ((𝐹‘𝐶)‘𝑘) ↔ 0 < (((𝐹‘𝐶)‘𝑘) + 1)))
209		0red 9920	. . . . . . . . 9 ⊢ (((𝐹‘𝐶)‘𝑘) ∈ ℤ → 0 ∈ ℝ)
210		zre 11258	. . . . . . . . . 10 ⊢ (((𝐹‘𝐶)‘𝑘) ∈ ℤ → ((𝐹‘𝐶)‘𝑘) ∈ ℝ)
211		1red 9934	. . . . . . . . . 10 ⊢ (((𝐹‘𝐶)‘𝑘) ∈ ℤ → 1 ∈ ℝ)
212	210, 211	readdcld 9948	. . . . . . . . 9 ⊢ (((𝐹‘𝐶)‘𝑘) ∈ ℤ → (((𝐹‘𝐶)‘𝑘) + 1) ∈ ℝ)
213	209, 212	ltnled 10063	. . . . . . . 8 ⊢ (((𝐹‘𝐶)‘𝑘) ∈ ℤ → (0 < (((𝐹‘𝐶)‘𝑘) + 1) ↔ ¬ (((𝐹‘𝐶)‘𝑘) + 1) ≤ 0))
214	208, 213	bitrd 267	. . . . . . 7 ⊢ (((𝐹‘𝐶)‘𝑘) ∈ ℤ → (0 ≤ ((𝐹‘𝐶)‘𝑘) ↔ ¬ (((𝐹‘𝐶)‘𝑘) + 1) ≤ 0))
215	206, 214	syl 17	. . . . . 6 ⊢ ((𝜑 ∧ ((𝑘 ∈ (1...𝐽) ∧ ((𝐹‘𝐶)‘𝑘) ≤ 0) ∧ ∀𝑗 ∈ {𝑖 ∈ (1...𝐽) ∣ ((𝐹‘𝐶)‘𝑖) ≤ 0}𝑗 ≤ 𝑘)) → (0 ≤ ((𝐹‘𝐶)‘𝑘) ↔ ¬ (((𝐹‘𝐶)‘𝑘) + 1) ≤ 0))
216	203, 215	mpbird 246	. . . . 5 ⊢ ((𝜑 ∧ ((𝑘 ∈ (1...𝐽) ∧ ((𝐹‘𝐶)‘𝑘) ≤ 0) ∧ ∀𝑗 ∈ {𝑖 ∈ (1...𝐽) ∣ ((𝐹‘𝐶)‘𝑖) ≤ 0}𝑗 ≤ 𝑘)) → 0 ≤ ((𝐹‘𝐶)‘𝑘))
217	206	zred 11358	. . . . . 6 ⊢ ((𝜑 ∧ ((𝑘 ∈ (1...𝐽) ∧ ((𝐹‘𝐶)‘𝑘) ≤ 0) ∧ ∀𝑗 ∈ {𝑖 ∈ (1...𝐽) ∣ ((𝐹‘𝐶)‘𝑖) ≤ 0}𝑗 ≤ 𝑘)) → ((𝐹‘𝐶)‘𝑘) ∈ ℝ)
218		0red 9920	. . . . . 6 ⊢ ((𝜑 ∧ ((𝑘 ∈ (1...𝐽) ∧ ((𝐹‘𝐶)‘𝑘) ≤ 0) ∧ ∀𝑗 ∈ {𝑖 ∈ (1...𝐽) ∣ ((𝐹‘𝐶)‘𝑖) ≤ 0}𝑗 ≤ 𝑘)) → 0 ∈ ℝ)
219	217, 218	letri3d 10058	. . . . 5 ⊢ ((𝜑 ∧ ((𝑘 ∈ (1...𝐽) ∧ ((𝐹‘𝐶)‘𝑘) ≤ 0) ∧ ∀𝑗 ∈ {𝑖 ∈ (1...𝐽) ∣ ((𝐹‘𝐶)‘𝑖) ≤ 0}𝑗 ≤ 𝑘)) → (((𝐹‘𝐶)‘𝑘) = 0 ↔ (((𝐹‘𝐶)‘𝑘) ≤ 0 ∧ 0 ≤ ((𝐹‘𝐶)‘𝑘))))
220	5, 216, 219	mpbir2and 959	. . . 4 ⊢ ((𝜑 ∧ ((𝑘 ∈ (1...𝐽) ∧ ((𝐹‘𝐶)‘𝑘) ≤ 0) ∧ ∀𝑗 ∈ {𝑖 ∈ (1...𝐽) ∣ ((𝐹‘𝐶)‘𝑖) ≤ 0}𝑗 ≤ 𝑘)) → ((𝐹‘𝐶)‘𝑘) = 0)
221	4, 220	sylan2b 491	. . 3 ⊢ ((𝜑 ∧ (𝑘 ∈ {𝑖 ∈ (1...𝐽) ∣ ((𝐹‘𝐶)‘𝑖) ≤ 0} ∧ ∀𝑗 ∈ {𝑖 ∈ (1...𝐽) ∣ ((𝐹‘𝐶)‘𝑖) ≤ 0}𝑗 ≤ 𝑘)) → ((𝐹‘𝐶)‘𝑘) = 0)
222		ssrab2 3650	. . . . . 6 ⊢ {𝑖 ∈ (1...𝐽) ∣ ((𝐹‘𝐶)‘𝑖) ≤ 0} ⊆ (1...𝐽)
223	222, 12	sstri 3577	. . . . 5 ⊢ {𝑖 ∈ (1...𝐽) ∣ ((𝐹‘𝐶)‘𝑖) ≤ 0} ⊆ ℝ
224	223	a1i 11	. . . 4 ⊢ (𝜑 → {𝑖 ∈ (1...𝐽) ∣ ((𝐹‘𝐶)‘𝑖) ≤ 0} ⊆ ℝ)
225		fzfi 12633	. . . . . 6 ⊢ (1...𝐽) ∈ Fin
226		ssfi 8065	. . . . . 6 ⊢ (((1...𝐽) ∈ Fin ∧ {𝑖 ∈ (1...𝐽) ∣ ((𝐹‘𝐶)‘𝑖) ≤ 0} ⊆ (1...𝐽)) → {𝑖 ∈ (1...𝐽) ∣ ((𝐹‘𝐶)‘𝑖) ≤ 0} ∈ Fin)
227	225, 222, 226	mp2an 704	. . . . 5 ⊢ {𝑖 ∈ (1...𝐽) ∣ ((𝐹‘𝐶)‘𝑖) ≤ 0} ∈ Fin
228	227	a1i 11	. . . 4 ⊢ (𝜑 → {𝑖 ∈ (1...𝐽) ∣ ((𝐹‘𝐶)‘𝑖) ≤ 0} ∈ Fin)
229		rabn0 3912	. . . . 5 ⊢ ({𝑖 ∈ (1...𝐽) ∣ ((𝐹‘𝐶)‘𝑖) ≤ 0} ≠ ∅ ↔ ∃𝑖 ∈ (1...𝐽)((𝐹‘𝐶)‘𝑖) ≤ 0)
230	60, 229	sylibr 223	. . . 4 ⊢ (𝜑 → {𝑖 ∈ (1...𝐽) ∣ ((𝐹‘𝐶)‘𝑖) ≤ 0} ≠ ∅)
231		fimaxre 10847	. . . 4 ⊢ (({𝑖 ∈ (1...𝐽) ∣ ((𝐹‘𝐶)‘𝑖) ≤ 0} ⊆ ℝ ∧ {𝑖 ∈ (1...𝐽) ∣ ((𝐹‘𝐶)‘𝑖) ≤ 0} ∈ Fin ∧ {𝑖 ∈ (1...𝐽) ∣ ((𝐹‘𝐶)‘𝑖) ≤ 0} ≠ ∅) → ∃𝑘 ∈ {𝑖 ∈ (1...𝐽) ∣ ((𝐹‘𝐶)‘𝑖) ≤ 0}∀𝑗 ∈ {𝑖 ∈ (1...𝐽) ∣ ((𝐹‘𝐶)‘𝑖) ≤ 0}𝑗 ≤ 𝑘)
232	224, 228, 230, 231	syl3anc 1318	. . 3 ⊢ (𝜑 → ∃𝑘 ∈ {𝑖 ∈ (1...𝐽) ∣ ((𝐹‘𝐶)‘𝑖) ≤ 0}∀𝑗 ∈ {𝑖 ∈ (1...𝐽) ∣ ((𝐹‘𝐶)‘𝑖) ≤ 0}𝑗 ≤ 𝑘)
233	221, 232	reximddv 3001	. 2 ⊢ (𝜑 → ∃𝑘 ∈ {𝑖 ∈ (1...𝐽) ∣ ((𝐹‘𝐶)‘𝑖) ≤ 0} ((𝐹‘𝐶)‘𝑘) = 0)
234		elrabi 3328	. . . 4 ⊢ (𝑘 ∈ {𝑖 ∈ (1...𝐽) ∣ ((𝐹‘𝐶)‘𝑖) ≤ 0} → 𝑘 ∈ (1...𝐽))
235	234	anim1i 590	. . 3 ⊢ ((𝑘 ∈ {𝑖 ∈ (1...𝐽) ∣ ((𝐹‘𝐶)‘𝑖) ≤ 0} ∧ ((𝐹‘𝐶)‘𝑘) = 0) → (𝑘 ∈ (1...𝐽) ∧ ((𝐹‘𝐶)‘𝑘) = 0))
236	235	reximi2 2993	. 2 ⊢ (∃𝑘 ∈ {𝑖 ∈ (1...𝐽) ∣ ((𝐹‘𝐶)‘𝑖) ≤ 0} ((𝐹‘𝐶)‘𝑘) = 0 → ∃𝑘 ∈ (1...𝐽)((𝐹‘𝐶)‘𝑘) = 0)
237	233, 236	syl 17	1 ⊢ (𝜑 → ∃𝑘 ∈ (1...𝐽)((𝐹‘𝐶)‘𝑘) = 0)

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ↔ wb 195 ∨ wo 382 ∧ wa 383 = wceq 1475 ∈ wcel 1977 ≠ wne 2780 ∀wral 2896 ∃wrex 2897 {crab 2900 ∖ cdif 3537 ∩ cin 3539 ⊆ wss 3540 ∅c0 3874 𝒫 cpw 4108 {csn 4125 class class class wbr 4583 ↦ cmpt 4643 ‘cfv 5804 (class class class)co 6549 Fincfn 7841 ℝcr 9814 0cc0 9815 1c1 9816 + caddc 9818 < clt 9953 ≤ cle 9954 − cmin 10145 / cdiv 10563 ℕcn 10897 2c2 10947 ℤcz 11254 ℤ_≥cuz 11563 ...cfz 12197 #chash 12979

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1713 ax-4 1728 ax-5 1827 ax-6 1875 ax-7 1922 ax-8 1979 ax-9 1986 ax-10 2006 ax-11 2021 ax-12 2034 ax-13 2234 ax-ext 2590 ax-rep 4699 ax-sep 4709 ax-nul 4717 ax-pow 4769 ax-pr 4833 ax-un 6847 ax-cnex 9871 ax-resscn 9872 ax-1cn 9873 ax-icn 9874 ax-addcl 9875 ax-addrcl 9876 ax-mulcl 9877 ax-mulrcl 9878 ax-mulcom 9879 ax-addass 9880 ax-mulass 9881 ax-distr 9882 ax-i2m1 9883 ax-1ne0 9884 ax-1rid 9885 ax-rnegex 9886 ax-rrecex 9887 ax-cnre 9888 ax-pre-lttri 9889 ax-pre-lttrn 9890 ax-pre-ltadd 9891 ax-pre-mulgt0 9892

This theorem depends on definitions: df-bi 196 df-or 384 df-an 385 df-3or 1032 df-3an 1033 df-tru 1478 df-ex 1696 df-nf 1701 df-sb 1868 df-eu 2462 df-mo 2463 df-clab 2597 df-cleq 2603 df-clel 2606 df-nfc 2740 df-ne 2782 df-nel 2783 df-ral 2901 df-rex 2902 df-reu 2903 df-rmo 2904 df-rab 2905 df-v 3175 df-sbc 3403 df-csb 3500 df-dif 3543 df-un 3545 df-in 3547 df-ss 3554 df-pss 3556 df-nul 3875 df-if 4037 df-pw 4110 df-sn 4126 df-pr 4128 df-tp 4130 df-op 4132 df-uni 4373 df-int 4411 df-iun 4457 df-br 4584 df-opab 4644 df-mpt 4645 df-tr 4681 df-eprel 4949 df-id 4953 df-po 4959 df-so 4960 df-fr 4997 df-we 4999 df-xp 5044 df-rel 5045 df-cnv 5046 df-co 5047 df-dm 5048 df-rn 5049 df-res 5050 df-ima 5051 df-pred 5597 df-ord 5643 df-on 5644 df-lim 5645 df-suc 5646 df-iota 5768 df-fun 5806 df-fn 5807 df-f 5808 df-f1 5809 df-fo 5810 df-f1o 5811 df-fv 5812 df-riota 6511 df-ov 6552 df-oprab 6553 df-mpt2 6554 df-om 6958 df-1st 7059 df-2nd 7060 df-wrecs 7294 df-recs 7355 df-rdg 7393 df-1o 7447 df-oadd 7451 df-er 7629 df-en 7842 df-dom 7843 df-sdom 7844 df-fin 7845 df-card 8648 df-cda 8873 df-pnf 9955 df-mnf 9956 df-xr 9957 df-ltxr 9958 df-le 9959 df-sub 10147 df-neg 10148 df-nn 10898 df-2 10956 df-n0 11170 df-z 11255 df-uz 11564 df-fz 12198 df-hash 12980

This theorem is referenced by: ballotlem5 29888 ballotlemic 29895

W3C validator