Metamath Proof Explorer

Theorem poimirlem28

Description: Lemma for poimir , a variant of Sperner's lemma. (Contributed by Brendan Leahy, 21-Aug-2020)

Ref Expression
Hypotheses poimir.0 
|- ( ph -> N e. NN )
poimirlem28.1 
|- ( p = ( ( 1st ` s ) oF + ( ( ( ( 2nd ` s ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` s ) " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) -> B = C )
poimirlem28.2 
|- ( ( ph /\ p : ( 1 ... N ) --> ( 0 ... K ) ) -> B e. ( 0 ... N ) )
poimirlem28.3 
|- ( ( ph /\ ( n e. ( 1 ... N ) /\ p : ( 1 ... N ) --> ( 0 ... K ) /\ ( p ` n ) = 0 ) ) -> B < n )
poimirlem28.4 
|- ( ( ph /\ ( n e. ( 1 ... N ) /\ p : ( 1 ... N ) --> ( 0 ... K ) /\ ( p ` n ) = K ) ) -> B =/= ( n - 1 ) )
poimirlem28.5 
|- ( ph -> K e. NN )
Assertion poimirlem28 
|- ( ph -> E. s e. ( ( ( 0 ..^ K ) ^m ( 1 ... N ) ) X. { f | f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } ) A. i e. ( 0 ... N ) E. j e. ( 0 ... N ) i = C )

Proof

Step Hyp Ref Expression
1 poimir.0 
 |-  ( ph -> N e. NN )
2 poimirlem28.1 
 |-  ( p = ( ( 1st ` s ) oF + ( ( ( ( 2nd ` s ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` s ) " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) -> B = C )
3 poimirlem28.2 
 |-  ( ( ph /\ p : ( 1 ... N ) --> ( 0 ... K ) ) -> B e. ( 0 ... N ) )
4 poimirlem28.3 
 |-  ( ( ph /\ ( n e. ( 1 ... N ) /\ p : ( 1 ... N ) --> ( 0 ... K ) /\ ( p ` n ) = 0 ) ) -> B < n )
5 poimirlem28.4 
 |-  ( ( ph /\ ( n e. ( 1 ... N ) /\ p : ( 1 ... N ) --> ( 0 ... K ) /\ ( p ` n ) = K ) ) -> B =/= ( n - 1 ) )
6 poimirlem28.5 
 |-  ( ph -> K e. NN )
7 1 nnnn0d 
 |-  ( ph -> N e. NN0 )
8 1 nnred 
 |-  ( ph -> N e. RR )
9 8 leidd 
 |-  ( ph -> N <_ N )
10 7 7 9 3jca 
 |-  ( ph -> ( N e. NN0 /\ N e. NN0 /\ N <_ N ) )
11 oveq2 
 |-  ( k = 0 -> ( 1 ... k ) = ( 1 ... 0 ) )
12 fz10 
 |-  ( 1 ... 0 ) = (/)
13 11 12 eqtrdi 
 |-  ( k = 0 -> ( 1 ... k ) = (/) )
14 13 oveq2d 
 |-  ( k = 0 -> ( ( 0 ..^ K ) ^m ( 1 ... k ) ) = ( ( 0 ..^ K ) ^m (/) ) )
15 fzofi 
 |-  ( 0 ..^ K ) e. Fin
16 map0e 
 |-  ( ( 0 ..^ K ) e. Fin -> ( ( 0 ..^ K ) ^m (/) ) = 1o )
17 15 16 ax-mp 
 |-  ( ( 0 ..^ K ) ^m (/) ) = 1o
18 df1o2 
 |-  1o = { (/) }
19 17 18 eqtri 
 |-  ( ( 0 ..^ K ) ^m (/) ) = { (/) }
20 14 19 eqtrdi 
 |-  ( k = 0 -> ( ( 0 ..^ K ) ^m ( 1 ... k ) ) = { (/) } )
21 eqidd 
 |-  ( k = 0 -> f = f )
22 21 13 13 f1oeq123d 
 |-  ( k = 0 -> ( f : ( 1 ... k ) -1-1-onto-> ( 1 ... k ) <-> f : (/) -1-1-onto-> (/) ) )
23 eqid 
 |-  (/) = (/)
24 f1o00 
 |-  ( f : (/) -1-1-onto-> (/) <-> ( f = (/) /\ (/) = (/) ) )
25 23 24 mpbiran2 
 |-  ( f : (/) -1-1-onto-> (/) <-> f = (/) )
26 22 25 bitrdi 
 |-  ( k = 0 -> ( f : ( 1 ... k ) -1-1-onto-> ( 1 ... k ) <-> f = (/) ) )
27 26 abbidv 
 |-  ( k = 0 -> { f | f : ( 1 ... k ) -1-1-onto-> ( 1 ... k ) } = { f | f = (/) } )
28 df-sn 
 |-  { (/) } = { f | f = (/) }
29 27 28 eqtr4di 
 |-  ( k = 0 -> { f | f : ( 1 ... k ) -1-1-onto-> ( 1 ... k ) } = { (/) } )
30 20 29 xpeq12d 
 |-  ( k = 0 -> ( ( ( 0 ..^ K ) ^m ( 1 ... k ) ) X. { f | f : ( 1 ... k ) -1-1-onto-> ( 1 ... k ) } ) = ( { (/) } X. { (/) } ) )
31 0ex 
 |-  (/) e. _V
32 31 31 xpsn 
 |-  ( { (/) } X. { (/) } ) = { <. (/) , (/) >. }
33 30 32 eqtr2di 
 |-  ( k = 0 -> { <. (/) , (/) >. } = ( ( ( 0 ..^ K ) ^m ( 1 ... k ) ) X. { f | f : ( 1 ... k ) -1-1-onto-> ( 1 ... k ) } ) )
34 elsni 
 |-  ( s e. { <. (/) , (/) >. } -> s = <. (/) , (/) >. )
35 31 31 op1std 
 |-  ( s = <. (/) , (/) >. -> ( 1st ` s ) = (/) )
36 34 35 syl 
 |-  ( s e. { <. (/) , (/) >. } -> ( 1st ` s ) = (/) )
37 36 oveq1d 
 |-  ( s e. { <. (/) , (/) >. } -> ( ( 1st ` s ) oF + (/) ) = ( (/) oF + (/) ) )
38 f0 
 |-  (/) : (/) --> (/)
39 ffn 
 |-  ( (/) : (/) --> (/) -> (/) Fn (/) )
40 38 39 mp1i 
 |-  ( s e. { <. (/) , (/) >. } -> (/) Fn (/) )
41 31 a1i 
 |-  ( s e. { <. (/) , (/) >. } -> (/) e. _V )
42 inidm 
 |-  ( (/) i^i (/) ) = (/)
43 0fv 
 |-  ( (/) ` n ) = (/)
44 43 a1i 
 |-  ( ( s e. { <. (/) , (/) >. } /\ n e. (/) ) -> ( (/) ` n ) = (/) )
45 40 40 41 41 42 44 44 offval 
 |-  ( s e. { <. (/) , (/) >. } -> ( (/) oF + (/) ) = ( n e. (/) |-> ( (/) + (/) ) ) )
46 mpt0 
 |-  ( n e. (/) |-> ( (/) + (/) ) ) = (/)
47 45 46 eqtrdi 
 |-  ( s e. { <. (/) , (/) >. } -> ( (/) oF + (/) ) = (/) )
48 37 47 eqtrd 
 |-  ( s e. { <. (/) , (/) >. } -> ( ( 1st ` s ) oF + (/) ) = (/) )
49 48 uneq1d 
 |-  ( s e. { <. (/) , (/) >. } -> ( ( ( 1st ` s ) oF + (/) ) u. ( ( 1 ... N ) X. { 0 } ) ) = ( (/) u. ( ( 1 ... N ) X. { 0 } ) ) )
50 uncom 
 |-  ( (/) u. ( ( 1 ... N ) X. { 0 } ) ) = ( ( ( 1 ... N ) X. { 0 } ) u. (/) )
51 un0 
 |-  ( ( ( 1 ... N ) X. { 0 } ) u. (/) ) = ( ( 1 ... N ) X. { 0 } )
52 50 51 eqtri 
 |-  ( (/) u. ( ( 1 ... N ) X. { 0 } ) ) = ( ( 1 ... N ) X. { 0 } )
53 49 52 eqtr2di 
 |-  ( s e. { <. (/) , (/) >. } -> ( ( 1 ... N ) X. { 0 } ) = ( ( ( 1st ` s ) oF + (/) ) u. ( ( 1 ... N ) X. { 0 } ) ) )
54 53 csbeq1d 
 |-  ( s e. { <. (/) , (/) >. } -> [_ ( ( 1 ... N ) X. { 0 } ) / p ]_ B = [_ ( ( ( 1st ` s ) oF + (/) ) u. ( ( 1 ... N ) X. { 0 } ) ) / p ]_ B )
55 54 eqeq2d 
 |-  ( s e. { <. (/) , (/) >. } -> ( 0 = [_ ( ( 1 ... N ) X. { 0 } ) / p ]_ B <-> 0 = [_ ( ( ( 1st ` s ) oF + (/) ) u. ( ( 1 ... N ) X. { 0 } ) ) / p ]_ B ) )
56 oveq2 
 |-  ( k = 0 -> ( 0 ... k ) = ( 0 ... 0 ) )
57 0z 
 |-  0 e. ZZ
58 fzsn 
 |-  ( 0 e. ZZ -> ( 0 ... 0 ) = { 0 } )
59 57 58 ax-mp 
 |-  ( 0 ... 0 ) = { 0 }
60 56 59 eqtrdi 
 |-  ( k = 0 -> ( 0 ... k ) = { 0 } )
61 oveq2 
 |-  ( k = 0 -> ( ( j + 1 ) ... k ) = ( ( j + 1 ) ... 0 ) )
62 61 imaeq2d 
 |-  ( k = 0 -> ( ( 2nd ` s ) " ( ( j + 1 ) ... k ) ) = ( ( 2nd ` s ) " ( ( j + 1 ) ... 0 ) ) )
63 62 xpeq1d 
 |-  ( k = 0 -> ( ( ( 2nd ` s ) " ( ( j + 1 ) ... k ) ) X. { 0 } ) = ( ( ( 2nd ` s ) " ( ( j + 1 ) ... 0 ) ) X. { 0 } ) )
64 63 uneq2d 
 |-  ( k = 0 -> ( ( ( ( 2nd ` s ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` s ) " ( ( j + 1 ) ... k ) ) X. { 0 } ) ) = ( ( ( ( 2nd ` s ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` s ) " ( ( j + 1 ) ... 0 ) ) X. { 0 } ) ) )
65 64 oveq2d 
 |-  ( k = 0 -> ( ( 1st ` s ) oF + ( ( ( ( 2nd ` s ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` s ) " ( ( j + 1 ) ... k ) ) X. { 0 } ) ) ) = ( ( 1st ` s ) oF + ( ( ( ( 2nd ` s ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` s ) " ( ( j + 1 ) ... 0 ) ) X. { 0 } ) ) ) )
66 oveq1 
 |-  ( k = 0 -> ( k + 1 ) = ( 0 + 1 ) )
67 0p1e1 
 |-  ( 0 + 1 ) = 1
68 66 67 eqtrdi 
 |-  ( k = 0 -> ( k + 1 ) = 1 )
69 68 oveq1d 
 |-  ( k = 0 -> ( ( k + 1 ) ... N ) = ( 1 ... N ) )
70 69 xpeq1d 
 |-  ( k = 0 -> ( ( ( k + 1 ) ... N ) X. { 0 } ) = ( ( 1 ... N ) X. { 0 } ) )
71 65 70 uneq12d 
 |-  ( k = 0 -> ( ( ( 1st ` s ) oF + ( ( ( ( 2nd ` s ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` s ) " ( ( j + 1 ) ... k ) ) X. { 0 } ) ) ) u. ( ( ( k + 1 ) ... N ) X. { 0 } ) ) = ( ( ( 1st ` s ) oF + ( ( ( ( 2nd ` s ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` s ) " ( ( j + 1 ) ... 0 ) ) X. { 0 } ) ) ) u. ( ( 1 ... N ) X. { 0 } ) ) )
72 71 csbeq1d 
 |-  ( k = 0 -> [_ ( ( ( 1st ` s ) oF + ( ( ( ( 2nd ` s ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` s ) " ( ( j + 1 ) ... k ) ) X. { 0 } ) ) ) u. ( ( ( k + 1 ) ... N ) X. { 0 } ) ) / p ]_ B = [_ ( ( ( 1st ` s ) oF + ( ( ( ( 2nd ` s ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` s ) " ( ( j + 1 ) ... 0 ) ) X. { 0 } ) ) ) u. ( ( 1 ... N ) X. { 0 } ) ) / p ]_ B )
73 72 eqeq2d 
 |-  ( k = 0 -> ( i = [_ ( ( ( 1st ` s ) oF + ( ( ( ( 2nd ` s ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` s ) " ( ( j + 1 ) ... k ) ) X. { 0 } ) ) ) u. ( ( ( k + 1 ) ... N ) X. { 0 } ) ) / p ]_ B <-> i = [_ ( ( ( 1st ` s ) oF + ( ( ( ( 2nd ` s ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` s ) " ( ( j + 1 ) ... 0 ) ) X. { 0 } ) ) ) u. ( ( 1 ... N ) X. { 0 } ) ) / p ]_ B ) )
74 60 73 rexeqbidv 
 |-  ( k = 0 -> ( E. j e. ( 0 ... k ) i = [_ ( ( ( 1st ` s ) oF + ( ( ( ( 2nd ` s ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` s ) " ( ( j + 1 ) ... k ) ) X. { 0 } ) ) ) u. ( ( ( k + 1 ) ... N ) X. { 0 } ) ) / p ]_ B <-> E. j e. { 0 } i = [_ ( ( ( 1st ` s ) oF + ( ( ( ( 2nd ` s ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` s ) " ( ( j + 1 ) ... 0 ) ) X. { 0 } ) ) ) u. ( ( 1 ... N ) X. { 0 } ) ) / p ]_ B ) )
75 c0ex 
 |-  0 e. _V
76 oveq2 
 |-  ( j = 0 -> ( 1 ... j ) = ( 1 ... 0 ) )
77 76 12 eqtrdi 
 |-  ( j = 0 -> ( 1 ... j ) = (/) )
78 77 imaeq2d 
 |-  ( j = 0 -> ( ( 2nd ` s ) " ( 1 ... j ) ) = ( ( 2nd ` s ) " (/) ) )
79 ima0 
 |-  ( ( 2nd ` s ) " (/) ) = (/)
80 78 79 eqtrdi 
 |-  ( j = 0 -> ( ( 2nd ` s ) " ( 1 ... j ) ) = (/) )
81 80 xpeq1d 
 |-  ( j = 0 -> ( ( ( 2nd ` s ) " ( 1 ... j ) ) X. { 1 } ) = ( (/) X. { 1 } ) )
82 0xp 
 |-  ( (/) X. { 1 } ) = (/)
83 81 82 eqtrdi 
 |-  ( j = 0 -> ( ( ( 2nd ` s ) " ( 1 ... j ) ) X. { 1 } ) = (/) )
84 oveq1 
 |-  ( j = 0 -> ( j + 1 ) = ( 0 + 1 ) )
85 84 67 eqtrdi 
 |-  ( j = 0 -> ( j + 1 ) = 1 )
86 85 oveq1d 
 |-  ( j = 0 -> ( ( j + 1 ) ... 0 ) = ( 1 ... 0 ) )
87 86 12 eqtrdi 
 |-  ( j = 0 -> ( ( j + 1 ) ... 0 ) = (/) )
88 87 imaeq2d 
 |-  ( j = 0 -> ( ( 2nd ` s ) " ( ( j + 1 ) ... 0 ) ) = ( ( 2nd ` s ) " (/) ) )
89 88 79 eqtrdi 
 |-  ( j = 0 -> ( ( 2nd ` s ) " ( ( j + 1 ) ... 0 ) ) = (/) )
90 89 xpeq1d 
 |-  ( j = 0 -> ( ( ( 2nd ` s ) " ( ( j + 1 ) ... 0 ) ) X. { 0 } ) = ( (/) X. { 0 } ) )
91 0xp 
 |-  ( (/) X. { 0 } ) = (/)
92 90 91 eqtrdi 
 |-  ( j = 0 -> ( ( ( 2nd ` s ) " ( ( j + 1 ) ... 0 ) ) X. { 0 } ) = (/) )
93 83 92 uneq12d 
 |-  ( j = 0 -> ( ( ( ( 2nd ` s ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` s ) " ( ( j + 1 ) ... 0 ) ) X. { 0 } ) ) = ( (/) u. (/) ) )
94 un0 
 |-  ( (/) u. (/) ) = (/)
95 93 94 eqtrdi 
 |-  ( j = 0 -> ( ( ( ( 2nd ` s ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` s ) " ( ( j + 1 ) ... 0 ) ) X. { 0 } ) ) = (/) )
96 95 oveq2d 
 |-  ( j = 0 -> ( ( 1st ` s ) oF + ( ( ( ( 2nd ` s ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` s ) " ( ( j + 1 ) ... 0 ) ) X. { 0 } ) ) ) = ( ( 1st ` s ) oF + (/) ) )
97 96 uneq1d 
 |-  ( j = 0 -> ( ( ( 1st ` s ) oF + ( ( ( ( 2nd ` s ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` s ) " ( ( j + 1 ) ... 0 ) ) X. { 0 } ) ) ) u. ( ( 1 ... N ) X. { 0 } ) ) = ( ( ( 1st ` s ) oF + (/) ) u. ( ( 1 ... N ) X. { 0 } ) ) )
98 97 csbeq1d 
 |-  ( j = 0 -> [_ ( ( ( 1st ` s ) oF + ( ( ( ( 2nd ` s ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` s ) " ( ( j + 1 ) ... 0 ) ) X. { 0 } ) ) ) u. ( ( 1 ... N ) X. { 0 } ) ) / p ]_ B = [_ ( ( ( 1st ` s ) oF + (/) ) u. ( ( 1 ... N ) X. { 0 } ) ) / p ]_ B )
99 98 eqeq2d 
 |-  ( j = 0 -> ( i = [_ ( ( ( 1st ` s ) oF + ( ( ( ( 2nd ` s ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` s ) " ( ( j + 1 ) ... 0 ) ) X. { 0 } ) ) ) u. ( ( 1 ... N ) X. { 0 } ) ) / p ]_ B <-> i = [_ ( ( ( 1st ` s ) oF + (/) ) u. ( ( 1 ... N ) X. { 0 } ) ) / p ]_ B ) )
100 75 99 rexsn 
 |-  ( E. j e. { 0 } i = [_ ( ( ( 1st ` s ) oF + ( ( ( ( 2nd ` s ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` s ) " ( ( j + 1 ) ... 0 ) ) X. { 0 } ) ) ) u. ( ( 1 ... N ) X. { 0 } ) ) / p ]_ B <-> i = [_ ( ( ( 1st ` s ) oF + (/) ) u. ( ( 1 ... N ) X. { 0 } ) ) / p ]_ B )
101 74 100 bitrdi 
 |-  ( k = 0 -> ( E. j e. ( 0 ... k ) i = [_ ( ( ( 1st ` s ) oF + ( ( ( ( 2nd ` s ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` s ) " ( ( j + 1 ) ... k ) ) X. { 0 } ) ) ) u. ( ( ( k + 1 ) ... N ) X. { 0 } ) ) / p ]_ B <-> i = [_ ( ( ( 1st ` s ) oF + (/) ) u. ( ( 1 ... N ) X. { 0 } ) ) / p ]_ B ) )
102 60 101 raleqbidv 
 |-  ( k = 0 -> ( A. i e. ( 0 ... k ) E. j e. ( 0 ... k ) i = [_ ( ( ( 1st ` s ) oF + ( ( ( ( 2nd ` s ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` s ) " ( ( j + 1 ) ... k ) ) X. { 0 } ) ) ) u. ( ( ( k + 1 ) ... N ) X. { 0 } ) ) / p ]_ B <-> A. i e. { 0 } i = [_ ( ( ( 1st ` s ) oF + (/) ) u. ( ( 1 ... N ) X. { 0 } ) ) / p ]_ B ) )
103 eqeq1 
 |-  ( i = 0 -> ( i = [_ ( ( ( 1st ` s ) oF + (/) ) u. ( ( 1 ... N ) X. { 0 } ) ) / p ]_ B <-> 0 = [_ ( ( ( 1st ` s ) oF + (/) ) u. ( ( 1 ... N ) X. { 0 } ) ) / p ]_ B ) )
104 75 103 ralsn 
 |-  ( A. i e. { 0 } i = [_ ( ( ( 1st ` s ) oF + (/) ) u. ( ( 1 ... N ) X. { 0 } ) ) / p ]_ B <-> 0 = [_ ( ( ( 1st ` s ) oF + (/) ) u. ( ( 1 ... N ) X. { 0 } ) ) / p ]_ B )
105 102 104 bitr2di 
 |-  ( k = 0 -> ( 0 = [_ ( ( ( 1st ` s ) oF + (/) ) u. ( ( 1 ... N ) X. { 0 } ) ) / p ]_ B <-> A. i e. ( 0 ... k ) E. j e. ( 0 ... k ) i = [_ ( ( ( 1st ` s ) oF + ( ( ( ( 2nd ` s ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` s ) " ( ( j + 1 ) ... k ) ) X. { 0 } ) ) ) u. ( ( ( k + 1 ) ... N ) X. { 0 } ) ) / p ]_ B ) )
106 55 105 sylan9bbr 
 |-  ( ( k = 0 /\ s e. { <. (/) , (/) >. } ) -> ( 0 = [_ ( ( 1 ... N ) X. { 0 } ) / p ]_ B <-> A. i e. ( 0 ... k ) E. j e. ( 0 ... k ) i = [_ ( ( ( 1st ` s ) oF + ( ( ( ( 2nd ` s ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` s ) " ( ( j + 1 ) ... k ) ) X. { 0 } ) ) ) u. ( ( ( k + 1 ) ... N ) X. { 0 } ) ) / p ]_ B ) )
107 33 106 rabeqbidva 
 |-  ( k = 0 -> { s e. { <. (/) , (/) >. } | 0 = [_ ( ( 1 ... N ) X. { 0 } ) / p ]_ B } = { s e. ( ( ( 0 ..^ K ) ^m ( 1 ... k ) ) X. { f | f : ( 1 ... k ) -1-1-onto-> ( 1 ... k ) } ) | A. i e. ( 0 ... k ) E. j e. ( 0 ... k ) i = [_ ( ( ( 1st ` s ) oF + ( ( ( ( 2nd ` s ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` s ) " ( ( j + 1 ) ... k ) ) X. { 0 } ) ) ) u. ( ( ( k + 1 ) ... N ) X. { 0 } ) ) / p ]_ B } )
108 107 eqcomd 
 |-  ( k = 0 -> { s e. ( ( ( 0 ..^ K ) ^m ( 1 ... k ) ) X. { f | f : ( 1 ... k ) -1-1-onto-> ( 1 ... k ) } ) | A. i e. ( 0 ... k ) E. j e. ( 0 ... k ) i = [_ ( ( ( 1st ` s ) oF + ( ( ( ( 2nd ` s ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` s ) " ( ( j + 1 ) ... k ) ) X. { 0 } ) ) ) u. ( ( ( k + 1 ) ... N ) X. { 0 } ) ) / p ]_ B } = { s e. { <. (/) , (/) >. } | 0 = [_ ( ( 1 ... N ) X. { 0 } ) / p ]_ B } )
109 108 fveq2d 
 |-  ( k = 0 -> ( # ` { s e. ( ( ( 0 ..^ K ) ^m ( 1 ... k ) ) X. { f | f : ( 1 ... k ) -1-1-onto-> ( 1 ... k ) } ) | A. i e. ( 0 ... k ) E. j e. ( 0 ... k ) i = [_ ( ( ( 1st ` s ) oF + ( ( ( ( 2nd ` s ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` s ) " ( ( j + 1 ) ... k ) ) X. { 0 } ) ) ) u. ( ( ( k + 1 ) ... N ) X. { 0 } ) ) / p ]_ B } ) = ( # ` { s e. { <. (/) , (/) >. } | 0 = [_ ( ( 1 ... N ) X. { 0 } ) / p ]_ B } ) )
110 109 breq2d 
 |-  ( k = 0 -> ( 2 || ( # ` { s e. ( ( ( 0 ..^ K ) ^m ( 1 ... k ) ) X. { f | f : ( 1 ... k ) -1-1-onto-> ( 1 ... k ) } ) | A. i e. ( 0 ... k ) E. j e. ( 0 ... k ) i = [_ ( ( ( 1st ` s ) oF + ( ( ( ( 2nd ` s ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` s ) " ( ( j + 1 ) ... k ) ) X. { 0 } ) ) ) u. ( ( ( k + 1 ) ... N ) X. { 0 } ) ) / p ]_ B } ) <-> 2 || ( # ` { s e. { <. (/) , (/) >. } | 0 = [_ ( ( 1 ... N ) X. { 0 } ) / p ]_ B } ) ) )
111 110 notbid 
 |-  ( k = 0 -> ( -. 2 || ( # ` { s e. ( ( ( 0 ..^ K ) ^m ( 1 ... k ) ) X. { f | f : ( 1 ... k ) -1-1-onto-> ( 1 ... k ) } ) | A. i e. ( 0 ... k ) E. j e. ( 0 ... k ) i = [_ ( ( ( 1st ` s ) oF + ( ( ( ( 2nd ` s ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` s ) " ( ( j + 1 ) ... k ) ) X. { 0 } ) ) ) u. ( ( ( k + 1 ) ... N ) X. { 0 } ) ) / p ]_ B } ) <-> -. 2 || ( # ` { s e. { <. (/) , (/) >. } | 0 = [_ ( ( 1 ... N ) X. { 0 } ) / p ]_ B } ) ) )
112 111 imbi2d 
 |-  ( k = 0 -> ( ( ph -> -. 2 || ( # ` { s e. ( ( ( 0 ..^ K ) ^m ( 1 ... k ) ) X. { f | f : ( 1 ... k ) -1-1-onto-> ( 1 ... k ) } ) | A. i e. ( 0 ... k ) E. j e. ( 0 ... k ) i = [_ ( ( ( 1st ` s ) oF + ( ( ( ( 2nd ` s ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` s ) " ( ( j + 1 ) ... k ) ) X. { 0 } ) ) ) u. ( ( ( k + 1 ) ... N ) X. { 0 } ) ) / p ]_ B } ) ) <-> ( ph -> -. 2 || ( # ` { s e. { <. (/) , (/) >. } | 0 = [_ ( ( 1 ... N ) X. { 0 } ) / p ]_ B } ) ) ) )
113 oveq2 
 |-  ( k = m -> ( 1 ... k ) = ( 1 ... m ) )
114 113 oveq2d 
 |-  ( k = m -> ( ( 0 ..^ K ) ^m ( 1 ... k ) ) = ( ( 0 ..^ K ) ^m ( 1 ... m ) ) )
115 eqidd 
 |-  ( k = m -> f = f )
116 115 113 113 f1oeq123d 
 |-  ( k = m -> ( f : ( 1 ... k ) -1-1-onto-> ( 1 ... k ) <-> f : ( 1 ... m ) -1-1-onto-> ( 1 ... m ) ) )
117 116 abbidv 
 |-  ( k = m -> { f | f : ( 1 ... k ) -1-1-onto-> ( 1 ... k ) } = { f | f : ( 1 ... m ) -1-1-onto-> ( 1 ... m ) } )
118 114 117 xpeq12d 
 |-  ( k = m -> ( ( ( 0 ..^ K ) ^m ( 1 ... k ) ) X. { f | f : ( 1 ... k ) -1-1-onto-> ( 1 ... k ) } ) = ( ( ( 0 ..^ K ) ^m ( 1 ... m ) ) X. { f | f : ( 1 ... m ) -1-1-onto-> ( 1 ... m ) } ) )
119 oveq2 
 |-  ( k = m -> ( 0 ... k ) = ( 0 ... m ) )
120 oveq2 
 |-  ( k = m -> ( ( j + 1 ) ... k ) = ( ( j + 1 ) ... m ) )
121 120 imaeq2d 
 |-  ( k = m -> ( ( 2nd ` s ) " ( ( j + 1 ) ... k ) ) = ( ( 2nd ` s ) " ( ( j + 1 ) ... m ) ) )
122 121 xpeq1d 
 |-  ( k = m -> ( ( ( 2nd ` s ) " ( ( j + 1 ) ... k ) ) X. { 0 } ) = ( ( ( 2nd ` s ) " ( ( j + 1 ) ... m ) ) X. { 0 } ) )
123 122 uneq2d 
 |-  ( k = m -> ( ( ( ( 2nd ` s ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` s ) " ( ( j + 1 ) ... k ) ) X. { 0 } ) ) = ( ( ( ( 2nd ` s ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` s ) " ( ( j + 1 ) ... m ) ) X. { 0 } ) ) )
124 123 oveq2d 
 |-  ( k = m -> ( ( 1st ` s ) oF + ( ( ( ( 2nd ` s ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` s ) " ( ( j + 1 ) ... k ) ) X. { 0 } ) ) ) = ( ( 1st ` s ) oF + ( ( ( ( 2nd ` s ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` s ) " ( ( j + 1 ) ... m ) ) X. { 0 } ) ) ) )
125 oveq1 
 |-  ( k = m -> ( k + 1 ) = ( m + 1 ) )
126 125 oveq1d 
 |-  ( k = m -> ( ( k + 1 ) ... N ) = ( ( m + 1 ) ... N ) )
127 126 xpeq1d 
 |-  ( k = m -> ( ( ( k + 1 ) ... N ) X. { 0 } ) = ( ( ( m + 1 ) ... N ) X. { 0 } ) )
128 124 127 uneq12d 
 |-  ( k = m -> ( ( ( 1st ` s ) oF + ( ( ( ( 2nd ` s ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` s ) " ( ( j + 1 ) ... k ) ) X. { 0 } ) ) ) u. ( ( ( k + 1 ) ... N ) X. { 0 } ) ) = ( ( ( 1st ` s ) oF + ( ( ( ( 2nd ` s ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` s ) " ( ( j + 1 ) ... m ) ) X. { 0 } ) ) ) u. ( ( ( m + 1 ) ... N ) X. { 0 } ) ) )
129 128 csbeq1d 
 |-  ( k = m -> [_ ( ( ( 1st ` s ) oF + ( ( ( ( 2nd ` s ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` s ) " ( ( j + 1 ) ... k ) ) X. { 0 } ) ) ) u. ( ( ( k + 1 ) ... N ) X. { 0 } ) ) / p ]_ B = [_ ( ( ( 1st ` s ) oF + ( ( ( ( 2nd ` s ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` s ) " ( ( j + 1 ) ... m ) ) X. { 0 } ) ) ) u. ( ( ( m + 1 ) ... N ) X. { 0 } ) ) / p ]_ B )
130 129 eqeq2d 
 |-  ( k = m -> ( i = [_ ( ( ( 1st ` s ) oF + ( ( ( ( 2nd ` s ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` s ) " ( ( j + 1 ) ... k ) ) X. { 0 } ) ) ) u. ( ( ( k + 1 ) ... N ) X. { 0 } ) ) / p ]_ B <-> i = [_ ( ( ( 1st ` s ) oF + ( ( ( ( 2nd ` s ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` s ) " ( ( j + 1 ) ... m ) ) X. { 0 } ) ) ) u. ( ( ( m + 1 ) ... N ) X. { 0 } ) ) / p ]_ B ) )
131 119 130 rexeqbidv 
 |-  ( k = m -> ( E. j e. ( 0 ... k ) i = [_ ( ( ( 1st ` s ) oF + ( ( ( ( 2nd ` s ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` s ) " ( ( j + 1 ) ... k ) ) X. { 0 } ) ) ) u. ( ( ( k + 1 ) ... N ) X. { 0 } ) ) / p ]_ B <-> E. j e. ( 0 ... m ) i = [_ ( ( ( 1st ` s ) oF + ( ( ( ( 2nd ` s ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` s ) " ( ( j + 1 ) ... m ) ) X. { 0 } ) ) ) u. ( ( ( m + 1 ) ... N ) X. { 0 } ) ) / p ]_ B ) )
132 119 131 raleqbidv 
 |-  ( k = m -> ( A. i e. ( 0 ... k ) E. j e. ( 0 ... k ) i = [_ ( ( ( 1st ` s ) oF + ( ( ( ( 2nd ` s ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` s ) " ( ( j + 1 ) ... k ) ) X. { 0 } ) ) ) u. ( ( ( k + 1 ) ... N ) X. { 0 } ) ) / p ]_ B <-> A. i e. ( 0 ... m ) E. j e. ( 0 ... m ) i = [_ ( ( ( 1st ` s ) oF + ( ( ( ( 2nd ` s ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` s ) " ( ( j + 1 ) ... m ) ) X. { 0 } ) ) ) u. ( ( ( m + 1 ) ... N ) X. { 0 } ) ) / p ]_ B ) )
133 118 132 rabeqbidv 
 |-  ( k = m -> { s e. ( ( ( 0 ..^ K ) ^m ( 1 ... k ) ) X. { f | f : ( 1 ... k ) -1-1-onto-> ( 1 ... k ) } ) | A. i e. ( 0 ... k ) E. j e. ( 0 ... k ) i = [_ ( ( ( 1st ` s ) oF + ( ( ( ( 2nd ` s ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` s ) " ( ( j + 1 ) ... k ) ) X. { 0 } ) ) ) u. ( ( ( k + 1 ) ... N ) X. { 0 } ) ) / p ]_ B } = { s e. ( ( ( 0 ..^ K ) ^m ( 1 ... m ) ) X. { f | f : ( 1 ... m ) -1-1-onto-> ( 1 ... m ) } ) | A. i e. ( 0 ... m ) E. j e. ( 0 ... m ) i = [_ ( ( ( 1st ` s ) oF + ( ( ( ( 2nd ` s ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` s ) " ( ( j + 1 ) ... m ) ) X. { 0 } ) ) ) u. ( ( ( m + 1 ) ... N ) X. { 0 } ) ) / p ]_ B } )
134 133 fveq2d 
 |-  ( k = m -> ( # ` { s e. ( ( ( 0 ..^ K ) ^m ( 1 ... k ) ) X. { f | f : ( 1 ... k ) -1-1-onto-> ( 1 ... k ) } ) | A. i e. ( 0 ... k ) E. j e. ( 0 ... k ) i = [_ ( ( ( 1st ` s ) oF + ( ( ( ( 2nd ` s ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` s ) " ( ( j + 1 ) ... k ) ) X. { 0 } ) ) ) u. ( ( ( k + 1 ) ... N ) X. { 0 } ) ) / p ]_ B } ) = ( # ` { s e. ( ( ( 0 ..^ K ) ^m ( 1 ... m ) ) X. { f | f : ( 1 ... m ) -1-1-onto-> ( 1 ... m ) } ) | A. i e. ( 0 ... m ) E. j e. ( 0 ... m ) i = [_ ( ( ( 1st ` s ) oF + ( ( ( ( 2nd ` s ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` s ) " ( ( j + 1 ) ... m ) ) X. { 0 } ) ) ) u. ( ( ( m + 1 ) ... N ) X. { 0 } ) ) / p ]_ B } ) )
135 134 breq2d 
 |-  ( k = m -> ( 2 || ( # ` { s e. ( ( ( 0 ..^ K ) ^m ( 1 ... k ) ) X. { f | f : ( 1 ... k ) -1-1-onto-> ( 1 ... k ) } ) | A. i e. ( 0 ... k ) E. j e. ( 0 ... k ) i = [_ ( ( ( 1st ` s ) oF + ( ( ( ( 2nd ` s ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` s ) " ( ( j + 1 ) ... k ) ) X. { 0 } ) ) ) u. ( ( ( k + 1 ) ... N ) X. { 0 } ) ) / p ]_ B } ) <-> 2 || ( # ` { s e. ( ( ( 0 ..^ K ) ^m ( 1 ... m ) ) X. { f | f : ( 1 ... m ) -1-1-onto-> ( 1 ... m ) } ) | A. i e. ( 0 ... m ) E. j e. ( 0 ... m ) i = [_ ( ( ( 1st ` s ) oF + ( ( ( ( 2nd ` s ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` s ) " ( ( j + 1 ) ... m ) ) X. { 0 } ) ) ) u. ( ( ( m + 1 ) ... N ) X. { 0 } ) ) / p ]_ B } ) ) )
136 135 notbid 
 |-  ( k = m -> ( -. 2 || ( # ` { s e. ( ( ( 0 ..^ K ) ^m ( 1 ... k ) ) X. { f | f : ( 1 ... k ) -1-1-onto-> ( 1 ... k ) } ) | A. i e. ( 0 ... k ) E. j e. ( 0 ... k ) i = [_ ( ( ( 1st ` s ) oF + ( ( ( ( 2nd ` s ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` s ) " ( ( j + 1 ) ... k ) ) X. { 0 } ) ) ) u. ( ( ( k + 1 ) ... N ) X. { 0 } ) ) / p ]_ B } ) <-> -. 2 || ( # ` { s e. ( ( ( 0 ..^ K ) ^m ( 1 ... m ) ) X. { f | f : ( 1 ... m ) -1-1-onto-> ( 1 ... m ) } ) | A. i e. ( 0 ... m ) E. j e. ( 0 ... m ) i = [_ ( ( ( 1st ` s ) oF + ( ( ( ( 2nd ` s ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` s ) " ( ( j + 1 ) ... m ) ) X. { 0 } ) ) ) u. ( ( ( m + 1 ) ... N ) X. { 0 } ) ) / p ]_ B } ) ) )
137 136 imbi2d 
 |-  ( k = m -> ( ( ph -> -. 2 || ( # ` { s e. ( ( ( 0 ..^ K ) ^m ( 1 ... k ) ) X. { f | f : ( 1 ... k ) -1-1-onto-> ( 1 ... k ) } ) | A. i e. ( 0 ... k ) E. j e. ( 0 ... k ) i = [_ ( ( ( 1st ` s ) oF + ( ( ( ( 2nd ` s ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` s ) " ( ( j + 1 ) ... k ) ) X. { 0 } ) ) ) u. ( ( ( k + 1 ) ... N ) X. { 0 } ) ) / p ]_ B } ) ) <-> ( ph -> -. 2 || ( # ` { s e. ( ( ( 0 ..^ K ) ^m ( 1 ... m ) ) X. { f | f : ( 1 ... m ) -1-1-onto-> ( 1 ... m ) } ) | A. i e. ( 0 ... m ) E. j e. ( 0 ... m ) i = [_ ( ( ( 1st ` s ) oF + ( ( ( ( 2nd ` s ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` s ) " ( ( j + 1 ) ... m ) ) X. { 0 } ) ) ) u. ( ( ( m + 1 ) ... N ) X. { 0 } ) ) / p ]_ B } ) ) ) )
138 oveq2 
 |-  ( k = ( m + 1 ) -> ( 1 ... k ) = ( 1 ... ( m + 1 ) ) )
139 138 oveq2d 
 |-  ( k = ( m + 1 ) -> ( ( 0 ..^ K ) ^m ( 1 ... k ) ) = ( ( 0 ..^ K ) ^m ( 1 ... ( m + 1 ) ) ) )
140 eqidd 
 |-  ( k = ( m + 1 ) -> f = f )
141 140 138 138 f1oeq123d 
 |-  ( k = ( m + 1 ) -> ( f : ( 1 ... k ) -1-1-onto-> ( 1 ... k ) <-> f : ( 1 ... ( m + 1 ) ) -1-1-onto-> ( 1 ... ( m + 1 ) ) ) )
142 141 abbidv 
 |-  ( k = ( m + 1 ) -> { f | f : ( 1 ... k ) -1-1-onto-> ( 1 ... k ) } = { f | f : ( 1 ... ( m + 1 ) ) -1-1-onto-> ( 1 ... ( m + 1 ) ) } )
143 139 142 xpeq12d 
 |-  ( k = ( m + 1 ) -> ( ( ( 0 ..^ K ) ^m ( 1 ... k ) ) X. { f | f : ( 1 ... k ) -1-1-onto-> ( 1 ... k ) } ) = ( ( ( 0 ..^ K ) ^m ( 1 ... ( m + 1 ) ) ) X. { f | f : ( 1 ... ( m + 1 ) ) -1-1-onto-> ( 1 ... ( m + 1 ) ) } ) )
144 oveq2 
 |-  ( k = ( m + 1 ) -> ( 0 ... k ) = ( 0 ... ( m + 1 ) ) )
145 oveq2 
 |-  ( k = ( m + 1 ) -> ( ( j + 1 ) ... k ) = ( ( j + 1 ) ... ( m + 1 ) ) )
146 145 imaeq2d 
 |-  ( k = ( m + 1 ) -> ( ( 2nd ` s ) " ( ( j + 1 ) ... k ) ) = ( ( 2nd ` s ) " ( ( j + 1 ) ... ( m + 1 ) ) ) )
147 146 xpeq1d 
 |-  ( k = ( m + 1 ) -> ( ( ( 2nd ` s ) " ( ( j + 1 ) ... k ) ) X. { 0 } ) = ( ( ( 2nd ` s ) " ( ( j + 1 ) ... ( m + 1 ) ) ) X. { 0 } ) )
148 147 uneq2d 
 |-  ( k = ( m + 1 ) -> ( ( ( ( 2nd ` s ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` s ) " ( ( j + 1 ) ... k ) ) X. { 0 } ) ) = ( ( ( ( 2nd ` s ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` s ) " ( ( j + 1 ) ... ( m + 1 ) ) ) X. { 0 } ) ) )
149 148 oveq2d 
 |-  ( k = ( m + 1 ) -> ( ( 1st ` s ) oF + ( ( ( ( 2nd ` s ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` s ) " ( ( j + 1 ) ... k ) ) X. { 0 } ) ) ) = ( ( 1st ` s ) oF + ( ( ( ( 2nd ` s ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` s ) " ( ( j + 1 ) ... ( m + 1 ) ) ) X. { 0 } ) ) ) )
150 oveq1 
 |-  ( k = ( m + 1 ) -> ( k + 1 ) = ( ( m + 1 ) + 1 ) )
151 150 oveq1d 
 |-  ( k = ( m + 1 ) -> ( ( k + 1 ) ... N ) = ( ( ( m + 1 ) + 1 ) ... N ) )
152 151 xpeq1d 
 |-  ( k = ( m + 1 ) -> ( ( ( k + 1 ) ... N ) X. { 0 } ) = ( ( ( ( m + 1 ) + 1 ) ... N ) X. { 0 } ) )
153 149 152 uneq12d 
 |-  ( k = ( m + 1 ) -> ( ( ( 1st ` s ) oF + ( ( ( ( 2nd ` s ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` s ) " ( ( j + 1 ) ... k ) ) X. { 0 } ) ) ) u. ( ( ( k + 1 ) ... N ) X. { 0 } ) ) = ( ( ( 1st ` s ) oF + ( ( ( ( 2nd ` s ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` s ) " ( ( j + 1 ) ... ( m + 1 ) ) ) X. { 0 } ) ) ) u. ( ( ( ( m + 1 ) + 1 ) ... N ) X. { 0 } ) ) )
154 153 csbeq1d 
 |-  ( k = ( m + 1 ) -> [_ ( ( ( 1st ` s ) oF + ( ( ( ( 2nd ` s ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` s ) " ( ( j + 1 ) ... k ) ) X. { 0 } ) ) ) u. ( ( ( k + 1 ) ... N ) X. { 0 } ) ) / p ]_ B = [_ ( ( ( 1st ` s ) oF + ( ( ( ( 2nd ` s ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` s ) " ( ( j + 1 ) ... ( m + 1 ) ) ) X. { 0 } ) ) ) u. ( ( ( ( m + 1 ) + 1 ) ... N ) X. { 0 } ) ) / p ]_ B )
155 154 eqeq2d 
 |-  ( k = ( m + 1 ) -> ( i = [_ ( ( ( 1st ` s ) oF + ( ( ( ( 2nd ` s ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` s ) " ( ( j + 1 ) ... k ) ) X. { 0 } ) ) ) u. ( ( ( k + 1 ) ... N ) X. { 0 } ) ) / p ]_ B <-> i = [_ ( ( ( 1st ` s ) oF + ( ( ( ( 2nd ` s ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` s ) " ( ( j + 1 ) ... ( m + 1 ) ) ) X. { 0 } ) ) ) u. ( ( ( ( m + 1 ) + 1 ) ... N ) X. { 0 } ) ) / p ]_ B ) )
156 144 155 rexeqbidv 
 |-  ( k = ( m + 1 ) -> ( E. j e. ( 0 ... k ) i = [_ ( ( ( 1st ` s ) oF + ( ( ( ( 2nd ` s ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` s ) " ( ( j + 1 ) ... k ) ) X. { 0 } ) ) ) u. ( ( ( k + 1 ) ... N ) X. { 0 } ) ) / p ]_ B <-> E. j e. ( 0 ... ( m + 1 ) ) i = [_ ( ( ( 1st ` s ) oF + ( ( ( ( 2nd ` s ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` s ) " ( ( j + 1 ) ... ( m + 1 ) ) ) X. { 0 } ) ) ) u. ( ( ( ( m + 1 ) + 1 ) ... N ) X. { 0 } ) ) / p ]_ B ) )
157 144 156 raleqbidv 
 |-  ( k = ( m + 1 ) -> ( A. i e. ( 0 ... k ) E. j e. ( 0 ... k ) i = [_ ( ( ( 1st ` s ) oF + ( ( ( ( 2nd ` s ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` s ) " ( ( j + 1 ) ... k ) ) X. { 0 } ) ) ) u. ( ( ( k + 1 ) ... N ) X. { 0 } ) ) / p ]_ B <-> A. i e. ( 0 ... ( m + 1 ) ) E. j e. ( 0 ... ( m + 1 ) ) i = [_ ( ( ( 1st ` s ) oF + ( ( ( ( 2nd ` s ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` s ) " ( ( j + 1 ) ... ( m + 1 ) ) ) X. { 0 } ) ) ) u. ( ( ( ( m + 1 ) + 1 ) ... N ) X. { 0 } ) ) / p ]_ B ) )
158 143 157 rabeqbidv 
 |-  ( k = ( m + 1 ) -> { s e. ( ( ( 0 ..^ K ) ^m ( 1 ... k ) ) X. { f | f : ( 1 ... k ) -1-1-onto-> ( 1 ... k ) } ) | A. i e. ( 0 ... k ) E. j e. ( 0 ... k ) i = [_ ( ( ( 1st ` s ) oF + ( ( ( ( 2nd ` s ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` s ) " ( ( j + 1 ) ... k ) ) X. { 0 } ) ) ) u. ( ( ( k + 1 ) ... N ) X. { 0 } ) ) / p ]_ B } = { s e. ( ( ( 0 ..^ K ) ^m ( 1 ... ( m + 1 ) ) ) X. { f | f : ( 1 ... ( m + 1 ) ) -1-1-onto-> ( 1 ... ( m + 1 ) ) } ) | A. i e. ( 0 ... ( m + 1 ) ) E. j e. ( 0 ... ( m + 1 ) ) i = [_ ( ( ( 1st ` s ) oF + ( ( ( ( 2nd ` s ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` s ) " ( ( j + 1 ) ... ( m + 1 ) ) ) X. { 0 } ) ) ) u. ( ( ( ( m + 1 ) + 1 ) ... N ) X. { 0 } ) ) / p ]_ B } )
159 158 fveq2d 
 |-  ( k = ( m + 1 ) -> ( # ` { s e. ( ( ( 0 ..^ K ) ^m ( 1 ... k ) ) X. { f | f : ( 1 ... k ) -1-1-onto-> ( 1 ... k ) } ) | A. i e. ( 0 ... k ) E. j e. ( 0 ... k ) i = [_ ( ( ( 1st ` s ) oF + ( ( ( ( 2nd ` s ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` s ) " ( ( j + 1 ) ... k ) ) X. { 0 } ) ) ) u. ( ( ( k + 1 ) ... N ) X. { 0 } ) ) / p ]_ B } ) = ( # ` { s e. ( ( ( 0 ..^ K ) ^m ( 1 ... ( m + 1 ) ) ) X. { f | f : ( 1 ... ( m + 1 ) ) -1-1-onto-> ( 1 ... ( m + 1 ) ) } ) | A. i e. ( 0 ... ( m + 1 ) ) E. j e. ( 0 ... ( m + 1 ) ) i = [_ ( ( ( 1st ` s ) oF + ( ( ( ( 2nd ` s ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` s ) " ( ( j + 1 ) ... ( m + 1 ) ) ) X. { 0 } ) ) ) u. ( ( ( ( m + 1 ) + 1 ) ... N ) X. { 0 } ) ) / p ]_ B } ) )
160 159 breq2d 
 |-  ( k = ( m + 1 ) -> ( 2 || ( # ` { s e. ( ( ( 0 ..^ K ) ^m ( 1 ... k ) ) X. { f | f : ( 1 ... k ) -1-1-onto-> ( 1 ... k ) } ) | A. i e. ( 0 ... k ) E. j e. ( 0 ... k ) i = [_ ( ( ( 1st ` s ) oF + ( ( ( ( 2nd ` s ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` s ) " ( ( j + 1 ) ... k ) ) X. { 0 } ) ) ) u. ( ( ( k + 1 ) ... N ) X. { 0 } ) ) / p ]_ B } ) <-> 2 || ( # ` { s e. ( ( ( 0 ..^ K ) ^m ( 1 ... ( m + 1 ) ) ) X. { f | f : ( 1 ... ( m + 1 ) ) -1-1-onto-> ( 1 ... ( m + 1 ) ) } ) | A. i e. ( 0 ... ( m + 1 ) ) E. j e. ( 0 ... ( m + 1 ) ) i = [_ ( ( ( 1st ` s ) oF + ( ( ( ( 2nd ` s ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` s ) " ( ( j + 1 ) ... ( m + 1 ) ) ) X. { 0 } ) ) ) u. ( ( ( ( m + 1 ) + 1 ) ... N ) X. { 0 } ) ) / p ]_ B } ) ) )
161 160 notbid 
 |-  ( k = ( m + 1 ) -> ( -. 2 || ( # ` { s e. ( ( ( 0 ..^ K ) ^m ( 1 ... k ) ) X. { f | f : ( 1 ... k ) -1-1-onto-> ( 1 ... k ) } ) | A. i e. ( 0 ... k ) E. j e. ( 0 ... k ) i = [_ ( ( ( 1st ` s ) oF + ( ( ( ( 2nd ` s ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` s ) " ( ( j + 1 ) ... k ) ) X. { 0 } ) ) ) u. ( ( ( k + 1 ) ... N ) X. { 0 } ) ) / p ]_ B } ) <-> -. 2 || ( # ` { s e. ( ( ( 0 ..^ K ) ^m ( 1 ... ( m + 1 ) ) ) X. { f | f : ( 1 ... ( m + 1 ) ) -1-1-onto-> ( 1 ... ( m + 1 ) ) } ) | A. i e. ( 0 ... ( m + 1 ) ) E. j e. ( 0 ... ( m + 1 ) ) i = [_ ( ( ( 1st ` s ) oF + ( ( ( ( 2nd ` s ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` s ) " ( ( j + 1 ) ... ( m + 1 ) ) ) X. { 0 } ) ) ) u. ( ( ( ( m + 1 ) + 1 ) ... N ) X. { 0 } ) ) / p ]_ B } ) ) )
162 161 imbi2d 
 |-  ( k = ( m + 1 ) -> ( ( ph -> -. 2 || ( # ` { s e. ( ( ( 0 ..^ K ) ^m ( 1 ... k ) ) X. { f | f : ( 1 ... k ) -1-1-onto-> ( 1 ... k ) } ) | A. i e. ( 0 ... k ) E. j e. ( 0 ... k ) i = [_ ( ( ( 1st ` s ) oF + ( ( ( ( 2nd ` s ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` s ) " ( ( j + 1 ) ... k ) ) X. { 0 } ) ) ) u. ( ( ( k + 1 ) ... N ) X. { 0 } ) ) / p ]_ B } ) ) <-> ( ph -> -. 2 || ( # ` { s e. ( ( ( 0 ..^ K ) ^m ( 1 ... ( m + 1 ) ) ) X. { f | f : ( 1 ... ( m + 1 ) ) -1-1-onto-> ( 1 ... ( m + 1 ) ) } ) | A. i e. ( 0 ... ( m + 1 ) ) E. j e. ( 0 ... ( m + 1 ) ) i = [_ ( ( ( 1st ` s ) oF + ( ( ( ( 2nd ` s ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` s ) " ( ( j + 1 ) ... ( m + 1 ) ) ) X. { 0 } ) ) ) u. ( ( ( ( m + 1 ) + 1 ) ... N ) X. { 0 } ) ) / p ]_ B } ) ) ) )
163 oveq2 
 |-  ( k = N -> ( 1 ... k ) = ( 1 ... N ) )
164 163 oveq2d 
 |-  ( k = N -> ( ( 0 ..^ K ) ^m ( 1 ... k ) ) = ( ( 0 ..^ K ) ^m ( 1 ... N ) ) )
165 eqidd 
 |-  ( k = N -> f = f )
166 165 163 163 f1oeq123d 
 |-  ( k = N -> ( f : ( 1 ... k ) -1-1-onto-> ( 1 ... k ) <-> f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) ) )
167 166 abbidv 
 |-  ( k = N -> { f | f : ( 1 ... k ) -1-1-onto-> ( 1 ... k ) } = { f | f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } )
168 164 167 xpeq12d 
 |-  ( k = N -> ( ( ( 0 ..^ K ) ^m ( 1 ... k ) ) X. { f | f : ( 1 ... k ) -1-1-onto-> ( 1 ... k ) } ) = ( ( ( 0 ..^ K ) ^m ( 1 ... N ) ) X. { f | f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } ) )
169 oveq2 
 |-  ( k = N -> ( 0 ... k ) = ( 0 ... N ) )
170 oveq2 
 |-  ( k = N -> ( ( j + 1 ) ... k ) = ( ( j + 1 ) ... N ) )
171 170 imaeq2d 
 |-  ( k = N -> ( ( 2nd ` s ) " ( ( j + 1 ) ... k ) ) = ( ( 2nd ` s ) " ( ( j + 1 ) ... N ) ) )
172 171 xpeq1d 
 |-  ( k = N -> ( ( ( 2nd ` s ) " ( ( j + 1 ) ... k ) ) X. { 0 } ) = ( ( ( 2nd ` s ) " ( ( j + 1 ) ... N ) ) X. { 0 } ) )
173 172 uneq2d 
 |-  ( k = N -> ( ( ( ( 2nd ` s ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` s ) " ( ( j + 1 ) ... k ) ) X. { 0 } ) ) = ( ( ( ( 2nd ` s ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` s ) " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) )
174 173 oveq2d 
 |-  ( k = N -> ( ( 1st ` s ) oF + ( ( ( ( 2nd ` s ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` s ) " ( ( j + 1 ) ... k ) ) X. { 0 } ) ) ) = ( ( 1st ` s ) oF + ( ( ( ( 2nd ` s ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` s ) " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) )
175 oveq1 
 |-  ( k = N -> ( k + 1 ) = ( N + 1 ) )
176 175 oveq1d 
 |-  ( k = N -> ( ( k + 1 ) ... N ) = ( ( N + 1 ) ... N ) )
177 176 xpeq1d 
 |-  ( k = N -> ( ( ( k + 1 ) ... N ) X. { 0 } ) = ( ( ( N + 1 ) ... N ) X. { 0 } ) )
178 174 177 uneq12d 
 |-  ( k = N -> ( ( ( 1st ` s ) oF + ( ( ( ( 2nd ` s ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` s ) " ( ( j + 1 ) ... k ) ) X. { 0 } ) ) ) u. ( ( ( k + 1 ) ... N ) X. { 0 } ) ) = ( ( ( 1st ` s ) oF + ( ( ( ( 2nd ` s ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` s ) " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) u. ( ( ( N + 1 ) ... N ) X. { 0 } ) ) )
179 178 csbeq1d 
 |-  ( k = N -> [_ ( ( ( 1st ` s ) oF + ( ( ( ( 2nd ` s ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` s ) " ( ( j + 1 ) ... k ) ) X. { 0 } ) ) ) u. ( ( ( k + 1 ) ... N ) X. { 0 } ) ) / p ]_ B = [_ ( ( ( 1st ` s ) oF + ( ( ( ( 2nd ` s ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` s ) " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) u. ( ( ( N + 1 ) ... N ) X. { 0 } ) ) / p ]_ B )
180 179 eqeq2d 
 |-  ( k = N -> ( i = [_ ( ( ( 1st ` s ) oF + ( ( ( ( 2nd ` s ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` s ) " ( ( j + 1 ) ... k ) ) X. { 0 } ) ) ) u. ( ( ( k + 1 ) ... N ) X. { 0 } ) ) / p ]_ B <-> i = [_ ( ( ( 1st ` s ) oF + ( ( ( ( 2nd ` s ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` s ) " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) u. ( ( ( N + 1 ) ... N ) X. { 0 } ) ) / p ]_ B ) )
181 169 180 rexeqbidv 
 |-  ( k = N -> ( E. j e. ( 0 ... k ) i = [_ ( ( ( 1st ` s ) oF + ( ( ( ( 2nd ` s ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` s ) " ( ( j + 1 ) ... k ) ) X. { 0 } ) ) ) u. ( ( ( k + 1 ) ... N ) X. { 0 } ) ) / p ]_ B <-> E. j e. ( 0 ... N ) i = [_ ( ( ( 1st ` s ) oF + ( ( ( ( 2nd ` s ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` s ) " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) u. ( ( ( N + 1 ) ... N ) X. { 0 } ) ) / p ]_ B ) )
182 169 181 raleqbidv 
 |-  ( k = N -> ( A. i e. ( 0 ... k ) E. j e. ( 0 ... k ) i = [_ ( ( ( 1st ` s ) oF + ( ( ( ( 2nd ` s ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` s ) " ( ( j + 1 ) ... k ) ) X. { 0 } ) ) ) u. ( ( ( k + 1 ) ... N ) X. { 0 } ) ) / p ]_ B <-> A. i e. ( 0 ... N ) E. j e. ( 0 ... N ) i = [_ ( ( ( 1st ` s ) oF + ( ( ( ( 2nd ` s ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` s ) " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) u. ( ( ( N + 1 ) ... N ) X. { 0 } ) ) / p ]_ B ) )
183 168 182 rabeqbidv 
 |-  ( k = N -> { s e. ( ( ( 0 ..^ K ) ^m ( 1 ... k ) ) X. { f | f : ( 1 ... k ) -1-1-onto-> ( 1 ... k ) } ) | A. i e. ( 0 ... k ) E. j e. ( 0 ... k ) i = [_ ( ( ( 1st ` s ) oF + ( ( ( ( 2nd ` s ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` s ) " ( ( j + 1 ) ... k ) ) X. { 0 } ) ) ) u. ( ( ( k + 1 ) ... N ) X. { 0 } ) ) / p ]_ B } = { s e. ( ( ( 0 ..^ K ) ^m ( 1 ... N ) ) X. { f | f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } ) | A. i e. ( 0 ... N ) E. j e. ( 0 ... N ) i = [_ ( ( ( 1st ` s ) oF + ( ( ( ( 2nd ` s ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` s ) " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) u. ( ( ( N + 1 ) ... N ) X. { 0 } ) ) / p ]_ B } )
184 183 fveq2d 
 |-  ( k = N -> ( # ` { s e. ( ( ( 0 ..^ K ) ^m ( 1 ... k ) ) X. { f | f : ( 1 ... k ) -1-1-onto-> ( 1 ... k ) } ) | A. i e. ( 0 ... k ) E. j e. ( 0 ... k ) i = [_ ( ( ( 1st ` s ) oF + ( ( ( ( 2nd ` s ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` s ) " ( ( j + 1 ) ... k ) ) X. { 0 } ) ) ) u. ( ( ( k + 1 ) ... N ) X. { 0 } ) ) / p ]_ B } ) = ( # ` { s e. ( ( ( 0 ..^ K ) ^m ( 1 ... N ) ) X. { f | f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } ) | A. i e. ( 0 ... N ) E. j e. ( 0 ... N ) i = [_ ( ( ( 1st ` s ) oF + ( ( ( ( 2nd ` s ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` s ) " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) u. ( ( ( N + 1 ) ... N ) X. { 0 } ) ) / p ]_ B } ) )
185 184 breq2d 
 |-  ( k = N -> ( 2 || ( # ` { s e. ( ( ( 0 ..^ K ) ^m ( 1 ... k ) ) X. { f | f : ( 1 ... k ) -1-1-onto-> ( 1 ... k ) } ) | A. i e. ( 0 ... k ) E. j e. ( 0 ... k ) i = [_ ( ( ( 1st ` s ) oF + ( ( ( ( 2nd ` s ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` s ) " ( ( j + 1 ) ... k ) ) X. { 0 } ) ) ) u. ( ( ( k + 1 ) ... N ) X. { 0 } ) ) / p ]_ B } ) <-> 2 || ( # ` { s e. ( ( ( 0 ..^ K ) ^m ( 1 ... N ) ) X. { f | f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } ) | A. i e. ( 0 ... N ) E. j e. ( 0 ... N ) i = [_ ( ( ( 1st ` s ) oF + ( ( ( ( 2nd ` s ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` s ) " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) u. ( ( ( N + 1 ) ... N ) X. { 0 } ) ) / p ]_ B } ) ) )
186 185 notbid 
 |-  ( k = N -> ( -. 2 || ( # ` { s e. ( ( ( 0 ..^ K ) ^m ( 1 ... k ) ) X. { f | f : ( 1 ... k ) -1-1-onto-> ( 1 ... k ) } ) | A. i e. ( 0 ... k ) E. j e. ( 0 ... k ) i = [_ ( ( ( 1st ` s ) oF + ( ( ( ( 2nd ` s ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` s ) " ( ( j + 1 ) ... k ) ) X. { 0 } ) ) ) u. ( ( ( k + 1 ) ... N ) X. { 0 } ) ) / p ]_ B } ) <-> -. 2 || ( # ` { s e. ( ( ( 0 ..^ K ) ^m ( 1 ... N ) ) X. { f | f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } ) | A. i e. ( 0 ... N ) E. j e. ( 0 ... N ) i = [_ ( ( ( 1st ` s ) oF + ( ( ( ( 2nd ` s ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` s ) " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) u. ( ( ( N + 1 ) ... N ) X. { 0 } ) ) / p ]_ B } ) ) )
187 186 imbi2d 
 |-  ( k = N -> ( ( ph -> -. 2 || ( # ` { s e. ( ( ( 0 ..^ K ) ^m ( 1 ... k ) ) X. { f | f : ( 1 ... k ) -1-1-onto-> ( 1 ... k ) } ) | A. i e. ( 0 ... k ) E. j e. ( 0 ... k ) i = [_ ( ( ( 1st ` s ) oF + ( ( ( ( 2nd ` s ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` s ) " ( ( j + 1 ) ... k ) ) X. { 0 } ) ) ) u. ( ( ( k + 1 ) ... N ) X. { 0 } ) ) / p ]_ B } ) ) <-> ( ph -> -. 2 || ( # ` { s e. ( ( ( 0 ..^ K ) ^m ( 1 ... N ) ) X. { f | f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } ) | A. i e. ( 0 ... N ) E. j e. ( 0 ... N ) i = [_ ( ( ( 1st ` s ) oF + ( ( ( ( 2nd ` s ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` s ) " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) u. ( ( ( N + 1 ) ... N ) X. { 0 } ) ) / p ]_ B } ) ) ) )
188 n2dvds1 
 |-  -. 2 || 1
189 opex 
 |-  <. (/) , (/) >. e. _V
190 hashsng 
 |-  ( <. (/) , (/) >. e. _V -> ( # ` { <. (/) , (/) >. } ) = 1 )
191 189 190 ax-mp 
 |-  ( # ` { <. (/) , (/) >. } ) = 1
192 nnuz 
 |-  NN = ( ZZ>= ` 1 )
193 1 192 eleqtrdi 
 |-  ( ph -> N e. ( ZZ>= ` 1 ) )
194 eluzfz1 
 |-  ( N e. ( ZZ>= ` 1 ) -> 1 e. ( 1 ... N ) )
195 193 194 syl 
 |-  ( ph -> 1 e. ( 1 ... N ) )
196 6 nnnn0d 
 |-  ( ph -> K e. NN0 )
197 0elfz 
 |-  ( K e. NN0 -> 0 e. ( 0 ... K ) )
198 fconst6g 
 |-  ( 0 e. ( 0 ... K ) -> ( ( 1 ... N ) X. { 0 } ) : ( 1 ... N ) --> ( 0 ... K ) )
199 196 197 198 3syl 
 |-  ( ph -> ( ( 1 ... N ) X. { 0 } ) : ( 1 ... N ) --> ( 0 ... K ) )
200 75 fvconst2 
 |-  ( 1 e. ( 1 ... N ) -> ( ( ( 1 ... N ) X. { 0 } ) ` 1 ) = 0 )
201 195 200 syl 
 |-  ( ph -> ( ( ( 1 ... N ) X. { 0 } ) ` 1 ) = 0 )
202 195 199 201 3jca 
 |-  ( ph -> ( 1 e. ( 1 ... N ) /\ ( ( 1 ... N ) X. { 0 } ) : ( 1 ... N ) --> ( 0 ... K ) /\ ( ( ( 1 ... N ) X. { 0 } ) ` 1 ) = 0 ) )
203 nfv 
 |-  F/ p ( ph /\ ( 1 e. ( 1 ... N ) /\ ( ( 1 ... N ) X. { 0 } ) : ( 1 ... N ) --> ( 0 ... K ) /\ ( ( ( 1 ... N ) X. { 0 } ) ` 1 ) = 0 ) )
204 nfcsb1v 
 |-  F/_ p [_ ( ( 1 ... N ) X. { 0 } ) / p ]_ B
205 204 nfeq1 
 |-  F/ p [_ ( ( 1 ... N ) X. { 0 } ) / p ]_ B = 0
206 203 205 nfim 
 |-  F/ p ( ( ph /\ ( 1 e. ( 1 ... N ) /\ ( ( 1 ... N ) X. { 0 } ) : ( 1 ... N ) --> ( 0 ... K ) /\ ( ( ( 1 ... N ) X. { 0 } ) ` 1 ) = 0 ) ) -> [_ ( ( 1 ... N ) X. { 0 } ) / p ]_ B = 0 )
207 ovex 
 |-  ( 1 ... N ) e. _V
208 snex 
 |-  { 0 } e. _V
209 207 208 xpex 
 |-  ( ( 1 ... N ) X. { 0 } ) e. _V
210 feq1 
 |-  ( p = ( ( 1 ... N ) X. { 0 } ) -> ( p : ( 1 ... N ) --> ( 0 ... K ) <-> ( ( 1 ... N ) X. { 0 } ) : ( 1 ... N ) --> ( 0 ... K ) ) )
211 fveq1 
 |-  ( p = ( ( 1 ... N ) X. { 0 } ) -> ( p ` 1 ) = ( ( ( 1 ... N ) X. { 0 } ) ` 1 ) )
212 211 eqeq1d 
 |-  ( p = ( ( 1 ... N ) X. { 0 } ) -> ( ( p ` 1 ) = 0 <-> ( ( ( 1 ... N ) X. { 0 } ) ` 1 ) = 0 ) )
213 210 212 3anbi23d 
 |-  ( p = ( ( 1 ... N ) X. { 0 } ) -> ( ( 1 e. ( 1 ... N ) /\ p : ( 1 ... N ) --> ( 0 ... K ) /\ ( p ` 1 ) = 0 ) <-> ( 1 e. ( 1 ... N ) /\ ( ( 1 ... N ) X. { 0 } ) : ( 1 ... N ) --> ( 0 ... K ) /\ ( ( ( 1 ... N ) X. { 0 } ) ` 1 ) = 0 ) ) )
214 213 anbi2d 
 |-  ( p = ( ( 1 ... N ) X. { 0 } ) -> ( ( ph /\ ( 1 e. ( 1 ... N ) /\ p : ( 1 ... N ) --> ( 0 ... K ) /\ ( p ` 1 ) = 0 ) ) <-> ( ph /\ ( 1 e. ( 1 ... N ) /\ ( ( 1 ... N ) X. { 0 } ) : ( 1 ... N ) --> ( 0 ... K ) /\ ( ( ( 1 ... N ) X. { 0 } ) ` 1 ) = 0 ) ) ) )
215 csbeq1a 
 |-  ( p = ( ( 1 ... N ) X. { 0 } ) -> B = [_ ( ( 1 ... N ) X. { 0 } ) / p ]_ B )
216 215 eqeq1d 
 |-  ( p = ( ( 1 ... N ) X. { 0 } ) -> ( B = 0 <-> [_ ( ( 1 ... N ) X. { 0 } ) / p ]_ B = 0 ) )
217 214 216 imbi12d 
 |-  ( p = ( ( 1 ... N ) X. { 0 } ) -> ( ( ( ph /\ ( 1 e. ( 1 ... N ) /\ p : ( 1 ... N ) --> ( 0 ... K ) /\ ( p ` 1 ) = 0 ) ) -> B = 0 ) <-> ( ( ph /\ ( 1 e. ( 1 ... N ) /\ ( ( 1 ... N ) X. { 0 } ) : ( 1 ... N ) --> ( 0 ... K ) /\ ( ( ( 1 ... N ) X. { 0 } ) ` 1 ) = 0 ) ) -> [_ ( ( 1 ... N ) X. { 0 } ) / p ]_ B = 0 ) ) )
218 1ex 
 |-  1 e. _V
219 eleq1 
 |-  ( n = 1 -> ( n e. ( 1 ... N ) <-> 1 e. ( 1 ... N ) ) )
220 fveqeq2 
 |-  ( n = 1 -> ( ( p ` n ) = 0 <-> ( p ` 1 ) = 0 ) )
221 219 220 3anbi13d 
 |-  ( n = 1 -> ( ( n e. ( 1 ... N ) /\ p : ( 1 ... N ) --> ( 0 ... K ) /\ ( p ` n ) = 0 ) <-> ( 1 e. ( 1 ... N ) /\ p : ( 1 ... N ) --> ( 0 ... K ) /\ ( p ` 1 ) = 0 ) ) )
222 221 anbi2d 
 |-  ( n = 1 -> ( ( ph /\ ( n e. ( 1 ... N ) /\ p : ( 1 ... N ) --> ( 0 ... K ) /\ ( p ` n ) = 0 ) ) <-> ( ph /\ ( 1 e. ( 1 ... N ) /\ p : ( 1 ... N ) --> ( 0 ... K ) /\ ( p ` 1 ) = 0 ) ) ) )
223 breq2 
 |-  ( n = 1 -> ( B < n <-> B < 1 ) )
224 222 223 imbi12d 
 |-  ( n = 1 -> ( ( ( ph /\ ( n e. ( 1 ... N ) /\ p : ( 1 ... N ) --> ( 0 ... K ) /\ ( p ` n ) = 0 ) ) -> B < n ) <-> ( ( ph /\ ( 1 e. ( 1 ... N ) /\ p : ( 1 ... N ) --> ( 0 ... K ) /\ ( p ` 1 ) = 0 ) ) -> B < 1 ) ) )
225 218 224 4 vtocl 
 |-  ( ( ph /\ ( 1 e. ( 1 ... N ) /\ p : ( 1 ... N ) --> ( 0 ... K ) /\ ( p ` 1 ) = 0 ) ) -> B < 1 )
226 elfznn0 
 |-  ( B e. ( 0 ... N ) -> B e. NN0 )
227 nn0lt10b 
 |-  ( B e. NN0 -> ( B < 1 <-> B = 0 ) )
228 3 226 227 3syl 
 |-  ( ( ph /\ p : ( 1 ... N ) --> ( 0 ... K ) ) -> ( B < 1 <-> B = 0 ) )
229 228 3ad2antr2 
 |-  ( ( ph /\ ( 1 e. ( 1 ... N ) /\ p : ( 1 ... N ) --> ( 0 ... K ) /\ ( p ` 1 ) = 0 ) ) -> ( B < 1 <-> B = 0 ) )
230 225 229 mpbid 
 |-  ( ( ph /\ ( 1 e. ( 1 ... N ) /\ p : ( 1 ... N ) --> ( 0 ... K ) /\ ( p ` 1 ) = 0 ) ) -> B = 0 )
231 206 209 217 230 vtoclf 
 |-  ( ( ph /\ ( 1 e. ( 1 ... N ) /\ ( ( 1 ... N ) X. { 0 } ) : ( 1 ... N ) --> ( 0 ... K ) /\ ( ( ( 1 ... N ) X. { 0 } ) ` 1 ) = 0 ) ) -> [_ ( ( 1 ... N ) X. { 0 } ) / p ]_ B = 0 )
232 202 231 mpdan 
 |-  ( ph -> [_ ( ( 1 ... N ) X. { 0 } ) / p ]_ B = 0 )
233 232 eqcomd 
 |-  ( ph -> 0 = [_ ( ( 1 ... N ) X. { 0 } ) / p ]_ B )
234 233 ralrimivw 
 |-  ( ph -> A. s e. { <. (/) , (/) >. } 0 = [_ ( ( 1 ... N ) X. { 0 } ) / p ]_ B )
235 rabid2 
 |-  ( { <. (/) , (/) >. } = { s e. { <. (/) , (/) >. } | 0 = [_ ( ( 1 ... N ) X. { 0 } ) / p ]_ B } <-> A. s e. { <. (/) , (/) >. } 0 = [_ ( ( 1 ... N ) X. { 0 } ) / p ]_ B )
236 234 235 sylibr 
 |-  ( ph -> { <. (/) , (/) >. } = { s e. { <. (/) , (/) >. } | 0 = [_ ( ( 1 ... N ) X. { 0 } ) / p ]_ B } )
237 236 fveq2d 
 |-  ( ph -> ( # ` { <. (/) , (/) >. } ) = ( # ` { s e. { <. (/) , (/) >. } | 0 = [_ ( ( 1 ... N ) X. { 0 } ) / p ]_ B } ) )
238 191 237 eqtr3id 
 |-  ( ph -> 1 = ( # ` { s e. { <. (/) , (/) >. } | 0 = [_ ( ( 1 ... N ) X. { 0 } ) / p ]_ B } ) )
239 238 breq2d 
 |-  ( ph -> ( 2 || 1 <-> 2 || ( # ` { s e. { <. (/) , (/) >. } | 0 = [_ ( ( 1 ... N ) X. { 0 } ) / p ]_ B } ) ) )
240 188 239 mtbii 
 |-  ( ph -> -. 2 || ( # ` { s e. { <. (/) , (/) >. } | 0 = [_ ( ( 1 ... N ) X. { 0 } ) / p ]_ B } ) )
241 240 a1i 
 |-  ( N e. NN0 -> ( ph -> -. 2 || ( # ` { s e. { <. (/) , (/) >. } | 0 = [_ ( ( 1 ... N ) X. { 0 } ) / p ]_ B } ) ) )
242 2z 
 |-  2 e. ZZ
243 fzfi 
 |-  ( 1 ... ( m + 1 ) ) e. Fin
244 mapfi 
 |-  ( ( ( 0 ..^ K ) e. Fin /\ ( 1 ... ( m + 1 ) ) e. Fin ) -> ( ( 0 ..^ K ) ^m ( 1 ... ( m + 1 ) ) ) e. Fin )
245 15 243 244 mp2an 
 |-  ( ( 0 ..^ K ) ^m ( 1 ... ( m + 1 ) ) ) e. Fin
246 ovex 
 |-  ( 1 ... ( m + 1 ) ) e. _V
247 246 246 mapval 
 |-  ( ( 1 ... ( m + 1 ) ) ^m ( 1 ... ( m + 1 ) ) ) = { f | f : ( 1 ... ( m + 1 ) ) --> ( 1 ... ( m + 1 ) ) }
248 mapfi 
 |-  ( ( ( 1 ... ( m + 1 ) ) e. Fin /\ ( 1 ... ( m + 1 ) ) e. Fin ) -> ( ( 1 ... ( m + 1 ) ) ^m ( 1 ... ( m + 1 ) ) ) e. Fin )
249 243 243 248 mp2an 
 |-  ( ( 1 ... ( m + 1 ) ) ^m ( 1 ... ( m + 1 ) ) ) e. Fin
250 247 249 eqeltrri 
 |-  { f | f : ( 1 ... ( m + 1 ) ) --> ( 1 ... ( m + 1 ) ) } e. Fin
251 f1of 
 |-  ( f : ( 1 ... ( m + 1 ) ) -1-1-onto-> ( 1 ... ( m + 1 ) ) -> f : ( 1 ... ( m + 1 ) ) --> ( 1 ... ( m + 1 ) ) )
252 251 ss2abi 
 |-  { f | f : ( 1 ... ( m + 1 ) ) -1-1-onto-> ( 1 ... ( m + 1 ) ) } C_ { f | f : ( 1 ... ( m + 1 ) ) --> ( 1 ... ( m + 1 ) ) }
253 ssfi 
 |-  ( ( { f | f : ( 1 ... ( m + 1 ) ) --> ( 1 ... ( m + 1 ) ) } e. Fin /\ { f | f : ( 1 ... ( m + 1 ) ) -1-1-onto-> ( 1 ... ( m + 1 ) ) } C_ { f | f : ( 1 ... ( m + 1 ) ) --> ( 1 ... ( m + 1 ) ) } ) -> { f | f : ( 1 ... ( m + 1 ) ) -1-1-onto-> ( 1 ... ( m + 1 ) ) } e. Fin )
254 250 252 253 mp2an 
 |-  { f | f : ( 1 ... ( m + 1 ) ) -1-1-onto-> ( 1 ... ( m + 1 ) ) } e. Fin
255 xpfi 
 |-  ( ( ( ( 0 ..^ K ) ^m ( 1 ... ( m + 1 ) ) ) e. Fin /\ { f | f : ( 1 ... ( m + 1 ) ) -1-1-onto-> ( 1 ... ( m + 1 ) ) } e. Fin ) -> ( ( ( 0 ..^ K ) ^m ( 1 ... ( m + 1 ) ) ) X. { f | f : ( 1 ... ( m + 1 ) ) -1-1-onto-> ( 1 ... ( m + 1 ) ) } ) e. Fin )
256 245 254 255 mp2an 
 |-  ( ( ( 0 ..^ K ) ^m ( 1 ... ( m + 1 ) ) ) X. { f | f : ( 1 ... ( m + 1 ) ) -1-1-onto-> ( 1 ... ( m + 1 ) ) } ) e. Fin
257 rabfi 
 |-  ( ( ( ( 0 ..^ K ) ^m ( 1 ... ( m + 1 ) ) ) X. { f | f : ( 1 ... ( m + 1 ) ) -1-1-onto-> ( 1 ... ( m + 1 ) ) } ) e. Fin -> { s e. ( ( ( 0 ..^ K ) ^m ( 1 ... ( m + 1 ) ) ) X. { f | f : ( 1 ... ( m + 1 ) ) -1-1-onto-> ( 1 ... ( m + 1 ) ) } ) | A. i e. ( 0 ... ( m + 1 ) ) E. j e. ( 0 ... ( m + 1 ) ) i = [_ ( ( ( 1st ` s ) oF + ( ( ( ( 2nd ` s ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` s ) " ( ( j + 1 ) ... ( m + 1 ) ) ) X. { 0 } ) ) ) u. ( ( ( ( m + 1 ) + 1 ) ... N ) X. { 0 } ) ) / p ]_ B } e. Fin )
258 hashcl 
 |-  ( { s e. ( ( ( 0 ..^ K ) ^m ( 1 ... ( m + 1 ) ) ) X. { f | f : ( 1 ... ( m + 1 ) ) -1-1-onto-> ( 1 ... ( m + 1 ) ) } ) | A. i e. ( 0 ... ( m + 1 ) ) E. j e. ( 0 ... ( m + 1 ) ) i = [_ ( ( ( 1st ` s ) oF + ( ( ( ( 2nd ` s ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` s ) " ( ( j + 1 ) ... ( m + 1 ) ) ) X. { 0 } ) ) ) u. ( ( ( ( m + 1 ) + 1 ) ... N ) X. { 0 } ) ) / p ]_ B } e. Fin -> ( # ` { s e. ( ( ( 0 ..^ K ) ^m ( 1 ... ( m + 1 ) ) ) X. { f | f : ( 1 ... ( m + 1 ) ) -1-1-onto-> ( 1 ... ( m + 1 ) ) } ) | A. i e. ( 0 ... ( m + 1 ) ) E. j e. ( 0 ... ( m + 1 ) ) i = [_ ( ( ( 1st ` s ) oF + ( ( ( ( 2nd ` s ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` s ) " ( ( j + 1 ) ... ( m + 1 ) ) ) X. { 0 } ) ) ) u. ( ( ( ( m + 1 ) + 1 ) ... N ) X. { 0 } ) ) / p ]_ B } ) e. NN0 )
259 256 257 258 mp2b 
 |-  ( # ` { s e. ( ( ( 0 ..^ K ) ^m ( 1 ... ( m + 1 ) ) ) X. { f | f : ( 1 ... ( m + 1 ) ) -1-1-onto-> ( 1 ... ( m + 1 ) ) } ) | A. i e. ( 0 ... ( m + 1 ) ) E. j e. ( 0 ... ( m + 1 ) ) i = [_ ( ( ( 1st ` s ) oF + ( ( ( ( 2nd ` s ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` s ) " ( ( j + 1 ) ... ( m + 1 ) ) ) X. { 0 } ) ) ) u. ( ( ( ( m + 1 ) + 1 ) ... N ) X. { 0 } ) ) / p ]_ B } ) e. NN0
260 259 nn0zi 
 |-  ( # ` { s e. ( ( ( 0 ..^ K ) ^m ( 1 ... ( m + 1 ) ) ) X. { f | f : ( 1 ... ( m + 1 ) ) -1-1-onto-> ( 1 ... ( m + 1 ) ) } ) | A. i e. ( 0 ... ( m + 1 ) ) E. j e. ( 0 ... ( m + 1 ) ) i = [_ ( ( ( 1st ` s ) oF + ( ( ( ( 2nd ` s ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` s ) " ( ( j + 1 ) ... ( m + 1 ) ) ) X. { 0 } ) ) ) u. ( ( ( ( m + 1 ) + 1 ) ... N ) X. { 0 } ) ) / p ]_ B } ) e. ZZ
261 rabfi 
 |-  ( ( ( ( 0 ..^ K ) ^m ( 1 ... ( m + 1 ) ) ) X. { f | f : ( 1 ... ( m + 1 ) ) -1-1-onto-> ( 1 ... ( m + 1 ) ) } ) e. Fin -> { s e. ( ( ( 0 ..^ K ) ^m ( 1 ... ( m + 1 ) ) ) X. { f | f : ( 1 ... ( m + 1 ) ) -1-1-onto-> ( 1 ... ( m + 1 ) ) } ) | ( A. i e. ( 0 ... ( ( m + 1 ) - 1 ) ) E. j e. ( 0 ... ( ( m + 1 ) - 1 ) ) i = [_ ( ( ( 1st ` s ) oF + ( ( ( ( 2nd ` s ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` s ) " ( ( j + 1 ) ... ( m + 1 ) ) ) X. { 0 } ) ) ) u. ( ( ( ( m + 1 ) + 1 ) ... N ) X. { 0 } ) ) / p ]_ B /\ ( ( 1st ` s ) ` ( m + 1 ) ) = 0 /\ ( ( 2nd ` s ) ` ( m + 1 ) ) = ( m + 1 ) ) } e. Fin )
262 hashcl 
 |-  ( { s e. ( ( ( 0 ..^ K ) ^m ( 1 ... ( m + 1 ) ) ) X. { f | f : ( 1 ... ( m + 1 ) ) -1-1-onto-> ( 1 ... ( m + 1 ) ) } ) | ( A. i e. ( 0 ... ( ( m + 1 ) - 1 ) ) E. j e. ( 0 ... ( ( m + 1 ) - 1 ) ) i = [_ ( ( ( 1st ` s ) oF + ( ( ( ( 2nd ` s ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` s ) " ( ( j + 1 ) ... ( m + 1 ) ) ) X. { 0 } ) ) ) u. ( ( ( ( m + 1 ) + 1 ) ... N ) X. { 0 } ) ) / p ]_ B /\ ( ( 1st ` s ) ` ( m + 1 ) ) = 0 /\ ( ( 2nd ` s ) ` ( m + 1 ) ) = ( m + 1 ) ) } e. Fin -> ( # ` { s e. ( ( ( 0 ..^ K ) ^m ( 1 ... ( m + 1 ) ) ) X. { f | f : ( 1 ... ( m + 1 ) ) -1-1-onto-> ( 1 ... ( m + 1 ) ) } ) | ( A. i e. ( 0 ... ( ( m + 1 ) - 1 ) ) E. j e. ( 0 ... ( ( m + 1 ) - 1 ) ) i = [_ ( ( ( 1st ` s ) oF + ( ( ( ( 2nd ` s ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` s ) " ( ( j + 1 ) ... ( m + 1 ) ) ) X. { 0 } ) ) ) u. ( ( ( ( m + 1 ) + 1 ) ... N ) X. { 0 } ) ) / p ]_ B /\ ( ( 1st ` s ) ` ( m + 1 ) ) = 0 /\ ( ( 2nd ` s ) ` ( m + 1 ) ) = ( m + 1 ) ) } ) e. NN0 )
263 256 261 262 mp2b 
 |-  ( # ` { s e. ( ( ( 0 ..^ K ) ^m ( 1 ... ( m + 1 ) ) ) X. { f | f : ( 1 ... ( m + 1 ) ) -1-1-onto-> ( 1 ... ( m + 1 ) ) } ) | ( A. i e. ( 0 ... ( ( m + 1 ) - 1 ) ) E. j e. ( 0 ... ( ( m + 1 ) - 1 ) ) i = [_ ( ( ( 1st ` s ) oF + ( ( ( ( 2nd ` s ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` s ) " ( ( j + 1 ) ... ( m + 1 ) ) ) X. { 0 } ) ) ) u. ( ( ( ( m + 1 ) + 1 ) ... N ) X. { 0 } ) ) / p ]_ B /\ ( ( 1st ` s ) ` ( m + 1 ) ) = 0 /\ ( ( 2nd ` s ) ` ( m + 1 ) ) = ( m + 1 ) ) } ) e. NN0
264 263 nn0zi 
 |-  ( # ` { s e. ( ( ( 0 ..^ K ) ^m ( 1 ... ( m + 1 ) ) ) X. { f | f : ( 1 ... ( m + 1 ) ) -1-1-onto-> ( 1 ... ( m + 1 ) ) } ) | ( A. i e. ( 0 ... ( ( m + 1 ) - 1 ) ) E. j e. ( 0 ... ( ( m + 1 ) - 1 ) ) i = [_ ( ( ( 1st ` s ) oF + ( ( ( ( 2nd ` s ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` s ) " ( ( j + 1 ) ... ( m + 1 ) ) ) X. { 0 } ) ) ) u. ( ( ( ( m + 1 ) + 1 ) ... N ) X. { 0 } ) ) / p ]_ B /\ ( ( 1st ` s ) ` ( m + 1 ) ) = 0 /\ ( ( 2nd ` s ) ` ( m + 1 ) ) = ( m + 1 ) ) } ) e. ZZ
265 242 260 264 3pm3.2i 
 |-  ( 2 e. ZZ /\ ( # ` { s e. ( ( ( 0 ..^ K ) ^m ( 1 ... ( m + 1 ) ) ) X. { f | f : ( 1 ... ( m + 1 ) ) -1-1-onto-> ( 1 ... ( m + 1 ) ) } ) | A. i e. ( 0 ... ( m + 1 ) ) E. j e. ( 0 ... ( m + 1 ) ) i = [_ ( ( ( 1st ` s ) oF + ( ( ( ( 2nd ` s ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` s ) " ( ( j + 1 ) ... ( m + 1 ) ) ) X. { 0 } ) ) ) u. ( ( ( ( m + 1 ) + 1 ) ... N ) X. { 0 } ) ) / p ]_ B } ) e. ZZ /\ ( # ` { s e. ( ( ( 0 ..^ K ) ^m ( 1 ... ( m + 1 ) ) ) X. { f | f : ( 1 ... ( m + 1 ) ) -1-1-onto-> ( 1 ... ( m + 1 ) ) } ) | ( A. i e. ( 0 ... ( ( m + 1 ) - 1 ) ) E. j e. ( 0 ... ( ( m + 1 ) - 1 ) ) i = [_ ( ( ( 1st ` s ) oF + ( ( ( ( 2nd ` s ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` s ) " ( ( j + 1 ) ... ( m + 1 ) ) ) X. { 0 } ) ) ) u. ( ( ( ( m + 1 ) + 1 ) ... N ) X. { 0 } ) ) / p ]_ B /\ ( ( 1st ` s ) ` ( m + 1 ) ) = 0 /\ ( ( 2nd ` s ) ` ( m + 1 ) ) = ( m + 1 ) ) } ) e. ZZ )
266 nn0p1nn 
 |-  ( m e. NN0 -> ( m + 1 ) e. NN )
267 266 ad2antrl 
 |-  ( ( ph /\ ( m e. NN0 /\ m < N ) ) -> ( m + 1 ) e. NN )
268 uneq1 
 |-  ( q = ( ( 1st ` s ) oF + ( ( ( ( 2nd ` s ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` s ) " ( ( j + 1 ) ... ( m + 1 ) ) ) X. { 0 } ) ) ) -> ( q u. ( ( ( ( m + 1 ) + 1 ) ... N ) X. { 0 } ) ) = ( ( ( 1st ` s ) oF + ( ( ( ( 2nd ` s ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` s ) " ( ( j + 1 ) ... ( m + 1 ) ) ) X. { 0 } ) ) ) u. ( ( ( ( m + 1 ) + 1 ) ... N ) X. { 0 } ) ) )
269 268 csbeq1d 
 |-  ( q = ( ( 1st ` s ) oF + ( ( ( ( 2nd ` s ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` s ) " ( ( j + 1 ) ... ( m + 1 ) ) ) X. { 0 } ) ) ) -> [_ ( q u. ( ( ( ( m + 1 ) + 1 ) ... N ) X. { 0 } ) ) / p ]_ B = [_ ( ( ( 1st ` s ) oF + ( ( ( ( 2nd ` s ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` s ) " ( ( j + 1 ) ... ( m + 1 ) ) ) X. { 0 } ) ) ) u. ( ( ( ( m + 1 ) + 1 ) ... N ) X. { 0 } ) ) / p ]_ B )
270 75 fconst 
 |-  ( ( ( ( m + 1 ) + 1 ) ... N ) X. { 0 } ) : ( ( ( m + 1 ) + 1 ) ... N ) --> { 0 }
271 270 jctr 
 |-  ( q : ( 1 ... ( m + 1 ) ) --> ( 0 ... K ) -> ( q : ( 1 ... ( m + 1 ) ) --> ( 0 ... K ) /\ ( ( ( ( m + 1 ) + 1 ) ... N ) X. { 0 } ) : ( ( ( m + 1 ) + 1 ) ... N ) --> { 0 } ) )
272 266 nnred 
 |-  ( m e. NN0 -> ( m + 1 ) e. RR )
273 272 ltp1d 
 |-  ( m e. NN0 -> ( m + 1 ) < ( ( m + 1 ) + 1 ) )
274 fzdisj 
 |-  ( ( m + 1 ) < ( ( m + 1 ) + 1 ) -> ( ( 1 ... ( m + 1 ) ) i^i ( ( ( m + 1 ) + 1 ) ... N ) ) = (/) )
275 273 274 syl 
 |-  ( m e. NN0 -> ( ( 1 ... ( m + 1 ) ) i^i ( ( ( m + 1 ) + 1 ) ... N ) ) = (/) )
276 fun 
 |-  ( ( ( q : ( 1 ... ( m + 1 ) ) --> ( 0 ... K ) /\ ( ( ( ( m + 1 ) + 1 ) ... N ) X. { 0 } ) : ( ( ( m + 1 ) + 1 ) ... N ) --> { 0 } ) /\ ( ( 1 ... ( m + 1 ) ) i^i ( ( ( m + 1 ) + 1 ) ... N ) ) = (/) ) -> ( q u. ( ( ( ( m + 1 ) + 1 ) ... N ) X. { 0 } ) ) : ( ( 1 ... ( m + 1 ) ) u. ( ( ( m + 1 ) + 1 ) ... N ) ) --> ( ( 0 ... K ) u. { 0 } ) )
277 271 275 276 syl2anr 
 |-  ( ( m e. NN0 /\ q : ( 1 ... ( m + 1 ) ) --> ( 0 ... K ) ) -> ( q u. ( ( ( ( m + 1 ) + 1 ) ... N ) X. { 0 } ) ) : ( ( 1 ... ( m + 1 ) ) u. ( ( ( m + 1 ) + 1 ) ... N ) ) --> ( ( 0 ... K ) u. { 0 } ) )
278 277 adantlr 
 |-  ( ( ( m e. NN0 /\ m < N ) /\ q : ( 1 ... ( m + 1 ) ) --> ( 0 ... K ) ) -> ( q u. ( ( ( ( m + 1 ) + 1 ) ... N ) X. { 0 } ) ) : ( ( 1 ... ( m + 1 ) ) u. ( ( ( m + 1 ) + 1 ) ... N ) ) --> ( ( 0 ... K ) u. { 0 } ) )
279 278 adantl 
 |-  ( ( ph /\ ( ( m e. NN0 /\ m < N ) /\ q : ( 1 ... ( m + 1 ) ) --> ( 0 ... K ) ) ) -> ( q u. ( ( ( ( m + 1 ) + 1 ) ... N ) X. { 0 } ) ) : ( ( 1 ... ( m + 1 ) ) u. ( ( ( m + 1 ) + 1 ) ... N ) ) --> ( ( 0 ... K ) u. { 0 } ) )
280 266 peano2nnd 
 |-  ( m e. NN0 -> ( ( m + 1 ) + 1 ) e. NN )
281 280 192 eleqtrdi 
 |-  ( m e. NN0 -> ( ( m + 1 ) + 1 ) e. ( ZZ>= ` 1 ) )
282 281 ad2antrl 
 |-  ( ( ph /\ ( m e. NN0 /\ m < N ) ) -> ( ( m + 1 ) + 1 ) e. ( ZZ>= ` 1 ) )
283 nn0z 
 |-  ( m e. NN0 -> m e. ZZ )
284 1 nnzd 
 |-  ( ph -> N e. ZZ )
285 zltp1le 
 |-  ( ( m e. ZZ /\ N e. ZZ ) -> ( m < N <-> ( m + 1 ) <_ N ) )
286 283 284 285 syl2anr 
 |-  ( ( ph /\ m e. NN0 ) -> ( m < N <-> ( m + 1 ) <_ N ) )
287 286 biimpa 
 |-  ( ( ( ph /\ m e. NN0 ) /\ m < N ) -> ( m + 1 ) <_ N )
288 287 anasss 
 |-  ( ( ph /\ ( m e. NN0 /\ m < N ) ) -> ( m + 1 ) <_ N )
289 283 peano2zd 
 |-  ( m e. NN0 -> ( m + 1 ) e. ZZ )
290 289 adantr 
 |-  ( ( m e. NN0 /\ m < N ) -> ( m + 1 ) e. ZZ )
291 eluz 
 |-  ( ( ( m + 1 ) e. ZZ /\ N e. ZZ ) -> ( N e. ( ZZ>= ` ( m + 1 ) ) <-> ( m + 1 ) <_ N ) )
292 290 284 291 syl2anr 
 |-  ( ( ph /\ ( m e. NN0 /\ m < N ) ) -> ( N e. ( ZZ>= ` ( m + 1 ) ) <-> ( m + 1 ) <_ N ) )
293 288 292 mpbird 
 |-  ( ( ph /\ ( m e. NN0 /\ m < N ) ) -> N e. ( ZZ>= ` ( m + 1 ) ) )
294 fzsplit2 
 |-  ( ( ( ( m + 1 ) + 1 ) e. ( ZZ>= ` 1 ) /\ N e. ( ZZ>= ` ( m + 1 ) ) ) -> ( 1 ... N ) = ( ( 1 ... ( m + 1 ) ) u. ( ( ( m + 1 ) + 1 ) ... N ) ) )
295 282 293 294 syl2anc 
 |-  ( ( ph /\ ( m e. NN0 /\ m < N ) ) -> ( 1 ... N ) = ( ( 1 ... ( m + 1 ) ) u. ( ( ( m + 1 ) + 1 ) ... N ) ) )
296 295 eqcomd 
 |-  ( ( ph /\ ( m e. NN0 /\ m < N ) ) -> ( ( 1 ... ( m + 1 ) ) u. ( ( ( m + 1 ) + 1 ) ... N ) ) = ( 1 ... N ) )
297 196 197 syl 
 |-  ( ph -> 0 e. ( 0 ... K ) )
298 297 snssd 
 |-  ( ph -> { 0 } C_ ( 0 ... K ) )
299 ssequn2 
 |-  ( { 0 } C_ ( 0 ... K ) <-> ( ( 0 ... K ) u. { 0 } ) = ( 0 ... K ) )
300 298 299 sylib 
 |-  ( ph -> ( ( 0 ... K ) u. { 0 } ) = ( 0 ... K ) )
301 300 adantr 
 |-  ( ( ph /\ ( m e. NN0 /\ m < N ) ) -> ( ( 0 ... K ) u. { 0 } ) = ( 0 ... K ) )
302 296 301 feq23d 
 |-  ( ( ph /\ ( m e. NN0 /\ m < N ) ) -> ( ( q u. ( ( ( ( m + 1 ) + 1 ) ... N ) X. { 0 } ) ) : ( ( 1 ... ( m + 1 ) ) u. ( ( ( m + 1 ) + 1 ) ... N ) ) --> ( ( 0 ... K ) u. { 0 } ) <-> ( q u. ( ( ( ( m + 1 ) + 1 ) ... N ) X. { 0 } ) ) : ( 1 ... N ) --> ( 0 ... K ) ) )
303 302 adantrr 
 |-  ( ( ph /\ ( ( m e. NN0 /\ m < N ) /\ q : ( 1 ... ( m + 1 ) ) --> ( 0 ... K ) ) ) -> ( ( q u. ( ( ( ( m + 1 ) + 1 ) ... N ) X. { 0 } ) ) : ( ( 1 ... ( m + 1 ) ) u. ( ( ( m + 1 ) + 1 ) ... N ) ) --> ( ( 0 ... K ) u. { 0 } ) <-> ( q u. ( ( ( ( m + 1 ) + 1 ) ... N ) X. { 0 } ) ) : ( 1 ... N ) --> ( 0 ... K ) ) )
304 279 303 mpbid 
 |-  ( ( ph /\ ( ( m e. NN0 /\ m < N ) /\ q : ( 1 ... ( m + 1 ) ) --> ( 0 ... K ) ) ) -> ( q u. ( ( ( ( m + 1 ) + 1 ) ... N ) X. { 0 } ) ) : ( 1 ... N ) --> ( 0 ... K ) )
305 nfv 
 |-  F/ p ( ph /\ ( q u. ( ( ( ( m + 1 ) + 1 ) ... N ) X. { 0 } ) ) : ( 1 ... N ) --> ( 0 ... K ) )
306 nfcsb1v 
 |-  F/_ p [_ ( q u. ( ( ( ( m + 1 ) + 1 ) ... N ) X. { 0 } ) ) / p ]_ B
307 306 nfel1 
 |-  F/ p [_ ( q u. ( ( ( ( m + 1 ) + 1 ) ... N ) X. { 0 } ) ) / p ]_ B e. ( 0 ... N )
308 305 307 nfim 
 |-  F/ p ( ( ph /\ ( q u. ( ( ( ( m + 1 ) + 1 ) ... N ) X. { 0 } ) ) : ( 1 ... N ) --> ( 0 ... K ) ) -> [_ ( q u. ( ( ( ( m + 1 ) + 1 ) ... N ) X. { 0 } ) ) / p ]_ B e. ( 0 ... N ) )
309 vex 
 |-  q e. _V
310 ovex 
 |-  ( ( ( m + 1 ) + 1 ) ... N ) e. _V
311 310 208 xpex 
 |-  ( ( ( ( m + 1 ) + 1 ) ... N ) X. { 0 } ) e. _V
312 309 311 unex 
 |-  ( q u. ( ( ( ( m + 1 ) + 1 ) ... N ) X. { 0 } ) ) e. _V
313 feq1 
 |-  ( p = ( q u. ( ( ( ( m + 1 ) + 1 ) ... N ) X. { 0 } ) ) -> ( p : ( 1 ... N ) --> ( 0 ... K ) <-> ( q u. ( ( ( ( m + 1 ) + 1 ) ... N ) X. { 0 } ) ) : ( 1 ... N ) --> ( 0 ... K ) ) )
314 313 anbi2d 
 |-  ( p = ( q u. ( ( ( ( m + 1 ) + 1 ) ... N ) X. { 0 } ) ) -> ( ( ph /\ p : ( 1 ... N ) --> ( 0 ... K ) ) <-> ( ph /\ ( q u. ( ( ( ( m + 1 ) + 1 ) ... N ) X. { 0 } ) ) : ( 1 ... N ) --> ( 0 ... K ) ) ) )
315 csbeq1a 
 |-  ( p = ( q u. ( ( ( ( m + 1 ) + 1 ) ... N ) X. { 0 } ) ) -> B = [_ ( q u. ( ( ( ( m + 1 ) + 1 ) ... N ) X. { 0 } ) ) / p ]_ B )
316 315 eleq1d 
 |-  ( p = ( q u. ( ( ( ( m + 1 ) + 1 ) ... N ) X. { 0 } ) ) -> ( B e. ( 0 ... N ) <-> [_ ( q u. ( ( ( ( m + 1 ) + 1 ) ... N ) X. { 0 } ) ) / p ]_ B e. ( 0 ... N ) ) )
317 314 316 imbi12d 
 |-  ( p = ( q u. ( ( ( ( m + 1 ) + 1 ) ... N ) X. { 0 } ) ) -> ( ( ( ph /\ p : ( 1 ... N ) --> ( 0 ... K ) ) -> B e. ( 0 ... N ) ) <-> ( ( ph /\ ( q u. ( ( ( ( m + 1 ) + 1 ) ... N ) X. { 0 } ) ) : ( 1 ... N ) --> ( 0 ... K ) ) -> [_ ( q u. ( ( ( ( m + 1 ) + 1 ) ... N ) X. { 0 } ) ) / p ]_ B e. ( 0 ... N ) ) ) )
318 308 312 317 3 vtoclf 
 |-  ( ( ph /\ ( q u. ( ( ( ( m + 1 ) + 1 ) ... N ) X. { 0 } ) ) : ( 1 ... N ) --> ( 0 ... K ) ) -> [_ ( q u. ( ( ( ( m + 1 ) + 1 ) ... N ) X. { 0 } ) ) / p ]_ B e. ( 0 ... N ) )
319 304 318 syldan 
 |-  ( ( ph /\ ( ( m e. NN0 /\ m < N ) /\ q : ( 1 ... ( m + 1 ) ) --> ( 0 ... K ) ) ) -> [_ ( q u. ( ( ( ( m + 1 ) + 1 ) ... N ) X. { 0 } ) ) / p ]_ B e. ( 0 ... N ) )
320 319 anassrs 
 |-  ( ( ( ph /\ ( m e. NN0 /\ m < N ) ) /\ q : ( 1 ... ( m + 1 ) ) --> ( 0 ... K ) ) -> [_ ( q u. ( ( ( ( m + 1 ) + 1 ) ... N ) X. { 0 } ) ) / p ]_ B e. ( 0 ... N ) )
321 elfznn0 
 |-  ( [_ ( q u. ( ( ( ( m + 1 ) + 1 ) ... N ) X. { 0 } ) ) / p ]_ B e. ( 0 ... N ) -> [_ ( q u. ( ( ( ( m + 1 ) + 1 ) ... N ) X. { 0 } ) ) / p ]_ B e. NN0 )
322 320 321 syl 
 |-  ( ( ( ph /\ ( m e. NN0 /\ m < N ) ) /\ q : ( 1 ... ( m + 1 ) ) --> ( 0 ... K ) ) -> [_ ( q u. ( ( ( ( m + 1 ) + 1 ) ... N ) X. { 0 } ) ) / p ]_ B e. NN0 )
323 266 nnnn0d 
 |-  ( m e. NN0 -> ( m + 1 ) e. NN0 )
324 323 adantr 
 |-  ( ( m e. NN0 /\ m < N ) -> ( m + 1 ) e. NN0 )
325 324 ad2antlr 
 |-  ( ( ( ph /\ ( m e. NN0 /\ m < N ) ) /\ q : ( 1 ... ( m + 1 ) ) --> ( 0 ... K ) ) -> ( m + 1 ) e. NN0 )
326 leloe 
 |-  ( ( ( m + 1 ) e. RR /\ N e. RR ) -> ( ( m + 1 ) <_ N <-> ( ( m + 1 ) < N \/ ( m + 1 ) = N ) ) )
327 272 8 326 syl2anr 
 |-  ( ( ph /\ m e. NN0 ) -> ( ( m + 1 ) <_ N <-> ( ( m + 1 ) < N \/ ( m + 1 ) = N ) ) )
328 286 327 bitrd 
 |-  ( ( ph /\ m e. NN0 ) -> ( m < N <-> ( ( m + 1 ) < N \/ ( m + 1 ) = N ) ) )
329 328 biimpd 
 |-  ( ( ph /\ m e. NN0 ) -> ( m < N -> ( ( m + 1 ) < N \/ ( m + 1 ) = N ) ) )
330 329 imdistani 
 |-  ( ( ( ph /\ m e. NN0 ) /\ m < N ) -> ( ( ph /\ m e. NN0 ) /\ ( ( m + 1 ) < N \/ ( m + 1 ) = N ) ) )
331 330 anasss 
 |-  ( ( ph /\ ( m e. NN0 /\ m < N ) ) -> ( ( ph /\ m e. NN0 ) /\ ( ( m + 1 ) < N \/ ( m + 1 ) = N ) ) )
332 simplll 
 |-  ( ( ( ( ph /\ m e. NN0 ) /\ q : ( 1 ... ( m + 1 ) ) --> ( 0 ... K ) ) /\ ( m + 1 ) < N ) -> ph )
333 280 nnge1d 
 |-  ( m e. NN0 -> 1 <_ ( ( m + 1 ) + 1 ) )
334 333 ad2antlr 
 |-  ( ( ( ph /\ m e. NN0 ) /\ ( m + 1 ) < N ) -> 1 <_ ( ( m + 1 ) + 1 ) )
335 zltp1le 
 |-  ( ( ( m + 1 ) e. ZZ /\ N e. ZZ ) -> ( ( m + 1 ) < N <-> ( ( m + 1 ) + 1 ) <_ N ) )
336 289 284 335 syl2anr 
 |-  ( ( ph /\ m e. NN0 ) -> ( ( m + 1 ) < N <-> ( ( m + 1 ) + 1 ) <_ N ) )
337 336 biimpa 
 |-  ( ( ( ph /\ m e. NN0 ) /\ ( m + 1 ) < N ) -> ( ( m + 1 ) + 1 ) <_ N )
338 289 peano2zd 
 |-  ( m e. NN0 -> ( ( m + 1 ) + 1 ) e. ZZ )
339 1z 
 |-  1 e. ZZ
340 elfz 
 |-  ( ( ( ( m + 1 ) + 1 ) e. ZZ /\ 1 e. ZZ /\ N e. ZZ ) -> ( ( ( m + 1 ) + 1 ) e. ( 1 ... N ) <-> ( 1 <_ ( ( m + 1 ) + 1 ) /\ ( ( m + 1 ) + 1 ) <_ N ) ) )
341 339 340 mp3an2 
 |-  ( ( ( ( m + 1 ) + 1 ) e. ZZ /\ N e. ZZ ) -> ( ( ( m + 1 ) + 1 ) e. ( 1 ... N ) <-> ( 1 <_ ( ( m + 1 ) + 1 ) /\ ( ( m + 1 ) + 1 ) <_ N ) ) )
342 338 284 341 syl2anr 
 |-  ( ( ph /\ m e. NN0 ) -> ( ( ( m + 1 ) + 1 ) e. ( 1 ... N ) <-> ( 1 <_ ( ( m + 1 ) + 1 ) /\ ( ( m + 1 ) + 1 ) <_ N ) ) )
343 342 adantr 
 |-  ( ( ( ph /\ m e. NN0 ) /\ ( m + 1 ) < N ) -> ( ( ( m + 1 ) + 1 ) e. ( 1 ... N ) <-> ( 1 <_ ( ( m + 1 ) + 1 ) /\ ( ( m + 1 ) + 1 ) <_ N ) ) )
344 334 337 343 mpbir2and 
 |-  ( ( ( ph /\ m e. NN0 ) /\ ( m + 1 ) < N ) -> ( ( m + 1 ) + 1 ) e. ( 1 ... N ) )
345 344 adantlr 
 |-  ( ( ( ( ph /\ m e. NN0 ) /\ q : ( 1 ... ( m + 1 ) ) --> ( 0 ... K ) ) /\ ( m + 1 ) < N ) -> ( ( m + 1 ) + 1 ) e. ( 1 ... N ) )
346 nn0re 
 |-  ( m e. NN0 -> m e. RR )
347 346 ad2antlr 
 |-  ( ( ( ph /\ m e. NN0 ) /\ ( m + 1 ) < N ) -> m e. RR )
348 272 ad2antlr 
 |-  ( ( ( ph /\ m e. NN0 ) /\ ( m + 1 ) < N ) -> ( m + 1 ) e. RR )
349 8 ad2antrr 
 |-  ( ( ( ph /\ m e. NN0 ) /\ ( m + 1 ) < N ) -> N e. RR )
350 346 ltp1d 
 |-  ( m e. NN0 -> m < ( m + 1 ) )
351 350 ad2antlr 
 |-  ( ( ( ph /\ m e. NN0 ) /\ ( m + 1 ) < N ) -> m < ( m + 1 ) )
352 simpr 
 |-  ( ( ( ph /\ m e. NN0 ) /\ ( m + 1 ) < N ) -> ( m + 1 ) < N )
353 347 348 349 351 352 lttrd 
 |-  ( ( ( ph /\ m e. NN0 ) /\ ( m + 1 ) < N ) -> m < N )
354 353 adantlr 
 |-  ( ( ( ( ph /\ m e. NN0 ) /\ q : ( 1 ... ( m + 1 ) ) --> ( 0 ... K ) ) /\ ( m + 1 ) < N ) -> m < N )
355 anass 
 |-  ( ( ( ph /\ m e. NN0 ) /\ m < N ) <-> ( ph /\ ( m e. NN0 /\ m < N ) ) )
356 304 anassrs 
 |-  ( ( ( ph /\ ( m e. NN0 /\ m < N ) ) /\ q : ( 1 ... ( m + 1 ) ) --> ( 0 ... K ) ) -> ( q u. ( ( ( ( m + 1 ) + 1 ) ... N ) X. { 0 } ) ) : ( 1 ... N ) --> ( 0 ... K ) )
357 355 356 sylanb 
 |-  ( ( ( ( ph /\ m e. NN0 ) /\ m < N ) /\ q : ( 1 ... ( m + 1 ) ) --> ( 0 ... K ) ) -> ( q u. ( ( ( ( m + 1 ) + 1 ) ... N ) X. { 0 } ) ) : ( 1 ... N ) --> ( 0 ... K ) )
358 357 an32s 
 |-  ( ( ( ( ph /\ m e. NN0 ) /\ q : ( 1 ... ( m + 1 ) ) --> ( 0 ... K ) ) /\ m < N ) -> ( q u. ( ( ( ( m + 1 ) + 1 ) ... N ) X. { 0 } ) ) : ( 1 ... N ) --> ( 0 ... K ) )
359 354 358 syldan 
 |-  ( ( ( ( ph /\ m e. NN0 ) /\ q : ( 1 ... ( m + 1 ) ) --> ( 0 ... K ) ) /\ ( m + 1 ) < N ) -> ( q u. ( ( ( ( m + 1 ) + 1 ) ... N ) X. { 0 } ) ) : ( 1 ... N ) --> ( 0 ... K ) )
360 ffn 
 |-  ( q : ( 1 ... ( m + 1 ) ) --> ( 0 ... K ) -> q Fn ( 1 ... ( m + 1 ) ) )
361 360 ad2antlr 
 |-  ( ( ( ( ph /\ m e. NN0 ) /\ q : ( 1 ... ( m + 1 ) ) --> ( 0 ... K ) ) /\ ( m + 1 ) < N ) -> q Fn ( 1 ... ( m + 1 ) ) )
362 275 ad3antlr 
 |-  ( ( ( ( ph /\ m e. NN0 ) /\ q : ( 1 ... ( m + 1 ) ) --> ( 0 ... K ) ) /\ ( m + 1 ) < N ) -> ( ( 1 ... ( m + 1 ) ) i^i ( ( ( m + 1 ) + 1 ) ... N ) ) = (/) )
363 eluz 
 |-  ( ( ( ( m + 1 ) + 1 ) e. ZZ /\ N e. ZZ ) -> ( N e. ( ZZ>= ` ( ( m + 1 ) + 1 ) ) <-> ( ( m + 1 ) + 1 ) <_ N ) )
364 338 284 363 syl2anr 
 |-  ( ( ph /\ m e. NN0 ) -> ( N e. ( ZZ>= ` ( ( m + 1 ) + 1 ) ) <-> ( ( m + 1 ) + 1 ) <_ N ) )
365 364 adantr 
 |-  ( ( ( ph /\ m e. NN0 ) /\ ( m + 1 ) < N ) -> ( N e. ( ZZ>= ` ( ( m + 1 ) + 1 ) ) <-> ( ( m + 1 ) + 1 ) <_ N ) )
366 337 365 mpbird 
 |-  ( ( ( ph /\ m e. NN0 ) /\ ( m + 1 ) < N ) -> N e. ( ZZ>= ` ( ( m + 1 ) + 1 ) ) )
367 eluzfz1 
 |-  ( N e. ( ZZ>= ` ( ( m + 1 ) + 1 ) ) -> ( ( m + 1 ) + 1 ) e. ( ( ( m + 1 ) + 1 ) ... N ) )
368 366 367 syl 
 |-  ( ( ( ph /\ m e. NN0 ) /\ ( m + 1 ) < N ) -> ( ( m + 1 ) + 1 ) e. ( ( ( m + 1 ) + 1 ) ... N ) )
369 368 adantlr 
 |-  ( ( ( ( ph /\ m e. NN0 ) /\ q : ( 1 ... ( m + 1 ) ) --> ( 0 ... K ) ) /\ ( m + 1 ) < N ) -> ( ( m + 1 ) + 1 ) e. ( ( ( m + 1 ) + 1 ) ... N ) )
370 fnconstg 
 |-  ( 0 e. _V -> ( ( ( ( m + 1 ) + 1 ) ... N ) X. { 0 } ) Fn ( ( ( m + 1 ) + 1 ) ... N ) )
371 75 370 ax-mp 
 |-  ( ( ( ( m + 1 ) + 1 ) ... N ) X. { 0 } ) Fn ( ( ( m + 1 ) + 1 ) ... N )
372 fvun2 
 |-  ( ( q Fn ( 1 ... ( m + 1 ) ) /\ ( ( ( ( m + 1 ) + 1 ) ... N ) X. { 0 } ) Fn ( ( ( m + 1 ) + 1 ) ... N ) /\ ( ( ( 1 ... ( m + 1 ) ) i^i ( ( ( m + 1 ) + 1 ) ... N ) ) = (/) /\ ( ( m + 1 ) + 1 ) e. ( ( ( m + 1 ) + 1 ) ... N ) ) ) -> ( ( q u. ( ( ( ( m + 1 ) + 1 ) ... N ) X. { 0 } ) ) ` ( ( m + 1 ) + 1 ) ) = ( ( ( ( ( m + 1 ) + 1 ) ... N ) X. { 0 } ) ` ( ( m + 1 ) + 1 ) ) )
373 371 372 mp3an2 
 |-  ( ( q Fn ( 1 ... ( m + 1 ) ) /\ ( ( ( 1 ... ( m + 1 ) ) i^i ( ( ( m + 1 ) + 1 ) ... N ) ) = (/) /\ ( ( m + 1 ) + 1 ) e. ( ( ( m + 1 ) + 1 ) ... N ) ) ) -> ( ( q u. ( ( ( ( m + 1 ) + 1 ) ... N ) X. { 0 } ) ) ` ( ( m + 1 ) + 1 ) ) = ( ( ( ( ( m + 1 ) + 1 ) ... N ) X. { 0 } ) ` ( ( m + 1 ) + 1 ) ) )
374 361 362 369 373 syl12anc 
 |-  ( ( ( ( ph /\ m e. NN0 ) /\ q : ( 1 ... ( m + 1 ) ) --> ( 0 ... K ) ) /\ ( m + 1 ) < N ) -> ( ( q u. ( ( ( ( m + 1 ) + 1 ) ... N ) X. { 0 } ) ) ` ( ( m + 1 ) + 1 ) ) = ( ( ( ( ( m + 1 ) + 1 ) ... N ) X. { 0 } ) ` ( ( m + 1 ) + 1 ) ) )
375 75 fvconst2 
 |-  ( ( ( m + 1 ) + 1 ) e. ( ( ( m + 1 ) + 1 ) ... N ) -> ( ( ( ( ( m + 1 ) + 1 ) ... N ) X. { 0 } ) ` ( ( m + 1 ) + 1 ) ) = 0 )
376 369 375 syl 
 |-  ( ( ( ( ph /\ m e. NN0 ) /\ q : ( 1 ... ( m + 1 ) ) --> ( 0 ... K ) ) /\ ( m + 1 ) < N ) -> ( ( ( ( ( m + 1 ) + 1 ) ... N ) X. { 0 } ) ` ( ( m + 1 ) + 1 ) ) = 0 )
377 374 376 eqtrd 
 |-  ( ( ( ( ph /\ m e. NN0 ) /\ q : ( 1 ... ( m + 1 ) ) --> ( 0 ... K ) ) /\ ( m + 1 ) < N ) -> ( ( q u. ( ( ( ( m + 1 ) + 1 ) ... N ) X. { 0 } ) ) ` ( ( m + 1 ) + 1 ) ) = 0 )
378 nfv 
 |-  F/ p ( ph /\ ( ( ( m + 1 ) + 1 ) e. ( 1 ... N ) /\ ( q u. ( ( ( ( m + 1 ) + 1 ) ... N ) X. { 0 } ) ) : ( 1 ... N ) --> ( 0 ... K ) /\ ( ( q u. ( ( ( ( m + 1 ) + 1 ) ... N ) X. { 0 } ) ) ` ( ( m + 1 ) + 1 ) ) = 0 ) )
379 nfcv 
 |-  F/_ p <
380 nfcv 
 |-  F/_ p ( ( m + 1 ) + 1 )
381 306 379 380 nfbr 
 |-  F/ p [_ ( q u. ( ( ( ( m + 1 ) + 1 ) ... N ) X. { 0 } ) ) / p ]_ B < ( ( m + 1 ) + 1 )
382 378 381 nfim 
 |-  F/ p ( ( ph /\ ( ( ( m + 1 ) + 1 ) e. ( 1 ... N ) /\ ( q u. ( ( ( ( m + 1 ) + 1 ) ... N ) X. { 0 } ) ) : ( 1 ... N ) --> ( 0 ... K ) /\ ( ( q u. ( ( ( ( m + 1 ) + 1 ) ... N ) X. { 0 } ) ) ` ( ( m + 1 ) + 1 ) ) = 0 ) ) -> [_ ( q u. ( ( ( ( m + 1 ) + 1 ) ... N ) X. { 0 } ) ) / p ]_ B < ( ( m + 1 ) + 1 ) )
383 fveq1 
 |-  ( p = ( q u. ( ( ( ( m + 1 ) + 1 ) ... N ) X. { 0 } ) ) -> ( p ` ( ( m + 1 ) + 1 ) ) = ( ( q u. ( ( ( ( m + 1 ) + 1 ) ... N ) X. { 0 } ) ) ` ( ( m + 1 ) + 1 ) ) )
384 383 eqeq1d 
 |-  ( p = ( q u. ( ( ( ( m + 1 ) + 1 ) ... N ) X. { 0 } ) ) -> ( ( p ` ( ( m + 1 ) + 1 ) ) = 0 <-> ( ( q u. ( ( ( ( m + 1 ) + 1 ) ... N ) X. { 0 } ) ) ` ( ( m + 1 ) + 1 ) ) = 0 ) )
385 313 384 3anbi23d 
 |-  ( p = ( q u. ( ( ( ( m + 1 ) + 1 ) ... N ) X. { 0 } ) ) -> ( ( ( ( m + 1 ) + 1 ) e. ( 1 ... N ) /\ p : ( 1 ... N ) --> ( 0 ... K ) /\ ( p ` ( ( m + 1 ) + 1 ) ) = 0 ) <-> ( ( ( m + 1 ) + 1 ) e. ( 1 ... N ) /\ ( q u. ( ( ( ( m + 1 ) + 1 ) ... N ) X. { 0 } ) ) : ( 1 ... N ) --> ( 0 ... K ) /\ ( ( q u. ( ( ( ( m + 1 ) + 1 ) ... N ) X. { 0 } ) ) ` ( ( m + 1 ) + 1 ) ) = 0 ) ) )
386 385 anbi2d 
 |-  ( p = ( q u. ( ( ( ( m + 1 ) + 1 ) ... N ) X. { 0 } ) ) -> ( ( ph /\ ( ( ( m + 1 ) + 1 ) e. ( 1 ... N ) /\ p : ( 1 ... N ) --> ( 0 ... K ) /\ ( p ` ( ( m + 1 ) + 1 ) ) = 0 ) ) <-> ( ph /\ ( ( ( m + 1 ) + 1 ) e. ( 1 ... N ) /\ ( q u. ( ( ( ( m + 1 ) + 1 ) ... N ) X. { 0 } ) ) : ( 1 ... N ) --> ( 0 ... K ) /\ ( ( q u. ( ( ( ( m + 1 ) + 1 ) ... N ) X. { 0 } ) ) ` ( ( m + 1 ) + 1 ) ) = 0 ) ) ) )
387 315 breq1d 
 |-  ( p = ( q u. ( ( ( ( m + 1 ) + 1 ) ... N ) X. { 0 } ) ) -> ( B < ( ( m + 1 ) + 1 ) <-> [_ ( q u. ( ( ( ( m + 1 ) + 1 ) ... N ) X. { 0 } ) ) / p ]_ B < ( ( m + 1 ) + 1 ) ) )
388 386 387 imbi12d 
 |-  ( p = ( q u. ( ( ( ( m + 1 ) + 1 ) ... N ) X. { 0 } ) ) -> ( ( ( ph /\ ( ( ( m + 1 ) + 1 ) e. ( 1 ... N ) /\ p : ( 1 ... N ) --> ( 0 ... K ) /\ ( p ` ( ( m + 1 ) + 1 ) ) = 0 ) ) -> B < ( ( m + 1 ) + 1 ) ) <-> ( ( ph /\ ( ( ( m + 1 ) + 1 ) e. ( 1 ... N ) /\ ( q u. ( ( ( ( m + 1 ) + 1 ) ... N ) X. { 0 } ) ) : ( 1 ... N ) --> ( 0 ... K ) /\ ( ( q u. ( ( ( ( m + 1 ) + 1 ) ... N ) X. { 0 } ) ) ` ( ( m + 1 ) + 1 ) ) = 0 ) ) -> [_ ( q u. ( ( ( ( m + 1 ) + 1 ) ... N ) X. { 0 } ) ) / p ]_ B < ( ( m + 1 ) + 1 ) ) ) )
389 ovex 
 |-  ( ( m + 1 ) + 1 ) e. _V
390 eleq1 
 |-  ( n = ( ( m + 1 ) + 1 ) -> ( n e. ( 1 ... N ) <-> ( ( m + 1 ) + 1 ) e. ( 1 ... N ) ) )
391 fveqeq2 
 |-  ( n = ( ( m + 1 ) + 1 ) -> ( ( p ` n ) = 0 <-> ( p ` ( ( m + 1 ) + 1 ) ) = 0 ) )
392 390 391 3anbi13d 
 |-  ( n = ( ( m + 1 ) + 1 ) -> ( ( n e. ( 1 ... N ) /\ p : ( 1 ... N ) --> ( 0 ... K ) /\ ( p ` n ) = 0 ) <-> ( ( ( m + 1 ) + 1 ) e. ( 1 ... N ) /\ p : ( 1 ... N ) --> ( 0 ... K ) /\ ( p ` ( ( m + 1 ) + 1 ) ) = 0 ) ) )
393 392 anbi2d 
 |-  ( n = ( ( m + 1 ) + 1 ) -> ( ( ph /\ ( n e. ( 1 ... N ) /\ p : ( 1 ... N ) --> ( 0 ... K ) /\ ( p ` n ) = 0 ) ) <-> ( ph /\ ( ( ( m + 1 ) + 1 ) e. ( 1 ... N ) /\ p : ( 1 ... N ) --> ( 0 ... K ) /\ ( p ` ( ( m + 1 ) + 1 ) ) = 0 ) ) ) )
394 breq2 
 |-  ( n = ( ( m + 1 ) + 1 ) -> ( B < n <-> B < ( ( m + 1 ) + 1 ) ) )
395 393 394 imbi12d 
 |-  ( n = ( ( m + 1 ) + 1 ) -> ( ( ( ph /\ ( n e. ( 1 ... N ) /\ p : ( 1 ... N ) --> ( 0 ... K ) /\ ( p ` n ) = 0 ) ) -> B < n ) <-> ( ( ph /\ ( ( ( m + 1 ) + 1 ) e. ( 1 ... N ) /\ p : ( 1 ... N ) --> ( 0 ... K ) /\ ( p ` ( ( m + 1 ) + 1 ) ) = 0 ) ) -> B < ( ( m + 1 ) + 1 ) ) ) )
396 389 395 4 vtocl 
 |-  ( ( ph /\ ( ( ( m + 1 ) + 1 ) e. ( 1 ... N ) /\ p : ( 1 ... N ) --> ( 0 ... K ) /\ ( p ` ( ( m + 1 ) + 1 ) ) = 0 ) ) -> B < ( ( m + 1 ) + 1 ) )
397 382 312 388 396 vtoclf 
 |-  ( ( ph /\ ( ( ( m + 1 ) + 1 ) e. ( 1 ... N ) /\ ( q u. ( ( ( ( m + 1 ) + 1 ) ... N ) X. { 0 } ) ) : ( 1 ... N ) --> ( 0 ... K ) /\ ( ( q u. ( ( ( ( m + 1 ) + 1 ) ... N ) X. { 0 } ) ) ` ( ( m + 1 ) + 1 ) ) = 0 ) ) -> [_ ( q u. ( ( ( ( m + 1 ) + 1 ) ... N ) X. { 0 } ) ) / p ]_ B < ( ( m + 1 ) + 1 ) )
398 332 345 359 377 397 syl13anc 
 |-  ( ( ( ( ph /\ m e. NN0 ) /\ q : ( 1 ... ( m + 1 ) ) --> ( 0 ... K ) ) /\ ( m + 1 ) < N ) -> [_ ( q u. ( ( ( ( m + 1 ) + 1 ) ... N ) X. { 0 } ) ) / p ]_ B < ( ( m + 1 ) + 1 ) )
399 355 320 sylanb 
 |-  ( ( ( ( ph /\ m e. NN0 ) /\ m < N ) /\ q : ( 1 ... ( m + 1 ) ) --> ( 0 ... K ) ) -> [_ ( q u. ( ( ( ( m + 1 ) + 1 ) ... N ) X. { 0 } ) ) / p ]_ B e. ( 0 ... N ) )
400 399 an32s 
 |-  ( ( ( ( ph /\ m e. NN0 ) /\ q : ( 1 ... ( m + 1 ) ) --> ( 0 ... K ) ) /\ m < N ) -> [_ ( q u. ( ( ( ( m + 1 ) + 1 ) ... N ) X. { 0 } ) ) / p ]_ B e. ( 0 ... N ) )
401 400 elfzelzd 
 |-  ( ( ( ( ph /\ m e. NN0 ) /\ q : ( 1 ... ( m + 1 ) ) --> ( 0 ... K ) ) /\ m < N ) -> [_ ( q u. ( ( ( ( m + 1 ) + 1 ) ... N ) X. { 0 } ) ) / p ]_ B e. ZZ )
402 354 401 syldan 
 |-  ( ( ( ( ph /\ m e. NN0 ) /\ q : ( 1 ... ( m + 1 ) ) --> ( 0 ... K ) ) /\ ( m + 1 ) < N ) -> [_ ( q u. ( ( ( ( m + 1 ) + 1 ) ... N ) X. { 0 } ) ) / p ]_ B e. ZZ )
403 289 ad3antlr 
 |-  ( ( ( ( ph /\ m e. NN0 ) /\ q : ( 1 ... ( m + 1 ) ) --> ( 0 ... K ) ) /\ ( m + 1 ) < N ) -> ( m + 1 ) e. ZZ )
404 zleltp1 
 |-  ( ( [_ ( q u. ( ( ( ( m + 1 ) + 1 ) ... N ) X. { 0 } ) ) / p ]_ B e. ZZ /\ ( m + 1 ) e. ZZ ) -> ( [_ ( q u. ( ( ( ( m + 1 ) + 1 ) ... N ) X. { 0 } ) ) / p ]_ B <_ ( m + 1 ) <-> [_ ( q u. ( ( ( ( m + 1 ) + 1 ) ... N ) X. { 0 } ) ) / p ]_ B < ( ( m + 1 ) + 1 ) ) )
405 402 403 404 syl2anc 
 |-  ( ( ( ( ph /\ m e. NN0 ) /\ q : ( 1 ... ( m + 1 ) ) --> ( 0 ... K ) ) /\ ( m + 1 ) < N ) -> ( [_ ( q u. ( ( ( ( m + 1 ) + 1 ) ... N ) X. { 0 } ) ) / p ]_ B <_ ( m + 1 ) <-> [_ ( q u. ( ( ( ( m + 1 ) + 1 ) ... N ) X. { 0 } ) ) / p ]_ B < ( ( m + 1 ) + 1 ) ) )
406 398 405 mpbird 
 |-  ( ( ( ( ph /\ m e. NN0 ) /\ q : ( 1 ... ( m + 1 ) ) --> ( 0 ... K ) ) /\ ( m + 1 ) < N ) -> [_ ( q u. ( ( ( ( m + 1 ) + 1 ) ... N ) X. { 0 } ) ) / p ]_ B <_ ( m + 1 ) )
407 350 ad2antlr 
 |-  ( ( ( ph /\ m e. NN0 ) /\ q : ( 1 ... ( m + 1 ) ) --> ( 0 ... K ) ) -> m < ( m + 1 ) )
408 breq2 
 |-  ( ( m + 1 ) = N -> ( m < ( m + 1 ) <-> m < N ) )
409 408 biimpac 
 |-  ( ( m < ( m + 1 ) /\ ( m + 1 ) = N ) -> m < N )
410 407 409 sylan 
 |-  ( ( ( ( ph /\ m e. NN0 ) /\ q : ( 1 ... ( m + 1 ) ) --> ( 0 ... K ) ) /\ ( m + 1 ) = N ) -> m < N )
411 elfzle2 
 |-  ( [_ ( q u. ( ( ( ( m + 1 ) + 1 ) ... N ) X. { 0 } ) ) / p ]_ B e. ( 0 ... N ) -> [_ ( q u. ( ( ( ( m + 1 ) + 1 ) ... N ) X. { 0 } ) ) / p ]_ B <_ N )
412 400 411 syl 
 |-  ( ( ( ( ph /\ m e. NN0 ) /\ q : ( 1 ... ( m + 1 ) ) --> ( 0 ... K ) ) /\ m < N ) -> [_ ( q u. ( ( ( ( m + 1 ) + 1 ) ... N ) X. { 0 } ) ) / p ]_ B <_ N )
413 410 412 syldan 
 |-  ( ( ( ( ph /\ m e. NN0 ) /\ q : ( 1 ... ( m + 1 ) ) --> ( 0 ... K ) ) /\ ( m + 1 ) = N ) -> [_ ( q u. ( ( ( ( m + 1 ) + 1 ) ... N ) X. { 0 } ) ) / p ]_ B <_ N )
414 simpr 
 |-  ( ( ( ( ph /\ m e. NN0 ) /\ q : ( 1 ... ( m + 1 ) ) --> ( 0 ... K ) ) /\ ( m + 1 ) = N ) -> ( m + 1 ) = N )
415 413 414 breqtrrd 
 |-  ( ( ( ( ph /\ m e. NN0 ) /\ q : ( 1 ... ( m + 1 ) ) --> ( 0 ... K ) ) /\ ( m + 1 ) = N ) -> [_ ( q u. ( ( ( ( m + 1 ) + 1 ) ... N ) X. { 0 } ) ) / p ]_ B <_ ( m + 1 ) )
416 406 415 jaodan 
 |-  ( ( ( ( ph /\ m e. NN0 ) /\ q : ( 1 ... ( m + 1 ) ) --> ( 0 ... K ) ) /\ ( ( m + 1 ) < N \/ ( m + 1 ) = N ) ) -> [_ ( q u. ( ( ( ( m + 1 ) + 1 ) ... N ) X. { 0 } ) ) / p ]_ B <_ ( m + 1 ) )
417 416 an32s 
 |-  ( ( ( ( ph /\ m e. NN0 ) /\ ( ( m + 1 ) < N \/ ( m + 1 ) = N ) ) /\ q : ( 1 ... ( m + 1 ) ) --> ( 0 ... K ) ) -> [_ ( q u. ( ( ( ( m + 1 ) + 1 ) ... N ) X. { 0 } ) ) / p ]_ B <_ ( m + 1 ) )
418 331 417 sylan 
 |-  ( ( ( ph /\ ( m e. NN0 /\ m < N ) ) /\ q : ( 1 ... ( m + 1 ) ) --> ( 0 ... K ) ) -> [_ ( q u. ( ( ( ( m + 1 ) + 1 ) ... N ) X. { 0 } ) ) / p ]_ B <_ ( m + 1 ) )
419 elfz2nn0 
 |-  ( [_ ( q u. ( ( ( ( m + 1 ) + 1 ) ... N ) X. { 0 } ) ) / p ]_ B e. ( 0 ... ( m + 1 ) ) <-> ( [_ ( q u. ( ( ( ( m + 1 ) + 1 ) ... N ) X. { 0 } ) ) / p ]_ B e. NN0 /\ ( m + 1 ) e. NN0 /\ [_ ( q u. ( ( ( ( m + 1 ) + 1 ) ... N ) X. { 0 } ) ) / p ]_ B <_ ( m + 1 ) ) )
420 322 325 418 419 syl3anbrc 
 |-  ( ( ( ph /\ ( m e. NN0 /\ m < N ) ) /\ q : ( 1 ... ( m + 1 ) ) --> ( 0 ... K ) ) -> [_ ( q u. ( ( ( ( m + 1 ) + 1 ) ... N ) X. { 0 } ) ) / p ]_ B e. ( 0 ... ( m + 1 ) ) )
421 fzss2 
 |-  ( N e. ( ZZ>= ` ( m + 1 ) ) -> ( 1 ... ( m + 1 ) ) C_ ( 1 ... N ) )
422 293 421 syl 
 |-  ( ( ph /\ ( m e. NN0 /\ m < N ) ) -> ( 1 ... ( m + 1 ) ) C_ ( 1 ... N ) )
423 422 sselda 
 |-  ( ( ( ph /\ ( m e. NN0 /\ m < N ) ) /\ n e. ( 1 ... ( m + 1 ) ) ) -> n e. ( 1 ... N ) )
424 423 3ad2antr1 
 |-  ( ( ( ph /\ ( m e. NN0 /\ m < N ) ) /\ ( n e. ( 1 ... ( m + 1 ) ) /\ q : ( 1 ... ( m + 1 ) ) --> ( 0 ... K ) /\ ( q ` n ) = 0 ) ) -> n e. ( 1 ... N ) )
425 356 3ad2antr2 
 |-  ( ( ( ph /\ ( m e. NN0 /\ m < N ) ) /\ ( n e. ( 1 ... ( m + 1 ) ) /\ q : ( 1 ... ( m + 1 ) ) --> ( 0 ... K ) /\ ( q ` n ) = 0 ) ) -> ( q u. ( ( ( ( m + 1 ) + 1 ) ... N ) X. { 0 } ) ) : ( 1 ... N ) --> ( 0 ... K ) )
426 360 ad2antll 
 |-  ( ( ( ph /\ m e. NN0 ) /\ ( n e. ( 1 ... ( m + 1 ) ) /\ q : ( 1 ... ( m + 1 ) ) --> ( 0 ... K ) ) ) -> q Fn ( 1 ... ( m + 1 ) ) )
427 275 ad2antlr 
 |-  ( ( ( ph /\ m e. NN0 ) /\ ( n e. ( 1 ... ( m + 1 ) ) /\ q : ( 1 ... ( m + 1 ) ) --> ( 0 ... K ) ) ) -> ( ( 1 ... ( m + 1 ) ) i^i ( ( ( m + 1 ) + 1 ) ... N ) ) = (/) )
428 simprl 
 |-  ( ( ( ph /\ m e. NN0 ) /\ ( n e. ( 1 ... ( m + 1 ) ) /\ q : ( 1 ... ( m + 1 ) ) --> ( 0 ... K ) ) ) -> n e. ( 1 ... ( m + 1 ) ) )
429 fvun1 
 |-  ( ( q Fn ( 1 ... ( m + 1 ) ) /\ ( ( ( ( m + 1 ) + 1 ) ... N ) X. { 0 } ) Fn ( ( ( m + 1 ) + 1 ) ... N ) /\ ( ( ( 1 ... ( m + 1 ) ) i^i ( ( ( m + 1 ) + 1 ) ... N ) ) = (/) /\ n e. ( 1 ... ( m + 1 ) ) ) ) -> ( ( q u. ( ( ( ( m + 1 ) + 1 ) ... N ) X. { 0 } ) ) ` n ) = ( q ` n ) )
430 371 429 mp3an2 
 |-  ( ( q Fn ( 1 ... ( m + 1 ) ) /\ ( ( ( 1 ... ( m + 1 ) ) i^i ( ( ( m + 1 ) + 1 ) ... N ) ) = (/) /\ n e. ( 1 ... ( m + 1 ) ) ) ) -> ( ( q u. ( ( ( ( m + 1 ) + 1 ) ... N ) X. { 0 } ) ) ` n ) = ( q ` n ) )
431 426 427 428 430 syl12anc 
 |-  ( ( ( ph /\ m e. NN0 ) /\ ( n e. ( 1 ... ( m + 1 ) ) /\ q : ( 1 ... ( m + 1 ) ) --> ( 0 ... K ) ) ) -> ( ( q u. ( ( ( ( m + 1 ) + 1 ) ... N ) X. { 0 } ) ) ` n ) = ( q ` n ) )
432 431 adantlrr 
 |-  ( ( ( ph /\ ( m e. NN0 /\ m < N ) ) /\ ( n e. ( 1 ... ( m + 1 ) ) /\ q : ( 1 ... ( m + 1 ) ) --> ( 0 ... K ) ) ) -> ( ( q u. ( ( ( ( m + 1 ) + 1 ) ... N ) X. { 0 } ) ) ` n ) = ( q ` n ) )
433 432 3adantr3 
 |-  ( ( ( ph /\ ( m e. NN0 /\ m < N ) ) /\ ( n e. ( 1 ... ( m + 1 ) ) /\ q : ( 1 ... ( m + 1 ) ) --> ( 0 ... K ) /\ ( q ` n ) = 0 ) ) -> ( ( q u. ( ( ( ( m + 1 ) + 1 ) ... N ) X. { 0 } ) ) ` n ) = ( q ` n ) )
434 simpr3 
 |-  ( ( ( ph /\ ( m e. NN0 /\ m < N ) ) /\ ( n e. ( 1 ... ( m + 1 ) ) /\ q : ( 1 ... ( m + 1 ) ) --> ( 0 ... K ) /\ ( q ` n ) = 0 ) ) -> ( q ` n ) = 0 )
435 433 434 eqtrd 
 |-  ( ( ( ph /\ ( m e. NN0 /\ m < N ) ) /\ ( n e. ( 1 ... ( m + 1 ) ) /\ q : ( 1 ... ( m + 1 ) ) --> ( 0 ... K ) /\ ( q ` n ) = 0 ) ) -> ( ( q u. ( ( ( ( m + 1 ) + 1 ) ... N ) X. { 0 } ) ) ` n ) = 0 )
436 424 425 435 3jca 
 |-  ( ( ( ph /\ ( m e. NN0 /\ m < N ) ) /\ ( n e. ( 1 ... ( m + 1 ) ) /\ q : ( 1 ... ( m + 1 ) ) --> ( 0 ... K ) /\ ( q ` n ) = 0 ) ) -> ( n e. ( 1 ... N ) /\ ( q u. ( ( ( ( m + 1 ) + 1 ) ... N ) X. { 0 } ) ) : ( 1 ... N ) --> ( 0 ... K ) /\ ( ( q u. ( ( ( ( m + 1 ) + 1 ) ... N ) X. { 0 } ) ) ` n ) = 0 ) )
437 nfv 
 |-  F/ p ( ph /\ ( n e. ( 1 ... N ) /\ ( q u. ( ( ( ( m + 1 ) + 1 ) ... N ) X. { 0 } ) ) : ( 1 ... N ) --> ( 0 ... K ) /\ ( ( q u. ( ( ( ( m + 1 ) + 1 ) ... N ) X. { 0 } ) ) ` n ) = 0 ) )
438 nfcv 
 |-  F/_ p n
439 306 379 438 nfbr 
 |-  F/ p [_ ( q u. ( ( ( ( m + 1 ) + 1 ) ... N ) X. { 0 } ) ) / p ]_ B < n
440 437 439 nfim 
 |-  F/ p ( ( ph /\ ( n e. ( 1 ... N ) /\ ( q u. ( ( ( ( m + 1 ) + 1 ) ... N ) X. { 0 } ) ) : ( 1 ... N ) --> ( 0 ... K ) /\ ( ( q u. ( ( ( ( m + 1 ) + 1 ) ... N ) X. { 0 } ) ) ` n ) = 0 ) ) -> [_ ( q u. ( ( ( ( m + 1 ) + 1 ) ... N ) X. { 0 } ) ) / p ]_ B < n )
441 fveq1 
 |-  ( p = ( q u. ( ( ( ( m + 1 ) + 1 ) ... N ) X. { 0 } ) ) -> ( p ` n ) = ( ( q u. ( ( ( ( m + 1 ) + 1 ) ... N ) X. { 0 } ) ) ` n ) )
442 441 eqeq1d 
 |-  ( p = ( q u. ( ( ( ( m + 1 ) + 1 ) ... N ) X. { 0 } ) ) -> ( ( p ` n ) = 0 <-> ( ( q u. ( ( ( ( m + 1 ) + 1 ) ... N ) X. { 0 } ) ) ` n ) = 0 ) )
443 313 442 3anbi23d 
 |-  ( p = ( q u. ( ( ( ( m + 1 ) + 1 ) ... N ) X. { 0 } ) ) -> ( ( n e. ( 1 ... N ) /\ p : ( 1 ... N ) --> ( 0 ... K ) /\ ( p ` n ) = 0 ) <-> ( n e. ( 1 ... N ) /\ ( q u. ( ( ( ( m + 1 ) + 1 ) ... N ) X. { 0 } ) ) : ( 1 ... N ) --> ( 0 ... K ) /\ ( ( q u. ( ( ( ( m + 1 ) + 1 ) ... N ) X. { 0 } ) ) ` n ) = 0 ) ) )
444 443 anbi2d 
 |-  ( p = ( q u. ( ( ( ( m + 1 ) + 1 ) ... N ) X. { 0 } ) ) -> ( ( ph /\ ( n e. ( 1 ... N ) /\ p : ( 1 ... N ) --> ( 0 ... K ) /\ ( p ` n ) = 0 ) ) <-> ( ph /\ ( n e. ( 1 ... N ) /\ ( q u. ( ( ( ( m + 1 ) + 1 ) ... N ) X. { 0 } ) ) : ( 1 ... N ) --> ( 0 ... K ) /\ ( ( q u. ( ( ( ( m + 1 ) + 1 ) ... N ) X. { 0 } ) ) ` n ) = 0 ) ) ) )
445 315 breq1d 
 |-  ( p = ( q u. ( ( ( ( m + 1 ) + 1 ) ... N ) X. { 0 } ) ) -> ( B < n <-> [_ ( q u. ( ( ( ( m + 1 ) + 1 ) ... N ) X. { 0 } ) ) / p ]_ B < n ) )
446 444 445 imbi12d 
 |-  ( p = ( q u. ( ( ( ( m + 1 ) + 1 ) ... N ) X. { 0 } ) ) -> ( ( ( ph /\ ( n e. ( 1 ... N ) /\ p : ( 1 ... N ) --> ( 0 ... K ) /\ ( p ` n ) = 0 ) ) -> B < n ) <-> ( ( ph /\ ( n e. ( 1 ... N ) /\ ( q u. ( ( ( ( m + 1 ) + 1 ) ... N ) X. { 0 } ) ) : ( 1 ... N ) --> ( 0 ... K ) /\ ( ( q u. ( ( ( ( m + 1 ) + 1 ) ... N ) X. { 0 } ) ) ` n ) = 0 ) ) -> [_ ( q u. ( ( ( ( m + 1 ) + 1 ) ... N ) X. { 0 } ) ) / p ]_ B < n ) ) )
447 440 312 446 4 vtoclf 
 |-  ( ( ph /\ ( n e. ( 1 ... N ) /\ ( q u. ( ( ( ( m + 1 ) + 1 ) ... N ) X. { 0 } ) ) : ( 1 ... N ) --> ( 0 ... K ) /\ ( ( q u. ( ( ( ( m + 1 ) + 1 ) ... N ) X. { 0 } ) ) ` n ) = 0 ) ) -> [_ ( q u. ( ( ( ( m + 1 ) + 1 ) ... N ) X. { 0 } ) ) / p ]_ B < n )
448 447 adantlr 
 |-  ( ( ( ph /\ ( m e. NN0 /\ m < N ) ) /\ ( n e. ( 1 ... N ) /\ ( q u. ( ( ( ( m + 1 ) + 1 ) ... N ) X. { 0 } ) ) : ( 1 ... N ) --> ( 0 ... K ) /\ ( ( q u. ( ( ( ( m + 1 ) + 1 ) ... N ) X. { 0 } ) ) ` n ) = 0 ) ) -> [_ ( q u. ( ( ( ( m + 1 ) + 1 ) ... N ) X. { 0 } ) ) / p ]_ B < n )
449 436 448 syldan 
 |-  ( ( ( ph /\ ( m e. NN0 /\ m < N ) ) /\ ( n e. ( 1 ... ( m + 1 ) ) /\ q : ( 1 ... ( m + 1 ) ) --> ( 0 ... K ) /\ ( q ` n ) = 0 ) ) -> [_ ( q u. ( ( ( ( m + 1 ) + 1 ) ... N ) X. { 0 } ) ) / p ]_ B < n )
450 simp1 
 |-  ( ( n e. ( 1 ... ( m + 1 ) ) /\ q : ( 1 ... ( m + 1 ) ) --> ( 0 ... K ) /\ ( q ` n ) = K ) -> n e. ( 1 ... ( m + 1 ) ) )
451 423 anasss 
 |-  ( ( ph /\ ( ( m e. NN0 /\ m < N ) /\ n e. ( 1 ... ( m + 1 ) ) ) ) -> n e. ( 1 ... N ) )
452 450 451 sylanr2 
 |-  ( ( ph /\ ( ( m e. NN0 /\ m < N ) /\ ( n e. ( 1 ... ( m + 1 ) ) /\ q : ( 1 ... ( m + 1 ) ) --> ( 0 ... K ) /\ ( q ` n ) = K ) ) ) -> n e. ( 1 ... N ) )
453 simp2 
 |-  ( ( n e. ( 1 ... ( m + 1 ) ) /\ q : ( 1 ... ( m + 1 ) ) --> ( 0 ... K ) /\ ( q ` n ) = K ) -> q : ( 1 ... ( m + 1 ) ) --> ( 0 ... K ) )
454 453 304 sylanr2 
 |-  ( ( ph /\ ( ( m e. NN0 /\ m < N ) /\ ( n e. ( 1 ... ( m + 1 ) ) /\ q : ( 1 ... ( m + 1 ) ) --> ( 0 ... K ) /\ ( q ` n ) = K ) ) ) -> ( q u. ( ( ( ( m + 1 ) + 1 ) ... N ) X. { 0 } ) ) : ( 1 ... N ) --> ( 0 ... K ) )
455 431 3adantr3 
 |-  ( ( ( ph /\ m e. NN0 ) /\ ( n e. ( 1 ... ( m + 1 ) ) /\ q : ( 1 ... ( m + 1 ) ) --> ( 0 ... K ) /\ ( q ` n ) = K ) ) -> ( ( q u. ( ( ( ( m + 1 ) + 1 ) ... N ) X. { 0 } ) ) ` n ) = ( q ` n ) )
456 simpr3 
 |-  ( ( ( ph /\ m e. NN0 ) /\ ( n e. ( 1 ... ( m + 1 ) ) /\ q : ( 1 ... ( m + 1 ) ) --> ( 0 ... K ) /\ ( q ` n ) = K ) ) -> ( q ` n ) = K )
457 455 456 eqtrd 
 |-  ( ( ( ph /\ m e. NN0 ) /\ ( n e. ( 1 ... ( m + 1 ) ) /\ q : ( 1 ... ( m + 1 ) ) --> ( 0 ... K ) /\ ( q ` n ) = K ) ) -> ( ( q u. ( ( ( ( m + 1 ) + 1 ) ... N ) X. { 0 } ) ) ` n ) = K )
458 457 anasss 
 |-  ( ( ph /\ ( m e. NN0 /\ ( n e. ( 1 ... ( m + 1 ) ) /\ q : ( 1 ... ( m + 1 ) ) --> ( 0 ... K ) /\ ( q ` n ) = K ) ) ) -> ( ( q u. ( ( ( ( m + 1 ) + 1 ) ... N ) X. { 0 } ) ) ` n ) = K )
459 458 adantrlr 
 |-  ( ( ph /\ ( ( m e. NN0 /\ m < N ) /\ ( n e. ( 1 ... ( m + 1 ) ) /\ q : ( 1 ... ( m + 1 ) ) --> ( 0 ... K ) /\ ( q ` n ) = K ) ) ) -> ( ( q u. ( ( ( ( m + 1 ) + 1 ) ... N ) X. { 0 } ) ) ` n ) = K )
460 452 454 459 3jca 
 |-  ( ( ph /\ ( ( m e. NN0 /\ m < N ) /\ ( n e. ( 1 ... ( m + 1 ) ) /\ q : ( 1 ... ( m + 1 ) ) --> ( 0 ... K ) /\ ( q ` n ) = K ) ) ) -> ( n e. ( 1 ... N ) /\ ( q u. ( ( ( ( m + 1 ) + 1 ) ... N ) X. { 0 } ) ) : ( 1 ... N ) --> ( 0 ... K ) /\ ( ( q u. ( ( ( ( m + 1 ) + 1 ) ... N ) X. { 0 } ) ) ` n ) = K ) )
461 nfv 
 |-  F/ p ( ph /\ ( n e. ( 1 ... N ) /\ ( q u. ( ( ( ( m + 1 ) + 1 ) ... N ) X. { 0 } ) ) : ( 1 ... N ) --> ( 0 ... K ) /\ ( ( q u. ( ( ( ( m + 1 ) + 1 ) ... N ) X. { 0 } ) ) ` n ) = K ) )
462 nfcv 
 |-  F/_ p ( n - 1 )
463 306 462 nfne 
 |-  F/ p [_ ( q u. ( ( ( ( m + 1 ) + 1 ) ... N ) X. { 0 } ) ) / p ]_ B =/= ( n - 1 )
464 461 463 nfim 
 |-  F/ p ( ( ph /\ ( n e. ( 1 ... N ) /\ ( q u. ( ( ( ( m + 1 ) + 1 ) ... N ) X. { 0 } ) ) : ( 1 ... N ) --> ( 0 ... K ) /\ ( ( q u. ( ( ( ( m + 1 ) + 1 ) ... N ) X. { 0 } ) ) ` n ) = K ) ) -> [_ ( q u. ( ( ( ( m + 1 ) + 1 ) ... N ) X. { 0 } ) ) / p ]_ B =/= ( n - 1 ) )
465 441 eqeq1d 
 |-  ( p = ( q u. ( ( ( ( m + 1 ) + 1 ) ... N ) X. { 0 } ) ) -> ( ( p ` n ) = K <-> ( ( q u. ( ( ( ( m + 1 ) + 1 ) ... N ) X. { 0 } ) ) ` n ) = K ) )
466 313 465 3anbi23d 
 |-  ( p = ( q u. ( ( ( ( m + 1 ) + 1 ) ... N ) X. { 0 } ) ) -> ( ( n e. ( 1 ... N ) /\ p : ( 1 ... N ) --> ( 0 ... K ) /\ ( p ` n ) = K ) <-> ( n e. ( 1 ... N ) /\ ( q u. ( ( ( ( m + 1 ) + 1 ) ... N ) X. { 0 } ) ) : ( 1 ... N ) --> ( 0 ... K ) /\ ( ( q u. ( ( ( ( m + 1 ) + 1 ) ... N ) X. { 0 } ) ) ` n ) = K ) ) )
467 466 anbi2d 
 |-  ( p = ( q u. ( ( ( ( m + 1 ) + 1 ) ... N ) X. { 0 } ) ) -> ( ( ph /\ ( n e. ( 1 ... N ) /\ p : ( 1 ... N ) --> ( 0 ... K ) /\ ( p ` n ) = K ) ) <-> ( ph /\ ( n e. ( 1 ... N ) /\ ( q u. ( ( ( ( m + 1 ) + 1 ) ... N ) X. { 0 } ) ) : ( 1 ... N ) --> ( 0 ... K ) /\ ( ( q u. ( ( ( ( m + 1 ) + 1 ) ... N ) X. { 0 } ) ) ` n ) = K ) ) ) )
468 315 neeq1d 
 |-  ( p = ( q u. ( ( ( ( m + 1 ) + 1 ) ... N ) X. { 0 } ) ) -> ( B =/= ( n - 1 ) <-> [_ ( q u. ( ( ( ( m + 1 ) + 1 ) ... N ) X. { 0 } ) ) / p ]_ B =/= ( n - 1 ) ) )
469 467 468 imbi12d 
 |-  ( p = ( q u. ( ( ( ( m + 1 ) + 1 ) ... N ) X. { 0 } ) ) -> ( ( ( ph /\ ( n e. ( 1 ... N ) /\ p : ( 1 ... N ) --> ( 0 ... K ) /\ ( p ` n ) = K ) ) -> B =/= ( n - 1 ) ) <-> ( ( ph /\ ( n e. ( 1 ... N ) /\ ( q u. ( ( ( ( m + 1 ) + 1 ) ... N ) X. { 0 } ) ) : ( 1 ... N ) --> ( 0 ... K ) /\ ( ( q u. ( ( ( ( m + 1 ) + 1 ) ... N ) X. { 0 } ) ) ` n ) = K ) ) -> [_ ( q u. ( ( ( ( m + 1 ) + 1 ) ... N ) X. { 0 } ) ) / p ]_ B =/= ( n - 1 ) ) ) )
470 464 312 469 5 vtoclf 
 |-  ( ( ph /\ ( n e. ( 1 ... N ) /\ ( q u. ( ( ( ( m + 1 ) + 1 ) ... N ) X. { 0 } ) ) : ( 1 ... N ) --> ( 0 ... K ) /\ ( ( q u. ( ( ( ( m + 1 ) + 1 ) ... N ) X. { 0 } ) ) ` n ) = K ) ) -> [_ ( q u. ( ( ( ( m + 1 ) + 1 ) ... N ) X. { 0 } ) ) / p ]_ B =/= ( n - 1 ) )
471 460 470 syldan 
 |-  ( ( ph /\ ( ( m e. NN0 /\ m < N ) /\ ( n e. ( 1 ... ( m + 1 ) ) /\ q : ( 1 ... ( m + 1 ) ) --> ( 0 ... K ) /\ ( q ` n ) = K ) ) ) -> [_ ( q u. ( ( ( ( m + 1 ) + 1 ) ... N ) X. { 0 } ) ) / p ]_ B =/= ( n - 1 ) )
472 471 anassrs 
 |-  ( ( ( ph /\ ( m e. NN0 /\ m < N ) ) /\ ( n e. ( 1 ... ( m + 1 ) ) /\ q : ( 1 ... ( m + 1 ) ) --> ( 0 ... K ) /\ ( q ` n ) = K ) ) -> [_ ( q u. ( ( ( ( m + 1 ) + 1 ) ... N ) X. { 0 } ) ) / p ]_ B =/= ( n - 1 ) )
473 267 269 420 449 472 poimirlem27 
 |-  ( ( ph /\ ( m e. NN0 /\ m < N ) ) -> 2 || ( ( # ` { t e. ( ( ( ( 0 ..^ K ) ^m ( 1 ... ( m + 1 ) ) ) X. { f | f : ( 1 ... ( m + 1 ) ) -1-1-onto-> ( 1 ... ( m + 1 ) ) } ) X. ( 0 ... ( m + 1 ) ) ) | A. i e. ( 0 ... ( ( m + 1 ) - 1 ) ) E. j e. ( ( 0 ... ( m + 1 ) ) \ { ( 2nd ` t ) } ) i = [_ ( 1st ` t ) / s ]_ [_ ( ( ( 1st ` s ) oF + ( ( ( ( 2nd ` s ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` s ) " ( ( j + 1 ) ... ( m + 1 ) ) ) X. { 0 } ) ) ) u. ( ( ( ( m + 1 ) + 1 ) ... N ) X. { 0 } ) ) / p ]_ B } ) - ( # ` { s e. ( ( ( 0 ..^ K ) ^m ( 1 ... ( m + 1 ) ) ) X. { f | f : ( 1 ... ( m + 1 ) ) -1-1-onto-> ( 1 ... ( m + 1 ) ) } ) | ( A. i e. ( 0 ... ( ( m + 1 ) - 1 ) ) E. j e. ( 0 ... ( ( m + 1 ) - 1 ) ) i = [_ ( ( ( 1st ` s ) oF + ( ( ( ( 2nd ` s ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` s ) " ( ( j + 1 ) ... ( m + 1 ) ) ) X. { 0 } ) ) ) u. ( ( ( ( m + 1 ) + 1 ) ... N ) X. { 0 } ) ) / p ]_ B /\ ( ( 1st ` s ) ` ( m + 1 ) ) = 0 /\ ( ( 2nd ` s ) ` ( m + 1 ) ) = ( m + 1 ) ) } ) ) )
474 267 269 420 poimirlem26 
 |-  ( ( ph /\ ( m e. NN0 /\ m < N ) ) -> 2 || ( ( # ` { t e. ( ( ( ( 0 ..^ K ) ^m ( 1 ... ( m + 1 ) ) ) X. { f | f : ( 1 ... ( m + 1 ) ) -1-1-onto-> ( 1 ... ( m + 1 ) ) } ) X. ( 0 ... ( m + 1 ) ) ) | A. i e. ( 0 ... ( ( m + 1 ) - 1 ) ) E. j e. ( ( 0 ... ( m + 1 ) ) \ { ( 2nd ` t ) } ) i = [_ ( 1st ` t ) / s ]_ [_ ( ( ( 1st ` s ) oF + ( ( ( ( 2nd ` s ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` s ) " ( ( j + 1 ) ... ( m + 1 ) ) ) X. { 0 } ) ) ) u. ( ( ( ( m + 1 ) + 1 ) ... N ) X. { 0 } ) ) / p ]_ B } ) - ( # ` { s e. ( ( ( 0 ..^ K ) ^m ( 1 ... ( m + 1 ) ) ) X. { f | f : ( 1 ... ( m + 1 ) ) -1-1-onto-> ( 1 ... ( m + 1 ) ) } ) | A. i e. ( 0 ... ( m + 1 ) ) E. j e. ( 0 ... ( m + 1 ) ) i = [_ ( ( ( 1st ` s ) oF + ( ( ( ( 2nd ` s ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` s ) " ( ( j + 1 ) ... ( m + 1 ) ) ) X. { 0 } ) ) ) u. ( ( ( ( m + 1 ) + 1 ) ... N ) X. { 0 } ) ) / p ]_ B } ) ) )
475 fzfi 
 |-  ( 0 ... ( m + 1 ) ) e. Fin
476 xpfi 
 |-  ( ( ( ( ( 0 ..^ K ) ^m ( 1 ... ( m + 1 ) ) ) X. { f | f : ( 1 ... ( m + 1 ) ) -1-1-onto-> ( 1 ... ( m + 1 ) ) } ) e. Fin /\ ( 0 ... ( m + 1 ) ) e. Fin ) -> ( ( ( ( 0 ..^ K ) ^m ( 1 ... ( m + 1 ) ) ) X. { f | f : ( 1 ... ( m + 1 ) ) -1-1-onto-> ( 1 ... ( m + 1 ) ) } ) X. ( 0 ... ( m + 1 ) ) ) e. Fin )
477 256 475 476 mp2an 
 |-  ( ( ( ( 0 ..^ K ) ^m ( 1 ... ( m + 1 ) ) ) X. { f | f : ( 1 ... ( m + 1 ) ) -1-1-onto-> ( 1 ... ( m + 1 ) ) } ) X. ( 0 ... ( m + 1 ) ) ) e. Fin
478 rabfi 
 |-  ( ( ( ( ( 0 ..^ K ) ^m ( 1 ... ( m + 1 ) ) ) X. { f | f : ( 1 ... ( m + 1 ) ) -1-1-onto-> ( 1 ... ( m + 1 ) ) } ) X. ( 0 ... ( m + 1 ) ) ) e. Fin -> { t e. ( ( ( ( 0 ..^ K ) ^m ( 1 ... ( m + 1 ) ) ) X. { f | f : ( 1 ... ( m + 1 ) ) -1-1-onto-> ( 1 ... ( m + 1 ) ) } ) X. ( 0 ... ( m + 1 ) ) ) | A. i e. ( 0 ... ( ( m + 1 ) - 1 ) ) E. j e. ( ( 0 ... ( m + 1 ) ) \ { ( 2nd ` t ) } ) i = [_ ( 1st ` t ) / s ]_ [_ ( ( ( 1st ` s ) oF + ( ( ( ( 2nd ` s ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` s ) " ( ( j + 1 ) ... ( m + 1 ) ) ) X. { 0 } ) ) ) u. ( ( ( ( m + 1 ) + 1 ) ... N ) X. { 0 } ) ) / p ]_ B } e. Fin )
479 hashcl 
 |-  ( { t e. ( ( ( ( 0 ..^ K ) ^m ( 1 ... ( m + 1 ) ) ) X. { f | f : ( 1 ... ( m + 1 ) ) -1-1-onto-> ( 1 ... ( m + 1 ) ) } ) X. ( 0 ... ( m + 1 ) ) ) | A. i e. ( 0 ... ( ( m + 1 ) - 1 ) ) E. j e. ( ( 0 ... ( m + 1 ) ) \ { ( 2nd ` t ) } ) i = [_ ( 1st ` t ) / s ]_ [_ ( ( ( 1st ` s ) oF + ( ( ( ( 2nd ` s ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` s ) " ( ( j + 1 ) ... ( m + 1 ) ) ) X. { 0 } ) ) ) u. ( ( ( ( m + 1 ) + 1 ) ... N ) X. { 0 } ) ) / p ]_ B } e. Fin -> ( # ` { t e. ( ( ( ( 0 ..^ K ) ^m ( 1 ... ( m + 1 ) ) ) X. { f | f : ( 1 ... ( m + 1 ) ) -1-1-onto-> ( 1 ... ( m + 1 ) ) } ) X. ( 0 ... ( m + 1 ) ) ) | A. i e. ( 0 ... ( ( m + 1 ) - 1 ) ) E. j e. ( ( 0 ... ( m + 1 ) ) \ { ( 2nd ` t ) } ) i = [_ ( 1st ` t ) / s ]_ [_ ( ( ( 1st ` s ) oF + ( ( ( ( 2nd ` s ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` s ) " ( ( j + 1 ) ... ( m + 1 ) ) ) X. { 0 } ) ) ) u. ( ( ( ( m + 1 ) + 1 ) ... N ) X. { 0 } ) ) / p ]_ B } ) e. NN0 )
480 477 478 479 mp2b 
 |-  ( # ` { t e. ( ( ( ( 0 ..^ K ) ^m ( 1 ... ( m + 1 ) ) ) X. { f | f : ( 1 ... ( m + 1 ) ) -1-1-onto-> ( 1 ... ( m + 1 ) ) } ) X. ( 0 ... ( m + 1 ) ) ) | A. i e. ( 0 ... ( ( m + 1 ) - 1 ) ) E. j e. ( ( 0 ... ( m + 1 ) ) \ { ( 2nd ` t ) } ) i = [_ ( 1st ` t ) / s ]_ [_ ( ( ( 1st ` s ) oF + ( ( ( ( 2nd ` s ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` s ) " ( ( j + 1 ) ... ( m + 1 ) ) ) X. { 0 } ) ) ) u. ( ( ( ( m + 1 ) + 1 ) ... N ) X. { 0 } ) ) / p ]_ B } ) e. NN0
481 480 nn0zi 
 |-  ( # ` { t e. ( ( ( ( 0 ..^ K ) ^m ( 1 ... ( m + 1 ) ) ) X. { f | f : ( 1 ... ( m + 1 ) ) -1-1-onto-> ( 1 ... ( m + 1 ) ) } ) X. ( 0 ... ( m + 1 ) ) ) | A. i e. ( 0 ... ( ( m + 1 ) - 1 ) ) E. j e. ( ( 0 ... ( m + 1 ) ) \ { ( 2nd ` t ) } ) i = [_ ( 1st ` t ) / s ]_ [_ ( ( ( 1st ` s ) oF + ( ( ( ( 2nd ` s ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` s ) " ( ( j + 1 ) ... ( m + 1 ) ) ) X. { 0 } ) ) ) u. ( ( ( ( m + 1 ) + 1 ) ... N ) X. { 0 } ) ) / p ]_ B } ) e. ZZ
482 zsubcl 
 |-  ( ( ( # ` { t e. ( ( ( ( 0 ..^ K ) ^m ( 1 ... ( m + 1 ) ) ) X. { f | f : ( 1 ... ( m + 1 ) ) -1-1-onto-> ( 1 ... ( m + 1 ) ) } ) X. ( 0 ... ( m + 1 ) ) ) | A. i e. ( 0 ... ( ( m + 1 ) - 1 ) ) E. j e. ( ( 0 ... ( m + 1 ) ) \ { ( 2nd ` t ) } ) i = [_ ( 1st ` t ) / s ]_ [_ ( ( ( 1st ` s ) oF + ( ( ( ( 2nd ` s ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` s ) " ( ( j + 1 ) ... ( m + 1 ) ) ) X. { 0 } ) ) ) u. ( ( ( ( m + 1 ) + 1 ) ... N ) X. { 0 } ) ) / p ]_ B } ) e. ZZ /\ ( # ` { s e. ( ( ( 0 ..^ K ) ^m ( 1 ... ( m + 1 ) ) ) X. { f | f : ( 1 ... ( m + 1 ) ) -1-1-onto-> ( 1 ... ( m + 1 ) ) } ) | ( A. i e. ( 0 ... ( ( m + 1 ) - 1 ) ) E. j e. ( 0 ... ( ( m + 1 ) - 1 ) ) i = [_ ( ( ( 1st ` s ) oF + ( ( ( ( 2nd ` s ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` s ) " ( ( j + 1 ) ... ( m + 1 ) ) ) X. { 0 } ) ) ) u. ( ( ( ( m + 1 ) + 1 ) ... N ) X. { 0 } ) ) / p ]_ B /\ ( ( 1st ` s ) ` ( m + 1 ) ) = 0 /\ ( ( 2nd ` s ) ` ( m + 1 ) ) = ( m + 1 ) ) } ) e. ZZ ) -> ( ( # ` { t e. ( ( ( ( 0 ..^ K ) ^m ( 1 ... ( m + 1 ) ) ) X. { f | f : ( 1 ... ( m + 1 ) ) -1-1-onto-> ( 1 ... ( m + 1 ) ) } ) X. ( 0 ... ( m + 1 ) ) ) | A. i e. ( 0 ... ( ( m + 1 ) - 1 ) ) E. j e. ( ( 0 ... ( m + 1 ) ) \ { ( 2nd ` t ) } ) i = [_ ( 1st ` t ) / s ]_ [_ ( ( ( 1st ` s ) oF + ( ( ( ( 2nd ` s ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` s ) " ( ( j + 1 ) ... ( m + 1 ) ) ) X. { 0 } ) ) ) u. ( ( ( ( m + 1 ) + 1 ) ... N ) X. { 0 } ) ) / p ]_ B } ) - ( # ` { s e. ( ( ( 0 ..^ K ) ^m ( 1 ... ( m + 1 ) ) ) X. { f | f : ( 1 ... ( m + 1 ) ) -1-1-onto-> ( 1 ... ( m + 1 ) ) } ) | ( A. i e. ( 0 ... ( ( m + 1 ) - 1 ) ) E. j e. ( 0 ... ( ( m + 1 ) - 1 ) ) i = [_ ( ( ( 1st ` s ) oF + ( ( ( ( 2nd ` s ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` s ) " ( ( j + 1 ) ... ( m + 1 ) ) ) X. { 0 } ) ) ) u. ( ( ( ( m + 1 ) + 1 ) ... N ) X. { 0 } ) ) / p ]_ B /\ ( ( 1st ` s ) ` ( m + 1 ) ) = 0 /\ ( ( 2nd ` s ) ` ( m + 1 ) ) = ( m + 1 ) ) } ) ) e. ZZ )
483 481 264 482 mp2an 
 |-  ( ( # ` { t e. ( ( ( ( 0 ..^ K ) ^m ( 1 ... ( m + 1 ) ) ) X. { f | f : ( 1 ... ( m + 1 ) ) -1-1-onto-> ( 1 ... ( m + 1 ) ) } ) X. ( 0 ... ( m + 1 ) ) ) | A. i e. ( 0 ... ( ( m + 1 ) - 1 ) ) E. j e. ( ( 0 ... ( m + 1 ) ) \ { ( 2nd ` t ) } ) i = [_ ( 1st ` t ) / s ]_ [_ ( ( ( 1st ` s ) oF + ( ( ( ( 2nd ` s ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` s ) " ( ( j + 1 ) ... ( m + 1 ) ) ) X. { 0 } ) ) ) u. ( ( ( ( m + 1 ) + 1 ) ... N ) X. { 0 } ) ) / p ]_ B } ) - ( # ` { s e. ( ( ( 0 ..^ K ) ^m ( 1 ... ( m + 1 ) ) ) X. { f | f : ( 1 ... ( m + 1 ) ) -1-1-onto-> ( 1 ... ( m + 1 ) ) } ) | ( A. i e. ( 0 ... ( ( m + 1 ) - 1 ) ) E. j e. ( 0 ... ( ( m + 1 ) - 1 ) ) i = [_ ( ( ( 1st ` s ) oF + ( ( ( ( 2nd ` s ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` s ) " ( ( j + 1 ) ... ( m + 1 ) ) ) X. { 0 } ) ) ) u. ( ( ( ( m + 1 ) + 1 ) ... N ) X. { 0 } ) ) / p ]_ B /\ ( ( 1st ` s ) ` ( m + 1 ) ) = 0 /\ ( ( 2nd ` s ) ` ( m + 1 ) ) = ( m + 1 ) ) } ) ) e. ZZ
484 zsubcl 
 |-  ( ( ( # ` { t e. ( ( ( ( 0 ..^ K ) ^m ( 1 ... ( m + 1 ) ) ) X. { f | f : ( 1 ... ( m + 1 ) ) -1-1-onto-> ( 1 ... ( m + 1 ) ) } ) X. ( 0 ... ( m + 1 ) ) ) | A. i e. ( 0 ... ( ( m + 1 ) - 1 ) ) E. j e. ( ( 0 ... ( m + 1 ) ) \ { ( 2nd ` t ) } ) i = [_ ( 1st ` t ) / s ]_ [_ ( ( ( 1st ` s ) oF + ( ( ( ( 2nd ` s ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` s ) " ( ( j + 1 ) ... ( m + 1 ) ) ) X. { 0 } ) ) ) u. ( ( ( ( m + 1 ) + 1 ) ... N ) X. { 0 } ) ) / p ]_ B } ) e. ZZ /\ ( # ` { s e. ( ( ( 0 ..^ K ) ^m ( 1 ... ( m + 1 ) ) ) X. { f | f : ( 1 ... ( m + 1 ) ) -1-1-onto-> ( 1 ... ( m + 1 ) ) } ) | A. i e. ( 0 ... ( m + 1 ) ) E. j e. ( 0 ... ( m + 1 ) ) i = [_ ( ( ( 1st ` s ) oF + ( ( ( ( 2nd ` s ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` s ) " ( ( j + 1 ) ... ( m + 1 ) ) ) X. { 0 } ) ) ) u. ( ( ( ( m + 1 ) + 1 ) ... N ) X. { 0 } ) ) / p ]_ B } ) e. ZZ ) -> ( ( # ` { t e. ( ( ( ( 0 ..^ K ) ^m ( 1 ... ( m + 1 ) ) ) X. { f | f : ( 1 ... ( m + 1 ) ) -1-1-onto-> ( 1 ... ( m + 1 ) ) } ) X. ( 0 ... ( m + 1 ) ) ) | A. i e. ( 0 ... ( ( m + 1 ) - 1 ) ) E. j e. ( ( 0 ... ( m + 1 ) ) \ { ( 2nd ` t ) } ) i = [_ ( 1st ` t ) / s ]_ [_ ( ( ( 1st ` s ) oF + ( ( ( ( 2nd ` s ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` s ) " ( ( j + 1 ) ... ( m + 1 ) ) ) X. { 0 } ) ) ) u. ( ( ( ( m + 1 ) + 1 ) ... N ) X. { 0 } ) ) / p ]_ B } ) - ( # ` { s e. ( ( ( 0 ..^ K ) ^m ( 1 ... ( m + 1 ) ) ) X. { f | f : ( 1 ... ( m + 1 ) ) -1-1-onto-> ( 1 ... ( m + 1 ) ) } ) | A. i e. ( 0 ... ( m + 1 ) ) E. j e. ( 0 ... ( m + 1 ) ) i = [_ ( ( ( 1st ` s ) oF + ( ( ( ( 2nd ` s ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` s ) " ( ( j + 1 ) ... ( m + 1 ) ) ) X. { 0 } ) ) ) u. ( ( ( ( m + 1 ) + 1 ) ... N ) X. { 0 } ) ) / p ]_ B } ) ) e. ZZ )
485 481 260 484 mp2an 
 |-  ( ( # ` { t e. ( ( ( ( 0 ..^ K ) ^m ( 1 ... ( m + 1 ) ) ) X. { f | f : ( 1 ... ( m + 1 ) ) -1-1-onto-> ( 1 ... ( m + 1 ) ) } ) X. ( 0 ... ( m + 1 ) ) ) | A. i e. ( 0 ... ( ( m + 1 ) - 1 ) ) E. j e. ( ( 0 ... ( m + 1 ) ) \ { ( 2nd ` t ) } ) i = [_ ( 1st ` t ) / s ]_ [_ ( ( ( 1st ` s ) oF + ( ( ( ( 2nd ` s ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` s ) " ( ( j + 1 ) ... ( m + 1 ) ) ) X. { 0 } ) ) ) u. ( ( ( ( m + 1 ) + 1 ) ... N ) X. { 0 } ) ) / p ]_ B } ) - ( # ` { s e. ( ( ( 0 ..^ K ) ^m ( 1 ... ( m + 1 ) ) ) X. { f | f : ( 1 ... ( m + 1 ) ) -1-1-onto-> ( 1 ... ( m + 1 ) ) } ) | A. i e. ( 0 ... ( m + 1 ) ) E. j e. ( 0 ... ( m + 1 ) ) i = [_ ( ( ( 1st ` s ) oF + ( ( ( ( 2nd ` s ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` s ) " ( ( j + 1 ) ... ( m + 1 ) ) ) X. { 0 } ) ) ) u. ( ( ( ( m + 1 ) + 1 ) ... N ) X. { 0 } ) ) / p ]_ B } ) ) e. ZZ
486 dvds2sub 
 |-  ( ( 2 e. ZZ /\ ( ( # ` { t e. ( ( ( ( 0 ..^ K ) ^m ( 1 ... ( m + 1 ) ) ) X. { f | f : ( 1 ... ( m + 1 ) ) -1-1-onto-> ( 1 ... ( m + 1 ) ) } ) X. ( 0 ... ( m + 1 ) ) ) | A. i e. ( 0 ... ( ( m + 1 ) - 1 ) ) E. j e. ( ( 0 ... ( m + 1 ) ) \ { ( 2nd ` t ) } ) i = [_ ( 1st ` t ) / s ]_ [_ ( ( ( 1st ` s ) oF + ( ( ( ( 2nd ` s ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` s ) " ( ( j + 1 ) ... ( m + 1 ) ) ) X. { 0 } ) ) ) u. ( ( ( ( m + 1 ) + 1 ) ... N ) X. { 0 } ) ) / p ]_ B } ) - ( # ` { s e. ( ( ( 0 ..^ K ) ^m ( 1 ... ( m + 1 ) ) ) X. { f | f : ( 1 ... ( m + 1 ) ) -1-1-onto-> ( 1 ... ( m + 1 ) ) } ) | ( A. i e. ( 0 ... ( ( m + 1 ) - 1 ) ) E. j e. ( 0 ... ( ( m + 1 ) - 1 ) ) i = [_ ( ( ( 1st ` s ) oF + ( ( ( ( 2nd ` s ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` s ) " ( ( j + 1 ) ... ( m + 1 ) ) ) X. { 0 } ) ) ) u. ( ( ( ( m + 1 ) + 1 ) ... N ) X. { 0 } ) ) / p ]_ B /\ ( ( 1st ` s ) ` ( m + 1 ) ) = 0 /\ ( ( 2nd ` s ) ` ( m + 1 ) ) = ( m + 1 ) ) } ) ) e. ZZ /\ ( ( # ` { t e. ( ( ( ( 0 ..^ K ) ^m ( 1 ... ( m + 1 ) ) ) X. { f | f : ( 1 ... ( m + 1 ) ) -1-1-onto-> ( 1 ... ( m + 1 ) ) } ) X. ( 0 ... ( m + 1 ) ) ) | A. i e. ( 0 ... ( ( m + 1 ) - 1 ) ) E. j e. ( ( 0 ... ( m + 1 ) ) \ { ( 2nd ` t ) } ) i = [_ ( 1st ` t ) / s ]_ [_ ( ( ( 1st ` s ) oF + ( ( ( ( 2nd ` s ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` s ) " ( ( j + 1 ) ... ( m + 1 ) ) ) X. { 0 } ) ) ) u. ( ( ( ( m + 1 ) + 1 ) ... N ) X. { 0 } ) ) / p ]_ B } ) - ( # ` { s e. ( ( ( 0 ..^ K ) ^m ( 1 ... ( m + 1 ) ) ) X. { f | f : ( 1 ... ( m + 1 ) ) -1-1-onto-> ( 1 ... ( m + 1 ) ) } ) | A. i e. ( 0 ... ( m + 1 ) ) E. j e. ( 0 ... ( m + 1 ) ) i = [_ ( ( ( 1st ` s ) oF + ( ( ( ( 2nd ` s ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` s ) " ( ( j + 1 ) ... ( m + 1 ) ) ) X. { 0 } ) ) ) u. ( ( ( ( m + 1 ) + 1 ) ... N ) X. { 0 } ) ) / p ]_ B } ) ) e. ZZ ) -> ( ( 2 || ( ( # ` { t e. ( ( ( ( 0 ..^ K ) ^m ( 1 ... ( m + 1 ) ) ) X. { f | f : ( 1 ... ( m + 1 ) ) -1-1-onto-> ( 1 ... ( m + 1 ) ) } ) X. ( 0 ... ( m + 1 ) ) ) | A. i e. ( 0 ... ( ( m + 1 ) - 1 ) ) E. j e. ( ( 0 ... ( m + 1 ) ) \ { ( 2nd ` t ) } ) i = [_ ( 1st ` t ) / s ]_ [_ ( ( ( 1st ` s ) oF + ( ( ( ( 2nd ` s ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` s ) " ( ( j + 1 ) ... ( m + 1 ) ) ) X. { 0 } ) ) ) u. ( ( ( ( m + 1 ) + 1 ) ... N ) X. { 0 } ) ) / p ]_ B } ) - ( # ` { s e. ( ( ( 0 ..^ K ) ^m ( 1 ... ( m + 1 ) ) ) X. { f | f : ( 1 ... ( m + 1 ) ) -1-1-onto-> ( 1 ... ( m + 1 ) ) } ) | ( A. i e. ( 0 ... ( ( m + 1 ) - 1 ) ) E. j e. ( 0 ... ( ( m + 1 ) - 1 ) ) i = [_ ( ( ( 1st ` s ) oF + ( ( ( ( 2nd ` s ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` s ) " ( ( j + 1 ) ... ( m + 1 ) ) ) X. { 0 } ) ) ) u. ( ( ( ( m + 1 ) + 1 ) ... N ) X. { 0 } ) ) / p ]_ B /\ ( ( 1st ` s ) ` ( m + 1 ) ) = 0 /\ ( ( 2nd ` s ) ` ( m + 1 ) ) = ( m + 1 ) ) } ) ) /\ 2 || ( ( # ` { t e. ( ( ( ( 0 ..^ K ) ^m ( 1 ... ( m + 1 ) ) ) X. { f | f : ( 1 ... ( m + 1 ) ) -1-1-onto-> ( 1 ... ( m + 1 ) ) } ) X. ( 0 ... ( m + 1 ) ) ) | A. i e. ( 0 ... ( ( m + 1 ) - 1 ) ) E. j e. ( ( 0 ... ( m + 1 ) ) \ { ( 2nd ` t ) } ) i = [_ ( 1st ` t ) / s ]_ [_ ( ( ( 1st ` s ) oF + ( ( ( ( 2nd ` s ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` s ) " ( ( j + 1 ) ... ( m + 1 ) ) ) X. { 0 } ) ) ) u. ( ( ( ( m + 1 ) + 1 ) ... N ) X. { 0 } ) ) / p ]_ B } ) - ( # ` { s e. ( ( ( 0 ..^ K ) ^m ( 1 ... ( m + 1 ) ) ) X. { f | f : ( 1 ... ( m + 1 ) ) -1-1-onto-> ( 1 ... ( m + 1 ) ) } ) | A. i e. ( 0 ... ( m + 1 ) ) E. j e. ( 0 ... ( m + 1 ) ) i = [_ ( ( ( 1st ` s ) oF + ( ( ( ( 2nd ` s ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` s ) " ( ( j + 1 ) ... ( m + 1 ) ) ) X. { 0 } ) ) ) u. ( ( ( ( m + 1 ) + 1 ) ... N ) X. { 0 } ) ) / p ]_ B } ) ) ) -> 2 || ( ( ( # ` { t e. ( ( ( ( 0 ..^ K ) ^m ( 1 ... ( m + 1 ) ) ) X. { f | f : ( 1 ... ( m + 1 ) ) -1-1-onto-> ( 1 ... ( m + 1 ) ) } ) X. ( 0 ... ( m + 1 ) ) ) | A. i e. ( 0 ... ( ( m + 1 ) - 1 ) ) E. j e. ( ( 0 ... ( m + 1 ) ) \ { ( 2nd ` t ) } ) i = [_ ( 1st ` t ) / s ]_ [_ ( ( ( 1st ` s ) oF + ( ( ( ( 2nd ` s ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` s ) " ( ( j + 1 ) ... ( m + 1 ) ) ) X. { 0 } ) ) ) u. ( ( ( ( m + 1 ) + 1 ) ... N ) X. { 0 } ) ) / p ]_ B } ) - ( # ` { s e. ( ( ( 0 ..^ K ) ^m ( 1 ... ( m + 1 ) ) ) X. { f | f : ( 1 ... ( m + 1 ) ) -1-1-onto-> ( 1 ... ( m + 1 ) ) } ) | ( A. i e. ( 0 ... ( ( m + 1 ) - 1 ) ) E. j e. ( 0 ... ( ( m + 1 ) - 1 ) ) i = [_ ( ( ( 1st ` s ) oF + ( ( ( ( 2nd ` s ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` s ) " ( ( j + 1 ) ... ( m + 1 ) ) ) X. { 0 } ) ) ) u. ( ( ( ( m + 1 ) + 1 ) ... N ) X. { 0 } ) ) / p ]_ B /\ ( ( 1st ` s ) ` ( m + 1 ) ) = 0 /\ ( ( 2nd ` s ) ` ( m + 1 ) ) = ( m + 1 ) ) } ) ) - ( ( # ` { t e. ( ( ( ( 0 ..^ K ) ^m ( 1 ... ( m + 1 ) ) ) X. { f | f : ( 1 ... ( m + 1 ) ) -1-1-onto-> ( 1 ... ( m + 1 ) ) } ) X. ( 0 ... ( m + 1 ) ) ) | A. i e. ( 0 ... ( ( m + 1 ) - 1 ) ) E. j e. ( ( 0 ... ( m + 1 ) ) \ { ( 2nd ` t ) } ) i = [_ ( 1st ` t ) / s ]_ [_ ( ( ( 1st ` s ) oF + ( ( ( ( 2nd ` s ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` s ) " ( ( j + 1 ) ... ( m + 1 ) ) ) X. { 0 } ) ) ) u. ( ( ( ( m + 1 ) + 1 ) ... N ) X. { 0 } ) ) / p ]_ B } ) - ( # ` { s e. ( ( ( 0 ..^ K ) ^m ( 1 ... ( m + 1 ) ) ) X. { f | f : ( 1 ... ( m + 1 ) ) -1-1-onto-> ( 1 ... ( m + 1 ) ) } ) | A. i e. ( 0 ... ( m + 1 ) ) E. j e. ( 0 ... ( m + 1 ) ) i = [_ ( ( ( 1st ` s ) oF + ( ( ( ( 2nd ` s ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` s ) " ( ( j + 1 ) ... ( m + 1 ) ) ) X. { 0 } ) ) ) u. ( ( ( ( m + 1 ) + 1 ) ... N ) X. { 0 } ) ) / p ]_ B } ) ) ) ) )
487 242 483 485 486 mp3an 
 |-  ( ( 2 || ( ( # ` { t e. ( ( ( ( 0 ..^ K ) ^m ( 1 ... ( m + 1 ) ) ) X. { f | f : ( 1 ... ( m + 1 ) ) -1-1-onto-> ( 1 ... ( m + 1 ) ) } ) X. ( 0 ... ( m + 1 ) ) ) | A. i e. ( 0 ... ( ( m + 1 ) - 1 ) ) E. j e. ( ( 0 ... ( m + 1 ) ) \ { ( 2nd ` t ) } ) i = [_ ( 1st ` t ) / s ]_ [_ ( ( ( 1st ` s ) oF + ( ( ( ( 2nd ` s ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` s ) " ( ( j + 1 ) ... ( m + 1 ) ) ) X. { 0 } ) ) ) u. ( ( ( ( m + 1 ) + 1 ) ... N ) X. { 0 } ) ) / p ]_ B } ) - ( # ` { s e. ( ( ( 0 ..^ K ) ^m ( 1 ... ( m + 1 ) ) ) X. { f | f : ( 1 ... ( m + 1 ) ) -1-1-onto-> ( 1 ... ( m + 1 ) ) } ) | ( A. i e. ( 0 ... ( ( m + 1 ) - 1 ) ) E. j e. ( 0 ... ( ( m + 1 ) - 1 ) ) i = [_ ( ( ( 1st ` s ) oF + ( ( ( ( 2nd ` s ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` s ) " ( ( j + 1 ) ... ( m + 1 ) ) ) X. { 0 } ) ) ) u. ( ( ( ( m + 1 ) + 1 ) ... N ) X. { 0 } ) ) / p ]_ B /\ ( ( 1st ` s ) ` ( m + 1 ) ) = 0 /\ ( ( 2nd ` s ) ` ( m + 1 ) ) = ( m + 1 ) ) } ) ) /\ 2 || ( ( # ` { t e. ( ( ( ( 0 ..^ K ) ^m ( 1 ... ( m + 1 ) ) ) X. { f | f : ( 1 ... ( m + 1 ) ) -1-1-onto-> ( 1 ... ( m + 1 ) ) } ) X. ( 0 ... ( m + 1 ) ) ) | A. i e. ( 0 ... ( ( m + 1 ) - 1 ) ) E. j e. ( ( 0 ... ( m + 1 ) ) \ { ( 2nd ` t ) } ) i = [_ ( 1st ` t ) / s ]_ [_ ( ( ( 1st ` s ) oF + ( ( ( ( 2nd ` s ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` s ) " ( ( j + 1 ) ... ( m + 1 ) ) ) X. { 0 } ) ) ) u. ( ( ( ( m + 1 ) + 1 ) ... N ) X. { 0 } ) ) / p ]_ B } ) - ( # ` { s e. ( ( ( 0 ..^ K ) ^m ( 1 ... ( m + 1 ) ) ) X. { f | f : ( 1 ... ( m + 1 ) ) -1-1-onto-> ( 1 ... ( m + 1 ) ) } ) | A. i e. ( 0 ... ( m + 1 ) ) E. j e. ( 0 ... ( m + 1 ) ) i = [_ ( ( ( 1st ` s ) oF + ( ( ( ( 2nd ` s ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` s ) " ( ( j + 1 ) ... ( m + 1 ) ) ) X. { 0 } ) ) ) u. ( ( ( ( m + 1 ) + 1 ) ... N ) X. { 0 } ) ) / p ]_ B } ) ) ) -> 2 || ( ( ( # ` { t e. ( ( ( ( 0 ..^ K ) ^m ( 1 ... ( m + 1 ) ) ) X. { f | f : ( 1 ... ( m + 1 ) ) -1-1-onto-> ( 1 ... ( m + 1 ) ) } ) X. ( 0 ... ( m + 1 ) ) ) | A. i e. ( 0 ... ( ( m + 1 ) - 1 ) ) E. j e. ( ( 0 ... ( m + 1 ) ) \ { ( 2nd ` t ) } ) i = [_ ( 1st ` t ) / s ]_ [_ ( ( ( 1st ` s ) oF + ( ( ( ( 2nd ` s ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` s ) " ( ( j + 1 ) ... ( m + 1 ) ) ) X. { 0 } ) ) ) u. ( ( ( ( m + 1 ) + 1 ) ... N ) X. { 0 } ) ) / p ]_ B } ) - ( # ` { s e. ( ( ( 0 ..^ K ) ^m ( 1 ... ( m + 1 ) ) ) X. { f | f : ( 1 ... ( m + 1 ) ) -1-1-onto-> ( 1 ... ( m + 1 ) ) } ) | ( A. i e. ( 0 ... ( ( m + 1 ) - 1 ) ) E. j e. ( 0 ... ( ( m + 1 ) - 1 ) ) i = [_ ( ( ( 1st ` s ) oF + ( ( ( ( 2nd ` s ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` s ) " ( ( j + 1 ) ... ( m + 1 ) ) ) X. { 0 } ) ) ) u. ( ( ( ( m + 1 ) + 1 ) ... N ) X. { 0 } ) ) / p ]_ B /\ ( ( 1st ` s ) ` ( m + 1 ) ) = 0 /\ ( ( 2nd ` s ) ` ( m + 1 ) ) = ( m + 1 ) ) } ) ) - ( ( # ` { t e. ( ( ( ( 0 ..^ K ) ^m ( 1 ... ( m + 1 ) ) ) X. { f | f : ( 1 ... ( m + 1 ) ) -1-1-onto-> ( 1 ... ( m + 1 ) ) } ) X. ( 0 ... ( m + 1 ) ) ) | A. i e. ( 0 ... ( ( m + 1 ) - 1 ) ) E. j e. ( ( 0 ... ( m + 1 ) ) \ { ( 2nd ` t ) } ) i = [_ ( 1st ` t ) / s ]_ [_ ( ( ( 1st ` s ) oF + ( ( ( ( 2nd ` s ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` s ) " ( ( j + 1 ) ... ( m + 1 ) ) ) X. { 0 } ) ) ) u. ( ( ( ( m + 1 ) + 1 ) ... N ) X. { 0 } ) ) / p ]_ B } ) - ( # ` { s e. ( ( ( 0 ..^ K ) ^m ( 1 ... ( m + 1 ) ) ) X. { f | f : ( 1 ... ( m + 1 ) ) -1-1-onto-> ( 1 ... ( m + 1 ) ) } ) | A. i e. ( 0 ... ( m + 1 ) ) E. j e. ( 0 ... ( m + 1 ) ) i = [_ ( ( ( 1st ` s ) oF + ( ( ( ( 2nd ` s ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` s ) " ( ( j + 1 ) ... ( m + 1 ) ) ) X. { 0 } ) ) ) u. ( ( ( ( m + 1 ) + 1 ) ... N ) X. { 0 } ) ) / p ]_ B } ) ) ) )
488 473 474 487 syl2anc 
 |-  ( ( ph /\ ( m e. NN0 /\ m < N ) ) -> 2 || ( ( ( # ` { t e. ( ( ( ( 0 ..^ K ) ^m ( 1 ... ( m + 1 ) ) ) X. { f | f : ( 1 ... ( m + 1 ) ) -1-1-onto-> ( 1 ... ( m + 1 ) ) } ) X. ( 0 ... ( m + 1 ) ) ) | A. i e. ( 0 ... ( ( m + 1 ) - 1 ) ) E. j e. ( ( 0 ... ( m + 1 ) ) \ { ( 2nd ` t ) } ) i = [_ ( 1st ` t ) / s ]_ [_ ( ( ( 1st ` s ) oF + ( ( ( ( 2nd ` s ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` s ) " ( ( j + 1 ) ... ( m + 1 ) ) ) X. { 0 } ) ) ) u. ( ( ( ( m + 1 ) + 1 ) ... N ) X. { 0 } ) ) / p ]_ B } ) - ( # ` { s e. ( ( ( 0 ..^ K ) ^m ( 1 ... ( m + 1 ) ) ) X. { f | f : ( 1 ... ( m + 1 ) ) -1-1-onto-> ( 1 ... ( m + 1 ) ) } ) | ( A. i e. ( 0 ... ( ( m + 1 ) - 1 ) ) E. j e. ( 0 ... ( ( m + 1 ) - 1 ) ) i = [_ ( ( ( 1st ` s ) oF + ( ( ( ( 2nd ` s ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` s ) " ( ( j + 1 ) ... ( m + 1 ) ) ) X. { 0 } ) ) ) u. ( ( ( ( m + 1 ) + 1 ) ... N ) X. { 0 } ) ) / p ]_ B /\ ( ( 1st ` s ) ` ( m + 1 ) ) = 0 /\ ( ( 2nd ` s ) ` ( m + 1 ) ) = ( m + 1 ) ) } ) ) - ( ( # ` { t e. ( ( ( ( 0 ..^ K ) ^m ( 1 ... ( m + 1 ) ) ) X. { f | f : ( 1 ... ( m + 1 ) ) -1-1-onto-> ( 1 ... ( m + 1 ) ) } ) X. ( 0 ... ( m + 1 ) ) ) | A. i e. ( 0 ... ( ( m + 1 ) - 1 ) ) E. j e. ( ( 0 ... ( m + 1 ) ) \ { ( 2nd ` t ) } ) i = [_ ( 1st ` t ) / s ]_ [_ ( ( ( 1st ` s ) oF + ( ( ( ( 2nd ` s ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` s ) " ( ( j + 1 ) ... ( m + 1 ) ) ) X. { 0 } ) ) ) u. ( ( ( ( m + 1 ) + 1 ) ... N ) X. { 0 } ) ) / p ]_ B } ) - ( # ` { s e. ( ( ( 0 ..^ K ) ^m ( 1 ... ( m + 1 ) ) ) X. { f | f : ( 1 ... ( m + 1 ) ) -1-1-onto-> ( 1 ... ( m + 1 ) ) } ) | A. i e. ( 0 ... ( m + 1 ) ) E. j e. ( 0 ... ( m + 1 ) ) i = [_ ( ( ( 1st ` s ) oF + ( ( ( ( 2nd ` s ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` s ) " ( ( j + 1 ) ... ( m + 1 ) ) ) X. { 0 } ) ) ) u. ( ( ( ( m + 1 ) + 1 ) ... N ) X. { 0 } ) ) / p ]_ B } ) ) ) )
489 480 nn0cni 
 |-  ( # ` { t e. ( ( ( ( 0 ..^ K ) ^m ( 1 ... ( m + 1 ) ) ) X. { f | f : ( 1 ... ( m + 1 ) ) -1-1-onto-> ( 1 ... ( m + 1 ) ) } ) X. ( 0 ... ( m + 1 ) ) ) | A. i e. ( 0 ... ( ( m + 1 ) - 1 ) ) E. j e. ( ( 0 ... ( m + 1 ) ) \ { ( 2nd ` t ) } ) i = [_ ( 1st ` t ) / s ]_ [_ ( ( ( 1st ` s ) oF + ( ( ( ( 2nd ` s ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` s ) " ( ( j + 1 ) ... ( m + 1 ) ) ) X. { 0 } ) ) ) u. ( ( ( ( m + 1 ) + 1 ) ... N ) X. { 0 } ) ) / p ]_ B } ) e. CC
490 263 nn0cni 
 |-  ( # ` { s e. ( ( ( 0 ..^ K ) ^m ( 1 ... ( m + 1 ) ) ) X. { f | f : ( 1 ... ( m + 1 ) ) -1-1-onto-> ( 1 ... ( m + 1 ) ) } ) | ( A. i e. ( 0 ... ( ( m + 1 ) - 1 ) ) E. j e. ( 0 ... ( ( m + 1 ) - 1 ) ) i = [_ ( ( ( 1st ` s ) oF + ( ( ( ( 2nd ` s ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` s ) " ( ( j + 1 ) ... ( m + 1 ) ) ) X. { 0 } ) ) ) u. ( ( ( ( m + 1 ) + 1 ) ... N ) X. { 0 } ) ) / p ]_ B /\ ( ( 1st ` s ) ` ( m + 1 ) ) = 0 /\ ( ( 2nd ` s ) ` ( m + 1 ) ) = ( m + 1 ) ) } ) e. CC
491 259 nn0cni 
 |-  ( # ` { s e. ( ( ( 0 ..^ K ) ^m ( 1 ... ( m + 1 ) ) ) X. { f | f : ( 1 ... ( m + 1 ) ) -1-1-onto-> ( 1 ... ( m + 1 ) ) } ) | A. i e. ( 0 ... ( m + 1 ) ) E. j e. ( 0 ... ( m + 1 ) ) i = [_ ( ( ( 1st ` s ) oF + ( ( ( ( 2nd ` s ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` s ) " ( ( j + 1 ) ... ( m + 1 ) ) ) X. { 0 } ) ) ) u. ( ( ( ( m + 1 ) + 1 ) ... N ) X. { 0 } ) ) / p ]_ B } ) e. CC
492 nnncan1 
 |-  ( ( ( # ` { t e. ( ( ( ( 0 ..^ K ) ^m ( 1 ... ( m + 1 ) ) ) X. { f | f : ( 1 ... ( m + 1 ) ) -1-1-onto-> ( 1 ... ( m + 1 ) ) } ) X. ( 0 ... ( m + 1 ) ) ) | A. i e. ( 0 ... ( ( m + 1 ) - 1 ) ) E. j e. ( ( 0 ... ( m + 1 ) ) \ { ( 2nd ` t ) } ) i = [_ ( 1st ` t ) / s ]_ [_ ( ( ( 1st ` s ) oF + ( ( ( ( 2nd ` s ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` s ) " ( ( j + 1 ) ... ( m + 1 ) ) ) X. { 0 } ) ) ) u. ( ( ( ( m + 1 ) + 1 ) ... N ) X. { 0 } ) ) / p ]_ B } ) e. CC /\ ( # ` { s e. ( ( ( 0 ..^ K ) ^m ( 1 ... ( m + 1 ) ) ) X. { f | f : ( 1 ... ( m + 1 ) ) -1-1-onto-> ( 1 ... ( m + 1 ) ) } ) | ( A. i e. ( 0 ... ( ( m + 1 ) - 1 ) ) E. j e. ( 0 ... ( ( m + 1 ) - 1 ) ) i = [_ ( ( ( 1st ` s ) oF + ( ( ( ( 2nd ` s ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` s ) " ( ( j + 1 ) ... ( m + 1 ) ) ) X. { 0 } ) ) ) u. ( ( ( ( m + 1 ) + 1 ) ... N ) X. { 0 } ) ) / p ]_ B /\ ( ( 1st ` s ) ` ( m + 1 ) ) = 0 /\ ( ( 2nd ` s ) ` ( m + 1 ) ) = ( m + 1 ) ) } ) e. CC /\ ( # ` { s e. ( ( ( 0 ..^ K ) ^m ( 1 ... ( m + 1 ) ) ) X. { f | f : ( 1 ... ( m + 1 ) ) -1-1-onto-> ( 1 ... ( m + 1 ) ) } ) | A. i e. ( 0 ... ( m + 1 ) ) E. j e. ( 0 ... ( m + 1 ) ) i = [_ ( ( ( 1st ` s ) oF + ( ( ( ( 2nd ` s ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` s ) " ( ( j + 1 ) ... ( m + 1 ) ) ) X. { 0 } ) ) ) u. ( ( ( ( m + 1 ) + 1 ) ... N ) X. { 0 } ) ) / p ]_ B } ) e. CC ) -> ( ( ( # ` { t e. ( ( ( ( 0 ..^ K ) ^m ( 1 ... ( m + 1 ) ) ) X. { f | f : ( 1 ... ( m + 1 ) ) -1-1-onto-> ( 1 ... ( m + 1 ) ) } ) X. ( 0 ... ( m + 1 ) ) ) | A. i e. ( 0 ... ( ( m + 1 ) - 1 ) ) E. j e. ( ( 0 ... ( m + 1 ) ) \ { ( 2nd ` t ) } ) i = [_ ( 1st ` t ) / s ]_ [_ ( ( ( 1st ` s ) oF + ( ( ( ( 2nd ` s ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` s ) " ( ( j + 1 ) ... ( m + 1 ) ) ) X. { 0 } ) ) ) u. ( ( ( ( m + 1 ) + 1 ) ... N ) X. { 0 } ) ) / p ]_ B } ) - ( # ` { s e. ( ( ( 0 ..^ K ) ^m ( 1 ... ( m + 1 ) ) ) X. { f | f : ( 1 ... ( m + 1 ) ) -1-1-onto-> ( 1 ... ( m + 1 ) ) } ) | ( A. i e. ( 0 ... ( ( m + 1 ) - 1 ) ) E. j e. ( 0 ... ( ( m + 1 ) - 1 ) ) i = [_ ( ( ( 1st ` s ) oF + ( ( ( ( 2nd ` s ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` s ) " ( ( j + 1 ) ... ( m + 1 ) ) ) X. { 0 } ) ) ) u. ( ( ( ( m + 1 ) + 1 ) ... N ) X. { 0 } ) ) / p ]_ B /\ ( ( 1st ` s ) ` ( m + 1 ) ) = 0 /\ ( ( 2nd ` s ) ` ( m + 1 ) ) = ( m + 1 ) ) } ) ) - ( ( # ` { t e. ( ( ( ( 0 ..^ K ) ^m ( 1 ... ( m + 1 ) ) ) X. { f | f : ( 1 ... ( m + 1 ) ) -1-1-onto-> ( 1 ... ( m + 1 ) ) } ) X. ( 0 ... ( m + 1 ) ) ) | A. i e. ( 0 ... ( ( m + 1 ) - 1 ) ) E. j e. ( ( 0 ... ( m + 1 ) ) \ { ( 2nd ` t ) } ) i = [_ ( 1st ` t ) / s ]_ [_ ( ( ( 1st ` s ) oF + ( ( ( ( 2nd ` s ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` s ) " ( ( j + 1 ) ... ( m + 1 ) ) ) X. { 0 } ) ) ) u. ( ( ( ( m + 1 ) + 1 ) ... N ) X. { 0 } ) ) / p ]_ B } ) - ( # ` { s e. ( ( ( 0 ..^ K ) ^m ( 1 ... ( m + 1 ) ) ) X. { f | f : ( 1 ... ( m + 1 ) ) -1-1-onto-> ( 1 ... ( m + 1 ) ) } ) | A. i e. ( 0 ... ( m + 1 ) ) E. j e. ( 0 ... ( m + 1 ) ) i = [_ ( ( ( 1st ` s ) oF + ( ( ( ( 2nd ` s ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` s ) " ( ( j + 1 ) ... ( m + 1 ) ) ) X. { 0 } ) ) ) u. ( ( ( ( m + 1 ) + 1 ) ... N ) X. { 0 } ) ) / p ]_ B } ) ) ) = ( ( # ` { s e. ( ( ( 0 ..^ K ) ^m ( 1 ... ( m + 1 ) ) ) X. { f | f : ( 1 ... ( m + 1 ) ) -1-1-onto-> ( 1 ... ( m + 1 ) ) } ) | A. i e. ( 0 ... ( m + 1 ) ) E. j e. ( 0 ... ( m + 1 ) ) i = [_ ( ( ( 1st ` s ) oF + ( ( ( ( 2nd ` s ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` s ) " ( ( j + 1 ) ... ( m + 1 ) ) ) X. { 0 } ) ) ) u. ( ( ( ( m + 1 ) + 1 ) ... N ) X. { 0 } ) ) / p ]_ B } ) - ( # ` { s e. ( ( ( 0 ..^ K ) ^m ( 1 ... ( m + 1 ) ) ) X. { f | f : ( 1 ... ( m + 1 ) ) -1-1-onto-> ( 1 ... ( m + 1 ) ) } ) | ( A. i e. ( 0 ... ( ( m + 1 ) - 1 ) ) E. j e. ( 0 ... ( ( m + 1 ) - 1 ) ) i = [_ ( ( ( 1st ` s ) oF + ( ( ( ( 2nd ` s ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` s ) " ( ( j + 1 ) ... ( m + 1 ) ) ) X. { 0 } ) ) ) u. ( ( ( ( m + 1 ) + 1 ) ... N ) X. { 0 } ) ) / p ]_ B /\ ( ( 1st ` s ) ` ( m + 1 ) ) = 0 /\ ( ( 2nd ` s ) ` ( m + 1 ) ) = ( m + 1 ) ) } ) ) )
493 489 490 491 492 mp3an 
 |-  ( ( ( # ` { t e. ( ( ( ( 0 ..^ K ) ^m ( 1 ... ( m + 1 ) ) ) X. { f | f : ( 1 ... ( m + 1 ) ) -1-1-onto-> ( 1 ... ( m + 1 ) ) } ) X. ( 0 ... ( m + 1 ) ) ) | A. i e. ( 0 ... ( ( m + 1 ) - 1 ) ) E. j e. ( ( 0 ... ( m + 1 ) ) \ { ( 2nd ` t ) } ) i = [_ ( 1st ` t ) / s ]_ [_ ( ( ( 1st ` s ) oF + ( ( ( ( 2nd ` s ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` s ) " ( ( j + 1 ) ... ( m + 1 ) ) ) X. { 0 } ) ) ) u. ( ( ( ( m + 1 ) + 1 ) ... N ) X. { 0 } ) ) / p ]_ B } ) - ( # ` { s e. ( ( ( 0 ..^ K ) ^m ( 1 ... ( m + 1 ) ) ) X. { f | f : ( 1 ... ( m + 1 ) ) -1-1-onto-> ( 1 ... ( m + 1 ) ) } ) | ( A. i e. ( 0 ... ( ( m + 1 ) - 1 ) ) E. j e. ( 0 ... ( ( m + 1 ) - 1 ) ) i = [_ ( ( ( 1st ` s ) oF + ( ( ( ( 2nd ` s ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` s ) " ( ( j + 1 ) ... ( m + 1 ) ) ) X. { 0 } ) ) ) u. ( ( ( ( m + 1 ) + 1 ) ... N ) X. { 0 } ) ) / p ]_ B /\ ( ( 1st ` s ) ` ( m + 1 ) ) = 0 /\ ( ( 2nd ` s ) ` ( m + 1 ) ) = ( m + 1 ) ) } ) ) - ( ( # ` { t e. ( ( ( ( 0 ..^ K ) ^m ( 1 ... ( m + 1 ) ) ) X. { f | f : ( 1 ... ( m + 1 ) ) -1-1-onto-> ( 1 ... ( m + 1 ) ) } ) X. ( 0 ... ( m + 1 ) ) ) | A. i e. ( 0 ... ( ( m + 1 ) - 1 ) ) E. j e. ( ( 0 ... ( m + 1 ) ) \ { ( 2nd ` t ) } ) i = [_ ( 1st ` t ) / s ]_ [_ ( ( ( 1st ` s ) oF + ( ( ( ( 2nd ` s ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` s ) " ( ( j + 1 ) ... ( m + 1 ) ) ) X. { 0 } ) ) ) u. ( ( ( ( m + 1 ) + 1 ) ... N ) X. { 0 } ) ) / p ]_ B } ) - ( # ` { s e. ( ( ( 0 ..^ K ) ^m ( 1 ... ( m + 1 ) ) ) X. { f | f : ( 1 ... ( m + 1 ) ) -1-1-onto-> ( 1 ... ( m + 1 ) ) } ) | A. i e. ( 0 ... ( m + 1 ) ) E. j e. ( 0 ... ( m + 1 ) ) i = [_ ( ( ( 1st ` s ) oF + ( ( ( ( 2nd ` s ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` s ) " ( ( j + 1 ) ... ( m + 1 ) ) ) X. { 0 } ) ) ) u. ( ( ( ( m + 1 ) + 1 ) ... N ) X. { 0 } ) ) / p ]_ B } ) ) ) = ( ( # ` { s e. ( ( ( 0 ..^ K ) ^m ( 1 ... ( m + 1 ) ) ) X. { f | f : ( 1 ... ( m + 1 ) ) -1-1-onto-> ( 1 ... ( m + 1 ) ) } ) | A. i e. ( 0 ... ( m + 1 ) ) E. j e. ( 0 ... ( m + 1 ) ) i = [_ ( ( ( 1st ` s ) oF + ( ( ( ( 2nd ` s ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` s ) " ( ( j + 1 ) ... ( m + 1 ) ) ) X. { 0 } ) ) ) u. ( ( ( ( m + 1 ) + 1 ) ... N ) X. { 0 } ) ) / p ]_ B } ) - ( # ` { s e. ( ( ( 0 ..^ K ) ^m ( 1 ... ( m + 1 ) ) ) X. { f | f : ( 1 ... ( m + 1 ) ) -1-1-onto-> ( 1 ... ( m + 1 ) ) } ) | ( A. i e. ( 0 ... ( ( m + 1 ) - 1 ) ) E. j e. ( 0 ... ( ( m + 1 ) - 1 ) ) i = [_ ( ( ( 1st ` s ) oF + ( ( ( ( 2nd ` s ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` s ) " ( ( j + 1 ) ... ( m + 1 ) ) ) X. { 0 } ) ) ) u. ( ( ( ( m + 1 ) + 1 ) ... N ) X. { 0 } ) ) / p ]_ B /\ ( ( 1st ` s ) ` ( m + 1 ) ) = 0 /\ ( ( 2nd ` s ) ` ( m + 1 ) ) = ( m + 1 ) ) } ) )
494 488 493 breqtrdi 
 |-  ( ( ph /\ ( m e. NN0 /\ m < N ) ) -> 2 || ( ( # ` { s e. ( ( ( 0 ..^ K ) ^m ( 1 ... ( m + 1 ) ) ) X. { f | f : ( 1 ... ( m + 1 ) ) -1-1-onto-> ( 1 ... ( m + 1 ) ) } ) | A. i e. ( 0 ... ( m + 1 ) ) E. j e. ( 0 ... ( m + 1 ) ) i = [_ ( ( ( 1st ` s ) oF + ( ( ( ( 2nd ` s ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` s ) " ( ( j + 1 ) ... ( m + 1 ) ) ) X. { 0 } ) ) ) u. ( ( ( ( m + 1 ) + 1 ) ... N ) X. { 0 } ) ) / p ]_ B } ) - ( # ` { s e. ( ( ( 0 ..^ K ) ^m ( 1 ... ( m + 1 ) ) ) X. { f | f : ( 1 ... ( m + 1 ) ) -1-1-onto-> ( 1 ... ( m + 1 ) ) } ) | ( A. i e. ( 0 ... ( ( m + 1 ) - 1 ) ) E. j e. ( 0 ... ( ( m + 1 ) - 1 ) ) i = [_ ( ( ( 1st ` s ) oF + ( ( ( ( 2nd ` s ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` s ) " ( ( j + 1 ) ... ( m + 1 ) ) ) X. { 0 } ) ) ) u. ( ( ( ( m + 1 ) + 1 ) ... N ) X. { 0 } ) ) / p ]_ B /\ ( ( 1st ` s ) ` ( m + 1 ) ) = 0 /\ ( ( 2nd ` s ) ` ( m + 1 ) ) = ( m + 1 ) ) } ) ) )
495 dvdssub2 
 |-  ( ( ( 2 e. ZZ /\ ( # ` { s e. ( ( ( 0 ..^ K ) ^m ( 1 ... ( m + 1 ) ) ) X. { f | f : ( 1 ... ( m + 1 ) ) -1-1-onto-> ( 1 ... ( m + 1 ) ) } ) | A. i e. ( 0 ... ( m + 1 ) ) E. j e. ( 0 ... ( m + 1 ) ) i = [_ ( ( ( 1st ` s ) oF + ( ( ( ( 2nd ` s ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` s ) " ( ( j + 1 ) ... ( m + 1 ) ) ) X. { 0 } ) ) ) u. ( ( ( ( m + 1 ) + 1 ) ... N ) X. { 0 } ) ) / p ]_ B } ) e. ZZ /\ ( # ` { s e. ( ( ( 0 ..^ K ) ^m ( 1 ... ( m + 1 ) ) ) X. { f | f : ( 1 ... ( m + 1 ) ) -1-1-onto-> ( 1 ... ( m + 1 ) ) } ) | ( A. i e. ( 0 ... ( ( m + 1 ) - 1 ) ) E. j e. ( 0 ... ( ( m + 1 ) - 1 ) ) i = [_ ( ( ( 1st ` s ) oF + ( ( ( ( 2nd ` s ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` s ) " ( ( j + 1 ) ... ( m + 1 ) ) ) X. { 0 } ) ) ) u. ( ( ( ( m + 1 ) + 1 ) ... N ) X. { 0 } ) ) / p ]_ B /\ ( ( 1st ` s ) ` ( m + 1 ) ) = 0 /\ ( ( 2nd ` s ) ` ( m + 1 ) ) = ( m + 1 ) ) } ) e. ZZ ) /\ 2 || ( ( # ` { s e. ( ( ( 0 ..^ K ) ^m ( 1 ... ( m + 1 ) ) ) X. { f | f : ( 1 ... ( m + 1 ) ) -1-1-onto-> ( 1 ... ( m + 1 ) ) } ) | A. i e. ( 0 ... ( m + 1 ) ) E. j e. ( 0 ... ( m + 1 ) ) i = [_ ( ( ( 1st ` s ) oF + ( ( ( ( 2nd ` s ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` s ) " ( ( j + 1 ) ... ( m + 1 ) ) ) X. { 0 } ) ) ) u. ( ( ( ( m + 1 ) + 1 ) ... N ) X. { 0 } ) ) / p ]_ B } ) - ( # ` { s e. ( ( ( 0 ..^ K ) ^m ( 1 ... ( m + 1 ) ) ) X. { f | f : ( 1 ... ( m + 1 ) ) -1-1-onto-> ( 1 ... ( m + 1 ) ) } ) | ( A. i e. ( 0 ... ( ( m + 1 ) - 1 ) ) E. j e. ( 0 ... ( ( m + 1 ) - 1 ) ) i = [_ ( ( ( 1st ` s ) oF + ( ( ( ( 2nd ` s ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` s ) " ( ( j + 1 ) ... ( m + 1 ) ) ) X. { 0 } ) ) ) u. ( ( ( ( m + 1 ) + 1 ) ... N ) X. { 0 } ) ) / p ]_ B /\ ( ( 1st ` s ) ` ( m + 1 ) ) = 0 /\ ( ( 2nd ` s ) ` ( m + 1 ) ) = ( m + 1 ) ) } ) ) ) -> ( 2 || ( # ` { s e. ( ( ( 0 ..^ K ) ^m ( 1 ... ( m + 1 ) ) ) X. { f | f : ( 1 ... ( m + 1 ) ) -1-1-onto-> ( 1 ... ( m + 1 ) ) } ) | A. i e. ( 0 ... ( m + 1 ) ) E. j e. ( 0 ... ( m + 1 ) ) i = [_ ( ( ( 1st ` s ) oF + ( ( ( ( 2nd ` s ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` s ) " ( ( j + 1 ) ... ( m + 1 ) ) ) X. { 0 } ) ) ) u. ( ( ( ( m + 1 ) + 1 ) ... N ) X. { 0 } ) ) / p ]_ B } ) <-> 2 || ( # ` { s e. ( ( ( 0 ..^ K ) ^m ( 1 ... ( m + 1 ) ) ) X. { f | f : ( 1 ... ( m + 1 ) ) -1-1-onto-> ( 1 ... ( m + 1 ) ) } ) | ( A. i e. ( 0 ... ( ( m + 1 ) - 1 ) ) E. j e. ( 0 ... ( ( m + 1 ) - 1 ) ) i = [_ ( ( ( 1st ` s ) oF + ( ( ( ( 2nd ` s ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` s ) " ( ( j + 1 ) ... ( m + 1 ) ) ) X. { 0 } ) ) ) u. ( ( ( ( m + 1 ) + 1 ) ... N ) X. { 0 } ) ) / p ]_ B /\ ( ( 1st ` s ) ` ( m + 1 ) ) = 0 /\ ( ( 2nd ` s ) ` ( m + 1 ) ) = ( m + 1 ) ) } ) ) )
496 265 494 495 sylancr 
 |-  ( ( ph /\ ( m e. NN0 /\ m < N ) ) -> ( 2 || ( # ` { s e. ( ( ( 0 ..^ K ) ^m ( 1 ... ( m + 1 ) ) ) X. { f | f : ( 1 ... ( m + 1 ) ) -1-1-onto-> ( 1 ... ( m + 1 ) ) } ) | A. i e. ( 0 ... ( m + 1 ) ) E. j e. ( 0 ... ( m + 1 ) ) i = [_ ( ( ( 1st ` s ) oF + ( ( ( ( 2nd ` s ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` s ) " ( ( j + 1 ) ... ( m + 1 ) ) ) X. { 0 } ) ) ) u. ( ( ( ( m + 1 ) + 1 ) ... N ) X. { 0 } ) ) / p ]_ B } ) <-> 2 || ( # ` { s e. ( ( ( 0 ..^ K ) ^m ( 1 ... ( m + 1 ) ) ) X. { f | f : ( 1 ... ( m + 1 ) ) -1-1-onto-> ( 1 ... ( m + 1 ) ) } ) | ( A. i e. ( 0 ... ( ( m + 1 ) - 1 ) ) E. j e. ( 0 ... ( ( m + 1 ) - 1 ) ) i = [_ ( ( ( 1st ` s ) oF + ( ( ( ( 2nd ` s ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` s ) " ( ( j + 1 ) ... ( m + 1 ) ) ) X. { 0 } ) ) ) u. ( ( ( ( m + 1 ) + 1 ) ... N ) X. { 0 } ) ) / p ]_ B /\ ( ( 1st ` s ) ` ( m + 1 ) ) = 0 /\ ( ( 2nd ` s ) ` ( m + 1 ) ) = ( m + 1 ) ) } ) ) )
497 nn0cn 
 |-  ( m e. NN0 -> m e. CC )
498 pncan1 
 |-  ( m e. CC -> ( ( m + 1 ) - 1 ) = m )
499 497 498 syl 
 |-  ( m e. NN0 -> ( ( m + 1 ) - 1 ) = m )
500 499 oveq2d 
 |-  ( m e. NN0 -> ( 0 ... ( ( m + 1 ) - 1 ) ) = ( 0 ... m ) )
501 500 rexeqdv 
 |-  ( m e. NN0 -> ( E. j e. ( 0 ... ( ( m + 1 ) - 1 ) ) i = [_ ( ( ( 1st ` s ) oF + ( ( ( ( 2nd ` s ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` s ) " ( ( j + 1 ) ... ( m + 1 ) ) ) X. { 0 } ) ) ) u. ( ( ( ( m + 1 ) + 1 ) ... N ) X. { 0 } ) ) / p ]_ B <-> E. j e. ( 0 ... m ) i = [_ ( ( ( 1st ` s ) oF + ( ( ( ( 2nd ` s ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` s ) " ( ( j + 1 ) ... ( m + 1 ) ) ) X. { 0 } ) ) ) u. ( ( ( ( m + 1 ) + 1 ) ... N ) X. { 0 } ) ) / p ]_ B ) )
502 500 501 raleqbidv 
 |-  ( m e. NN0 -> ( A. i e. ( 0 ... ( ( m + 1 ) - 1 ) ) E. j e. ( 0 ... ( ( m + 1 ) - 1 ) ) i = [_ ( ( ( 1st ` s ) oF + ( ( ( ( 2nd ` s ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` s ) " ( ( j + 1 ) ... ( m + 1 ) ) ) X. { 0 } ) ) ) u. ( ( ( ( m + 1 ) + 1 ) ... N ) X. { 0 } ) ) / p ]_ B <-> A. i e. ( 0 ... m ) E. j e. ( 0 ... m ) i = [_ ( ( ( 1st ` s ) oF + ( ( ( ( 2nd ` s ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` s ) " ( ( j + 1 ) ... ( m + 1 ) ) ) X. { 0 } ) ) ) u. ( ( ( ( m + 1 ) + 1 ) ... N ) X. { 0 } ) ) / p ]_ B ) )
503 502 3anbi1d 
 |-  ( m e. NN0 -> ( ( A. i e. ( 0 ... ( ( m + 1 ) - 1 ) ) E. j e. ( 0 ... ( ( m + 1 ) - 1 ) ) i = [_ ( ( ( 1st ` s ) oF + ( ( ( ( 2nd ` s ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` s ) " ( ( j + 1 ) ... ( m + 1 ) ) ) X. { 0 } ) ) ) u. ( ( ( ( m + 1 ) + 1 ) ... N ) X. { 0 } ) ) / p ]_ B /\ ( ( 1st ` s ) ` ( m + 1 ) ) = 0 /\ ( ( 2nd ` s ) ` ( m + 1 ) ) = ( m + 1 ) ) <-> ( A. i e. ( 0 ... m ) E. j e. ( 0 ... m ) i = [_ ( ( ( 1st ` s ) oF + ( ( ( ( 2nd ` s ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` s ) " ( ( j + 1 ) ... ( m + 1 ) ) ) X. { 0 } ) ) ) u. ( ( ( ( m + 1 ) + 1 ) ... N ) X. { 0 } ) ) / p ]_ B /\ ( ( 1st ` s ) ` ( m + 1 ) ) = 0 /\ ( ( 2nd ` s ) ` ( m + 1 ) ) = ( m + 1 ) ) ) )
504 503 rabbidv 
 |-  ( m e. NN0 -> { s e. ( ( ( 0 ..^ K ) ^m ( 1 ... ( m + 1 ) ) ) X. { f | f : ( 1 ... ( m + 1 ) ) -1-1-onto-> ( 1 ... ( m + 1 ) ) } ) | ( A. i e. ( 0 ... ( ( m + 1 ) - 1 ) ) E. j e. ( 0 ... ( ( m + 1 ) - 1 ) ) i = [_ ( ( ( 1st ` s ) oF + ( ( ( ( 2nd ` s ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` s ) " ( ( j + 1 ) ... ( m + 1 ) ) ) X. { 0 } ) ) ) u. ( ( ( ( m + 1 ) + 1 ) ... N ) X. { 0 } ) ) / p ]_ B /\ ( ( 1st ` s ) ` ( m + 1 ) ) = 0 /\ ( ( 2nd ` s ) ` ( m + 1 ) ) = ( m + 1 ) ) } = { s e. ( ( ( 0 ..^ K ) ^m ( 1 ... ( m + 1 ) ) ) X. { f | f : ( 1 ... ( m + 1 ) ) -1-1-onto-> ( 1 ... ( m + 1 ) ) } ) | ( A. i e. ( 0 ... m ) E. j e. ( 0 ... m ) i = [_ ( ( ( 1st ` s ) oF + ( ( ( ( 2nd ` s ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` s ) " ( ( j + 1 ) ... ( m + 1 ) ) ) X. { 0 } ) ) ) u. ( ( ( ( m + 1 ) + 1 ) ... N ) X. { 0 } ) ) / p ]_ B /\ ( ( 1st ` s ) ` ( m + 1 ) ) = 0 /\ ( ( 2nd ` s ) ` ( m + 1 ) ) = ( m + 1 ) ) } )
505 504 fveq2d 
 |-  ( m e. NN0 -> ( # ` { s e. ( ( ( 0 ..^ K ) ^m ( 1 ... ( m + 1 ) ) ) X. { f | f : ( 1 ... ( m + 1 ) ) -1-1-onto-> ( 1 ... ( m + 1 ) ) } ) | ( A. i e. ( 0 ... ( ( m + 1 ) - 1 ) ) E. j e. ( 0 ... ( ( m + 1 ) - 1 ) ) i = [_ ( ( ( 1st ` s ) oF + ( ( ( ( 2nd ` s ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` s ) " ( ( j + 1 ) ... ( m + 1 ) ) ) X. { 0 } ) ) ) u. ( ( ( ( m + 1 ) + 1 ) ... N ) X. { 0 } ) ) / p ]_ B /\ ( ( 1st ` s ) ` ( m + 1 ) ) = 0 /\ ( ( 2nd ` s ) ` ( m + 1 ) ) = ( m + 1 ) ) } ) = ( # ` { s e. ( ( ( 0 ..^ K ) ^m ( 1 ... ( m + 1 ) ) ) X. { f | f : ( 1 ... ( m + 1 ) ) -1-1-onto-> ( 1 ... ( m + 1 ) ) } ) | ( A. i e. ( 0 ... m ) E. j e. ( 0 ... m ) i = [_ ( ( ( 1st ` s ) oF + ( ( ( ( 2nd ` s ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` s ) " ( ( j + 1 ) ... ( m + 1 ) ) ) X. { 0 } ) ) ) u. ( ( ( ( m + 1 ) + 1 ) ... N ) X. { 0 } ) ) / p ]_ B /\ ( ( 1st ` s ) ` ( m + 1 ) ) = 0 /\ ( ( 2nd ` s ) ` ( m + 1 ) ) = ( m + 1 ) ) } ) )
506 505 ad2antrl 
 |-  ( ( ph /\ ( m e. NN0 /\ m < N ) ) -> ( # ` { s e. ( ( ( 0 ..^ K ) ^m ( 1 ... ( m + 1 ) ) ) X. { f | f : ( 1 ... ( m + 1 ) ) -1-1-onto-> ( 1 ... ( m + 1 ) ) } ) | ( A. i e. ( 0 ... ( ( m + 1 ) - 1 ) ) E. j e. ( 0 ... ( ( m + 1 ) - 1 ) ) i = [_ ( ( ( 1st ` s ) oF + ( ( ( ( 2nd ` s ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` s ) " ( ( j + 1 ) ... ( m + 1 ) ) ) X. { 0 } ) ) ) u. ( ( ( ( m + 1 ) + 1 ) ... N ) X. { 0 } ) ) / p ]_ B /\ ( ( 1st ` s ) ` ( m + 1 ) ) = 0 /\ ( ( 2nd ` s ) ` ( m + 1 ) ) = ( m + 1 ) ) } ) = ( # ` { s e. ( ( ( 0 ..^ K ) ^m ( 1 ... ( m + 1 ) ) ) X. { f | f : ( 1 ... ( m + 1 ) ) -1-1-onto-> ( 1 ... ( m + 1 ) ) } ) | ( A. i e. ( 0 ... m ) E. j e. ( 0 ... m ) i = [_ ( ( ( 1st ` s ) oF + ( ( ( ( 2nd ` s ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` s ) " ( ( j + 1 ) ... ( m + 1 ) ) ) X. { 0 } ) ) ) u. ( ( ( ( m + 1 ) + 1 ) ... N ) X. { 0 } ) ) / p ]_ B /\ ( ( 1st ` s ) ` ( m + 1 ) ) = 0 /\ ( ( 2nd ` s ) ` ( m + 1 ) ) = ( m + 1 ) ) } ) )
507 1 adantr 
 |-  ( ( ph /\ ( m e. NN0 /\ m < N ) ) -> N e. NN )
508 6 adantr 
 |-  ( ( ph /\ ( m e. NN0 /\ m < N ) ) -> K e. NN )
509 simprl 
 |-  ( ( ph /\ ( m e. NN0 /\ m < N ) ) -> m e. NN0 )
510 simprr 
 |-  ( ( ph /\ ( m e. NN0 /\ m < N ) ) -> m < N )
511 507 508 509 510 poimirlem4 
 |-  ( ( ph /\ ( m e. NN0 /\ m < N ) ) -> { s e. ( ( ( 0 ..^ K ) ^m ( 1 ... m ) ) X. { f | f : ( 1 ... m ) -1-1-onto-> ( 1 ... m ) } ) | A. i e. ( 0 ... m ) E. j e. ( 0 ... m ) i = [_ ( ( ( 1st ` s ) oF + ( ( ( ( 2nd ` s ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` s ) " ( ( j + 1 ) ... m ) ) X. { 0 } ) ) ) u. ( ( ( m + 1 ) ... N ) X. { 0 } ) ) / p ]_ B } ~~ { s e. ( ( ( 0 ..^ K ) ^m ( 1 ... ( m + 1 ) ) ) X. { f | f : ( 1 ... ( m + 1 ) ) -1-1-onto-> ( 1 ... ( m + 1 ) ) } ) | ( A. i e. ( 0 ... m ) E. j e. ( 0 ... m ) i = [_ ( ( ( 1st ` s ) oF + ( ( ( ( 2nd ` s ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` s ) " ( ( j + 1 ) ... ( m + 1 ) ) ) X. { 0 } ) ) ) u. ( ( ( ( m + 1 ) + 1 ) ... N ) X. { 0 } ) ) / p ]_ B /\ ( ( 1st ` s ) ` ( m + 1 ) ) = 0 /\ ( ( 2nd ` s ) ` ( m + 1 ) ) = ( m + 1 ) ) } )
512 fzfi 
 |-  ( 1 ... m ) e. Fin
513 mapfi 
 |-  ( ( ( 0 ..^ K ) e. Fin /\ ( 1 ... m ) e. Fin ) -> ( ( 0 ..^ K ) ^m ( 1 ... m ) ) e. Fin )
514 15 512 513 mp2an 
 |-  ( ( 0 ..^ K ) ^m ( 1 ... m ) ) e. Fin
515 ovex 
 |-  ( 1 ... m ) e. _V
516 515 515 mapval 
 |-  ( ( 1 ... m ) ^m ( 1 ... m ) ) = { f | f : ( 1 ... m ) --> ( 1 ... m ) }
517 mapfi 
 |-  ( ( ( 1 ... m ) e. Fin /\ ( 1 ... m ) e. Fin ) -> ( ( 1 ... m ) ^m ( 1 ... m ) ) e. Fin )
518 512 512 517 mp2an 
 |-  ( ( 1 ... m ) ^m ( 1 ... m ) ) e. Fin
519 516 518 eqeltrri 
 |-  { f | f : ( 1 ... m ) --> ( 1 ... m ) } e. Fin
520 f1of 
 |-  ( f : ( 1 ... m ) -1-1-onto-> ( 1 ... m ) -> f : ( 1 ... m ) --> ( 1 ... m ) )
521 520 ss2abi 
 |-  { f | f : ( 1 ... m ) -1-1-onto-> ( 1 ... m ) } C_ { f | f : ( 1 ... m ) --> ( 1 ... m ) }
522 ssfi 
 |-  ( ( { f | f : ( 1 ... m ) --> ( 1 ... m ) } e. Fin /\ { f | f : ( 1 ... m ) -1-1-onto-> ( 1 ... m ) } C_ { f | f : ( 1 ... m ) --> ( 1 ... m ) } ) -> { f | f : ( 1 ... m ) -1-1-onto-> ( 1 ... m ) } e. Fin )
523 519 521 522 mp2an 
 |-  { f | f : ( 1 ... m ) -1-1-onto-> ( 1 ... m ) } e. Fin
524 xpfi 
 |-  ( ( ( ( 0 ..^ K ) ^m ( 1 ... m ) ) e. Fin /\ { f | f : ( 1 ... m ) -1-1-onto-> ( 1 ... m ) } e. Fin ) -> ( ( ( 0 ..^ K ) ^m ( 1 ... m ) ) X. { f | f : ( 1 ... m ) -1-1-onto-> ( 1 ... m ) } ) e. Fin )
525 514 523 524 mp2an 
 |-  ( ( ( 0 ..^ K ) ^m ( 1 ... m ) ) X. { f | f : ( 1 ... m ) -1-1-onto-> ( 1 ... m ) } ) e. Fin
526 rabfi 
 |-  ( ( ( ( 0 ..^ K ) ^m ( 1 ... m ) ) X. { f | f : ( 1 ... m ) -1-1-onto-> ( 1 ... m ) } ) e. Fin -> { s e. ( ( ( 0 ..^ K ) ^m ( 1 ... m ) ) X. { f | f : ( 1 ... m ) -1-1-onto-> ( 1 ... m ) } ) | A. i e. ( 0 ... m ) E. j e. ( 0 ... m ) i = [_ ( ( ( 1st ` s ) oF + ( ( ( ( 2nd ` s ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` s ) " ( ( j + 1 ) ... m ) ) X. { 0 } ) ) ) u. ( ( ( m + 1 ) ... N ) X. { 0 } ) ) / p ]_ B } e. Fin )
527 525 526 ax-mp 
 |-  { s e. ( ( ( 0 ..^ K ) ^m ( 1 ... m ) ) X. { f | f : ( 1 ... m ) -1-1-onto-> ( 1 ... m ) } ) | A. i e. ( 0 ... m ) E. j e. ( 0 ... m ) i = [_ ( ( ( 1st ` s ) oF + ( ( ( ( 2nd ` s ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` s ) " ( ( j + 1 ) ... m ) ) X. { 0 } ) ) ) u. ( ( ( m + 1 ) ... N ) X. { 0 } ) ) / p ]_ B } e. Fin
528 rabfi 
 |-  ( ( ( ( 0 ..^ K ) ^m ( 1 ... ( m + 1 ) ) ) X. { f | f : ( 1 ... ( m + 1 ) ) -1-1-onto-> ( 1 ... ( m + 1 ) ) } ) e. Fin -> { s e. ( ( ( 0 ..^ K ) ^m ( 1 ... ( m + 1 ) ) ) X. { f | f : ( 1 ... ( m + 1 ) ) -1-1-onto-> ( 1 ... ( m + 1 ) ) } ) | ( A. i e. ( 0 ... m ) E. j e. ( 0 ... m ) i = [_ ( ( ( 1st ` s ) oF + ( ( ( ( 2nd ` s ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` s ) " ( ( j + 1 ) ... ( m + 1 ) ) ) X. { 0 } ) ) ) u. ( ( ( ( m + 1 ) + 1 ) ... N ) X. { 0 } ) ) / p ]_ B /\ ( ( 1st ` s ) ` ( m + 1 ) ) = 0 /\ ( ( 2nd ` s ) ` ( m + 1 ) ) = ( m + 1 ) ) } e. Fin )
529 256 528 ax-mp 
 |-  { s e. ( ( ( 0 ..^ K ) ^m ( 1 ... ( m + 1 ) ) ) X. { f | f : ( 1 ... ( m + 1 ) ) -1-1-onto-> ( 1 ... ( m + 1 ) ) } ) | ( A. i e. ( 0 ... m ) E. j e. ( 0 ... m ) i = [_ ( ( ( 1st ` s ) oF + ( ( ( ( 2nd ` s ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` s ) " ( ( j + 1 ) ... ( m + 1 ) ) ) X. { 0 } ) ) ) u. ( ( ( ( m + 1 ) + 1 ) ... N ) X. { 0 } ) ) / p ]_ B /\ ( ( 1st ` s ) ` ( m + 1 ) ) = 0 /\ ( ( 2nd ` s ) ` ( m + 1 ) ) = ( m + 1 ) ) } e. Fin
530 hashen 
 |-  ( ( { s e. ( ( ( 0 ..^ K ) ^m ( 1 ... m ) ) X. { f | f : ( 1 ... m ) -1-1-onto-> ( 1 ... m ) } ) | A. i e. ( 0 ... m ) E. j e. ( 0 ... m ) i = [_ ( ( ( 1st ` s ) oF + ( ( ( ( 2nd ` s ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` s ) " ( ( j + 1 ) ... m ) ) X. { 0 } ) ) ) u. ( ( ( m + 1 ) ... N ) X. { 0 } ) ) / p ]_ B } e. Fin /\ { s e. ( ( ( 0 ..^ K ) ^m ( 1 ... ( m + 1 ) ) ) X. { f | f : ( 1 ... ( m + 1 ) ) -1-1-onto-> ( 1 ... ( m + 1 ) ) } ) | ( A. i e. ( 0 ... m ) E. j e. ( 0 ... m ) i = [_ ( ( ( 1st ` s ) oF + ( ( ( ( 2nd ` s ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` s ) " ( ( j + 1 ) ... ( m + 1 ) ) ) X. { 0 } ) ) ) u. ( ( ( ( m + 1 ) + 1 ) ... N ) X. { 0 } ) ) / p ]_ B /\ ( ( 1st ` s ) ` ( m + 1 ) ) = 0 /\ ( ( 2nd ` s ) ` ( m + 1 ) ) = ( m + 1 ) ) } e. Fin ) -> ( ( # ` { s e. ( ( ( 0 ..^ K ) ^m ( 1 ... m ) ) X. { f | f : ( 1 ... m ) -1-1-onto-> ( 1 ... m ) } ) | A. i e. ( 0 ... m ) E. j e. ( 0 ... m ) i = [_ ( ( ( 1st ` s ) oF + ( ( ( ( 2nd ` s ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` s ) " ( ( j + 1 ) ... m ) ) X. { 0 } ) ) ) u. ( ( ( m + 1 ) ... N ) X. { 0 } ) ) / p ]_ B } ) = ( # ` { s e. ( ( ( 0 ..^ K ) ^m ( 1 ... ( m + 1 ) ) ) X. { f | f : ( 1 ... ( m + 1 ) ) -1-1-onto-> ( 1 ... ( m + 1 ) ) } ) | ( A. i e. ( 0 ... m ) E. j e. ( 0 ... m ) i = [_ ( ( ( 1st ` s ) oF + ( ( ( ( 2nd ` s ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` s ) " ( ( j + 1 ) ... ( m + 1 ) ) ) X. { 0 } ) ) ) u. ( ( ( ( m + 1 ) + 1 ) ... N ) X. { 0 } ) ) / p ]_ B /\ ( ( 1st ` s ) ` ( m + 1 ) ) = 0 /\ ( ( 2nd ` s ) ` ( m + 1 ) ) = ( m + 1 ) ) } ) <-> { s e. ( ( ( 0 ..^ K ) ^m ( 1 ... m ) ) X. { f | f : ( 1 ... m ) -1-1-onto-> ( 1 ... m ) } ) | A. i e. ( 0 ... m ) E. j e. ( 0 ... m ) i = [_ ( ( ( 1st ` s ) oF + ( ( ( ( 2nd ` s ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` s ) " ( ( j + 1 ) ... m ) ) X. { 0 } ) ) ) u. ( ( ( m + 1 ) ... N ) X. { 0 } ) ) / p ]_ B } ~~ { s e. ( ( ( 0 ..^ K ) ^m ( 1 ... ( m + 1 ) ) ) X. { f | f : ( 1 ... ( m + 1 ) ) -1-1-onto-> ( 1 ... ( m + 1 ) ) } ) | ( A. i e. ( 0 ... m ) E. j e. ( 0 ... m ) i = [_ ( ( ( 1st ` s ) oF + ( ( ( ( 2nd ` s ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` s ) " ( ( j + 1 ) ... ( m + 1 ) ) ) X. { 0 } ) ) ) u. ( ( ( ( m + 1 ) + 1 ) ... N ) X. { 0 } ) ) / p ]_ B /\ ( ( 1st ` s ) ` ( m + 1 ) ) = 0 /\ ( ( 2nd ` s ) ` ( m + 1 ) ) = ( m + 1 ) ) } ) )
531 527 529 530 mp2an 
 |-  ( ( # ` { s e. ( ( ( 0 ..^ K ) ^m ( 1 ... m ) ) X. { f | f : ( 1 ... m ) -1-1-onto-> ( 1 ... m ) } ) | A. i e. ( 0 ... m ) E. j e. ( 0 ... m ) i = [_ ( ( ( 1st ` s ) oF + ( ( ( ( 2nd ` s ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` s ) " ( ( j + 1 ) ... m ) ) X. { 0 } ) ) ) u. ( ( ( m + 1 ) ... N ) X. { 0 } ) ) / p ]_ B } ) = ( # ` { s e. ( ( ( 0 ..^ K ) ^m ( 1 ... ( m + 1 ) ) ) X. { f | f : ( 1 ... ( m + 1 ) ) -1-1-onto-> ( 1 ... ( m + 1 ) ) } ) | ( A. i e. ( 0 ... m ) E. j e. ( 0 ... m ) i = [_ ( ( ( 1st ` s ) oF + ( ( ( ( 2nd ` s ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` s ) " ( ( j + 1 ) ... ( m + 1 ) ) ) X. { 0 } ) ) ) u. ( ( ( ( m + 1 ) + 1 ) ... N ) X. { 0 } ) ) / p ]_ B /\ ( ( 1st ` s ) ` ( m + 1 ) ) = 0 /\ ( ( 2nd ` s ) ` ( m + 1 ) ) = ( m + 1 ) ) } ) <-> { s e. ( ( ( 0 ..^ K ) ^m ( 1 ... m ) ) X. { f | f : ( 1 ... m ) -1-1-onto-> ( 1 ... m ) } ) | A. i e. ( 0 ... m ) E. j e. ( 0 ... m ) i = [_ ( ( ( 1st ` s ) oF + ( ( ( ( 2nd ` s ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` s ) " ( ( j + 1 ) ... m ) ) X. { 0 } ) ) ) u. ( ( ( m + 1 ) ... N ) X. { 0 } ) ) / p ]_ B } ~~ { s e. ( ( ( 0 ..^ K ) ^m ( 1 ... ( m + 1 ) ) ) X. { f | f : ( 1 ... ( m + 1 ) ) -1-1-onto-> ( 1 ... ( m + 1 ) ) } ) | ( A. i e. ( 0 ... m ) E. j e. ( 0 ... m ) i = [_ ( ( ( 1st ` s ) oF + ( ( ( ( 2nd ` s ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` s ) " ( ( j + 1 ) ... ( m + 1 ) ) ) X. { 0 } ) ) ) u. ( ( ( ( m + 1 ) + 1 ) ... N ) X. { 0 } ) ) / p ]_ B /\ ( ( 1st ` s ) ` ( m + 1 ) ) = 0 /\ ( ( 2nd ` s ) ` ( m + 1 ) ) = ( m + 1 ) ) } )
532 511 531 sylibr 
 |-  ( ( ph /\ ( m e. NN0 /\ m < N ) ) -> ( # ` { s e. ( ( ( 0 ..^ K ) ^m ( 1 ... m ) ) X. { f | f : ( 1 ... m ) -1-1-onto-> ( 1 ... m ) } ) | A. i e. ( 0 ... m ) E. j e. ( 0 ... m ) i = [_ ( ( ( 1st ` s ) oF + ( ( ( ( 2nd ` s ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` s ) " ( ( j + 1 ) ... m ) ) X. { 0 } ) ) ) u. ( ( ( m + 1 ) ... N ) X. { 0 } ) ) / p ]_ B } ) = ( # ` { s e. ( ( ( 0 ..^ K ) ^m ( 1 ... ( m + 1 ) ) ) X. { f | f : ( 1 ... ( m + 1 ) ) -1-1-onto-> ( 1 ... ( m + 1 ) ) } ) | ( A. i e. ( 0 ... m ) E. j e. ( 0 ... m ) i = [_ ( ( ( 1st ` s ) oF + ( ( ( ( 2nd ` s ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` s ) " ( ( j + 1 ) ... ( m + 1 ) ) ) X. { 0 } ) ) ) u. ( ( ( ( m + 1 ) + 1 ) ... N ) X. { 0 } ) ) / p ]_ B /\ ( ( 1st ` s ) ` ( m + 1 ) ) = 0 /\ ( ( 2nd ` s ) ` ( m + 1 ) ) = ( m + 1 ) ) } ) )
533 506 532 eqtr4d 
 |-  ( ( ph /\ ( m e. NN0 /\ m < N ) ) -> ( # ` { s e. ( ( ( 0 ..^ K ) ^m ( 1 ... ( m + 1 ) ) ) X. { f | f : ( 1 ... ( m + 1 ) ) -1-1-onto-> ( 1 ... ( m + 1 ) ) } ) | ( A. i e. ( 0 ... ( ( m + 1 ) - 1 ) ) E. j e. ( 0 ... ( ( m + 1 ) - 1 ) ) i = [_ ( ( ( 1st ` s ) oF + ( ( ( ( 2nd ` s ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` s ) " ( ( j + 1 ) ... ( m + 1 ) ) ) X. { 0 } ) ) ) u. ( ( ( ( m + 1 ) + 1 ) ... N ) X. { 0 } ) ) / p ]_ B /\ ( ( 1st ` s ) ` ( m + 1 ) ) = 0 /\ ( ( 2nd ` s ) ` ( m + 1 ) ) = ( m + 1 ) ) } ) = ( # ` { s e. ( ( ( 0 ..^ K ) ^m ( 1 ... m ) ) X. { f | f : ( 1 ... m ) -1-1-onto-> ( 1 ... m ) } ) | A. i e. ( 0 ... m ) E. j e. ( 0 ... m ) i = [_ ( ( ( 1st ` s ) oF + ( ( ( ( 2nd ` s ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` s ) " ( ( j + 1 ) ... m ) ) X. { 0 } ) ) ) u. ( ( ( m + 1 ) ... N ) X. { 0 } ) ) / p ]_ B } ) )
534 533 breq2d 
 |-  ( ( ph /\ ( m e. NN0 /\ m < N ) ) -> ( 2 || ( # ` { s e. ( ( ( 0 ..^ K ) ^m ( 1 ... ( m + 1 ) ) ) X. { f | f : ( 1 ... ( m + 1 ) ) -1-1-onto-> ( 1 ... ( m + 1 ) ) } ) | ( A. i e. ( 0 ... ( ( m + 1 ) - 1 ) ) E. j e. ( 0 ... ( ( m + 1 ) - 1 ) ) i = [_ ( ( ( 1st ` s ) oF + ( ( ( ( 2nd ` s ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` s ) " ( ( j + 1 ) ... ( m + 1 ) ) ) X. { 0 } ) ) ) u. ( ( ( ( m + 1 ) + 1 ) ... N ) X. { 0 } ) ) / p ]_ B /\ ( ( 1st ` s ) ` ( m + 1 ) ) = 0 /\ ( ( 2nd ` s ) ` ( m + 1 ) ) = ( m + 1 ) ) } ) <-> 2 || ( # ` { s e. ( ( ( 0 ..^ K ) ^m ( 1 ... m ) ) X. { f | f : ( 1 ... m ) -1-1-onto-> ( 1 ... m ) } ) | A. i e. ( 0 ... m ) E. j e. ( 0 ... m ) i = [_ ( ( ( 1st ` s ) oF + ( ( ( ( 2nd ` s ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` s ) " ( ( j + 1 ) ... m ) ) X. { 0 } ) ) ) u. ( ( ( m + 1 ) ... N ) X. { 0 } ) ) / p ]_ B } ) ) )
535 496 534 bitrd 
 |-  ( ( ph /\ ( m e. NN0 /\ m < N ) ) -> ( 2 || ( # ` { s e. ( ( ( 0 ..^ K ) ^m ( 1 ... ( m + 1 ) ) ) X. { f | f : ( 1 ... ( m + 1 ) ) -1-1-onto-> ( 1 ... ( m + 1 ) ) } ) | A. i e. ( 0 ... ( m + 1 ) ) E. j e. ( 0 ... ( m + 1 ) ) i = [_ ( ( ( 1st ` s ) oF + ( ( ( ( 2nd ` s ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` s ) " ( ( j + 1 ) ... ( m + 1 ) ) ) X. { 0 } ) ) ) u. ( ( ( ( m + 1 ) + 1 ) ... N ) X. { 0 } ) ) / p ]_ B } ) <-> 2 || ( # ` { s e. ( ( ( 0 ..^ K ) ^m ( 1 ... m ) ) X. { f | f : ( 1 ... m ) -1-1-onto-> ( 1 ... m ) } ) | A. i e. ( 0 ... m ) E. j e. ( 0 ... m ) i = [_ ( ( ( 1st ` s ) oF + ( ( ( ( 2nd ` s ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` s ) " ( ( j + 1 ) ... m ) ) X. { 0 } ) ) ) u. ( ( ( m + 1 ) ... N ) X. { 0 } ) ) / p ]_ B } ) ) )
536 535 biimpd 
 |-  ( ( ph /\ ( m e. NN0 /\ m < N ) ) -> ( 2 || ( # ` { s e. ( ( ( 0 ..^ K ) ^m ( 1 ... ( m + 1 ) ) ) X. { f | f : ( 1 ... ( m + 1 ) ) -1-1-onto-> ( 1 ... ( m + 1 ) ) } ) | A. i e. ( 0 ... ( m + 1 ) ) E. j e. ( 0 ... ( m + 1 ) ) i = [_ ( ( ( 1st ` s ) oF + ( ( ( ( 2nd ` s ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` s ) " ( ( j + 1 ) ... ( m + 1 ) ) ) X. { 0 } ) ) ) u. ( ( ( ( m + 1 ) + 1 ) ... N ) X. { 0 } ) ) / p ]_ B } ) -> 2 || ( # ` { s e. ( ( ( 0 ..^ K ) ^m ( 1 ... m ) ) X. { f | f : ( 1 ... m ) -1-1-onto-> ( 1 ... m ) } ) | A. i e. ( 0 ... m ) E. j e. ( 0 ... m ) i = [_ ( ( ( 1st ` s ) oF + ( ( ( ( 2nd ` s ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` s ) " ( ( j + 1 ) ... m ) ) X. { 0 } ) ) ) u. ( ( ( m + 1 ) ... N ) X. { 0 } ) ) / p ]_ B } ) ) )
537 536 con3d 
 |-  ( ( ph /\ ( m e. NN0 /\ m < N ) ) -> ( -. 2 || ( # ` { s e. ( ( ( 0 ..^ K ) ^m ( 1 ... m ) ) X. { f | f : ( 1 ... m ) -1-1-onto-> ( 1 ... m ) } ) | A. i e. ( 0 ... m ) E. j e. ( 0 ... m ) i = [_ ( ( ( 1st ` s ) oF + ( ( ( ( 2nd ` s ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` s ) " ( ( j + 1 ) ... m ) ) X. { 0 } ) ) ) u. ( ( ( m + 1 ) ... N ) X. { 0 } ) ) / p ]_ B } ) -> -. 2 || ( # ` { s e. ( ( ( 0 ..^ K ) ^m ( 1 ... ( m + 1 ) ) ) X. { f | f : ( 1 ... ( m + 1 ) ) -1-1-onto-> ( 1 ... ( m + 1 ) ) } ) | A. i e. ( 0 ... ( m + 1 ) ) E. j e. ( 0 ... ( m + 1 ) ) i = [_ ( ( ( 1st ` s ) oF + ( ( ( ( 2nd ` s ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` s ) " ( ( j + 1 ) ... ( m + 1 ) ) ) X. { 0 } ) ) ) u. ( ( ( ( m + 1 ) + 1 ) ... N ) X. { 0 } ) ) / p ]_ B } ) ) )
538 537 expcom 
 |-  ( ( m e. NN0 /\ m < N ) -> ( ph -> ( -. 2 || ( # ` { s e. ( ( ( 0 ..^ K ) ^m ( 1 ... m ) ) X. { f | f : ( 1 ... m ) -1-1-onto-> ( 1 ... m ) } ) | A. i e. ( 0 ... m ) E. j e. ( 0 ... m ) i = [_ ( ( ( 1st ` s ) oF + ( ( ( ( 2nd ` s ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` s ) " ( ( j + 1 ) ... m ) ) X. { 0 } ) ) ) u. ( ( ( m + 1 ) ... N ) X. { 0 } ) ) / p ]_ B } ) -> -. 2 || ( # ` { s e. ( ( ( 0 ..^ K ) ^m ( 1 ... ( m + 1 ) ) ) X. { f | f : ( 1 ... ( m + 1 ) ) -1-1-onto-> ( 1 ... ( m + 1 ) ) } ) | A. i e. ( 0 ... ( m + 1 ) ) E. j e. ( 0 ... ( m + 1 ) ) i = [_ ( ( ( 1st ` s ) oF + ( ( ( ( 2nd ` s ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` s ) " ( ( j + 1 ) ... ( m + 1 ) ) ) X. { 0 } ) ) ) u. ( ( ( ( m + 1 ) + 1 ) ... N ) X. { 0 } ) ) / p ]_ B } ) ) ) )
539 538 a2d 
 |-  ( ( m e. NN0 /\ m < N ) -> ( ( ph -> -. 2 || ( # ` { s e. ( ( ( 0 ..^ K ) ^m ( 1 ... m ) ) X. { f | f : ( 1 ... m ) -1-1-onto-> ( 1 ... m ) } ) | A. i e. ( 0 ... m ) E. j e. ( 0 ... m ) i = [_ ( ( ( 1st ` s ) oF + ( ( ( ( 2nd ` s ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` s ) " ( ( j + 1 ) ... m ) ) X. { 0 } ) ) ) u. ( ( ( m + 1 ) ... N ) X. { 0 } ) ) / p ]_ B } ) ) -> ( ph -> -. 2 || ( # ` { s e. ( ( ( 0 ..^ K ) ^m ( 1 ... ( m + 1 ) ) ) X. { f | f : ( 1 ... ( m + 1 ) ) -1-1-onto-> ( 1 ... ( m + 1 ) ) } ) | A. i e. ( 0 ... ( m + 1 ) ) E. j e. ( 0 ... ( m + 1 ) ) i = [_ ( ( ( 1st ` s ) oF + ( ( ( ( 2nd ` s ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` s ) " ( ( j + 1 ) ... ( m + 1 ) ) ) X. { 0 } ) ) ) u. ( ( ( ( m + 1 ) + 1 ) ... N ) X. { 0 } ) ) / p ]_ B } ) ) ) )
540 539 3adant1 
 |-  ( ( N e. NN0 /\ m e. NN0 /\ m < N ) -> ( ( ph -> -. 2 || ( # ` { s e. ( ( ( 0 ..^ K ) ^m ( 1 ... m ) ) X. { f | f : ( 1 ... m ) -1-1-onto-> ( 1 ... m ) } ) | A. i e. ( 0 ... m ) E. j e. ( 0 ... m ) i = [_ ( ( ( 1st ` s ) oF + ( ( ( ( 2nd ` s ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` s ) " ( ( j + 1 ) ... m ) ) X. { 0 } ) ) ) u. ( ( ( m + 1 ) ... N ) X. { 0 } ) ) / p ]_ B } ) ) -> ( ph -> -. 2 || ( # ` { s e. ( ( ( 0 ..^ K ) ^m ( 1 ... ( m + 1 ) ) ) X. { f | f : ( 1 ... ( m + 1 ) ) -1-1-onto-> ( 1 ... ( m + 1 ) ) } ) | A. i e. ( 0 ... ( m + 1 ) ) E. j e. ( 0 ... ( m + 1 ) ) i = [_ ( ( ( 1st ` s ) oF + ( ( ( ( 2nd ` s ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` s ) " ( ( j + 1 ) ... ( m + 1 ) ) ) X. { 0 } ) ) ) u. ( ( ( ( m + 1 ) + 1 ) ... N ) X. { 0 } ) ) / p ]_ B } ) ) ) )
541 112 137 162 187 241 540 fnn0ind 
 |-  ( ( N e. NN0 /\ N e. NN0 /\ N <_ N ) -> ( ph -> -. 2 || ( # ` { s e. ( ( ( 0 ..^ K ) ^m ( 1 ... N ) ) X. { f | f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } ) | A. i e. ( 0 ... N ) E. j e. ( 0 ... N ) i = [_ ( ( ( 1st ` s ) oF + ( ( ( ( 2nd ` s ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` s ) " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) u. ( ( ( N + 1 ) ... N ) X. { 0 } ) ) / p ]_ B } ) ) )
542 10 541 mpcom 
 |-  ( ph -> -. 2 || ( # ` { s e. ( ( ( 0 ..^ K ) ^m ( 1 ... N ) ) X. { f | f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } ) | A. i e. ( 0 ... N ) E. j e. ( 0 ... N ) i = [_ ( ( ( 1st ` s ) oF + ( ( ( ( 2nd ` s ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` s ) " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) u. ( ( ( N + 1 ) ... N ) X. { 0 } ) ) / p ]_ B } ) )
543 dvds0 
 |-  ( 2 e. ZZ -> 2 || 0 )
544 242 543 ax-mp 
 |-  2 || 0
545 hash0 
 |-  ( # ` (/) ) = 0
546 544 545 breqtrri 
 |-  2 || ( # ` (/) )
547 fveq2 
 |-  ( { s e. ( ( ( 0 ..^ K ) ^m ( 1 ... N ) ) X. { f | f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } ) | A. i e. ( 0 ... N ) E. j e. ( 0 ... N ) i = C } = (/) -> ( # ` { s e. ( ( ( 0 ..^ K ) ^m ( 1 ... N ) ) X. { f | f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } ) | A. i e. ( 0 ... N ) E. j e. ( 0 ... N ) i = C } ) = ( # ` (/) ) )
548 546 547 breqtrrid 
 |-  ( { s e. ( ( ( 0 ..^ K ) ^m ( 1 ... N ) ) X. { f | f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } ) | A. i e. ( 0 ... N ) E. j e. ( 0 ... N ) i = C } = (/) -> 2 || ( # ` { s e. ( ( ( 0 ..^ K ) ^m ( 1 ... N ) ) X. { f | f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } ) | A. i e. ( 0 ... N ) E. j e. ( 0 ... N ) i = C } ) )
549 8 ltp1d 
 |-  ( ph -> N < ( N + 1 ) )
550 284 peano2zd 
 |-  ( ph -> ( N + 1 ) e. ZZ )
551 fzn 
 |-  ( ( ( N + 1 ) e. ZZ /\ N e. ZZ ) -> ( N < ( N + 1 ) <-> ( ( N + 1 ) ... N ) = (/) ) )
552 550 284 551 syl2anc 
 |-  ( ph -> ( N < ( N + 1 ) <-> ( ( N + 1 ) ... N ) = (/) ) )
553 549 552 mpbid 
 |-  ( ph -> ( ( N + 1 ) ... N ) = (/) )
554 553 xpeq1d 
 |-  ( ph -> ( ( ( N + 1 ) ... N ) X. { 0 } ) = ( (/) X. { 0 } ) )
555 554 91 eqtrdi 
 |-  ( ph -> ( ( ( N + 1 ) ... N ) X. { 0 } ) = (/) )
556 555 uneq2d 
 |-  ( ph -> ( ( ( 1st ` s ) oF + ( ( ( ( 2nd ` s ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` s ) " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) u. ( ( ( N + 1 ) ... N ) X. { 0 } ) ) = ( ( ( 1st ` s ) oF + ( ( ( ( 2nd ` s ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` s ) " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) u. (/) ) )
557 un0 
 |-  ( ( ( 1st ` s ) oF + ( ( ( ( 2nd ` s ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` s ) " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) u. (/) ) = ( ( 1st ` s ) oF + ( ( ( ( 2nd ` s ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` s ) " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) )
558 556 557 eqtrdi 
 |-  ( ph -> ( ( ( 1st ` s ) oF + ( ( ( ( 2nd ` s ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` s ) " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) u. ( ( ( N + 1 ) ... N ) X. { 0 } ) ) = ( ( 1st ` s ) oF + ( ( ( ( 2nd ` s ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` s ) " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) )
559 558 csbeq1d 
 |-  ( ph -> [_ ( ( ( 1st ` s ) oF + ( ( ( ( 2nd ` s ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` s ) " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) u. ( ( ( N + 1 ) ... N ) X. { 0 } ) ) / p ]_ B = [_ ( ( 1st ` s ) oF + ( ( ( ( 2nd ` s ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` s ) " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) / p ]_ B )
560 ovex 
 |-  ( ( 1st ` s ) oF + ( ( ( ( 2nd ` s ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` s ) " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) e. _V
561 560 2 csbie 
 |-  [_ ( ( 1st ` s ) oF + ( ( ( ( 2nd ` s ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` s ) " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) / p ]_ B = C
562 559 561 eqtrdi 
 |-  ( ph -> [_ ( ( ( 1st ` s ) oF + ( ( ( ( 2nd ` s ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` s ) " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) u. ( ( ( N + 1 ) ... N ) X. { 0 } ) ) / p ]_ B = C )
563 562 eqeq2d 
 |-  ( ph -> ( i = [_ ( ( ( 1st ` s ) oF + ( ( ( ( 2nd ` s ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` s ) " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) u. ( ( ( N + 1 ) ... N ) X. { 0 } ) ) / p ]_ B <-> i = C ) )
564 563 rexbidv 
 |-  ( ph -> ( E. j e. ( 0 ... N ) i = [_ ( ( ( 1st ` s ) oF + ( ( ( ( 2nd ` s ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` s ) " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) u. ( ( ( N + 1 ) ... N ) X. { 0 } ) ) / p ]_ B <-> E. j e. ( 0 ... N ) i = C ) )
565 564 ralbidv 
 |-  ( ph -> ( A. i e. ( 0 ... N ) E. j e. ( 0 ... N ) i = [_ ( ( ( 1st ` s ) oF + ( ( ( ( 2nd ` s ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` s ) " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) u. ( ( ( N + 1 ) ... N ) X. { 0 } ) ) / p ]_ B <-> A. i e. ( 0 ... N ) E. j e. ( 0 ... N ) i = C ) )
566 565 rabbidv 
 |-  ( ph -> { s e. ( ( ( 0 ..^ K ) ^m ( 1 ... N ) ) X. { f | f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } ) | A. i e. ( 0 ... N ) E. j e. ( 0 ... N ) i = [_ ( ( ( 1st ` s ) oF + ( ( ( ( 2nd ` s ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` s ) " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) u. ( ( ( N + 1 ) ... N ) X. { 0 } ) ) / p ]_ B } = { s e. ( ( ( 0 ..^ K ) ^m ( 1 ... N ) ) X. { f | f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } ) | A. i e. ( 0 ... N ) E. j e. ( 0 ... N ) i = C } )
567 566 fveq2d 
 |-  ( ph -> ( # ` { s e. ( ( ( 0 ..^ K ) ^m ( 1 ... N ) ) X. { f | f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } ) | A. i e. ( 0 ... N ) E. j e. ( 0 ... N ) i = [_ ( ( ( 1st ` s ) oF + ( ( ( ( 2nd ` s ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` s ) " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) u. ( ( ( N + 1 ) ... N ) X. { 0 } ) ) / p ]_ B } ) = ( # ` { s e. ( ( ( 0 ..^ K ) ^m ( 1 ... N ) ) X. { f | f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } ) | A. i e. ( 0 ... N ) E. j e. ( 0 ... N ) i = C } ) )
568 567 breq2d 
 |-  ( ph -> ( 2 || ( # ` { s e. ( ( ( 0 ..^ K ) ^m ( 1 ... N ) ) X. { f | f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } ) | A. i e. ( 0 ... N ) E. j e. ( 0 ... N ) i = [_ ( ( ( 1st ` s ) oF + ( ( ( ( 2nd ` s ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` s ) " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) u. ( ( ( N + 1 ) ... N ) X. { 0 } ) ) / p ]_ B } ) <-> 2 || ( # ` { s e. ( ( ( 0 ..^ K ) ^m ( 1 ... N ) ) X. { f | f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } ) | A. i e. ( 0 ... N ) E. j e. ( 0 ... N ) i = C } ) ) )
569 548 568 imbitrrid 
 |-  ( ph -> ( { s e. ( ( ( 0 ..^ K ) ^m ( 1 ... N ) ) X. { f | f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } ) | A. i e. ( 0 ... N ) E. j e. ( 0 ... N ) i = C } = (/) -> 2 || ( # ` { s e. ( ( ( 0 ..^ K ) ^m ( 1 ... N ) ) X. { f | f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } ) | A. i e. ( 0 ... N ) E. j e. ( 0 ... N ) i = [_ ( ( ( 1st ` s ) oF + ( ( ( ( 2nd ` s ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` s ) " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) u. ( ( ( N + 1 ) ... N ) X. { 0 } ) ) / p ]_ B } ) ) )
570 569 necon3bd 
 |-  ( ph -> ( -. 2 || ( # ` { s e. ( ( ( 0 ..^ K ) ^m ( 1 ... N ) ) X. { f | f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } ) | A. i e. ( 0 ... N ) E. j e. ( 0 ... N ) i = [_ ( ( ( 1st ` s ) oF + ( ( ( ( 2nd ` s ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` s ) " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) u. ( ( ( N + 1 ) ... N ) X. { 0 } ) ) / p ]_ B } ) -> { s e. ( ( ( 0 ..^ K ) ^m ( 1 ... N ) ) X. { f | f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } ) | A. i e. ( 0 ... N ) E. j e. ( 0 ... N ) i = C } =/= (/) ) )
571 542 570 mpd 
 |-  ( ph -> { s e. ( ( ( 0 ..^ K ) ^m ( 1 ... N ) ) X. { f | f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } ) | A. i e. ( 0 ... N ) E. j e. ( 0 ... N ) i = C } =/= (/) )
572 rabn0 
 |-  ( { s e. ( ( ( 0 ..^ K ) ^m ( 1 ... N ) ) X. { f | f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } ) | A. i e. ( 0 ... N ) E. j e. ( 0 ... N ) i = C } =/= (/) <-> E. s e. ( ( ( 0 ..^ K ) ^m ( 1 ... N ) ) X. { f | f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } ) A. i e. ( 0 ... N ) E. j e. ( 0 ... N ) i = C )
573 571 572 sylib 
 |-  ( ph -> E. s e. ( ( ( 0 ..^ K ) ^m ( 1 ... N ) ) X. { f | f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } ) A. i e. ( 0 ... N ) E. j e. ( 0 ... N ) i = C )