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 26657

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 12437	. . . . . 6 ⊢ (𝐵 ∈ ℕ₀ ↔ (𝐵 ∈ ℕ ∨ 𝐵 = 0))
2		nncn 12180	. . . . . . . . 9 ⊢ (𝐵 ∈ ℕ → 𝐵 ∈ ℂ)
3		nnne0 12209	. . . . . . . . 9 ⊢ (𝐵 ∈ ℕ → 𝐵 ≠ 0)
4		0cxp 26655	. . . . . . . . 9 ⊢ ((𝐵 ∈ ℂ ∧ 𝐵 ≠ 0) → (0↑_𝑐𝐵) = 0)
5	2, 3, 4	syl2anc 590	. . . . . . . 8 ⊢ (𝐵 ∈ ℕ → (0↑_𝑐𝐵) = 0)
6		0exp 14057	. . . . . . . 8 ⊢ (𝐵 ∈ ℕ → (0↑𝐵) = 0)
7	5, 6	eqtr4d 2778	. . . . . . 7 ⊢ (𝐵 ∈ ℕ → (0↑_𝑐𝐵) = (0↑𝐵))
8		0cn 11134	. . . . . . . . . . 11 ⊢ 0 ∈ ℂ
9		cxpval 26653	. . . . . . . . . . 11 ⊢ ((0 ∈ ℂ ∧ 0 ∈ ℂ) → (0↑_𝑐0) = if(0 = 0, if(0 = 0, 1, 0), (exp‘(0 · (log‘0)))))
10	8, 8, 9	mp2an 698	. . . . . . . . . 10 ⊢ (0↑_𝑐0) = if(0 = 0, if(0 = 0, 1, 0), (exp‘(0 · (log‘0))))
11		eqid 2740	. . . . . . . . . . 11 ⊢ 0 = 0
12	11	iftruei 4468	. . . . . . . . . 10 ⊢ if(0 = 0, if(0 = 0, 1, 0), (exp‘(0 · (log‘0)))) = if(0 = 0, 1, 0)
13	11	iftruei 4468	. . . . . . . . . 10 ⊢ if(0 = 0, 1, 0) = 1
14	10, 12, 13	3eqtri 2767	. . . . . . . . 9 ⊢ (0↑_𝑐0) = 1
15		0exp0e1 14026	. . . . . . . . 9 ⊢ (0↑0) = 1
16	14, 15	eqtr4i 2766	. . . . . . . 8 ⊢ (0↑_𝑐0) = (0↑0)
17		oveq2 7371	. . . . . . . 8 ⊢ (𝐵 = 0 → (0↑_𝑐𝐵) = (0↑_𝑐0))
18		oveq2 7371	. . . . . . . 8 ⊢ (𝐵 = 0 → (0↑𝐵) = (0↑0))
19	16, 17, 18	3eqtr4a 2801	. . . . . . 7 ⊢ (𝐵 = 0 → (0↑_𝑐𝐵) = (0↑𝐵))
20	7, 19	jaoi 863	. . . . . 6 ⊢ ((𝐵 ∈ ℕ ∨ 𝐵 = 0) → (0↑_𝑐𝐵) = (0↑𝐵))
21	1, 20	sylbi 218	. . . . 5 ⊢ (𝐵 ∈ ℕ₀ → (0↑_𝑐𝐵) = (0↑𝐵))
22		oveq1 7370	. . . . . 6 ⊢ (𝐴 = 0 → (𝐴↑_𝑐𝐵) = (0↑_𝑐𝐵))
23		oveq1 7370	. . . . . 6 ⊢ (𝐴 = 0 → (𝐴↑𝐵) = (0↑𝐵))
24	22, 23	eqeq12d 2756	. . . . 5 ⊢ (𝐴 = 0 → ((𝐴↑_𝑐𝐵) = (𝐴↑𝐵) ↔ (0↑_𝑐𝐵) = (0↑𝐵)))
25	21, 24	syl5ibrcom 248	. . . 4 ⊢ (𝐵 ∈ ℕ₀ → (𝐴 = 0 → (𝐴↑_𝑐𝐵) = (𝐴↑𝐵)))
26	25	adantl 482	. . 3 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℕ₀) → (𝐴 = 0 → (𝐴↑_𝑐𝐵) = (𝐴↑𝐵)))
27	26	imp 407	. 2 ⊢ (((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℕ₀) ∧ 𝐴 = 0) → (𝐴↑_𝑐𝐵) = (𝐴↑𝐵))
28		nn0z 12546	. . . 4 ⊢ (𝐵 ∈ ℕ₀ → 𝐵 ∈ ℤ)
29		cxpexpz 26656	. . . . 5 ⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐵 ∈ ℤ) → (𝐴↑_𝑐𝐵) = (𝐴↑𝐵))
30	29	3expa 1124	. . . 4 ⊢ (((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℤ) → (𝐴↑_𝑐𝐵) = (𝐴↑𝐵))
31	28, 30	sylan2 599	. . 3 ⊢ (((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℕ₀) → (𝐴↑_𝑐𝐵) = (𝐴↑𝐵))
32	31	an32s 658	. 2 ⊢ (((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℕ₀) ∧ 𝐴 ≠ 0) → (𝐴↑_𝑐𝐵) = (𝐴↑𝐵))
33	27, 32	pm2.61dane 3022	1 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℕ₀) → (𝐴↑_𝑐𝐵) = (𝐴↑𝐵))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ∧ wa 396 ∨ wo 853 = wceq 1547 ∈ wcel 2119 ≠ wne 2935 ifcif 4461 ‘cfv 6492 (class class class)co 7363 ℂcc 11034 0cc0 11036 1c1 11037 · cmul 11041 ℕcn 12172 ℕ₀cn0 12435 ℤcz 12522 ↑cexp 14021 expce 16024 logclog 26543 ↑_𝑐ccxp 26544

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1802 ax-4 1816 ax-5 1917 ax-6 1974 ax-7 2015 ax-8 2121 ax-9 2129 ax-10 2152 ax-11 2168 ax-12 2189 ax-ext 2712 ax-rep 5206 ax-sep 5225 ax-nul 5235 ax-pow 5301 ax-pr 5369 ax-un 7685 ax-inf2 9560 ax-cnex 11092 ax-resscn 11093 ax-1cn 11094 ax-icn 11095 ax-addcl 11096 ax-addrcl 11097 ax-mulcl 11098 ax-mulrcl 11099 ax-mulcom 11100 ax-addass 11101 ax-mulass 11102 ax-distr 11103 ax-i2m1 11104 ax-1ne0 11105 ax-1rid 11106 ax-rnegex 11107 ax-rrecex 11108 ax-cnre 11109 ax-pre-lttri 11110 ax-pre-lttrn 11111 ax-pre-ltadd 11112 ax-pre-mulgt0 11113 ax-pre-sup 11114 ax-addf 11115

