Axiom ax-icn 9563

Description: _i is a complex number. Axiom 3 of 22 for real and complex numbers, justified by theorem axicn 9539. (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 9506	. 2 class _i
2		cc 9502	. 2 class CC
3	1, 2	wcel 1767	1 wff _i e. CC

This axiom is referenced by:  0cn  9600  mulid1  9605  mul02lem2  9768  mul02  9769  addid1  9771  cnegex  9772  cnegex2  9773  0cnALT  9821  negicn  9833  ine0  10004  ixi  10190  recextlem1  10191  recextlem2  10192  recex  10193  rimul  10539  cru  10540  crne0  10541  cju  10544  it0e0  10773  2mulicn  10774  2muline0  10775  cnref1o  11227  irec  12247  i2  12248  i3  12249  i4  12250  iexpcyc  12252  crreczi  12271  imre  12920  reim  12921  crre  12926  crim  12927  remim  12929  mulre  12933  cjreb  12935  recj  12936  reneg  12937  readd  12938  remullem  12940  imcj  12944  imneg  12945  imadd  12946  cjadd  12953  cjneg  12959  imval2  12963  rei  12968  imi  12969  cji  12971  cjreim  12972  cjreim2  12973  rennim  13051  cnpart  13052  sqrtneglem  13079  sqrtneg  13080  sqrtm1  13088  absi  13098  absreimsq  13104  absreim  13105  absimle  13121  abs1m  13147  sqreulem  13171  sqreu  13172  caucvgr  13477  sinf  13736  cosf  13737  tanval2  13745  tanval3  13746  resinval  13747  recosval  13748  efi4p  13749  resin4p  13750  recos4p  13751  resincl  13752  recoscl  13753  sinneg  13758  cosneg  13759  efival  13764  efmival  13765  sinhval  13766  coshval  13767  retanhcl  13771  tanhlt1  13772  tanhbnd  13773  efeul  13774  sinadd  13776  cosadd  13777  ef01bndlem  13796  sin01bnd  13797  cos01bnd  13798  absef  13809  absefib  13810  efieq1re  13811  demoivre  13812  demoivreALT  13813  nthruc  13861  igz  14327  4sqlem17  14354  cnsubrg  18346  cnrehmeo  21319  itg0  22052  itgz  22053  itgcl  22056  ibl0  22059  iblcnlem1  22060  itgcnlem  22062  itgneg  22076  iblss  22077  iblss2  22078  itgss  22084  itgeqa  22086  iblconst  22090  itgconst  22091  itgadd  22097  iblabs  22101  iblabsr  22102  iblmulc2  22103  itgmulc2  22106  itgsplit  22108  dvsincos  22248  iaa  22586  sincn  22704  coscn  22705  efhalfpi  22728  ef2kpi  22735  efper  22736  sinperlem  22737  efimpi  22748  pige3  22774  sineq0  22778  efeq1  22780  tanregt0  22790  efif1olem4  22796  efifo  22798  eff1olem  22799  circgrp  22803  circsubm  22804  logneg  22836  logm1  22837  lognegb  22838  eflogeq  22850  efiarg  22856  cosargd  22857  logimul  22863  logneg2  22864  abslogle  22867  tanarg  22868  logcn  22892  logf1o2  22895  cxpsqrtlem  22947  cxpsqrt  22948  root1eq1  22993  cxpeq  22995  ang180lem1  23005  ang180lem2  23006  ang180lem3  23007  ang180lem4  23008  1cubrlem  23036  1cubr  23037  asinlem  23063  asinlem2  23064  asinlem3a  23065  asinlem3  23066  asinf  23067  atandm2  23072  atandm3  23073  atanf  23075  asinneg  23081  efiasin  23083  sinasin  23084  asinsinlem  23086  asinsin  23087  asin1  23089  asinbnd  23094  cosasin  23099  atanneg  23102  atancj  23105  efiatan  23107  atanlogaddlem  23108  atanlogadd  23109  atanlogsublem  23110  atanlogsub  23111  efiatan2  23112  2efiatan  23113  tanatan  23114  cosatan  23116  atantan  23118  atanbndlem  23120  atans2  23126  dvatan  23130  atantayl  23132  atantayl2  23133  log2cnv  23139  basellem3  23220  2sqlem2  23503  circgrpOLD  25207  nvpi  25400  ipval2  25448  4ipval2  25449  ipval3  25450  4ipval3  25453  ipidsq  25454  dipcl  25456  dipcj  25458  dip0r  25461  dipcn  25464  sspival  25482  ip1ilem  25572  ipasslem10  25585  ipasslem11  25586  polid2i  25905  polidi  25906  lnopeq0lem1  26755  lnopeq0i  26757  lnophmlem2  26767  bhmafibid1  27464  cnre2csqima  27725  itgaddnc  30009  iblabsnc  30013  iblmulc2nc  30014  itgmulc2nc  30017  ftc1anclem3  30026  ftc1anclem6  30029  ftc1anclem7  30030  ftc1anclem8  30031  ftc1anc  30032  dvasin  30037  areacirclem4  30044  cntotbnd  30226  proot1ex  31096  iblsplit  31613  sinh-conventional  32620