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	syl5eqr	|- ( 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		elfzelz	|- ( [_ ( q u. ( ( ( ( m + 1 ) + 1 ) ... N ) X. { 0 } ) ) / p ]_ B e. ( 0 ... N ) -> [_ ( q u. ( ( ( ( m + 1 ) + 1 ) ... N ) X. { 0 } ) ) / p ]_ B e. ZZ )
402	400 401	syl	|- ( ( ( ( ph /\ m e. NN0 ) /\ q : ( 1 ... ( m + 1 ) ) --> ( 0 ... K ) ) /\ m < N ) -> [_ ( q u. ( ( ( ( m + 1 ) + 1 ) ... N ) X. { 0 } ) ) / p ]_ B e. ZZ )
403	354 402	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 )
404	289	ad3antlr	|- ( ( ( ( ph /\ m e. NN0 ) /\ q : ( 1 ... ( m + 1 ) ) --> ( 0 ... K ) ) /\ ( m + 1 ) < N ) -> ( m + 1 ) e. ZZ )
405		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 ) ) )
406	403 404 405	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 ) ) )
407	398 406	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 ) )
408	350	ad2antlr	|- ( ( ( ph /\ m e. NN0 ) /\ q : ( 1 ... ( m + 1 ) ) --> ( 0 ... K ) ) -> m < ( m + 1 ) )
409		breq2	|- ( ( m + 1 ) = N -> ( m < ( m + 1 ) <-> m < N ) )
410	409	biimpac	|- ( ( m < ( m + 1 ) /\ ( m + 1 ) = N ) -> m < N )
411	408 410	sylan	|- ( ( ( ( ph /\ m e. NN0 ) /\ q : ( 1 ... ( m + 1 ) ) --> ( 0 ... K ) ) /\ ( m + 1 ) = N ) -> m < N )
412		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 )
413	400 412	syl	|- ( ( ( ( ph /\ m e. NN0 ) /\ q : ( 1 ... ( m + 1 ) ) --> ( 0 ... K ) ) /\ m < N ) -> [_ ( q u. ( ( ( ( m + 1 ) + 1 ) ... N ) X. { 0 } ) ) / p ]_ B <_ N )
414	411 413	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 )
415		simpr	|- ( ( ( ( ph /\ m e. NN0 ) /\ q : ( 1 ... ( m + 1 ) ) --> ( 0 ... K ) ) /\ ( m + 1 ) = N ) -> ( m + 1 ) = N )
416	414 415	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 ) )
417	407 416	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 ) )
418	417	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 ) )
419	331 418	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 ) )
420		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 ) ) )
421	322 325 419 420	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 ) ) )
422		fzss2	|- ( N e. ( ZZ>= ` ( m + 1 ) ) -> ( 1 ... ( m + 1 ) ) C_ ( 1 ... N ) )
423	293 422	syl	|- ( ( ph /\ ( m e. NN0 /\ m < N ) ) -> ( 1 ... ( m + 1 ) ) C_ ( 1 ... N ) )
424	423	sselda	|- ( ( ( ph /\ ( m e. NN0 /\ m < N ) ) /\ n e. ( 1 ... ( m + 1 ) ) ) -> n e. ( 1 ... N ) )
425	424	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 ) )
426	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 ) )
427	360	ad2antll	|- ( ( ( ph /\ m e. NN0 ) /\ ( n e. ( 1 ... ( m + 1 ) ) /\ q : ( 1 ... ( m + 1 ) ) --> ( 0 ... K ) ) ) -> q Fn ( 1 ... ( m + 1 ) ) )
428	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 ) ) = (/) )
429		simprl	|- ( ( ( ph /\ m e. NN0 ) /\ ( n e. ( 1 ... ( m + 1 ) ) /\ q : ( 1 ... ( m + 1 ) ) --> ( 0 ... K ) ) ) -> n e. ( 1 ... ( m + 1 ) ) )
430		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 ) )
431	371 430	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 ) )
432	427 428 429 431	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 ) )
433	432	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 ) )
434	433	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 ) )
435		simpr3	|- ( ( ( ph /\ ( m e. NN0 /\ m < N ) ) /\ ( n e. ( 1 ... ( m + 1 ) ) /\ q : ( 1 ... ( m + 1 ) ) --> ( 0 ... K ) /\ ( q ` n ) = 0 ) ) -> ( q ` n ) = 0 )
436	434 435	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 )
437	425 426 436	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 ) )
438		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 ) )
439		nfcv	|- F/_ p n
440	306 379 439	nfbr	|- F/ p [_ ( q u. ( ( ( ( m + 1 ) + 1 ) ... N ) X. { 0 } ) ) / p ]_ B < n
441	438 440	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 )
442		fveq1	|- ( p = ( q u. ( ( ( ( m + 1 ) + 1 ) ... N ) X. { 0 } ) ) -> ( p ` n ) = ( ( q u. ( ( ( ( m + 1 ) + 1 ) ... N ) X. { 0 } ) ) ` n ) )
443	442	eqeq1d	|- ( p = ( q u. ( ( ( ( m + 1 ) + 1 ) ... N ) X. { 0 } ) ) -> ( ( p ` n ) = 0 <-> ( ( q u. ( ( ( ( m + 1 ) + 1 ) ... N ) X. { 0 } ) ) ` n ) = 0 ) )
444	313 443	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 ) ) )
445	444	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 ) ) ) )
446	315	breq1d	|- ( p = ( q u. ( ( ( ( m + 1 ) + 1 ) ... N ) X. { 0 } ) ) -> ( B < n <-> [_ ( q u. ( ( ( ( m + 1 ) + 1 ) ... N ) X. { 0 } ) ) / p ]_ B < n ) )
447	445 446	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 ) ) )
448	441 312 447 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 )
449	448	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 )
450	437 449	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 )
451		simp1	|- ( ( n e. ( 1 ... ( m + 1 ) ) /\ q : ( 1 ... ( m + 1 ) ) --> ( 0 ... K ) /\ ( q ` n ) = K ) -> n e. ( 1 ... ( m + 1 ) ) )
452	424	anasss	|- ( ( ph /\ ( ( m e. NN0 /\ m < N ) /\ n e. ( 1 ... ( m + 1 ) ) ) ) -> n e. ( 1 ... N ) )
453	451 452	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 ) )
454		simp2	|- ( ( n e. ( 1 ... ( m + 1 ) ) /\ q : ( 1 ... ( m + 1 ) ) --> ( 0 ... K ) /\ ( q ` n ) = K ) -> q : ( 1 ... ( m + 1 ) ) --> ( 0 ... K ) )
455	454 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 ) )
456	432	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 ) )
457		simpr3	|- ( ( ( ph /\ m e. NN0 ) /\ ( n e. ( 1 ... ( m + 1 ) ) /\ q : ( 1 ... ( m + 1 ) ) --> ( 0 ... K ) /\ ( q ` n ) = K ) ) -> ( q ` n ) = K )
458	456 457	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 )
459	458	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 )
460	459	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 )
461	453 455 460	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 ) )
462		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 ) )
463		nfcv	|- F/_ p ( n - 1 )
464	306 463	nfne	|- F/ p [_ ( q u. ( ( ( ( m + 1 ) + 1 ) ... N ) X. { 0 } ) ) / p ]_ B =/= ( n - 1 )
465	462 464	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 ) )
466	442	eqeq1d	|- ( p = ( q u. ( ( ( ( m + 1 ) + 1 ) ... N ) X. { 0 } ) ) -> ( ( p ` n ) = K <-> ( ( q u. ( ( ( ( m + 1 ) + 1 ) ... N ) X. { 0 } ) ) ` n ) = K ) )
467	313 466	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 ) ) )
468	467	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 ) ) ) )
469	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 ) ) )
470	468 469	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 ) ) ) )
471	465 312 470 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 ) )
472	461 471	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 ) )
473	472	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 ) )
474	267 269 421 450 473	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 ) ) } ) ) )
475	267 269 421	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 } ) ) )
476		fzfi	|- ( 0 ... ( m + 1 ) ) e. Fin
477		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 )
478	256 476 477	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
479		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 )
480		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 )
481	478 479 480	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
482	481	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
483		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 )
484	482 264 483	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
485		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 )
486	482 260 485	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
487		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 } ) ) ) ) )
488	242 484 486 487	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 } ) ) ) )
489	474 475 488	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 } ) ) ) )
490	481	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
491	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
492	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
493		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 ) ) } ) ) )
494	490 491 492 493	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 ) ) } ) )
495	489 494	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 ) ) } ) ) )
496		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 ) ) } ) ) )
497	265 495 496	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 ) ) } ) ) )
498		nn0cn	|- ( m e. NN0 -> m e. CC )
499		pncan1	|- ( m e. CC -> ( ( m + 1 ) - 1 ) = m )
500	498 499	syl	|- ( m e. NN0 -> ( ( m + 1 ) - 1 ) = m )
501	500	oveq2d	|- ( m e. NN0 -> ( 0 ... ( ( m + 1 ) - 1 ) ) = ( 0 ... m ) )
502	501	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 ) )
503	501 502	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 ) )
504	503	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 ) ) ) )
505	504	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 ) ) } )
506	505	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 ) ) } ) )
507	506	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 ) ) } ) )
508	1	adantr	|- ( ( ph /\ ( m e. NN0 /\ m < N ) ) -> N e. NN )
509	6	adantr	|- ( ( ph /\ ( m e. NN0 /\ m < N ) ) -> K e. NN )
510		simprl	|- ( ( ph /\ ( m e. NN0 /\ m < N ) ) -> m e. NN0 )
511		simprr	|- ( ( ph /\ ( m e. NN0 /\ m < N ) ) -> m < N )
512	508 509 510 511	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 ) ) } )
513		fzfi	|- ( 1 ... m ) e. Fin
514		mapfi	|- ( ( ( 0 ..^ K ) e. Fin /\ ( 1 ... m ) e. Fin ) -> ( ( 0 ..^ K ) ^m ( 1 ... m ) ) e. Fin )
515	15 513 514	mp2an	|- ( ( 0 ..^ K ) ^m ( 1 ... m ) ) e. Fin
516		ovex	|- ( 1 ... m ) e. _V
517	516 516	mapval	|- ( ( 1 ... m ) ^m ( 1 ... m ) ) = { f | f : ( 1 ... m ) --> ( 1 ... m ) }
518		mapfi	|- ( ( ( 1 ... m ) e. Fin /\ ( 1 ... m ) e. Fin ) -> ( ( 1 ... m ) ^m ( 1 ... m ) ) e. Fin )
519	513 513 518	mp2an	|- ( ( 1 ... m ) ^m ( 1 ... m ) ) e. Fin
520	517 519	eqeltrri	|- { f | f : ( 1 ... m ) --> ( 1 ... m ) } e. Fin
521		f1of	|- ( f : ( 1 ... m ) -1-1-onto-> ( 1 ... m ) -> f : ( 1 ... m ) --> ( 1 ... m ) )
522	521	ss2abi	|- { f | f : ( 1 ... m ) -1-1-onto-> ( 1 ... m ) } C_ { f | f : ( 1 ... m ) --> ( 1 ... m ) }
523		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 )
524	520 522 523	mp2an	|- { f | f : ( 1 ... m ) -1-1-onto-> ( 1 ... m ) } e. Fin
525		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 )
526	515 524 525	mp2an	|- ( ( ( 0 ..^ K ) ^m ( 1 ... m ) ) X. { f | f : ( 1 ... m ) -1-1-onto-> ( 1 ... m ) } ) e. Fin
527		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 )
528	526 527	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
529		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 )
530	256 529	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
531		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 ) ) } ) )
532	528 530 531	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 ) ) } )
533	512 532	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 ) ) } ) )
534	507 533	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 } ) )
535	534	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 } ) ) )
536	497 535	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 } ) ) )
537	536	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 } ) ) )
538	537	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 } ) ) )
539	538	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 } ) ) ) )
540	539	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 } ) ) ) )
541	540	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 } ) ) ) )
542	112 137 162 187 241 541	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 } ) ) )
543	10 542	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 } ) )
544		dvds0	|- ( 2 e. ZZ -> 2 || 0 )
545	242 544	ax-mp	|- 2 || 0
546		hash0	|- ( # ` (/) ) = 0
547	545 546	breqtrri	|- 2 || ( # ` (/) )
548		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 } ) = ( # ` (/) ) )
549	547 548	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 } ) )
550	8	ltp1d	|- ( ph -> N < ( N + 1 ) )
551	284	peano2zd	|- ( ph -> ( N + 1 ) e. ZZ )
552		fzn	|- ( ( ( N + 1 ) e. ZZ /\ N e. ZZ ) -> ( N < ( N + 1 ) <-> ( ( N + 1 ) ... N ) = (/) ) )
553	551 284 552	syl2anc	|- ( ph -> ( N < ( N + 1 ) <-> ( ( N + 1 ) ... N ) = (/) ) )
554	550 553	mpbid	|- ( ph -> ( ( N + 1 ) ... N ) = (/) )
555	554	xpeq1d	|- ( ph -> ( ( ( N + 1 ) ... N ) X. { 0 } ) = ( (/) X. { 0 } ) )
556	555 91	eqtrdi	|- ( ph -> ( ( ( N + 1 ) ... N ) X. { 0 } ) = (/) )
557	556	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. (/) ) )
558		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 } ) ) )
559	557 558	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 } ) ) ) )
560	559	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 )
561		ovex	|- ( ( 1st ` s ) oF + ( ( ( ( 2nd ` s ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` s ) " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) e. _V
562	561 2	csbie	|- [_ ( ( 1st ` s ) oF + ( ( ( ( 2nd ` s ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` s ) " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) / p ]_ B = C
563	560 562	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 )
564	563	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 ) )
565	564	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 ) )
566	565	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 ) )
567	566	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 } )
568	567	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 } ) )
569	568	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 } ) ) )
570	549 569	syl5ibr	|- ( 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 } ) ) )
571	570	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 } =/= (/) ) )
572	543 571	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 } =/= (/) )
573		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 )
574	572 573	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 )