Axiom ax-icn 9995

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

This axiom is referenced by:  0cn  10032  mulid1  10037  mul02lem2  10213  mul02  10214  addid1  10216  cnegex  10217  cnegex2  10218  0cnALT  10270  negicn  10282  ine0  10465  ixi  10656  recextlem1  10657  recextlem2  10658  recex  10659  rimul  11011  cru  11012  crne0  11013  cju  11016  it0e0  11254  2mulicn  11255  2muline0  11256  cnref1o  11827  irec  12964  i2  12965  i3  12966  i4  12967  iexpcyc  12969  crreczi  12989  imre  13848  reim  13849  crre  13854  crim  13855  remim  13857  mulre  13861  cjreb  13863  recj  13864  reneg  13865  readd  13866  remullem  13868  imcj  13872  imneg  13873  imadd  13874  cjadd  13881  cjneg  13887  imval2  13891  rei  13896  imi  13897  cji  13899  cjreim  13900  cjreim2  13901  rennim  13979  cnpart  13980  sqrtneglem  14007  sqrtneg  14008  sqrtm1  14016  absi  14026  absreimsq  14032  absreim  14033  absimle  14049  abs1m  14075  sqreulem  14099  sqreu  14100  caucvgr  14406  sinf  14854  cosf  14855  tanval2  14863  tanval3  14864  resinval  14865  recosval  14866  efi4p  14867  resin4p  14868  recos4p  14869  resincl  14870  recoscl  14871  sinneg  14876  cosneg  14877  efival  14882  efmival  14883  sinhval  14884  coshval  14885  retanhcl  14889  tanhlt1  14890  tanhbnd  14891  efeul  14892  sinadd  14894  cosadd  14895  ef01bndlem  14914  sin01bnd  14915  cos01bnd  14916  absef  14927  absefib  14928  efieq1re  14929  demoivre  14930  demoivreALT  14931  nthruc  14981  igz  15638  4sqlem17  15665  cnsubrg  19806  cnrehmeo  22752  cmodscexp  22921  ncvspi  22956  cphipval2  23040  4cphipval2  23041  cphipval  23042  itg0  23546  itgz  23547  itgcl  23550  ibl0  23553  iblcnlem1  23554  itgcnlem  23556  itgneg  23570  iblss  23571  iblss2  23572  itgss  23578  itgeqa  23580  iblconst  23584  itgconst  23585  itgadd  23591  iblabs  23595  iblabsr  23596  iblmulc2  23597  itgmulc2  23600  itgsplit  23602  dvsincos  23744  iaa  24080  sincn  24198  coscn  24199  efhalfpi  24223  ef2kpi  24230  efper  24231  sinperlem  24232  efimpi  24243  pige3  24269  sineq0  24273  efeq1  24275  tanregt0  24285  efif1olem4  24291  efifo  24293  eff1olem  24294  circgrp  24298  circsubm  24299  logneg  24334  logm1  24335  lognegb  24336  eflogeq  24348  efiarg  24353  cosargd  24354  logimul  24360  logneg2  24361  abslogle  24364  tanarg  24365  logcn  24393  logf1o2  24396  cxpsqrtlem  24448  cxpsqrt  24449  root1eq1  24496  cxpeq  24498  ang180lem1  24539  ang180lem2  24540  ang180lem3  24541  ang180lem4  24542  1cubrlem  24568  1cubr  24569  asinlem  24595  asinlem2  24596  asinlem3a  24597  asinlem3  24598  asinf  24599  atandm2  24604  atandm3  24605  atanf  24607  asinneg  24613  efiasin  24615  sinasin  24616  asinsinlem  24618  asinsin  24619  asin1  24621  asinbnd  24626  cosasin  24631  atanneg  24634  atancj  24637  efiatan  24639  atanlogaddlem  24640  atanlogadd  24641  atanlogsublem  24642  atanlogsub  24643  efiatan2  24644  2efiatan  24645  tanatan  24646  cosatan  24648  atantan  24650  atanbndlem  24652  atans2  24658  dvatan  24662  atantayl  24664  atantayl2  24665  log2cnv  24671  basellem3  24809  2sqlem2  25143  nvpi  27522  ipval2  27562  4ipval2  27563  ipval3  27564  ipidsq  27565  dipcl  27567  dipcj  27569  dip0r  27572  dipcn  27575  ip1ilem  27681  ipasslem10  27694  ipasslem11  27695  polid2i  28014  polidi  28015  lnopeq0lem1  28864  lnopeq0i  28866  lnophmlem2  28876  bhmafibid1  29644  cnre2csqima  29957  efmul2picn  30674  itgexpif  30684  vtscl  30716  vtsprod  30717  circlemeth  30718  logi  31620  iexpire  31621  itgaddnc  33470  iblabsnc  33474  iblmulc2nc  33475  itgmulc2nc  33478  ftc1anclem3  33487  ftc1anclem6  33490  ftc1anclem7  33491  ftc1anclem8  33492  ftc1anc  33493  dvasin  33496  areacirclem4  33503  cntotbnd  33595  proot1ex  37779  sineq0ALT  39173  iblsplit  40182  sinh-conventional  42480