Step | Hyp | Ref
| Expression |
1 | | dvadd.bf |
. . . 4
|
2 | | eqid 2157 |
. . . . 5
↾t ↾t |
3 | | dvaddcntop.j |
. . . . 5
|
4 | | eqid 2157 |
. . . . 5
# # |
5 | | dvaddbr.s |
. . . . 5
|
6 | | dvadd.f |
. . . . 5
|
7 | | dvadd.x |
. . . . 5
|
8 | 2, 3, 4, 5, 6, 7 | eldvap 13051 |
. . . 4
↾t #
lim |
9 | 1, 8 | mpbid 146 |
. . 3
↾t #
lim |
10 | 9 | simpld 111 |
. 2
↾t |
11 | 7, 5 | sstrd 3138 |
. . . . . 6
|
12 | 3 | cntoptopon 12932 |
. . . . . . . . . 10
TopOn |
13 | | resttopon 12571 |
. . . . . . . . . 10
TopOn
↾t TopOn |
14 | 12, 5, 13 | sylancr 411 |
. . . . . . . . 9
↾t TopOn |
15 | | topontop 12412 |
. . . . . . . . 9
↾t TopOn ↾t |
16 | 14, 15 | syl 14 |
. . . . . . . 8
↾t |
17 | | toponuni 12413 |
. . . . . . . . . 10
↾t TopOn ↾t |
18 | 14, 17 | syl 14 |
. . . . . . . . 9
↾t |
19 | 7, 18 | sseqtrd 3166 |
. . . . . . . 8
↾t |
20 | | eqid 2157 |
. . . . . . . . 9
↾t
↾t |
21 | 20 | ntrss2 12521 |
. . . . . . . 8
↾t
↾t ↾t |
22 | 16, 19, 21 | syl2anc 409 |
. . . . . . 7
↾t |
23 | 22, 10 | sseldd 3129 |
. . . . . 6
|
24 | 6, 11, 23 | dvlemap 13049 |
. . . . 5
# |
25 | | dvaddxx.g |
. . . . . . 7
|
26 | 25 | adantr 274 |
. . . . . 6
# |
27 | | elrabi 2865 |
. . . . . . 7
# |
28 | 27 | adantl 275 |
. . . . . 6
# |
29 | 26, 28 | ffvelrnd 5603 |
. . . . 5
# |
30 | 24, 29 | mulcld 7898 |
. . . 4
# |
31 | 25, 11, 23 | dvlemap 13049 |
. . . . 5
# |
32 | 6, 23 | ffvelrnd 5603 |
. . . . . 6
|
33 | 32 | adantr 274 |
. . . . 5
# |
34 | 31, 33 | mulcld 7898 |
. . . 4
# |
35 | | ssidd 3149 |
. . . 4
|
36 | | txtopon 12662 |
. . . . . 6
TopOn
TopOn
TopOn |
37 | 12, 12, 36 | mp2an 423 |
. . . . 5
TopOn |
38 | 37 | toponrestid 12419 |
. . . 4
↾t |
39 | 9 | simprd 113 |
. . . . 5
#
lim |
40 | | cnex 7856 |
. . . . . . . . . . . . 13
|
41 | 40 | a1i 9 |
. . . . . . . . . . . 12
|
42 | 41, 5 | ssexd 4104 |
. . . . . . . . . . . 12
|
43 | | elpm2r 6611 |
. . . . . . . . . . . 12
|
44 | 41, 42, 25, 7, 43 | syl22anc 1221 |
. . . . . . . . . . 11
|
45 | | reldvg 13048 |
. . . . . . . . . . 11
|
46 | 5, 44, 45 | syl2anc 409 |
. . . . . . . . . 10
|
47 | | dvadd.bg |
. . . . . . . . . 10
|
48 | | releldm 4821 |
. . . . . . . . . 10
|
49 | 46, 47, 48 | syl2anc 409 |
. . . . . . . . 9
|
50 | | eqid 2157 |
. . . . . . . . . 10
↾t ↾t |
51 | 50, 3 | dvcnp2cntop 13063 |
. . . . . . . . 9
↾t |
52 | 5, 25, 7, 49, 51 | syl31anc 1223 |
. . . . . . . 8
↾t |
53 | 3, 50 | cnplimccntop 13039 |
. . . . . . . . 9
↾t lim |
54 | 11, 23, 53 | syl2anc 409 |
. . . . . . . 8
↾t
lim |
55 | 52, 54 | mpbid 146 |
. . . . . . 7
lim |
56 | 55 | simprd 113 |
. . . . . 6
lim |
57 | 25, 11 | limcdifap 13031 |
. . . . . . 7
lim
# lim |
58 | | ssrab2 3213 |
. . . . . . . . . 10
#
|
59 | 58 | a1i 9 |
. . . . . . . . 9
#
|
60 | 25, 59 | feqresmpt 5522 |
. . . . . . . 8
#
#
|
61 | 60 | oveq1d 5839 |
. . . . . . 7
#
lim
# lim |
62 | 57, 61 | eqtrd 2190 |
. . . . . 6
lim
#
lim |
63 | 56, 62 | eleqtrd 2236 |
. . . . 5
#
lim |
64 | 3 | mulcncntop 12954 |
. . . . . 6
|
65 | 5, 6, 7 | dvcl 13052 |
. . . . . . . 8
|
66 | 1, 65 | mpdan 418 |
. . . . . . 7
|
67 | 25, 23 | ffvelrnd 5603 |
. . . . . . 7
|
68 | 66, 67 | opelxpd 4619 |
. . . . . 6
|
69 | 37 | toponunii 12415 |
. . . . . . 7
|
70 | 69 | cncnpi 12628 |
. . . . . 6
|
71 | 64, 68, 70 | sylancr 411 |
. . . . 5
|
72 | 24, 29, 35, 35, 3, 38, 39, 63, 71 | limccnp2cntop 13046 |
. . . 4
#
lim |
73 | | eqid 2157 |
. . . . . . . 8
# # |
74 | 2, 3, 73, 5, 25, 7 | eldvap 13051 |
. . . . . . 7
↾t #
lim |
75 | 47, 74 | mpbid 146 |
. . . . . 6
↾t #
lim |
76 | 75 | simprd 113 |
. . . . 5
#
lim |
77 | | cncfmptc 12982 |
. . . . . . . 8
|
78 | 32, 11, 35, 77 | syl3anc 1220 |
. . . . . . 7
|
79 | | eqidd 2158 |
. . . . . . 7
|
80 | 78, 23, 79 | cnmptlimc 13043 |
. . . . . 6
lim |
81 | 32 | adantr 274 |
. . . . . . . . 9
|
82 | 81 | fmpttd 5622 |
. . . . . . . 8
|
83 | 82, 11 | limcdifap 13031 |
. . . . . . 7
lim
#
lim
|
84 | | resmpt 4914 |
. . . . . . . . 9
#
#
# |
85 | 58, 84 | mp1i 10 |
. . . . . . . 8
#
# |
86 | 85 | oveq1d 5839 |
. . . . . . 7
#
lim
# lim |
87 | 83, 86 | eqtrd 2190 |
. . . . . 6
lim # lim |
88 | 80, 87 | eleqtrd 2236 |
. . . . 5
#
lim |
89 | 5, 25, 7 | dvcl 13052 |
. . . . . . . 8
|
90 | 47, 89 | mpdan 418 |
. . . . . . 7
|
91 | 90, 32 | opelxpd 4619 |
. . . . . 6
|
92 | 69 | cncnpi 12628 |
. . . . . 6
|
93 | 64, 91, 92 | sylancr 411 |
. . . . 5
|
94 | 31, 33, 35, 35, 3, 38, 76, 88, 93 | limccnp2cntop 13046 |
. . . 4
#
lim |
95 | 3 | addcncntop 12952 |
. . . . 5
|
96 | 66, 67 | mulcld 7898 |
. . . . . 6
|
97 | 90, 32 | mulcld 7898 |
. . . . . 6
|
98 | 96, 97 | opelxpd 4619 |
. . . . 5
|
99 | 69 | cncnpi 12628 |
. . . . 5
|
100 | 95, 98, 99 | sylancr 411 |
. . . 4
|
101 | 30, 34, 35, 35, 3, 38, 72, 94, 100 | limccnp2cntop 13046 |
. . 3
# lim |
102 | 6 | adantr 274 |
. . . . . . . . . 10
# |
103 | 102, 28 | ffvelrnd 5603 |
. . . . . . . . 9
# |
104 | 103, 33 | subcld 8186 |
. . . . . . . 8
# |
105 | 104, 29 | mulcld 7898 |
. . . . . . 7
# |
106 | 67 | adantr 274 |
. . . . . . . . 9
# |
107 | 29, 106 | subcld 8186 |
. . . . . . . 8
# |
108 | 107, 33 | mulcld 7898 |
. . . . . . 7
# |
109 | 11 | adantr 274 |
. . . . . . . . 9
# |
110 | 109, 28 | sseldd 3129 |
. . . . . . . 8
# |
111 | 11, 23 | sseldd 3129 |
. . . . . . . . 9
|
112 | 111 | adantr 274 |
. . . . . . . 8
#
|
113 | 110, 112 | subcld 8186 |
. . . . . . 7
# |
114 | | breq1 3968 |
. . . . . . . . . . 11
#
# |
115 | 114 | elrab 2868 |
. . . . . . . . . 10
# #
|
116 | 115 | simprbi 273 |
. . . . . . . . 9
# # |
117 | 116 | adantl 275 |
. . . . . . . 8
# # |
118 | 110, 112,
117 | subap0d 8519 |
. . . . . . 7
# # |
119 | 105, 108,
113, 118 | divdirapd 8702 |
. . . . . 6
# |
120 | 103, 29 | mulcld 7898 |
. . . . . . . . 9
# |
121 | 33, 29 | mulcld 7898 |
. . . . . . . . 9
# |
122 | 33, 106 | mulcld 7898 |
. . . . . . . . 9
# |
123 | 120, 121,
122 | npncand 8210 |
. . . . . . . 8
# |
124 | 103, 33, 29 | subdird 8290 |
. . . . . . . . 9
# |
125 | 107, 33 | mulcomd 7899 |
. . . . . . . . . 10
# |
126 | 33, 29, 106 | subdid 8289 |
. . . . . . . . . 10
# |
127 | 125, 126 | eqtrd 2190 |
. . . . . . . . 9
# |
128 | 124, 127 | oveq12d 5842 |
. . . . . . . 8
# |
129 | 28, 28 | elind 3292 |
. . . . . . . . . 10
# |
130 | 6 | ffnd 5320 |
. . . . . . . . . . . 12
|
131 | 130 | adantr 274 |
. . . . . . . . . . 11
#
|
132 | 25 | ffnd 5320 |
. . . . . . . . . . . 12
|
133 | 132 | adantr 274 |
. . . . . . . . . . 11
#
|
134 | | ssexg 4103 |
. . . . . . . . . . . . 13
|
135 | 11, 40, 134 | sylancl 410 |
. . . . . . . . . . . 12
|
136 | 135 | adantr 274 |
. . . . . . . . . . 11
#
|
137 | | eqid 2157 |
. . . . . . . . . . 11
|
138 | | eqidd 2158 |
. . . . . . . . . . 11
#
|
139 | | eqidd 2158 |
. . . . . . . . . . 11
#
|
140 | 120 | adantr 274 |
. . . . . . . . . . 11
#
|
141 | 131, 133,
136, 136, 137, 138, 139, 140 | ofvalg 6041 |
. . . . . . . . . 10
#
|
142 | 129, 141 | mpdan 418 |
. . . . . . . . 9
#
|
143 | 23, 23 | elind 3292 |
. . . . . . . . . 10
|
144 | | eqidd 2158 |
. . . . . . . . . . 11
#
|
145 | | eqidd 2158 |
. . . . . . . . . . 11
#
|
146 | 122 | adantr 274 |
. . . . . . . . . . 11
#
|
147 | 131, 133,
136, 136, 137, 144, 145, 146 | ofvalg 6041 |
. . . . . . . . . 10
#
|
148 | 143, 147 | mpidan 420 |
. . . . . . . . 9
#
|
149 | 142, 148 | oveq12d 5842 |
. . . . . . . 8
# |
150 | 123, 128,
149 | 3eqtr4d 2200 |
. . . . . . 7
# |
151 | 150 | oveq1d 5839 |
. . . . . 6
# |
152 | 104, 29, 113, 118 | div23apd 8701 |
. . . . . . 7
# |
153 | 107, 33, 113, 118 | div23apd 8701 |
. . . . . . 7
# |
154 | 152, 153 | oveq12d 5842 |
. . . . . 6
# |
155 | 119, 151,
154 | 3eqtr3d 2198 |
. . . . 5
# |
156 | 155 | mpteq2dva 4054 |
. . . 4
#
# |
157 | 156 | oveq1d 5839 |
. . 3
#
lim
#
lim |
158 | 101, 157 | eleqtrrd 2237 |
. 2
# lim |
159 | | eqid 2157 |
. . 3
# #
|
160 | | mulcl 7859 |
. . . . 5
|
161 | 160 | adantl 275 |
. . . 4
|
162 | | inidm 3316 |
. . . 4
|
163 | 161, 6, 25, 135, 135, 162 | off 6044 |
. . 3
|
164 | 2, 3, 159, 5, 163, 7 | eldvap 13051 |
. 2
↾t # lim |
165 | 10, 158, 164 | mpbir2and 929 |
1
|