dvexp - Intuitionistic Logic Explorer

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

Theorem dvexp 15216

Description: Derivative of a power function. (Contributed by Mario Carneiro, 9-Aug-2014.) (Revised by Mario Carneiro, 10-Feb-2015.)

**Assertion**
Ref	Expression
dvexp

Distinct variable group:

Proof of Theorem dvexp Dummy variables

are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		oveq2 5954	. . . . 5
2	1	mpteq2dv 4136	. . . 4
3	2	oveq2d 5962	. . 3
4		id 19	. . . . 5
5		oveq1 5953	. . . . . 6
6	5	oveq2d 5962	. . . . 5
7	4, 6	oveq12d 5964	. . . 4
8	7	mpteq2dv 4136	. . 3
9	3, 8	eqeq12d 2220	. 2
10		oveq2 5954	. . . . 5
11	10	mpteq2dv 4136	. . . 4
12	11	oveq2d 5962	. . 3
13		id 19	. . . . 5
14		oveq1 5953	. . . . . 6
15	14	oveq2d 5962	. . . . 5
16	13, 15	oveq12d 5964	. . . 4
17	16	mpteq2dv 4136	. . 3
18	12, 17	eqeq12d 2220	. 2
19		oveq2 5954	. . . . 5
20	19	mpteq2dv 4136	. . . 4
21	20	oveq2d 5962	. . 3
22		id 19	. . . . 5
23		oveq1 5953	. . . . . 6
24	23	oveq2d 5962	. . . . 5
25	22, 24	oveq12d 5964	. . . 4
26	25	mpteq2dv 4136	. . 3
27	21, 26	eqeq12d 2220	. 2
28		oveq2 5954	. . . . 5
29	28	mpteq2dv 4136	. . . 4
30	29	oveq2d 5962	. . 3
31		id 19	. . . . 5
32		oveq1 5953	. . . . . 6
33	32	oveq2d 5962	. . . . 5
34	31, 33	oveq12d 5964	. . . 4
35	34	mpteq2dv 4136	. . 3
36	30, 35	eqeq12d 2220	. 2
37		exp1 10692	. . . . . 6
38	37	mpteq2ia 4131	. . . . 5
39		mptresid 5014	. . . . 5
40	38, 39	eqtr4i 2229	. . . 4
41	40	oveq2i 5957	. . 3
42		1m1e0 9107	. . . . . . . . . 10
43	42	oveq2i 5957	. . . . . . . . 9
44		exp0 10690	. . . . . . . . 9
45	43, 44	eqtrid 2250	. . . . . . . 8
46	45	oveq2d 5962	. . . . . . 7
47		1t1e1 9191	. . . . . . 7
48	46, 47	eqtrdi 2254	. . . . . 6
49	48	mpteq2ia 4131	. . . . 5
50		fconstmpt 4723	. . . . 5
51	49, 50	eqtr4i 2229	. . . 4
52		dvid 15200	. . . 4
53	51, 52	eqtr4i 2229	. . 3
54	41, 53	eqtr4i 2229	. 2
55		nncn 9046	. . . . . . . . . . . 12
56	55	adantr 276	. . . . . . . . . . 11 $/\$
57		ax-1cn 8020	. . . . . . . . . . 11
58		pncan 8280	. . . . . . . . . . 11 $/\$
59	56, 57, 58	sylancl 413	. . . . . . . . . 10 $/\$
60	59	oveq2d 5962	. . . . . . . . 9 $/\$
61	60	oveq2d 5962	. . . . . . . 8 $/\$
62	57	a1i 9	. . . . . . . . 9 $/\$
63		id 19	. . . . . . . . . 10
64		nnnn0 9304	. . . . . . . . . 10
65		expcl 10704	. . . . . . . . . 10 $/\$
66	63, 64, 65	syl2anr 290	. . . . . . . . 9 $/\$
67	56, 62, 66	adddird 8100	. . . . . . . 8 $/\$
68	66	mulid2d 8093	. . . . . . . . 9 $/\$
69	68	oveq2d 5962	. . . . . . . 8 $/\$
70	61, 67, 69	3eqtrd 2242	. . . . . . 7 $/\$
71	70	mpteq2dva 4135	. . . . . 6
72		cnex 8051	. . . . . . . 8
73	72	a1i 9	. . . . . . 7
74	56, 66	mulcld 8095	. . . . . . 7 $/\$
75		nnm1nn0 9338	. . . . . . . . . . 11
76		expcl 10704	. . . . . . . . . . 11 $/\$
77	63, 75, 76	syl2anr 290	. . . . . . . . . 10 $/\$
78	56, 77	mulcld 8095	. . . . . . . . 9 $/\$
79		simpr 110	. . . . . . . . 9 $/\$
80		eqidd 2206	. . . . . . . . 9
81	39	a1i 9	. . . . . . . . 9
82	73, 78, 79, 80, 81	offval2 6176	. . . . . . . 8
83	56, 77, 79	mulassd 8098	. . . . . . . . . 10 $/\$
84		expm1t 10714	. . . . . . . . . . . 12 $/\$
85	84	ancoms 268	. . . . . . . . . . 11 $/\$
86	85	oveq2d 5962	. . . . . . . . . 10 $/\$
87	83, 86	eqtr4d 2241	. . . . . . . . 9 $/\$
88	87	mpteq2dva 4135	. . . . . . . 8
89	82, 88	eqtrd 2238	. . . . . . 7
90	52, 50	eqtri 2226	. . . . . . . . . 10
91	90	a1i 9	. . . . . . . . 9
92		eqidd 2206	. . . . . . . . 9
93	73, 62, 66, 91, 92	offval2 6176	. . . . . . . 8
94	68	mpteq2dva 4135	. . . . . . . 8
95	93, 94	eqtrd 2238	. . . . . . 7
96	73, 74, 66, 89, 95	offval2 6176	. . . . . 6
97	71, 96	eqtr4d 2241	. . . . 5
98		oveq1 5953	. . . . . . 7
99	98	oveq1d 5961	. . . . . 6
100	99	eqcomd 2211	. . . . 5
101	97, 100	sylan9eq 2258	. . . 4 $/\$
102		cnelprrecn 8063	. . . . . 6
103	102	a1i 9	. . . . 5 $/\$
104		ssidd 3214	. . . . 5 $/\$
105	66	fmpttd 5737	. . . . . 6
106	105	adantr 276	. . . . 5 $/\$
107		f1oi 5562	. . . . . 6
108		f1of 5524	. . . . . 6
109	107, 108	mp1i 10	. . . . 5 $/\$
110		simpr 110	. . . . . . 7 $/\$
111	110	dmeqd 4881	. . . . . 6 $/\$
112	78	fmpttd 5737	. . . . . . . 8
113	112	adantr 276	. . . . . . 7 $/\$
114	113	fdmd 5434	. . . . . 6 $/\$
115	111, 114	eqtrd 2238	. . . . 5 $/\$
116		1ex 8069	. . . . . . . . 9
117	116	fconst 5473	. . . . . . . 8
118	52	feq1i 5420	. . . . . . . 8
119	117, 118	mpbir 146	. . . . . . 7
120	119	fdmi 5435	. . . . . 6
121	120	a1i 9	. . . . 5 $/\$
122	103, 104, 106, 109, 115, 121	dvimulf 15211	. . . 4 $/\$
123	73, 66, 79, 92, 81	offval2 6176	. . . . . . 7
124		expp1 10693	. . . . . . . . 9 $/\$
125	63, 64, 124	syl2anr 290	. . . . . . . 8 $/\$
126	125	mpteq2dva 4135	. . . . . . 7
127	123, 126	eqtr4d 2241	. . . . . 6
128	127	oveq2d 5962	. . . . 5
129	128	adantr 276	. . . 4 $/\$
130	101, 122, 129	3eqtr2rd 2245	. . 3 $/\$
131	130	ex 115	. 2
132	9, 18, 27, 36, 54, 131	nnind 9054	1

