expp1d - Metamath Proof Explorer

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

Theorem expp1d 14070

Description: Value of a complex number raised to a nonnegative integer power plus one. Part of Definition 10-4.1 of [Gleason] p. 134. (Contributed by Mario Carneiro, 28-May-2016.)

**Hypotheses**
Ref	Expression
expcld.1	⊢ (𝜑 → 𝐴 ∈ ℂ)
expcld.2	⊢ (𝜑 → 𝑁 ∈ ℕ₀)

**Assertion**
Ref	Expression
expp1d	⊢ (𝜑 → (𝐴↑(𝑁 + 1)) = ((𝐴↑𝑁) · 𝐴))

**Proof of Theorem expp1d**
Step	Hyp	Ref	Expression
1		expcld.1	. 2 ⊢ (𝜑 → 𝐴 ∈ ℂ)
2		expcld.2	. 2 ⊢ (𝜑 → 𝑁 ∈ ℕ₀)
3		expp1 13991	. 2 ⊢ ((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ₀) → (𝐴↑(𝑁 + 1)) = ((𝐴↑𝑁) · 𝐴))
4	1, 2, 3	syl2anc 584	1 ⊢ (𝜑 → (𝐴↑(𝑁 + 1)) = ((𝐴↑𝑁) · 𝐴))

Colors of variables: wff setvar class

Syntax hints: → wi 4 = wceq 1541 ∈ wcel 2113 (class class class)co 7358 ℂcc 11024 1c1 11027 + caddc 11029 · cmul 11031 ℕ₀cn0 12401 ↑cexp 13984

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1796 ax-4 1810 ax-5 1911 ax-6 1968 ax-7 2009 ax-8 2115 ax-9 2123 ax-10 2146 ax-11 2162 ax-12 2184 ax-ext 2708 ax-sep 5241 ax-nul 5251 ax-pow 5310 ax-pr 5377 ax-un 7680 ax-cnex 11082 ax-resscn 11083 ax-1cn 11084 ax-icn 11085 ax-addcl 11086 ax-addrcl 11087 ax-mulcl 11088 ax-mulrcl 11089 ax-mulcom 11090 ax-addass 11091 ax-mulass 11092 ax-distr 11093 ax-i2m1 11094 ax-1ne0 11095 ax-1rid 11096 ax-rnegex 11097 ax-rrecex 11098 ax-cnre 11099 ax-pre-lttri 11100 ax-pre-lttrn 11101 ax-pre-ltadd 11102 ax-pre-mulgt0 11103

This theorem depends on definitions: df-bi 207 df-an 396 df-or 848 df-3or 1087 df-3an 1088 df-tru 1544 df-fal 1554 df-ex 1781 df-nf 1785 df-sb 2068 df-mo 2539 df-eu 2569 df-clab 2715 df-cleq 2728 df-clel 2811 df-nfc 2885 df-ne 2933 df-nel 3037 df-ral 3052 df-rex 3061 df-reu 3351 df-rab 3400 df-v 3442 df-sbc 3741 df-csb 3850 df-dif 3904 df-un 3906 df-in 3908 df-ss 3918 df-pss 3921 df-nul 4286 df-if 4480 df-pw 4556 df-sn 4581 df-pr 4583 df-op 4587 df-uni 4864 df-iun 4948 df-br 5099 df-opab 5161 df-mpt 5180 df-tr 5206 df-id 5519 df-eprel 5524 df-po 5532 df-so 5533 df-fr 5577 df-we 5579 df-xp 5630 df-rel 5631 df-cnv 5632 df-co 5633 df-dm 5634 df-rn 5635 df-res 5636 df-ima 5637 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-riota 7315 df-ov 7361 df-oprab 7362 df-mpo 7363 df-om 7809 df-2nd 7934 df-frecs 8223 df-wrecs 8254 df-recs 8303 df-rdg 8341 df-er 8635 df-en 8884 df-dom 8885 df-sdom 8886 df-pnf 11168 df-mnf 11169 df-xr 11170 df-ltxr 11171 df-le 11172 df-sub 11366 df-neg 11367 df-nn 12146 df-n0 12402 df-z 12489 df-uz 12752 df-seq 13925 df-exp 13985

This theorem is referenced by: expmordi 14090 facubnd 14223 hashmap 14358 binomlem 15752 incexclem 15759 geoserg 15789 cvgrat 15806 efcllem 16000 oexpneg 16272 pwp1fsum 16318 bitsp1 16358 bitsmod 16363 bitsinv1lem 16368 sadcaddlem 16384 sadadd2lem 16386 rplpwr 16485 eulerthlem2 16709 prmdiv 16712 vfermltlALT 16730 pcprendvds2 16769 pcpremul 16771 prmpwdvds 16832 2expltfac 17020 plyco 26202 dgrcolem1 26235 ftalem5 27043 bposlem5 27255 pntlemq 27568 pntlemr 27569 pntlemj 27570 ostth2lem2 27601 ostth2lem3 27602 rusgrnumwwlks 30050 ex-ind-dvds 30536 nexple 32925 2exple2exp 32926 oexpled 32928 fldext2rspun 33839 fldext2chn 33885 faclimlem3 35939 faclim2 35942 nn0prpwlem 36516 3lexlogpow5ineq5 42310 nicomachus 42563 abvexp 42783 3cubeslem2 42923 3cubeslem3l 42924 3cubeslem3r 42925 mzpexpmpt 42983 pell14qrexpclnn0 43104 jm2.17a 43198 jm2.17b 43199 jm2.17c 43200 jm2.18 43226 cnsrexpcl 43403 inductionexd 44392 binomcxplemnotnn0 44593 stoweidlem3 46243 stoweidlem19 46259 stirlinglem4 46317 stirlinglem7 46320 etransclem23 46497 sqrtpwpw2p 47780 fmtnorec2lem 47784 fmtnorec4 47791 fmtnoprmfac1lem 47806 fmtnoprmfac2 47809 fmtnofac1 47812 lighneallem3 47849 oexpnegALTV 47919 fppr2odd 47973 tgoldbachlt 48058 dignn0flhalflem2 48858 dignn0ehalf 48859 nn0sumshdiglemA 48861 nn0sumshdiglemB 48862 itcovalt2lem2lem2 48916

W3C validator