Axiom ax-icn 11065

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

This axiom is referenced by:  0cn  11104  mulrid  11110  mul02lem2  11290  mul02  11291  addrid  11293  cnegex  11294  cnegex2  11295  0cnALT  11348  0cnALT2  11349  negicn  11361  ine0  11552  ixi  11746  recextlem1  11747  recextlem2  11748  recex  11749  rimul  12116  cru  12117  crne0  12118  cju  12121  it0e0  12344  2mulicn  12345  2muline0  12346  cnref1o  12883  irec  14108  i2  14109  i3  14110  i4  14111  iexpcyc  14114  crreczi  14135  imre  15015  reim  15016  crre  15021  crim  15022  remim  15024  mulre  15028  cjreb  15030  recj  15031  reneg  15032  readd  15033  remullem  15035  imcj  15039  imneg  15040  imadd  15041  cjadd  15048  cjneg  15054  imval2  15058  rei  15063  imi  15064  cji  15066  cjreim  15067  cjreim2  15068  rennim  15146  cnpart  15147  sqrtneglem  15173  sqrtneg  15174  sqrtm1  15182  absi  15193  absreimsq  15199  absreim  15200  absimle  15216  abs1m  15243  sqreulem  15267  sqreu  15268  bhmafibid1  15375  caucvgr  15583  sinf  16033  cosf  16034  tanval2  16042  tanval3  16043  resinval  16044  recosval  16045  efi4p  16046  resin4p  16047  recos4p  16048  resincl  16049  recoscl  16050  sinneg  16055  cosneg  16056  efival  16061  efmival  16062  sinhval  16063  coshval  16064  retanhcl  16068  tanhlt1  16069  tanhbnd  16070  efeul  16071  sinadd  16073  cosadd  16074  ef01bndlem  16093  sin01bnd  16094  cos01bnd  16095  absef  16106  absefib  16107  efieq1re  16108  demoivre  16109  demoivreALT  16110  nthruc  16161  igz  16846  4sqlem17  16873  cnsubrg  21364  cnrehmeo  24878  cnrehmeoOLD  24879  cmodscexp  25048  ncvspi  25083  cphipval2  25168  4cphipval2  25169  cphipval  25170  itg0  25708  itgz  25709  itgcl  25712  ibl0  25715  iblcnlem1  25716  itgcnlem  25718  itgneg  25732  iblss  25733  iblss2  25734  itgss  25740  itgeqa  25742  iblconst  25746  itgconst  25747  itgadd  25753  iblabs  25757  iblabsr  25758  iblmulc2  25759  itgmulc2  25762  itgsplit  25764  dvsincos  25912  iaa  26260  sincn  26381  coscn  26382  efhalfpi  26407  ef2kpi  26414  efper  26415  sinperlem  26416  efimpi  26427  pige3ALT  26456  sineq0  26460  efeq1  26464  tanregt0  26475  efif1olem4  26481  efifo  26483  eff1olem  26484  circgrp  26488  circsubm  26489  logi  26523  logneg  26524  logm1  26525  lognegb  26526  eflogeq  26538  efiarg  26543  cosargd  26544  logimul  26550  logneg2  26551  abslogle  26554  tanarg  26555  logcn  26583  logf1o2  26586  cxpsqrtlem  26638  cxpsqrt  26639  root1eq1  26692  cxpeq  26694  ang180lem1  26746  ang180lem2  26747  ang180lem3  26748  ang180lem4  26749  1cubrlem  26778  1cubr  26779  asinlem  26805  asinlem2  26806  asinlem3a  26807  asinlem3  26808  asinf  26809  atandm2  26814  atandm3  26815  atanf  26817  asinneg  26823  efiasin  26825  sinasin  26826  asinsinlem  26828  asinsin  26829  asin1  26831  asinbnd  26836  cosasin  26841  atanneg  26844  atancj  26847  efiatan  26849  atanlogaddlem  26850  atanlogadd  26851  atanlogsublem  26852  atanlogsub  26853  efiatan2  26854  2efiatan  26855  tanatan  26856  cosatan  26858  atantan  26860  atanbndlem  26862  atans2  26868  dvatan  26872  atantayl  26874  atantayl2  26875  log2cnv  26881  basellem3  27020  2sqlem2  27356  nvpi  30647  ipval2  30687  4ipval2  30688  ipval3  30689  ipidsq  30690  dipcl  30692  dipcj  30694  dip0r  30697  dipcn  30700  ip1ilem  30806  ipasslem10  30819  ipasslem11  30820  polid2i  31137  polidi  31138  lnopeq0lem1  31985  lnopeq0i  31987  lnophmlem2  31997  re0cj  32727  pythagreim  32729  ccfldextdgrr  33685  constrelextdg2  33760  iconstr  33779  constrrecl  33782  constrimcl  33783  constrmulcl  33784  constrresqrtcl  33790  cos9thpiminplylem3  33797  cos9thpiminplylem4  33798  cos9thpiminplylem5  33799  cos9thpiminply  33801  cos9thpinconstrlem1  33802  cos9thpinconstrlem2  33803  cos9thpinconstr  33804  cnre2csqima  33924  efmul2picn  34609  itgexpif  34619  vtscl  34651  vtsprod  34652  circlemeth  34653  iexpire  35779  itgaddnc  37719  iblabsnc  37723  iblmulc2nc  37724  itgmulc2nc  37727  ftc1anclem3  37734  ftc1anclem6  37737  ftc1anclem7  37738  ftc1anclem8  37739  ftc1anc  37740  dvasin  37743  areacirclem4  37750  cntotbnd  37835  sn-1ne2  42357  0tie0  42407  it1ei  42408  1tiei  42409  retire  42411  ef11d  42431  cxp112d  42433  cxp111d  42434  cxpi11d  42435  re1m1e0m0  42489  sn-addlid  42496  sn-it0e0  42508  sn-negex12  42509  reixi  42515  sn-1ticom  42527  sn-mullid  42528  sn-it1ei  42529  ipiiie0  42530  sn-0tie0  42543  sn-mul02  42544  sn-itrere  42580  sn-retire  42581  cnreeu  42582  proot1ex  43288  sqrtcval  43733  sqrtcval2  43734  resqrtvalex  43737  imsqrtvalex  43738  sineq0ALT  45028  iblsplit  46063  sqrtnegnre  47406  requad01  47720  sinh-conventional  49839