Theorem 0cn 11305

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

Assertion

Ref	Expression
0cn	⊢ 0 ∈ ℂ

Proof of Theorem 0cn

Step	Hyp	Ref	Expression
1		ax-i2m1 11275	. 2 ⊢ ((i · i) + 1) = 0
2		ax-icn 11266	. . . 4 ⊢ i ∈ ℂ
3		mulcl 11291	. . . 4 ⊢ ((i ∈ ℂ ∧ i ∈ ℂ) → (i · i) ∈ ℂ)
4	2, 2, 3	mp2an 705	. . 3 ⊢ (i · i) ∈ ℂ
5		ax-1cn 11265	. . 3 ⊢ 1 ∈ ℂ
6		addcl 11289	. . 3 ⊢ (((i · i) ∈ ℂ ∧ 1 ∈ ℂ) → ((i · i) + 1) ∈ ℂ)
7	4, 5, 6	mp2an 705	. 2 ⊢ ((i · i) + 1) ∈ ℂ
8	1, 7	eqeltrri 2857	1 ⊢ 0 ∈ ℂ

This proof depends on syntax axioms:   ∈ wcel 2144  (class class class)co 7424  ℂcc 11205  0cc0 11207  1c1 11208  ici 11209   + caddc 11210   · cmul 11212

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732  ax-1cn 11265  ax-icn 11266  ax-addcl 11267  ax-mulcl 11269  ax-i2m1 11275

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1812  df-cleq 2752  df-clel 2835