This theorem depends on definitions: df-bi 208 df-an 397 df-or 854 df-3or 1093 df-3an 1094 df-tru 1550 df-fal 1560 df-ex 1787 df-nf 1791 df-sb 2074 df-mo 2543 df-eu 2573 df-clab 2719 df-cleq 2732 df-clel 2815 df-nfc 2889 df-ne 2936 df-nel 3040 df-ral 3055 df-rex 3065 df-rmo 3345 df-reu 3346 df-rab 3393 df-v 3434 df-sbc 3731 df-csb 3839 df-dif 3893 df-un 3895 df-in 3897 df-ss 3907 df-pss 3910 df-nul 4269 df-if 4462 df-pw 4538 df-sn 4563 df-pr 4565 df-tp 4567 df-op 4569 df-uni 4846 df-int 4885 df-iun 4930 df-iin 4931 df-br 5080 df-opab 5142 df-mpt 5161 df-tr 5187 df-id 5520 df-eprel 5525 df-po 5533 df-so 5534 df-fr 5578 df-se 5579 df-we 5580 df-xp 5631 df-rel 5632 df-cnv 5633 df-co 5634 df-dm 5635 df-rn 5636 df-res 5637 df-ima 5638 df-pred 6259 df-ord 6320 df-on 6321 df-lim 6322 df-suc 6323 df-iota 6448 df-fun 6494 df-fn 6495 df-f 6496 df-f1 6497 df-fo 6498 df-f1o 6499 df-fv 6500 df-isom 6501 df-riota 7320 df-ov 7366 df-oprab 7367 df-mpo 7368 df-of 7627 df-om 7814 df-1st 7938 df-2nd 7939 df-supp 8108 df-frecs 8228 df-wrecs 8259 df-recs 8308 df-rdg 8346 df-1o 8402 df-2o 8403 df-er 8640 df-map 8772 df-pm 8773 df-ixp 8843 df-en 8891 df-dom 8892 df-sdom 8893 df-fin 8894 df-fsupp 9272 df-fi 9321 df-sup 9352 df-inf 9353 df-oi 9422 df-card 9861 df-pnf 11179 df-mnf 11180 df-xr 11181 df-ltxr 11182 df-le 11183 df-sub 11377 df-neg 11378 df-div 11806 df-nn 12173 df-2 12242 df-3 12243 df-4 12244 df-5 12245 df-6 12246 df-7 12247 df-8 12248 df-9 12249 df-n0 12436 df-z 12523 df-dec 12643 df-uz 12787 df-q 12897 df-rp 12941 df-xneg 13061 df-xadd 13062 df-xmul 13063 df-ioo 13300 df-ioc 13301 df-ico 13302 df-icc 13303 df-fz 13460 df-fzo 13607 df-fl 13749 df-mod 13827 df-seq 13962 df-exp 14022 df-fac 14234 df-bc 14263 df-hash 14291 df-shft 15027 df-cj 15059 df-re 15060 df-im 15061 df-sqrt 15195 df-abs 15196 df-limsup 15431 df-clim 15448 df-rlim 15449 df-sum 15647 df-ef 16030 df-sin 16032 df-cos 16033 df-pi 16035 df-struct 17115 df-sets 17132 df-slot 17150 df-ndx 17162 df-base 17178 df-ress 17199 df-plusg 17231 df-mulr 17232 df-starv 17233 df-sca 17234 df-vsca 17235 df-ip 17236 df-tset 17237 df-ple 17238 df-ds 17240 df-unif 17241 df-hom 17242 df-cco 17243 df-rest 17383 df-topn 17384 df-0g 17402 df-gsum 17403 df-topgen 17404 df-pt 17405 df-prds 17408 df-xrs 17464 df-qtop 17469 df-imas 17470 df-xps 17472 df-mre 17546 df-mrc 17547 df-acs 17549 df-mgm 18606 df-sgrp 18685 df-mnd 18701 df-submnd 18750 df-mulg 19042 df-cntz 19290 df-cmn 19755 df-psmet 21346 df-xmet 21347 df-met 21348 df-bl 21349 df-mopn 21350 df-fbas 21351 df-fg 21352 df-cnfld 21355 df-top 22884 df-topon 22901 df-topsp 22923 df-bases 22936 df-cld 23009 df-ntr 23010 df-cls 23011 df-nei 23088 df-lp 23126 df-perf 23127 df-cn 23217 df-cnp 23218 df-haus 23305 df-tx 23552 df-hmeo 23745 df-fil 23836 df-fm 23928 df-flim 23929 df-flf 23930 df-xms 24310 df-ms 24311 df-tms 24312 df-cncf 24870 df-limc 25858 df-dv 25859 df-log 26545 df-cxp 26546

This theorem is referenced by: cxp0 26659 cxp1 26660 root1id 26743 dfef2 26959 zetacvg 27003 sgmppw 27185 chpchtsum 27207 logexprlim 27213 dchrabs 27248 bposlem5 27276 bposlem6 27277 ostth2lem3 27623 2sqr3minply 33971 aks4d1p1p2 42556 aks4d1p1p4 42557 binomcxplemnn0 44794 binomcxplemnotnn0 44801 etransclem46 46724

W3C validator