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 26648

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 12428	. . . . . 6 ⊢ (𝐵 ∈ ℕ₀ ↔ (𝐵 ∈ ℕ ∨ 𝐵 = 0))
2		nncn 12171	. . . . . . . . 9 ⊢ (𝐵 ∈ ℕ → 𝐵 ∈ ℂ)
3		nnne0 12200	. . . . . . . . 9 ⊢ (𝐵 ∈ ℕ → 𝐵 ≠ 0)
4		0cxp 26646	. . . . . . . . 9 ⊢ ((𝐵 ∈ ℂ ∧ 𝐵 ≠ 0) → (0↑_𝑐𝐵) = 0)
5	2, 3, 4	syl2anc 585	. . . . . . . 8 ⊢ (𝐵 ∈ ℕ → (0↑_𝑐𝐵) = 0)
6		0exp 14048	. . . . . . . 8 ⊢ (𝐵 ∈ ℕ → (0↑𝐵) = 0)
7	5, 6	eqtr4d 2775	. . . . . . 7 ⊢ (𝐵 ∈ ℕ → (0↑_𝑐𝐵) = (0↑𝐵))
8		0cn 11125	. . . . . . . . . . 11 ⊢ 0 ∈ ℂ
9		cxpval 26644	. . . . . . . . . . 11 ⊢ ((0 ∈ ℂ ∧ 0 ∈ ℂ) → (0↑_𝑐0) = if(0 = 0, if(0 = 0, 1, 0), (exp‘(0 · (log‘0)))))
10	8, 8, 9	mp2an 693	. . . . . . . . . 10 ⊢ (0↑_𝑐0) = if(0 = 0, if(0 = 0, 1, 0), (exp‘(0 · (log‘0))))
11		eqid 2737	. . . . . . . . . . 11 ⊢ 0 = 0
12	11	iftruei 4474	. . . . . . . . . 10 ⊢ if(0 = 0, if(0 = 0, 1, 0), (exp‘(0 · (log‘0)))) = if(0 = 0, 1, 0)
13	11	iftruei 4474	. . . . . . . . . 10 ⊢ if(0 = 0, 1, 0) = 1
14	10, 12, 13	3eqtri 2764	. . . . . . . . 9 ⊢ (0↑_𝑐0) = 1
15		0exp0e1 14017	. . . . . . . . 9 ⊢ (0↑0) = 1
16	14, 15	eqtr4i 2763	. . . . . . . 8 ⊢ (0↑_𝑐0) = (0↑0)
17		oveq2 7366	. . . . . . . 8 ⊢ (𝐵 = 0 → (0↑_𝑐𝐵) = (0↑_𝑐0))
18		oveq2 7366	. . . . . . . 8 ⊢ (𝐵 = 0 → (0↑𝐵) = (0↑0))
19	16, 17, 18	3eqtr4a 2798	. . . . . . 7 ⊢ (𝐵 = 0 → (0↑_𝑐𝐵) = (0↑𝐵))
20	7, 19	jaoi 858	. . . . . 6 ⊢ ((𝐵 ∈ ℕ ∨ 𝐵 = 0) → (0↑_𝑐𝐵) = (0↑𝐵))
21	1, 20	sylbi 217	. . . . 5 ⊢ (𝐵 ∈ ℕ₀ → (0↑_𝑐𝐵) = (0↑𝐵))
22		oveq1 7365	. . . . . 6 ⊢ (𝐴 = 0 → (𝐴↑_𝑐𝐵) = (0↑_𝑐𝐵))
23		oveq1 7365	. . . . . 6 ⊢ (𝐴 = 0 → (𝐴↑𝐵) = (0↑𝐵))
24	22, 23	eqeq12d 2753	. . . . 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 12537	. . . 4 ⊢ (𝐵 ∈ ℕ₀ → 𝐵 ∈ ℤ)
29		cxpexpz 26647	. . . . 5 ⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐵 ∈ ℤ) → (𝐴↑_𝑐𝐵) = (𝐴↑𝐵))
30	29	3expa 1119	. . . 4 ⊢ (((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℤ) → (𝐴↑_𝑐𝐵) = (𝐴↑𝐵))
31	28, 30	sylan2 594	. . 3 ⊢ (((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℕ₀) → (𝐴↑_𝑐𝐵) = (𝐴↑𝐵))
32	31	an32s 653	. 2 ⊢ (((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℕ₀) ∧ 𝐴 ≠ 0) → (𝐴↑_𝑐𝐵) = (𝐴↑𝐵))
33	27, 32	pm2.61dane 3020	1 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℕ₀) → (𝐴↑_𝑐𝐵) = (𝐴↑𝐵))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ∧ wa 395 ∨ wo 848 = wceq 1542 ∈ wcel 2114 ≠ wne 2933 ifcif 4467 ‘cfv 6490 (class class class)co 7358 ℂcc 11025 0cc0 11027 1c1 11028 · cmul 11032 ℕcn 12163 ℕ₀cn0 12426 ℤcz 12513 ↑cexp 14012 expce 16015 logclog 26534 ↑_𝑐ccxp 26535

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1797 ax-4 1811 ax-5 1912 ax-6 1969 ax-7 2010 ax-8 2116 ax-9 2124 ax-10 2147 ax-11 2163 ax-12 2185 ax-ext 2709 ax-rep 5212 ax-sep 5231 ax-nul 5241 ax-pow 5300 ax-pr 5368 ax-un 7680 ax-inf2 9551 ax-cnex 11083 ax-resscn 11084 ax-1cn 11085 ax-icn 11086 ax-addcl 11087 ax-addrcl 11088 ax-mulcl 11089 ax-mulrcl 11090 ax-mulcom 11091 ax-addass 11092 ax-mulass 11093 ax-distr 11094 ax-i2m1 11095 ax-1ne0 11096 ax-1rid 11097 ax-rnegex 11098 ax-rrecex 11099 ax-cnre 11100 ax-pre-lttri 11101 ax-pre-lttrn 11102 ax-pre-ltadd 11103 ax-pre-mulgt0 11104 ax-pre-sup 11105 ax-addf 11106

