Axiom ax-icn 11230

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

This axiom is used by:  0cn  11269  mulrid  11277  mul02lem2  11458  mul02  11459  addrid  11461  cnegex  11462  cnegex2  11463  0cnALT  11516  0cnALT2  11517  negicn  11529  ine0  11720  ixi  11914  recextlem1  11915  recextlem2  11916  recex  11917  rimul  12280  cru  12281  crne0  12282  cju  12285  it0e0  12538  2mulicn  12539  2muline0  12540  cnref1o  13082  irec  14312  i2  14313  i3  14314  i4  14315  iexpcyc  14318  crreczi  14339  imre  15242  reim  15243  crre  15248  crim  15249  remim  15251  mulre  15255  cjreb  15257  recj  15258  reneg  15259  readd  15260  remullem  15262  imcj  15266  imneg  15267  imadd  15268  cjadd  15275  cjneg  15281  imval2  15285  rei  15290  imi  15291  cji  15293  cjreim  15294  cjreim2  15295  rennim  15373  cnpart  15374  sqrtneglem  15400  sqrtneg  15401  sqrtm1  15409  absi  15420  absreimsq  15426  absreim  15427  absimle  15443  abs1m  15470  sqreulem  15494  sqreu  15495  bhmafibid1  15602  caucvgr  15810  sinf  16259  cosf  16260  tanval2  16268  tanval3  16269  resinval  16270  recosval  16271  efi4p  16272  resin4p  16273  recos4p  16274  resincl  16275  recoscl  16276  sinneg  16281  cosneg  16282  efival  16287  efmival  16288  sinhval  16289  coshval  16290  retanhcl  16294  tanhlt1  16295  tanhbnd  16296  efeul  16297  sinadd  16299  cosadd  16300  ef01bndlem  16319  sin01bnd  16320  cos01bnd  16321  absef  16332  absefib  16333  efieq1re  16334  demoivre  16335  demoivreALT  16336  nthruc  16387  igz  17073  4sqlem17  17100  cnsubrg  21694  cnrehmeo  25235  cmodscexp  25403  ncvspi  25438  cphipval2  25523  4cphipval2  25524  cphipval  25525  itg0  26061  itgz  26062  itgcl  26065  ibl0  26068  iblcnlem1  26069  itgcnlem  26071  itgneg  26085  iblss  26086  iblss2  26087  itgss  26093  itgeqa  26095  iblconst  26099  itgconst  26100  itgadd  26106  iblabs  26110  iblabsr  26111  iblmulc2  26112  itgmulc2  26115  itgsplit  26117  dvsincos  26262  iaa  26614  iaaOLD  26615  sincn  26734  coscn  26735  efhalfpi  26763  ef2kpi  26770  efper  26771  sinperlem  26772  efimpi  26783  pige3ALT  26811  sineq0  26815  efeq1  26819  tanregt0  26830  efif1olem4  26836  efifo  26838  eff1olem  26839  circgrp  26843  circsubm  26844  logi  26878  logneg  26879  logm1  26880  lognegb  26881  eflogeq  26893  efiarg  26898  cosargd  26899  logimul  26905  logneg2  26906  abslogle  26909  tanarg  26910  logcn  26938  logf1o2  26941  cxpsqrtlem  26993  cxpsqrt  26994  root1eq1  27046  cxpeq  27048  ang180lem1  27100  ang180lem2  27101  ang180lem3  27102  ang180lem4  27103  1cubrlem  27132  1cubr  27133  asinlem  27159  asinlem2  27160  asinlem3a  27161  asinlem3  27162  asinf  27163  atandm2  27168  atandm3  27169  atanf  27171  asinneg  27177  efiasin  27179  sinasin  27180  asinsinlem  27182  asinsin  27183  asin1  27185  asinbnd  27190  cosasin  27195  atanneg  27198  atancj  27201  efiatan  27203  atanlogaddlem  27204  atanlogadd  27205  atanlogsublem  27206  atanlogsub  27207  efiatan2  27208  2efiatan  27209  tanatan  27210  cosatan  27212  atantan  27214  atanbndlem  27216  atans2  27222  dvatan  27226  atantayl  27228  atantayl2  27229  log2cnv  27235  basellem3  27373  2sqlem2  27708  nvpi  31202  ipval2  31242  4ipval2  31243  ipval3  31244  ipidsq  31245  dipcl  31247  dipcj  31249  dip0r  31252  dipcn  31255  ip1ilem  31361  ipasslem10  31374  ipasslem11  31375  polid2i  31692  polidi  31693  lnopeq0lem1  32540  lnopeq0i  32542  lnophmlem2  32552  re0cj  33268  pythagreim  33270  ccfldextdgrr  34237  constrelextdg2  34312  iconstr  34331  constrrecl  34334  constrimcl  34335  constrmulcl  34336  constrresqrtcl  34342  cos9thpiminplylem3  34349  cos9thpiminplylem4  34350  cos9thpiminplylem5  34351  cos9thpiminply  34353  cos9thpinconstrlem1  34354  cos9thpinconstrlem2  34355  cos9thpinconstr  34356  cnre2csqima  34476  efmul2picn  35159  itgexpif  35169  vtscl  35201  vtsprod  35202  circlemeth  35203  iexpire  36421  itgaddnc  38518  iblabsnc  38522  iblmulc2nc  38523  itgmulc2nc  38526  ftc1anclem3  38533  ftc1anclem6  38536  ftc1anclem7  38537  ftc1anclem8  38538  ftc1anc  38539  dvasin  38542  areacirclem4  38549  cntotbnd  38650  sn-1ne2  43250  0tie0  43294  it1ei  43295  1tiei  43296  retire  43298  ef11d  43318  cxp112d  43320  cxp111d  43321  cxpi11d  43322  re1m1e0m0  43376  sn-addlid  43383  sn-it0e0  43395  sn-negex12  43396  reixi  43402  sn-1ticom  43414  sn-mullid  43415  sn-it1ei  43416  ipiiie0  43417  sn-0tie0  43443  sn-mul02  43444  sn-itrere  43480  sn-retire  43481  cnreeu  43482  proot1ex  44141  sqrtcval  44585  sqrtcval2  44586  resqrtvalex  44589  imsqrtvalex  44590  sineq0ALT  45863  iblsplit  46898  sqrtnegnre  48299  requad01  48641  sinh-conventional  50754