This theorem is used by:  0cnd  11306  c0ex  11307  1re  11315  00id  11492  mul02lem1  11493  mul02  11495  mul01  11496  addrid  11497  addlid  11500  negcl  11564  subid  11584  subid1  11585  neg0  11611  negid  11612  negsub  11613  subneg  11614  negneg  11615  negeq0  11619  negsubdi  11621  renegcli  11626  mulneg1  11759  msqge0  11844  ixi  11952  muleqadd  11967  diveq0  11991  div0  12012  ofsubge0  12326  0m0e0  12468  nn0sscn  12618  elznn0  12715  ser0  14204  0exp0e1  14216  0exp  14247  sq0  14342  sqeqor  14367  binom2  14368  bcval5  14469  s1co  14992  shftval3  15238  shftidt2  15243  sgnneg  15262  cjne0  15339  sqrt0  15417  abs0  15461  abs00bd  15467  abs2dif  15509  clim0  15682  climz  15725  serclim0  15753  rlimneg  15823  sumrblem  15886  fsumcvg  15887  summolem2a  15890  sumss  15899  fsumss  15900  fsumcvg2  15902  fsumsplit  15916  sumsplit  15943  fsumrelem  15983  fsumrlim  15987  fsumo1  15988  0fallfac  16212  0risefac  16213  binomfallfac  16216  fsumcube  16235  ef0  16266  eftlub  16286  sin0  16326  tan0  16328  divalglem9  16580  sadadd2lem2  16629  sadadd3  16640  bezout  16725  pcmpt2  17080  4sqlem11  17142  ramcl  17216  4001lem2  17329  odadd1  20071  cnaddablx  20091  cnaddabl  20092  cnaddid  20093  frgpnabllem1  20096  cncrng  21708  cnfld0  21711  pzriprnglem5  21800  pzriprnglem6  21801  psdmplcl  22492  cnbl0  25101  cnblcld  25102  cnfldnm  25106  cnn0opn  25115  xrge0gsumle  25162  xrge0tsms  25163  cnheibor  25285  cnlmod  25470  csscld  25579  clsocv  25580  cnflduss  25686  cnfldcusp  25687  rrxmvallem  25734  rrxmval  25735  mbfss  25976  mbfmulc2lem  25977  0plef  26002  0pledm  26003  itg1ge0  26016  itg1addlem4  26029  itg2splitlem  26078  itg2addlem  26088  ibl0  26116  iblcnlem  26118  iblss2  26135  itgss3  26144  dvconst  26246  dvcnp2  26249  dveflem  26308  dv11cn  26330  lhop1lem  26342  plyun0  26524  plyeq0lem  26538  coeeulem  26552  coeeu  26553  coef3  26560  dgrle  26571  0dgrb  26574  coefv0  26576  coemulc  26583  coe1termlem  26586  coe1term  26587  dgr0  26590  dgrmulc  26599  dgrcolem2  26602  vieta1lem2  26643  iaaOLD  26661  aareccl  26662  aalioulem3  26670  taylthlem2  26710  psercn  26762  pserdvlem2  26764  abelthlem2  26768  abelthlem3  26769  abelthlem5  26771  abelthlem7  26774  abelth  26777  sin2kpi  26821  cos2kpi  26822  sinkpi  26859  efopn  26995  logtayl  26997  cxpval  27001  0cxp  27003  cxpexp  27005  cxpcl  27011  cxpge0  27020  mulcxplem  27021  mulcxp  27022  cxpmul2  27026  dvsqrt  27079  dvcnsqrt  27081  cxpcn3  27085  abscxpbnd  27090  efrlim  27306  ftalem2  27410  ftalem3  27411  ftalem4  27412  ftalem5  27413  ftalem7  27415  prmorcht  27514  muinv  27529  1sgm2ppw  27536  logfacbnd3  27559  logexprlim  27561  dchrelbas2  27573  dchrmullid  27588  dchrfi  27591  dchrinv  27597  lgsdir2  27666  lgsdir  27668  addsqnreup  27779  dchrvmasumiflem1  27837  dchrvmasumiflem2  27838  rpvmasum2  27848  log2sumbnd  27880  selberg2lem  27886  logdivbnd  27892  ax5seglem8  29523  axlowdimlem6  29534  axlowdimlem13  29541  ex-co  31048  avril1  31073  vc0  31185  vcz  31186  cnaddabloOLD  31192  cnidOLD  31193  ipasslem8  31448  siilem2  31463  hvmul0  31635  hi01  31707  norm-iii  31751  h1de2ctlem  32166  pjmuli  32300  pjneli  32334  eigre  32446  eigorth  32449  elnlfn  32539  0cnfn  32591  0lnfn  32596  lnopunilem2  32622  xrge0tsmsd  33684  constrsscn  34422  qqh0  34666  qqhcn  34673  eulerpartlemgs2  35062  breprexpnat  35313  hgt750lem2  35331  subfacp1lem6  36068  sinccvglem  36555  abs2sqle  36563  abs2sqlt  36564  tan2h  38672  poimirlem16  38691  poimirlem19  38694  poimirlem31  38706  mblfinlem2  38713  ovoliunnfl  38717  voliunnfl  38719  ftc1anclem5  38752  cntotbnd  38867  60lcm7e420  43197  lcmineqlem10  43225  3lexlogpow5ineq1  43241  25or6to4  43393  sn-1ne2  43467  0tie0  43509  sn-it0e0  43604  addinvcom  43620  sn-0tie0  43652  fltnltalem  43810  flcidc  44309  dvconstbi  45455  expgrowth  45456  dvradcnv2  45468  binomcxplemdvbinom  45474  binomcxplemnotnn0  45477  xralrple3  46521  negcncfg  47027  ioodvbdlimc1  47079  ioodvbdlimc2  47081  itgsinexplem1  47100  stoweidlem26  47172  stoweidlem36  47182  stoweidlem55  47201  stirlinglem8  47227  fourierdlem103  47355  sqwvfoura  47374  sqwvfourb  47375  ovn0lem  47711  sqrtnnaa  48049  sqrtnzqaa  48050  nn0sumshdiglemA  49867  nn0sumshdiglemB  49868  nn0sumshdiglem1  49869  sec0  51064