cxpexp - Metamath Proof Explorer

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

Theorem cxpexp 26593

Description: Relate the complex power function to the integer power function. (Contributed by Mario Carneiro, 2-Aug-2014.)

**Assertion**
Ref	Expression
cxpexp	⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℕ₀) → (𝐴↑_𝑐𝐵) = (𝐴↑𝐵))

**Proof of Theorem cxpexp**
Step	Hyp	Ref	Expression
1		elnn0 12404	. . . . . 6 ⊢ (𝐵 ∈ ℕ₀ ↔ (𝐵 ∈ ℕ ∨ 𝐵 = 0))
2		nncn 12154	. . . . . . . . 9 ⊢ (𝐵 ∈ ℕ → 𝐵 ∈ ℂ)
3		nnne0 12180	. . . . . . . . 9 ⊢ (𝐵 ∈ ℕ → 𝐵 ≠ 0)
4		0cxp 26591	. . . . . . . . 9 ⊢ ((𝐵 ∈ ℂ ∧ 𝐵 ≠ 0) → (0↑_𝑐𝐵) = 0)
5	2, 3, 4	syl2anc 584	. . . . . . . 8 ⊢ (𝐵 ∈ ℕ → (0↑_𝑐𝐵) = 0)
6		0exp 14022	. . . . . . . 8 ⊢ (𝐵 ∈ ℕ → (0↑𝐵) = 0)
7	5, 6	eqtr4d 2767	. . . . . . 7 ⊢ (𝐵 ∈ ℕ → (0↑_𝑐𝐵) = (0↑𝐵))
8		0cn 11126	. . . . . . . . . . 11 ⊢ 0 ∈ ℂ
9		cxpval 26589	. . . . . . . . . . 11 ⊢ ((0 ∈ ℂ ∧ 0 ∈ ℂ) → (0↑_𝑐0) = if(0 = 0, if(0 = 0, 1, 0), (exp‘(0 · (log‘0)))))
10	8, 8, 9	mp2an 692	. . . . . . . . . 10 ⊢ (0↑_𝑐0) = if(0 = 0, if(0 = 0, 1, 0), (exp‘(0 · (log‘0))))
11		eqid 2729	. . . . . . . . . . 11 ⊢ 0 = 0
12	11	iftruei 4485	. . . . . . . . . 10 ⊢ if(0 = 0, if(0 = 0, 1, 0), (exp‘(0 · (log‘0)))) = if(0 = 0, 1, 0)
13	11	iftruei 4485	. . . . . . . . . 10 ⊢ if(0 = 0, 1, 0) = 1
14	10, 12, 13	3eqtri 2756	. . . . . . . . 9 ⊢ (0↑_𝑐0) = 1
15		0exp0e1 13991	. . . . . . . . 9 ⊢ (0↑0) = 1
16	14, 15	eqtr4i 2755	. . . . . . . 8 ⊢ (0↑_𝑐0) = (0↑0)
17		oveq2 7361	. . . . . . . 8 ⊢ (𝐵 = 0 → (0↑_𝑐𝐵) = (0↑_𝑐0))
18		oveq2 7361	. . . . . . . 8 ⊢ (𝐵 = 0 → (0↑𝐵) = (0↑0))
19	16, 17, 18	3eqtr4a 2790	. . . . . . 7 ⊢ (𝐵 = 0 → (0↑_𝑐𝐵) = (0↑𝐵))
20	7, 19	jaoi 857	. . . . . 6 ⊢ ((𝐵 ∈ ℕ ∨ 𝐵 = 0) → (0↑_𝑐𝐵) = (0↑𝐵))
21	1, 20	sylbi 217	. . . . 5 ⊢ (𝐵 ∈ ℕ₀ → (0↑_𝑐𝐵) = (0↑𝐵))
22		oveq1 7360	. . . . . 6 ⊢ (𝐴 = 0 → (𝐴↑_𝑐𝐵) = (0↑_𝑐𝐵))
23		oveq1 7360	. . . . . 6 ⊢ (𝐴 = 0 → (𝐴↑𝐵) = (0↑𝐵))
24	22, 23	eqeq12d 2745	. . . . 5 ⊢ (𝐴 = 0 → ((𝐴↑_𝑐𝐵) = (𝐴↑𝐵) ↔ (0↑_𝑐𝐵) = (0↑𝐵)))
25	21, 24	syl5ibrcom 247	. . . 4 ⊢ (𝐵 ∈ ℕ₀ → (𝐴 = 0 → (𝐴↑_𝑐𝐵) = (𝐴↑𝐵)))
26	25	adantl 481	. . 3 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℕ₀) → (𝐴 = 0 → (𝐴↑_𝑐𝐵) = (𝐴↑𝐵)))
27	26	imp 406	. 2 ⊢ (((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℕ₀) ∧ 𝐴 = 0) → (𝐴↑_𝑐𝐵) = (𝐴↑𝐵))
28		nn0z 12514	. . . 4 ⊢ (𝐵 ∈ ℕ₀ → 𝐵 ∈ ℤ)
29		cxpexpz 26592	. . . . 5 ⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐵 ∈ ℤ) → (𝐴↑_𝑐𝐵) = (𝐴↑𝐵))
30	29	3expa 1118	. . . 4 ⊢ (((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℤ) → (𝐴↑_𝑐𝐵) = (𝐴↑𝐵))
31	28, 30	sylan2 593	. . 3 ⊢ (((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℕ₀) → (𝐴↑_𝑐𝐵) = (𝐴↑𝐵))
32	31	an32s 652	. 2 ⊢ (((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℕ₀) ∧ 𝐴 ≠ 0) → (𝐴↑_𝑐𝐵) = (𝐴↑𝐵))
33	27, 32	pm2.61dane 3012	1 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℕ₀) → (𝐴↑_𝑐𝐵) = (𝐴↑𝐵))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ∧ wa 395 ∨ wo 847 = wceq 1540 ∈ wcel 2109 ≠ wne 2925 ifcif 4478 ‘cfv 6486 (class class class)co 7353 ℂcc 11026 0cc0 11028 1c1 11029 · cmul 11033 ℕcn 12146 ℕ₀cn0 12402 ℤcz 12489 ↑cexp 13986 expce 15986 logclog 26479 ↑_𝑐ccxp 26480

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 1910 ax-6 1967 ax-7 2008 ax-8 2111 ax-9 2119 ax-10 2142 ax-11 2158 ax-12 2178 ax-ext 2701 ax-rep 5221 ax-sep 5238 ax-nul 5248 ax-pow 5307 ax-pr 5374 ax-un 7675 ax-inf2 9556 ax-cnex 11084 ax-resscn 11085 ax-1cn 11086 ax-icn 11087 ax-addcl 11088 ax-addrcl 11089 ax-mulcl 11090 ax-mulrcl 11091 ax-mulcom 11092 ax-addass 11093 ax-mulass 11094 ax-distr 11095 ax-i2m1 11096 ax-1ne0 11097 ax-1rid 11098 ax-rnegex 11099 ax-rrecex 11100 ax-cnre 11101 ax-pre-lttri 11102 ax-pre-lttrn 11103 ax-pre-ltadd 11104 ax-pre-mulgt0 11105 ax-pre-sup 11106 ax-addf 11107

