Intuitionistic Logic Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  ILE Home  >  Th. List  >  dvcnp2cntop Unicode version

Theorem dvcnp2cntop 13010
 Description: A function is continuous at each point for which it is differentiable. (Contributed by Mario Carneiro, 9-Aug-2014.) (Revised by Mario Carneiro, 28-Dec-2016.)
Hypotheses
Ref Expression
dvcnp.j t
dvcnpcntop.k
Assertion
Ref Expression
dvcnp2cntop

Proof of Theorem dvcnp2cntop
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 dvcnpcntop.k . . . . 5
2 dvcnp.j . . . . 5 t
3 simpl3 987 . . . . . 6
4 simpl1 985 . . . . . 6
53, 4sstrd 3134 . . . . 5
6 simpl2 986 . . . . 5
71cntoptop 12880 . . . . . . . 8
8 cnex 7835 . . . . . . . . 9
9 ssexg 4099 . . . . . . . . 9
104, 8, 9sylancl 410 . . . . . . . 8
11 resttop 12517 . . . . . . . 8 t
127, 10, 11sylancr 411 . . . . . . 7 t
131cntoptopon 12879 . . . . . . . . . 10 TopOn
14 resttopon 12518 . . . . . . . . . 10 TopOn t TopOn
1513, 4, 14sylancr 411 . . . . . . . . 9 t TopOn
16 toponuni 12360 . . . . . . . . 9 t TopOn t
1715, 16syl 14 . . . . . . . 8 t
183, 17sseqtrd 3162 . . . . . . 7 t
19 eqid 2154 . . . . . . . 8 t t
2019ntrss2 12468 . . . . . . 7 t t t
2112, 18, 20syl2anc 409 . . . . . 6 t
22 eqid 2154 . . . . . . . 8 t t
23 eqid 2154 . . . . . . . 8 # #
24 simp1 982 . . . . . . . 8
25 simp2 983 . . . . . . . 8
26 simp3 984 . . . . . . . 8
2722, 1, 23, 24, 25, 26eldvap 12998 . . . . . . 7 t # lim
2827simprbda 381 . . . . . 6 t
2921, 28sseldd 3125 . . . . 5
306ffvelrnda 5595 . . . . . . . 8
316, 29ffvelrnd 5596 . . . . . . . . 9
3231adantr 274 . . . . . . . 8
3330, 32subcld 8165 . . . . . . 7
34 ssid 3144 . . . . . . . 8
3534a1i 9 . . . . . . 7
36 txtopon 12609 . . . . . . . . 9 TopOn TopOn TopOn
3713, 13, 36mp2an 423 . . . . . . . 8 TopOn
3837toponrestid 12366 . . . . . . 7 t
396, 5, 29dvlemap 12996 . . . . . . . . . 10 #
40 ssrab2 3209 . . . . . . . . . . . . 13 #
4140, 5sstrid 3135 . . . . . . . . . . . 12 #
4241sselda 3124 . . . . . . . . . . 11 #
435, 29sseldd 3125 . . . . . . . . . . . 12
4443adantr 274 . . . . . . . . . . 11 #
4542, 44subcld 8165 . . . . . . . . . 10 #
4627simplbda 382 . . . . . . . . . 10 # lim
47 limcresi 12982 . . . . . . . . . . . 12 lim # lim
48 resmpt 4907 . . . . . . . . . . . . . 14 # # #
4940, 48ax-mp 5 . . . . . . . . . . . . 13 # #
5049oveq1i 5824 . . . . . . . . . . . 12 # lim # lim
5147, 50sseqtri 3158 . . . . . . . . . . 11 lim # lim
5243subidd 8153 . . . . . . . . . . . 12
531subcncntop 12900 . . . . . . . . . . . . . . 15
5453a1i 9 . . . . . . . . . . . . . 14
55 cncfmptid 12930 . . . . . . . . . . . . . . 15
565, 34, 55sylancl 410 . . . . . . . . . . . . . 14
57 cncfmptc 12929 . . . . . . . . . . . . . . 15
5843, 5, 35, 57syl3anc 1217 . . . . . . . . . . . . . 14
591, 54, 56, 58cncfmpt2fcntop 12932 . . . . . . . . . . . . 13
60 oveq1 5821 . . . . . . . . . . . . 13
6159, 29, 60cnmptlimc 12990 . . . . . . . . . . . 12 lim
6252, 61eqeltrrd 2232 . . . . . . . . . . 11 lim
6351, 62sseldi 3122 . . . . . . . . . 10 # lim
641mulcncntop 12901 . . . . . . . . . . 11
6524, 25, 26dvcl 12999 . . . . . . . . . . . 12
66 0cn 7849 . . . . . . . . . . . 12
67 opelxpi 4611 . . . . . . . . . . . 12
6865, 66, 67sylancl 410 . . . . . . . . . . 11
6937toponunii 12362 . . . . . . . . . . . 12
7069cncnpi 12575 . . . . . . . . . . 11
7164, 68, 70sylancr 411 . . . . . . . . . 10
7239, 45, 35, 35, 1, 38, 46, 63, 71limccnp2cntop 12993 . . . . . . . . 9 # lim
7365mul01d 8247 . . . . . . . . 9
746adantr 274 . . . . . . . . . . . . . 14 #
75 simpr 109 . . . . . . . . . . . . . . 15 # #
7640, 75sseldi 3122 . . . . . . . . . . . . . 14 #
7774, 76ffvelrnd 5596 . . . . . . . . . . . . 13 #
7831adantr 274 . . . . . . . . . . . . 13 #
7977, 78subcld 8165 . . . . . . . . . . . 12 #
80 breq1 3964 . . . . . . . . . . . . . . . 16 # #
8180elrab 2864 . . . . . . . . . . . . . . 15 # #
8281simprbi 273 . . . . . . . . . . . . . 14 # #
8382adantl 275 . . . . . . . . . . . . 13 # #
8442, 44, 83subap0d 8498 . . . . . . . . . . . 12 # #
8579, 45, 84divcanap1d 8643 . . . . . . . . . . 11 #
8685mpteq2dva 4050 . . . . . . . . . 10 # #
8786oveq1d 5829 . . . . . . . . 9 # lim # lim
8872, 73, 873eltr3d 2237 . . . . . . . 8 # lim
8933fmpttd 5615 . . . . . . . . . 10
9089, 5limcdifap 12978 . . . . . . . . 9 lim # lim
91 resmpt 4907 . . . . . . . . . . 11 # # #
9240, 91ax-mp 5 . . . . . . . . . 10 # #
9392oveq1i 5824 . . . . . . . . 9 # lim # lim
9490, 93eqtrdi 2203 . . . . . . . 8 lim # lim
9588, 94eleqtrrd 2234 . . . . . . 7 lim
96 cncfmptc 12929 . . . . . . . . 9
9731, 5, 35, 96syl3anc 1217 . . . . . . . 8
98 eqidd 2155 . . . . . . . 8
9997, 29, 98cnmptlimc 12990 . . . . . . 7 lim
1001addcncntop 12899 . . . . . . . 8
101 opelxpi 4611 . . . . . . . . 9
10266, 31, 101sylancr 411 . . . . . . . 8
10369cncnpi 12575 . . . . . . . 8
104100, 102, 103sylancr 411 . . . . . . 7
10533, 32, 35, 35, 1, 38, 95, 99, 104limccnp2cntop 12993 . . . . . 6 lim
10631addid2d 8004 . . . . . 6
10730, 32npcand 8169 . . . . . . . . 9
108107mpteq2dva 4050 . . . . . . . 8
1096feqmptd 5514 . . . . . . . 8
110108, 109eqtr4d 2190 . . . . . . 7
111110oveq1d 5829 . . . . . 6 lim lim
112105, 106, 1113eltr3d 2237 . . . . 5 lim
1131, 2, 5, 6, 29, 112cnplimclemr 12985 . . . 4
114113ex 114 . . 3
115114exlimdv 1796 . 2
116 eldmg 4774 . . 3
117116ibi 175 . 2
118115, 117impel 278 1
 Colors of variables: wff set class Syntax hints:   wi 4   wa 103   w3a 963   wceq 1332  wex 1469   wcel 2125  crab 2436  cvv 2709   wss 3098  cop 3559  cuni 3768   class class class wbr 3961   cmpt 4021   cxp 4577   cdm 4579   cres 4581   ccom 4583  wf 5159  cfv 5163  (class class class)co 5814  cc 7709  cc0 7711   caddc 7714   cmul 7716   cmin 8025   # cap 8435   cdiv 8524  cabs 10874   ↾t crest 12298  cmopn 12332  ctop 12342  TopOnctopon 12355  cnt 12440   ccn 12532   ccnp 12533   ctx 12599  ccncf 12904   lim climc 12970   cdv 12971 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-in1 604  ax-in2 605  ax-io 699  ax-5 1424  ax-7 1425  ax-gen 1426  ax-ie1 1470  ax-ie2 1471  ax-8 1481  ax-10 1482  ax-11 1483  ax-i12 1484  ax-bndl 1486  ax-4 1487  ax-17 1503  ax-i9 1507  ax-ial 1511  ax-i5r 1512  ax-13 2127  ax-14 2128  ax-ext 2136  ax-coll 4075  ax-sep 4078  ax-nul 4086  ax-pow 4130  ax-pr 4164  ax-un 4388  ax-setind 4490  ax-iinf 4541  ax-cnex 7802  ax-resscn 7803  ax-1cn 7804  ax-1re 7805  ax-icn 7806  ax-addcl 7807  ax-addrcl 7808  ax-mulcl 7809  ax-mulrcl 7810  ax-addcom 7811  ax-mulcom 7812  ax-addass 7813  ax-mulass 7814  ax-distr 7815  ax-i2m1 7816  ax-0lt1 7817  ax-1rid 7818  ax-0id 7819  ax-rnegex 7820  ax-precex 7821  ax-cnre 7822  ax-pre-ltirr 7823  ax-pre-ltwlin 7824  ax-pre-lttrn 7825  ax-pre-apti 7826  ax-pre-ltadd 7827  ax-pre-mulgt0 7828  ax-pre-mulext 7829  ax-arch 7830  ax-caucvg 7831  ax-addf 7833  ax-mulf 7834 This theorem depends on definitions:  df-bi 116  df-stab 817  df-dc 821  df-3or 964  df-3an 965  df-tru 1335  df-fal 1338  df-nf 1438  df-sb 1740  df-eu 2006  df-mo 2007  df-clab 2141  df-cleq 2147  df-clel 2150  df-nfc 2285  df-ne 2325  df-nel 2420  df-ral 2437  df-rex 2438  df-reu 2439  df-rmo 2440  df-rab 2441  df-v 2711  df-sbc 2934  df-csb 3028  df-dif 3100  df-un 3102  df-in 3104  df-ss 3111  df-nul 3391  df-if 3502  df-pw 3541  df-sn 3562  df-pr 3563  df-op 3565  df-uni 3769  df-int 3804  df-iun 3847  df-br 3962  df-opab 4022  df-mpt 4023  df-tr 4059  df-id 4248  df-po 4251  df-iso 4252  df-iord 4321  df-on 4323  df-ilim 4324  df-suc 4326  df-iom 4544  df-xp 4585  df-rel 4586  df-cnv 4587  df-co 4588  df-dm 4589  df-rn 4590  df-res 4591  df-ima 4592  df-iota 5128  df-fun 5165  df-fn 5166  df-f 5167  df-f1 5168  df-fo 5169  df-f1o 5170  df-fv 5171  df-isom 5172  df-riota 5770  df-ov 5817  df-oprab 5818  df-mpo 5819  df-1st 6078  df-2nd 6079  df-recs 6242  df-frec 6328  df-map 6584  df-pm 6585  df-sup 6916  df-inf 6917  df-pnf 7893  df-mnf 7894  df-xr 7895  df-ltxr 7896  df-le 7897  df-sub 8027  df-neg 8028  df-reap 8429  df-ap 8436  df-div 8525  df-inn 8813  df-2 8871  df-3 8872  df-4 8873  df-n0 9070  df-z 9147  df-uz 9419  df-q 9507  df-rp 9539  df-xneg 9657  df-xadd 9658  df-seqfrec 10323  df-exp 10397  df-cj 10719  df-re 10720  df-im 10721  df-rsqrt 10875  df-abs 10876  df-rest 12300  df-topgen 12319  df-psmet 12334  df-xmet 12335  df-met 12336  df-bl 12337  df-mopn 12338  df-top 12343  df-topon 12356  df-bases 12388  df-ntr 12443  df-cn 12535  df-cnp 12536  df-tx 12600  df-cncf 12905  df-limced 12972  df-dvap 12973 This theorem is referenced by:  dvcn  13011  dvmulxxbr  13013  dvcoapbr  13018
 Copyright terms: Public domain W3C validator