Axiom ax-icn 11127

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

This axiom is referenced by:  0cn  11166  mulrid  11172  mul02lem2  11351  mul02  11352  addrid  11354  cnegex  11355  cnegex2  11356  0cnALT  11409  0cnALT2  11410  negicn  11422  ine0  11613  ixi  11807  recextlem1  11808  recextlem2  11809  recex  11810  rimul  12177  cru  12178  crne0  12179  cju  12182  it0e0  12405  2mulicn  12406  2muline0  12407  cnref1o  12944  irec  14166  i2  14167  i3  14168  i4  14169  iexpcyc  14172  crreczi  14193  imre  15074  reim  15075  crre  15080  crim  15081  remim  15083  mulre  15087  cjreb  15089  recj  15090  reneg  15091  readd  15092  remullem  15094  imcj  15098  imneg  15099  imadd  15100  cjadd  15107  cjneg  15113  imval2  15117  rei  15122  imi  15123  cji  15125  cjreim  15126  cjreim2  15127  rennim  15205  cnpart  15206  sqrtneglem  15232  sqrtneg  15233  sqrtm1  15241  absi  15252  absreimsq  15258  absreim  15259  absimle  15275  abs1m  15302  sqreulem  15326  sqreu  15327  bhmafibid1  15434  caucvgr  15642  sinf  16092  cosf  16093  tanval2  16101  tanval3  16102  resinval  16103  recosval  16104  efi4p  16105  resin4p  16106  recos4p  16107  resincl  16108  recoscl  16109  sinneg  16114  cosneg  16115  efival  16120  efmival  16121  sinhval  16122  coshval  16123  retanhcl  16127  tanhlt1  16128  tanhbnd  16129  efeul  16130  sinadd  16132  cosadd  16133  ef01bndlem  16152  sin01bnd  16153  cos01bnd  16154  absef  16165  absefib  16166  efieq1re  16167  demoivre  16168  demoivreALT  16169  nthruc  16220  igz  16905  4sqlem17  16932  cnsubrg  21344  cnrehmeo  24851  cnrehmeoOLD  24852  cmodscexp  25021  ncvspi  25056  cphipval2  25141  4cphipval2  25142  cphipval  25143  itg0  25681  itgz  25682  itgcl  25685  ibl0  25688  iblcnlem1  25689  itgcnlem  25691  itgneg  25705  iblss  25706  iblss2  25707  itgss  25713  itgeqa  25715  iblconst  25719  itgconst  25720  itgadd  25726  iblabs  25730  iblabsr  25731  iblmulc2  25732  itgmulc2  25735  itgsplit  25737  dvsincos  25885  iaa  26233  sincn  26354  coscn  26355  efhalfpi  26380  ef2kpi  26387  efper  26388  sinperlem  26389  efimpi  26400  pige3ALT  26429  sineq0  26433  efeq1  26437  tanregt0  26448  efif1olem4  26454  efifo  26456  eff1olem  26457  circgrp  26461  circsubm  26462  logi  26496  logneg  26497  logm1  26498  lognegb  26499  eflogeq  26511  efiarg  26516  cosargd  26517  logimul  26523  logneg2  26524  abslogle  26527  tanarg  26528  logcn  26556  logf1o2  26559  cxpsqrtlem  26611  cxpsqrt  26612  root1eq1  26665  cxpeq  26667  ang180lem1  26719  ang180lem2  26720  ang180lem3  26721  ang180lem4  26722  1cubrlem  26751  1cubr  26752  asinlem  26778  asinlem2  26779  asinlem3a  26780  asinlem3  26781  asinf  26782  atandm2  26787  atandm3  26788  atanf  26790  asinneg  26796  efiasin  26798  sinasin  26799  asinsinlem  26801  asinsin  26802  asin1  26804  asinbnd  26809  cosasin  26814  atanneg  26817  atancj  26820  efiatan  26822  atanlogaddlem  26823  atanlogadd  26824  atanlogsublem  26825  atanlogsub  26826  efiatan2  26827  2efiatan  26828  tanatan  26829  cosatan  26831  atantan  26833  atanbndlem  26835  atans2  26841  dvatan  26845  atantayl  26847  atantayl2  26848  log2cnv  26854  basellem3  26993  2sqlem2  27329  nvpi  30596  ipval2  30636  4ipval2  30637  ipval3  30638  ipidsq  30639  dipcl  30641  dipcj  30643  dip0r  30646  dipcn  30649  ip1ilem  30755  ipasslem10  30768  ipasslem11  30769  polid2i  31086  polidi  31087  lnopeq0lem1  31934  lnopeq0i  31936  lnophmlem2  31946  re0cj  32667  pythagreim  32669  ccfldextdgrr  33667  constrelextdg2  33737  iconstr  33756  constrrecl  33759  constrimcl  33760  constrmulcl  33761  constrresqrtcl  33767  cos9thpiminplylem3  33774  cos9thpiminplylem4  33775  cos9thpiminplylem5  33776  cos9thpiminply  33778  cos9thpinconstrlem1  33779  cos9thpinconstrlem2  33780  cos9thpinconstr  33781  cnre2csqima  33901  efmul2picn  34587  itgexpif  34597  vtscl  34629  vtsprod  34630  circlemeth  34631  iexpire  35722  itgaddnc  37674  iblabsnc  37678  iblmulc2nc  37679  itgmulc2nc  37682  ftc1anclem3  37689  ftc1anclem6  37692  ftc1anclem7  37693  ftc1anclem8  37694  ftc1anc  37695  dvasin  37698  areacirclem4  37705  cntotbnd  37790  sn-1ne2  42253  0tie0  42303  it1ei  42304  1tiei  42305  retire  42307  ef11d  42327  cxp112d  42329  cxp111d  42330  cxpi11d  42331  re1m1e0m0  42385  sn-addlid  42392  sn-it0e0  42404  sn-negex12  42405  reixi  42411  sn-1ticom  42423  sn-mullid  42424  sn-it1ei  42425  ipiiie0  42426  sn-0tie0  42439  sn-mul02  42440  sn-itrere  42476  sn-retire  42477  cnreeu  42478  proot1ex  43185  sqrtcval  43630  sqrtcval2  43631  resqrtvalex  43634  imsqrtvalex  43635  sineq0ALT  44926  iblsplit  45964  sqrtnegnre  47308  requad01  47622  sinh-conventional  49728