Step | Hyp | Ref
| Expression |
1 | | dvcnpcntop.k |
. . . . 5
β’ πΎ = (MetOpenβ(abs β
β )) |
2 | | dvcnp.j |
. . . . 5
β’ π½ = (πΎ βΎt π΄) |
3 | | simpl3 1002 |
. . . . . 6
β’ (((π β β β§ πΉ:π΄βΆβ β§ π΄ β π) β§ π΅(π D πΉ)π¦) β π΄ β π) |
4 | | simpl1 1000 |
. . . . . 6
β’ (((π β β β§ πΉ:π΄βΆβ β§ π΄ β π) β§ π΅(π D πΉ)π¦) β π β β) |
5 | 3, 4 | sstrd 3163 |
. . . . 5
β’ (((π β β β§ πΉ:π΄βΆβ β§ π΄ β π) β§ π΅(π D πΉ)π¦) β π΄ β β) |
6 | | simpl2 1001 |
. . . . 5
β’ (((π β β β§ πΉ:π΄βΆβ β§ π΄ β π) β§ π΅(π D πΉ)π¦) β πΉ:π΄βΆβ) |
7 | 1 | cntoptop 13526 |
. . . . . . . 8
β’ πΎ β Top |
8 | | cnex 7910 |
. . . . . . . . 9
β’ β
β V |
9 | | ssexg 4137 |
. . . . . . . . 9
β’ ((π β β β§ β
β V) β π β
V) |
10 | 4, 8, 9 | sylancl 413 |
. . . . . . . 8
β’ (((π β β β§ πΉ:π΄βΆβ β§ π΄ β π) β§ π΅(π D πΉ)π¦) β π β V) |
11 | | resttop 13163 |
. . . . . . . 8
β’ ((πΎ β Top β§ π β V) β (πΎ βΎt π) β Top) |
12 | 7, 10, 11 | sylancr 414 |
. . . . . . 7
β’ (((π β β β§ πΉ:π΄βΆβ β§ π΄ β π) β§ π΅(π D πΉ)π¦) β (πΎ βΎt π) β Top) |
13 | 1 | cntoptopon 13525 |
. . . . . . . . . 10
β’ πΎ β
(TopOnββ) |
14 | | resttopon 13164 |
. . . . . . . . . 10
β’ ((πΎ β (TopOnββ)
β§ π β β)
β (πΎ
βΎt π)
β (TopOnβπ)) |
15 | 13, 4, 14 | sylancr 414 |
. . . . . . . . 9
β’ (((π β β β§ πΉ:π΄βΆβ β§ π΄ β π) β§ π΅(π D πΉ)π¦) β (πΎ βΎt π) β (TopOnβπ)) |
16 | | toponuni 13006 |
. . . . . . . . 9
β’ ((πΎ βΎt π) β (TopOnβπ) β π = βͺ (πΎ βΎt π)) |
17 | 15, 16 | syl 14 |
. . . . . . . 8
β’ (((π β β β§ πΉ:π΄βΆβ β§ π΄ β π) β§ π΅(π D πΉ)π¦) β π = βͺ (πΎ βΎt π)) |
18 | 3, 17 | sseqtrd 3191 |
. . . . . . 7
β’ (((π β β β§ πΉ:π΄βΆβ β§ π΄ β π) β§ π΅(π D πΉ)π¦) β π΄ β βͺ (πΎ βΎt π)) |
19 | | eqid 2175 |
. . . . . . . 8
β’ βͺ (πΎ
βΎt π) =
βͺ (πΎ βΎt π) |
20 | 19 | ntrss2 13114 |
. . . . . . 7
β’ (((πΎ βΎt π) β Top β§ π΄ β βͺ (πΎ
βΎt π))
β ((intβ(πΎ
βΎt π))βπ΄) β π΄) |
21 | 12, 18, 20 | syl2anc 411 |
. . . . . 6
β’ (((π β β β§ πΉ:π΄βΆβ β§ π΄ β π) β§ π΅(π D πΉ)π¦) β ((intβ(πΎ βΎt π))βπ΄) β π΄) |
22 | | eqid 2175 |
. . . . . . . 8
β’ (πΎ βΎt π) = (πΎ βΎt π) |
23 | | eqid 2175 |
. . . . . . . 8
β’ (π§ β {π€ β π΄ β£ π€ # π΅} β¦ (((πΉβπ§) β (πΉβπ΅)) / (π§ β π΅))) = (π§ β {π€ β π΄ β£ π€ # π΅} β¦ (((πΉβπ§) β (πΉβπ΅)) / (π§ β π΅))) |
24 | | simp1 997 |
. . . . . . . 8
β’ ((π β β β§ πΉ:π΄βΆβ β§ π΄ β π) β π β β) |
25 | | simp2 998 |
. . . . . . . 8
β’ ((π β β β§ πΉ:π΄βΆβ β§ π΄ β π) β πΉ:π΄βΆβ) |
26 | | simp3 999 |
. . . . . . . 8
β’ ((π β β β§ πΉ:π΄βΆβ β§ π΄ β π) β π΄ β π) |
27 | 22, 1, 23, 24, 25, 26 | eldvap 13644 |
. . . . . . 7
β’ ((π β β β§ πΉ:π΄βΆβ β§ π΄ β π) β (π΅(π D πΉ)π¦ β (π΅ β ((intβ(πΎ βΎt π))βπ΄) β§ π¦ β ((π§ β {π€ β π΄ β£ π€ # π΅} β¦ (((πΉβπ§) β (πΉβπ΅)) / (π§ β π΅))) limβ π΅)))) |
28 | 27 | simprbda 383 |
. . . . . 6
β’ (((π β β β§ πΉ:π΄βΆβ β§ π΄ β π) β§ π΅(π D πΉ)π¦) β π΅ β ((intβ(πΎ βΎt π))βπ΄)) |
29 | 21, 28 | sseldd 3154 |
. . . . 5
β’ (((π β β β§ πΉ:π΄βΆβ β§ π΄ β π) β§ π΅(π D πΉ)π¦) β π΅ β π΄) |
30 | 6 | ffvelcdmda 5643 |
. . . . . . . 8
β’ ((((π β β β§ πΉ:π΄βΆβ β§ π΄ β π) β§ π΅(π D πΉ)π¦) β§ π§ β π΄) β (πΉβπ§) β β) |
31 | 6, 29 | ffvelrnd 5644 |
. . . . . . . . 9
β’ (((π β β β§ πΉ:π΄βΆβ β§ π΄ β π) β§ π΅(π D πΉ)π¦) β (πΉβπ΅) β β) |
32 | 31 | adantr 276 |
. . . . . . . 8
β’ ((((π β β β§ πΉ:π΄βΆβ β§ π΄ β π) β§ π΅(π D πΉ)π¦) β§ π§ β π΄) β (πΉβπ΅) β β) |
33 | 30, 32 | subcld 8242 |
. . . . . . 7
β’ ((((π β β β§ πΉ:π΄βΆβ β§ π΄ β π) β§ π΅(π D πΉ)π¦) β§ π§ β π΄) β ((πΉβπ§) β (πΉβπ΅)) β β) |
34 | | ssid 3173 |
. . . . . . . 8
β’ β
β β |
35 | 34 | a1i 9 |
. . . . . . 7
β’ (((π β β β§ πΉ:π΄βΆβ β§ π΄ β π) β§ π΅(π D πΉ)π¦) β β β
β) |
36 | | txtopon 13255 |
. . . . . . . . 9
β’ ((πΎ β (TopOnββ)
β§ πΎ β
(TopOnββ)) β (πΎ Γt πΎ) β (TopOnβ(β Γ
β))) |
37 | 13, 13, 36 | mp2an 426 |
. . . . . . . 8
β’ (πΎ Γt πΎ) β (TopOnβ(β
Γ β)) |
38 | 37 | toponrestid 13012 |
. . . . . . 7
β’ (πΎ Γt πΎ) = ((πΎ Γt πΎ) βΎt (β Γ
β)) |
39 | 6, 5, 29 | dvlemap 13642 |
. . . . . . . . . 10
β’ ((((π β β β§ πΉ:π΄βΆβ β§ π΄ β π) β§ π΅(π D πΉ)π¦) β§ π§ β {π€ β π΄ β£ π€ # π΅}) β (((πΉβπ§) β (πΉβπ΅)) / (π§ β π΅)) β β) |
40 | | ssrab2 3238 |
. . . . . . . . . . . . 13
β’ {π€ β π΄ β£ π€ # π΅} β π΄ |
41 | 40, 5 | sstrid 3164 |
. . . . . . . . . . . 12
β’ (((π β β β§ πΉ:π΄βΆβ β§ π΄ β π) β§ π΅(π D πΉ)π¦) β {π€ β π΄ β£ π€ # π΅} β β) |
42 | 41 | sselda 3153 |
. . . . . . . . . . 11
β’ ((((π β β β§ πΉ:π΄βΆβ β§ π΄ β π) β§ π΅(π D πΉ)π¦) β§ π§ β {π€ β π΄ β£ π€ # π΅}) β π§ β β) |
43 | 5, 29 | sseldd 3154 |
. . . . . . . . . . . 12
β’ (((π β β β§ πΉ:π΄βΆβ β§ π΄ β π) β§ π΅(π D πΉ)π¦) β π΅ β β) |
44 | 43 | adantr 276 |
. . . . . . . . . . 11
β’ ((((π β β β§ πΉ:π΄βΆβ β§ π΄ β π) β§ π΅(π D πΉ)π¦) β§ π§ β {π€ β π΄ β£ π€ # π΅}) β π΅ β β) |
45 | 42, 44 | subcld 8242 |
. . . . . . . . . 10
β’ ((((π β β β§ πΉ:π΄βΆβ β§ π΄ β π) β§ π΅(π D πΉ)π¦) β§ π§ β {π€ β π΄ β£ π€ # π΅}) β (π§ β π΅) β β) |
46 | 27 | simplbda 384 |
. . . . . . . . . 10
β’ (((π β β β§ πΉ:π΄βΆβ β§ π΄ β π) β§ π΅(π D πΉ)π¦) β π¦ β ((π§ β {π€ β π΄ β£ π€ # π΅} β¦ (((πΉβπ§) β (πΉβπ΅)) / (π§ β π΅))) limβ π΅)) |
47 | | limcresi 13628 |
. . . . . . . . . . . 12
β’ ((π§ β π΄ β¦ (π§ β π΅)) limβ π΅) β (((π§ β π΄ β¦ (π§ β π΅)) βΎ {π€ β π΄ β£ π€ # π΅}) limβ π΅) |
48 | | resmpt 4948 |
. . . . . . . . . . . . . 14
β’ ({π€ β π΄ β£ π€ # π΅} β π΄ β ((π§ β π΄ β¦ (π§ β π΅)) βΎ {π€ β π΄ β£ π€ # π΅}) = (π§ β {π€ β π΄ β£ π€ # π΅} β¦ (π§ β π΅))) |
49 | 40, 48 | ax-mp 5 |
. . . . . . . . . . . . 13
β’ ((π§ β π΄ β¦ (π§ β π΅)) βΎ {π€ β π΄ β£ π€ # π΅}) = (π§ β {π€ β π΄ β£ π€ # π΅} β¦ (π§ β π΅)) |
50 | 49 | oveq1i 5875 |
. . . . . . . . . . . 12
β’ (((π§ β π΄ β¦ (π§ β π΅)) βΎ {π€ β π΄ β£ π€ # π΅}) limβ π΅) = ((π§ β {π€ β π΄ β£ π€ # π΅} β¦ (π§ β π΅)) limβ π΅) |
51 | 47, 50 | sseqtri 3187 |
. . . . . . . . . . 11
β’ ((π§ β π΄ β¦ (π§ β π΅)) limβ π΅) β ((π§ β {π€ β π΄ β£ π€ # π΅} β¦ (π§ β π΅)) limβ π΅) |
52 | 43 | subidd 8230 |
. . . . . . . . . . . 12
β’ (((π β β β§ πΉ:π΄βΆβ β§ π΄ β π) β§ π΅(π D πΉ)π¦) β (π΅ β π΅) = 0) |
53 | 1 | subcncntop 13546 |
. . . . . . . . . . . . . . 15
β’ β
β ((πΎ
Γt πΎ) Cn
πΎ) |
54 | 53 | a1i 9 |
. . . . . . . . . . . . . 14
β’ (((π β β β§ πΉ:π΄βΆβ β§ π΄ β π) β§ π΅(π D πΉ)π¦) β β β ((πΎ Γt πΎ) Cn πΎ)) |
55 | | cncfmptid 13576 |
. . . . . . . . . . . . . . 15
β’ ((π΄ β β β§ β
β β) β (π§
β π΄ β¦ π§) β (π΄βcnββ)) |
56 | 5, 34, 55 | sylancl 413 |
. . . . . . . . . . . . . 14
β’ (((π β β β§ πΉ:π΄βΆβ β§ π΄ β π) β§ π΅(π D πΉ)π¦) β (π§ β π΄ β¦ π§) β (π΄βcnββ)) |
57 | | cncfmptc 13575 |
. . . . . . . . . . . . . . 15
β’ ((π΅ β β β§ π΄ β β β§ β
β β) β (π§
β π΄ β¦ π΅) β (π΄βcnββ)) |
58 | 43, 5, 35, 57 | syl3anc 1238 |
. . . . . . . . . . . . . 14
β’ (((π β β β§ πΉ:π΄βΆβ β§ π΄ β π) β§ π΅(π D πΉ)π¦) β (π§ β π΄ β¦ π΅) β (π΄βcnββ)) |
59 | 1, 54, 56, 58 | cncfmpt2fcntop 13578 |
. . . . . . . . . . . . 13
β’ (((π β β β§ πΉ:π΄βΆβ β§ π΄ β π) β§ π΅(π D πΉ)π¦) β (π§ β π΄ β¦ (π§ β π΅)) β (π΄βcnββ)) |
60 | | oveq1 5872 |
. . . . . . . . . . . . 13
β’ (π§ = π΅ β (π§ β π΅) = (π΅ β π΅)) |
61 | 59, 29, 60 | cnmptlimc 13636 |
. . . . . . . . . . . 12
β’ (((π β β β§ πΉ:π΄βΆβ β§ π΄ β π) β§ π΅(π D πΉ)π¦) β (π΅ β π΅) β ((π§ β π΄ β¦ (π§ β π΅)) limβ π΅)) |
62 | 52, 61 | eqeltrrd 2253 |
. . . . . . . . . . 11
β’ (((π β β β§ πΉ:π΄βΆβ β§ π΄ β π) β§ π΅(π D πΉ)π¦) β 0 β ((π§ β π΄ β¦ (π§ β π΅)) limβ π΅)) |
63 | 51, 62 | sselid 3151 |
. . . . . . . . . 10
β’ (((π β β β§ πΉ:π΄βΆβ β§ π΄ β π) β§ π΅(π D πΉ)π¦) β 0 β ((π§ β {π€ β π΄ β£ π€ # π΅} β¦ (π§ β π΅)) limβ π΅)) |
64 | 1 | mulcncntop 13547 |
. . . . . . . . . . 11
β’ Β·
β ((πΎ
Γt πΎ) Cn
πΎ) |
65 | 24, 25, 26 | dvcl 13645 |
. . . . . . . . . . . 12
β’ (((π β β β§ πΉ:π΄βΆβ β§ π΄ β π) β§ π΅(π D πΉ)π¦) β π¦ β β) |
66 | | 0cn 7924 |
. . . . . . . . . . . 12
β’ 0 β
β |
67 | | opelxpi 4652 |
. . . . . . . . . . . 12
β’ ((π¦ β β β§ 0 β
β) β β¨π¦,
0β© β (β Γ β)) |
68 | 65, 66, 67 | sylancl 413 |
. . . . . . . . . . 11
β’ (((π β β β§ πΉ:π΄βΆβ β§ π΄ β π) β§ π΅(π D πΉ)π¦) β β¨π¦, 0β© β (β Γ
β)) |
69 | 37 | toponunii 13008 |
. . . . . . . . . . . 12
β’ (β
Γ β) = βͺ (πΎ Γt πΎ) |
70 | 69 | cncnpi 13221 |
. . . . . . . . . . 11
β’ ((
Β· β ((πΎ
Γt πΎ) Cn
πΎ) β§ β¨π¦, 0β© β (β
Γ β)) β Β· β (((πΎ Γt πΎ) CnP πΎ)ββ¨π¦, 0β©)) |
71 | 64, 68, 70 | sylancr 414 |
. . . . . . . . . 10
β’ (((π β β β§ πΉ:π΄βΆβ β§ π΄ β π) β§ π΅(π D πΉ)π¦) β Β· β (((πΎ Γt πΎ) CnP πΎ)ββ¨π¦, 0β©)) |
72 | 39, 45, 35, 35, 1, 38, 46, 63, 71 | limccnp2cntop 13639 |
. . . . . . . . 9
β’ (((π β β β§ πΉ:π΄βΆβ β§ π΄ β π) β§ π΅(π D πΉ)π¦) β (π¦ Β· 0) β ((π§ β {π€ β π΄ β£ π€ # π΅} β¦ ((((πΉβπ§) β (πΉβπ΅)) / (π§ β π΅)) Β· (π§ β π΅))) limβ π΅)) |
73 | 65 | mul01d 8324 |
. . . . . . . . 9
β’ (((π β β β§ πΉ:π΄βΆβ β§ π΄ β π) β§ π΅(π D πΉ)π¦) β (π¦ Β· 0) = 0) |
74 | 6 | adantr 276 |
. . . . . . . . . . . . . 14
β’ ((((π β β β§ πΉ:π΄βΆβ β§ π΄ β π) β§ π΅(π D πΉ)π¦) β§ π§ β {π€ β π΄ β£ π€ # π΅}) β πΉ:π΄βΆβ) |
75 | | simpr 110 |
. . . . . . . . . . . . . . 15
β’ ((((π β β β§ πΉ:π΄βΆβ β§ π΄ β π) β§ π΅(π D πΉ)π¦) β§ π§ β {π€ β π΄ β£ π€ # π΅}) β π§ β {π€ β π΄ β£ π€ # π΅}) |
76 | 40, 75 | sselid 3151 |
. . . . . . . . . . . . . 14
β’ ((((π β β β§ πΉ:π΄βΆβ β§ π΄ β π) β§ π΅(π D πΉ)π¦) β§ π§ β {π€ β π΄ β£ π€ # π΅}) β π§ β π΄) |
77 | 74, 76 | ffvelrnd 5644 |
. . . . . . . . . . . . 13
β’ ((((π β β β§ πΉ:π΄βΆβ β§ π΄ β π) β§ π΅(π D πΉ)π¦) β§ π§ β {π€ β π΄ β£ π€ # π΅}) β (πΉβπ§) β β) |
78 | 31 | adantr 276 |
. . . . . . . . . . . . 13
β’ ((((π β β β§ πΉ:π΄βΆβ β§ π΄ β π) β§ π΅(π D πΉ)π¦) β§ π§ β {π€ β π΄ β£ π€ # π΅}) β (πΉβπ΅) β β) |
79 | 77, 78 | subcld 8242 |
. . . . . . . . . . . 12
β’ ((((π β β β§ πΉ:π΄βΆβ β§ π΄ β π) β§ π΅(π D πΉ)π¦) β§ π§ β {π€ β π΄ β£ π€ # π΅}) β ((πΉβπ§) β (πΉβπ΅)) β β) |
80 | | breq1 4001 |
. . . . . . . . . . . . . . . 16
β’ (π€ = π§ β (π€ # π΅ β π§ # π΅)) |
81 | 80 | elrab 2891 |
. . . . . . . . . . . . . . 15
β’ (π§ β {π€ β π΄ β£ π€ # π΅} β (π§ β π΄ β§ π§ # π΅)) |
82 | 81 | simprbi 275 |
. . . . . . . . . . . . . 14
β’ (π§ β {π€ β π΄ β£ π€ # π΅} β π§ # π΅) |
83 | 82 | adantl 277 |
. . . . . . . . . . . . 13
β’ ((((π β β β§ πΉ:π΄βΆβ β§ π΄ β π) β§ π΅(π D πΉ)π¦) β§ π§ β {π€ β π΄ β£ π€ # π΅}) β π§ # π΅) |
84 | 42, 44, 83 | subap0d 8575 |
. . . . . . . . . . . 12
β’ ((((π β β β§ πΉ:π΄βΆβ β§ π΄ β π) β§ π΅(π D πΉ)π¦) β§ π§ β {π€ β π΄ β£ π€ # π΅}) β (π§ β π΅) # 0) |
85 | 79, 45, 84 | divcanap1d 8720 |
. . . . . . . . . . 11
β’ ((((π β β β§ πΉ:π΄βΆβ β§ π΄ β π) β§ π΅(π D πΉ)π¦) β§ π§ β {π€ β π΄ β£ π€ # π΅}) β ((((πΉβπ§) β (πΉβπ΅)) / (π§ β π΅)) Β· (π§ β π΅)) = ((πΉβπ§) β (πΉβπ΅))) |
86 | 85 | mpteq2dva 4088 |
. . . . . . . . . 10
β’ (((π β β β§ πΉ:π΄βΆβ β§ π΄ β π) β§ π΅(π D πΉ)π¦) β (π§ β {π€ β π΄ β£ π€ # π΅} β¦ ((((πΉβπ§) β (πΉβπ΅)) / (π§ β π΅)) Β· (π§ β π΅))) = (π§ β {π€ β π΄ β£ π€ # π΅} β¦ ((πΉβπ§) β (πΉβπ΅)))) |
87 | 86 | oveq1d 5880 |
. . . . . . . . 9
β’ (((π β β β§ πΉ:π΄βΆβ β§ π΄ β π) β§ π΅(π D πΉ)π¦) β ((π§ β {π€ β π΄ β£ π€ # π΅} β¦ ((((πΉβπ§) β (πΉβπ΅)) / (π§ β π΅)) Β· (π§ β π΅))) limβ π΅) = ((π§ β {π€ β π΄ β£ π€ # π΅} β¦ ((πΉβπ§) β (πΉβπ΅))) limβ π΅)) |
88 | 72, 73, 87 | 3eltr3d 2258 |
. . . . . . . 8
β’ (((π β β β§ πΉ:π΄βΆβ β§ π΄ β π) β§ π΅(π D πΉ)π¦) β 0 β ((π§ β {π€ β π΄ β£ π€ # π΅} β¦ ((πΉβπ§) β (πΉβπ΅))) limβ π΅)) |
89 | 33 | fmpttd 5663 |
. . . . . . . . . 10
β’ (((π β β β§ πΉ:π΄βΆβ β§ π΄ β π) β§ π΅(π D πΉ)π¦) β (π§ β π΄ β¦ ((πΉβπ§) β (πΉβπ΅))):π΄βΆβ) |
90 | 89, 5 | limcdifap 13624 |
. . . . . . . . 9
β’ (((π β β β§ πΉ:π΄βΆβ β§ π΄ β π) β§ π΅(π D πΉ)π¦) β ((π§ β π΄ β¦ ((πΉβπ§) β (πΉβπ΅))) limβ π΅) = (((π§ β π΄ β¦ ((πΉβπ§) β (πΉβπ΅))) βΎ {π€ β π΄ β£ π€ # π΅}) limβ π΅)) |
91 | | resmpt 4948 |
. . . . . . . . . . 11
β’ ({π€ β π΄ β£ π€ # π΅} β π΄ β ((π§ β π΄ β¦ ((πΉβπ§) β (πΉβπ΅))) βΎ {π€ β π΄ β£ π€ # π΅}) = (π§ β {π€ β π΄ β£ π€ # π΅} β¦ ((πΉβπ§) β (πΉβπ΅)))) |
92 | 40, 91 | ax-mp 5 |
. . . . . . . . . 10
β’ ((π§ β π΄ β¦ ((πΉβπ§) β (πΉβπ΅))) βΎ {π€ β π΄ β£ π€ # π΅}) = (π§ β {π€ β π΄ β£ π€ # π΅} β¦ ((πΉβπ§) β (πΉβπ΅))) |
93 | 92 | oveq1i 5875 |
. . . . . . . . 9
β’ (((π§ β π΄ β¦ ((πΉβπ§) β (πΉβπ΅))) βΎ {π€ β π΄ β£ π€ # π΅}) limβ π΅) = ((π§ β {π€ β π΄ β£ π€ # π΅} β¦ ((πΉβπ§) β (πΉβπ΅))) limβ π΅) |
94 | 90, 93 | eqtrdi 2224 |
. . . . . . . 8
β’ (((π β β β§ πΉ:π΄βΆβ β§ π΄ β π) β§ π΅(π D πΉ)π¦) β ((π§ β π΄ β¦ ((πΉβπ§) β (πΉβπ΅))) limβ π΅) = ((π§ β {π€ β π΄ β£ π€ # π΅} β¦ ((πΉβπ§) β (πΉβπ΅))) limβ π΅)) |
95 | 88, 94 | eleqtrrd 2255 |
. . . . . . 7
β’ (((π β β β§ πΉ:π΄βΆβ β§ π΄ β π) β§ π΅(π D πΉ)π¦) β 0 β ((π§ β π΄ β¦ ((πΉβπ§) β (πΉβπ΅))) limβ π΅)) |
96 | | cncfmptc 13575 |
. . . . . . . . 9
β’ (((πΉβπ΅) β β β§ π΄ β β β§ β β
β) β (π§ β
π΄ β¦ (πΉβπ΅)) β (π΄βcnββ)) |
97 | 31, 5, 35, 96 | syl3anc 1238 |
. . . . . . . 8
β’ (((π β β β§ πΉ:π΄βΆβ β§ π΄ β π) β§ π΅(π D πΉ)π¦) β (π§ β π΄ β¦ (πΉβπ΅)) β (π΄βcnββ)) |
98 | | eqidd 2176 |
. . . . . . . 8
β’ (π§ = π΅ β (πΉβπ΅) = (πΉβπ΅)) |
99 | 97, 29, 98 | cnmptlimc 13636 |
. . . . . . 7
β’ (((π β β β§ πΉ:π΄βΆβ β§ π΄ β π) β§ π΅(π D πΉ)π¦) β (πΉβπ΅) β ((π§ β π΄ β¦ (πΉβπ΅)) limβ π΅)) |
100 | 1 | addcncntop 13545 |
. . . . . . . 8
β’ + β
((πΎ Γt
πΎ) Cn πΎ) |
101 | | opelxpi 4652 |
. . . . . . . . 9
β’ ((0
β β β§ (πΉβπ΅) β β) β β¨0, (πΉβπ΅)β© β (β Γ
β)) |
102 | 66, 31, 101 | sylancr 414 |
. . . . . . . 8
β’ (((π β β β§ πΉ:π΄βΆβ β§ π΄ β π) β§ π΅(π D πΉ)π¦) β β¨0, (πΉβπ΅)β© β (β Γ
β)) |
103 | 69 | cncnpi 13221 |
. . . . . . . 8
β’ (( +
β ((πΎ
Γt πΎ) Cn
πΎ) β§ β¨0, (πΉβπ΅)β© β (β Γ β))
β + β (((πΎ
Γt πΎ) CnP
πΎ)ββ¨0, (πΉβπ΅)β©)) |
104 | 100, 102,
103 | sylancr 414 |
. . . . . . 7
β’ (((π β β β§ πΉ:π΄βΆβ β§ π΄ β π) β§ π΅(π D πΉ)π¦) β + β (((πΎ Γt πΎ) CnP πΎ)ββ¨0, (πΉβπ΅)β©)) |
105 | 33, 32, 35, 35, 1, 38, 95, 99, 104 | limccnp2cntop 13639 |
. . . . . 6
β’ (((π β β β§ πΉ:π΄βΆβ β§ π΄ β π) β§ π΅(π D πΉ)π¦) β (0 + (πΉβπ΅)) β ((π§ β π΄ β¦ (((πΉβπ§) β (πΉβπ΅)) + (πΉβπ΅))) limβ π΅)) |
106 | 31 | addid2d 8081 |
. . . . . 6
β’ (((π β β β§ πΉ:π΄βΆβ β§ π΄ β π) β§ π΅(π D πΉ)π¦) β (0 + (πΉβπ΅)) = (πΉβπ΅)) |
107 | 30, 32 | npcand 8246 |
. . . . . . . . 9
β’ ((((π β β β§ πΉ:π΄βΆβ β§ π΄ β π) β§ π΅(π D πΉ)π¦) β§ π§ β π΄) β (((πΉβπ§) β (πΉβπ΅)) + (πΉβπ΅)) = (πΉβπ§)) |
108 | 107 | mpteq2dva 4088 |
. . . . . . . 8
β’ (((π β β β§ πΉ:π΄βΆβ β§ π΄ β π) β§ π΅(π D πΉ)π¦) β (π§ β π΄ β¦ (((πΉβπ§) β (πΉβπ΅)) + (πΉβπ΅))) = (π§ β π΄ β¦ (πΉβπ§))) |
109 | 6 | feqmptd 5561 |
. . . . . . . 8
β’ (((π β β β§ πΉ:π΄βΆβ β§ π΄ β π) β§ π΅(π D πΉ)π¦) β πΉ = (π§ β π΄ β¦ (πΉβπ§))) |
110 | 108, 109 | eqtr4d 2211 |
. . . . . . 7
β’ (((π β β β§ πΉ:π΄βΆβ β§ π΄ β π) β§ π΅(π D πΉ)π¦) β (π§ β π΄ β¦ (((πΉβπ§) β (πΉβπ΅)) + (πΉβπ΅))) = πΉ) |
111 | 110 | oveq1d 5880 |
. . . . . 6
β’ (((π β β β§ πΉ:π΄βΆβ β§ π΄ β π) β§ π΅(π D πΉ)π¦) β ((π§ β π΄ β¦ (((πΉβπ§) β (πΉβπ΅)) + (πΉβπ΅))) limβ π΅) = (πΉ limβ π΅)) |
112 | 105, 106,
111 | 3eltr3d 2258 |
. . . . 5
β’ (((π β β β§ πΉ:π΄βΆβ β§ π΄ β π) β§ π΅(π D πΉ)π¦) β (πΉβπ΅) β (πΉ limβ π΅)) |
113 | 1, 2, 5, 6, 29, 112 | cnplimclemr 13631 |
. . . 4
β’ (((π β β β§ πΉ:π΄βΆβ β§ π΄ β π) β§ π΅(π D πΉ)π¦) β πΉ β ((π½ CnP πΎ)βπ΅)) |
114 | 113 | ex 115 |
. . 3
β’ ((π β β β§ πΉ:π΄βΆβ β§ π΄ β π) β (π΅(π D πΉ)π¦ β πΉ β ((π½ CnP πΎ)βπ΅))) |
115 | 114 | exlimdv 1817 |
. 2
β’ ((π β β β§ πΉ:π΄βΆβ β§ π΄ β π) β (βπ¦ π΅(π D πΉ)π¦ β πΉ β ((π½ CnP πΎ)βπ΅))) |
116 | | eldmg 4815 |
. . 3
β’ (π΅ β dom (π D πΉ) β (π΅ β dom (π D πΉ) β βπ¦ π΅(π D πΉ)π¦)) |
117 | 116 | ibi 176 |
. 2
β’ (π΅ β dom (π D πΉ) β βπ¦ π΅(π D πΉ)π¦) |
118 | 115, 117 | impel 280 |
1
β’ (((π β β β§ πΉ:π΄βΆβ β§ π΄ β π) β§ π΅ β dom (π D πΉ)) β πΉ β ((π½ CnP πΎ)βπ΅)) |