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 33093

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 6842	. . . . . . 7 ⊢ (𝑖 = 𝑘 → ((𝐹‘𝐶)‘𝑖) = ((𝐹‘𝐶)‘𝑘))
2	1	breq2d 5117	. . . . . 6 ⊢ (𝑖 = 𝑘 → (0 ≤ ((𝐹‘𝐶)‘𝑖) ↔ 0 ≤ ((𝐹‘𝐶)‘𝑘)))
3	2	elrab 3645	. . . . 5 ⊢ (𝑘 ∈ {𝑖 ∈ (1...𝐽) ∣ 0 ≤ ((𝐹‘𝐶)‘𝑖)} ↔ (𝑘 ∈ (1...𝐽) ∧ 0 ≤ ((𝐹‘𝐶)‘𝑘)))
4	3	anbi1i 624	. . . 4 ⊢ ((𝑘 ∈ {𝑖 ∈ (1...𝐽) ∣ 0 ≤ ((𝐹‘𝐶)‘𝑖)} ∧ ∀𝑗 ∈ {𝑖 ∈ (1...𝐽) ∣ 0 ≤ ((𝐹‘𝐶)‘𝑖)}𝑗 ≤ 𝑘) ↔ ((𝑘 ∈ (1...𝐽) ∧ 0 ≤ ((𝐹‘𝐶)‘𝑘)) ∧ ∀𝑗 ∈ {𝑖 ∈ (1...𝐽) ∣ 0 ≤ ((𝐹‘𝐶)‘𝑖)}𝑗 ≤ 𝑘))
5		simprl 769	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑘 ∈ (1...𝐽) ∧ 0 ≤ ((𝐹‘𝐶)‘𝑘))) → 𝑘 ∈ (1...𝐽))
6	5	adantrr 715	. . . . . . . . 9 ⊢ ((𝜑 ∧ ((𝑘 ∈ (1...𝐽) ∧ 0 ≤ ((𝐹‘𝐶)‘𝑘)) ∧ ∀𝑗 ∈ {𝑖 ∈ (1...𝐽) ∣ 0 ≤ ((𝐹‘𝐶)‘𝑖)}𝑗 ≤ 𝑘)) → 𝑘 ∈ (1...𝐽))
7		fzssuz 13482	. . . . . . . . . . . . . 14 ⊢ (1...𝐽) ⊆ (ℤ_≥‘1)
8		uzssz 12784	. . . . . . . . . . . . . 14 ⊢ (ℤ_≥‘1) ⊆ ℤ
9	7, 8	sstri 3953	. . . . . . . . . . . . 13 ⊢ (1...𝐽) ⊆ ℤ
10		zssre 12506	. . . . . . . . . . . . 13 ⊢ ℤ ⊆ ℝ
11	9, 10	sstri 3953	. . . . . . . . . . . 12 ⊢ (1...𝐽) ⊆ ℝ
12	11	sseli 3940	. . . . . . . . . . 11 ⊢ (𝑘 ∈ (1...𝐽) → 𝑘 ∈ ℝ)
13	12	ltp1d 12085	. . . . . . . . . 10 ⊢ (𝑘 ∈ (1...𝐽) → 𝑘 < (𝑘 + 1))
14		1red 11156	. . . . . . . . . . . 12 ⊢ (𝑘 ∈ (1...𝐽) → 1 ∈ ℝ)
15	12, 14	readdcld 11184	. . . . . . . . . . 11 ⊢ (𝑘 ∈ (1...𝐽) → (𝑘 + 1) ∈ ℝ)
16	12, 15	ltnled 11302	. . . . . . . . . 10 ⊢ (𝑘 ∈ (1...𝐽) → (𝑘 < (𝑘 + 1) ↔ ¬ (𝑘 + 1) ≤ 𝑘))
17	13, 16	mpbid 231	. . . . . . . . 9 ⊢ (𝑘 ∈ (1...𝐽) → ¬ (𝑘 + 1) ≤ 𝑘)
18	6, 17	syl 17	. . . . . . . 8 ⊢ ((𝜑 ∧ ((𝑘 ∈ (1...𝐽) ∧ 0 ≤ ((𝐹‘𝐶)‘𝑘)) ∧ ∀𝑗 ∈ {𝑖 ∈ (1...𝐽) ∣ 0 ≤ ((𝐹‘𝐶)‘𝑖)}𝑗 ≤ 𝑘)) → ¬ (𝑘 + 1) ≤ 𝑘)
19		simprr 771	. . . . . . . . 9 ⊢ ((𝜑 ∧ ((𝑘 ∈ (1...𝐽) ∧ 0 ≤ ((𝐹‘𝐶)‘𝑘)) ∧ ∀𝑗 ∈ {𝑖 ∈ (1...𝐽) ∣ 0 ≤ ((𝐹‘𝐶)‘𝑖)}𝑗 ≤ 𝑘)) → ∀𝑗 ∈ {𝑖 ∈ (1...𝐽) ∣ 0 ≤ ((𝐹‘𝐶)‘𝑖)}𝑗 ≤ 𝑘)
20		ballotlemfcc.4	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ((𝐹‘𝐶)‘𝐽) < 0)
21	20	adantr 481	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑘 = 𝐽) → ((𝐹‘𝐶)‘𝐽) < 0)
22		simpr 485	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑘 = 𝐽) → 𝑘 = 𝐽)
23	22	fveq2d 6846	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑘 = 𝐽) → ((𝐹‘𝐶)‘𝑘) = ((𝐹‘𝐶)‘𝐽))
24	23	breq1d 5115	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑘 = 𝐽) → (((𝐹‘𝐶)‘𝑘) < 0 ↔ ((𝐹‘𝐶)‘𝐽) < 0))
25		ballotlemfcc.j	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜑 → 𝐽 ∈ ℕ)
26		elnnuz 12807	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝐽 ∈ ℕ ↔ 𝐽 ∈ (ℤ_≥‘1))
27	25, 26	sylib 217	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → 𝐽 ∈ (ℤ_≥‘1))
28		eluzfz2 13449	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝐽 ∈ (ℤ_≥‘1) → 𝐽 ∈ (1...𝐽))
29	27, 28	syl 17	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → 𝐽 ∈ (1...𝐽))
30		eleq1 2825	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑘 = 𝐽 → (𝑘 ∈ (1...𝐽) ↔ 𝐽 ∈ (1...𝐽)))
31	29, 30	syl5ibrcom 246	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → (𝑘 = 𝐽 → 𝑘 ∈ (1...𝐽)))
32	31	anc2li 556	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (𝑘 = 𝐽 → (𝜑 ∧ 𝑘 ∈ (1...𝐽))))
33		1eluzge0 12817	. . . . . . . . . . . . . . . . . . . 20 ⊢ 1 ∈ (ℤ_≥‘0)
34		fzss1 13480	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (1 ∈ (ℤ_≥‘0) → (1...𝐽) ⊆ (0...𝐽))
35	34	sseld 3943	. . . . . . . . . . . . . . . . . . . 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 481	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝐽)) → 𝐶 ∈ 𝑂)
44		elfzelz 13441	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑘 ∈ (0...𝐽) → 𝑘 ∈ ℤ)
45	44	adantl 482	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝐽)) → 𝑘 ∈ ℤ)
46	37, 38, 39, 40, 41, 43, 45	ballotlemfelz 33090	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝐽)) → ((𝐹‘𝐶)‘𝑘) ∈ ℤ)
47	46	zred 12607	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝐽)) → ((𝐹‘𝐶)‘𝑘) ∈ ℝ)
48		0red 11158	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝐽)) → 0 ∈ ℝ)
49	47, 48	ltnled 11302	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝐽)) → (((𝐹‘𝐶)‘𝑘) < 0 ↔ ¬ 0 ≤ ((𝐹‘𝐶)‘𝑘)))
50	36, 49	sylan2 593	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑘 ∈ (1...𝐽)) → (((𝐹‘𝐶)‘𝑘) < 0 ↔ ¬ 0 ≤ ((𝐹‘𝐶)‘𝑘)))
51	32, 50	syl6 35	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (𝑘 = 𝐽 → (((𝐹‘𝐶)‘𝑘) < 0 ↔ ¬ 0 ≤ ((𝐹‘𝐶)‘𝑘))))
52	51	imp 407	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑘 = 𝐽) → (((𝐹‘𝐶)‘𝑘) < 0 ↔ ¬ 0 ≤ ((𝐹‘𝐶)‘𝑘)))
53	24, 52	bitr3d 280	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑘 = 𝐽) → (((𝐹‘𝐶)‘𝐽) < 0 ↔ ¬ 0 ≤ ((𝐹‘𝐶)‘𝑘)))
54	21, 53	mpbid 231	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑘 = 𝐽) → ¬ 0 ≤ ((𝐹‘𝐶)‘𝑘))
55	54	ex 413	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝑘 = 𝐽 → ¬ 0 ≤ ((𝐹‘𝐶)‘𝑘)))
56	55	con2d 134	. . . . . . . . . . . 12 ⊢ (𝜑 → (0 ≤ ((𝐹‘𝐶)‘𝑘) → ¬ 𝑘 = 𝐽))
57		nn1m1nn 12174	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝐽 ∈ ℕ → (𝐽 = 1 ∨ (𝐽 − 1) ∈ ℕ))
58	25, 57	syl 17	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → (𝐽 = 1 ∨ (𝐽 − 1) ∈ ℕ))
59		ballotlemfcc.3	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝜑 → ∃𝑖 ∈ (1...𝐽)0 ≤ ((𝐹‘𝐶)‘𝑖))
60	59	adantr 481	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝜑 ∧ 𝐽 = 1) → ∃𝑖 ∈ (1...𝐽)0 ≤ ((𝐹‘𝐶)‘𝑖))
61		oveq1 7364	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝐽 = 1 → (𝐽...𝐽) = (1...𝐽))
62	61	adantl 482	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝜑 ∧ 𝐽 = 1) → (𝐽...𝐽) = (1...𝐽))
63	25	nnzd 12526	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝜑 → 𝐽 ∈ ℤ)
64		fzsn 13483	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝐽 ∈ ℤ → (𝐽...𝐽) = {𝐽})
65	63, 64	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝜑 → (𝐽...𝐽) = {𝐽})
66	65	adantr 481	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝜑 ∧ 𝐽 = 1) → (𝐽...𝐽) = {𝐽})
67	62, 66	eqtr3d 2778	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝜑 ∧ 𝐽 = 1) → (1...𝐽) = {𝐽})
68	67	rexeqdv 3314	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝜑 ∧ 𝐽 = 1) → (∃𝑖 ∈ (1...𝐽)0 ≤ ((𝐹‘𝐶)‘𝑖) ↔ ∃𝑖 ∈ {𝐽}0 ≤ ((𝐹‘𝐶)‘𝑖)))
69	60, 68	mpbid 231	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝜑 ∧ 𝐽 = 1) → ∃𝑖 ∈ {𝐽}0 ≤ ((𝐹‘𝐶)‘𝑖))
70		fveq2 6842	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝑖 = 𝐽 → ((𝐹‘𝐶)‘𝑖) = ((𝐹‘𝐶)‘𝐽))
71	70	breq2d 5117	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑖 = 𝐽 → (0 ≤ ((𝐹‘𝐶)‘𝑖) ↔ 0 ≤ ((𝐹‘𝐶)‘𝐽)))
72	71	rexsng 4635	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝐽 ∈ ℕ → (∃𝑖 ∈ {𝐽}0 ≤ ((𝐹‘𝐶)‘𝑖) ↔ 0 ≤ ((𝐹‘𝐶)‘𝐽)))
73	25, 72	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝜑 → (∃𝑖 ∈ {𝐽}0 ≤ ((𝐹‘𝐶)‘𝑖) ↔ 0 ≤ ((𝐹‘𝐶)‘𝐽)))
74	73	adantr 481	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝜑 ∧ 𝐽 = 1) → (∃𝑖 ∈ {𝐽}0 ≤ ((𝐹‘𝐶)‘𝑖) ↔ 0 ≤ ((𝐹‘𝐶)‘𝐽)))
75	69, 74	mpbid 231	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ 𝐽 = 1) → 0 ≤ ((𝐹‘𝐶)‘𝐽))
76	20	adantr 481	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝜑 ∧ 𝐽 = 1) → ((𝐹‘𝐶)‘𝐽) < 0)
77	37, 38, 39, 40, 41, 42, 63	ballotlemfelz 33090	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝜑 → ((𝐹‘𝐶)‘𝐽) ∈ ℤ)
78	77	zred 12607	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝜑 → ((𝐹‘𝐶)‘𝐽) ∈ ℝ)
79		0red 11158	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝜑 → 0 ∈ ℝ)
80	78, 79	ltnled 11302	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝜑 → (((𝐹‘𝐶)‘𝐽) < 0 ↔ ¬ 0 ≤ ((𝐹‘𝐶)‘𝐽)))
81	80	adantr 481	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝜑 ∧ 𝐽 = 1) → (((𝐹‘𝐶)‘𝐽) < 0 ↔ ¬ 0 ≤ ((𝐹‘𝐶)‘𝐽)))
82	76, 81	mpbid 231	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ 𝐽 = 1) → ¬ 0 ≤ ((𝐹‘𝐶)‘𝐽))
83	75, 82	pm2.65da 815	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜑 → ¬ 𝐽 = 1)
84		biortn 936	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (¬ 𝐽 = 1 → ((𝐽 − 1) ∈ ℕ ↔ (¬ ¬ 𝐽 = 1 ∨ (𝐽 − 1) ∈ ℕ)))
85	83, 84	syl 17	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → ((𝐽 − 1) ∈ ℕ ↔ (¬ ¬ 𝐽 = 1 ∨ (𝐽 − 1) ∈ ℕ)))
86		notnotb 314	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝐽 = 1 ↔ ¬ ¬ 𝐽 = 1)
87	86	orbi1i 912	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝐽 = 1 ∨ (𝐽 − 1) ∈ ℕ) ↔ (¬ ¬ 𝐽 = 1 ∨ (𝐽 − 1) ∈ ℕ))
88	85, 87	bitr4di 288	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → ((𝐽 − 1) ∈ ℕ ↔ (𝐽 = 1 ∨ (𝐽 − 1) ∈ ℕ)))
89	58, 88	mpbird 256	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → (𝐽 − 1) ∈ ℕ)
90		elnnuz 12807	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝐽 − 1) ∈ ℕ ↔ (𝐽 − 1) ∈ (ℤ_≥‘1))
91	89, 90	sylib 217	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (𝐽 − 1) ∈ (ℤ_≥‘1))
92		elfzp1 13491	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝐽 − 1) ∈ (ℤ_≥‘1) → (𝑘 ∈ (1...((𝐽 − 1) + 1)) ↔ (𝑘 ∈ (1...(𝐽 − 1)) ∨ 𝑘 = ((𝐽 − 1) + 1))))
93	91, 92	syl 17	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (𝑘 ∈ (1...((𝐽 − 1) + 1)) ↔ (𝑘 ∈ (1...(𝐽 − 1)) ∨ 𝑘 = ((𝐽 − 1) + 1))))
94	25	nncnd 12169	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → 𝐽 ∈ ℂ)
95		1cnd 11150	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → 1 ∈ ℂ)
96	94, 95	npcand 11516	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → ((𝐽 − 1) + 1) = 𝐽)
97	96	oveq2d 7373	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (1...((𝐽 − 1) + 1)) = (1...𝐽))
98	97	eleq2d 2823	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (𝑘 ∈ (1...((𝐽 − 1) + 1)) ↔ 𝑘 ∈ (1...𝐽)))
99	96	eqeq2d 2747	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (𝑘 = ((𝐽 − 1) + 1) ↔ 𝑘 = 𝐽))
100	99	orbi2d 914	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → ((𝑘 ∈ (1...(𝐽 − 1)) ∨ 𝑘 = ((𝐽 − 1) + 1)) ↔ (𝑘 ∈ (1...(𝐽 − 1)) ∨ 𝑘 = 𝐽)))
101	93, 98, 100	3bitr3d 308	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (𝑘 ∈ (1...𝐽) ↔ (𝑘 ∈ (1...(𝐽 − 1)) ∨ 𝑘 = 𝐽)))
102		orcom 868	. . . . . . . . . . . . . . . 16 ⊢ ((𝑘 ∈ (1...(𝐽 − 1)) ∨ 𝑘 = 𝐽) ↔ (𝑘 = 𝐽 ∨ 𝑘 ∈ (1...(𝐽 − 1))))
103	101, 102	bitrdi 286	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝑘 ∈ (1...𝐽) ↔ (𝑘 = 𝐽 ∨ 𝑘 ∈ (1...(𝐽 − 1)))))
104	103	biimpd 228	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝑘 ∈ (1...𝐽) → (𝑘 = 𝐽 ∨ 𝑘 ∈ (1...(𝐽 − 1)))))
105		pm5.6 1000	. . . . . . . . . . . . . 14 ⊢ (((𝑘 ∈ (1...𝐽) ∧ ¬ 𝑘 = 𝐽) → 𝑘 ∈ (1...(𝐽 − 1))) ↔ (𝑘 ∈ (1...𝐽) → (𝑘 = 𝐽 ∨ 𝑘 ∈ (1...(𝐽 − 1)))))
106	104, 105	sylibr 233	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((𝑘 ∈ (1...𝐽) ∧ ¬ 𝑘 = 𝐽) → 𝑘 ∈ (1...(𝐽 − 1))))
107	89	nnzd 12526	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → (𝐽 − 1) ∈ ℤ)
108		1z 12533	. . . . . . . . . . . . . . . . . . 19 ⊢ 1 ∈ ℤ
109	107, 108	jctil 520	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (1 ∈ ℤ ∧ (𝐽 − 1) ∈ ℤ))
110		elfzelz 13441	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑘 ∈ (1...(𝐽 − 1)) → 𝑘 ∈ ℤ)
111	110, 108	jctir 521	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑘 ∈ (1...(𝐽 − 1)) → (𝑘 ∈ ℤ ∧ 1 ∈ ℤ))
112		fzaddel 13475	. . . . . . . . . . . . . . . . . 18 ⊢ (((1 ∈ ℤ ∧ (𝐽 − 1) ∈ ℤ) ∧ (𝑘 ∈ ℤ ∧ 1 ∈ ℤ)) → (𝑘 ∈ (1...(𝐽 − 1)) ↔ (𝑘 + 1) ∈ ((1 + 1)...((𝐽 − 1) + 1))))
113	109, 111, 112	syl2an 596	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑘 ∈ (1...(𝐽 − 1))) → (𝑘 ∈ (1...(𝐽 − 1)) ↔ (𝑘 + 1) ∈ ((1 + 1)...((𝐽 − 1) + 1))))
114	113	biimp3a 1469	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑘 ∈ (1...(𝐽 − 1)) ∧ 𝑘 ∈ (1...(𝐽 − 1))) → (𝑘 + 1) ∈ ((1 + 1)...((𝐽 − 1) + 1)))
115	114	3anidm23 1421	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑘 ∈ (1...(𝐽 − 1))) → (𝑘 + 1) ∈ ((1 + 1)...((𝐽 − 1) + 1)))
116		1p1e2 12278	. . . . . . . . . . . . . . . . . . . 20 ⊢ (1 + 1) = 2
117	116	a1i 11	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → (1 + 1) = 2)
118	117, 96	oveq12d 7375	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → ((1 + 1)...((𝐽 − 1) + 1)) = (2...𝐽))
119	118	eleq2d 2823	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → ((𝑘 + 1) ∈ ((1 + 1)...((𝐽 − 1) + 1)) ↔ (𝑘 + 1) ∈ (2...𝐽)))
120		2eluzge1 12819	. . . . . . . . . . . . . . . . . . 19 ⊢ 2 ∈ (ℤ_≥‘1)
121		fzss1 13480	. . . . . . . . . . . . . . . . . . 19 ⊢ (2 ∈ (ℤ_≥‘1) → (2...𝐽) ⊆ (1...𝐽))
122	120, 121	ax-mp 5	. . . . . . . . . . . . . . . . . 18 ⊢ (2...𝐽) ⊆ (1...𝐽)
123	122	sseli 3940	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑘 + 1) ∈ (2...𝐽) → (𝑘 + 1) ∈ (1...𝐽))
124	119, 123	syl6bi 252	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ((𝑘 + 1) ∈ ((1 + 1)...((𝐽 − 1) + 1)) → (𝑘 + 1) ∈ (1...𝐽)))
125	124	adantr 481	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑘 ∈ (1...(𝐽 − 1))) → ((𝑘 + 1) ∈ ((1 + 1)...((𝐽 − 1) + 1)) → (𝑘 + 1) ∈ (1...𝐽)))
126	115, 125	mpd 15	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑘 ∈ (1...(𝐽 − 1))) → (𝑘 + 1) ∈ (1...𝐽))
127	126	ex 413	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝑘 ∈ (1...(𝐽 − 1)) → (𝑘 + 1) ∈ (1...𝐽)))
128	106, 127	syld 47	. . . . . . . . . . . 12 ⊢ (𝜑 → ((𝑘 ∈ (1...𝐽) ∧ ¬ 𝑘 = 𝐽) → (𝑘 + 1) ∈ (1...𝐽)))
129	56, 128	sylan2d 605	. . . . . . . . . . 11 ⊢ (𝜑 → ((𝑘 ∈ (1...𝐽) ∧ 0 ≤ ((𝐹‘𝐶)‘𝑘)) → (𝑘 + 1) ∈ (1...𝐽)))
130	129	imp 407	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑘 ∈ (1...𝐽) ∧ 0 ≤ ((𝐹‘𝐶)‘𝑘))) → (𝑘 + 1) ∈ (1...𝐽))
131	130	adantrr 715	. . . . . . . . 9 ⊢ ((𝜑 ∧ ((𝑘 ∈ (1...𝐽) ∧ 0 ≤ ((𝐹‘𝐶)‘𝑘)) ∧ ∀𝑗 ∈ {𝑖 ∈ (1...𝐽) ∣ 0 ≤ ((𝐹‘𝐶)‘𝑖)}𝑗 ≤ 𝑘)) → (𝑘 + 1) ∈ (1...𝐽))
132		fveq2 6842	. . . . . . . . . . . . . 14 ⊢ (𝑖 = (𝑘 + 1) → ((𝐹‘𝐶)‘𝑖) = ((𝐹‘𝐶)‘(𝑘 + 1)))
133	132	breq2d 5117	. . . . . . . . . . . . 13 ⊢ (𝑖 = (𝑘 + 1) → (0 ≤ ((𝐹‘𝐶)‘𝑖) ↔ 0 ≤ ((𝐹‘𝐶)‘(𝑘 + 1))))
134	133	elrab 3645	. . . . . . . . . . . 12 ⊢ ((𝑘 + 1) ∈ {𝑖 ∈ (1...𝐽) ∣ 0 ≤ ((𝐹‘𝐶)‘𝑖)} ↔ ((𝑘 + 1) ∈ (1...𝐽) ∧ 0 ≤ ((𝐹‘𝐶)‘(𝑘 + 1))))
135		breq1 5108	. . . . . . . . . . . . 13 ⊢ (𝑗 = (𝑘 + 1) → (𝑗 ≤ 𝑘 ↔ (𝑘 + 1) ≤ 𝑘))
136	135	rspccva 3580	. . . . . . . . . . . 12 ⊢ ((∀𝑗 ∈ {𝑖 ∈ (1...𝐽) ∣ 0 ≤ ((𝐹‘𝐶)‘𝑖)}𝑗 ≤ 𝑘 ∧ (𝑘 + 1) ∈ {𝑖 ∈ (1...𝐽) ∣ 0 ≤ ((𝐹‘𝐶)‘𝑖)}) → (𝑘 + 1) ≤ 𝑘)
137	134, 136	sylan2br 595	. . . . . . . . . . 11 ⊢ ((∀𝑗 ∈ {𝑖 ∈ (1...𝐽) ∣ 0 ≤ ((𝐹‘𝐶)‘𝑖)}𝑗 ≤ 𝑘 ∧ ((𝑘 + 1) ∈ (1...𝐽) ∧ 0 ≤ ((𝐹‘𝐶)‘(𝑘 + 1)))) → (𝑘 + 1) ≤ 𝑘)
138	137	expr 457	. . . . . . . . . 10 ⊢ ((∀𝑗 ∈ {𝑖 ∈ (1...𝐽) ∣ 0 ≤ ((𝐹‘𝐶)‘𝑖)}𝑗 ≤ 𝑘 ∧ (𝑘 + 1) ∈ (1...𝐽)) → (0 ≤ ((𝐹‘𝐶)‘(𝑘 + 1)) → (𝑘 + 1) ≤ 𝑘))
139	138	con3d 152	. . . . . . . . 9 ⊢ ((∀𝑗 ∈ {𝑖 ∈ (1...𝐽) ∣ 0 ≤ ((𝐹‘𝐶)‘𝑖)}𝑗 ≤ 𝑘 ∧ (𝑘 + 1) ∈ (1...𝐽)) → (¬ (𝑘 + 1) ≤ 𝑘 → ¬ 0 ≤ ((𝐹‘𝐶)‘(𝑘 + 1))))
140	19, 131, 139	syl2anc 584	. . . . . . . 8 ⊢ ((𝜑 ∧ ((𝑘 ∈ (1...𝐽) ∧ 0 ≤ ((𝐹‘𝐶)‘𝑘)) ∧ ∀𝑗 ∈ {𝑖 ∈ (1...𝐽) ∣ 0 ≤ ((𝐹‘𝐶)‘𝑖)}𝑗 ≤ 𝑘)) → (¬ (𝑘 + 1) ≤ 𝑘 → ¬ 0 ≤ ((𝐹‘𝐶)‘(𝑘 + 1))))
141	18, 140	mpd 15	. . . . . . 7 ⊢ ((𝜑 ∧ ((𝑘 ∈ (1...𝐽) ∧ 0 ≤ ((𝐹‘𝐶)‘𝑘)) ∧ ∀𝑗 ∈ {𝑖 ∈ (1...𝐽) ∣ 0 ≤ ((𝐹‘𝐶)‘𝑖)}𝑗 ≤ 𝑘)) → ¬ 0 ≤ ((𝐹‘𝐶)‘(𝑘 + 1)))
142		simplrr 776	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ ((𝑘 ∈ (1...𝐽) ∧ 0 ≤ ((𝐹‘𝐶)‘𝑘)) ∧ ∀𝑗 ∈ {𝑖 ∈ (1...𝐽) ∣ 0 ≤ ((𝐹‘𝐶)‘𝑖)}𝑗 ≤ 𝑘)) ∧ (𝑘 + 1) ∈ 𝐶) → ∀𝑗 ∈ {𝑖 ∈ (1...𝐽) ∣ 0 ≤ ((𝐹‘𝐶)‘𝑖)}𝑗 ≤ 𝑘)
143	131	adantr 481	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ ((𝑘 ∈ (1...𝐽) ∧ 0 ≤ ((𝐹‘𝐶)‘𝑘)) ∧ ∀𝑗 ∈ {𝑖 ∈ (1...𝐽) ∣ 0 ≤ ((𝐹‘𝐶)‘𝑖)}𝑗 ≤ 𝑘)) ∧ (𝑘 + 1) ∈ 𝐶) → (𝑘 + 1) ∈ (1...𝐽))
144		0red 11158	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑘 ∈ (1...𝐽) ∧ 0 ≤ ((𝐹‘𝐶)‘𝑘))) ∧ (𝑘 + 1) ∈ 𝐶) → 0 ∈ ℝ)
145		simpll 765	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (𝑘 ∈ (1...𝐽) ∧ 0 ≤ ((𝐹‘𝐶)‘𝑘))) ∧ (𝑘 + 1) ∈ 𝐶) → 𝜑)
146	130	adantr 481	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ (𝑘 ∈ (1...𝐽) ∧ 0 ≤ ((𝐹‘𝐶)‘𝑘))) ∧ (𝑘 + 1) ∈ 𝐶) → (𝑘 + 1) ∈ (1...𝐽))
147	34	sseld 3943	. . . . . . . . . . . . . . 15 ⊢ (1 ∈ (ℤ_≥‘0) → ((𝑘 + 1) ∈ (1...𝐽) → (𝑘 + 1) ∈ (0...𝐽)))
148	33, 146, 147	mpsyl 68	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (𝑘 ∈ (1...𝐽) ∧ 0 ≤ ((𝐹‘𝐶)‘𝑘))) ∧ (𝑘 + 1) ∈ 𝐶) → (𝑘 + 1) ∈ (0...𝐽))
149	42	adantr 481	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ (𝑘 + 1) ∈ (0...𝐽)) → 𝐶 ∈ 𝑂)
150		elfzelz 13441	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑘 + 1) ∈ (0...𝐽) → (𝑘 + 1) ∈ ℤ)
151	150	adantl 482	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ (𝑘 + 1) ∈ (0...𝐽)) → (𝑘 + 1) ∈ ℤ)
152	37, 38, 39, 40, 41, 149, 151	ballotlemfelz 33090	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ (𝑘 + 1) ∈ (0...𝐽)) → ((𝐹‘𝐶)‘(𝑘 + 1)) ∈ ℤ)
153	152	zred 12607	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑘 + 1) ∈ (0...𝐽)) → ((𝐹‘𝐶)‘(𝑘 + 1)) ∈ ℝ)
154	145, 148, 153	syl2anc 584	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑘 ∈ (1...𝐽) ∧ 0 ≤ ((𝐹‘𝐶)‘𝑘))) ∧ (𝑘 + 1) ∈ 𝐶) → ((𝐹‘𝐶)‘(𝑘 + 1)) ∈ ℝ)
155		simplrr 776	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (𝑘 ∈ (1...𝐽) ∧ 0 ≤ ((𝐹‘𝐶)‘𝑘))) ∧ (𝑘 + 1) ∈ 𝐶) → 0 ≤ ((𝐹‘𝐶)‘𝑘))
156	5	adantr 481	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ (𝑘 ∈ (1...𝐽) ∧ 0 ≤ ((𝐹‘𝐶)‘𝑘))) ∧ (𝑘 + 1) ∈ 𝐶) → 𝑘 ∈ (1...𝐽))
157	156, 36	syl 17	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ (𝑘 ∈ (1...𝐽) ∧ 0 ≤ ((𝐹‘𝐶)‘𝑘))) ∧ (𝑘 + 1) ∈ 𝐶) → 𝑘 ∈ (0...𝐽))
158	129	imdistani 569	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ (𝑘 ∈ (1...𝐽) ∧ 0 ≤ ((𝐹‘𝐶)‘𝑘))) → (𝜑 ∧ (𝑘 + 1) ∈ (1...𝐽)))
159	42	adantr 481	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ (𝑘 + 1) ∈ (1...𝐽)) → 𝐶 ∈ 𝑂)
160		elfznn 13470	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑘 + 1) ∈ (1...𝐽) → (𝑘 + 1) ∈ ℕ)
161	160	adantl 482	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ (𝑘 + 1) ∈ (1...𝐽)) → (𝑘 + 1) ∈ ℕ)
162	37, 38, 39, 40, 41, 159, 161	ballotlemfp1 33091	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ (𝑘 + 1) ∈ (1...𝐽)) → ((¬ (𝑘 + 1) ∈ 𝐶 → ((𝐹‘𝐶)‘(𝑘 + 1)) = (((𝐹‘𝐶)‘((𝑘 + 1) − 1)) − 1)) ∧ ((𝑘 + 1) ∈ 𝐶 → ((𝐹‘𝐶)‘(𝑘 + 1)) = (((𝐹‘𝐶)‘((𝑘 + 1) − 1)) + 1))))
163	162	simprd 496	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ (𝑘 + 1) ∈ (1...𝐽)) → ((𝑘 + 1) ∈ 𝐶 → ((𝐹‘𝐶)‘(𝑘 + 1)) = (((𝐹‘𝐶)‘((𝑘 + 1) − 1)) + 1)))
164	163	imp 407	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ (𝑘 + 1) ∈ (1...𝐽)) ∧ (𝑘 + 1) ∈ 𝐶) → ((𝐹‘𝐶)‘(𝑘 + 1)) = (((𝐹‘𝐶)‘((𝑘 + 1) − 1)) + 1))
165	158, 164	sylan 580	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ (𝑘 ∈ (1...𝐽) ∧ 0 ≤ ((𝐹‘𝐶)‘𝑘))) ∧ (𝑘 + 1) ∈ 𝐶) → ((𝐹‘𝐶)‘(𝑘 + 1)) = (((𝐹‘𝐶)‘((𝑘 + 1) − 1)) + 1))
166		elfzelz 13441	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑘 ∈ (1...𝐽) → 𝑘 ∈ ℤ)
167	166	zcnd 12608	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑘 ∈ (1...𝐽) → 𝑘 ∈ ℂ)
168		1cnd 11150	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑘 ∈ (1...𝐽) → 1 ∈ ℂ)
169	167, 168	pncand 11513	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑘 ∈ (1...𝐽) → ((𝑘 + 1) − 1) = 𝑘)
170	169	fveq2d 6846	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑘 ∈ (1...𝐽) → ((𝐹‘𝐶)‘((𝑘 + 1) − 1)) = ((𝐹‘𝐶)‘𝑘))
171	170	oveq1d 7372	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑘 ∈ (1...𝐽) → (((𝐹‘𝐶)‘((𝑘 + 1) − 1)) + 1) = (((𝐹‘𝐶)‘𝑘) + 1))
172	171	eqeq2d 2747	. . . . . . . . . . . . . . . . 17 ⊢ (𝑘 ∈ (1...𝐽) → (((𝐹‘𝐶)‘(𝑘 + 1)) = (((𝐹‘𝐶)‘((𝑘 + 1) − 1)) + 1) ↔ ((𝐹‘𝐶)‘(𝑘 + 1)) = (((𝐹‘𝐶)‘𝑘) + 1)))
173	156, 172	syl 17	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ (𝑘 ∈ (1...𝐽) ∧ 0 ≤ ((𝐹‘𝐶)‘𝑘))) ∧ (𝑘 + 1) ∈ 𝐶) → (((𝐹‘𝐶)‘(𝑘 + 1)) = (((𝐹‘𝐶)‘((𝑘 + 1) − 1)) + 1) ↔ ((𝐹‘𝐶)‘(𝑘 + 1)) = (((𝐹‘𝐶)‘𝑘) + 1)))
174	165, 173	mpbid 231	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ (𝑘 ∈ (1...𝐽) ∧ 0 ≤ ((𝐹‘𝐶)‘𝑘))) ∧ (𝑘 + 1) ∈ 𝐶) → ((𝐹‘𝐶)‘(𝑘 + 1)) = (((𝐹‘𝐶)‘𝑘) + 1))
175		0z 12510	. . . . . . . . . . . . . . . . . 18 ⊢ 0 ∈ ℤ
176		zleltp1 12554	. . . . . . . . . . . . . . . . . 18 ⊢ ((0 ∈ ℤ ∧ ((𝐹‘𝐶)‘𝑘) ∈ ℤ) → (0 ≤ ((𝐹‘𝐶)‘𝑘) ↔ 0 < (((𝐹‘𝐶)‘𝑘) + 1)))
177	175, 46, 176	sylancr 587	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝐽)) → (0 ≤ ((𝐹‘𝐶)‘𝑘) ↔ 0 < (((𝐹‘𝐶)‘𝑘) + 1)))
178	177	adantr 481	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑘 ∈ (0...𝐽)) ∧ ((𝐹‘𝐶)‘(𝑘 + 1)) = (((𝐹‘𝐶)‘𝑘) + 1)) → (0 ≤ ((𝐹‘𝐶)‘𝑘) ↔ 0 < (((𝐹‘𝐶)‘𝑘) + 1)))
179		breq2 5109	. . . . . . . . . . . . . . . . 17 ⊢ (((𝐹‘𝐶)‘(𝑘 + 1)) = (((𝐹‘𝐶)‘𝑘) + 1) → (0 < ((𝐹‘𝐶)‘(𝑘 + 1)) ↔ 0 < (((𝐹‘𝐶)‘𝑘) + 1)))
180	179	adantl 482	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑘 ∈ (0...𝐽)) ∧ ((𝐹‘𝐶)‘(𝑘 + 1)) = (((𝐹‘𝐶)‘𝑘) + 1)) → (0 < ((𝐹‘𝐶)‘(𝑘 + 1)) ↔ 0 < (((𝐹‘𝐶)‘𝑘) + 1)))
181	178, 180	bitr4d 281	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑘 ∈ (0...𝐽)) ∧ ((𝐹‘𝐶)‘(𝑘 + 1)) = (((𝐹‘𝐶)‘𝑘) + 1)) → (0 ≤ ((𝐹‘𝐶)‘𝑘) ↔ 0 < ((𝐹‘𝐶)‘(𝑘 + 1))))
182	145, 157, 174, 181	syl21anc 836	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (𝑘 ∈ (1...𝐽) ∧ 0 ≤ ((𝐹‘𝐶)‘𝑘))) ∧ (𝑘 + 1) ∈ 𝐶) → (0 ≤ ((𝐹‘𝐶)‘𝑘) ↔ 0 < ((𝐹‘𝐶)‘(𝑘 + 1))))
183	155, 182	mpbid 231	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑘 ∈ (1...𝐽) ∧ 0 ≤ ((𝐹‘𝐶)‘𝑘))) ∧ (𝑘 + 1) ∈ 𝐶) → 0 < ((𝐹‘𝐶)‘(𝑘 + 1)))
184	144, 154, 183	ltled 11303	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝑘 ∈ (1...𝐽) ∧ 0 ≤ ((𝐹‘𝐶)‘𝑘))) ∧ (𝑘 + 1) ∈ 𝐶) → 0 ≤ ((𝐹‘𝐶)‘(𝑘 + 1)))
185	184	adantlrr 719	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ ((𝑘 ∈ (1...𝐽) ∧ 0 ≤ ((𝐹‘𝐶)‘𝑘)) ∧ ∀𝑗 ∈ {𝑖 ∈ (1...𝐽) ∣ 0 ≤ ((𝐹‘𝐶)‘𝑖)}𝑗 ≤ 𝑘)) ∧ (𝑘 + 1) ∈ 𝐶) → 0 ≤ ((𝐹‘𝐶)‘(𝑘 + 1)))
186	142, 143, 185, 137	syl12anc 835	. . . . . . . . . 10 ⊢ (((𝜑 ∧ ((𝑘 ∈ (1...𝐽) ∧ 0 ≤ ((𝐹‘𝐶)‘𝑘)) ∧ ∀𝑗 ∈ {𝑖 ∈ (1...𝐽) ∣ 0 ≤ ((𝐹‘𝐶)‘𝑖)}𝑗 ≤ 𝑘)) ∧ (𝑘 + 1) ∈ 𝐶) → (𝑘 + 1) ≤ 𝑘)
187	18, 186	mtand 814	. . . . . . . . 9 ⊢ ((𝜑 ∧ ((𝑘 ∈ (1...𝐽) ∧ 0 ≤ ((𝐹‘𝐶)‘𝑘)) ∧ ∀𝑗 ∈ {𝑖 ∈ (1...𝐽) ∣ 0 ≤ ((𝐹‘𝐶)‘𝑖)}𝑗 ≤ 𝑘)) → ¬ (𝑘 + 1) ∈ 𝐶)
188	162	simpld 495	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑘 + 1) ∈ (1...𝐽)) → (¬ (𝑘 + 1) ∈ 𝐶 → ((𝐹‘𝐶)‘(𝑘 + 1)) = (((𝐹‘𝐶)‘((𝑘 + 1) − 1)) − 1)))
189	188	imp 407	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝑘 + 1) ∈ (1...𝐽)) ∧ ¬ (𝑘 + 1) ∈ 𝐶) → ((𝐹‘𝐶)‘(𝑘 + 1)) = (((𝐹‘𝐶)‘((𝑘 + 1) − 1)) − 1))
190	158, 189	sylan 580	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝑘 ∈ (1...𝐽) ∧ 0 ≤ ((𝐹‘𝐶)‘𝑘))) ∧ ¬ (𝑘 + 1) ∈ 𝐶) → ((𝐹‘𝐶)‘(𝑘 + 1)) = (((𝐹‘𝐶)‘((𝑘 + 1) − 1)) − 1))
191	5	adantr 481	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝑘 ∈ (1...𝐽) ∧ 0 ≤ ((𝐹‘𝐶)‘𝑘))) ∧ ¬ (𝑘 + 1) ∈ 𝐶) → 𝑘 ∈ (1...𝐽))
192	170	oveq1d 7372	. . . . . . . . . . . . 13 ⊢ (𝑘 ∈ (1...𝐽) → (((𝐹‘𝐶)‘((𝑘 + 1) − 1)) − 1) = (((𝐹‘𝐶)‘𝑘) − 1))
193	192	eqeq2d 2747	. . . . . . . . . . . 12 ⊢ (𝑘 ∈ (1...𝐽) → (((𝐹‘𝐶)‘(𝑘 + 1)) = (((𝐹‘𝐶)‘((𝑘 + 1) − 1)) − 1) ↔ ((𝐹‘𝐶)‘(𝑘 + 1)) = (((𝐹‘𝐶)‘𝑘) − 1)))
194	191, 193	syl 17	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝑘 ∈ (1...𝐽) ∧ 0 ≤ ((𝐹‘𝐶)‘𝑘))) ∧ ¬ (𝑘 + 1) ∈ 𝐶) → (((𝐹‘𝐶)‘(𝑘 + 1)) = (((𝐹‘𝐶)‘((𝑘 + 1) − 1)) − 1) ↔ ((𝐹‘𝐶)‘(𝑘 + 1)) = (((𝐹‘𝐶)‘𝑘) − 1)))
195	190, 194	mpbid 231	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝑘 ∈ (1...𝐽) ∧ 0 ≤ ((𝐹‘𝐶)‘𝑘))) ∧ ¬ (𝑘 + 1) ∈ 𝐶) → ((𝐹‘𝐶)‘(𝑘 + 1)) = (((𝐹‘𝐶)‘𝑘) − 1))
196	195	adantlrr 719	. . . . . . . . 9 ⊢ (((𝜑 ∧ ((𝑘 ∈ (1...𝐽) ∧ 0 ≤ ((𝐹‘𝐶)‘𝑘)) ∧ ∀𝑗 ∈ {𝑖 ∈ (1...𝐽) ∣ 0 ≤ ((𝐹‘𝐶)‘𝑖)}𝑗 ≤ 𝑘)) ∧ ¬ (𝑘 + 1) ∈ 𝐶) → ((𝐹‘𝐶)‘(𝑘 + 1)) = (((𝐹‘𝐶)‘𝑘) − 1))
197	187, 196	mpdan 685	. . . . . . . 8 ⊢ ((𝜑 ∧ ((𝑘 ∈ (1...𝐽) ∧ 0 ≤ ((𝐹‘𝐶)‘𝑘)) ∧ ∀𝑗 ∈ {𝑖 ∈ (1...𝐽) ∣ 0 ≤ ((𝐹‘𝐶)‘𝑖)}𝑗 ≤ 𝑘)) → ((𝐹‘𝐶)‘(𝑘 + 1)) = (((𝐹‘𝐶)‘𝑘) − 1))
198		breq2 5109	. . . . . . . . 9 ⊢ (((𝐹‘𝐶)‘(𝑘 + 1)) = (((𝐹‘𝐶)‘𝑘) − 1) → (0 ≤ ((𝐹‘𝐶)‘(𝑘 + 1)) ↔ 0 ≤ (((𝐹‘𝐶)‘𝑘) − 1)))
199	198	notbid 317	. . . . . . . 8 ⊢ (((𝐹‘𝐶)‘(𝑘 + 1)) = (((𝐹‘𝐶)‘𝑘) − 1) → (¬ 0 ≤ ((𝐹‘𝐶)‘(𝑘 + 1)) ↔ ¬ 0 ≤ (((𝐹‘𝐶)‘𝑘) − 1)))
200	197, 199	syl 17	. . . . . . 7 ⊢ ((𝜑 ∧ ((𝑘 ∈ (1...𝐽) ∧ 0 ≤ ((𝐹‘𝐶)‘𝑘)) ∧ ∀𝑗 ∈ {𝑖 ∈ (1...𝐽) ∣ 0 ≤ ((𝐹‘𝐶)‘𝑖)}𝑗 ≤ 𝑘)) → (¬ 0 ≤ ((𝐹‘𝐶)‘(𝑘 + 1)) ↔ ¬ 0 ≤ (((𝐹‘𝐶)‘𝑘) − 1)))
201	141, 200	mpbid 231	. . . . . 6 ⊢ ((𝜑 ∧ ((𝑘 ∈ (1...𝐽) ∧ 0 ≤ ((𝐹‘𝐶)‘𝑘)) ∧ ∀𝑗 ∈ {𝑖 ∈ (1...𝐽) ∣ 0 ≤ ((𝐹‘𝐶)‘𝑖)}𝑗 ≤ 𝑘)) → ¬ 0 ≤ (((𝐹‘𝐶)‘𝑘) − 1))
202	5, 36	syl 17	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑘 ∈ (1...𝐽) ∧ 0 ≤ ((𝐹‘𝐶)‘𝑘))) → 𝑘 ∈ (0...𝐽))
203	202, 46	syldan 591	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑘 ∈ (1...𝐽) ∧ 0 ≤ ((𝐹‘𝐶)‘𝑘))) → ((𝐹‘𝐶)‘𝑘) ∈ ℤ)
204	203	adantrr 715	. . . . . . 7 ⊢ ((𝜑 ∧ ((𝑘 ∈ (1...𝐽) ∧ 0 ≤ ((𝐹‘𝐶)‘𝑘)) ∧ ∀𝑗 ∈ {𝑖 ∈ (1...𝐽) ∣ 0 ≤ ((𝐹‘𝐶)‘𝑖)}𝑗 ≤ 𝑘)) → ((𝐹‘𝐶)‘𝑘) ∈ ℤ)
205		zlem1lt 12555	. . . . . . . . 9 ⊢ ((((𝐹‘𝐶)‘𝑘) ∈ ℤ ∧ 0 ∈ ℤ) → (((𝐹‘𝐶)‘𝑘) ≤ 0 ↔ (((𝐹‘𝐶)‘𝑘) − 1) < 0))
206	175, 205	mpan2 689	. . . . . . . 8 ⊢ (((𝐹‘𝐶)‘𝑘) ∈ ℤ → (((𝐹‘𝐶)‘𝑘) ≤ 0 ↔ (((𝐹‘𝐶)‘𝑘) − 1) < 0))
207		zre 12503	. . . . . . . . . 10 ⊢ (((𝐹‘𝐶)‘𝑘) ∈ ℤ → ((𝐹‘𝐶)‘𝑘) ∈ ℝ)
208		1red 11156	. . . . . . . . . 10 ⊢ (((𝐹‘𝐶)‘𝑘) ∈ ℤ → 1 ∈ ℝ)
209	207, 208	resubcld 11583	. . . . . . . . 9 ⊢ (((𝐹‘𝐶)‘𝑘) ∈ ℤ → (((𝐹‘𝐶)‘𝑘) − 1) ∈ ℝ)
210		0red 11158	. . . . . . . . 9 ⊢ (((𝐹‘𝐶)‘𝑘) ∈ ℤ → 0 ∈ ℝ)
211	209, 210	ltnled 11302	. . . . . . . 8 ⊢ (((𝐹‘𝐶)‘𝑘) ∈ ℤ → ((((𝐹‘𝐶)‘𝑘) − 1) < 0 ↔ ¬ 0 ≤ (((𝐹‘𝐶)‘𝑘) − 1)))
212	206, 211	bitrd 278	. . . . . . 7 ⊢ (((𝐹‘𝐶)‘𝑘) ∈ ℤ → (((𝐹‘𝐶)‘𝑘) ≤ 0 ↔ ¬ 0 ≤ (((𝐹‘𝐶)‘𝑘) − 1)))
213	204, 212	syl 17	. . . . . 6 ⊢ ((𝜑 ∧ ((𝑘 ∈ (1...𝐽) ∧ 0 ≤ ((𝐹‘𝐶)‘𝑘)) ∧ ∀𝑗 ∈ {𝑖 ∈ (1...𝐽) ∣ 0 ≤ ((𝐹‘𝐶)‘𝑖)}𝑗 ≤ 𝑘)) → (((𝐹‘𝐶)‘𝑘) ≤ 0 ↔ ¬ 0 ≤ (((𝐹‘𝐶)‘𝑘) − 1)))
214	201, 213	mpbird 256	. . . . 5 ⊢ ((𝜑 ∧ ((𝑘 ∈ (1...𝐽) ∧ 0 ≤ ((𝐹‘𝐶)‘𝑘)) ∧ ∀𝑗 ∈ {𝑖 ∈ (1...𝐽) ∣ 0 ≤ ((𝐹‘𝐶)‘𝑖)}𝑗 ≤ 𝑘)) → ((𝐹‘𝐶)‘𝑘) ≤ 0)
215		simprlr 778	. . . . 5 ⊢ ((𝜑 ∧ ((𝑘 ∈ (1...𝐽) ∧ 0 ≤ ((𝐹‘𝐶)‘𝑘)) ∧ ∀𝑗 ∈ {𝑖 ∈ (1...𝐽) ∣ 0 ≤ ((𝐹‘𝐶)‘𝑖)}𝑗 ≤ 𝑘)) → 0 ≤ ((𝐹‘𝐶)‘𝑘))
216	204	zred 12607	. . . . . 6 ⊢ ((𝜑 ∧ ((𝑘 ∈ (1...𝐽) ∧ 0 ≤ ((𝐹‘𝐶)‘𝑘)) ∧ ∀𝑗 ∈ {𝑖 ∈ (1...𝐽) ∣ 0 ≤ ((𝐹‘𝐶)‘𝑖)}𝑗 ≤ 𝑘)) → ((𝐹‘𝐶)‘𝑘) ∈ ℝ)
217		0red 11158	. . . . . 6 ⊢ ((𝜑 ∧ ((𝑘 ∈ (1...𝐽) ∧ 0 ≤ ((𝐹‘𝐶)‘𝑘)) ∧ ∀𝑗 ∈ {𝑖 ∈ (1...𝐽) ∣ 0 ≤ ((𝐹‘𝐶)‘𝑖)}𝑗 ≤ 𝑘)) → 0 ∈ ℝ)
218	216, 217	letri3d 11297	. . . . 5 ⊢ ((𝜑 ∧ ((𝑘 ∈ (1...𝐽) ∧ 0 ≤ ((𝐹‘𝐶)‘𝑘)) ∧ ∀𝑗 ∈ {𝑖 ∈ (1...𝐽) ∣ 0 ≤ ((𝐹‘𝐶)‘𝑖)}𝑗 ≤ 𝑘)) → (((𝐹‘𝐶)‘𝑘) = 0 ↔ (((𝐹‘𝐶)‘𝑘) ≤ 0 ∧ 0 ≤ ((𝐹‘𝐶)‘𝑘))))
219	214, 215, 218	mpbir2and 711	. . . 4 ⊢ ((𝜑 ∧ ((𝑘 ∈ (1...𝐽) ∧ 0 ≤ ((𝐹‘𝐶)‘𝑘)) ∧ ∀𝑗 ∈ {𝑖 ∈ (1...𝐽) ∣ 0 ≤ ((𝐹‘𝐶)‘𝑖)}𝑗 ≤ 𝑘)) → ((𝐹‘𝐶)‘𝑘) = 0)
220	4, 219	sylan2b 594	. . 3 ⊢ ((𝜑 ∧ (𝑘 ∈ {𝑖 ∈ (1...𝐽) ∣ 0 ≤ ((𝐹‘𝐶)‘𝑖)} ∧ ∀𝑗 ∈ {𝑖 ∈ (1...𝐽) ∣ 0 ≤ ((𝐹‘𝐶)‘𝑖)}𝑗 ≤ 𝑘)) → ((𝐹‘𝐶)‘𝑘) = 0)
221		ssrab2 4037	. . . . . 6 ⊢ {𝑖 ∈ (1...𝐽) ∣ 0 ≤ ((𝐹‘𝐶)‘𝑖)} ⊆ (1...𝐽)
222	221, 11	sstri 3953	. . . . 5 ⊢ {𝑖 ∈ (1...𝐽) ∣ 0 ≤ ((𝐹‘𝐶)‘𝑖)} ⊆ ℝ
223	222	a1i 11	. . . 4 ⊢ (𝜑 → {𝑖 ∈ (1...𝐽) ∣ 0 ≤ ((𝐹‘𝐶)‘𝑖)} ⊆ ℝ)
224		fzfi 13877	. . . . . 6 ⊢ (1...𝐽) ∈ Fin
225		ssfi 9117	. . . . . 6 ⊢ (((1...𝐽) ∈ Fin ∧ {𝑖 ∈ (1...𝐽) ∣ 0 ≤ ((𝐹‘𝐶)‘𝑖)} ⊆ (1...𝐽)) → {𝑖 ∈ (1...𝐽) ∣ 0 ≤ ((𝐹‘𝐶)‘𝑖)} ∈ Fin)
226	224, 221, 225	mp2an 690	. . . . 5 ⊢ {𝑖 ∈ (1...𝐽) ∣ 0 ≤ ((𝐹‘𝐶)‘𝑖)} ∈ Fin
227	226	a1i 11	. . . 4 ⊢ (𝜑 → {𝑖 ∈ (1...𝐽) ∣ 0 ≤ ((𝐹‘𝐶)‘𝑖)} ∈ Fin)
228		rabn0 4345	. . . . 5 ⊢ ({𝑖 ∈ (1...𝐽) ∣ 0 ≤ ((𝐹‘𝐶)‘𝑖)} ≠ ∅ ↔ ∃𝑖 ∈ (1...𝐽)0 ≤ ((𝐹‘𝐶)‘𝑖))
229	59, 228	sylibr 233	. . . 4 ⊢ (𝜑 → {𝑖 ∈ (1...𝐽) ∣ 0 ≤ ((𝐹‘𝐶)‘𝑖)} ≠ ∅)
230		fimaxre 12099	. . . 4 ⊢ (({𝑖 ∈ (1...𝐽) ∣ 0 ≤ ((𝐹‘𝐶)‘𝑖)} ⊆ ℝ ∧ {𝑖 ∈ (1...𝐽) ∣ 0 ≤ ((𝐹‘𝐶)‘𝑖)} ∈ Fin ∧ {𝑖 ∈ (1...𝐽) ∣ 0 ≤ ((𝐹‘𝐶)‘𝑖)} ≠ ∅) → ∃𝑘 ∈ {𝑖 ∈ (1...𝐽) ∣ 0 ≤ ((𝐹‘𝐶)‘𝑖)}∀𝑗 ∈ {𝑖 ∈ (1...𝐽) ∣ 0 ≤ ((𝐹‘𝐶)‘𝑖)}𝑗 ≤ 𝑘)
231	223, 227, 229, 230	syl3anc 1371	. . 3 ⊢ (𝜑 → ∃𝑘 ∈ {𝑖 ∈ (1...𝐽) ∣ 0 ≤ ((𝐹‘𝐶)‘𝑖)}∀𝑗 ∈ {𝑖 ∈ (1...𝐽) ∣ 0 ≤ ((𝐹‘𝐶)‘𝑖)}𝑗 ≤ 𝑘)
232	220, 231	reximddv 3168	. 2 ⊢ (𝜑 → ∃𝑘 ∈ {𝑖 ∈ (1...𝐽) ∣ 0 ≤ ((𝐹‘𝐶)‘𝑖)} ((𝐹‘𝐶)‘𝑘) = 0)
233		elrabi 3639	. . . 4 ⊢ (𝑘 ∈ {𝑖 ∈ (1...𝐽) ∣ 0 ≤ ((𝐹‘𝐶)‘𝑖)} → 𝑘 ∈ (1...𝐽))
234	233	anim1i 615	. . 3 ⊢ ((𝑘 ∈ {𝑖 ∈ (1...𝐽) ∣ 0 ≤ ((𝐹‘𝐶)‘𝑖)} ∧ ((𝐹‘𝐶)‘𝑘) = 0) → (𝑘 ∈ (1...𝐽) ∧ ((𝐹‘𝐶)‘𝑘) = 0))
235	234	reximi2 3082	. 2 ⊢ (∃𝑘 ∈ {𝑖 ∈ (1...𝐽) ∣ 0 ≤ ((𝐹‘𝐶)‘𝑖)} ((𝐹‘𝐶)‘𝑘) = 0 → ∃𝑘 ∈ (1...𝐽)((𝐹‘𝐶)‘𝑘) = 0)
236	232, 235	syl 17	1 ⊢ (𝜑 → ∃𝑘 ∈ (1...𝐽)((𝐹‘𝐶)‘𝑘) = 0)

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ↔ wb 205 ∧ wa 396 ∨ wo 845 = wceq 1541 ∈ wcel 2106 ≠ wne 2943 ∀wral 3064 ∃wrex 3073 {crab 3407 ∖ cdif 3907 ∩ cin 3909 ⊆ wss 3910 ∅c0 4282 𝒫 cpw 4560 {csn 4586 class class class wbr 5105 ↦ cmpt 5188 ‘cfv 6496 (class class class)co 7357 Fincfn 8883 ℝcr 11050 0cc0 11051 1c1 11052 + caddc 11054 < clt 11189 ≤ cle 11190 − cmin 11385 / cdiv 11812 ℕcn 12153 2c2 12208 ℤcz 12499 ℤ_≥cuz 12763 ...cfz 13424 ♯chash 14230

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1797 ax-4 1811 ax-5 1913 ax-6 1971 ax-7 2011 ax-8 2108 ax-9 2116 ax-10 2137 ax-11 2154 ax-12 2171 ax-ext 2707 ax-rep 5242 ax-sep 5256 ax-nul 5263 ax-pow 5320 ax-pr 5384 ax-un 7672 ax-cnex 11107 ax-resscn 11108 ax-1cn 11109 ax-icn 11110 ax-addcl 11111 ax-addrcl 11112 ax-mulcl 11113 ax-mulrcl 11114 ax-mulcom 11115 ax-addass 11116 ax-mulass 11117 ax-distr 11118 ax-i2m1 11119 ax-1ne0 11120 ax-1rid 11121 ax-rnegex 11122 ax-rrecex 11123 ax-cnre 11124 ax-pre-lttri 11125 ax-pre-lttrn 11126 ax-pre-ltadd 11127 ax-pre-mulgt0 11128

This theorem depends on definitions: df-bi 206 df-an 397 df-or 846 df-3or 1088 df-3an 1089 df-tru 1544 df-fal 1554 df-ex 1782 df-nf 1786 df-sb 2068 df-mo 2538 df-eu 2567 df-clab 2714 df-cleq 2728 df-clel 2814 df-nfc 2889 df-ne 2944 df-nel 3050 df-ral 3065 df-rex 3074 df-reu 3354 df-rab 3408 df-v 3447 df-sbc 3740 df-csb 3856 df-dif 3913 df-un 3915 df-in 3917 df-ss 3927 df-pss 3929 df-nul 4283 df-if 4487 df-pw 4562 df-sn 4587 df-pr 4589 df-op 4593 df-uni 4866 df-int 4908 df-iun 4956 df-br 5106 df-opab 5168 df-mpt 5189 df-tr 5223 df-id 5531 df-eprel 5537 df-po 5545 df-so 5546 df-fr 5588 df-we 5590 df-xp 5639 df-rel 5640 df-cnv 5641 df-co 5642 df-dm 5643 df-rn 5644 df-res 5645 df-ima 5646 df-pred 6253 df-ord 6320 df-on 6321 df-lim 6322 df-suc 6323 df-iota 6448 df-fun 6498 df-fn 6499 df-f 6500 df-f1 6501 df-fo 6502 df-f1o 6503 df-fv 6504 df-riota 7313 df-ov 7360 df-oprab 7361 df-mpo 7362 df-om 7803 df-1st 7921 df-2nd 7922 df-frecs 8212 df-wrecs 8243 df-recs 8317 df-rdg 8356 df-1o 8412 df-oadd 8416 df-er 8648 df-en 8884 df-dom 8885 df-sdom 8886 df-fin 8887 df-dju 9837 df-card 9875 df-pnf 11191 df-mnf 11192 df-xr 11193 df-ltxr 11194 df-le 11195 df-sub 11387 df-neg 11388 df-nn 12154 df-2 12216 df-n0 12414 df-z 12500 df-uz 12764 df-fz 13425 df-hash 14231

This theorem is referenced by: ballotlem1c 33107

W3C validator