Mathbox for Glauco Siliprandi < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  stoweidlem59 Unicode version

Theorem stoweidlem59 27675
 Description: This lemma proves that there exists a function as in the proof in [BrosowskiDeutsh] p. 91, after Lemma 2: xj is in the subalgebra, 0 <= xj <= 1, xj < ε / n on Aj (meaning A in the paper), xj > 1 - \epslon / n on Bj. Here is used to represent A in the paper (because A is used for the subalgebra of functions), is used to represent ε. (Contributed by Glauco Siliprandi, 20-Apr-2017.)
Hypotheses
Ref Expression
stoweidlem59.1
stoweidlem59.2
stoweidlem59.3
stoweidlem59.4
stoweidlem59.5
stoweidlem59.6
stoweidlem59.7
stoweidlem59.8
stoweidlem59.9
stoweidlem59.10
stoweidlem59.11
stoweidlem59.12
stoweidlem59.13
stoweidlem59.14
stoweidlem59.15
stoweidlem59.16
stoweidlem59.17
stoweidlem59.18
stoweidlem59.19
Assertion
Ref Expression
stoweidlem59
Distinct variable groups:   ,,   ,   ,   ,,,   ,   ,,,,,,   ,,,,,   ,,,,   ,,,,   ,,,,   ,,,,   ,,,,   ,,,,   ,,,,,   ,,,,,   ,,   ,   ,   ,,   ,,   ,   ,   ,   ,   ,
Allowed substitution hints:   ()   ()   (,)   (,,,,,,,)   (,)   ()   (,)   (,,,,,,,)   (,,,,,,)   (,,,)   (,,,,,,)   (,,,,,)

