![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > expp1d | Structured version Visualization version GIF version |
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.) |
Ref | Expression |
---|---|
expcld.1 | ⊢ (𝜑 → 𝐴 ∈ ℂ) |
expcld.2 | ⊢ (𝜑 → 𝑁 ∈ ℕ0) |
Ref | Expression |
---|---|
expp1d | ⊢ (𝜑 → (𝐴↑(𝑁 + 1)) = ((𝐴↑𝑁) · 𝐴)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | expcld.1 | . 2 ⊢ (𝜑 → 𝐴 ∈ ℂ) | |
2 | expcld.2 | . 2 ⊢ (𝜑 → 𝑁 ∈ ℕ0) | |
3 | expp1 13929 | . 2 ⊢ ((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ0) → (𝐴↑(𝑁 + 1)) = ((𝐴↑𝑁) · 𝐴)) | |
4 | 1, 2, 3 | syl2anc 585 | 1 ⊢ (𝜑 → (𝐴↑(𝑁 + 1)) = ((𝐴↑𝑁) · 𝐴)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 = wceq 1542 ∈ wcel 2107 (class class class)co 7352 ℂcc 11008 1c1 11011 + caddc 11013 · cmul 11015 ℕ0cn0 12372 ↑cexp 13922 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1798 ax-4 1812 ax-5 1914 ax-6 1972 ax-7 2012 ax-8 2109 ax-9 2117 ax-10 2138 ax-11 2155 ax-12 2172 ax-ext 2709 ax-sep 5255 ax-nul 5262 ax-pow 5319 ax-pr 5383 ax-un 7665 ax-cnex 11066 ax-resscn 11067 ax-1cn 11068 ax-icn 11069 ax-addcl 11070 ax-addrcl 11071 ax-mulcl 11072 ax-mulrcl 11073 ax-mulcom 11074 ax-addass 11075 ax-mulass 11076 ax-distr 11077 ax-i2m1 11078 ax-1ne0 11079 ax-1rid 11080 ax-rnegex 11081 ax-rrecex 11082 ax-cnre 11083 ax-pre-lttri 11084 ax-pre-lttrn 11085 ax-pre-ltadd 11086 ax-pre-mulgt0 11087 |
This theorem depends on definitions: df-bi 206 df-an 398 df-or 847 df-3or 1089 df-3an 1090 df-tru 1545 df-fal 1555 df-ex 1783 df-nf 1787 df-sb 2069 df-mo 2540 df-eu 2569 df-clab 2716 df-cleq 2730 df-clel 2816 df-nfc 2888 df-ne 2943 df-nel 3049 df-ral 3064 df-rex 3073 df-reu 3353 df-rab 3407 df-v 3446 df-sbc 3739 df-csb 3855 df-dif 3912 df-un 3914 df-in 3916 df-ss 3926 df-pss 3928 df-nul 4282 df-if 4486 df-pw 4561 df-sn 4586 df-pr 4588 df-op 4592 df-uni 4865 df-iun 4955 df-br 5105 df-opab 5167 df-mpt 5188 df-tr 5222 df-id 5530 df-eprel 5536 df-po 5544 df-so 5545 df-fr 5587 df-we 5589 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 6252 df-ord 6319 df-on 6320 df-lim 6321 df-suc 6322 df-iota 6446 df-fun 6496 df-fn 6497 df-f 6498 df-f1 6499 df-fo 6500 df-f1o 6501 df-fv 6502 df-riota 7308 df-ov 7355 df-oprab 7356 df-mpo 7357 df-om 7796 df-2nd 7915 df-frecs 8205 df-wrecs 8236 df-recs 8310 df-rdg 8349 df-er 8607 df-en 8843 df-dom 8844 df-sdom 8845 df-pnf 11150 df-mnf 11151 df-xr 11152 df-ltxr 11153 df-le 11154 df-sub 11346 df-neg 11347 df-nn 12113 df-n0 12373 df-z 12459 df-uz 12723 df-seq 13862 df-exp 13923 |
This theorem is referenced by: expmordi 14025 facubnd 14154 hashmap 14289 binomlem 15674 incexclem 15681 geoserg 15711 cvgrat 15728 efcllem 15920 oexpneg 16187 pwp1fsum 16233 bitsp1 16271 bitsmod 16276 bitsinv1lem 16281 sadcaddlem 16297 sadadd2lem 16299 rplpwr 16398 eulerthlem2 16614 prmdiv 16617 vfermltlALT 16634 pcprendvds2 16673 pcpremul 16675 prmpwdvds 16736 2expltfac 16925 plyco 25554 dgrcolem1 25586 ftalem5 26378 bposlem5 26588 pntlemq 26901 pntlemr 26902 pntlemj 26903 ostth2lem2 26934 ostth2lem3 26935 rusgrnumwwlks 28748 ex-ind-dvds 29234 nexple 32412 faclimlem3 34128 faclim2 34131 nn0prpwlem 34726 3lexlogpow5ineq5 40449 3cubeslem2 40911 3cubeslem3l 40912 3cubeslem3r 40913 mzpexpmpt 40971 pell14qrexpclnn0 41092 jm2.17a 41187 jm2.17b 41188 jm2.17c 41189 jm2.18 41215 cnsrexpcl 41395 inductionexd 42332 binomcxplemnotnn0 42541 stoweidlem3 44139 stoweidlem19 44155 stirlinglem4 44213 stirlinglem7 44216 etransclem23 44393 sqrtpwpw2p 45625 fmtnorec2lem 45629 fmtnorec4 45636 fmtnoprmfac1lem 45651 fmtnoprmfac2 45654 fmtnofac1 45657 lighneallem3 45694 oexpnegALTV 45764 fppr2odd 45818 tgoldbachlt 45903 dignn0flhalflem2 46597 dignn0ehalf 46598 nn0sumshdiglemA 46600 nn0sumshdiglemB 46601 itcovalt2lem2lem2 46655 |
Copyright terms: Public domain | W3C validator |