Axiom ax-icn 11166

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

This axiom is referenced by:  0cn  11203  mulrid  11209  mul02lem2  11388  mul02  11389  addrid  11391  cnegex  11392  cnegex2  11393  0cnALT  11445  0cnALT2  11446  negicn  11458  ine0  11646  ixi  11840  recextlem1  11841  recextlem2  11842  recex  11843  rimul  12200  cru  12201  crne0  12202  cju  12205  it0e0  12431  2mulicn  12432  2muline0  12433  cnref1o  12966  irec  14162  i2  14163  i3  14164  i4  14165  iexpcyc  14168  crreczi  14188  imre  15052  reim  15053  crre  15058  crim  15059  remim  15061  mulre  15065  cjreb  15067  recj  15068  reneg  15069  readd  15070  remullem  15072  imcj  15076  imneg  15077  imadd  15078  cjadd  15085  cjneg  15091  imval2  15095  rei  15100  imi  15101  cji  15103  cjreim  15104  cjreim2  15105  rennim  15183  cnpart  15184  sqrtneglem  15210  sqrtneg  15211  sqrtm1  15219  absi  15230  absreimsq  15236  absreim  15237  absimle  15253  abs1m  15279  sqreulem  15303  sqreu  15304  bhmafibid1  15409  caucvgr  15619  sinf  16064  cosf  16065  tanval2  16073  tanval3  16074  resinval  16075  recosval  16076  efi4p  16077  resin4p  16078  recos4p  16079  resincl  16080  recoscl  16081  sinneg  16086  cosneg  16087  efival  16092  efmival  16093  sinhval  16094  coshval  16095  retanhcl  16099  tanhlt1  16100  tanhbnd  16101  efeul  16102  sinadd  16104  cosadd  16105  ef01bndlem  16124  sin01bnd  16125  cos01bnd  16126  absef  16137  absefib  16138  efieq1re  16139  demoivre  16140  demoivreALT  16141  nthruc  16192  igz  16864  4sqlem17  16891  cnsubrg  20998  cnrehmeo  24461  cmodscexp  24629  ncvspi  24665  cphipval2  24750  4cphipval2  24751  cphipval  24752  itg0  25289  itgz  25290  itgcl  25293  ibl0  25296  iblcnlem1  25297  itgcnlem  25299  itgneg  25313  iblss  25314  iblss2  25315  itgss  25321  itgeqa  25323  iblconst  25327  itgconst  25328  itgadd  25334  iblabs  25338  iblabsr  25339  iblmulc2  25340  itgmulc2  25343  itgsplit  25345  dvsincos  25490  iaa  25830  sincn  25948  coscn  25949  efhalfpi  25973  ef2kpi  25980  efper  25981  sinperlem  25982  efimpi  25993  pige3ALT  26021  sineq0  26025  efeq1  26029  tanregt0  26040  efif1olem4  26046  efifo  26048  eff1olem  26049  circgrp  26053  circsubm  26054  logneg  26088  logm1  26089  lognegb  26090  eflogeq  26102  efiarg  26107  cosargd  26108  logimul  26114  logneg2  26115  abslogle  26118  tanarg  26119  logcn  26147  logf1o2  26150  cxpsqrtlem  26202  cxpsqrt  26203  root1eq1  26253  cxpeq  26255  ang180lem1  26304  ang180lem2  26305  ang180lem3  26306  ang180lem4  26307  1cubrlem  26336  1cubr  26337  asinlem  26363  asinlem2  26364  asinlem3a  26365  asinlem3  26366  asinf  26367  atandm2  26372  atandm3  26373  atanf  26375  asinneg  26381  efiasin  26383  sinasin  26384  asinsinlem  26386  asinsin  26387  asin1  26389  asinbnd  26394  cosasin  26399  atanneg  26402  atancj  26405  efiatan  26407  atanlogaddlem  26408  atanlogadd  26409  atanlogsublem  26410  atanlogsub  26411  efiatan2  26412  2efiatan  26413  tanatan  26414  cosatan  26416  atantan  26418  atanbndlem  26420  atans2  26426  dvatan  26430  atantayl  26432  atantayl2  26433  log2cnv  26439  basellem3  26577  2sqlem2  26911  nvpi  29908  ipval2  29948  4ipval2  29949  ipval3  29950  ipidsq  29951  dipcl  29953  dipcj  29955  dip0r  29958  dipcn  29961  ip1ilem  30067  ipasslem10  30080  ipasslem11  30081  polid2i  30398  polidi  30399  lnopeq0lem1  31246  lnopeq0i  31248  lnophmlem2  31258  ccfldextdgrr  32735  cnre2csqima  32880  efmul2picn  33597  itgexpif  33607  vtscl  33639  vtsprod  33640  circlemeth  33641  logi  34693  iexpire  34694  gg-cnrehmeo  35160  itgaddnc  36537  iblabsnc  36541  iblmulc2nc  36542  itgmulc2nc  36545  ftc1anclem3  36552  ftc1anclem6  36555  ftc1anclem7  36556  ftc1anclem8  36557  ftc1anc  36558  dvasin  36561  areacirclem4  36568  cntotbnd  36653  sn-1ne2  41177  re1m1e0m0  41267  sn-addlid  41274  sn-it0e0  41285  sn-negex12  41286  reixi  41292  sn-1ticom  41304  sn-mullid  41305  it1ei  41306  ipiiie0  41307  sn-0tie0  41309  sn-mul02  41310  sn-inelr  41335  itrere  41336  retire  41337  cnreeu  41338  proot1ex  41929  sqrtcval  42378  sqrtcval2  42379  resqrtvalex  42382  imsqrtvalex  42383  sineq0ALT  43684  iblsplit  44669  sqrtnegnre  46002  requad01  46276  sinh-conventional  47738