Proof of Theorem stoweidlem59
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 stoweidlem59.8 . . . . . . . . . 10
2 nfrab1 2848 . . . . . . . . . 10
31, 2nfcxfr 2537 . . . . . . . . 9
4 nfcv 2540 . . . . . . . . 9
5 nfv 1626 . . . . . . . . 9
6 nfv 1626 . . . . . . . . 9
7 fveq1 5686 . . . . . . . . . . . 12
87breq1d 4182 . . . . . . . . . . 11
98ralbidv 2686 . . . . . . . . . 10
107breq2d 4184 . . . . . . . . . . 11
1110ralbidv 2686 . . . . . . . . . 10
129, 11anbi12d 692 . . . . . . . . 9
133, 4, 5, 6, 12cbvrab 2914 . . . . . . . 8
14 stoweidlem59.10 . . . . . . . . . . . . 13
15 cmptop 17412 . . . . . . . . . . . . 13
1614, 15syl 16 . . . . . . . . . . . 12
17 stoweidlem59.3 . . . . . . . . . . . . 13
18 retop 18748 . . . . . . . . . . . . 13
1917, 18eqeltri 2474 . . . . . . . . . . . 12
20 cnfex 27566 . . . . . . . . . . . 12
2116, 19, 20sylancl 644 . . . . . . . . . . 11
22 stoweidlem59.11 . . . . . . . . . . . 12
23 stoweidlem59.5 . . . . . . . . . . . 12
2422, 23syl6sseq 3354 . . . . . . . . . . 11
2521, 24ssexd 4310 . . . . . . . . . 10
26 ssrab2 3388 . . . . . . . . . . . 12
271, 26eqsstri 3338 . . . . . . . . . . 11
2827a1i 11 . . . . . . . . . 10
2925, 28ssexd 4310 . . . . . . . . 9
30 rabexg 4313 . . . . . . . . 9
3129, 30syl 16 . . . . . . . 8
3213, 31syl5eqel 2488 . . . . . . 7
3332ralrimivw 2750 . . . . . 6
34 stoweidlem59.9 . . . . . . 7
3534fnmpt 5530 . . . . . 6
3633, 35syl 16 . . . . 5
37 fzfi 11266 . . . . 5
38 fnfi 7343 . . . . 5
3936, 37, 38sylancl 644 . . . 4
40 rnfi 7350 . . . 4
4139, 40syl 16 . . 3
42 fnchoice 27567 . . 3
4341, 42syl 16 . 2
44 simprl 733 . . . . 5
45 ovex 6065 . . . . . . . 8
4645mptex 5925 . . . . . . 7
4734, 46eqeltri 2474 . . . . . 6
4847rnex 5092 . . . . 5
49 fnex 5920 . . . . 5
5044, 48, 49sylancl 644 . . . 4
51 coexg 5371 . . . 4
5250, 47, 51sylancl 644 . . 3
53 dffn3 5557 . . . . . . 7
5444, 53sylib 189 . . . . . 6
55 nfv 1626 . . . . . . . . . 10
56 nfv 1626 . . . . . . . . . . 11
57 nfra1 2716 . . . . . . . . . . 11
5856, 57nfan 1842 . . . . . . . . . 10
5955, 58nfan 1842 . . . . . . . . 9
60 simplrr 738 . . . . . . . . . . 11
61 simpr 448 . . . . . . . . . . 11
62 fvelrnb 5733 . . . . . . . . . . . . . . . 16
63 nfv 1626 . . . . . . . . . . . . . . . . 17
64 nfmpt1 4258 . . . . . . . . . . . . . . . . . . . 20
6534, 64nfcxfr 2537 . . . . . . . . . . . . . . . . . . 19
66 nfcv 2540 . . . . . . . . . . . . . . . . . . 19
6765, 66nffv 5694 . . . . . . . . . . . . . . . . . 18
68 nfcv 2540 . . . . . . . . . . . . . . . . . 18
6967, 68nfeq 2547 . . . . . . . . . . . . . . . . 17
70 fveq2 5687 . . . . . . . . . . . . . . . . . 18
7170eqeq1d 2412 . . . . . . . . . . . . . . . . 17
7263, 69, 71cbvrex 2889 . . . . . . . . . . . . . . . 16
7362, 72syl6bbr 255 . . . . . . . . . . . . . . 15
7436, 73syl 16 . . . . . . . . . . . . . 14
7574biimpa 471 . . . . . . . . . . . . 13
76 simp3 959 . . . . . . . . . . . . . . . . 17
77 simpr 448 . . . . . . . . . . . . . . . . . . . 20
7832adantr 452 . . . . . . . . . . . . . . . . . . . 20
7934fvmpt2 5771 . . . . . . . . . . . . . . . . . . . 20
8077, 78, 79syl2anc 643 . . . . . . . . . . . . . . . . . . 19
81 stoweidlem59.6 . . . . . . . . . . . . . . . . . . . . . . . . 25
82 nfcv 2540 . . . . . . . . . . . . . . . . . . . . . . . . . 26
83 nfrab1 2848 . . . . . . . . . . . . . . . . . . . . . . . . . 26
8482, 83nfmpt 4257 . . . . . . . . . . . . . . . . . . . . . . . . 25
8581, 84nfcxfr 2537 . . . . . . . . . . . . . . . . . . . . . . . 24
86 nfcv 2540 . . . . . . . . . . . . . . . . . . . . . . . 24
8785, 86nffv 5694 . . . . . . . . . . . . . . . . . . . . . . 23
88 nfcv 2540 . . . . . . . . . . . . . . . . . . . . . . . 24
89 stoweidlem59.7 . . . . . . . . . . . . . . . . . . . . . . . . . 26
90 nfrab1 2848 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
9182, 90nfmpt 4257 . . . . . . . . . . . . . . . . . . . . . . . . . 26
9289, 91nfcxfr 2537 . . . . . . . . . . . . . . . . . . . . . . . . 25
9392, 86nffv 5694 . . . . . . . . . . . . . . . . . . . . . . . 24
9488, 93nfdif 3428 . . . . . . . . . . . . . . . . . . . . . . 23
95 stoweidlem59.2 . . . . . . . . . . . . . . . . . . . . . . . 24
96 nfv 1626 . . . . . . . . . . . . . . . . . . . . . . . 24
9795, 96nfan 1842 . . . . . . . . . . . . . . . . . . . . . . 23
98 stoweidlem59.4 . . . . . . . . . . . . . . . . . . . . . . 23
9914adantr 452 . . . . . . . . . . . . . . . . . . . . . . 23
10022adantr 452 . . . . . . . . . . . . . . . . . . . . . . 23
101 stoweidlem59.12 . . . . . . . . . . . . . . . . . . . . . . . 24
1021013adant1r 1177 . . . . . . . . . . . . . . . . . . . . . . 23
103 stoweidlem59.13 . . . . . . . . . . . . . . . . . . . . . . . 24
1041033adant1r 1177 . . . . . . . . . . . . . . . . . . . . . . 23
105 stoweidlem59.14 . . . . . . . . . . . . . . . . . . . . . . . 24
106105adantlr 696 . . . . . . . . . . . . . . . . . . . . . . 23
107 stoweidlem59.15 . . . . . . . . . . . . . . . . . . . . . . . 24
108107adantlr 696 . . . . . . . . . . . . . . . . . . . . . . 23
109 uniexg 4665 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
11014, 109syl 16 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
11198, 110syl5eqel 2488 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
112111adantr 452 . . . . . . . . . . . . . . . . . . . . . . . . . 26
113 rabexg 4313 . . . . . . . . . . . . . . . . . . . . . . . . . 26
114112, 113syl 16 . . . . . . . . . . . . . . . . . . . . . . . . 25
11589fvmpt2 5771 . . . . . . . . . . . . . . . . . . . . . . . . 25
11677, 114, 115syl2anc 643 . . . . . . . . . . . . . . . . . . . . . . . 24
117 stoweidlem59.1 . . . . . . . . . . . . . . . . . . . . . . . . 25
118 eqid 2404 . . . . . . . . . . . . . . . . . . . . . . . . 25
119 elfzelz 11015 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
120119zred 10331 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
121 3re 10027 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
122 3ne0 10041 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
123121, 122rereccli 9735 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
124 readdcl 9029 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
125120, 123, 124sylancl 644 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
126125adantl 453 . . . . . . . . . . . . . . . . . . . . . . . . . 26
127 stoweidlem59.17 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
128127rpred 10604 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
129128adantr 452 . . . . . . . . . . . . . . . . . . . . . . . . . 26
130126, 129remulcld 9072 . . . . . . . . . . . . . . . . . . . . . . . . 25
131 stoweidlem59.16 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
132131, 23syl6eleq 2494 . . . . . . . . . . . . . . . . . . . . . . . . . 26
133132adantr 452 . . . . . . . . . . . . . . . . . . . . . . . . 25
134117, 17, 98, 118, 130, 133rfcnpre3 27571 . . . . . . . . . . . . . . . . . . . . . . . 24
135116, 134eqeltrd 2478 . . . . . . . . . . . . . . . . . . . . . . 23
136 rabexg 4313 . . . . . . . . . . . . . . . . . . . . . . . . . 26
137112, 136syl 16 . . . . . . . . . . . . . . . . . . . . . . . . 25
13881fvmpt2 5771 . . . . . . . . . . . . . . . . . . . . . . . . 25
13977, 137, 138syl2anc 643 . . . . . . . . . . . . . . . . . . . . . . . 24
140 eqid 2404 . . . . . . . . . . . . . . . . . . . . . . . . 25
141 resubcl 9321 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
142120, 123, 141sylancl 644 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
143142adantl 453 . . . . . . . . . . . . . . . . . . . . . . . . . 26
144143, 129remulcld 9072 . . . . . . . . . . . . . . . . . . . . . . . . 25
145117, 17, 98, 140, 144, 133rfcnpre4 27572 . . . . . . . . . . . . . . . . . . . . . . . 24
146139, 145eqeltrd 2478 . . . . . . . . . . . . . . . . . . . . . . 23
147144adantr 452 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
148130adantr 452 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
14917, 98, 23, 131fcnre 27563 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
150149ad2antrr 707 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
151 ssrab2 3388 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
152116, 151syl6eqss 3358 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
153152sselda 3308 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
154150, 153ffvelrnd 5830 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
155123, 141mpan2 653 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36
156 id 20 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36
157123, 124mpan2 653 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36
158 3pos 10040 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39
159121, 158recgt0ii 9872 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38
160123, 159elrpii 10571 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37
161 ltsubrp 10599 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37
162160, 161mpan2 653 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36
163 ltaddrp 10600 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37
164160, 163mpan2 653 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36
165155, 156, 157, 162, 164lttrd 9187 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
166120, 165syl 16 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
167166adantl 453 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
168127rpregt0d 10610 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
169168adantr 452 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
170 ltmul1 9816 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
171143, 126, 169, 170syl3anc 1184 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
172167, 171mpbid 202 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
173172adantr 452 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
174116eleq2d 2471 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
175174biimpa 471 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
176 rabid 2844 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
177175, 176sylib 189 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
178177simprd 450 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
179147, 148, 154, 173, 178ltletrd 9186 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
180147, 154ltnled 9176 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
181179, 180mpbid 202 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
182181intnand 883 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
183 rabid 2844 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
184182, 183sylnibr 297 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
185139adantr 452 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
186184, 185neleqtrrd 2500 . . . . . . . . . . . . . . . . . . . . . . . . . 26
187186ex 424 . . . . . . . . . . . . . . . . . . . . . . . . 25
18897, 187ralrimi 2747 . . . . . . . . . . . . . . . . . . . . . . . 24
189 disj 3628 . . . . . . . . . . . . . . . . . . . . . . . . 25
190 nfcv 2540 . . . . . . . . . . . . . . . . . . . . . . . . . 26
19187nfcri 2534 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
192191nfn 1807 . . . . . . . . . . . . . . . . . . . . . . . . . 26
193 nfv 1626 . . . . . . . . . . . . . . . . . . . . . . . . . 26
194 eleq1 2464 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
195194notbid 286 . . . . . . . . . . . . . . . . . . . . . . . . . 26
196190, 93, 192, 193, 195cbvralf 2886 . . . . . . . . . . . . . . . . . . . . . . . . 25
197189, 196bitri 241 . . . . . . . . . . . . . . . . . . . . . . . 24
198188, 197sylibr 204 . . . . . . . . . . . . . . . . . . . . . . 23
199 eqid 2404 . . . . . . . . . . . . . . . . . . . . . . 23
200 stoweidlem59.19 . . . . . . . . . . . . . . . . . . . . . . . . . 26
201200nnrpd 10603 . . . . . . . . . . . . . . . . . . . . . . . . 25
202127, 201rpdivcld 10621 . . . . . . . . . . . . . . . . . . . . . . . 24
203202adantr 452 . . . . . . . . . . . . . . . . . . . . . . 23
204128, 200nndivred 10004 . . . . . . . . . . . . . . . . . . . . . . . . 25
205123a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . 25
206200nnge1d 9998 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
207 1re 9046 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
208 0lt1 9506 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
209207, 208pm3.2i 442 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
210209a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
211200nnred 9971 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
212200nngt0d 9999 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
213 lediv2 9856 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
214210, 211, 212, 168, 213syl121anc 1189 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
215206, 214mpbid 202 . . . . . . . . . . . . . . . . . . . . . . . . . 26
216127rpcnd 10606 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
217216div1d 9738 . . . . . . . . . . . . . . . . . . . . . . . . . 26
218215, 217breqtrd 4196 . . . . . . . . . . . . . . . . . . . . . . . . 25
219 stoweidlem59.18 . . . . . . . . . . . . . . . . . . . . . . . . 25
220204, 128, 205, 218, 219lelttrd 9184 . . . . . . . . . . . . . . . . . . . . . . . 24
221220adantr 452 . . . . . . . . . . . . . . . . . . . . . . 23
22287, 94, 97, 17, 98, 23, 99, 100, 102, 104, 106, 108, 135, 146, 198, 199, 203, 221stoweidlem58 27674 . . . . . . . . . . . . . . . . . . . . . 22
223 df-rex 2672 . . . . . . . . . . . . . . . . . . . . . 22
224222, 223sylib 189 . . . . . . . . . . . . . . . . . . . . 21
225 simprl 733 . . . . . . . . . . . . . . . . . . . . . . . . 25
226 simprr1 1005 . . . . . . . . . . . . . . . . . . . . . . . . 25
227 fveq1 5686 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
228227breq2d 4184 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
229227breq1d 4182 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
230228, 229anbi12d 692 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
231230ralbidv 2686 . . . . . . . . . . . . . . . . . . . . . . . . . 26
232231, 1elrab2 3054 . . . . . . . . . . . . . . . . . . . . . . . . 25
233225, 226, 232sylanbrc 646 . . . . . . . . . . . . . . . . . . . . . . . 24
234 simprr2 1006 . . . . . . . . . . . . . . . . . . . . . . . . 25
235 simprr3 1007 . . . . . . . . . . . . . . . . . . . . . . . . 25
236234, 235jca 519 . . . . . . . . . . . . . . . . . . . . . . . 24
237 nfcv 2540 . . . . . . . . . . . . . . . . . . . . . . . . 25
238 nfv 1626 . . . . . . . . . . . . . . . . . . . . . . . . 25
239227breq1d 4182 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
240239ralbidv 2686 . . . . . . . . . . . . . . . . . . . . . . . . . 26
241227breq2d 4184 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
242241ralbidv 2686 . . . . . . . . . . . . . . . . . . . . . . . . . 26
243240, 242anbi12d 692 . . . . . . . . . . . . . . . . . . . . . . . . 25
244237, 3, 238, 243elrabf 3051 . . . . . . . . . . . . . . . . . . . . . . . 24
245233, 236, 244sylanbrc 646 . . . . . . . . . . . . . . . . . . . . . . 23
246245ex 424 . . . . . . . . . . . . . . . . . . . . . 22
247246eximdv 1629 . . . . . . . . . . . . . . . . . . . . 21
248224, 247mpd 15 . . . . . . . . . . . . . . . . . . . 20
249 ne0i 3594 . . . . . . . . . . . . . . . . . . . . 21
250249exlimiv 1641 . . . . . . . . . . . . . . . . . . . 20
251248, 250syl 16 . . . . . . . . . . . . . . . . . . 19
25280, 251eqnetrd 2585 . . . . . . . . . . . . . . . . . 18
2532523adant3 977 . . . . . . . . . . . . . . . . 17
25476, 253eqnetrrd 2587 . . . . . . . . . . . . . . . 16
2552543exp 1152 . . . . . . . . . . . . . . 15
256255rexlimdv 2789 . . . . . . . . . . . . . 14
257256adantr 452 . . . . . . . . . . . . 13
25875, 257mpd 15 . . . . . . . . . . . 12
259258adantlr 696 . . . . . . . . . . 11
260 rsp 2726 . . . . . . . . . . 11
26160, 61, 259, 260syl3c 59 . . . . . . . . . 10
262261ex 424 . . . . . . . . 9
26359, 262ralrimi 2747 . . . . . . . 8
264 chfnrn 5800 . . . . . . . 8
26544, 263, 264syl2anc 643 . . . . . . 7
266 nfv 1626 . . . . . . . . . . 11
267 nfcv 2540 . . . . . . . . . . . . 13
268 nfcv 2540 . . . . . . . . . . . . . . . 16
269 nfrab1 2848 . . . . . . . . . . . . . . . 16
270268, 269nfmpt 4257 . . . . . . . . . . . . . . 15
27134, 270nfcxfr 2537 . . . . . . . . . . . . . 14
272271nfrn 5071 . . . . . . . . . . . . 13
273267, 272nffn 5500 . . . . . . . . . . . 12
274 nfv 1626 . . . . . . . . . . . . 13
275272, 274nfral 2719 . . . . . . . . . . . 12
276273, 275nfan 1842 . . . . . . . . . . 11
277266, 276nfan 1842 . . . . . . . . . 10
278 fnunirn 5958 . . . . . . . . . . . . . . . 16
279 nfcv 2540 . . . . . . . . . . . . . . . . . . 19
28065, 279nffv 5694 . . . . . . . . . . . . . . . . . 18
281280nfcri 2534 . . . . . . . . . . . . . . . . 17
282 nfv 1626 . . . . . . . . . . . . . . . . 17
283 fveq2 5687 . . . . . . . . . . . . . . . . . 18
284283eleq2d 2471 . . . . . . . . . . . . . . . . 17
285281, 282, 284cbvrex 2889 . . . . . . . . . . . . . . . 16
286278, 285syl6bb 253 . . . . . . . . . . . . . . 15
28736, 286syl 16 . . . . . . . . . . . . . 14
288287biimpa 471 . . . . . . . . . . . . 13
289 nfv 1626 . . . . . . . . . . . . . . 15
29065nfrn 5071 . . . . . . . . . . . . . . . . 17
291290nfuni 3981 . . . . . . . . . . . . . . . 16
292291nfcri 2534 . . . . . . . . . . . . . . 15
293289, 292nfan 1842 . . . . . . . . . . . . . 14
294 nfv 1626 . . . . . . . . . . . . . 14
295 simp1l 981 . . . . . . . . . . . . . . . 16
296 simp2 958 . . . . . . . . . . . . . . . 16
297 simp3 959 . . . . . . . . . . . . . . . 16
29880eleq2d 2471 . . . . . . . . . . . . . . . . . . 19
299298biimpa 471 . . . . . . . . . . . . . . . . . 18
300 rabid 2844 . . . . . . . . . . . . . . . . . 18
301299, 300sylib 189 . . . . . . . . . . . . . . . . 17
302301simpld 446 . . . . . . . . . . . . . . . 16
303295, 296, 297, 302syl21anc 1183 . . . . . . . . . . . . . . 15
3043033exp 1152 . . . . . . . . . . . . . 14
305293, 294, 304rexlimd 2787 . . . . . . . . . . . . 13
306288, 305mpd 15 . . . . . . . . . . . 12
307306adantlr 696 . . . . . . . . . . 11
308307ex 424 . . . . . . . . . 10
309277, 308alrimi 1777 . . . . . . . . 9
310272nfuni 3981 . . . . . . . . . 10
311310, 3dfss2f 3299 . . . . . . . . 9
312309, 311sylibr 204 . . . . . . . 8
313312, 27syl6ss 3320 . . . . . . 7
314265, 313sstrd 3318 . . . . . 6
315 fss 5558 . . . . . 6
31654, 314, 315syl2anc 643 . . . . 5
317 dffn3 5557 . . . . . . 7
31836, 317sylib 189 . . . . . 6
319318adantr 452 . . . . 5
320 fco 5559 . . . . 5
321316, 319, 320syl2anc 643 . . . 4
322 nfcv 2540 . . . . . . . 8
323322, 290nffn 5500 . . . . . . 7
324 nfv 1626 . . . . . . . 8
325290, 324nfral 2719 . . . . . . 7
326323, 325nfan 1842 . . . . . 6
327289, 326nfan 1842 . . . . 5
328 simpll 731 . . . . . . . . . 10
329 simpr 448 . . . . . . . . . 10
33036ad2antrr 707 . . . . . . . . . . . 12
331 fvco2 5757 . . . . . . . . . . . 12
332330, 331sylancom 649 . . . . . . . . . . 11
333 simplrr 738 . . . . . . . . . . . . 13
334 fnfun 5501 . . . . . . . . . . . . . . . 16
33536, 334syl 16 . . . . . . . . . . . . . . 15
336335ad2antrr 707 . . . . . . . . . . . . . 14
337 fndm 5503 . . . . . . . . . . . . . . . . . 18
33836, 337syl 16 . . . . . . . . . . . . . . . . 17
339338adantr 452 . . . . . . . . . . . . . . . 16
34077, 339eleqtrrd 2481 . . . . . . . . . . . . . . 15
341340adantlr 696 . . . . . . . . . . . . . 14
342 fvelrn 5825 . . . . . . . . . . . . . 14
343336, 341, 342syl2anc 643 . . . . . . . . . . . . 13
344333, 343jca 519 . . . . . . . . . . . 12
345252adantlr 696 . . . . . . . . . . . 12
346 neeq1 2575 . . . . . . . . . . . . . 14
347 fveq2 5687 . . . . . . . . . . . . . . 15
348 id 20 . . . . . . . . . . . . . . 15
349347, 348eleq12d 2472 . . . . . . . . . . . . . 14
350346, 349imbi12d 312 . . . . . . . . . . . . 13
351350rspccva 3011 . . . . . . . . . . . 12
352344, 345, 351sylc 58 . . . . . . . . . . 11
353332, 352eqeltrd 2478 . . . . . . . . . 10
354267, 271nfco 4997 . . . . . . . . . . . . 13
355 nfcv 2540 . . . . . . . . . . . . 13
356354, 355nffv 5694 . . . . . . . . . . . 12
357 nfv 1626 . . . . . . . . . . . . . 14
358271, 355nffv 5694 . . . . . . . . . . . . . . 15
359356, 358nfel 2548 . . . . . . . . . . . . . 14
360357, 359nfan 1842 . . . . . . . . . . . . 13
361356, 3nfel 2548 . . . . . . . . . . . . 13
362360, 361nfim 1828 . . . . . . . . . . . 12
363 eleq1 2464 . . . . . . . . . . . . . 14
364363anbi2d 685 . . . . . . . . . . . . 13
365 eleq1 2464 . . . . . . . . . . . . 13
366364, 365imbi12d 312 . . . . . . . . . . . 12
367356, 362, 366, 302vtoclgf 2970 . . . . . . . . . . 11
368367anabsi7 793 . . . . . . . . . 10
369328, 329, 353, 368syl21anc 1183 . . . . . . . . 9
3701eleq2i 2468 . . . . . . . . . 10
371 nfcv 2540 . . . . . . . . . . 11
372 nfcv 2540 . . . . . . . . . . . 12
373 nfcv 2540 . . . . . . . . . . . . . 14
374 nfcv 2540 . . . . . . . . . . . . . 14
375 nfcv 2540 . . . . . . . . . . . . . . 15
376356, 375nffv 5694 . . . . . . . . . . . . . 14
377373, 374, 376nfbr 4216 . . . . . . . . . . . . 13
378 nfcv 2540 . . . . . . . . . . . . . 14
379376, 374, 378nfbr 4216 . . . . . . . . . . . . 13
380377, 379nfan 1842 . . . . . . . . . . . 12
381372, 380nfral 2719 . . . . . . . . . . 11
382 nfcv 2540 . . . . . . . . . . . . 13
383 nfcv 2540 . . . . . . . . . . . . . . 15
384 nfra1 2716 . . . . . . . . . . . . . . . . . . 19
385 nfra1 2716 . . . . . . . . . . . . . . . . . . 19
386384, 385nfan 1842 . . . . . . . . . . . . . . . . . 18
387 nfra1 2716 . . . . . . . . . . . . . . . . . . . 20
388 nfcv 2540 . . . . . . . . . . . . . . . . . . . 20
389387, 388nfrab 2849 . . . . . . . . . . . . . . . . . . 19
3901, 389nfcxfr 2537 . . . . . . . . . . . . . . . . . 18
391386, 390nfrab 2849 . . . . . . . . . . . . . . . . 17
39282, 391nfmpt 4257 . . . . . . . . . . . . . . . 16
39334, 392nfcxfr 2537 . . . . . . . . . . . . . . 15
394383, 393nfco 4997 . . . . . . . . . . . . . 14
395394, 86nffv 5694 . . . . . . . . . . . . 13
396382, 395nfeq 2547 . . . . . . . . . . . 12
397 fveq1 5686 . . . . . . . . . . . . . 14
398397breq2d 4184 . . . . . . . . . . . . 13
399397breq1d 4182 . . . . . . . . . . . . 13
400398, 399anbi12d 692 . . . . . . . . . . . 12
401396, 400ralbid 2684 . . . . . . . . . . 11
402356, 371, 381, 401elrabf 3051 . . . . . . . . . 10
403370, 402bitri 241 . . . . . . . . 9
404369, 403sylib 189 . . . . . . . 8
405404simprd 450 . . . . . . 7
406 nfcv 2540 . . . . . . . . . . . 12
407 nfcv 2540 . . . . . . . . . . . . 13
408 nfcv 2540 . . . . . . . . . . . . 13
409376, 407, 408nfbr 4216 . . . . . . . . . . . 12
410406, 409nfral 2719 . . . . . . . . . . 11
411360, 410nfim 1828 . . . . . . . . . 10
412397breq1d 4182 . . . . . . . . . . . 12
413396, 412ralbid 2684 . . . . . . . . . . 11
414364, 413imbi12d 312 . . . . . . . . . 10
415301simprd 450 . . . . . . . . . . 11
416415simpld 446 . . . . . . . . . 10
417356, 411, 414, 416vtoclgf 2970 . . . . . . . . 9
418417anabsi7 793 . . . . . . . 8
419328, 329, 353, 418syl21anc 1183 . . . . . . 7
420 nfcv 2540 . . . . . . . . . . . 12
421 nfcv 2540 . . . . . . . . . . . . 13
422421, 407, 376nfbr 4216 . . . . . . . . . . . 12
423420, 422nfral 2719 . . . . . . . . . . 11
424360, 423nfim 1828 . . . . . . . . . 10
425397breq2d 4184 . . . . . . . . . . . 12
426396, 425ralbid 2684 . . . . . . . . . . 11
427364, 426imbi12d 312 . . . . . . . . . 10
428415simprd 450 . . . . . . . . . 10
429356, 424, 427, 428vtoclgf 2970 . . . . . . . . 9
430429anabsi7 793 . . . . . . . 8
431328, 329, 353, 430syl21anc 1183 . . . . . . 7
432405, 419, 4313jca 1134 . . . . . 6
433432ex 424 . . . . 5