Axiom ax-icn 11134

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

This axiom is referenced by:  0cn  11173  mulrid  11181  mul02lem2  11362  mul02  11363  addrid  11365  cnegex  11366  cnegex2  11367  0cnALT  11420  0cnALT2  11421  negicn  11433  ine0  11624  ixi  11818  recextlem1  11819  recextlem2  11820  recex  11821  rimul  12188  cru  12189  crne0  12190  cju  12193  it0e0  12446  2mulicn  12447  2muline0  12448  cnref1o  12988  irec  14216  i2  14217  i3  14218  i4  14219  iexpcyc  14222  crreczi  14243  imre  15137  reim  15138  crre  15143  crim  15144  remim  15146  mulre  15150  cjreb  15152  recj  15153  reneg  15154  readd  15155  remullem  15157  imcj  15161  imneg  15162  imadd  15163  cjadd  15170  cjneg  15176  imval2  15180  rei  15185  imi  15186  cji  15188  cjreim  15189  cjreim2  15190  rennim  15268  cnpart  15269  sqrtneglem  15295  sqrtneg  15296  sqrtm1  15304  absi  15315  absreimsq  15321  absreim  15322  absimle  15338  abs1m  15365  sqreulem  15389  sqreu  15390  bhmafibid1  15497  caucvgr  15705  sinf  16158  cosf  16159  tanval2  16167  tanval3  16168  resinval  16169  recosval  16170  efi4p  16171  resin4p  16172  recos4p  16173  resincl  16174  recoscl  16175  sinneg  16180  cosneg  16181  efival  16186  efmival  16187  sinhval  16188  coshval  16189  retanhcl  16193  tanhlt1  16194  tanhbnd  16195  efeul  16196  sinadd  16198  cosadd  16199  ef01bndlem  16218  sin01bnd  16219  cos01bnd  16220  absef  16231  absefib  16232  efieq1re  16233  demoivre  16234  demoivreALT  16235  nthruc  16286  igz  16972  4sqlem17  16999  cnsubrg  21481  cnrehmeo  25017  cmodscexp  25185  ncvspi  25220  cphipval2  25305  4cphipval2  25306  cphipval  25307  itg0  25844  itgz  25845  itgcl  25848  ibl0  25851  iblcnlem1  25852  itgcnlem  25854  itgneg  25868  iblss  25869  iblss2  25870  itgss  25876  itgeqa  25878  iblconst  25882  itgconst  25883  itgadd  25889  iblabs  25893  iblabsr  25894  iblmulc2  25895  itgmulc2  25898  itgsplit  25900  dvsincos  26045  iaa  26391  sincn  26509  coscn  26510  efhalfpi  26538  ef2kpi  26545  efper  26546  sinperlem  26547  efimpi  26558  pige3ALT  26587  sineq0  26591  efeq1  26595  tanregt0  26606  efif1olem4  26612  efifo  26614  eff1olem  26615  circgrp  26619  circsubm  26620  logi  26654  logneg  26655  logm1  26656  lognegb  26657  eflogeq  26669  efiarg  26674  cosargd  26675  logimul  26681  logneg2  26682  abslogle  26685  tanarg  26686  logcn  26714  logf1o2  26717  cxpsqrtlem  26769  cxpsqrt  26770  root1eq1  26822  cxpeq  26824  ang180lem1  26876  ang180lem2  26877  ang180lem3  26878  ang180lem4  26879  1cubrlem  26908  1cubr  26909  asinlem  26935  asinlem2  26936  asinlem3a  26937  asinlem3  26938  asinf  26939  atandm2  26944  atandm3  26945  atanf  26947  asinneg  26953  efiasin  26955  sinasin  26956  asinsinlem  26958  asinsin  26959  asin1  26961  asinbnd  26966  cosasin  26971  atanneg  26974  atancj  26977  efiatan  26979  atanlogaddlem  26980  atanlogadd  26981  atanlogsublem  26982  atanlogsub  26983  efiatan2  26984  2efiatan  26985  tanatan  26986  cosatan  26988  atantan  26990  atanbndlem  26992  atans2  26998  dvatan  27002  atantayl  27004  atantayl2  27005  log2cnv  27011  basellem3  27149  2sqlem2  27484  nvpi  30872  ipval2  30912  4ipval2  30913  ipval3  30914  ipidsq  30915  dipcl  30917  dipcj  30919  dip0r  30922  dipcn  30925  ip1ilem  31031  ipasslem10  31044  ipasslem11  31045  polid2i  31362  polidi  31363  lnopeq0lem1  32210  lnopeq0i  32212  lnophmlem2  32222  re0cj  32947  pythagreim  32949  ccfldextdgrr  33971  constrelextdg2  34046  iconstr  34065  constrrecl  34068  constrimcl  34069  constrmulcl  34070  constrresqrtcl  34076  cos9thpiminplylem3  34083  cos9thpiminplylem4  34084  cos9thpiminplylem5  34085  cos9thpiminply  34087  cos9thpinconstrlem1  34088  cos9thpinconstrlem2  34089  cos9thpinconstr  34090  cnre2csqima  34210  efmul2picn  34892  itgexpif  34902  vtscl  34934  vtsprod  34935  circlemeth  34936  iexpire  36090  itgaddnc  38184  iblabsnc  38188  iblmulc2nc  38189  itgmulc2nc  38192  ftc1anclem3  38199  ftc1anclem6  38202  ftc1anclem7  38203  ftc1anclem8  38204  ftc1anc  38205  dvasin  38208  areacirclem4  38215  cntotbnd  38300  sn-1ne2  42885  0tie0  42929  it1ei  42930  1tiei  42931  retire  42933  ef11d  42953  cxp112d  42955  cxp111d  42956  cxpi11d  42957  re1m1e0m0  43011  sn-addlid  43018  sn-it0e0  43030  sn-negex12  43031  reixi  43037  sn-1ticom  43049  sn-mullid  43050  sn-it1ei  43051  ipiiie0  43052  sn-0tie0  43078  sn-mul02  43079  sn-itrere  43115  sn-retire  43116  cnreeu  43117  proot1ex  43778  sqrtcval  44222  sqrtcval2  44223  resqrtvalex  44226  imsqrtvalex  44227  sineq0ALT  45517  iblsplit  46545  sqrtnegnre  47906  requad01  48248  sinh-conventional  50365