Colors of variables: wff set class

Syntax hints:

wi 4 $/\$ wa 104

wceq 1373

wcel 2176

cvv 2772

csn 3633

cpr 3634

cmpt 4106

cid 4336

cxp 4674

cdm 4676

cres 4678

wf 5268

wf1o 5271 (class class class)co 5946

cof 6158

cc 7925

cr 7926

cc0 7927

c1 7928

caddc 7930

cmul 7932

cmin 8245

cn 9038

cn0 9297

cexp 10685

cdv 15160

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 106 ax-ia2 107 ax-ia3 108 ax-in1 615 ax-in2 616 ax-io 711 ax-5 1470 ax-7 1471 ax-gen 1472 ax-ie1 1516 ax-ie2 1517 ax-8 1527 ax-10 1528 ax-11 1529 ax-i12 1530 ax-bndl 1532 ax-4 1533 ax-17 1549 ax-i9 1553 ax-ial 1557 ax-i5r 1558 ax-13 2178 ax-14 2179 ax-ext 2187 ax-coll 4160 ax-sep 4163 ax-nul 4171 ax-pow 4219 ax-pr 4254 ax-un 4481 ax-setind 4586 ax-iinf 4637 ax-cnex 8018 ax-resscn 8019 ax-1cn 8020 ax-1re 8021 ax-icn 8022 ax-addcl 8023 ax-addrcl 8024 ax-mulcl 8025 ax-mulrcl 8026 ax-addcom 8027 ax-mulcom 8028 ax-addass 8029 ax-mulass 8030 ax-distr 8031 ax-i2m1 8032 ax-0lt1 8033 ax-1rid 8034 ax-0id 8035 ax-rnegex 8036 ax-precex 8037 ax-cnre 8038 ax-pre-ltirr 8039 ax-pre-ltwlin 8040 ax-pre-lttrn 8041 ax-pre-apti 8042 ax-pre-ltadd 8043 ax-pre-mulgt0 8044 ax-pre-mulext 8045 ax-arch 8046 ax-caucvg 8047 ax-addf 8049 ax-mulf 8050

