Metamath Proof Explorer

Theorem ballotlemfp1

Description: If the J th ballot is for A, ( FC ) goes up 1. If the J th ballot is for B, ( FC ) goes down 1. (Contributed by Thierry Arnoux, 24-Nov-2016)

Ref Expression
Hypotheses ballotth.m 
|- M e. NN
ballotth.n 
|- N e. NN
ballotth.o 
|- O = { c e. ~P ( 1 ... ( M + N ) ) | ( # ` c ) = M }
ballotth.p 
|- P = ( x e. ~P O |-> ( ( # ` x ) / ( # ` O ) ) )
ballotth.f 
|- F = ( c e. O |-> ( i e. ZZ |-> ( ( # ` ( ( 1 ... i ) i^i c ) ) - ( # ` ( ( 1 ... i ) \ c ) ) ) ) )
ballotlemfp1.c 
|- ( ph -> C e. O )
ballotlemfp1.j 
|- ( ph -> J e. NN )
Assertion ballotlemfp1 
|- ( ph -> ( ( -. J e. C -> ( ( F ` C ) ` J ) = ( ( ( F ` C ) ` ( J - 1 ) ) - 1 ) ) /\ ( J e. C -> ( ( F ` C ) ` J ) = ( ( ( F ` C ) ` ( J - 1 ) ) + 1 ) ) ) )

Proof

Step Hyp Ref Expression
1 ballotth.m 
 |-  M e. NN
2 ballotth.n 
 |-  N e. NN
3 ballotth.o 
 |-  O = { c e. ~P ( 1 ... ( M + N ) ) | ( # ` c ) = M }
4 ballotth.p 
 |-  P = ( x e. ~P O |-> ( ( # ` x ) / ( # ` O ) ) )
5 ballotth.f 
 |-  F = ( c e. O |-> ( i e. ZZ |-> ( ( # ` ( ( 1 ... i ) i^i c ) ) - ( # ` ( ( 1 ... i ) \ c ) ) ) ) )
6 ballotlemfp1.c 
 |-  ( ph -> C e. O )
7 ballotlemfp1.j 
 |-  ( ph -> J e. NN )
8 7 nnzd 
 |-  ( ph -> J e. ZZ )
9 1 2 3 4 5 6 8 ballotlemfval 
 |-  ( ph -> ( ( F ` C ) ` J ) = ( ( # ` ( ( 1 ... J ) i^i C ) ) - ( # ` ( ( 1 ... J ) \ C ) ) ) )
10 9 adantr 
 |-  ( ( ph /\ -. J e. C ) -> ( ( F ` C ) ` J ) = ( ( # ` ( ( 1 ... J ) i^i C ) ) - ( # ` ( ( 1 ... J ) \ C ) ) ) )
11 fzfi 
 |-  ( 1 ... ( J - 1 ) ) e. Fin
12 inss1 
 |-  ( ( 1 ... ( J - 1 ) ) i^i C ) C_ ( 1 ... ( J - 1 ) )
13 ssfi 
 |-  ( ( ( 1 ... ( J - 1 ) ) e. Fin /\ ( ( 1 ... ( J - 1 ) ) i^i C ) C_ ( 1 ... ( J - 1 ) ) ) -> ( ( 1 ... ( J - 1 ) ) i^i C ) e. Fin )
14 11 12 13 mp2an 
 |-  ( ( 1 ... ( J - 1 ) ) i^i C ) e. Fin
15 hashcl 
 |-  ( ( ( 1 ... ( J - 1 ) ) i^i C ) e. Fin -> ( # ` ( ( 1 ... ( J - 1 ) ) i^i C ) ) e. NN0 )
16 14 15 ax-mp 
 |-  ( # ` ( ( 1 ... ( J - 1 ) ) i^i C ) ) e. NN0
17 16 nn0cni 
 |-  ( # ` ( ( 1 ... ( J - 1 ) ) i^i C ) ) e. CC
18 17 a1i 
 |-  ( ( ph /\ -. J e. C ) -> ( # ` ( ( 1 ... ( J - 1 ) ) i^i C ) ) e. CC )
19 diffi 
 |-  ( ( 1 ... ( J - 1 ) ) e. Fin -> ( ( 1 ... ( J - 1 ) ) \ C ) e. Fin )
20 11 19 ax-mp 
 |-  ( ( 1 ... ( J - 1 ) ) \ C ) e. Fin
21 hashcl 
 |-  ( ( ( 1 ... ( J - 1 ) ) \ C ) e. Fin -> ( # ` ( ( 1 ... ( J - 1 ) ) \ C ) ) e. NN0 )
22 20 21 ax-mp 
 |-  ( # ` ( ( 1 ... ( J - 1 ) ) \ C ) ) e. NN0
23 22 nn0cni 
 |-  ( # ` ( ( 1 ... ( J - 1 ) ) \ C ) ) e. CC
24 23 a1i 
 |-  ( ( ph /\ -. J e. C ) -> ( # ` ( ( 1 ... ( J - 1 ) ) \ C ) ) e. CC )
25 1cnd 
 |-  ( ( ph /\ -. J e. C ) -> 1 e. CC )
26 18 24 25 subsub4d 
 |-  ( ( ph /\ -. J e. C ) -> ( ( ( # ` ( ( 1 ... ( J - 1 ) ) i^i C ) ) - ( # ` ( ( 1 ... ( J - 1 ) ) \ C ) ) ) - 1 ) = ( ( # ` ( ( 1 ... ( J - 1 ) ) i^i C ) ) - ( ( # ` ( ( 1 ... ( J - 1 ) ) \ C ) ) + 1 ) ) )
27 1zzd 
 |-  ( ph -> 1 e. ZZ )
28 8 27 zsubcld 
 |-  ( ph -> ( J - 1 ) e. ZZ )
29 1 2 3 4 5 6 28 ballotlemfval 
 |-  ( ph -> ( ( F ` C ) ` ( J - 1 ) ) = ( ( # ` ( ( 1 ... ( J - 1 ) ) i^i C ) ) - ( # ` ( ( 1 ... ( J - 1 ) ) \ C ) ) ) )
30 29 adantr 
 |-  ( ( ph /\ -. J e. C ) -> ( ( F ` C ) ` ( J - 1 ) ) = ( ( # ` ( ( 1 ... ( J - 1 ) ) i^i C ) ) - ( # ` ( ( 1 ... ( J - 1 ) ) \ C ) ) ) )
31 30 oveq1d 
 |-  ( ( ph /\ -. J e. C ) -> ( ( ( F ` C ) ` ( J - 1 ) ) - 1 ) = ( ( ( # ` ( ( 1 ... ( J - 1 ) ) i^i C ) ) - ( # ` ( ( 1 ... ( J - 1 ) ) \ C ) ) ) - 1 ) )
32 elnnuz 
 |-  ( J e. NN <-> J e. ( ZZ>= ` 1 ) )
33 7 32 sylib 
 |-  ( ph -> J e. ( ZZ>= ` 1 ) )
34 fzspl 
 |-  ( J e. ( ZZ>= ` 1 ) -> ( 1 ... J ) = ( ( 1 ... ( J - 1 ) ) u. { J } ) )
35 34 ineq1d 
 |-  ( J e. ( ZZ>= ` 1 ) -> ( ( 1 ... J ) i^i C ) = ( ( ( 1 ... ( J - 1 ) ) u. { J } ) i^i C ) )
36 indir 
 |-  ( ( ( 1 ... ( J - 1 ) ) u. { J } ) i^i C ) = ( ( ( 1 ... ( J - 1 ) ) i^i C ) u. ( { J } i^i C ) )
37 35 36 eqtrdi 
 |-  ( J e. ( ZZ>= ` 1 ) -> ( ( 1 ... J ) i^i C ) = ( ( ( 1 ... ( J - 1 ) ) i^i C ) u. ( { J } i^i C ) ) )
38 33 37 syl 
 |-  ( ph -> ( ( 1 ... J ) i^i C ) = ( ( ( 1 ... ( J - 1 ) ) i^i C ) u. ( { J } i^i C ) ) )
39 38 adantr 
 |-  ( ( ph /\ -. J e. C ) -> ( ( 1 ... J ) i^i C ) = ( ( ( 1 ... ( J - 1 ) ) i^i C ) u. ( { J } i^i C ) ) )
40 disjsn 
 |-  ( ( C i^i { J } ) = (/) <-> -. J e. C )
41 incom 
 |-  ( C i^i { J } ) = ( { J } i^i C )
42 41 eqeq1i 
 |-  ( ( C i^i { J } ) = (/) <-> ( { J } i^i C ) = (/) )
43 40 42 sylbb1 
 |-  ( -. J e. C -> ( { J } i^i C ) = (/) )
44 43 adantl 
 |-  ( ( ph /\ -. J e. C ) -> ( { J } i^i C ) = (/) )
45 44 uneq2d 
 |-  ( ( ph /\ -. J e. C ) -> ( ( ( 1 ... ( J - 1 ) ) i^i C ) u. ( { J } i^i C ) ) = ( ( ( 1 ... ( J - 1 ) ) i^i C ) u. (/) ) )
46 un0 
 |-  ( ( ( 1 ... ( J - 1 ) ) i^i C ) u. (/) ) = ( ( 1 ... ( J - 1 ) ) i^i C )
47 45 46 eqtrdi 
 |-  ( ( ph /\ -. J e. C ) -> ( ( ( 1 ... ( J - 1 ) ) i^i C ) u. ( { J } i^i C ) ) = ( ( 1 ... ( J - 1 ) ) i^i C ) )
48 39 47 eqtrd 
 |-  ( ( ph /\ -. J e. C ) -> ( ( 1 ... J ) i^i C ) = ( ( 1 ... ( J - 1 ) ) i^i C ) )
49 48 fveq2d 
 |-  ( ( ph /\ -. J e. C ) -> ( # ` ( ( 1 ... J ) i^i C ) ) = ( # ` ( ( 1 ... ( J - 1 ) ) i^i C ) ) )
50 34 difeq1d 
 |-  ( J e. ( ZZ>= ` 1 ) -> ( ( 1 ... J ) \ C ) = ( ( ( 1 ... ( J - 1 ) ) u. { J } ) \ C ) )
51 difundir 
 |-  ( ( ( 1 ... ( J - 1 ) ) u. { J } ) \ C ) = ( ( ( 1 ... ( J - 1 ) ) \ C ) u. ( { J } \ C ) )
52 50 51 eqtrdi 
 |-  ( J e. ( ZZ>= ` 1 ) -> ( ( 1 ... J ) \ C ) = ( ( ( 1 ... ( J - 1 ) ) \ C ) u. ( { J } \ C ) ) )
53 33 52 syl 
 |-  ( ph -> ( ( 1 ... J ) \ C ) = ( ( ( 1 ... ( J - 1 ) ) \ C ) u. ( { J } \ C ) ) )
54 disj3 
 |-  ( ( { J } i^i C ) = (/) <-> { J } = ( { J } \ C ) )
55 43 54 sylib 
 |-  ( -. J e. C -> { J } = ( { J } \ C ) )
56 55 eqcomd 
 |-  ( -. J e. C -> ( { J } \ C ) = { J } )
57 56 uneq2d 
 |-  ( -. J e. C -> ( ( ( 1 ... ( J - 1 ) ) \ C ) u. ( { J } \ C ) ) = ( ( ( 1 ... ( J - 1 ) ) \ C ) u. { J } ) )
58 53 57 sylan9eq 
 |-  ( ( ph /\ -. J e. C ) -> ( ( 1 ... J ) \ C ) = ( ( ( 1 ... ( J - 1 ) ) \ C ) u. { J } ) )
59 58 fveq2d 
 |-  ( ( ph /\ -. J e. C ) -> ( # ` ( ( 1 ... J ) \ C ) ) = ( # ` ( ( ( 1 ... ( J - 1 ) ) \ C ) u. { J } ) ) )
60 8 adantr 
 |-  ( ( ph /\ -. J e. C ) -> J e. ZZ )
61 uzid 
 |-  ( J e. ZZ -> J e. ( ZZ>= ` J ) )
62 uznfz 
 |-  ( J e. ( ZZ>= ` J ) -> -. J e. ( 1 ... ( J - 1 ) ) )
63 8 61 62 3syl 
 |-  ( ph -> -. J e. ( 1 ... ( J - 1 ) ) )
64 63 adantr 
 |-  ( ( ph /\ -. J e. C ) -> -. J e. ( 1 ... ( J - 1 ) ) )
65 difss 
 |-  ( ( 1 ... ( J - 1 ) ) \ C ) C_ ( 1 ... ( J - 1 ) )
66 65 sseli 
 |-  ( J e. ( ( 1 ... ( J - 1 ) ) \ C ) -> J e. ( 1 ... ( J - 1 ) ) )
67 64 66 nsyl 
 |-  ( ( ph /\ -. J e. C ) -> -. J e. ( ( 1 ... ( J - 1 ) ) \ C ) )
68 ssfi 
 |-  ( ( ( 1 ... ( J - 1 ) ) e. Fin /\ ( ( 1 ... ( J - 1 ) ) \ C ) C_ ( 1 ... ( J - 1 ) ) ) -> ( ( 1 ... ( J - 1 ) ) \ C ) e. Fin )
69 11 65 68 mp2an 
 |-  ( ( 1 ... ( J - 1 ) ) \ C ) e. Fin
70 67 69 jctil 
 |-  ( ( ph /\ -. J e. C ) -> ( ( ( 1 ... ( J - 1 ) ) \ C ) e. Fin /\ -. J e. ( ( 1 ... ( J - 1 ) ) \ C ) ) )
71 hashunsng 
 |-  ( J e. ZZ -> ( ( ( ( 1 ... ( J - 1 ) ) \ C ) e. Fin /\ -. J e. ( ( 1 ... ( J - 1 ) ) \ C ) ) -> ( # ` ( ( ( 1 ... ( J - 1 ) ) \ C ) u. { J } ) ) = ( ( # ` ( ( 1 ... ( J - 1 ) ) \ C ) ) + 1 ) ) )
72 60 70 71 sylc 
 |-  ( ( ph /\ -. J e. C ) -> ( # ` ( ( ( 1 ... ( J - 1 ) ) \ C ) u. { J } ) ) = ( ( # ` ( ( 1 ... ( J - 1 ) ) \ C ) ) + 1 ) )
73 59 72 eqtrd 
 |-  ( ( ph /\ -. J e. C ) -> ( # ` ( ( 1 ... J ) \ C ) ) = ( ( # ` ( ( 1 ... ( J - 1 ) ) \ C ) ) + 1 ) )
74 49 73 oveq12d 
 |-  ( ( ph /\ -. J e. C ) -> ( ( # ` ( ( 1 ... J ) i^i C ) ) - ( # ` ( ( 1 ... J ) \ C ) ) ) = ( ( # ` ( ( 1 ... ( J - 1 ) ) i^i C ) ) - ( ( # ` ( ( 1 ... ( J - 1 ) ) \ C ) ) + 1 ) ) )
75 26 31 74 3eqtr4rd 
 |-  ( ( ph /\ -. J e. C ) -> ( ( # ` ( ( 1 ... J ) i^i C ) ) - ( # ` ( ( 1 ... J ) \ C ) ) ) = ( ( ( F ` C ) ` ( J - 1 ) ) - 1 ) )
76 10 75 eqtrd 
 |-  ( ( ph /\ -. J e. C ) -> ( ( F ` C ) ` J ) = ( ( ( F ` C ) ` ( J - 1 ) ) - 1 ) )
77 76 ex 
 |-  ( ph -> ( -. J e. C -> ( ( F ` C ) ` J ) = ( ( ( F ` C ) ` ( J - 1 ) ) - 1 ) ) )
78 9 adantr 
 |-  ( ( ph /\ J e. C ) -> ( ( F ` C ) ` J ) = ( ( # ` ( ( 1 ... J ) i^i C ) ) - ( # ` ( ( 1 ... J ) \ C ) ) ) )
79 17 a1i 
 |-  ( ( ph /\ J e. C ) -> ( # ` ( ( 1 ... ( J - 1 ) ) i^i C ) ) e. CC )
80 1cnd 
 |-  ( ( ph /\ J e. C ) -> 1 e. CC )
81 23 a1i 
 |-  ( ( ph /\ J e. C ) -> ( # ` ( ( 1 ... ( J - 1 ) ) \ C ) ) e. CC )
82 79 80 81 addsubd 
 |-  ( ( ph /\ J e. C ) -> ( ( ( # ` ( ( 1 ... ( J - 1 ) ) i^i C ) ) + 1 ) - ( # ` ( ( 1 ... ( J - 1 ) ) \ C ) ) ) = ( ( ( # ` ( ( 1 ... ( J - 1 ) ) i^i C ) ) - ( # ` ( ( 1 ... ( J - 1 ) ) \ C ) ) ) + 1 ) )
83 38 fveq2d 
 |-  ( ph -> ( # ` ( ( 1 ... J ) i^i C ) ) = ( # ` ( ( ( 1 ... ( J - 1 ) ) i^i C ) u. ( { J } i^i C ) ) ) )
84 83 adantr 
 |-  ( ( ph /\ J e. C ) -> ( # ` ( ( 1 ... J ) i^i C ) ) = ( # ` ( ( ( 1 ... ( J - 1 ) ) i^i C ) u. ( { J } i^i C ) ) ) )
85 snssi 
 |-  ( J e. C -> { J } C_ C )
86 df-ss 
 |-  ( { J } C_ C <-> ( { J } i^i C ) = { J } )
87 85 86 sylib 
 |-  ( J e. C -> ( { J } i^i C ) = { J } )
88 87 uneq2d 
 |-  ( J e. C -> ( ( ( 1 ... ( J - 1 ) ) i^i C ) u. ( { J } i^i C ) ) = ( ( ( 1 ... ( J - 1 ) ) i^i C ) u. { J } ) )
89 88 fveq2d 
 |-  ( J e. C -> ( # ` ( ( ( 1 ... ( J - 1 ) ) i^i C ) u. ( { J } i^i C ) ) ) = ( # ` ( ( ( 1 ... ( J - 1 ) ) i^i C ) u. { J } ) ) )
90 89 adantl 
 |-  ( ( ph /\ J e. C ) -> ( # ` ( ( ( 1 ... ( J - 1 ) ) i^i C ) u. ( { J } i^i C ) ) ) = ( # ` ( ( ( 1 ... ( J - 1 ) ) i^i C ) u. { J } ) ) )
91 simpr 
 |-  ( ( ph /\ J e. C ) -> J e. C )
92 8 adantr 
 |-  ( ( ph /\ J e. C ) -> J e. ZZ )
93 92 61 62 3syl 
 |-  ( ( ph /\ J e. C ) -> -. J e. ( 1 ... ( J - 1 ) ) )
94 12 sseli 
 |-  ( J e. ( ( 1 ... ( J - 1 ) ) i^i C ) -> J e. ( 1 ... ( J - 1 ) ) )
95 93 94 nsyl 
 |-  ( ( ph /\ J e. C ) -> -. J e. ( ( 1 ... ( J - 1 ) ) i^i C ) )
96 95 14 jctil 
 |-  ( ( ph /\ J e. C ) -> ( ( ( 1 ... ( J - 1 ) ) i^i C ) e. Fin /\ -. J e. ( ( 1 ... ( J - 1 ) ) i^i C ) ) )
97 hashunsng 
 |-  ( J e. C -> ( ( ( ( 1 ... ( J - 1 ) ) i^i C ) e. Fin /\ -. J e. ( ( 1 ... ( J - 1 ) ) i^i C ) ) -> ( # ` ( ( ( 1 ... ( J - 1 ) ) i^i C ) u. { J } ) ) = ( ( # ` ( ( 1 ... ( J - 1 ) ) i^i C ) ) + 1 ) ) )
98 91 96 97 sylc 
 |-  ( ( ph /\ J e. C ) -> ( # ` ( ( ( 1 ... ( J - 1 ) ) i^i C ) u. { J } ) ) = ( ( # ` ( ( 1 ... ( J - 1 ) ) i^i C ) ) + 1 ) )
99 84 90 98 3eqtrd 
 |-  ( ( ph /\ J e. C ) -> ( # ` ( ( 1 ... J ) i^i C ) ) = ( ( # ` ( ( 1 ... ( J - 1 ) ) i^i C ) ) + 1 ) )
100 53 fveq2d 
 |-  ( ph -> ( # ` ( ( 1 ... J ) \ C ) ) = ( # ` ( ( ( 1 ... ( J - 1 ) ) \ C ) u. ( { J } \ C ) ) ) )
101 100 adantr 
 |-  ( ( ph /\ J e. C ) -> ( # ` ( ( 1 ... J ) \ C ) ) = ( # ` ( ( ( 1 ... ( J - 1 ) ) \ C ) u. ( { J } \ C ) ) ) )
102 difin2 
 |-  ( { J } C_ C -> ( { J } \ C ) = ( ( C \ C ) i^i { J } ) )
103 difid 
 |-  ( C \ C ) = (/)
104 103 ineq1i 
 |-  ( ( C \ C ) i^i { J } ) = ( (/) i^i { J } )
105 0in 
 |-  ( (/) i^i { J } ) = (/)
106 104 105 eqtri 
 |-  ( ( C \ C ) i^i { J } ) = (/)
107 102 106 eqtrdi 
 |-  ( { J } C_ C -> ( { J } \ C ) = (/) )
108 85 107 syl 
 |-  ( J e. C -> ( { J } \ C ) = (/) )
109 108 uneq2d 
 |-  ( J e. C -> ( ( ( 1 ... ( J - 1 ) ) \ C ) u. ( { J } \ C ) ) = ( ( ( 1 ... ( J - 1 ) ) \ C ) u. (/) ) )
110 109 fveq2d 
 |-  ( J e. C -> ( # ` ( ( ( 1 ... ( J - 1 ) ) \ C ) u. ( { J } \ C ) ) ) = ( # ` ( ( ( 1 ... ( J - 1 ) ) \ C ) u. (/) ) ) )
111 110 adantl 
 |-  ( ( ph /\ J e. C ) -> ( # ` ( ( ( 1 ... ( J - 1 ) ) \ C ) u. ( { J } \ C ) ) ) = ( # ` ( ( ( 1 ... ( J - 1 ) ) \ C ) u. (/) ) ) )
112 un0 
 |-  ( ( ( 1 ... ( J - 1 ) ) \ C ) u. (/) ) = ( ( 1 ... ( J - 1 ) ) \ C )
113 112 a1i 
 |-  ( ( ph /\ J e. C ) -> ( ( ( 1 ... ( J - 1 ) ) \ C ) u. (/) ) = ( ( 1 ... ( J - 1 ) ) \ C ) )
114 113 fveq2d 
 |-  ( ( ph /\ J e. C ) -> ( # ` ( ( ( 1 ... ( J - 1 ) ) \ C ) u. (/) ) ) = ( # ` ( ( 1 ... ( J - 1 ) ) \ C ) ) )
115 101 111 114 3eqtrd 
 |-  ( ( ph /\ J e. C ) -> ( # ` ( ( 1 ... J ) \ C ) ) = ( # ` ( ( 1 ... ( J - 1 ) ) \ C ) ) )
116 99 115 oveq12d 
 |-  ( ( ph /\ J e. C ) -> ( ( # ` ( ( 1 ... J ) i^i C ) ) - ( # ` ( ( 1 ... J ) \ C ) ) ) = ( ( ( # ` ( ( 1 ... ( J - 1 ) ) i^i C ) ) + 1 ) - ( # ` ( ( 1 ... ( J - 1 ) ) \ C ) ) ) )
117 29 adantr 
 |-  ( ( ph /\ J e. C ) -> ( ( F ` C ) ` ( J - 1 ) ) = ( ( # ` ( ( 1 ... ( J - 1 ) ) i^i C ) ) - ( # ` ( ( 1 ... ( J - 1 ) ) \ C ) ) ) )
118 117 oveq1d 
 |-  ( ( ph /\ J e. C ) -> ( ( ( F ` C ) ` ( J - 1 ) ) + 1 ) = ( ( ( # ` ( ( 1 ... ( J - 1 ) ) i^i C ) ) - ( # ` ( ( 1 ... ( J - 1 ) ) \ C ) ) ) + 1 ) )
119 82 116 118 3eqtr4d 
 |-  ( ( ph /\ J e. C ) -> ( ( # ` ( ( 1 ... J ) i^i C ) ) - ( # ` ( ( 1 ... J ) \ C ) ) ) = ( ( ( F ` C ) ` ( J - 1 ) ) + 1 ) )
120 78 119 eqtrd 
 |-  ( ( ph /\ J e. C ) -> ( ( F ` C ) ` J ) = ( ( ( F ` C ) ` ( J - 1 ) ) + 1 ) )
121 120 ex 
 |-  ( ph -> ( J e. C -> ( ( F ` C ) ` J ) = ( ( ( F ` C ) ` ( J - 1 ) ) + 1 ) ) )
122 77 121 jca 
 |-  ( ph -> ( ( -. J e. C -> ( ( F ` C ) ` J ) = ( ( ( F ` C ) ` ( J - 1 ) ) - 1 ) ) /\ ( J e. C -> ( ( F ` C ) ` J ) = ( ( ( F ` C ) ` ( J - 1 ) ) + 1 ) ) ) )