![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > exp1 | Structured version Visualization version GIF version |
Description: Value of a complex number raised to the first power. (Contributed by NM, 20-Oct-2004.) (Revised by Mario Carneiro, 2-Jul-2013.) |
Ref | Expression |
---|---|
exp1 | ⊢ (𝐴 ∈ ℂ → (𝐴↑1) = 𝐴) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | 1nn 11444 | . . . 4 ⊢ 1 ∈ ℕ | |
2 | expnnval 13240 | . . . 4 ⊢ ((𝐴 ∈ ℂ ∧ 1 ∈ ℕ) → (𝐴↑1) = (seq1( · , (ℕ × {𝐴}))‘1)) | |
3 | 1, 2 | mpan2 678 | . . 3 ⊢ (𝐴 ∈ ℂ → (𝐴↑1) = (seq1( · , (ℕ × {𝐴}))‘1)) |
4 | 1z 11818 | . . . 4 ⊢ 1 ∈ ℤ | |
5 | seq1 13190 | . . . 4 ⊢ (1 ∈ ℤ → (seq1( · , (ℕ × {𝐴}))‘1) = ((ℕ × {𝐴})‘1)) | |
6 | 4, 5 | ax-mp 5 | . . 3 ⊢ (seq1( · , (ℕ × {𝐴}))‘1) = ((ℕ × {𝐴})‘1) |
7 | 3, 6 | syl6eq 2824 | . 2 ⊢ (𝐴 ∈ ℂ → (𝐴↑1) = ((ℕ × {𝐴})‘1)) |
8 | fvconst2g 6785 | . . 3 ⊢ ((𝐴 ∈ ℂ ∧ 1 ∈ ℕ) → ((ℕ × {𝐴})‘1) = 𝐴) | |
9 | 1, 8 | mpan2 678 | . 2 ⊢ (𝐴 ∈ ℂ → ((ℕ × {𝐴})‘1) = 𝐴) |
10 | 7, 9 | eqtrd 2808 | 1 ⊢ (𝐴 ∈ ℂ → (𝐴↑1) = 𝐴) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 = wceq 1507 ∈ wcel 2048 {csn 4435 × cxp 5398 ‘cfv 6182 (class class class)co 6970 ℂcc 10325 1c1 10328 · cmul 10332 ℕcn 11431 ℤcz 11786 seqcseq 13177 ↑cexp 13237 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1758 ax-4 1772 ax-5 1869 ax-6 1928 ax-7 1964 ax-8 2050 ax-9 2057 ax-10 2077 ax-11 2091 ax-12 2104 ax-13 2299 ax-ext 2745 ax-sep 5054 ax-nul 5061 ax-pow 5113 ax-pr 5180 ax-un 7273 ax-cnex 10383 ax-resscn 10384 ax-1cn 10385 ax-icn 10386 ax-addcl 10387 ax-addrcl 10388 ax-mulcl 10389 ax-mulrcl 10390 ax-mulcom 10391 ax-addass 10392 ax-mulass 10393 ax-distr 10394 ax-i2m1 10395 ax-1ne0 10396 ax-1rid 10397 ax-rnegex 10398 ax-rrecex 10399 ax-cnre 10400 ax-pre-lttri 10401 ax-pre-lttrn 10402 ax-pre-ltadd 10403 ax-pre-mulgt0 10404 |
This theorem depends on definitions: df-bi 199 df-an 388 df-or 834 df-3or 1069 df-3an 1070 df-tru 1510 df-ex 1743 df-nf 1747 df-sb 2014 df-mo 2544 df-eu 2580 df-clab 2754 df-cleq 2765 df-clel 2840 df-nfc 2912 df-ne 2962 df-nel 3068 df-ral 3087 df-rex 3088 df-reu 3089 df-rab 3091 df-v 3411 df-sbc 3678 df-csb 3783 df-dif 3828 df-un 3830 df-in 3832 df-ss 3839 df-pss 3841 df-nul 4174 df-if 4345 df-pw 4418 df-sn 4436 df-pr 4438 df-tp 4440 df-op 4442 df-uni 4707 df-iun 4788 df-br 4924 df-opab 4986 df-mpt 5003 df-tr 5025 df-id 5305 df-eprel 5310 df-po 5319 df-so 5320 df-fr 5359 df-we 5361 df-xp 5406 df-rel 5407 df-cnv 5408 df-co 5409 df-dm 5410 df-rn 5411 df-res 5412 df-ima 5413 df-pred 5980 df-ord 6026 df-on 6027 df-lim 6028 df-suc 6029 df-iota 6146 df-fun 6184 df-fn 6185 df-f 6186 df-f1 6187 df-fo 6188 df-f1o 6189 df-fv 6190 df-riota 6931 df-ov 6973 df-oprab 6974 df-mpo 6975 df-om 7391 df-2nd 7495 df-wrecs 7743 df-recs 7805 df-rdg 7843 df-er 8081 df-en 8299 df-dom 8300 df-sdom 8301 df-pnf 10468 df-mnf 10469 df-xr 10470 df-ltxr 10471 df-le 10472 df-sub 10664 df-neg 10665 df-nn 11432 df-n0 11701 df-z 11787 df-uz 12052 df-seq 13178 df-exp 13238 |
This theorem is referenced by: expp1 13244 expn1 13247 expcllem 13248 expeq0 13267 expp1z 13286 expm1 13287 sqval 13289 exp1d 13313 expmordi 13339 expnbnd 13401 digit1 13406 faclbnd4lem1 13461 climcndslem1 15054 climcndslem2 15055 geoisum1 15085 bpoly1 15255 ef4p 15316 efgt1p2 15317 efgt1p 15318 rpnnen2lem3 15419 modxp1i 16252 numexp1 16259 psgnpmtr 18390 lt6abl 18759 cphipval 23539 iblcnlem1 24081 itgcnlem 24083 dvexp 24243 dveflem 24269 plyid 24492 coeidp 24546 dgrid 24547 cxp1 24945 1cubrlem 25110 1cubr 25111 log2ublem3 25218 basellem5 25354 perfectlem2 25498 logdivsum 25801 log2sumbnd 25812 ipval2 28251 0dp2dp 30320 subfacval2 31979 dvasin 34367 areacirclem1 34371 1t10e1p1e11 42862 fmtnoge3 43000 fmtno0 43010 fmtno1 43011 lighneallem2 43079 lighneallem3 43080 41prothprmlem2 43091 perfectALTVlem2 43195 8exp8mod9 43209 tgblthelfgott 43288 exple2lt6 43718 pw2m1lepw2m1 43883 logbpw2m1 43935 nnpw2pmod 43951 |
Copyright terms: Public domain | W3C validator |