Axiom ax-icn 10596

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

This axiom is referenced by:  0cn  10633  mulid1  10639  mul02lem2  10817  mul02  10818  addid1  10820  cnegex  10821  cnegex2  10822  0cnALT  10874  0cnALT2  10875  negicn  10887  ine0  11075  ixi  11269  recextlem1  11270  recextlem2  11271  recex  11272  rimul  11629  cru  11630  crne0  11631  cju  11634  it0e0  11860  2mulicn  11861  2muline0  11862  cnref1o  12385  irec  13565  i2  13566  i3  13567  i4  13568  iexpcyc  13570  crreczi  13590  imre  14467  reim  14468  crre  14473  crim  14474  remim  14476  mulre  14480  cjreb  14482  recj  14483  reneg  14484  readd  14485  remullem  14487  imcj  14491  imneg  14492  imadd  14493  cjadd  14500  cjneg  14506  imval2  14510  rei  14515  imi  14516  cji  14518  cjreim  14519  cjreim2  14520  rennim  14598  cnpart  14599  sqrtneglem  14626  sqrtneg  14627  sqrtm1  14635  absi  14646  absreimsq  14652  absreim  14653  absimle  14669  abs1m  14695  sqreulem  14719  sqreu  14720  bhmafibid1  14825  caucvgr  15032  sinf  15477  cosf  15478  tanval2  15486  tanval3  15487  resinval  15488  recosval  15489  efi4p  15490  resin4p  15491  recos4p  15492  resincl  15493  recoscl  15494  sinneg  15499  cosneg  15500  efival  15505  efmival  15506  sinhval  15507  coshval  15508  retanhcl  15512  tanhlt1  15513  tanhbnd  15514  efeul  15515  sinadd  15517  cosadd  15518  ef01bndlem  15537  sin01bnd  15538  cos01bnd  15539  absef  15550  absefib  15551  efieq1re  15552  demoivre  15553  demoivreALT  15554  nthruc  15605  igz  16270  4sqlem17  16297  cnsubrg  20605  cnrehmeo  23557  cmodscexp  23725  ncvspi  23760  cphipval2  23844  4cphipval2  23845  cphipval  23846  itg0  24380  itgz  24381  itgcl  24384  ibl0  24387  iblcnlem1  24388  itgcnlem  24390  itgneg  24404  iblss  24405  iblss2  24406  itgss  24412  itgeqa  24414  iblconst  24418  itgconst  24419  itgadd  24425  iblabs  24429  iblabsr  24430  iblmulc2  24431  itgmulc2  24434  itgsplit  24436  dvsincos  24578  iaa  24914  sincn  25032  coscn  25033  efhalfpi  25057  ef2kpi  25064  efper  25065  sinperlem  25066  efimpi  25077  pige3ALT  25105  sineq0  25109  efeq1  25113  tanregt0  25123  efif1olem4  25129  efifo  25131  eff1olem  25132  circgrp  25136  circsubm  25137  logneg  25171  logm1  25172  lognegb  25173  eflogeq  25185  efiarg  25190  cosargd  25191  logimul  25197  logneg2  25198  abslogle  25201  tanarg  25202  logcn  25230  logf1o2  25233  cxpsqrtlem  25285  cxpsqrt  25286  root1eq1  25336  cxpeq  25338  ang180lem1  25387  ang180lem2  25388  ang180lem3  25389  ang180lem4  25390  1cubrlem  25419  1cubr  25420  asinlem  25446  asinlem2  25447  asinlem3a  25448  asinlem3  25449  asinf  25450  atandm2  25455  atandm3  25456  atanf  25458  asinneg  25464  efiasin  25466  sinasin  25467  asinsinlem  25469  asinsin  25470  asin1  25472  asinbnd  25477  cosasin  25482  atanneg  25485  atancj  25488  efiatan  25490  atanlogaddlem  25491  atanlogadd  25492  atanlogsublem  25493  atanlogsub  25494  efiatan2  25495  2efiatan  25496  tanatan  25497  cosatan  25499  atantan  25501  atanbndlem  25503  atans2  25509  dvatan  25513  atantayl  25515  atantayl2  25516  log2cnv  25522  basellem3  25660  2sqlem2  25994  nvpi  28444  ipval2  28484  4ipval2  28485  ipval3  28486  ipidsq  28487  dipcl  28489  dipcj  28491  dip0r  28494  dipcn  28497  ip1ilem  28603  ipasslem10  28616  ipasslem11  28617  polid2i  28934  polidi  28935  lnopeq0lem1  29782  lnopeq0i  29784  lnophmlem2  29794  ccfldextdgrr  31057  cnre2csqima  31154  efmul2picn  31867  itgexpif  31877  vtscl  31909  vtsprod  31910  circlemeth  31911  logi  32966  iexpire  32967  itgaddnc  34967  iblabsnc  34971  iblmulc2nc  34972  itgmulc2nc  34975  ftc1anclem3  34984  ftc1anclem6  34987  ftc1anclem7  34988  ftc1anclem8  34989  ftc1anc  34990  dvasin  34993  areacirclem4  35000  cntotbnd  35089  sn-1ne2  39207  re1m1e0m0  39276  sn-addid2  39283  proot1ex  39850  sineq0ALT  41320  iblsplit  42300  sqrtnegnre  43556  requad01  43835  sinh-conventional  44887