Theorem 0cn 11223

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

Assertion

Ref	Expression
0cn	⊢ 0 ∈ ℂ

Proof of Theorem 0cn

Step	Hyp	Ref	Expression
1		ax-i2m1 11193	. 2 ⊢ ((i · i) + 1) = 0
2		ax-icn 11184	. . . 4 ⊢ i ∈ ℂ
3		mulcl 11209	. . . 4 ⊢ ((i ∈ ℂ ∧ i ∈ ℂ) → (i · i) ∈ ℂ)
4	2, 2, 3	mp2an 705	. . 3 ⊢ (i · i) ∈ ℂ
5		ax-1cn 11183	. . 3 ⊢ 1 ∈ ℂ
6		addcl 11207	. . 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 2145  (class class class)co 7414  ℂcc 11123  0cc0 11125  1c1 11126  ici 11127   + caddc 11128   · cmul 11130

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2732  ax-1cn 11183  ax-icn 11184  ax-addcl 11185  ax-mulcl 11187  ax-i2m1 11193

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

This theorem is used by:  0cnd  11224  c0ex  11225  1re  11233  00id  11410  mul02lem1  11411  mul02  11413  mul01  11414  addrid  11415  addlid  11418  negcl  11482  subid  11502  subid1  11503  neg0  11529  negid  11530  negsub  11531  subneg  11532  negneg  11533  negeq0  11537  negsubdi  11539  renegcli  11544  mulneg1  11675  msqge0  11760  ixi  11868  muleqadd  11883  diveq0  11907  div0  11928  ofsubge0  12242  0m0e0  12384  nn0sscn  12534  elznn0  12631  ser0  14119  0exp0e1  14131  0exp  14162  sq0  14257  sqeqor  14281  binom2  14282  bcval5  14383  s1co  14905  shftval3  15150  shftidt2  15155  sgnneg  15174  cjne0  15251  sqrt0  15329  abs0  15373  abs00bd  15379  abs2dif  15421  clim0  15594  climz  15637  serclim0  15665  rlimneg  15735  sumrblem  15798  fsumcvg  15799  summolem2a  15802  sumss  15811  fsumss  15812  fsumcvg2  15814  fsumsplit  15828  sumsplit  15855  fsumrelem  15895  fsumrlim  15899  fsumo1  15900  0fallfac  16124  0risefac  16125  binomfallfac  16128  fsumcube  16147  ef0  16178  eftlub  16198  sin0  16238  tan0  16240  divalglem9  16492  sadadd2lem2  16541  sadadd3  16552  bezout  16634  pcmpt2  16986  4sqlem11  17048  ramcl  17122  4001lem2  17235  odadd1  19976  cnaddablx  19996  cnaddabl  19997  cnaddid  19998  frgpnabllem1  20001  cncrng  21607  cnfld0  21610  pzriprnglem5  21699  pzriprnglem6  21700  psdmplcl  22391  cnbl0  25000  cnblcld  25001  cnfldnm  25005  cnn0opn  25014  xrge0gsumle  25061  xrge0tsms  25062  cnheibor  25184  cnlmod  25369  csscld  25478  clsocv  25479  cnflduss  25585  cnfldcusp  25586  rrxmvallem  25633  rrxmval  25634  mbfss  25875  mbfmulc2lem  25876  0plef  25901  0pledm  25902  itg1ge0  25915  itg1addlem4  25928  itg2splitlem  25977  itg2addlem  25987  ibl0  26015  iblcnlem  26017  iblss2  26034  itgss3  26043  dvconst  26145  dvcnp2  26148  dveflem  26207  dv11cn  26229  lhop1lem  26241  plyun0  26423  plyeq0lem  26437  coeeulem  26451  coeeu  26452  coef3  26459  dgrle  26470  0dgrb  26473  coefv0  26475  coemulc  26482  coe1termlem  26485  coe1term  26486  dgr0  26489  dgrmulc  26498  dgrcolem2  26501  vieta1lem2  26544  iaaOLD  26562  aareccl  26563  aalioulem3  26571  taylthlem2  26611  psercn  26663  pserdvlem2  26665  abelthlem2  26669  abelthlem3  26670  abelthlem5  26672  abelthlem7  26675  abelth  26678  sin2kpi  26722  cos2kpi  26723  sinkpi  26760  efopn  26896  logtayl  26898  cxpval  26902  0cxp  26904  cxpexp  26906  cxpcl  26912  cxpge0  26921  mulcxplem  26922  mulcxp  26923  cxpmul2  26927  dvsqrt  26980  dvcnsqrt  26982  cxpcn3  26986  abscxpbnd  26991  efrlim  27207  ftalem2  27311  ftalem3  27312  ftalem4  27313  ftalem5  27314  ftalem7  27316  prmorcht  27415  muinv  27430  1sgm2ppw  27437  logfacbnd3  27460  logexprlim  27462  dchrelbas2  27474  dchrmullid  27489  dchrfi  27492  dchrinv  27498  lgsdir2  27567  lgsdir  27569  addsqnreup  27680  dchrvmasumiflem1  27738  dchrvmasumiflem2  27739  rpvmasum2  27749  log2sumbnd  27781  selberg2lem  27787  logdivbnd  27793  ax5seglem8  29394  axlowdimlem6  29405  axlowdimlem13  29412  ex-co  30919  avril1  30944  vc0  31056  vcz  31057  cnaddabloOLD  31063  cnidOLD  31064  ipasslem8  31319  siilem2  31334  hvmul0  31506  hi01  31578  norm-iii  31622  h1de2ctlem  32037  pjmuli  32171  pjneli  32205  eigre  32317  eigorth  32320  elnlfn  32410  0cnfn  32462  0lnfn  32467  lnopunilem2  32493  xrge0tsmsd  33514  constrsscn  34251  qqh0  34495  qqhcn  34502  eulerpartlemgs2  34892  breprexpnat  35143  hgt750lem2  35161  subfacp1lem6  35765  sinccvglem  36252  abs2sqle  36260  abs2sqlt  36261  tan2h  38367  poimirlem16  38386  poimirlem19  38389  poimirlem31  38401  mblfinlem2  38408  ovoliunnfl  38412  voliunnfl  38414  ftc1anclem5  38447  cntotbnd  38547  60lcm7e420  42877  lcmineqlem10  42905  3lexlogpow5ineq1  42921  25or6to4  43073  sn-1ne2  43147  0tie0  43191  sn-it0e0  43292  addinvcom  43308  sn-0tie0  43340  fltnltalem  43509  flcidc  44012  dvconstbi  45159  expgrowth  45160  dvradcnv2  45172  binomcxplemdvbinom  45178  binomcxplemnotnn0  45181  xralrple3  46204  negcncfg  46710  ioodvbdlimc1  46762  ioodvbdlimc2  46764  itgsinexplem1  46783  stoweidlem26  46855  stoweidlem36  46865  stoweidlem55  46884  stirlinglem8  46910  fourierdlem103  47038  sqwvfoura  47057  sqwvfourb  47058  ovn0lem  47394  sqrtnnaa  47732  sqrtnzqaa  47733  nn0sumshdiglemA  49550  nn0sumshdiglemB  49551  nn0sumshdiglem1  49552  sec0  50687