ballotlemfcc - Mathbox for Thierry Arnoux

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

Theorem ballotlemfcc 34828

Description: 𝐹 takes value 0 between positive and negative values. (Contributed by Thierry Arnoux, 2-Apr-2017.)

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

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

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

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

Step	Hyp	Ref	Expression
1		fveq2 6882	. . . . . . 7 ⊢ (𝑖 = 𝑘 → ((𝐹‘𝐶)‘𝑖) = ((𝐹‘𝐶)‘𝑘))
2	1	breq2d 5125	. . . . . 6 ⊢ (𝑖 = 𝑘 → (0 ≤ ((𝐹‘𝐶)‘𝑖) ↔ 0 ≤ ((𝐹‘𝐶)‘𝑘)))
3	2	elrab 3659	. . . . 5 ⊢ (𝑘 ∈ {𝑖 ∈ (1...𝐽) ∣ 0 ≤ ((𝐹‘𝐶)‘𝑖)} ↔ (𝑘 ∈ (1...𝐽) ∧ 0 ≤ ((𝐹‘𝐶)‘𝑘)))
4	3	anbi1i 635	. . . 4 ⊢ ((𝑘 ∈ {𝑖 ∈ (1...𝐽) ∣ 0 ≤ ((𝐹‘𝐶)‘𝑖)} ∧ ∀𝑗 ∈ {𝑖 ∈ (1...𝐽) ∣ 0 ≤ ((𝐹‘𝐶)‘𝑖)}𝑗 ≤ 𝑘) ↔ ((𝑘 ∈ (1...𝐽) ∧ 0 ≤ ((𝐹‘𝐶)‘𝑘)) ∧ ∀𝑗 ∈ {𝑖 ∈ (1...𝐽) ∣ 0 ≤ ((𝐹‘𝐶)‘𝑖)}𝑗 ≤ 𝑘))
5		simprl 782	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑘 ∈ (1...𝐽) ∧ 0 ≤ ((𝐹‘𝐶)‘𝑘))) → 𝑘 ∈ (1...𝐽))
6	5	adantrr 729	. . . . . . . . 9 ⊢ ((𝜑 ∧ ((𝑘 ∈ (1...𝐽) ∧ 0 ≤ ((𝐹‘𝐶)‘𝑘)) ∧ ∀𝑗 ∈ {𝑖 ∈ (1...𝐽) ∣ 0 ≤ ((𝐹‘𝐶)‘𝑖)}𝑗 ≤ 𝑘)) → 𝑘 ∈ (1...𝐽))
7		fzssuz 13592	. . . . . . . . . . . . . 14 ⊢ (1...𝐽) ⊆ (ℤ_≥‘1)
8		uzssz 12882	. . . . . . . . . . . . . 14 ⊢ (ℤ_≥‘1) ⊆ ℤ
9	7, 8	sstri 3954	. . . . . . . . . . . . 13 ⊢ (1...𝐽) ⊆ ℤ
10		zssre 12597	. . . . . . . . . . . . 13 ⊢ ℤ ⊆ ℝ
11	9, 10	sstri 3954	. . . . . . . . . . . 12 ⊢ (1...𝐽) ⊆ ℝ
12	11	sseli 3941	. . . . . . . . . . 11 ⊢ (𝑘 ∈ (1...𝐽) → 𝑘 ∈ ℝ)
13	12	ltp1d 12144	. . . . . . . . . 10 ⊢ (𝑘 ∈ (1...𝐽) → 𝑘 < (𝑘 + 1))
14		1red 11208	. . . . . . . . . . . 12 ⊢ (𝑘 ∈ (1...𝐽) → 1 ∈ ℝ)
15	12, 14	readdcld 11237	. . . . . . . . . . 11 ⊢ (𝑘 ∈ (1...𝐽) → (𝑘 + 1) ∈ ℝ)
16	12, 15	ltnled 11356	. . . . . . . . . 10 ⊢ (𝑘 ∈ (1...𝐽) → (𝑘 < (𝑘 + 1) ↔ ¬ (𝑘 + 1) ≤ 𝑘))
17	13, 16	mpbid 235	. . . . . . . . 9 ⊢ (𝑘 ∈ (1...𝐽) → ¬ (𝑘 + 1) ≤ 𝑘)
18	6, 17	syl 18	. . . . . . . 8 ⊢ ((𝜑 ∧ ((𝑘 ∈ (1...𝐽) ∧ 0 ≤ ((𝐹‘𝐶)‘𝑘)) ∧ ∀𝑗 ∈ {𝑖 ∈ (1...𝐽) ∣ 0 ≤ ((𝐹‘𝐶)‘𝑖)}𝑗 ≤ 𝑘)) → ¬ (𝑘 + 1) ≤ 𝑘)
19		simprr 784	. . . . . . . . 9 ⊢ ((𝜑 ∧ ((𝑘 ∈ (1...𝐽) ∧ 0 ≤ ((𝐹‘𝐶)‘𝑘)) ∧ ∀𝑗 ∈ {𝑖 ∈ (1...𝐽) ∣ 0 ≤ ((𝐹‘𝐶)‘𝑖)}𝑗 ≤ 𝑘)) → ∀𝑗 ∈ {𝑖 ∈ (1...𝐽) ∣ 0 ≤ ((𝐹‘𝐶)‘𝑖)}𝑗 ≤ 𝑘)
20		ballotlemfcc.4	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ((𝐹‘𝐶)‘𝐽) < 0)
21	20	adantr 485	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑘 = 𝐽) → ((𝐹‘𝐶)‘𝐽) < 0)
22		simpr 489	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑘 = 𝐽) → 𝑘 = 𝐽)
23	22	fveq2d 6886	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑘 = 𝐽) → ((𝐹‘𝐶)‘𝑘) = ((𝐹‘𝐶)‘𝐽))
24	23	breq1d 5123	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑘 = 𝐽) → (((𝐹‘𝐶)‘𝑘) < 0 ↔ ((𝐹‘𝐶)‘𝐽) < 0))
25		ballotlemfcc.j	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜑 → 𝐽 ∈ ℕ)
26		elnnuz 12901	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝐽 ∈ ℕ ↔ 𝐽 ∈ (ℤ_≥‘1))
27	25, 26	sylib 221	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → 𝐽 ∈ (ℤ_≥‘1))
28		eluzfz2 13559	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝐽 ∈ (ℤ_≥‘1) → 𝐽 ∈ (1...𝐽))
29	27, 28	syl 18	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → 𝐽 ∈ (1...𝐽))
30		eleq1 2857	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑘 = 𝐽 → (𝑘 ∈ (1...𝐽) ↔ 𝐽 ∈ (1...𝐽)))
31	29, 30	syl5ibrcom 250	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → (𝑘 = 𝐽 → 𝑘 ∈ (1...𝐽)))
32	31	anc2li 564	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (𝑘 = 𝐽 → (𝜑 ∧ 𝑘 ∈ (1...𝐽))))
33		1eluzge0 12903	. . . . . . . . . . . . . . . . . . . 20 ⊢ 1 ∈ (ℤ_≥‘0)
34		fzss1 13590	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (1 ∈ (ℤ_≥‘0) → (1...𝐽) ⊆ (0...𝐽))
35	34	sseld 3944	. . . . . . . . . . . . . . . . . . . 20 ⊢ (1 ∈ (ℤ_≥‘0) → (𝑘 ∈ (1...𝐽) → 𝑘 ∈ (0...𝐽)))
36	33, 35	ax-mp 5	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑘 ∈ (1...𝐽) → 𝑘 ∈ (0...𝐽))
37		ballotth.m	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ 𝑀 ∈ ℕ
38		ballotth.n	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ 𝑁 ∈ ℕ
39		ballotth.o	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ 𝑂 = {𝑐 ∈ 𝒫 (1...(𝑀 + 𝑁)) ∣ (♯‘𝑐) = 𝑀}
40		ballotth.p	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ 𝑃 = (𝑥 ∈ 𝒫 𝑂 ↦ ((♯‘𝑥) / (♯‘𝑂)))
41		ballotth.f	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ 𝐹 = (𝑐 ∈ 𝑂 ↦ (𝑖 ∈ ℤ ↦ ((♯‘((1...𝑖) ∩ 𝑐)) − (♯‘((1...𝑖) ∖ 𝑐)))))
42		ballotlemfcc.c	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝜑 → 𝐶 ∈ 𝑂)
43	42	adantr 485	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝐽)) → 𝐶 ∈ 𝑂)
44		elfzelz 13551	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑘 ∈ (0...𝐽) → 𝑘 ∈ ℤ)
45	44	adantl 486	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝐽)) → 𝑘 ∈ ℤ)
46	37, 38, 39, 40, 41, 43, 45	ballotlemfelz 34825	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝐽)) → ((𝐹‘𝐶)‘𝑘) ∈ ℤ)
47	46	zred 12699	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝐽)) → ((𝐹‘𝐶)‘𝑘) ∈ ℝ)
48		0red 11210	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝐽)) → 0 ∈ ℝ)
49	47, 48	ltnled 11356	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝐽)) → (((𝐹‘𝐶)‘𝑘) < 0 ↔ ¬ 0 ≤ ((𝐹‘𝐶)‘𝑘)))
50	36, 49	sylan2 604	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑘 ∈ (1...𝐽)) → (((𝐹‘𝐶)‘𝑘) < 0 ↔ ¬ 0 ≤ ((𝐹‘𝐶)‘𝑘)))
51	32, 50	syl6 36	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (𝑘 = 𝐽 → (((𝐹‘𝐶)‘𝑘) < 0 ↔ ¬ 0 ≤ ((𝐹‘𝐶)‘𝑘))))
52	51	imp 411	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑘 = 𝐽) → (((𝐹‘𝐶)‘𝑘) < 0 ↔ ¬ 0 ≤ ((𝐹‘𝐶)‘𝑘)))
53	24, 52	bitr3d 284	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑘 = 𝐽) → (((𝐹‘𝐶)‘𝐽) < 0 ↔ ¬ 0 ≤ ((𝐹‘𝐶)‘𝑘)))
54	21, 53	mpbid 235	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑘 = 𝐽) → ¬ 0 ≤ ((𝐹‘𝐶)‘𝑘))
55	54	ex 417	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝑘 = 𝐽 → ¬ 0 ≤ ((𝐹‘𝐶)‘𝑘)))
56	55	con2d 135	. . . . . . . . . . . 12 ⊢ (𝜑 → (0 ≤ ((𝐹‘𝐶)‘𝑘) → ¬ 𝑘 = 𝐽))
57		nn1m1nn 12253	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝐽 ∈ ℕ → (𝐽 = 1 ∨ (𝐽 − 1) ∈ ℕ))
58	25, 57	syl 18	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → (𝐽 = 1 ∨ (𝐽 − 1) ∈ ℕ))
59		ballotlemfcc.3	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝜑 → ∃𝑖 ∈ (1...𝐽)0 ≤ ((𝐹‘𝐶)‘𝑖))
60	59	adantr 485	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝜑 ∧ 𝐽 = 1) → ∃𝑖 ∈ (1...𝐽)0 ≤ ((𝐹‘𝐶)‘𝑖))
61		oveq1 7418	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝐽 = 1 → (𝐽...𝐽) = (1...𝐽))
62	61	adantl 486	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝜑 ∧ 𝐽 = 1) → (𝐽...𝐽) = (1...𝐽))
63	25	nnzd 12616	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝜑 → 𝐽 ∈ ℤ)
64		fzsn 13593	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝐽 ∈ ℤ → (𝐽...𝐽) = {𝐽})
65	63, 64	syl 18	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝜑 → (𝐽...𝐽) = {𝐽})
66	65	adantr 485	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝜑 ∧ 𝐽 = 1) → (𝐽...𝐽) = {𝐽})
67	62, 66	eqtr3d 2806	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝜑 ∧ 𝐽 = 1) → (1...𝐽) = {𝐽})
68	60, 67	rexeqtrdv 3332	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝜑 ∧ 𝐽 = 1) → ∃𝑖 ∈ {𝐽}0 ≤ ((𝐹‘𝐶)‘𝑖))
69		fveq2 6882	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝑖 = 𝐽 → ((𝐹‘𝐶)‘𝑖) = ((𝐹‘𝐶)‘𝐽))
70	69	breq2d 5125	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑖 = 𝐽 → (0 ≤ ((𝐹‘𝐶)‘𝑖) ↔ 0 ≤ ((𝐹‘𝐶)‘𝐽)))
71	70	rexsng 4647	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝐽 ∈ ℕ → (∃𝑖 ∈ {𝐽}0 ≤ ((𝐹‘𝐶)‘𝑖) ↔ 0 ≤ ((𝐹‘𝐶)‘𝐽)))
72	25, 71	syl 18	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝜑 → (∃𝑖 ∈ {𝐽}0 ≤ ((𝐹‘𝐶)‘𝑖) ↔ 0 ≤ ((𝐹‘𝐶)‘𝐽)))
73	72	adantr 485	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝜑 ∧ 𝐽 = 1) → (∃𝑖 ∈ {𝐽}0 ≤ ((𝐹‘𝐶)‘𝑖) ↔ 0 ≤ ((𝐹‘𝐶)‘𝐽)))
74	68, 73	mpbid 235	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ 𝐽 = 1) → 0 ≤ ((𝐹‘𝐶)‘𝐽))
75	20	adantr 485	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝜑 ∧ 𝐽 = 1) → ((𝐹‘𝐶)‘𝐽) < 0)
76	37, 38, 39, 40, 41, 42, 63	ballotlemfelz 34825	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝜑 → ((𝐹‘𝐶)‘𝐽) ∈ ℤ)
77	76	zred 12699	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝜑 → ((𝐹‘𝐶)‘𝐽) ∈ ℝ)
78		0red 11210	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝜑 → 0 ∈ ℝ)
79	77, 78	ltnled 11356	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝜑 → (((𝐹‘𝐶)‘𝐽) < 0 ↔ ¬ 0 ≤ ((𝐹‘𝐶)‘𝐽)))
80	79	adantr 485	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝜑 ∧ 𝐽 = 1) → (((𝐹‘𝐶)‘𝐽) < 0 ↔ ¬ 0 ≤ ((𝐹‘𝐶)‘𝐽)))
81	75, 80	mpbid 235	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ 𝐽 = 1) → ¬ 0 ≤ ((𝐹‘𝐶)‘𝐽))
82	74, 81	pm2.65da 828	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜑 → ¬ 𝐽 = 1)
83		biortn 950	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (¬ 𝐽 = 1 → ((𝐽 − 1) ∈ ℕ ↔ (¬ ¬ 𝐽 = 1 ∨ (𝐽 − 1) ∈ ℕ)))
84	82, 83	syl 18	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → ((𝐽 − 1) ∈ ℕ ↔ (¬ ¬ 𝐽 = 1 ∨ (𝐽 − 1) ∈ ℕ)))
85		notnotb 318	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝐽 = 1 ↔ ¬ ¬ 𝐽 = 1)
86	85	orbi1i 926	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝐽 = 1 ∨ (𝐽 − 1) ∈ ℕ) ↔ (¬ ¬ 𝐽 = 1 ∨ (𝐽 − 1) ∈ ℕ))
87	84, 86	bitr4di 292	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → ((𝐽 − 1) ∈ ℕ ↔ (𝐽 = 1 ∨ (𝐽 − 1) ∈ ℕ)))
88	58, 87	mpbird 260	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → (𝐽 − 1) ∈ ℕ)
89		elnnuz 12901	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝐽 − 1) ∈ ℕ ↔ (𝐽 − 1) ∈ (ℤ_≥‘1))
90	88, 89	sylib 221	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (𝐽 − 1) ∈ (ℤ_≥‘1))
91		elfzp1 13601	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝐽 − 1) ∈ (ℤ_≥‘1) → (𝑘 ∈ (1...((𝐽 − 1) + 1)) ↔ (𝑘 ∈ (1...(𝐽 − 1)) ∨ 𝑘 = ((𝐽 − 1) + 1))))
92	90, 91	syl 18	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (𝑘 ∈ (1...((𝐽 − 1) + 1)) ↔ (𝑘 ∈ (1...(𝐽 − 1)) ∨ 𝑘 = ((𝐽 − 1) + 1))))
93	25	nncnd 12248	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → 𝐽 ∈ ℂ)
94		1cnd 11201	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → 1 ∈ ℂ)
95	93, 94	npcand 11572	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → ((𝐽 − 1) + 1) = 𝐽)
96	95	oveq2d 7427	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (1...((𝐽 − 1) + 1)) = (1...𝐽))
97	96	eleq2d 2855	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (𝑘 ∈ (1...((𝐽 − 1) + 1)) ↔ 𝑘 ∈ (1...𝐽)))
98	95	eqeq2d 2780	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (𝑘 = ((𝐽 − 1) + 1) ↔ 𝑘 = 𝐽))
99	98	orbi2d 928	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → ((𝑘 ∈ (1...(𝐽 − 1)) ∨ 𝑘 = ((𝐽 − 1) + 1)) ↔ (𝑘 ∈ (1...(𝐽 − 1)) ∨ 𝑘 = 𝐽)))
100	92, 97, 99	3bitr3d 312	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (𝑘 ∈ (1...𝐽) ↔ (𝑘 ∈ (1...(𝐽 − 1)) ∨ 𝑘 = 𝐽)))
101		orcom 883	. . . . . . . . . . . . . . . 16 ⊢ ((𝑘 ∈ (1...(𝐽 − 1)) ∨ 𝑘 = 𝐽) ↔ (𝑘 = 𝐽 ∨ 𝑘 ∈ (1...(𝐽 − 1))))
102	100, 101	bitrdi 290	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝑘 ∈ (1...𝐽) ↔ (𝑘 = 𝐽 ∨ 𝑘 ∈ (1...(𝐽 − 1)))))
103	102	biimpd 232	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝑘 ∈ (1...𝐽) → (𝑘 = 𝐽 ∨ 𝑘 ∈ (1...(𝐽 − 1)))))
104		pm5.6 1017	. . . . . . . . . . . . . 14 ⊢ (((𝑘 ∈ (1...𝐽) ∧ ¬ 𝑘 = 𝐽) → 𝑘 ∈ (1...(𝐽 − 1))) ↔ (𝑘 ∈ (1...𝐽) → (𝑘 = 𝐽 ∨ 𝑘 ∈ (1...(𝐽 − 1)))))
105	103, 104	sylibr 237	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((𝑘 ∈ (1...𝐽) ∧ ¬ 𝑘 = 𝐽) → 𝑘 ∈ (1...(𝐽 − 1))))
106	88	nnzd 12616	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → (𝐽 − 1) ∈ ℤ)
107		1z 12623	. . . . . . . . . . . . . . . . . . 19 ⊢ 1 ∈ ℤ
108	106, 107	jctil 528	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (1 ∈ ℤ ∧ (𝐽 − 1) ∈ ℤ))
109		elfzelz 13551	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑘 ∈ (1...(𝐽 − 1)) → 𝑘 ∈ ℤ)
110	109, 107	jctir 529	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑘 ∈ (1...(𝐽 − 1)) → (𝑘 ∈ ℤ ∧ 1 ∈ ℤ))
111		fzaddel 13585	. . . . . . . . . . . . . . . . . 18 ⊢ (((1 ∈ ℤ ∧ (𝐽 − 1) ∈ ℤ) ∧ (𝑘 ∈ ℤ ∧ 1 ∈ ℤ)) → (𝑘 ∈ (1...(𝐽 − 1)) ↔ (𝑘 + 1) ∈ ((1 + 1)...((𝐽 − 1) + 1))))
112	108, 110, 111	syl2an 607	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑘 ∈ (1...(𝐽 − 1))) → (𝑘 ∈ (1...(𝐽 − 1)) ↔ (𝑘 + 1) ∈ ((1 + 1)...((𝐽 − 1) + 1))))
113	112	biimp3a 1495	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑘 ∈ (1...(𝐽 − 1)) ∧ 𝑘 ∈ (1...(𝐽 − 1))) → (𝑘 + 1) ∈ ((1 + 1)...((𝐽 − 1) + 1)))
114	113	3anidm23 1446	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑘 ∈ (1...(𝐽 − 1))) → (𝑘 + 1) ∈ ((1 + 1)...((𝐽 − 1) + 1)))
115		1p1e2 12363	. . . . . . . . . . . . . . . . . . . 20 ⊢ (1 + 1) = 2
116	115	a1i 11	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → (1 + 1) = 2)
117	116, 95	oveq12d 7429	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → ((1 + 1)...((𝐽 − 1) + 1)) = (2...𝐽))
118	117	eleq2d 2855	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → ((𝑘 + 1) ∈ ((1 + 1)...((𝐽 − 1) + 1)) ↔ (𝑘 + 1) ∈ (2...𝐽)))
119		2eluzge1 12905	. . . . . . . . . . . . . . . . . . 19 ⊢ 2 ∈ (ℤ_≥‘1)
120		fzss1 13590	. . . . . . . . . . . . . . . . . . 19 ⊢ (2 ∈ (ℤ_≥‘1) → (2...𝐽) ⊆ (1...𝐽))
121	119, 120	ax-mp 5	. . . . . . . . . . . . . . . . . 18 ⊢ (2...𝐽) ⊆ (1...𝐽)
122	121	sseli 3941	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑘 + 1) ∈ (2...𝐽) → (𝑘 + 1) ∈ (1...𝐽))
123	118, 122	biimtrdi 256	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ((𝑘 + 1) ∈ ((1 + 1)...((𝐽 − 1) + 1)) → (𝑘 + 1) ∈ (1...𝐽)))
124	123	adantr 485	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑘 ∈ (1...(𝐽 − 1))) → ((𝑘 + 1) ∈ ((1 + 1)...((𝐽 − 1) + 1)) → (𝑘 + 1) ∈ (1...𝐽)))
125	114, 124	mpd 16	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑘 ∈ (1...(𝐽 − 1))) → (𝑘 + 1) ∈ (1...𝐽))
126	125	ex 417	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝑘 ∈ (1...(𝐽 − 1)) → (𝑘 + 1) ∈ (1...𝐽)))
127	105, 126	syld 48	. . . . . . . . . . . 12 ⊢ (𝜑 → ((𝑘 ∈ (1...𝐽) ∧ ¬ 𝑘 = 𝐽) → (𝑘 + 1) ∈ (1...𝐽)))
128	56, 127	sylan2d 616	. . . . . . . . . . 11 ⊢ (𝜑 → ((𝑘 ∈ (1...𝐽) ∧ 0 ≤ ((𝐹‘𝐶)‘𝑘)) → (𝑘 + 1) ∈ (1...𝐽)))
129	128	imp 411	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑘 ∈ (1...𝐽) ∧ 0 ≤ ((𝐹‘𝐶)‘𝑘))) → (𝑘 + 1) ∈ (1...𝐽))
130	129	adantrr 729	. . . . . . . . 9 ⊢ ((𝜑 ∧ ((𝑘 ∈ (1...𝐽) ∧ 0 ≤ ((𝐹‘𝐶)‘𝑘)) ∧ ∀𝑗 ∈ {𝑖 ∈ (1...𝐽) ∣ 0 ≤ ((𝐹‘𝐶)‘𝑖)}𝑗 ≤ 𝑘)) → (𝑘 + 1) ∈ (1...𝐽))
131		fveq2 6882	. . . . . . . . . . . . . 14 ⊢ (𝑖 = (𝑘 + 1) → ((𝐹‘𝐶)‘𝑖) = ((𝐹‘𝐶)‘(𝑘 + 1)))
132	131	breq2d 5125	. . . . . . . . . . . . 13 ⊢ (𝑖 = (𝑘 + 1) → (0 ≤ ((𝐹‘𝐶)‘𝑖) ↔ 0 ≤ ((𝐹‘𝐶)‘(𝑘 + 1))))
133	132	elrab 3659	. . . . . . . . . . . 12 ⊢ ((𝑘 + 1) ∈ {𝑖 ∈ (1...𝐽) ∣ 0 ≤ ((𝐹‘𝐶)‘𝑖)} ↔ ((𝑘 + 1) ∈ (1...𝐽) ∧ 0 ≤ ((𝐹‘𝐶)‘(𝑘 + 1))))
134		breq1 5116	. . . . . . . . . . . . 13 ⊢ (𝑗 = (𝑘 + 1) → (𝑗 ≤ 𝑘 ↔ (𝑘 + 1) ≤ 𝑘))
135	134	rspccva 3589	. . . . . . . . . . . 12 ⊢ ((∀𝑗 ∈ {𝑖 ∈ (1...𝐽) ∣ 0 ≤ ((𝐹‘𝐶)‘𝑖)}𝑗 ≤ 𝑘 ∧ (𝑘 + 1) ∈ {𝑖 ∈ (1...𝐽) ∣ 0 ≤ ((𝐹‘𝐶)‘𝑖)}) → (𝑘 + 1) ≤ 𝑘)
136	133, 135	sylan2br 606	. . . . . . . . . . 11 ⊢ ((∀𝑗 ∈ {𝑖 ∈ (1...𝐽) ∣ 0 ≤ ((𝐹‘𝐶)‘𝑖)}𝑗 ≤ 𝑘 ∧ ((𝑘 + 1) ∈ (1...𝐽) ∧ 0 ≤ ((𝐹‘𝐶)‘(𝑘 + 1)))) → (𝑘 + 1) ≤ 𝑘)
137	136	expr 461	. . . . . . . . . 10 ⊢ ((∀𝑗 ∈ {𝑖 ∈ (1...𝐽) ∣ 0 ≤ ((𝐹‘𝐶)‘𝑖)}𝑗 ≤ 𝑘 ∧ (𝑘 + 1) ∈ (1...𝐽)) → (0 ≤ ((𝐹‘𝐶)‘(𝑘 + 1)) → (𝑘 + 1) ≤ 𝑘))
138	137	con3d 153	. . . . . . . . 9 ⊢ ((∀𝑗 ∈ {𝑖 ∈ (1...𝐽) ∣ 0 ≤ ((𝐹‘𝐶)‘𝑖)}𝑗 ≤ 𝑘 ∧ (𝑘 + 1) ∈ (1...𝐽)) → (¬ (𝑘 + 1) ≤ 𝑘 → ¬ 0 ≤ ((𝐹‘𝐶)‘(𝑘 + 1))))
139	19, 130, 138	syl2anc 595	. . . . . . . 8 ⊢ ((𝜑 ∧ ((𝑘 ∈ (1...𝐽) ∧ 0 ≤ ((𝐹‘𝐶)‘𝑘)) ∧ ∀𝑗 ∈ {𝑖 ∈ (1...𝐽) ∣ 0 ≤ ((𝐹‘𝐶)‘𝑖)}𝑗 ≤ 𝑘)) → (¬ (𝑘 + 1) ≤ 𝑘 → ¬ 0 ≤ ((𝐹‘𝐶)‘(𝑘 + 1))))
140	18, 139	mpd 16	. . . . . . 7 ⊢ ((𝜑 ∧ ((𝑘 ∈ (1...𝐽) ∧ 0 ≤ ((𝐹‘𝐶)‘𝑘)) ∧ ∀𝑗 ∈ {𝑖 ∈ (1...𝐽) ∣ 0 ≤ ((𝐹‘𝐶)‘𝑖)}𝑗 ≤ 𝑘)) → ¬ 0 ≤ ((𝐹‘𝐶)‘(𝑘 + 1)))
141		simplrr 789	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ ((𝑘 ∈ (1...𝐽) ∧ 0 ≤ ((𝐹‘𝐶)‘𝑘)) ∧ ∀𝑗 ∈ {𝑖 ∈ (1...𝐽) ∣ 0 ≤ ((𝐹‘𝐶)‘𝑖)}𝑗 ≤ 𝑘)) ∧ (𝑘 + 1) ∈ 𝐶) → ∀𝑗 ∈ {𝑖 ∈ (1...𝐽) ∣ 0 ≤ ((𝐹‘𝐶)‘𝑖)}𝑗 ≤ 𝑘)
142	130	adantr 485	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ ((𝑘 ∈ (1...𝐽) ∧ 0 ≤ ((𝐹‘𝐶)‘𝑘)) ∧ ∀𝑗 ∈ {𝑖 ∈ (1...𝐽) ∣ 0 ≤ ((𝐹‘𝐶)‘𝑖)}𝑗 ≤ 𝑘)) ∧ (𝑘 + 1) ∈ 𝐶) → (𝑘 + 1) ∈ (1...𝐽))
143		0red 11210	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑘 ∈ (1...𝐽) ∧ 0 ≤ ((𝐹‘𝐶)‘𝑘))) ∧ (𝑘 + 1) ∈ 𝐶) → 0 ∈ ℝ)
144		simpll 778	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (𝑘 ∈ (1...𝐽) ∧ 0 ≤ ((𝐹‘𝐶)‘𝑘))) ∧ (𝑘 + 1) ∈ 𝐶) → 𝜑)
145	129	adantr 485	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ (𝑘 ∈ (1...𝐽) ∧ 0 ≤ ((𝐹‘𝐶)‘𝑘))) ∧ (𝑘 + 1) ∈ 𝐶) → (𝑘 + 1) ∈ (1...𝐽))
146	34	sseld 3944	. . . . . . . . . . . . . . 15 ⊢ (1 ∈ (ℤ_≥‘0) → ((𝑘 + 1) ∈ (1...𝐽) → (𝑘 + 1) ∈ (0...𝐽)))
147	33, 145, 146	mpsyl 69	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (𝑘 ∈ (1...𝐽) ∧ 0 ≤ ((𝐹‘𝐶)‘𝑘))) ∧ (𝑘 + 1) ∈ 𝐶) → (𝑘 + 1) ∈ (0...𝐽))
148	42	adantr 485	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ (𝑘 + 1) ∈ (0...𝐽)) → 𝐶 ∈ 𝑂)
149		elfzelz 13551	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑘 + 1) ∈ (0...𝐽) → (𝑘 + 1) ∈ ℤ)
150	149	adantl 486	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ (𝑘 + 1) ∈ (0...𝐽)) → (𝑘 + 1) ∈ ℤ)
151	37, 38, 39, 40, 41, 148, 150	ballotlemfelz 34825	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ (𝑘 + 1) ∈ (0...𝐽)) → ((𝐹‘𝐶)‘(𝑘 + 1)) ∈ ℤ)
152	151	zred 12699	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑘 + 1) ∈ (0...𝐽)) → ((𝐹‘𝐶)‘(𝑘 + 1)) ∈ ℝ)
153	144, 147, 152	syl2anc 595	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑘 ∈ (1...𝐽) ∧ 0 ≤ ((𝐹‘𝐶)‘𝑘))) ∧ (𝑘 + 1) ∈ 𝐶) → ((𝐹‘𝐶)‘(𝑘 + 1)) ∈ ℝ)
154		simplrr 789	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (𝑘 ∈ (1...𝐽) ∧ 0 ≤ ((𝐹‘𝐶)‘𝑘))) ∧ (𝑘 + 1) ∈ 𝐶) → 0 ≤ ((𝐹‘𝐶)‘𝑘))
155	5	adantr 485	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ (𝑘 ∈ (1...𝐽) ∧ 0 ≤ ((𝐹‘𝐶)‘𝑘))) ∧ (𝑘 + 1) ∈ 𝐶) → 𝑘 ∈ (1...𝐽))
156	155, 36	syl 18	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ (𝑘 ∈ (1...𝐽) ∧ 0 ≤ ((𝐹‘𝐶)‘𝑘))) ∧ (𝑘 + 1) ∈ 𝐶) → 𝑘 ∈ (0...𝐽))
157	128	imdistani 578	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ (𝑘 ∈ (1...𝐽) ∧ 0 ≤ ((𝐹‘𝐶)‘𝑘))) → (𝜑 ∧ (𝑘 + 1) ∈ (1...𝐽)))
158	42	adantr 485	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ (𝑘 + 1) ∈ (1...𝐽)) → 𝐶 ∈ 𝑂)
159		elfznn 13580	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑘 + 1) ∈ (1...𝐽) → (𝑘 + 1) ∈ ℕ)
160	159	adantl 486	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ (𝑘 + 1) ∈ (1...𝐽)) → (𝑘 + 1) ∈ ℕ)
161	37, 38, 39, 40, 41, 158, 160	ballotlemfp1 34826	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ (𝑘 + 1) ∈ (1...𝐽)) → ((¬ (𝑘 + 1) ∈ 𝐶 → ((𝐹‘𝐶)‘(𝑘 + 1)) = (((𝐹‘𝐶)‘((𝑘 + 1) − 1)) − 1)) ∧ ((𝑘 + 1) ∈ 𝐶 → ((𝐹‘𝐶)‘(𝑘 + 1)) = (((𝐹‘𝐶)‘((𝑘 + 1) − 1)) + 1))))
162	161	simprd 500	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ (𝑘 + 1) ∈ (1...𝐽)) → ((𝑘 + 1) ∈ 𝐶 → ((𝐹‘𝐶)‘(𝑘 + 1)) = (((𝐹‘𝐶)‘((𝑘 + 1) − 1)) + 1)))
163	162	imp 411	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ (𝑘 + 1) ∈ (1...𝐽)) ∧ (𝑘 + 1) ∈ 𝐶) → ((𝐹‘𝐶)‘(𝑘 + 1)) = (((𝐹‘𝐶)‘((𝑘 + 1) − 1)) + 1))
164	157, 163	sylan 591	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ (𝑘 ∈ (1...𝐽) ∧ 0 ≤ ((𝐹‘𝐶)‘𝑘))) ∧ (𝑘 + 1) ∈ 𝐶) → ((𝐹‘𝐶)‘(𝑘 + 1)) = (((𝐹‘𝐶)‘((𝑘 + 1) − 1)) + 1))
165		elfzelz 13551	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑘 ∈ (1...𝐽) → 𝑘 ∈ ℤ)
166	165	zcnd 12700	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑘 ∈ (1...𝐽) → 𝑘 ∈ ℂ)
167		1cnd 11201	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑘 ∈ (1...𝐽) → 1 ∈ ℂ)
168	166, 167	pncand 11569	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑘 ∈ (1...𝐽) → ((𝑘 + 1) − 1) = 𝑘)
169	168	fveq2d 6886	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑘 ∈ (1...𝐽) → ((𝐹‘𝐶)‘((𝑘 + 1) − 1)) = ((𝐹‘𝐶)‘𝑘))
170	169	oveq1d 7426	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑘 ∈ (1...𝐽) → (((𝐹‘𝐶)‘((𝑘 + 1) − 1)) + 1) = (((𝐹‘𝐶)‘𝑘) + 1))
171	170	eqeq2d 2780	. . . . . . . . . . . . . . . . 17 ⊢ (𝑘 ∈ (1...𝐽) → (((𝐹‘𝐶)‘(𝑘 + 1)) = (((𝐹‘𝐶)‘((𝑘 + 1) − 1)) + 1) ↔ ((𝐹‘𝐶)‘(𝑘 + 1)) = (((𝐹‘𝐶)‘𝑘) + 1)))
172	155, 171	syl 18	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ (𝑘 ∈ (1...𝐽) ∧ 0 ≤ ((𝐹‘𝐶)‘𝑘))) ∧ (𝑘 + 1) ∈ 𝐶) → (((𝐹‘𝐶)‘(𝑘 + 1)) = (((𝐹‘𝐶)‘((𝑘 + 1) − 1)) + 1) ↔ ((𝐹‘𝐶)‘(𝑘 + 1)) = (((𝐹‘𝐶)‘𝑘) + 1)))
173	164, 172	mpbid 235	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ (𝑘 ∈ (1...𝐽) ∧ 0 ≤ ((𝐹‘𝐶)‘𝑘))) ∧ (𝑘 + 1) ∈ 𝐶) → ((𝐹‘𝐶)‘(𝑘 + 1)) = (((𝐹‘𝐶)‘𝑘) + 1))
174		0z 12601	. . . . . . . . . . . . . . . . . 18 ⊢ 0 ∈ ℤ
175		zleltp1 12644	. . . . . . . . . . . . . . . . . 18 ⊢ ((0 ∈ ℤ ∧ ((𝐹‘𝐶)‘𝑘) ∈ ℤ) → (0 ≤ ((𝐹‘𝐶)‘𝑘) ↔ 0 < (((𝐹‘𝐶)‘𝑘) + 1)))
176	174, 46, 175	sylancr 598	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝐽)) → (0 ≤ ((𝐹‘𝐶)‘𝑘) ↔ 0 < (((𝐹‘𝐶)‘𝑘) + 1)))
177	176	adantr 485	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑘 ∈ (0...𝐽)) ∧ ((𝐹‘𝐶)‘(𝑘 + 1)) = (((𝐹‘𝐶)‘𝑘) + 1)) → (0 ≤ ((𝐹‘𝐶)‘𝑘) ↔ 0 < (((𝐹‘𝐶)‘𝑘) + 1)))
178		breq2 5117	. . . . . . . . . . . . . . . . 17 ⊢ (((𝐹‘𝐶)‘(𝑘 + 1)) = (((𝐹‘𝐶)‘𝑘) + 1) → (0 < ((𝐹‘𝐶)‘(𝑘 + 1)) ↔ 0 < (((𝐹‘𝐶)‘𝑘) + 1)))
179	178	adantl 486	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑘 ∈ (0...𝐽)) ∧ ((𝐹‘𝐶)‘(𝑘 + 1)) = (((𝐹‘𝐶)‘𝑘) + 1)) → (0 < ((𝐹‘𝐶)‘(𝑘 + 1)) ↔ 0 < (((𝐹‘𝐶)‘𝑘) + 1)))
180	177, 179	bitr4d 285	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑘 ∈ (0...𝐽)) ∧ ((𝐹‘𝐶)‘(𝑘 + 1)) = (((𝐹‘𝐶)‘𝑘) + 1)) → (0 ≤ ((𝐹‘𝐶)‘𝑘) ↔ 0 < ((𝐹‘𝐶)‘(𝑘 + 1))))
181	144, 156, 173, 180	syl21anc 850	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (𝑘 ∈ (1...𝐽) ∧ 0 ≤ ((𝐹‘𝐶)‘𝑘))) ∧ (𝑘 + 1) ∈ 𝐶) → (0 ≤ ((𝐹‘𝐶)‘𝑘) ↔ 0 < ((𝐹‘𝐶)‘(𝑘 + 1))))
182	154, 181	mpbid 235	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑘 ∈ (1...𝐽) ∧ 0 ≤ ((𝐹‘𝐶)‘𝑘))) ∧ (𝑘 + 1) ∈ 𝐶) → 0 < ((𝐹‘𝐶)‘(𝑘 + 1)))
183	143, 153, 182	ltled 11357	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝑘 ∈ (1...𝐽) ∧ 0 ≤ ((𝐹‘𝐶)‘𝑘))) ∧ (𝑘 + 1) ∈ 𝐶) → 0 ≤ ((𝐹‘𝐶)‘(𝑘 + 1)))
184	183	adantlrr 733	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ ((𝑘 ∈ (1...𝐽) ∧ 0 ≤ ((𝐹‘𝐶)‘𝑘)) ∧ ∀𝑗 ∈ {𝑖 ∈ (1...𝐽) ∣ 0 ≤ ((𝐹‘𝐶)‘𝑖)}𝑗 ≤ 𝑘)) ∧ (𝑘 + 1) ∈ 𝐶) → 0 ≤ ((𝐹‘𝐶)‘(𝑘 + 1)))
185	141, 142, 184, 136	syl12anc 849	. . . . . . . . . 10 ⊢ (((𝜑 ∧ ((𝑘 ∈ (1...𝐽) ∧ 0 ≤ ((𝐹‘𝐶)‘𝑘)) ∧ ∀𝑗 ∈ {𝑖 ∈ (1...𝐽) ∣ 0 ≤ ((𝐹‘𝐶)‘𝑖)}𝑗 ≤ 𝑘)) ∧ (𝑘 + 1) ∈ 𝐶) → (𝑘 + 1) ≤ 𝑘)
186	18, 185	mtand 827	. . . . . . . . 9 ⊢ ((𝜑 ∧ ((𝑘 ∈ (1...𝐽) ∧ 0 ≤ ((𝐹‘𝐶)‘𝑘)) ∧ ∀𝑗 ∈ {𝑖 ∈ (1...𝐽) ∣ 0 ≤ ((𝐹‘𝐶)‘𝑖)}𝑗 ≤ 𝑘)) → ¬ (𝑘 + 1) ∈ 𝐶)
187	161	simpld 499	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑘 + 1) ∈ (1...𝐽)) → (¬ (𝑘 + 1) ∈ 𝐶 → ((𝐹‘𝐶)‘(𝑘 + 1)) = (((𝐹‘𝐶)‘((𝑘 + 1) − 1)) − 1)))
188	187	imp 411	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝑘 + 1) ∈ (1...𝐽)) ∧ ¬ (𝑘 + 1) ∈ 𝐶) → ((𝐹‘𝐶)‘(𝑘 + 1)) = (((𝐹‘𝐶)‘((𝑘 + 1) − 1)) − 1))
189	157, 188	sylan 591	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝑘 ∈ (1...𝐽) ∧ 0 ≤ ((𝐹‘𝐶)‘𝑘))) ∧ ¬ (𝑘 + 1) ∈ 𝐶) → ((𝐹‘𝐶)‘(𝑘 + 1)) = (((𝐹‘𝐶)‘((𝑘 + 1) − 1)) − 1))
190	5	adantr 485	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝑘 ∈ (1...𝐽) ∧ 0 ≤ ((𝐹‘𝐶)‘𝑘))) ∧ ¬ (𝑘 + 1) ∈ 𝐶) → 𝑘 ∈ (1...𝐽))
191	169	oveq1d 7426	. . . . . . . . . . . . 13 ⊢ (𝑘 ∈ (1...𝐽) → (((𝐹‘𝐶)‘((𝑘 + 1) − 1)) − 1) = (((𝐹‘𝐶)‘𝑘) − 1))
192	191	eqeq2d 2780	. . . . . . . . . . . 12 ⊢ (𝑘 ∈ (1...𝐽) → (((𝐹‘𝐶)‘(𝑘 + 1)) = (((𝐹‘𝐶)‘((𝑘 + 1) − 1)) − 1) ↔ ((𝐹‘𝐶)‘(𝑘 + 1)) = (((𝐹‘𝐶)‘𝑘) − 1)))
193	190, 192	syl 18	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝑘 ∈ (1...𝐽) ∧ 0 ≤ ((𝐹‘𝐶)‘𝑘))) ∧ ¬ (𝑘 + 1) ∈ 𝐶) → (((𝐹‘𝐶)‘(𝑘 + 1)) = (((𝐹‘𝐶)‘((𝑘 + 1) − 1)) − 1) ↔ ((𝐹‘𝐶)‘(𝑘 + 1)) = (((𝐹‘𝐶)‘𝑘) − 1)))
194	189, 193	mpbid 235	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝑘 ∈ (1...𝐽) ∧ 0 ≤ ((𝐹‘𝐶)‘𝑘))) ∧ ¬ (𝑘 + 1) ∈ 𝐶) → ((𝐹‘𝐶)‘(𝑘 + 1)) = (((𝐹‘𝐶)‘𝑘) − 1))
195	194	adantlrr 733	. . . . . . . . 9 ⊢ (((𝜑 ∧ ((𝑘 ∈ (1...𝐽) ∧ 0 ≤ ((𝐹‘𝐶)‘𝑘)) ∧ ∀𝑗 ∈ {𝑖 ∈ (1...𝐽) ∣ 0 ≤ ((𝐹‘𝐶)‘𝑖)}𝑗 ≤ 𝑘)) ∧ ¬ (𝑘 + 1) ∈ 𝐶) → ((𝐹‘𝐶)‘(𝑘 + 1)) = (((𝐹‘𝐶)‘𝑘) − 1))
196	186, 195	mpdan 699	. . . . . . . 8 ⊢ ((𝜑 ∧ ((𝑘 ∈ (1...𝐽) ∧ 0 ≤ ((𝐹‘𝐶)‘𝑘)) ∧ ∀𝑗 ∈ {𝑖 ∈ (1...𝐽) ∣ 0 ≤ ((𝐹‘𝐶)‘𝑖)}𝑗 ≤ 𝑘)) → ((𝐹‘𝐶)‘(𝑘 + 1)) = (((𝐹‘𝐶)‘𝑘) − 1))
197		breq2 5117	. . . . . . . . 9 ⊢ (((𝐹‘𝐶)‘(𝑘 + 1)) = (((𝐹‘𝐶)‘𝑘) − 1) → (0 ≤ ((𝐹‘𝐶)‘(𝑘 + 1)) ↔ 0 ≤ (((𝐹‘𝐶)‘𝑘) − 1)))
198	197	notbid 321	. . . . . . . 8 ⊢ (((𝐹‘𝐶)‘(𝑘 + 1)) = (((𝐹‘𝐶)‘𝑘) − 1) → (¬ 0 ≤ ((𝐹‘𝐶)‘(𝑘 + 1)) ↔ ¬ 0 ≤ (((𝐹‘𝐶)‘𝑘) − 1)))
199	196, 198	syl 18	. . . . . . 7 ⊢ ((𝜑 ∧ ((𝑘 ∈ (1...𝐽) ∧ 0 ≤ ((𝐹‘𝐶)‘𝑘)) ∧ ∀𝑗 ∈ {𝑖 ∈ (1...𝐽) ∣ 0 ≤ ((𝐹‘𝐶)‘𝑖)}𝑗 ≤ 𝑘)) → (¬ 0 ≤ ((𝐹‘𝐶)‘(𝑘 + 1)) ↔ ¬ 0 ≤ (((𝐹‘𝐶)‘𝑘) − 1)))
200	140, 199	mpbid 235	. . . . . 6 ⊢ ((𝜑 ∧ ((𝑘 ∈ (1...𝐽) ∧ 0 ≤ ((𝐹‘𝐶)‘𝑘)) ∧ ∀𝑗 ∈ {𝑖 ∈ (1...𝐽) ∣ 0 ≤ ((𝐹‘𝐶)‘𝑖)}𝑗 ≤ 𝑘)) → ¬ 0 ≤ (((𝐹‘𝐶)‘𝑘) − 1))
201	5, 36	syl 18	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑘 ∈ (1...𝐽) ∧ 0 ≤ ((𝐹‘𝐶)‘𝑘))) → 𝑘 ∈ (0...𝐽))
202	201, 46	syldan 602	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑘 ∈ (1...𝐽) ∧ 0 ≤ ((𝐹‘𝐶)‘𝑘))) → ((𝐹‘𝐶)‘𝑘) ∈ ℤ)
203	202	adantrr 729	. . . . . . 7 ⊢ ((𝜑 ∧ ((𝑘 ∈ (1...𝐽) ∧ 0 ≤ ((𝐹‘𝐶)‘𝑘)) ∧ ∀𝑗 ∈ {𝑖 ∈ (1...𝐽) ∣ 0 ≤ ((𝐹‘𝐶)‘𝑖)}𝑗 ≤ 𝑘)) → ((𝐹‘𝐶)‘𝑘) ∈ ℤ)
204		zlem1lt 12645	. . . . . . . . 9 ⊢ ((((𝐹‘𝐶)‘𝑘) ∈ ℤ ∧ 0 ∈ ℤ) → (((𝐹‘𝐶)‘𝑘) ≤ 0 ↔ (((𝐹‘𝐶)‘𝑘) − 1) < 0))
205	174, 204	mpan2 703	. . . . . . . 8 ⊢ (((𝐹‘𝐶)‘𝑘) ∈ ℤ → (((𝐹‘𝐶)‘𝑘) ≤ 0 ↔ (((𝐹‘𝐶)‘𝑘) − 1) < 0))
206		zre 12594	. . . . . . . . . 10 ⊢ (((𝐹‘𝐶)‘𝑘) ∈ ℤ → ((𝐹‘𝐶)‘𝑘) ∈ ℝ)
207		1red 11208	. . . . . . . . . 10 ⊢ (((𝐹‘𝐶)‘𝑘) ∈ ℤ → 1 ∈ ℝ)
208	206, 207	resubcld 11641	. . . . . . . . 9 ⊢ (((𝐹‘𝐶)‘𝑘) ∈ ℤ → (((𝐹‘𝐶)‘𝑘) − 1) ∈ ℝ)
209		0red 11210	. . . . . . . . 9 ⊢ (((𝐹‘𝐶)‘𝑘) ∈ ℤ → 0 ∈ ℝ)
210	208, 209	ltnled 11356	. . . . . . . 8 ⊢ (((𝐹‘𝐶)‘𝑘) ∈ ℤ → ((((𝐹‘𝐶)‘𝑘) − 1) < 0 ↔ ¬ 0 ≤ (((𝐹‘𝐶)‘𝑘) − 1)))
211	205, 210	bitrd 282	. . . . . . 7 ⊢ (((𝐹‘𝐶)‘𝑘) ∈ ℤ → (((𝐹‘𝐶)‘𝑘) ≤ 0 ↔ ¬ 0 ≤ (((𝐹‘𝐶)‘𝑘) − 1)))
212	203, 211	syl 18	. . . . . 6 ⊢ ((𝜑 ∧ ((𝑘 ∈ (1...𝐽) ∧ 0 ≤ ((𝐹‘𝐶)‘𝑘)) ∧ ∀𝑗 ∈ {𝑖 ∈ (1...𝐽) ∣ 0 ≤ ((𝐹‘𝐶)‘𝑖)}𝑗 ≤ 𝑘)) → (((𝐹‘𝐶)‘𝑘) ≤ 0 ↔ ¬ 0 ≤ (((𝐹‘𝐶)‘𝑘) − 1)))
213	200, 212	mpbird 260	. . . . 5 ⊢ ((𝜑 ∧ ((𝑘 ∈ (1...𝐽) ∧ 0 ≤ ((𝐹‘𝐶)‘𝑘)) ∧ ∀𝑗 ∈ {𝑖 ∈ (1...𝐽) ∣ 0 ≤ ((𝐹‘𝐶)‘𝑖)}𝑗 ≤ 𝑘)) → ((𝐹‘𝐶)‘𝑘) ≤ 0)
214		simprlr 791	. . . . 5 ⊢ ((𝜑 ∧ ((𝑘 ∈ (1...𝐽) ∧ 0 ≤ ((𝐹‘𝐶)‘𝑘)) ∧ ∀𝑗 ∈ {𝑖 ∈ (1...𝐽) ∣ 0 ≤ ((𝐹‘𝐶)‘𝑖)}𝑗 ≤ 𝑘)) → 0 ≤ ((𝐹‘𝐶)‘𝑘))
215	203	zred 12699	. . . . . 6 ⊢ ((𝜑 ∧ ((𝑘 ∈ (1...𝐽) ∧ 0 ≤ ((𝐹‘𝐶)‘𝑘)) ∧ ∀𝑗 ∈ {𝑖 ∈ (1...𝐽) ∣ 0 ≤ ((𝐹‘𝐶)‘𝑖)}𝑗 ≤ 𝑘)) → ((𝐹‘𝐶)‘𝑘) ∈ ℝ)
216		0red 11210	. . . . . 6 ⊢ ((𝜑 ∧ ((𝑘 ∈ (1...𝐽) ∧ 0 ≤ ((𝐹‘𝐶)‘𝑘)) ∧ ∀𝑗 ∈ {𝑖 ∈ (1...𝐽) ∣ 0 ≤ ((𝐹‘𝐶)‘𝑖)}𝑗 ≤ 𝑘)) → 0 ∈ ℝ)
217	215, 216	letri3d 11351	. . . . 5 ⊢ ((𝜑 ∧ ((𝑘 ∈ (1...𝐽) ∧ 0 ≤ ((𝐹‘𝐶)‘𝑘)) ∧ ∀𝑗 ∈ {𝑖 ∈ (1...𝐽) ∣ 0 ≤ ((𝐹‘𝐶)‘𝑖)}𝑗 ≤ 𝑘)) → (((𝐹‘𝐶)‘𝑘) = 0 ↔ (((𝐹‘𝐶)‘𝑘) ≤ 0 ∧ 0 ≤ ((𝐹‘𝐶)‘𝑘))))
218	213, 214, 217	mpbir2and 725	. . . 4 ⊢ ((𝜑 ∧ ((𝑘 ∈ (1...𝐽) ∧ 0 ≤ ((𝐹‘𝐶)‘𝑘)) ∧ ∀𝑗 ∈ {𝑖 ∈ (1...𝐽) ∣ 0 ≤ ((𝐹‘𝐶)‘𝑖)}𝑗 ≤ 𝑘)) → ((𝐹‘𝐶)‘𝑘) = 0)
219	4, 218	sylan2b 605	. . 3 ⊢ ((𝜑 ∧ (𝑘 ∈ {𝑖 ∈ (1...𝐽) ∣ 0 ≤ ((𝐹‘𝐶)‘𝑖)} ∧ ∀𝑗 ∈ {𝑖 ∈ (1...𝐽) ∣ 0 ≤ ((𝐹‘𝐶)‘𝑖)}𝑗 ≤ 𝑘)) → ((𝐹‘𝐶)‘𝑘) = 0)
220		ssrab2 4042	. . . . . 6 ⊢ {𝑖 ∈ (1...𝐽) ∣ 0 ≤ ((𝐹‘𝐶)‘𝑖)} ⊆ (1...𝐽)
221	220, 11	sstri 3954	. . . . 5 ⊢ {𝑖 ∈ (1...𝐽) ∣ 0 ≤ ((𝐹‘𝐶)‘𝑖)} ⊆ ℝ
222	221	a1i 11	. . . 4 ⊢ (𝜑 → {𝑖 ∈ (1...𝐽) ∣ 0 ≤ ((𝐹‘𝐶)‘𝑖)} ⊆ ℝ)
223		fzfi 14007	. . . . . 6 ⊢ (1...𝐽) ∈ Fin
224		ssfi 9156	. . . . . 6 ⊢ (((1...𝐽) ∈ Fin ∧ {𝑖 ∈ (1...𝐽) ∣ 0 ≤ ((𝐹‘𝐶)‘𝑖)} ⊆ (1...𝐽)) → {𝑖 ∈ (1...𝐽) ∣ 0 ≤ ((𝐹‘𝐶)‘𝑖)} ∈ Fin)
225	223, 220, 224	mp2an 704	. . . . 5 ⊢ {𝑖 ∈ (1...𝐽) ∣ 0 ≤ ((𝐹‘𝐶)‘𝑖)} ∈ Fin
226	225	a1i 11	. . . 4 ⊢ (𝜑 → {𝑖 ∈ (1...𝐽) ∣ 0 ≤ ((𝐹‘𝐶)‘𝑖)} ∈ Fin)
227		rabn0 4353	. . . . 5 ⊢ ({𝑖 ∈ (1...𝐽) ∣ 0 ≤ ((𝐹‘𝐶)‘𝑖)} ≠ ∅ ↔ ∃𝑖 ∈ (1...𝐽)0 ≤ ((𝐹‘𝐶)‘𝑖))
228	59, 227	sylibr 237	. . . 4 ⊢ (𝜑 → {𝑖 ∈ (1...𝐽) ∣ 0 ≤ ((𝐹‘𝐶)‘𝑖)} ≠ ∅)
229		fimaxre 12158	. . . 4 ⊢ (({𝑖 ∈ (1...𝐽) ∣ 0 ≤ ((𝐹‘𝐶)‘𝑖)} ⊆ ℝ ∧ {𝑖 ∈ (1...𝐽) ∣ 0 ≤ ((𝐹‘𝐶)‘𝑖)} ∈ Fin ∧ {𝑖 ∈ (1...𝐽) ∣ 0 ≤ ((𝐹‘𝐶)‘𝑖)} ≠ ∅) → ∃𝑘 ∈ {𝑖 ∈ (1...𝐽) ∣ 0 ≤ ((𝐹‘𝐶)‘𝑖)}∀𝑗 ∈ {𝑖 ∈ (1...𝐽) ∣ 0 ≤ ((𝐹‘𝐶)‘𝑖)}𝑗 ≤ 𝑘)
230	222, 226, 228, 229	syl3anc 1396	. . 3 ⊢ (𝜑 → ∃𝑘 ∈ {𝑖 ∈ (1...𝐽) ∣ 0 ≤ ((𝐹‘𝐶)‘𝑖)}∀𝑗 ∈ {𝑖 ∈ (1...𝐽) ∣ 0 ≤ ((𝐹‘𝐶)‘𝑖)}𝑗 ≤ 𝑘)
231	219, 230	reximddv 3187	. 2 ⊢ (𝜑 → ∃𝑘 ∈ {𝑖 ∈ (1...𝐽) ∣ 0 ≤ ((𝐹‘𝐶)‘𝑖)} ((𝐹‘𝐶)‘𝑘) = 0)
232		elrabi 3655	. . . 4 ⊢ (𝑘 ∈ {𝑖 ∈ (1...𝐽) ∣ 0 ≤ ((𝐹‘𝐶)‘𝑖)} → 𝑘 ∈ (1...𝐽))
233	232	anim1i 626	. . 3 ⊢ ((𝑘 ∈ {𝑖 ∈ (1...𝐽) ∣ 0 ≤ ((𝐹‘𝐶)‘𝑖)} ∧ ((𝐹‘𝐶)‘𝑘) = 0) → (𝑘 ∈ (1...𝐽) ∧ ((𝐹‘𝐶)‘𝑘) = 0))
234	233	reximi2 3104	. 2 ⊢ (∃𝑘 ∈ {𝑖 ∈ (1...𝐽) ∣ 0 ≤ ((𝐹‘𝐶)‘𝑖)} ((𝐹‘𝐶)‘𝑘) = 0 → ∃𝑘 ∈ (1...𝐽)((𝐹‘𝐶)‘𝑘) = 0)
235	231, 234	syl 18	1 ⊢ (𝜑 → ∃𝑘 ∈ (1...𝐽)((𝐹‘𝐶)‘𝑘) = 0)

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ↔ wb 209 ∧ wa 400 ∨ wo 860 = wceq 1567 ∈ wcel 2149 ≠ wne 2964 ∀wral 3085 ∃wrex 3095 {crab 3423 ∖ cdif 3910 ∩ cin 3912 ⊆ wss 3913 ∅c0 4294 𝒫 cpw 4567 {csn 4594 class class class wbr 5113 ↦ cmpt 5196 ‘cfv 6537 (class class class)co 7411 Fincfn 8942 ℝcr 11098 0cc0 11099 1c1 11100 + caddc 11102 < clt 11242 ≤ cle 11243 − cmin 11440 / cdiv 11870 ℕcn 12232 2c2 12294 ℤcz 12590 ℤ_≥cuz 12861 ...cfz 13534 ♯chash 14365

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1822 ax-4 1836 ax-5 1937 ax-6 1994 ax-7 2035 ax-8 2151 ax-9 2159 ax-10 2182 ax-11 2198 ax-12 2219 ax-ext 2741 ax-rep 5242 ax-sep 5261 ax-nul 5271 ax-pow 5337 ax-pr 5405 ax-un 7733 ax-cnex 11155 ax-resscn 11156 ax-1cn 11157 ax-icn 11158 ax-addcl 11159 ax-addrcl 11160 ax-mulcl 11161 ax-mulrcl 11162 ax-mulcom 11163 ax-addass 11164 ax-mulass 11165 ax-distr 11166 ax-i2m1 11167 ax-1ne0 11168 ax-1rid 11169 ax-rnegex 11170 ax-rrecex 11171 ax-cnre 11172 ax-pre-lttri 11173 ax-pre-lttrn 11174 ax-pre-ltadd 11175 ax-pre-mulgt0 11176

This theorem depends on definitions: df-bi 210 df-an 401 df-or 861 df-3or 1102 df-3an 1103 df-tru 1570 df-fal 1580 df-ex 1807 df-nf 1811 df-sb 2098 df-mo 2573 df-eu 2603 df-clab 2748 df-cleq 2761 df-clel 2844 df-nfc 2918 df-ne 2965 df-nel 3071 df-ral 3086 df-rex 3096 df-reu 3377 df-rab 3424 df-v 3465 df-sbc 3754 df-csb 3862 df-dif 3916 df-un 3918 df-in 3920 df-ss 3930 df-pss 3933 df-nul 4295 df-if 4493 df-pw 4569 df-sn 4595 df-pr 4597 df-op 4601 df-uni 4877 df-int 4917 df-iun 4962 df-br 5114 df-opab 5178 df-mpt 5197 df-tr 5223 df-id 5557 df-eprel 5562 df-po 5570 df-so 5571 df-fr 5615 df-we 5617 df-xp 5668 df-rel 5669 df-cnv 5670 df-co 5671 df-dm 5672 df-rn 5673 df-res 5674 df-ima 5675 df-pred 6303 df-ord 6364 df-on 6365 df-lim 6366 df-suc 6367 df-iota 6493 df-fun 6539 df-fn 6540 df-f 6541 df-f1 6542 df-fo 6543 df-f1o 6544 df-fv 6545 df-riota 7368 df-ov 7414 df-oprab 7415 df-mpo 7416 df-om 7862 df-1st 7985 df-2nd 7986 df-frecs 8277 df-wrecs 8308 df-recs 8357 df-rdg 8396 df-1o 8452 df-oadd 8456 df-er 8693 df-en 8943 df-dom 8944 df-sdom 8945 df-fin 8946 df-dju 9886 df-card 9924 df-pnf 11244 df-mnf 11245 df-xr 11246 df-ltxr 11247 df-le 11248 df-sub 11442 df-neg 11443 df-nn 12233 df-2 12302 df-n0 12504 df-z 12591 df-uz 12862 df-fz 13535 df-hash 14366

This theorem is referenced by: ballotlem1c 34842

W3C validator