dvexp - Intuitionistic Logic Explorer

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

Theorem dvexp 13035

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 5826	. . . . 5
2	1	mpteq2dv 4055	. . . 4
3	2	oveq2d 5834	. . 3
4		id 19	. . . . 5
5		oveq1 5825	. . . . . 6
6	5	oveq2d 5834	. . . . 5
7	4, 6	oveq12d 5836	. . . 4
8	7	mpteq2dv 4055	. . 3
9	3, 8	eqeq12d 2172	. 2
10		oveq2 5826	. . . . 5
11	10	mpteq2dv 4055	. . . 4
12	11	oveq2d 5834	. . 3
13		id 19	. . . . 5
14		oveq1 5825	. . . . . 6
15	14	oveq2d 5834	. . . . 5
16	13, 15	oveq12d 5836	. . . 4
17	16	mpteq2dv 4055	. . 3
18	12, 17	eqeq12d 2172	. 2
19		oveq2 5826	. . . . 5
20	19	mpteq2dv 4055	. . . 4
21	20	oveq2d 5834	. . 3
22		id 19	. . . . 5
23		oveq1 5825	. . . . . 6
24	23	oveq2d 5834	. . . . 5
25	22, 24	oveq12d 5836	. . . 4
26	25	mpteq2dv 4055	. . 3
27	21, 26	eqeq12d 2172	. 2
28		oveq2 5826	. . . . 5
29	28	mpteq2dv 4055	. . . 4
30	29	oveq2d 5834	. . 3
31		id 19	. . . . 5
32		oveq1 5825	. . . . . 6
33	32	oveq2d 5834	. . . . 5
34	31, 33	oveq12d 5836	. . . 4
35	34	mpteq2dv 4055	. . 3
36	30, 35	eqeq12d 2172	. 2
37		exp1 10407	. . . . . 6
38	37	mpteq2ia 4050	. . . . 5
39		mptresid 4917	. . . . 5
40	38, 39	eqtri 2178	. . . 4
41	40	oveq2i 5829	. . 3
42		1m1e0 8885	. . . . . . . . . 10
43	42	oveq2i 5829	. . . . . . . . 9
44		exp0 10405	. . . . . . . . 9
45	43, 44	syl5eq 2202	. . . . . . . 8
46	45	oveq2d 5834	. . . . . . 7
47		1t1e1 8968	. . . . . . 7
48	46, 47	eqtrdi 2206	. . . . . 6
49	48	mpteq2ia 4050	. . . . 5
50		fconstmpt 4630	. . . . 5
51	49, 50	eqtr4i 2181	. . . 4
52		dvid 13022	. . . 4
53	51, 52	eqtr4i 2181	. . 3
54	41, 53	eqtr4i 2181	. 2
55		nncn 8824	. . . . . . . . . . . 12
56	55	adantr 274	. . . . . . . . . . 11 $/\$
57		ax-1cn 7808	. . . . . . . . . . 11
58		pncan 8064	. . . . . . . . . . 11 $/\$
59	56, 57, 58	sylancl 410	. . . . . . . . . 10 $/\$
60	59	oveq2d 5834	. . . . . . . . 9 $/\$
61	60	oveq2d 5834	. . . . . . . 8 $/\$
62	57	a1i 9	. . . . . . . . 9 $/\$
63		id 19	. . . . . . . . . 10
64		nnnn0 9080	. . . . . . . . . 10
65		expcl 10419	. . . . . . . . . 10 $/\$
66	63, 64, 65	syl2anr 288	. . . . . . . . 9 $/\$
67	56, 62, 66	adddird 7886	. . . . . . . 8 $/\$
68	66	mulid2d 7879	. . . . . . . . 9 $/\$
69	68	oveq2d 5834	. . . . . . . 8 $/\$
70	61, 67, 69	3eqtrd 2194	. . . . . . 7 $/\$
71	70	mpteq2dva 4054	. . . . . 6
72		cnex 7839	. . . . . . . 8
73	72	a1i 9	. . . . . . 7
74	56, 66	mulcld 7881	. . . . . . 7 $/\$
75		nnm1nn0 9114	. . . . . . . . . . 11
76		expcl 10419	. . . . . . . . . . 11 $/\$
77	63, 75, 76	syl2anr 288	. . . . . . . . . 10 $/\$
78	56, 77	mulcld 7881	. . . . . . . . 9 $/\$
79		simpr 109	. . . . . . . . 9 $/\$
80		eqidd 2158	. . . . . . . . 9
81	39	eqcomi 2161	. . . . . . . . . 10
82	81	a1i 9	. . . . . . . . 9
83	73, 78, 79, 80, 82	offval2 6041	. . . . . . . 8
84	56, 77, 79	mulassd 7884	. . . . . . . . . 10 $/\$
85		expm1t 10429	. . . . . . . . . . . 12 $/\$
86	85	ancoms 266	. . . . . . . . . . 11 $/\$
87	86	oveq2d 5834	. . . . . . . . . 10 $/\$
88	84, 87	eqtr4d 2193	. . . . . . . . 9 $/\$
89	88	mpteq2dva 4054	. . . . . . . 8
90	83, 89	eqtrd 2190	. . . . . . 7
91	52, 50	eqtri 2178	. . . . . . . . . 10
92	91	a1i 9	. . . . . . . . 9
93		eqidd 2158	. . . . . . . . 9
94	73, 62, 66, 92, 93	offval2 6041	. . . . . . . 8
95	68	mpteq2dva 4054	. . . . . . . 8
96	94, 95	eqtrd 2190	. . . . . . 7
97	73, 74, 66, 90, 96	offval2 6041	. . . . . 6
98	71, 97	eqtr4d 2193	. . . . 5
99		oveq1 5825	. . . . . . 7
100	99	oveq1d 5833	. . . . . 6
101	100	eqcomd 2163	. . . . 5
102	98, 101	sylan9eq 2210	. . . 4 $/\$
103		cnelprrecn 7851	. . . . . 6
104	103	a1i 9	. . . . 5 $/\$
105		ssidd 3149	. . . . 5 $/\$
106	66	fmpttd 5619	. . . . . 6
107	106	adantr 274	. . . . 5 $/\$
108		f1oi 5449	. . . . . 6
109		f1of 5411	. . . . . 6
110	108, 109	mp1i 10	. . . . 5 $/\$
111		simpr 109	. . . . . . 7 $/\$
112	111	dmeqd 4785	. . . . . 6 $/\$
113	78	fmpttd 5619	. . . . . . . 8
114	113	adantr 274	. . . . . . 7 $/\$
115	114	fdmd 5323	. . . . . 6 $/\$
116	112, 115	eqtrd 2190	. . . . 5 $/\$
117		1ex 7856	. . . . . . . . 9
118	117	fconst 5362	. . . . . . . 8
119	52	feq1i 5309	. . . . . . . 8
120	118, 119	mpbir 145	. . . . . . 7
121	120	fdmi 5324	. . . . . 6
122	121	a1i 9	. . . . 5 $/\$
123	104, 105, 107, 110, 116, 122	dvimulf 13030	. . . 4 $/\$
124	73, 66, 79, 93, 82	offval2 6041	. . . . . . 7
125		expp1 10408	. . . . . . . . 9 $/\$
126	63, 64, 125	syl2anr 288	. . . . . . . 8 $/\$
127	126	mpteq2dva 4054	. . . . . . 7
128	124, 127	eqtr4d 2193	. . . . . 6
129	128	oveq2d 5834	. . . . 5
130	129	adantr 274	. . . 4 $/\$
131	102, 123, 130	3eqtr2rd 2197	. . 3 $/\$
132	131	ex 114	. 2
133	9, 18, 27, 36, 54, 132	nnind 8832	1

