Theorem 0cn 11122

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

Assertion

Ref	Expression
0cn	⊢ 0 ∈ ℂ

Proof of Theorem 0cn

Step	Hyp	Ref	Expression
1		ax-i2m1 11092	. 2 ⊢ ((i · i) + 1) = 0
2		ax-icn 11083	. . . 4 ⊢ i ∈ ℂ
3		mulcl 11108	. . . 4 ⊢ ((i ∈ ℂ ∧ i ∈ ℂ) → (i · i) ∈ ℂ)
4	2, 2, 3	mp2an 692	. . 3 ⊢ (i · i) ∈ ℂ
5		ax-1cn 11082	. . 3 ⊢ 1 ∈ ℂ
6		addcl 11106	. . 3 ⊢ (((i · i) ∈ ℂ ∧ 1 ∈ ℂ) → ((i · i) + 1) ∈ ℂ)
7	4, 5, 6	mp2an 692	. 2 ⊢ ((i · i) + 1) ∈ ℂ
8	1, 7	eqeltrri 2831	1 ⊢ 0 ∈ ℂ

Syntax hints:   ∈ wcel 2113  (class class class)co 7356  ℂcc 11022  0cc0 11024  1c1 11025  ici 11026   + caddc 11027   · cmul 11029

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2706  ax-1cn 11082  ax-icn 11083  ax-addcl 11084  ax-mulcl 11086  ax-i2m1 11092

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

