Theorem 0cn 11193

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

Assertion

Ref	Expression
0cn	⊢ 0 ∈ ℂ

Proof of Theorem 0cn

Step	Hyp	Ref	Expression
1		ax-i2m1 11163	. 2 ⊢ ((i · i) + 1) = 0
2		ax-icn 11154	. . . 4 ⊢ i ∈ ℂ
3		mulcl 11179	. . . 4 ⊢ ((i ∈ ℂ ∧ i ∈ ℂ) → (i · i) ∈ ℂ)
4	2, 2, 3	mp2an 704	. . 3 ⊢ (i · i) ∈ ℂ
5		ax-1cn 11153	. . 3 ⊢ 1 ∈ ℂ
6		addcl 11177	. . 3 ⊢ (((i · i) ∈ ℂ ∧ 1 ∈ ℂ) → ((i · i) + 1) ∈ ℂ)
7	4, 5, 6	mp2an 704	. 2 ⊢ ((i · i) + 1) ∈ ℂ
8	1, 7	eqeltrri 2860	1 ⊢ 0 ∈ ℂ

Syntax hints:   ∈ wcel 2143  (class class class)co 7410  ℂcc 11093  0cc0 11095  1c1 11096  ici 11097   + caddc 11098   · cmul 11100

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-ext 2735  ax-1cn 11153  ax-icn 11154  ax-addcl 11155  ax-mulcl 11157  ax-i2m1 11163

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1810  df-cleq 2755  df-clel 2838

