Theorem 0cn 11107

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

Assertion

Ref	Expression
0cn	⊢ 0 ∈ ℂ

Proof of Theorem 0cn

Step	Hyp	Ref	Expression
1		ax-i2m1 11077	. 2 ⊢ ((i · i) + 1) = 0
2		ax-icn 11068	. . . 4 ⊢ i ∈ ℂ
3		mulcl 11093	. . . 4 ⊢ ((i ∈ ℂ ∧ i ∈ ℂ) → (i · i) ∈ ℂ)
4	2, 2, 3	mp2an 692	. . 3 ⊢ (i · i) ∈ ℂ
5		ax-1cn 11067	. . 3 ⊢ 1 ∈ ℂ
6		addcl 11091	. . 3 ⊢ (((i · i) ∈ ℂ ∧ 1 ∈ ℂ) → ((i · i) + 1) ∈ ℂ)
7	4, 5, 6	mp2an 692	. 2 ⊢ ((i · i) + 1) ∈ ℂ
8	1, 7	eqeltrri 2825	1 ⊢ 0 ∈ ℂ

Syntax hints:   ∈ wcel 2109  (class class class)co 7349  ℂcc 11007  0cc0 11009  1c1 11010  ici 11011   + caddc 11012   · cmul 11014

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701  ax-1cn 11067  ax-icn 11068  ax-addcl 11069  ax-mulcl 11071  ax-i2m1 11077

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-cleq 2721  df-clel 2803

