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 34915

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 6888	. . . . . . 7 ⊢ (𝑖 = 𝑘 → ((𝐹‘𝐶)‘𝑖) = ((𝐹‘𝐶)‘𝑘))
2	1	breq1d 5124	. . . . . 6 ⊢ (𝑖 = 𝑘 → (((𝐹‘𝐶)‘𝑖) ≤ 0 ↔ ((𝐹‘𝐶)‘𝑘) ≤ 0))
3	2	elrab 3653	. . . . 5 ⊢ (𝑘 ∈ {𝑖 ∈ (1...𝐽) ∣ ((𝐹‘𝐶)‘𝑖) ≤ 0} ↔ (𝑘 ∈ (1...𝐽) ∧ ((𝐹‘𝐶)‘𝑘) ≤ 0))
4	3	anbi1i 636	. . . 4 ⊢ ((𝑘 ∈ {𝑖 ∈ (1...𝐽) ∣ ((𝐹‘𝐶)‘𝑖) ≤ 0} ∧ ∀𝑗 ∈ {𝑖 ∈ (1...𝐽) ∣ ((𝐹‘𝐶)‘𝑖) ≤ 0}𝑗 ≤ 𝑘) ↔ ((𝑘 ∈ (1...𝐽) ∧ ((𝐹‘𝐶)‘𝑘) ≤ 0) ∧ ∀𝑗 ∈ {𝑖 ∈ (1...𝐽) ∣ ((𝐹‘𝐶)‘𝑖) ≤ 0}𝑗 ≤ 𝑘))
5		simprlr 792	. . . . 5 ⊢ ((𝜑 ∧ ((𝑘 ∈ (1...𝐽) ∧ ((𝐹‘𝐶)‘𝑘) ≤ 0) ∧ ∀𝑗 ∈ {𝑖 ∈ (1...𝐽) ∣ ((𝐹‘𝐶)‘𝑖) ≤ 0}𝑗 ≤ 𝑘)) → ((𝐹‘𝐶)‘𝑘) ≤ 0)
6		simprl 783	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑘 ∈ (1...𝐽) ∧ ((𝐹‘𝐶)‘𝑘) ≤ 0)) → 𝑘 ∈ (1...𝐽))
7	6	adantrr 730	. . . . . . . . 9 ⊢ ((𝜑 ∧ ((𝑘 ∈ (1...𝐽) ∧ ((𝐹‘𝐶)‘𝑘) ≤ 0) ∧ ∀𝑗 ∈ {𝑖 ∈ (1...𝐽) ∣ ((𝐹‘𝐶)‘𝑖) ≤ 0}𝑗 ≤ 𝑘)) → 𝑘 ∈ (1...𝐽))
8		fzssuz 13612	. . . . . . . . . . . . . 14 ⊢ (1...𝐽) ⊆ (ℤ_≥‘1)
9		uzssz 12901	. . . . . . . . . . . . . 14 ⊢ (ℤ_≥‘1) ⊆ ℤ
10	8, 9	sstri 3949	. . . . . . . . . . . . 13 ⊢ (1...𝐽) ⊆ ℤ
11		zssre 12616	. . . . . . . . . . . . 13 ⊢ ℤ ⊆ ℝ
12	10, 11	sstri 3949	. . . . . . . . . . . 12 ⊢ (1...𝐽) ⊆ ℝ
13	12	sseli 3936	. . . . . . . . . . 11 ⊢ (𝑘 ∈ (1...𝐽) → 𝑘 ∈ ℝ)
14	13	ltp1d 12163	. . . . . . . . . 10 ⊢ (𝑘 ∈ (1...𝐽) → 𝑘 < (𝑘 + 1))
15		1red 11227	. . . . . . . . . . . 12 ⊢ (𝑘 ∈ (1...𝐽) → 1 ∈ ℝ)
16	13, 15	readdcld 11256	. . . . . . . . . . 11 ⊢ (𝑘 ∈ (1...𝐽) → (𝑘 + 1) ∈ ℝ)
17	13, 16	ltnled 11375	. . . . . . . . . 10 ⊢ (𝑘 ∈ (1...𝐽) → (𝑘 < (𝑘 + 1) ↔ ¬ (𝑘 + 1) ≤ 𝑘))
18	14, 17	mpbid 235	. . . . . . . . 9 ⊢ (𝑘 ∈ (1...𝐽) → ¬ (𝑘 + 1) ≤ 𝑘)
19	7, 18	syl 18	. . . . . . . 8 ⊢ ((𝜑 ∧ ((𝑘 ∈ (1...𝐽) ∧ ((𝐹‘𝐶)‘𝑘) ≤ 0) ∧ ∀𝑗 ∈ {𝑖 ∈ (1...𝐽) ∣ ((𝐹‘𝐶)‘𝑖) ≤ 0}𝑗 ≤ 𝑘)) → ¬ (𝑘 + 1) ≤ 𝑘)
20		simprr 785	. . . . . . . . 9 ⊢ ((𝜑 ∧ ((𝑘 ∈ (1...𝐽) ∧ ((𝐹‘𝐶)‘𝑘) ≤ 0) ∧ ∀𝑗 ∈ {𝑖 ∈ (1...𝐽) ∣ ((𝐹‘𝐶)‘𝑖) ≤ 0}𝑗 ≤ 𝑘)) → ∀𝑗 ∈ {𝑖 ∈ (1...𝐽) ∣ ((𝐹‘𝐶)‘𝑖) ≤ 0}𝑗 ≤ 𝑘)
21		ballotlemfc0.4	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → 0 < ((𝐹‘𝐶)‘𝐽))
22	21	adantr 486	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑘 = 𝐽) → 0 < ((𝐹‘𝐶)‘𝐽))
23		simpr 490	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑘 = 𝐽) → 𝑘 = 𝐽)
24	23	fveq2d 6892	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑘 = 𝐽) → ((𝐹‘𝐶)‘𝑘) = ((𝐹‘𝐶)‘𝐽))
25	24	breq2d 5126	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑘 = 𝐽) → (0 < ((𝐹‘𝐶)‘𝑘) ↔ 0 < ((𝐹‘𝐶)‘𝐽)))
26		ballotlemfp1.j	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜑 → 𝐽 ∈ ℕ)
27		elnnuz 12920	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝐽 ∈ ℕ ↔ 𝐽 ∈ (ℤ_≥‘1))
28	26, 27	sylib 221	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → 𝐽 ∈ (ℤ_≥‘1))
29		eluzfz2 13578	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝐽 ∈ (ℤ_≥‘1) → 𝐽 ∈ (1...𝐽))
30	28, 29	syl 18	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → 𝐽 ∈ (1...𝐽))
31		eleq1 2854	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑘 = 𝐽 → (𝑘 ∈ (1...𝐽) ↔ 𝐽 ∈ (1...𝐽)))
32	30, 31	syl5ibrcom 250	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → (𝑘 = 𝐽 → 𝑘 ∈ (1...𝐽)))
33	32	anc2li 565	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (𝑘 = 𝐽 → (𝜑 ∧ 𝑘 ∈ (1...𝐽))))
34		1eluzge0 12922	. . . . . . . . . . . . . . . . . . . 20 ⊢ 1 ∈ (ℤ_≥‘0)
35		fzss1 13610	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (1 ∈ (ℤ_≥‘0) → (1...𝐽) ⊆ (0...𝐽))
36	35	sseld 3939	. . . . . . . . . . . . . . . . . . . 20 ⊢ (1 ∈ (ℤ_≥‘0) → (𝑘 ∈ (1...𝐽) → 𝑘 ∈ (0...𝐽)))
37	34, 36	ax-mp 5	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑘 ∈ (1...𝐽) → 𝑘 ∈ (0...𝐽))
38		0red 11229	. . . . . . . . . . . . . . . . . . . 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 486	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝐽)) → 𝐶 ∈ 𝑂)
46		elfzelz 13570	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑘 ∈ (0...𝐽) → 𝑘 ∈ ℤ)
47	46	adantl 487	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝐽)) → 𝑘 ∈ ℤ)
48	39, 40, 41, 42, 43, 45, 47	ballotlemfelz 34913	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝐽)) → ((𝐹‘𝐶)‘𝑘) ∈ ℤ)
49	48	zred 12718	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝐽)) → ((𝐹‘𝐶)‘𝑘) ∈ ℝ)
50	38, 49	ltnled 11375	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝐽)) → (0 < ((𝐹‘𝐶)‘𝑘) ↔ ¬ ((𝐹‘𝐶)‘𝑘) ≤ 0))
51	37, 50	sylan2 605	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑘 ∈ (1...𝐽)) → (0 < ((𝐹‘𝐶)‘𝑘) ↔ ¬ ((𝐹‘𝐶)‘𝑘) ≤ 0))
52	33, 51	syl6 36	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (𝑘 = 𝐽 → (0 < ((𝐹‘𝐶)‘𝑘) ↔ ¬ ((𝐹‘𝐶)‘𝑘) ≤ 0)))
53	52	imp 412	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑘 = 𝐽) → (0 < ((𝐹‘𝐶)‘𝑘) ↔ ¬ ((𝐹‘𝐶)‘𝑘) ≤ 0))
54	25, 53	bitr3d 284	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑘 = 𝐽) → (0 < ((𝐹‘𝐶)‘𝐽) ↔ ¬ ((𝐹‘𝐶)‘𝑘) ≤ 0))
55	22, 54	mpbid 235	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑘 = 𝐽) → ¬ ((𝐹‘𝐶)‘𝑘) ≤ 0)
56	55	ex 418	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝑘 = 𝐽 → ¬ ((𝐹‘𝐶)‘𝑘) ≤ 0))
57	56	con2d 135	. . . . . . . . . . . 12 ⊢ (𝜑 → (((𝐹‘𝐶)‘𝑘) ≤ 0 → ¬ 𝑘 = 𝐽))
58		nn1m1nn 12272	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝐽 ∈ ℕ → (𝐽 = 1 ∨ (𝐽 − 1) ∈ ℕ))
59	26, 58	syl 18	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → (𝐽 = 1 ∨ (𝐽 − 1) ∈ ℕ))
60		ballotlemfc0.3	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝜑 → ∃𝑖 ∈ (1...𝐽)((𝐹‘𝐶)‘𝑖) ≤ 0)
61	60	adantr 486	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝜑 ∧ 𝐽 = 1) → ∃𝑖 ∈ (1...𝐽)((𝐹‘𝐶)‘𝑖) ≤ 0)
62		oveq1 7430	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝐽 = 1 → (𝐽...𝐽) = (1...𝐽))
63	62	adantl 487	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝜑 ∧ 𝐽 = 1) → (𝐽...𝐽) = (1...𝐽))
64	26	nnzd 12635	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝜑 → 𝐽 ∈ ℤ)
65		fzsn 13613	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝐽 ∈ ℤ → (𝐽...𝐽) = {𝐽})
66	64, 65	syl 18	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝜑 → (𝐽...𝐽) = {𝐽})
67	66	adantr 486	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝜑 ∧ 𝐽 = 1) → (𝐽...𝐽) = {𝐽})
68	63, 67	eqtr3d 2803	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝜑 ∧ 𝐽 = 1) → (1...𝐽) = {𝐽})
69	61, 68	rexeqtrdv 3329	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝜑 ∧ 𝐽 = 1) → ∃𝑖 ∈ {𝐽} ((𝐹‘𝐶)‘𝑖) ≤ 0)
70		fveq2 6888	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝑖 = 𝐽 → ((𝐹‘𝐶)‘𝑖) = ((𝐹‘𝐶)‘𝐽))
71	70	breq1d 5124	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑖 = 𝐽 → (((𝐹‘𝐶)‘𝑖) ≤ 0 ↔ ((𝐹‘𝐶)‘𝐽) ≤ 0))
72	71	rexsng 4647	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝐽 ∈ ℕ → (∃𝑖 ∈ {𝐽} ((𝐹‘𝐶)‘𝑖) ≤ 0 ↔ ((𝐹‘𝐶)‘𝐽) ≤ 0))
73	26, 72	syl 18	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝜑 → (∃𝑖 ∈ {𝐽} ((𝐹‘𝐶)‘𝑖) ≤ 0 ↔ ((𝐹‘𝐶)‘𝐽) ≤ 0))
74	73	adantr 486	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝜑 ∧ 𝐽 = 1) → (∃𝑖 ∈ {𝐽} ((𝐹‘𝐶)‘𝑖) ≤ 0 ↔ ((𝐹‘𝐶)‘𝐽) ≤ 0))
75	69, 74	mpbid 235	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ 𝐽 = 1) → ((𝐹‘𝐶)‘𝐽) ≤ 0)
76	21	adantr 486	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝜑 ∧ 𝐽 = 1) → 0 < ((𝐹‘𝐶)‘𝐽))
77		0red 11229	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝜑 → 0 ∈ ℝ)
78	39, 40, 41, 42, 43, 44, 64	ballotlemfelz 34913	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝜑 → ((𝐹‘𝐶)‘𝐽) ∈ ℤ)
79	78	zred 12718	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝜑 → ((𝐹‘𝐶)‘𝐽) ∈ ℝ)
80	77, 79	ltnled 11375	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝜑 → (0 < ((𝐹‘𝐶)‘𝐽) ↔ ¬ ((𝐹‘𝐶)‘𝐽) ≤ 0))
81	80	adantr 486	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝜑 ∧ 𝐽 = 1) → (0 < ((𝐹‘𝐶)‘𝐽) ↔ ¬ ((𝐹‘𝐶)‘𝐽) ≤ 0))
82	76, 81	mpbid 235	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ 𝐽 = 1) → ¬ ((𝐹‘𝐶)‘𝐽) ≤ 0)
83	75, 82	pm2.65da 829	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜑 → ¬ 𝐽 = 1)
84		biortn 951	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (¬ 𝐽 = 1 → ((𝐽 − 1) ∈ ℕ ↔ (¬ ¬ 𝐽 = 1 ∨ (𝐽 − 1) ∈ ℕ)))
85	83, 84	syl 18	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → ((𝐽 − 1) ∈ ℕ ↔ (¬ ¬ 𝐽 = 1 ∨ (𝐽 − 1) ∈ ℕ)))
86		notnotb 318	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝐽 = 1 ↔ ¬ ¬ 𝐽 = 1)
87	86	orbi1i 927	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝐽 = 1 ∨ (𝐽 − 1) ∈ ℕ) ↔ (¬ ¬ 𝐽 = 1 ∨ (𝐽 − 1) ∈ ℕ))
88	85, 87	bitr4di 292	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → ((𝐽 − 1) ∈ ℕ ↔ (𝐽 = 1 ∨ (𝐽 − 1) ∈ ℕ)))
89	59, 88	mpbird 260	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → (𝐽 − 1) ∈ ℕ)
90		elnnuz 12920	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝐽 − 1) ∈ ℕ ↔ (𝐽 − 1) ∈ (ℤ_≥‘1))
91	89, 90	sylib 221	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (𝐽 − 1) ∈ (ℤ_≥‘1))
92		elfzp1 13621	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝐽 − 1) ∈ (ℤ_≥‘1) → (𝑘 ∈ (1...((𝐽 − 1) + 1)) ↔ (𝑘 ∈ (1...(𝐽 − 1)) ∨ 𝑘 = ((𝐽 − 1) + 1))))
93	91, 92	syl 18	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (𝑘 ∈ (1...((𝐽 − 1) + 1)) ↔ (𝑘 ∈ (1...(𝐽 − 1)) ∨ 𝑘 = ((𝐽 − 1) + 1))))
94	26	nncnd 12267	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → 𝐽 ∈ ℂ)
95		1cnd 11220	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → 1 ∈ ℂ)
96	94, 95	npcand 11591	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → ((𝐽 − 1) + 1) = 𝐽)
97	96	oveq2d 7439	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (1...((𝐽 − 1) + 1)) = (1...𝐽))
98	97	eleq2d 2852	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (𝑘 ∈ (1...((𝐽 − 1) + 1)) ↔ 𝑘 ∈ (1...𝐽)))
99	96	eqeq2d 2777	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (𝑘 = ((𝐽 − 1) + 1) ↔ 𝑘 = 𝐽))
100	99	orbi2d 929	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → ((𝑘 ∈ (1...(𝐽 − 1)) ∨ 𝑘 = ((𝐽 − 1) + 1)) ↔ (𝑘 ∈ (1...(𝐽 − 1)) ∨ 𝑘 = 𝐽)))
101	93, 98, 100	3bitr3d 312	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (𝑘 ∈ (1...𝐽) ↔ (𝑘 ∈ (1...(𝐽 − 1)) ∨ 𝑘 = 𝐽)))
102		orcom 884	. . . . . . . . . . . . . . . 16 ⊢ ((𝑘 ∈ (1...(𝐽 − 1)) ∨ 𝑘 = 𝐽) ↔ (𝑘 = 𝐽 ∨ 𝑘 ∈ (1...(𝐽 − 1))))
103	101, 102	bitrdi 290	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝑘 ∈ (1...𝐽) ↔ (𝑘 = 𝐽 ∨ 𝑘 ∈ (1...(𝐽 − 1)))))
104	103	biimpd 232	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝑘 ∈ (1...𝐽) → (𝑘 = 𝐽 ∨ 𝑘 ∈ (1...(𝐽 − 1)))))
105		pm5.6 1017	. . . . . . . . . . . . . 14 ⊢ (((𝑘 ∈ (1...𝐽) ∧ ¬ 𝑘 = 𝐽) → 𝑘 ∈ (1...(𝐽 − 1))) ↔ (𝑘 ∈ (1...𝐽) → (𝑘 = 𝐽 ∨ 𝑘 ∈ (1...(𝐽 − 1)))))
106	104, 105	sylibr 237	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((𝑘 ∈ (1...𝐽) ∧ ¬ 𝑘 = 𝐽) → 𝑘 ∈ (1...(𝐽 − 1))))
107	89	nnzd 12635	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → (𝐽 − 1) ∈ ℤ)
108		1z 12642	. . . . . . . . . . . . . . . . . . 19 ⊢ 1 ∈ ℤ
109	107, 108	jctil 529	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (1 ∈ ℤ ∧ (𝐽 − 1) ∈ ℤ))
110		elfzelz 13570	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑘 ∈ (1...(𝐽 − 1)) → 𝑘 ∈ ℤ)
111	110, 108	jctir 530	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑘 ∈ (1...(𝐽 − 1)) → (𝑘 ∈ ℤ ∧ 1 ∈ ℤ))
112		fzaddel 13605	. . . . . . . . . . . . . . . . . 18 ⊢ (((1 ∈ ℤ ∧ (𝐽 − 1) ∈ ℤ) ∧ (𝑘 ∈ ℤ ∧ 1 ∈ ℤ)) → (𝑘 ∈ (1...(𝐽 − 1)) ↔ (𝑘 + 1) ∈ ((1 + 1)...((𝐽 − 1) + 1))))
113	109, 111, 112	syl2an 608	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑘 ∈ (1...(𝐽 − 1))) → (𝑘 ∈ (1...(𝐽 − 1)) ↔ (𝑘 + 1) ∈ ((1 + 1)...((𝐽 − 1) + 1))))
114	113	biimp3a 1498	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑘 ∈ (1...(𝐽 − 1)) ∧ 𝑘 ∈ (1...(𝐽 − 1))) → (𝑘 + 1) ∈ ((1 + 1)...((𝐽 − 1) + 1)))
115	114	3anidm23 1448	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑘 ∈ (1...(𝐽 − 1))) → (𝑘 + 1) ∈ ((1 + 1)...((𝐽 − 1) + 1)))
116		1p1e2 12382	. . . . . . . . . . . . . . . . . . . 20 ⊢ (1 + 1) = 2
117	116	a1i 11	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → (1 + 1) = 2)
118	117, 96	oveq12d 7441	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → ((1 + 1)...((𝐽 − 1) + 1)) = (2...𝐽))
119	118	eleq2d 2852	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → ((𝑘 + 1) ∈ ((1 + 1)...((𝐽 − 1) + 1)) ↔ (𝑘 + 1) ∈ (2...𝐽)))
120		2eluzge1 12924	. . . . . . . . . . . . . . . . . . 19 ⊢ 2 ∈ (ℤ_≥‘1)
121		fzss1 13610	. . . . . . . . . . . . . . . . . . 19 ⊢ (2 ∈ (ℤ_≥‘1) → (2...𝐽) ⊆ (1...𝐽))
122	120, 121	ax-mp 5	. . . . . . . . . . . . . . . . . 18 ⊢ (2...𝐽) ⊆ (1...𝐽)
123	122	sseli 3936	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑘 + 1) ∈ (2...𝐽) → (𝑘 + 1) ∈ (1...𝐽))
124	119, 123	biimtrdi 256	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ((𝑘 + 1) ∈ ((1 + 1)...((𝐽 − 1) + 1)) → (𝑘 + 1) ∈ (1...𝐽)))
125	124	adantr 486	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑘 ∈ (1...(𝐽 − 1))) → ((𝑘 + 1) ∈ ((1 + 1)...((𝐽 − 1) + 1)) → (𝑘 + 1) ∈ (1...𝐽)))
126	115, 125	mpd 16	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑘 ∈ (1...(𝐽 − 1))) → (𝑘 + 1) ∈ (1...𝐽))
127	126	ex 418	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝑘 ∈ (1...(𝐽 − 1)) → (𝑘 + 1) ∈ (1...𝐽)))
128	106, 127	syld 48	. . . . . . . . . . . 12 ⊢ (𝜑 → ((𝑘 ∈ (1...𝐽) ∧ ¬ 𝑘 = 𝐽) → (𝑘 + 1) ∈ (1...𝐽)))
129	57, 128	sylan2d 617	. . . . . . . . . . 11 ⊢ (𝜑 → ((𝑘 ∈ (1...𝐽) ∧ ((𝐹‘𝐶)‘𝑘) ≤ 0) → (𝑘 + 1) ∈ (1...𝐽)))
130	129	imp 412	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑘 ∈ (1...𝐽) ∧ ((𝐹‘𝐶)‘𝑘) ≤ 0)) → (𝑘 + 1) ∈ (1...𝐽))
131	130	adantrr 730	. . . . . . . . 9 ⊢ ((𝜑 ∧ ((𝑘 ∈ (1...𝐽) ∧ ((𝐹‘𝐶)‘𝑘) ≤ 0) ∧ ∀𝑗 ∈ {𝑖 ∈ (1...𝐽) ∣ ((𝐹‘𝐶)‘𝑖) ≤ 0}𝑗 ≤ 𝑘)) → (𝑘 + 1) ∈ (1...𝐽))
132		fveq2 6888	. . . . . . . . . . . . . 14 ⊢ (𝑖 = (𝑘 + 1) → ((𝐹‘𝐶)‘𝑖) = ((𝐹‘𝐶)‘(𝑘 + 1)))
133	132	breq1d 5124	. . . . . . . . . . . . 13 ⊢ (𝑖 = (𝑘 + 1) → (((𝐹‘𝐶)‘𝑖) ≤ 0 ↔ ((𝐹‘𝐶)‘(𝑘 + 1)) ≤ 0))
134	133	elrab 3653	. . . . . . . . . . . 12 ⊢ ((𝑘 + 1) ∈ {𝑖 ∈ (1...𝐽) ∣ ((𝐹‘𝐶)‘𝑖) ≤ 0} ↔ ((𝑘 + 1) ∈ (1...𝐽) ∧ ((𝐹‘𝐶)‘(𝑘 + 1)) ≤ 0))
135		breq1 5117	. . . . . . . . . . . . 13 ⊢ (𝑗 = (𝑘 + 1) → (𝑗 ≤ 𝑘 ↔ (𝑘 + 1) ≤ 𝑘))
136	135	rspccva 3583	. . . . . . . . . . . 12 ⊢ ((∀𝑗 ∈ {𝑖 ∈ (1...𝐽) ∣ ((𝐹‘𝐶)‘𝑖) ≤ 0}𝑗 ≤ 𝑘 ∧ (𝑘 + 1) ∈ {𝑖 ∈ (1...𝐽) ∣ ((𝐹‘𝐶)‘𝑖) ≤ 0}) → (𝑘 + 1) ≤ 𝑘)
137	134, 136	sylan2br 607	. . . . . . . . . . 11 ⊢ ((∀𝑗 ∈ {𝑖 ∈ (1...𝐽) ∣ ((𝐹‘𝐶)‘𝑖) ≤ 0}𝑗 ≤ 𝑘 ∧ ((𝑘 + 1) ∈ (1...𝐽) ∧ ((𝐹‘𝐶)‘(𝑘 + 1)) ≤ 0)) → (𝑘 + 1) ≤ 𝑘)
138	137	expr 462	. . . . . . . . . 10 ⊢ ((∀𝑗 ∈ {𝑖 ∈ (1...𝐽) ∣ ((𝐹‘𝐶)‘𝑖) ≤ 0}𝑗 ≤ 𝑘 ∧ (𝑘 + 1) ∈ (1...𝐽)) → (((𝐹‘𝐶)‘(𝑘 + 1)) ≤ 0 → (𝑘 + 1) ≤ 𝑘))
139	138	con3d 153	. . . . . . . . 9 ⊢ ((∀𝑗 ∈ {𝑖 ∈ (1...𝐽) ∣ ((𝐹‘𝐶)‘𝑖) ≤ 0}𝑗 ≤ 𝑘 ∧ (𝑘 + 1) ∈ (1...𝐽)) → (¬ (𝑘 + 1) ≤ 𝑘 → ¬ ((𝐹‘𝐶)‘(𝑘 + 1)) ≤ 0))
140	20, 131, 139	syl2anc 596	. . . . . . . 8 ⊢ ((𝜑 ∧ ((𝑘 ∈ (1...𝐽) ∧ ((𝐹‘𝐶)‘𝑘) ≤ 0) ∧ ∀𝑗 ∈ {𝑖 ∈ (1...𝐽) ∣ ((𝐹‘𝐶)‘𝑖) ≤ 0}𝑗 ≤ 𝑘)) → (¬ (𝑘 + 1) ≤ 𝑘 → ¬ ((𝐹‘𝐶)‘(𝑘 + 1)) ≤ 0))
141	19, 140	mpd 16	. . . . . . 7 ⊢ ((𝜑 ∧ ((𝑘 ∈ (1...𝐽) ∧ ((𝐹‘𝐶)‘𝑘) ≤ 0) ∧ ∀𝑗 ∈ {𝑖 ∈ (1...𝐽) ∣ ((𝐹‘𝐶)‘𝑖) ≤ 0}𝑗 ≤ 𝑘)) → ¬ ((𝐹‘𝐶)‘(𝑘 + 1)) ≤ 0)
142		simplrr 790	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ ((𝑘 ∈ (1...𝐽) ∧ ((𝐹‘𝐶)‘𝑘) ≤ 0) ∧ ∀𝑗 ∈ {𝑖 ∈ (1...𝐽) ∣ ((𝐹‘𝐶)‘𝑖) ≤ 0}𝑗 ≤ 𝑘)) ∧ ¬ (𝑘 + 1) ∈ 𝐶) → ∀𝑗 ∈ {𝑖 ∈ (1...𝐽) ∣ ((𝐹‘𝐶)‘𝑖) ≤ 0}𝑗 ≤ 𝑘)
143	131	adantr 486	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ ((𝑘 ∈ (1...𝐽) ∧ ((𝐹‘𝐶)‘𝑘) ≤ 0) ∧ ∀𝑗 ∈ {𝑖 ∈ (1...𝐽) ∣ ((𝐹‘𝐶)‘𝑖) ≤ 0}𝑗 ≤ 𝑘)) ∧ ¬ (𝑘 + 1) ∈ 𝐶) → (𝑘 + 1) ∈ (1...𝐽))
144		simpll 779	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (𝑘 ∈ (1...𝐽) ∧ ((𝐹‘𝐶)‘𝑘) ≤ 0)) ∧ ¬ (𝑘 + 1) ∈ 𝐶) → 𝜑)
145	130	adantr 486	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ (𝑘 ∈ (1...𝐽) ∧ ((𝐹‘𝐶)‘𝑘) ≤ 0)) ∧ ¬ (𝑘 + 1) ∈ 𝐶) → (𝑘 + 1) ∈ (1...𝐽))
146	35	sseld 3939	. . . . . . . . . . . . . . 15 ⊢ (1 ∈ (ℤ_≥‘0) → ((𝑘 + 1) ∈ (1...𝐽) → (𝑘 + 1) ∈ (0...𝐽)))
147	34, 145, 146	mpsyl 69	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (𝑘 ∈ (1...𝐽) ∧ ((𝐹‘𝐶)‘𝑘) ≤ 0)) ∧ ¬ (𝑘 + 1) ∈ 𝐶) → (𝑘 + 1) ∈ (0...𝐽))
148	44	adantr 486	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ (𝑘 + 1) ∈ (0...𝐽)) → 𝐶 ∈ 𝑂)
149		elfzelz 13570	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑘 + 1) ∈ (0...𝐽) → (𝑘 + 1) ∈ ℤ)
150	149	adantl 487	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ (𝑘 + 1) ∈ (0...𝐽)) → (𝑘 + 1) ∈ ℤ)
151	39, 40, 41, 42, 43, 148, 150	ballotlemfelz 34913	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ (𝑘 + 1) ∈ (0...𝐽)) → ((𝐹‘𝐶)‘(𝑘 + 1)) ∈ ℤ)
152	151	zred 12718	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑘 + 1) ∈ (0...𝐽)) → ((𝐹‘𝐶)‘(𝑘 + 1)) ∈ ℝ)
153	144, 147, 152	syl2anc 596	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑘 ∈ (1...𝐽) ∧ ((𝐹‘𝐶)‘𝑘) ≤ 0)) ∧ ¬ (𝑘 + 1) ∈ 𝐶) → ((𝐹‘𝐶)‘(𝑘 + 1)) ∈ ℝ)
154		0red 11229	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑘 ∈ (1...𝐽) ∧ ((𝐹‘𝐶)‘𝑘) ≤ 0)) ∧ ¬ (𝑘 + 1) ∈ 𝐶) → 0 ∈ ℝ)
155		simplrr 790	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (𝑘 ∈ (1...𝐽) ∧ ((𝐹‘𝐶)‘𝑘) ≤ 0)) ∧ ¬ (𝑘 + 1) ∈ 𝐶) → ((𝐹‘𝐶)‘𝑘) ≤ 0)
156	6	adantr 486	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ (𝑘 ∈ (1...𝐽) ∧ ((𝐹‘𝐶)‘𝑘) ≤ 0)) ∧ ¬ (𝑘 + 1) ∈ 𝐶) → 𝑘 ∈ (1...𝐽))
157	156, 37	syl 18	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ (𝑘 ∈ (1...𝐽) ∧ ((𝐹‘𝐶)‘𝑘) ≤ 0)) ∧ ¬ (𝑘 + 1) ∈ 𝐶) → 𝑘 ∈ (0...𝐽))
158	129	imdistani 579	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ (𝑘 ∈ (1...𝐽) ∧ ((𝐹‘𝐶)‘𝑘) ≤ 0)) → (𝜑 ∧ (𝑘 + 1) ∈ (1...𝐽)))
159	44	adantr 486	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ (𝑘 + 1) ∈ (1...𝐽)) → 𝐶 ∈ 𝑂)
160		elfznn 13600	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑘 + 1) ∈ (1...𝐽) → (𝑘 + 1) ∈ ℕ)
161	160	adantl 487	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ (𝑘 + 1) ∈ (1...𝐽)) → (𝑘 + 1) ∈ ℕ)
162	39, 40, 41, 42, 43, 159, 161	ballotlemfp1 34914	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ (𝑘 + 1) ∈ (1...𝐽)) → ((¬ (𝑘 + 1) ∈ 𝐶 → ((𝐹‘𝐶)‘(𝑘 + 1)) = (((𝐹‘𝐶)‘((𝑘 + 1) − 1)) − 1)) ∧ ((𝑘 + 1) ∈ 𝐶 → ((𝐹‘𝐶)‘(𝑘 + 1)) = (((𝐹‘𝐶)‘((𝑘 + 1) − 1)) + 1))))
163	162	simpld 500	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ (𝑘 + 1) ∈ (1...𝐽)) → (¬ (𝑘 + 1) ∈ 𝐶 → ((𝐹‘𝐶)‘(𝑘 + 1)) = (((𝐹‘𝐶)‘((𝑘 + 1) − 1)) − 1)))
164	163	imp 412	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ (𝑘 + 1) ∈ (1...𝐽)) ∧ ¬ (𝑘 + 1) ∈ 𝐶) → ((𝐹‘𝐶)‘(𝑘 + 1)) = (((𝐹‘𝐶)‘((𝑘 + 1) − 1)) − 1))
165	158, 164	sylan 592	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ (𝑘 ∈ (1...𝐽) ∧ ((𝐹‘𝐶)‘𝑘) ≤ 0)) ∧ ¬ (𝑘 + 1) ∈ 𝐶) → ((𝐹‘𝐶)‘(𝑘 + 1)) = (((𝐹‘𝐶)‘((𝑘 + 1) − 1)) − 1))
166		elfzelz 13570	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑘 ∈ (1...𝐽) → 𝑘 ∈ ℤ)
167	166	zcnd 12719	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑘 ∈ (1...𝐽) → 𝑘 ∈ ℂ)
168		1cnd 11220	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑘 ∈ (1...𝐽) → 1 ∈ ℂ)
169	167, 168	pncand 11588	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑘 ∈ (1...𝐽) → ((𝑘 + 1) − 1) = 𝑘)
170	169	fveq2d 6892	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑘 ∈ (1...𝐽) → ((𝐹‘𝐶)‘((𝑘 + 1) − 1)) = ((𝐹‘𝐶)‘𝑘))
171	170	oveq1d 7438	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑘 ∈ (1...𝐽) → (((𝐹‘𝐶)‘((𝑘 + 1) − 1)) − 1) = (((𝐹‘𝐶)‘𝑘) − 1))
172	171	eqeq2d 2777	. . . . . . . . . . . . . . . . 17 ⊢ (𝑘 ∈ (1...𝐽) → (((𝐹‘𝐶)‘(𝑘 + 1)) = (((𝐹‘𝐶)‘((𝑘 + 1) − 1)) − 1) ↔ ((𝐹‘𝐶)‘(𝑘 + 1)) = (((𝐹‘𝐶)‘𝑘) − 1)))
173	156, 172	syl 18	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ (𝑘 ∈ (1...𝐽) ∧ ((𝐹‘𝐶)‘𝑘) ≤ 0)) ∧ ¬ (𝑘 + 1) ∈ 𝐶) → (((𝐹‘𝐶)‘(𝑘 + 1)) = (((𝐹‘𝐶)‘((𝑘 + 1) − 1)) − 1) ↔ ((𝐹‘𝐶)‘(𝑘 + 1)) = (((𝐹‘𝐶)‘𝑘) − 1)))
174	165, 173	mpbid 235	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ (𝑘 ∈ (1...𝐽) ∧ ((𝐹‘𝐶)‘𝑘) ≤ 0)) ∧ ¬ (𝑘 + 1) ∈ 𝐶) → ((𝐹‘𝐶)‘(𝑘 + 1)) = (((𝐹‘𝐶)‘𝑘) − 1))
175		0z 12620	. . . . . . . . . . . . . . . . . 18 ⊢ 0 ∈ ℤ
176		zlem1lt 12664	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝐹‘𝐶)‘𝑘) ∈ ℤ ∧ 0 ∈ ℤ) → (((𝐹‘𝐶)‘𝑘) ≤ 0 ↔ (((𝐹‘𝐶)‘𝑘) − 1) < 0))
177	48, 175, 176	sylancl 598	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝐽)) → (((𝐹‘𝐶)‘𝑘) ≤ 0 ↔ (((𝐹‘𝐶)‘𝑘) − 1) < 0))
178	177	adantr 486	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑘 ∈ (0...𝐽)) ∧ ((𝐹‘𝐶)‘(𝑘 + 1)) = (((𝐹‘𝐶)‘𝑘) − 1)) → (((𝐹‘𝐶)‘𝑘) ≤ 0 ↔ (((𝐹‘𝐶)‘𝑘) − 1) < 0))
179		breq1 5117	. . . . . . . . . . . . . . . . 17 ⊢ (((𝐹‘𝐶)‘(𝑘 + 1)) = (((𝐹‘𝐶)‘𝑘) − 1) → (((𝐹‘𝐶)‘(𝑘 + 1)) < 0 ↔ (((𝐹‘𝐶)‘𝑘) − 1) < 0))
180	179	adantl 487	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑘 ∈ (0...𝐽)) ∧ ((𝐹‘𝐶)‘(𝑘 + 1)) = (((𝐹‘𝐶)‘𝑘) − 1)) → (((𝐹‘𝐶)‘(𝑘 + 1)) < 0 ↔ (((𝐹‘𝐶)‘𝑘) − 1) < 0))
181	178, 180	bitr4d 285	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑘 ∈ (0...𝐽)) ∧ ((𝐹‘𝐶)‘(𝑘 + 1)) = (((𝐹‘𝐶)‘𝑘) − 1)) → (((𝐹‘𝐶)‘𝑘) ≤ 0 ↔ ((𝐹‘𝐶)‘(𝑘 + 1)) < 0))
182	144, 157, 174, 181	syl21anc 851	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (𝑘 ∈ (1...𝐽) ∧ ((𝐹‘𝐶)‘𝑘) ≤ 0)) ∧ ¬ (𝑘 + 1) ∈ 𝐶) → (((𝐹‘𝐶)‘𝑘) ≤ 0 ↔ ((𝐹‘𝐶)‘(𝑘 + 1)) < 0))
183	155, 182	mpbid 235	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑘 ∈ (1...𝐽) ∧ ((𝐹‘𝐶)‘𝑘) ≤ 0)) ∧ ¬ (𝑘 + 1) ∈ 𝐶) → ((𝐹‘𝐶)‘(𝑘 + 1)) < 0)
184	153, 154, 183	ltled 11376	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝑘 ∈ (1...𝐽) ∧ ((𝐹‘𝐶)‘𝑘) ≤ 0)) ∧ ¬ (𝑘 + 1) ∈ 𝐶) → ((𝐹‘𝐶)‘(𝑘 + 1)) ≤ 0)
185	184	adantlrr 734	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ ((𝑘 ∈ (1...𝐽) ∧ ((𝐹‘𝐶)‘𝑘) ≤ 0) ∧ ∀𝑗 ∈ {𝑖 ∈ (1...𝐽) ∣ ((𝐹‘𝐶)‘𝑖) ≤ 0}𝑗 ≤ 𝑘)) ∧ ¬ (𝑘 + 1) ∈ 𝐶) → ((𝐹‘𝐶)‘(𝑘 + 1)) ≤ 0)
186	142, 143, 185, 137	syl12anc 850	. . . . . . . . . 10 ⊢ (((𝜑 ∧ ((𝑘 ∈ (1...𝐽) ∧ ((𝐹‘𝐶)‘𝑘) ≤ 0) ∧ ∀𝑗 ∈ {𝑖 ∈ (1...𝐽) ∣ ((𝐹‘𝐶)‘𝑖) ≤ 0}𝑗 ≤ 𝑘)) ∧ ¬ (𝑘 + 1) ∈ 𝐶) → (𝑘 + 1) ≤ 𝑘)
187	19	adantr 486	. . . . . . . . . 10 ⊢ (((𝜑 ∧ ((𝑘 ∈ (1...𝐽) ∧ ((𝐹‘𝐶)‘𝑘) ≤ 0) ∧ ∀𝑗 ∈ {𝑖 ∈ (1...𝐽) ∣ ((𝐹‘𝐶)‘𝑖) ≤ 0}𝑗 ≤ 𝑘)) ∧ ¬ (𝑘 + 1) ∈ 𝐶) → ¬ (𝑘 + 1) ≤ 𝑘)
188	186, 187	condan 830	. . . . . . . . 9 ⊢ ((𝜑 ∧ ((𝑘 ∈ (1...𝐽) ∧ ((𝐹‘𝐶)‘𝑘) ≤ 0) ∧ ∀𝑗 ∈ {𝑖 ∈ (1...𝐽) ∣ ((𝐹‘𝐶)‘𝑖) ≤ 0}𝑗 ≤ 𝑘)) → (𝑘 + 1) ∈ 𝐶)
189	162	simprd 501	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑘 + 1) ∈ (1...𝐽)) → ((𝑘 + 1) ∈ 𝐶 → ((𝐹‘𝐶)‘(𝑘 + 1)) = (((𝐹‘𝐶)‘((𝑘 + 1) − 1)) + 1)))
190	189	imp 412	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝑘 + 1) ∈ (1...𝐽)) ∧ (𝑘 + 1) ∈ 𝐶) → ((𝐹‘𝐶)‘(𝑘 + 1)) = (((𝐹‘𝐶)‘((𝑘 + 1) − 1)) + 1))
191	158, 190	sylan 592	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝑘 ∈ (1...𝐽) ∧ ((𝐹‘𝐶)‘𝑘) ≤ 0)) ∧ (𝑘 + 1) ∈ 𝐶) → ((𝐹‘𝐶)‘(𝑘 + 1)) = (((𝐹‘𝐶)‘((𝑘 + 1) − 1)) + 1))
192	6	adantr 486	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝑘 ∈ (1...𝐽) ∧ ((𝐹‘𝐶)‘𝑘) ≤ 0)) ∧ (𝑘 + 1) ∈ 𝐶) → 𝑘 ∈ (1...𝐽))
193	170	oveq1d 7438	. . . . . . . . . . . . 13 ⊢ (𝑘 ∈ (1...𝐽) → (((𝐹‘𝐶)‘((𝑘 + 1) − 1)) + 1) = (((𝐹‘𝐶)‘𝑘) + 1))
194	193	eqeq2d 2777	. . . . . . . . . . . 12 ⊢ (𝑘 ∈ (1...𝐽) → (((𝐹‘𝐶)‘(𝑘 + 1)) = (((𝐹‘𝐶)‘((𝑘 + 1) − 1)) + 1) ↔ ((𝐹‘𝐶)‘(𝑘 + 1)) = (((𝐹‘𝐶)‘𝑘) + 1)))
195	192, 194	syl 18	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝑘 ∈ (1...𝐽) ∧ ((𝐹‘𝐶)‘𝑘) ≤ 0)) ∧ (𝑘 + 1) ∈ 𝐶) → (((𝐹‘𝐶)‘(𝑘 + 1)) = (((𝐹‘𝐶)‘((𝑘 + 1) − 1)) + 1) ↔ ((𝐹‘𝐶)‘(𝑘 + 1)) = (((𝐹‘𝐶)‘𝑘) + 1)))
196	191, 195	mpbid 235	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝑘 ∈ (1...𝐽) ∧ ((𝐹‘𝐶)‘𝑘) ≤ 0)) ∧ (𝑘 + 1) ∈ 𝐶) → ((𝐹‘𝐶)‘(𝑘 + 1)) = (((𝐹‘𝐶)‘𝑘) + 1))
197	196	adantlrr 734	. . . . . . . . 9 ⊢ (((𝜑 ∧ ((𝑘 ∈ (1...𝐽) ∧ ((𝐹‘𝐶)‘𝑘) ≤ 0) ∧ ∀𝑗 ∈ {𝑖 ∈ (1...𝐽) ∣ ((𝐹‘𝐶)‘𝑖) ≤ 0}𝑗 ≤ 𝑘)) ∧ (𝑘 + 1) ∈ 𝐶) → ((𝐹‘𝐶)‘(𝑘 + 1)) = (((𝐹‘𝐶)‘𝑘) + 1))
198	188, 197	mpdan 700	. . . . . . . 8 ⊢ ((𝜑 ∧ ((𝑘 ∈ (1...𝐽) ∧ ((𝐹‘𝐶)‘𝑘) ≤ 0) ∧ ∀𝑗 ∈ {𝑖 ∈ (1...𝐽) ∣ ((𝐹‘𝐶)‘𝑖) ≤ 0}𝑗 ≤ 𝑘)) → ((𝐹‘𝐶)‘(𝑘 + 1)) = (((𝐹‘𝐶)‘𝑘) + 1))
199		breq1 5117	. . . . . . . . 9 ⊢ (((𝐹‘𝐶)‘(𝑘 + 1)) = (((𝐹‘𝐶)‘𝑘) + 1) → (((𝐹‘𝐶)‘(𝑘 + 1)) ≤ 0 ↔ (((𝐹‘𝐶)‘𝑘) + 1) ≤ 0))
200	199	notbid 321	. . . . . . . 8 ⊢ (((𝐹‘𝐶)‘(𝑘 + 1)) = (((𝐹‘𝐶)‘𝑘) + 1) → (¬ ((𝐹‘𝐶)‘(𝑘 + 1)) ≤ 0 ↔ ¬ (((𝐹‘𝐶)‘𝑘) + 1) ≤ 0))
201	198, 200	syl 18	. . . . . . 7 ⊢ ((𝜑 ∧ ((𝑘 ∈ (1...𝐽) ∧ ((𝐹‘𝐶)‘𝑘) ≤ 0) ∧ ∀𝑗 ∈ {𝑖 ∈ (1...𝐽) ∣ ((𝐹‘𝐶)‘𝑖) ≤ 0}𝑗 ≤ 𝑘)) → (¬ ((𝐹‘𝐶)‘(𝑘 + 1)) ≤ 0 ↔ ¬ (((𝐹‘𝐶)‘𝑘) + 1) ≤ 0))
202	141, 201	mpbid 235	. . . . . 6 ⊢ ((𝜑 ∧ ((𝑘 ∈ (1...𝐽) ∧ ((𝐹‘𝐶)‘𝑘) ≤ 0) ∧ ∀𝑗 ∈ {𝑖 ∈ (1...𝐽) ∣ ((𝐹‘𝐶)‘𝑖) ≤ 0}𝑗 ≤ 𝑘)) → ¬ (((𝐹‘𝐶)‘𝑘) + 1) ≤ 0)
203	6, 37	syl 18	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑘 ∈ (1...𝐽) ∧ ((𝐹‘𝐶)‘𝑘) ≤ 0)) → 𝑘 ∈ (0...𝐽))
204	203, 48	syldan 603	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑘 ∈ (1...𝐽) ∧ ((𝐹‘𝐶)‘𝑘) ≤ 0)) → ((𝐹‘𝐶)‘𝑘) ∈ ℤ)
205	204	adantrr 730	. . . . . . 7 ⊢ ((𝜑 ∧ ((𝑘 ∈ (1...𝐽) ∧ ((𝐹‘𝐶)‘𝑘) ≤ 0) ∧ ∀𝑗 ∈ {𝑖 ∈ (1...𝐽) ∣ ((𝐹‘𝐶)‘𝑖) ≤ 0}𝑗 ≤ 𝑘)) → ((𝐹‘𝐶)‘𝑘) ∈ ℤ)
206		zleltp1 12663	. . . . . . . . 9 ⊢ ((0 ∈ ℤ ∧ ((𝐹‘𝐶)‘𝑘) ∈ ℤ) → (0 ≤ ((𝐹‘𝐶)‘𝑘) ↔ 0 < (((𝐹‘𝐶)‘𝑘) + 1)))
207	175, 206	mpan 703	. . . . . . . 8 ⊢ (((𝐹‘𝐶)‘𝑘) ∈ ℤ → (0 ≤ ((𝐹‘𝐶)‘𝑘) ↔ 0 < (((𝐹‘𝐶)‘𝑘) + 1)))
208		0red 11229	. . . . . . . . 9 ⊢ (((𝐹‘𝐶)‘𝑘) ∈ ℤ → 0 ∈ ℝ)
209		zre 12613	. . . . . . . . . 10 ⊢ (((𝐹‘𝐶)‘𝑘) ∈ ℤ → ((𝐹‘𝐶)‘𝑘) ∈ ℝ)
210		1red 11227	. . . . . . . . . 10 ⊢ (((𝐹‘𝐶)‘𝑘) ∈ ℤ → 1 ∈ ℝ)
211	209, 210	readdcld 11256	. . . . . . . . 9 ⊢ (((𝐹‘𝐶)‘𝑘) ∈ ℤ → (((𝐹‘𝐶)‘𝑘) + 1) ∈ ℝ)
212	208, 211	ltnled 11375	. . . . . . . 8 ⊢ (((𝐹‘𝐶)‘𝑘) ∈ ℤ → (0 < (((𝐹‘𝐶)‘𝑘) + 1) ↔ ¬ (((𝐹‘𝐶)‘𝑘) + 1) ≤ 0))
213	207, 212	bitrd 282	. . . . . . 7 ⊢ (((𝐹‘𝐶)‘𝑘) ∈ ℤ → (0 ≤ ((𝐹‘𝐶)‘𝑘) ↔ ¬ (((𝐹‘𝐶)‘𝑘) + 1) ≤ 0))
214	205, 213	syl 18	. . . . . 6 ⊢ ((𝜑 ∧ ((𝑘 ∈ (1...𝐽) ∧ ((𝐹‘𝐶)‘𝑘) ≤ 0) ∧ ∀𝑗 ∈ {𝑖 ∈ (1...𝐽) ∣ ((𝐹‘𝐶)‘𝑖) ≤ 0}𝑗 ≤ 𝑘)) → (0 ≤ ((𝐹‘𝐶)‘𝑘) ↔ ¬ (((𝐹‘𝐶)‘𝑘) + 1) ≤ 0))
215	202, 214	mpbird 260	. . . . 5 ⊢ ((𝜑 ∧ ((𝑘 ∈ (1...𝐽) ∧ ((𝐹‘𝐶)‘𝑘) ≤ 0) ∧ ∀𝑗 ∈ {𝑖 ∈ (1...𝐽) ∣ ((𝐹‘𝐶)‘𝑖) ≤ 0}𝑗 ≤ 𝑘)) → 0 ≤ ((𝐹‘𝐶)‘𝑘))
216	205	zred 12718	. . . . . 6 ⊢ ((𝜑 ∧ ((𝑘 ∈ (1...𝐽) ∧ ((𝐹‘𝐶)‘𝑘) ≤ 0) ∧ ∀𝑗 ∈ {𝑖 ∈ (1...𝐽) ∣ ((𝐹‘𝐶)‘𝑖) ≤ 0}𝑗 ≤ 𝑘)) → ((𝐹‘𝐶)‘𝑘) ∈ ℝ)
217		0red 11229	. . . . . 6 ⊢ ((𝜑 ∧ ((𝑘 ∈ (1...𝐽) ∧ ((𝐹‘𝐶)‘𝑘) ≤ 0) ∧ ∀𝑗 ∈ {𝑖 ∈ (1...𝐽) ∣ ((𝐹‘𝐶)‘𝑖) ≤ 0}𝑗 ≤ 𝑘)) → 0 ∈ ℝ)
218	216, 217	letri3d 11370	. . . . 5 ⊢ ((𝜑 ∧ ((𝑘 ∈ (1...𝐽) ∧ ((𝐹‘𝐶)‘𝑘) ≤ 0) ∧ ∀𝑗 ∈ {𝑖 ∈ (1...𝐽) ∣ ((𝐹‘𝐶)‘𝑖) ≤ 0}𝑗 ≤ 𝑘)) → (((𝐹‘𝐶)‘𝑘) = 0 ↔ (((𝐹‘𝐶)‘𝑘) ≤ 0 ∧ 0 ≤ ((𝐹‘𝐶)‘𝑘))))
219	5, 215, 218	mpbir2and 726	. . . 4 ⊢ ((𝜑 ∧ ((𝑘 ∈ (1...𝐽) ∧ ((𝐹‘𝐶)‘𝑘) ≤ 0) ∧ ∀𝑗 ∈ {𝑖 ∈ (1...𝐽) ∣ ((𝐹‘𝐶)‘𝑖) ≤ 0}𝑗 ≤ 𝑘)) → ((𝐹‘𝐶)‘𝑘) = 0)
220	4, 219	sylan2b 606	. . 3 ⊢ ((𝜑 ∧ (𝑘 ∈ {𝑖 ∈ (1...𝐽) ∣ ((𝐹‘𝐶)‘𝑖) ≤ 0} ∧ ∀𝑗 ∈ {𝑖 ∈ (1...𝐽) ∣ ((𝐹‘𝐶)‘𝑖) ≤ 0}𝑗 ≤ 𝑘)) → ((𝐹‘𝐶)‘𝑘) = 0)
221		ssrab2 4037	. . . . . 6 ⊢ {𝑖 ∈ (1...𝐽) ∣ ((𝐹‘𝐶)‘𝑖) ≤ 0} ⊆ (1...𝐽)
222	221, 12	sstri 3949	. . . . 5 ⊢ {𝑖 ∈ (1...𝐽) ∣ ((𝐹‘𝐶)‘𝑖) ≤ 0} ⊆ ℝ
223	222	a1i 11	. . . 4 ⊢ (𝜑 → {𝑖 ∈ (1...𝐽) ∣ ((𝐹‘𝐶)‘𝑖) ≤ 0} ⊆ ℝ)
224		fzfi 14028	. . . . . 6 ⊢ (1...𝐽) ∈ Fin
225		ssfi 9167	. . . . . 6 ⊢ (((1...𝐽) ∈ Fin ∧ {𝑖 ∈ (1...𝐽) ∣ ((𝐹‘𝐶)‘𝑖) ≤ 0} ⊆ (1...𝐽)) → {𝑖 ∈ (1...𝐽) ∣ ((𝐹‘𝐶)‘𝑖) ≤ 0} ∈ Fin)
226	224, 221, 225	mp2an 705	. . . . 5 ⊢ {𝑖 ∈ (1...𝐽) ∣ ((𝐹‘𝐶)‘𝑖) ≤ 0} ∈ Fin
227	226	a1i 11	. . . 4 ⊢ (𝜑 → {𝑖 ∈ (1...𝐽) ∣ ((𝐹‘𝐶)‘𝑖) ≤ 0} ∈ Fin)
228		rabn0 4349	. . . . 5 ⊢ ({𝑖 ∈ (1...𝐽) ∣ ((𝐹‘𝐶)‘𝑖) ≤ 0} ≠ ∅ ↔ ∃𝑖 ∈ (1...𝐽)((𝐹‘𝐶)‘𝑖) ≤ 0)
229	60, 228	sylibr 237	. . . 4 ⊢ (𝜑 → {𝑖 ∈ (1...𝐽) ∣ ((𝐹‘𝐶)‘𝑖) ≤ 0} ≠ ∅)
230		fimaxre 12177	. . . 4 ⊢ (({𝑖 ∈ (1...𝐽) ∣ ((𝐹‘𝐶)‘𝑖) ≤ 0} ⊆ ℝ ∧ {𝑖 ∈ (1...𝐽) ∣ ((𝐹‘𝐶)‘𝑖) ≤ 0} ∈ Fin ∧ {𝑖 ∈ (1...𝐽) ∣ ((𝐹‘𝐶)‘𝑖) ≤ 0} ≠ ∅) → ∃𝑘 ∈ {𝑖 ∈ (1...𝐽) ∣ ((𝐹‘𝐶)‘𝑖) ≤ 0}∀𝑗 ∈ {𝑖 ∈ (1...𝐽) ∣ ((𝐹‘𝐶)‘𝑖) ≤ 0}𝑗 ≤ 𝑘)
231	223, 227, 229, 230	syl3anc 1398	. . 3 ⊢ (𝜑 → ∃𝑘 ∈ {𝑖 ∈ (1...𝐽) ∣ ((𝐹‘𝐶)‘𝑖) ≤ 0}∀𝑗 ∈ {𝑖 ∈ (1...𝐽) ∣ ((𝐹‘𝐶)‘𝑖) ≤ 0}𝑗 ≤ 𝑘)
232	220, 231	reximddv 3184	. 2 ⊢ (𝜑 → ∃𝑘 ∈ {𝑖 ∈ (1...𝐽) ∣ ((𝐹‘𝐶)‘𝑖) ≤ 0} ((𝐹‘𝐶)‘𝑘) = 0)
233		elrabi 3649	. . . 4 ⊢ (𝑘 ∈ {𝑖 ∈ (1...𝐽) ∣ ((𝐹‘𝐶)‘𝑖) ≤ 0} → 𝑘 ∈ (1...𝐽))
234	233	anim1i 627	. . 3 ⊢ ((𝑘 ∈ {𝑖 ∈ (1...𝐽) ∣ ((𝐹‘𝐶)‘𝑖) ≤ 0} ∧ ((𝐹‘𝐶)‘𝑘) = 0) → (𝑘 ∈ (1...𝐽) ∧ ((𝐹‘𝐶)‘𝑘) = 0))
235	234	reximi2 3101	. 2 ⊢ (∃𝑘 ∈ {𝑖 ∈ (1...𝐽) ∣ ((𝐹‘𝐶)‘𝑖) ≤ 0} ((𝐹‘𝐶)‘𝑘) = 0 → ∃𝑘 ∈ (1...𝐽)((𝐹‘𝐶)‘𝑘) = 0)
236	232, 235	syl 18	1 ⊢ (𝜑 → ∃𝑘 ∈ (1...𝐽)((𝐹‘𝐶)‘𝑘) = 0)

