Axiom ax-icn 10634

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

This axiom is referenced by:  0cn  10671  mulid1  10677  mul02lem2  10855  mul02  10856  addid1  10858  cnegex  10859  cnegex2  10860  0cnALT  10912  0cnALT2  10913  negicn  10925  ine0  11113  ixi  11307  recextlem1  11308  recextlem2  11309  recex  11310  rimul  11665  cru  11666  crne0  11667  cju  11670  it0e0  11896  2mulicn  11897  2muline0  11898  cnref1o  12425  irec  13614  i2  13615  i3  13616  i4  13617  iexpcyc  13619  crreczi  13639  imre  14515  reim  14516  crre  14521  crim  14522  remim  14524  mulre  14528  cjreb  14530  recj  14531  reneg  14532  readd  14533  remullem  14535  imcj  14539  imneg  14540  imadd  14541  cjadd  14548  cjneg  14554  imval2  14558  rei  14563  imi  14564  cji  14566  cjreim  14567  cjreim2  14568  rennim  14646  cnpart  14647  sqrtneglem  14674  sqrtneg  14675  sqrtm1  14683  absi  14694  absreimsq  14700  absreim  14701  absimle  14717  abs1m  14743  sqreulem  14767  sqreu  14768  bhmafibid1  14873  caucvgr  15080  sinf  15525  cosf  15526  tanval2  15534  tanval3  15535  resinval  15536  recosval  15537  efi4p  15538  resin4p  15539  recos4p  15540  resincl  15541  recoscl  15542  sinneg  15547  cosneg  15548  efival  15553  efmival  15554  sinhval  15555  coshval  15556  retanhcl  15560  tanhlt1  15561  tanhbnd  15562  efeul  15563  sinadd  15565  cosadd  15566  ef01bndlem  15585  sin01bnd  15586  cos01bnd  15587  absef  15598  absefib  15599  efieq1re  15600  demoivre  15601  demoivreALT  15602  nthruc  15653  igz  16325  4sqlem17  16352  cnsubrg  20226  cnrehmeo  23654  cmodscexp  23822  ncvspi  23857  cphipval2  23941  4cphipval2  23942  cphipval  23943  itg0  24479  itgz  24480  itgcl  24483  ibl0  24486  iblcnlem1  24487  itgcnlem  24489  itgneg  24503  iblss  24504  iblss2  24505  itgss  24511  itgeqa  24513  iblconst  24517  itgconst  24518  itgadd  24524  iblabs  24528  iblabsr  24529  iblmulc2  24530  itgmulc2  24533  itgsplit  24535  dvsincos  24680  iaa  25020  sincn  25138  coscn  25139  efhalfpi  25163  ef2kpi  25170  efper  25171  sinperlem  25172  efimpi  25183  pige3ALT  25211  sineq0  25215  efeq1  25219  tanregt0  25230  efif1olem4  25236  efifo  25238  eff1olem  25239  circgrp  25243  circsubm  25244  logneg  25278  logm1  25279  lognegb  25280  eflogeq  25292  efiarg  25297  cosargd  25298  logimul  25304  logneg2  25305  abslogle  25308  tanarg  25309  logcn  25337  logf1o2  25340  cxpsqrtlem  25392  cxpsqrt  25393  root1eq1  25443  cxpeq  25445  ang180lem1  25494  ang180lem2  25495  ang180lem3  25496  ang180lem4  25497  1cubrlem  25526  1cubr  25527  asinlem  25553  asinlem2  25554  asinlem3a  25555  asinlem3  25556  asinf  25557  atandm2  25562  atandm3  25563  atanf  25565  asinneg  25571  efiasin  25573  sinasin  25574  asinsinlem  25576  asinsin  25577  asin1  25579  asinbnd  25584  cosasin  25589  atanneg  25592  atancj  25595  efiatan  25597  atanlogaddlem  25598  atanlogadd  25599  atanlogsublem  25600  atanlogsub  25601  efiatan2  25602  2efiatan  25603  tanatan  25604  cosatan  25606  atantan  25608  atanbndlem  25610  atans2  25616  dvatan  25620  atantayl  25622  atantayl2  25623  log2cnv  25629  basellem3  25767  2sqlem2  26101  nvpi  28549  ipval2  28589  4ipval2  28590  ipval3  28591  ipidsq  28592  dipcl  28594  dipcj  28596  dip0r  28599  dipcn  28602  ip1ilem  28708  ipasslem10  28721  ipasslem11  28722  polid2i  29039  polidi  29040  lnopeq0lem1  29887  lnopeq0i  29889  lnophmlem2  29899  ccfldextdgrr  31263  cnre2csqima  31382  efmul2picn  32095  itgexpif  32105  vtscl  32137  vtsprod  32138  circlemeth  32139  logi  33215  iexpire  33216  itgaddnc  35397  iblabsnc  35401  iblmulc2nc  35402  itgmulc2nc  35405  ftc1anclem3  35412  ftc1anclem6  35415  ftc1anclem7  35416  ftc1anclem8  35417  ftc1anc  35418  dvasin  35421  areacirclem4  35428  cntotbnd  35514  sn-1ne2  39797  re1m1e0m0  39877  sn-addid2  39884  sn-it0e0  39894  sn-negex12  39895  reixi  39901  sn-1ticom  39913  sn-mulid2  39914  it1ei  39915  ipiiie0  39916  sn-0tie0  39918  sn-mul02  39919  sn-inelr  39932  itrere  39933  retire  39934  cnreeu  39935  proot1ex  40518  sqrtcval  40714  sqrtcval2  40715  resqrtvalex  40718  imsqrtvalex  40719  sineq0ALT  42016  iblsplit  42974  sqrtnegnre  44232  requad01  44506  sinh-conventional  45656