Axiom ax-icn 9005

Description: _i is a complex number. Axiom 3 of 22 for real and complex numbers, justified by theorem axicn 8981. (Contributed by NM, 1-Mar-1995.)

Assertion

Ref	Expression
ax-icn	|- _i e. CC

Detailed syntax breakdown of Axiom ax-icn

Step	Hyp	Ref	Expression
1		ci 8948	. 2 class _i
2		cc 8944	. 2 class CC
3	1, 2	wcel 1721	1 wff _i e. CC

This axiom is referenced by:  0cn  9040  mulid1  9044  mul02lem2  9199  mul02  9200  addid1  9202  cnegex  9203  cnegex2  9204  0cnALT  9251  ine0  9425  ixi  9607  recextlem1  9608  recextlem2  9609  recex  9610  rimul  9947  cru  9948  crne0  9949  cju  9952  cnref1o  10563  irec  11435  i2  11436  i3  11437  i4  11438  iexpcyc  11440  crreczi  11459  imre  11868  reim  11869  imcl  11871  crre  11874  crim  11875  remim  11877  reim0  11878  reim0b  11879  rereb  11880  mulre  11881  cjreb  11883  recj  11884  reneg  11885  readd  11886  remullem  11888  imcj  11892  imneg  11893  imadd  11894  cjadd  11901  cjneg  11907  imval2  11911  rei  11916  imi  11917  cji  11919  cjreim  11920  cjreim2  11921  rennim  11999  cnpart  12000  sqrneglem  12027  sqrneg  12028  sqrm1  12036  absi  12046  absreimsq  12052  absreim  12053  absimle  12069  abs1m  12094  recan  12095  sqreulem  12118  sqreu  12119  caucvgr  12424  sinf  12680  cosf  12681  tanval2  12689  tanval3  12690  resinval  12691  recosval  12692  efi4p  12693  resin4p  12694  recos4p  12695  resincl  12696  recoscl  12697  sinneg  12702  cosneg  12703  cos0  12706  efival  12708  efmival  12709  sinhval  12710  coshval  12711  retanhcl  12715  tanhlt1  12716  tanhbnd  12717  efeul  12718  sinadd  12720  cosadd  12721  ef01bndlem  12740  sin01bnd  12741  cos01bnd  12742  absef  12753  absefib  12754  efieq1re  12755  demoivre  12756  demoivreALT  12757  nthruc  12805  igz  13257  4sqlem17  13284  cnsubrg  16714  cnrehmeo  18931  itg0  19624  itgz  19625  itgcl  19628  ibl0  19631  iblcnlem1  19632  itgcnlem  19634  itgrevallem1  19639  itgneg  19648  iblss  19649  iblss2  19650  itgss  19656  itgeqa  19658  iblconst  19662  itgconst  19663  itgadd  19669  iblabs  19673  iblabsr  19674  iblmulc2  19675  itgmulc2  19678  itgsplit  19680  dvmptim  19809  dvsincos  19818  iaa  20195  sincn  20313  coscn  20314  efhalfpi  20332  efipi  20334  ef2pi  20338  ef2kpi  20339  efper  20340  sinperlem  20341  efimpi  20352  pige3  20378  sineq0  20382  efeq1  20384  tanregt0  20394  efif1olem4  20400  efifo  20402  eff1olem  20403  logneg  20435  logm1  20436  lognegb  20437  eflogeq  20449  efiarg  20455  cosargd  20456  logimul  20462  logneg2  20463  abslogle  20466  tanarg  20467  logcn  20491  logf1o2  20494  cxpsqrlem  20546  cxpsqr  20547  root1eq1  20592  cxpeq  20594  ang180lem1  20604  ang180lem2  20605  ang180lem3  20606  ang180lem4  20607  1cubrlem  20634  1cubr  20635  asinlem  20661  asinlem2  20662  asinlem3a  20663  asinlem3  20664  asinf  20665  atandm2  20670  atandm3  20671  atanf  20673  asinneg  20679  efiasin  20681  sinasin  20682  asinsinlem  20684  asinsin  20685  asin1  20687  asinbnd  20692  cosasin  20697  atanneg  20700  atancj  20703  efiatan  20705  atanlogaddlem  20706  atanlogadd  20707  atanlogsublem  20708  atanlogsub  20709  efiatan2  20710  2efiatan  20711  tanatan  20712  cosatan  20714  atantan  20716  atanbndlem  20718  atans2  20724  dvatan  20728  atantayl  20730  atantayl2  20731  log2cnv  20737  basellem3  20818  2sqlem2  21101  circgrp  21915  nvpi  22108  ipval2  22156  4ipval2  22157  ipval3  22158  4ipval3  22161  ipidsq  22162  dipcl  22164  dipcj  22166  dip0r  22169  dipcn  22172  sspival  22190  ip1ilem  22280  ipasslem10  22293  ipasslem11  22294  polid2i  22612  polidi  22613  lnopeq0lem1  23461  lnopeq0i  23463  lnophmlem2  23473  cnre2csqima  24262  itgaddnc  26164  iblabsnc  26168  iblmulc2nc  26169  itgmulc2nc  26172  dvreasin  26179  areacirclem5  26185  cntotbnd  26395  proot1ex  27388  sinh-conventional  28196