Theorem ballotlemfcc

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

	Ref	Expression
Hypotheses	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	ballotlemfcc	⊢ ( 𝜑 → ∃ 𝑘 ∈ ( 1 ... 𝐽 ) ( ( 𝐹 ‘ 𝐶 ) ‘ 𝑘 ) = 0 )

Proof

Step	Hyp	Ref	Expression
1		ballotth.m	⊢ 𝑀 ∈ ℕ
2		ballotth.n	⊢ 𝑁 ∈ ℕ
3		ballotth.o	⊢ 𝑂 = { 𝑐 ∈ 𝒫 ( 1 ... ( 𝑀 + 𝑁 ) ) ∣ ( ♯ ‘ 𝑐 ) = 𝑀 }
4		ballotth.p	⊢ 𝑃 = ( 𝑥 ∈ 𝒫 𝑂 ↦ ( ( ♯ ‘ 𝑥 ) / ( ♯ ‘ 𝑂 ) ) )
5		ballotth.f	⊢ 𝐹 = ( 𝑐 ∈ 𝑂 ↦ ( 𝑖 ∈ ℤ ↦ ( ( ♯ ‘ ( ( 1 ... 𝑖 ) ∩ 𝑐 ) ) − ( ♯ ‘ ( ( 1 ... 𝑖 ) ∖ 𝑐 ) ) ) ) )
6		ballotlemfcc.c	⊢ ( 𝜑 → 𝐶 ∈ 𝑂 )
7		ballotlemfcc.j	⊢ ( 𝜑 → 𝐽 ∈ ℕ )
8		ballotlemfcc.3	⊢ ( 𝜑 → ∃ 𝑖 ∈ ( 1 ... 𝐽 ) 0 ≤ ( ( 𝐹 ‘ 𝐶 ) ‘ 𝑖 ) )
9		ballotlemfcc.4	⊢ ( 𝜑 → ( ( 𝐹 ‘ 𝐶 ) ‘ 𝐽 ) < 0 )
10		fveq2	⊢ ( 𝑖 = 𝑘 → ( ( 𝐹 ‘ 𝐶 ) ‘ 𝑖 ) = ( ( 𝐹 ‘ 𝐶 ) ‘ 𝑘 ) )
11	10	breq2d	⊢ ( 𝑖 = 𝑘 → ( 0 ≤ ( ( 𝐹 ‘ 𝐶 ) ‘ 𝑖 ) ↔ 0 ≤ ( ( 𝐹 ‘ 𝐶 ) ‘ 𝑘 ) ) )
12	11	elrab	⊢ ( 𝑘 ∈ { 𝑖 ∈ ( 1 ... 𝐽 ) ∣ 0 ≤ ( ( 𝐹 ‘ 𝐶 ) ‘ 𝑖 ) } ↔ ( 𝑘 ∈ ( 1 ... 𝐽 ) ∧ 0 ≤ ( ( 𝐹 ‘ 𝐶 ) ‘ 𝑘 ) ) )
13	12	anbi1i	⊢ ( ( 𝑘 ∈ { 𝑖 ∈ ( 1 ... 𝐽 ) ∣ 0 ≤ ( ( 𝐹 ‘ 𝐶 ) ‘ 𝑖 ) } ∧ ∀ 𝑗 ∈ { 𝑖 ∈ ( 1 ... 𝐽 ) ∣ 0 ≤ ( ( 𝐹 ‘ 𝐶 ) ‘ 𝑖 ) } 𝑗 ≤ 𝑘 ) ↔ ( ( 𝑘 ∈ ( 1 ... 𝐽 ) ∧ 0 ≤ ( ( 𝐹 ‘ 𝐶 ) ‘ 𝑘 ) ) ∧ ∀ 𝑗 ∈ { 𝑖 ∈ ( 1 ... 𝐽 ) ∣ 0 ≤ ( ( 𝐹 ‘ 𝐶 ) ‘ 𝑖 ) } 𝑗 ≤ 𝑘 ) )
14		simprl	⊢ ( ( 𝜑 ∧ ( 𝑘 ∈ ( 1 ... 𝐽 ) ∧ 0 ≤ ( ( 𝐹 ‘ 𝐶 ) ‘ 𝑘 ) ) ) → 𝑘 ∈ ( 1 ... 𝐽 ) )
15	14	adantrr	⊢ ( ( 𝜑 ∧ ( ( 𝑘 ∈ ( 1 ... 𝐽 ) ∧ 0 ≤ ( ( 𝐹 ‘ 𝐶 ) ‘ 𝑘 ) ) ∧ ∀ 𝑗 ∈ { 𝑖 ∈ ( 1 ... 𝐽 ) ∣ 0 ≤ ( ( 𝐹 ‘ 𝐶 ) ‘ 𝑖 ) } 𝑗 ≤ 𝑘 ) ) → 𝑘 ∈ ( 1 ... 𝐽 ) )
16		fzssuz	⊢ ( 1 ... 𝐽 ) ⊆ ( ℤ≥ ‘ 1 )
17		uzssz	⊢ ( ℤ≥ ‘ 1 ) ⊆ ℤ
18	16 17	sstri	⊢ ( 1 ... 𝐽 ) ⊆ ℤ
19		zssre	⊢ ℤ ⊆ ℝ
20	18 19	sstri	⊢ ( 1 ... 𝐽 ) ⊆ ℝ
21	20	sseli	⊢ ( 𝑘 ∈ ( 1 ... 𝐽 ) → 𝑘 ∈ ℝ )
22	21	ltp1d	⊢ ( 𝑘 ∈ ( 1 ... 𝐽 ) → 𝑘 < ( 𝑘 + 1 ) )
23		1red	⊢ ( 𝑘 ∈ ( 1 ... 𝐽 ) → 1 ∈ ℝ )
24	21 23	readdcld	⊢ ( 𝑘 ∈ ( 1 ... 𝐽 ) → ( 𝑘 + 1 ) ∈ ℝ )
25	21 24	ltnled	⊢ ( 𝑘 ∈ ( 1 ... 𝐽 ) → ( 𝑘 < ( 𝑘 + 1 ) ↔ ¬ ( 𝑘 + 1 ) ≤ 𝑘 ) )
26	22 25	mpbid	⊢ ( 𝑘 ∈ ( 1 ... 𝐽 ) → ¬ ( 𝑘 + 1 ) ≤ 𝑘 )
27	15 26	syl	⊢ ( ( 𝜑 ∧ ( ( 𝑘 ∈ ( 1 ... 𝐽 ) ∧ 0 ≤ ( ( 𝐹 ‘ 𝐶 ) ‘ 𝑘 ) ) ∧ ∀ 𝑗 ∈ { 𝑖 ∈ ( 1 ... 𝐽 ) ∣ 0 ≤ ( ( 𝐹 ‘ 𝐶 ) ‘ 𝑖 ) } 𝑗 ≤ 𝑘 ) ) → ¬ ( 𝑘 + 1 ) ≤ 𝑘 )
28		simprr	⊢ ( ( 𝜑 ∧ ( ( 𝑘 ∈ ( 1 ... 𝐽 ) ∧ 0 ≤ ( ( 𝐹 ‘ 𝐶 ) ‘ 𝑘 ) ) ∧ ∀ 𝑗 ∈ { 𝑖 ∈ ( 1 ... 𝐽 ) ∣ 0 ≤ ( ( 𝐹 ‘ 𝐶 ) ‘ 𝑖 ) } 𝑗 ≤ 𝑘 ) ) → ∀ 𝑗 ∈ { 𝑖 ∈ ( 1 ... 𝐽 ) ∣ 0 ≤ ( ( 𝐹 ‘ 𝐶 ) ‘ 𝑖 ) } 𝑗 ≤ 𝑘 )
29	9	adantr	⊢ ( ( 𝜑 ∧ 𝑘 = 𝐽 ) → ( ( 𝐹 ‘ 𝐶 ) ‘ 𝐽 ) < 0 )
30		simpr	⊢ ( ( 𝜑 ∧ 𝑘 = 𝐽 ) → 𝑘 = 𝐽 )
31	30	fveq2d	⊢ ( ( 𝜑 ∧ 𝑘 = 𝐽 ) → ( ( 𝐹 ‘ 𝐶 ) ‘ 𝑘 ) = ( ( 𝐹 ‘ 𝐶 ) ‘ 𝐽 ) )
32	31	breq1d	⊢ ( ( 𝜑 ∧ 𝑘 = 𝐽 ) → ( ( ( 𝐹 ‘ 𝐶 ) ‘ 𝑘 ) < 0 ↔ ( ( 𝐹 ‘ 𝐶 ) ‘ 𝐽 ) < 0 ) )
33		elnnuz	⊢ ( 𝐽 ∈ ℕ ↔ 𝐽 ∈ ( ℤ≥ ‘ 1 ) )
34	7 33	sylib	⊢ ( 𝜑 → 𝐽 ∈ ( ℤ≥ ‘ 1 ) )
35		eluzfz2	⊢ ( 𝐽 ∈ ( ℤ≥ ‘ 1 ) → 𝐽 ∈ ( 1 ... 𝐽 ) )
36	34 35	syl	⊢ ( 𝜑 → 𝐽 ∈ ( 1 ... 𝐽 ) )
37		eleq1	⊢ ( 𝑘 = 𝐽 → ( 𝑘 ∈ ( 1 ... 𝐽 ) ↔ 𝐽 ∈ ( 1 ... 𝐽 ) ) )
38	36 37	syl5ibrcom	⊢ ( 𝜑 → ( 𝑘 = 𝐽 → 𝑘 ∈ ( 1 ... 𝐽 ) ) )
39	38	anc2li	⊢ ( 𝜑 → ( 𝑘 = 𝐽 → ( 𝜑 ∧ 𝑘 ∈ ( 1 ... 𝐽 ) ) ) )
40		1eluzge0	⊢ 1 ∈ ( ℤ≥ ‘ 0 )
41		fzss1	⊢ ( 1 ∈ ( ℤ≥ ‘ 0 ) → ( 1 ... 𝐽 ) ⊆ ( 0 ... 𝐽 ) )
42	41	sseld	⊢ ( 1 ∈ ( ℤ≥ ‘ 0 ) → ( 𝑘 ∈ ( 1 ... 𝐽 ) → 𝑘 ∈ ( 0 ... 𝐽 ) ) )
43	40 42	ax-mp	⊢ ( 𝑘 ∈ ( 1 ... 𝐽 ) → 𝑘 ∈ ( 0 ... 𝐽 ) )
44	6	adantr	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... 𝐽 ) ) → 𝐶 ∈ 𝑂 )
45		elfzelz	⊢ ( 𝑘 ∈ ( 0 ... 𝐽 ) → 𝑘 ∈ ℤ )
46	45	adantl	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... 𝐽 ) ) → 𝑘 ∈ ℤ )
47	1 2 3 4 5 44 46	ballotlemfelz	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... 𝐽 ) ) → ( ( 𝐹 ‘ 𝐶 ) ‘ 𝑘 ) ∈ ℤ )
48	47	zred	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... 𝐽 ) ) → ( ( 𝐹 ‘ 𝐶 ) ‘ 𝑘 ) ∈ ℝ )
49		0red	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... 𝐽 ) ) → 0 ∈ ℝ )
50	48 49	ltnled	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... 𝐽 ) ) → ( ( ( 𝐹 ‘ 𝐶 ) ‘ 𝑘 ) < 0 ↔ ¬ 0 ≤ ( ( 𝐹 ‘ 𝐶 ) ‘ 𝑘 ) ) )
51	43 50	sylan2	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 1 ... 𝐽 ) ) → ( ( ( 𝐹 ‘ 𝐶 ) ‘ 𝑘 ) < 0 ↔ ¬ 0 ≤ ( ( 𝐹 ‘ 𝐶 ) ‘ 𝑘 ) ) )
52	39 51	syl6	⊢ ( 𝜑 → ( 𝑘 = 𝐽 → ( ( ( 𝐹 ‘ 𝐶 ) ‘ 𝑘 ) < 0 ↔ ¬ 0 ≤ ( ( 𝐹 ‘ 𝐶 ) ‘ 𝑘 ) ) ) )
53	52	imp	⊢ ( ( 𝜑 ∧ 𝑘 = 𝐽 ) → ( ( ( 𝐹 ‘ 𝐶 ) ‘ 𝑘 ) < 0 ↔ ¬ 0 ≤ ( ( 𝐹 ‘ 𝐶 ) ‘ 𝑘 ) ) )
54	32 53	bitr3d	⊢ ( ( 𝜑 ∧ 𝑘 = 𝐽 ) → ( ( ( 𝐹 ‘ 𝐶 ) ‘ 𝐽 ) < 0 ↔ ¬ 0 ≤ ( ( 𝐹 ‘ 𝐶 ) ‘ 𝑘 ) ) )
55	29 54	mpbid	⊢ ( ( 𝜑 ∧ 𝑘 = 𝐽 ) → ¬ 0 ≤ ( ( 𝐹 ‘ 𝐶 ) ‘ 𝑘 ) )
56	55	ex	⊢ ( 𝜑 → ( 𝑘 = 𝐽 → ¬ 0 ≤ ( ( 𝐹 ‘ 𝐶 ) ‘ 𝑘 ) ) )
57	56	con2d	⊢ ( 𝜑 → ( 0 ≤ ( ( 𝐹 ‘ 𝐶 ) ‘ 𝑘 ) → ¬ 𝑘 = 𝐽 ) )
58		nn1m1nn	⊢ ( 𝐽 ∈ ℕ → ( 𝐽 = 1 ∨ ( 𝐽 − 1 ) ∈ ℕ ) )
59	7 58	syl	⊢ ( 𝜑 → ( 𝐽 = 1 ∨ ( 𝐽 − 1 ) ∈ ℕ ) )
60	8	adantr	⊢ ( ( 𝜑 ∧ 𝐽 = 1 ) → ∃ 𝑖 ∈ ( 1 ... 𝐽 ) 0 ≤ ( ( 𝐹 ‘ 𝐶 ) ‘ 𝑖 ) )
61		oveq1	⊢ ( 𝐽 = 1 → ( 𝐽 ... 𝐽 ) = ( 1 ... 𝐽 ) )
62	61	adantl	⊢ ( ( 𝜑 ∧ 𝐽 = 1 ) → ( 𝐽 ... 𝐽 ) = ( 1 ... 𝐽 ) )
63	7	nnzd	⊢ ( 𝜑 → 𝐽 ∈ ℤ )
64		fzsn	⊢ ( 𝐽 ∈ ℤ → ( 𝐽 ... 𝐽 ) = { 𝐽 } )
65	63 64	syl	⊢ ( 𝜑 → ( 𝐽 ... 𝐽 ) = { 𝐽 } )
66	65	adantr	⊢ ( ( 𝜑 ∧ 𝐽 = 1 ) → ( 𝐽 ... 𝐽 ) = { 𝐽 } )
67	62 66	eqtr3d	⊢ ( ( 𝜑 ∧ 𝐽 = 1 ) → ( 1 ... 𝐽 ) = { 𝐽 } )
68	67	rexeqdv	⊢ ( ( 𝜑 ∧ 𝐽 = 1 ) → ( ∃ 𝑖 ∈ ( 1 ... 𝐽 ) 0 ≤ ( ( 𝐹 ‘ 𝐶 ) ‘ 𝑖 ) ↔ ∃ 𝑖 ∈ { 𝐽 } 0 ≤ ( ( 𝐹 ‘ 𝐶 ) ‘ 𝑖 ) ) )
69	60 68	mpbid	⊢ ( ( 𝜑 ∧ 𝐽 = 1 ) → ∃ 𝑖 ∈ { 𝐽 } 0 ≤ ( ( 𝐹 ‘ 𝐶 ) ‘ 𝑖 ) )
70		fveq2	⊢ ( 𝑖 = 𝐽 → ( ( 𝐹 ‘ 𝐶 ) ‘ 𝑖 ) = ( ( 𝐹 ‘ 𝐶 ) ‘ 𝐽 ) )
71	70	breq2d	⊢ ( 𝑖 = 𝐽 → ( 0 ≤ ( ( 𝐹 ‘ 𝐶 ) ‘ 𝑖 ) ↔ 0 ≤ ( ( 𝐹 ‘ 𝐶 ) ‘ 𝐽 ) ) )
72	71	rexsng	⊢ ( 𝐽 ∈ ℕ → ( ∃ 𝑖 ∈ { 𝐽 } 0 ≤ ( ( 𝐹 ‘ 𝐶 ) ‘ 𝑖 ) ↔ 0 ≤ ( ( 𝐹 ‘ 𝐶 ) ‘ 𝐽 ) ) )
73	7 72	syl	⊢ ( 𝜑 → ( ∃ 𝑖 ∈ { 𝐽 } 0 ≤ ( ( 𝐹 ‘ 𝐶 ) ‘ 𝑖 ) ↔ 0 ≤ ( ( 𝐹 ‘ 𝐶 ) ‘ 𝐽 ) ) )
74	73	adantr	⊢ ( ( 𝜑 ∧ 𝐽 = 1 ) → ( ∃ 𝑖 ∈ { 𝐽 } 0 ≤ ( ( 𝐹 ‘ 𝐶 ) ‘ 𝑖 ) ↔ 0 ≤ ( ( 𝐹 ‘ 𝐶 ) ‘ 𝐽 ) ) )
75	69 74	mpbid	⊢ ( ( 𝜑 ∧ 𝐽 = 1 ) → 0 ≤ ( ( 𝐹 ‘ 𝐶 ) ‘ 𝐽 ) )
76	9	adantr	⊢ ( ( 𝜑 ∧ 𝐽 = 1 ) → ( ( 𝐹 ‘ 𝐶 ) ‘ 𝐽 ) < 0 )
77	1 2 3 4 5 6 63	ballotlemfelz	⊢ ( 𝜑 → ( ( 𝐹 ‘ 𝐶 ) ‘ 𝐽 ) ∈ ℤ )
78	77	zred	⊢ ( 𝜑 → ( ( 𝐹 ‘ 𝐶 ) ‘ 𝐽 ) ∈ ℝ )
79		0red	⊢ ( 𝜑 → 0 ∈ ℝ )
80	78 79	ltnled	⊢ ( 𝜑 → ( ( ( 𝐹 ‘ 𝐶 ) ‘ 𝐽 ) < 0 ↔ ¬ 0 ≤ ( ( 𝐹 ‘ 𝐶 ) ‘ 𝐽 ) ) )
81	80	adantr	⊢ ( ( 𝜑 ∧ 𝐽 = 1 ) → ( ( ( 𝐹 ‘ 𝐶 ) ‘ 𝐽 ) < 0 ↔ ¬ 0 ≤ ( ( 𝐹 ‘ 𝐶 ) ‘ 𝐽 ) ) )
82	76 81	mpbid	⊢ ( ( 𝜑 ∧ 𝐽 = 1 ) → ¬ 0 ≤ ( ( 𝐹 ‘ 𝐶 ) ‘ 𝐽 ) )
83	75 82	pm2.65da	⊢ ( 𝜑 → ¬ 𝐽 = 1 )
84		biortn	⊢ ( ¬ 𝐽 = 1 → ( ( 𝐽 − 1 ) ∈ ℕ ↔ ( ¬ ¬ 𝐽 = 1 ∨ ( 𝐽 − 1 ) ∈ ℕ ) ) )
85	83 84	syl	⊢ ( 𝜑 → ( ( 𝐽 − 1 ) ∈ ℕ ↔ ( ¬ ¬ 𝐽 = 1 ∨ ( 𝐽 − 1 ) ∈ ℕ ) ) )
86		notnotb	⊢ ( 𝐽 = 1 ↔ ¬ ¬ 𝐽 = 1 )
87	86	orbi1i	⊢ ( ( 𝐽 = 1 ∨ ( 𝐽 − 1 ) ∈ ℕ ) ↔ ( ¬ ¬ 𝐽 = 1 ∨ ( 𝐽 − 1 ) ∈ ℕ ) )
88	85 87	bitr4di	⊢ ( 𝜑 → ( ( 𝐽 − 1 ) ∈ ℕ ↔ ( 𝐽 = 1 ∨ ( 𝐽 − 1 ) ∈ ℕ ) ) )
89	59 88	mpbird	⊢ ( 𝜑 → ( 𝐽 − 1 ) ∈ ℕ )
90		elnnuz	⊢ ( ( 𝐽 − 1 ) ∈ ℕ ↔ ( 𝐽 − 1 ) ∈ ( ℤ≥ ‘ 1 ) )
91	89 90	sylib	⊢ ( 𝜑 → ( 𝐽 − 1 ) ∈ ( ℤ≥ ‘ 1 ) )
92		elfzp1	⊢ ( ( 𝐽 − 1 ) ∈ ( ℤ≥ ‘ 1 ) → ( 𝑘 ∈ ( 1 ... ( ( 𝐽 − 1 ) + 1 ) ) ↔ ( 𝑘 ∈ ( 1 ... ( 𝐽 − 1 ) ) ∨ 𝑘 = ( ( 𝐽 − 1 ) + 1 ) ) ) )
93	91 92	syl	⊢ ( 𝜑 → ( 𝑘 ∈ ( 1 ... ( ( 𝐽 − 1 ) + 1 ) ) ↔ ( 𝑘 ∈ ( 1 ... ( 𝐽 − 1 ) ) ∨ 𝑘 = ( ( 𝐽 − 1 ) + 1 ) ) ) )
94	7	nncnd	⊢ ( 𝜑 → 𝐽 ∈ ℂ )
95		1cnd	⊢ ( 𝜑 → 1 ∈ ℂ )
96	94 95	npcand	⊢ ( 𝜑 → ( ( 𝐽 − 1 ) + 1 ) = 𝐽 )
97	96	oveq2d	⊢ ( 𝜑 → ( 1 ... ( ( 𝐽 − 1 ) + 1 ) ) = ( 1 ... 𝐽 ) )
98	97	eleq2d	⊢ ( 𝜑 → ( 𝑘 ∈ ( 1 ... ( ( 𝐽 − 1 ) + 1 ) ) ↔ 𝑘 ∈ ( 1 ... 𝐽 ) ) )
99	96	eqeq2d	⊢ ( 𝜑 → ( 𝑘 = ( ( 𝐽 − 1 ) + 1 ) ↔ 𝑘 = 𝐽 ) )
100	99	orbi2d	⊢ ( 𝜑 → ( ( 𝑘 ∈ ( 1 ... ( 𝐽 − 1 ) ) ∨ 𝑘 = ( ( 𝐽 − 1 ) + 1 ) ) ↔ ( 𝑘 ∈ ( 1 ... ( 𝐽 − 1 ) ) ∨ 𝑘 = 𝐽 ) ) )
101	93 98 100	3bitr3d	⊢ ( 𝜑 → ( 𝑘 ∈ ( 1 ... 𝐽 ) ↔ ( 𝑘 ∈ ( 1 ... ( 𝐽 − 1 ) ) ∨ 𝑘 = 𝐽 ) ) )
102		orcom	⊢ ( ( 𝑘 ∈ ( 1 ... ( 𝐽 − 1 ) ) ∨ 𝑘 = 𝐽 ) ↔ ( 𝑘 = 𝐽 ∨ 𝑘 ∈ ( 1 ... ( 𝐽 − 1 ) ) ) )
103	101 102	bitrdi	⊢ ( 𝜑 → ( 𝑘 ∈ ( 1 ... 𝐽 ) ↔ ( 𝑘 = 𝐽 ∨ 𝑘 ∈ ( 1 ... ( 𝐽 − 1 ) ) ) ) )
104	103	biimpd	⊢ ( 𝜑 → ( 𝑘 ∈ ( 1 ... 𝐽 ) → ( 𝑘 = 𝐽 ∨ 𝑘 ∈ ( 1 ... ( 𝐽 − 1 ) ) ) ) )
105		pm5.6	⊢ ( ( ( 𝑘 ∈ ( 1 ... 𝐽 ) ∧ ¬ 𝑘 = 𝐽 ) → 𝑘 ∈ ( 1 ... ( 𝐽 − 1 ) ) ) ↔ ( 𝑘 ∈ ( 1 ... 𝐽 ) → ( 𝑘 = 𝐽 ∨ 𝑘 ∈ ( 1 ... ( 𝐽 − 1 ) ) ) ) )
106	104 105	sylibr	⊢ ( 𝜑 → ( ( 𝑘 ∈ ( 1 ... 𝐽 ) ∧ ¬ 𝑘 = 𝐽 ) → 𝑘 ∈ ( 1 ... ( 𝐽 − 1 ) ) ) )
107	89	nnzd	⊢ ( 𝜑 → ( 𝐽 − 1 ) ∈ ℤ )
108		1z	⊢ 1 ∈ ℤ
109	107 108	jctil	⊢ ( 𝜑 → ( 1 ∈ ℤ ∧ ( 𝐽 − 1 ) ∈ ℤ ) )
110		elfzelz	⊢ ( 𝑘 ∈ ( 1 ... ( 𝐽 − 1 ) ) → 𝑘 ∈ ℤ )
111	110 108	jctir	⊢ ( 𝑘 ∈ ( 1 ... ( 𝐽 − 1 ) ) → ( 𝑘 ∈ ℤ ∧ 1 ∈ ℤ ) )
112		fzaddel	⊢ ( ( ( 1 ∈ ℤ ∧ ( 𝐽 − 1 ) ∈ ℤ ) ∧ ( 𝑘 ∈ ℤ ∧ 1 ∈ ℤ ) ) → ( 𝑘 ∈ ( 1 ... ( 𝐽 − 1 ) ) ↔ ( 𝑘 + 1 ) ∈ ( ( 1 + 1 ) ... ( ( 𝐽 − 1 ) + 1 ) ) ) )
113	109 111 112	syl2an	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 1 ... ( 𝐽 − 1 ) ) ) → ( 𝑘 ∈ ( 1 ... ( 𝐽 − 1 ) ) ↔ ( 𝑘 + 1 ) ∈ ( ( 1 + 1 ) ... ( ( 𝐽 − 1 ) + 1 ) ) ) )
114	113	biimp3a	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 1 ... ( 𝐽 − 1 ) ) ∧ 𝑘 ∈ ( 1 ... ( 𝐽 − 1 ) ) ) → ( 𝑘 + 1 ) ∈ ( ( 1 + 1 ) ... ( ( 𝐽 − 1 ) + 1 ) ) )
115	114	3anidm23	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 1 ... ( 𝐽 − 1 ) ) ) → ( 𝑘 + 1 ) ∈ ( ( 1 + 1 ) ... ( ( 𝐽 − 1 ) + 1 ) ) )
116		1p1e2	⊢ ( 1 + 1 ) = 2
117	116	a1i	⊢ ( 𝜑 → ( 1 + 1 ) = 2 )
118	117 96	oveq12d	⊢ ( 𝜑 → ( ( 1 + 1 ) ... ( ( 𝐽 − 1 ) + 1 ) ) = ( 2 ... 𝐽 ) )
119	118	eleq2d	⊢ ( 𝜑 → ( ( 𝑘 + 1 ) ∈ ( ( 1 + 1 ) ... ( ( 𝐽 − 1 ) + 1 ) ) ↔ ( 𝑘 + 1 ) ∈ ( 2 ... 𝐽 ) ) )
120		2eluzge1	⊢ 2 ∈ ( ℤ≥ ‘ 1 )
121		fzss1	⊢ ( 2 ∈ ( ℤ≥ ‘ 1 ) → ( 2 ... 𝐽 ) ⊆ ( 1 ... 𝐽 ) )
122	120 121	ax-mp	⊢ ( 2 ... 𝐽 ) ⊆ ( 1 ... 𝐽 )
123	122	sseli	⊢ ( ( 𝑘 + 1 ) ∈ ( 2 ... 𝐽 ) → ( 𝑘 + 1 ) ∈ ( 1 ... 𝐽 ) )
124	119 123	syl6bi	⊢ ( 𝜑 → ( ( 𝑘 + 1 ) ∈ ( ( 1 + 1 ) ... ( ( 𝐽 − 1 ) + 1 ) ) → ( 𝑘 + 1 ) ∈ ( 1 ... 𝐽 ) ) )
125	124	adantr	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 1 ... ( 𝐽 − 1 ) ) ) → ( ( 𝑘 + 1 ) ∈ ( ( 1 + 1 ) ... ( ( 𝐽 − 1 ) + 1 ) ) → ( 𝑘 + 1 ) ∈ ( 1 ... 𝐽 ) ) )
126	115 125	mpd	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 1 ... ( 𝐽 − 1 ) ) ) → ( 𝑘 + 1 ) ∈ ( 1 ... 𝐽 ) )
127	126	ex	⊢ ( 𝜑 → ( 𝑘 ∈ ( 1 ... ( 𝐽 − 1 ) ) → ( 𝑘 + 1 ) ∈ ( 1 ... 𝐽 ) ) )
128	106 127	syld	⊢ ( 𝜑 → ( ( 𝑘 ∈ ( 1 ... 𝐽 ) ∧ ¬ 𝑘 = 𝐽 ) → ( 𝑘 + 1 ) ∈ ( 1 ... 𝐽 ) ) )
129	57 128	sylan2d	⊢ ( 𝜑 → ( ( 𝑘 ∈ ( 1 ... 𝐽 ) ∧ 0 ≤ ( ( 𝐹 ‘ 𝐶 ) ‘ 𝑘 ) ) → ( 𝑘 + 1 ) ∈ ( 1 ... 𝐽 ) ) )
130	129	imp	⊢ ( ( 𝜑 ∧ ( 𝑘 ∈ ( 1 ... 𝐽 ) ∧ 0 ≤ ( ( 𝐹 ‘ 𝐶 ) ‘ 𝑘 ) ) ) → ( 𝑘 + 1 ) ∈ ( 1 ... 𝐽 ) )
131	130	adantrr	⊢ ( ( 𝜑 ∧ ( ( 𝑘 ∈ ( 1 ... 𝐽 ) ∧ 0 ≤ ( ( 𝐹 ‘ 𝐶 ) ‘ 𝑘 ) ) ∧ ∀ 𝑗 ∈ { 𝑖 ∈ ( 1 ... 𝐽 ) ∣ 0 ≤ ( ( 𝐹 ‘ 𝐶 ) ‘ 𝑖 ) } 𝑗 ≤ 𝑘 ) ) → ( 𝑘 + 1 ) ∈ ( 1 ... 𝐽 ) )
132		fveq2	⊢ ( 𝑖 = ( 𝑘 + 1 ) → ( ( 𝐹 ‘ 𝐶 ) ‘ 𝑖 ) = ( ( 𝐹 ‘ 𝐶 ) ‘ ( 𝑘 + 1 ) ) )
133	132	breq2d	⊢ ( 𝑖 = ( 𝑘 + 1 ) → ( 0 ≤ ( ( 𝐹 ‘ 𝐶 ) ‘ 𝑖 ) ↔ 0 ≤ ( ( 𝐹 ‘ 𝐶 ) ‘ ( 𝑘 + 1 ) ) ) )
134	133	elrab	⊢ ( ( 𝑘 + 1 ) ∈ { 𝑖 ∈ ( 1 ... 𝐽 ) ∣ 0 ≤ ( ( 𝐹 ‘ 𝐶 ) ‘ 𝑖 ) } ↔ ( ( 𝑘 + 1 ) ∈ ( 1 ... 𝐽 ) ∧ 0 ≤ ( ( 𝐹 ‘ 𝐶 ) ‘ ( 𝑘 + 1 ) ) ) )
135		breq1	⊢ ( 𝑗 = ( 𝑘 + 1 ) → ( 𝑗 ≤ 𝑘 ↔ ( 𝑘 + 1 ) ≤ 𝑘 ) )
136	135	rspccva	⊢ ( ( ∀ 𝑗 ∈ { 𝑖 ∈ ( 1 ... 𝐽 ) ∣ 0 ≤ ( ( 𝐹 ‘ 𝐶 ) ‘ 𝑖 ) } 𝑗 ≤ 𝑘 ∧ ( 𝑘 + 1 ) ∈ { 𝑖 ∈ ( 1 ... 𝐽 ) ∣ 0 ≤ ( ( 𝐹 ‘ 𝐶 ) ‘ 𝑖 ) } ) → ( 𝑘 + 1 ) ≤ 𝑘 )
137	134 136	sylan2br	⊢ ( ( ∀ 𝑗 ∈ { 𝑖 ∈ ( 1 ... 𝐽 ) ∣ 0 ≤ ( ( 𝐹 ‘ 𝐶 ) ‘ 𝑖 ) } 𝑗 ≤ 𝑘 ∧ ( ( 𝑘 + 1 ) ∈ ( 1 ... 𝐽 ) ∧ 0 ≤ ( ( 𝐹 ‘ 𝐶 ) ‘ ( 𝑘 + 1 ) ) ) ) → ( 𝑘 + 1 ) ≤ 𝑘 )
138	137	expr	⊢ ( ( ∀ 𝑗 ∈ { 𝑖 ∈ ( 1 ... 𝐽 ) ∣ 0 ≤ ( ( 𝐹 ‘ 𝐶 ) ‘ 𝑖 ) } 𝑗 ≤ 𝑘 ∧ ( 𝑘 + 1 ) ∈ ( 1 ... 𝐽 ) ) → ( 0 ≤ ( ( 𝐹 ‘ 𝐶 ) ‘ ( 𝑘 + 1 ) ) → ( 𝑘 + 1 ) ≤ 𝑘 ) )
139	138	con3d	⊢ ( ( ∀ 𝑗 ∈ { 𝑖 ∈ ( 1 ... 𝐽 ) ∣ 0 ≤ ( ( 𝐹 ‘ 𝐶 ) ‘ 𝑖 ) } 𝑗 ≤ 𝑘 ∧ ( 𝑘 + 1 ) ∈ ( 1 ... 𝐽 ) ) → ( ¬ ( 𝑘 + 1 ) ≤ 𝑘 → ¬ 0 ≤ ( ( 𝐹 ‘ 𝐶 ) ‘ ( 𝑘 + 1 ) ) ) )
140	28 131 139	syl2anc	⊢ ( ( 𝜑 ∧ ( ( 𝑘 ∈ ( 1 ... 𝐽 ) ∧ 0 ≤ ( ( 𝐹 ‘ 𝐶 ) ‘ 𝑘 ) ) ∧ ∀ 𝑗 ∈ { 𝑖 ∈ ( 1 ... 𝐽 ) ∣ 0 ≤ ( ( 𝐹 ‘ 𝐶 ) ‘ 𝑖 ) } 𝑗 ≤ 𝑘 ) ) → ( ¬ ( 𝑘 + 1 ) ≤ 𝑘 → ¬ 0 ≤ ( ( 𝐹 ‘ 𝐶 ) ‘ ( 𝑘 + 1 ) ) ) )
141	27 140	mpd	⊢ ( ( 𝜑 ∧ ( ( 𝑘 ∈ ( 1 ... 𝐽 ) ∧ 0 ≤ ( ( 𝐹 ‘ 𝐶 ) ‘ 𝑘 ) ) ∧ ∀ 𝑗 ∈ { 𝑖 ∈ ( 1 ... 𝐽 ) ∣ 0 ≤ ( ( 𝐹 ‘ 𝐶 ) ‘ 𝑖 ) } 𝑗 ≤ 𝑘 ) ) → ¬ 0 ≤ ( ( 𝐹 ‘ 𝐶 ) ‘ ( 𝑘 + 1 ) ) )
142		simplrr	⊢ ( ( ( 𝜑 ∧ ( ( 𝑘 ∈ ( 1 ... 𝐽 ) ∧ 0 ≤ ( ( 𝐹 ‘ 𝐶 ) ‘ 𝑘 ) ) ∧ ∀ 𝑗 ∈ { 𝑖 ∈ ( 1 ... 𝐽 ) ∣ 0 ≤ ( ( 𝐹 ‘ 𝐶 ) ‘ 𝑖 ) } 𝑗 ≤ 𝑘 ) ) ∧ ( 𝑘 + 1 ) ∈ 𝐶 ) → ∀ 𝑗 ∈ { 𝑖 ∈ ( 1 ... 𝐽 ) ∣ 0 ≤ ( ( 𝐹 ‘ 𝐶 ) ‘ 𝑖 ) } 𝑗 ≤ 𝑘 )
143	131	adantr	⊢ ( ( ( 𝜑 ∧ ( ( 𝑘 ∈ ( 1 ... 𝐽 ) ∧ 0 ≤ ( ( 𝐹 ‘ 𝐶 ) ‘ 𝑘 ) ) ∧ ∀ 𝑗 ∈ { 𝑖 ∈ ( 1 ... 𝐽 ) ∣ 0 ≤ ( ( 𝐹 ‘ 𝐶 ) ‘ 𝑖 ) } 𝑗 ≤ 𝑘 ) ) ∧ ( 𝑘 + 1 ) ∈ 𝐶 ) → ( 𝑘 + 1 ) ∈ ( 1 ... 𝐽 ) )
144		0red	⊢ ( ( ( 𝜑 ∧ ( 𝑘 ∈ ( 1 ... 𝐽 ) ∧ 0 ≤ ( ( 𝐹 ‘ 𝐶 ) ‘ 𝑘 ) ) ) ∧ ( 𝑘 + 1 ) ∈ 𝐶 ) → 0 ∈ ℝ )
145		simpll	⊢ ( ( ( 𝜑 ∧ ( 𝑘 ∈ ( 1 ... 𝐽 ) ∧ 0 ≤ ( ( 𝐹 ‘ 𝐶 ) ‘ 𝑘 ) ) ) ∧ ( 𝑘 + 1 ) ∈ 𝐶 ) → 𝜑 )
146	130	adantr	⊢ ( ( ( 𝜑 ∧ ( 𝑘 ∈ ( 1 ... 𝐽 ) ∧ 0 ≤ ( ( 𝐹 ‘ 𝐶 ) ‘ 𝑘 ) ) ) ∧ ( 𝑘 + 1 ) ∈ 𝐶 ) → ( 𝑘 + 1 ) ∈ ( 1 ... 𝐽 ) )
147	41	sseld	⊢ ( 1 ∈ ( ℤ≥ ‘ 0 ) → ( ( 𝑘 + 1 ) ∈ ( 1 ... 𝐽 ) → ( 𝑘 + 1 ) ∈ ( 0 ... 𝐽 ) ) )
148	40 146 147	mpsyl	⊢ ( ( ( 𝜑 ∧ ( 𝑘 ∈ ( 1 ... 𝐽 ) ∧ 0 ≤ ( ( 𝐹 ‘ 𝐶 ) ‘ 𝑘 ) ) ) ∧ ( 𝑘 + 1 ) ∈ 𝐶 ) → ( 𝑘 + 1 ) ∈ ( 0 ... 𝐽 ) )
149	6	adantr	⊢ ( ( 𝜑 ∧ ( 𝑘 + 1 ) ∈ ( 0 ... 𝐽 ) ) → 𝐶 ∈ 𝑂 )
150		elfzelz	⊢ ( ( 𝑘 + 1 ) ∈ ( 0 ... 𝐽 ) → ( 𝑘 + 1 ) ∈ ℤ )
151	150	adantl	⊢ ( ( 𝜑 ∧ ( 𝑘 + 1 ) ∈ ( 0 ... 𝐽 ) ) → ( 𝑘 + 1 ) ∈ ℤ )
152	1 2 3 4 5 149 151	ballotlemfelz	⊢ ( ( 𝜑 ∧ ( 𝑘 + 1 ) ∈ ( 0 ... 𝐽 ) ) → ( ( 𝐹 ‘ 𝐶 ) ‘ ( 𝑘 + 1 ) ) ∈ ℤ )
153	152	zred	⊢ ( ( 𝜑 ∧ ( 𝑘 + 1 ) ∈ ( 0 ... 𝐽 ) ) → ( ( 𝐹 ‘ 𝐶 ) ‘ ( 𝑘 + 1 ) ) ∈ ℝ )
154	145 148 153	syl2anc	⊢ ( ( ( 𝜑 ∧ ( 𝑘 ∈ ( 1 ... 𝐽 ) ∧ 0 ≤ ( ( 𝐹 ‘ 𝐶 ) ‘ 𝑘 ) ) ) ∧ ( 𝑘 + 1 ) ∈ 𝐶 ) → ( ( 𝐹 ‘ 𝐶 ) ‘ ( 𝑘 + 1 ) ) ∈ ℝ )
155		simplrr	⊢ ( ( ( 𝜑 ∧ ( 𝑘 ∈ ( 1 ... 𝐽 ) ∧ 0 ≤ ( ( 𝐹 ‘ 𝐶 ) ‘ 𝑘 ) ) ) ∧ ( 𝑘 + 1 ) ∈ 𝐶 ) → 0 ≤ ( ( 𝐹 ‘ 𝐶 ) ‘ 𝑘 ) )
156	14	adantr	⊢ ( ( ( 𝜑 ∧ ( 𝑘 ∈ ( 1 ... 𝐽 ) ∧ 0 ≤ ( ( 𝐹 ‘ 𝐶 ) ‘ 𝑘 ) ) ) ∧ ( 𝑘 + 1 ) ∈ 𝐶 ) → 𝑘 ∈ ( 1 ... 𝐽 ) )
157	156 43	syl	⊢ ( ( ( 𝜑 ∧ ( 𝑘 ∈ ( 1 ... 𝐽 ) ∧ 0 ≤ ( ( 𝐹 ‘ 𝐶 ) ‘ 𝑘 ) ) ) ∧ ( 𝑘 + 1 ) ∈ 𝐶 ) → 𝑘 ∈ ( 0 ... 𝐽 ) )
158	129	imdistani	⊢ ( ( 𝜑 ∧ ( 𝑘 ∈ ( 1 ... 𝐽 ) ∧ 0 ≤ ( ( 𝐹 ‘ 𝐶 ) ‘ 𝑘 ) ) ) → ( 𝜑 ∧ ( 𝑘 + 1 ) ∈ ( 1 ... 𝐽 ) ) )
159	6	adantr	⊢ ( ( 𝜑 ∧ ( 𝑘 + 1 ) ∈ ( 1 ... 𝐽 ) ) → 𝐶 ∈ 𝑂 )
160		elfznn	⊢ ( ( 𝑘 + 1 ) ∈ ( 1 ... 𝐽 ) → ( 𝑘 + 1 ) ∈ ℕ )
161	160	adantl	⊢ ( ( 𝜑 ∧ ( 𝑘 + 1 ) ∈ ( 1 ... 𝐽 ) ) → ( 𝑘 + 1 ) ∈ ℕ )
162	1 2 3 4 5 159 161	ballotlemfp1	⊢ ( ( 𝜑 ∧ ( 𝑘 + 1 ) ∈ ( 1 ... 𝐽 ) ) → ( ( ¬ ( 𝑘 + 1 ) ∈ 𝐶 → ( ( 𝐹 ‘ 𝐶 ) ‘ ( 𝑘 + 1 ) ) = ( ( ( 𝐹 ‘ 𝐶 ) ‘ ( ( 𝑘 + 1 ) − 1 ) ) − 1 ) ) ∧ ( ( 𝑘 + 1 ) ∈ 𝐶 → ( ( 𝐹 ‘ 𝐶 ) ‘ ( 𝑘 + 1 ) ) = ( ( ( 𝐹 ‘ 𝐶 ) ‘ ( ( 𝑘 + 1 ) − 1 ) ) + 1 ) ) ) )
163	162	simprd	⊢ ( ( 𝜑 ∧ ( 𝑘 + 1 ) ∈ ( 1 ... 𝐽 ) ) → ( ( 𝑘 + 1 ) ∈ 𝐶 → ( ( 𝐹 ‘ 𝐶 ) ‘ ( 𝑘 + 1 ) ) = ( ( ( 𝐹 ‘ 𝐶 ) ‘ ( ( 𝑘 + 1 ) − 1 ) ) + 1 ) ) )
164	163	imp	⊢ ( ( ( 𝜑 ∧ ( 𝑘 + 1 ) ∈ ( 1 ... 𝐽 ) ) ∧ ( 𝑘 + 1 ) ∈ 𝐶 ) → ( ( 𝐹 ‘ 𝐶 ) ‘ ( 𝑘 + 1 ) ) = ( ( ( 𝐹 ‘ 𝐶 ) ‘ ( ( 𝑘 + 1 ) − 1 ) ) + 1 ) )
165	158 164	sylan	⊢ ( ( ( 𝜑 ∧ ( 𝑘 ∈ ( 1 ... 𝐽 ) ∧ 0 ≤ ( ( 𝐹 ‘ 𝐶 ) ‘ 𝑘 ) ) ) ∧ ( 𝑘 + 1 ) ∈ 𝐶 ) → ( ( 𝐹 ‘ 𝐶 ) ‘ ( 𝑘 + 1 ) ) = ( ( ( 𝐹 ‘ 𝐶 ) ‘ ( ( 𝑘 + 1 ) − 1 ) ) + 1 ) )
166		elfzelz	⊢ ( 𝑘 ∈ ( 1 ... 𝐽 ) → 𝑘 ∈ ℤ )
167	166	zcnd	⊢ ( 𝑘 ∈ ( 1 ... 𝐽 ) → 𝑘 ∈ ℂ )
168		1cnd	⊢ ( 𝑘 ∈ ( 1 ... 𝐽 ) → 1 ∈ ℂ )
169	167 168	pncand	⊢ ( 𝑘 ∈ ( 1 ... 𝐽 ) → ( ( 𝑘 + 1 ) − 1 ) = 𝑘 )
170	169	fveq2d	⊢ ( 𝑘 ∈ ( 1 ... 𝐽 ) → ( ( 𝐹 ‘ 𝐶 ) ‘ ( ( 𝑘 + 1 ) − 1 ) ) = ( ( 𝐹 ‘ 𝐶 ) ‘ 𝑘 ) )
171	170	oveq1d	⊢ ( 𝑘 ∈ ( 1 ... 𝐽 ) → ( ( ( 𝐹 ‘ 𝐶 ) ‘ ( ( 𝑘 + 1 ) − 1 ) ) + 1 ) = ( ( ( 𝐹 ‘ 𝐶 ) ‘ 𝑘 ) + 1 ) )
172	171	eqeq2d	⊢ ( 𝑘 ∈ ( 1 ... 𝐽 ) → ( ( ( 𝐹 ‘ 𝐶 ) ‘ ( 𝑘 + 1 ) ) = ( ( ( 𝐹 ‘ 𝐶 ) ‘ ( ( 𝑘 + 1 ) − 1 ) ) + 1 ) ↔ ( ( 𝐹 ‘ 𝐶 ) ‘ ( 𝑘 + 1 ) ) = ( ( ( 𝐹 ‘ 𝐶 ) ‘ 𝑘 ) + 1 ) ) )
173	156 172	syl	⊢ ( ( ( 𝜑 ∧ ( 𝑘 ∈ ( 1 ... 𝐽 ) ∧ 0 ≤ ( ( 𝐹 ‘ 𝐶 ) ‘ 𝑘 ) ) ) ∧ ( 𝑘 + 1 ) ∈ 𝐶 ) → ( ( ( 𝐹 ‘ 𝐶 ) ‘ ( 𝑘 + 1 ) ) = ( ( ( 𝐹 ‘ 𝐶 ) ‘ ( ( 𝑘 + 1 ) − 1 ) ) + 1 ) ↔ ( ( 𝐹 ‘ 𝐶 ) ‘ ( 𝑘 + 1 ) ) = ( ( ( 𝐹 ‘ 𝐶 ) ‘ 𝑘 ) + 1 ) ) )
174	165 173	mpbid	⊢ ( ( ( 𝜑 ∧ ( 𝑘 ∈ ( 1 ... 𝐽 ) ∧ 0 ≤ ( ( 𝐹 ‘ 𝐶 ) ‘ 𝑘 ) ) ) ∧ ( 𝑘 + 1 ) ∈ 𝐶 ) → ( ( 𝐹 ‘ 𝐶 ) ‘ ( 𝑘 + 1 ) ) = ( ( ( 𝐹 ‘ 𝐶 ) ‘ 𝑘 ) + 1 ) )
175		0z	⊢ 0 ∈ ℤ
176		zleltp1	⊢ ( ( 0 ∈ ℤ ∧ ( ( 𝐹 ‘ 𝐶 ) ‘ 𝑘 ) ∈ ℤ ) → ( 0 ≤ ( ( 𝐹 ‘ 𝐶 ) ‘ 𝑘 ) ↔ 0 < ( ( ( 𝐹 ‘ 𝐶 ) ‘ 𝑘 ) + 1 ) ) )
177	175 47 176	sylancr	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... 𝐽 ) ) → ( 0 ≤ ( ( 𝐹 ‘ 𝐶 ) ‘ 𝑘 ) ↔ 0 < ( ( ( 𝐹 ‘ 𝐶 ) ‘ 𝑘 ) + 1 ) ) )
178	177	adantr	⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... 𝐽 ) ) ∧ ( ( 𝐹 ‘ 𝐶 ) ‘ ( 𝑘 + 1 ) ) = ( ( ( 𝐹 ‘ 𝐶 ) ‘ 𝑘 ) + 1 ) ) → ( 0 ≤ ( ( 𝐹 ‘ 𝐶 ) ‘ 𝑘 ) ↔ 0 < ( ( ( 𝐹 ‘ 𝐶 ) ‘ 𝑘 ) + 1 ) ) )
179		breq2	⊢ ( ( ( 𝐹 ‘ 𝐶 ) ‘ ( 𝑘 + 1 ) ) = ( ( ( 𝐹 ‘ 𝐶 ) ‘ 𝑘 ) + 1 ) → ( 0 < ( ( 𝐹 ‘ 𝐶 ) ‘ ( 𝑘 + 1 ) ) ↔ 0 < ( ( ( 𝐹 ‘ 𝐶 ) ‘ 𝑘 ) + 1 ) ) )
180	179	adantl	⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... 𝐽 ) ) ∧ ( ( 𝐹 ‘ 𝐶 ) ‘ ( 𝑘 + 1 ) ) = ( ( ( 𝐹 ‘ 𝐶 ) ‘ 𝑘 ) + 1 ) ) → ( 0 < ( ( 𝐹 ‘ 𝐶 ) ‘ ( 𝑘 + 1 ) ) ↔ 0 < ( ( ( 𝐹 ‘ 𝐶 ) ‘ 𝑘 ) + 1 ) ) )
181	178 180	bitr4d	⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... 𝐽 ) ) ∧ ( ( 𝐹 ‘ 𝐶 ) ‘ ( 𝑘 + 1 ) ) = ( ( ( 𝐹 ‘ 𝐶 ) ‘ 𝑘 ) + 1 ) ) → ( 0 ≤ ( ( 𝐹 ‘ 𝐶 ) ‘ 𝑘 ) ↔ 0 < ( ( 𝐹 ‘ 𝐶 ) ‘ ( 𝑘 + 1 ) ) ) )
182	145 157 174 181	syl21anc	⊢ ( ( ( 𝜑 ∧ ( 𝑘 ∈ ( 1 ... 𝐽 ) ∧ 0 ≤ ( ( 𝐹 ‘ 𝐶 ) ‘ 𝑘 ) ) ) ∧ ( 𝑘 + 1 ) ∈ 𝐶 ) → ( 0 ≤ ( ( 𝐹 ‘ 𝐶 ) ‘ 𝑘 ) ↔ 0 < ( ( 𝐹 ‘ 𝐶 ) ‘ ( 𝑘 + 1 ) ) ) )
183	155 182	mpbid	⊢ ( ( ( 𝜑 ∧ ( 𝑘 ∈ ( 1 ... 𝐽 ) ∧ 0 ≤ ( ( 𝐹 ‘ 𝐶 ) ‘ 𝑘 ) ) ) ∧ ( 𝑘 + 1 ) ∈ 𝐶 ) → 0 < ( ( 𝐹 ‘ 𝐶 ) ‘ ( 𝑘 + 1 ) ) )
184	144 154 183	ltled	⊢ ( ( ( 𝜑 ∧ ( 𝑘 ∈ ( 1 ... 𝐽 ) ∧ 0 ≤ ( ( 𝐹 ‘ 𝐶 ) ‘ 𝑘 ) ) ) ∧ ( 𝑘 + 1 ) ∈ 𝐶 ) → 0 ≤ ( ( 𝐹 ‘ 𝐶 ) ‘ ( 𝑘 + 1 ) ) )
185	184	adantlrr	⊢ ( ( ( 𝜑 ∧ ( ( 𝑘 ∈ ( 1 ... 𝐽 ) ∧ 0 ≤ ( ( 𝐹 ‘ 𝐶 ) ‘ 𝑘 ) ) ∧ ∀ 𝑗 ∈ { 𝑖 ∈ ( 1 ... 𝐽 ) ∣ 0 ≤ ( ( 𝐹 ‘ 𝐶 ) ‘ 𝑖 ) } 𝑗 ≤ 𝑘 ) ) ∧ ( 𝑘 + 1 ) ∈ 𝐶 ) → 0 ≤ ( ( 𝐹 ‘ 𝐶 ) ‘ ( 𝑘 + 1 ) ) )
186	142 143 185 137	syl12anc	⊢ ( ( ( 𝜑 ∧ ( ( 𝑘 ∈ ( 1 ... 𝐽 ) ∧ 0 ≤ ( ( 𝐹 ‘ 𝐶 ) ‘ 𝑘 ) ) ∧ ∀ 𝑗 ∈ { 𝑖 ∈ ( 1 ... 𝐽 ) ∣ 0 ≤ ( ( 𝐹 ‘ 𝐶 ) ‘ 𝑖 ) } 𝑗 ≤ 𝑘 ) ) ∧ ( 𝑘 + 1 ) ∈ 𝐶 ) → ( 𝑘 + 1 ) ≤ 𝑘 )
187	27 186	mtand	⊢ ( ( 𝜑 ∧ ( ( 𝑘 ∈ ( 1 ... 𝐽 ) ∧ 0 ≤ ( ( 𝐹 ‘ 𝐶 ) ‘ 𝑘 ) ) ∧ ∀ 𝑗 ∈ { 𝑖 ∈ ( 1 ... 𝐽 ) ∣ 0 ≤ ( ( 𝐹 ‘ 𝐶 ) ‘ 𝑖 ) } 𝑗 ≤ 𝑘 ) ) → ¬ ( 𝑘 + 1 ) ∈ 𝐶 )
188	162	simpld	⊢ ( ( 𝜑 ∧ ( 𝑘 + 1 ) ∈ ( 1 ... 𝐽 ) ) → ( ¬ ( 𝑘 + 1 ) ∈ 𝐶 → ( ( 𝐹 ‘ 𝐶 ) ‘ ( 𝑘 + 1 ) ) = ( ( ( 𝐹 ‘ 𝐶 ) ‘ ( ( 𝑘 + 1 ) − 1 ) ) − 1 ) ) )
189	188	imp	⊢ ( ( ( 𝜑 ∧ ( 𝑘 + 1 ) ∈ ( 1 ... 𝐽 ) ) ∧ ¬ ( 𝑘 + 1 ) ∈ 𝐶 ) → ( ( 𝐹 ‘ 𝐶 ) ‘ ( 𝑘 + 1 ) ) = ( ( ( 𝐹 ‘ 𝐶 ) ‘ ( ( 𝑘 + 1 ) − 1 ) ) − 1 ) )
190	158 189	sylan	⊢ ( ( ( 𝜑 ∧ ( 𝑘 ∈ ( 1 ... 𝐽 ) ∧ 0 ≤ ( ( 𝐹 ‘ 𝐶 ) ‘ 𝑘 ) ) ) ∧ ¬ ( 𝑘 + 1 ) ∈ 𝐶 ) → ( ( 𝐹 ‘ 𝐶 ) ‘ ( 𝑘 + 1 ) ) = ( ( ( 𝐹 ‘ 𝐶 ) ‘ ( ( 𝑘 + 1 ) − 1 ) ) − 1 ) )
191	14	adantr	⊢ ( ( ( 𝜑 ∧ ( 𝑘 ∈ ( 1 ... 𝐽 ) ∧ 0 ≤ ( ( 𝐹 ‘ 𝐶 ) ‘ 𝑘 ) ) ) ∧ ¬ ( 𝑘 + 1 ) ∈ 𝐶 ) → 𝑘 ∈ ( 1 ... 𝐽 ) )
192	170	oveq1d	⊢ ( 𝑘 ∈ ( 1 ... 𝐽 ) → ( ( ( 𝐹 ‘ 𝐶 ) ‘ ( ( 𝑘 + 1 ) − 1 ) ) − 1 ) = ( ( ( 𝐹 ‘ 𝐶 ) ‘ 𝑘 ) − 1 ) )
193	192	eqeq2d	⊢ ( 𝑘 ∈ ( 1 ... 𝐽 ) → ( ( ( 𝐹 ‘ 𝐶 ) ‘ ( 𝑘 + 1 ) ) = ( ( ( 𝐹 ‘ 𝐶 ) ‘ ( ( 𝑘 + 1 ) − 1 ) ) − 1 ) ↔ ( ( 𝐹 ‘ 𝐶 ) ‘ ( 𝑘 + 1 ) ) = ( ( ( 𝐹 ‘ 𝐶 ) ‘ 𝑘 ) − 1 ) ) )
194	191 193	syl	⊢ ( ( ( 𝜑 ∧ ( 𝑘 ∈ ( 1 ... 𝐽 ) ∧ 0 ≤ ( ( 𝐹 ‘ 𝐶 ) ‘ 𝑘 ) ) ) ∧ ¬ ( 𝑘 + 1 ) ∈ 𝐶 ) → ( ( ( 𝐹 ‘ 𝐶 ) ‘ ( 𝑘 + 1 ) ) = ( ( ( 𝐹 ‘ 𝐶 ) ‘ ( ( 𝑘 + 1 ) − 1 ) ) − 1 ) ↔ ( ( 𝐹 ‘ 𝐶 ) ‘ ( 𝑘 + 1 ) ) = ( ( ( 𝐹 ‘ 𝐶 ) ‘ 𝑘 ) − 1 ) ) )
195	190 194	mpbid	⊢ ( ( ( 𝜑 ∧ ( 𝑘 ∈ ( 1 ... 𝐽 ) ∧ 0 ≤ ( ( 𝐹 ‘ 𝐶 ) ‘ 𝑘 ) ) ) ∧ ¬ ( 𝑘 + 1 ) ∈ 𝐶 ) → ( ( 𝐹 ‘ 𝐶 ) ‘ ( 𝑘 + 1 ) ) = ( ( ( 𝐹 ‘ 𝐶 ) ‘ 𝑘 ) − 1 ) )
196	195	adantlrr	⊢ ( ( ( 𝜑 ∧ ( ( 𝑘 ∈ ( 1 ... 𝐽 ) ∧ 0 ≤ ( ( 𝐹 ‘ 𝐶 ) ‘ 𝑘 ) ) ∧ ∀ 𝑗 ∈ { 𝑖 ∈ ( 1 ... 𝐽 ) ∣ 0 ≤ ( ( 𝐹 ‘ 𝐶 ) ‘ 𝑖 ) } 𝑗 ≤ 𝑘 ) ) ∧ ¬ ( 𝑘 + 1 ) ∈ 𝐶 ) → ( ( 𝐹 ‘ 𝐶 ) ‘ ( 𝑘 + 1 ) ) = ( ( ( 𝐹 ‘ 𝐶 ) ‘ 𝑘 ) − 1 ) )
197	187 196	mpdan	⊢ ( ( 𝜑 ∧ ( ( 𝑘 ∈ ( 1 ... 𝐽 ) ∧ 0 ≤ ( ( 𝐹 ‘ 𝐶 ) ‘ 𝑘 ) ) ∧ ∀ 𝑗 ∈ { 𝑖 ∈ ( 1 ... 𝐽 ) ∣ 0 ≤ ( ( 𝐹 ‘ 𝐶 ) ‘ 𝑖 ) } 𝑗 ≤ 𝑘 ) ) → ( ( 𝐹 ‘ 𝐶 ) ‘ ( 𝑘 + 1 ) ) = ( ( ( 𝐹 ‘ 𝐶 ) ‘ 𝑘 ) − 1 ) )
198		breq2	⊢ ( ( ( 𝐹 ‘ 𝐶 ) ‘ ( 𝑘 + 1 ) ) = ( ( ( 𝐹 ‘ 𝐶 ) ‘ 𝑘 ) − 1 ) → ( 0 ≤ ( ( 𝐹 ‘ 𝐶 ) ‘ ( 𝑘 + 1 ) ) ↔ 0 ≤ ( ( ( 𝐹 ‘ 𝐶 ) ‘ 𝑘 ) − 1 ) ) )
199	198	notbid	⊢ ( ( ( 𝐹 ‘ 𝐶 ) ‘ ( 𝑘 + 1 ) ) = ( ( ( 𝐹 ‘ 𝐶 ) ‘ 𝑘 ) − 1 ) → ( ¬ 0 ≤ ( ( 𝐹 ‘ 𝐶 ) ‘ ( 𝑘 + 1 ) ) ↔ ¬ 0 ≤ ( ( ( 𝐹 ‘ 𝐶 ) ‘ 𝑘 ) − 1 ) ) )
200	197 199	syl	⊢ ( ( 𝜑 ∧ ( ( 𝑘 ∈ ( 1 ... 𝐽 ) ∧ 0 ≤ ( ( 𝐹 ‘ 𝐶 ) ‘ 𝑘 ) ) ∧ ∀ 𝑗 ∈ { 𝑖 ∈ ( 1 ... 𝐽 ) ∣ 0 ≤ ( ( 𝐹 ‘ 𝐶 ) ‘ 𝑖 ) } 𝑗 ≤ 𝑘 ) ) → ( ¬ 0 ≤ ( ( 𝐹 ‘ 𝐶 ) ‘ ( 𝑘 + 1 ) ) ↔ ¬ 0 ≤ ( ( ( 𝐹 ‘ 𝐶 ) ‘ 𝑘 ) − 1 ) ) )
201	141 200	mpbid	⊢ ( ( 𝜑 ∧ ( ( 𝑘 ∈ ( 1 ... 𝐽 ) ∧ 0 ≤ ( ( 𝐹 ‘ 𝐶 ) ‘ 𝑘 ) ) ∧ ∀ 𝑗 ∈ { 𝑖 ∈ ( 1 ... 𝐽 ) ∣ 0 ≤ ( ( 𝐹 ‘ 𝐶 ) ‘ 𝑖 ) } 𝑗 ≤ 𝑘 ) ) → ¬ 0 ≤ ( ( ( 𝐹 ‘ 𝐶 ) ‘ 𝑘 ) − 1 ) )
202	14 43	syl	⊢ ( ( 𝜑 ∧ ( 𝑘 ∈ ( 1 ... 𝐽 ) ∧ 0 ≤ ( ( 𝐹 ‘ 𝐶 ) ‘ 𝑘 ) ) ) → 𝑘 ∈ ( 0 ... 𝐽 ) )
203	202 47	syldan	⊢ ( ( 𝜑 ∧ ( 𝑘 ∈ ( 1 ... 𝐽 ) ∧ 0 ≤ ( ( 𝐹 ‘ 𝐶 ) ‘ 𝑘 ) ) ) → ( ( 𝐹 ‘ 𝐶 ) ‘ 𝑘 ) ∈ ℤ )
204	203	adantrr	⊢ ( ( 𝜑 ∧ ( ( 𝑘 ∈ ( 1 ... 𝐽 ) ∧ 0 ≤ ( ( 𝐹 ‘ 𝐶 ) ‘ 𝑘 ) ) ∧ ∀ 𝑗 ∈ { 𝑖 ∈ ( 1 ... 𝐽 ) ∣ 0 ≤ ( ( 𝐹 ‘ 𝐶 ) ‘ 𝑖 ) } 𝑗 ≤ 𝑘 ) ) → ( ( 𝐹 ‘ 𝐶 ) ‘ 𝑘 ) ∈ ℤ )
205		zlem1lt	⊢ ( ( ( ( 𝐹 ‘ 𝐶 ) ‘ 𝑘 ) ∈ ℤ ∧ 0 ∈ ℤ ) → ( ( ( 𝐹 ‘ 𝐶 ) ‘ 𝑘 ) ≤ 0 ↔ ( ( ( 𝐹 ‘ 𝐶 ) ‘ 𝑘 ) − 1 ) < 0 ) )
206	175 205	mpan2	⊢ ( ( ( 𝐹 ‘ 𝐶 ) ‘ 𝑘 ) ∈ ℤ → ( ( ( 𝐹 ‘ 𝐶 ) ‘ 𝑘 ) ≤ 0 ↔ ( ( ( 𝐹 ‘ 𝐶 ) ‘ 𝑘 ) − 1 ) < 0 ) )
207		zre	⊢ ( ( ( 𝐹 ‘ 𝐶 ) ‘ 𝑘 ) ∈ ℤ → ( ( 𝐹 ‘ 𝐶 ) ‘ 𝑘 ) ∈ ℝ )
208		1red	⊢ ( ( ( 𝐹 ‘ 𝐶 ) ‘ 𝑘 ) ∈ ℤ → 1 ∈ ℝ )
209	207 208	resubcld	⊢ ( ( ( 𝐹 ‘ 𝐶 ) ‘ 𝑘 ) ∈ ℤ → ( ( ( 𝐹 ‘ 𝐶 ) ‘ 𝑘 ) − 1 ) ∈ ℝ )
210		0red	⊢ ( ( ( 𝐹 ‘ 𝐶 ) ‘ 𝑘 ) ∈ ℤ → 0 ∈ ℝ )
211	209 210	ltnled	⊢ ( ( ( 𝐹 ‘ 𝐶 ) ‘ 𝑘 ) ∈ ℤ → ( ( ( ( 𝐹 ‘ 𝐶 ) ‘ 𝑘 ) − 1 ) < 0 ↔ ¬ 0 ≤ ( ( ( 𝐹 ‘ 𝐶 ) ‘ 𝑘 ) − 1 ) ) )
212	206 211	bitrd	⊢ ( ( ( 𝐹 ‘ 𝐶 ) ‘ 𝑘 ) ∈ ℤ → ( ( ( 𝐹 ‘ 𝐶 ) ‘ 𝑘 ) ≤ 0 ↔ ¬ 0 ≤ ( ( ( 𝐹 ‘ 𝐶 ) ‘ 𝑘 ) − 1 ) ) )
213	204 212	syl	⊢ ( ( 𝜑 ∧ ( ( 𝑘 ∈ ( 1 ... 𝐽 ) ∧ 0 ≤ ( ( 𝐹 ‘ 𝐶 ) ‘ 𝑘 ) ) ∧ ∀ 𝑗 ∈ { 𝑖 ∈ ( 1 ... 𝐽 ) ∣ 0 ≤ ( ( 𝐹 ‘ 𝐶 ) ‘ 𝑖 ) } 𝑗 ≤ 𝑘 ) ) → ( ( ( 𝐹 ‘ 𝐶 ) ‘ 𝑘 ) ≤ 0 ↔ ¬ 0 ≤ ( ( ( 𝐹 ‘ 𝐶 ) ‘ 𝑘 ) − 1 ) ) )
214	201 213	mpbird	⊢ ( ( 𝜑 ∧ ( ( 𝑘 ∈ ( 1 ... 𝐽 ) ∧ 0 ≤ ( ( 𝐹 ‘ 𝐶 ) ‘ 𝑘 ) ) ∧ ∀ 𝑗 ∈ { 𝑖 ∈ ( 1 ... 𝐽 ) ∣ 0 ≤ ( ( 𝐹 ‘ 𝐶 ) ‘ 𝑖 ) } 𝑗 ≤ 𝑘 ) ) → ( ( 𝐹 ‘ 𝐶 ) ‘ 𝑘 ) ≤ 0 )
215		simprlr	⊢ ( ( 𝜑 ∧ ( ( 𝑘 ∈ ( 1 ... 𝐽 ) ∧ 0 ≤ ( ( 𝐹 ‘ 𝐶 ) ‘ 𝑘 ) ) ∧ ∀ 𝑗 ∈ { 𝑖 ∈ ( 1 ... 𝐽 ) ∣ 0 ≤ ( ( 𝐹 ‘ 𝐶 ) ‘ 𝑖 ) } 𝑗 ≤ 𝑘 ) ) → 0 ≤ ( ( 𝐹 ‘ 𝐶 ) ‘ 𝑘 ) )
216	204	zred	⊢ ( ( 𝜑 ∧ ( ( 𝑘 ∈ ( 1 ... 𝐽 ) ∧ 0 ≤ ( ( 𝐹 ‘ 𝐶 ) ‘ 𝑘 ) ) ∧ ∀ 𝑗 ∈ { 𝑖 ∈ ( 1 ... 𝐽 ) ∣ 0 ≤ ( ( 𝐹 ‘ 𝐶 ) ‘ 𝑖 ) } 𝑗 ≤ 𝑘 ) ) → ( ( 𝐹 ‘ 𝐶 ) ‘ 𝑘 ) ∈ ℝ )
217		0red	⊢ ( ( 𝜑 ∧ ( ( 𝑘 ∈ ( 1 ... 𝐽 ) ∧ 0 ≤ ( ( 𝐹 ‘ 𝐶 ) ‘ 𝑘 ) ) ∧ ∀ 𝑗 ∈ { 𝑖 ∈ ( 1 ... 𝐽 ) ∣ 0 ≤ ( ( 𝐹 ‘ 𝐶 ) ‘ 𝑖 ) } 𝑗 ≤ 𝑘 ) ) → 0 ∈ ℝ )
218	216 217	letri3d	⊢ ( ( 𝜑 ∧ ( ( 𝑘 ∈ ( 1 ... 𝐽 ) ∧ 0 ≤ ( ( 𝐹 ‘ 𝐶 ) ‘ 𝑘 ) ) ∧ ∀ 𝑗 ∈ { 𝑖 ∈ ( 1 ... 𝐽 ) ∣ 0 ≤ ( ( 𝐹 ‘ 𝐶 ) ‘ 𝑖 ) } 𝑗 ≤ 𝑘 ) ) → ( ( ( 𝐹 ‘ 𝐶 ) ‘ 𝑘 ) = 0 ↔ ( ( ( 𝐹 ‘ 𝐶 ) ‘ 𝑘 ) ≤ 0 ∧ 0 ≤ ( ( 𝐹 ‘ 𝐶 ) ‘ 𝑘 ) ) ) )
219	214 215 218	mpbir2and	⊢ ( ( 𝜑 ∧ ( ( 𝑘 ∈ ( 1 ... 𝐽 ) ∧ 0 ≤ ( ( 𝐹 ‘ 𝐶 ) ‘ 𝑘 ) ) ∧ ∀ 𝑗 ∈ { 𝑖 ∈ ( 1 ... 𝐽 ) ∣ 0 ≤ ( ( 𝐹 ‘ 𝐶 ) ‘ 𝑖 ) } 𝑗 ≤ 𝑘 ) ) → ( ( 𝐹 ‘ 𝐶 ) ‘ 𝑘 ) = 0 )
220	13 219	sylan2b	⊢ ( ( 𝜑 ∧ ( 𝑘 ∈ { 𝑖 ∈ ( 1 ... 𝐽 ) ∣ 0 ≤ ( ( 𝐹 ‘ 𝐶 ) ‘ 𝑖 ) } ∧ ∀ 𝑗 ∈ { 𝑖 ∈ ( 1 ... 𝐽 ) ∣ 0 ≤ ( ( 𝐹 ‘ 𝐶 ) ‘ 𝑖 ) } 𝑗 ≤ 𝑘 ) ) → ( ( 𝐹 ‘ 𝐶 ) ‘ 𝑘 ) = 0 )
221		ssrab2	⊢ { 𝑖 ∈ ( 1 ... 𝐽 ) ∣ 0 ≤ ( ( 𝐹 ‘ 𝐶 ) ‘ 𝑖 ) } ⊆ ( 1 ... 𝐽 )
222	221 20	sstri	⊢ { 𝑖 ∈ ( 1 ... 𝐽 ) ∣ 0 ≤ ( ( 𝐹 ‘ 𝐶 ) ‘ 𝑖 ) } ⊆ ℝ
223	222	a1i	⊢ ( 𝜑 → { 𝑖 ∈ ( 1 ... 𝐽 ) ∣ 0 ≤ ( ( 𝐹 ‘ 𝐶 ) ‘ 𝑖 ) } ⊆ ℝ )
224		fzfi	⊢ ( 1 ... 𝐽 ) ∈ Fin
225		ssfi	⊢ ( ( ( 1 ... 𝐽 ) ∈ Fin ∧ { 𝑖 ∈ ( 1 ... 𝐽 ) ∣ 0 ≤ ( ( 𝐹 ‘ 𝐶 ) ‘ 𝑖 ) } ⊆ ( 1 ... 𝐽 ) ) → { 𝑖 ∈ ( 1 ... 𝐽 ) ∣ 0 ≤ ( ( 𝐹 ‘ 𝐶 ) ‘ 𝑖 ) } ∈ Fin )
226	224 221 225	mp2an	⊢ { 𝑖 ∈ ( 1 ... 𝐽 ) ∣ 0 ≤ ( ( 𝐹 ‘ 𝐶 ) ‘ 𝑖 ) } ∈ Fin
227	226	a1i	⊢ ( 𝜑 → { 𝑖 ∈ ( 1 ... 𝐽 ) ∣ 0 ≤ ( ( 𝐹 ‘ 𝐶 ) ‘ 𝑖 ) } ∈ Fin )
228		rabn0	⊢ ( { 𝑖 ∈ ( 1 ... 𝐽 ) ∣ 0 ≤ ( ( 𝐹 ‘ 𝐶 ) ‘ 𝑖 ) } ≠ ∅ ↔ ∃ 𝑖 ∈ ( 1 ... 𝐽 ) 0 ≤ ( ( 𝐹 ‘ 𝐶 ) ‘ 𝑖 ) )
229	8 228	sylibr	⊢ ( 𝜑 → { 𝑖 ∈ ( 1 ... 𝐽 ) ∣ 0 ≤ ( ( 𝐹 ‘ 𝐶 ) ‘ 𝑖 ) } ≠ ∅ )
230		fimaxre	⊢ ( ( { 𝑖 ∈ ( 1 ... 𝐽 ) ∣ 0 ≤ ( ( 𝐹 ‘ 𝐶 ) ‘ 𝑖 ) } ⊆ ℝ ∧ { 𝑖 ∈ ( 1 ... 𝐽 ) ∣ 0 ≤ ( ( 𝐹 ‘ 𝐶 ) ‘ 𝑖 ) } ∈ Fin ∧ { 𝑖 ∈ ( 1 ... 𝐽 ) ∣ 0 ≤ ( ( 𝐹 ‘ 𝐶 ) ‘ 𝑖 ) } ≠ ∅ ) → ∃ 𝑘 ∈ { 𝑖 ∈ ( 1 ... 𝐽 ) ∣ 0 ≤ ( ( 𝐹 ‘ 𝐶 ) ‘ 𝑖 ) } ∀ 𝑗 ∈ { 𝑖 ∈ ( 1 ... 𝐽 ) ∣ 0 ≤ ( ( 𝐹 ‘ 𝐶 ) ‘ 𝑖 ) } 𝑗 ≤ 𝑘 )
231	223 227 229 230	syl3anc	⊢ ( 𝜑 → ∃ 𝑘 ∈ { 𝑖 ∈ ( 1 ... 𝐽 ) ∣ 0 ≤ ( ( 𝐹 ‘ 𝐶 ) ‘ 𝑖 ) } ∀ 𝑗 ∈ { 𝑖 ∈ ( 1 ... 𝐽 ) ∣ 0 ≤ ( ( 𝐹 ‘ 𝐶 ) ‘ 𝑖 ) } 𝑗 ≤ 𝑘 )
232	220 231	reximddv	⊢ ( 𝜑 → ∃ 𝑘 ∈ { 𝑖 ∈ ( 1 ... 𝐽 ) ∣ 0 ≤ ( ( 𝐹 ‘ 𝐶 ) ‘ 𝑖 ) } ( ( 𝐹 ‘ 𝐶 ) ‘ 𝑘 ) = 0 )
233		elrabi	⊢ ( 𝑘 ∈ { 𝑖 ∈ ( 1 ... 𝐽 ) ∣ 0 ≤ ( ( 𝐹 ‘ 𝐶 ) ‘ 𝑖 ) } → 𝑘 ∈ ( 1 ... 𝐽 ) )
234	233	anim1i	⊢ ( ( 𝑘 ∈ { 𝑖 ∈ ( 1 ... 𝐽 ) ∣ 0 ≤ ( ( 𝐹 ‘ 𝐶 ) ‘ 𝑖 ) } ∧ ( ( 𝐹 ‘ 𝐶 ) ‘ 𝑘 ) = 0 ) → ( 𝑘 ∈ ( 1 ... 𝐽 ) ∧ ( ( 𝐹 ‘ 𝐶 ) ‘ 𝑘 ) = 0 ) )
235	234	reximi2	⊢ ( ∃ 𝑘 ∈ { 𝑖 ∈ ( 1 ... 𝐽 ) ∣ 0 ≤ ( ( 𝐹 ‘ 𝐶 ) ‘ 𝑖 ) } ( ( 𝐹 ‘ 𝐶 ) ‘ 𝑘 ) = 0 → ∃ 𝑘 ∈ ( 1 ... 𝐽 ) ( ( 𝐹 ‘ 𝐶 ) ‘ 𝑘 ) = 0 )
236	232 235	syl	⊢ ( 𝜑 → ∃ 𝑘 ∈ ( 1 ... 𝐽 ) ( ( 𝐹 ‘ 𝐶 ) ‘ 𝑘 ) = 0 )