![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > dvmptid | Structured version Visualization version Unicode version |
Description: Function-builder for derivative: derivative of the identity. (Contributed by Mario Carneiro, 1-Sep-2014.) (Revised by Mario Carneiro, 11-Feb-2015.) |
Ref | Expression |
---|---|
dvmptid.1 |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Ref | Expression |
---|---|
dvmptid |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | eqid 2462 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
2 | dvmptid.1 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
3 | 1 | cnfldtopon 21858 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
4 | toponmax 19998 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
5 | 3, 4 | mp1i 13 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
6 | recnprss 22915 |
. . . 4
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
7 | 2, 6 | syl 17 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
8 | df-ss 3430 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
9 | 7, 8 | sylib 201 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
10 | simpr 467 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
11 | 1cnd 9690 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
12 | mptresid 5181 |
. . . . 5
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
13 | 12 | oveq2i 6331 |
. . . 4
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
14 | dvid 22928 |
. . . 4
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
15 | fconstmpt 4900 |
. . . 4
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
16 | 13, 14, 15 | 3eqtri 2488 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
17 | 16 | a1i 11 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
18 | 1, 2, 5, 9, 10, 11, 17 | dvmptres3 22966 |
1
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff setvar class |
Syntax hints: ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1680 ax-4 1693 ax-5 1769 ax-6 1816 ax-7 1862 ax-8 1900 ax-9 1907 ax-10 1926 ax-11 1931 ax-12 1944 ax-13 2102 ax-ext 2442 ax-rep 4531 ax-sep 4541 ax-nul 4550 ax-pow 4598 ax-pr 4656 ax-un 6615 ax-cnex 9626 ax-resscn 9627 ax-1cn 9628 ax-icn 9629 ax-addcl 9630 ax-addrcl 9631 ax-mulcl 9632 ax-mulrcl 9633 ax-mulcom 9634 ax-addass 9635 ax-mulass 9636 ax-distr 9637 ax-i2m1 9638 ax-1ne0 9639 ax-1rid 9640 ax-rnegex 9641 ax-rrecex 9642 ax-cnre 9643 ax-pre-lttri 9644 ax-pre-lttrn 9645 ax-pre-ltadd 9646 ax-pre-mulgt0 9647 ax-pre-sup 9648 |
This theorem depends on definitions: df-bi 190 df-or 376 df-an 377 df-3or 992 df-3an 993 df-tru 1458 df-ex 1675 df-nf 1679 df-sb 1809 df-eu 2314 df-mo 2315 df-clab 2449 df-cleq 2455 df-clel 2458 df-nfc 2592 df-ne 2635 df-nel 2636 df-ral 2754 df-rex 2755 df-reu 2756 df-rmo 2757 df-rab 2758 df-v 3059 df-sbc 3280 df-csb 3376 df-dif 3419 df-un 3421 df-in 3423 df-ss 3430 df-pss 3432 df-nul 3744 df-if 3894 df-pw 3965 df-sn 3981 df-pr 3983 df-tp 3985 df-op 3987 df-uni 4213 df-int 4249 df-iun 4294 df-iin 4295 df-br 4419 df-opab 4478 df-mpt 4479 df-tr 4514 df-eprel 4767 df-id 4771 df-po 4777 df-so 4778 df-fr 4815 df-we 4817 df-xp 4862 df-rel 4863 df-cnv 4864 df-co 4865 df-dm 4866 df-rn 4867 df-res 4868 df-ima 4869 df-pred 5403 df-ord 5449 df-on 5450 df-lim 5451 df-suc 5452 df-iota 5569 df-fun 5607 df-fn 5608 df-f 5609 df-f1 5610 df-fo 5611 df-f1o 5612 df-fv 5613 df-riota 6282 df-ov 6323 df-oprab 6324 df-mpt2 6325 df-om 6725 df-1st 6825 df-2nd 6826 df-wrecs 7059 df-recs 7121 df-rdg 7159 df-1o 7213 df-oadd 7217 df-er 7394 df-map 7505 df-pm 7506 df-en 7601 df-dom 7602 df-sdom 7603 df-fin 7604 df-fi 7956 df-sup 7987 df-inf 7988 df-pnf 9708 df-mnf 9709 df-xr 9710 df-ltxr 9711 df-le 9712 df-sub 9893 df-neg 9894 df-div 10303 df-nn 10643 df-2 10701 df-3 10702 df-4 10703 df-5 10704 df-6 10705 df-7 10706 df-8 10707 df-9 10708 df-10 10709 df-n0 10904 df-z 10972 df-dec 11086 df-uz 11194 df-q 11299 df-rp 11337 df-xneg 11443 df-xadd 11444 df-xmul 11445 df-icc 11676 df-fz 11820 df-seq 12252 df-exp 12311 df-cj 13217 df-re 13218 df-im 13219 df-sqrt 13353 df-abs 13354 df-struct 15178 df-ndx 15179 df-slot 15180 df-base 15181 df-plusg 15258 df-mulr 15259 df-starv 15260 df-tset 15264 df-ple 15265 df-ds 15267 df-unif 15268 df-rest 15376 df-topn 15377 df-topgen 15397 df-psmet 19017 df-xmet 19018 df-met 19019 df-bl 19020 df-mopn 19021 df-fbas 19022 df-fg 19023 df-cnfld 19026 df-top 19976 df-bases 19977 df-topon 19978 df-topsp 19979 df-cld 20089 df-ntr 20090 df-cls 20091 df-nei 20169 df-lp 20207 df-perf 20208 df-cn 20298 df-cnp 20299 df-haus 20386 df-fil 20916 df-fm 21008 df-flim 21009 df-flf 21010 df-xms 21390 df-ms 21391 df-cncf 21965 df-limc 22877 df-dv 22878 |
This theorem is referenced by: dvef 22988 dvsincos 22989 mvth 23000 dvlipcn 23002 dvivthlem1 23016 lhop2 23023 dvfsumle 23029 dvfsumabs 23031 dvfsumlem2 23035 dvtaylp 23381 taylthlem2 23385 pige3 23528 advlog 23655 advlogexp 23656 logtayl 23661 dvcxp1 23736 dvcxp2 23737 dvcncxp1 23739 loglesqrt 23754 dvatan 23917 lgamgulmlem2 24011 log2sumbnd 24438 dvasin 32074 areacirclem1 32078 lhe4.4ex1a 36723 expgrowthi 36727 expgrowth 36729 binomcxplemdvbinom 36747 dvsinax 37869 dvmptidg 37873 dvcosax 37884 itgiccshift 37943 itgperiod 37944 itgsbtaddcnst 37945 dirkeritg 38065 fourierdlem39 38110 fourierdlem56 38127 fourierdlem60 38131 fourierdlem61 38132 fourierdlem62 38133 etransclem46 38246 |
Copyright terms: Public domain | W3C validator |