Axiom ax-icn 10197

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

This axiom is referenced by:  0cn  10234  mulid1  10239  mul02lem2  10415  mul02  10416  addid1  10418  cnegex  10419  cnegex2  10420  0cnALT  10472  negicn  10484  ine0  10667  ixi  10858  recextlem1  10859  recextlem2  10860  recex  10861  rimul  11213  cru  11214  crne0  11215  cju  11218  it0e0  11456  2mulicn  11457  2muline0  11458  cnref1o  12030  irec  13171  i2  13172  i3  13173  i4  13174  iexpcyc  13176  crreczi  13196  imre  14056  reim  14057  crre  14062  crim  14063  remim  14065  mulre  14069  cjreb  14071  recj  14072  reneg  14073  readd  14074  remullem  14076  imcj  14080  imneg  14081  imadd  14082  cjadd  14089  cjneg  14095  imval2  14099  rei  14104  imi  14105  cji  14107  cjreim  14108  cjreim2  14109  rennim  14187  cnpart  14188  sqrtneglem  14215  sqrtneg  14216  sqrtm1  14224  absi  14234  absreimsq  14240  absreim  14241  absimle  14257  abs1m  14283  sqreulem  14307  sqreu  14308  caucvgr  14614  sinf  15060  cosf  15061  tanval2  15069  tanval3  15070  resinval  15071  recosval  15072  efi4p  15073  resin4p  15074  recos4p  15075  resincl  15076  recoscl  15077  sinneg  15082  cosneg  15083  efival  15088  efmival  15089  sinhval  15090  coshval  15091  retanhcl  15095  tanhlt1  15096  tanhbnd  15097  efeul  15098  sinadd  15100  cosadd  15101  ef01bndlem  15120  sin01bnd  15121  cos01bnd  15122  absef  15133  absefib  15134  efieq1re  15135  demoivre  15136  demoivreALT  15137  nthruc  15187  igz  15845  4sqlem17  15872  cnsubrg  20021  cnrehmeo  22972  cmodscexp  23140  ncvspi  23175  cphipval2  23259  4cphipval2  23260  cphipval  23261  itg0  23766  itgz  23767  itgcl  23770  ibl0  23773  iblcnlem1  23774  itgcnlem  23776  itgneg  23790  iblss  23791  iblss2  23792  itgss  23798  itgeqa  23800  iblconst  23804  itgconst  23805  itgadd  23811  iblabs  23815  iblabsr  23816  iblmulc2  23817  itgmulc2  23820  itgsplit  23822  dvsincos  23964  iaa  24300  sincn  24418  coscn  24419  efhalfpi  24444  ef2kpi  24451  efper  24452  sinperlem  24453  efimpi  24464  pige3  24490  sineq0  24494  efeq1  24496  tanregt0  24506  efif1olem4  24512  efifo  24514  eff1olem  24515  circgrp  24519  circsubm  24520  logneg  24555  logm1  24556  lognegb  24557  eflogeq  24569  efiarg  24574  cosargd  24575  logimul  24581  logneg2  24582  abslogle  24585  tanarg  24586  logcn  24614  logf1o2  24617  cxpsqrtlem  24669  cxpsqrt  24670  root1eq1  24717  cxpeq  24719  ang180lem1  24760  ang180lem2  24761  ang180lem3  24762  ang180lem4  24763  1cubrlem  24789  1cubr  24790  asinlem  24816  asinlem2  24817  asinlem3a  24818  asinlem3  24819  asinf  24820  atandm2  24825  atandm3  24826  atanf  24828  asinneg  24834  efiasin  24836  sinasin  24837  asinsinlem  24839  asinsin  24840  asin1  24842  asinbnd  24847  cosasin  24852  atanneg  24855  atancj  24858  efiatan  24860  atanlogaddlem  24861  atanlogadd  24862  atanlogsublem  24863  atanlogsub  24864  efiatan2  24865  2efiatan  24866  tanatan  24867  cosatan  24869  atantan  24871  atanbndlem  24873  atans2  24879  dvatan  24883  atantayl  24885  atantayl2  24886  log2cnv  24892  basellem3  25030  2sqlem2  25364  nvpi  27862  ipval2  27902  4ipval2  27903  ipval3  27904  ipidsq  27905  dipcl  27907  dipcj  27909  dip0r  27912  dipcn  27915  ip1ilem  28021  ipasslem10  28034  ipasslem11  28035  polid2i  28354  polidi  28355  lnopeq0lem1  29204  lnopeq0i  29206  lnophmlem2  29216  bhmafibid1  29984  cnre2csqima  30297  efmul2picn  31014  itgexpif  31024  vtscl  31056  vtsprod  31057  circlemeth  31058  logi  31958  iexpire  31959  itgaddnc  33802  iblabsnc  33806  iblmulc2nc  33807  itgmulc2nc  33810  ftc1anclem3  33819  ftc1anclem6  33822  ftc1anclem7  33823  ftc1anclem8  33824  ftc1anc  33825  dvasin  33828  areacirclem4  33835  cntotbnd  33927  proot1ex  38305  sineq0ALT  39695  iblsplit  40699  sinh-conventional  43011