Axiom ax-icn 9600

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

This axiom is referenced by:  0cn  9637  mulid1  9642  mul02lem2  9812  mul02  9813  addid1  9815  cnegex  9816  cnegex2  9817  0cnALT  9866  negicn  9878  ine0  10056  ixi  10243  recextlem1  10244  recextlem2  10245  recex  10246  rimul  10602  cru  10603  crne0  10604  cju  10607  it0e0  10837  2mulicn  10838  2muline0  10839  cnref1o  11299  irec  12375  i2  12376  i3  12377  i4  12378  iexpcyc  12380  crreczi  12398  imre  13165  reim  13166  crre  13171  crim  13172  remim  13174  mulre  13178  cjreb  13180  recj  13181  reneg  13182  readd  13183  remullem  13185  imcj  13189  imneg  13190  imadd  13191  cjadd  13198  cjneg  13204  imval2  13208  rei  13213  imi  13214  cji  13216  cjreim  13217  cjreim2  13218  rennim  13296  cnpart  13297  sqrtneglem  13324  sqrtneg  13325  sqrtm1  13333  absi  13343  absreimsq  13349  absreim  13350  absimle  13366  abs1m  13392  sqreulem  13416  sqreu  13417  caucvgr  13734  sinf  14171  cosf  14172  tanval2  14180  tanval3  14181  resinval  14182  recosval  14183  efi4p  14184  resin4p  14185  recos4p  14186  resincl  14187  recoscl  14188  sinneg  14193  cosneg  14194  efival  14199  efmival  14200  sinhval  14201  coshval  14202  retanhcl  14206  tanhlt1  14207  tanhbnd  14208  efeul  14209  sinadd  14211  cosadd  14212  ef01bndlem  14231  sin01bnd  14232  cos01bnd  14233  absef  14244  absefib  14245  efieq1re  14246  demoivre  14247  demoivreALT  14248  nthruc  14296  igz  14871  4sqlem17OLD  14898  4sqlem17  14904  cnsubrg  19021  cnrehmeo  21973  itg0  22729  itgz  22730  itgcl  22733  ibl0  22736  iblcnlem1  22737  itgcnlem  22739  itgneg  22753  iblss  22754  iblss2  22755  itgss  22761  itgeqa  22763  iblconst  22767  itgconst  22768  itgadd  22774  iblabs  22778  iblabsr  22779  iblmulc2  22780  itgmulc2  22783  itgsplit  22785  dvsincos  22925  iaa  23273  sincn  23391  coscn  23392  efhalfpi  23418  ef2kpi  23425  efper  23426  sinperlem  23427  efimpi  23438  pige3  23464  sineq0  23468  efeq1  23470  tanregt0  23480  efif1olem4  23486  efifo  23488  eff1olem  23489  circgrp  23493  circsubm  23494  logneg  23529  logm1  23530  lognegb  23531  eflogeq  23543  efiarg  23548  cosargd  23549  logimul  23555  logneg2  23556  abslogle  23559  tanarg  23560  logcn  23584  logf1o2  23587  cxpsqrtlem  23639  cxpsqrt  23640  root1eq1  23687  cxpeq  23689  ang180lem1  23730  ang180lem2  23731  ang180lem3  23732  ang180lem4  23733  1cubrlem  23759  1cubr  23760  asinlem  23786  asinlem2  23787  asinlem3a  23788  asinlem3  23789  asinf  23790  atandm2  23795  atandm3  23796  atanf  23798  asinneg  23804  efiasin  23806  sinasin  23807  asinsinlem  23809  asinsin  23810  asin1  23812  asinbnd  23817  cosasin  23822  atanneg  23825  atancj  23828  efiatan  23830  atanlogaddlem  23831  atanlogadd  23832  atanlogsublem  23833  atanlogsub  23834  efiatan2  23835  2efiatan  23836  tanatan  23837  cosatan  23839  atantan  23841  atanbndlem  23843  atans2  23849  dvatan  23853  atantayl  23855  atantayl2  23856  log2cnv  23862  basellem3  24001  2sqlem2  24284  circgrpOLD  26094  nvpi  26287  ipval2  26335  4ipval2  26336  ipval3  26337  4ipval3  26340  ipidsq  26341  dipcl  26343  dipcj  26345  dip0r  26348  dipcn  26351  sspival  26369  ip1ilem  26459  ipasslem10  26472  ipasslem11  26473  polid2i  26802  polidi  26803  lnopeq0lem1  27650  lnopeq0i  27652  lnophmlem2  27662  bhmafibid1  28406  cnre2csqima  28719  logi  30371  iexpire  30372  itgaddnc  31960  iblabsnc  31964  iblmulc2nc  31965  itgmulc2nc  31968  ftc1anclem3  31977  ftc1anclem6  31980  ftc1anclem7  31981  ftc1anclem8  31982  ftc1anc  31983  dvasin  31986  areacirclem4  31993  cntotbnd  32086  proot1ex  36042  iblsplit  37707  sinh-conventional  39803