Axiom ax-icn 11060

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

This axiom is referenced by:  0cn  11099  mulrid  11105  mul02lem2  11285  mul02  11286  addrid  11288  cnegex  11289  cnegex2  11290  0cnALT  11343  0cnALT2  11344  negicn  11356  ine0  11547  ixi  11741  recextlem1  11742  recextlem2  11743  recex  11744  rimul  12111  cru  12112  crne0  12113  cju  12116  it0e0  12339  2mulicn  12340  2muline0  12341  cnref1o  12878  irec  14103  i2  14104  i3  14105  i4  14106  iexpcyc  14109  crreczi  14130  imre  15010  reim  15011  crre  15016  crim  15017  remim  15019  mulre  15023  cjreb  15025  recj  15026  reneg  15027  readd  15028  remullem  15030  imcj  15034  imneg  15035  imadd  15036  cjadd  15043  cjneg  15049  imval2  15053  rei  15058  imi  15059  cji  15061  cjreim  15062  cjreim2  15063  rennim  15141  cnpart  15142  sqrtneglem  15168  sqrtneg  15169  sqrtm1  15177  absi  15188  absreimsq  15194  absreim  15195  absimle  15211  abs1m  15238  sqreulem  15262  sqreu  15263  bhmafibid1  15370  caucvgr  15578  sinf  16028  cosf  16029  tanval2  16037  tanval3  16038  resinval  16039  recosval  16040  efi4p  16041  resin4p  16042  recos4p  16043  resincl  16044  recoscl  16045  sinneg  16050  cosneg  16051  efival  16056  efmival  16057  sinhval  16058  coshval  16059  retanhcl  16063  tanhlt1  16064  tanhbnd  16065  efeul  16066  sinadd  16068  cosadd  16069  ef01bndlem  16088  sin01bnd  16089  cos01bnd  16090  absef  16101  absefib  16102  efieq1re  16103  demoivre  16104  demoivreALT  16105  nthruc  16156  igz  16841  4sqlem17  16868  cnsubrg  21359  cnrehmeo  24873  cnrehmeoOLD  24874  cmodscexp  25043  ncvspi  25078  cphipval2  25163  4cphipval2  25164  cphipval  25165  itg0  25703  itgz  25704  itgcl  25707  ibl0  25710  iblcnlem1  25711  itgcnlem  25713  itgneg  25727  iblss  25728  iblss2  25729  itgss  25735  itgeqa  25737  iblconst  25741  itgconst  25742  itgadd  25748  iblabs  25752  iblabsr  25753  iblmulc2  25754  itgmulc2  25757  itgsplit  25759  dvsincos  25907  iaa  26255  sincn  26376  coscn  26377  efhalfpi  26402  ef2kpi  26409  efper  26410  sinperlem  26411  efimpi  26422  pige3ALT  26451  sineq0  26455  efeq1  26459  tanregt0  26470  efif1olem4  26476  efifo  26478  eff1olem  26479  circgrp  26483  circsubm  26484  logi  26518  logneg  26519  logm1  26520  lognegb  26521  eflogeq  26533  efiarg  26538  cosargd  26539  logimul  26545  logneg2  26546  abslogle  26549  tanarg  26550  logcn  26578  logf1o2  26581  cxpsqrtlem  26633  cxpsqrt  26634  root1eq1  26687  cxpeq  26689  ang180lem1  26741  ang180lem2  26742  ang180lem3  26743  ang180lem4  26744  1cubrlem  26773  1cubr  26774  asinlem  26800  asinlem2  26801  asinlem3a  26802  asinlem3  26803  asinf  26804  atandm2  26809  atandm3  26810  atanf  26812  asinneg  26818  efiasin  26820  sinasin  26821  asinsinlem  26823  asinsin  26824  asin1  26826  asinbnd  26831  cosasin  26836  atanneg  26839  atancj  26842  efiatan  26844  atanlogaddlem  26845  atanlogadd  26846  atanlogsublem  26847  atanlogsub  26848  efiatan2  26849  2efiatan  26850  tanatan  26851  cosatan  26853  atantan  26855  atanbndlem  26857  atans2  26863  dvatan  26867  atantayl  26869  atantayl2  26870  log2cnv  26876  basellem3  27015  2sqlem2  27351  nvpi  30639  ipval2  30679  4ipval2  30680  ipval3  30681  ipidsq  30682  dipcl  30684  dipcj  30686  dip0r  30689  dipcn  30692  ip1ilem  30798  ipasslem10  30811  ipasslem11  30812  polid2i  31129  polidi  31130  lnopeq0lem1  31977  lnopeq0i  31979  lnophmlem2  31989  re0cj  32719  pythagreim  32721  ccfldextdgrr  33677  constrelextdg2  33752  iconstr  33771  constrrecl  33774  constrimcl  33775  constrmulcl  33776  constrresqrtcl  33782  cos9thpiminplylem3  33789  cos9thpiminplylem4  33790  cos9thpiminplylem5  33791  cos9thpiminply  33793  cos9thpinconstrlem1  33794  cos9thpinconstrlem2  33795  cos9thpinconstr  33796  cnre2csqima  33916  efmul2picn  34601  itgexpif  34611  vtscl  34643  vtsprod  34644  circlemeth  34645  iexpire  35771  itgaddnc  37720  iblabsnc  37724  iblmulc2nc  37725  itgmulc2nc  37728  ftc1anclem3  37735  ftc1anclem6  37738  ftc1anclem7  37739  ftc1anclem8  37740  ftc1anc  37741  dvasin  37744  areacirclem4  37751  cntotbnd  37836  sn-1ne2  42298  0tie0  42348  it1ei  42349  1tiei  42350  retire  42352  ef11d  42372  cxp112d  42374  cxp111d  42375  cxpi11d  42376  re1m1e0m0  42430  sn-addlid  42437  sn-it0e0  42449  sn-negex12  42450  reixi  42456  sn-1ticom  42468  sn-mullid  42469  sn-it1ei  42470  ipiiie0  42471  sn-0tie0  42484  sn-mul02  42485  sn-itrere  42521  sn-retire  42522  cnreeu  42523  proot1ex  43229  sqrtcval  43674  sqrtcval2  43675  resqrtvalex  43678  imsqrtvalex  43679  sineq0ALT  44969  iblsplit  46004  sqrtnegnre  47338  requad01  47652  sinh-conventional  49771