Axiom ax-icn 9980

Description: i is a complex number. Axiom 3 of 22 for real and complex numbers, justified by theorem axicn 9956. (Contributed by NM, 1-Mar-1995.)

Assertion

Ref	Expression
ax-icn	⊢ i ∈ ℂ

Detailed syntax breakdown of Axiom ax-icn

Step	Hyp	Ref	Expression
1		ci 9923	. 2 class i
2		cc 9919	. 2 class ℂ
3	1, 2	wcel 1988	1 wff i ∈ ℂ

This axiom is referenced by:  0cn  10017  mulid1  10022  mul02lem2  10198  mul02  10199  addid1  10201  cnegex  10202  cnegex2  10203  0cnALT  10255  negicn  10267  ine0  10450  ixi  10641  recextlem1  10642  recextlem2  10643  recex  10644  rimul  10996  cru  10997  crne0  10998  cju  11001  it0e0  11239  2mulicn  11240  2muline0  11241  cnref1o  11812  irec  12947  i2  12948  i3  12949  i4  12950  iexpcyc  12952  crreczi  12972  imre  13829  reim  13830  crre  13835  crim  13836  remim  13838  mulre  13842  cjreb  13844  recj  13845  reneg  13846  readd  13847  remullem  13849  imcj  13853  imneg  13854  imadd  13855  cjadd  13862  cjneg  13868  imval2  13872  rei  13877  imi  13878  cji  13880  cjreim  13881  cjreim2  13882  rennim  13960  cnpart  13961  sqrtneglem  13988  sqrtneg  13989  sqrtm1  13997  absi  14007  absreimsq  14013  absreim  14014  absimle  14030  abs1m  14056  sqreulem  14080  sqreu  14081  caucvgr  14387  sinf  14835  cosf  14836  tanval2  14844  tanval3  14845  resinval  14846  recosval  14847  efi4p  14848  resin4p  14849  recos4p  14850  resincl  14851  recoscl  14852  sinneg  14857  cosneg  14858  efival  14863  efmival  14864  sinhval  14865  coshval  14866  retanhcl  14870  tanhlt1  14871  tanhbnd  14872  efeul  14873  sinadd  14875  cosadd  14876  ef01bndlem  14895  sin01bnd  14896  cos01bnd  14897  absef  14908  absefib  14909  efieq1re  14910  demoivre  14911  demoivreALT  14912  nthruc  14962  igz  15619  4sqlem17  15646  cnsubrg  19787  cnrehmeo  22733  cmodscexp  22902  ncvspi  22937  cphipval2  23021  4cphipval2  23022  cphipval  23023  itg0  23527  itgz  23528  itgcl  23531  ibl0  23534  iblcnlem1  23535  itgcnlem  23537  itgneg  23551  iblss  23552  iblss2  23553  itgss  23559  itgeqa  23561  iblconst  23565  itgconst  23566  itgadd  23572  iblabs  23576  iblabsr  23577  iblmulc2  23578  itgmulc2  23581  itgsplit  23583  dvsincos  23725  iaa  24061  sincn  24179  coscn  24180  efhalfpi  24204  ef2kpi  24211  efper  24212  sinperlem  24213  efimpi  24224  pige3  24250  sineq0  24254  efeq1  24256  tanregt0  24266  efif1olem4  24272  efifo  24274  eff1olem  24275  circgrp  24279  circsubm  24280  logneg  24315  logm1  24316  lognegb  24317  eflogeq  24329  efiarg  24334  cosargd  24335  logimul  24341  logneg2  24342  abslogle  24345  tanarg  24346  logcn  24374  logf1o2  24377  cxpsqrtlem  24429  cxpsqrt  24430  root1eq1  24477  cxpeq  24479  ang180lem1  24520  ang180lem2  24521  ang180lem3  24522  ang180lem4  24523  1cubrlem  24549  1cubr  24550  asinlem  24576  asinlem2  24577  asinlem3a  24578  asinlem3  24579  asinf  24580  atandm2  24585  atandm3  24586  atanf  24588  asinneg  24594  efiasin  24596  sinasin  24597  asinsinlem  24599  asinsin  24600  asin1  24602  asinbnd  24607  cosasin  24612  atanneg  24615  atancj  24618  efiatan  24620  atanlogaddlem  24621  atanlogadd  24622  atanlogsublem  24623  atanlogsub  24624  efiatan2  24625  2efiatan  24626  tanatan  24627  cosatan  24629  atantan  24631  atanbndlem  24633  atans2  24639  dvatan  24643  atantayl  24645  atantayl2  24646  log2cnv  24652  basellem3  24790  2sqlem2  25124  nvpi  27492  ipval2  27532  4ipval2  27533  ipval3  27534  ipidsq  27535  dipcl  27537  dipcj  27539  dip0r  27542  dipcn  27545  ip1ilem  27651  ipasslem10  27664  ipasslem11  27665  polid2i  27984  polidi  27985  lnopeq0lem1  28834  lnopeq0i  28836  lnophmlem2  28846  bhmafibid1  29618  cnre2csqima  29931  efmul2picn  30648  itgexpif  30658  vtscl  30690  vtsprod  30691  circlemeth  30692  logi  31595  iexpire  31596  itgaddnc  33441  iblabsnc  33445  iblmulc2nc  33446  itgmulc2nc  33449  ftc1anclem3  33458  ftc1anclem6  33461  ftc1anclem7  33462  ftc1anclem8  33463  ftc1anc  33464  dvasin  33467  areacirclem4  33474  cntotbnd  33566  proot1ex  37598  sineq0ALT  38993  iblsplit  39945  sinh-conventional  42245