This theorem is referenced by:  0cnd  11108  c0ex  11109  1re  11115  00id  11291  mul02lem1  11292  mul02  11294  mul01  11295  addrid  11296  addlid  11299  negcl  11363  subid  11383  subid1  11384  neg0  11410  negid  11411  negsub  11412  subneg  11413  negneg  11414  negeq0  11418  negsubdi  11420  renegcli  11425  mulneg1  11556  msqge0  11641  ixi  11749  muleqadd  11764  diveq0  11789  div0  11812  div0OLD  11813  ofsubge0  12127  0m0e0  12243  nn0sscn  12389  elznn0  12486  ser0  13961  0exp0e1  13973  0exp  14004  sq0  14099  sqeqor  14123  binom2  14124  bcval5  14225  s1co  14740  shftval3  14983  shftidt2  14988  cjne0  15070  sqrt0  15148  abs0  15192  abs00bd  15198  abs2dif  15240  clim0  15413  climz  15456  serclim0  15484  rlimneg  15554  sumrblem  15618  fsumcvg  15619  summolem2a  15622  sumss  15631  fsumss  15632  fsumcvg2  15634  fsumsplit  15648  sumsplit  15675  fsumrelem  15714  fsumrlim  15718  fsumo1  15719  0fallfac  15944  0risefac  15945  binomfallfac  15948  fsumcube  15967  ef0  15998  eftlub  16018  sin0  16058  tan0  16060  divalglem9  16312  sadadd2lem2  16361  sadadd3  16372  bezout  16454  pcmpt2  16805  4sqlem11  16867  ramcl  16941  4001lem2  17053  odadd1  19727  cnaddablx  19747  cnaddabl  19748  cnaddid  19749  frgpnabllem1  19752  cncrng  21295  cncrngOLD  21296  cnfld0  21299  pzriprnglem5  21392  pzriprnglem6  21393  psdmplcl  22047  cnbl0  24659  cnblcld  24660  cnfldnm  24664  cnn0opn  24673  xrge0gsumle  24720  xrge0tsms  24721  cnheibor  24852  cnlmod  25038  csscld  25147  clsocv  25148  cnflduss  25254  cnfldcusp  25255  rrxmvallem  25302  rrxmval  25303  mbfss  25545  mbfmulc2lem  25546  0plef  25571  0pledm  25572  itg1ge0  25585  itg1addlem4  25598  itg2splitlem  25647  itg2addlem  25657  ibl0  25686  iblcnlem  25688  iblss2  25705  itgss3  25714  dvconst  25816  dvcnp2  25819  dvcnp2OLD  25820  dveflem  25881  dv11cn  25904  lhop1lem  25916  plyun0  26100  plyeq0lem  26113  coeeulem  26127  coeeu  26128  coef3  26135  dgrle  26146  0dgrb  26149  coefv0  26151  coemulc  26158  coe1termlem  26161  coe1term  26162  dgr0  26166  dgrmulc  26175  dgrcolem2  26178  vieta1lem2  26217  iaa  26231  aareccl  26232  aalioulem3  26240  taylthlem2  26280  taylthlem2OLD  26281  psercn  26334  pserdvlem2  26336  abelthlem2  26340  abelthlem3  26341  abelthlem5  26343  abelthlem7  26346  abelth  26349  sin2kpi  26390  cos2kpi  26391  sinkpi  26429  efopn  26565  logtayl  26567  cxpval  26571  0cxp  26573  cxpexp  26575  cxpcl  26581  cxpge0  26590  mulcxplem  26591  mulcxp  26592  cxpmul2  26596  dvsqrt  26649  dvcnsqrt  26651  cxpcn3  26656  abscxpbnd  26661  efrlim  26877  efrlimOLD  26878  ftalem2  26982  ftalem3  26983  ftalem4  26984  ftalem5  26985  ftalem7  26987  prmorcht  27086  muinv  27101  1sgm2ppw  27109  logfacbnd3  27132  logexprlim  27134  dchrelbas2  27146  dchrmullid  27161  dchrfi  27164  dchrinv  27170  lgsdir2  27239  lgsdir  27241  addsqnreup  27352  dchrvmasumiflem1  27410  dchrvmasumiflem2  27411  rpvmasum2  27421  log2sumbnd  27453  selberg2lem  27459  logdivbnd  27465  ax5seglem8  28881  axlowdimlem6  28892  axlowdimlem13  28899  ex-co  30382  avril1  30407  vc0  30518  vcz  30519  cnaddabloOLD  30525  cnidOLD  30526  ipasslem8  30781  siilem2  30796  hvmul0  30968  hi01  31040  norm-iii  31084  h1de2ctlem  31499  pjmuli  31633  pjneli  31667  eigre  31779  eigorth  31782  elnlfn  31872  0cnfn  31924  0lnfn  31929  lnopunilem2  31955  sgnneg  32778  xrge0tsmsd  33015  constrsscn  33707  qqh0  33951  qqhcn  33958  eulerpartlemgs2  34348  breprexpnat  34602  hgt750lem2  34620  subfacp1lem6  35158  sinccvglem  35645  abs2sqle  35653  abs2sqlt  35654  tan2h  37592  poimirlem16  37616  poimirlem19  37619  poimirlem31  37631  mblfinlem2  37638  ovoliunnfl  37642  voliunnfl  37644  ftc1anclem5  37677  cntotbnd  37776  60lcm7e420  41983  lcmineqlem10  42011  3lexlogpow5ineq1  42027  sn-1ne2  42238  0tie0  42288  sn-it0e0  42389  addinvcom  42405  sn-0tie0  42424  fltnltalem  42635  flcidc  43143  dvconstbi  44307  expgrowth  44308  dvradcnv2  44320  binomcxplemdvbinom  44326  binomcxplemnotnn0  44329  xralrple3  45353  negcncfg  45862  ioodvbdlimc1  45914  ioodvbdlimc2  45916  itgsinexplem1  45935  stoweidlem26  46007  stoweidlem36  46017  stoweidlem55  46036  stirlinglem8  46062  fourierdlem103  46190  sqwvfoura  46209  sqwvfourb  46210  ovn0lem  46546  nn0sumshdiglemA  48604  nn0sumshdiglemB  48605  nn0sumshdiglem1  48606  sec0  49745