dvcxp2 - Metamath Proof Explorer

	Metamath Proof Explorer		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > dvcxp2		Structured version Visualization version GIF version

Theorem dvcxp2 24703

Description: The derivative of a complex power with respect to the second argument. (Contributed by Mario Carneiro, 24-Feb-2015.)

**Assertion**
Ref	Expression
dvcxp2	⊢ (𝐴 ∈ ℝ⁺ → (ℂ D (𝑥 ∈ ℂ ↦ (𝐴↑_𝑐𝑥))) = (𝑥 ∈ ℂ ↦ ((log‘𝐴) · (𝐴↑_𝑐𝑥))))

Distinct variable group: 𝑥,𝐴

Proof of Theorem dvcxp2 Dummy variable 𝑦 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		cnelprrecn 10242	. . . 4 ⊢ ℂ ∈ {ℝ, ℂ}
2	1	a1i 11	. . 3 ⊢ (𝐴 ∈ ℝ⁺ → ℂ ∈ {ℝ, ℂ})
3		simpr 479	. . . 4 ⊢ ((𝐴 ∈ ℝ⁺ ∧ 𝑥 ∈ ℂ) → 𝑥 ∈ ℂ)
4		relogcl 24543	. . . . . 6 ⊢ (𝐴 ∈ ℝ⁺ → (log‘𝐴) ∈ ℝ)
5	4	adantr 472	. . . . 5 ⊢ ((𝐴 ∈ ℝ⁺ ∧ 𝑥 ∈ ℂ) → (log‘𝐴) ∈ ℝ)
6	5	recnd 10281	. . . 4 ⊢ ((𝐴 ∈ ℝ⁺ ∧ 𝑥 ∈ ℂ) → (log‘𝐴) ∈ ℂ)
7	3, 6	mulcld 10273	. . 3 ⊢ ((𝐴 ∈ ℝ⁺ ∧ 𝑥 ∈ ℂ) → (𝑥 · (log‘𝐴)) ∈ ℂ)
8		efcl 15033	. . . 4 ⊢ (𝑦 ∈ ℂ → (exp‘𝑦) ∈ ℂ)
9	8	adantl 473	. . 3 ⊢ ((𝐴 ∈ ℝ⁺ ∧ 𝑦 ∈ ℂ) → (exp‘𝑦) ∈ ℂ)
10	3, 6	mulcomd 10274	. . . . . 6 ⊢ ((𝐴 ∈ ℝ⁺ ∧ 𝑥 ∈ ℂ) → (𝑥 · (log‘𝐴)) = ((log‘𝐴) · 𝑥))
11	10	mpteq2dva 4897	. . . . 5 ⊢ (𝐴 ∈ ℝ⁺ → (𝑥 ∈ ℂ ↦ (𝑥 · (log‘𝐴))) = (𝑥 ∈ ℂ ↦ ((log‘𝐴) · 𝑥)))
12	11	oveq2d 6831	. . . 4 ⊢ (𝐴 ∈ ℝ⁺ → (ℂ D (𝑥 ∈ ℂ ↦ (𝑥 · (log‘𝐴)))) = (ℂ D (𝑥 ∈ ℂ ↦ ((log‘𝐴) · 𝑥))))
13		1cnd 10269	. . . . 5 ⊢ ((𝐴 ∈ ℝ⁺ ∧ 𝑥 ∈ ℂ) → 1 ∈ ℂ)
14	2	dvmptid 23940	. . . . 5 ⊢ (𝐴 ∈ ℝ⁺ → (ℂ D (𝑥 ∈ ℂ ↦ 𝑥)) = (𝑥 ∈ ℂ ↦ 1))
15	4	recnd 10281	. . . . 5 ⊢ (𝐴 ∈ ℝ⁺ → (log‘𝐴) ∈ ℂ)
16	2, 3, 13, 14, 15	dvmptcmul 23947	. . . 4 ⊢ (𝐴 ∈ ℝ⁺ → (ℂ D (𝑥 ∈ ℂ ↦ ((log‘𝐴) · 𝑥))) = (𝑥 ∈ ℂ ↦ ((log‘𝐴) · 1)))
17	6	mulid1d 10270	. . . . 5 ⊢ ((𝐴 ∈ ℝ⁺ ∧ 𝑥 ∈ ℂ) → ((log‘𝐴) · 1) = (log‘𝐴))
18	17	mpteq2dva 4897	. . . 4 ⊢ (𝐴 ∈ ℝ⁺ → (𝑥 ∈ ℂ ↦ ((log‘𝐴) · 1)) = (𝑥 ∈ ℂ ↦ (log‘𝐴)))
19	12, 16, 18	3eqtrd 2799	. . 3 ⊢ (𝐴 ∈ ℝ⁺ → (ℂ D (𝑥 ∈ ℂ ↦ (𝑥 · (log‘𝐴)))) = (𝑥 ∈ ℂ ↦ (log‘𝐴)))
20		dvef 23963	. . . 4 ⊢ (ℂ D exp) = exp
21		eff 15032	. . . . . . . 8 ⊢ exp:ℂ⟶ℂ
22	21	a1i 11	. . . . . . 7 ⊢ (𝐴 ∈ ℝ⁺ → exp:ℂ⟶ℂ)
23	22	feqmptd 6413	. . . . . 6 ⊢ (𝐴 ∈ ℝ⁺ → exp = (𝑦 ∈ ℂ ↦ (exp‘𝑦)))
24	23	eqcomd 2767	. . . . 5 ⊢ (𝐴 ∈ ℝ⁺ → (𝑦 ∈ ℂ ↦ (exp‘𝑦)) = exp)
25	24	oveq2d 6831	. . . 4 ⊢ (𝐴 ∈ ℝ⁺ → (ℂ D (𝑦 ∈ ℂ ↦ (exp‘𝑦))) = (ℂ D exp))
26	20, 25, 24	3eqtr4a 2821	. . 3 ⊢ (𝐴 ∈ ℝ⁺ → (ℂ D (𝑦 ∈ ℂ ↦ (exp‘𝑦))) = (𝑦 ∈ ℂ ↦ (exp‘𝑦)))
27		fveq2 6354	. . 3 ⊢ (𝑦 = (𝑥 · (log‘𝐴)) → (exp‘𝑦) = (exp‘(𝑥 · (log‘𝐴))))
28	2, 2, 7, 5, 9, 9, 19, 26, 27, 27	dvmptco 23955	. 2 ⊢ (𝐴 ∈ ℝ⁺ → (ℂ D (𝑥 ∈ ℂ ↦ (exp‘(𝑥 · (log‘𝐴))))) = (𝑥 ∈ ℂ ↦ ((exp‘(𝑥 · (log‘𝐴))) · (log‘𝐴))))
29		rpcn 12055	. . . . . 6 ⊢ (𝐴 ∈ ℝ⁺ → 𝐴 ∈ ℂ)
30	29	adantr 472	. . . . 5 ⊢ ((𝐴 ∈ ℝ⁺ ∧ 𝑥 ∈ ℂ) → 𝐴 ∈ ℂ)
31		rpne0 12062	. . . . . 6 ⊢ (𝐴 ∈ ℝ⁺ → 𝐴 ≠ 0)
32	31	adantr 472	. . . . 5 ⊢ ((𝐴 ∈ ℝ⁺ ∧ 𝑥 ∈ ℂ) → 𝐴 ≠ 0)
33	30, 32, 3	cxpefd 24679	. . . 4 ⊢ ((𝐴 ∈ ℝ⁺ ∧ 𝑥 ∈ ℂ) → (𝐴↑_𝑐𝑥) = (exp‘(𝑥 · (log‘𝐴))))
34	33	mpteq2dva 4897	. . 3 ⊢ (𝐴 ∈ ℝ⁺ → (𝑥 ∈ ℂ ↦ (𝐴↑_𝑐𝑥)) = (𝑥 ∈ ℂ ↦ (exp‘(𝑥 · (log‘𝐴)))))
35	34	oveq2d 6831	. 2 ⊢ (𝐴 ∈ ℝ⁺ → (ℂ D (𝑥 ∈ ℂ ↦ (𝐴↑_𝑐𝑥))) = (ℂ D (𝑥 ∈ ℂ ↦ (exp‘(𝑥 · (log‘𝐴))))))
36	30, 3	cxpcld 24675	. . . . 5 ⊢ ((𝐴 ∈ ℝ⁺ ∧ 𝑥 ∈ ℂ) → (𝐴↑_𝑐𝑥) ∈ ℂ)
37	6, 36	mulcomd 10274	. . . 4 ⊢ ((𝐴 ∈ ℝ⁺ ∧ 𝑥 ∈ ℂ) → ((log‘𝐴) · (𝐴↑_𝑐𝑥)) = ((𝐴↑_𝑐𝑥) · (log‘𝐴)))
38	33	oveq1d 6830	. . . 4 ⊢ ((𝐴 ∈ ℝ⁺ ∧ 𝑥 ∈ ℂ) → ((𝐴↑_𝑐𝑥) · (log‘𝐴)) = ((exp‘(𝑥 · (log‘𝐴))) · (log‘𝐴)))
39	37, 38	eqtrd 2795	. . 3 ⊢ ((𝐴 ∈ ℝ⁺ ∧ 𝑥 ∈ ℂ) → ((log‘𝐴) · (𝐴↑_𝑐𝑥)) = ((exp‘(𝑥 · (log‘𝐴))) · (log‘𝐴)))
40	39	mpteq2dva 4897	. 2 ⊢ (𝐴 ∈ ℝ⁺ → (𝑥 ∈ ℂ ↦ ((log‘𝐴) · (𝐴↑_𝑐𝑥))) = (𝑥 ∈ ℂ ↦ ((exp‘(𝑥 · (log‘𝐴))) · (log‘𝐴))))
41	28, 35, 40	3eqtr4d 2805	1 ⊢ (𝐴 ∈ ℝ⁺ → (ℂ D (𝑥 ∈ ℂ ↦ (𝐴↑_𝑐𝑥))) = (𝑥 ∈ ℂ ↦ ((log‘𝐴) · (𝐴↑_𝑐𝑥))))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ∧ wa 383 = wceq 1632 ∈ wcel 2140 ≠ wne 2933 {cpr 4324 ↦ cmpt 4882 ⟶wf 6046 ‘cfv 6050 (class class class)co 6815 ℂcc 10147 ℝcr 10148 0cc0 10149 1c1 10150 · cmul 10154 ℝ⁺crp 12046 expce 15012 D cdv 23847 logclog 24522 ↑_𝑐ccxp 24523

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1871 ax-4 1886 ax-5 1989 ax-6 2055 ax-7 2091 ax-8 2142 ax-9 2149 ax-10 2169 ax-11 2184 ax-12 2197 ax-13 2392 ax-ext 2741 ax-rep 4924 ax-sep 4934 ax-nul 4942 ax-pow 4993 ax-pr 5056 ax-un 7116 ax-inf2 8714 ax-cnex 10205 ax-resscn 10206 ax-1cn 10207 ax-icn 10208 ax-addcl 10209 ax-addrcl 10210 ax-mulcl 10211 ax-mulrcl 10212 ax-mulcom 10213 ax-addass 10214 ax-mulass 10215 ax-distr 10216 ax-i2m1 10217 ax-1ne0 10218 ax-1rid 10219 ax-rnegex 10220 ax-rrecex 10221 ax-cnre 10222 ax-pre-lttri 10223 ax-pre-lttrn 10224 ax-pre-ltadd 10225 ax-pre-mulgt0 10226 ax-pre-sup 10227 ax-addf 10228 ax-mulf 10229

This theorem depends on definitions: df-bi 197 df-or 384 df-an 385 df-3or 1073 df-3an 1074 df-tru 1635 df-fal 1638 df-ex 1854 df-nf 1859 df-sb 2048 df-eu 2612 df-mo 2613 df-clab 2748 df-cleq 2754 df-clel 2757 df-nfc 2892 df-ne 2934 df-nel 3037 df-ral 3056 df-rex 3057 df-reu 3058 df-rmo 3059 df-rab 3060 df-v 3343 df-sbc 3578 df-csb 3676 df-dif 3719 df-un 3721 df-in 3723 df-ss 3730 df-pss 3732 df-nul 4060 df-if 4232 df-pw 4305 df-sn 4323 df-pr 4325 df-tp 4327 df-op 4329 df-uni 4590 df-int 4629 df-iun 4675 df-iin 4676 df-br 4806 df-opab 4866 df-mpt 4883 df-tr 4906 df-id 5175 df-eprel 5180 df-po 5188 df-so 5189 df-fr 5226 df-se 5227 df-we 5228 df-xp 5273 df-rel 5274 df-cnv 5275 df-co 5276 df-dm 5277 df-rn 5278 df-res 5279 df-ima 5280 df-pred 5842 df-ord 5888 df-on 5889 df-lim 5890 df-suc 5891 df-iota 6013 df-fun 6052 df-fn 6053 df-f 6054 df-f1 6055 df-fo 6056 df-f1o 6057 df-fv 6058 df-isom 6059 df-riota 6776 df-ov 6818 df-oprab 6819 df-mpt2 6820 df-of 7064 df-om 7233 df-1st 7335 df-2nd 7336 df-supp 7466 df-wrecs 7578 df-recs 7639 df-rdg 7677 df-1o 7731 df-2o 7732 df-oadd 7735 df-er 7914 df-map 8028 df-pm 8029 df-ixp 8078 df-en 8125 df-dom 8126 df-sdom 8127 df-fin 8128 df-fsupp 8444 df-fi 8485 df-sup 8516 df-inf 8517 df-oi 8583 df-card 8976 df-cda 9203 df-pnf 10289 df-mnf 10290 df-xr 10291 df-ltxr 10292 df-le 10293 df-sub 10481 df-neg 10482 df-div 10898 df-nn 11234 df-2 11292 df-3 11293 df-4 11294 df-5 11295 df-6 11296 df-7 11297 df-8 11298 df-9 11299 df-n0 11506 df-z 11591 df-dec 11707 df-uz 11901 df-q 12003 df-rp 12047 df-xneg 12160 df-xadd 12161 df-xmul 12162 df-ioo 12393 df-ioc 12394 df-ico 12395 df-icc 12396 df-fz 12541 df-fzo 12681 df-fl 12808 df-mod 12884 df-seq 13017 df-exp 13076 df-fac 13276 df-bc 13305 df-hash 13333 df-shft 14027 df-cj 14059 df-re 14060 df-im 14061 df-sqrt 14195 df-abs 14196 df-limsup 14422 df-clim 14439 df-rlim 14440 df-sum 14637 df-ef 15018 df-sin 15020 df-cos 15021 df-pi 15023 df-struct 16082 df-ndx 16083 df-slot 16084 df-base 16086 df-sets 16087 df-ress 16088 df-plusg 16177 df-mulr 16178 df-starv 16179 df-sca 16180 df-vsca 16181 df-ip 16182 df-tset 16183 df-ple 16184 df-ds 16187 df-unif 16188 df-hom 16189 df-cco 16190 df-rest 16306 df-topn 16307 df-0g 16325 df-gsum 16326 df-topgen 16327 df-pt 16328 df-prds 16331 df-xrs 16385 df-qtop 16390 df-imas 16391 df-xps 16393 df-mre 16469 df-mrc 16470 df-acs 16472 df-mgm 17464 df-sgrp 17506 df-mnd 17517 df-submnd 17558 df-mulg 17763 df-cntz 17971 df-cmn 18416 df-psmet 19961 df-xmet 19962 df-met 19963 df-bl 19964 df-mopn 19965 df-fbas 19966 df-fg 19967 df-cnfld 19970 df-top 20922 df-topon 20939 df-topsp 20960 df-bases 20973 df-cld 21046 df-ntr 21047 df-cls 21048 df-nei 21125 df-lp 21163 df-perf 21164 df-cn 21254 df-cnp 21255 df-haus 21342 df-tx 21588 df-hmeo 21781 df-fil 21872 df-fm 21964 df-flim 21965 df-flf 21966 df-xms 22347 df-ms 22348 df-tms 22349 df-cncf 22903 df-limc 23850 df-dv 23851 df-log 24524 df-cxp 24525

This theorem is referenced by: etransclem46 41019

W3C validator