Step | Hyp | Ref
| Expression |
1 | | fzofi 12773 |
. . . . . 6
..^ |
2 | | fzfi 12771 |
. . . . . 6
|
3 | | mapfi 8262 |
. . . . . 6
..^ ..^ |
4 | 1, 2, 3 | mp2an 708 |
. . . . 5
..^ |
5 | | mapfi 8262 |
. . . . . . 7
|
6 | 2, 2, 5 | mp2an 708 |
. . . . . 6
|
7 | | f1of 6137 |
. . . . . . . 8
|
8 | 7 | ss2abi 3674 |
. . . . . . 7
|
9 | | ovex 6678 |
. . . . . . . 8
|
10 | 9, 9 | mapval 7869 |
. . . . . . 7
|
11 | 8, 10 | sseqtr4i 3638 |
. . . . . 6
|
12 | | ssfi 8180 |
. . . . . 6
|
13 | 6, 11, 12 | mp2an 708 |
. . . . 5
|
14 | 4, 13 | pm3.2i 471 |
. . . 4
..^
|
15 | | xpfi 8231 |
. . . 4
..^ ..^ |
16 | 14, 15 | mp1i 13 |
. . 3
..^ |
17 | | 2z 11409 |
. . . 4
|
18 | 17 | a1i 11 |
. . 3
|
19 | | snfi 8038 |
. . . . . . 7
|
20 | | fzfi 12771 |
. . . . . . . 8
|
21 | | rabfi 8185 |
. . . . . . . 8
|
22 | 20, 21 | ax-mp 5 |
. . . . . . 7
|
23 | | xpfi 8231 |
. . . . . . 7
|
24 | 19, 22, 23 | mp2an 708 |
. . . . . 6
|
25 | | hashcl 13147 |
. . . . . 6
|
26 | 24, 25 | ax-mp 5 |
. . . . 5
|
27 | 26 | nn0zi 11402 |
. . . 4
|
28 | 27 | a1i 11 |
. . 3
..^
|
29 | | poimir.0 |
. . . . . . . . 9
|
30 | 29 | ad2antrr 762 |
. . . . . . . 8
..^
|
31 | | nfv 1843 |
. . . . . . . . . 10
|
32 | | nfcsb1v 3549 |
. . . . . . . . . . 11
|
33 | 32 | nfeq2 2780 |
. . . . . . . . . 10
|
34 | 31, 33 | nfim 1825 |
. . . . . . . . 9
|
35 | | oveq2 6658 |
. . . . . . . . . . . . . . 15
|
36 | 35 | imaeq2d 5466 |
. . . . . . . . . . . . . 14
|
37 | 36 | xpeq1d 5138 |
. . . . . . . . . . . . 13
|
38 | | oveq1 6657 |
. . . . . . . . . . . . . . . 16
|
39 | 38 | oveq1d 6665 |
. . . . . . . . . . . . . . 15
|
40 | 39 | imaeq2d 5466 |
. . . . . . . . . . . . . 14
|
41 | 40 | xpeq1d 5138 |
. . . . . . . . . . . . 13
|
42 | 37, 41 | uneq12d 3768 |
. . . . . . . . . . . 12
|
43 | 42 | oveq2d 6666 |
. . . . . . . . . . 11
|
44 | 43 | eqeq2d 2632 |
. . . . . . . . . 10
|
45 | | csbeq1a 3542 |
. . . . . . . . . . 11
|
46 | 45 | eqeq2d 2632 |
. . . . . . . . . 10
|
47 | 44, 46 | imbi12d 334 |
. . . . . . . . 9
|
48 | | nfv 1843 |
. . . . . . . . . . 11
|
49 | | nfcsb1v 3549 |
. . . . . . . . . . . 12
|
50 | 49 | nfeq2 2780 |
. . . . . . . . . . 11
|
51 | 48, 50 | nfim 1825 |
. . . . . . . . . 10
|
52 | | fveq2 6191 |
. . . . . . . . . . . . 13
|
53 | | fveq2 6191 |
. . . . . . . . . . . . . . . 16
|
54 | 53 | imaeq1d 5465 |
. . . . . . . . . . . . . . 15
|
55 | 54 | xpeq1d 5138 |
. . . . . . . . . . . . . 14
|
56 | 53 | imaeq1d 5465 |
. . . . . . . . . . . . . . 15
|
57 | 56 | xpeq1d 5138 |
. . . . . . . . . . . . . 14
|
58 | 55, 57 | uneq12d 3768 |
. . . . . . . . . . . . 13
|
59 | 52, 58 | oveq12d 6668 |
. . . . . . . . . . . 12
|
60 | 59 | eqeq2d 2632 |
. . . . . . . . . . 11
|
61 | | csbeq1a 3542 |
. . . . . . . . . . . 12
|
62 | 61 | eqeq2d 2632 |
. . . . . . . . . . 11
|
63 | 60, 62 | imbi12d 334 |
. . . . . . . . . 10
|
64 | | poimirlem28.1 |
. . . . . . . . . 10
|
65 | 51, 63, 64 | chvar 2262 |
. . . . . . . . 9
|
66 | 34, 47, 65 | chvar 2262 |
. . . . . . . 8
|
67 | | poimirlem28.2 |
. . . . . . . . 9
|
68 | 67 | ad4ant14 1293 |
. . . . . . . 8
..^
|
69 | | xp1st 7198 |
. . . . . . . . . 10
..^ ..^ |
70 | | elmapi 7879 |
. . . . . . . . . 10
..^ ..^ |
71 | 69, 70 | syl 17 |
. . . . . . . . 9
..^ ..^ |
72 | 71 | ad2antlr 763 |
. . . . . . . 8
..^
..^ |
73 | | xp2nd 7199 |
. . . . . . . . . 10
..^ |
74 | | fvex 6201 |
. . . . . . . . . . 11
|
75 | | f1oeq1 6127 |
. . . . . . . . . . 11
|
76 | 74, 75 | elab 3350 |
. . . . . . . . . 10
|
77 | 73, 76 | sylib 208 |
. . . . . . . . 9
..^ |
78 | 77 | ad2antlr 763 |
. . . . . . . 8
..^
|
79 | | nfcv 2764 |
. . . . . . . . . . . . 13
|
80 | | nfcv 2764 |
. . . . . . . . . . . . . 14
|
81 | 80, 32 | nfcsb 3551 |
. . . . . . . . . . . . 13
|
82 | 79, 81 | nfne 2894 |
. . . . . . . . . . . 12
|
83 | | nfcv 2764 |
. . . . . . . . . . . . . . 15
|
84 | 83, 49, 61 | cbvcsb 3538 |
. . . . . . . . . . . . . 14
|
85 | 45 | csbeq2dv 3992 |
. . . . . . . . . . . . . 14
|
86 | 84, 85 | syl5eq 2668 |
. . . . . . . . . . . . 13
|
87 | 86 | neeq2d 2854 |
. . . . . . . . . . . 12
|
88 | 82, 87 | rspc 3303 |
. . . . . . . . . . 11
|
89 | 88 | impcom 446 |
. . . . . . . . . 10
|
90 | 89 | adantll 750 |
. . . . . . . . 9
..^
|
91 | | 1st2nd2 7205 |
. . . . . . . . . . 11
..^
|
92 | 91 | csbeq1d 3540 |
. . . . . . . . . 10
..^
|
93 | 92 | ad3antlr 767 |
. . . . . . . . 9
..^
|
94 | 90, 93 | neeqtrd 2863 |
. . . . . . . 8
..^
|
95 | 30, 66, 68, 72, 78, 94 | poimirlem25 33434 |
. . . . . . 7
..^
|
96 | | nfv 1843 |
. . . . . . . . . . . . . 14
|
97 | 81 | nfeq2 2780 |
. . . . . . . . . . . . . 14
|
98 | 86 | eqeq2d 2632 |
. . . . . . . . . . . . . 14
|
99 | 96, 97, 98 | cbvrex 3168 |
. . . . . . . . . . . . 13
|
100 | 92 | eqeq2d 2632 |
. . . . . . . . . . . . . 14
..^
|
101 | 100 | rexbidv 3052 |
. . . . . . . . . . . . 13
..^
|
102 | 99, 101 | syl5rbb 273 |
. . . . . . . . . . . 12
..^
|
103 | 102 | ralbidv 2986 |
. . . . . . . . . . 11
..^
|
104 | | iba 524 |
. . . . . . . . . . 11
|
105 | 103, 104 | sylan9bb 736 |
. . . . . . . . . 10
..^
|
106 | 105 | rabbidv 3189 |
. . . . . . . . 9
..^
|
107 | 106 | fveq2d 6195 |
. . . . . . . 8
..^
|
108 | 107 | adantll 750 |
. . . . . . 7
..^
|
109 | 95, 108 | breqtrd 4679 |
. . . . . 6
..^
|
110 | 109 | ex 450 |
. . . . 5
..^
|
111 | | dvds0 14997 |
. . . . . . . 8
|
112 | 17, 111 | ax-mp 5 |
. . . . . . 7
|
113 | | hash0 13158 |
. . . . . . 7
|
114 | 112, 113 | breqtrri 4680 |
. . . . . 6
|
115 | | simpr 477 |
. . . . . . . . . 10
|
116 | 115 | con3i 150 |
. . . . . . . . 9
|
117 | 116 | ralrimivw 2967 |
. . . . . . . 8
|
118 | | rabeq0 3957 |
. . . . . . . 8
|
119 | 117, 118 | sylibr 224 |
. . . . . . 7
|
120 | 119 | fveq2d 6195 |
. . . . . 6
|
121 | 114, 120 | syl5breqr 4691 |
. . . . 5
|
122 | 110, 121 | pm2.61d1 171 |
. . . 4
..^
|
123 | | hashxp 13221 |
. . . . . 6
|
124 | 19, 22, 123 | mp2an 708 |
. . . . 5
|
125 | | vex 3203 |
. . . . . . 7
|
126 | | hashsng 13159 |
. . . . . . 7
|
127 | 125, 126 | ax-mp 5 |
. . . . . 6
|
128 | 127 | oveq1i 6660 |
. . . . 5
|
129 | | hashcl 13147 |
. . . . . . . 8
|
130 | 22, 129 | ax-mp 5 |
. . . . . . 7
|
131 | 130 | nn0cni 11304 |
. . . . . 6
|
132 | 131 | mulid2i 10043 |
. . . . 5
|
133 | 124, 128,
132 | 3eqtri 2648 |
. . . 4
|
134 | 122, 133 | syl6breqr 4695 |
. . 3
..^
|
135 | 16, 18, 28, 134 | fsumdvds 15030 |
. 2
..^
|
136 | 4, 13, 15 | mp2an 708 |
. . . . . 6
..^ |
137 | | xpfi 8231 |
. . . . . 6
..^ ..^ |
138 | 136, 20, 137 | mp2an 708 |
. . . . 5
..^ |
139 | | rabfi 8185 |
. . . . 5
..^ ..^
|
140 | 138, 139 | ax-mp 5 |
. . . 4
..^
|
141 | 29 | nncnd 11036 |
. . . . . . . . . . . 12
|
142 | | npcan1 10455 |
. . . . . . . . . . . 12
|
143 | 141, 142 | syl 17 |
. . . . . . . . . . 11
|
144 | | nnm1nn0 11334 |
. . . . . . . . . . . . . 14
|
145 | 29, 144 | syl 17 |
. . . . . . . . . . . . 13
|
146 | 145 | nn0zd 11480 |
. . . . . . . . . . . 12
|
147 | | uzid 11702 |
. . . . . . . . . . . 12
|
148 | | peano2uz 11741 |
. . . . . . . . . . . 12
|
149 | 146, 147,
148 | 3syl 18 |
. . . . . . . . . . 11
|
150 | 143, 149 | eqeltrrd 2702 |
. . . . . . . . . 10
|
151 | | fzss2 12381 |
. . . . . . . . . 10
|
152 | | ssralv 3666 |
. . . . . . . . . 10
|
153 | 150, 151,
152 | 3syl 18 |
. . . . . . . . 9
|
154 | 153 | adantr 481 |
. . . . . . . 8
|
155 | | raldifb 3750 |
. . . . . . . . . . . 12
|
156 | | nfv 1843 |
. . . . . . . . . . . . . . 15
|
157 | | nfcsb1v 3549 |
. . . . . . . . . . . . . . . 16
|
158 | 157 | nfeq2 2780 |
. . . . . . . . . . . . . . 15
|
159 | 156, 158 | nfan 1828 |
. . . . . . . . . . . . . 14
|
160 | | nfv 1843 |
. . . . . . . . . . . . . 14
|
161 | 159, 160 | nfan 1828 |
. . . . . . . . . . . . 13
|
162 | | nnel 2906 |
. . . . . . . . . . . . . . . . 17
|
163 | | velsn 4193 |
. . . . . . . . . . . . . . . . 17
|
164 | 162, 163 | bitri 264 |
. . . . . . . . . . . . . . . 16
|
165 | | csbeq1a 3542 |
. . . . . . . . . . . . . . . . . . . . 21
|
166 | 165 | eqeq2d 2632 |
. . . . . . . . . . . . . . . . . . . 20
|
167 | 166 | biimparc 504 |
. . . . . . . . . . . . . . . . . . 19
|
168 | 29 | nnred 11035 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
|
169 | 168 | ltm1d 10956 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
|
170 | 145 | nn0red 11352 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
|
171 | 170, 168 | ltnled 10184 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
|
172 | 169, 171 | mpbid 222 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
173 | | elfzle2 12345 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
174 | 172, 173 | nsyl 135 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
175 | | eleq1 2689 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
176 | 175 | notbid 308 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
177 | 174, 176 | syl5ibrcom 237 |
. . . . . . . . . . . . . . . . . . . . . 22
|
178 | 177 | con2d 129 |
. . . . . . . . . . . . . . . . . . . . 21
|
179 | 178 | imp 445 |
. . . . . . . . . . . . . . . . . . . 20
|
180 | | eqeq2 2633 |
. . . . . . . . . . . . . . . . . . . . 21
|
181 | 180 | notbid 308 |
. . . . . . . . . . . . . . . . . . . 20
|
182 | 179, 181 | syl5ibcom 235 |
. . . . . . . . . . . . . . . . . . 19
|
183 | 167, 182 | syl5 34 |
. . . . . . . . . . . . . . . . . 18
|
184 | 183 | expdimp 453 |
. . . . . . . . . . . . . . . . 17
|
185 | 184 | an32s 846 |
. . . . . . . . . . . . . . . 16
|
186 | 164, 185 | syl5bi 232 |
. . . . . . . . . . . . . . 15
|
187 | | idd 24 |
. . . . . . . . . . . . . . 15
|
188 | 186, 187 | jad 174 |
. . . . . . . . . . . . . 14
|
189 | 188 | adantr 481 |
. . . . . . . . . . . . 13
|
190 | 161, 189 | ralimdaa 2958 |
. . . . . . . . . . . 12
|
191 | 155, 190 | syl5bir 233 |
. . . . . . . . . . 11
|
192 | 191 | con3d 148 |
. . . . . . . . . 10
|
193 | | dfrex2 2996 |
. . . . . . . . . 10
|
194 | | dfrex2 2996 |
. . . . . . . . . 10
|
195 | 192, 193,
194 | 3imtr4g 285 |
. . . . . . . . 9
|
196 | 195 | ralimdva 2962 |
. . . . . . . 8
|
197 | 154, 196 | syld 47 |
. . . . . . 7
|
198 | 197 | expimpd 629 |
. . . . . 6
|
199 | 198 | adantr 481 |
. . . . 5
..^
|
200 | 199 | ss2rabdv 3683 |
. . . 4
..^ ..^
|
201 | | hashssdif 13200 |
. . . 4
..^
..^ ..^
..^
..^ ..^
..^
|
202 | 140, 200,
201 | sylancr 695 |
. . 3
..^
..^ ..^
..^
|
203 | | xp2nd 7199 |
. . . . . . . 8
..^ |
204 | | df-ne 2795 |
. . . . . . . . . . . 12
|
205 | 204 | ralbii 2980 |
. . . . . . . . . . 11
|
206 | | ralnex 2992 |
. . . . . . . . . . 11
|
207 | 205, 206 | bitri 264 |
. . . . . . . . . 10
|
208 | 29 | nnnn0d 11351 |
. . . . . . . . . . . . . . . . . . 19
|
209 | | nn0uz 11722 |
. . . . . . . . . . . . . . . . . . 19
|
210 | 208, 209 | syl6eleq 2711 |
. . . . . . . . . . . . . . . . . 18
|
211 | 143, 210 | eqeltrd 2701 |
. . . . . . . . . . . . . . . . 17
|
212 | | fzsplit2 12366 |
. . . . . . . . . . . . . . . . 17
|
213 | 211, 150,
212 | syl2anc 693 |
. . . . . . . . . . . . . . . 16
|
214 | 143 | oveq1d 6665 |
. . . . . . . . . . . . . . . . . 18
|
215 | 29 | nnzd 11481 |
. . . . . . . . . . . . . . . . . . 19
|
216 | | fzsn 12383 |
. . . . . . . . . . . . . . . . . . 19
|
217 | 215, 216 | syl 17 |
. . . . . . . . . . . . . . . . . 18
|
218 | 214, 217 | eqtrd 2656 |
. . . . . . . . . . . . . . . . 17
|
219 | 218 | uneq2d 3767 |
. . . . . . . . . . . . . . . 16
|
220 | 213, 219 | eqtrd 2656 |
. . . . . . . . . . . . . . 15
|
221 | 220 | raleqdv 3144 |
. . . . . . . . . . . . . 14
|
222 | | difss 3737 |
. . . . . . . . . . . . . . . . . 18
|
223 | | ssrexv 3667 |
. . . . . . . . . . . . . . . . . 18
|
224 | 222, 223 | ax-mp 5 |
. . . . . . . . . . . . . . . . 17
|
225 | 224 | ralimi 2952 |
. . . . . . . . . . . . . . . 16
|
226 | 225 | biantrurd 529 |
. . . . . . . . . . . . . . 15
|
227 | | ralunb 3794 |
. . . . . . . . . . . . . . 15
|
228 | 226, 227 | syl6rbbr 279 |
. . . . . . . . . . . . . 14
|
229 | 221, 228 | sylan9bb 736 |
. . . . . . . . . . . . 13
|
230 | 229 | adantlr 751 |
. . . . . . . . . . . 12
|
231 | | nn0fz0 12437 |
. . . . . . . . . . . . . . . 16
|
232 | 208, 231 | sylib 208 |
. . . . . . . . . . . . . . 15
|
233 | 232 | ad2antrr 762 |
. . . . . . . . . . . . . 14
|
234 | | eqeq1 2626 |
. . . . . . . . . . . . . . . . 17
|
235 | 234 | rexbidv 3052 |
. . . . . . . . . . . . . . . 16
|
236 | 235 | rspcva 3307 |
. . . . . . . . . . . . . . 15
|
237 | | nfv 1843 |
. . . . . . . . . . . . . . . . 17
|
238 | | nfcv 2764 |
. . . . . . . . . . . . . . . . . 18
|
239 | | nfre1 3005 |
. . . . . . . . . . . . . . . . . 18
|
240 | 238, 239 | nfral 2945 |
. . . . . . . . . . . . . . . . 17
|
241 | 237, 240 | nfan 1828 |
. . . . . . . . . . . . . . . 16
|
242 | | eleq1 2689 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
243 | 242 | notbid 308 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
244 | 174, 243 | syl5ibcom 235 |
. . . . . . . . . . . . . . . . . . . . . 22
|
245 | 244 | ad3antrrr 766 |
. . . . . . . . . . . . . . . . . . . . 21
|
246 | | eldifsn 4317 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
247 | | diffi 8192 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
|
248 | 20, 247 | ax-mp 5 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
|
249 | | ssrab2 3687 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
|
250 | | ssdomg 8001 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
|
251 | 248, 249,
250 | mp2 9 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
|
252 | | hashdifsn 13202 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
|
253 | 20, 252 | mpan 706 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
|
254 | | 1cnd 10056 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
|
255 | 141, 254,
254 | addsubd 10413 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
|
256 | | hashfz0 13219 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
|
257 | 208, 256 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
|
258 | 257 | oveq1d 6665 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
|
259 | | hashfz0 13219 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
|
260 | 145, 259 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
|
261 | 255, 258,
260 | 3eqtr4d 2666 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
|
262 | 253, 261 | sylan9eqr 2678 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
|
263 | | fzfi 12771 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
|
264 | | hashen 13135 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
|
265 | 248, 263,
264 | mp2an 708 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
|
266 | 262, 265 | sylib 208 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
|
267 | | rabfi 8185 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
|
268 | 248, 267 | ax-mp 5 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
|
269 | | eleq1 2689 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . 41
|
270 | 269 | biimpac 503 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . 40
|
271 | | rabid 3116 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . 41
|
272 | 271 | simplbi2com 657 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . 40
|
273 | 270, 272 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . 39
|
274 | 273 | impancom 456 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . 38
|
275 | 274 | ancrd 577 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
|
276 | 275 | expimpd 629 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
|
277 | 276 | reximdv2 3014 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
|
278 | 271 | simplbi 476 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . 38
|
279 | 274 | pm4.71rd 667 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . 39
|
280 | | df-mpt 4730 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . 42
|
281 | | nfv 1843 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . 43
|
282 | | nfrab1 3122 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . 45
|
283 | 282 | nfcri 2758 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . 44
|
284 | | nfcsb1v 3549 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . 45
|
285 | 284 | nfeq2 2780 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . 44
|
286 | 283, 285 | nfan 1828 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . 43
|
287 | | eleq1 2689 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . 44
|
288 | | csbeq1a 3542 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . 45
|
289 | 288 | eqeq2d 2632 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . 44
|
290 | 287, 289 | anbi12d 747 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . 43
|
291 | 281, 286,
290 | cbvopab1 4723 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . 42
|
292 | 280, 291 | eqtr4i 2647 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . 41
|
293 | 292 | breqi 4659 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . 40
|
294 | | df-br 4654 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . 40
|
295 | | opabid 4982 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . 40
|
296 | 293, 294,
295 | 3bitri 286 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . 39
|
297 | 279, 296 | syl6bbr 278 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . 38
|
298 | 278, 297 | sylan2 491 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
|
299 | 298 | rexbidva 3049 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
|
300 | | nfcv 2764 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
|
301 | | nfv 1843 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
|
302 | | nfcv 2764 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . 38
|
303 | 282, 284 | nfmpt 4746 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . 38
|
304 | | nfcv 2764 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . 38
|
305 | 302, 303,
304 | nfbr 4699 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
|
306 | | breq1 4656 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
|
307 | 282, 300,
301, 305, 306 | cbvrexf 3166 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
|
308 | 299, 307 | syl6bb 276 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
|
309 | 277, 308 | sylibd 229 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
|
310 | 309 | ralimia 2950 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
|
311 | | eqid 2622 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
|
312 | | nfcv 2764 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
|
313 | | nfcv 2764 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
|
314 | 284 | nfel1 2779 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
|
315 | 288 | eleq1d 2686 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
|
316 | 312, 313,
314, 315 | elrabf 3360 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
|
317 | 316 | simprbi 480 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
|
318 | 311, 317 | fmpti 6383 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
|
319 | 310, 318 | jctil 560 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
|
320 | | dffo4 6375 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
|
321 | 319, 320 | sylibr 224 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
|
322 | | fodomfi 8239 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
|
323 | 268, 321,
322 | sylancr 695 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
|
324 | | endomtr 8014 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
|
325 | 266, 323,
324 | syl2an 494 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
|
326 | | sbth 8080 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
|
327 | 251, 325,
326 | sylancr 695 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
|
328 | | fisseneq 8171 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
|
329 | 248, 249,
327, 328 | mp3an12i 1428 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
|
330 | 329 | eleq2d 2687 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
|
331 | 330 | biimpar 502 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
|
332 | 288 | equcoms 1947 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
|
333 | 332 | eqcomd 2628 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
|
334 | 333 | eleq1d 2686 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
|
335 | 334, 317 | vtoclga 3272 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
|
336 | 331, 335 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
337 | 246, 336 | sylan2br 493 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
338 | 337 | expr 643 |
. . . . . . . . . . . . . . . . . . . . . 22
|
339 | 338 | necon1bd 2812 |
. . . . . . . . . . . . . . . . . . . . 21
|
340 | 245, 339 | syld 47 |
. . . . . . . . . . . . . . . . . . . 20
|
341 | 340 | imp 445 |
. . . . . . . . . . . . . . . . . . 19
|
342 | 341, 165 | syl 17 |
. . . . . . . . . . . . . . . . . 18
|
343 | | eqtr 2641 |
. . . . . . . . . . . . . . . . . . . 20
|
344 | 343 | ex 450 |
. . . . . . . . . . . . . . . . . . 19
|
345 | 344 | adantl 482 |
. . . . . . . . . . . . . . . . . 18
|
346 | 342, 345 | mpd 15 |
. . . . . . . . . . . . . . . . 17
|
347 | 346 | exp31 630 |
. . . . . . . . . . . . . . . 16
|
348 | 241, 158,
347 | rexlimd 3026 |
. . . . . . . . . . . . . . 15
|
349 | 236, 348 | syl5 34 |
. . . . . . . . . . . . . 14
|
350 | 233, 349 | mpand 711 |
. . . . . . . . . . . . 13
|
351 | 350 | pm4.71rd 667 |
. . . . . . . . . . . 12
|
352 | 235 | ralsng 4218 |
. . . . . . . . . . . . . 14
|
353 | 29, 352 | syl 17 |
. . . . . . . . . . . . 13
|
354 | 353 | ad2antrr 762 |
. . . . . . . . . . . 12
|
355 | 230, 351,
354 | 3bitr3rd 299 |
. . . . . . . . . . 11
|
356 | 355 | notbid 308 |
. . . . . . . . . 10
|
357 | 207, 356 | syl5bb 272 |
. . . . . . . . 9
|
358 | 357 | pm5.32da 673 |
. . . . . . . 8
|
359 | 203, 358 | sylan2 491 |
. . . . . . 7
..^
|
360 | 359 | rabbidva 3188 |
. . . . . 6
..^
..^
|
361 | | nfv 1843 |
. . . . . . . . . . . 12
|
362 | | nfv 1843 |
. . . . . . . . . . . . 13
..^ |
363 | | nfrab1 3122 |
. . . . . . . . . . . . . 14
|
364 | 363 | nfcri 2758 |
. . . . . . . . . . . . 13
|
365 | 362, 364 | nfan 1828 |
. . . . . . . . . . . 12
..^
|
366 | 361, 365 | nfan 1828 |
. . . . . . . . . . 11
..^
|
367 | | nfv 1843 |
. . . . . . . . . . 11
..^
|
368 | | opeq2 4403 |
. . . . . . . . . . . . 13
|
369 | 368 | eqeq2d 2632 |
. . . . . . . . . . . 12
|
370 | | eleq1 2689 |
. . . . . . . . . . . . . . 15
|
371 | | rabid 3116 |
. . . . . . . . . . . . . . 15
|
372 | 370, 371 | syl6bb 276 |
. . . . . . . . . . . . . 14
|
373 | 372 | anbi2d 740 |
. . . . . . . . . . . . 13
..^
..^
|
374 | | 3anass 1042 |
. . . . . . . . . . . . 13
..^
..^
|
375 | 373, 374 | syl6bbr 278 |
. . . . . . . . . . . 12
..^
..^
|
376 | 369, 375 | anbi12d 747 |
. . . . . . . . . . 11
..^
..^
|
377 | 366, 367,
376 | cbvex 2272 |
. . . . . . . . . 10
..^
..^
|
378 | 377 | exbii 1774 |
. . . . . . . . 9
..^
..^
|
379 | | eliunxp 5259 |
. . . . . . . . 9
..^
..^
|
380 | | elopab 4983 |
. . . . . . . . 9
..^
..^
|
381 | 378, 379,
380 | 3bitr4i 292 |
. . . . . . . 8
..^
..^
|
382 | 381 | eqriv 2619 |
. . . . . . 7
..^
..^
|
383 | | vex 3203 |
. . . . . . . . . . . . . 14
|
384 | 125, 383 | op2ndd 7179 |
. . . . . . . . . . . . 13
|
385 | 384 | sneqd 4189 |
. . . . . . . . . . . 12
|
386 | 385 | difeq2d 3728 |
. . . . . . . . . . 11
|
387 | 125, 383 | op1std 7178 |
. . . . . . . . . . . . 13
|
388 | 387 | csbeq1d 3540 |
. . . . . . . . . . . 12
|
389 | 388 | eqeq2d 2632 |
. . . . . . . . . . 11
|
390 | 386, 389 | rexeqbidv 3153 |
. . . . . . . . . 10
|
391 | 390 | ralbidv 2986 |
. . . . . . . . 9
|
392 | 388 | neeq2d 2854 |
. . . . . . . . . 10
|
393 | 392 | ralbidv 2986 |
. . . . . . . . 9
|
394 | 391, 393 | anbi12d 747 |
. . . . . . . 8
|
395 | 394 | rabxp 5154 |
. . . . . . 7
..^
..^
|
396 | 382, 395 | eqtr4i 2647 |
. . . . . 6
..^
..^
|
397 | | difrab 3901 |
. . . . . 6
..^
..^ ..^
|
398 | 360, 396,
397 | 3eqtr4g 2681 |
. . . . 5
..^
..^
..^ |
399 | 398 | fveq2d 6195 |
. . . 4
..^
..^
..^ |
400 | 24 | a1i 11 |
. . . . 5
..^
|
401 | | inxp 5254 |
. . . . . . . . . 10
|
402 | | df-ne 2795 |
. . . . . . . . . . . . 13
|
403 | | disjsn2 4247 |
. . . . . . . . . . . . 13
|
404 | 402, 403 | sylbir 225 |
. . . . . . . . . . . 12
|
405 | 404 | xpeq1d 5138 |
. . . . . . . . . . 11
|
406 | | 0xp 5199 |
. . . . . . . . . . 11
|
407 | 405, 406 | syl6eq 2672 |
. . . . . . . . . 10
|
408 | 401, 407 | syl5eq 2668 |
. . . . . . . . 9
|
409 | 408 | orri 391 |
. . . . . . . 8
|
410 | 409 | rgen2w 2925 |
. . . . . . 7
..^ ..^
|
411 | | sneq 4187 |
. . . . . . . . 9
|
412 | | csbeq1 3536 |
. . . . . . . . . . . . . 14
|
413 | 412 | eqeq2d 2632 |
. . . . . . . . . . . . 13
|
414 | 413 | rexbidv 3052 |
. . . . . . . . . . . 12
|
415 | 414 | ralbidv 2986 |
. . . . . . . . . . 11
|
416 | 412 | neeq2d 2854 |
. . . . . . . . . . . 12
|
417 | 416 | ralbidv 2986 |
. . . . . . . . . . 11
|
418 | 415, 417 | anbi12d 747 |
. . . . . . . . . 10
|
419 | 418 | rabbidv 3189 |
. . . . . . . . 9
|
420 | 411, 419 | xpeq12d 5140 |
. . . . . . . 8
|
421 | 420 | disjor 4634 |
. . . . . . 7
Disj ..^
..^ ..^
|
422 | 410, 421 | mpbir 221 |
. . . . . 6
Disj ..^
|
423 | 422 | a1i 11 |
. . . . 5
Disj
..^
|
424 | 16, 400, 423 | hashiun 14554 |
. . . 4
..^
..^
|
425 | 399, 424 | eqtr3d 2658 |
. . 3
..^
..^ ..^
|
426 | | fo1st 7188 |
. . . . . . . . . . . 12
|
427 | | fofun 6116 |
. . . . . . . . . . . 12
|
428 | 426, 427 | ax-mp 5 |
. . . . . . . . . . 11
|
429 | | ssv 3625 |
. . . . . . . . . . . 12
..^
|
430 | | fof 6115 |
. . . . . . . . . . . . . 14
|
431 | 426, 430 | ax-mp 5 |
. . . . . . . . . . . . 13
|
432 | 431 | fdmi 6052 |
. . . . . . . . . . . 12
|
433 | 429, 432 | sseqtr4i 3638 |
. . . . . . . . . . 11
..^
|
434 | | fores 6124 |
. . . . . . . . . . 11
..^
..^ ..^ ..^ |
435 | 428, 433,
434 | mp2an 708 |
. . . . . . . . . 10
..^ ..^ ..^ |
436 | | fveq2 6191 |
. . . . . . . . . . . . . . . . . . 19
|
437 | 436 | csbeq1d 3540 |
. . . . . . . . . . . . . . . . . 18
|
438 | | fveq2 6191 |
. . . . . . . . . . . . . . . . . . . 20
|
439 | 438 | csbeq1d 3540 |
. . . . . . . . . . . . . . . . . . 19
|
440 | 439 | csbeq2dv 3992 |
. . . . . . . . . . . . . . . . . 18
|
441 | 437, 440 | eqtrd 2656 |
. . . . . . . . . . . . . . . . 17
|
442 | 441 | eqeq2d 2632 |
. . . . . . . . . . . . . . . 16
|
443 | 439 | eqeq2d 2632 |
. . . . . . . . . . . . . . . . . 18
|
444 | 443 | rexbidv 3052 |
. . . . . . . . . . . . . . . . 17
|
445 | 444 | ralbidv 2986 |
. . . . . . . . . . . . . . . 16
|
446 | 442, 445 | anbi12d 747 |
. . . . . . . . . . . . . . 15
|
447 | 446 | rexrab 3370 |
. . . . . . . . . . . . . 14
..^
..^
|
448 | | xp1st 7198 |
. . . . . . . . . . . . . . . . . . . 20
..^ ..^ |
449 | 448 | anim1i 592 |
. . . . . . . . . . . . . . . . . . 19
..^
..^ |
450 | | eleq1 2689 |
. . . . . . . . . . . . . . . . . . . 20
..^
..^ |
451 | | csbeq1a 3542 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
|
452 | 451 | eqcoms 2630 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
453 | 452 | eqcomd 2628 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
454 | 453 | eqeq2d 2632 |
. . . . . . . . . . . . . . . . . . . . . 22
|
455 | 454 | rexbidv 3052 |
. . . . . . . . . . . . . . . . . . . . 21
|
456 | 455 | ralbidv 2986 |
. . . . . . . . . . . . . . . . . . . 20
|
457 | 450, 456 | anbi12d 747 |
. . . . . . . . . . . . . . . . . . 19
..^
..^ |
458 | 449, 457 | syl5ibcom 235 |
. . . . . . . . . . . . . . . . . 18
..^
..^ |
459 | 458 | adantrl 752 |
. . . . . . . . . . . . . . . . 17
..^ ..^ |
460 | 459 | expimpd 629 |
. . . . . . . . . . . . . . . 16
..^
..^ |
461 | 460 | rexlimiv 3027 |
. . . . . . . . . . . . . . 15
..^
..^ |
462 | | simplr 792 |
. . . . . . . . . . . . . . . . . 18
..^
..^ |
463 | | ovex 6678 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
464 | 463 | enref 7988 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
465 | | phpreu 33393 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
466 | 20, 464, 465 | mp2an 708 |
. . . . . . . . . . . . . . . . . . . . . 22
|
467 | 466 | biimpi 206 |
. . . . . . . . . . . . . . . . . . . . 21
|
468 | | eqeq1 2626 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
469 | 468 | reubidv 3126 |
. . . . . . . . . . . . . . . . . . . . . 22
|
470 | 469 | rspcva 3307 |
. . . . . . . . . . . . . . . . . . . . 21
|
471 | 232, 467,
470 | syl2an 494 |
. . . . . . . . . . . . . . . . . . . 20
|
472 | | riotacl 6625 |
. . . . . . . . . . . . . . . . . . . 20
|
473 | 471, 472 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
|
474 | 473 | adantlr 751 |
. . . . . . . . . . . . . . . . . 18
..^
|
475 | | opelxpi 5148 |
. . . . . . . . . . . . . . . . . 18
..^ ..^ |
476 | 462, 474,
475 | syl2anc 693 |
. . . . . . . . . . . . . . . . 17
..^
..^ |
477 | | riotasbc 6626 |
. . . . . . . . . . . . . . . . . . . . . 22
|
478 | 471, 477 | syl 17 |
. . . . . . . . . . . . . . . . . . . . 21
|
479 | | riotaex 6615 |
. . . . . . . . . . . . . . . . . . . . . 22
|
480 | | sbceq2g 3990 |
. . . . . . . . . . . . . . . . . . . . . 22
|
481 | 479, 480 | ax-mp 5 |
. . . . . . . . . . . . . . . . . . . . 21
|
482 | 478, 481 | sylib 208 |
. . . . . . . . . . . . . . . . . . . 20
|
483 | 482 | expcom 451 |
. . . . . . . . . . . . . . . . . . 19
|
484 | 483 | imdistanri 727 |
. . . . . . . . . . . . . . . . . 18
|
485 | 484 | adantlr 751 |
. . . . . . . . . . . . . . . . 17
..^
|
486 | | vex 3203 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
487 | 486, 479 | op2ndd 7179 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
488 | 487 | csbeq1d 3540 |
. . . . . . . . . . . . . . . . . . . . . 22
|
489 | | nfcv 2764 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
|
490 | | nfriota1 6618 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
|
491 | 489, 490 | nfop 4418 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
492 | 491 | nfeq2 2780 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
493 | 486, 479 | op1std 7178 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
|
494 | 493 | eqcomd 2628 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
495 | 494, 451 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
496 | 492, 495 | csbeq2d 3991 |
. . . . . . . . . . . . . . . . . . . . . 22
|
497 | 488, 496 | eqtr3d 2658 |
. . . . . . . . . . . . . . . . . . . . 21
|
498 | 497 | eqeq2d 2632 |
. . . . . . . . . . . . . . . . . . . 20
|
499 | 495 | eqeq2d 2632 |
. . . . . . . . . . . . . . . . . . . . . 22
|
500 | 492, 499 | rexbid 3051 |
. . . . . . . . . . . . . . . . . . . . 21
|
501 | 500 | ralbidv 2986 |
. . . . . . . . . . . . . . . . . . . 20
|
502 | 498, 501 | anbi12d 747 |
. . . . . . . . . . . . . . . . . . 19
|
503 | 493 | biantrud 528 |
. . . . . . . . . . . . . . . . . . 19
|
504 | 502, 503 | bitr2d 269 |
. . . . . . . . . . . . . . . . . 18
|
505 | 504 | rspcev 3309 |
. . . . . . . . . . . . . . . . 17
..^ ..^
|
506 | 476, 485,
505 | syl2anc 693 |
. . . . . . . . . . . . . . . 16
..^
..^
|
507 | 506 | expl 648 |
. . . . . . . . . . . . . . 15
..^
..^
|
508 | 461, 507 | impbid2 216 |
. . . . . . . . . . . . . 14
..^
..^ |
509 | 447, 508 | syl5bb 272 |
. . . . . . . . . . . . 13
..^ ..^ |
510 | 509 | abbidv 2741 |
. . . . . . . . . . . 12
..^
..^ |
511 | | dfimafn 6245 |
. . . . . . . . . . . . . 14
..^
..^
..^
|
512 | 428, 433,
511 | mp2an 708 |
. . . . . . . . . . . . 13
..^
..^
|
513 | | nfcv 2764 |
. . . . . . . . . . . . . . . . . . 19
|
514 | | nfcsb1v 3549 |
. . . . . . . . . . . . . . . . . . 19
|
515 | 513, 514 | nfcsb 3551 |
. . . . . . . . . . . . . . . . . 18
|
516 | 515 | nfeq2 2780 |
. . . . . . . . . . . . . . . . 17
|
517 | | nfcv 2764 |
. . . . . . . . . . . . . . . . . 18
|
518 | 514 | nfeq2 2780 |
. . . . . . . . . . . . . . . . . . 19
|
519 | 517, 518 | nfrex 3007 |
. . . . . . . . . . . . . . . . . 18
|
520 | 517, 519 | nfral 2945 |
. . . . . . . . . . . . . . . . 17
|
521 | 516, 520 | nfan 1828 |
. . . . . . . . . . . . . . . 16
|
522 | | nfcv 2764 |
. . . . . . . . . . . . . . . 16
..^ |
523 | 521, 522 | nfrab 3123 |
. . . . . . . . . . . . . . 15
..^ |
524 | | nfv 1843 |
. . . . . . . . . . . . . . 15
|
525 | 523, 524 | nfrex 3007 |
. . . . . . . . . . . . . 14
..^ |
526 | | nfv 1843 |
. . . . . . . . . . . . . 14
..^ |
527 | | eqeq2 2633 |
. . . . . . . . . . . . . . 15
|
528 | 527 | rexbidv 3052 |
. . . . . . . . . . . . . 14
..^
..^
|
529 | 525, 526,
528 | cbvab 2746 |
. . . . . . . . . . . . 13
..^ ..^ |
530 | 512, 529 | eqtri 2644 |
. . . . . . . . . . . 12
..^
..^
|
531 | | df-rab 2921 |
. . . . . . . . . . . 12
..^ ..^ |
532 | 510, 530,
531 | 3eqtr4g 2681 |
. . . . . . . . . . 11
..^ ..^ |
533 | | foeq3 6113 |
. . . . . . . . . . 11
..^
..^
..^
..^ ..^
..^ ..^ ..^ |
534 | 532, 533 | syl 17 |
. . . . . . . . . 10
..^
..^ ..^
..^ ..^ ..^ |
535 | 435, 534 | mpbii 223 |
. . . . . . . . 9
..^
..^ ..^ |
536 | | fof 6115 |
. . . . . . . . 9
..^
..^ ..^ ..^
..^ ..^ |
537 | 535, 536 | syl 17 |
. . . . . . . 8
..^
..^ ..^ |
538 | | fvres 6207 |
. . . . . . . . . . . 12
..^
..^
|
539 | | fvres 6207 |
. . . . . . . . . . . 12
..^
..^
|
540 | 538, 539 | eqeqan12d 2638 |
. . . . . . . . . . 11
..^
..^ ..^ ..^
|
541 | 540 | adantl 482 |
. . . . . . . . . 10
..^ ..^
..^
..^
|
542 | 446 | elrab 3363 |
. . . . . . . . . . . . . . 15
..^
..^
|
543 | | xp2nd 7199 |
. . . . . . . . . . . . . . . 16
..^ |
544 | 543 | anim1i 592 |
. . . . . . . . . . . . . . 15
..^
|
545 | 542, 544 | sylbi 207 |
. . . . . . . . . . . . . 14
..^
|
546 | | simpl 473 |
. . . . . . . . . . . . . . . . . 18
|
547 | 546 | a1i 11 |
. . . . . . . . . . . . . . . . 17
..^
|
548 | 547 | ss2rabi 3684 |
. . . . . . . . . . . . . . . 16
..^
..^ |
549 | 548 | sseli 3599 |
. . . . . . . . . . . . . . 15
..^
..^ |
550 | | fveq2 6191 |
. . . . . . . . . . . . . . . . . . . 20
|
551 | 550 | csbeq1d 3540 |
. . . . . . . . . . . . . . . . . . 19
|
552 | | fveq2 6191 |
. . . . . . . . . . . . . . . . . . . . 21
|
553 | 552 | csbeq1d 3540 |
. . . . . . . . . . . . . . . . . . . 20
|
554 | 553 | csbeq2dv 3992 |
. . . . . . . . . . . . . . . . . . 19
|
555 | 551, 554 | eqtrd 2656 |
. . . . . . . . . . . . . . . . . 18
|
556 | 555 | eqeq2d 2632 |
. . . . . . . . . . . . . . . . 17
|
557 | 556 | elrab 3363 |
. . . . . . . . . . . . . . . 16
..^
..^ |
558 | | xp2nd 7199 |
. . . . . . . . . . . . . . . . 17
..^ |
559 | 558 | anim1i 592 |
. . . . . . . . . . . . . . . 16
..^
|
560 | 557, 559 | sylbi 207 |
. . . . . . . . . . . . . . 15
..^
|
561 | 549, 560 | syl 17 |
. . . . . . . . . . . . . 14
..^
|
562 | 545, 561 | anim12i 590 |
. . . . . . . . . . . . 13
..^
..^
|
563 | | an4 865 |
. . . . . . . . . . . . . . 15
|
564 | 563 | anbi2i 730 |
. . . . . . . . . . . . . 14
|
565 | | anass 681 |
. . . . . . . . . . . . . . . . 17
|
566 | | ancom 466 |
. . . . . . . . . . . . . . . . 17
|
567 | 565, 566 | bitr3i 266 |
. . . . . . . . . . . . . . . 16
|
568 | 567 | anbi1i 731 |
. . . . . . . . . . . . . . 15
|
569 | | anass 681 |
. . . . . . . . . . . . . . 15
|
570 | 568, 569 | bitri 264 |
. . . . . . . . . . . . . 14
|
571 | | anass 681 |
. . . . . . . . . . . . . 14
|
572 | 564, 570,
571 | 3bitr4i 292 |
. . . . . . . . . . . . 13
|
573 | 562, 572 | sylib 208 |
. . . . . . . . . . . 12
..^
..^ |
574 | | phpreu 33393 |
. . . . . . . . . . . . . . . . . . . . 21
|
575 | 20, 464, 574 | mp2an 708 |
. . . . . . . . . . . . . . . . . . . 20
|
576 | | reurmo 3161 |
. . . . . . . . . . . . . . . . . . . . 21
|
577 | 576 | ralimi 2952 |
. . . . . . . . . . . . . . . . . . . 20
|
578 | 575, 577 | sylbi 207 |
. . . . . . . . . . . . . . . . . . 19
|
579 | | eqeq1 2626 |
. . . . . . . . . . . . . . . . . . . . 21
|
580 | 579 | rmobidv 3131 |
. . . . . . . . . . . . . . . . . . . 20
|
581 | 580 | rspcva 3307 |
. . . . . . . . . . . . . . . . . . 19
|
582 | 232, 578,
581 | syl2an 494 |
. . . . . . . . . . . . . . . . . 18
|
583 | | nfv 1843 |
. . . . . . . . . . . . . . . . . . 19
|
584 | 583 | rmo3 3528 |
. . . . . . . . . . . . . . . . . 18
|
585 | 582, 584 | sylib 208 |
. . . . . . . . . . . . . . . . 17
|
586 | | nfcsb1v 3549 |
. . . . . . . . . . . . . . . . . . . . 21
|
587 | 586 | nfeq2 2780 |
. . . . . . . . . . . . . . . . . . . 20
|
588 | | nfs1v 2437 |
. . . . . . . . . . . . . . . . . . . 20
|
589 | 587, 588 | nfan 1828 |
. . . . . . . . . . . . . . . . . . 19
|
590 | | nfv 1843 |
. . . . . . . . . . . . . . . . . . 19
|
591 | 589, 590 | nfim 1825 |
. . . . . . . . . . . . . . . . . 18
|
592 | | nfv 1843 |
. . . . . . . . . . . . . . . . . 18
|
593 | | csbeq1a 3542 |
. . . . . . . . . . . . . . . . . . . . 21
|
594 | 593 | eqeq2d 2632 |
. . . . . . . . . . . . . . . . . . . 20
|
595 | 594 | anbi1d 741 |
. . . . . . . . . . . . . . . . . . 19
|
596 | | eqeq1 2626 |
. . . . . . . . . . . . . . . . . . 19
|
597 | 595, 596 | imbi12d 334 |
. . . . . . . . . . . . . . . . . 18
|
598 | | sbsbc 3439 |
. . . . . . . . . . . . . . . . . . . . . 22
|
599 | | vex 3203 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
600 | | sbceq2g 3990 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
601 | 599, 600 | ax-mp 5 |
. . . . . . . . . . . . . . . . . . . . . 22
|
602 | 598, 601 | bitri 264 |
. . . . . . . . . . . . . . . . . . . . 21
|
603 | | csbeq1 3536 |
. . . . . . . . . . . . . . . . . . . . . 22
|
604 | 603 | eqeq2d 2632 |
. . . . . . . . . . . . . . . . . . . . 21
|
605 | 602, 604 | syl5bb 272 |
. . . . . . . . . . . . . . . . . . . 20
|
606 | 605 | anbi2d 740 |
. . . . . . . . . . . . . . . . . . 19
|
607 | | eqeq2 2633 |
. . . . . . . . . . . . . . . . . . 19
|
608 | 606, 607 | imbi12d 334 |
. . . . . . . . . . . . . . . . . 18
|
609 | 591, 592,
597, 608 | rspc2 3320 |
. . . . . . . . . . . . . . . . 17
|
610 | 585, 609 | syl5com 31 |
. . . . . . . . . . . . . . . 16
|
611 | 610 | impr 649 |
. . . . . . . . . . . . . . 15
|
612 | | csbeq1 3536 |
. . . . . . . . . . . . . . . . . . 19
|
613 | 612 | csbeq2dv 3992 |
. . . . . . . . . . . . . . . . . 18
|
614 | 613 | eqeq2d 2632 |
. . . . . . . . . . . . . . . . 17
|
615 | 614 | anbi2d 740 |
. . . . . . . . . . . . . . . 16
|
616 | 615 | imbi1d 331 |
. . . . . . . . . . . . . . 15
|
617 | 611, 616 | syl5ibcom 235 |
. . . . . . . . . . . . . 14
|
618 | 617 | com23 86 |
. . . . . . . . . . . . 13
|
619 | 618 | impr 649 |
. . . . . . . . . . . 12
|
620 | 573, 619 | sylan2 491 |
. . . . . . . . . . 11
..^ ..^ |
621 | | elrabi 3359 |
. . . . . . . . . . . . 13
..^
..^ |
622 | | elrabi 3359 |
. . . . . . . . . . . . 13
..^
..^ |
623 | | xpopth 7207 |
. . . . . . . . . . . . . . 15
..^ ..^
|
624 | 623 | biimpd 219 |
. . . . . . . . . . . . . 14
..^ ..^
|
625 | 624 | expd 452 |
. . . . . . . . . . . . 13
..^ ..^
|
626 | 621, 622,
625 | syl2an 494 |
. . . . . . . . . . . 12
..^
..^ |
627 | 626 | adantl 482 |
. . . . . . . . . . 11
..^ ..^ |
628 | 620, 627 | mpdd 43 |
. . . . . . . . . 10
..^ ..^ |
629 | 541, 628 | sylbid 230 |
. . . . . . . . 9
..^ ..^
..^
..^
|
630 | 629 | ralrimivva 2971 |
. . . . . . . 8
..^ ..^ ..^
..^
|
631 | | dff13 6512 |
. . . . . . . 8
..^
..^ ..^ ..^
..^ ..^ ..^ ..^ ..^
..^
|
632 | 537, 630,
631 | sylanbrc 698 |
. . . . . . 7
..^
..^ ..^ |
633 | | df-f1o 5895 |
. . . . . . 7
..^
..^ ..^ ..^ ..^ ..^ ..^
..^ ..^ |
634 | 632, 535,
633 | sylanbrc 698 |
. . . . . 6
..^
..^ ..^ |
635 | | rabfi 8185 |
. . . . . . . . 9
..^ ..^
|
636 | 138, 635 | ax-mp 5 |
. . . . . . . 8
..^
|
637 | 636 | elexi 3213 |
. . . . . . 7
..^
|
638 | 637 | f1oen 7976 |
. . . . . 6
..^
..^ ..^
..^
..^ |
639 | 634, 638 | syl 17 |
. . . . 5
..^ ..^ |
640 | | rabfi 8185 |
. . . . . . 7
..^ ..^ |
641 | 136, 640 | ax-mp 5 |
. . . . . 6
..^ |
642 | | hashen 13135 |
. . . . . 6
..^ ..^ ..^ ..^ ..^ ..^ |
643 | 636, 641,
642 | mp2an 708 |
. . . . 5
..^
..^ ..^ ..^ |
644 | 639, 643 | sylibr 224 |
. . . 4
..^ ..^ |
645 | 644 | oveq2d 6666 |
. . 3
..^
..^
..^
..^ |
646 | 202, 425,
645 | 3eqtr3d 2664 |
. 2
..^
..^
..^ |
647 | 135, 646 | breqtrd 4679 |
1
..^
..^ |