Axiom ax-icn 11283

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

This axiom is used by:  0cn  11322  mulrid  11330  mul02lem2  11511  mul02  11512  addrid  11514  cnegex  11515  cnegex2  11516  0cnALT  11569  0cnALT2  11570  negicn  11582  ine0  11775  ixi  11969  recextlem1  11970  recextlem2  11971  recex  11972  rimul  12335  cru  12336  crne0  12337  cju  12340  it0e0  12593  2mulicn  12594  2muline0  12595  cnref1o  13137  irec  14369  i2  14370  i3  14371  i4  14372  iexpcyc  14375  crreczi  14396  imre  15301  reim  15302  crre  15307  crim  15308  remim  15310  mulre  15314  cjreb  15316  recj  15317  reneg  15318  readd  15319  remullem  15321  imcj  15325  imneg  15326  imadd  15327  cjadd  15334  cjneg  15340  imval2  15344  rei  15349  imi  15350  cji  15352  cjreim  15353  cjreim2  15354  rennim  15432  cnpart  15433  sqrtneglem  15459  sqrtneg  15460  sqrtm1  15468  absi  15479  absreimsq  15485  absreim  15486  absimle  15502  abs1m  15529  sqreulem  15553  sqreu  15554  bhmafibid1  15661  caucvgr  15869  sinf  16318  cosf  16319  tanval2  16327  tanval3  16328  resinval  16329  recosval  16330  efi4p  16331  resin4p  16332  recos4p  16333  resincl  16334  recoscl  16335  sinneg  16340  cosneg  16341  efival  16346  efmival  16347  sinhval  16348  coshval  16349  retanhcl  16353  tanhlt1  16354  tanhbnd  16355  efeul  16356  sinadd  16358  cosadd  16359  ef01bndlem  16378  sin01bnd  16379  cos01bnd  16380  absef  16391  absefib  16392  efieq1re  16393  demoivre  16394  demoivreALT  16395  nthruc  16446  igz  17138  4sqlem17  17165  cnsubrg  21760  cnrehmeo  25301  cmodscexp  25469  ncvspi  25504  cphipval2  25589  4cphipval2  25590  cphipval  25591  itg0  26127  itgz  26128  itgcl  26131  ibl0  26134  iblcnlem1  26135  itgcnlem  26137  itgneg  26151  iblss  26152  iblss2  26153  itgss  26159  itgeqa  26161  iblconst  26165  itgconst  26166  itgadd  26172  iblabs  26176  iblabsr  26177  iblmulc2  26178  itgmulc2  26181  itgsplit  26183  dvsincos  26328  iaa  26678  iaaOLD  26679  sincn  26798  coscn  26799  efhalfpi  26827  ef2kpi  26834  efper  26835  sinperlem  26836  efimpi  26847  pige3ALT  26875  sineq0  26879  efeq1  26883  tanregt0  26894  efif1olem4  26900  efifo  26902  eff1olem  26903  circgrp  26907  circsubm  26908  logi  26942  logneg  26943  logm1  26944  lognegb  26945  eflogeq  26957  efiarg  26962  cosargd  26963  logimul  26969  logneg2  26970  abslogle  26973  tanarg  26974  logcn  27002  logf1o2  27005  cxpsqrtlem  27057  cxpsqrt  27058  root1eq1  27110  cxpeq  27112  ang180lem1  27164  ang180lem2  27165  ang180lem3  27166  ang180lem4  27167  1cubrlem  27196  1cubr  27197  asinlem  27223  asinlem2  27224  asinlem3a  27225  asinlem3  27226  asinf  27227  atandm2  27232  atandm3  27233  atanf  27235  asinneg  27241  efiasin  27243  sinasin  27244  asinsinlem  27246  asinsin  27247  asin1  27249  asinbnd  27254  cosasin  27259  atanneg  27262  atancj  27265  efiatan  27267  atanlogaddlem  27268  atanlogadd  27269  atanlogsublem  27270  atanlogsub  27271  efiatan2  27272  2efiatan  27273  tanatan  27274  cosatan  27276  atantan  27278  atanbndlem  27280  atans2  27286  dvatan  27290  atantayl  27292  atantayl2  27293  log2cnv  27299  basellem3  27437  2sqlem2  27772  nvpi  31296  ipval2  31336  4ipval2  31337  ipval3  31338  ipidsq  31339  dipcl  31341  dipcj  31343  dip0r  31346  dipcn  31349  ip1ilem  31455  ipasslem10  31468  ipasslem11  31469  polid2i  31786  polidi  31787  lnopeq0lem1  32634  lnopeq0i  32636  lnophmlem2  32646  re0cj  33402  pythagreim  33404  ccfldextdgrr  34371  constrelextdg2  34446  iconstr  34465  constrrecl  34468  constrimcl  34469  constrmulcl  34470  constrresqrtcl  34476  cos9thpiminplylem3  34483  cos9thpiminplylem4  34484  cos9thpiminplylem5  34485  cos9thpiminply  34487  cos9thpinconstrlem1  34488  cos9thpinconstrlem2  34489  cos9thpinconstr  34490  cnre2csqima  34610  efmul2picn  35292  itgexpif  35302  vtscl  35334  vtsprod  35335  circlemeth  35336  iexpire  36677  itgaddnc  38789  iblabsnc  38793  iblmulc2nc  38794  itgmulc2nc  38797  ftc1anclem3  38804  ftc1anclem6  38807  ftc1anclem7  38808  ftc1anclem8  38809  ftc1anc  38810  dvasin  38813  areacirclem4  38820  cntotbnd  38921  sn-1ne2  43521  0tie0  43563  it1ei  43564  1tiei  43565  retire  43567  ef11d  43581  cxp112d  43583  cxp111d  43584  cxpi11d  43585  re1m1e0m0  43639  sn-addlid  43646  sn-it0e0  43658  sn-negex12  43659  reixi  43665  sn-1ticom  43677  sn-mullid  43678  sn-it1ei  43679  ipiiie0  43680  sn-0tie0  43706  sn-mul02  43707  sn-itrere  43743  sn-retire  43744  cnreeu  43745  proot1ex  44388  sqrtcval  44831  sqrtcval2  44832  resqrtvalex  44835  imsqrtvalex  44836  sineq0ALT  46108  iblsplit  47179  sqrtnegnre  48580  requad01  48922  sinh-conventional  51110