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