Theorem exp1 14237

Description: Value of a complex number raised to the first power. (Contributed by NM, 20-Oct-2004.) (Revised by Mario Carneiro, 2-Jul-2013.)

Assertion

Ref	Expression
exp1	⊢ (𝐴 ∈ ℂ → (𝐴↑1) = 𝐴)

Proof of Theorem exp1

Step	Hyp	Ref	Expression
1		1nn 12373	. . . 4 ⊢ 1 ∈ ℕ
2		expnnval 14234	. . . 4 ⊢ ((𝐴 ∈ ℂ ∧ 1 ∈ ℕ) → (𝐴↑1) = (seq1( · , (ℕ × {𝐴}))‘1))
3	1, 2	mpan2 704	. . 3 ⊢ (𝐴 ∈ ℂ → (𝐴↑1) = (seq1( · , (ℕ × {𝐴}))‘1))
4		1z 12753	. . . 4 ⊢ 1 ∈ ℤ
5		seq1 14184	. . . 4 ⊢ (1 ∈ ℤ → (seq1( · , (ℕ × {𝐴}))‘1) = ((ℕ × {𝐴})‘1))
6	4, 5	ax-mp 5	. . 3 ⊢ (seq1( · , (ℕ × {𝐴}))‘1) = ((ℕ × {𝐴})‘1)
7	3, 6	eqtrdi 2814	. 2 ⊢ (𝐴 ∈ ℂ → (𝐴↑1) = ((ℕ × {𝐴})‘1))
8		fvconst2g 7231	. . 3 ⊢ ((𝐴 ∈ ℂ ∧ 1 ∈ ℕ) → ((ℕ × {𝐴})‘1) = 𝐴)
9	1, 8	mpan2 704	. 2 ⊢ (𝐴 ∈ ℂ → ((ℕ × {𝐴})‘1) = 𝐴)
10	7, 9	eqtrd 2798	1 ⊢ (𝐴 ∈ ℂ → (𝐴↑1) = 𝐴)

This proof depends on syntax axioms:   → wi 4   = wceq 1570   ∈ wcel 2147  {csn 4588   × cxp 5653  ‘cfv 6558  (class class class)co 7443  ℂcc 11225  1c1 11228   · cmul 11232  ℕcn 12362  ℤcz 12720  seqcseq 14171  ↑cexp 14231

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-10 2180  ax-11 2197  ax-12 2216  ax-ext 2735  ax-sep 5252  ax-nul 5263  ax-pow 5331  ax-pr 5395  ax-un 7775  ax-cnex 11283  ax-resscn 11284  ax-1cn 11285  ax-icn 11286  ax-addcl 11287  ax-addrcl 11288  ax-mulcl 11289  ax-mulrcl 11290  ax-mulcom 11291  ax-addass 11292  ax-mulass 11293  ax-distr 11294  ax-i2m1 11295  ax-1ne0 11296  ax-1rid 11297  ax-rnegex 11298  ax-rrecex 11299  ax-cnre 11300  ax-pre-lttri 11301  ax-pre-lttrn 11302  ax-pre-ltadd 11303  ax-pre-mulgt0 11304

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3or 1104  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2102  df-mo 2567  df-eu 2597  df-clab 2742  df-cleq 2755  df-clel 2839  df-nfc 2913  df-ne 2960  df-nel 3066  df-ral 3081  df-rex 3091  df-reu 3370  df-rab 3417  df-v 3456  df-sbc 3743  df-csb 3852  df-ss 3901  df-pss 4017  df-dif 4050  df-in 4094  df-un 4154  df-nul 4282  df-if 4486  df-pw 4562  df-sn 4589  df-pr 4591  df-op 4839  df-uni 4871  df-iun 4956  df-br 5107  df-opab 5171  df-mpt 5190  df-tr 5216  df-id 5550  df-eprel 5555  df-po 5563  df-so 5564  df-fr 5608  df-we 5610  df-xp 5661  df-rel 5662  df-cnv 5663  df-co 5664  df-dm 5665  df-rn 5666  df-res 5667  df-ima 5668  df-pred 6322  df-ord 6383  df-on 6384  df-lim 6385  df-suc 6386  df-iota 6512  df-fun 6560  df-fn 6561  df-f 6562  df-f1 6563  df-fo 6564  df-f1o 6565  df-fv 6566  df-riota 7400  df-ov 7446  df-oprab 7447  df-mpo 7448  df-om 7902  df-2nd 8026  df-frecs 8327  df-wrecs 8358  df-recs 8407  df-rdg 8446  df-er 8745  df-en 9002  df-dom 9003  df-sdom 9004  df-pnf 11372  df-mnf 11373  df-xr 11374  df-ltxr 11375  df-le 11376  df-sub 11570  df-neg 11571  df-nn 12363  df-n0 12634  df-z 12721  df-uz 12993  df-seq 14172  df-exp 14232

This theorem is used by:  expp1  14238  expn1  14241  expcllem  14242  expeq0  14262  expp1z  14281  expm1  14282  sqval  14284  exp1d  14311  expmordi  14337  expnbnd  14403  digit1  14408  faclbnd4lem1  14464  climcndslem1  16047  climcndslem2  16048  geoisum1  16077  bpoly1  16246  ef4p  16310  efgt1p2  16311  efgt1p  16312  rpnnen2lem3  16413  modxp1i  17277  numexp1  17283  psgnpmtr  19754  lt6abl  20139  cphipval  25594  iblcnlem1  26138  itgcnlem  26140  dvexp  26303  dveflem  26329  plyid  26557  coeidp  26612  dgrid  26613  cxp1  27029  1cubrlem  27199  1cubr  27200  log2ublem3  27306  basellem5  27442  perfectlem2  27587  logdivsum  27890  log2sumbnd  27901  fltoprmlem2  28024  ipval2  31339  0dp2dp  33545  cos9thpiminplylem5  34488  subfacval2  36119  dvasin  38814  areacirclem1  38818  goldratmolem2  48138  1t10e1p1e11  48585  fmtnoge3  48820  fmtno0  48830  fmtno1  48831  lighneallem2  48896  lighneallem3  48897  41prothprmlem2  48908  perfectALTVlem2  49025  8exp8mod9  49039  tgblthelfgott  49118  exple2lt6  49681  pw2m1lepw2m1  49837  logbpw2m1  49884  nnpw2pmod  49900