Axiom ax-icn 11169

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

This axiom is referenced by:  0cn  11206  mulrid  11212  mul02lem2  11391  mul02  11392  addrid  11394  cnegex  11395  cnegex2  11396  0cnALT  11448  0cnALT2  11449  negicn  11461  ine0  11649  ixi  11843  recextlem1  11844  recextlem2  11845  recex  11846  rimul  12203  cru  12204  crne0  12205  cju  12208  it0e0  12434  2mulicn  12435  2muline0  12436  cnref1o  12969  irec  14165  i2  14166  i3  14167  i4  14168  iexpcyc  14171  crreczi  14191  imre  15055  reim  15056  crre  15061  crim  15062  remim  15064  mulre  15068  cjreb  15070  recj  15071  reneg  15072  readd  15073  remullem  15075  imcj  15079  imneg  15080  imadd  15081  cjadd  15088  cjneg  15094  imval2  15098  rei  15103  imi  15104  cji  15106  cjreim  15107  cjreim2  15108  rennim  15186  cnpart  15187  sqrtneglem  15213  sqrtneg  15214  sqrtm1  15222  absi  15233  absreimsq  15239  absreim  15240  absimle  15256  abs1m  15282  sqreulem  15306  sqreu  15307  bhmafibid1  15412  caucvgr  15622  sinf  16067  cosf  16068  tanval2  16076  tanval3  16077  resinval  16078  recosval  16079  efi4p  16080  resin4p  16081  recos4p  16082  resincl  16083  recoscl  16084  sinneg  16089  cosneg  16090  efival  16095  efmival  16096  sinhval  16097  coshval  16098  retanhcl  16102  tanhlt1  16103  tanhbnd  16104  efeul  16105  sinadd  16107  cosadd  16108  ef01bndlem  16127  sin01bnd  16128  cos01bnd  16129  absef  16140  absefib  16141  efieq1re  16142  demoivre  16143  demoivreALT  16144  nthruc  16195  igz  16867  4sqlem17  16894  cnsubrg  21005  cnrehmeo  24469  cmodscexp  24637  ncvspi  24673  cphipval2  24758  4cphipval2  24759  cphipval  24760  itg0  25297  itgz  25298  itgcl  25301  ibl0  25304  iblcnlem1  25305  itgcnlem  25307  itgneg  25321  iblss  25322  iblss2  25323  itgss  25329  itgeqa  25331  iblconst  25335  itgconst  25336  itgadd  25342  iblabs  25346  iblabsr  25347  iblmulc2  25348  itgmulc2  25351  itgsplit  25353  dvsincos  25498  iaa  25838  sincn  25956  coscn  25957  efhalfpi  25981  ef2kpi  25988  efper  25989  sinperlem  25990  efimpi  26001  pige3ALT  26029  sineq0  26033  efeq1  26037  tanregt0  26048  efif1olem4  26054  efifo  26056  eff1olem  26057  circgrp  26061  circsubm  26062  logneg  26096  logm1  26097  lognegb  26098  eflogeq  26110  efiarg  26115  cosargd  26116  logimul  26122  logneg2  26123  abslogle  26126  tanarg  26127  logcn  26155  logf1o2  26158  cxpsqrtlem  26210  cxpsqrt  26211  root1eq1  26263  cxpeq  26265  ang180lem1  26314  ang180lem2  26315  ang180lem3  26316  ang180lem4  26317  1cubrlem  26346  1cubr  26347  asinlem  26373  asinlem2  26374  asinlem3a  26375  asinlem3  26376  asinf  26377  atandm2  26382  atandm3  26383  atanf  26385  asinneg  26391  efiasin  26393  sinasin  26394  asinsinlem  26396  asinsin  26397  asin1  26399  asinbnd  26404  cosasin  26409  atanneg  26412  atancj  26415  efiatan  26417  atanlogaddlem  26418  atanlogadd  26419  atanlogsublem  26420  atanlogsub  26421  efiatan2  26422  2efiatan  26423  tanatan  26424  cosatan  26426  atantan  26428  atanbndlem  26430  atans2  26436  dvatan  26440  atantayl  26442  atantayl2  26443  log2cnv  26449  basellem3  26587  2sqlem2  26921  nvpi  29920  ipval2  29960  4ipval2  29961  ipval3  29962  ipidsq  29963  dipcl  29965  dipcj  29967  dip0r  29970  dipcn  29973  ip1ilem  30079  ipasslem10  30092  ipasslem11  30093  polid2i  30410  polidi  30411  lnopeq0lem1  31258  lnopeq0i  31260  lnophmlem2  31270  ccfldextdgrr  32746  cnre2csqima  32891  efmul2picn  33608  itgexpif  33618  vtscl  33650  vtsprod  33651  circlemeth  33652  logi  34704  iexpire  34705  gg-cnrehmeo  35171  itgaddnc  36548  iblabsnc  36552  iblmulc2nc  36553  itgmulc2nc  36556  ftc1anclem3  36563  ftc1anclem6  36566  ftc1anclem7  36567  ftc1anclem8  36568  ftc1anc  36569  dvasin  36572  areacirclem4  36579  cntotbnd  36664  sn-1ne2  41179  re1m1e0m0  41270  sn-addlid  41277  sn-it0e0  41288  sn-negex12  41289  reixi  41295  sn-1ticom  41307  sn-mullid  41308  it1ei  41309  ipiiie0  41310  sn-0tie0  41312  sn-mul02  41313  sn-inelr  41338  itrere  41339  retire  41340  cnreeu  41341  proot1ex  41943  sqrtcval  42392  sqrtcval2  42393  resqrtvalex  42396  imsqrtvalex  42397  sineq0ALT  43698  iblsplit  44682  sqrtnegnre  46015  requad01  46289  sinh-conventional  47784