Axiom ax-icn 11086

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

This axiom is referenced by:  0cn  11125  mulrid  11131  mul02lem2  11312  mul02  11313  addrid  11315  cnegex  11316  cnegex2  11317  0cnALT  11370  0cnALT2  11371  negicn  11383  ine0  11574  ixi  11768  recextlem1  11769  recextlem2  11770  recex  11771  rimul  12139  cru  12140  crne0  12141  cju  12144  it0e0  12389  2mulicn  12390  2muline0  12391  cnref1o  12924  irec  14152  i2  14153  i3  14154  i4  14155  iexpcyc  14158  crreczi  14179  imre  15059  reim  15060  crre  15065  crim  15066  remim  15068  mulre  15072  cjreb  15074  recj  15075  reneg  15076  readd  15077  remullem  15079  imcj  15083  imneg  15084  imadd  15085  cjadd  15092  cjneg  15098  imval2  15102  rei  15107  imi  15108  cji  15110  cjreim  15111  cjreim2  15112  rennim  15190  cnpart  15191  sqrtneglem  15217  sqrtneg  15218  sqrtm1  15226  absi  15237  absreimsq  15243  absreim  15244  absimle  15260  abs1m  15287  sqreulem  15311  sqreu  15312  bhmafibid1  15419  caucvgr  15627  sinf  16080  cosf  16081  tanval2  16089  tanval3  16090  resinval  16091  recosval  16092  efi4p  16093  resin4p  16094  recos4p  16095  resincl  16096  recoscl  16097  sinneg  16102  cosneg  16103  efival  16108  efmival  16109  sinhval  16110  coshval  16111  retanhcl  16115  tanhlt1  16116  tanhbnd  16117  efeul  16118  sinadd  16120  cosadd  16121  ef01bndlem  16140  sin01bnd  16141  cos01bnd  16142  absef  16153  absefib  16154  efieq1re  16155  demoivre  16156  demoivreALT  16157  nthruc  16208  igz  16894  4sqlem17  16921  cnsubrg  21396  cnrehmeo  24908  cmodscexp  25076  ncvspi  25111  cphipval2  25196  4cphipval2  25197  cphipval  25198  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  25936  iaa  26279  sincn  26397  coscn  26398  efhalfpi  26423  ef2kpi  26430  efper  26431  sinperlem  26432  efimpi  26443  pige3ALT  26472  sineq0  26476  efeq1  26480  tanregt0  26491  efif1olem4  26497  efifo  26499  eff1olem  26500  circgrp  26504  circsubm  26505  logi  26539  logneg  26540  logm1  26541  lognegb  26542  eflogeq  26554  efiarg  26559  cosargd  26560  logimul  26566  logneg2  26567  abslogle  26570  tanarg  26571  logcn  26599  logf1o2  26602  cxpsqrtlem  26654  cxpsqrt  26655  root1eq1  26707  cxpeq  26709  ang180lem1  26761  ang180lem2  26762  ang180lem3  26763  ang180lem4  26764  1cubrlem  26793  1cubr  26794  asinlem  26820  asinlem2  26821  asinlem3a  26822  asinlem3  26823  asinf  26824  atandm2  26829  atandm3  26830  atanf  26832  asinneg  26838  efiasin  26840  sinasin  26841  asinsinlem  26843  asinsin  26844  asin1  26846  asinbnd  26851  cosasin  26856  atanneg  26859  atancj  26862  efiatan  26864  atanlogaddlem  26865  atanlogadd  26866  atanlogsublem  26867  atanlogsub  26868  efiatan2  26869  2efiatan  26870  tanatan  26871  cosatan  26873  atantan  26875  atanbndlem  26877  atans2  26883  dvatan  26887  atantayl  26889  atantayl2  26890  log2cnv  26896  basellem3  27034  2sqlem2  27369  nvpi  30726  ipval2  30766  4ipval2  30767  ipval3  30768  ipidsq  30769  dipcl  30771  dipcj  30773  dip0r  30776  dipcn  30779  ip1ilem  30885  ipasslem10  30898  ipasslem11  30899  polid2i  31216  polidi  31217  lnopeq0lem1  32064  lnopeq0i  32066  lnophmlem2  32076  re0cj  32804  pythagreim  32806  ccfldextdgrr  33804  constrelextdg2  33879  iconstr  33898  constrrecl  33901  constrimcl  33902  constrmulcl  33903  constrresqrtcl  33909  cos9thpiminplylem3  33916  cos9thpiminplylem4  33917  cos9thpiminplylem5  33918  cos9thpiminply  33920  cos9thpinconstrlem1  33921  cos9thpinconstrlem2  33922  cos9thpinconstr  33923  cnre2csqima  34043  efmul2picn  34728  itgexpif  34738  vtscl  34770  vtsprod  34771  circlemeth  34772  iexpire  35905  itgaddnc  37989  iblabsnc  37993  iblmulc2nc  37994  itgmulc2nc  37997  ftc1anclem3  38004  ftc1anclem6  38007  ftc1anclem7  38008  ftc1anclem8  38009  ftc1anc  38010  dvasin  38013  areacirclem4  38020  cntotbnd  38105  sn-1ne2  42691  0tie0  42735  it1ei  42736  1tiei  42737  retire  42739  ef11d  42759  cxp112d  42761  cxp111d  42762  cxpi11d  42763  re1m1e0m0  42817  sn-addlid  42824  sn-it0e0  42836  sn-negex12  42837  reixi  42843  sn-1ticom  42855  sn-mullid  42856  sn-it1ei  42857  ipiiie0  42858  sn-0tie0  42884  sn-mul02  42885  sn-itrere  42921  sn-retire  42922  cnreeu  42923  proot1ex  43612  sqrtcval  44056  sqrtcval2  44057  resqrtvalex  44060  imsqrtvalex  44061  sineq0ALT  45351  iblsplit  46382  sqrtnegnre  47743  requad01  48085  sinh-conventional  50202