Axiom ax-icn 9568

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

This axiom is referenced by:  0cn  9605  mulid1  9610  mul02lem2  9774  mul02  9775  addid1  9777  cnegex  9778  cnegex2  9779  0cnALT  9828  negicn  9840  ine0  10013  ixi  10199  recextlem1  10200  recextlem2  10201  recex  10202  rimul  10547  cru  10548  crne0  10549  cju  10552  it0e0  10782  2mulicn  10783  2muline0  10784  cnref1o  11240  irec  12269  i2  12270  i3  12271  i4  12272  iexpcyc  12274  crreczi  12293  imre  12952  reim  12953  crre  12958  crim  12959  remim  12961  mulre  12965  cjreb  12967  recj  12968  reneg  12969  readd  12970  remullem  12972  imcj  12976  imneg  12977  imadd  12978  cjadd  12985  cjneg  12991  imval2  12995  rei  13000  imi  13001  cji  13003  cjreim  13004  cjreim2  13005  rennim  13083  cnpart  13084  sqrtneglem  13111  sqrtneg  13112  sqrtm1  13120  absi  13130  absreimsq  13136  absreim  13137  absimle  13153  abs1m  13179  sqreulem  13203  sqreu  13204  caucvgr  13509  sinf  13870  cosf  13871  tanval2  13879  tanval3  13880  resinval  13881  recosval  13882  efi4p  13883  resin4p  13884  recos4p  13885  resincl  13886  recoscl  13887  sinneg  13892  cosneg  13893  efival  13898  efmival  13899  sinhval  13900  coshval  13901  retanhcl  13905  tanhlt1  13906  tanhbnd  13907  efeul  13908  sinadd  13910  cosadd  13911  ef01bndlem  13930  sin01bnd  13931  cos01bnd  13932  absef  13943  absefib  13944  efieq1re  13945  demoivre  13946  demoivreALT  13947  nthruc  13995  igz  14463  4sqlem17  14490  cnsubrg  18604  cnrehmeo  21578  itg0  22311  itgz  22312  itgcl  22315  ibl0  22318  iblcnlem1  22319  itgcnlem  22321  itgneg  22335  iblss  22336  iblss2  22337  itgss  22343  itgeqa  22345  iblconst  22349  itgconst  22350  itgadd  22356  iblabs  22360  iblabsr  22361  iblmulc2  22362  itgmulc2  22365  itgsplit  22367  dvsincos  22507  iaa  22846  sincn  22964  coscn  22965  efhalfpi  22989  ef2kpi  22996  efper  22997  sinperlem  22998  efimpi  23009  pige3  23035  sineq0  23039  efeq1  23041  tanregt0  23051  efif1olem4  23057  efifo  23059  eff1olem  23060  circgrp  23064  circsubm  23065  logneg  23097  logm1  23098  lognegb  23099  eflogeq  23111  efiarg  23117  cosargd  23118  logimul  23124  logneg2  23125  abslogle  23128  tanarg  23129  logcn  23153  logf1o2  23156  cxpsqrtlem  23208  cxpsqrt  23209  root1eq1  23254  cxpeq  23256  ang180lem1  23266  ang180lem2  23267  ang180lem3  23268  ang180lem4  23269  1cubrlem  23297  1cubr  23298  asinlem  23324  asinlem2  23325  asinlem3a  23326  asinlem3  23327  asinf  23328  atandm2  23333  atandm3  23334  atanf  23336  asinneg  23342  efiasin  23344  sinasin  23345  asinsinlem  23347  asinsin  23348  asin1  23350  asinbnd  23355  cosasin  23360  atanneg  23363  atancj  23366  efiatan  23368  atanlogaddlem  23369  atanlogadd  23370  atanlogsublem  23371  atanlogsub  23372  efiatan2  23373  2efiatan  23374  tanatan  23375  cosatan  23377  atantan  23379  atanbndlem  23381  atans2  23387  dvatan  23391  atantayl  23393  atantayl2  23394  log2cnv  23400  basellem3  23481  2sqlem2  23764  circgrpOLD  25502  nvpi  25695  ipval2  25743  4ipval2  25744  ipval3  25745  4ipval3  25748  ipidsq  25749  dipcl  25751  dipcj  25753  dip0r  25756  dipcn  25759  sspival  25777  ip1ilem  25867  ipasslem10  25880  ipasslem11  25881  polid2i  26200  polidi  26201  lnopeq0lem1  27050  lnopeq0i  27052  lnophmlem2  27062  bhmafibid1  27784  cnre2csqima  28046  logi  29296  iexpire  29297  itgaddnc  30237  iblabsnc  30241  iblmulc2nc  30242  itgmulc2nc  30245  ftc1anclem3  30254  ftc1anclem6  30257  ftc1anclem7  30258  ftc1anclem8  30259  ftc1anc  30260  dvasin  30265  areacirclem4  30272  cntotbnd  30454  proot1ex  31323  iblsplit  31926  sinh-conventional  33235