Theorem 0cn 11250

Description: Zero is a complex number. See also 0cnALT 11493. (Contributed by NM, 19-Feb-2005.)

Assertion

Ref	Expression
0cn	⊢ 0 ∈ ℂ

Proof of Theorem 0cn

Step	Hyp	Ref	Expression
1		ax-i2m1 11220	. 2 ⊢ ((i · i) + 1) = 0
2		ax-icn 11211	. . . 4 ⊢ i ∈ ℂ
3		mulcl 11236	. . . 4 ⊢ ((i ∈ ℂ ∧ i ∈ ℂ) → (i · i) ∈ ℂ)
4	2, 2, 3	mp2an 692	. . 3 ⊢ (i · i) ∈ ℂ
5		ax-1cn 11210	. . 3 ⊢ 1 ∈ ℂ
6		addcl 11234	. . 3 ⊢ (((i · i) ∈ ℂ ∧ 1 ∈ ℂ) → ((i · i) + 1) ∈ ℂ)
7	4, 5, 6	mp2an 692	. 2 ⊢ ((i · i) + 1) ∈ ℂ
8	1, 7	eqeltrri 2835	1 ⊢ 0 ∈ ℂ

Syntax hints:   ∈ wcel 2105  (class class class)co 7430  ℂcc 11150  0cc0 11152  1c1 11153  ici 11154   + caddc 11155   · cmul 11157

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-8 2107  ax-9 2115  ax-ext 2705  ax-1cn 11210  ax-icn 11211  ax-addcl 11212  ax-mulcl 11214  ax-i2m1 11220

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1776  df-cleq 2726  df-clel 2813

