Axiom ax-icn 10836

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

This axiom is referenced by:  0cn  10873  mulid1  10879  mul02lem2  11057  mul02  11058  addid1  11060  cnegex  11061  cnegex2  11062  0cnALT  11114  0cnALT2  11115  negicn  11127  ine0  11315  ixi  11509  recextlem1  11510  recextlem2  11511  recex  11512  rimul  11869  cru  11870  crne0  11871  cju  11874  it0e0  12100  2mulicn  12101  2muline0  12102  cnref1o  12629  irec  13821  i2  13822  i3  13823  i4  13824  iexpcyc  13826  crreczi  13846  imre  14722  reim  14723  crre  14728  crim  14729  remim  14731  mulre  14735  cjreb  14737  recj  14738  reneg  14739  readd  14740  remullem  14742  imcj  14746  imneg  14747  imadd  14748  cjadd  14755  cjneg  14761  imval2  14765  rei  14770  imi  14771  cji  14773  cjreim  14774  cjreim2  14775  rennim  14853  cnpart  14854  sqrtneglem  14881  sqrtneg  14882  sqrtm1  14890  absi  14901  absreimsq  14907  absreim  14908  absimle  14924  abs1m  14950  sqreulem  14974  sqreu  14975  bhmafibid1  15080  caucvgr  15290  sinf  15736  cosf  15737  tanval2  15745  tanval3  15746  resinval  15747  recosval  15748  efi4p  15749  resin4p  15750  recos4p  15751  resincl  15752  recoscl  15753  sinneg  15758  cosneg  15759  efival  15764  efmival  15765  sinhval  15766  coshval  15767  retanhcl  15771  tanhlt1  15772  tanhbnd  15773  efeul  15774  sinadd  15776  cosadd  15777  ef01bndlem  15796  sin01bnd  15797  cos01bnd  15798  absef  15809  absefib  15810  efieq1re  15811  demoivre  15812  demoivreALT  15813  nthruc  15864  igz  16538  4sqlem17  16565  cnsubrg  20545  cnrehmeo  23997  cmodscexp  24165  ncvspi  24200  cphipval2  24285  4cphipval2  24286  cphipval  24287  itg0  24824  itgz  24825  itgcl  24828  ibl0  24831  iblcnlem1  24832  itgcnlem  24834  itgneg  24848  iblss  24849  iblss2  24850  itgss  24856  itgeqa  24858  iblconst  24862  itgconst  24863  itgadd  24869  iblabs  24873  iblabsr  24874  iblmulc2  24875  itgmulc2  24878  itgsplit  24880  dvsincos  25025  iaa  25365  sincn  25483  coscn  25484  efhalfpi  25508  ef2kpi  25515  efper  25516  sinperlem  25517  efimpi  25528  pige3ALT  25556  sineq0  25560  efeq1  25564  tanregt0  25575  efif1olem4  25581  efifo  25583  eff1olem  25584  circgrp  25588  circsubm  25589  logneg  25623  logm1  25624  lognegb  25625  eflogeq  25637  efiarg  25642  cosargd  25643  logimul  25649  logneg2  25650  abslogle  25653  tanarg  25654  logcn  25682  logf1o2  25685  cxpsqrtlem  25737  cxpsqrt  25738  root1eq1  25788  cxpeq  25790  ang180lem1  25839  ang180lem2  25840  ang180lem3  25841  ang180lem4  25842  1cubrlem  25871  1cubr  25872  asinlem  25898  asinlem2  25899  asinlem3a  25900  asinlem3  25901  asinf  25902  atandm2  25907  atandm3  25908  atanf  25910  asinneg  25916  efiasin  25918  sinasin  25919  asinsinlem  25921  asinsin  25922  asin1  25924  asinbnd  25929  cosasin  25934  atanneg  25937  atancj  25940  efiatan  25942  atanlogaddlem  25943  atanlogadd  25944  atanlogsublem  25945  atanlogsub  25946  efiatan2  25947  2efiatan  25948  tanatan  25949  cosatan  25951  atantan  25953  atanbndlem  25955  atans2  25961  dvatan  25965  atantayl  25967  atantayl2  25968  log2cnv  25974  basellem3  26112  2sqlem2  26446  nvpi  28905  ipval2  28945  4ipval2  28946  ipval3  28947  ipidsq  28948  dipcl  28950  dipcj  28952  dip0r  28955  dipcn  28958  ip1ilem  29064  ipasslem10  29077  ipasslem11  29078  polid2i  29395  polidi  29396  lnopeq0lem1  30243  lnopeq0i  30245  lnophmlem2  30255  ccfldextdgrr  31619  cnre2csqima  31738  efmul2picn  32451  itgexpif  32461  vtscl  32493  vtsprod  32494  circlemeth  32495  logi  33581  iexpire  33582  itgaddnc  35743  iblabsnc  35747  iblmulc2nc  35748  itgmulc2nc  35751  ftc1anclem3  35758  ftc1anclem6  35761  ftc1anclem7  35762  ftc1anclem8  35763  ftc1anc  35764  dvasin  35767  areacirclem4  35774  cntotbnd  35860  sn-1ne2  40188  re1m1e0m0  40273  sn-addid2  40280  sn-it0e0  40290  sn-negex12  40291  reixi  40297  sn-1ticom  40309  sn-mulid2  40310  it1ei  40311  ipiiie0  40312  sn-0tie0  40314  sn-mul02  40315  sn-inelr  40328  itrere  40329  retire  40330  cnreeu  40331  proot1ex  40914  sqrtcval  41110  sqrtcval2  41111  resqrtvalex  41114  imsqrtvalex  41115  sineq0ALT  42419  iblsplit  43370  sqrtnegnre  44660  requad01  44934  sinh-conventional  46300