Metamath Proof Explorer


Theorem poimirlem28

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

Ref Expression
Hypotheses poimir.0 φ 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
poimirlem28.5 φ K
Assertion poimirlem28 φ s 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N i 0 N j 0 N i = C

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