Axiom ax-icn 9851

Description: i is a complex number. Axiom 3 of 22 for real and complex numbers, justified by theorem axicn 9827. (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 9794	. 2 class i
2		cc 9790	. 2 class ℂ
3	1, 2	wcel 1976	1 wff i ∈ ℂ

This axiom is referenced by:  0cn  9888  mulid1  9893  mul02lem2  10064  mul02  10065  addid1  10067  cnegex  10068  cnegex2  10069  0cnALT  10121  negicn  10133  ine0  10316  ixi  10507  recextlem1  10508  recextlem2  10509  recex  10510  rimul  10860  cru  10861  crne0  10862  cju  10865  it0e0  11103  2mulicn  11104  2muline0  11105  cnref1o  11661  irec  12783  i2  12784  i3  12785  i4  12786  iexpcyc  12788  crreczi  12808  imre  13644  reim  13645  crre  13650  crim  13651  remim  13653  mulre  13657  cjreb  13659  recj  13660  reneg  13661  readd  13662  remullem  13664  imcj  13668  imneg  13669  imadd  13670  cjadd  13677  cjneg  13683  imval2  13687  rei  13692  imi  13693  cji  13695  cjreim  13696  cjreim2  13697  rennim  13775  cnpart  13776  sqrtneglem  13803  sqrtneg  13804  sqrtm1  13812  absi  13822  absreimsq  13828  absreim  13829  absimle  13845  abs1m  13871  sqreulem  13895  sqreu  13896  caucvgr  14202  sinf  14641  cosf  14642  tanval2  14650  tanval3  14651  resinval  14652  recosval  14653  efi4p  14654  resin4p  14655  recos4p  14656  resincl  14657  recoscl  14658  sinneg  14663  cosneg  14664  efival  14669  efmival  14670  sinhval  14671  coshval  14672  retanhcl  14676  tanhlt1  14677  tanhbnd  14678  efeul  14679  sinadd  14681  cosadd  14682  ef01bndlem  14701  sin01bnd  14702  cos01bnd  14703  absef  14714  absefib  14715  efieq1re  14716  demoivre  14717  demoivreALT  14718  nthruc  14767  igz  15424  4sqlem17  15451  cnsubrg  19573  cnrehmeo  22507  cmodscexp  22676  ncvspi  22708  cphipval2  22792  4cphipval2  22793  cphipval  22794  itg0  23296  itgz  23297  itgcl  23300  ibl0  23303  iblcnlem1  23304  itgcnlem  23306  itgneg  23320  iblss  23321  iblss2  23322  itgss  23328  itgeqa  23330  iblconst  23334  itgconst  23335  itgadd  23341  iblabs  23345  iblabsr  23346  iblmulc2  23347  itgmulc2  23350  itgsplit  23352  dvsincos  23492  iaa  23828  sincn  23946  coscn  23947  efhalfpi  23971  ef2kpi  23978  efper  23979  sinperlem  23980  efimpi  23991  pige3  24017  sineq0  24021  efeq1  24023  tanregt0  24033  efif1olem4  24039  efifo  24041  eff1olem  24042  circgrp  24046  circsubm  24047  logneg  24082  logm1  24083  lognegb  24084  eflogeq  24096  efiarg  24101  cosargd  24102  logimul  24108  logneg2  24109  abslogle  24112  tanarg  24113  logcn  24137  logf1o2  24140  cxpsqrtlem  24192  cxpsqrt  24193  root1eq1  24240  cxpeq  24242  ang180lem1  24283  ang180lem2  24284  ang180lem3  24285  ang180lem4  24286  1cubrlem  24312  1cubr  24313  asinlem  24339  asinlem2  24340  asinlem3a  24341  asinlem3  24342  asinf  24343  atandm2  24348  atandm3  24349  atanf  24351  asinneg  24357  efiasin  24359  sinasin  24360  asinsinlem  24362  asinsin  24363  asin1  24365  asinbnd  24370  cosasin  24375  atanneg  24378  atancj  24381  efiatan  24383  atanlogaddlem  24384  atanlogadd  24385  atanlogsublem  24386  atanlogsub  24387  efiatan2  24388  2efiatan  24389  tanatan  24390  cosatan  24392  atantan  24394  atanbndlem  24396  atans2  24402  dvatan  24406  atantayl  24408  atantayl2  24409  log2cnv  24415  basellem3  24553  2sqlem2  24887  nvpi  26699  ipval2  26739  4ipval2  26740  ipval3  26741  ipidsq  26742  dipcl  26744  dipcj  26746  dip0r  26749  dipcn  26752  ip1ilem  26858  ipasslem10  26871  ipasslem11  26872  polid2i  27191  polidi  27192  lnopeq0lem1  28041  lnopeq0i  28043  lnophmlem2  28053  bhmafibid1  28768  cnre2csqima  29078  logi  30666  iexpire  30667  itgaddnc  32423  iblabsnc  32427  iblmulc2nc  32428  itgmulc2nc  32431  ftc1anclem3  32440  ftc1anclem6  32443  ftc1anclem7  32444  ftc1anclem8  32445  ftc1anc  32446  dvasin  32449  areacirclem4  32456  cntotbnd  32548  proot1ex  36581  sineq0ALT  37978  iblsplit  38641  sinh-conventional  42221