Axiom ax-icn 11186

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

This axiom is referenced by:  0cn  11225  mulrid  11231  mul02lem2  11410  mul02  11411  addrid  11413  cnegex  11414  cnegex2  11415  0cnALT  11468  0cnALT2  11469  negicn  11481  ine0  11670  ixi  11864  recextlem1  11865  recextlem2  11866  recex  11867  rimul  12229  cru  12230  crne0  12231  cju  12234  it0e0  12462  2mulicn  12463  2muline0  12464  cnref1o  12999  irec  14217  i2  14218  i3  14219  i4  14220  iexpcyc  14223  crreczi  14244  imre  15125  reim  15126  crre  15131  crim  15132  remim  15134  mulre  15138  cjreb  15140  recj  15141  reneg  15142  readd  15143  remullem  15145  imcj  15149  imneg  15150  imadd  15151  cjadd  15158  cjneg  15164  imval2  15168  rei  15173  imi  15174  cji  15176  cjreim  15177  cjreim2  15178  rennim  15256  cnpart  15257  sqrtneglem  15283  sqrtneg  15284  sqrtm1  15292  absi  15303  absreimsq  15309  absreim  15310  absimle  15326  abs1m  15352  sqreulem  15376  sqreu  15377  bhmafibid1  15482  caucvgr  15690  sinf  16140  cosf  16141  tanval2  16149  tanval3  16150  resinval  16151  recosval  16152  efi4p  16153  resin4p  16154  recos4p  16155  resincl  16156  recoscl  16157  sinneg  16162  cosneg  16163  efival  16168  efmival  16169  sinhval  16170  coshval  16171  retanhcl  16175  tanhlt1  16176  tanhbnd  16177  efeul  16178  sinadd  16180  cosadd  16181  ef01bndlem  16200  sin01bnd  16201  cos01bnd  16202  absef  16213  absefib  16214  efieq1re  16215  demoivre  16216  demoivreALT  16217  nthruc  16268  igz  16952  4sqlem17  16979  cnsubrg  21393  cnrehmeo  24900  cnrehmeoOLD  24901  cmodscexp  25070  ncvspi  25106  cphipval2  25191  4cphipval2  25192  cphipval  25193  itg0  25731  itgz  25732  itgcl  25735  ibl0  25738  iblcnlem1  25739  itgcnlem  25741  itgneg  25755  iblss  25756  iblss2  25757  itgss  25763  itgeqa  25765  iblconst  25769  itgconst  25770  itgadd  25776  iblabs  25780  iblabsr  25781  iblmulc2  25782  itgmulc2  25785  itgsplit  25787  dvsincos  25935  iaa  26283  sincn  26404  coscn  26405  efhalfpi  26430  ef2kpi  26437  efper  26438  sinperlem  26439  efimpi  26450  pige3ALT  26479  sineq0  26483  efeq1  26487  tanregt0  26498  efif1olem4  26504  efifo  26506  eff1olem  26507  circgrp  26511  circsubm  26512  logi  26546  logneg  26547  logm1  26548  lognegb  26549  eflogeq  26561  efiarg  26566  cosargd  26567  logimul  26573  logneg2  26574  abslogle  26577  tanarg  26578  logcn  26606  logf1o2  26609  cxpsqrtlem  26661  cxpsqrt  26662  root1eq1  26715  cxpeq  26717  ang180lem1  26769  ang180lem2  26770  ang180lem3  26771  ang180lem4  26772  1cubrlem  26801  1cubr  26802  asinlem  26828  asinlem2  26829  asinlem3a  26830  asinlem3  26831  asinf  26832  atandm2  26837  atandm3  26838  atanf  26840  asinneg  26846  efiasin  26848  sinasin  26849  asinsinlem  26851  asinsin  26852  asin1  26854  asinbnd  26859  cosasin  26864  atanneg  26867  atancj  26870  efiatan  26872  atanlogaddlem  26873  atanlogadd  26874  atanlogsublem  26875  atanlogsub  26876  efiatan2  26877  2efiatan  26878  tanatan  26879  cosatan  26881  atantan  26883  atanbndlem  26885  atans2  26891  dvatan  26895  atantayl  26897  atantayl2  26898  log2cnv  26904  basellem3  27043  2sqlem2  27379  nvpi  30594  ipval2  30634  4ipval2  30635  ipval3  30636  ipidsq  30637  dipcl  30639  dipcj  30641  dip0r  30644  dipcn  30647  ip1ilem  30753  ipasslem10  30766  ipasslem11  30767  polid2i  31084  polidi  31085  lnopeq0lem1  31932  lnopeq0i  31934  lnophmlem2  31944  re0cj  32667  pythagreim  32669  ccfldextdgrr  33659  constrelextdg2  33727  iconstr  33746  constrrecl  33749  constrimcl  33750  constrmulcl  33751  constrresqrtcl  33757  cos9thpiminplylem3  33764  cos9thpiminplylem4  33765  cos9thpiminplylem5  33766  cos9thpiminply  33768  cos9thpinconstrlem1  33769  cnre2csqima  33888  efmul2picn  34574  itgexpif  34584  vtscl  34616  vtsprod  34617  circlemeth  34618  iexpire  35698  itgaddnc  37650  iblabsnc  37654  iblmulc2nc  37655  itgmulc2nc  37658  ftc1anclem3  37665  ftc1anclem6  37668  ftc1anclem7  37669  ftc1anclem8  37670  ftc1anc  37671  dvasin  37674  areacirclem4  37681  cntotbnd  37766  sn-1ne2  42262  0tie0  42311  it1ei  42312  1tiei  42313  itrere  42314  retire  42315  ef11d  42335  cxp112d  42337  cxp111d  42338  cxpi11d  42339  re1m1e0m0  42387  sn-addlid  42394  sn-it0e0  42405  sn-negex12  42406  reixi  42412  sn-1ticom  42424  sn-mullid  42425  sn-it1ei  42426  ipiiie0  42427  sn-0tie0  42429  sn-mul02  42430  sn-inelr  42457  sn-itrere  42458  sn-retire  42459  cnreeu  42460  proot1ex  43167  sqrtcval  43612  sqrtcval2  43613  resqrtvalex  43616  imsqrtvalex  43617  sineq0ALT  44909  iblsplit  45943  sqrtnegnre  47284  requad01  47583  sinh-conventional  49551