Axiom ax-icn 10930

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

This axiom is referenced by:  0cn  10967  mulid1  10973  mul02lem2  11152  mul02  11153  addid1  11155  cnegex  11156  cnegex2  11157  0cnALT  11209  0cnALT2  11210  negicn  11222  ine0  11410  ixi  11604  recextlem1  11605  recextlem2  11606  recex  11607  rimul  11964  cru  11965  crne0  11966  cju  11969  it0e0  12195  2mulicn  12196  2muline0  12197  cnref1o  12725  irec  13918  i2  13919  i3  13920  i4  13921  iexpcyc  13923  crreczi  13943  imre  14819  reim  14820  crre  14825  crim  14826  remim  14828  mulre  14832  cjreb  14834  recj  14835  reneg  14836  readd  14837  remullem  14839  imcj  14843  imneg  14844  imadd  14845  cjadd  14852  cjneg  14858  imval2  14862  rei  14867  imi  14868  cji  14870  cjreim  14871  cjreim2  14872  rennim  14950  cnpart  14951  sqrtneglem  14978  sqrtneg  14979  sqrtm1  14987  absi  14998  absreimsq  15004  absreim  15005  absimle  15021  abs1m  15047  sqreulem  15071  sqreu  15072  bhmafibid1  15177  caucvgr  15387  sinf  15833  cosf  15834  tanval2  15842  tanval3  15843  resinval  15844  recosval  15845  efi4p  15846  resin4p  15847  recos4p  15848  resincl  15849  recoscl  15850  sinneg  15855  cosneg  15856  efival  15861  efmival  15862  sinhval  15863  coshval  15864  retanhcl  15868  tanhlt1  15869  tanhbnd  15870  efeul  15871  sinadd  15873  cosadd  15874  ef01bndlem  15893  sin01bnd  15894  cos01bnd  15895  absef  15906  absefib  15907  efieq1re  15908  demoivre  15909  demoivreALT  15910  nthruc  15961  igz  16635  4sqlem17  16662  cnsubrg  20658  cnrehmeo  24116  cmodscexp  24284  ncvspi  24320  cphipval2  24405  4cphipval2  24406  cphipval  24407  itg0  24944  itgz  24945  itgcl  24948  ibl0  24951  iblcnlem1  24952  itgcnlem  24954  itgneg  24968  iblss  24969  iblss2  24970  itgss  24976  itgeqa  24978  iblconst  24982  itgconst  24983  itgadd  24989  iblabs  24993  iblabsr  24994  iblmulc2  24995  itgmulc2  24998  itgsplit  25000  dvsincos  25145  iaa  25485  sincn  25603  coscn  25604  efhalfpi  25628  ef2kpi  25635  efper  25636  sinperlem  25637  efimpi  25648  pige3ALT  25676  sineq0  25680  efeq1  25684  tanregt0  25695  efif1olem4  25701  efifo  25703  eff1olem  25704  circgrp  25708  circsubm  25709  logneg  25743  logm1  25744  lognegb  25745  eflogeq  25757  efiarg  25762  cosargd  25763  logimul  25769  logneg2  25770  abslogle  25773  tanarg  25774  logcn  25802  logf1o2  25805  cxpsqrtlem  25857  cxpsqrt  25858  root1eq1  25908  cxpeq  25910  ang180lem1  25959  ang180lem2  25960  ang180lem3  25961  ang180lem4  25962  1cubrlem  25991  1cubr  25992  asinlem  26018  asinlem2  26019  asinlem3a  26020  asinlem3  26021  asinf  26022  atandm2  26027  atandm3  26028  atanf  26030  asinneg  26036  efiasin  26038  sinasin  26039  asinsinlem  26041  asinsin  26042  asin1  26044  asinbnd  26049  cosasin  26054  atanneg  26057  atancj  26060  efiatan  26062  atanlogaddlem  26063  atanlogadd  26064  atanlogsublem  26065  atanlogsub  26066  efiatan2  26067  2efiatan  26068  tanatan  26069  cosatan  26071  atantan  26073  atanbndlem  26075  atans2  26081  dvatan  26085  atantayl  26087  atantayl2  26088  log2cnv  26094  basellem3  26232  2sqlem2  26566  nvpi  29029  ipval2  29069  4ipval2  29070  ipval3  29071  ipidsq  29072  dipcl  29074  dipcj  29076  dip0r  29079  dipcn  29082  ip1ilem  29188  ipasslem10  29201  ipasslem11  29202  polid2i  29519  polidi  29520  lnopeq0lem1  30367  lnopeq0i  30369  lnophmlem2  30379  ccfldextdgrr  31742  cnre2csqima  31861  efmul2picn  32576  itgexpif  32586  vtscl  32618  vtsprod  32619  circlemeth  32620  logi  33700  iexpire  33701  itgaddnc  35837  iblabsnc  35841  iblmulc2nc  35842  itgmulc2nc  35845  ftc1anclem3  35852  ftc1anclem6  35855  ftc1anclem7  35856  ftc1anclem8  35857  ftc1anc  35858  dvasin  35861  areacirclem4  35868  cntotbnd  35954  sn-1ne2  40295  re1m1e0m0  40380  sn-addid2  40387  sn-it0e0  40397  sn-negex12  40398  reixi  40404  sn-1ticom  40416  sn-mulid2  40417  it1ei  40418  ipiiie0  40419  sn-0tie0  40421  sn-mul02  40422  sn-inelr  40435  itrere  40436  retire  40437  cnreeu  40438  proot1ex  41026  sqrtcval  41249  sqrtcval2  41250  resqrtvalex  41253  imsqrtvalex  41254  sineq0ALT  42557  iblsplit  43507  sqrtnegnre  44799  requad01  45073  sinh-conventional  46441