Colors of variables: wff set class

Syntax hints:

wi 4 $/\$ wa 103

wceq 1335

wcel 2128

cvv 2712

csn 3560

cpr 3561

cmpt 4025

cid 4247

cxp 4581

cdm 4583

cres 4585

wf 5163

wf1o 5166 (class class class)co 5818

cof 6024

cc 7713

cr 7714

cc0 7715

c1 7716

caddc 7718

cmul 7720

cmin 8029

cn 8816

cn0 9073

cexp 10400

cdv 12984

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 1427 ax-7 1428 ax-gen 1429 ax-ie1 1473 ax-ie2 1474 ax-8 1484 ax-10 1485 ax-11 1486 ax-i12 1487 ax-bndl 1489 ax-4 1490 ax-17 1506 ax-i9 1510 ax-ial 1514 ax-i5r 1515 ax-13 2130 ax-14 2131 ax-ext 2139 ax-coll 4079 ax-sep 4082 ax-nul 4090 ax-pow 4134 ax-pr 4168 ax-un 4392 ax-setind 4494 ax-iinf 4545 ax-cnex 7806 ax-resscn 7807 ax-1cn 7808 ax-1re 7809 ax-icn 7810 ax-addcl 7811 ax-addrcl 7812 ax-mulcl 7813 ax-mulrcl 7814 ax-addcom 7815 ax-mulcom 7816 ax-addass 7817 ax-mulass 7818 ax-distr 7819 ax-i2m1 7820 ax-0lt1 7821 ax-1rid 7822 ax-0id 7823 ax-rnegex 7824 ax-precex 7825 ax-cnre 7826 ax-pre-ltirr 7827 ax-pre-ltwlin 7828 ax-pre-lttrn 7829 ax-pre-apti 7830 ax-pre-ltadd 7831 ax-pre-mulgt0 7832 ax-pre-mulext 7833 ax-arch 7834 ax-caucvg 7835 ax-addf 7837 ax-mulf 7838

