![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > eldv | Structured version Visualization version GIF version |
Description: The differentiable predicate. A function πΉ is differentiable at π΅ with derivative πΆ iff πΉ is defined in a neighborhood of π΅ and the difference quotient has limit πΆ at π΅. (Contributed by Mario Carneiro, 7-Aug-2014.) (Revised by Mario Carneiro, 25-Dec-2016.) |
Ref | Expression |
---|---|
dvval.t | β’ π = (πΎ βΎt π) |
dvval.k | β’ πΎ = (TopOpenββfld) |
eldv.g | β’ πΊ = (π§ β (π΄ β {π΅}) β¦ (((πΉβπ§) β (πΉβπ΅)) / (π§ β π΅))) |
eldv.s | β’ (π β π β β) |
eldv.f | β’ (π β πΉ:π΄βΆβ) |
eldv.a | β’ (π β π΄ β π) |
Ref | Expression |
---|---|
eldv | β’ (π β (π΅(π D πΉ)πΆ β (π΅ β ((intβπ)βπ΄) β§ πΆ β (πΊ limβ π΅)))) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | eldv.s | . . . . 5 β’ (π β π β β) | |
2 | eldv.f | . . . . 5 β’ (π β πΉ:π΄βΆβ) | |
3 | eldv.a | . . . . 5 β’ (π β π΄ β π) | |
4 | dvval.t | . . . . . 6 β’ π = (πΎ βΎt π) | |
5 | dvval.k | . . . . . 6 β’ πΎ = (TopOpenββfld) | |
6 | 4, 5 | dvfval 25648 | . . . . 5 β’ ((π β β β§ πΉ:π΄βΆβ β§ π΄ β π) β ((π D πΉ) = βͺ π₯ β ((intβπ)βπ΄)({π₯} Γ ((π§ β (π΄ β {π₯}) β¦ (((πΉβπ§) β (πΉβπ₯)) / (π§ β π₯))) limβ π₯)) β§ (π D πΉ) β (((intβπ)βπ΄) Γ β))) |
7 | 1, 2, 3, 6 | syl3anc 1369 | . . . 4 β’ (π β ((π D πΉ) = βͺ π₯ β ((intβπ)βπ΄)({π₯} Γ ((π§ β (π΄ β {π₯}) β¦ (((πΉβπ§) β (πΉβπ₯)) / (π§ β π₯))) limβ π₯)) β§ (π D πΉ) β (((intβπ)βπ΄) Γ β))) |
8 | 7 | simpld 493 | . . 3 β’ (π β (π D πΉ) = βͺ π₯ β ((intβπ)βπ΄)({π₯} Γ ((π§ β (π΄ β {π₯}) β¦ (((πΉβπ§) β (πΉβπ₯)) / (π§ β π₯))) limβ π₯))) |
9 | 8 | eleq2d 2817 | . 2 β’ (π β (β¨π΅, πΆβ© β (π D πΉ) β β¨π΅, πΆβ© β βͺ π₯ β ((intβπ)βπ΄)({π₯} Γ ((π§ β (π΄ β {π₯}) β¦ (((πΉβπ§) β (πΉβπ₯)) / (π§ β π₯))) limβ π₯)))) |
10 | df-br 5150 | . . 3 β’ (π΅(π D πΉ)πΆ β β¨π΅, πΆβ© β (π D πΉ)) | |
11 | 10 | bicomi 223 | . 2 β’ (β¨π΅, πΆβ© β (π D πΉ) β π΅(π D πΉ)πΆ) |
12 | sneq 4639 | . . . . . . 7 β’ (π₯ = π΅ β {π₯} = {π΅}) | |
13 | 12 | difeq2d 4123 | . . . . . 6 β’ (π₯ = π΅ β (π΄ β {π₯}) = (π΄ β {π΅})) |
14 | fveq2 6892 | . . . . . . . 8 β’ (π₯ = π΅ β (πΉβπ₯) = (πΉβπ΅)) | |
15 | 14 | oveq2d 7429 | . . . . . . 7 β’ (π₯ = π΅ β ((πΉβπ§) β (πΉβπ₯)) = ((πΉβπ§) β (πΉβπ΅))) |
16 | oveq2 7421 | . . . . . . 7 β’ (π₯ = π΅ β (π§ β π₯) = (π§ β π΅)) | |
17 | 15, 16 | oveq12d 7431 | . . . . . 6 β’ (π₯ = π΅ β (((πΉβπ§) β (πΉβπ₯)) / (π§ β π₯)) = (((πΉβπ§) β (πΉβπ΅)) / (π§ β π΅))) |
18 | 13, 17 | mpteq12dv 5240 | . . . . 5 β’ (π₯ = π΅ β (π§ β (π΄ β {π₯}) β¦ (((πΉβπ§) β (πΉβπ₯)) / (π§ β π₯))) = (π§ β (π΄ β {π΅}) β¦ (((πΉβπ§) β (πΉβπ΅)) / (π§ β π΅)))) |
19 | eldv.g | . . . . 5 β’ πΊ = (π§ β (π΄ β {π΅}) β¦ (((πΉβπ§) β (πΉβπ΅)) / (π§ β π΅))) | |
20 | 18, 19 | eqtr4di 2788 | . . . 4 β’ (π₯ = π΅ β (π§ β (π΄ β {π₯}) β¦ (((πΉβπ§) β (πΉβπ₯)) / (π§ β π₯))) = πΊ) |
21 | id 22 | . . . 4 β’ (π₯ = π΅ β π₯ = π΅) | |
22 | 20, 21 | oveq12d 7431 | . . 3 β’ (π₯ = π΅ β ((π§ β (π΄ β {π₯}) β¦ (((πΉβπ§) β (πΉβπ₯)) / (π§ β π₯))) limβ π₯) = (πΊ limβ π΅)) |
23 | 22 | opeliunxp2 5839 | . 2 β’ (β¨π΅, πΆβ© β βͺ π₯ β ((intβπ)βπ΄)({π₯} Γ ((π§ β (π΄ β {π₯}) β¦ (((πΉβπ§) β (πΉβπ₯)) / (π§ β π₯))) limβ π₯)) β (π΅ β ((intβπ)βπ΄) β§ πΆ β (πΊ limβ π΅))) |
24 | 9, 11, 23 | 3bitr3g 312 | 1 β’ (π β (π΅(π D πΉ)πΆ β (π΅ β ((intβπ)βπ΄) β§ πΆ β (πΊ limβ π΅)))) |
Colors of variables: wff setvar class |
Syntax hints: β wi 4 β wb 205 β§ wa 394 = wceq 1539 β wcel 2104 β cdif 3946 β wss 3949 {csn 4629 β¨cop 4635 βͺ ciun 4998 class class class wbr 5149 β¦ cmpt 5232 Γ cxp 5675 βΆwf 6540 βcfv 6544 (class class class)co 7413 βcc 11112 β cmin 11450 / cdiv 11877 βΎt crest 17372 TopOpenctopn 17373 βfldccnfld 21146 intcnt 22743 limβ climc 25613 D cdv 25614 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1911 ax-6 1969 ax-7 2009 ax-8 2106 ax-9 2114 ax-10 2135 ax-11 2152 ax-12 2169 ax-ext 2701 ax-rep 5286 ax-sep 5300 ax-nul 5307 ax-pow 5364 ax-pr 5428 ax-un 7729 ax-cnex 11170 ax-resscn 11171 ax-1cn 11172 ax-icn 11173 ax-addcl 11174 ax-addrcl 11175 ax-mulcl 11176 ax-mulrcl 11177 ax-mulcom 11178 ax-addass 11179 ax-mulass 11180 ax-distr 11181 ax-i2m1 11182 ax-1ne0 11183 ax-1rid 11184 ax-rnegex 11185 ax-rrecex 11186 ax-cnre 11187 ax-pre-lttri 11188 ax-pre-lttrn 11189 ax-pre-ltadd 11190 ax-pre-mulgt0 11191 ax-pre-sup 11192 |
This theorem depends on definitions: df-bi 206 df-an 395 df-or 844 df-3or 1086 df-3an 1087 df-tru 1542 df-fal 1552 df-ex 1780 df-nf 1784 df-sb 2066 df-mo 2532 df-eu 2561 df-clab 2708 df-cleq 2722 df-clel 2808 df-nfc 2883 df-ne 2939 df-nel 3045 df-ral 3060 df-rex 3069 df-rmo 3374 df-reu 3375 df-rab 3431 df-v 3474 df-sbc 3779 df-csb 3895 df-dif 3952 df-un 3954 df-in 3956 df-ss 3966 df-pss 3968 df-nul 4324 df-if 4530 df-pw 4605 df-sn 4630 df-pr 4632 df-tp 4634 df-op 4636 df-uni 4910 df-int 4952 df-iun 5000 df-br 5150 df-opab 5212 df-mpt 5233 df-tr 5267 df-id 5575 df-eprel 5581 df-po 5589 df-so 5590 df-fr 5632 df-we 5634 df-xp 5683 df-rel 5684 df-cnv 5685 df-co 5686 df-dm 5687 df-rn 5688 df-res 5689 df-ima 5690 df-pred 6301 df-ord 6368 df-on 6369 df-lim 6370 df-suc 6371 df-iota 6496 df-fun 6546 df-fn 6547 df-f 6548 df-f1 6549 df-fo 6550 df-f1o 6551 df-fv 6552 df-riota 7369 df-ov 7416 df-oprab 7417 df-mpo 7418 df-om 7860 df-1st 7979 df-2nd 7980 df-frecs 8270 df-wrecs 8301 df-recs 8375 df-rdg 8414 df-1o 8470 df-er 8707 df-map 8826 df-pm 8827 df-en 8944 df-dom 8945 df-sdom 8946 df-fin 8947 df-fi 9410 df-sup 9441 df-inf 9442 df-pnf 11256 df-mnf 11257 df-xr 11258 df-ltxr 11259 df-le 11260 df-sub 11452 df-neg 11453 df-div 11878 df-nn 12219 df-2 12281 df-3 12282 df-4 12283 df-5 12284 df-6 12285 df-7 12286 df-8 12287 df-9 12288 df-n0 12479 df-z 12565 df-dec 12684 df-uz 12829 df-q 12939 df-rp 12981 df-xneg 13098 df-xadd 13099 df-xmul 13100 df-fz 13491 df-seq 13973 df-exp 14034 df-cj 15052 df-re 15053 df-im 15054 df-sqrt 15188 df-abs 15189 df-struct 17086 df-slot 17121 df-ndx 17133 df-base 17151 df-plusg 17216 df-mulr 17217 df-starv 17218 df-tset 17222 df-ple 17223 df-ds 17225 df-unif 17226 df-rest 17374 df-topn 17375 df-topgen 17395 df-psmet 21138 df-xmet 21139 df-met 21140 df-bl 21141 df-mopn 21142 df-cnfld 21147 df-top 22618 df-topon 22635 df-topsp 22657 df-bases 22671 df-cnp 22954 df-xms 24048 df-ms 24049 df-limc 25617 df-dv 25618 |
This theorem is referenced by: dvcl 25650 perfdvf 25654 dvreslem 25660 dvres2lem 25661 dvidlem 25666 dvcnp 25670 dvcnp2 25671 dvaddbr 25689 dvmulbr 25690 dvcobr 25697 dvcjbr 25700 dvrec 25706 dvcnvlem 25727 dveflem 25730 dvferm1 25736 dvferm2 25738 ftc1 25793 taylthlem1 26119 ulmdvlem3 26148 gg-dvcnp2 35462 gg-dvmulbr 35463 gg-dvcobr 35464 unbdqndv1 35689 ftc1cnnc 36865 fperdvper 44935 |
Copyright terms: Public domain | W3C validator |