This theorem depends on definitions: df-bi 117 df-stab 833 df-dc 837 df-3or 982 df-3an 983 df-tru 1376 df-fal 1379 df-nf 1484 df-sb 1786 df-eu 2057 df-mo 2058 df-clab 2192 df-cleq 2198 df-clel 2201 df-nfc 2337 df-ne 2377 df-nel 2472 df-ral 2489 df-rex 2490 df-reu 2491 df-rmo 2492 df-rab 2493 df-v 2774 df-sbc 2999 df-csb 3094 df-dif 3168 df-un 3170 df-in 3172 df-ss 3179 df-nul 3461 df-if 3572 df-pw 3618 df-sn 3639 df-pr 3640 df-op 3642 df-uni 3851 df-int 3886 df-iun 3929 df-br 4046 df-opab 4107 df-mpt 4108 df-tr 4144 df-id 4341 df-po 4344 df-iso 4345 df-iord 4414 df-on 4416 df-ilim 4417 df-suc 4419 df-iom 4640 df-xp 4682 df-rel 4683 df-cnv 4684 df-co 4685 df-dm 4686 df-rn 4687 df-res 4688 df-ima 4689 df-iota 5233 df-fun 5274 df-fn 5275 df-f 5276 df-f1 5277 df-fo 5278 df-f1o 5279 df-fv 5280 df-isom 5281 df-riota 5901 df-ov 5949 df-oprab 5950 df-mpo 5951 df-of 6160 df-1st 6228 df-2nd 6229 df-recs 6393 df-frec 6479 df-map 6739 df-pm 6740 df-sup 7088 df-inf 7089 df-pnf 8111 df-mnf 8112 df-xr 8113 df-ltxr 8114 df-le 8115 df-sub 8247 df-neg 8248 df-reap 8650 df-ap 8657 df-div 8748 df-inn 9039 df-2 9097 df-3 9098 df-4 9099 df-n0 9298 df-z 9375 df-uz 9651 df-q 9743 df-rp 9778 df-xneg 9896 df-xadd 9897 df-seqfrec 10595 df-exp 10686 df-cj 11186 df-re 11187 df-im 11188 df-rsqrt 11342 df-abs 11343 df-rest 13106 df-topgen 13125 df-psmet 14338 df-xmet 14339 df-met 14340 df-bl 14341 df-mopn 14342 df-top 14503 df-topon 14516 df-bases 14548 df-ntr 14601 df-cn 14693 df-cnp 14694 df-tx 14758 df-cncf 15076 df-limced 15161 df-dvap 15162

This theorem is referenced by: dvexp2 15217

W3C validator