Axiom ax-icn 11164

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

This axiom is referenced by:  0cn  11201  mulrid  11207  mul02lem2  11386  mul02  11387  addrid  11389  cnegex  11390  cnegex2  11391  0cnALT  11443  0cnALT2  11444  negicn  11456  ine0  11644  ixi  11838  recextlem1  11839  recextlem2  11840  recex  11841  rimul  12198  cru  12199  crne0  12200  cju  12203  it0e0  12429  2mulicn  12430  2muline0  12431  cnref1o  12964  irec  14160  i2  14161  i3  14162  i4  14163  iexpcyc  14166  crreczi  14186  imre  15050  reim  15051  crre  15056  crim  15057  remim  15059  mulre  15063  cjreb  15065  recj  15066  reneg  15067  readd  15068  remullem  15070  imcj  15074  imneg  15075  imadd  15076  cjadd  15083  cjneg  15089  imval2  15093  rei  15098  imi  15099  cji  15101  cjreim  15102  cjreim2  15103  rennim  15181  cnpart  15182  sqrtneglem  15208  sqrtneg  15209  sqrtm1  15217  absi  15228  absreimsq  15234  absreim  15235  absimle  15251  abs1m  15277  sqreulem  15301  sqreu  15302  bhmafibid1  15407  caucvgr  15617  sinf  16062  cosf  16063  tanval2  16071  tanval3  16072  resinval  16073  recosval  16074  efi4p  16075  resin4p  16076  recos4p  16077  resincl  16078  recoscl  16079  sinneg  16084  cosneg  16085  efival  16090  efmival  16091  sinhval  16092  coshval  16093  retanhcl  16097  tanhlt1  16098  tanhbnd  16099  efeul  16100  sinadd  16102  cosadd  16103  ef01bndlem  16122  sin01bnd  16123  cos01bnd  16124  absef  16135  absefib  16136  efieq1re  16137  demoivre  16138  demoivreALT  16139  nthruc  16190  igz  16862  4sqlem17  16889  cnsubrg  20989  cnrehmeo  24450  cmodscexp  24618  ncvspi  24654  cphipval2  24739  4cphipval2  24740  cphipval  24741  itg0  25278  itgz  25279  itgcl  25282  ibl0  25285  iblcnlem1  25286  itgcnlem  25288  itgneg  25302  iblss  25303  iblss2  25304  itgss  25310  itgeqa  25312  iblconst  25316  itgconst  25317  itgadd  25323  iblabs  25327  iblabsr  25328  iblmulc2  25329  itgmulc2  25332  itgsplit  25334  dvsincos  25479  iaa  25819  sincn  25937  coscn  25938  efhalfpi  25962  ef2kpi  25969  efper  25970  sinperlem  25971  efimpi  25982  pige3ALT  26010  sineq0  26014  efeq1  26018  tanregt0  26029  efif1olem4  26035  efifo  26037  eff1olem  26038  circgrp  26042  circsubm  26043  logneg  26077  logm1  26078  lognegb  26079  eflogeq  26091  efiarg  26096  cosargd  26097  logimul  26103  logneg2  26104  abslogle  26107  tanarg  26108  logcn  26136  logf1o2  26139  cxpsqrtlem  26191  cxpsqrt  26192  root1eq1  26242  cxpeq  26244  ang180lem1  26293  ang180lem2  26294  ang180lem3  26295  ang180lem4  26296  1cubrlem  26325  1cubr  26326  asinlem  26352  asinlem2  26353  asinlem3a  26354  asinlem3  26355  asinf  26356  atandm2  26361  atandm3  26362  atanf  26364  asinneg  26370  efiasin  26372  sinasin  26373  asinsinlem  26375  asinsin  26376  asin1  26378  asinbnd  26383  cosasin  26388  atanneg  26391  atancj  26394  efiatan  26396  atanlogaddlem  26397  atanlogadd  26398  atanlogsublem  26399  atanlogsub  26400  efiatan2  26401  2efiatan  26402  tanatan  26403  cosatan  26405  atantan  26407  atanbndlem  26409  atans2  26415  dvatan  26419  atantayl  26421  atantayl2  26422  log2cnv  26428  basellem3  26566  2sqlem2  26900  nvpi  29897  ipval2  29937  4ipval2  29938  ipval3  29939  ipidsq  29940  dipcl  29942  dipcj  29944  dip0r  29947  dipcn  29950  ip1ilem  30056  ipasslem10  30069  ipasslem11  30070  polid2i  30387  polidi  30388  lnopeq0lem1  31235  lnopeq0i  31237  lnophmlem2  31247  ccfldextdgrr  32690  cnre2csqima  32828  efmul2picn  33545  itgexpif  33555  vtscl  33587  vtsprod  33588  circlemeth  33589  logi  34641  iexpire  34642  gg-cnrehmeo  35108  itgaddnc  36485  iblabsnc  36489  iblmulc2nc  36490  itgmulc2nc  36493  ftc1anclem3  36500  ftc1anclem6  36503  ftc1anclem7  36504  ftc1anclem8  36505  ftc1anc  36506  dvasin  36509  areacirclem4  36516  cntotbnd  36601  sn-1ne2  41128  re1m1e0m0  41213  sn-addlid  41220  sn-it0e0  41231  sn-negex12  41232  reixi  41238  sn-1ticom  41250  sn-mullid  41251  it1ei  41252  ipiiie0  41253  sn-0tie0  41255  sn-mul02  41256  sn-inelr  41281  itrere  41282  retire  41283  cnreeu  41284  proot1ex  41875  sqrtcval  42324  sqrtcval2  42325  resqrtvalex  42328  imsqrtvalex  42329  sineq0ALT  43630  iblsplit  44616  sqrtnegnre  45949  requad01  46223  sinh-conventional  47685