This theorem is referenced by:  0cnd  11123  c0ex  11124  1re  11130  00id  11306  mul02lem1  11307  mul02  11309  mul01  11310  addrid  11311  addlid  11314  negcl  11378  subid  11398  subid1  11399  neg0  11425  negid  11426  negsub  11427  subneg  11428  negneg  11429  negeq0  11433  negsubdi  11435  renegcli  11440  mulneg1  11571  msqge0  11656  ixi  11764  muleqadd  11779  diveq0  11804  div0  11827  div0OLD  11828  ofsubge0  12142  0m0e0  12258  nn0sscn  12404  elznn0  12501  ser0  13975  0exp0e1  13987  0exp  14018  sq0  14113  sqeqor  14137  binom2  14138  bcval5  14239  s1co  14754  shftval3  14997  shftidt2  15002  cjne0  15084  sqrt0  15162  abs0  15206  abs00bd  15212  abs2dif  15254  clim0  15427  climz  15470  serclim0  15498  rlimneg  15568  sumrblem  15632  fsumcvg  15633  summolem2a  15636  sumss  15645  fsumss  15646  fsumcvg2  15648  fsumsplit  15662  sumsplit  15689  fsumrelem  15728  fsumrlim  15732  fsumo1  15733  0fallfac  15958  0risefac  15959  binomfallfac  15962  fsumcube  15981  ef0  16012  eftlub  16032  sin0  16072  tan0  16074  divalglem9  16326  sadadd2lem2  16375  sadadd3  16386  bezout  16468  pcmpt2  16819  4sqlem11  16881  ramcl  16955  4001lem2  17067  odadd1  19775  cnaddablx  19795  cnaddabl  19796  cnaddid  19797  frgpnabllem1  19800  cncrng  21341  cncrngOLD  21342  cnfld0  21345  pzriprnglem5  21438  pzriprnglem6  21439  psdmplcl  22103  cnbl0  24715  cnblcld  24716  cnfldnm  24720  cnn0opn  24729  xrge0gsumle  24776  xrge0tsms  24777  cnheibor  24908  cnlmod  25094  csscld  25203  clsocv  25204  cnflduss  25310  cnfldcusp  25311  rrxmvallem  25358  rrxmval  25359  mbfss  25601  mbfmulc2lem  25602  0plef  25627  0pledm  25628  itg1ge0  25641  itg1addlem4  25654  itg2splitlem  25703  itg2addlem  25713  ibl0  25742  iblcnlem  25744  iblss2  25761  itgss3  25770  dvconst  25872  dvcnp2  25875  dvcnp2OLD  25876  dveflem  25937  dv11cn  25960  lhop1lem  25972  plyun0  26156  plyeq0lem  26169  coeeulem  26183  coeeu  26184  coef3  26191  dgrle  26202  0dgrb  26205  coefv0  26207  coemulc  26214  coe1termlem  26217  coe1term  26218  dgr0  26222  dgrmulc  26231  dgrcolem2  26234  vieta1lem2  26273  iaa  26287  aareccl  26288  aalioulem3  26296  taylthlem2  26336  taylthlem2OLD  26337  psercn  26390  pserdvlem2  26392  abelthlem2  26396  abelthlem3  26397  abelthlem5  26399  abelthlem7  26402  abelth  26405  sin2kpi  26446  cos2kpi  26447  sinkpi  26485  efopn  26621  logtayl  26623  cxpval  26627  0cxp  26629  cxpexp  26631  cxpcl  26637  cxpge0  26646  mulcxplem  26647  mulcxp  26648  cxpmul2  26652  dvsqrt  26705  dvcnsqrt  26707  cxpcn3  26712  abscxpbnd  26717  efrlim  26933  efrlimOLD  26934  ftalem2  27038  ftalem3  27039  ftalem4  27040  ftalem5  27041  ftalem7  27043  prmorcht  27142  muinv  27157  1sgm2ppw  27165  logfacbnd3  27188  logexprlim  27190  dchrelbas2  27202  dchrmullid  27217  dchrfi  27220  dchrinv  27226  lgsdir2  27295  lgsdir  27297  addsqnreup  27408  dchrvmasumiflem1  27466  dchrvmasumiflem2  27467  rpvmasum2  27477  log2sumbnd  27509  selberg2lem  27515  logdivbnd  27521  ax5seglem8  28958  axlowdimlem6  28969  axlowdimlem13  28976  ex-co  30462  avril1  30487  vc0  30598  vcz  30599  cnaddabloOLD  30605  cnidOLD  30606  ipasslem8  30861  siilem2  30876  hvmul0  31048  hi01  31120  norm-iii  31164  h1de2ctlem  31579  pjmuli  31713  pjneli  31747  eigre  31859  eigorth  31862  elnlfn  31952  0cnfn  32004  0lnfn  32009  lnopunilem2  32035  sgnneg  32863  xrge0tsmsd  33104  constrsscn  33846  qqh0  34090  qqhcn  34097  eulerpartlemgs2  34486  breprexpnat  34740  hgt750lem2  34758  subfacp1lem6  35328  sinccvglem  35815  abs2sqle  35823  abs2sqlt  35824  tan2h  37752  poimirlem16  37776  poimirlem19  37779  poimirlem31  37791  mblfinlem2  37798  ovoliunnfl  37802  voliunnfl  37804  ftc1anclem5  37837  cntotbnd  37936  60lcm7e420  42203  lcmineqlem10  42231  3lexlogpow5ineq1  42247  sn-1ne2  42462  0tie0  42512  sn-it0e0  42613  addinvcom  42629  sn-0tie0  42648  fltnltalem  42847  flcidc  43354  dvconstbi  44517  expgrowth  44518  dvradcnv2  44530  binomcxplemdvbinom  44536  binomcxplemnotnn0  44539  xralrple3  45560  negcncfg  46067  ioodvbdlimc1  46119  ioodvbdlimc2  46121  itgsinexplem1  46140  stoweidlem26  46212  stoweidlem36  46222  stoweidlem55  46241  stirlinglem8  46267  fourierdlem103  46395  sqwvfoura  46414  sqwvfourb  46415  ovn0lem  46751  nthrucw  47072  nn0sumshdiglemA  48807  nn0sumshdiglemB  48808  nn0sumshdiglem1  48809  sec0  49947