This theorem is referenced by:  0cnd  11251  c0ex  11252  1re  11258  00id  11433  mul02lem1  11434  mul02  11436  mul01  11437  addrid  11438  addlid  11441  negcl  11505  subid  11525  subid1  11526  neg0  11552  negid  11553  negsub  11554  subneg  11555  negneg  11556  negeq0  11560  negsubdi  11562  renegcli  11567  mulneg1  11696  msqge0  11781  ixi  11889  muleqadd  11904  diveq0  11929  div0  11952  div0OLD  11953  ofsubge0  12262  0m0e0  12383  nn0sscn  12528  elznn0  12625  ser0  14091  0exp0e1  14103  0exp  14134  sq0  14227  sqeqor  14251  binom2  14252  bcval5  14353  s1co  14868  shftval3  15111  shftidt2  15116  cjne0  15198  sqrt0  15276  abs0  15320  abs00bd  15326  abs2dif  15367  clim0  15538  climz  15581  serclim0  15609  rlimneg  15679  sumrblem  15743  fsumcvg  15744  summolem2a  15747  sumss  15756  fsumss  15757  fsumcvg2  15759  fsumsplit  15773  sumsplit  15800  fsumrelem  15839  fsumrlim  15843  fsumo1  15844  0fallfac  16069  0risefac  16070  binomfallfac  16073  fsumcube  16092  ef0  16123  eftlub  16141  sin0  16181  tan0  16183  divalglem9  16434  sadadd2lem2  16483  sadadd3  16494  bezout  16576  pcmpt2  16926  4sqlem11  16988  ramcl  17062  4001lem2  17175  odadd1  19880  cnaddablx  19900  cnaddabl  19901  cnaddid  19902  frgpnabllem1  19905  cncrng  21418  cncrngOLD  21419  cnfld0  21422  pzriprnglem5  21513  pzriprnglem6  21514  psdmplcl  22183  cnbl0  24809  cnblcld  24810  cnfldnm  24814  xrge0gsumle  24868  xrge0tsms  24869  cnheibor  25000  cnlmod  25186  csscld  25296  clsocv  25297  cnflduss  25403  cnfldcusp  25404  rrxmvallem  25451  rrxmval  25452  mbfss  25694  mbfmulc2lem  25695  0plef  25720  0pledm  25721  itg1ge0  25734  itg1addlem4  25747  itg1addlem4OLD  25748  itg2splitlem  25797  itg2addlem  25807  ibl0  25836  iblcnlem  25838  iblss2  25855  itgss3  25864  dvconst  25966  dvcnp2  25969  dvcnp2OLD  25970  dvrec  26007  dvexp3  26030  dveflem  26031  dv11cn  26054  lhop1lem  26066  plyun0  26250  plyeq0lem  26263  coeeulem  26277  coeeu  26278  coef3  26285  dgrle  26296  0dgrb  26299  coefv0  26301  coemulc  26308  coe1termlem  26311  coe1term  26312  dgr0  26316  dgrmulc  26325  dgrcolem2  26328  vieta1lem2  26367  iaa  26381  aareccl  26382  aalioulem3  26390  taylthlem2  26430  taylthlem2OLD  26431  psercn  26484  pserdvlem2  26486  abelthlem2  26490  abelthlem3  26491  abelthlem5  26493  abelthlem7  26496  abelth  26499  sin2kpi  26539  cos2kpi  26540  sinkpi  26578  efopn  26714  logtayl  26716  cxpval  26720  0cxp  26722  cxpexp  26724  cxpcl  26730  cxpge0  26739  mulcxplem  26740  mulcxp  26741  cxpmul2  26745  dvsqrt  26798  dvcnsqrt  26800  cxpcn3  26805  abscxpbnd  26810  efrlim  27026  efrlimOLD  27027  ftalem2  27131  ftalem3  27132  ftalem4  27133  ftalem5  27134  ftalem7  27136  prmorcht  27235  muinv  27250  1sgm2ppw  27258  logfacbnd3  27281  logexprlim  27283  dchrelbas2  27295  dchrmullid  27310  dchrfi  27313  dchrinv  27319  lgsdir2  27388  lgsdir  27390  addsqnreup  27501  dchrvmasumiflem1  27559  dchrvmasumiflem2  27560  rpvmasum2  27570  log2sumbnd  27602  selberg2lem  27608  logdivbnd  27614  ax5seglem8  28965  axlowdimlem6  28976  axlowdimlem13  28983  ex-co  30466  avril1  30491  vc0  30602  vcz  30603  cnaddabloOLD  30609  cnidOLD  30610  ipasslem8  30865  siilem2  30880  hvmul0  31052  hi01  31124  norm-iii  31168  h1de2ctlem  31583  pjmuli  31717  pjneli  31751  eigre  31863  eigorth  31866  elnlfn  31956  0cnfn  32008  0lnfn  32013  lnopunilem2  32039  xrge0tsmsd  33047  constrsscn  33744  qqh0  33946  qqhcn  33953  eulerpartlemgs2  34361  sgnneg  34521  breprexpnat  34627  hgt750lem2  34645  subfacp1lem6  35169  sinccvglem  35656  abs2sqle  35664  abs2sqlt  35665  tan2h  37598  poimirlem16  37622  poimirlem19  37625  poimirlem31  37637  mblfinlem2  37644  ovoliunnfl  37648  voliunnfl  37650  dvtanlem  37655  ftc1anclem5  37683  cntotbnd  37782  60lcm7e420  41991  lcmineqlem10  42019  3lexlogpow5ineq1  42035  sn-1ne2  42278  0tie0  42328  sn-it0e0  42421  addinvcom  42437  sn-0tie0  42445  fltnltalem  42648  flcidc  43158  dvconstbi  44329  expgrowth  44330  dvradcnv2  44342  binomcxplemdvbinom  44348  binomcxplemnotnn0  44351  xralrple3  45323  negcncfg  45836  ioodvbdlimc1  45888  ioodvbdlimc2  45890  itgsinexplem1  45909  stoweidlem26  45981  stoweidlem36  45991  stoweidlem55  46010  stirlinglem8  46036  fourierdlem103  46164  sqwvfoura  46183  sqwvfourb  46184  ovn0lem  46520  nn0sumshdiglemA  48468  nn0sumshdiglemB  48469  nn0sumshdiglem1  48470  sec0  48990