This theorem depends on definitions: df-bi 207 df-an 396 df-or 849 df-3or 1088 df-3an 1089 df-tru 1545 df-fal 1555 df-ex 1782 df-nf 1786 df-sb 2069 df-mo 2540 df-eu 2570 df-clab 2716 df-cleq 2729 df-clel 2812 df-nfc 2886 df-ne 2934 df-nel 3038 df-ral 3053 df-rex 3063 df-rmo 3343 df-reu 3344 df-rab 3391 df-v 3432 df-sbc 3730 df-csb 3839 df-dif 3893 df-un 3895 df-in 3897 df-ss 3907 df-pss 3910 df-nul 4275 df-if 4468 df-pw 4544 df-sn 4569 df-pr 4571 df-tp 4573 df-op 4575 df-uni 4852 df-int 4891 df-iun 4936 df-iin 4937 df-br 5087 df-opab 5149 df-mpt 5168 df-tr 5194 df-id 5517 df-eprel 5522 df-po 5530 df-so 5531 df-fr 5575 df-se 5576 df-we 5577 df-xp 5628 df-rel 5629 df-cnv 5630 df-co 5631 df-dm 5632 df-rn 5633 df-res 5634 df-ima 5635 df-pred 6257 df-ord 6318 df-on 6319 df-lim 6320 df-suc 6321 df-iota 6446 df-fun 6492 df-fn 6493 df-f 6494 df-f1 6495 df-fo 6496 df-f1o 6497 df-fv 6498 df-isom 6499 df-riota 7315 df-ov 7361 df-oprab 7362 df-mpo 7363 df-of 7622 df-om 7809 df-1st 7933 df-2nd 7934 df-supp 8102 df-frecs 8222 df-wrecs 8253 df-recs 8302 df-rdg 8340 df-1o 8396 df-2o 8397 df-er 8634 df-map 8766 df-pm 8767 df-ixp 8837 df-en 8885 df-dom 8886 df-sdom 8887 df-fin 8888 df-fsupp 9266 df-fi 9315 df-sup 9346 df-inf 9347 df-oi 9416 df-card 9852 df-pnf 11170 df-mnf 11171 df-xr 11172 df-ltxr 11173 df-le 11174 df-sub 11368 df-neg 11369 df-div 11797 df-nn 12164 df-2 12233 df-3 12234 df-4 12235 df-5 12236 df-6 12237 df-7 12238 df-8 12239 df-9 12240 df-n0 12427 df-z 12514 df-dec 12634 df-uz 12778 df-q 12888 df-rp 12932 df-xneg 13052 df-xadd 13053 df-xmul 13054 df-ioo 13291 df-ioc 13292 df-ico 13293 df-icc 13294 df-fz 13451 df-fzo 13598 df-fl 13740 df-mod 13818 df-seq 13953 df-exp 14013 df-fac 14225 df-bc 14254 df-hash 14282 df-shft 15018 df-cj 15050 df-re 15051 df-im 15052 df-sqrt 15186 df-abs 15187 df-limsup 15422 df-clim 15439 df-rlim 15440 df-sum 15638 df-ef 16021 df-sin 16023 df-cos 16024 df-pi 16026 df-struct 17106 df-sets 17123 df-slot 17141 df-ndx 17153 df-base 17169 df-ress 17190 df-plusg 17222 df-mulr 17223 df-starv 17224 df-sca 17225 df-vsca 17226 df-ip 17227 df-tset 17228 df-ple 17229 df-ds 17231 df-unif 17232 df-hom 17233 df-cco 17234 df-rest 17374 df-topn 17375 df-0g 17393 df-gsum 17394 df-topgen 17395 df-pt 17396 df-prds 17399 df-xrs 17455 df-qtop 17460 df-imas 17461 df-xps 17463 df-mre 17537 df-mrc 17538 df-acs 17540 df-mgm 18597 df-sgrp 18676 df-mnd 18692 df-submnd 18741 df-mulg 19033 df-cntz 19281 df-cmn 19746 df-psmet 21334 df-xmet 21335 df-met 21336 df-bl 21337 df-mopn 21338 df-fbas 21339 df-fg 21340 df-cnfld 21343 df-top 22868 df-topon 22885 df-topsp 22907 df-bases 22920 df-cld 22993 df-ntr 22994 df-cls 22995 df-nei 23072 df-lp 23110 df-perf 23111 df-cn 23201 df-cnp 23202 df-haus 23289 df-tx 23536 df-hmeo 23729 df-fil 23820 df-fm 23912 df-flim 23913 df-flf 23914 df-xms 24294 df-ms 24295 df-tms 24296 df-cncf 24854 df-limc 25842 df-dv 25843 df-log 26536 df-cxp 26537

This theorem is referenced by: cxp0 26650 cxp1 26651 root1id 26735 dfef2 26952 zetacvg 26996 sgmppw 27179 chpchtsum 27201 logexprlim 27207 dchrabs 27242 bposlem5 27270 bposlem6 27271 ostth2lem3 27617 2sqr3minply 33945 aks4d1p1p2 42520 aks4d1p1p4 42521 binomcxplemnn0 44791 binomcxplemnotnn0 44798 etransclem46 46723

W3C validator