Axiom ax-icn 11173

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

This axiom is referenced by:  0cn  11212  mulrid  11218  mul02lem2  11397  mul02  11398  addrid  11400  cnegex  11401  cnegex2  11402  0cnALT  11454  0cnALT2  11455  negicn  11467  ine0  11655  ixi  11849  recextlem1  11850  recextlem2  11851  recex  11852  rimul  12209  cru  12210  crne0  12211  cju  12214  it0e0  12440  2mulicn  12441  2muline0  12442  cnref1o  12975  irec  14171  i2  14172  i3  14173  i4  14174  iexpcyc  14177  crreczi  14197  imre  15061  reim  15062  crre  15067  crim  15068  remim  15070  mulre  15074  cjreb  15076  recj  15077  reneg  15078  readd  15079  remullem  15081  imcj  15085  imneg  15086  imadd  15087  cjadd  15094  cjneg  15100  imval2  15104  rei  15109  imi  15110  cji  15112  cjreim  15113  cjreim2  15114  rennim  15192  cnpart  15193  sqrtneglem  15219  sqrtneg  15220  sqrtm1  15228  absi  15239  absreimsq  15245  absreim  15246  absimle  15262  abs1m  15288  sqreulem  15312  sqreu  15313  bhmafibid1  15418  caucvgr  15628  sinf  16073  cosf  16074  tanval2  16082  tanval3  16083  resinval  16084  recosval  16085  efi4p  16086  resin4p  16087  recos4p  16088  resincl  16089  recoscl  16090  sinneg  16095  cosneg  16096  efival  16101  efmival  16102  sinhval  16103  coshval  16104  retanhcl  16108  tanhlt1  16109  tanhbnd  16110  efeul  16111  sinadd  16113  cosadd  16114  ef01bndlem  16133  sin01bnd  16134  cos01bnd  16135  absef  16146  absefib  16147  efieq1re  16148  demoivre  16149  demoivreALT  16150  nthruc  16201  igz  16873  4sqlem17  16900  cnsubrg  21207  cnrehmeo  24700  cnrehmeoOLD  24701  cmodscexp  24870  ncvspi  24906  cphipval2  24991  4cphipval2  24992  cphipval  24993  itg0  25531  itgz  25532  itgcl  25535  ibl0  25538  iblcnlem1  25539  itgcnlem  25541  itgneg  25555  iblss  25556  iblss2  25557  itgss  25563  itgeqa  25565  iblconst  25569  itgconst  25570  itgadd  25576  iblabs  25580  iblabsr  25581  iblmulc2  25582  itgmulc2  25585  itgsplit  25587  dvsincos  25732  iaa  26072  sincn  26190  coscn  26191  efhalfpi  26215  ef2kpi  26222  efper  26223  sinperlem  26224  efimpi  26235  pige3ALT  26263  sineq0  26267  efeq1  26271  tanregt0  26282  efif1olem4  26288  efifo  26290  eff1olem  26291  circgrp  26295  circsubm  26296  logneg  26330  logm1  26331  lognegb  26332  eflogeq  26344  efiarg  26349  cosargd  26350  logimul  26356  logneg2  26357  abslogle  26360  tanarg  26361  logcn  26389  logf1o2  26392  cxpsqrtlem  26444  cxpsqrt  26445  root1eq1  26497  cxpeq  26499  ang180lem1  26548  ang180lem2  26549  ang180lem3  26550  ang180lem4  26551  1cubrlem  26580  1cubr  26581  asinlem  26607  asinlem2  26608  asinlem3a  26609  asinlem3  26610  asinf  26611  atandm2  26616  atandm3  26617  atanf  26619  asinneg  26625  efiasin  26627  sinasin  26628  asinsinlem  26630  asinsin  26631  asin1  26633  asinbnd  26638  cosasin  26643  atanneg  26646  atancj  26649  efiatan  26651  atanlogaddlem  26652  atanlogadd  26653  atanlogsublem  26654  atanlogsub  26655  efiatan2  26656  2efiatan  26657  tanatan  26658  cosatan  26660  atantan  26662  atanbndlem  26664  atans2  26670  dvatan  26674  atantayl  26676  atantayl2  26677  log2cnv  26683  basellem3  26821  2sqlem2  27155  nvpi  30185  ipval2  30225  4ipval2  30226  ipval3  30227  ipidsq  30228  dipcl  30230  dipcj  30232  dip0r  30235  dipcn  30238  ip1ilem  30344  ipasslem10  30357  ipasslem11  30358  polid2i  30675  polidi  30676  lnopeq0lem1  31523  lnopeq0i  31525  lnophmlem2  31535  ccfldextdgrr  33033  cnre2csqima  33187  efmul2picn  33904  itgexpif  33914  vtscl  33946  vtsprod  33947  circlemeth  33948  logi  35006  iexpire  35007  itgaddnc  36853  iblabsnc  36857  iblmulc2nc  36858  itgmulc2nc  36861  ftc1anclem3  36868  ftc1anclem6  36871  ftc1anclem7  36872  ftc1anclem8  36873  ftc1anc  36874  dvasin  36877  areacirclem4  36884  cntotbnd  36969  sn-1ne2  41483  re1m1e0m0  41574  sn-addlid  41581  sn-it0e0  41592  sn-negex12  41593  reixi  41599  sn-1ticom  41611  sn-mullid  41612  it1ei  41613  ipiiie0  41614  sn-0tie0  41616  sn-mul02  41617  sn-inelr  41642  itrere  41643  retire  41644  cnreeu  41645  proot1ex  42247  sqrtcval  42696  sqrtcval2  42697  resqrtvalex  42700  imsqrtvalex  42701  sineq0ALT  44002  iblsplit  44982  sqrtnegnre  46315  requad01  46589  sinh-conventional  47873