Colors of variables: wff setvar class

This proof depends on syntax axioms: ¬ wn 3 → wi 4 ↔ wb 209 ∧ wa 401 ∨ wo 861 = wceq 1570 ∈ wcel 2146 ≠ wne 2961 ∀wral 3082 ∃wrex 3092 {crab 3419 ∖ cdif 3905 ∩ cin 3907 ⊆ wss 3908 ∅c0 4289 𝒫 cpw 4567 {csn 4594 class class class wbr 5114 ↦ cmpt 5197 ‘cfv 6543 (class class class)co 7423 Fincfn 8952 ℝcr 11117 0cc0 11118 1c1 11119 + caddc 11121 < clt 11261 ≤ cle 11262 − cmin 11459 / cdiv 11889 ℕcn 12251 2c2 12313 ℤcz 12609 ℤ_≥cuz 12880 ...cfz 13553 ♯chash 14386

This proof depends on axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1828 ax-4 1842 ax-5 1943 ax-6 2000 ax-7 2041 ax-8 2148 ax-9 2156 ax-10 2179 ax-11 2195 ax-12 2216 ax-ext 2738 ax-rep 5243 ax-sep 5262 ax-nul 5274 ax-pow 5341 ax-pr 5409 ax-un 7745 ax-cnex 11174 ax-resscn 11175 ax-1cn 11176 ax-icn 11177 ax-addcl 11178 ax-addrcl 11179 ax-mulcl 11180 ax-mulrcl 11181 ax-mulcom 11182 ax-addass 11183 ax-mulass 11184 ax-distr 11185 ax-i2m1 11186 ax-1ne0 11187 ax-1rid 11188 ax-rnegex 11189 ax-rrecex 11190 ax-cnre 11191 ax-pre-lttri 11192 ax-pre-lttrn 11193 ax-pre-ltadd 11194 ax-pre-mulgt0 11195

This proof depends on definitions: df-bi 210 df-an 402 df-or 862 df-3or 1104 df-3an 1105 df-tru 1573 df-fal 1583 df-ex 1813 df-nf 1817 df-sb 2100 df-mo 2570 df-eu 2600 df-clab 2745 df-cleq 2758 df-clel 2841 df-nfc 2915 df-ne 2962 df-nel 3068 df-ral 3083 df-rex 3093 df-reu 3373 df-rab 3420 df-v 3460 df-sbc 3748 df-csb 3857 df-dif 3911 df-un 3913 df-in 3915 df-ss 3925 df-pss 3928 df-nul 4290 df-if 4493 df-pw 4569 df-sn 4595 df-pr 4597 df-op 4601 df-uni 4878 df-int 4918 df-iun 4963 df-br 5115 df-opab 5179 df-mpt 5198 df-tr 5224 df-id 5561 df-eprel 5566 df-po 5574 df-so 5575 df-fr 5619 df-we 5621 df-xp 5672 df-rel 5673 df-cnv 5674 df-co 5675 df-dm 5676 df-rn 5677 df-res 5678 df-ima 5679 df-pred 6309 df-ord 6370 df-on 6371 df-lim 6372 df-suc 6373 df-iota 6499 df-fun 6545 df-fn 6546 df-f 6547 df-f1 6548 df-fo 6549 df-f1o 6550 df-fv 6551 df-riota 7380 df-ov 7426 df-oprab 7427 df-mpo 7428 df-om 7872 df-1st 7995 df-2nd 7996 df-frecs 8287 df-wrecs 8318 df-recs 8367 df-rdg 8406 df-1o 8462 df-oadd 8466 df-er 8703 df-en 8953 df-dom 8954 df-sdom 8955 df-fin 8956 df-dju 9906 df-card 9944 df-pnf 11263 df-mnf 11264 df-xr 11265 df-ltxr 11266 df-le 11267 df-sub 11461 df-neg 11462 df-nn 12252 df-2 12321 df-n0 12523 df-z 12610 df-uz 12881 df-fz 13554 df-hash 14387

This theorem is used by: ballotlem5 34922 ballotlemic 34929

W3C validator