This theorem is referenced by:  0cnd  11194  c0ex  11195  1re  11203  00id  11380  mul02lem1  11381  mul02  11383  mul01  11384  addrid  11385  addlid  11388  negcl  11452  subid  11472  subid1  11473  neg0  11499  negid  11500  negsub  11501  subneg  11502  negneg  11503  negeq0  11507  negsubdi  11509  renegcli  11514  mulneg1  11645  msqge0  11730  ixi  11838  muleqadd  11853  diveq0  11877  div0  11898  ofsubge0  12212  0m0e0  12354  nn0sscn  12504  elznn0  12601  ser0  14086  0exp0e1  14098  0exp  14129  sq0  14224  sqeqor  14248  binom2  14249  bcval5  14350  s1co  14866  shftval3  15109  shftidt2  15114  sgnneg  15133  cjne0  15210  sqrt0  15288  abs0  15332  abs00bd  15338  abs2dif  15380  clim0  15553  climz  15596  serclim0  15624  rlimneg  15694  sumrblem  15758  fsumcvg  15759  summolem2a  15762  sumss  15771  fsumss  15772  fsumcvg2  15774  fsumsplit  15788  sumsplit  15815  fsumrelem  15855  fsumrlim  15859  fsumo1  15860  0fallfac  16086  0risefac  16087  binomfallfac  16090  fsumcube  16109  ef0  16140  eftlub  16160  sin0  16200  tan0  16202  divalglem9  16454  sadadd2lem2  16503  sadadd3  16514  bezout  16596  pcmpt2  16948  4sqlem11  17010  ramcl  17084  4001lem2  17197  odadd1  19913  cnaddablx  19933  cnaddabl  19934  cnaddid  19935  frgpnabllem1  19938  cncrng  21543  cnfld0  21546  pzriprnglem5  21635  pzriprnglem6  21636  psdmplcl  22325  cnbl0  24930  cnblcld  24931  cnfldnm  24935  cnn0opn  24944  xrge0gsumle  24991  xrge0tsms  24992  cnheibor  25114  cnlmod  25299  csscld  25408  clsocv  25409  cnflduss  25515  cnfldcusp  25516  rrxmvallem  25563  rrxmval  25564  mbfss  25805  mbfmulc2lem  25806  0plef  25831  0pledm  25832  itg1ge0  25845  itg1addlem4  25858  itg2splitlem  25907  itg2addlem  25917  ibl0  25946  iblcnlem  25948  iblss2  25965  itgss3  25974  dvconst  26076  dvcnp2  26079  dveflem  26138  dv11cn  26160  lhop1lem  26172  plyun0  26354  plyeq0lem  26367  coeeulem  26381  coeeu  26382  coef3  26389  dgrle  26400  0dgrb  26403  coefv0  26405  coemulc  26412  coe1termlem  26415  coe1term  26416  dgr0  26419  dgrmulc  26428  dgrcolem2  26431  vieta1lem2  26472  iaa  26488  aareccl  26489  aalioulem3  26497  taylthlem2  26537  psercn  26589  pserdvlem2  26591  abelthlem2  26595  abelthlem3  26596  abelthlem5  26598  abelthlem7  26601  abelth  26604  sin2kpi  26648  cos2kpi  26649  sinkpi  26687  efopn  26823  logtayl  26825  cxpval  26829  0cxp  26831  cxpexp  26833  cxpcl  26839  cxpge0  26848  mulcxplem  26849  mulcxp  26850  cxpmul2  26854  dvsqrt  26907  dvcnsqrt  26909  cxpcn3  26913  abscxpbnd  26918  efrlim  27134  ftalem2  27238  ftalem3  27239  ftalem4  27240  ftalem5  27241  ftalem7  27243  prmorcht  27342  muinv  27357  1sgm2ppw  27364  logfacbnd3  27387  logexprlim  27389  dchrelbas2  27401  dchrmullid  27416  dchrfi  27419  dchrinv  27425  lgsdir2  27494  lgsdir  27496  addsqnreup  27607  dchrvmasumiflem1  27665  dchrvmasumiflem2  27666  rpvmasum2  27676  log2sumbnd  27708  selberg2lem  27714  logdivbnd  27720  ax5seglem8  29286  axlowdimlem6  29297  axlowdimlem13  29304  ex-co  30789  avril1  30814  vc0  30926  vcz  30927  cnaddabloOLD  30933  cnidOLD  30934  ipasslem8  31189  siilem2  31204  hvmul0  31376  hi01  31448  norm-iii  31492  h1de2ctlem  31907  pjmuli  32041  pjneli  32075  eigre  32187  eigorth  32190  elnlfn  32280  0cnfn  32332  0lnfn  32337  lnopunilem2  32363  xrge0tsmsd  33393  constrsscn  34130  qqh0  34374  qqhcn  34381  eulerpartlemgs2  34770  breprexpnat  35021  hgt750lem2  35039  subfacp1lem6  35677  sinccvglem  36164  abs2sqle  36172  abs2sqlt  36173  tan2h  38283  poimirlem16  38307  poimirlem19  38310  poimirlem31  38322  mblfinlem2  38329  ovoliunnfl  38333  voliunnfl  38335  ftc1anclem5  38368  cntotbnd  38467  60lcm7e420  42797  lcmineqlem10  42825  3lexlogpow5ineq1  42841  25or6to4  42993  sn-1ne2  43052  0tie0  43096  sn-it0e0  43197  addinvcom  43213  sn-0tie0  43245  fltnltalem  43414  flcidc  43917  dvconstbi  45064  expgrowth  45065  dvradcnv2  45077  binomcxplemdvbinom  45083  binomcxplemnotnn0  45086  xralrple3  46109  negcncfg  46615  ioodvbdlimc1  46667  ioodvbdlimc2  46669  itgsinexplem1  46688  stoweidlem26  46760  stoweidlem36  46770  stoweidlem55  46789  stirlinglem8  46815  fourierdlem103  46943  sqwvfoura  46962  sqwvfourb  46963  ovn0lem  47299  sqrtnnaa  47624  sqrtnzqaa  47625  nn0sumshdiglemA  49419  nn0sumshdiglemB  49420  nn0sumshdiglem1  49421  sec0  50558