Axiom ax-icn 11103

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

This axiom is referenced by:  0cn  11142  mulrid  11148  mul02lem2  11327  mul02  11328  addrid  11330  cnegex  11331  cnegex2  11332  0cnALT  11385  0cnALT2  11386  negicn  11398  ine0  11589  ixi  11783  recextlem1  11784  recextlem2  11785  recex  11786  rimul  12153  cru  12154  crne0  12155  cju  12158  it0e0  12381  2mulicn  12382  2muline0  12383  cnref1o  12920  irec  14142  i2  14143  i3  14144  i4  14145  iexpcyc  14148  crreczi  14169  imre  15050  reim  15051  crre  15056  crim  15057  remim  15059  mulre  15063  cjreb  15065  recj  15066  reneg  15067  readd  15068  remullem  15070  imcj  15074  imneg  15075  imadd  15076  cjadd  15083  cjneg  15089  imval2  15093  rei  15098  imi  15099  cji  15101  cjreim  15102  cjreim2  15103  rennim  15181  cnpart  15182  sqrtneglem  15208  sqrtneg  15209  sqrtm1  15217  absi  15228  absreimsq  15234  absreim  15235  absimle  15251  abs1m  15278  sqreulem  15302  sqreu  15303  bhmafibid1  15410  caucvgr  15618  sinf  16068  cosf  16069  tanval2  16077  tanval3  16078  resinval  16079  recosval  16080  efi4p  16081  resin4p  16082  recos4p  16083  resincl  16084  recoscl  16085  sinneg  16090  cosneg  16091  efival  16096  efmival  16097  sinhval  16098  coshval  16099  retanhcl  16103  tanhlt1  16104  tanhbnd  16105  efeul  16106  sinadd  16108  cosadd  16109  ef01bndlem  16128  sin01bnd  16129  cos01bnd  16130  absef  16141  absefib  16142  efieq1re  16143  demoivre  16144  demoivreALT  16145  nthruc  16196  igz  16881  4sqlem17  16908  cnsubrg  21320  cnrehmeo  24827  cnrehmeoOLD  24828  cmodscexp  24997  ncvspi  25032  cphipval2  25117  4cphipval2  25118  cphipval  25119  itg0  25657  itgz  25658  itgcl  25661  ibl0  25664  iblcnlem1  25665  itgcnlem  25667  itgneg  25681  iblss  25682  iblss2  25683  itgss  25689  itgeqa  25691  iblconst  25695  itgconst  25696  itgadd  25702  iblabs  25706  iblabsr  25707  iblmulc2  25708  itgmulc2  25711  itgsplit  25713  dvsincos  25861  iaa  26209  sincn  26330  coscn  26331  efhalfpi  26356  ef2kpi  26363  efper  26364  sinperlem  26365  efimpi  26376  pige3ALT  26405  sineq0  26409  efeq1  26413  tanregt0  26424  efif1olem4  26430  efifo  26432  eff1olem  26433  circgrp  26437  circsubm  26438  logi  26472  logneg  26473  logm1  26474  lognegb  26475  eflogeq  26487  efiarg  26492  cosargd  26493  logimul  26499  logneg2  26500  abslogle  26503  tanarg  26504  logcn  26532  logf1o2  26535  cxpsqrtlem  26587  cxpsqrt  26588  root1eq1  26641  cxpeq  26643  ang180lem1  26695  ang180lem2  26696  ang180lem3  26697  ang180lem4  26698  1cubrlem  26727  1cubr  26728  asinlem  26754  asinlem2  26755  asinlem3a  26756  asinlem3  26757  asinf  26758  atandm2  26763  atandm3  26764  atanf  26766  asinneg  26772  efiasin  26774  sinasin  26775  asinsinlem  26777  asinsin  26778  asin1  26780  asinbnd  26785  cosasin  26790  atanneg  26793  atancj  26796  efiatan  26798  atanlogaddlem  26799  atanlogadd  26800  atanlogsublem  26801  atanlogsub  26802  efiatan2  26803  2efiatan  26804  tanatan  26805  cosatan  26807  atantan  26809  atanbndlem  26811  atans2  26817  dvatan  26821  atantayl  26823  atantayl2  26824  log2cnv  26830  basellem3  26969  2sqlem2  27305  nvpi  30569  ipval2  30609  4ipval2  30610  ipval3  30611  ipidsq  30612  dipcl  30614  dipcj  30616  dip0r  30619  dipcn  30622  ip1ilem  30728  ipasslem10  30741  ipasslem11  30742  polid2i  31059  polidi  31060  lnopeq0lem1  31907  lnopeq0i  31909  lnophmlem2  31919  re0cj  32640  pythagreim  32642  ccfldextdgrr  33640  constrelextdg2  33710  iconstr  33729  constrrecl  33732  constrimcl  33733  constrmulcl  33734  constrresqrtcl  33740  cos9thpiminplylem3  33747  cos9thpiminplylem4  33748  cos9thpiminplylem5  33749  cos9thpiminply  33751  cos9thpinconstrlem1  33752  cos9thpinconstrlem2  33753  cos9thpinconstr  33754  cnre2csqima  33874  efmul2picn  34560  itgexpif  34570  vtscl  34602  vtsprod  34603  circlemeth  34604  iexpire  35695  itgaddnc  37647  iblabsnc  37651  iblmulc2nc  37652  itgmulc2nc  37655  ftc1anclem3  37662  ftc1anclem6  37665  ftc1anclem7  37666  ftc1anclem8  37667  ftc1anc  37668  dvasin  37671  areacirclem4  37678  cntotbnd  37763  sn-1ne2  42226  0tie0  42276  it1ei  42277  1tiei  42278  retire  42280  ef11d  42300  cxp112d  42302  cxp111d  42303  cxpi11d  42304  re1m1e0m0  42358  sn-addlid  42365  sn-it0e0  42377  sn-negex12  42378  reixi  42384  sn-1ticom  42396  sn-mullid  42397  sn-it1ei  42398  ipiiie0  42399  sn-0tie0  42412  sn-mul02  42413  sn-itrere  42449  sn-retire  42450  cnreeu  42451  proot1ex  43158  sqrtcval  43603  sqrtcval2  43604  resqrtvalex  43607  imsqrtvalex  43608  sineq0ALT  44899  iblsplit  45937  sqrtnegnre  47281  requad01  47595  sinh-conventional  49701