Axiom ax-icn 11083

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

This axiom is referenced by:  0cn  11122  mulrid  11128  mul02lem2  11308  mul02  11309  addrid  11311  cnegex  11312  cnegex2  11313  0cnALT  11366  0cnALT2  11367  negicn  11379  ine0  11570  ixi  11764  recextlem1  11765  recextlem2  11766  recex  11767  rimul  12134  cru  12135  crne0  12136  cju  12139  it0e0  12362  2mulicn  12363  2muline0  12364  cnref1o  12896  irec  14122  i2  14123  i3  14124  i4  14125  iexpcyc  14128  crreczi  14149  imre  15029  reim  15030  crre  15035  crim  15036  remim  15038  mulre  15042  cjreb  15044  recj  15045  reneg  15046  readd  15047  remullem  15049  imcj  15053  imneg  15054  imadd  15055  cjadd  15062  cjneg  15068  imval2  15072  rei  15077  imi  15078  cji  15080  cjreim  15081  cjreim2  15082  rennim  15160  cnpart  15161  sqrtneglem  15187  sqrtneg  15188  sqrtm1  15196  absi  15207  absreimsq  15213  absreim  15214  absimle  15230  abs1m  15257  sqreulem  15281  sqreu  15282  bhmafibid1  15389  caucvgr  15597  sinf  16047  cosf  16048  tanval2  16056  tanval3  16057  resinval  16058  recosval  16059  efi4p  16060  resin4p  16061  recos4p  16062  resincl  16063  recoscl  16064  sinneg  16069  cosneg  16070  efival  16075  efmival  16076  sinhval  16077  coshval  16078  retanhcl  16082  tanhlt1  16083  tanhbnd  16084  efeul  16085  sinadd  16087  cosadd  16088  ef01bndlem  16107  sin01bnd  16108  cos01bnd  16109  absef  16120  absefib  16121  efieq1re  16122  demoivre  16123  demoivreALT  16124  nthruc  16175  igz  16860  4sqlem17  16887  cnsubrg  21380  cnrehmeo  24905  cnrehmeoOLD  24906  cmodscexp  25075  ncvspi  25110  cphipval2  25195  4cphipval2  25196  cphipval  25197  itg0  25735  itgz  25736  itgcl  25739  ibl0  25742  iblcnlem1  25743  itgcnlem  25745  itgneg  25759  iblss  25760  iblss2  25761  itgss  25767  itgeqa  25769  iblconst  25773  itgconst  25774  itgadd  25780  iblabs  25784  iblabsr  25785  iblmulc2  25786  itgmulc2  25789  itgsplit  25791  dvsincos  25939  iaa  26287  sincn  26408  coscn  26409  efhalfpi  26434  ef2kpi  26441  efper  26442  sinperlem  26443  efimpi  26454  pige3ALT  26483  sineq0  26487  efeq1  26491  tanregt0  26502  efif1olem4  26508  efifo  26510  eff1olem  26511  circgrp  26515  circsubm  26516  logi  26550  logneg  26551  logm1  26552  lognegb  26553  eflogeq  26565  efiarg  26570  cosargd  26571  logimul  26577  logneg2  26578  abslogle  26581  tanarg  26582  logcn  26610  logf1o2  26613  cxpsqrtlem  26665  cxpsqrt  26666  root1eq1  26719  cxpeq  26721  ang180lem1  26773  ang180lem2  26774  ang180lem3  26775  ang180lem4  26776  1cubrlem  26805  1cubr  26806  asinlem  26832  asinlem2  26833  asinlem3a  26834  asinlem3  26835  asinf  26836  atandm2  26841  atandm3  26842  atanf  26844  asinneg  26850  efiasin  26852  sinasin  26853  asinsinlem  26855  asinsin  26856  asin1  26858  asinbnd  26863  cosasin  26868  atanneg  26871  atancj  26874  efiatan  26876  atanlogaddlem  26877  atanlogadd  26878  atanlogsublem  26879  atanlogsub  26880  efiatan2  26881  2efiatan  26882  tanatan  26883  cosatan  26885  atantan  26887  atanbndlem  26889  atans2  26895  dvatan  26899  atantayl  26901  atantayl2  26902  log2cnv  26908  basellem3  27047  2sqlem2  27383  nvpi  30691  ipval2  30731  4ipval2  30732  ipval3  30733  ipidsq  30734  dipcl  30736  dipcj  30738  dip0r  30741  dipcn  30744  ip1ilem  30850  ipasslem10  30863  ipasslem11  30864  polid2i  31181  polidi  31182  lnopeq0lem1  32029  lnopeq0i  32031  lnophmlem2  32041  re0cj  32772  pythagreim  32774  ccfldextdgrr  33778  constrelextdg2  33853  iconstr  33872  constrrecl  33875  constrimcl  33876  constrmulcl  33877  constrresqrtcl  33883  cos9thpiminplylem3  33890  cos9thpiminplylem4  33891  cos9thpiminplylem5  33892  cos9thpiminply  33894  cos9thpinconstrlem1  33895  cos9thpinconstrlem2  33896  cos9thpinconstr  33897  cnre2csqima  34017  efmul2picn  34702  itgexpif  34712  vtscl  34744  vtsprod  34745  circlemeth  34746  iexpire  35878  itgaddnc  37820  iblabsnc  37824  iblmulc2nc  37825  itgmulc2nc  37828  ftc1anclem3  37835  ftc1anclem6  37838  ftc1anclem7  37839  ftc1anclem8  37840  ftc1anc  37841  dvasin  37844  areacirclem4  37851  cntotbnd  37936  sn-1ne2  42462  0tie0  42512  it1ei  42513  1tiei  42514  retire  42516  ef11d  42536  cxp112d  42538  cxp111d  42539  cxpi11d  42540  re1m1e0m0  42594  sn-addlid  42601  sn-it0e0  42613  sn-negex12  42614  reixi  42620  sn-1ticom  42632  sn-mullid  42633  sn-it1ei  42634  ipiiie0  42635  sn-0tie0  42648  sn-mul02  42649  sn-itrere  42685  sn-retire  42686  cnreeu  42687  proot1ex  43380  sqrtcval  43824  sqrtcval2  43825  resqrtvalex  43828  imsqrtvalex  43829  sineq0ALT  45119  iblsplit  46152  sqrtnegnre  47495  requad01  47809  sinh-conventional  49926