Theorem 0cn 11253

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

Assertion

Ref	Expression
0cn	⊢ 0 ∈ ℂ

Proof of Theorem 0cn

Step	Hyp	Ref	Expression
1		ax-i2m1 11223	. 2 ⊢ ((i · i) + 1) = 0
2		ax-icn 11214	. . . 4 ⊢ i ∈ ℂ
3		mulcl 11239	. . . 4 ⊢ ((i ∈ ℂ ∧ i ∈ ℂ) → (i · i) ∈ ℂ)
4	2, 2, 3	mp2an 692	. . 3 ⊢ (i · i) ∈ ℂ
5		ax-1cn 11213	. . 3 ⊢ 1 ∈ ℂ
6		addcl 11237	. . 3 ⊢ (((i · i) ∈ ℂ ∧ 1 ∈ ℂ) → ((i · i) + 1) ∈ ℂ)
7	4, 5, 6	mp2an 692	. 2 ⊢ ((i · i) + 1) ∈ ℂ
8	1, 7	eqeltrri 2838	1 ⊢ 0 ∈ ℂ

Syntax hints:   ∈ wcel 2108  (class class class)co 7431  ℂcc 11153  0cc0 11155  1c1 11156  ici 11157   + caddc 11158   · cmul 11160

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 2007  ax-8 2110  ax-9 2118  ax-ext 2708  ax-1cn 11213  ax-icn 11214  ax-addcl 11215  ax-mulcl 11217  ax-i2m1 11223

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