This theorem depends on definitions: df-bi 207 df-an 396 df-or 848 df-3or 1087 df-3an 1088 df-tru 1543 df-fal 1553 df-ex 1780 df-nf 1784 df-sb 2066 df-mo 2533 df-eu 2562 df-clab 2708 df-cleq 2721 df-clel 2803 df-nfc 2878 df-ne 2926 df-nel 3030 df-ral 3045 df-rex 3054 df-rmo 3345 df-reu 3346 df-rab 3397 df-v 3440 df-sbc 3745 df-csb 3854 df-dif 3908 df-un 3910 df-in 3912 df-ss 3922 df-pss 3925 df-nul 4287 df-if 4479 df-pw 4555 df-sn 4580 df-pr 4582 df-tp 4584 df-op 4586 df-uni 4862 df-int 4900 df-iun 4946 df-iin 4947 df-br 5096 df-opab 5158 df-mpt 5177 df-tr 5203 df-id 5518 df-eprel 5523 df-po 5531 df-so 5532 df-fr 5576 df-se 5577 df-we 5578 df-xp 5629 df-rel 5630 df-cnv 5631 df-co 5632 df-dm 5633 df-rn 5634 df-res 5635 df-ima 5636 df-pred 6253 df-ord 6314 df-on 6315 df-lim 6316 df-suc 6317 df-iota 6442 df-fun 6488 df-fn 6489 df-f 6490 df-f1 6491 df-fo 6492 df-f1o 6493 df-fv 6494 df-isom 6495 df-riota 7310 df-ov 7356 df-oprab 7357 df-mpo 7358 df-of 7617 df-om 7807 df-1st 7931 df-2nd 7932 df-supp 8101 df-frecs 8221 df-wrecs 8252 df-recs 8301 df-rdg 8339 df-1o 8395 df-2o 8396 df-er 8632 df-map 8762 df-pm 8763 df-ixp 8832 df-en 8880 df-dom 8881 df-sdom 8882 df-fin 8883 df-fsupp 9271 df-fi 9320 df-sup 9351 df-inf 9352 df-oi 9421 df-card 9854 df-pnf 11170 df-mnf 11171 df-xr 11172 df-ltxr 11173 df-le 11174 df-sub 11367 df-neg 11368 df-div 11796 df-nn 12147 df-2 12209 df-3 12210 df-4 12211 df-5 12212 df-6 12213 df-7 12214 df-8 12215 df-9 12216 df-n0 12403 df-z 12490 df-dec 12610 df-uz 12754 df-q 12868 df-rp 12912 df-xneg 13032 df-xadd 13033 df-xmul 13034 df-ioo 13270 df-ioc 13271 df-ico 13272 df-icc 13273 df-fz 13429 df-fzo 13576 df-fl 13714 df-mod 13792 df-seq 13927 df-exp 13987 df-fac 14199 df-bc 14228 df-hash 14256 df-shft 14992 df-cj 15024 df-re 15025 df-im 15026 df-sqrt 15160 df-abs 15161 df-limsup 15396 df-clim 15413 df-rlim 15414 df-sum 15612 df-ef 15992 df-sin 15994 df-cos 15995 df-pi 15997 df-struct 17076 df-sets 17093 df-slot 17111 df-ndx 17123 df-base 17139 df-ress 17160 df-plusg 17192 df-mulr 17193 df-starv 17194 df-sca 17195 df-vsca 17196 df-ip 17197 df-tset 17198 df-ple 17199 df-ds 17201 df-unif 17202 df-hom 17203 df-cco 17204 df-rest 17344 df-topn 17345 df-0g 17363 df-gsum 17364 df-topgen 17365 df-pt 17366 df-prds 17369 df-xrs 17424 df-qtop 17429 df-imas 17430 df-xps 17432 df-mre 17506 df-mrc 17507 df-acs 17509 df-mgm 18532 df-sgrp 18611 df-mnd 18627 df-submnd 18676 df-mulg 18965 df-cntz 19214 df-cmn 19679 df-psmet 21271 df-xmet 21272 df-met 21273 df-bl 21274 df-mopn 21275 df-fbas 21276 df-fg 21277 df-cnfld 21280 df-top 22797 df-topon 22814 df-topsp 22836 df-bases 22849 df-cld 22922 df-ntr 22923 df-cls 22924 df-nei 23001 df-lp 23039 df-perf 23040 df-cn 23130 df-cnp 23131 df-haus 23218 df-tx 23465 df-hmeo 23658 df-fil 23749 df-fm 23841 df-flim 23842 df-flf 23843 df-xms 24224 df-ms 24225 df-tms 24226 df-cncf 24787 df-limc 25783 df-dv 25784 df-log 26481 df-cxp 26482

This theorem is referenced by: cxp0 26595 cxp1 26596 root1id 26680 dfef2 26897 zetacvg 26941 sgmppw 27124 chpchtsum 27146 logexprlim 27152 dchrabs 27187 bposlem5 27215 bposlem6 27216 ostth2lem3 27562 2sqr3minply 33746 aks4d1p1p2 42043 aks4d1p1p4 42044 binomcxplemnn0 44322 binomcxplemnotnn0 44329 etransclem46 46262

W3C validator