Metamath Proof Explorer


Theorem poimirlem27

Description: Lemma for poimir showing that the difference between admissible faces in the whole cube and admissible faces on the back face is even. Equation (7) of Kulpa p. 548. (Contributed by Brendan Leahy, 21-Aug-2020)

Ref Expression
Hypotheses poimir.0 φ N
poimirlem28.1 p = 1 st s + f 2 nd s 1 j × 1 2 nd s j + 1 N × 0 B = C
poimirlem28.2 φ p : 1 N 0 K B 0 N
poimirlem28.3 φ n 1 N p : 1 N 0 K p n = 0 B < n
poimirlem28.4 φ n 1 N p : 1 N 0 K p n = K B n 1
Assertion poimirlem27 φ 2 t 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N × 0 N | i 0 N 1 j 0 N 2 nd t i = 1 st t / s C s 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N | i 0 N 1 j 0 N 1 i = C 1 st s N = 0 2 nd s N = N

Proof

Step Hyp Ref Expression
1 poimir.0 φ N
2 poimirlem28.1 p = 1 st s + f 2 nd s 1 j × 1 2 nd s j + 1 N × 0 B = C
3 poimirlem28.2 φ p : 1 N 0 K B 0 N
4 poimirlem28.3 φ n 1 N p : 1 N 0 K p n = 0 B < n
5 poimirlem28.4 φ n 1 N p : 1 N 0 K p n = K B n 1
6 fzfi 0 K Fin
7 fzfi 1 N Fin
8 mapfi 0 K Fin 1 N Fin 0 K 1 N Fin
9 6 7 8 mp2an 0 K 1 N Fin
10 fzfi 0 N 1 Fin
11 mapfi 0 K 1 N Fin 0 N 1 Fin 0 K 1 N 0 N 1 Fin
12 9 10 11 mp2an 0 K 1 N 0 N 1 Fin
13 12 a1i φ 0 K 1 N 0 N 1 Fin
14 2z 2
15 14 a1i φ 2
16 fzofi 0 ..^ K Fin
17 mapfi 0 ..^ K Fin 1 N Fin 0 ..^ K 1 N Fin
18 16 7 17 mp2an 0 ..^ K 1 N Fin
19 mapfi 1 N Fin 1 N Fin 1 N 1 N Fin
20 7 7 19 mp2an 1 N 1 N Fin
21 f1of f : 1 N 1-1 onto 1 N f : 1 N 1 N
22 21 ss2abi f | f : 1 N 1-1 onto 1 N f | f : 1 N 1 N
23 ovex 1 N V
24 23 23 mapval 1 N 1 N = f | f : 1 N 1 N
25 22 24 sseqtrri f | f : 1 N 1-1 onto 1 N 1 N 1 N
26 ssfi 1 N 1 N Fin f | f : 1 N 1-1 onto 1 N 1 N 1 N f | f : 1 N 1-1 onto 1 N Fin
27 20 25 26 mp2an f | f : 1 N 1-1 onto 1 N Fin
28 xpfi 0 ..^ K 1 N Fin f | f : 1 N 1-1 onto 1 N Fin 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N Fin
29 18 27 28 mp2an 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N Fin
30 fzfi 0 N Fin
31 xpfi 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N Fin 0 N Fin 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N × 0 N Fin
32 29 30 31 mp2an 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N × 0 N Fin
33 rabfi 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N × 0 N Fin t 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N × 0 N | x = y 0 N 1 if y < 2 nd t y y + 1 / j 1 st 1 st t + f 2 nd 1 st t 1 j × 1 2 nd 1 st t j + 1 N × 0 0 N 1 ran p ran x B n 1 N p ran x p n 0 p ran x p n K Fin
34 32 33 ax-mp t 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N × 0 N | x = y 0 N 1 if y < 2 nd t y y + 1 / j 1 st 1 st t + f 2 nd 1 st t 1 j × 1 2 nd 1 st t j + 1 N × 0 0 N 1 ran p ran x B n 1 N p ran x p n 0 p ran x p n K Fin
35 hashcl t 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N × 0 N | x = y 0 N 1 if y < 2 nd t y y + 1 / j 1 st 1 st t + f 2 nd 1 st t 1 j × 1 2 nd 1 st t j + 1 N × 0 0 N 1 ran p ran x B n 1 N p ran x p n 0 p ran x p n K Fin t 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N × 0 N | x = y 0 N 1 if y < 2 nd t y y + 1 / j 1 st 1 st t + f 2 nd 1 st t 1 j × 1 2 nd 1 st t j + 1 N × 0 0 N 1 ran p ran x B n 1 N p ran x p n 0 p ran x p n K 0
36 35 nn0zd t 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N × 0 N | x = y 0 N 1 if y < 2 nd t y y + 1 / j 1 st 1 st t + f 2 nd 1 st t 1 j × 1 2 nd 1 st t j + 1 N × 0 0 N 1 ran p ran x B n 1 N p ran x p n 0 p ran x p n K Fin t 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N × 0 N | x = y 0 N 1 if y < 2 nd t y y + 1 / j 1 st 1 st t + f 2 nd 1 st t 1 j × 1 2 nd 1 st t j + 1 N × 0 0 N 1 ran p ran x B n 1 N p ran x p n 0 p ran x p n K
37 34 36 mp1i φ x 0 K 1 N 0 N 1 t 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N × 0 N | x = y 0 N 1 if y < 2 nd t y y + 1 / j 1 st 1 st t + f 2 nd 1 st t 1 j × 1 2 nd 1 st t j + 1 N × 0 0 N 1 ran p ran x B n 1 N p ran x p n 0 p ran x p n K
38 dfrex2 t 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N × 0 N 0 N 1 ran p ran x B n 1 N p ran x p n 0 p ran x p n K ¬ t 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N × 0 N ¬ 0 N 1 ran p ran x B n 1 N p ran x p n 0 p ran x p n K
39 nfv t φ x 0 K 1 N 0 N 1
40 nfcv _ t 2
41 nfcv _ t
42 nfcv _ t .
43 nfrab1 _ t t 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N × 0 N | x = y 0 N 1 if y < 2 nd t y y + 1 / j 1 st 1 st t + f 2 nd 1 st t 1 j × 1 2 nd 1 st t j + 1 N × 0 0 N 1 ran p ran x B n 1 N p ran x p n 0 p ran x p n K
44 42 43 nffv _ t t 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N × 0 N | x = y 0 N 1 if y < 2 nd t y y + 1 / j 1 st 1 st t + f 2 nd 1 st t 1 j × 1 2 nd 1 st t j + 1 N × 0 0 N 1 ran p ran x B n 1 N p ran x p n 0 p ran x p n K
45 40 41 44 nfbr t 2 t 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N × 0 N | x = y 0 N 1 if y < 2 nd t y y + 1 / j 1 st 1 st t + f 2 nd 1 st t 1 j × 1 2 nd 1 st t j + 1 N × 0 0 N 1 ran p ran x B n 1 N p ran x p n 0 p ran x p n K
46 neq0 ¬ t 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N × 0 N | x = y 0 N 1 if y < 2 nd t y y + 1 / j 1 st 1 st t + f 2 nd 1 st t 1 j × 1 2 nd 1 st t j + 1 N × 0 = s s t 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N × 0 N | x = y 0 N 1 if y < 2 nd t y y + 1 / j 1 st 1 st t + f 2 nd 1 st t 1 j × 1 2 nd 1 st t j + 1 N × 0
47 iddvds 2 2 2
48 14 47 ax-mp 2 2
49 vex s V
50 hashsng s V s = 1
51 49 50 ax-mp s = 1
52 51 oveq2i 1 + s = 1 + 1
53 df-2 2 = 1 + 1
54 52 53 eqtr4i 1 + s = 2
55 48 54 breqtrri 2 1 + s
56 rabfi 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N × 0 N Fin t 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N × 0 N | x = y 0 N 1 if y < 2 nd t y y + 1 / j 1 st 1 st t + f 2 nd 1 st t 1 j × 1 2 nd 1 st t j + 1 N × 0 Fin
57 diffi t 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N × 0 N | x = y 0 N 1 if y < 2 nd t y y + 1 / j 1 st 1 st t + f 2 nd 1 st t 1 j × 1 2 nd 1 st t j + 1 N × 0 Fin t 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N × 0 N | x = y 0 N 1 if y < 2 nd t y y + 1 / j 1 st 1 st t + f 2 nd 1 st t 1 j × 1 2 nd 1 st t j + 1 N × 0 s Fin
58 32 56 57 mp2b t 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N × 0 N | x = y 0 N 1 if y < 2 nd t y y + 1 / j 1 st 1 st t + f 2 nd 1 st t 1 j × 1 2 nd 1 st t j + 1 N × 0 s Fin
59 snfi s Fin
60 disjdifr t 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N × 0 N | x = y 0 N 1 if y < 2 nd t y y + 1 / j 1 st 1 st t + f 2 nd 1 st t 1 j × 1 2 nd 1 st t j + 1 N × 0 s s =
61 hashun t 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N × 0 N | x = y 0 N 1 if y < 2 nd t y y + 1 / j 1 st 1 st t + f 2 nd 1 st t 1 j × 1 2 nd 1 st t j + 1 N × 0 s Fin s Fin t 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N × 0 N | x = y 0 N 1 if y < 2 nd t y y + 1 / j 1 st 1 st t + f 2 nd 1 st t 1 j × 1 2 nd 1 st t j + 1 N × 0 s s = t 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N × 0 N | x = y 0 N 1 if y < 2 nd t y y + 1 / j 1 st 1 st t + f 2 nd 1 st t 1 j × 1 2 nd 1 st t j + 1 N × 0 s s = t 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N × 0 N | x = y 0 N 1 if y < 2 nd t y y + 1 / j 1 st 1 st t + f 2 nd 1 st t 1 j × 1 2 nd 1 st t j + 1 N × 0 s + s
62 58 59 60 61 mp3an t 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N × 0 N | x = y 0 N 1 if y < 2 nd t y y + 1 / j 1 st 1 st t + f 2 nd 1 st t 1 j × 1 2 nd 1 st t j + 1 N × 0 s s = t 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N × 0 N | x = y 0 N 1 if y < 2 nd t y y + 1 / j 1 st 1 st t + f 2 nd 1 st t 1 j × 1 2 nd 1 st t j + 1 N × 0 s + s
63 difsnid s t 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N × 0 N | x = y 0 N 1 if y < 2 nd t y y + 1 / j 1 st 1 st t + f 2 nd 1 st t 1 j × 1 2 nd 1 st t j + 1 N × 0 t 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N × 0 N | x = y 0 N 1 if y < 2 nd t y y + 1 / j 1 st 1 st t + f 2 nd 1 st t 1 j × 1 2 nd 1 st t j + 1 N × 0 s s = t 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N × 0 N | x = y 0 N 1 if y < 2 nd t y y + 1 / j 1 st 1 st t + f 2 nd 1 st t 1 j × 1 2 nd 1 st t j + 1 N × 0
64 63 fveq2d s t 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N × 0 N | x = y 0 N 1 if y < 2 nd t y y + 1 / j 1 st 1 st t + f 2 nd 1 st t 1 j × 1 2 nd 1 st t j + 1 N × 0 t 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N × 0 N | x = y 0 N 1 if y < 2 nd t y y + 1 / j 1 st 1 st t + f 2 nd 1 st t 1 j × 1 2 nd 1 st t j + 1 N × 0 s s = t 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N × 0 N | x = y 0 N 1 if y < 2 nd t y y + 1 / j 1 st 1 st t + f 2 nd 1 st t 1 j × 1 2 nd 1 st t j + 1 N × 0
65 62 64 eqtr3id s t 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N × 0 N | x = y 0 N 1 if y < 2 nd t y y + 1 / j 1 st 1 st t + f 2 nd 1 st t 1 j × 1 2 nd 1 st t j + 1 N × 0 t 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N × 0 N | x = y 0 N 1 if y < 2 nd t y y + 1 / j 1 st 1 st t + f 2 nd 1 st t 1 j × 1 2 nd 1 st t j + 1 N × 0 s + s = t 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N × 0 N | x = y 0 N 1 if y < 2 nd t y y + 1 / j 1 st 1 st t + f 2 nd 1 st t 1 j × 1 2 nd 1 st t j + 1 N × 0
66 65 adantl φ x 0 K 1 N 0 N 1 n 1 N p ran x p n 0 p ran x p n K s t 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N × 0 N | x = y 0 N 1 if y < 2 nd t y y + 1 / j 1 st 1 st t + f 2 nd 1 st t 1 j × 1 2 nd 1 st t j + 1 N × 0 t 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N × 0 N | x = y 0 N 1 if y < 2 nd t y y + 1 / j 1 st 1 st t + f 2 nd 1 st t 1 j × 1 2 nd 1 st t j + 1 N × 0 s + s = t 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N × 0 N | x = y 0 N 1 if y < 2 nd t y y + 1 / j 1 st 1 st t + f 2 nd 1 st t 1 j × 1 2 nd 1 st t j + 1 N × 0
67 1 ad3antrrr φ x 0 K 1 N 0 N 1 n 1 N p ran x p n 0 p ran x p n K s t 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N × 0 N | x = y 0 N 1 if y < 2 nd t y y + 1 / j 1 st 1 st t + f 2 nd 1 st t 1 j × 1 2 nd 1 st t j + 1 N × 0 N
68 fveq2 t = u 2 nd t = 2 nd u
69 68 breq2d t = u y < 2 nd t y < 2 nd u
70 69 ifbid t = u if y < 2 nd t y y + 1 = if y < 2 nd u y y + 1
71 70 csbeq1d t = u if y < 2 nd t y y + 1 / j 1 st 1 st t + f 2 nd 1 st t 1 j × 1 2 nd 1 st t j + 1 N × 0 = if y < 2 nd u y y + 1 / j 1 st 1 st t + f 2 nd 1 st t 1 j × 1 2 nd 1 st t j + 1 N × 0
72 2fveq3 t = u 1 st 1 st t = 1 st 1 st u
73 2fveq3 t = u 2 nd 1 st t = 2 nd 1 st u
74 73 imaeq1d t = u 2 nd 1 st t 1 j = 2 nd 1 st u 1 j
75 74 xpeq1d t = u 2 nd 1 st t 1 j × 1 = 2 nd 1 st u 1 j × 1
76 73 imaeq1d t = u 2 nd 1 st t j + 1 N = 2 nd 1 st u j + 1 N
77 76 xpeq1d t = u 2 nd 1 st t j + 1 N × 0 = 2 nd 1 st u j + 1 N × 0
78 75 77 uneq12d t = u 2 nd 1 st t 1 j × 1 2 nd 1 st t j + 1 N × 0 = 2 nd 1 st u 1 j × 1 2 nd 1 st u j + 1 N × 0
79 72 78 oveq12d t = u 1 st 1 st t + f 2 nd 1 st t 1 j × 1 2 nd 1 st t j + 1 N × 0 = 1 st 1 st u + f 2 nd 1 st u 1 j × 1 2 nd 1 st u j + 1 N × 0
80 79 csbeq2dv t = u if y < 2 nd u y y + 1 / j 1 st 1 st t + f 2 nd 1 st t 1 j × 1 2 nd 1 st t j + 1 N × 0 = if y < 2 nd u y y + 1 / j 1 st 1 st u + f 2 nd 1 st u 1 j × 1 2 nd 1 st u j + 1 N × 0
81 71 80 eqtrd t = u if y < 2 nd t y y + 1 / j 1 st 1 st t + f 2 nd 1 st t 1 j × 1 2 nd 1 st t j + 1 N × 0 = if y < 2 nd u y y + 1 / j 1 st 1 st u + f 2 nd 1 st u 1 j × 1 2 nd 1 st u j + 1 N × 0
82 81 mpteq2dv t = u y 0 N 1 if y < 2 nd t y y + 1 / j 1 st 1 st t + f 2 nd 1 st t 1 j × 1 2 nd 1 st t j + 1 N × 0 = y 0 N 1 if y < 2 nd u y y + 1 / j 1 st 1 st u + f 2 nd 1 st u 1 j × 1 2 nd 1 st u j + 1 N × 0
83 breq1 y = w y < 2 nd u w < 2 nd u
84 id y = w y = w
85 oveq1 y = w y + 1 = w + 1
86 83 84 85 ifbieq12d y = w if y < 2 nd u y y + 1 = if w < 2 nd u w w + 1
87 86 csbeq1d y = w if y < 2 nd u y y + 1 / j 1 st 1 st u + f 2 nd 1 st u 1 j × 1 2 nd 1 st u j + 1 N × 0 = if w < 2 nd u w w + 1 / j 1 st 1 st u + f 2 nd 1 st u 1 j × 1 2 nd 1 st u j + 1 N × 0
88 oveq2 j = i 1 j = 1 i
89 88 imaeq2d j = i 2 nd 1 st u 1 j = 2 nd 1 st u 1 i
90 89 xpeq1d j = i 2 nd 1 st u 1 j × 1 = 2 nd 1 st u 1 i × 1
91 oveq1 j = i j + 1 = i + 1
92 91 oveq1d j = i j + 1 N = i + 1 N
93 92 imaeq2d j = i 2 nd 1 st u j + 1 N = 2 nd 1 st u i + 1 N
94 93 xpeq1d j = i 2 nd 1 st u j + 1 N × 0 = 2 nd 1 st u i + 1 N × 0
95 90 94 uneq12d j = i 2 nd 1 st u 1 j × 1 2 nd 1 st u j + 1 N × 0 = 2 nd 1 st u 1 i × 1 2 nd 1 st u i + 1 N × 0
96 95 oveq2d j = i 1 st 1 st u + f 2 nd 1 st u 1 j × 1 2 nd 1 st u j + 1 N × 0 = 1 st 1 st u + f 2 nd 1 st u 1 i × 1 2 nd 1 st u i + 1 N × 0
97 96 cbvcsbv if w < 2 nd u w w + 1 / j 1 st 1 st u + f 2 nd 1 st u 1 j × 1 2 nd 1 st u j + 1 N × 0 = if w < 2 nd u w w + 1 / i 1 st 1 st u + f 2 nd 1 st u 1 i × 1 2 nd 1 st u i + 1 N × 0
98 87 97 eqtrdi y = w if y < 2 nd u y y + 1 / j 1 st 1 st u + f 2 nd 1 st u 1 j × 1 2 nd 1 st u j + 1 N × 0 = if w < 2 nd u w w + 1 / i 1 st 1 st u + f 2 nd 1 st u 1 i × 1 2 nd 1 st u i + 1 N × 0
99 98 cbvmptv y 0 N 1 if y < 2 nd u y y + 1 / j 1 st 1 st u + f 2 nd 1 st u 1 j × 1 2 nd 1 st u j + 1 N × 0 = w 0 N 1 if w < 2 nd u w w + 1 / i 1 st 1 st u + f 2 nd 1 st u 1 i × 1 2 nd 1 st u i + 1 N × 0
100 82 99 eqtrdi t = u y 0 N 1 if y < 2 nd t y y + 1 / j 1 st 1 st t + f 2 nd 1 st t 1 j × 1 2 nd 1 st t j + 1 N × 0 = w 0 N 1 if w < 2 nd u w w + 1 / i 1 st 1 st u + f 2 nd 1 st u 1 i × 1 2 nd 1 st u i + 1 N × 0
101 100 eqeq2d t = u x = y 0 N 1 if y < 2 nd t y y + 1 / j 1 st 1 st t + f 2 nd 1 st t 1 j × 1 2 nd 1 st t j + 1 N × 0 x = w 0 N 1 if w < 2 nd u w w + 1 / i 1 st 1 st u + f 2 nd 1 st u 1 i × 1 2 nd 1 st u i + 1 N × 0
102 101 cbvrabv t 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N × 0 N | x = y 0 N 1 if y < 2 nd t y y + 1 / j 1 st 1 st t + f 2 nd 1 st t 1 j × 1 2 nd 1 st t j + 1 N × 0 = u 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N × 0 N | x = w 0 N 1 if w < 2 nd u w w + 1 / i 1 st 1 st u + f 2 nd 1 st u 1 i × 1 2 nd 1 st u i + 1 N × 0
103 elmapi x 0 K 1 N 0 N 1 x : 0 N 1 0 K 1 N
104 103 ad3antlr φ x 0 K 1 N 0 N 1 n 1 N p ran x p n 0 p ran x p n K s t 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N × 0 N | x = y 0 N 1 if y < 2 nd t y y + 1 / j 1 st 1 st t + f 2 nd 1 st t 1 j × 1 2 nd 1 st t j + 1 N × 0 x : 0 N 1 0 K 1 N
105 simpr φ x 0 K 1 N 0 N 1 n 1 N p ran x p n 0 p ran x p n K s t 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N × 0 N | x = y 0 N 1 if y < 2 nd t y y + 1 / j 1 st 1 st t + f 2 nd 1 st t 1 j × 1 2 nd 1 st t j + 1 N × 0 s t 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N × 0 N | x = y 0 N 1 if y < 2 nd t y y + 1 / j 1 st 1 st t + f 2 nd 1 st t 1 j × 1 2 nd 1 st t j + 1 N × 0
106 simpl p ran x p n 0 p ran x p n K p ran x p n 0
107 106 ralimi n 1 N p ran x p n 0 p ran x p n K n 1 N p ran x p n 0
108 107 ad2antlr φ x 0 K 1 N 0 N 1 n 1 N p ran x p n 0 p ran x p n K s t 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N × 0 N | x = y 0 N 1 if y < 2 nd t y y + 1 / j 1 st 1 st t + f 2 nd 1 st t 1 j × 1 2 nd 1 st t j + 1 N × 0 n 1 N p ran x p n 0
109 fveq2 n = m p n = p m
110 109 neeq1d n = m p n 0 p m 0
111 110 rexbidv n = m p ran x p n 0 p ran x p m 0
112 fveq1 p = q p m = q m
113 112 neeq1d p = q p m 0 q m 0
114 113 cbvrexvw p ran x p m 0 q ran x q m 0
115 111 114 bitrdi n = m p ran x p n 0 q ran x q m 0
116 115 rspccva n 1 N p ran x p n 0 m 1 N q ran x q m 0
117 108 116 sylan φ x 0 K 1 N 0 N 1 n 1 N p ran x p n 0 p ran x p n K s t 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N × 0 N | x = y 0 N 1 if y < 2 nd t y y + 1 / j 1 st 1 st t + f 2 nd 1 st t 1 j × 1 2 nd 1 st t j + 1 N × 0 m 1 N q ran x q m 0
118 simpr p ran x p n 0 p ran x p n K p ran x p n K
119 118 ralimi n 1 N p ran x p n 0 p ran x p n K n 1 N p ran x p n K
120 119 ad2antlr φ x 0 K 1 N 0 N 1 n 1 N p ran x p n 0 p ran x p n K s t 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N × 0 N | x = y 0 N 1 if y < 2 nd t y y + 1 / j 1 st 1 st t + f 2 nd 1 st t 1 j × 1 2 nd 1 st t j + 1 N × 0 n 1 N p ran x p n K
121 109 neeq1d n = m p n K p m K
122 121 rexbidv n = m p ran x p n K p ran x p m K
123 112 neeq1d p = q p m K q m K
124 123 cbvrexvw p ran x p m K q ran x q m K
125 122 124 bitrdi n = m p ran x p n K q ran x q m K
126 125 rspccva n 1 N p ran x p n K m 1 N q ran x q m K
127 120 126 sylan φ x 0 K 1 N 0 N 1 n 1 N p ran x p n 0 p ran x p n K s t 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N × 0 N | x = y 0 N 1 if y < 2 nd t y y + 1 / j 1 st 1 st t + f 2 nd 1 st t 1 j × 1 2 nd 1 st t j + 1 N × 0 m 1 N q ran x q m K
128 67 102 104 105 117 127 poimirlem22 φ x 0 K 1 N 0 N 1 n 1 N p ran x p n 0 p ran x p n K s t 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N × 0 N | x = y 0 N 1 if y < 2 nd t y y + 1 / j 1 st 1 st t + f 2 nd 1 st t 1 j × 1 2 nd 1 st t j + 1 N × 0 ∃! z t 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N × 0 N | x = y 0 N 1 if y < 2 nd t y y + 1 / j 1 st 1 st t + f 2 nd 1 st t 1 j × 1 2 nd 1 st t j + 1 N × 0 z s
129 eldifsn z t 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N × 0 N | x = y 0 N 1 if y < 2 nd t y y + 1 / j 1 st 1 st t + f 2 nd 1 st t 1 j × 1 2 nd 1 st t j + 1 N × 0 s z t 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N × 0 N | x = y 0 N 1 if y < 2 nd t y y + 1 / j 1 st 1 st t + f 2 nd 1 st t 1 j × 1 2 nd 1 st t j + 1 N × 0 z s
130 129 eubii ∃! z z t 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N × 0 N | x = y 0 N 1 if y < 2 nd t y y + 1 / j 1 st 1 st t + f 2 nd 1 st t 1 j × 1 2 nd 1 st t j + 1 N × 0 s ∃! z z t 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N × 0 N | x = y 0 N 1 if y < 2 nd t y y + 1 / j 1 st 1 st t + f 2 nd 1 st t 1 j × 1 2 nd 1 st t j + 1 N × 0 z s
131 58 elexi t 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N × 0 N | x = y 0 N 1 if y < 2 nd t y y + 1 / j 1 st 1 st t + f 2 nd 1 st t 1 j × 1 2 nd 1 st t j + 1 N × 0 s V
132 euhash1 t 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N × 0 N | x = y 0 N 1 if y < 2 nd t y y + 1 / j 1 st 1 st t + f 2 nd 1 st t 1 j × 1 2 nd 1 st t j + 1 N × 0 s V t 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N × 0 N | x = y 0 N 1 if y < 2 nd t y y + 1 / j 1 st 1 st t + f 2 nd 1 st t 1 j × 1 2 nd 1 st t j + 1 N × 0 s = 1 ∃! z z t 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N × 0 N | x = y 0 N 1 if y < 2 nd t y y + 1 / j 1 st 1 st t + f 2 nd 1 st t 1 j × 1 2 nd 1 st t j + 1 N × 0 s
133 131 132 ax-mp t 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N × 0 N | x = y 0 N 1 if y < 2 nd t y y + 1 / j 1 st 1 st t + f 2 nd 1 st t 1 j × 1 2 nd 1 st t j + 1 N × 0 s = 1 ∃! z z t 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N × 0 N | x = y 0 N 1 if y < 2 nd t y y + 1 / j 1 st 1 st t + f 2 nd 1 st t 1 j × 1 2 nd 1 st t j + 1 N × 0 s
134 df-reu ∃! z t 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N × 0 N | x = y 0 N 1 if y < 2 nd t y y + 1 / j 1 st 1 st t + f 2 nd 1 st t 1 j × 1 2 nd 1 st t j + 1 N × 0 z s ∃! z z t 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N × 0 N | x = y 0 N 1 if y < 2 nd t y y + 1 / j 1 st 1 st t + f 2 nd 1 st t 1 j × 1 2 nd 1 st t j + 1 N × 0 z s
135 130 133 134 3bitr4ri ∃! z t 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N × 0 N | x = y 0 N 1 if y < 2 nd t y y + 1 / j 1 st 1 st t + f 2 nd 1 st t 1 j × 1 2 nd 1 st t j + 1 N × 0 z s t 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N × 0 N | x = y 0 N 1 if y < 2 nd t y y + 1 / j 1 st 1 st t + f 2 nd 1 st t 1 j × 1 2 nd 1 st t j + 1 N × 0 s = 1
136 128 135 sylib φ x 0 K 1 N 0 N 1 n 1 N p ran x p n 0 p ran x p n K s t 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N × 0 N | x = y 0 N 1 if y < 2 nd t y y + 1 / j 1 st 1 st t + f 2 nd 1 st t 1 j × 1 2 nd 1 st t j + 1 N × 0 t 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N × 0 N | x = y 0 N 1 if y < 2 nd t y y + 1 / j 1 st 1 st t + f 2 nd 1 st t 1 j × 1 2 nd 1 st t j + 1 N × 0 s = 1
137 136 oveq1d φ x 0 K 1 N 0 N 1 n 1 N p ran x p n 0 p ran x p n K s t 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N × 0 N | x = y 0 N 1 if y < 2 nd t y y + 1 / j 1 st 1 st t + f 2 nd 1 st t 1 j × 1 2 nd 1 st t j + 1 N × 0 t 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N × 0 N | x = y 0 N 1 if y < 2 nd t y y + 1 / j 1 st 1 st t + f 2 nd 1 st t 1 j × 1 2 nd 1 st t j + 1 N × 0 s + s = 1 + s
138 66 137 eqtr3d φ x 0 K 1 N 0 N 1 n 1 N p ran x p n 0 p ran x p n K s t 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N × 0 N | x = y 0 N 1 if y < 2 nd t y y + 1 / j 1 st 1 st t + f 2 nd 1 st t 1 j × 1 2 nd 1 st t j + 1 N × 0 t 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N × 0 N | x = y 0 N 1 if y < 2 nd t y y + 1 / j 1 st 1 st t + f 2 nd 1 st t 1 j × 1 2 nd 1 st t j + 1 N × 0 = 1 + s
139 55 138 breqtrrid φ x 0 K 1 N 0 N 1 n 1 N p ran x p n 0 p ran x p n K s t 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N × 0 N | x = y 0 N 1 if y < 2 nd t y y + 1 / j 1 st 1 st t + f 2 nd 1 st t 1 j × 1 2 nd 1 st t j + 1 N × 0 2 t 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N × 0 N | x = y 0 N 1 if y < 2 nd t y y + 1 / j 1 st 1 st t + f 2 nd 1 st t 1 j × 1 2 nd 1 st t j + 1 N × 0
140 139 ex φ x 0 K 1 N 0 N 1 n 1 N p ran x p n 0 p ran x p n K s t 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N × 0 N | x = y 0 N 1 if y < 2 nd t y y + 1 / j 1 st 1 st t + f 2 nd 1 st t 1 j × 1 2 nd 1 st t j + 1 N × 0 2 t 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N × 0 N | x = y 0 N 1 if y < 2 nd t y y + 1 / j 1 st 1 st t + f 2 nd 1 st t 1 j × 1 2 nd 1 st t j + 1 N × 0
141 140 exlimdv φ x 0 K 1 N 0 N 1 n 1 N p ran x p n 0 p ran x p n K s s t 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N × 0 N | x = y 0 N 1 if y < 2 nd t y y + 1 / j 1 st 1 st t + f 2 nd 1 st t 1 j × 1 2 nd 1 st t j + 1 N × 0 2 t 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N × 0 N | x = y 0 N 1 if y < 2 nd t y y + 1 / j 1 st 1 st t + f 2 nd 1 st t 1 j × 1 2 nd 1 st t j + 1 N × 0
142 46 141 biimtrid φ x 0 K 1 N 0 N 1 n 1 N p ran x p n 0 p ran x p n K ¬ t 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N × 0 N | x = y 0 N 1 if y < 2 nd t y y + 1 / j 1 st 1 st t + f 2 nd 1 st t 1 j × 1 2 nd 1 st t j + 1 N × 0 = 2 t 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N × 0 N | x = y 0 N 1 if y < 2 nd t y y + 1 / j 1 st 1 st t + f 2 nd 1 st t 1 j × 1 2 nd 1 st t j + 1 N × 0
143 dvds0 2 2 0
144 14 143 ax-mp 2 0
145 hash0 = 0
146 144 145 breqtrri 2
147 fveq2 t 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N × 0 N | x = y 0 N 1 if y < 2 nd t y y + 1 / j 1 st 1 st t + f 2 nd 1 st t 1 j × 1 2 nd 1 st t j + 1 N × 0 = t 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N × 0 N | x = y 0 N 1 if y < 2 nd t y y + 1 / j 1 st 1 st t + f 2 nd 1 st t 1 j × 1 2 nd 1 st t j + 1 N × 0 =
148 146 147 breqtrrid t 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N × 0 N | x = y 0 N 1 if y < 2 nd t y y + 1 / j 1 st 1 st t + f 2 nd 1 st t 1 j × 1 2 nd 1 st t j + 1 N × 0 = 2 t 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N × 0 N | x = y 0 N 1 if y < 2 nd t y y + 1 / j 1 st 1 st t + f 2 nd 1 st t 1 j × 1 2 nd 1 st t j + 1 N × 0
149 142 148 pm2.61d2 φ x 0 K 1 N 0 N 1 n 1 N p ran x p n 0 p ran x p n K 2 t 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N × 0 N | x = y 0 N 1 if y < 2 nd t y y + 1 / j 1 st 1 st t + f 2 nd 1 st t 1 j × 1 2 nd 1 st t j + 1 N × 0
150 149 ex φ x 0 K 1 N 0 N 1 n 1 N p ran x p n 0 p ran x p n K 2 t 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N × 0 N | x = y 0 N 1 if y < 2 nd t y y + 1 / j 1 st 1 st t + f 2 nd 1 st t 1 j × 1 2 nd 1 st t j + 1 N × 0
151 150 adantld φ x 0 K 1 N 0 N 1 0 N 1 ran p ran x B n 1 N p ran x p n 0 p ran x p n K 2 t 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N × 0 N | x = y 0 N 1 if y < 2 nd t y y + 1 / j 1 st 1 st t + f 2 nd 1 st t 1 j × 1 2 nd 1 st t j + 1 N × 0
152 iba 0 N 1 ran p ran x B n 1 N p ran x p n 0 p ran x p n K x = y 0 N 1 if y < 2 nd t y y + 1 / j 1 st 1 st t + f 2 nd 1 st t 1 j × 1 2 nd 1 st t j + 1 N × 0 x = y 0 N 1 if y < 2 nd t y y + 1 / j 1 st 1 st t + f 2 nd 1 st t 1 j × 1 2 nd 1 st t j + 1 N × 0 0 N 1 ran p ran x B n 1 N p ran x p n 0 p ran x p n K
153 152 rabbidv 0 N 1 ran p ran x B n 1 N p ran x p n 0 p ran x p n K t 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N × 0 N | x = y 0 N 1 if y < 2 nd t y y + 1 / j 1 st 1 st t + f 2 nd 1 st t 1 j × 1 2 nd 1 st t j + 1 N × 0 = t 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N × 0 N | x = y 0 N 1 if y < 2 nd t y y + 1 / j 1 st 1 st t + f 2 nd 1 st t 1 j × 1 2 nd 1 st t j + 1 N × 0 0 N 1 ran p ran x B n 1 N p ran x p n 0 p ran x p n K
154 153 fveq2d 0 N 1 ran p ran x B n 1 N p ran x p n 0 p ran x p n K t 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N × 0 N | x = y 0 N 1 if y < 2 nd t y y + 1 / j 1 st 1 st t + f 2 nd 1 st t 1 j × 1 2 nd 1 st t j + 1 N × 0 = t 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N × 0 N | x = y 0 N 1 if y < 2 nd t y y + 1 / j 1 st 1 st t + f 2 nd 1 st t 1 j × 1 2 nd 1 st t j + 1 N × 0 0 N 1 ran p ran x B n 1 N p ran x p n 0 p ran x p n K
155 154 breq2d 0 N 1 ran p ran x B n 1 N p ran x p n 0 p ran x p n K 2 t 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N × 0 N | x = y 0 N 1 if y < 2 nd t y y + 1 / j 1 st 1 st t + f 2 nd 1 st t 1 j × 1 2 nd 1 st t j + 1 N × 0 2 t 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N × 0 N | x = y 0 N 1 if y < 2 nd t y y + 1 / j 1 st 1 st t + f 2 nd 1 st t 1 j × 1 2 nd 1 st t j + 1 N × 0 0 N 1 ran p ran x B n 1 N p ran x p n 0 p ran x p n K
156 151 155 mpbidi φ x 0 K 1 N 0 N 1 0 N 1 ran p ran x B n 1 N p ran x p n 0 p ran x p n K 2 t 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N × 0 N | x = y 0 N 1 if y < 2 nd t y y + 1 / j 1 st 1 st t + f 2 nd 1 st t 1 j × 1 2 nd 1 st t j + 1 N × 0 0 N 1 ran p ran x B n 1 N p ran x p n 0 p ran x p n K
157 156 a1d φ x 0 K 1 N 0 N 1 t 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N × 0 N 0 N 1 ran p ran x B n 1 N p ran x p n 0 p ran x p n K 2 t 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N × 0 N | x = y 0 N 1 if y < 2 nd t y y + 1 / j 1 st 1 st t + f 2 nd 1 st t 1 j × 1 2 nd 1 st t j + 1 N × 0 0 N 1 ran p ran x B n 1 N p ran x p n 0 p ran x p n K
158 39 45 157 rexlimd φ x 0 K 1 N 0 N 1 t 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N × 0 N 0 N 1 ran p ran x B n 1 N p ran x p n 0 p ran x p n K 2 t 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N × 0 N | x = y 0 N 1 if y < 2 nd t y y + 1 / j 1 st 1 st t + f 2 nd 1 st t 1 j × 1 2 nd 1 st t j + 1 N × 0 0 N 1 ran p ran x B n 1 N p ran x p n 0 p ran x p n K
159 38 158 biimtrrid φ x 0 K 1 N 0 N 1 ¬ t 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N × 0 N ¬ 0 N 1 ran p ran x B n 1 N p ran x p n 0 p ran x p n K 2 t 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N × 0 N | x = y 0 N 1 if y < 2 nd t y y + 1 / j 1 st 1 st t + f 2 nd 1 st t 1 j × 1 2 nd 1 st t j + 1 N × 0 0 N 1 ran p ran x B n 1 N p ran x p n 0 p ran x p n K
160 simpr x = y 0 N 1 if y < 2 nd t y y + 1 / j 1 st 1 st t + f 2 nd 1 st t 1 j × 1 2 nd 1 st t j + 1 N × 0 0 N 1 ran p ran x B n 1 N p ran x p n 0 p ran x p n K 0 N 1 ran p ran x B n 1 N p ran x p n 0 p ran x p n K
161 160 con3i ¬ 0 N 1 ran p ran x B n 1 N p ran x p n 0 p ran x p n K ¬ x = y 0 N 1 if y < 2 nd t y y + 1 / j 1 st 1 st t + f 2 nd 1 st t 1 j × 1 2 nd 1 st t j + 1 N × 0 0 N 1 ran p ran x B n 1 N p ran x p n 0 p ran x p n K
162 161 ralimi t 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N × 0 N ¬ 0 N 1 ran p ran x B n 1 N p ran x p n 0 p ran x p n K t 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N × 0 N ¬ x = y 0 N 1 if y < 2 nd t y y + 1 / j 1 st 1 st t + f 2 nd 1 st t 1 j × 1 2 nd 1 st t j + 1 N × 0 0 N 1 ran p ran x B n 1 N p ran x p n 0 p ran x p n K
163 rabeq0 t 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N × 0 N | x = y 0 N 1 if y < 2 nd t y y + 1 / j 1 st 1 st t + f 2 nd 1 st t 1 j × 1 2 nd 1 st t j + 1 N × 0 0 N 1 ran p ran x B n 1 N p ran x p n 0 p ran x p n K = t 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N × 0 N ¬ x = y 0 N 1 if y < 2 nd t y y + 1 / j 1 st 1 st t + f 2 nd 1 st t 1 j × 1 2 nd 1 st t j + 1 N × 0 0 N 1 ran p ran x B n 1 N p ran x p n 0 p ran x p n K
164 162 163 sylibr t 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N × 0 N ¬ 0 N 1 ran p ran x B n 1 N p ran x p n 0 p ran x p n K t 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N × 0 N | x = y 0 N 1 if y < 2 nd t y y + 1 / j 1 st 1 st t + f 2 nd 1 st t 1 j × 1 2 nd 1 st t j + 1 N × 0 0 N 1 ran p ran x B n 1 N p ran x p n 0 p ran x p n K =
165 164 fveq2d t 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N × 0 N ¬ 0 N 1 ran p ran x B n 1 N p ran x p n 0 p ran x p n K t 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N × 0 N | x = y 0 N 1 if y < 2 nd t y y + 1 / j 1 st 1 st t + f 2 nd 1 st t 1 j × 1 2 nd 1 st t j + 1 N × 0 0 N 1 ran p ran x B n 1 N p ran x p n 0 p ran x p n K =
166 146 165 breqtrrid t 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N × 0 N ¬ 0 N 1 ran p ran x B n 1 N p ran x p n 0 p ran x p n K 2 t 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N × 0 N | x = y 0 N 1 if y < 2 nd t y y + 1 / j 1 st 1 st t + f 2 nd 1 st t 1 j × 1 2 nd 1 st t j + 1 N × 0 0 N 1 ran p ran x B n 1 N p ran x p n 0 p ran x p n K
167 159 166 pm2.61d2 φ x 0 K 1 N 0 N 1 2 t 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N × 0 N | x = y 0 N 1 if y < 2 nd t y y + 1 / j 1 st 1 st t + f 2 nd 1 st t 1 j × 1 2 nd 1 st t j + 1 N × 0 0 N 1 ran p ran x B n 1 N p ran x p n 0 p ran x p n K
168 13 15 37 167 fsumdvds φ 2 x 0 K 1 N 0 N 1 t 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N × 0 N | x = y 0 N 1 if y < 2 nd t y y + 1 / j 1 st 1 st t + f 2 nd 1 st t 1 j × 1 2 nd 1 st t j + 1 N × 0 0 N 1 ran p ran x B n 1 N p ran x p n 0 p ran x p n K
169 rabfi 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N × 0 N Fin t 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N × 0 N | i 0 N 1 j 0 N 2 nd t i = 1 st t / s C Fin
170 32 169 ax-mp t 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N × 0 N | i 0 N 1 j 0 N 2 nd t i = 1 st t / s C Fin
171 simp1 i 0 N 1 j 0 N 1 i = 1 st t / s C 1 st 1 st t N = 0 2 nd 1 st t N = N i 0 N 1 j 0 N 1 i = 1 st t / s C
172 sneq 2 nd t = N 2 nd t = N
173 172 difeq2d 2 nd t = N 0 N 2 nd t = 0 N N
174 difun2 0 N 1 N N = 0 N 1 N
175 1 nnnn0d φ N 0
176 nn0uz 0 = 0
177 175 176 eleqtrdi φ N 0
178 fzm1 N 0 n 0 N n 0 N 1 n = N
179 177 178 syl φ n 0 N n 0 N 1 n = N
180 elun n 0 N 1 N n 0 N 1 n N
181 velsn n N n = N
182 181 orbi2i n 0 N 1 n N n 0 N 1 n = N
183 180 182 bitri n 0 N 1 N n 0 N 1 n = N
184 179 183 bitr4di φ n 0 N n 0 N 1 N
185 184 eqrdv φ 0 N = 0 N 1 N
186 185 difeq1d φ 0 N N = 0 N 1 N N
187 1 nnzd φ N
188 uzid N N N
189 uznfz N N ¬ N 0 N 1
190 187 188 189 3syl φ ¬ N 0 N 1
191 disjsn 0 N 1 N = ¬ N 0 N 1
192 disj3 0 N 1 N = 0 N 1 = 0 N 1 N
193 191 192 bitr3i ¬ N 0 N 1 0 N 1 = 0 N 1 N
194 190 193 sylib φ 0 N 1 = 0 N 1 N
195 174 186 194 3eqtr4a φ 0 N N = 0 N 1
196 173 195 sylan9eqr φ 2 nd t = N 0 N 2 nd t = 0 N 1
197 196 rexeqdv φ 2 nd t = N j 0 N 2 nd t i = 1 st t / s C j 0 N 1 i = 1 st t / s C
198 197 biimprd φ 2 nd t = N j 0 N 1 i = 1 st t / s C j 0 N 2 nd t i = 1 st t / s C
199 198 ralimdv φ 2 nd t = N i 0 N 1 j 0 N 1 i = 1 st t / s C i 0 N 1 j 0 N 2 nd t i = 1 st t / s C
200 199 expimpd φ 2 nd t = N i 0 N 1 j 0 N 1 i = 1 st t / s C i 0 N 1 j 0 N 2 nd t i = 1 st t / s C
201 171 200 sylan2i φ 2 nd t = N i 0 N 1 j 0 N 1 i = 1 st t / s C 1 st 1 st t N = 0 2 nd 1 st t N = N i 0 N 1 j 0 N 2 nd t i = 1 st t / s C
202 201 adantr φ t 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N × 0 N 2 nd t = N i 0 N 1 j 0 N 1 i = 1 st t / s C 1 st 1 st t N = 0 2 nd 1 st t N = N i 0 N 1 j 0 N 2 nd t i = 1 st t / s C
203 202 ss2rabdv φ t 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N × 0 N | 2 nd t = N i 0 N 1 j 0 N 1 i = 1 st t / s C 1 st 1 st t N = 0 2 nd 1 st t N = N t 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N × 0 N | i 0 N 1 j 0 N 2 nd t i = 1 st t / s C
204 hashssdif t 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N × 0 N | i 0 N 1 j 0 N 2 nd t i = 1 st t / s C Fin t 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N × 0 N | 2 nd t = N i 0 N 1 j 0 N 1 i = 1 st t / s C 1 st 1 st t N = 0 2 nd 1 st t N = N t 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N × 0 N | i 0 N 1 j 0 N 2 nd t i = 1 st t / s C t 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N × 0 N | i 0 N 1 j 0 N 2 nd t i = 1 st t / s C t 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N × 0 N | 2 nd t = N i 0 N 1 j 0 N 1 i = 1 st t / s C 1 st 1 st t N = 0 2 nd 1 st t N = N = t 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N × 0 N | i 0 N 1 j 0 N 2 nd t i = 1 st t / s C t 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N × 0 N | 2 nd t = N i 0 N 1 j 0 N 1 i = 1 st t / s C 1 st 1 st t N = 0 2 nd 1 st t N = N
205 170 203 204 sylancr φ t 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N × 0 N | i 0 N 1 j 0 N 2 nd t i = 1 st t / s C t 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N × 0 N | 2 nd t = N i 0 N 1 j 0 N 1 i = 1 st t / s C 1 st 1 st t N = 0 2 nd 1 st t N = N = t 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N × 0 N | i 0 N 1 j 0 N 2 nd t i = 1 st t / s C t 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N × 0 N | 2 nd t = N i 0 N 1 j 0 N 1 i = 1 st t / s C 1 st 1 st t N = 0 2 nd 1 st t N = N
206 1 adantr φ t 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N × 0 N N
207 3 adantlr φ t 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N × 0 N p : 1 N 0 K B 0 N
208 xp1st t 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N × 0 N 1 st t 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N
209 xp1st 1 st t 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N 1 st 1 st t 0 ..^ K 1 N
210 elmapi 1 st 1 st t 0 ..^ K 1 N 1 st 1 st t : 1 N 0 ..^ K
211 208 209 210 3syl t 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N × 0 N 1 st 1 st t : 1 N 0 ..^ K
212 211 adantl φ t 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N × 0 N 1 st 1 st t : 1 N 0 ..^ K
213 xp2nd 1 st t 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N 2 nd 1 st t f | f : 1 N 1-1 onto 1 N
214 fvex 2 nd 1 st t V
215 f1oeq1 f = 2 nd 1 st t f : 1 N 1-1 onto 1 N 2 nd 1 st t : 1 N 1-1 onto 1 N
216 214 215 elab 2 nd 1 st t f | f : 1 N 1-1 onto 1 N 2 nd 1 st t : 1 N 1-1 onto 1 N
217 213 216 sylib 1 st t 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N 2 nd 1 st t : 1 N 1-1 onto 1 N
218 208 217 syl t 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N × 0 N 2 nd 1 st t : 1 N 1-1 onto 1 N
219 218 adantl φ t 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N × 0 N 2 nd 1 st t : 1 N 1-1 onto 1 N
220 xp2nd t 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N × 0 N 2 nd t 0 N
221 220 adantl φ t 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N × 0 N 2 nd t 0 N
222 206 2 207 212 219 221 poimirlem24 φ t 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N × 0 N x 0 K 1 N 0 N 1 x = y 0 N 1 if y < 2 nd t y y + 1 / j 1 st 1 st t + f 2 nd 1 st t 1 j × 1 2 nd 1 st t j + 1 N × 0 0 N 1 ran p ran x B p ran x p N 0 i 0 N 1 j 0 N 2 nd t i = 1 st 1 st t 2 nd 1 st t / s C ¬ 2 nd t = N 1 st 1 st t N = 0 2 nd 1 st t N = N
223 208 adantl φ t 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N × 0 N 1 st t 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N
224 1st2nd2 1 st t 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N 1 st t = 1 st 1 st t 2 nd 1 st t
225 224 csbeq1d 1 st t 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N 1 st t / s C = 1 st 1 st t 2 nd 1 st t / s C
226 225 eqeq2d 1 st t 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N i = 1 st t / s C i = 1 st 1 st t 2 nd 1 st t / s C
227 226 rexbidv 1 st t 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N j 0 N 2 nd t i = 1 st t / s C j 0 N 2 nd t i = 1 st 1 st t 2 nd 1 st t / s C
228 227 ralbidv 1 st t 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N i 0 N 1 j 0 N 2 nd t i = 1 st t / s C i 0 N 1 j 0 N 2 nd t i = 1 st 1 st t 2 nd 1 st t / s C
229 228 anbi1d 1 st t 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N i 0 N 1 j 0 N 2 nd t i = 1 st t / s C ¬ 2 nd t = N 1 st 1 st t N = 0 2 nd 1 st t N = N i 0 N 1 j 0 N 2 nd t i = 1 st 1 st t 2 nd 1 st t / s C ¬ 2 nd t = N 1 st 1 st t N = 0 2 nd 1 st t N = N
230 223 229 syl φ t 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N × 0 N i 0 N 1 j 0 N 2 nd t i = 1 st t / s C ¬ 2 nd t = N 1 st 1 st t N = 0 2 nd 1 st t N = N i 0 N 1 j 0 N 2 nd t i = 1 st 1 st t 2 nd 1 st t / s C ¬ 2 nd t = N 1 st 1 st t N = 0 2 nd 1 st t N = N
231 222 230 bitr4d φ t 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N × 0 N x 0 K 1 N 0 N 1 x = y 0 N 1 if y < 2 nd t y y + 1 / j 1 st 1 st t + f 2 nd 1 st t 1 j × 1 2 nd 1 st t j + 1 N × 0 0 N 1 ran p ran x B p ran x p N 0 i 0 N 1 j 0 N 2 nd t i = 1 st t / s C ¬ 2 nd t = N 1 st 1 st t N = 0 2 nd 1 st t N = N
232 103 frnd x 0 K 1 N 0 N 1 ran x 0 K 1 N
233 232 anim2i φ x 0 K 1 N 0 N 1 φ ran x 0 K 1 N
234 dfss3 0 N 1 ran p ran x B n 0 N 1 n ran p ran x B
235 vex n V
236 eqid p ran x B = p ran x B
237 236 elrnmpt n V n ran p ran x B p ran x n = B
238 235 237 ax-mp n ran p ran x B p ran x n = B
239 238 ralbii n 0 N 1 n ran p ran x B n 0 N 1 p ran x n = B
240 234 239 sylbb 0 N 1 ran p ran x B n 0 N 1 p ran x n = B
241 1eluzge0 1 0
242 fzss1 1 0 1 N 1 0 N 1
243 ssralv 1 N 1 0 N 1 n 0 N 1 p ran x n = B n 1 N 1 p ran x n = B
244 241 242 243 mp2b n 0 N 1 p ran x n = B n 1 N 1 p ran x n = B
245 1 nncnd φ N
246 npcan1 N N - 1 + 1 = N
247 245 246 syl φ N - 1 + 1 = N
248 peano2zm N N 1
249 uzid N 1 N 1 N 1
250 peano2uz N 1 N 1 N - 1 + 1 N 1
251 187 248 249 250 4syl φ N - 1 + 1 N 1
252 247 251 eqeltrrd φ N N 1
253 fzss2 N N 1 1 N 1 1 N
254 252 253 syl φ 1 N 1 1 N
255 254 sselda φ n 1 N 1 n 1 N
256 255 adantlr φ ran x 0 K 1 N n 1 N 1 n 1 N
257 simplr φ ran x 0 K 1 N n 1 N ran x 0 K 1 N
258 ssel2 ran x 0 K 1 N p ran x p 0 K 1 N
259 elmapi p 0 K 1 N p : 1 N 0 K
260 258 259 syl ran x 0 K 1 N p ran x p : 1 N 0 K
261 257 260 sylan φ ran x 0 K 1 N n 1 N p ran x p : 1 N 0 K
262 elfzelz n 1 N n
263 262 zred n 1 N n
264 263 ltnrd n 1 N ¬ n < n
265 breq1 n = B n < n B < n
266 265 notbid n = B ¬ n < n ¬ B < n
267 264 266 syl5ibcom n 1 N n = B ¬ B < n
268 267 necon2ad n 1 N B < n n B
269 268 3ad2ant1 n 1 N p : 1 N 0 K p n = 0 B < n n B
270 269 adantl φ n 1 N p : 1 N 0 K p n = 0 B < n n B
271 4 270 mpd φ n 1 N p : 1 N 0 K p n = 0 n B
272 271 3exp2 φ n 1 N p : 1 N 0 K p n = 0 n B
273 272 imp31 φ n 1 N p : 1 N 0 K p n = 0 n B
274 273 necon2d φ n 1 N p : 1 N 0 K n = B p n 0
275 274 adantllr φ ran x 0 K 1 N n 1 N p : 1 N 0 K n = B p n 0
276 261 275 syldan φ ran x 0 K 1 N n 1 N p ran x n = B p n 0
277 276 reximdva φ ran x 0 K 1 N n 1 N p ran x n = B p ran x p n 0
278 256 277 syldan φ ran x 0 K 1 N n 1 N 1 p ran x n = B p ran x p n 0
279 278 ralimdva φ ran x 0 K 1 N n 1 N 1 p ran x n = B n 1 N 1 p ran x p n 0
280 279 imp φ ran x 0 K 1 N n 1 N 1 p ran x n = B n 1 N 1 p ran x p n 0
281 244 280 sylan2 φ ran x 0 K 1 N n 0 N 1 p ran x n = B n 1 N 1 p ran x p n 0
282 281 biantrurd φ ran x 0 K 1 N n 0 N 1 p ran x n = B p ran x p N 0 n 1 N 1 p ran x p n 0 p ran x p N 0
283 nnuz = 1
284 1 283 eleqtrdi φ N 1
285 fzm1 N 1 n 1 N n 1 N 1 n = N
286 284 285 syl φ n 1 N n 1 N 1 n = N
287 elun n 1 N 1 N n 1 N 1 n N
288 181 orbi2i n 1 N 1 n N n 1 N 1 n = N
289 287 288 bitri n 1 N 1 N n 1 N 1 n = N
290 286 289 bitr4di φ n 1 N n 1 N 1 N
291 290 eqrdv φ 1 N = 1 N 1 N
292 291 raleqdv φ n 1 N p ran x p n 0 n 1 N 1 N p ran x p n 0
293 ralunb n 1 N 1 N p ran x p n 0 n 1 N 1 p ran x p n 0 n N p ran x p n 0
294 292 293 bitrdi φ n 1 N p ran x p n 0 n 1 N 1 p ran x p n 0 n N p ran x p n 0
295 fveq2 n = N p n = p N
296 295 neeq1d n = N p n 0 p N 0
297 296 rexbidv n = N p ran x p n 0 p ran x p N 0
298 297 ralsng N n N p ran x p n 0 p ran x p N 0
299 1 298 syl φ n N p ran x p n 0 p ran x p N 0
300 299 anbi2d φ n 1 N 1 p ran x p n 0 n N p ran x p n 0 n 1 N 1 p ran x p n 0 p ran x p N 0
301 294 300 bitrd φ n 1 N p ran x p n 0 n 1 N 1 p ran x p n 0 p ran x p N 0
302 301 ad2antrr φ ran x 0 K 1 N n 0 N 1 p ran x n = B n 1 N p ran x p n 0 n 1 N 1 p ran x p n 0 p ran x p N 0
303 0z 0
304 1z 1
305 fzshftral 0 N 1 1 n 0 N 1 p ran x n = B m 0 + 1 N - 1 + 1 [˙m 1 / n]˙ p ran x n = B
306 303 304 305 mp3an13 N 1 n 0 N 1 p ran x n = B m 0 + 1 N - 1 + 1 [˙m 1 / n]˙ p ran x n = B
307 187 248 306 3syl φ n 0 N 1 p ran x n = B m 0 + 1 N - 1 + 1 [˙m 1 / n]˙ p ran x n = B
308 0p1e1 0 + 1 = 1
309 308 a1i φ 0 + 1 = 1
310 309 247 oveq12d φ 0 + 1 N - 1 + 1 = 1 N
311 310 raleqdv φ m 0 + 1 N - 1 + 1 [˙m 1 / n]˙ p ran x n = B m 1 N [˙m 1 / n]˙ p ran x n = B
312 307 311 bitrd φ n 0 N 1 p ran x n = B m 1 N [˙m 1 / n]˙ p ran x n = B
313 ovex m 1 V
314 eqeq1 n = m 1 n = B m 1 = B
315 314 rexbidv n = m 1 p ran x n = B p ran x m 1 = B
316 313 315 sbcie [˙m 1 / n]˙ p ran x n = B p ran x m 1 = B
317 316 ralbii m 1 N [˙m 1 / n]˙ p ran x n = B m 1 N p ran x m 1 = B
318 oveq1 m = n m 1 = n 1
319 318 eqeq1d m = n m 1 = B n 1 = B
320 319 rexbidv m = n p ran x m 1 = B p ran x n 1 = B
321 320 cbvralvw m 1 N p ran x m 1 = B n 1 N p ran x n 1 = B
322 317 321 bitri m 1 N [˙m 1 / n]˙ p ran x n = B n 1 N p ran x n 1 = B
323 312 322 bitrdi φ n 0 N 1 p ran x n = B n 1 N p ran x n 1 = B
324 323 biimpa φ n 0 N 1 p ran x n = B n 1 N p ran x n 1 = B
325 324 adantlr φ ran x 0 K 1 N n 0 N 1 p ran x n = B n 1 N p ran x n 1 = B
326 5 necomd φ n 1 N p : 1 N 0 K p n = K n 1 B
327 326 3exp2 φ n 1 N p : 1 N 0 K p n = K n 1 B
328 327 imp31 φ n 1 N p : 1 N 0 K p n = K n 1 B
329 328 necon2d φ n 1 N p : 1 N 0 K n 1 = B p n K
330 329 adantllr φ ran x 0 K 1 N n 1 N p : 1 N 0 K n 1 = B p n K
331 261 330 syldan φ ran x 0 K 1 N n 1 N p ran x n 1 = B p n K
332 331 reximdva φ ran x 0 K 1 N n 1 N p ran x n 1 = B p ran x p n K
333 332 ralimdva φ ran x 0 K 1 N n 1 N p ran x n 1 = B n 1 N p ran x p n K
334 333 imp φ ran x 0 K 1 N n 1 N p ran x n 1 = B n 1 N p ran x p n K
335 325 334 syldan φ ran x 0 K 1 N n 0 N 1 p ran x n = B n 1 N p ran x p n K
336 335 biantrud φ ran x 0 K 1 N n 0 N 1 p ran x n = B n 1 N p ran x p n 0 n 1 N p ran x p n 0 n 1 N p ran x p n K
337 r19.26 n 1 N p ran x p n 0 p ran x p n K n 1 N p ran x p n 0 n 1 N p ran x p n K
338 336 337 bitr4di φ ran x 0 K 1 N n 0 N 1 p ran x n = B n 1 N p ran x p n 0 n 1 N p ran x p n 0 p ran x p n K
339 282 302 338 3bitr2d φ ran x 0 K 1 N n 0 N 1 p ran x n = B p ran x p N 0 n 1 N p ran x p n 0 p ran x p n K
340 233 240 339 syl2an φ x 0 K 1 N 0 N 1 0 N 1 ran p ran x B p ran x p N 0 n 1 N p ran x p n 0 p ran x p n K
341 340 pm5.32da φ x 0 K 1 N 0 N 1 0 N 1 ran p ran x B p ran x p N 0 0 N 1 ran p ran x B n 1 N p ran x p n 0 p ran x p n K
342 341 anbi2d φ x 0 K 1 N 0 N 1 x = y 0 N 1 if y < 2 nd t y y + 1 / j 1 st 1 st t + f 2 nd 1 st t 1 j × 1 2 nd 1 st t j + 1 N × 0 0 N 1 ran p ran x B p ran x p N 0 x = y 0 N 1 if y < 2 nd t y y + 1 / j 1 st 1 st t + f 2 nd 1 st t 1 j × 1 2 nd 1 st t j + 1 N × 0 0 N 1 ran p ran x B n 1 N p ran x p n 0 p ran x p n K
343 342 rexbidva φ x 0 K 1 N 0 N 1 x = y 0 N 1 if y < 2 nd t y y + 1 / j 1 st 1 st t + f 2 nd 1 st t 1 j × 1 2 nd 1 st t j + 1 N × 0 0 N 1 ran p ran x B p ran x p N 0 x 0 K 1 N 0 N 1 x = y 0 N 1 if y < 2 nd t y y + 1 / j 1 st 1 st t + f 2 nd 1 st t 1 j × 1 2 nd 1 st t j + 1 N × 0 0 N 1 ran p ran x B n 1 N p ran x p n 0 p ran x p n K
344 343 adantr φ t 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N × 0 N x 0 K 1 N 0 N 1 x = y 0 N 1 if y < 2 nd t y y + 1 / j 1 st 1 st t + f 2 nd 1 st t 1 j × 1 2 nd 1 st t j + 1 N × 0 0 N 1 ran p ran x B p ran x p N 0 x 0 K 1 N 0 N 1 x = y 0 N 1 if y < 2 nd t y y + 1 / j 1 st 1 st t + f 2 nd 1 st t 1 j × 1 2 nd 1 st t j + 1 N × 0 0 N 1 ran p ran x B n 1 N p ran x p n 0 p ran x p n K
345 195 rexeqdv φ j 0 N N i = 1 st t / s C j 0 N 1 i = 1 st t / s C
346 345 biimpd φ j 0 N N i = 1 st t / s C j 0 N 1 i = 1 st t / s C
347 346 ralimdv φ i 0 N 1 j 0 N N i = 1 st t / s C i 0 N 1 j 0 N 1 i = 1 st t / s C
348 173 rexeqdv 2 nd t = N j 0 N 2 nd t i = 1 st t / s C j 0 N N i = 1 st t / s C
349 348 ralbidv 2 nd t = N i 0 N 1 j 0 N 2 nd t i = 1 st t / s C i 0 N 1 j 0 N N i = 1 st t / s C
350 349 imbi1d 2 nd t = N i 0 N 1 j 0 N 2 nd t i = 1 st t / s C i 0 N 1 j 0 N 1 i = 1 st t / s C i 0 N 1 j 0 N N i = 1 st t / s C i 0 N 1 j 0 N 1 i = 1 st t / s C
351 347 350 syl5ibrcom φ 2 nd t = N i 0 N 1 j 0 N 2 nd t i = 1 st t / s C i 0 N 1 j 0 N 1 i = 1 st t / s C
352 351 com23 φ i 0 N 1 j 0 N 2 nd t i = 1 st t / s C 2 nd t = N i 0 N 1 j 0 N 1 i = 1 st t / s C
353 352 imp φ i 0 N 1 j 0 N 2 nd t i = 1 st t / s C 2 nd t = N i 0 N 1 j 0 N 1 i = 1 st t / s C
354 353 adantrd φ i 0 N 1 j 0 N 2 nd t i = 1 st t / s C 2 nd t = N 1 st 1 st t N = 0 2 nd 1 st t N = N i 0 N 1 j 0 N 1 i = 1 st t / s C
355 354 pm4.71rd φ i 0 N 1 j 0 N 2 nd t i = 1 st t / s C 2 nd t = N 1 st 1 st t N = 0 2 nd 1 st t N = N i 0 N 1 j 0 N 1 i = 1 st t / s C 2 nd t = N 1 st 1 st t N = 0 2 nd 1 st t N = N
356 an12 i 0 N 1 j 0 N 1 i = 1 st t / s C 2 nd t = N 1 st 1 st t N = 0 2 nd 1 st t N = N 2 nd t = N i 0 N 1 j 0 N 1 i = 1 st t / s C 1 st 1 st t N = 0 2 nd 1 st t N = N
357 3anass i 0 N 1 j 0 N 1 i = 1 st t / s C 1 st 1 st t N = 0 2 nd 1 st t N = N i 0 N 1 j 0 N 1 i = 1 st t / s C 1 st 1 st t N = 0 2 nd 1 st t N = N
358 357 anbi2i 2 nd t = N i 0 N 1 j 0 N 1 i = 1 st t / s C 1 st 1 st t N = 0 2 nd 1 st t N = N 2 nd t = N i 0 N 1 j 0 N 1 i = 1 st t / s C 1 st 1 st t N = 0 2 nd 1 st t N = N
359 356 358 bitr4i i 0 N 1 j 0 N 1 i = 1 st t / s C 2 nd t = N 1 st 1 st t N = 0 2 nd 1 st t N = N 2 nd t = N i 0 N 1 j 0 N 1 i = 1 st t / s C 1 st 1 st t N = 0 2 nd 1 st t N = N
360 355 359 bitrdi φ i 0 N 1 j 0 N 2 nd t i = 1 st t / s C 2 nd t = N 1 st 1 st t N = 0 2 nd 1 st t N = N 2 nd t = N i 0 N 1 j 0 N 1 i = 1 st t / s C 1 st 1 st t N = 0 2 nd 1 st t N = N
361 360 notbid φ i 0 N 1 j 0 N 2 nd t i = 1 st t / s C ¬ 2 nd t = N 1 st 1 st t N = 0 2 nd 1 st t N = N ¬ 2 nd t = N i 0 N 1 j 0 N 1 i = 1 st t / s C 1 st 1 st t N = 0 2 nd 1 st t N = N
362 361 pm5.32da φ i 0 N 1 j 0 N 2 nd t i = 1 st t / s C ¬ 2 nd t = N 1 st 1 st t N = 0 2 nd 1 st t N = N i 0 N 1 j 0 N 2 nd t i = 1 st t / s C ¬ 2 nd t = N i 0 N 1 j 0 N 1 i = 1 st t / s C 1 st 1 st t N = 0 2 nd 1 st t N = N
363 362 adantr φ t 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N × 0 N i 0 N 1 j 0 N 2 nd t i = 1 st t / s C ¬ 2 nd t = N 1 st 1 st t N = 0 2 nd 1 st t N = N i 0 N 1 j 0 N 2 nd t i = 1 st t / s C ¬ 2 nd t = N i 0 N 1 j 0 N 1 i = 1 st t / s C 1 st 1 st t N = 0 2 nd 1 st t N = N
364 231 344 363 3bitr3d φ t 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N × 0 N x 0 K 1 N 0 N 1 x = y 0 N 1 if y < 2 nd t y y + 1 / j 1 st 1 st t + f 2 nd 1 st t 1 j × 1 2 nd 1 st t j + 1 N × 0 0 N 1 ran p ran x B n 1 N p ran x p n 0 p ran x p n K i 0 N 1 j 0 N 2 nd t i = 1 st t / s C ¬ 2 nd t = N i 0 N 1 j 0 N 1 i = 1 st t / s C 1 st 1 st t N = 0 2 nd 1 st t N = N
365 364 rabbidva φ t 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N × 0 N | x 0 K 1 N 0 N 1 x = y 0 N 1 if y < 2 nd t y y + 1 / j 1 st 1 st t + f 2 nd 1 st t 1 j × 1 2 nd 1 st t j + 1 N × 0 0 N 1 ran p ran x B n 1 N p ran x p n 0 p ran x p n K = t 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N × 0 N | i 0 N 1 j 0 N 2 nd t i = 1 st t / s C ¬ 2 nd t = N i 0 N 1 j 0 N 1 i = 1 st t / s C 1 st 1 st t N = 0 2 nd 1 st t N = N
366 iunrab x 0 K 1 N 0 N 1 t 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N × 0 N | x = y 0 N 1 if y < 2 nd t y y + 1 / j 1 st 1 st t + f 2 nd 1 st t 1 j × 1 2 nd 1 st t j + 1 N × 0 0 N 1 ran p ran x B n 1 N p ran x p n 0 p ran x p n K = t 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N × 0 N | x 0 K 1 N 0 N 1 x = y 0 N 1 if y < 2 nd t y y + 1 / j 1 st 1 st t + f 2 nd 1 st t 1 j × 1 2 nd 1 st t j + 1 N × 0 0 N 1 ran p ran x B n 1 N p ran x p n 0 p ran x p n K
367 difrab t 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N × 0 N | i 0 N 1 j 0 N 2 nd t i = 1 st t / s C t 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N × 0 N | 2 nd t = N i 0 N 1 j 0 N 1 i = 1 st t / s C 1 st 1 st t N = 0 2 nd 1 st t N = N = t 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N × 0 N | i 0 N 1 j 0 N 2 nd t i = 1 st t / s C ¬ 2 nd t = N i 0 N 1 j 0 N 1 i = 1 st t / s C 1 st 1 st t N = 0 2 nd 1 st t N = N
368 365 366 367 3eqtr4g φ x 0 K 1 N 0 N 1 t 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N × 0 N | x = y 0 N 1 if y < 2 nd t y y + 1 / j 1 st 1 st t + f 2 nd 1 st t 1 j × 1 2 nd 1 st t j + 1 N × 0 0 N 1 ran p ran x B n 1 N p ran x p n 0 p ran x p n K = t 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N × 0 N | i 0 N 1 j 0 N 2 nd t i = 1 st t / s C t 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N × 0 N | 2 nd t = N i 0 N 1 j 0 N 1 i = 1 st t / s C 1 st 1 st t N = 0 2 nd 1 st t N = N
369 368 fveq2d φ x 0 K 1 N 0 N 1 t 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N × 0 N | x = y 0 N 1 if y < 2 nd t y y + 1 / j 1 st 1 st t + f 2 nd 1 st t 1 j × 1 2 nd 1 st t j + 1 N × 0 0 N 1 ran p ran x B n 1 N p ran x p n 0 p ran x p n K = t 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N × 0 N | i 0 N 1 j 0 N 2 nd t i = 1 st t / s C t 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N × 0 N | 2 nd t = N i 0 N 1 j 0 N 1 i = 1 st t / s C 1 st 1 st t N = 0 2 nd 1 st t N = N
370 32 33 mp1i φ x 0 K 1 N 0 N 1 t 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N × 0 N | x = y 0 N 1 if y < 2 nd t y y + 1 / j 1 st 1 st t + f 2 nd 1 st t 1 j × 1 2 nd 1 st t j + 1 N × 0 0 N 1 ran p ran x B n 1 N p ran x p n 0 p ran x p n K Fin
371 simpl x = y 0 N 1 if y < 2 nd t y y + 1 / j 1 st 1 st t + f 2 nd 1 st t 1 j × 1 2 nd 1 st t j + 1 N × 0 0 N 1 ran p ran x B n 1 N p ran x p n 0 p ran x p n K x = y 0 N 1 if y < 2 nd t y y + 1 / j 1 st 1 st t + f 2 nd 1 st t 1 j × 1 2 nd 1 st t j + 1 N × 0
372 371 a1i t 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N × 0 N x = y 0 N 1 if y < 2 nd t y y + 1 / j 1 st 1 st t + f 2 nd 1 st t 1 j × 1 2 nd 1 st t j + 1 N × 0 0 N 1 ran p ran x B n 1 N p ran x p n 0 p ran x p n K x = y 0 N 1 if y < 2 nd t y y + 1 / j 1 st 1 st t + f 2 nd 1 st t 1 j × 1 2 nd 1 st t j + 1 N × 0
373 372 ss2rabi t 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N × 0 N | x = y 0 N 1 if y < 2 nd t y y + 1 / j 1 st 1 st t + f 2 nd 1 st t 1 j × 1 2 nd 1 st t j + 1 N × 0 0 N 1 ran p ran x B n 1 N p ran x p n 0 p ran x p n K t 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N × 0 N | x = y 0 N 1 if y < 2 nd t y y + 1 / j 1 st 1 st t + f 2 nd 1 st t 1 j × 1 2 nd 1 st t j + 1 N × 0
374 373 sseli s t 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N × 0 N | x = y 0 N 1 if y < 2 nd t y y + 1 / j 1 st 1 st t + f 2 nd 1 st t 1 j × 1 2 nd 1 st t j + 1 N × 0 0 N 1 ran p ran x B n 1 N p ran x p n 0 p ran x p n K s t 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N × 0 N | x = y 0 N 1 if y < 2 nd t y y + 1 / j 1 st 1 st t + f 2 nd 1 st t 1 j × 1 2 nd 1 st t j + 1 N × 0
375 fveq2 t = s 2 nd t = 2 nd s
376 375 breq2d t = s y < 2 nd t y < 2 nd s
377 376 ifbid t = s if y < 2 nd t y y + 1 = if y < 2 nd s y y + 1
378 377 csbeq1d t = s if y < 2 nd t y y + 1 / j 1 st 1 st t + f 2 nd 1 st t 1 j × 1 2 nd 1 st t j + 1 N × 0 = if y < 2 nd s y y + 1 / j 1 st 1 st t + f 2 nd 1 st t 1 j × 1 2 nd 1 st t j + 1 N × 0
379 2fveq3 t = s 1 st 1 st t = 1 st 1 st s
380 2fveq3 t = s 2 nd 1 st t = 2 nd 1 st s
381 380 imaeq1d t = s 2 nd 1 st t 1 j = 2 nd 1 st s 1 j
382 381 xpeq1d t = s 2 nd 1 st t 1 j × 1 = 2 nd 1 st s 1 j × 1
383 380 imaeq1d t = s 2 nd 1 st t j + 1 N = 2 nd 1 st s j + 1 N
384 383 xpeq1d t = s 2 nd 1 st t j + 1 N × 0 = 2 nd 1 st s j + 1 N × 0
385 382 384 uneq12d t = s 2 nd 1 st t 1 j × 1 2 nd 1 st t j + 1 N × 0 = 2 nd 1 st s 1 j × 1 2 nd 1 st s j + 1 N × 0
386 379 385 oveq12d t = s 1 st 1 st t + f 2 nd 1 st t 1 j × 1 2 nd 1 st t j + 1 N × 0 = 1 st 1 st s + f 2 nd 1 st s 1 j × 1 2 nd 1 st s j + 1 N × 0
387 386 csbeq2dv t = s if y < 2 nd s y y + 1 / j 1 st 1 st t + f 2 nd 1 st t 1 j × 1 2 nd 1 st t j + 1 N × 0 = if y < 2 nd s y y + 1 / j 1 st 1 st s + f 2 nd 1 st s 1 j × 1 2 nd 1 st s j + 1 N × 0
388 378 387 eqtrd t = s if y < 2 nd t y y + 1 / j 1 st 1 st t + f 2 nd 1 st t 1 j × 1 2 nd 1 st t j + 1 N × 0 = if y < 2 nd s y y + 1 / j 1 st 1 st s + f 2 nd 1 st s 1 j × 1 2 nd 1 st s j + 1 N × 0
389 388 mpteq2dv t = s y 0 N 1 if y < 2 nd t y y + 1 / j 1 st 1 st t + f 2 nd 1 st t 1 j × 1 2 nd 1 st t j + 1 N × 0 = y 0 N 1 if y < 2 nd s y y + 1 / j 1 st 1 st s + f 2 nd 1 st s 1 j × 1 2 nd 1 st s j + 1 N × 0
390 389 eqeq2d t = s x = y 0 N 1 if y < 2 nd t y y + 1 / j 1 st 1 st t + f 2 nd 1 st t 1 j × 1 2 nd 1 st t j + 1 N × 0 x = y 0 N 1 if y < 2 nd s y y + 1 / j 1 st 1 st s + f 2 nd 1 st s 1 j × 1 2 nd 1 st s j + 1 N × 0
391 eqcom x = y 0 N 1 if y < 2 nd s y y + 1 / j 1 st 1 st s + f 2 nd 1 st s 1 j × 1 2 nd 1 st s j + 1 N × 0 y 0 N 1 if y < 2 nd s y y + 1 / j 1 st 1 st s + f 2 nd 1 st s 1 j × 1 2 nd 1 st s j + 1 N × 0 = x
392 390 391 bitrdi t = s x = y 0 N 1 if y < 2 nd t y y + 1 / j 1 st 1 st t + f 2 nd 1 st t 1 j × 1 2 nd 1 st t j + 1 N × 0 y 0 N 1 if y < 2 nd s y y + 1 / j 1 st 1 st s + f 2 nd 1 st s 1 j × 1 2 nd 1 st s j + 1 N × 0 = x
393 392 elrab s t 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N × 0 N | x = y 0 N 1 if y < 2 nd t y y + 1 / j 1 st 1 st t + f 2 nd 1 st t 1 j × 1 2 nd 1 st t j + 1 N × 0 s 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N × 0 N y 0 N 1 if y < 2 nd s y y + 1 / j 1 st 1 st s + f 2 nd 1 st s 1 j × 1 2 nd 1 st s j + 1 N × 0 = x
394 393 simprbi s t 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N × 0 N | x = y 0 N 1 if y < 2 nd t y y + 1 / j 1 st 1 st t + f 2 nd 1 st t 1 j × 1 2 nd 1 st t j + 1 N × 0 y 0 N 1 if y < 2 nd s y y + 1 / j 1 st 1 st s + f 2 nd 1 st s 1 j × 1 2 nd 1 st s j + 1 N × 0 = x
395 374 394 syl s t 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N × 0 N | x = y 0 N 1 if y < 2 nd t y y + 1 / j 1 st 1 st t + f 2 nd 1 st t 1 j × 1 2 nd 1 st t j + 1 N × 0 0 N 1 ran p ran x B n 1 N p ran x p n 0 p ran x p n K y 0 N 1 if y < 2 nd s y y + 1 / j 1 st 1 st s + f 2 nd 1 st s 1 j × 1 2 nd 1 st s j + 1 N × 0 = x
396 395 rgen s t 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N × 0 N | x = y 0 N 1 if y < 2 nd t y y + 1 / j 1 st 1 st t + f 2 nd 1 st t 1 j × 1 2 nd 1 st t j + 1 N × 0 0 N 1 ran p ran x B n 1 N p ran x p n 0 p ran x p n K y 0 N 1 if y < 2 nd s y y + 1 / j 1 st 1 st s + f 2 nd 1 st s 1 j × 1 2 nd 1 st s j + 1 N × 0 = x
397 396 rgenw x 0 K 1 N 0 N 1 s t 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N × 0 N | x = y 0 N 1 if y < 2 nd t y y + 1 / j 1 st 1 st t + f 2 nd 1 st t 1 j × 1 2 nd 1 st t j + 1 N × 0 0 N 1 ran p ran x B n 1 N p ran x p n 0 p ran x p n K y 0 N 1 if y < 2 nd s y y + 1 / j 1 st 1 st s + f 2 nd 1 st s 1 j × 1 2 nd 1 st s j + 1 N × 0 = x
398 invdisj x 0 K 1 N 0 N 1 s t 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N × 0 N | x = y 0 N 1 if y < 2 nd t y y + 1 / j 1 st 1 st t + f 2 nd 1 st t 1 j × 1 2 nd 1 st t j + 1 N × 0 0 N 1 ran p ran x B n 1 N p ran x p n 0 p ran x p n K y 0 N 1 if y < 2 nd s y y + 1 / j 1 st 1 st s + f 2 nd 1 st s 1 j × 1 2 nd 1 st s j + 1 N × 0 = x Disj x 0 K 1 N 0 N 1 t 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N × 0 N | x = y 0 N 1 if y < 2 nd t y y + 1 / j 1 st 1 st t + f 2 nd 1 st t 1 j × 1 2 nd 1 st t j + 1 N × 0 0 N 1 ran p ran x B n 1 N p ran x p n 0 p ran x p n K
399 397 398 mp1i φ Disj x 0 K 1 N 0 N 1 t 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N × 0 N | x = y 0 N 1 if y < 2 nd t y y + 1 / j 1 st 1 st t + f 2 nd 1 st t 1 j × 1 2 nd 1 st t j + 1 N × 0 0 N 1 ran p ran x B n 1 N p ran x p n 0 p ran x p n K
400 13 370 399 hashiun φ x 0 K 1 N 0 N 1 t 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N × 0 N | x = y 0 N 1 if y < 2 nd t y y + 1 / j 1 st 1 st t + f 2 nd 1 st t 1 j × 1 2 nd 1 st t j + 1 N × 0 0 N 1 ran p ran x B n 1 N p ran x p n 0 p ran x p n K = x 0 K 1 N 0 N 1 t 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N × 0 N | x = y 0 N 1 if y < 2 nd t y y + 1 / j 1 st 1 st t + f 2 nd 1 st t 1 j × 1 2 nd 1 st t j + 1 N × 0 0 N 1 ran p ran x B n 1 N p ran x p n 0 p ran x p n K
401 369 400 eqtr3d φ t 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N × 0 N | i 0 N 1 j 0 N 2 nd t i = 1 st t / s C t 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N × 0 N | 2 nd t = N i 0 N 1 j 0 N 1 i = 1 st t / s C 1 st 1 st t N = 0 2 nd 1 st t N = N = x 0 K 1 N 0 N 1 t 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N × 0 N | x = y 0 N 1 if y < 2 nd t y y + 1 / j 1 st 1 st t + f 2 nd 1 st t 1 j × 1 2 nd 1 st t j + 1 N × 0 0 N 1 ran p ran x B n 1 N p ran x p n 0 p ran x p n K
402 fo1st 1 st : V onto V
403 fofun 1 st : V onto V Fun 1 st
404 402 403 ax-mp Fun 1 st
405 ssv t 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N × 0 N | 2 nd t = N i 0 N 1 j 0 N 1 i = 1 st t / s C 1 st 1 st t N = 0 2 nd 1 st t N = N V
406 fof 1 st : V onto V 1 st : V V
407 402 406 ax-mp 1 st : V V
408 407 fdmi dom 1 st = V
409 405 408 sseqtrri t 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N × 0 N | 2 nd t = N i 0 N 1 j 0 N 1 i = 1 st t / s C 1 st 1 st t N = 0 2 nd 1 st t N = N dom 1 st
410 fores Fun 1 st t 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N × 0 N | 2 nd t = N i 0 N 1 j 0 N 1 i = 1 st t / s C 1 st 1 st t N = 0 2 nd 1 st t N = N dom 1 st 1 st t 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N × 0 N | 2 nd t = N i 0 N 1 j 0 N 1 i = 1 st t / s C 1 st 1 st t N = 0 2 nd 1 st t N = N : t 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N × 0 N | 2 nd t = N i 0 N 1 j 0 N 1 i = 1 st t / s C 1 st 1 st t N = 0 2 nd 1 st t N = N onto 1 st t 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N × 0 N | 2 nd t = N i 0 N 1 j 0 N 1 i = 1 st t / s C 1 st 1 st t N = 0 2 nd 1 st t N = N
411 404 409 410 mp2an 1 st t 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N × 0 N | 2 nd t = N i 0 N 1 j 0 N 1 i = 1 st t / s C 1 st 1 st t N = 0 2 nd 1 st t N = N : t 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N × 0 N | 2 nd t = N i 0 N 1 j 0 N 1 i = 1 st t / s C 1 st 1 st t N = 0 2 nd 1 st t N = N onto 1 st t 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N × 0 N | 2 nd t = N i 0 N 1 j 0 N 1 i = 1 st t / s C 1 st 1 st t N = 0 2 nd 1 st t N = N
412 fveqeq2 t = x 2 nd t = N 2 nd x = N
413 fveq2 t = x 1 st t = 1 st x
414 413 csbeq1d t = x 1 st t / s C = 1 st x / s C
415 414 eqeq2d t = x i = 1 st t / s C i = 1 st x / s C
416 415 rexbidv t = x j 0 N 1 i = 1 st t / s C j 0 N 1 i = 1 st x / s C
417 416 ralbidv t = x i 0 N 1 j 0 N 1 i = 1 st t / s C i 0 N 1 j 0 N 1 i = 1 st x / s C
418 2fveq3 t = x 1 st 1 st t = 1 st 1 st x
419 418 fveq1d t = x 1 st 1 st t N = 1 st 1 st x N
420 419 eqeq1d t = x 1 st 1 st t N = 0 1 st 1 st x N = 0
421 2fveq3 t = x 2 nd 1 st t = 2 nd 1 st x
422 421 fveq1d t = x 2 nd 1 st t N = 2 nd 1 st x N
423 422 eqeq1d t = x 2 nd 1 st t N = N 2 nd 1 st x N = N
424 417 420 423 3anbi123d t = x i 0 N 1 j 0 N 1 i = 1 st t / s C 1 st 1 st t N = 0 2 nd 1 st t N = N i 0 N 1 j 0 N 1 i = 1 st x / s C 1 st 1 st x N = 0 2 nd 1 st x N = N
425 412 424 anbi12d t = x 2 nd t = N i 0 N 1 j 0 N 1 i = 1 st t / s C 1 st 1 st t N = 0 2 nd 1 st t N = N 2 nd x = N i 0 N 1 j 0 N 1 i = 1 st x / s C 1 st 1 st x N = 0 2 nd 1 st x N = N
426 425 rexrab x t 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N × 0 N | 2 nd t = N i 0 N 1 j 0 N 1 i = 1 st t / s C 1 st 1 st t N = 0 2 nd 1 st t N = N 1 st x = s x 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N × 0 N 2 nd x = N i 0 N 1 j 0 N 1 i = 1 st x / s C 1 st 1 st x N = 0 2 nd 1 st x N = N 1 st x = s
427 xp1st x 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N × 0 N 1 st x 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N
428 427 anim1i x 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N × 0 N i 0 N 1 j 0 N 1 i = 1 st x / s C 1 st 1 st x N = 0 2 nd 1 st x N = N 1 st x 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N i 0 N 1 j 0 N 1 i = 1 st x / s C 1 st 1 st x N = 0 2 nd 1 st x N = N
429 eleq1 1 st x = s 1 st x 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N s 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N
430 csbeq1a s = 1 st x C = 1 st x / s C
431 430 eqcoms 1 st x = s C = 1 st x / s C
432 431 eqcomd 1 st x = s 1 st x / s C = C
433 432 eqeq2d 1 st x = s i = 1 st x / s C i = C
434 433 rexbidv 1 st x = s j 0 N 1 i = 1 st x / s C j 0 N 1 i = C
435 434 ralbidv 1 st x = s i 0 N 1 j 0 N 1 i = 1 st x / s C i 0 N 1 j 0 N 1 i = C
436 fveq2 1 st x = s 1 st 1 st x = 1 st s
437 436 fveq1d 1 st x = s 1 st 1 st x N = 1 st s N
438 437 eqeq1d 1 st x = s 1 st 1 st x N = 0 1 st s N = 0
439 fveq2 1 st x = s 2 nd 1 st x = 2 nd s
440 439 fveq1d 1 st x = s 2 nd 1 st x N = 2 nd s N
441 440 eqeq1d 1 st x = s 2 nd 1 st x N = N 2 nd s N = N
442 435 438 441 3anbi123d 1 st x = s i 0 N 1 j 0 N 1 i = 1 st x / s C 1 st 1 st x N = 0 2 nd 1 st x N = N i 0 N 1 j 0 N 1 i = C 1 st s N = 0 2 nd s N = N
443 429 442 anbi12d 1 st x = s 1 st x 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N i 0 N 1 j 0 N 1 i = 1 st x / s C 1 st 1 st x N = 0 2 nd 1 st x N = N s 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N i 0 N 1 j 0 N 1 i = C 1 st s N = 0 2 nd s N = N
444 428 443 syl5ibcom x 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N × 0 N i 0 N 1 j 0 N 1 i = 1 st x / s C 1 st 1 st x N = 0 2 nd 1 st x N = N 1 st x = s s 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N i 0 N 1 j 0 N 1 i = C 1 st s N = 0 2 nd s N = N
445 444 adantrl x 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N × 0 N 2 nd x = N i 0 N 1 j 0 N 1 i = 1 st x / s C 1 st 1 st x N = 0 2 nd 1 st x N = N 1 st x = s s 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N i 0 N 1 j 0 N 1 i = C 1 st s N = 0 2 nd s N = N
446 445 expimpd x 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N × 0 N 2 nd x = N i 0 N 1 j 0 N 1 i = 1 st x / s C 1 st 1 st x N = 0 2 nd 1 st x N = N 1 st x = s s 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N i 0 N 1 j 0 N 1 i = C 1 st s N = 0 2 nd s N = N
447 446 rexlimiv x 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N × 0 N 2 nd x = N i 0 N 1 j 0 N 1 i = 1 st x / s C 1 st 1 st x N = 0 2 nd 1 st x N = N 1 st x = s s 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N i 0 N 1 j 0 N 1 i = C 1 st s N = 0 2 nd s N = N
448 nn0fz0 N 0 N 0 N
449 175 448 sylib φ N 0 N
450 opelxpi s 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N N 0 N s N 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N × 0 N
451 449 450 sylan2 s 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N φ s N 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N × 0 N
452 451 ancoms φ s 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N s N 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N × 0 N
453 opelxp2 s N 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N × 0 N N 0 N
454 op2ndg s V N 0 N 2 nd s N = N
455 454 biantrurd s V N 0 N i 0 N 1 j 0 N 1 i = 1 st s N / s C 1 st 1 st s N N = 0 2 nd 1 st s N N = N 2 nd s N = N i 0 N 1 j 0 N 1 i = 1 st s N / s C 1 st 1 st s N N = 0 2 nd 1 st s N N = N
456 op1stg s V N 0 N 1 st s N = s
457 csbeq1a s = 1 st s N C = 1 st s N / s C
458 457 eqcoms 1 st s N = s C = 1 st s N / s C
459 458 eqcomd 1 st s N = s 1 st s N / s C = C
460 456 459 syl s V N 0 N 1 st s N / s C = C
461 460 eqeq2d s V N 0 N i = 1 st s N / s C i = C
462 461 rexbidv s V N 0 N j 0 N 1 i = 1 st s N / s C j 0 N 1 i = C
463 462 ralbidv s V N 0 N i 0 N 1 j 0 N 1 i = 1 st s N / s C i 0 N 1 j 0 N 1 i = C
464 456 fveq2d s V N 0 N 1 st 1 st s N = 1 st s
465 464 fveq1d s V N 0 N 1 st 1 st s N N = 1 st s N
466 465 eqeq1d s V N 0 N 1 st 1 st s N N = 0 1 st s N = 0
467 456 fveq2d s V N 0 N 2 nd 1 st s N = 2 nd s
468 467 fveq1d s V N 0 N 2 nd 1 st s N N = 2 nd s N
469 468 eqeq1d s V N 0 N 2 nd 1 st s N N = N 2 nd s N = N
470 463 466 469 3anbi123d s V N 0 N i 0 N 1 j 0 N 1 i = 1 st s N / s C 1 st 1 st s N N = 0 2 nd 1 st s N N = N i 0 N 1 j 0 N 1 i = C 1 st s N = 0 2 nd s N = N
471 456 biantrud s V N 0 N 2 nd s N = N i 0 N 1 j 0 N 1 i = 1 st s N / s C 1 st 1 st s N N = 0 2 nd 1 st s N N = N 2 nd s N = N i 0 N 1 j 0 N 1 i = 1 st s N / s C 1 st 1 st s N N = 0 2 nd 1 st s N N = N 1 st s N = s
472 455 470 471 3bitr3d s V N 0 N i 0 N 1 j 0 N 1 i = C 1 st s N = 0 2 nd s N = N 2 nd s N = N i 0 N 1 j 0 N 1 i = 1 st s N / s C 1 st 1 st s N N = 0 2 nd 1 st s N N = N 1 st s N = s
473 49 453 472 sylancr s N 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N × 0 N i 0 N 1 j 0 N 1 i = C 1 st s N = 0 2 nd s N = N 2 nd s N = N i 0 N 1 j 0 N 1 i = 1 st s N / s C 1 st 1 st s N N = 0 2 nd 1 st s N N = N 1 st s N = s
474 473 biimpa s N 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N × 0 N i 0 N 1 j 0 N 1 i = C 1 st s N = 0 2 nd s N = N 2 nd s N = N i 0 N 1 j 0 N 1 i = 1 st s N / s C 1 st 1 st s N N = 0 2 nd 1 st s N N = N 1 st s N = s
475 fveqeq2 x = s N 2 nd x = N 2 nd s N = N
476 fveq2 x = s N 1 st x = 1 st s N
477 476 csbeq1d x = s N 1 st x / s C = 1 st s N / s C
478 477 eqeq2d x = s N i = 1 st x / s C i = 1 st s N / s C
479 478 rexbidv x = s N j 0 N 1 i = 1 st x / s C j 0 N 1 i = 1 st s N / s C
480 479 ralbidv x = s N i 0 N 1 j 0 N 1 i = 1 st x / s C i 0 N 1 j 0 N 1 i = 1 st s N / s C
481 2fveq3 x = s N 1 st 1 st x = 1 st 1 st s N
482 481 fveq1d x = s N 1 st 1 st x N = 1 st 1 st s N N
483 482 eqeq1d x = s N 1 st 1 st x N = 0 1 st 1 st s N N = 0
484 2fveq3 x = s N 2 nd 1 st x = 2 nd 1 st s N
485 484 fveq1d x = s N 2 nd 1 st x N = 2 nd 1 st s N N
486 485 eqeq1d x = s N 2 nd 1 st x N = N 2 nd 1 st s N N = N
487 480 483 486 3anbi123d x = s N i 0 N 1 j 0 N 1 i = 1 st x / s C 1 st 1 st x N = 0 2 nd 1 st x N = N i 0 N 1 j 0 N 1 i = 1 st s N / s C 1 st 1 st s N N = 0 2 nd 1 st s N N = N
488 475 487 anbi12d x = s N 2 nd x = N i 0 N 1 j 0 N 1 i = 1 st x / s C 1 st 1 st x N = 0 2 nd 1 st x N = N 2 nd s N = N i 0 N 1 j 0 N 1 i = 1 st s N / s C 1 st 1 st s N N = 0 2 nd 1 st s N N = N
489 fveqeq2 x = s N 1 st x = s 1 st s N = s
490 488 489 anbi12d x = s N 2 nd x = N i 0 N 1 j 0 N 1 i = 1 st x / s C 1 st 1 st x N = 0 2 nd 1 st x N = N 1 st x = s 2 nd s N = N i 0 N 1 j 0 N 1 i = 1 st s N / s C 1 st 1 st s N N = 0 2 nd 1 st s N N = N 1 st s N = s
491 490 rspcev s N 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N × 0 N 2 nd s N = N i 0 N 1 j 0 N 1 i = 1 st s N / s C 1 st 1 st s N N = 0 2 nd 1 st s N N = N 1 st s N = s x 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N × 0 N 2 nd x = N i 0 N 1 j 0 N 1 i = 1 st x / s C 1 st 1 st x N = 0 2 nd 1 st x N = N 1 st x = s
492 474 491 syldan s N 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N × 0 N i 0 N 1 j 0 N 1 i = C 1 st s N = 0 2 nd s N = N x 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N × 0 N 2 nd x = N i 0 N 1 j 0 N 1 i = 1 st x / s C 1 st 1 st x N = 0 2 nd 1 st x N = N 1 st x = s
493 452 492 sylan φ s 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N i 0 N 1 j 0 N 1 i = C 1 st s N = 0 2 nd s N = N x 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N × 0 N 2 nd x = N i 0 N 1 j 0 N 1 i = 1 st x / s C 1 st 1 st x N = 0 2 nd 1 st x N = N 1 st x = s
494 493 expl φ s 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N i 0 N 1 j 0 N 1 i = C 1 st s N = 0 2 nd s N = N x 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N × 0 N 2 nd x = N i 0 N 1 j 0 N 1 i = 1 st x / s C 1 st 1 st x N = 0 2 nd 1 st x N = N 1 st x = s
495 447 494 impbid2 φ x 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N × 0 N 2 nd x = N i 0 N 1 j 0 N 1 i = 1 st x / s C 1 st 1 st x N = 0 2 nd 1 st x N = N 1 st x = s s 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N i 0 N 1 j 0 N 1 i = C 1 st s N = 0 2 nd s N = N
496 426 495 bitrid φ x t 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N × 0 N | 2 nd t = N i 0 N 1 j 0 N 1 i = 1 st t / s C 1 st 1 st t N = 0 2 nd 1 st t N = N 1 st x = s s 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N i 0 N 1 j 0 N 1 i = C 1 st s N = 0 2 nd s N = N
497 496 abbidv φ s | x t 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N × 0 N | 2 nd t = N i 0 N 1 j 0 N 1 i = 1 st t / s C 1 st 1 st t N = 0 2 nd 1 st t N = N 1 st x = s = s | s 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N i 0 N 1 j 0 N 1 i = C 1 st s N = 0 2 nd s N = N
498 dfimafn Fun 1 st t 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N × 0 N | 2 nd t = N i 0 N 1 j 0 N 1 i = 1 st t / s C 1 st 1 st t N = 0 2 nd 1 st t N = N dom 1 st 1 st t 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N × 0 N | 2 nd t = N i 0 N 1 j 0 N 1 i = 1 st t / s C 1 st 1 st t N = 0 2 nd 1 st t N = N = y | x t 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N × 0 N | 2 nd t = N i 0 N 1 j 0 N 1 i = 1 st t / s C 1 st 1 st t N = 0 2 nd 1 st t N = N 1 st x = y
499 404 409 498 mp2an 1 st t 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N × 0 N | 2 nd t = N i 0 N 1 j 0 N 1 i = 1 st t / s C 1 st 1 st t N = 0 2 nd 1 st t N = N = y | x t 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N × 0 N | 2 nd t = N i 0 N 1 j 0 N 1 i = 1 st t / s C 1 st 1 st t N = 0 2 nd 1 st t N = N 1 st x = y
500 nfv s 2 nd t = N
501 nfcv _ s 0 N 1
502 nfcsb1v _ s 1 st t / s C
503 502 nfeq2 s i = 1 st t / s C
504 501 503 nfrexw s j 0 N 1 i = 1 st t / s C
505 501 504 nfralw s i 0 N 1 j 0 N 1 i = 1 st t / s C
506 nfv s 1 st 1 st t N = 0
507 nfv s 2 nd 1 st t N = N
508 505 506 507 nf3an s i 0 N 1 j 0 N 1 i = 1 st t / s C 1 st 1 st t N = 0 2 nd 1 st t N = N
509 500 508 nfan s 2 nd t = N i 0 N 1 j 0 N 1 i = 1 st t / s C 1 st 1 st t N = 0 2 nd 1 st t N = N
510 nfcv _ s 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N × 0 N
511 509 510 nfrabw _ s t 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N × 0 N | 2 nd t = N i 0 N 1 j 0 N 1 i = 1 st t / s C 1 st 1 st t N = 0 2 nd 1 st t N = N
512 nfv s 1 st x = y
513 511 512 nfrexw s x t 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N × 0 N | 2 nd t = N i 0 N 1 j 0 N 1 i = 1 st t / s C 1 st 1 st t N = 0 2 nd 1 st t N = N 1 st x = y
514 nfv y x t 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N × 0 N | 2 nd t = N i 0 N 1 j 0 N 1 i = 1 st t / s C 1 st 1 st t N = 0 2 nd 1 st t N = N 1 st x = s
515 eqeq2 y = s 1 st x = y 1 st x = s
516 515 rexbidv y = s x t 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N × 0 N | 2 nd t = N i 0 N 1 j 0 N 1 i = 1 st t / s C 1 st 1 st t N = 0 2 nd 1 st t N = N 1 st x = y x t 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N × 0 N | 2 nd t = N i 0 N 1 j 0 N 1 i = 1 st t / s C 1 st 1 st t N = 0 2 nd 1 st t N = N 1 st x = s
517 513 514 516 cbvabw y | x t 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N × 0 N | 2 nd t = N i 0 N 1 j 0 N 1 i = 1 st t / s C 1 st 1 st t N = 0 2 nd 1 st t N = N 1 st x = y = s | x t 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N × 0 N | 2 nd t = N i 0 N 1 j 0 N 1 i = 1 st t / s C 1 st 1 st t N = 0 2 nd 1 st t N = N 1 st x = s
518 499 517 eqtri 1 st t 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N × 0 N | 2 nd t = N i 0 N 1 j 0 N 1 i = 1 st t / s C 1 st 1 st t N = 0 2 nd 1 st t N = N = s | x t 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N × 0 N | 2 nd t = N i 0 N 1 j 0 N 1 i = 1 st t / s C 1 st 1 st t N = 0 2 nd 1 st t N = N 1 st x = s
519 df-rab s 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N | i 0 N 1 j 0 N 1 i = C 1 st s N = 0 2 nd s N = N = s | s 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N i 0 N 1 j 0 N 1 i = C 1 st s N = 0 2 nd s N = N
520 497 518 519 3eqtr4g φ 1 st t 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N × 0 N | 2 nd t = N i 0 N 1 j 0 N 1 i = 1 st t / s C 1 st 1 st t N = 0 2 nd 1 st t N = N = s 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N | i 0 N 1 j 0 N 1 i = C 1 st s N = 0 2 nd s N = N
521 foeq3 1 st t 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N × 0 N | 2 nd t = N i 0 N 1 j 0 N 1 i = 1 st t / s C 1 st 1 st t N = 0 2 nd 1 st t N = N = s 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N | i 0 N 1 j 0 N 1 i = C 1 st s N = 0 2 nd s N = N 1 st t 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N × 0 N | 2 nd t = N i 0 N 1 j 0 N 1 i = 1 st t / s C 1 st 1 st t N = 0 2 nd 1 st t N = N : t 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N × 0 N | 2 nd t = N i 0 N 1 j 0 N 1 i = 1 st t / s C 1 st 1 st t N = 0 2 nd 1 st t N = N onto 1 st t 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N × 0 N | 2 nd t = N i 0 N 1 j 0 N 1 i = 1 st t / s C 1 st 1 st t N = 0 2 nd 1 st t N = N 1 st t 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N × 0 N | 2 nd t = N i 0 N 1 j 0 N 1 i = 1 st t / s C 1 st 1 st t N = 0 2 nd 1 st t N = N : t 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N × 0 N | 2 nd t = N i 0 N 1 j 0 N 1 i = 1 st t / s C 1 st 1 st t N = 0 2 nd 1 st t N = N onto s 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N | i 0 N 1 j 0 N 1 i = C 1 st s N = 0 2 nd s N = N
522 520 521 syl φ 1 st t 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N × 0 N | 2 nd t = N i 0 N 1 j 0 N 1 i = 1 st t / s C 1 st 1 st t N = 0 2 nd 1 st t N = N : t 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N × 0 N | 2 nd t = N i 0 N 1 j 0 N 1 i = 1 st t / s C 1 st 1 st t N = 0 2 nd 1 st t N = N onto 1 st t 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N × 0 N | 2 nd t = N i 0 N 1 j 0 N 1 i = 1 st t / s C 1 st 1 st t N = 0 2 nd 1 st t N = N 1 st t 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N × 0 N | 2 nd t = N i 0 N 1 j 0 N 1 i = 1 st t / s C 1 st 1 st t N = 0 2 nd 1 st t N = N : t 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N × 0 N | 2 nd t = N i 0 N 1 j 0 N 1 i = 1 st t / s C 1 st 1 st t N = 0 2 nd 1 st t N = N onto s 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N | i 0 N 1 j 0 N 1 i = C 1 st s N = 0 2 nd s N = N
523 411 522 mpbii φ 1 st t 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N × 0 N | 2 nd t = N i 0 N 1 j 0 N 1 i = 1 st t / s C 1 st 1 st t N = 0 2 nd 1 st t N = N : t 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N × 0 N | 2 nd t = N i 0 N 1 j 0 N 1 i = 1 st t / s C 1 st 1 st t N = 0 2 nd 1 st t N = N onto s 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N | i 0 N 1 j 0 N 1 i = C 1 st s N = 0 2 nd s N = N
524 fof 1 st t 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N × 0 N | 2 nd t = N i 0 N 1 j 0 N 1 i = 1 st t / s C 1 st 1 st t N = 0 2 nd 1 st t N = N : t 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N × 0 N | 2 nd t = N i 0 N 1 j 0 N 1 i = 1 st t / s C 1 st 1 st t N = 0 2 nd 1 st t N = N onto s 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N | i 0 N 1 j 0 N 1 i = C 1 st s N = 0 2 nd s N = N 1 st t 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N × 0 N | 2 nd t = N i 0 N 1 j 0 N 1 i = 1 st t / s C 1 st 1 st t N = 0 2 nd 1 st t N = N : t 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N × 0 N | 2 nd t = N i 0 N 1 j 0 N 1 i = 1 st t / s C 1 st 1 st t N = 0 2 nd 1 st t N = N s 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N | i 0 N 1 j 0 N 1 i = C 1 st s N = 0 2 nd s N = N
525 523 524 syl φ 1 st t 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N × 0 N | 2 nd t = N i 0 N 1 j 0 N 1 i = 1 st t / s C 1 st 1 st t N = 0 2 nd 1 st t N = N : t 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N × 0 N | 2 nd t = N i 0 N 1 j 0 N 1 i = 1 st t / s C 1 st 1 st t N = 0 2 nd 1 st t N = N s 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N | i 0 N 1 j 0 N 1 i = C 1 st s N = 0 2 nd s N = N
526 fvres x t 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N × 0 N | 2 nd t = N i 0 N 1 j 0 N 1 i = 1 st t / s C 1 st 1 st t N = 0 2 nd 1 st t N = N 1 st t 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N × 0 N | 2 nd t = N i 0 N 1 j 0 N 1 i = 1 st t / s C 1 st 1 st t N = 0 2 nd 1 st t N = N x = 1 st x
527 fvres y t 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N × 0 N | 2 nd t = N i 0 N 1 j 0 N 1 i = 1 st t / s C 1 st 1 st t N = 0 2 nd 1 st t N = N 1 st t 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N × 0 N | 2 nd t = N i 0 N 1 j 0 N 1 i = 1 st t / s C 1 st 1 st t N = 0 2 nd 1 st t N = N y = 1 st y
528 526 527 eqeqan12d x t 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N × 0 N | 2 nd t = N i 0 N 1 j 0 N 1 i = 1 st t / s C 1 st 1 st t N = 0 2 nd 1 st t N = N y t 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N × 0 N | 2 nd t = N i 0 N 1 j 0 N 1 i = 1 st t / s C 1 st 1 st t N = 0 2 nd 1 st t N = N 1 st t 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N × 0 N | 2 nd t = N i 0 N 1 j 0 N 1 i = 1 st t / s C 1 st 1 st t N = 0 2 nd 1 st t N = N x = 1 st t 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N × 0 N | 2 nd t = N i 0 N 1 j 0 N 1 i = 1 st t / s C 1 st 1 st t N = 0 2 nd 1 st t N = N y 1 st x = 1 st y
529 simpl 2 nd t = N i 0 N 1 j 0 N 1 i = 1 st t / s C 1 st 1 st t N = 0 2 nd 1 st t N = N 2 nd t = N
530 529 a1i t 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N × 0 N 2 nd t = N i 0 N 1 j 0 N 1 i = 1 st t / s C 1 st 1 st t N = 0 2 nd 1 st t N = N 2 nd t = N
531 530 ss2rabi t 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N × 0 N | 2 nd t = N i 0 N 1 j 0 N 1 i = 1 st t / s C 1 st 1 st t N = 0 2 nd 1 st t N = N t 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N × 0 N | 2 nd t = N
532 531 sseli x t 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N × 0 N | 2 nd t = N i 0 N 1 j 0 N 1 i = 1 st t / s C 1 st 1 st t N = 0 2 nd 1 st t N = N x t 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N × 0 N | 2 nd t = N
533 412 elrab x t 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N × 0 N | 2 nd t = N x 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N × 0 N 2 nd x = N
534 532 533 sylib x t 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N × 0 N | 2 nd t = N i 0 N 1 j 0 N 1 i = 1 st t / s C 1 st 1 st t N = 0 2 nd 1 st t N = N x 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N × 0 N 2 nd x = N
535 531 sseli y t 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N × 0 N | 2 nd t = N i 0 N 1 j 0 N 1 i = 1 st t / s C 1 st 1 st t N = 0 2 nd 1 st t N = N y t 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N × 0 N | 2 nd t = N
536 fveqeq2 t = y 2 nd t = N 2 nd y = N
537 536 elrab y t 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N × 0 N | 2 nd t = N y 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N × 0 N 2 nd y = N
538 535 537 sylib y t 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N × 0 N | 2 nd t = N i 0 N 1 j 0 N 1 i = 1 st t / s C 1 st 1 st t N = 0 2 nd 1 st t N = N y 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N × 0 N 2 nd y = N
539 eqtr3 2 nd x = N 2 nd y = N 2 nd x = 2 nd y
540 xpopth x 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N × 0 N y 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N × 0 N 1 st x = 1 st y 2 nd x = 2 nd y x = y
541 540 biimpd x 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N × 0 N y 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N × 0 N 1 st x = 1 st y 2 nd x = 2 nd y x = y
542 541 ancomsd x 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N × 0 N y 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N × 0 N 2 nd x = 2 nd y 1 st x = 1 st y x = y
543 542 expdimp x 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N × 0 N y 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N × 0 N 2 nd x = 2 nd y 1 st x = 1 st y x = y
544 539 543 sylan2 x 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N × 0 N y 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N × 0 N 2 nd x = N 2 nd y = N 1 st x = 1 st y x = y
545 544 an4s x 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N × 0 N 2 nd x = N y 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N × 0 N 2 nd y = N 1 st x = 1 st y x = y
546 534 538 545 syl2an x t 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N × 0 N | 2 nd t = N i 0 N 1 j 0 N 1 i = 1 st t / s C 1 st 1 st t N = 0 2 nd 1 st t N = N y t 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N × 0 N | 2 nd t = N i 0 N 1 j 0 N 1 i = 1 st t / s C 1 st 1 st t N = 0 2 nd 1 st t N = N 1 st x = 1 st y x = y
547 528 546 sylbid x t 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N × 0 N | 2 nd t = N i 0 N 1 j 0 N 1 i = 1 st t / s C 1 st 1 st t N = 0 2 nd 1 st t N = N y t 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N × 0 N | 2 nd t = N i 0 N 1 j 0 N 1 i = 1 st t / s C 1 st 1 st t N = 0 2 nd 1 st t N = N 1 st t 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N × 0 N | 2 nd t = N i 0 N 1 j 0 N 1 i = 1 st t / s C 1 st 1 st t N = 0 2 nd 1 st t N = N x = 1 st t 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N × 0 N | 2 nd t = N i 0 N 1 j 0 N 1 i = 1 st t / s C 1 st 1 st t N = 0 2 nd 1 st t N = N y x = y
548 547 rgen2 x t 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N × 0 N | 2 nd t = N i 0 N 1 j 0 N 1 i = 1 st t / s C 1 st 1 st t N = 0 2 nd 1 st t N = N y t 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N × 0 N | 2 nd t = N i 0 N 1 j 0 N 1 i = 1 st t / s C 1 st 1 st t N = 0 2 nd 1 st t N = N 1 st t 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N × 0 N | 2 nd t = N i 0 N 1 j 0 N 1 i = 1 st t / s C 1 st 1 st t N = 0 2 nd 1 st t N = N x = 1 st t 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N × 0 N | 2 nd t = N i 0 N 1 j 0 N 1 i = 1 st t / s C 1 st 1 st t N = 0 2 nd 1 st t N = N y x = y
549 525 548 jctir φ 1 st t 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N × 0 N | 2 nd t = N i 0 N 1 j 0 N 1 i = 1 st t / s C 1 st 1 st t N = 0 2 nd 1 st t N = N : t 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N × 0 N | 2 nd t = N i 0 N 1 j 0 N 1 i = 1 st t / s C 1 st 1 st t N = 0 2 nd 1 st t N = N s 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N | i 0 N 1 j 0 N 1 i = C 1 st s N = 0 2 nd s N = N x t 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N × 0 N | 2 nd t = N i 0 N 1 j 0 N 1 i = 1 st t / s C 1 st 1 st t N = 0 2 nd 1 st t N = N y t 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N × 0 N | 2 nd t = N i 0 N 1 j 0 N 1 i = 1 st t / s C 1 st 1 st t N = 0 2 nd 1 st t N = N 1 st t 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N × 0 N | 2 nd t = N i 0 N 1 j 0 N 1 i = 1 st t / s C 1 st 1 st t N = 0 2 nd 1 st t N = N x = 1 st t 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N × 0 N | 2 nd t = N i 0 N 1 j 0 N 1 i = 1 st t / s C 1 st 1 st t N = 0 2 nd 1 st t N = N y x = y
550 dff13 1 st t 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N × 0 N | 2 nd t = N i 0 N 1 j 0 N 1 i = 1 st t / s C 1 st 1 st t N = 0 2 nd 1 st t N = N : t 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N × 0 N | 2 nd t = N i 0 N 1 j 0 N 1 i = 1 st t / s C 1 st 1 st t N = 0 2 nd 1 st t N = N 1-1 s 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N | i 0 N 1 j 0 N 1 i = C 1 st s N = 0 2 nd s N = N 1 st t 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N × 0 N | 2 nd t = N i 0 N 1 j 0 N 1 i = 1 st t / s C 1 st 1 st t N = 0 2 nd 1 st t N = N : t 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N × 0 N | 2 nd t = N i 0 N 1 j 0 N 1 i = 1 st t / s C 1 st 1 st t N = 0 2 nd 1 st t N = N s 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N | i 0 N 1 j 0 N 1 i = C 1 st s N = 0 2 nd s N = N x t 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N × 0 N | 2 nd t = N i 0 N 1 j 0 N 1 i = 1 st t / s C 1 st 1 st t N = 0 2 nd 1 st t N = N y t 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N × 0 N | 2 nd t = N i 0 N 1 j 0 N 1 i = 1 st t / s C 1 st 1 st t N = 0 2 nd 1 st t N = N 1 st t 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N × 0 N | 2 nd t = N i 0 N 1 j 0 N 1 i = 1 st t / s C 1 st 1 st t N = 0 2 nd 1 st t N = N x = 1 st t 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N × 0 N | 2 nd t = N i 0 N 1 j 0 N 1 i = 1 st t / s C 1 st 1 st t N = 0 2 nd 1 st t N = N y x = y
551 549 550 sylibr φ 1 st t 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N × 0 N | 2 nd t = N i 0 N 1 j 0 N 1 i = 1 st t / s C 1 st 1 st t N = 0 2 nd 1 st t N = N : t 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N × 0 N | 2 nd t = N i 0 N 1 j 0 N 1 i = 1 st t / s C 1 st 1 st t N = 0 2 nd 1 st t N = N 1-1 s 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N | i 0 N 1 j 0 N 1 i = C 1 st s N = 0 2 nd s N = N
552 df-f1o 1 st t 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N × 0 N | 2 nd t = N i 0 N 1 j 0 N 1 i = 1 st t / s C 1 st 1 st t N = 0 2 nd 1 st t N = N : t 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N × 0 N | 2 nd t = N i 0 N 1 j 0 N 1 i = 1 st t / s C 1 st 1 st t N = 0 2 nd 1 st t N = N 1-1 onto s 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N | i 0 N 1 j 0 N 1 i = C 1 st s N = 0 2 nd s N = N 1 st t 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N × 0 N | 2 nd t = N i 0 N 1 j 0 N 1 i = 1 st t / s C 1 st 1 st t N = 0 2 nd 1 st t N = N : t 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N × 0 N | 2 nd t = N i 0 N 1 j 0 N 1 i = 1 st t / s C 1 st 1 st t N = 0 2 nd 1 st t N = N 1-1 s 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N | i 0 N 1 j 0 N 1 i = C 1 st s N = 0 2 nd s N = N 1 st t 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N × 0 N | 2 nd t = N i 0 N 1 j 0 N 1 i = 1 st t / s C 1 st 1 st t N = 0 2 nd 1 st t N = N : t 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N × 0 N | 2 nd t = N i 0 N 1 j 0 N 1 i = 1 st t / s C 1 st 1 st t N = 0 2 nd 1 st t N = N onto s 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N | i 0 N 1 j 0 N 1 i = C 1 st s N = 0 2 nd s N = N
553 551 523 552 sylanbrc φ 1 st t 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N × 0 N | 2 nd t = N i 0 N 1 j 0 N 1 i = 1 st t / s C 1 st 1 st t N = 0 2 nd 1 st t N = N : t 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N × 0 N | 2 nd t = N i 0 N 1 j 0 N 1 i = 1 st t / s C 1 st 1 st t N = 0 2 nd 1 st t N = N 1-1 onto s 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N | i 0 N 1 j 0 N 1 i = C 1 st s N = 0 2 nd s N = N
554 rabfi 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N × 0 N Fin t 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N × 0 N | 2 nd t = N i 0 N 1 j 0 N 1 i = 1 st t / s C 1 st 1 st t N = 0 2 nd 1 st t N = N Fin
555 32 554 ax-mp t 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N × 0 N | 2 nd t = N i 0 N 1 j 0 N 1 i = 1 st t / s C 1 st 1 st t N = 0 2 nd 1 st t N = N Fin
556 555 elexi t 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N × 0 N | 2 nd t = N i 0 N 1 j 0 N 1 i = 1 st t / s C 1 st 1 st t N = 0 2 nd 1 st t N = N V
557 556 f1oen 1 st t 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N × 0 N | 2 nd t = N i 0 N 1 j 0 N 1 i = 1 st t / s C 1 st 1 st t N = 0 2 nd 1 st t N = N : t 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N × 0 N | 2 nd t = N i 0 N 1 j 0 N 1 i = 1 st t / s C 1 st 1 st t N = 0 2 nd 1 st t N = N 1-1 onto s 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N | i 0 N 1 j 0 N 1 i = C 1 st s N = 0 2 nd s N = N t 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N × 0 N | 2 nd t = N i 0 N 1 j 0 N 1 i = 1 st t / s C 1 st 1 st t N = 0 2 nd 1 st t N = N s 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N | i 0 N 1 j 0 N 1 i = C 1 st s N = 0 2 nd s N = N
558 553 557 syl φ t 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N × 0 N | 2 nd t = N i 0 N 1 j 0 N 1 i = 1 st t / s C 1 st 1 st t N = 0 2 nd 1 st t N = N s 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N | i 0 N 1 j 0 N 1 i = C 1 st s N = 0 2 nd s N = N
559 rabfi 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N Fin s 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N | i 0 N 1 j 0 N 1 i = C 1 st s N = 0 2 nd s N = N Fin
560 29 559 ax-mp s 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N | i 0 N 1 j 0 N 1 i = C 1 st s N = 0 2 nd s N = N Fin
561 hashen t 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N × 0 N | 2 nd t = N i 0 N 1 j 0 N 1 i = 1 st t / s C 1 st 1 st t N = 0 2 nd 1 st t N = N Fin s 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N | i 0 N 1 j 0 N 1 i = C 1 st s N = 0 2 nd s N = N Fin t 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N × 0 N | 2 nd t = N i 0 N 1 j 0 N 1 i = 1 st t / s C 1 st 1 st t N = 0 2 nd 1 st t N = N = s 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N | i 0 N 1 j 0 N 1 i = C 1 st s N = 0 2 nd s N = N t 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N × 0 N | 2 nd t = N i 0 N 1 j 0 N 1 i = 1 st t / s C 1 st 1 st t N = 0 2 nd 1 st t N = N s 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N | i 0 N 1 j 0 N 1 i = C 1 st s N = 0 2 nd s N = N
562 555 560 561 mp2an t 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N × 0 N | 2 nd t = N i 0 N 1 j 0 N 1 i = 1 st t / s C 1 st 1 st t N = 0 2 nd 1 st t N = N = s 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N | i 0 N 1 j 0 N 1 i = C 1 st s N = 0 2 nd s N = N t 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N × 0 N | 2 nd t = N i 0 N 1 j 0 N 1 i = 1 st t / s C 1 st 1 st t N = 0 2 nd 1 st t N = N s 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N | i 0 N 1 j 0 N 1 i = C 1 st s N = 0 2 nd s N = N
563 558 562 sylibr φ t 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N × 0 N | 2 nd t = N i 0 N 1 j 0 N 1 i = 1 st t / s C 1 st 1 st t N = 0 2 nd 1 st t N = N = s 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N | i 0 N 1 j 0 N 1 i = C 1 st s N = 0 2 nd s N = N
564 563 oveq2d φ t 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N × 0 N | i 0 N 1 j 0 N 2 nd t i = 1 st t / s C t 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N × 0 N | 2 nd t = N i 0 N 1 j 0 N 1 i = 1 st t / s C 1 st 1 st t N = 0 2 nd 1 st t N = N = t 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N × 0 N | i 0 N 1 j 0 N 2 nd t i = 1 st t / s C s 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N | i 0 N 1 j 0 N 1 i = C 1 st s N = 0 2 nd s N = N
565 205 401 564 3eqtr3d φ x 0 K 1 N 0 N 1 t 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N × 0 N | x = y 0 N 1 if y < 2 nd t y y + 1 / j 1 st 1 st t + f 2 nd 1 st t 1 j × 1 2 nd 1 st t j + 1 N × 0 0 N 1 ran p ran x B n 1 N p ran x p n 0 p ran x p n K = t 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N × 0 N | i 0 N 1 j 0 N 2 nd t i = 1 st t / s C s 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N | i 0 N 1 j 0 N 1 i = C 1 st s N = 0 2 nd s N = N
566 168 565 breqtrd φ 2 t 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N × 0 N | i 0 N 1 j 0 N 2 nd t i = 1 st t / s C s 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N | i 0 N 1 j 0 N 1 i = C 1 st s N = 0 2 nd s N = N