Axiom ax-icn 9501

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

This axiom is referenced by:  0cn  9538  mulid1  9543  mul02lem2  9711  mul02  9712  addid1  9714  cnegex  9715  cnegex2  9716  0cnALT  9765  negicn  9777  ine0  9953  ixi  10139  recextlem1  10140  recextlem2  10141  recex  10142  rimul  10487  cru  10488  crne0  10489  cju  10492  it0e0  10722  2mulicn  10723  2muline0  10724  cnref1o  11178  irec  12222  i2  12223  i3  12224  i4  12225  iexpcyc  12227  crreczi  12245  imre  12997  reim  12998  crre  13003  crim  13004  remim  13006  mulre  13010  cjreb  13012  recj  13013  reneg  13014  readd  13015  remullem  13017  imcj  13021  imneg  13022  imadd  13023  cjadd  13030  cjneg  13036  imval2  13040  rei  13045  imi  13046  cji  13048  cjreim  13049  cjreim2  13050  rennim  13128  cnpart  13129  sqrtneglem  13156  sqrtneg  13157  sqrtm1  13165  absi  13175  absreimsq  13181  absreim  13182  absimle  13198  abs1m  13224  sqreulem  13248  sqreu  13249  caucvgr  13554  sinf  13960  cosf  13961  tanval2  13969  tanval3  13970  resinval  13971  recosval  13972  efi4p  13973  resin4p  13974  recos4p  13975  resincl  13976  recoscl  13977  sinneg  13982  cosneg  13983  efival  13988  efmival  13989  sinhval  13990  coshval  13991  retanhcl  13995  tanhlt1  13996  tanhbnd  13997  efeul  13998  sinadd  14000  cosadd  14001  ef01bndlem  14020  sin01bnd  14021  cos01bnd  14022  absef  14033  absefib  14034  efieq1re  14035  demoivre  14036  demoivreALT  14037  nthruc  14085  igz  14553  4sqlem17  14580  cnsubrg  18690  cnrehmeo  21637  itg0  22370  itgz  22371  itgcl  22374  ibl0  22377  iblcnlem1  22378  itgcnlem  22380  itgneg  22394  iblss  22395  iblss2  22396  itgss  22402  itgeqa  22404  iblconst  22408  itgconst  22409  itgadd  22415  iblabs  22419  iblabsr  22420  iblmulc2  22421  itgmulc2  22424  itgsplit  22426  dvsincos  22566  iaa  22905  sincn  23023  coscn  23024  efhalfpi  23048  ef2kpi  23055  efper  23056  sinperlem  23057  efimpi  23068  pige3  23094  sineq0  23098  efeq1  23100  tanregt0  23110  efif1olem4  23116  efifo  23118  eff1olem  23119  circgrp  23123  circsubm  23124  logneg  23159  logm1  23160  lognegb  23161  eflogeq  23173  efiarg  23178  cosargd  23179  logimul  23185  logneg2  23186  abslogle  23189  tanarg  23190  logcn  23214  logf1o2  23217  cxpsqrtlem  23269  cxpsqrt  23270  root1eq1  23317  cxpeq  23319  ang180lem1  23360  ang180lem2  23361  ang180lem3  23362  ang180lem4  23363  1cubrlem  23389  1cubr  23390  asinlem  23416  asinlem2  23417  asinlem3a  23418  asinlem3  23419  asinf  23420  atandm2  23425  atandm3  23426  atanf  23428  asinneg  23434  efiasin  23436  sinasin  23437  asinsinlem  23439  asinsin  23440  asin1  23442  asinbnd  23447  cosasin  23452  atanneg  23455  atancj  23458  efiatan  23460  atanlogaddlem  23461  atanlogadd  23462  atanlogsublem  23463  atanlogsub  23464  efiatan2  23465  2efiatan  23466  tanatan  23467  cosatan  23469  atantan  23471  atanbndlem  23473  atans2  23479  dvatan  23483  atantayl  23485  atantayl2  23486  log2cnv  23492  basellem3  23629  2sqlem2  23912  circgrpOLD  25670  nvpi  25863  ipval2  25911  4ipval2  25912  ipval3  25913  4ipval3  25916  ipidsq  25917  dipcl  25919  dipcj  25921  dip0r  25924  dipcn  25927  sspival  25945  ip1ilem  26035  ipasslem10  26048  ipasslem11  26049  polid2i  26368  polidi  26369  lnopeq0lem1  27217  lnopeq0i  27219  lnophmlem2  27229  bhmafibid1  27964  cnre2csqima  28226  logi  29829  iexpire  29830  itgaddnc  31429  iblabsnc  31433  iblmulc2nc  31434  itgmulc2nc  31437  ftc1anclem3  31446  ftc1anclem6  31449  ftc1anclem7  31450  ftc1anclem8  31451  ftc1anc  31452  dvasin  31455  areacirclem4  31462  cntotbnd  31555  proot1ex  35506  iblsplit  37115  sinh-conventional  38759