Theorem exp0 14025

Description: Value of a complex number raised to the zeroth power. Under our definition, 0↑0 = 1 (0exp0e1 14026), following standard convention, for instance Definition 10-4.1 of [Gleason] p. 134. (Contributed by NM, 20-May-2004.) (Revised by Mario Carneiro, 4-Jun-2014.)

Assertion

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

Proof of Theorem exp0

Step	Hyp	Ref	Expression
1		0z 12533	. . 3 ⊢ 0 ∈ ℤ
2		expval 14023	. . 3 ⊢ ((𝐴 ∈ ℂ ∧ 0 ∈ ℤ) → (𝐴↑0) = if(0 = 0, 1, if(0 < 0, (seq1( · , (ℕ × {𝐴}))‘0), (1 / (seq1( · , (ℕ × {𝐴}))‘-0)))))
3	1, 2	mpan2 697	. 2 ⊢ (𝐴 ∈ ℂ → (𝐴↑0) = if(0 = 0, 1, if(0 < 0, (seq1( · , (ℕ × {𝐴}))‘0), (1 / (seq1( · , (ℕ × {𝐴}))‘-0)))))
4		eqid 2740	. . 3 ⊢ 0 = 0
5	4	iftruei 4468	. 2 ⊢ if(0 = 0, 1, if(0 < 0, (seq1( · , (ℕ × {𝐴}))‘0), (1 / (seq1( · , (ℕ × {𝐴}))‘-0)))) = 1
6	3, 5	eqtrdi 2791	1 ⊢ (𝐴 ∈ ℂ → (𝐴↑0) = 1)

Syntax hints:   → wi 4   = wceq 1547   ∈ wcel 2119  ifcif 4461  {csn 4562   class class class wbr 5079   × cxp 5623  ‘cfv 6492  (class class class)co 7363  ℂcc 11034  0cc0 11036  1c1 11037   · cmul 11041   < clt 11177  -cneg 11376   / cdiv 11805  ℕcn 12172  ℤcz 12522  seqcseq 13961  ↑cexp 14021

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-10 2152  ax-11 2168  ax-12 2189  ax-ext 2712  ax-sep 5225  ax-nul 5235  ax-pr 5369  ax-1cn 11094  ax-addrcl 11097  ax-rnegex 11107  ax-cnre 11109

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 854  df-3or 1093  df-3an 1094  df-tru 1550  df-fal 1560  df-ex 1787  df-nf 1791  df-sb 2074  df-mo 2543  df-eu 2573  df-clab 2719  df-cleq 2732  df-clel 2815  df-nfc 2889  df-ne 2936  df-ral 3055  df-rex 3065  df-rab 3393  df-v 3434  df-sbc 3731  df-dif 3893  df-un 3895  df-in 3897  df-ss 3907  df-nul 4269  df-if 4462  df-sn 4563  df-pr 4565  df-op 4569  df-uni 4846  df-br 5080  df-opab 5142  df-mpt 5161  df-id 5520  df-xp 5631  df-rel 5632  df-cnv 5633  df-co 5634  df-dm 5635  df-rn 5636  df-res 5637  df-ima 5638  df-pred 6259  df-iota 6448  df-fun 6494  df-fv 6500  df-ov 7366  df-oprab 7367  df-mpo 7368  df-frecs 8228  df-wrecs 8259  df-recs 8308  df-rdg 8346  df-neg 11378  df-z 12523  df-seq 13962  df-exp 14022

This theorem is referenced by:  0exp0e1  14026  expp1  14028  expneg  14029  expcllem  14032  mulexp  14061  expadd  14064  expmul  14067  exp0d  14100  leexp1a  14135  exple1  14137  bernneq  14189  modexp  14198  faclbnd4lem1  14253  faclbnd4lem3  14255  faclbnd4lem4  14256  cjexp  15110  absexp  15264  binom  15793  incexclem  15799  incexc  15800  climcndslem1  15812  pwdif  15831  fprodconst  15941  fallfac0  15991  bpoly0  16013  ege2le3  16053  eft0val  16077  demoivreALT  16166  pwp1fsum  16358  bits0  16395  0bits  16406  bitsinv1  16409  sadcadd  16425  smumullem  16459  numexp0  17044  psgnunilem4  19470  psgn0fv0  19484  psgnsn  19493  psgnprfval1  19495  cnfldexp  21387  expmhm  21418  expcn  24864  iblcnlem1  25780  itgcnlem  25782  dvexp  25945  dvexp2  25946  plyconst  26196  0dgr  26235  0dgrb  26236  aaliou3lem2  26334  cxp0  26659  1cubr  26831  log2ublem3  26937  basellem2  27070  basellem5  27073  lgsquad2lem2  27373  0dp2dp  32994  fldext2chn  33919  oddpwdc  34545  breprexp  34824  subfacval2  35422  fwddifn0  36399  stoweidlem19  46469  fmtno0  48025  bits0ALTV  48177  0dig2nn0e  49110  0dig2nn0o  49111  nn0sumshdiglemA  49117  nn0sumshdiglemB  49118  nn0sumshdiglem1  49119  nn0sumshdiglem2  49120