Axiom ax-icn 11214

Description: i is a complex number. Axiom 3 of 22 for real and complex numbers, justified by Theorem axicn 11190. (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 11157	. 2 class i
2		cc 11153	. 2 class ℂ
3	1, 2	wcel 2108	1 wff i ∈ ℂ

This axiom is referenced by:  0cn  11253  mulrid  11259  mul02lem2  11438  mul02  11439  addrid  11441  cnegex  11442  cnegex2  11443  0cnALT  11496  0cnALT2  11497  negicn  11509  ine0  11698  ixi  11892  recextlem1  11893  recextlem2  11894  recex  11895  rimul  12257  cru  12258  crne0  12259  cju  12262  it0e0  12488  2mulicn  12489  2muline0  12490  cnref1o  13027  irec  14240  i2  14241  i3  14242  i4  14243  iexpcyc  14246  crreczi  14267  imre  15147  reim  15148  crre  15153  crim  15154  remim  15156  mulre  15160  cjreb  15162  recj  15163  reneg  15164  readd  15165  remullem  15167  imcj  15171  imneg  15172  imadd  15173  cjadd  15180  cjneg  15186  imval2  15190  rei  15195  imi  15196  cji  15198  cjreim  15199  cjreim2  15200  rennim  15278  cnpart  15279  sqrtneglem  15305  sqrtneg  15306  sqrtm1  15314  absi  15325  absreimsq  15331  absreim  15332  absimle  15348  abs1m  15374  sqreulem  15398  sqreu  15399  bhmafibid1  15504  caucvgr  15712  sinf  16160  cosf  16161  tanval2  16169  tanval3  16170  resinval  16171  recosval  16172  efi4p  16173  resin4p  16174  recos4p  16175  resincl  16176  recoscl  16177  sinneg  16182  cosneg  16183  efival  16188  efmival  16189  sinhval  16190  coshval  16191  retanhcl  16195  tanhlt1  16196  tanhbnd  16197  efeul  16198  sinadd  16200  cosadd  16201  ef01bndlem  16220  sin01bnd  16221  cos01bnd  16222  absef  16233  absefib  16234  efieq1re  16235  demoivre  16236  demoivreALT  16237  nthruc  16288  igz  16972  4sqlem17  16999  cnsubrg  21445  cnrehmeo  24984  cnrehmeoOLD  24985  cmodscexp  25154  ncvspi  25190  cphipval2  25275  4cphipval2  25276  cphipval  25277  itg0  25815  itgz  25816  itgcl  25819  ibl0  25822  iblcnlem1  25823  itgcnlem  25825  itgneg  25839  iblss  25840  iblss2  25841  itgss  25847  itgeqa  25849  iblconst  25853  itgconst  25854  itgadd  25860  iblabs  25864  iblabsr  25865  iblmulc2  25866  itgmulc2  25869  itgsplit  25871  dvsincos  26019  iaa  26367  sincn  26488  coscn  26489  efhalfpi  26513  ef2kpi  26520  efper  26521  sinperlem  26522  efimpi  26533  pige3ALT  26562  sineq0  26566  efeq1  26570  tanregt0  26581  efif1olem4  26587  efifo  26589  eff1olem  26590  circgrp  26594  circsubm  26595  logi  26629  logneg  26630  logm1  26631  lognegb  26632  eflogeq  26644  efiarg  26649  cosargd  26650  logimul  26656  logneg2  26657  abslogle  26660  tanarg  26661  logcn  26689  logf1o2  26692  cxpsqrtlem  26744  cxpsqrt  26745  root1eq1  26798  cxpeq  26800  ang180lem1  26852  ang180lem2  26853  ang180lem3  26854  ang180lem4  26855  1cubrlem  26884  1cubr  26885  asinlem  26911  asinlem2  26912  asinlem3a  26913  asinlem3  26914  asinf  26915  atandm2  26920  atandm3  26921  atanf  26923  asinneg  26929  efiasin  26931  sinasin  26932  asinsinlem  26934  asinsin  26935  asin1  26937  asinbnd  26942  cosasin  26947  atanneg  26950  atancj  26953  efiatan  26955  atanlogaddlem  26956  atanlogadd  26957  atanlogsublem  26958  atanlogsub  26959  efiatan2  26960  2efiatan  26961  tanatan  26962  cosatan  26964  atantan  26966  atanbndlem  26968  atans2  26974  dvatan  26978  atantayl  26980  atantayl2  26981  log2cnv  26987  basellem3  27126  2sqlem2  27462  nvpi  30686  ipval2  30726  4ipval2  30727  ipval3  30728  ipidsq  30729  dipcl  30731  dipcj  30733  dip0r  30736  dipcn  30739  ip1ilem  30845  ipasslem10  30858  ipasslem11  30859  polid2i  31176  polidi  31177  lnopeq0lem1  32024  lnopeq0i  32026  lnophmlem2  32036  re0cj  32753  ccfldextdgrr  33722  constrelextdg2  33788  cnre2csqima  33910  efmul2picn  34611  itgexpif  34621  vtscl  34653  vtsprod  34654  circlemeth  34655  iexpire  35735  itgaddnc  37687  iblabsnc  37691  iblmulc2nc  37692  itgmulc2nc  37695  ftc1anclem3  37702  ftc1anclem6  37705  ftc1anclem7  37706  ftc1anclem8  37707  ftc1anc  37708  dvasin  37711  areacirclem4  37718  cntotbnd  37803  sn-1ne2  42300  0tie0  42350  it1ei  42351  1tiei  42352  itrere  42353  retire  42354  ef11d  42375  cxp112d  42377  cxp111d  42378  cxpi11d  42379  re1m1e0m0  42427  sn-addlid  42434  sn-it0e0  42445  sn-negex12  42446  reixi  42452  sn-1ticom  42464  sn-mullid  42465  sn-it1ei  42466  ipiiie0  42467  sn-0tie0  42469  sn-mul02  42470  sn-inelr  42497  sn-itrere  42498  sn-retire  42499  cnreeu  42500  proot1ex  43208  sqrtcval  43654  sqrtcval2  43655  resqrtvalex  43658  imsqrtvalex  43659  sineq0ALT  44957  iblsplit  45981  sqrtnegnre  47319  requad01  47608  sinh-conventional  49258