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 14082

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

Colors of variables: wff setvar class

Syntax hints: → wi 4 = wceq 1542 ∈ wcel 2114 (class class class)co 7368 ℂcc 11036 1c1 11039 + caddc 11041 · cmul 11043 ℕ₀cn0 12413 ↑cexp 13996

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-sep 5243 ax-nul 5253 ax-pow 5312 ax-pr 5379 ax-un 7690 ax-cnex 11094 ax-resscn 11095 ax-1cn 11096 ax-icn 11097 ax-addcl 11098 ax-addrcl 11099 ax-mulcl 11100 ax-mulrcl 11101 ax-mulcom 11102 ax-addass 11103 ax-mulass 11104 ax-distr 11105 ax-i2m1 11106 ax-1ne0 11107 ax-1rid 11108 ax-rnegex 11109 ax-rrecex 11110 ax-cnre 11111 ax-pre-lttri 11112 ax-pre-lttrn 11113 ax-pre-ltadd 11114 ax-pre-mulgt0 11115

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-reu 3353 df-rab 3402 df-v 3444 df-sbc 3743 df-csb 3852 df-dif 3906 df-un 3908 df-in 3910 df-ss 3920 df-pss 3923 df-nul 4288 df-if 4482 df-pw 4558 df-sn 4583 df-pr 4585 df-op 4589 df-uni 4866 df-iun 4950 df-br 5101 df-opab 5163 df-mpt 5182 df-tr 5208 df-id 5527 df-eprel 5532 df-po 5540 df-so 5541 df-fr 5585 df-we 5587 df-xp 5638 df-rel 5639 df-cnv 5640 df-co 5641 df-dm 5642 df-rn 5643 df-res 5644 df-ima 5645 df-pred 6267 df-ord 6328 df-on 6329 df-lim 6330 df-suc 6331 df-iota 6456 df-fun 6502 df-fn 6503 df-f 6504 df-f1 6505 df-fo 6506 df-f1o 6507 df-fv 6508 df-riota 7325 df-ov 7371 df-oprab 7372 df-mpo 7373 df-om 7819 df-2nd 7944 df-frecs 8233 df-wrecs 8264 df-recs 8313 df-rdg 8351 df-er 8645 df-en 8896 df-dom 8897 df-sdom 8898 df-pnf 11180 df-mnf 11181 df-xr 11182 df-ltxr 11183 df-le 11184 df-sub 11378 df-neg 11379 df-nn 12158 df-n0 12414 df-z 12501 df-uz 12764 df-seq 13937 df-exp 13997

This theorem is referenced by: expmordi 14102 facubnd 14235 hashmap 14370 binomlem 15764 incexclem 15771 geoserg 15801 cvgrat 15818 efcllem 16012 oexpneg 16284 pwp1fsum 16330 bitsp1 16370 bitsmod 16375 bitsinv1lem 16380 sadcaddlem 16396 sadadd2lem 16398 rplpwr 16497 eulerthlem2 16721 prmdiv 16724 vfermltlALT 16742 pcprendvds2 16781 pcpremul 16783 prmpwdvds 16844 2expltfac 17032 plyco 26214 dgrcolem1 26247 ftalem5 27055 bposlem5 27267 pntlemq 27580 pntlemr 27581 pntlemj 27582 ostth2lem2 27613 ostth2lem3 27614 rusgrnumwwlks 30062 ex-ind-dvds 30548 nexple 32935 2exple2exp 32936 oexpled 32938 fldext2rspun 33859 fldext2chn 33905 faclimlem3 35958 faclim2 35961 nn0prpwlem 36535 3lexlogpow5ineq5 42424 nicomachus 42676 abvexp 42896 3cubeslem2 43036 3cubeslem3l 43037 3cubeslem3r 43038 mzpexpmpt 43096 pell14qrexpclnn0 43217 jm2.17a 43311 jm2.17b 43312 jm2.17c 43313 jm2.18 43339 cnsrexpcl 43516 inductionexd 44505 binomcxplemnotnn0 44706 stoweidlem3 46355 stoweidlem19 46371 stirlinglem4 46429 stirlinglem7 46432 etransclem23 46609 sqrtpwpw2p 47892 fmtnorec2lem 47896 fmtnorec4 47903 fmtnoprmfac1lem 47918 fmtnoprmfac2 47921 fmtnofac1 47924 lighneallem3 47961 oexpnegALTV 48031 fppr2odd 48085 tgoldbachlt 48170 dignn0flhalflem2 48970 dignn0ehalf 48971 nn0sumshdiglemA 48973 nn0sumshdiglemB 48974 itcovalt2lem2lem2 49028

W3C validator