Step | Hyp | Ref
| Expression |
1 | | eldmg 5319 |
. . . 4
|
2 | 1 | ibi 256 |
. . 3
|
3 | | ulmcau.z |
. . . . . . . 8
|
4 | | ulmcau.m |
. . . . . . . . 9
|
5 | 4 | ad2antrr 762 |
. . . . . . . 8
|
6 | | ulmcau.f |
. . . . . . . . 9
|
7 | 6 | ad2antrr 762 |
. . . . . . . 8
|
8 | | eqidd 2623 |
. . . . . . . 8
|
9 | | eqidd 2623 |
. . . . . . . 8
|
10 | | simplr 792 |
. . . . . . . 8
|
11 | | rphalfcl 11858 |
. . . . . . . . 9
|
12 | 11 | adantl 482 |
. . . . . . . 8
|
13 | 3, 5, 7, 8, 9, 10,
12 | ulmi 24140 |
. . . . . . 7
|
14 | | simpr 477 |
. . . . . . . . . . 11
|
15 | 14, 3 | syl6eleq 2711 |
. . . . . . . . . 10
|
16 | | eluzelz 11697 |
. . . . . . . . . 10
|
17 | | uzid 11702 |
. . . . . . . . . 10
|
18 | | fveq2 6191 |
. . . . . . . . . . . . . . . 16
|
19 | 18 | fveq1d 6193 |
. . . . . . . . . . . . . . 15
|
20 | 19 | oveq1d 6665 |
. . . . . . . . . . . . . 14
|
21 | 20 | fveq2d 6195 |
. . . . . . . . . . . . 13
|
22 | 21 | breq1d 4663 |
. . . . . . . . . . . 12
|
23 | 22 | ralbidv 2986 |
. . . . . . . . . . 11
|
24 | 23 | rspcv 3305 |
. . . . . . . . . 10
|
25 | 15, 16, 17, 24 | 4syl 19 |
. . . . . . . . 9
|
26 | | r19.26 3064 |
. . . . . . . . . . . . . . 15
|
27 | 7 | ffvelrnda 6359 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
28 | 27 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
29 | | elmapi 7879 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
30 | 28, 29 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . 22
|
31 | 30 | ffvelrnda 6359 |
. . . . . . . . . . . . . . . . . . . . 21
|
32 | | ulmcl 24135 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
33 | 32 | ad4antlr 769 |
. . . . . . . . . . . . . . . . . . . . . 22
|
34 | 33 | ffvelrnda 6359 |
. . . . . . . . . . . . . . . . . . . . 21
|
35 | 31, 34 | abssubd 14192 |
. . . . . . . . . . . . . . . . . . . 20
|
36 | 35 | breq1d 4663 |
. . . . . . . . . . . . . . . . . . 19
|
37 | 36 | biimpd 219 |
. . . . . . . . . . . . . . . . . 18
|
38 | 3 | uztrn2 11705 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
39 | | ffvelrn 6357 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
40 | 7, 38, 39 | syl2an 494 |
. . . . . . . . . . . . . . . . . . . . . 22
|
41 | 40 | anassrs 680 |
. . . . . . . . . . . . . . . . . . . . 21
|
42 | | elmapi 7879 |
. . . . . . . . . . . . . . . . . . . . 21
|
43 | 41, 42 | syl 17 |
. . . . . . . . . . . . . . . . . . . 20
|
44 | 43 | ffvelrnda 6359 |
. . . . . . . . . . . . . . . . . . 19
|
45 | | rpre 11839 |
. . . . . . . . . . . . . . . . . . . 20
|
46 | 45 | ad4antlr 769 |
. . . . . . . . . . . . . . . . . . 19
|
47 | | abs3lem 14078 |
. . . . . . . . . . . . . . . . . . 19
|
48 | 44, 31, 34, 46, 47 | syl22anc 1327 |
. . . . . . . . . . . . . . . . . 18
|
49 | 37, 48 | sylan2d 499 |
. . . . . . . . . . . . . . . . 17
|
50 | 49 | ancomsd 470 |
. . . . . . . . . . . . . . . 16
|
51 | 50 | ralimdva 2962 |
. . . . . . . . . . . . . . 15
|
52 | 26, 51 | syl5bir 233 |
. . . . . . . . . . . . . 14
|
53 | 52 | expdimp 453 |
. . . . . . . . . . . . 13
|
54 | 53 | an32s 846 |
. . . . . . . . . . . 12
|
55 | 54 | ralimdva 2962 |
. . . . . . . . . . 11
|
56 | 55 | ex 450 |
. . . . . . . . . 10
|
57 | 56 | com23 86 |
. . . . . . . . 9
|
58 | 25, 57 | mpdd 43 |
. . . . . . . 8
|
59 | 58 | reximdva 3017 |
. . . . . . 7
|
60 | 13, 59 | mpd 15 |
. . . . . 6
|
61 | 60 | ralrimiva 2966 |
. . . . 5
|
62 | 61 | ex 450 |
. . . 4
|
63 | 62 | exlimdv 1861 |
. . 3
|
64 | 2, 63 | syl5 34 |
. 2
|
65 | | ulmrel 24132 |
. . . 4
|
66 | | ulmcau.s |
. . . . . . . . . 10
|
67 | 3, 4, 66, 6 | ulmcaulem 24148 |
. . . . . . . . 9
|
68 | 67 | biimpa 501 |
. . . . . . . 8
|
69 | | rphalfcl 11858 |
. . . . . . . 8
|
70 | | breq2 4657 |
. . . . . . . . . . . . 13
|
71 | 70 | ralbidv 2986 |
. . . . . . . . . . . 12
|
72 | 71 | 2ralbidv 2989 |
. . . . . . . . . . 11
|
73 | 72 | rexbidv 3052 |
. . . . . . . . . 10
|
74 | | ralcom 3098 |
. . . . . . . . . . . . . 14
|
75 | | fveq2 6191 |
. . . . . . . . . . . . . . 15
|
76 | | fveq2 6191 |
. . . . . . . . . . . . . . . . . . . 20
|
77 | | fveq2 6191 |
. . . . . . . . . . . . . . . . . . . 20
|
78 | 76, 77 | oveq12d 6668 |
. . . . . . . . . . . . . . . . . . 19
|
79 | 78 | fveq2d 6195 |
. . . . . . . . . . . . . . . . . 18
|
80 | 79 | breq1d 4663 |
. . . . . . . . . . . . . . . . 17
|
81 | 80 | cbvralv 3171 |
. . . . . . . . . . . . . . . 16
|
82 | | fveq2 6191 |
. . . . . . . . . . . . . . . . . . . . 21
|
83 | 82 | fveq1d 6193 |
. . . . . . . . . . . . . . . . . . . 20
|
84 | 83 | oveq1d 6665 |
. . . . . . . . . . . . . . . . . . 19
|
85 | 84 | fveq2d 6195 |
. . . . . . . . . . . . . . . . . 18
|
86 | 85 | breq1d 4663 |
. . . . . . . . . . . . . . . . 17
|
87 | 86 | ralbidv 2986 |
. . . . . . . . . . . . . . . 16
|
88 | 81, 87 | syl5bb 272 |
. . . . . . . . . . . . . . 15
|
89 | 75, 88 | raleqbidv 3152 |
. . . . . . . . . . . . . 14
|
90 | 74, 89 | syl5bb 272 |
. . . . . . . . . . . . 13
|
91 | 90 | cbvralv 3171 |
. . . . . . . . . . . 12
|
92 | | fveq2 6191 |
. . . . . . . . . . . . 13
|
93 | 92 | raleqdv 3144 |
. . . . . . . . . . . 12
|
94 | 91, 93 | syl5bb 272 |
. . . . . . . . . . 11
|
95 | 94 | cbvrexv 3172 |
. . . . . . . . . 10
|
96 | 73, 95 | syl6bbr 278 |
. . . . . . . . 9
|
97 | 96 | rspccva 3308 |
. . . . . . . 8
|
98 | 68, 69, 97 | syl2an 494 |
. . . . . . 7
|
99 | 3 | uztrn2 11705 |
. . . . . . . . . . 11
|
100 | | eqid 2622 |
. . . . . . . . . . . . . 14
|
101 | | eluzelz 11697 |
. . . . . . . . . . . . . . . 16
|
102 | 101, 3 | eleq2s 2719 |
. . . . . . . . . . . . . . 15
|
103 | 102 | ad2antlr 763 |
. . . . . . . . . . . . . 14
|
104 | 69 | adantl 482 |
. . . . . . . . . . . . . . 15
|
105 | 104 | ad2antrr 762 |
. . . . . . . . . . . . . 14
|
106 | | simplr 792 |
. . . . . . . . . . . . . . . 16
|
107 | 3 | uztrn2 11705 |
. . . . . . . . . . . . . . . 16
|
108 | 106, 107 | sylan 488 |
. . . . . . . . . . . . . . 15
|
109 | | fveq2 6191 |
. . . . . . . . . . . . . . . . 17
|
110 | 109 | fveq1d 6193 |
. . . . . . . . . . . . . . . 16
|
111 | | eqid 2622 |
. . . . . . . . . . . . . . . 16
|
112 | | fvex 6201 |
. . . . . . . . . . . . . . . 16
|
113 | 110, 111,
112 | fvmpt 6282 |
. . . . . . . . . . . . . . 15
|
114 | 108, 113 | syl 17 |
. . . . . . . . . . . . . 14
|
115 | 6 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
|
116 | 115 | ffvelrnda 6359 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
117 | | elmapi 7879 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
118 | 116, 117 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
119 | 118 | ffvelrnda 6359 |
. . . . . . . . . . . . . . . . . . . . . 22
|
120 | 119 | an32s 846 |
. . . . . . . . . . . . . . . . . . . . 21
|
121 | | eqid 2622 |
. . . . . . . . . . . . . . . . . . . . 21
|
122 | 120, 121 | fmptd 6385 |
. . . . . . . . . . . . . . . . . . . 20
|
123 | 122 | ffvelrnda 6359 |
. . . . . . . . . . . . . . . . . . 19
|
124 | | fveq2 6191 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
|
125 | | fveq2 6191 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
|
126 | 124, 125 | oveq12d 6668 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
|
127 | 126 | fveq2d 6195 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
|
128 | 127 | breq1d 4663 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
|
129 | 128 | rspcv 3305 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
|
130 | 129 | ralimdv 2963 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
131 | 130 | reximdv 3016 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
132 | 131 | ralimdv 2963 |
. . . . . . . . . . . . . . . . . . . . . 22
|
133 | 132 | impcom 446 |
. . . . . . . . . . . . . . . . . . . . 21
|
134 | 133 | adantll 750 |
. . . . . . . . . . . . . . . . . . . 20
|
135 | | fveq2 6191 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
|
136 | 135 | oveq1d 6665 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
|
137 | 136 | fveq2d 6195 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
|
138 | 137 | breq1d 4663 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
|
139 | 138 | cbvralv 3171 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
|
140 | | fveq2 6191 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
|
141 | 140 | oveq2d 6666 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
|
142 | 141 | fveq2d 6195 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
|
143 | 142 | breq1d 4663 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
|
144 | 92, 143 | raleqbidv 3152 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
|
145 | 139, 144 | syl5bb 272 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
146 | 145 | cbvrexv 3172 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
147 | | fveq2 6191 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
|
148 | 147 | fveq1d 6193 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
|
149 | | fvex 6201 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
|
150 | 148, 121,
149 | fvmpt 6282 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
|
151 | 38, 150 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
|
152 | | fveq2 6191 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
|
153 | 152 | fveq1d 6193 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
|
154 | | fvex 6201 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
|
155 | 153, 121,
154 | fvmpt 6282 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
|
156 | 155 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
|
157 | 151, 156 | oveq12d 6668 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
|
158 | 157 | fveq2d 6195 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
|
159 | 158 | breq1d 4663 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
|
160 | 159 | ralbidva 2985 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
161 | 160 | rexbiia 3040 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
162 | 146, 161 | bitri 264 |
. . . . . . . . . . . . . . . . . . . . . 22
|
163 | | breq2 4657 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
164 | 163 | ralbidv 2986 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
165 | 164 | rexbidv 3052 |
. . . . . . . . . . . . . . . . . . . . . 22
|
166 | 162, 165 | syl5bb 272 |
. . . . . . . . . . . . . . . . . . . . 21
|
167 | 166 | cbvralv 3171 |
. . . . . . . . . . . . . . . . . . . 20
|
168 | 134, 167 | sylibr 224 |
. . . . . . . . . . . . . . . . . . 19
|
169 | | fvex 6201 |
. . . . . . . . . . . . . . . . . . . . . 22
|
170 | 3, 169 | eqeltri 2697 |
. . . . . . . . . . . . . . . . . . . . 21
|
171 | 170 | mptex 6486 |
. . . . . . . . . . . . . . . . . . . 20
|
172 | 171 | a1i 11 |
. . . . . . . . . . . . . . . . . . 19
|
173 | 3, 123, 168, 172 | caucvg 14409 |
. . . . . . . . . . . . . . . . . 18
|
174 | 173 | ralrimiva 2966 |
. . . . . . . . . . . . . . . . 17
|
175 | 174 | ad2antrr 762 |
. . . . . . . . . . . . . . . 16
|
176 | | fveq2 6191 |
. . . . . . . . . . . . . . . . . . 19
|
177 | 176 | mpteq2dv 4745 |
. . . . . . . . . . . . . . . . . 18
|
178 | 177 | eleq1d 2686 |
. . . . . . . . . . . . . . . . 17
|
179 | 178 | rspccva 3308 |
. . . . . . . . . . . . . . . 16
|
180 | 175, 179 | sylan 488 |
. . . . . . . . . . . . . . 15
|
181 | | climdm 14285 |
. . . . . . . . . . . . . . 15
|
182 | 180, 181 | sylib 208 |
. . . . . . . . . . . . . 14
|
183 | 100, 103,
105, 114, 182 | climi2 14242 |
. . . . . . . . . . . . 13
|
184 | 100 | r19.29uz 14090 |
. . . . . . . . . . . . . . 15
|
185 | 100 | r19.2uz 14091 |
. . . . . . . . . . . . . . 15
|
186 | 184, 185 | syl 17 |
. . . . . . . . . . . . . 14
|
187 | 6 | ad2antrr 762 |
. . . . . . . . . . . . . . . . . . . 20
|
188 | 187 | ffvelrnda 6359 |
. . . . . . . . . . . . . . . . . . 19
|
189 | | elmapi 7879 |
. . . . . . . . . . . . . . . . . . 19
|
190 | 188, 189 | syl 17 |
. . . . . . . . . . . . . . . . . 18
|
191 | 190 | ffvelrnda 6359 |
. . . . . . . . . . . . . . . . 17
|
192 | 191 | adantr 481 |
. . . . . . . . . . . . . . . 16
|
193 | | climcl 14230 |
. . . . . . . . . . . . . . . . . 18
|
194 | 182, 193 | syl 17 |
. . . . . . . . . . . . . . . . 17
|
195 | 194 | adantr 481 |
. . . . . . . . . . . . . . . 16
|
196 | 6 | ad5antr 770 |
. . . . . . . . . . . . . . . . . . 19
|
197 | 196, 108 | ffvelrnd 6360 |
. . . . . . . . . . . . . . . . . 18
|
198 | | elmapi 7879 |
. . . . . . . . . . . . . . . . . 18
|
199 | 197, 198 | syl 17 |
. . . . . . . . . . . . . . . . 17
|
200 | | simplr 792 |
. . . . . . . . . . . . . . . . 17
|
201 | 199, 200 | ffvelrnd 6360 |
. . . . . . . . . . . . . . . 16
|
202 | | rpre 11839 |
. . . . . . . . . . . . . . . . 17
|
203 | 202 | ad4antlr 769 |
. . . . . . . . . . . . . . . 16
|
204 | | abs3lem 14078 |
. . . . . . . . . . . . . . . 16
|
205 | 192, 195,
201, 203, 204 | syl22anc 1327 |
. . . . . . . . . . . . . . 15
|
206 | 205 | rexlimdva 3031 |
. . . . . . . . . . . . . 14
|
207 | 186, 206 | syl5 34 |
. . . . . . . . . . . . 13
|
208 | 183, 207 | mpan2d 710 |
. . . . . . . . . . . 12
|
209 | 208 | ralimdva 2962 |
. . . . . . . . . . 11
|
210 | 99, 209 | sylan2 491 |
. . . . . . . . . 10
|
211 | 210 | anassrs 680 |
. . . . . . . . 9
|
212 | 211 | ralimdva 2962 |
. . . . . . . 8
|
213 | 212 | reximdva 3017 |
. . . . . . 7
|
214 | 98, 213 | mpd 15 |
. . . . . 6
|
215 | 214 | ralrimiva 2966 |
. . . . 5
|
216 | 4 | adantr 481 |
. . . . . 6
|
217 | | eqidd 2623 |
. . . . . 6
|
218 | 177 | fveq2d 6195 |
. . . . . . . 8
|
219 | | eqid 2622 |
. . . . . . . 8
|
220 | | fvex 6201 |
. . . . . . . 8
|
221 | 218, 219,
220 | fvmpt 6282 |
. . . . . . 7
|
222 | 221 | adantl 482 |
. . . . . 6
|
223 | | climdm 14285 |
. . . . . . . . 9
|
224 | 173, 223 | sylib 208 |
. . . . . . . 8
|
225 | | climcl 14230 |
. . . . . . . 8
|
226 | 224, 225 | syl 17 |
. . . . . . 7
|
227 | 226, 219 | fmptd 6385 |
. . . . . 6
|
228 | 66 | adantr 481 |
. . . . . 6
|
229 | 3, 216, 115, 217, 222, 227, 228 | ulm2 24139 |
. . . . 5
|
230 | 215, 229 | mpbird 247 |
. . . 4
|
231 | | releldm 5358 |
. . . 4
|
232 | 65, 230, 231 | sylancr 695 |
. . 3
|
233 | 232 | ex 450 |
. 2
|
234 | 64, 233 | impbid 202 |
1
|