This theorem depends on definitions: df-bi 116 df-stab 817 df-dc 821 df-3or 964 df-3an 965 df-tru 1338 df-fal 1341 df-nf 1441 df-sb 1743 df-eu 2009 df-mo 2010 df-clab 2144 df-cleq 2150 df-clel 2153 df-nfc 2288 df-ne 2328 df-nel 2423 df-ral 2440 df-rex 2441 df-reu 2442 df-rmo 2443 df-rab 2444 df-v 2714 df-sbc 2938 df-csb 3032 df-dif 3104 df-un 3106 df-in 3108 df-ss 3115 df-nul 3395 df-if 3506 df-pw 3545 df-sn 3566 df-pr 3567 df-op 3569 df-uni 3773 df-int 3808 df-iun 3851 df-br 3966 df-opab 4026 df-mpt 4027 df-tr 4063 df-id 4252 df-po 4255 df-iso 4256 df-iord 4325 df-on 4327 df-ilim 4328 df-suc 4330 df-iom 4548 df-xp 4589 df-rel 4590 df-cnv 4591 df-co 4592 df-dm 4593 df-rn 4594 df-res 4595 df-ima 4596 df-iota 5132 df-fun 5169 df-fn 5170 df-f 5171 df-f1 5172 df-fo 5173 df-f1o 5174 df-fv 5175 df-isom 5176 df-riota 5774 df-ov 5821 df-oprab 5822 df-mpo 5823 df-of 6026 df-1st 6082 df-2nd 6083 df-recs 6246 df-frec 6332 df-map 6588 df-pm 6589 df-sup 6920 df-inf 6921 df-pnf 7897 df-mnf 7898 df-xr 7899 df-ltxr 7900 df-le 7901 df-sub 8031 df-neg 8032 df-reap 8433 df-ap 8440 df-div 8529 df-inn 8817 df-2 8875 df-3 8876 df-4 8877 df-n0 9074 df-z 9151 df-uz 9423 df-q 9511 df-rp 9543 df-xneg 9661 df-xadd 9662 df-seqfrec 10327 df-exp 10401 df-cj 10724 df-re 10725 df-im 10726 df-rsqrt 10880 df-abs 10881 df-rest 12313 df-topgen 12332 df-psmet 12347 df-xmet 12348 df-met 12349 df-bl 12350 df-mopn 12351 df-top 12356 df-topon 12369 df-bases 12401 df-ntr 12456 df-cn 12548 df-cnp 12549 df-tx 12613 df-cncf 12918 df-limced 12985 df-dvap 12986

This theorem is referenced by: dvexp2 13036

W3C validator