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 68 rexeqdv ⊢ ( ( 𝜑 ∧ 𝐽 = 1 ) → ( ∃ 𝑖 ∈ ( 1 ... 𝐽 ) ( ( 𝐹 ‘ 𝐶 ) ‘ 𝑖 ) ≤ 0 ↔ ∃ 𝑖 ∈ { 𝐽 } ( ( 𝐹 ‘ 𝐶 ) ‘ 𝑖 ) ≤ 0 ) )
70 61 69 mpbid ⊢ ( ( 𝜑 ∧ 𝐽 = 1 ) → ∃ 𝑖 ∈ { 𝐽 } ( ( 𝐹 ‘ 𝐶 ) ‘ 𝑖 ) ≤ 0 )
71 fveq2 ⊢ ( 𝑖 = 𝐽 → ( ( 𝐹 ‘ 𝐶 ) ‘ 𝑖 ) = ( ( 𝐹 ‘ 𝐶 ) ‘ 𝐽 ) )
72 71 breq1d ⊢ ( 𝑖 = 𝐽 → ( ( ( 𝐹 ‘ 𝐶 ) ‘ 𝑖 ) ≤ 0 ↔ ( ( 𝐹 ‘ 𝐶 ) ‘ 𝐽 ) ≤ 0 ) )
73 72 rexsng ⊢ ( 𝐽 ∈ ℕ → ( ∃ 𝑖 ∈ { 𝐽 } ( ( 𝐹 ‘ 𝐶 ) ‘ 𝑖 ) ≤ 0 ↔ ( ( 𝐹 ‘ 𝐶 ) ‘ 𝐽 ) ≤ 0 ) )
74 7 73 syl ⊢ ( 𝜑 → ( ∃ 𝑖 ∈ { 𝐽 } ( ( 𝐹 ‘ 𝐶 ) ‘ 𝑖 ) ≤ 0 ↔ ( ( 𝐹 ‘ 𝐶 ) ‘ 𝐽 ) ≤ 0 ) )
75 74 adantr ⊢ ( ( 𝜑 ∧ 𝐽 = 1 ) → ( ∃ 𝑖 ∈ { 𝐽 } ( ( 𝐹 ‘ 𝐶 ) ‘ 𝑖 ) ≤ 0 ↔ ( ( 𝐹 ‘ 𝐶 ) ‘ 𝐽 ) ≤ 0 ) )
76 70 75 mpbid ⊢ ( ( 𝜑 ∧ 𝐽 = 1 ) → ( ( 𝐹 ‘ 𝐶 ) ‘ 𝐽 ) ≤ 0 )
77 9 adantr ⊢ ( ( 𝜑 ∧ 𝐽 = 1 ) → 0 < ( ( 𝐹 ‘ 𝐶 ) ‘ 𝐽 ) )
78 0red ⊢ ( 𝜑 → 0 ∈ ℝ )
79 1 2 3 4 5 6 64 ballotlemfelz ⊢ ( 𝜑 → ( ( 𝐹 ‘ 𝐶 ) ‘ 𝐽 ) ∈ ℤ )
80 79 zred ⊢ ( 𝜑 → ( ( 𝐹 ‘ 𝐶 ) ‘ 𝐽 ) ∈ ℝ )
81 78 80 ltnled ⊢ ( 𝜑 → ( 0 < ( ( 𝐹 ‘ 𝐶 ) ‘ 𝐽 ) ↔ ¬ ( ( 𝐹 ‘ 𝐶 ) ‘ 𝐽 ) ≤ 0 ) )
82 81 adantr ⊢ ( ( 𝜑 ∧ 𝐽 = 1 ) → ( 0 < ( ( 𝐹 ‘ 𝐶 ) ‘ 𝐽 ) ↔ ¬ ( ( 𝐹 ‘ 𝐶 ) ‘ 𝐽 ) ≤ 0 ) )
83 77 82 mpbid ⊢ ( ( 𝜑 ∧ 𝐽 = 1 ) → ¬ ( ( 𝐹 ‘ 𝐶 ) ‘ 𝐽 ) ≤ 0 )
84 76 83 pm2.65da ⊢ ( 𝜑 → ¬ 𝐽 = 1 )
85 biortn ⊢ ( ¬ 𝐽 = 1 → ( ( 𝐽 − 1 ) ∈ ℕ ↔ ( ¬ ¬ 𝐽 = 1 ∨ ( 𝐽 − 1 ) ∈ ℕ ) ) )
86 84 85 syl ⊢ ( 𝜑 → ( ( 𝐽 − 1 ) ∈ ℕ ↔ ( ¬ ¬ 𝐽 = 1 ∨ ( 𝐽 − 1 ) ∈ ℕ ) ) )
87 notnotb ⊢ ( 𝐽 = 1 ↔ ¬ ¬ 𝐽 = 1 )
88 87 orbi1i ⊢ ( ( 𝐽 = 1 ∨ ( 𝐽 − 1 ) ∈ ℕ ) ↔ ( ¬ ¬ 𝐽 = 1 ∨ ( 𝐽 − 1 ) ∈ ℕ ) )
89 86 88 bitr4di ⊢ ( 𝜑 → ( ( 𝐽 − 1 ) ∈ ℕ ↔ ( 𝐽 = 1 ∨ ( 𝐽 − 1 ) ∈ ℕ ) ) )
90 60 89 mpbird ⊢ ( 𝜑 → ( 𝐽 − 1 ) ∈ ℕ )
91 elnnuz ⊢ ( ( 𝐽 − 1 ) ∈ ℕ ↔ ( 𝐽 − 1 ) ∈ ( ℤ≥ ‘ 1 ) )
92 90 91 sylib ⊢ ( 𝜑 → ( 𝐽 − 1 ) ∈ ( ℤ≥ ‘ 1 ) )
93 elfzp1 ⊢ ( ( 𝐽 − 1 ) ∈ ( ℤ≥ ‘ 1 ) → ( 𝑘 ∈ ( 1 ... ( ( 𝐽 − 1 ) + 1 ) ) ↔ ( 𝑘 ∈ ( 1 ... ( 𝐽 − 1 ) ) ∨ 𝑘 = ( ( 𝐽 − 1 ) + 1 ) ) ) )
94 92 93 syl ⊢ ( 𝜑 → ( 𝑘 ∈ ( 1 ... ( ( 𝐽 − 1 ) + 1 ) ) ↔ ( 𝑘 ∈ ( 1 ... ( 𝐽 − 1 ) ) ∨ 𝑘 = ( ( 𝐽 − 1 ) + 1 ) ) ) )
95 7 nncnd ⊢ ( 𝜑 → 𝐽 ∈ ℂ )
96 1cnd ⊢ ( 𝜑 → 1 ∈ ℂ )
97 95 96 npcand ⊢ ( 𝜑 → ( ( 𝐽 − 1 ) + 1 ) = 𝐽 )
98 97 oveq2d ⊢ ( 𝜑 → ( 1 ... ( ( 𝐽 − 1 ) + 1 ) ) = ( 1 ... 𝐽 ) )
99 98 eleq2d ⊢ ( 𝜑 → ( 𝑘 ∈ ( 1 ... ( ( 𝐽 − 1 ) + 1 ) ) ↔ 𝑘 ∈ ( 1 ... 𝐽 ) ) )
100 97 eqeq2d ⊢ ( 𝜑 → ( 𝑘 = ( ( 𝐽 − 1 ) + 1 ) ↔ 𝑘 = 𝐽 ) )
101 100 orbi2d ⊢ ( 𝜑 → ( ( 𝑘 ∈ ( 1 ... ( 𝐽 − 1 ) ) ∨ 𝑘 = ( ( 𝐽 − 1 ) + 1 ) ) ↔ ( 𝑘 ∈ ( 1 ... ( 𝐽 − 1 ) ) ∨ 𝑘 = 𝐽 ) ) )
102 94 99 101 3bitr3d ⊢ ( 𝜑 → ( 𝑘 ∈ ( 1 ... 𝐽 ) ↔ ( 𝑘 ∈ ( 1 ... ( 𝐽 − 1 ) ) ∨ 𝑘 = 𝐽 ) ) )
103 orcom ⊢ ( ( 𝑘 ∈ ( 1 ... ( 𝐽 − 1 ) ) ∨ 𝑘 = 𝐽 ) ↔ ( 𝑘 = 𝐽 ∨ 𝑘 ∈ ( 1 ... ( 𝐽 − 1 ) ) ) )
104 102 103 bitrdi ⊢ ( 𝜑 → ( 𝑘 ∈ ( 1 ... 𝐽 ) ↔ ( 𝑘 = 𝐽 ∨ 𝑘 ∈ ( 1 ... ( 𝐽 − 1 ) ) ) ) )
105 104 biimpd ⊢ ( 𝜑 → ( 𝑘 ∈ ( 1 ... 𝐽 ) → ( 𝑘 = 𝐽 ∨ 𝑘 ∈ ( 1 ... ( 𝐽 − 1 ) ) ) ) )
106 pm5.6 ⊢ ( ( ( 𝑘 ∈ ( 1 ... 𝐽 ) ∧ ¬ 𝑘 = 𝐽 ) → 𝑘 ∈ ( 1 ... ( 𝐽 − 1 ) ) ) ↔ ( 𝑘 ∈ ( 1 ... 𝐽 ) → ( 𝑘 = 𝐽 ∨ 𝑘 ∈ ( 1 ... ( 𝐽 − 1 ) ) ) ) )
107 105 106 sylibr ⊢ ( 𝜑 → ( ( 𝑘 ∈ ( 1 ... 𝐽 ) ∧ ¬ 𝑘 = 𝐽 ) → 𝑘 ∈ ( 1 ... ( 𝐽 − 1 ) ) ) )
108 90 nnzd ⊢ ( 𝜑 → ( 𝐽 − 1 ) ∈ ℤ )
109 1z ⊢ 1 ∈ ℤ
110 108 109 jctil ⊢ ( 𝜑 → ( 1 ∈ ℤ ∧ ( 𝐽 − 1 ) ∈ ℤ ) )
111 elfzelz ⊢ ( 𝑘 ∈ ( 1 ... ( 𝐽 − 1 ) ) → 𝑘 ∈ ℤ )
112 111 109 jctir ⊢ ( 𝑘 ∈ ( 1 ... ( 𝐽 − 1 ) ) → ( 𝑘 ∈ ℤ ∧ 1 ∈ ℤ ) )
113 fzaddel ⊢ ( ( ( 1 ∈ ℤ ∧ ( 𝐽 − 1 ) ∈ ℤ ) ∧ ( 𝑘 ∈ ℤ ∧ 1 ∈ ℤ ) ) → ( 𝑘 ∈ ( 1 ... ( 𝐽 − 1 ) ) ↔ ( 𝑘 + 1 ) ∈ ( ( 1 + 1 ) ... ( ( 𝐽 − 1 ) + 1 ) ) ) )
114 110 112 113 syl2an ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 1 ... ( 𝐽 − 1 ) ) ) → ( 𝑘 ∈ ( 1 ... ( 𝐽 − 1 ) ) ↔ ( 𝑘 + 1 ) ∈ ( ( 1 + 1 ) ... ( ( 𝐽 − 1 ) + 1 ) ) ) )
115 114 biimp3a ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 1 ... ( 𝐽 − 1 ) ) ∧ 𝑘 ∈ ( 1 ... ( 𝐽 − 1 ) ) ) → ( 𝑘 + 1 ) ∈ ( ( 1 + 1 ) ... ( ( 𝐽 − 1 ) + 1 ) ) )
116 115 3anidm23 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 1 ... ( 𝐽 − 1 ) ) ) → ( 𝑘 + 1 ) ∈ ( ( 1 + 1 ) ... ( ( 𝐽 − 1 ) + 1 ) ) )
117 1p1e2 ⊢ ( 1 + 1 ) = 2
118 117 a1i ⊢ ( 𝜑 → ( 1 + 1 ) = 2 )
119 118 97 oveq12d ⊢ ( 𝜑 → ( ( 1 + 1 ) ... ( ( 𝐽 − 1 ) + 1 ) ) = ( 2 ... 𝐽 ) )
120 119 eleq2d ⊢ ( 𝜑 → ( ( 𝑘 + 1 ) ∈ ( ( 1 + 1 ) ... ( ( 𝐽 − 1 ) + 1 ) ) ↔ ( 𝑘 + 1 ) ∈ ( 2 ... 𝐽 ) ) )
121 2eluzge1 ⊢ 2 ∈ ( ℤ≥ ‘ 1 )
122 fzss1 ⊢ ( 2 ∈ ( ℤ≥ ‘ 1 ) → ( 2 ... 𝐽 ) ⊆ ( 1 ... 𝐽 ) )
123 121 122 ax-mp ⊢ ( 2 ... 𝐽 ) ⊆ ( 1 ... 𝐽 )
124 123 sseli ⊢ ( ( 𝑘 + 1 ) ∈ ( 2 ... 𝐽 ) → ( 𝑘 + 1 ) ∈ ( 1 ... 𝐽 ) )
125 120 124 syl6bi ⊢ ( 𝜑 → ( ( 𝑘 + 1 ) ∈ ( ( 1 + 1 ) ... ( ( 𝐽 − 1 ) + 1 ) ) → ( 𝑘 + 1 ) ∈ ( 1 ... 𝐽 ) ) )
126 125 adantr ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 1 ... ( 𝐽 − 1 ) ) ) → ( ( 𝑘 + 1 ) ∈ ( ( 1 + 1 ) ... ( ( 𝐽 − 1 ) + 1 ) ) → ( 𝑘 + 1 ) ∈ ( 1 ... 𝐽 ) ) )
127 116 126 mpd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 1 ... ( 𝐽 − 1 ) ) ) → ( 𝑘 + 1 ) ∈ ( 1 ... 𝐽 ) )
128 127 ex ⊢ ( 𝜑 → ( 𝑘 ∈ ( 1 ... ( 𝐽 − 1 ) ) → ( 𝑘 + 1 ) ∈ ( 1 ... 𝐽 ) ) )
129 107 128 syld ⊢ ( 𝜑 → ( ( 𝑘 ∈ ( 1 ... 𝐽 ) ∧ ¬ 𝑘 = 𝐽 ) → ( 𝑘 + 1 ) ∈ ( 1 ... 𝐽 ) ) )
130 58 129 sylan2d ⊢ ( 𝜑 → ( ( 𝑘 ∈ ( 1 ... 𝐽 ) ∧ ( ( 𝐹 ‘ 𝐶 ) ‘ 𝑘 ) ≤ 0 ) → ( 𝑘 + 1 ) ∈ ( 1 ... 𝐽 ) ) )
131 130 imp ⊢ ( ( 𝜑 ∧ ( 𝑘 ∈ ( 1 ... 𝐽 ) ∧ ( ( 𝐹 ‘ 𝐶 ) ‘ 𝑘 ) ≤ 0 ) ) → ( 𝑘 + 1 ) ∈ ( 1 ... 𝐽 ) )
132 131 adantrr ⊢ ( ( 𝜑 ∧ ( ( 𝑘 ∈ ( 1 ... 𝐽 ) ∧ ( ( 𝐹 ‘ 𝐶 ) ‘ 𝑘 ) ≤ 0 ) ∧ ∀ 𝑗 ∈ { 𝑖 ∈ ( 1 ... 𝐽 ) ∣ ( ( 𝐹 ‘ 𝐶 ) ‘ 𝑖 ) ≤ 0 } 𝑗 ≤ 𝑘 ) ) → ( 𝑘 + 1 ) ∈ ( 1 ... 𝐽 ) )
133 fveq2 ⊢ ( 𝑖 = ( 𝑘 + 1 ) → ( ( 𝐹 ‘ 𝐶 ) ‘ 𝑖 ) = ( ( 𝐹 ‘ 𝐶 ) ‘ ( 𝑘 + 1 ) ) )
134 133 breq1d ⊢ ( 𝑖 = ( 𝑘 + 1 ) → ( ( ( 𝐹 ‘ 𝐶 ) ‘ 𝑖 ) ≤ 0 ↔ ( ( 𝐹 ‘ 𝐶 ) ‘ ( 𝑘 + 1 ) ) ≤ 0 ) )
135 134 elrab ⊢ ( ( 𝑘 + 1 ) ∈ { 𝑖 ∈ ( 1 ... 𝐽 ) ∣ ( ( 𝐹 ‘ 𝐶 ) ‘ 𝑖 ) ≤ 0 } ↔ ( ( 𝑘 + 1 ) ∈ ( 1 ... 𝐽 ) ∧ ( ( 𝐹 ‘ 𝐶 ) ‘ ( 𝑘 + 1 ) ) ≤ 0 ) )
136 breq1 ⊢ ( 𝑗 = ( 𝑘 + 1 ) → ( 𝑗 ≤ 𝑘 ↔ ( 𝑘 + 1 ) ≤ 𝑘 ) )
137 136 rspccva ⊢ ( ( ∀ 𝑗 ∈ { 𝑖 ∈ ( 1 ... 𝐽 ) ∣ ( ( 𝐹 ‘ 𝐶 ) ‘ 𝑖 ) ≤ 0 } 𝑗 ≤ 𝑘 ∧ ( 𝑘 + 1 ) ∈ { 𝑖 ∈ ( 1 ... 𝐽 ) ∣ ( ( 𝐹 ‘ 𝐶 ) ‘ 𝑖 ) ≤ 0 } ) → ( 𝑘 + 1 ) ≤ 𝑘 )
138 135 137 sylan2br ⊢ ( ( ∀ 𝑗 ∈ { 𝑖 ∈ ( 1 ... 𝐽 ) ∣ ( ( 𝐹 ‘ 𝐶 ) ‘ 𝑖 ) ≤ 0 } 𝑗 ≤ 𝑘 ∧ ( ( 𝑘 + 1 ) ∈ ( 1 ... 𝐽 ) ∧ ( ( 𝐹 ‘ 𝐶 ) ‘ ( 𝑘 + 1 ) ) ≤ 0 ) ) → ( 𝑘 + 1 ) ≤ 𝑘 )
139 138 expr ⊢ ( ( ∀ 𝑗 ∈ { 𝑖 ∈ ( 1 ... 𝐽 ) ∣ ( ( 𝐹 ‘ 𝐶 ) ‘ 𝑖 ) ≤ 0 } 𝑗 ≤ 𝑘 ∧ ( 𝑘 + 1 ) ∈ ( 1 ... 𝐽 ) ) → ( ( ( 𝐹 ‘ 𝐶 ) ‘ ( 𝑘 + 1 ) ) ≤ 0 → ( 𝑘 + 1 ) ≤ 𝑘 ) )
140 139 con3d ⊢ ( ( ∀ 𝑗 ∈ { 𝑖 ∈ ( 1 ... 𝐽 ) ∣ ( ( 𝐹 ‘ 𝐶 ) ‘ 𝑖 ) ≤ 0 } 𝑗 ≤ 𝑘 ∧ ( 𝑘 + 1 ) ∈ ( 1 ... 𝐽 ) ) → ( ¬ ( 𝑘 + 1 ) ≤ 𝑘 → ¬ ( ( 𝐹 ‘ 𝐶 ) ‘ ( 𝑘 + 1 ) ) ≤ 0 ) )
141 29 132 140 syl2anc ⊢ ( ( 𝜑 ∧ ( ( 𝑘 ∈ ( 1 ... 𝐽 ) ∧ ( ( 𝐹 ‘ 𝐶 ) ‘ 𝑘 ) ≤ 0 ) ∧ ∀ 𝑗 ∈ { 𝑖 ∈ ( 1 ... 𝐽 ) ∣ ( ( 𝐹 ‘ 𝐶 ) ‘ 𝑖 ) ≤ 0 } 𝑗 ≤ 𝑘 ) ) → ( ¬ ( 𝑘 + 1 ) ≤ 𝑘 → ¬ ( ( 𝐹 ‘ 𝐶 ) ‘ ( 𝑘 + 1 ) ) ≤ 0 ) )
142 28 141 mpd ⊢ ( ( 𝜑 ∧ ( ( 𝑘 ∈ ( 1 ... 𝐽 ) ∧ ( ( 𝐹 ‘ 𝐶 ) ‘ 𝑘 ) ≤ 0 ) ∧ ∀ 𝑗 ∈ { 𝑖 ∈ ( 1 ... 𝐽 ) ∣ ( ( 𝐹 ‘ 𝐶 ) ‘ 𝑖 ) ≤ 0 } 𝑗 ≤ 𝑘 ) ) → ¬ ( ( 𝐹 ‘ 𝐶 ) ‘ ( 𝑘 + 1 ) ) ≤ 0 )
143 simplrr ⊢ ( ( ( 𝜑 ∧ ( ( 𝑘 ∈ ( 1 ... 𝐽 ) ∧ ( ( 𝐹 ‘ 𝐶 ) ‘ 𝑘 ) ≤ 0 ) ∧ ∀ 𝑗 ∈ { 𝑖 ∈ ( 1 ... 𝐽 ) ∣ ( ( 𝐹 ‘ 𝐶 ) ‘ 𝑖 ) ≤ 0 } 𝑗 ≤ 𝑘 ) ) ∧ ¬ ( 𝑘 + 1 ) ∈ 𝐶 ) → ∀ 𝑗 ∈ { 𝑖 ∈ ( 1 ... 𝐽 ) ∣ ( ( 𝐹 ‘ 𝐶 ) ‘ 𝑖 ) ≤ 0 } 𝑗 ≤ 𝑘 )
144 132 adantr ⊢ ( ( ( 𝜑 ∧ ( ( 𝑘 ∈ ( 1 ... 𝐽 ) ∧ ( ( 𝐹 ‘ 𝐶 ) ‘ 𝑘 ) ≤ 0 ) ∧ ∀ 𝑗 ∈ { 𝑖 ∈ ( 1 ... 𝐽 ) ∣ ( ( 𝐹 ‘ 𝐶 ) ‘ 𝑖 ) ≤ 0 } 𝑗 ≤ 𝑘 ) ) ∧ ¬ ( 𝑘 + 1 ) ∈ 𝐶 ) → ( 𝑘 + 1 ) ∈ ( 1 ... 𝐽 ) )
145 simpll ⊢ ( ( ( 𝜑 ∧ ( 𝑘 ∈ ( 1 ... 𝐽 ) ∧ ( ( 𝐹 ‘ 𝐶 ) ‘ 𝑘 ) ≤ 0 ) ) ∧ ¬ ( 𝑘 + 1 ) ∈ 𝐶 ) → 𝜑 )
146 131 adantr ⊢ ( ( ( 𝜑 ∧ ( 𝑘 ∈ ( 1 ... 𝐽 ) ∧ ( ( 𝐹 ‘ 𝐶 ) ‘ 𝑘 ) ≤ 0 ) ) ∧ ¬ ( 𝑘 + 1 ) ∈ 𝐶 ) → ( 𝑘 + 1 ) ∈ ( 1 ... 𝐽 ) )
147 42 sseld ⊢ ( 1 ∈ ( ℤ≥ ‘ 0 ) → ( ( 𝑘 + 1 ) ∈ ( 1 ... 𝐽 ) → ( 𝑘 + 1 ) ∈ ( 0 ... 𝐽 ) ) )
148 41 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 0red ⊢ ( ( ( 𝜑 ∧ ( 𝑘 ∈ ( 1 ... 𝐽 ) ∧ ( ( 𝐹 ‘ 𝐶 ) ‘ 𝑘 ) ≤ 0 ) ) ∧ ¬ ( 𝑘 + 1 ) ∈ 𝐶 ) → 0 ∈ ℝ )
156 simplrr ⊢ ( ( ( 𝜑 ∧ ( 𝑘 ∈ ( 1 ... 𝐽 ) ∧ ( ( 𝐹 ‘ 𝐶 ) ‘ 𝑘 ) ≤ 0 ) ) ∧ ¬ ( 𝑘 + 1 ) ∈ 𝐶 ) → ( ( 𝐹 ‘ 𝐶 ) ‘ 𝑘 ) ≤ 0 )
157 15 adantr ⊢ ( ( ( 𝜑 ∧ ( 𝑘 ∈ ( 1 ... 𝐽 ) ∧ ( ( 𝐹 ‘ 𝐶 ) ‘ 𝑘 ) ≤ 0 ) ) ∧ ¬ ( 𝑘 + 1 ) ∈ 𝐶 ) → 𝑘 ∈ ( 1 ... 𝐽 ) )
158 157 44 syl ⊢ ( ( ( 𝜑 ∧ ( 𝑘 ∈ ( 1 ... 𝐽 ) ∧ ( ( 𝐹 ‘ 𝐶 ) ‘ 𝑘 ) ≤ 0 ) ) ∧ ¬ ( 𝑘 + 1 ) ∈ 𝐶 ) → 𝑘 ∈ ( 0 ... 𝐽 ) )
159 130 imdistani ⊢ ( ( 𝜑 ∧ ( 𝑘 ∈ ( 1 ... 𝐽 ) ∧ ( ( 𝐹 ‘ 𝐶 ) ‘ 𝑘 ) ≤ 0 ) ) → ( 𝜑 ∧ ( 𝑘 + 1 ) ∈ ( 1 ... 𝐽 ) ) )
160 6 adantr ⊢ ( ( 𝜑 ∧ ( 𝑘 + 1 ) ∈ ( 1 ... 𝐽 ) ) → 𝐶 ∈ 𝑂 )
161 elfznn ⊢ ( ( 𝑘 + 1 ) ∈ ( 1 ... 𝐽 ) → ( 𝑘 + 1 ) ∈ ℕ )
162 161 adantl ⊢ ( ( 𝜑 ∧ ( 𝑘 + 1 ) ∈ ( 1 ... 𝐽 ) ) → ( 𝑘 + 1 ) ∈ ℕ )
163 1 2 3 4 5 160 162 ballotlemfp1 ⊢ ( ( 𝜑 ∧ ( 𝑘 + 1 ) ∈ ( 1 ... 𝐽 ) ) → ( ( ¬ ( 𝑘 + 1 ) ∈ 𝐶 → ( ( 𝐹 ‘ 𝐶 ) ‘ ( 𝑘 + 1 ) ) = ( ( ( 𝐹 ‘ 𝐶 ) ‘ ( ( 𝑘 + 1 ) − 1 ) ) − 1 ) ) ∧ ( ( 𝑘 + 1 ) ∈ 𝐶 → ( ( 𝐹 ‘ 𝐶 ) ‘ ( 𝑘 + 1 ) ) = ( ( ( 𝐹 ‘ 𝐶 ) ‘ ( ( 𝑘 + 1 ) − 1 ) ) + 1 ) ) ) )
164 163 simpld ⊢ ( ( 𝜑 ∧ ( 𝑘 + 1 ) ∈ ( 1 ... 𝐽 ) ) → ( ¬ ( 𝑘 + 1 ) ∈ 𝐶 → ( ( 𝐹 ‘ 𝐶 ) ‘ ( 𝑘 + 1 ) ) = ( ( ( 𝐹 ‘ 𝐶 ) ‘ ( ( 𝑘 + 1 ) − 1 ) ) − 1 ) ) )
165 164 imp ⊢ ( ( ( 𝜑 ∧ ( 𝑘 + 1 ) ∈ ( 1 ... 𝐽 ) ) ∧ ¬ ( 𝑘 + 1 ) ∈ 𝐶 ) → ( ( 𝐹 ‘ 𝐶 ) ‘ ( 𝑘 + 1 ) ) = ( ( ( 𝐹 ‘ 𝐶 ) ‘ ( ( 𝑘 + 1 ) − 1 ) ) − 1 ) )
166 159 165 sylan ⊢ ( ( ( 𝜑 ∧ ( 𝑘 ∈ ( 1 ... 𝐽 ) ∧ ( ( 𝐹 ‘ 𝐶 ) ‘ 𝑘 ) ≤ 0 ) ) ∧ ¬ ( 𝑘 + 1 ) ∈ 𝐶 ) → ( ( 𝐹 ‘ 𝐶 ) ‘ ( 𝑘 + 1 ) ) = ( ( ( 𝐹 ‘ 𝐶 ) ‘ ( ( 𝑘 + 1 ) − 1 ) ) − 1 ) )
167 elfzelz ⊢ ( 𝑘 ∈ ( 1 ... 𝐽 ) → 𝑘 ∈ ℤ )
168 167 zcnd ⊢ ( 𝑘 ∈ ( 1 ... 𝐽 ) → 𝑘 ∈ ℂ )
169 1cnd ⊢ ( 𝑘 ∈ ( 1 ... 𝐽 ) → 1 ∈ ℂ )
170 168 169 pncand ⊢ ( 𝑘 ∈ ( 1 ... 𝐽 ) → ( ( 𝑘 + 1 ) − 1 ) = 𝑘 )
171 170 fveq2d ⊢ ( 𝑘 ∈ ( 1 ... 𝐽 ) → ( ( 𝐹 ‘ 𝐶 ) ‘ ( ( 𝑘 + 1 ) − 1 ) ) = ( ( 𝐹 ‘ 𝐶 ) ‘ 𝑘 ) )
172 171 oveq1d ⊢ ( 𝑘 ∈ ( 1 ... 𝐽 ) → ( ( ( 𝐹 ‘ 𝐶 ) ‘ ( ( 𝑘 + 1 ) − 1 ) ) − 1 ) = ( ( ( 𝐹 ‘ 𝐶 ) ‘ 𝑘 ) − 1 ) )
173 172 eqeq2d ⊢ ( 𝑘 ∈ ( 1 ... 𝐽 ) → ( ( ( 𝐹 ‘ 𝐶 ) ‘ ( 𝑘 + 1 ) ) = ( ( ( 𝐹 ‘ 𝐶 ) ‘ ( ( 𝑘 + 1 ) − 1 ) ) − 1 ) ↔ ( ( 𝐹 ‘ 𝐶 ) ‘ ( 𝑘 + 1 ) ) = ( ( ( 𝐹 ‘ 𝐶 ) ‘ 𝑘 ) − 1 ) ) )
174 157 173 syl ⊢ ( ( ( 𝜑 ∧ ( 𝑘 ∈ ( 1 ... 𝐽 ) ∧ ( ( 𝐹 ‘ 𝐶 ) ‘ 𝑘 ) ≤ 0 ) ) ∧ ¬ ( 𝑘 + 1 ) ∈ 𝐶 ) → ( ( ( 𝐹 ‘ 𝐶 ) ‘ ( 𝑘 + 1 ) ) = ( ( ( 𝐹 ‘ 𝐶 ) ‘ ( ( 𝑘 + 1 ) − 1 ) ) − 1 ) ↔ ( ( 𝐹 ‘ 𝐶 ) ‘ ( 𝑘 + 1 ) ) = ( ( ( 𝐹 ‘ 𝐶 ) ‘ 𝑘 ) − 1 ) ) )
175 166 174 mpbid ⊢ ( ( ( 𝜑 ∧ ( 𝑘 ∈ ( 1 ... 𝐽 ) ∧ ( ( 𝐹 ‘ 𝐶 ) ‘ 𝑘 ) ≤ 0 ) ) ∧ ¬ ( 𝑘 + 1 ) ∈ 𝐶 ) → ( ( 𝐹 ‘ 𝐶 ) ‘ ( 𝑘 + 1 ) ) = ( ( ( 𝐹 ‘ 𝐶 ) ‘ 𝑘 ) − 1 ) )
176 0z ⊢ 0 ∈ ℤ
177 zlem1lt ⊢ ( ( ( ( 𝐹 ‘ 𝐶 ) ‘ 𝑘 ) ∈ ℤ ∧ 0 ∈ ℤ ) → ( ( ( 𝐹 ‘ 𝐶 ) ‘ 𝑘 ) ≤ 0 ↔ ( ( ( 𝐹 ‘ 𝐶 ) ‘ 𝑘 ) − 1 ) < 0 ) )
178 49 176 177 sylancl ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... 𝐽 ) ) → ( ( ( 𝐹 ‘ 𝐶 ) ‘ 𝑘 ) ≤ 0 ↔ ( ( ( 𝐹 ‘ 𝐶 ) ‘ 𝑘 ) − 1 ) < 0 ) )
179 178 adantr ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... 𝐽 ) ) ∧ ( ( 𝐹 ‘ 𝐶 ) ‘ ( 𝑘 + 1 ) ) = ( ( ( 𝐹 ‘ 𝐶 ) ‘ 𝑘 ) − 1 ) ) → ( ( ( 𝐹 ‘ 𝐶 ) ‘ 𝑘 ) ≤ 0 ↔ ( ( ( 𝐹 ‘ 𝐶 ) ‘ 𝑘 ) − 1 ) < 0 ) )
180 breq1 ⊢ ( ( ( 𝐹 ‘ 𝐶 ) ‘ ( 𝑘 + 1 ) ) = ( ( ( 𝐹 ‘ 𝐶 ) ‘ 𝑘 ) − 1 ) → ( ( ( 𝐹 ‘ 𝐶 ) ‘ ( 𝑘 + 1 ) ) < 0 ↔ ( ( ( 𝐹 ‘ 𝐶 ) ‘ 𝑘 ) − 1 ) < 0 ) )
181 180 adantl ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... 𝐽 ) ) ∧ ( ( 𝐹 ‘ 𝐶 ) ‘ ( 𝑘 + 1 ) ) = ( ( ( 𝐹 ‘ 𝐶 ) ‘ 𝑘 ) − 1 ) ) → ( ( ( 𝐹 ‘ 𝐶 ) ‘ ( 𝑘 + 1 ) ) < 0 ↔ ( ( ( 𝐹 ‘ 𝐶 ) ‘ 𝑘 ) − 1 ) < 0 ) )
182 179 181 bitr4d ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... 𝐽 ) ) ∧ ( ( 𝐹 ‘ 𝐶 ) ‘ ( 𝑘 + 1 ) ) = ( ( ( 𝐹 ‘ 𝐶 ) ‘ 𝑘 ) − 1 ) ) → ( ( ( 𝐹 ‘ 𝐶 ) ‘ 𝑘 ) ≤ 0 ↔ ( ( 𝐹 ‘ 𝐶 ) ‘ ( 𝑘 + 1 ) ) < 0 ) )
183 145 158 175 182 syl21anc ⊢ ( ( ( 𝜑 ∧ ( 𝑘 ∈ ( 1 ... 𝐽 ) ∧ ( ( 𝐹 ‘ 𝐶 ) ‘ 𝑘 ) ≤ 0 ) ) ∧ ¬ ( 𝑘 + 1 ) ∈ 𝐶 ) → ( ( ( 𝐹 ‘ 𝐶 ) ‘ 𝑘 ) ≤ 0 ↔ ( ( 𝐹 ‘ 𝐶 ) ‘ ( 𝑘 + 1 ) ) < 0 ) )
184 156 183 mpbid ⊢ ( ( ( 𝜑 ∧ ( 𝑘 ∈ ( 1 ... 𝐽 ) ∧ ( ( 𝐹 ‘ 𝐶 ) ‘ 𝑘 ) ≤ 0 ) ) ∧ ¬ ( 𝑘 + 1 ) ∈ 𝐶 ) → ( ( 𝐹 ‘ 𝐶 ) ‘ ( 𝑘 + 1 ) ) < 0 )
185 154 155 184 ltled ⊢ ( ( ( 𝜑 ∧ ( 𝑘 ∈ ( 1 ... 𝐽 ) ∧ ( ( 𝐹 ‘ 𝐶 ) ‘ 𝑘 ) ≤ 0 ) ) ∧ ¬ ( 𝑘 + 1 ) ∈ 𝐶 ) → ( ( 𝐹 ‘ 𝐶 ) ‘ ( 𝑘 + 1 ) ) ≤ 0 )
186 185 adantlrr ⊢ ( ( ( 𝜑 ∧ ( ( 𝑘 ∈ ( 1 ... 𝐽 ) ∧ ( ( 𝐹 ‘ 𝐶 ) ‘ 𝑘 ) ≤ 0 ) ∧ ∀ 𝑗 ∈ { 𝑖 ∈ ( 1 ... 𝐽 ) ∣ ( ( 𝐹 ‘ 𝐶 ) ‘ 𝑖 ) ≤ 0 } 𝑗 ≤ 𝑘 ) ) ∧ ¬ ( 𝑘 + 1 ) ∈ 𝐶 ) → ( ( 𝐹 ‘ 𝐶 ) ‘ ( 𝑘 + 1 ) ) ≤ 0 )
187 143 144 186 138 syl12anc ⊢ ( ( ( 𝜑 ∧ ( ( 𝑘 ∈ ( 1 ... 𝐽 ) ∧ ( ( 𝐹 ‘ 𝐶 ) ‘ 𝑘 ) ≤ 0 ) ∧ ∀ 𝑗 ∈ { 𝑖 ∈ ( 1 ... 𝐽 ) ∣ ( ( 𝐹 ‘ 𝐶 ) ‘ 𝑖 ) ≤ 0 } 𝑗 ≤ 𝑘 ) ) ∧ ¬ ( 𝑘 + 1 ) ∈ 𝐶 ) → ( 𝑘 + 1 ) ≤ 𝑘 )
188 28 adantr ⊢ ( ( ( 𝜑 ∧ ( ( 𝑘 ∈ ( 1 ... 𝐽 ) ∧ ( ( 𝐹 ‘ 𝐶 ) ‘ 𝑘 ) ≤ 0 ) ∧ ∀ 𝑗 ∈ { 𝑖 ∈ ( 1 ... 𝐽 ) ∣ ( ( 𝐹 ‘ 𝐶 ) ‘ 𝑖 ) ≤ 0 } 𝑗 ≤ 𝑘 ) ) ∧ ¬ ( 𝑘 + 1 ) ∈ 𝐶 ) → ¬ ( 𝑘 + 1 ) ≤ 𝑘 )
189 187 188 condan ⊢ ( ( 𝜑 ∧ ( ( 𝑘 ∈ ( 1 ... 𝐽 ) ∧ ( ( 𝐹 ‘ 𝐶 ) ‘ 𝑘 ) ≤ 0 ) ∧ ∀ 𝑗 ∈ { 𝑖 ∈ ( 1 ... 𝐽 ) ∣ ( ( 𝐹 ‘ 𝐶 ) ‘ 𝑖 ) ≤ 0 } 𝑗 ≤ 𝑘 ) ) → ( 𝑘 + 1 ) ∈ 𝐶 )
190 163 simprd ⊢ ( ( 𝜑 ∧ ( 𝑘 + 1 ) ∈ ( 1 ... 𝐽 ) ) → ( ( 𝑘 + 1 ) ∈ 𝐶 → ( ( 𝐹 ‘ 𝐶 ) ‘ ( 𝑘 + 1 ) ) = ( ( ( 𝐹 ‘ 𝐶 ) ‘ ( ( 𝑘 + 1 ) − 1 ) ) + 1 ) ) )
191 190 imp ⊢ ( ( ( 𝜑 ∧ ( 𝑘 + 1 ) ∈ ( 1 ... 𝐽 ) ) ∧ ( 𝑘 + 1 ) ∈ 𝐶 ) → ( ( 𝐹 ‘ 𝐶 ) ‘ ( 𝑘 + 1 ) ) = ( ( ( 𝐹 ‘ 𝐶 ) ‘ ( ( 𝑘 + 1 ) − 1 ) ) + 1 ) )
192 159 191 sylan ⊢ ( ( ( 𝜑 ∧ ( 𝑘 ∈ ( 1 ... 𝐽 ) ∧ ( ( 𝐹 ‘ 𝐶 ) ‘ 𝑘 ) ≤ 0 ) ) ∧ ( 𝑘 + 1 ) ∈ 𝐶 ) → ( ( 𝐹 ‘ 𝐶 ) ‘ ( 𝑘 + 1 ) ) = ( ( ( 𝐹 ‘ 𝐶 ) ‘ ( ( 𝑘 + 1 ) − 1 ) ) + 1 ) )
193 15 adantr ⊢ ( ( ( 𝜑 ∧ ( 𝑘 ∈ ( 1 ... 𝐽 ) ∧ ( ( 𝐹 ‘ 𝐶 ) ‘ 𝑘 ) ≤ 0 ) ) ∧ ( 𝑘 + 1 ) ∈ 𝐶 ) → 𝑘 ∈ ( 1 ... 𝐽 ) )
194 171 oveq1d ⊢ ( 𝑘 ∈ ( 1 ... 𝐽 ) → ( ( ( 𝐹 ‘ 𝐶 ) ‘ ( ( 𝑘 + 1 ) − 1 ) ) + 1 ) = ( ( ( 𝐹 ‘ 𝐶 ) ‘ 𝑘 ) + 1 ) )
195 194 eqeq2d ⊢ ( 𝑘 ∈ ( 1 ... 𝐽 ) → ( ( ( 𝐹 ‘ 𝐶 ) ‘ ( 𝑘 + 1 ) ) = ( ( ( 𝐹 ‘ 𝐶 ) ‘ ( ( 𝑘 + 1 ) − 1 ) ) + 1 ) ↔ ( ( 𝐹 ‘ 𝐶 ) ‘ ( 𝑘 + 1 ) ) = ( ( ( 𝐹 ‘ 𝐶 ) ‘ 𝑘 ) + 1 ) ) )
196 193 195 syl ⊢ ( ( ( 𝜑 ∧ ( 𝑘 ∈ ( 1 ... 𝐽 ) ∧ ( ( 𝐹 ‘ 𝐶 ) ‘ 𝑘 ) ≤ 0 ) ) ∧ ( 𝑘 + 1 ) ∈ 𝐶 ) → ( ( ( 𝐹 ‘ 𝐶 ) ‘ ( 𝑘 + 1 ) ) = ( ( ( 𝐹 ‘ 𝐶 ) ‘ ( ( 𝑘 + 1 ) − 1 ) ) + 1 ) ↔ ( ( 𝐹 ‘ 𝐶 ) ‘ ( 𝑘 + 1 ) ) = ( ( ( 𝐹 ‘ 𝐶 ) ‘ 𝑘 ) + 1 ) ) )
197 192 196 mpbid ⊢ ( ( ( 𝜑 ∧ ( 𝑘 ∈ ( 1 ... 𝐽 ) ∧ ( ( 𝐹 ‘ 𝐶 ) ‘ 𝑘 ) ≤ 0 ) ) ∧ ( 𝑘 + 1 ) ∈ 𝐶 ) → ( ( 𝐹 ‘ 𝐶 ) ‘ ( 𝑘 + 1 ) ) = ( ( ( 𝐹 ‘ 𝐶 ) ‘ 𝑘 ) + 1 ) )
198 197 adantlrr ⊢ ( ( ( 𝜑 ∧ ( ( 𝑘 ∈ ( 1 ... 𝐽 ) ∧ ( ( 𝐹 ‘ 𝐶 ) ‘ 𝑘 ) ≤ 0 ) ∧ ∀ 𝑗 ∈ { 𝑖 ∈ ( 1 ... 𝐽 ) ∣ ( ( 𝐹 ‘ 𝐶 ) ‘ 𝑖 ) ≤ 0 } 𝑗 ≤ 𝑘 ) ) ∧ ( 𝑘 + 1 ) ∈ 𝐶 ) → ( ( 𝐹 ‘ 𝐶 ) ‘ ( 𝑘 + 1 ) ) = ( ( ( 𝐹 ‘ 𝐶 ) ‘ 𝑘 ) + 1 ) )
199 189 198 mpdan ⊢ ( ( 𝜑 ∧ ( ( 𝑘 ∈ ( 1 ... 𝐽 ) ∧ ( ( 𝐹 ‘ 𝐶 ) ‘ 𝑘 ) ≤ 0 ) ∧ ∀ 𝑗 ∈ { 𝑖 ∈ ( 1 ... 𝐽 ) ∣ ( ( 𝐹 ‘ 𝐶 ) ‘ 𝑖 ) ≤ 0 } 𝑗 ≤ 𝑘 ) ) → ( ( 𝐹 ‘ 𝐶 ) ‘ ( 𝑘 + 1 ) ) = ( ( ( 𝐹 ‘ 𝐶 ) ‘ 𝑘 ) + 1 ) )
200 breq1 ⊢ ( ( ( 𝐹 ‘ 𝐶 ) ‘ ( 𝑘 + 1 ) ) = ( ( ( 𝐹 ‘ 𝐶 ) ‘ 𝑘 ) + 1 ) → ( ( ( 𝐹 ‘ 𝐶 ) ‘ ( 𝑘 + 1 ) ) ≤ 0 ↔ ( ( ( 𝐹 ‘ 𝐶 ) ‘ 𝑘 ) + 1 ) ≤ 0 ) )
201 200 notbid ⊢ ( ( ( 𝐹 ‘ 𝐶 ) ‘ ( 𝑘 + 1 ) ) = ( ( ( 𝐹 ‘ 𝐶 ) ‘ 𝑘 ) + 1 ) → ( ¬ ( ( 𝐹 ‘ 𝐶 ) ‘ ( 𝑘 + 1 ) ) ≤ 0 ↔ ¬ ( ( ( 𝐹 ‘ 𝐶 ) ‘ 𝑘 ) + 1 ) ≤ 0 ) )
202 199 201 syl ⊢ ( ( 𝜑 ∧ ( ( 𝑘 ∈ ( 1 ... 𝐽 ) ∧ ( ( 𝐹 ‘ 𝐶 ) ‘ 𝑘 ) ≤ 0 ) ∧ ∀ 𝑗 ∈ { 𝑖 ∈ ( 1 ... 𝐽 ) ∣ ( ( 𝐹 ‘ 𝐶 ) ‘ 𝑖 ) ≤ 0 } 𝑗 ≤ 𝑘 ) ) → ( ¬ ( ( 𝐹 ‘ 𝐶 ) ‘ ( 𝑘 + 1 ) ) ≤ 0 ↔ ¬ ( ( ( 𝐹 ‘ 𝐶 ) ‘ 𝑘 ) + 1 ) ≤ 0 ) )
203 142 202 mpbid ⊢ ( ( 𝜑 ∧ ( ( 𝑘 ∈ ( 1 ... 𝐽 ) ∧ ( ( 𝐹 ‘ 𝐶 ) ‘ 𝑘 ) ≤ 0 ) ∧ ∀ 𝑗 ∈ { 𝑖 ∈ ( 1 ... 𝐽 ) ∣ ( ( 𝐹 ‘ 𝐶 ) ‘ 𝑖 ) ≤ 0 } 𝑗 ≤ 𝑘 ) ) → ¬ ( ( ( 𝐹 ‘ 𝐶 ) ‘ 𝑘 ) + 1 ) ≤ 0 )
204 15 44 syl ⊢ ( ( 𝜑 ∧ ( 𝑘 ∈ ( 1 ... 𝐽 ) ∧ ( ( 𝐹 ‘ 𝐶 ) ‘ 𝑘 ) ≤ 0 ) ) → 𝑘 ∈ ( 0 ... 𝐽 ) )
205 204 49 syldan ⊢ ( ( 𝜑 ∧ ( 𝑘 ∈ ( 1 ... 𝐽 ) ∧ ( ( 𝐹 ‘ 𝐶 ) ‘ 𝑘 ) ≤ 0 ) ) → ( ( 𝐹 ‘ 𝐶 ) ‘ 𝑘 ) ∈ ℤ )
206 205 adantrr ⊢ ( ( 𝜑 ∧ ( ( 𝑘 ∈ ( 1 ... 𝐽 ) ∧ ( ( 𝐹 ‘ 𝐶 ) ‘ 𝑘 ) ≤ 0 ) ∧ ∀ 𝑗 ∈ { 𝑖 ∈ ( 1 ... 𝐽 ) ∣ ( ( 𝐹 ‘ 𝐶 ) ‘ 𝑖 ) ≤ 0 } 𝑗 ≤ 𝑘 ) ) → ( ( 𝐹 ‘ 𝐶 ) ‘ 𝑘 ) ∈ ℤ )
207 zleltp1 ⊢ ( ( 0 ∈ ℤ ∧ ( ( 𝐹 ‘ 𝐶 ) ‘ 𝑘 ) ∈ ℤ ) → ( 0 ≤ ( ( 𝐹 ‘ 𝐶 ) ‘ 𝑘 ) ↔ 0 < ( ( ( 𝐹 ‘ 𝐶 ) ‘ 𝑘 ) + 1 ) ) )
208 176 207 mpan ⊢ ( ( ( 𝐹 ‘ 𝐶 ) ‘ 𝑘 ) ∈ ℤ → ( 0 ≤ ( ( 𝐹 ‘ 𝐶 ) ‘ 𝑘 ) ↔ 0 < ( ( ( 𝐹 ‘ 𝐶 ) ‘ 𝑘 ) + 1 ) ) )
209 0red ⊢ ( ( ( 𝐹 ‘ 𝐶 ) ‘ 𝑘 ) ∈ ℤ → 0 ∈ ℝ )
210 zre ⊢ ( ( ( 𝐹 ‘ 𝐶 ) ‘ 𝑘 ) ∈ ℤ → ( ( 𝐹 ‘ 𝐶 ) ‘ 𝑘 ) ∈ ℝ )
211 1red ⊢ ( ( ( 𝐹 ‘ 𝐶 ) ‘ 𝑘 ) ∈ ℤ → 1 ∈ ℝ )
212 210 211 readdcld ⊢ ( ( ( 𝐹 ‘ 𝐶 ) ‘ 𝑘 ) ∈ ℤ → ( ( ( 𝐹 ‘ 𝐶 ) ‘ 𝑘 ) + 1 ) ∈ ℝ )
213 209 212 ltnled ⊢ ( ( ( 𝐹 ‘ 𝐶 ) ‘ 𝑘 ) ∈ ℤ → ( 0 < ( ( ( 𝐹 ‘ 𝐶 ) ‘ 𝑘 ) + 1 ) ↔ ¬ ( ( ( 𝐹 ‘ 𝐶 ) ‘ 𝑘 ) + 1 ) ≤ 0 ) )
214 208 213 bitrd ⊢ ( ( ( 𝐹 ‘ 𝐶 ) ‘ 𝑘 ) ∈ ℤ → ( 0 ≤ ( ( 𝐹 ‘ 𝐶 ) ‘ 𝑘 ) ↔ ¬ ( ( ( 𝐹 ‘ 𝐶 ) ‘ 𝑘 ) + 1 ) ≤ 0 ) )
215 206 214 syl ⊢ ( ( 𝜑 ∧ ( ( 𝑘 ∈ ( 1 ... 𝐽 ) ∧ ( ( 𝐹 ‘ 𝐶 ) ‘ 𝑘 ) ≤ 0 ) ∧ ∀ 𝑗 ∈ { 𝑖 ∈ ( 1 ... 𝐽 ) ∣ ( ( 𝐹 ‘ 𝐶 ) ‘ 𝑖 ) ≤ 0 } 𝑗 ≤ 𝑘 ) ) → ( 0 ≤ ( ( 𝐹 ‘ 𝐶 ) ‘ 𝑘 ) ↔ ¬ ( ( ( 𝐹 ‘ 𝐶 ) ‘ 𝑘 ) + 1 ) ≤ 0 ) )
216 203 215 mpbird ⊢ ( ( 𝜑 ∧ ( ( 𝑘 ∈ ( 1 ... 𝐽 ) ∧ ( ( 𝐹 ‘ 𝐶 ) ‘ 𝑘 ) ≤ 0 ) ∧ ∀ 𝑗 ∈ { 𝑖 ∈ ( 1 ... 𝐽 ) ∣ ( ( 𝐹 ‘ 𝐶 ) ‘ 𝑖 ) ≤ 0 } 𝑗 ≤ 𝑘 ) ) → 0 ≤ ( ( 𝐹 ‘ 𝐶 ) ‘ 𝑘 ) )
217 206 zred ⊢ ( ( 𝜑 ∧ ( ( 𝑘 ∈ ( 1 ... 𝐽 ) ∧ ( ( 𝐹 ‘ 𝐶 ) ‘ 𝑘 ) ≤ 0 ) ∧ ∀ 𝑗 ∈ { 𝑖 ∈ ( 1 ... 𝐽 ) ∣ ( ( 𝐹 ‘ 𝐶 ) ‘ 𝑖 ) ≤ 0 } 𝑗 ≤ 𝑘 ) ) → ( ( 𝐹 ‘ 𝐶 ) ‘ 𝑘 ) ∈ ℝ )
218 0red ⊢ ( ( 𝜑 ∧ ( ( 𝑘 ∈ ( 1 ... 𝐽 ) ∧ ( ( 𝐹 ‘ 𝐶 ) ‘ 𝑘 ) ≤ 0 ) ∧ ∀ 𝑗 ∈ { 𝑖 ∈ ( 1 ... 𝐽 ) ∣ ( ( 𝐹 ‘ 𝐶 ) ‘ 𝑖 ) ≤ 0 } 𝑗 ≤ 𝑘 ) ) → 0 ∈ ℝ )
219 217 218 letri3d ⊢ ( ( 𝜑 ∧ ( ( 𝑘 ∈ ( 1 ... 𝐽 ) ∧ ( ( 𝐹 ‘ 𝐶 ) ‘ 𝑘 ) ≤ 0 ) ∧ ∀ 𝑗 ∈ { 𝑖 ∈ ( 1 ... 𝐽 ) ∣ ( ( 𝐹 ‘ 𝐶 ) ‘ 𝑖 ) ≤ 0 } 𝑗 ≤ 𝑘 ) ) → ( ( ( 𝐹 ‘ 𝐶 ) ‘ 𝑘 ) = 0 ↔ ( ( ( 𝐹 ‘ 𝐶 ) ‘ 𝑘 ) ≤ 0 ∧ 0 ≤ ( ( 𝐹 ‘ 𝐶 ) ‘ 𝑘 ) ) ) )
220 14 216 219 mpbir2and ⊢ ( ( 𝜑 ∧ ( ( 𝑘 ∈ ( 1 ... 𝐽 ) ∧ ( ( 𝐹 ‘ 𝐶 ) ‘ 𝑘 ) ≤ 0 ) ∧ ∀ 𝑗 ∈ { 𝑖 ∈ ( 1 ... 𝐽 ) ∣ ( ( 𝐹 ‘ 𝐶 ) ‘ 𝑖 ) ≤ 0 } 𝑗 ≤ 𝑘 ) ) → ( ( 𝐹 ‘ 𝐶 ) ‘ 𝑘 ) = 0 )
221 13 220 sylan2b ⊢ ( ( 𝜑 ∧ ( 𝑘 ∈ { 𝑖 ∈ ( 1 ... 𝐽 ) ∣ ( ( 𝐹 ‘ 𝐶 ) ‘ 𝑖 ) ≤ 0 } ∧ ∀ 𝑗 ∈ { 𝑖 ∈ ( 1 ... 𝐽 ) ∣ ( ( 𝐹 ‘ 𝐶 ) ‘ 𝑖 ) ≤ 0 } 𝑗 ≤ 𝑘 ) ) → ( ( 𝐹 ‘ 𝐶 ) ‘ 𝑘 ) = 0 )
222 ssrab2 ⊢ { 𝑖 ∈ ( 1 ... 𝐽 ) ∣ ( ( 𝐹 ‘ 𝐶 ) ‘ 𝑖 ) ≤ 0 } ⊆ ( 1 ... 𝐽 )
223 222 21 sstri ⊢ { 𝑖 ∈ ( 1 ... 𝐽 ) ∣ ( ( 𝐹 ‘ 𝐶 ) ‘ 𝑖 ) ≤ 0 } ⊆ ℝ
224 223 a1i ⊢ ( 𝜑 → { 𝑖 ∈ ( 1 ... 𝐽 ) ∣ ( ( 𝐹 ‘ 𝐶 ) ‘ 𝑖 ) ≤ 0 } ⊆ ℝ )
225 fzfi ⊢ ( 1 ... 𝐽 ) ∈ Fin
226 ssfi ⊢ ( ( ( 1 ... 𝐽 ) ∈ Fin ∧ { 𝑖 ∈ ( 1 ... 𝐽 ) ∣ ( ( 𝐹 ‘ 𝐶 ) ‘ 𝑖 ) ≤ 0 } ⊆ ( 1 ... 𝐽 ) ) → { 𝑖 ∈ ( 1 ... 𝐽 ) ∣ ( ( 𝐹 ‘ 𝐶 ) ‘ 𝑖 ) ≤ 0 } ∈ Fin )
227 225 222 226 mp2an ⊢ { 𝑖 ∈ ( 1 ... 𝐽 ) ∣ ( ( 𝐹 ‘ 𝐶 ) ‘ 𝑖 ) ≤ 0 } ∈ Fin
228 227 a1i ⊢ ( 𝜑 → { 𝑖 ∈ ( 1 ... 𝐽 ) ∣ ( ( 𝐹 ‘ 𝐶 ) ‘ 𝑖 ) ≤ 0 } ∈ Fin )
229 rabn0 ⊢ ( { 𝑖 ∈ ( 1 ... 𝐽 ) ∣ ( ( 𝐹 ‘ 𝐶 ) ‘ 𝑖 ) ≤ 0 } ≠ ∅ ↔ ∃ 𝑖 ∈ ( 1 ... 𝐽 ) ( ( 𝐹 ‘ 𝐶 ) ‘ 𝑖 ) ≤ 0 )
230 8 229 sylibr ⊢ ( 𝜑 → { 𝑖 ∈ ( 1 ... 𝐽 ) ∣ ( ( 𝐹 ‘ 𝐶 ) ‘ 𝑖 ) ≤ 0 } ≠ ∅ )
231 fimaxre ⊢ ( ( { 𝑖 ∈ ( 1 ... 𝐽 ) ∣ ( ( 𝐹 ‘ 𝐶 ) ‘ 𝑖 ) ≤ 0 } ⊆ ℝ ∧ { 𝑖 ∈ ( 1 ... 𝐽 ) ∣ ( ( 𝐹 ‘ 𝐶 ) ‘ 𝑖 ) ≤ 0 } ∈ Fin ∧ { 𝑖 ∈ ( 1 ... 𝐽 ) ∣ ( ( 𝐹 ‘ 𝐶 ) ‘ 𝑖 ) ≤ 0 } ≠ ∅ ) → ∃ 𝑘 ∈ { 𝑖 ∈ ( 1 ... 𝐽 ) ∣ ( ( 𝐹 ‘ 𝐶 ) ‘ 𝑖 ) ≤ 0 } ∀ 𝑗 ∈ { 𝑖 ∈ ( 1 ... 𝐽 ) ∣ ( ( 𝐹 ‘ 𝐶 ) ‘ 𝑖 ) ≤ 0 } 𝑗 ≤ 𝑘 )
232 224 228 230 231 syl3anc ⊢ ( 𝜑 → ∃ 𝑘 ∈ { 𝑖 ∈ ( 1 ... 𝐽 ) ∣ ( ( 𝐹 ‘ 𝐶 ) ‘ 𝑖 ) ≤ 0 } ∀ 𝑗 ∈ { 𝑖 ∈ ( 1 ... 𝐽 ) ∣ ( ( 𝐹 ‘ 𝐶 ) ‘ 𝑖 ) ≤ 0 } 𝑗 ≤ 𝑘 )
233 221 232 reximddv ⊢ ( 𝜑 → ∃ 𝑘 ∈ { 𝑖 ∈ ( 1 ... 𝐽 ) ∣ ( ( 𝐹 ‘ 𝐶 ) ‘ 𝑖 ) ≤ 0 } ( ( 𝐹 ‘ 𝐶 ) ‘ 𝑘 ) = 0 )
234 elrabi ⊢ ( 𝑘 ∈ { 𝑖 ∈ ( 1 ... 𝐽 ) ∣ ( ( 𝐹 ‘ 𝐶 ) ‘ 𝑖 ) ≤ 0 } → 𝑘 ∈ ( 1 ... 𝐽 ) )
235 234 anim1i ⊢ ( ( 𝑘 ∈ { 𝑖 ∈ ( 1 ... 𝐽 ) ∣ ( ( 𝐹 ‘ 𝐶 ) ‘ 𝑖 ) ≤ 0 } ∧ ( ( 𝐹 ‘ 𝐶 ) ‘ 𝑘 ) = 0 ) → ( 𝑘 ∈ ( 1 ... 𝐽 ) ∧ ( ( 𝐹 ‘ 𝐶 ) ‘ 𝑘 ) = 0 ) )
236 235 reximi2 ⊢ ( ∃ 𝑘 ∈ { 𝑖 ∈ ( 1 ... 𝐽 ) ∣ ( ( 𝐹 ‘ 𝐶 ) ‘ 𝑖 ) ≤ 0 } ( ( 𝐹 ‘ 𝐶 ) ‘ 𝑘 ) = 0 → ∃ 𝑘 ∈ ( 1 ... 𝐽 ) ( ( 𝐹 ‘ 𝐶 ) ‘ 𝑘 ) = 0 )
237 233 236 syl ⊢ ( 𝜑 → ∃ 𝑘 ∈ ( 1 ... 𝐽 ) ( ( 𝐹 ‘ 𝐶 ) ‘ 𝑘 ) = 0 )