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 14165

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 14086	. 2 ⊢ ((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ₀) → (𝐴↑(𝑁 + 1)) = ((𝐴↑𝑁) · 𝐴))
4	1, 2, 3	syl2anc 584	1 ⊢ (𝜑 → (𝐴↑(𝑁 + 1)) = ((𝐴↑𝑁) · 𝐴))

Colors of variables: wff setvar class

Syntax hints: → wi 4 = wceq 1540 ∈ wcel 2108 (class class class)co 7405 ℂcc 11127 1c1 11130 + caddc 11132 · cmul 11134 ℕ₀cn0 12501 ↑cexp 14079

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 2007 ax-8 2110 ax-9 2118 ax-10 2141 ax-11 2157 ax-12 2177 ax-ext 2707 ax-sep 5266 ax-nul 5276 ax-pow 5335 ax-pr 5402 ax-un 7729 ax-cnex 11185 ax-resscn 11186 ax-1cn 11187 ax-icn 11188 ax-addcl 11189 ax-addrcl 11190 ax-mulcl 11191 ax-mulrcl 11192 ax-mulcom 11193 ax-addass 11194 ax-mulass 11195 ax-distr 11196 ax-i2m1 11197 ax-1ne0 11198 ax-1rid 11199 ax-rnegex 11200 ax-rrecex 11201 ax-cnre 11202 ax-pre-lttri 11203 ax-pre-lttrn 11204 ax-pre-ltadd 11205 ax-pre-mulgt0 11206

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 2065 df-mo 2539 df-eu 2568 df-clab 2714 df-cleq 2727 df-clel 2809 df-nfc 2885 df-ne 2933 df-nel 3037 df-ral 3052 df-rex 3061 df-reu 3360 df-rab 3416 df-v 3461 df-sbc 3766 df-csb 3875 df-dif 3929 df-un 3931 df-in 3933 df-ss 3943 df-pss 3946 df-nul 4309 df-if 4501 df-pw 4577 df-sn 4602 df-pr 4604 df-op 4608 df-uni 4884 df-iun 4969 df-br 5120 df-opab 5182 df-mpt 5202 df-tr 5230 df-id 5548 df-eprel 5553 df-po 5561 df-so 5562 df-fr 5606 df-we 5608 df-xp 5660 df-rel 5661 df-cnv 5662 df-co 5663 df-dm 5664 df-rn 5665 df-res 5666 df-ima 5667 df-pred 6290 df-ord 6355 df-on 6356 df-lim 6357 df-suc 6358 df-iota 6484 df-fun 6533 df-fn 6534 df-f 6535 df-f1 6536 df-fo 6537 df-f1o 6538 df-fv 6539 df-riota 7362 df-ov 7408 df-oprab 7409 df-mpo 7410 df-om 7862 df-2nd 7989 df-frecs 8280 df-wrecs 8311 df-recs 8385 df-rdg 8424 df-er 8719 df-en 8960 df-dom 8961 df-sdom 8962 df-pnf 11271 df-mnf 11272 df-xr 11273 df-ltxr 11274 df-le 11275 df-sub 11468 df-neg 11469 df-nn 12241 df-n0 12502 df-z 12589 df-uz 12853 df-seq 14020 df-exp 14080

This theorem is referenced by: expmordi 14185 facubnd 14318 hashmap 14453 binomlem 15845 incexclem 15852 geoserg 15882 cvgrat 15899 efcllem 16093 oexpneg 16364 pwp1fsum 16410 bitsp1 16450 bitsmod 16455 bitsinv1lem 16460 sadcaddlem 16476 sadadd2lem 16478 rplpwr 16577 eulerthlem2 16801 prmdiv 16804 vfermltlALT 16822 pcprendvds2 16861 pcpremul 16863 prmpwdvds 16924 2expltfac 17112 plyco 26198 dgrcolem1 26231 ftalem5 27039 bposlem5 27251 pntlemq 27564 pntlemr 27565 pntlemj 27566 ostth2lem2 27597 ostth2lem3 27598 rusgrnumwwlks 29956 ex-ind-dvds 30442 nexple 32823 2exple2exp 32824 oexpled 32826 fldext2rspun 33723 fldext2chn 33762 faclimlem3 35762 faclim2 35765 nn0prpwlem 36340 3lexlogpow5ineq5 42073 nicomachus 42361 abvexp 42555 3cubeslem2 42708 3cubeslem3l 42709 3cubeslem3r 42710 mzpexpmpt 42768 pell14qrexpclnn0 42889 jm2.17a 42984 jm2.17b 42985 jm2.17c 42986 jm2.18 43012 cnsrexpcl 43189 inductionexd 44179 binomcxplemnotnn0 44380 stoweidlem3 46032 stoweidlem19 46048 stirlinglem4 46106 stirlinglem7 46109 etransclem23 46286 sqrtpwpw2p 47552 fmtnorec2lem 47556 fmtnorec4 47563 fmtnoprmfac1lem 47578 fmtnoprmfac2 47581 fmtnofac1 47584 lighneallem3 47621 oexpnegALTV 47691 fppr2odd 47745 tgoldbachlt 47830 dignn0flhalflem2 48596 dignn0ehalf 48597 nn0sumshdiglemA 48599 nn0sumshdiglemB 48600 itcovalt2lem2lem2 48654

W3C validator