Axiom ax-icn 9616

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

This axiom is referenced by:  0cn  9653  mulid1  9658  mul02lem2  9828  mul02  9829  addid1  9831  cnegex  9832  cnegex2  9833  0cnALT  9884  negicn  9896  ine0  10075  ixi  10263  recextlem1  10264  recextlem2  10265  recex  10266  rimul  10622  cru  10623  crne0  10624  cju  10627  it0e0  10858  2mulicn  10859  2muline0  10860  cnref1o  11320  irec  12412  i2  12413  i3  12414  i4  12415  iexpcyc  12417  crreczi  12435  imre  13248  reim  13249  crre  13254  crim  13255  remim  13257  mulre  13261  cjreb  13263  recj  13264  reneg  13265  readd  13266  remullem  13268  imcj  13272  imneg  13273  imadd  13274  cjadd  13281  cjneg  13287  imval2  13291  rei  13296  imi  13297  cji  13299  cjreim  13300  cjreim2  13301  rennim  13379  cnpart  13380  sqrtneglem  13407  sqrtneg  13408  sqrtm1  13416  absi  13426  absreimsq  13432  absreim  13433  absimle  13449  abs1m  13475  sqreulem  13499  sqreu  13500  caucvgr  13818  sinf  14255  cosf  14256  tanval2  14264  tanval3  14265  resinval  14266  recosval  14267  efi4p  14268  resin4p  14269  recos4p  14270  resincl  14271  recoscl  14272  sinneg  14277  cosneg  14278  efival  14283  efmival  14284  sinhval  14285  coshval  14286  retanhcl  14290  tanhlt1  14291  tanhbnd  14292  efeul  14293  sinadd  14295  cosadd  14296  ef01bndlem  14315  sin01bnd  14316  cos01bnd  14317  absef  14328  absefib  14329  efieq1re  14330  demoivre  14331  demoivreALT  14332  nthruc  14380  igz  14957  4sqlem17OLD  14984  4sqlem17  14990  cnsubrg  19105  cnrehmeo  22059  itg0  22816  itgz  22817  itgcl  22820  ibl0  22823  iblcnlem1  22824  itgcnlem  22826  itgneg  22840  iblss  22841  iblss2  22842  itgss  22848  itgeqa  22850  iblconst  22854  itgconst  22855  itgadd  22861  iblabs  22865  iblabsr  22866  iblmulc2  22867  itgmulc2  22870  itgsplit  22872  dvsincos  23012  iaa  23360  sincn  23478  coscn  23479  efhalfpi  23505  ef2kpi  23512  efper  23513  sinperlem  23514  efimpi  23525  pige3  23551  sineq0  23555  efeq1  23557  tanregt0  23567  efif1olem4  23573  efifo  23575  eff1olem  23576  circgrp  23580  circsubm  23581  logneg  23616  logm1  23617  lognegb  23618  eflogeq  23630  efiarg  23635  cosargd  23636  logimul  23642  logneg2  23643  abslogle  23646  tanarg  23647  logcn  23671  logf1o2  23674  cxpsqrtlem  23726  cxpsqrt  23727  root1eq1  23774  cxpeq  23776  ang180lem1  23817  ang180lem2  23818  ang180lem3  23819  ang180lem4  23820  1cubrlem  23846  1cubr  23847  asinlem  23873  asinlem2  23874  asinlem3a  23875  asinlem3  23876  asinf  23877  atandm2  23882  atandm3  23883  atanf  23885  asinneg  23891  efiasin  23893  sinasin  23894  asinsinlem  23896  asinsin  23897  asin1  23899  asinbnd  23904  cosasin  23909  atanneg  23912  atancj  23915  efiatan  23917  atanlogaddlem  23918  atanlogadd  23919  atanlogsublem  23920  atanlogsub  23921  efiatan2  23922  2efiatan  23923  tanatan  23924  cosatan  23926  atantan  23928  atanbndlem  23930  atans2  23936  dvatan  23940  atantayl  23942  atantayl2  23943  log2cnv  23949  basellem3  24088  2sqlem2  24371  circgrpOLD  26183  nvpi  26376  ipval2  26424  4ipval2  26425  ipval3  26426  4ipval3  26429  ipidsq  26430  dipcl  26432  dipcj  26434  dip0r  26437  dipcn  26440  sspival  26458  ip1ilem  26548  ipasslem10  26561  ipasslem11  26562  polid2i  26891  polidi  26892  lnopeq0lem1  27739  lnopeq0i  27741  lnophmlem2  27751  bhmafibid1  28480  cnre2csqima  28791  logi  30441  iexpire  30442  itgaddnc  32066  iblabsnc  32070  iblmulc2nc  32071  itgmulc2nc  32074  ftc1anclem3  32083  ftc1anclem6  32086  ftc1anclem7  32087  ftc1anclem8  32088  ftc1anc  32089  dvasin  32092  areacirclem4  32099  cntotbnd  32192  proot1ex  36149  iblsplit  37940  sinh-conventional  40967