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 32171

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 6717	. . . . . . 7 ⊢ (𝑖 = 𝑘 → ((𝐹‘𝐶)‘𝑖) = ((𝐹‘𝐶)‘𝑘))
2	1	breq1d 5063	. . . . . 6 ⊢ (𝑖 = 𝑘 → (((𝐹‘𝐶)‘𝑖) ≤ 0 ↔ ((𝐹‘𝐶)‘𝑘) ≤ 0))
3	2	elrab 3602	. . . . 5 ⊢ (𝑘 ∈ {𝑖 ∈ (1...𝐽) ∣ ((𝐹‘𝐶)‘𝑖) ≤ 0} ↔ (𝑘 ∈ (1...𝐽) ∧ ((𝐹‘𝐶)‘𝑘) ≤ 0))
4	3	anbi1i 627	. . . 4 ⊢ ((𝑘 ∈ {𝑖 ∈ (1...𝐽) ∣ ((𝐹‘𝐶)‘𝑖) ≤ 0} ∧ ∀𝑗 ∈ {𝑖 ∈ (1...𝐽) ∣ ((𝐹‘𝐶)‘𝑖) ≤ 0}𝑗 ≤ 𝑘) ↔ ((𝑘 ∈ (1...𝐽) ∧ ((𝐹‘𝐶)‘𝑘) ≤ 0) ∧ ∀𝑗 ∈ {𝑖 ∈ (1...𝐽) ∣ ((𝐹‘𝐶)‘𝑖) ≤ 0}𝑗 ≤ 𝑘))
5		simprlr 780	. . . . 5 ⊢ ((𝜑 ∧ ((𝑘 ∈ (1...𝐽) ∧ ((𝐹‘𝐶)‘𝑘) ≤ 0) ∧ ∀𝑗 ∈ {𝑖 ∈ (1...𝐽) ∣ ((𝐹‘𝐶)‘𝑖) ≤ 0}𝑗 ≤ 𝑘)) → ((𝐹‘𝐶)‘𝑘) ≤ 0)
6		simprl 771	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑘 ∈ (1...𝐽) ∧ ((𝐹‘𝐶)‘𝑘) ≤ 0)) → 𝑘 ∈ (1...𝐽))
7	6	adantrr 717	. . . . . . . . 9 ⊢ ((𝜑 ∧ ((𝑘 ∈ (1...𝐽) ∧ ((𝐹‘𝐶)‘𝑘) ≤ 0) ∧ ∀𝑗 ∈ {𝑖 ∈ (1...𝐽) ∣ ((𝐹‘𝐶)‘𝑖) ≤ 0}𝑗 ≤ 𝑘)) → 𝑘 ∈ (1...𝐽))
8		fzssuz 13153	. . . . . . . . . . . . . 14 ⊢ (1...𝐽) ⊆ (ℤ_≥‘1)
9		uzssz 12459	. . . . . . . . . . . . . 14 ⊢ (ℤ_≥‘1) ⊆ ℤ
10	8, 9	sstri 3910	. . . . . . . . . . . . 13 ⊢ (1...𝐽) ⊆ ℤ
11		zssre 12183	. . . . . . . . . . . . 13 ⊢ ℤ ⊆ ℝ
12	10, 11	sstri 3910	. . . . . . . . . . . 12 ⊢ (1...𝐽) ⊆ ℝ
13	12	sseli 3896	. . . . . . . . . . 11 ⊢ (𝑘 ∈ (1...𝐽) → 𝑘 ∈ ℝ)
14	13	ltp1d 11762	. . . . . . . . . 10 ⊢ (𝑘 ∈ (1...𝐽) → 𝑘 < (𝑘 + 1))
15		1red 10834	. . . . . . . . . . . 12 ⊢ (𝑘 ∈ (1...𝐽) → 1 ∈ ℝ)
16	13, 15	readdcld 10862	. . . . . . . . . . 11 ⊢ (𝑘 ∈ (1...𝐽) → (𝑘 + 1) ∈ ℝ)
17	13, 16	ltnled 10979	. . . . . . . . . 10 ⊢ (𝑘 ∈ (1...𝐽) → (𝑘 < (𝑘 + 1) ↔ ¬ (𝑘 + 1) ≤ 𝑘))
18	14, 17	mpbid 235	. . . . . . . . 9 ⊢ (𝑘 ∈ (1...𝐽) → ¬ (𝑘 + 1) ≤ 𝑘)
19	7, 18	syl 17	. . . . . . . 8 ⊢ ((𝜑 ∧ ((𝑘 ∈ (1...𝐽) ∧ ((𝐹‘𝐶)‘𝑘) ≤ 0) ∧ ∀𝑗 ∈ {𝑖 ∈ (1...𝐽) ∣ ((𝐹‘𝐶)‘𝑖) ≤ 0}𝑗 ≤ 𝑘)) → ¬ (𝑘 + 1) ≤ 𝑘)
20		simprr 773	. . . . . . . . 9 ⊢ ((𝜑 ∧ ((𝑘 ∈ (1...𝐽) ∧ ((𝐹‘𝐶)‘𝑘) ≤ 0) ∧ ∀𝑗 ∈ {𝑖 ∈ (1...𝐽) ∣ ((𝐹‘𝐶)‘𝑖) ≤ 0}𝑗 ≤ 𝑘)) → ∀𝑗 ∈ {𝑖 ∈ (1...𝐽) ∣ ((𝐹‘𝐶)‘𝑖) ≤ 0}𝑗 ≤ 𝑘)
21		ballotlemfc0.4	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → 0 < ((𝐹‘𝐶)‘𝐽))
22	21	adantr 484	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑘 = 𝐽) → 0 < ((𝐹‘𝐶)‘𝐽))
23		simpr 488	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑘 = 𝐽) → 𝑘 = 𝐽)
24	23	fveq2d 6721	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑘 = 𝐽) → ((𝐹‘𝐶)‘𝑘) = ((𝐹‘𝐶)‘𝐽))
25	24	breq2d 5065	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑘 = 𝐽) → (0 < ((𝐹‘𝐶)‘𝑘) ↔ 0 < ((𝐹‘𝐶)‘𝐽)))
26		ballotlemfp1.j	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜑 → 𝐽 ∈ ℕ)
27		elnnuz 12478	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝐽 ∈ ℕ ↔ 𝐽 ∈ (ℤ_≥‘1))
28	26, 27	sylib 221	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → 𝐽 ∈ (ℤ_≥‘1))
29		eluzfz2 13120	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝐽 ∈ (ℤ_≥‘1) → 𝐽 ∈ (1...𝐽))
30	28, 29	syl 17	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → 𝐽 ∈ (1...𝐽))
31		eleq1 2825	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑘 = 𝐽 → (𝑘 ∈ (1...𝐽) ↔ 𝐽 ∈ (1...𝐽)))
32	30, 31	syl5ibrcom 250	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → (𝑘 = 𝐽 → 𝑘 ∈ (1...𝐽)))
33	32	anc2li 559	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (𝑘 = 𝐽 → (𝜑 ∧ 𝑘 ∈ (1...𝐽))))
34		1eluzge0 12488	. . . . . . . . . . . . . . . . . . . 20 ⊢ 1 ∈ (ℤ_≥‘0)
35		fzss1 13151	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (1 ∈ (ℤ_≥‘0) → (1...𝐽) ⊆ (0...𝐽))
36	35	sseld 3900	. . . . . . . . . . . . . . . . . . . 20 ⊢ (1 ∈ (ℤ_≥‘0) → (𝑘 ∈ (1...𝐽) → 𝑘 ∈ (0...𝐽)))
37	34, 36	ax-mp 5	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑘 ∈ (1...𝐽) → 𝑘 ∈ (0...𝐽))
38		0red 10836	. . . . . . . . . . . . . . . . . . . 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 484	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝐽)) → 𝐶 ∈ 𝑂)
46		elfzelz 13112	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑘 ∈ (0...𝐽) → 𝑘 ∈ ℤ)
47	46	adantl 485	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝐽)) → 𝑘 ∈ ℤ)
48	39, 40, 41, 42, 43, 45, 47	ballotlemfelz 32169	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝐽)) → ((𝐹‘𝐶)‘𝑘) ∈ ℤ)
49	48	zred 12282	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝐽)) → ((𝐹‘𝐶)‘𝑘) ∈ ℝ)
50	38, 49	ltnled 10979	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝐽)) → (0 < ((𝐹‘𝐶)‘𝑘) ↔ ¬ ((𝐹‘𝐶)‘𝑘) ≤ 0))
51	37, 50	sylan2 596	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑘 ∈ (1...𝐽)) → (0 < ((𝐹‘𝐶)‘𝑘) ↔ ¬ ((𝐹‘𝐶)‘𝑘) ≤ 0))
52	33, 51	syl6 35	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (𝑘 = 𝐽 → (0 < ((𝐹‘𝐶)‘𝑘) ↔ ¬ ((𝐹‘𝐶)‘𝑘) ≤ 0)))
53	52	imp 410	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑘 = 𝐽) → (0 < ((𝐹‘𝐶)‘𝑘) ↔ ¬ ((𝐹‘𝐶)‘𝑘) ≤ 0))
54	25, 53	bitr3d 284	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑘 = 𝐽) → (0 < ((𝐹‘𝐶)‘𝐽) ↔ ¬ ((𝐹‘𝐶)‘𝑘) ≤ 0))
55	22, 54	mpbid 235	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑘 = 𝐽) → ¬ ((𝐹‘𝐶)‘𝑘) ≤ 0)
56	55	ex 416	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝑘 = 𝐽 → ¬ ((𝐹‘𝐶)‘𝑘) ≤ 0))
57	56	con2d 136	. . . . . . . . . . . 12 ⊢ (𝜑 → (((𝐹‘𝐶)‘𝑘) ≤ 0 → ¬ 𝑘 = 𝐽))
58		nn1m1nn 11851	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝐽 ∈ ℕ → (𝐽 = 1 ∨ (𝐽 − 1) ∈ ℕ))
59	26, 58	syl 17	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → (𝐽 = 1 ∨ (𝐽 − 1) ∈ ℕ))
60		ballotlemfc0.3	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝜑 → ∃𝑖 ∈ (1...𝐽)((𝐹‘𝐶)‘𝑖) ≤ 0)
61	60	adantr 484	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝜑 ∧ 𝐽 = 1) → ∃𝑖 ∈ (1...𝐽)((𝐹‘𝐶)‘𝑖) ≤ 0)
62		oveq1 7220	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝐽 = 1 → (𝐽...𝐽) = (1...𝐽))
63	62	adantl 485	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝜑 ∧ 𝐽 = 1) → (𝐽...𝐽) = (1...𝐽))
64	26	nnzd 12281	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝜑 → 𝐽 ∈ ℤ)
65		fzsn 13154	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝐽 ∈ ℤ → (𝐽...𝐽) = {𝐽})
66	64, 65	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝜑 → (𝐽...𝐽) = {𝐽})
67	66	adantr 484	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝜑 ∧ 𝐽 = 1) → (𝐽...𝐽) = {𝐽})
68	63, 67	eqtr3d 2779	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝜑 ∧ 𝐽 = 1) → (1...𝐽) = {𝐽})
69	68	rexeqdv 3326	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝜑 ∧ 𝐽 = 1) → (∃𝑖 ∈ (1...𝐽)((𝐹‘𝐶)‘𝑖) ≤ 0 ↔ ∃𝑖 ∈ {𝐽} ((𝐹‘𝐶)‘𝑖) ≤ 0))
70	61, 69	mpbid 235	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝜑 ∧ 𝐽 = 1) → ∃𝑖 ∈ {𝐽} ((𝐹‘𝐶)‘𝑖) ≤ 0)
71		fveq2 6717	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝑖 = 𝐽 → ((𝐹‘𝐶)‘𝑖) = ((𝐹‘𝐶)‘𝐽))
72	71	breq1d 5063	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑖 = 𝐽 → (((𝐹‘𝐶)‘𝑖) ≤ 0 ↔ ((𝐹‘𝐶)‘𝐽) ≤ 0))
73	72	rexsng 4590	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝐽 ∈ ℕ → (∃𝑖 ∈ {𝐽} ((𝐹‘𝐶)‘𝑖) ≤ 0 ↔ ((𝐹‘𝐶)‘𝐽) ≤ 0))
74	26, 73	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝜑 → (∃𝑖 ∈ {𝐽} ((𝐹‘𝐶)‘𝑖) ≤ 0 ↔ ((𝐹‘𝐶)‘𝐽) ≤ 0))
75	74	adantr 484	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝜑 ∧ 𝐽 = 1) → (∃𝑖 ∈ {𝐽} ((𝐹‘𝐶)‘𝑖) ≤ 0 ↔ ((𝐹‘𝐶)‘𝐽) ≤ 0))
76	70, 75	mpbid 235	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ 𝐽 = 1) → ((𝐹‘𝐶)‘𝐽) ≤ 0)
77	21	adantr 484	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝜑 ∧ 𝐽 = 1) → 0 < ((𝐹‘𝐶)‘𝐽))
78		0red 10836	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝜑 → 0 ∈ ℝ)
79	39, 40, 41, 42, 43, 44, 64	ballotlemfelz 32169	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝜑 → ((𝐹‘𝐶)‘𝐽) ∈ ℤ)
80	79	zred 12282	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝜑 → ((𝐹‘𝐶)‘𝐽) ∈ ℝ)
81	78, 80	ltnled 10979	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝜑 → (0 < ((𝐹‘𝐶)‘𝐽) ↔ ¬ ((𝐹‘𝐶)‘𝐽) ≤ 0))
82	81	adantr 484	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝜑 ∧ 𝐽 = 1) → (0 < ((𝐹‘𝐶)‘𝐽) ↔ ¬ ((𝐹‘𝐶)‘𝐽) ≤ 0))
83	77, 82	mpbid 235	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ 𝐽 = 1) → ¬ ((𝐹‘𝐶)‘𝐽) ≤ 0)
84	76, 83	pm2.65da 817	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜑 → ¬ 𝐽 = 1)
85		biortn 938	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (¬ 𝐽 = 1 → ((𝐽 − 1) ∈ ℕ ↔ (¬ ¬ 𝐽 = 1 ∨ (𝐽 − 1) ∈ ℕ)))
86	84, 85	syl 17	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → ((𝐽 − 1) ∈ ℕ ↔ (¬ ¬ 𝐽 = 1 ∨ (𝐽 − 1) ∈ ℕ)))
87		notnotb 318	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝐽 = 1 ↔ ¬ ¬ 𝐽 = 1)
88	87	orbi1i 914	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝐽 = 1 ∨ (𝐽 − 1) ∈ ℕ) ↔ (¬ ¬ 𝐽 = 1 ∨ (𝐽 − 1) ∈ ℕ))
89	86, 88	bitr4di 292	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → ((𝐽 − 1) ∈ ℕ ↔ (𝐽 = 1 ∨ (𝐽 − 1) ∈ ℕ)))
90	59, 89	mpbird 260	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → (𝐽 − 1) ∈ ℕ)
91		elnnuz 12478	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝐽 − 1) ∈ ℕ ↔ (𝐽 − 1) ∈ (ℤ_≥‘1))
92	90, 91	sylib 221	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (𝐽 − 1) ∈ (ℤ_≥‘1))
93		elfzp1 13162	. . . . . . . . . . . . . . . . . 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 11846	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → 𝐽 ∈ ℂ)
96		1cnd 10828	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → 1 ∈ ℂ)
97	95, 96	npcand 11193	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → ((𝐽 − 1) + 1) = 𝐽)
98	97	oveq2d 7229	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (1...((𝐽 − 1) + 1)) = (1...𝐽))
99	98	eleq2d 2823	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (𝑘 ∈ (1...((𝐽 − 1) + 1)) ↔ 𝑘 ∈ (1...𝐽)))
100	97	eqeq2d 2748	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (𝑘 = ((𝐽 − 1) + 1) ↔ 𝑘 = 𝐽))
101	100	orbi2d 916	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → ((𝑘 ∈ (1...(𝐽 − 1)) ∨ 𝑘 = ((𝐽 − 1) + 1)) ↔ (𝑘 ∈ (1...(𝐽 − 1)) ∨ 𝑘 = 𝐽)))
102	94, 99, 101	3bitr3d 312	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (𝑘 ∈ (1...𝐽) ↔ (𝑘 ∈ (1...(𝐽 − 1)) ∨ 𝑘 = 𝐽)))
103		orcom 870	. . . . . . . . . . . . . . . 16 ⊢ ((𝑘 ∈ (1...(𝐽 − 1)) ∨ 𝑘 = 𝐽) ↔ (𝑘 = 𝐽 ∨ 𝑘 ∈ (1...(𝐽 − 1))))
104	102, 103	bitrdi 290	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝑘 ∈ (1...𝐽) ↔ (𝑘 = 𝐽 ∨ 𝑘 ∈ (1...(𝐽 − 1)))))
105	104	biimpd 232	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝑘 ∈ (1...𝐽) → (𝑘 = 𝐽 ∨ 𝑘 ∈ (1...(𝐽 − 1)))))
106		pm5.6 1002	. . . . . . . . . . . . . 14 ⊢ (((𝑘 ∈ (1...𝐽) ∧ ¬ 𝑘 = 𝐽) → 𝑘 ∈ (1...(𝐽 − 1))) ↔ (𝑘 ∈ (1...𝐽) → (𝑘 = 𝐽 ∨ 𝑘 ∈ (1...(𝐽 − 1)))))
107	105, 106	sylibr 237	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((𝑘 ∈ (1...𝐽) ∧ ¬ 𝑘 = 𝐽) → 𝑘 ∈ (1...(𝐽 − 1))))
108	90	nnzd 12281	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → (𝐽 − 1) ∈ ℤ)
109		1z 12207	. . . . . . . . . . . . . . . . . . 19 ⊢ 1 ∈ ℤ
110	108, 109	jctil 523	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (1 ∈ ℤ ∧ (𝐽 − 1) ∈ ℤ))
111		elfzelz 13112	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑘 ∈ (1...(𝐽 − 1)) → 𝑘 ∈ ℤ)
112	111, 109	jctir 524	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑘 ∈ (1...(𝐽 − 1)) → (𝑘 ∈ ℤ ∧ 1 ∈ ℤ))
113		fzaddel 13146	. . . . . . . . . . . . . . . . . 18 ⊢ (((1 ∈ ℤ ∧ (𝐽 − 1) ∈ ℤ) ∧ (𝑘 ∈ ℤ ∧ 1 ∈ ℤ)) → (𝑘 ∈ (1...(𝐽 − 1)) ↔ (𝑘 + 1) ∈ ((1 + 1)...((𝐽 − 1) + 1))))
114	110, 112, 113	syl2an 599	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑘 ∈ (1...(𝐽 − 1))) → (𝑘 ∈ (1...(𝐽 − 1)) ↔ (𝑘 + 1) ∈ ((1 + 1)...((𝐽 − 1) + 1))))
115	114	biimp3a 1471	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑘 ∈ (1...(𝐽 − 1)) ∧ 𝑘 ∈ (1...(𝐽 − 1))) → (𝑘 + 1) ∈ ((1 + 1)...((𝐽 − 1) + 1)))
116	115	3anidm23 1423	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑘 ∈ (1...(𝐽 − 1))) → (𝑘 + 1) ∈ ((1 + 1)...((𝐽 − 1) + 1)))
117		1p1e2 11955	. . . . . . . . . . . . . . . . . . . 20 ⊢ (1 + 1) = 2
118	117	a1i 11	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → (1 + 1) = 2)
119	118, 97	oveq12d 7231	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → ((1 + 1)...((𝐽 − 1) + 1)) = (2...𝐽))
120	119	eleq2d 2823	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → ((𝑘 + 1) ∈ ((1 + 1)...((𝐽 − 1) + 1)) ↔ (𝑘 + 1) ∈ (2...𝐽)))
121		2eluzge1 12490	. . . . . . . . . . . . . . . . . . 19 ⊢ 2 ∈ (ℤ_≥‘1)
122		fzss1 13151	. . . . . . . . . . . . . . . . . . 19 ⊢ (2 ∈ (ℤ_≥‘1) → (2...𝐽) ⊆ (1...𝐽))
123	121, 122	ax-mp 5	. . . . . . . . . . . . . . . . . 18 ⊢ (2...𝐽) ⊆ (1...𝐽)
124	123	sseli 3896	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑘 + 1) ∈ (2...𝐽) → (𝑘 + 1) ∈ (1...𝐽))
125	120, 124	syl6bi 256	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ((𝑘 + 1) ∈ ((1 + 1)...((𝐽 − 1) + 1)) → (𝑘 + 1) ∈ (1...𝐽)))
126	125	adantr 484	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑘 ∈ (1...(𝐽 − 1))) → ((𝑘 + 1) ∈ ((1 + 1)...((𝐽 − 1) + 1)) → (𝑘 + 1) ∈ (1...𝐽)))
127	116, 126	mpd 15	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑘 ∈ (1...(𝐽 − 1))) → (𝑘 + 1) ∈ (1...𝐽))
128	127	ex 416	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝑘 ∈ (1...(𝐽 − 1)) → (𝑘 + 1) ∈ (1...𝐽)))
129	107, 128	syld 47	. . . . . . . . . . . 12 ⊢ (𝜑 → ((𝑘 ∈ (1...𝐽) ∧ ¬ 𝑘 = 𝐽) → (𝑘 + 1) ∈ (1...𝐽)))
130	57, 129	sylan2d 608	. . . . . . . . . . 11 ⊢ (𝜑 → ((𝑘 ∈ (1...𝐽) ∧ ((𝐹‘𝐶)‘𝑘) ≤ 0) → (𝑘 + 1) ∈ (1...𝐽)))
131	130	imp 410	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑘 ∈ (1...𝐽) ∧ ((𝐹‘𝐶)‘𝑘) ≤ 0)) → (𝑘 + 1) ∈ (1...𝐽))
132	131	adantrr 717	. . . . . . . . 9 ⊢ ((𝜑 ∧ ((𝑘 ∈ (1...𝐽) ∧ ((𝐹‘𝐶)‘𝑘) ≤ 0) ∧ ∀𝑗 ∈ {𝑖 ∈ (1...𝐽) ∣ ((𝐹‘𝐶)‘𝑖) ≤ 0}𝑗 ≤ 𝑘)) → (𝑘 + 1) ∈ (1...𝐽))
133		fveq2 6717	. . . . . . . . . . . . . 14 ⊢ (𝑖 = (𝑘 + 1) → ((𝐹‘𝐶)‘𝑖) = ((𝐹‘𝐶)‘(𝑘 + 1)))
134	133	breq1d 5063	. . . . . . . . . . . . 13 ⊢ (𝑖 = (𝑘 + 1) → (((𝐹‘𝐶)‘𝑖) ≤ 0 ↔ ((𝐹‘𝐶)‘(𝑘 + 1)) ≤ 0))
135	134	elrab 3602	. . . . . . . . . . . 12 ⊢ ((𝑘 + 1) ∈ {𝑖 ∈ (1...𝐽) ∣ ((𝐹‘𝐶)‘𝑖) ≤ 0} ↔ ((𝑘 + 1) ∈ (1...𝐽) ∧ ((𝐹‘𝐶)‘(𝑘 + 1)) ≤ 0))
136		breq1 5056	. . . . . . . . . . . . 13 ⊢ (𝑗 = (𝑘 + 1) → (𝑗 ≤ 𝑘 ↔ (𝑘 + 1) ≤ 𝑘))
137	136	rspccva 3536	. . . . . . . . . . . 12 ⊢ ((∀𝑗 ∈ {𝑖 ∈ (1...𝐽) ∣ ((𝐹‘𝐶)‘𝑖) ≤ 0}𝑗 ≤ 𝑘 ∧ (𝑘 + 1) ∈ {𝑖 ∈ (1...𝐽) ∣ ((𝐹‘𝐶)‘𝑖) ≤ 0}) → (𝑘 + 1) ≤ 𝑘)
138	135, 137	sylan2br 598	. . . . . . . . . . 11 ⊢ ((∀𝑗 ∈ {𝑖 ∈ (1...𝐽) ∣ ((𝐹‘𝐶)‘𝑖) ≤ 0}𝑗 ≤ 𝑘 ∧ ((𝑘 + 1) ∈ (1...𝐽) ∧ ((𝐹‘𝐶)‘(𝑘 + 1)) ≤ 0)) → (𝑘 + 1) ≤ 𝑘)
139	138	expr 460	. . . . . . . . . 10 ⊢ ((∀𝑗 ∈ {𝑖 ∈ (1...𝐽) ∣ ((𝐹‘𝐶)‘𝑖) ≤ 0}𝑗 ≤ 𝑘 ∧ (𝑘 + 1) ∈ (1...𝐽)) → (((𝐹‘𝐶)‘(𝑘 + 1)) ≤ 0 → (𝑘 + 1) ≤ 𝑘))
140	139	con3d 155	. . . . . . . . 9 ⊢ ((∀𝑗 ∈ {𝑖 ∈ (1...𝐽) ∣ ((𝐹‘𝐶)‘𝑖) ≤ 0}𝑗 ≤ 𝑘 ∧ (𝑘 + 1) ∈ (1...𝐽)) → (¬ (𝑘 + 1) ≤ 𝑘 → ¬ ((𝐹‘𝐶)‘(𝑘 + 1)) ≤ 0))
141	20, 132, 140	syl2anc 587	. . . . . . . 8 ⊢ ((𝜑 ∧ ((𝑘 ∈ (1...𝐽) ∧ ((𝐹‘𝐶)‘𝑘) ≤ 0) ∧ ∀𝑗 ∈ {𝑖 ∈ (1...𝐽) ∣ ((𝐹‘𝐶)‘𝑖) ≤ 0}𝑗 ≤ 𝑘)) → (¬ (𝑘 + 1) ≤ 𝑘 → ¬ ((𝐹‘𝐶)‘(𝑘 + 1)) ≤ 0))
142	19, 141	mpd 15	. . . . . . 7 ⊢ ((𝜑 ∧ ((𝑘 ∈ (1...𝐽) ∧ ((𝐹‘𝐶)‘𝑘) ≤ 0) ∧ ∀𝑗 ∈ {𝑖 ∈ (1...𝐽) ∣ ((𝐹‘𝐶)‘𝑖) ≤ 0}𝑗 ≤ 𝑘)) → ¬ ((𝐹‘𝐶)‘(𝑘 + 1)) ≤ 0)
143		simplrr 778	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ ((𝑘 ∈ (1...𝐽) ∧ ((𝐹‘𝐶)‘𝑘) ≤ 0) ∧ ∀𝑗 ∈ {𝑖 ∈ (1...𝐽) ∣ ((𝐹‘𝐶)‘𝑖) ≤ 0}𝑗 ≤ 𝑘)) ∧ ¬ (𝑘 + 1) ∈ 𝐶) → ∀𝑗 ∈ {𝑖 ∈ (1...𝐽) ∣ ((𝐹‘𝐶)‘𝑖) ≤ 0}𝑗 ≤ 𝑘)
144	132	adantr 484	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ ((𝑘 ∈ (1...𝐽) ∧ ((𝐹‘𝐶)‘𝑘) ≤ 0) ∧ ∀𝑗 ∈ {𝑖 ∈ (1...𝐽) ∣ ((𝐹‘𝐶)‘𝑖) ≤ 0}𝑗 ≤ 𝑘)) ∧ ¬ (𝑘 + 1) ∈ 𝐶) → (𝑘 + 1) ∈ (1...𝐽))
145		simpll 767	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (𝑘 ∈ (1...𝐽) ∧ ((𝐹‘𝐶)‘𝑘) ≤ 0)) ∧ ¬ (𝑘 + 1) ∈ 𝐶) → 𝜑)
146	131	adantr 484	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ (𝑘 ∈ (1...𝐽) ∧ ((𝐹‘𝐶)‘𝑘) ≤ 0)) ∧ ¬ (𝑘 + 1) ∈ 𝐶) → (𝑘 + 1) ∈ (1...𝐽))
147	35	sseld 3900	. . . . . . . . . . . . . . 15 ⊢ (1 ∈ (ℤ_≥‘0) → ((𝑘 + 1) ∈ (1...𝐽) → (𝑘 + 1) ∈ (0...𝐽)))
148	34, 146, 147	mpsyl 68	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (𝑘 ∈ (1...𝐽) ∧ ((𝐹‘𝐶)‘𝑘) ≤ 0)) ∧ ¬ (𝑘 + 1) ∈ 𝐶) → (𝑘 + 1) ∈ (0...𝐽))
149	44	adantr 484	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ (𝑘 + 1) ∈ (0...𝐽)) → 𝐶 ∈ 𝑂)
150		elfzelz 13112	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑘 + 1) ∈ (0...𝐽) → (𝑘 + 1) ∈ ℤ)
151	150	adantl 485	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ (𝑘 + 1) ∈ (0...𝐽)) → (𝑘 + 1) ∈ ℤ)
152	39, 40, 41, 42, 43, 149, 151	ballotlemfelz 32169	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ (𝑘 + 1) ∈ (0...𝐽)) → ((𝐹‘𝐶)‘(𝑘 + 1)) ∈ ℤ)
153	152	zred 12282	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑘 + 1) ∈ (0...𝐽)) → ((𝐹‘𝐶)‘(𝑘 + 1)) ∈ ℝ)
154	145, 148, 153	syl2anc 587	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑘 ∈ (1...𝐽) ∧ ((𝐹‘𝐶)‘𝑘) ≤ 0)) ∧ ¬ (𝑘 + 1) ∈ 𝐶) → ((𝐹‘𝐶)‘(𝑘 + 1)) ∈ ℝ)
155		0red 10836	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑘 ∈ (1...𝐽) ∧ ((𝐹‘𝐶)‘𝑘) ≤ 0)) ∧ ¬ (𝑘 + 1) ∈ 𝐶) → 0 ∈ ℝ)
156		simplrr 778	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (𝑘 ∈ (1...𝐽) ∧ ((𝐹‘𝐶)‘𝑘) ≤ 0)) ∧ ¬ (𝑘 + 1) ∈ 𝐶) → ((𝐹‘𝐶)‘𝑘) ≤ 0)
157	6	adantr 484	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ (𝑘 ∈ (1...𝐽) ∧ ((𝐹‘𝐶)‘𝑘) ≤ 0)) ∧ ¬ (𝑘 + 1) ∈ 𝐶) → 𝑘 ∈ (1...𝐽))
158	157, 37	syl 17	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ (𝑘 ∈ (1...𝐽) ∧ ((𝐹‘𝐶)‘𝑘) ≤ 0)) ∧ ¬ (𝑘 + 1) ∈ 𝐶) → 𝑘 ∈ (0...𝐽))
159	130	imdistani 572	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ (𝑘 ∈ (1...𝐽) ∧ ((𝐹‘𝐶)‘𝑘) ≤ 0)) → (𝜑 ∧ (𝑘 + 1) ∈ (1...𝐽)))
160	44	adantr 484	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ (𝑘 + 1) ∈ (1...𝐽)) → 𝐶 ∈ 𝑂)
161		elfznn 13141	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑘 + 1) ∈ (1...𝐽) → (𝑘 + 1) ∈ ℕ)
162	161	adantl 485	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ (𝑘 + 1) ∈ (1...𝐽)) → (𝑘 + 1) ∈ ℕ)
163	39, 40, 41, 42, 43, 160, 162	ballotlemfp1 32170	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ (𝑘 + 1) ∈ (1...𝐽)) → ((¬ (𝑘 + 1) ∈ 𝐶 → ((𝐹‘𝐶)‘(𝑘 + 1)) = (((𝐹‘𝐶)‘((𝑘 + 1) − 1)) − 1)) ∧ ((𝑘 + 1) ∈ 𝐶 → ((𝐹‘𝐶)‘(𝑘 + 1)) = (((𝐹‘𝐶)‘((𝑘 + 1) − 1)) + 1))))
164	163	simpld 498	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ (𝑘 + 1) ∈ (1...𝐽)) → (¬ (𝑘 + 1) ∈ 𝐶 → ((𝐹‘𝐶)‘(𝑘 + 1)) = (((𝐹‘𝐶)‘((𝑘 + 1) − 1)) − 1)))
165	164	imp 410	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ (𝑘 + 1) ∈ (1...𝐽)) ∧ ¬ (𝑘 + 1) ∈ 𝐶) → ((𝐹‘𝐶)‘(𝑘 + 1)) = (((𝐹‘𝐶)‘((𝑘 + 1) − 1)) − 1))
166	159, 165	sylan 583	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ (𝑘 ∈ (1...𝐽) ∧ ((𝐹‘𝐶)‘𝑘) ≤ 0)) ∧ ¬ (𝑘 + 1) ∈ 𝐶) → ((𝐹‘𝐶)‘(𝑘 + 1)) = (((𝐹‘𝐶)‘((𝑘 + 1) − 1)) − 1))
167		elfzelz 13112	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑘 ∈ (1...𝐽) → 𝑘 ∈ ℤ)
168	167	zcnd 12283	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑘 ∈ (1...𝐽) → 𝑘 ∈ ℂ)
169		1cnd 10828	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑘 ∈ (1...𝐽) → 1 ∈ ℂ)
170	168, 169	pncand 11190	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑘 ∈ (1...𝐽) → ((𝑘 + 1) − 1) = 𝑘)
171	170	fveq2d 6721	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑘 ∈ (1...𝐽) → ((𝐹‘𝐶)‘((𝑘 + 1) − 1)) = ((𝐹‘𝐶)‘𝑘))
172	171	oveq1d 7228	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑘 ∈ (1...𝐽) → (((𝐹‘𝐶)‘((𝑘 + 1) − 1)) − 1) = (((𝐹‘𝐶)‘𝑘) − 1))
173	172	eqeq2d 2748	. . . . . . . . . . . . . . . . 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 235	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ (𝑘 ∈ (1...𝐽) ∧ ((𝐹‘𝐶)‘𝑘) ≤ 0)) ∧ ¬ (𝑘 + 1) ∈ 𝐶) → ((𝐹‘𝐶)‘(𝑘 + 1)) = (((𝐹‘𝐶)‘𝑘) − 1))
176		0z 12187	. . . . . . . . . . . . . . . . . 18 ⊢ 0 ∈ ℤ
177		zlem1lt 12229	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝐹‘𝐶)‘𝑘) ∈ ℤ ∧ 0 ∈ ℤ) → (((𝐹‘𝐶)‘𝑘) ≤ 0 ↔ (((𝐹‘𝐶)‘𝑘) − 1) < 0))
178	48, 176, 177	sylancl 589	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝐽)) → (((𝐹‘𝐶)‘𝑘) ≤ 0 ↔ (((𝐹‘𝐶)‘𝑘) − 1) < 0))
179	178	adantr 484	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑘 ∈ (0...𝐽)) ∧ ((𝐹‘𝐶)‘(𝑘 + 1)) = (((𝐹‘𝐶)‘𝑘) − 1)) → (((𝐹‘𝐶)‘𝑘) ≤ 0 ↔ (((𝐹‘𝐶)‘𝑘) − 1) < 0))
180		breq1 5056	. . . . . . . . . . . . . . . . 17 ⊢ (((𝐹‘𝐶)‘(𝑘 + 1)) = (((𝐹‘𝐶)‘𝑘) − 1) → (((𝐹‘𝐶)‘(𝑘 + 1)) < 0 ↔ (((𝐹‘𝐶)‘𝑘) − 1) < 0))
181	180	adantl 485	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑘 ∈ (0...𝐽)) ∧ ((𝐹‘𝐶)‘(𝑘 + 1)) = (((𝐹‘𝐶)‘𝑘) − 1)) → (((𝐹‘𝐶)‘(𝑘 + 1)) < 0 ↔ (((𝐹‘𝐶)‘𝑘) − 1) < 0))
182	179, 181	bitr4d 285	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑘 ∈ (0...𝐽)) ∧ ((𝐹‘𝐶)‘(𝑘 + 1)) = (((𝐹‘𝐶)‘𝑘) − 1)) → (((𝐹‘𝐶)‘𝑘) ≤ 0 ↔ ((𝐹‘𝐶)‘(𝑘 + 1)) < 0))
183	145, 158, 175, 182	syl21anc 838	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (𝑘 ∈ (1...𝐽) ∧ ((𝐹‘𝐶)‘𝑘) ≤ 0)) ∧ ¬ (𝑘 + 1) ∈ 𝐶) → (((𝐹‘𝐶)‘𝑘) ≤ 0 ↔ ((𝐹‘𝐶)‘(𝑘 + 1)) < 0))
184	156, 183	mpbid 235	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑘 ∈ (1...𝐽) ∧ ((𝐹‘𝐶)‘𝑘) ≤ 0)) ∧ ¬ (𝑘 + 1) ∈ 𝐶) → ((𝐹‘𝐶)‘(𝑘 + 1)) < 0)
185	154, 155, 184	ltled 10980	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝑘 ∈ (1...𝐽) ∧ ((𝐹‘𝐶)‘𝑘) ≤ 0)) ∧ ¬ (𝑘 + 1) ∈ 𝐶) → ((𝐹‘𝐶)‘(𝑘 + 1)) ≤ 0)
186	185	adantlrr 721	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ ((𝑘 ∈ (1...𝐽) ∧ ((𝐹‘𝐶)‘𝑘) ≤ 0) ∧ ∀𝑗 ∈ {𝑖 ∈ (1...𝐽) ∣ ((𝐹‘𝐶)‘𝑖) ≤ 0}𝑗 ≤ 𝑘)) ∧ ¬ (𝑘 + 1) ∈ 𝐶) → ((𝐹‘𝐶)‘(𝑘 + 1)) ≤ 0)
187	143, 144, 186, 138	syl12anc 837	. . . . . . . . . 10 ⊢ (((𝜑 ∧ ((𝑘 ∈ (1...𝐽) ∧ ((𝐹‘𝐶)‘𝑘) ≤ 0) ∧ ∀𝑗 ∈ {𝑖 ∈ (1...𝐽) ∣ ((𝐹‘𝐶)‘𝑖) ≤ 0}𝑗 ≤ 𝑘)) ∧ ¬ (𝑘 + 1) ∈ 𝐶) → (𝑘 + 1) ≤ 𝑘)
188	19	adantr 484	. . . . . . . . . 10 ⊢ (((𝜑 ∧ ((𝑘 ∈ (1...𝐽) ∧ ((𝐹‘𝐶)‘𝑘) ≤ 0) ∧ ∀𝑗 ∈ {𝑖 ∈ (1...𝐽) ∣ ((𝐹‘𝐶)‘𝑖) ≤ 0}𝑗 ≤ 𝑘)) ∧ ¬ (𝑘 + 1) ∈ 𝐶) → ¬ (𝑘 + 1) ≤ 𝑘)
189	187, 188	condan 818	. . . . . . . . 9 ⊢ ((𝜑 ∧ ((𝑘 ∈ (1...𝐽) ∧ ((𝐹‘𝐶)‘𝑘) ≤ 0) ∧ ∀𝑗 ∈ {𝑖 ∈ (1...𝐽) ∣ ((𝐹‘𝐶)‘𝑖) ≤ 0}𝑗 ≤ 𝑘)) → (𝑘 + 1) ∈ 𝐶)
190	163	simprd 499	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑘 + 1) ∈ (1...𝐽)) → ((𝑘 + 1) ∈ 𝐶 → ((𝐹‘𝐶)‘(𝑘 + 1)) = (((𝐹‘𝐶)‘((𝑘 + 1) − 1)) + 1)))
191	190	imp 410	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝑘 + 1) ∈ (1...𝐽)) ∧ (𝑘 + 1) ∈ 𝐶) → ((𝐹‘𝐶)‘(𝑘 + 1)) = (((𝐹‘𝐶)‘((𝑘 + 1) − 1)) + 1))
192	159, 191	sylan 583	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝑘 ∈ (1...𝐽) ∧ ((𝐹‘𝐶)‘𝑘) ≤ 0)) ∧ (𝑘 + 1) ∈ 𝐶) → ((𝐹‘𝐶)‘(𝑘 + 1)) = (((𝐹‘𝐶)‘((𝑘 + 1) − 1)) + 1))
193	6	adantr 484	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝑘 ∈ (1...𝐽) ∧ ((𝐹‘𝐶)‘𝑘) ≤ 0)) ∧ (𝑘 + 1) ∈ 𝐶) → 𝑘 ∈ (1...𝐽))
194	171	oveq1d 7228	. . . . . . . . . . . . 13 ⊢ (𝑘 ∈ (1...𝐽) → (((𝐹‘𝐶)‘((𝑘 + 1) − 1)) + 1) = (((𝐹‘𝐶)‘𝑘) + 1))
195	194	eqeq2d 2748	. . . . . . . . . . . 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 235	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝑘 ∈ (1...𝐽) ∧ ((𝐹‘𝐶)‘𝑘) ≤ 0)) ∧ (𝑘 + 1) ∈ 𝐶) → ((𝐹‘𝐶)‘(𝑘 + 1)) = (((𝐹‘𝐶)‘𝑘) + 1))
198	197	adantlrr 721	. . . . . . . . 9 ⊢ (((𝜑 ∧ ((𝑘 ∈ (1...𝐽) ∧ ((𝐹‘𝐶)‘𝑘) ≤ 0) ∧ ∀𝑗 ∈ {𝑖 ∈ (1...𝐽) ∣ ((𝐹‘𝐶)‘𝑖) ≤ 0}𝑗 ≤ 𝑘)) ∧ (𝑘 + 1) ∈ 𝐶) → ((𝐹‘𝐶)‘(𝑘 + 1)) = (((𝐹‘𝐶)‘𝑘) + 1))
199	189, 198	mpdan 687	. . . . . . . 8 ⊢ ((𝜑 ∧ ((𝑘 ∈ (1...𝐽) ∧ ((𝐹‘𝐶)‘𝑘) ≤ 0) ∧ ∀𝑗 ∈ {𝑖 ∈ (1...𝐽) ∣ ((𝐹‘𝐶)‘𝑖) ≤ 0}𝑗 ≤ 𝑘)) → ((𝐹‘𝐶)‘(𝑘 + 1)) = (((𝐹‘𝐶)‘𝑘) + 1))
200		breq1 5056	. . . . . . . . 9 ⊢ (((𝐹‘𝐶)‘(𝑘 + 1)) = (((𝐹‘𝐶)‘𝑘) + 1) → (((𝐹‘𝐶)‘(𝑘 + 1)) ≤ 0 ↔ (((𝐹‘𝐶)‘𝑘) + 1) ≤ 0))
201	200	notbid 321	. . . . . . . 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 235	. . . . . 6 ⊢ ((𝜑 ∧ ((𝑘 ∈ (1...𝐽) ∧ ((𝐹‘𝐶)‘𝑘) ≤ 0) ∧ ∀𝑗 ∈ {𝑖 ∈ (1...𝐽) ∣ ((𝐹‘𝐶)‘𝑖) ≤ 0}𝑗 ≤ 𝑘)) → ¬ (((𝐹‘𝐶)‘𝑘) + 1) ≤ 0)
204	6, 37	syl 17	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑘 ∈ (1...𝐽) ∧ ((𝐹‘𝐶)‘𝑘) ≤ 0)) → 𝑘 ∈ (0...𝐽))
205	204, 48	syldan 594	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑘 ∈ (1...𝐽) ∧ ((𝐹‘𝐶)‘𝑘) ≤ 0)) → ((𝐹‘𝐶)‘𝑘) ∈ ℤ)
206	205	adantrr 717	. . . . . . 7 ⊢ ((𝜑 ∧ ((𝑘 ∈ (1...𝐽) ∧ ((𝐹‘𝐶)‘𝑘) ≤ 0) ∧ ∀𝑗 ∈ {𝑖 ∈ (1...𝐽) ∣ ((𝐹‘𝐶)‘𝑖) ≤ 0}𝑗 ≤ 𝑘)) → ((𝐹‘𝐶)‘𝑘) ∈ ℤ)
207		zleltp1 12228	. . . . . . . . 9 ⊢ ((0 ∈ ℤ ∧ ((𝐹‘𝐶)‘𝑘) ∈ ℤ) → (0 ≤ ((𝐹‘𝐶)‘𝑘) ↔ 0 < (((𝐹‘𝐶)‘𝑘) + 1)))
208	176, 207	mpan 690	. . . . . . . 8 ⊢ (((𝐹‘𝐶)‘𝑘) ∈ ℤ → (0 ≤ ((𝐹‘𝐶)‘𝑘) ↔ 0 < (((𝐹‘𝐶)‘𝑘) + 1)))
209		0red 10836	. . . . . . . . 9 ⊢ (((𝐹‘𝐶)‘𝑘) ∈ ℤ → 0 ∈ ℝ)
210		zre 12180	. . . . . . . . . 10 ⊢ (((𝐹‘𝐶)‘𝑘) ∈ ℤ → ((𝐹‘𝐶)‘𝑘) ∈ ℝ)
211		1red 10834	. . . . . . . . . 10 ⊢ (((𝐹‘𝐶)‘𝑘) ∈ ℤ → 1 ∈ ℝ)
212	210, 211	readdcld 10862	. . . . . . . . 9 ⊢ (((𝐹‘𝐶)‘𝑘) ∈ ℤ → (((𝐹‘𝐶)‘𝑘) + 1) ∈ ℝ)
213	209, 212	ltnled 10979	. . . . . . . 8 ⊢ (((𝐹‘𝐶)‘𝑘) ∈ ℤ → (0 < (((𝐹‘𝐶)‘𝑘) + 1) ↔ ¬ (((𝐹‘𝐶)‘𝑘) + 1) ≤ 0))
214	208, 213	bitrd 282	. . . . . . 7 ⊢ (((𝐹‘𝐶)‘𝑘) ∈ ℤ → (0 ≤ ((𝐹‘𝐶)‘𝑘) ↔ ¬ (((𝐹‘𝐶)‘𝑘) + 1) ≤ 0))
215	206, 214	syl 17	. . . . . 6 ⊢ ((𝜑 ∧ ((𝑘 ∈ (1...𝐽) ∧ ((𝐹‘𝐶)‘𝑘) ≤ 0) ∧ ∀𝑗 ∈ {𝑖 ∈ (1...𝐽) ∣ ((𝐹‘𝐶)‘𝑖) ≤ 0}𝑗 ≤ 𝑘)) → (0 ≤ ((𝐹‘𝐶)‘𝑘) ↔ ¬ (((𝐹‘𝐶)‘𝑘) + 1) ≤ 0))
216	203, 215	mpbird 260	. . . . 5 ⊢ ((𝜑 ∧ ((𝑘 ∈ (1...𝐽) ∧ ((𝐹‘𝐶)‘𝑘) ≤ 0) ∧ ∀𝑗 ∈ {𝑖 ∈ (1...𝐽) ∣ ((𝐹‘𝐶)‘𝑖) ≤ 0}𝑗 ≤ 𝑘)) → 0 ≤ ((𝐹‘𝐶)‘𝑘))
217	206	zred 12282	. . . . . 6 ⊢ ((𝜑 ∧ ((𝑘 ∈ (1...𝐽) ∧ ((𝐹‘𝐶)‘𝑘) ≤ 0) ∧ ∀𝑗 ∈ {𝑖 ∈ (1...𝐽) ∣ ((𝐹‘𝐶)‘𝑖) ≤ 0}𝑗 ≤ 𝑘)) → ((𝐹‘𝐶)‘𝑘) ∈ ℝ)
218		0red 10836	. . . . . 6 ⊢ ((𝜑 ∧ ((𝑘 ∈ (1...𝐽) ∧ ((𝐹‘𝐶)‘𝑘) ≤ 0) ∧ ∀𝑗 ∈ {𝑖 ∈ (1...𝐽) ∣ ((𝐹‘𝐶)‘𝑖) ≤ 0}𝑗 ≤ 𝑘)) → 0 ∈ ℝ)
219	217, 218	letri3d 10974	. . . . 5 ⊢ ((𝜑 ∧ ((𝑘 ∈ (1...𝐽) ∧ ((𝐹‘𝐶)‘𝑘) ≤ 0) ∧ ∀𝑗 ∈ {𝑖 ∈ (1...𝐽) ∣ ((𝐹‘𝐶)‘𝑖) ≤ 0}𝑗 ≤ 𝑘)) → (((𝐹‘𝐶)‘𝑘) = 0 ↔ (((𝐹‘𝐶)‘𝑘) ≤ 0 ∧ 0 ≤ ((𝐹‘𝐶)‘𝑘))))
220	5, 216, 219	mpbir2and 713	. . . 4 ⊢ ((𝜑 ∧ ((𝑘 ∈ (1...𝐽) ∧ ((𝐹‘𝐶)‘𝑘) ≤ 0) ∧ ∀𝑗 ∈ {𝑖 ∈ (1...𝐽) ∣ ((𝐹‘𝐶)‘𝑖) ≤ 0}𝑗 ≤ 𝑘)) → ((𝐹‘𝐶)‘𝑘) = 0)
221	4, 220	sylan2b 597	. . 3 ⊢ ((𝜑 ∧ (𝑘 ∈ {𝑖 ∈ (1...𝐽) ∣ ((𝐹‘𝐶)‘𝑖) ≤ 0} ∧ ∀𝑗 ∈ {𝑖 ∈ (1...𝐽) ∣ ((𝐹‘𝐶)‘𝑖) ≤ 0}𝑗 ≤ 𝑘)) → ((𝐹‘𝐶)‘𝑘) = 0)
222		ssrab2 3993	. . . . . 6 ⊢ {𝑖 ∈ (1...𝐽) ∣ ((𝐹‘𝐶)‘𝑖) ≤ 0} ⊆ (1...𝐽)
223	222, 12	sstri 3910	. . . . 5 ⊢ {𝑖 ∈ (1...𝐽) ∣ ((𝐹‘𝐶)‘𝑖) ≤ 0} ⊆ ℝ
224	223	a1i 11	. . . 4 ⊢ (𝜑 → {𝑖 ∈ (1...𝐽) ∣ ((𝐹‘𝐶)‘𝑖) ≤ 0} ⊆ ℝ)
225		fzfi 13545	. . . . . 6 ⊢ (1...𝐽) ∈ Fin
226		ssfi 8851	. . . . . 6 ⊢ (((1...𝐽) ∈ Fin ∧ {𝑖 ∈ (1...𝐽) ∣ ((𝐹‘𝐶)‘𝑖) ≤ 0} ⊆ (1...𝐽)) → {𝑖 ∈ (1...𝐽) ∣ ((𝐹‘𝐶)‘𝑖) ≤ 0} ∈ Fin)
227	225, 222, 226	mp2an 692	. . . . 5 ⊢ {𝑖 ∈ (1...𝐽) ∣ ((𝐹‘𝐶)‘𝑖) ≤ 0} ∈ Fin
228	227	a1i 11	. . . 4 ⊢ (𝜑 → {𝑖 ∈ (1...𝐽) ∣ ((𝐹‘𝐶)‘𝑖) ≤ 0} ∈ Fin)
229		rabn0 4300	. . . . 5 ⊢ ({𝑖 ∈ (1...𝐽) ∣ ((𝐹‘𝐶)‘𝑖) ≤ 0} ≠ ∅ ↔ ∃𝑖 ∈ (1...𝐽)((𝐹‘𝐶)‘𝑖) ≤ 0)
230	60, 229	sylibr 237	. . . 4 ⊢ (𝜑 → {𝑖 ∈ (1...𝐽) ∣ ((𝐹‘𝐶)‘𝑖) ≤ 0} ≠ ∅)
231		fimaxre 11776	. . . 4 ⊢ (({𝑖 ∈ (1...𝐽) ∣ ((𝐹‘𝐶)‘𝑖) ≤ 0} ⊆ ℝ ∧ {𝑖 ∈ (1...𝐽) ∣ ((𝐹‘𝐶)‘𝑖) ≤ 0} ∈ Fin ∧ {𝑖 ∈ (1...𝐽) ∣ ((𝐹‘𝐶)‘𝑖) ≤ 0} ≠ ∅) → ∃𝑘 ∈ {𝑖 ∈ (1...𝐽) ∣ ((𝐹‘𝐶)‘𝑖) ≤ 0}∀𝑗 ∈ {𝑖 ∈ (1...𝐽) ∣ ((𝐹‘𝐶)‘𝑖) ≤ 0}𝑗 ≤ 𝑘)
232	224, 228, 230, 231	syl3anc 1373	. . 3 ⊢ (𝜑 → ∃𝑘 ∈ {𝑖 ∈ (1...𝐽) ∣ ((𝐹‘𝐶)‘𝑖) ≤ 0}∀𝑗 ∈ {𝑖 ∈ (1...𝐽) ∣ ((𝐹‘𝐶)‘𝑖) ≤ 0}𝑗 ≤ 𝑘)
233	221, 232	reximddv 3194	. 2 ⊢ (𝜑 → ∃𝑘 ∈ {𝑖 ∈ (1...𝐽) ∣ ((𝐹‘𝐶)‘𝑖) ≤ 0} ((𝐹‘𝐶)‘𝑘) = 0)
234		elrabi 3596	. . . 4 ⊢ (𝑘 ∈ {𝑖 ∈ (1...𝐽) ∣ ((𝐹‘𝐶)‘𝑖) ≤ 0} → 𝑘 ∈ (1...𝐽))
235	234	anim1i 618	. . 3 ⊢ ((𝑘 ∈ {𝑖 ∈ (1...𝐽) ∣ ((𝐹‘𝐶)‘𝑖) ≤ 0} ∧ ((𝐹‘𝐶)‘𝑘) = 0) → (𝑘 ∈ (1...𝐽) ∧ ((𝐹‘𝐶)‘𝑘) = 0))
236	235	reximi2 3167	. 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 209 ∧ wa 399 ∨ wo 847 = wceq 1543 ∈ wcel 2110 ≠ wne 2940 ∀wral 3061 ∃wrex 3062 {crab 3065 ∖ cdif 3863 ∩ cin 3865 ⊆ wss 3866 ∅c0 4237 𝒫 cpw 4513 {csn 4541 class class class wbr 5053 ↦ cmpt 5135 ‘cfv 6380 (class class class)co 7213 Fincfn 8626 ℝcr 10728 0cc0 10729 1c1 10730 + caddc 10732 < clt 10867 ≤ cle 10868 − cmin 11062 / cdiv 11489 ℕcn 11830 2c2 11885 ℤcz 12176 ℤ_≥cuz 12438 ...cfz 13095 ♯chash 13896

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1803 ax-4 1817 ax-5 1918 ax-6 1976 ax-7 2016 ax-8 2112 ax-9 2120 ax-10 2141 ax-11 2158 ax-12 2175 ax-ext 2708 ax-rep 5179 ax-sep 5192 ax-nul 5199 ax-pow 5258 ax-pr 5322 ax-un 7523 ax-cnex 10785 ax-resscn 10786 ax-1cn 10787 ax-icn 10788 ax-addcl 10789 ax-addrcl 10790 ax-mulcl 10791 ax-mulrcl 10792 ax-mulcom 10793 ax-addass 10794 ax-mulass 10795 ax-distr 10796 ax-i2m1 10797 ax-1ne0 10798 ax-1rid 10799 ax-rnegex 10800 ax-rrecex 10801 ax-cnre 10802 ax-pre-lttri 10803 ax-pre-lttrn 10804 ax-pre-ltadd 10805 ax-pre-mulgt0 10806

This theorem depends on definitions: df-bi 210 df-an 400 df-or 848 df-3or 1090 df-3an 1091 df-tru 1546 df-fal 1556 df-ex 1788 df-nf 1792 df-sb 2071 df-mo 2539 df-eu 2568 df-clab 2715 df-cleq 2729 df-clel 2816 df-nfc 2886 df-ne 2941 df-nel 3047 df-ral 3066 df-rex 3067 df-reu 3068 df-rab 3070 df-v 3410 df-sbc 3695 df-csb 3812 df-dif 3869 df-un 3871 df-in 3873 df-ss 3883 df-pss 3885 df-nul 4238 df-if 4440 df-pw 4515 df-sn 4542 df-pr 4544 df-tp 4546 df-op 4548 df-uni 4820 df-int 4860 df-iun 4906 df-br 5054 df-opab 5116 df-mpt 5136 df-tr 5162 df-id 5455 df-eprel 5460 df-po 5468 df-so 5469 df-fr 5509 df-we 5511 df-xp 5557 df-rel 5558 df-cnv 5559 df-co 5560 df-dm 5561 df-rn 5562 df-res 5563 df-ima 5564 df-pred 6160 df-ord 6216 df-on 6217 df-lim 6218 df-suc 6219 df-iota 6338 df-fun 6382 df-fn 6383 df-f 6384 df-f1 6385 df-fo 6386 df-f1o 6387 df-fv 6388 df-riota 7170 df-ov 7216 df-oprab 7217 df-mpo 7218 df-om 7645 df-1st 7761 df-2nd 7762 df-wrecs 8047 df-recs 8108 df-rdg 8146 df-1o 8202 df-oadd 8206 df-er 8391 df-en 8627 df-dom 8628 df-sdom 8629 df-fin 8630 df-dju 9517 df-card 9555 df-pnf 10869 df-mnf 10870 df-xr 10871 df-ltxr 10872 df-le 10873 df-sub 11064 df-neg 11065 df-nn 11831 df-2 11893 df-n0 12091 df-z 12177 df-uz 12439 df-fz 13096 df-hash 13897

This theorem is referenced by: ballotlem5 32178 ballotlemic 32185

W3C validator