Metamath Proof Explorer

Theorem ballotlemfc0

Description: F takes value 0 between negative and positive values. (Contributed by Thierry Arnoux, 24-Nov-2016)

Ref Expression
Hypotheses 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 ballotlemfc0 ( 𝜑 → ∃ 𝑘 ∈ ( 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 ballotlemfp1.c ⊢ ( 𝜑 → 𝐶 ∈ 𝑂 )
7 ballotlemfp1.j ⊢ ( 𝜑 → 𝐽 ∈ ℕ )
8 ballotlemfc0.3 ⊢ ( 𝜑 → ∃ 𝑖 ∈ ( 1 ... 𝐽 ) ( ( 𝐹 ‘ 𝐶 ) ‘ 𝑖 ) ≤ 0 )
9 ballotlemfc0.4 ⊢ ( 𝜑 → 0 < ( ( 𝐹 ‘ 𝐶 ) ‘ 𝐽 ) )
10 fveq2 ⊢ ( 𝑖 = 𝑘 → ( ( 𝐹 ‘ 𝐶 ) ‘ 𝑖 ) = ( ( 𝐹 ‘ 𝐶 ) ‘ 𝑘 ) )
11 10 breq1d ⊢ ( 𝑖 = 𝑘 → ( ( ( 𝐹 ‘ 𝐶 ) ‘ 𝑖 ) ≤ 0 ↔ ( ( 𝐹 ‘ 𝐶 ) ‘ 𝑘 ) ≤ 0 ) )
12 11 elrab ⊢ ( 𝑘 ∈ { 𝑖 ∈ ( 1 ... 𝐽 ) ∣ ( ( 𝐹 ‘ 𝐶 ) ‘ 𝑖 ) ≤ 0 } ↔ ( 𝑘 ∈ ( 1 ... 𝐽 ) ∧ ( ( 𝐹 ‘ 𝐶 ) ‘ 𝑘 ) ≤ 0 ) )
13 12 anbi1i ⊢ ( ( 𝑘 ∈ { 𝑖 ∈ ( 1 ... 𝐽 ) ∣ ( ( 𝐹 ‘ 𝐶 ) ‘ 𝑖 ) ≤ 0 } ∧ ∀ 𝑗 ∈ { 𝑖 ∈ ( 1 ... 𝐽 ) ∣ ( ( 𝐹 ‘ 𝐶 ) ‘ 𝑖 ) ≤ 0 } 𝑗 ≤ 𝑘 ) ↔ ( ( 𝑘 ∈ ( 1 ... 𝐽 ) ∧ ( ( 𝐹 ‘ 𝐶 ) ‘ 𝑘 ) ≤ 0 ) ∧ ∀ 𝑗 ∈ { 𝑖 ∈ ( 1 ... 𝐽 ) ∣ ( ( 𝐹 ‘ 𝐶 ) ‘ 𝑖 ) ≤ 0 } 𝑗 ≤ 𝑘 ) )
14 simprlr ⊢ ( ( 𝜑 ∧ ( ( 𝑘 ∈ ( 1 ... 𝐽 ) ∧ ( ( 𝐹 ‘ 𝐶 ) ‘ 𝑘 ) ≤ 0 ) ∧ ∀ 𝑗 ∈ { 𝑖 ∈ ( 1 ... 𝐽 ) ∣ ( ( 𝐹 ‘ 𝐶 ) ‘ 𝑖 ) ≤ 0 } 𝑗 ≤ 𝑘 ) ) → ( ( 𝐹 ‘ 𝐶 ) ‘ 𝑘 ) ≤ 0 )
15 simprl ⊢ ( ( 𝜑 ∧ ( 𝑘 ∈ ( 1 ... 𝐽 ) ∧ ( ( 𝐹 ‘ 𝐶 ) ‘ 𝑘 ) ≤ 0 ) ) → 𝑘 ∈ ( 1 ... 𝐽 ) )
16 15 adantrr ⊢ ( ( 𝜑 ∧ ( ( 𝑘 ∈ ( 1 ... 𝐽 ) ∧ ( ( 𝐹 ‘ 𝐶 ) ‘ 𝑘 ) ≤ 0 ) ∧ ∀ 𝑗 ∈ { 𝑖 ∈ ( 1 ... 𝐽 ) ∣ ( ( 𝐹 ‘ 𝐶 ) ‘ 𝑖 ) ≤ 0 } 𝑗 ≤ 𝑘 ) ) → 𝑘 ∈ ( 1 ... 𝐽 ) )
17 fzssuz ⊢ ( 1 ... 𝐽 ) ⊆ ( ℤ≥ ‘ 1 )
18 uzssz ⊢ ( ℤ≥ ‘ 1 ) ⊆ ℤ
19 17 18 sstri ⊢ ( 1 ... 𝐽 ) ⊆ ℤ
20 zssre ⊢ ℤ ⊆ ℝ
21 19 20 sstri ⊢ ( 1 ... 𝐽 ) ⊆ ℝ
22 21 sseli ⊢ ( 𝑘 ∈ ( 1 ... 𝐽 ) → 𝑘 ∈ ℝ )
23 22 ltp1d ⊢ ( 𝑘 ∈ ( 1 ... 𝐽 ) → 𝑘 < ( 𝑘 + 1 ) )
24 1red ⊢ ( 𝑘 ∈ ( 1 ... 𝐽 ) → 1 ∈ ℝ )
25 22 24 readdcld ⊢ ( 𝑘 ∈ ( 1 ... 𝐽 ) → ( 𝑘 + 1 ) ∈ ℝ )
26 22 25 ltnled ⊢ ( 𝑘 ∈ ( 1 ... 𝐽 ) → ( 𝑘 < ( 𝑘 + 1 ) ↔ ¬ ( 𝑘 + 1 ) ≤ 𝑘 ) )
27 23 26 mpbid ⊢ ( 𝑘 ∈ ( 1 ... 𝐽 ) → ¬ ( 𝑘 + 1 ) ≤ 𝑘 )
28 16 27 syl ⊢ ( ( 𝜑 ∧ ( ( 𝑘 ∈ ( 1 ... 𝐽 ) ∧ ( ( 𝐹 ‘ 𝐶 ) ‘ 𝑘 ) ≤ 0 ) ∧ ∀ 𝑗 ∈ { 𝑖 ∈ ( 1 ... 𝐽 ) ∣ ( ( 𝐹 ‘ 𝐶 ) ‘ 𝑖 ) ≤ 0 } 𝑗 ≤ 𝑘 ) ) → ¬ ( 𝑘 + 1 ) ≤ 𝑘 )
29 simprr ⊢ ( ( 𝜑 ∧ ( ( 𝑘 ∈ ( 1 ... 𝐽 ) ∧ ( ( 𝐹 ‘ 𝐶 ) ‘ 𝑘 ) ≤ 0 ) ∧ ∀ 𝑗 ∈ { 𝑖 ∈ ( 1 ... 𝐽 ) ∣ ( ( 𝐹 ‘ 𝐶 ) ‘ 𝑖 ) ≤ 0 } 𝑗 ≤ 𝑘 ) ) → ∀ 𝑗 ∈ { 𝑖 ∈ ( 1 ... 𝐽 ) ∣ ( ( 𝐹 ‘ 𝐶 ) ‘ 𝑖 ) ≤ 0 } 𝑗 ≤ 𝑘 )
30 9 adantr ⊢ ( ( 𝜑 ∧ 𝑘 = 𝐽 ) → 0 < ( ( 𝐹 ‘ 𝐶 ) ‘ 𝐽 ) )
31 simpr ⊢ ( ( 𝜑 ∧ 𝑘 = 𝐽 ) → 𝑘 = 𝐽 )
32 31 fveq2d ⊢ ( ( 𝜑 ∧ 𝑘 = 𝐽 ) → ( ( 𝐹 ‘ 𝐶 ) ‘ 𝑘 ) = ( ( 𝐹 ‘ 𝐶 ) ‘ 𝐽 ) )
33 32 breq2d ⊢ ( ( 𝜑 ∧ 𝑘 = 𝐽 ) → ( 0 < ( ( 𝐹 ‘ 𝐶 ) ‘ 𝑘 ) ↔ 0 < ( ( 𝐹 ‘ 𝐶 ) ‘ 𝐽 ) ) )
34 elnnuz ⊢ ( 𝐽 ∈ ℕ ↔ 𝐽 ∈ ( ℤ≥ ‘ 1 ) )
35 7 34 sylib ⊢ ( 𝜑 → 𝐽 ∈ ( ℤ≥ ‘ 1 ) )
36 eluzfz2 ⊢ ( 𝐽 ∈ ( ℤ≥ ‘ 1 ) → 𝐽 ∈ ( 1 ... 𝐽 ) )
37 35 36 syl ⊢ ( 𝜑 → 𝐽 ∈ ( 1 ... 𝐽 ) )
38 eleq1 ⊢ ( 𝑘 = 𝐽 → ( 𝑘 ∈ ( 1 ... 𝐽 ) ↔ 𝐽 ∈ ( 1 ... 𝐽 ) ) )
39 37 38 syl5ibrcom ⊢ ( 𝜑 → ( 𝑘 = 𝐽 → 𝑘 ∈ ( 1 ... 𝐽 ) ) )
40 39 anc2li ⊢ ( 𝜑 → ( 𝑘 = 𝐽 → ( 𝜑 ∧ 𝑘 ∈ ( 1 ... 𝐽 ) ) ) )
41 1eluzge0 ⊢ 1 ∈ ( ℤ≥ ‘ 0 )
42 fzss1 ⊢ ( 1 ∈ ( ℤ≥ ‘ 0 ) → ( 1 ... 𝐽 ) ⊆ ( 0 ... 𝐽 ) )
43 42 sseld ⊢ ( 1 ∈ ( ℤ≥ ‘ 0 ) → ( 𝑘 ∈ ( 1 ... 𝐽 ) → 𝑘 ∈ ( 0 ... 𝐽 ) ) )
44 41 43 ax-mp ⊢ ( 𝑘 ∈ ( 1 ... 𝐽 ) → 𝑘 ∈ ( 0 ... 𝐽 ) )
45 0red ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... 𝐽 ) ) → 0 ∈ ℝ )
46 6 adantr ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... 𝐽 ) ) → 𝐶 ∈ 𝑂 )
47 elfzelz ⊢ ( 𝑘 ∈ ( 0 ... 𝐽 ) → 𝑘 ∈ ℤ )
48 47 adantl ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... 𝐽 ) ) → 𝑘 ∈ ℤ )
49 1 2 3 4 5 46 48 ballotlemfelz ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... 𝐽 ) ) → ( ( 𝐹 ‘ 𝐶 ) ‘ 𝑘 ) ∈ ℤ )
50 49 zred ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... 𝐽 ) ) → ( ( 𝐹 ‘ 𝐶 ) ‘ 𝑘 ) ∈ ℝ )
51 45 50 ltnled ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... 𝐽 ) ) → ( 0 < ( ( 𝐹 ‘ 𝐶 ) ‘ 𝑘 ) ↔ ¬ ( ( 𝐹 ‘ 𝐶 ) ‘ 𝑘 ) ≤ 0 ) )
52 44 51 sylan2 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 1 ... 𝐽 ) ) → ( 0 < ( ( 𝐹 ‘ 𝐶 ) ‘ 𝑘 ) ↔ ¬ ( ( 𝐹 ‘ 𝐶 ) ‘ 𝑘 ) ≤ 0 ) )
53 40 52 syl6 ⊢ ( 𝜑 → ( 𝑘 = 𝐽 → ( 0 < ( ( 𝐹 ‘ 𝐶 ) ‘ 𝑘 ) ↔ ¬ ( ( 𝐹 ‘ 𝐶 ) ‘ 𝑘 ) ≤ 0 ) ) )
54 53 imp ⊢ ( ( 𝜑 ∧ 𝑘 = 𝐽 ) → ( 0 < ( ( 𝐹 ‘ 𝐶 ) ‘ 𝑘 ) ↔ ¬ ( ( 𝐹 ‘ 𝐶 ) ‘ 𝑘 ) ≤ 0 ) )
55 33 54 bitr3d ⊢ ( ( 𝜑 ∧ 𝑘 = 𝐽 ) → ( 0 < ( ( 𝐹 ‘ 𝐶 ) ‘ 𝐽 ) ↔ ¬ ( ( 𝐹 ‘ 𝐶 ) ‘ 𝑘 ) ≤ 0 ) )
56 30 55 mpbid ⊢ ( ( 𝜑 ∧ 𝑘 = 𝐽 ) → ¬ ( ( 𝐹 ‘ 𝐶 ) ‘ 𝑘 ) ≤ 0 )
57 56 ex ⊢ ( 𝜑 → ( 𝑘 = 𝐽 → ¬ ( ( 𝐹 ‘ 𝐶 ) ‘ 𝑘 ) ≤ 0 ) )
58 57 con2d ⊢ ( 𝜑 → ( ( ( 𝐹 ‘ 𝐶 ) ‘ 𝑘 ) ≤ 0 → ¬ 𝑘 = 𝐽 ) )
59 nn1m1nn ⊢ ( 𝐽 ∈ ℕ → ( 𝐽 = 1 ∨ ( 𝐽 − 1 ) ∈ ℕ ) )
60 7 59 syl ⊢ ( 𝜑 → ( 𝐽 = 1 ∨ ( 𝐽 − 1 ) ∈ ℕ ) )
61 8 adantr ⊢ ( ( 𝜑 ∧ 𝐽 = 1 ) → ∃ 𝑖 ∈ ( 1 ... 𝐽 ) ( ( 𝐹 ‘ 𝐶 ) ‘ 𝑖 ) ≤ 0 )
62 oveq1 ⊢ ( 𝐽 = 1 → ( 𝐽 ... 𝐽 ) = ( 1 ... 𝐽 ) )
63 62 adantl ⊢ ( ( 𝜑 ∧ 𝐽 = 1 ) → ( 𝐽 ... 𝐽 ) = ( 1 ... 𝐽 ) )
64 7 nnzd ⊢ ( 𝜑 → 𝐽 ∈ ℤ )
65 fzsn ⊢ ( 𝐽 ∈ ℤ → ( 𝐽 ... 𝐽 ) = { 𝐽 } )
66 64 65 syl ⊢ ( 𝜑 → ( 𝐽 ... 𝐽 ) = { 𝐽 } )
67 66 adantr ⊢ ( ( 𝜑 ∧ 𝐽 = 1 ) → ( 𝐽 ... 𝐽 ) = { 𝐽 } )
68 63 67 eqtr3d ⊢ ( ( 𝜑 ∧ 𝐽 = 1 ) → ( 1 ... 𝐽 ) = { 𝐽 } )
69 61 68 rexeqtrdv ⊢ ( ( 𝜑 ∧ 𝐽 = 1 ) → ∃ 𝑖 ∈ { 𝐽 } ( ( 𝐹 ‘ 𝐶 ) ‘ 𝑖 ) ≤ 0 )
70 fveq2 ⊢ ( 𝑖 = 𝐽 → ( ( 𝐹 ‘ 𝐶 ) ‘ 𝑖 ) = ( ( 𝐹 ‘ 𝐶 ) ‘ 𝐽 ) )
71 70 breq1d ⊢ ( 𝑖 = 𝐽 → ( ( ( 𝐹 ‘ 𝐶 ) ‘ 𝑖 ) ≤ 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 0red ⊢ ( 𝜑 → 0 ∈ ℝ )
78 1 2 3 4 5 6 64 ballotlemfelz ⊢ ( 𝜑 → ( ( 𝐹 ‘ 𝐶 ) ‘ 𝐽 ) ∈ ℤ )
79 78 zred ⊢ ( 𝜑 → ( ( 𝐹 ‘ 𝐶 ) ‘ 𝐽 ) ∈ ℝ )
80 77 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 60 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 biimtrdi ⊢ ( 𝜑 → ( ( 𝑘 + 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 58 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 breq1d ⊢ ( 𝑖 = ( 𝑘 + 1 ) → ( ( ( 𝐹 ‘ 𝐶 ) ‘ 𝑖 ) ≤ 0 ↔ ( ( 𝐹 ‘ 𝐶 ) ‘ ( 𝑘 + 1 ) ) ≤ 0 ) )
134 133 elrab ⊢ ( ( 𝑘 + 1 ) ∈ { 𝑖 ∈ ( 1 ... 𝐽 ) ∣ ( ( 𝐹 ‘ 𝐶 ) ‘ 𝑖 ) ≤ 0 } ↔ ( ( 𝑘 + 1 ) ∈ ( 1 ... 𝐽 ) ∧ ( ( 𝐹 ‘ 𝐶 ) ‘ ( 𝑘 + 1 ) ) ≤ 0 ) )
135 breq1 ⊢ ( 𝑗 = ( 𝑘 + 1 ) → ( 𝑗 ≤ 𝑘 ↔ ( 𝑘 + 1 ) ≤ 𝑘 ) )
136 135 rspccva ⊢ ( ( ∀ 𝑗 ∈ { 𝑖 ∈ ( 1 ... 𝐽 ) ∣ ( ( 𝐹 ‘ 𝐶 ) ‘ 𝑖 ) ≤ 0 } 𝑗 ≤ 𝑘 ∧ ( 𝑘 + 1 ) ∈ { 𝑖 ∈ ( 1 ... 𝐽 ) ∣ ( ( 𝐹 ‘ 𝐶 ) ‘ 𝑖 ) ≤ 0 } ) → ( 𝑘 + 1 ) ≤ 𝑘 )
137 134 136 sylan2br ⊢ ( ( ∀ 𝑗 ∈ { 𝑖 ∈ ( 1 ... 𝐽 ) ∣ ( ( 𝐹 ‘ 𝐶 ) ‘ 𝑖 ) ≤ 0 } 𝑗 ≤ 𝑘 ∧ ( ( 𝑘 + 1 ) ∈ ( 1 ... 𝐽 ) ∧ ( ( 𝐹 ‘ 𝐶 ) ‘ ( 𝑘 + 1 ) ) ≤ 0 ) ) → ( 𝑘 + 1 ) ≤ 𝑘 )
138 137 expr ⊢ ( ( ∀ 𝑗 ∈ { 𝑖 ∈ ( 1 ... 𝐽 ) ∣ ( ( 𝐹 ‘ 𝐶 ) ‘ 𝑖 ) ≤ 0 } 𝑗 ≤ 𝑘 ∧ ( 𝑘 + 1 ) ∈ ( 1 ... 𝐽 ) ) → ( ( ( 𝐹 ‘ 𝐶 ) ‘ ( 𝑘 + 1 ) ) ≤ 0 → ( 𝑘 + 1 ) ≤ 𝑘 ) )
139 138 con3d ⊢ ( ( ∀ 𝑗 ∈ { 𝑖 ∈ ( 1 ... 𝐽 ) ∣ ( ( 𝐹 ‘ 𝐶 ) ‘ 𝑖 ) ≤ 0 } 𝑗 ≤ 𝑘 ∧ ( 𝑘 + 1 ) ∈ ( 1 ... 𝐽 ) ) → ( ¬ ( 𝑘 + 1 ) ≤ 𝑘 → ¬ ( ( 𝐹 ‘ 𝐶 ) ‘ ( 𝑘 + 1 ) ) ≤ 0 ) )
140 29 131 139 syl2anc ⊢ ( ( 𝜑 ∧ ( ( 𝑘 ∈ ( 1 ... 𝐽 ) ∧ ( ( 𝐹 ‘ 𝐶 ) ‘ 𝑘 ) ≤ 0 ) ∧ ∀ 𝑗 ∈ { 𝑖 ∈ ( 1 ... 𝐽 ) ∣ ( ( 𝐹 ‘ 𝐶 ) ‘ 𝑖 ) ≤ 0 } 𝑗 ≤ 𝑘 ) ) → ( ¬ ( 𝑘 + 1 ) ≤ 𝑘 → ¬ ( ( 𝐹 ‘ 𝐶 ) ‘ ( 𝑘 + 1 ) ) ≤ 0 ) )
141 28 140 mpd ⊢ ( ( 𝜑 ∧ ( ( 𝑘 ∈ ( 1 ... 𝐽 ) ∧ ( ( 𝐹 ‘ 𝐶 ) ‘ 𝑘 ) ≤ 0 ) ∧ ∀ 𝑗 ∈ { 𝑖 ∈ ( 1 ... 𝐽 ) ∣ ( ( 𝐹 ‘ 𝐶 ) ‘ 𝑖 ) ≤ 0 } 𝑗 ≤ 𝑘 ) ) → ¬ ( ( 𝐹 ‘ 𝐶 ) ‘ ( 𝑘 + 1 ) ) ≤ 0 )
142 simplrr ⊢ ( ( ( 𝜑 ∧ ( ( 𝑘 ∈ ( 1 ... 𝐽 ) ∧ ( ( 𝐹 ‘ 𝐶 ) ‘ 𝑘 ) ≤ 0 ) ∧ ∀ 𝑗 ∈ { 𝑖 ∈ ( 1 ... 𝐽 ) ∣ ( ( 𝐹 ‘ 𝐶 ) ‘ 𝑖 ) ≤ 0 } 𝑗 ≤ 𝑘 ) ) ∧ ¬ ( 𝑘 + 1 ) ∈ 𝐶 ) → ∀ 𝑗 ∈ { 𝑖 ∈ ( 1 ... 𝐽 ) ∣ ( ( 𝐹 ‘ 𝐶 ) ‘ 𝑖 ) ≤ 0 } 𝑗 ≤ 𝑘 )
143 131 adantr ⊢ ( ( ( 𝜑 ∧ ( ( 𝑘 ∈ ( 1 ... 𝐽 ) ∧ ( ( 𝐹 ‘ 𝐶 ) ‘ 𝑘 ) ≤ 0 ) ∧ ∀ 𝑗 ∈ { 𝑖 ∈ ( 1 ... 𝐽 ) ∣ ( ( 𝐹 ‘ 𝐶 ) ‘ 𝑖 ) ≤ 0 } 𝑗 ≤ 𝑘 ) ) ∧ ¬ ( 𝑘 + 1 ) ∈ 𝐶 ) → ( 𝑘 + 1 ) ∈ ( 1 ... 𝐽 ) )
144 simpll ⊢ ( ( ( 𝜑 ∧ ( 𝑘 ∈ ( 1 ... 𝐽 ) ∧ ( ( 𝐹 ‘ 𝐶 ) ‘ 𝑘 ) ≤ 0 ) ) ∧ ¬ ( 𝑘 + 1 ) ∈ 𝐶 ) → 𝜑 )
145 130 adantr ⊢ ( ( ( 𝜑 ∧ ( 𝑘 ∈ ( 1 ... 𝐽 ) ∧ ( ( 𝐹 ‘ 𝐶 ) ‘ 𝑘 ) ≤ 0 ) ) ∧ ¬ ( 𝑘 + 1 ) ∈ 𝐶 ) → ( 𝑘 + 1 ) ∈ ( 1 ... 𝐽 ) )
146 42 sseld ⊢ ( 1 ∈ ( ℤ≥ ‘ 0 ) → ( ( 𝑘 + 1 ) ∈ ( 1 ... 𝐽 ) → ( 𝑘 + 1 ) ∈ ( 0 ... 𝐽 ) ) )
147 41 145 146 mpsyl ⊢ ( ( ( 𝜑 ∧ ( 𝑘 ∈ ( 1 ... 𝐽 ) ∧ ( ( 𝐹 ‘ 𝐶 ) ‘ 𝑘 ) ≤ 0 ) ) ∧ ¬ ( 𝑘 + 1 ) ∈ 𝐶 ) → ( 𝑘 + 1 ) ∈ ( 0 ... 𝐽 ) )
148 6 adantr ⊢ ( ( 𝜑 ∧ ( 𝑘 + 1 ) ∈ ( 0 ... 𝐽 ) ) → 𝐶 ∈ 𝑂 )
149 elfzelz ⊢ ( ( 𝑘 + 1 ) ∈ ( 0 ... 𝐽 ) → ( 𝑘 + 1 ) ∈ ℤ )
150 149 adantl ⊢ ( ( 𝜑 ∧ ( 𝑘 + 1 ) ∈ ( 0 ... 𝐽 ) ) → ( 𝑘 + 1 ) ∈ ℤ )
151 1 2 3 4 5 148 150 ballotlemfelz ⊢ ( ( 𝜑 ∧ ( 𝑘 + 1 ) ∈ ( 0 ... 𝐽 ) ) → ( ( 𝐹 ‘ 𝐶 ) ‘ ( 𝑘 + 1 ) ) ∈ ℤ )
152 151 zred ⊢ ( ( 𝜑 ∧ ( 𝑘 + 1 ) ∈ ( 0 ... 𝐽 ) ) → ( ( 𝐹 ‘ 𝐶 ) ‘ ( 𝑘 + 1 ) ) ∈ ℝ )
153 144 147 152 syl2anc ⊢ ( ( ( 𝜑 ∧ ( 𝑘 ∈ ( 1 ... 𝐽 ) ∧ ( ( 𝐹 ‘ 𝐶 ) ‘ 𝑘 ) ≤ 0 ) ) ∧ ¬ ( 𝑘 + 1 ) ∈ 𝐶 ) → ( ( 𝐹 ‘ 𝐶 ) ‘ ( 𝑘 + 1 ) ) ∈ ℝ )
154 0red ⊢ ( ( ( 𝜑 ∧ ( 𝑘 ∈ ( 1 ... 𝐽 ) ∧ ( ( 𝐹 ‘ 𝐶 ) ‘ 𝑘 ) ≤ 0 ) ) ∧ ¬ ( 𝑘 + 1 ) ∈ 𝐶 ) → 0 ∈ ℝ )
155 simplrr ⊢ ( ( ( 𝜑 ∧ ( 𝑘 ∈ ( 1 ... 𝐽 ) ∧ ( ( 𝐹 ‘ 𝐶 ) ‘ 𝑘 ) ≤ 0 ) ) ∧ ¬ ( 𝑘 + 1 ) ∈ 𝐶 ) → ( ( 𝐹 ‘ 𝐶 ) ‘ 𝑘 ) ≤ 0 )
156 15 adantr ⊢ ( ( ( 𝜑 ∧ ( 𝑘 ∈ ( 1 ... 𝐽 ) ∧ ( ( 𝐹 ‘ 𝐶 ) ‘ 𝑘 ) ≤ 0 ) ) ∧ ¬ ( 𝑘 + 1 ) ∈ 𝐶 ) → 𝑘 ∈ ( 1 ... 𝐽 ) )
157 156 44 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 simpld ⊢ ( ( 𝜑 ∧ ( 𝑘 + 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 zlem1lt ⊢ ( ( ( ( 𝐹 ‘ 𝐶 ) ‘ 𝑘 ) ∈ ℤ ∧ 0 ∈ ℤ ) → ( ( ( 𝐹 ‘ 𝐶 ) ‘ 𝑘 ) ≤ 0 ↔ ( ( ( 𝐹 ‘ 𝐶 ) ‘ 𝑘 ) − 1 ) < 0 ) )
177 49 175 176 sylancl ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... 𝐽 ) ) → ( ( ( 𝐹 ‘ 𝐶 ) ‘ 𝑘 ) ≤ 0 ↔ ( ( ( 𝐹 ‘ 𝐶 ) ‘ 𝑘 ) − 1 ) < 0 ) )
178 177 adantr ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... 𝐽 ) ) ∧ ( ( 𝐹 ‘ 𝐶 ) ‘ ( 𝑘 + 1 ) ) = ( ( ( 𝐹 ‘ 𝐶 ) ‘ 𝑘 ) − 1 ) ) → ( ( ( 𝐹 ‘ 𝐶 ) ‘ 𝑘 ) ≤ 0 ↔ ( ( ( 𝐹 ‘ 𝐶 ) ‘ 𝑘 ) − 1 ) < 0 ) )
179 breq1 ⊢ ( ( ( 𝐹 ‘ 𝐶 ) ‘ ( 𝑘 + 1 ) ) = ( ( ( 𝐹 ‘ 𝐶 ) ‘ 𝑘 ) − 1 ) → ( ( ( 𝐹 ‘ 𝐶 ) ‘ ( 𝑘 + 1 ) ) < 0 ↔ ( ( ( 𝐹 ‘ 𝐶 ) ‘ 𝑘 ) − 1 ) < 0 ) )
180 179 adantl ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... 𝐽 ) ) ∧ ( ( 𝐹 ‘ 𝐶 ) ‘ ( 𝑘 + 1 ) ) = ( ( ( 𝐹 ‘ 𝐶 ) ‘ 𝑘 ) − 1 ) ) → ( ( ( 𝐹 ‘ 𝐶 ) ‘ ( 𝑘 + 1 ) ) < 0 ↔ ( ( ( 𝐹 ‘ 𝐶 ) ‘ 𝑘 ) − 1 ) < 0 ) )
181 178 180 bitr4d ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... 𝐽 ) ) ∧ ( ( 𝐹 ‘ 𝐶 ) ‘ ( 𝑘 + 1 ) ) = ( ( ( 𝐹 ‘ 𝐶 ) ‘ 𝑘 ) − 1 ) ) → ( ( ( 𝐹 ‘ 𝐶 ) ‘ 𝑘 ) ≤ 0 ↔ ( ( 𝐹 ‘ 𝐶 ) ‘ ( 𝑘 + 1 ) ) < 0 ) )
182 144 157 174 181 syl21anc ⊢ ( ( ( 𝜑 ∧ ( 𝑘 ∈ ( 1 ... 𝐽 ) ∧ ( ( 𝐹 ‘ 𝐶 ) ‘ 𝑘 ) ≤ 0 ) ) ∧ ¬ ( 𝑘 + 1 ) ∈ 𝐶 ) → ( ( ( 𝐹 ‘ 𝐶 ) ‘ 𝑘 ) ≤ 0 ↔ ( ( 𝐹 ‘ 𝐶 ) ‘ ( 𝑘 + 1 ) ) < 0 ) )
183 155 182 mpbid ⊢ ( ( ( 𝜑 ∧ ( 𝑘 ∈ ( 1 ... 𝐽 ) ∧ ( ( 𝐹 ‘ 𝐶 ) ‘ 𝑘 ) ≤ 0 ) ) ∧ ¬ ( 𝑘 + 1 ) ∈ 𝐶 ) → ( ( 𝐹 ‘ 𝐶 ) ‘ ( 𝑘 + 1 ) ) < 0 )
184 153 154 183 ltled ⊢ ( ( ( 𝜑 ∧ ( 𝑘 ∈ ( 1 ... 𝐽 ) ∧ ( ( 𝐹 ‘ 𝐶 ) ‘ 𝑘 ) ≤ 0 ) ) ∧ ¬ ( 𝑘 + 1 ) ∈ 𝐶 ) → ( ( 𝐹 ‘ 𝐶 ) ‘ ( 𝑘 + 1 ) ) ≤ 0 )
185 184 adantlrr ⊢ ( ( ( 𝜑 ∧ ( ( 𝑘 ∈ ( 1 ... 𝐽 ) ∧ ( ( 𝐹 ‘ 𝐶 ) ‘ 𝑘 ) ≤ 0 ) ∧ ∀ 𝑗 ∈ { 𝑖 ∈ ( 1 ... 𝐽 ) ∣ ( ( 𝐹 ‘ 𝐶 ) ‘ 𝑖 ) ≤ 0 } 𝑗 ≤ 𝑘 ) ) ∧ ¬ ( 𝑘 + 1 ) ∈ 𝐶 ) → ( ( 𝐹 ‘ 𝐶 ) ‘ ( 𝑘 + 1 ) ) ≤ 0 )
186 142 143 185 137 syl12anc ⊢ ( ( ( 𝜑 ∧ ( ( 𝑘 ∈ ( 1 ... 𝐽 ) ∧ ( ( 𝐹 ‘ 𝐶 ) ‘ 𝑘 ) ≤ 0 ) ∧ ∀ 𝑗 ∈ { 𝑖 ∈ ( 1 ... 𝐽 ) ∣ ( ( 𝐹 ‘ 𝐶 ) ‘ 𝑖 ) ≤ 0 } 𝑗 ≤ 𝑘 ) ) ∧ ¬ ( 𝑘 + 1 ) ∈ 𝐶 ) → ( 𝑘 + 1 ) ≤ 𝑘 )
187 28 adantr ⊢ ( ( ( 𝜑 ∧ ( ( 𝑘 ∈ ( 1 ... 𝐽 ) ∧ ( ( 𝐹 ‘ 𝐶 ) ‘ 𝑘 ) ≤ 0 ) ∧ ∀ 𝑗 ∈ { 𝑖 ∈ ( 1 ... 𝐽 ) ∣ ( ( 𝐹 ‘ 𝐶 ) ‘ 𝑖 ) ≤ 0 } 𝑗 ≤ 𝑘 ) ) ∧ ¬ ( 𝑘 + 1 ) ∈ 𝐶 ) → ¬ ( 𝑘 + 1 ) ≤ 𝑘 )
188 186 187 condan ⊢ ( ( 𝜑 ∧ ( ( 𝑘 ∈ ( 1 ... 𝐽 ) ∧ ( ( 𝐹 ‘ 𝐶 ) ‘ 𝑘 ) ≤ 0 ) ∧ ∀ 𝑗 ∈ { 𝑖 ∈ ( 1 ... 𝐽 ) ∣ ( ( 𝐹 ‘ 𝐶 ) ‘ 𝑖 ) ≤ 0 } 𝑗 ≤ 𝑘 ) ) → ( 𝑘 + 1 ) ∈ 𝐶 )
189 162 simprd ⊢ ( ( 𝜑 ∧ ( 𝑘 + 1 ) ∈ ( 1 ... 𝐽 ) ) → ( ( 𝑘 + 1 ) ∈ 𝐶 → ( ( 𝐹 ‘ 𝐶 ) ‘ ( 𝑘 + 1 ) ) = ( ( ( 𝐹 ‘ 𝐶 ) ‘ ( ( 𝑘 + 1 ) − 1 ) ) + 1 ) ) )
190 189 imp ⊢ ( ( ( 𝜑 ∧ ( 𝑘 + 1 ) ∈ ( 1 ... 𝐽 ) ) ∧ ( 𝑘 + 1 ) ∈ 𝐶 ) → ( ( 𝐹 ‘ 𝐶 ) ‘ ( 𝑘 + 1 ) ) = ( ( ( 𝐹 ‘ 𝐶 ) ‘ ( ( 𝑘 + 1 ) − 1 ) ) + 1 ) )
191 158 190 sylan ⊢ ( ( ( 𝜑 ∧ ( 𝑘 ∈ ( 1 ... 𝐽 ) ∧ ( ( 𝐹 ‘ 𝐶 ) ‘ 𝑘 ) ≤ 0 ) ) ∧ ( 𝑘 + 1 ) ∈ 𝐶 ) → ( ( 𝐹 ‘ 𝐶 ) ‘ ( 𝑘 + 1 ) ) = ( ( ( 𝐹 ‘ 𝐶 ) ‘ ( ( 𝑘 + 1 ) − 1 ) ) + 1 ) )
192 15 adantr ⊢ ( ( ( 𝜑 ∧ ( 𝑘 ∈ ( 1 ... 𝐽 ) ∧ ( ( 𝐹 ‘ 𝐶 ) ‘ 𝑘 ) ≤ 0 ) ) ∧ ( 𝑘 + 1 ) ∈ 𝐶 ) → 𝑘 ∈ ( 1 ... 𝐽 ) )
193 170 oveq1d ⊢ ( 𝑘 ∈ ( 1 ... 𝐽 ) → ( ( ( 𝐹 ‘ 𝐶 ) ‘ ( ( 𝑘 + 1 ) − 1 ) ) + 1 ) = ( ( ( 𝐹 ‘ 𝐶 ) ‘ 𝑘 ) + 1 ) )
194 193 eqeq2d ⊢ ( 𝑘 ∈ ( 1 ... 𝐽 ) → ( ( ( 𝐹 ‘ 𝐶 ) ‘ ( 𝑘 + 1 ) ) = ( ( ( 𝐹 ‘ 𝐶 ) ‘ ( ( 𝑘 + 1 ) − 1 ) ) + 1 ) ↔ ( ( 𝐹 ‘ 𝐶 ) ‘ ( 𝑘 + 1 ) ) = ( ( ( 𝐹 ‘ 𝐶 ) ‘ 𝑘 ) + 1 ) ) )
195 192 194 syl ⊢ ( ( ( 𝜑 ∧ ( 𝑘 ∈ ( 1 ... 𝐽 ) ∧ ( ( 𝐹 ‘ 𝐶 ) ‘ 𝑘 ) ≤ 0 ) ) ∧ ( 𝑘 + 1 ) ∈ 𝐶 ) → ( ( ( 𝐹 ‘ 𝐶 ) ‘ ( 𝑘 + 1 ) ) = ( ( ( 𝐹 ‘ 𝐶 ) ‘ ( ( 𝑘 + 1 ) − 1 ) ) + 1 ) ↔ ( ( 𝐹 ‘ 𝐶 ) ‘ ( 𝑘 + 1 ) ) = ( ( ( 𝐹 ‘ 𝐶 ) ‘ 𝑘 ) + 1 ) ) )
196 191 195 mpbid ⊢ ( ( ( 𝜑 ∧ ( 𝑘 ∈ ( 1 ... 𝐽 ) ∧ ( ( 𝐹 ‘ 𝐶 ) ‘ 𝑘 ) ≤ 0 ) ) ∧ ( 𝑘 + 1 ) ∈ 𝐶 ) → ( ( 𝐹 ‘ 𝐶 ) ‘ ( 𝑘 + 1 ) ) = ( ( ( 𝐹 ‘ 𝐶 ) ‘ 𝑘 ) + 1 ) )
197 196 adantlrr ⊢ ( ( ( 𝜑 ∧ ( ( 𝑘 ∈ ( 1 ... 𝐽 ) ∧ ( ( 𝐹 ‘ 𝐶 ) ‘ 𝑘 ) ≤ 0 ) ∧ ∀ 𝑗 ∈ { 𝑖 ∈ ( 1 ... 𝐽 ) ∣ ( ( 𝐹 ‘ 𝐶 ) ‘ 𝑖 ) ≤ 0 } 𝑗 ≤ 𝑘 ) ) ∧ ( 𝑘 + 1 ) ∈ 𝐶 ) → ( ( 𝐹 ‘ 𝐶 ) ‘ ( 𝑘 + 1 ) ) = ( ( ( 𝐹 ‘ 𝐶 ) ‘ 𝑘 ) + 1 ) )
198 188 197 mpdan ⊢ ( ( 𝜑 ∧ ( ( 𝑘 ∈ ( 1 ... 𝐽 ) ∧ ( ( 𝐹 ‘ 𝐶 ) ‘ 𝑘 ) ≤ 0 ) ∧ ∀ 𝑗 ∈ { 𝑖 ∈ ( 1 ... 𝐽 ) ∣ ( ( 𝐹 ‘ 𝐶 ) ‘ 𝑖 ) ≤ 0 } 𝑗 ≤ 𝑘 ) ) → ( ( 𝐹 ‘ 𝐶 ) ‘ ( 𝑘 + 1 ) ) = ( ( ( 𝐹 ‘ 𝐶 ) ‘ 𝑘 ) + 1 ) )
199 breq1 ⊢ ( ( ( 𝐹 ‘ 𝐶 ) ‘ ( 𝑘 + 1 ) ) = ( ( ( 𝐹 ‘ 𝐶 ) ‘ 𝑘 ) + 1 ) → ( ( ( 𝐹 ‘ 𝐶 ) ‘ ( 𝑘 + 1 ) ) ≤ 0 ↔ ( ( ( 𝐹 ‘ 𝐶 ) ‘ 𝑘 ) + 1 ) ≤ 0 ) )
200 199 notbid ⊢ ( ( ( 𝐹 ‘ 𝐶 ) ‘ ( 𝑘 + 1 ) ) = ( ( ( 𝐹 ‘ 𝐶 ) ‘ 𝑘 ) + 1 ) → ( ¬ ( ( 𝐹 ‘ 𝐶 ) ‘ ( 𝑘 + 1 ) ) ≤ 0 ↔ ¬ ( ( ( 𝐹 ‘ 𝐶 ) ‘ 𝑘 ) + 1 ) ≤ 0 ) )
201 198 200 syl ⊢ ( ( 𝜑 ∧ ( ( 𝑘 ∈ ( 1 ... 𝐽 ) ∧ ( ( 𝐹 ‘ 𝐶 ) ‘ 𝑘 ) ≤ 0 ) ∧ ∀ 𝑗 ∈ { 𝑖 ∈ ( 1 ... 𝐽 ) ∣ ( ( 𝐹 ‘ 𝐶 ) ‘ 𝑖 ) ≤ 0 } 𝑗 ≤ 𝑘 ) ) → ( ¬ ( ( 𝐹 ‘ 𝐶 ) ‘ ( 𝑘 + 1 ) ) ≤ 0 ↔ ¬ ( ( ( 𝐹 ‘ 𝐶 ) ‘ 𝑘 ) + 1 ) ≤ 0 ) )
202 141 201 mpbid ⊢ ( ( 𝜑 ∧ ( ( 𝑘 ∈ ( 1 ... 𝐽 ) ∧ ( ( 𝐹 ‘ 𝐶 ) ‘ 𝑘 ) ≤ 0 ) ∧ ∀ 𝑗 ∈ { 𝑖 ∈ ( 1 ... 𝐽 ) ∣ ( ( 𝐹 ‘ 𝐶 ) ‘ 𝑖 ) ≤ 0 } 𝑗 ≤ 𝑘 ) ) → ¬ ( ( ( 𝐹 ‘ 𝐶 ) ‘ 𝑘 ) + 1 ) ≤ 0 )
203 15 44 syl ⊢ ( ( 𝜑 ∧ ( 𝑘 ∈ ( 1 ... 𝐽 ) ∧ ( ( 𝐹 ‘ 𝐶 ) ‘ 𝑘 ) ≤ 0 ) ) → 𝑘 ∈ ( 0 ... 𝐽 ) )
204 203 49 syldan ⊢ ( ( 𝜑 ∧ ( 𝑘 ∈ ( 1 ... 𝐽 ) ∧ ( ( 𝐹 ‘ 𝐶 ) ‘ 𝑘 ) ≤ 0 ) ) → ( ( 𝐹 ‘ 𝐶 ) ‘ 𝑘 ) ∈ ℤ )
205 204 adantrr ⊢ ( ( 𝜑 ∧ ( ( 𝑘 ∈ ( 1 ... 𝐽 ) ∧ ( ( 𝐹 ‘ 𝐶 ) ‘ 𝑘 ) ≤ 0 ) ∧ ∀ 𝑗 ∈ { 𝑖 ∈ ( 1 ... 𝐽 ) ∣ ( ( 𝐹 ‘ 𝐶 ) ‘ 𝑖 ) ≤ 0 } 𝑗 ≤ 𝑘 ) ) → ( ( 𝐹 ‘ 𝐶 ) ‘ 𝑘 ) ∈ ℤ )
206 zleltp1 ⊢ ( ( 0 ∈ ℤ ∧ ( ( 𝐹 ‘ 𝐶 ) ‘ 𝑘 ) ∈ ℤ ) → ( 0 ≤ ( ( 𝐹 ‘ 𝐶 ) ‘ 𝑘 ) ↔ 0 < ( ( ( 𝐹 ‘ 𝐶 ) ‘ 𝑘 ) + 1 ) ) )
207 175 206 mpan ⊢ ( ( ( 𝐹 ‘ 𝐶 ) ‘ 𝑘 ) ∈ ℤ → ( 0 ≤ ( ( 𝐹 ‘ 𝐶 ) ‘ 𝑘 ) ↔ 0 < ( ( ( 𝐹 ‘ 𝐶 ) ‘ 𝑘 ) + 1 ) ) )
208 0red ⊢ ( ( ( 𝐹 ‘ 𝐶 ) ‘ 𝑘 ) ∈ ℤ → 0 ∈ ℝ )
209 zre ⊢ ( ( ( 𝐹 ‘ 𝐶 ) ‘ 𝑘 ) ∈ ℤ → ( ( 𝐹 ‘ 𝐶 ) ‘ 𝑘 ) ∈ ℝ )
210 1red ⊢ ( ( ( 𝐹 ‘ 𝐶 ) ‘ 𝑘 ) ∈ ℤ → 1 ∈ ℝ )
211 209 210 readdcld ⊢ ( ( ( 𝐹 ‘ 𝐶 ) ‘ 𝑘 ) ∈ ℤ → ( ( ( 𝐹 ‘ 𝐶 ) ‘ 𝑘 ) + 1 ) ∈ ℝ )
212 208 211 ltnled ⊢ ( ( ( 𝐹 ‘ 𝐶 ) ‘ 𝑘 ) ∈ ℤ → ( 0 < ( ( ( 𝐹 ‘ 𝐶 ) ‘ 𝑘 ) + 1 ) ↔ ¬ ( ( ( 𝐹 ‘ 𝐶 ) ‘ 𝑘 ) + 1 ) ≤ 0 ) )
213 207 212 bitrd ⊢ ( ( ( 𝐹 ‘ 𝐶 ) ‘ 𝑘 ) ∈ ℤ → ( 0 ≤ ( ( 𝐹 ‘ 𝐶 ) ‘ 𝑘 ) ↔ ¬ ( ( ( 𝐹 ‘ 𝐶 ) ‘ 𝑘 ) + 1 ) ≤ 0 ) )
214 205 213 syl ⊢ ( ( 𝜑 ∧ ( ( 𝑘 ∈ ( 1 ... 𝐽 ) ∧ ( ( 𝐹 ‘ 𝐶 ) ‘ 𝑘 ) ≤ 0 ) ∧ ∀ 𝑗 ∈ { 𝑖 ∈ ( 1 ... 𝐽 ) ∣ ( ( 𝐹 ‘ 𝐶 ) ‘ 𝑖 ) ≤ 0 } 𝑗 ≤ 𝑘 ) ) → ( 0 ≤ ( ( 𝐹 ‘ 𝐶 ) ‘ 𝑘 ) ↔ ¬ ( ( ( 𝐹 ‘ 𝐶 ) ‘ 𝑘 ) + 1 ) ≤ 0 ) )
215 202 214 mpbird ⊢ ( ( 𝜑 ∧ ( ( 𝑘 ∈ ( 1 ... 𝐽 ) ∧ ( ( 𝐹 ‘ 𝐶 ) ‘ 𝑘 ) ≤ 0 ) ∧ ∀ 𝑗 ∈ { 𝑖 ∈ ( 1 ... 𝐽 ) ∣ ( ( 𝐹 ‘ 𝐶 ) ‘ 𝑖 ) ≤ 0 } 𝑗 ≤ 𝑘 ) ) → 0 ≤ ( ( 𝐹 ‘ 𝐶 ) ‘ 𝑘 ) )
216 205 zred ⊢ ( ( 𝜑 ∧ ( ( 𝑘 ∈ ( 1 ... 𝐽 ) ∧ ( ( 𝐹 ‘ 𝐶 ) ‘ 𝑘 ) ≤ 0 ) ∧ ∀ 𝑗 ∈ { 𝑖 ∈ ( 1 ... 𝐽 ) ∣ ( ( 𝐹 ‘ 𝐶 ) ‘ 𝑖 ) ≤ 0 } 𝑗 ≤ 𝑘 ) ) → ( ( 𝐹 ‘ 𝐶 ) ‘ 𝑘 ) ∈ ℝ )
217 0red ⊢ ( ( 𝜑 ∧ ( ( 𝑘 ∈ ( 1 ... 𝐽 ) ∧ ( ( 𝐹 ‘ 𝐶 ) ‘ 𝑘 ) ≤ 0 ) ∧ ∀ 𝑗 ∈ { 𝑖 ∈ ( 1 ... 𝐽 ) ∣ ( ( 𝐹 ‘ 𝐶 ) ‘ 𝑖 ) ≤ 0 } 𝑗 ≤ 𝑘 ) ) → 0 ∈ ℝ )
218 216 217 letri3d ⊢ ( ( 𝜑 ∧ ( ( 𝑘 ∈ ( 1 ... 𝐽 ) ∧ ( ( 𝐹 ‘ 𝐶 ) ‘ 𝑘 ) ≤ 0 ) ∧ ∀ 𝑗 ∈ { 𝑖 ∈ ( 1 ... 𝐽 ) ∣ ( ( 𝐹 ‘ 𝐶 ) ‘ 𝑖 ) ≤ 0 } 𝑗 ≤ 𝑘 ) ) → ( ( ( 𝐹 ‘ 𝐶 ) ‘ 𝑘 ) = 0 ↔ ( ( ( 𝐹 ‘ 𝐶 ) ‘ 𝑘 ) ≤ 0 ∧ 0 ≤ ( ( 𝐹 ‘ 𝐶 ) ‘ 𝑘 ) ) ) )
219 14 215 218 mpbir2and ⊢ ( ( 𝜑 ∧ ( ( 𝑘 ∈ ( 1 ... 𝐽 ) ∧ ( ( 𝐹 ‘ 𝐶 ) ‘ 𝑘 ) ≤ 0 ) ∧ ∀ 𝑗 ∈ { 𝑖 ∈ ( 1 ... 𝐽 ) ∣ ( ( 𝐹 ‘ 𝐶 ) ‘ 𝑖 ) ≤ 0 } 𝑗 ≤ 𝑘 ) ) → ( ( 𝐹 ‘ 𝐶 ) ‘ 𝑘 ) = 0 )
220 13 219 sylan2b ⊢ ( ( 𝜑 ∧ ( 𝑘 ∈ { 𝑖 ∈ ( 1 ... 𝐽 ) ∣ ( ( 𝐹 ‘ 𝐶 ) ‘ 𝑖 ) ≤ 0 } ∧ ∀ 𝑗 ∈ { 𝑖 ∈ ( 1 ... 𝐽 ) ∣ ( ( 𝐹 ‘ 𝐶 ) ‘ 𝑖 ) ≤ 0 } 𝑗 ≤ 𝑘 ) ) → ( ( 𝐹 ‘ 𝐶 ) ‘ 𝑘 ) = 0 )
221 ssrab2 ⊢ { 𝑖 ∈ ( 1 ... 𝐽 ) ∣ ( ( 𝐹 ‘ 𝐶 ) ‘ 𝑖 ) ≤ 0 } ⊆ ( 1 ... 𝐽 )
222 221 21 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 )