This theorem is referenced by:  0cnd  11254  c0ex  11255  1re  11261  00id  11436  mul02lem1  11437  mul02  11439  mul01  11440  addrid  11441  addlid  11444  negcl  11508  subid  11528  subid1  11529  neg0  11555  negid  11556  negsub  11557  subneg  11558  negneg  11559  negeq0  11563  negsubdi  11565  renegcli  11570  mulneg1  11699  msqge0  11784  ixi  11892  muleqadd  11907  diveq0  11932  div0  11955  div0OLD  11956  ofsubge0  12265  0m0e0  12386  nn0sscn  12531  elznn0  12628  ser0  14095  0exp0e1  14107  0exp  14138  sq0  14231  sqeqor  14255  binom2  14256  bcval5  14357  s1co  14872  shftval3  15115  shftidt2  15120  cjne0  15202  sqrt0  15280  abs0  15324  abs00bd  15330  abs2dif  15371  clim0  15542  climz  15585  serclim0  15613  rlimneg  15683  sumrblem  15747  fsumcvg  15748  summolem2a  15751  sumss  15760  fsumss  15761  fsumcvg2  15763  fsumsplit  15777  sumsplit  15804  fsumrelem  15843  fsumrlim  15847  fsumo1  15848  0fallfac  16073  0risefac  16074  binomfallfac  16077  fsumcube  16096  ef0  16127  eftlub  16145  sin0  16185  tan0  16187  divalglem9  16438  sadadd2lem2  16487  sadadd3  16498  bezout  16580  pcmpt2  16931  4sqlem11  16993  ramcl  17067  4001lem2  17179  odadd1  19866  cnaddablx  19886  cnaddabl  19887  cnaddid  19888  frgpnabllem1  19891  cncrng  21401  cncrngOLD  21402  cnfld0  21405  pzriprnglem5  21496  pzriprnglem6  21497  psdmplcl  22166  cnbl0  24794  cnblcld  24795  cnfldnm  24799  cnn0opn  24808  xrge0gsumle  24855  xrge0tsms  24856  cnheibor  24987  cnlmod  25173  csscld  25283  clsocv  25284  cnflduss  25390  cnfldcusp  25391  rrxmvallem  25438  rrxmval  25439  mbfss  25681  mbfmulc2lem  25682  0plef  25707  0pledm  25708  itg1ge0  25721  itg1addlem4  25734  itg2splitlem  25783  itg2addlem  25793  ibl0  25822  iblcnlem  25824  iblss2  25841  itgss3  25850  dvconst  25952  dvcnp2  25955  dvcnp2OLD  25956  dveflem  26017  dv11cn  26040  lhop1lem  26052  plyun0  26236  plyeq0lem  26249  coeeulem  26263  coeeu  26264  coef3  26271  dgrle  26282  0dgrb  26285  coefv0  26287  coemulc  26294  coe1termlem  26297  coe1term  26298  dgr0  26302  dgrmulc  26311  dgrcolem2  26314  vieta1lem2  26353  iaa  26367  aareccl  26368  aalioulem3  26376  taylthlem2  26416  taylthlem2OLD  26417  psercn  26470  pserdvlem2  26472  abelthlem2  26476  abelthlem3  26477  abelthlem5  26479  abelthlem7  26482  abelth  26485  sin2kpi  26525  cos2kpi  26526  sinkpi  26564  efopn  26700  logtayl  26702  cxpval  26706  0cxp  26708  cxpexp  26710  cxpcl  26716  cxpge0  26725  mulcxplem  26726  mulcxp  26727  cxpmul2  26731  dvsqrt  26784  dvcnsqrt  26786  cxpcn3  26791  abscxpbnd  26796  efrlim  27012  efrlimOLD  27013  ftalem2  27117  ftalem3  27118  ftalem4  27119  ftalem5  27120  ftalem7  27122  prmorcht  27221  muinv  27236  1sgm2ppw  27244  logfacbnd3  27267  logexprlim  27269  dchrelbas2  27281  dchrmullid  27296  dchrfi  27299  dchrinv  27305  lgsdir2  27374  lgsdir  27376  addsqnreup  27487  dchrvmasumiflem1  27545  dchrvmasumiflem2  27546  rpvmasum2  27556  log2sumbnd  27588  selberg2lem  27594  logdivbnd  27600  ax5seglem8  28951  axlowdimlem6  28962  axlowdimlem13  28969  ex-co  30457  avril1  30482  vc0  30593  vcz  30594  cnaddabloOLD  30600  cnidOLD  30601  ipasslem8  30856  siilem2  30871  hvmul0  31043  hi01  31115  norm-iii  31159  h1de2ctlem  31574  pjmuli  31708  pjneli  31742  eigre  31854  eigorth  31857  elnlfn  31947  0cnfn  31999  0lnfn  32004  lnopunilem2  32030  xrge0tsmsd  33065  constrsscn  33781  qqh0  33985  qqhcn  33992  eulerpartlemgs2  34382  sgnneg  34543  breprexpnat  34649  hgt750lem2  34667  subfacp1lem6  35190  sinccvglem  35677  abs2sqle  35685  abs2sqlt  35686  tan2h  37619  poimirlem16  37643  poimirlem19  37646  poimirlem31  37658  mblfinlem2  37665  ovoliunnfl  37669  voliunnfl  37671  ftc1anclem5  37704  cntotbnd  37803  60lcm7e420  42011  lcmineqlem10  42039  3lexlogpow5ineq1  42055  sn-1ne2  42300  0tie0  42350  sn-it0e0  42445  addinvcom  42461  sn-0tie0  42469  fltnltalem  42672  flcidc  43182  dvconstbi  44353  expgrowth  44354  dvradcnv2  44366  binomcxplemdvbinom  44372  binomcxplemnotnn0  44375  xralrple3  45385  negcncfg  45896  ioodvbdlimc1  45948  ioodvbdlimc2  45950  itgsinexplem1  45969  stoweidlem26  46041  stoweidlem36  46051  stoweidlem55  46070  stirlinglem8  46096  fourierdlem103  46224  sqwvfoura  46243  sqwvfourb  46244  ovn0lem  46580  nn0sumshdiglemA  48540  nn0sumshdiglemB  48541  nn0sumshdiglem1  48542  sec0  49279