Metamath Proof Explorer

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 )