Axiom ax-icn 10585

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

This axiom is referenced by:  0cn  10622  mulid1  10628  mul02lem2  10806  mul02  10807  addid1  10809  cnegex  10810  cnegex2  10811  0cnALT  10863  0cnALT2  10864  negicn  10876  ine0  11064  ixi  11258  recextlem1  11259  recextlem2  11260  recex  11261  rimul  11616  cru  11617  crne0  11618  cju  11621  it0e0  11847  2mulicn  11848  2muline0  11849  cnref1o  12372  irec  13560  i2  13561  i3  13562  i4  13563  iexpcyc  13565  crreczi  13585  imre  14459  reim  14460  crre  14465  crim  14466  remim  14468  mulre  14472  cjreb  14474  recj  14475  reneg  14476  readd  14477  remullem  14479  imcj  14483  imneg  14484  imadd  14485  cjadd  14492  cjneg  14498  imval2  14502  rei  14507  imi  14508  cji  14510  cjreim  14511  cjreim2  14512  rennim  14590  cnpart  14591  sqrtneglem  14618  sqrtneg  14619  sqrtm1  14627  absi  14638  absreimsq  14644  absreim  14645  absimle  14661  abs1m  14687  sqreulem  14711  sqreu  14712  bhmafibid1  14817  caucvgr  15024  sinf  15469  cosf  15470  tanval2  15478  tanval3  15479  resinval  15480  recosval  15481  efi4p  15482  resin4p  15483  recos4p  15484  resincl  15485  recoscl  15486  sinneg  15491  cosneg  15492  efival  15497  efmival  15498  sinhval  15499  coshval  15500  retanhcl  15504  tanhlt1  15505  tanhbnd  15506  efeul  15507  sinadd  15509  cosadd  15510  ef01bndlem  15529  sin01bnd  15530  cos01bnd  15531  absef  15542  absefib  15543  efieq1re  15544  demoivre  15545  demoivreALT  15546  nthruc  15597  igz  16260  4sqlem17  16287  cnsubrg  20151  cnrehmeo  23558  cmodscexp  23726  ncvspi  23761  cphipval2  23845  4cphipval2  23846  cphipval  23847  itg0  24383  itgz  24384  itgcl  24387  ibl0  24390  iblcnlem1  24391  itgcnlem  24393  itgneg  24407  iblss  24408  iblss2  24409  itgss  24415  itgeqa  24417  iblconst  24421  itgconst  24422  itgadd  24428  iblabs  24432  iblabsr  24433  iblmulc2  24434  itgmulc2  24437  itgsplit  24439  dvsincos  24584  iaa  24921  sincn  25039  coscn  25040  efhalfpi  25064  ef2kpi  25071  efper  25072  sinperlem  25073  efimpi  25084  pige3ALT  25112  sineq0  25116  efeq1  25120  tanregt0  25131  efif1olem4  25137  efifo  25139  eff1olem  25140  circgrp  25144  circsubm  25145  logneg  25179  logm1  25180  lognegb  25181  eflogeq  25193  efiarg  25198  cosargd  25199  logimul  25205  logneg2  25206  abslogle  25209  tanarg  25210  logcn  25238  logf1o2  25241  cxpsqrtlem  25293  cxpsqrt  25294  root1eq1  25344  cxpeq  25346  ang180lem1  25395  ang180lem2  25396  ang180lem3  25397  ang180lem4  25398  1cubrlem  25427  1cubr  25428  asinlem  25454  asinlem2  25455  asinlem3a  25456  asinlem3  25457  asinf  25458  atandm2  25463  atandm3  25464  atanf  25466  asinneg  25472  efiasin  25474  sinasin  25475  asinsinlem  25477  asinsin  25478  asin1  25480  asinbnd  25485  cosasin  25490  atanneg  25493  atancj  25496  efiatan  25498  atanlogaddlem  25499  atanlogadd  25500  atanlogsublem  25501  atanlogsub  25502  efiatan2  25503  2efiatan  25504  tanatan  25505  cosatan  25507  atantan  25509  atanbndlem  25511  atans2  25517  dvatan  25521  atantayl  25523  atantayl2  25524  log2cnv  25530  basellem3  25668  2sqlem2  26002  nvpi  28450  ipval2  28490  4ipval2  28491  ipval3  28492  ipidsq  28493  dipcl  28495  dipcj  28497  dip0r  28500  dipcn  28503  ip1ilem  28609  ipasslem10  28622  ipasslem11  28623  polid2i  28940  polidi  28941  lnopeq0lem1  29788  lnopeq0i  29790  lnophmlem2  29800  ccfldextdgrr  31145  cnre2csqima  31264  efmul2picn  31977  itgexpif  31987  vtscl  32019  vtsprod  32020  circlemeth  32021  logi  33079  iexpire  33080  itgaddnc  35117  iblabsnc  35121  iblmulc2nc  35122  itgmulc2nc  35125  ftc1anclem3  35132  ftc1anclem6  35135  ftc1anclem7  35136  ftc1anclem8  35137  ftc1anc  35138  dvasin  35141  areacirclem4  35148  cntotbnd  35234  sn-1ne2  39466  re1m1e0m0  39535  sn-addid2  39542  sn-it0e0  39552  sn-negex12  39553  reixi  39559  sn-1ticom  39571  sn-mulid2  39572  it1ei  39573  ipiiie0  39574  sn-0tie0  39576  sn-mul02  39577  sn-inelr  39590  itrere  39591  retire  39592  cnreeu  39593  proot1ex  40145  sqrtcval  40341  sqrtcval2  40342  resqrtvalex  40345  imsqrtvalex  40346  sineq0ALT  41643  iblsplit  42608  sqrtnegnre  43864  requad01  44139  sinh-conventional  45265