Axiom ax-icn 11099

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

This axiom is referenced by:  0cn  11138  mulrid  11144  mul02lem2  11324  mul02  11325  addrid  11327  cnegex  11328  cnegex2  11329  0cnALT  11382  0cnALT2  11383  negicn  11395  ine0  11586  ixi  11780  recextlem1  11781  recextlem2  11782  recex  11783  rimul  12150  cru  12151  crne0  12152  cju  12155  it0e0  12378  2mulicn  12379  2muline0  12380  cnref1o  12912  irec  14138  i2  14139  i3  14140  i4  14141  iexpcyc  14144  crreczi  14165  imre  15045  reim  15046  crre  15051  crim  15052  remim  15054  mulre  15058  cjreb  15060  recj  15061  reneg  15062  readd  15063  remullem  15065  imcj  15069  imneg  15070  imadd  15071  cjadd  15078  cjneg  15084  imval2  15088  rei  15093  imi  15094  cji  15096  cjreim  15097  cjreim2  15098  rennim  15176  cnpart  15177  sqrtneglem  15203  sqrtneg  15204  sqrtm1  15212  absi  15223  absreimsq  15229  absreim  15230  absimle  15246  abs1m  15273  sqreulem  15297  sqreu  15298  bhmafibid1  15405  caucvgr  15613  sinf  16063  cosf  16064  tanval2  16072  tanval3  16073  resinval  16074  recosval  16075  efi4p  16076  resin4p  16077  recos4p  16078  resincl  16079  recoscl  16080  sinneg  16085  cosneg  16086  efival  16091  efmival  16092  sinhval  16093  coshval  16094  retanhcl  16098  tanhlt1  16099  tanhbnd  16100  efeul  16101  sinadd  16103  cosadd  16104  ef01bndlem  16123  sin01bnd  16124  cos01bnd  16125  absef  16136  absefib  16137  efieq1re  16138  demoivre  16139  demoivreALT  16140  nthruc  16191  igz  16876  4sqlem17  16903  cnsubrg  21399  cnrehmeo  24924  cnrehmeoOLD  24925  cmodscexp  25094  ncvspi  25129  cphipval2  25214  4cphipval2  25215  cphipval  25216  itg0  25754  itgz  25755  itgcl  25758  ibl0  25761  iblcnlem1  25762  itgcnlem  25764  itgneg  25778  iblss  25779  iblss2  25780  itgss  25786  itgeqa  25788  iblconst  25792  itgconst  25793  itgadd  25799  iblabs  25803  iblabsr  25804  iblmulc2  25805  itgmulc2  25808  itgsplit  25810  dvsincos  25958  iaa  26306  sincn  26427  coscn  26428  efhalfpi  26453  ef2kpi  26460  efper  26461  sinperlem  26462  efimpi  26473  pige3ALT  26502  sineq0  26506  efeq1  26510  tanregt0  26521  efif1olem4  26527  efifo  26529  eff1olem  26530  circgrp  26534  circsubm  26535  logi  26569  logneg  26570  logm1  26571  lognegb  26572  eflogeq  26584  efiarg  26589  cosargd  26590  logimul  26596  logneg2  26597  abslogle  26600  tanarg  26601  logcn  26629  logf1o2  26632  cxpsqrtlem  26684  cxpsqrt  26685  root1eq1  26738  cxpeq  26740  ang180lem1  26792  ang180lem2  26793  ang180lem3  26794  ang180lem4  26795  1cubrlem  26824  1cubr  26825  asinlem  26851  asinlem2  26852  asinlem3a  26853  asinlem3  26854  asinf  26855  atandm2  26860  atandm3  26861  atanf  26863  asinneg  26869  efiasin  26871  sinasin  26872  asinsinlem  26874  asinsin  26875  asin1  26877  asinbnd  26882  cosasin  26887  atanneg  26890  atancj  26893  efiatan  26895  atanlogaddlem  26896  atanlogadd  26897  atanlogsublem  26898  atanlogsub  26899  efiatan2  26900  2efiatan  26901  tanatan  26902  cosatan  26904  atantan  26906  atanbndlem  26908  atans2  26914  dvatan  26918  atantayl  26920  atantayl2  26921  log2cnv  26927  basellem3  27066  2sqlem2  27402  nvpi  30761  ipval2  30801  4ipval2  30802  ipval3  30803  ipidsq  30804  dipcl  30806  dipcj  30808  dip0r  30811  dipcn  30814  ip1ilem  30920  ipasslem10  30933  ipasslem11  30934  polid2i  31251  polidi  31252  lnopeq0lem1  32099  lnopeq0i  32101  lnophmlem2  32111  re0cj  32840  pythagreim  32842  ccfldextdgrr  33856  constrelextdg2  33931  iconstr  33950  constrrecl  33953  constrimcl  33954  constrmulcl  33955  constrresqrtcl  33961  cos9thpiminplylem3  33968  cos9thpiminplylem4  33969  cos9thpiminplylem5  33970  cos9thpiminply  33972  cos9thpinconstrlem1  33973  cos9thpinconstrlem2  33974  cos9thpinconstr  33975  cnre2csqima  34095  efmul2picn  34780  itgexpif  34790  vtscl  34822  vtsprod  34823  circlemeth  34824  iexpire  35957  itgaddnc  37960  iblabsnc  37964  iblmulc2nc  37965  itgmulc2nc  37968  ftc1anclem3  37975  ftc1anclem6  37978  ftc1anclem7  37979  ftc1anclem8  37980  ftc1anc  37981  dvasin  37984  areacirclem4  37991  cntotbnd  38076  sn-1ne2  42664  0tie0  42714  it1ei  42715  1tiei  42716  retire  42718  ef11d  42738  cxp112d  42740  cxp111d  42741  cxpi11d  42742  re1m1e0m0  42796  sn-addlid  42803  sn-it0e0  42815  sn-negex12  42816  reixi  42822  sn-1ticom  42834  sn-mullid  42835  sn-it1ei  42836  ipiiie0  42837  sn-0tie0  42850  sn-mul02  42851  sn-itrere  42887  sn-retire  42888  cnreeu  42889  proot1ex  43582  sqrtcval  44026  sqrtcval2  44027  resqrtvalex  44030  imsqrtvalex  44031  sineq0ALT  45321  iblsplit  46353  sqrtnegnre  47696  requad01  48010  sinh-conventional  50127