Axiom ax-icn 11094

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

This axiom is referenced by:  0cn  11133  mulrid  11139  mul02lem2  11320  mul02  11321  addrid  11323  cnegex  11324  cnegex2  11325  0cnALT  11378  0cnALT2  11379  negicn  11391  ine0  11582  ixi  11776  recextlem1  11777  recextlem2  11778  recex  11779  rimul  12147  cru  12148  crne0  12149  cju  12152  it0e0  12397  2mulicn  12398  2muline0  12399  cnref1o  12932  irec  14160  i2  14161  i3  14162  i4  14163  iexpcyc  14166  crreczi  14187  imre  15067  reim  15068  crre  15073  crim  15074  remim  15076  mulre  15080  cjreb  15082  recj  15083  reneg  15084  readd  15085  remullem  15087  imcj  15091  imneg  15092  imadd  15093  cjadd  15100  cjneg  15106  imval2  15110  rei  15115  imi  15116  cji  15118  cjreim  15119  cjreim2  15120  rennim  15198  cnpart  15199  sqrtneglem  15225  sqrtneg  15226  sqrtm1  15234  absi  15245  absreimsq  15251  absreim  15252  absimle  15268  abs1m  15295  sqreulem  15319  sqreu  15320  bhmafibid1  15427  caucvgr  15635  sinf  16088  cosf  16089  tanval2  16097  tanval3  16098  resinval  16099  recosval  16100  efi4p  16101  resin4p  16102  recos4p  16103  resincl  16104  recoscl  16105  sinneg  16110  cosneg  16111  efival  16116  efmival  16117  sinhval  16118  coshval  16119  retanhcl  16123  tanhlt1  16124  tanhbnd  16125  efeul  16126  sinadd  16128  cosadd  16129  ef01bndlem  16148  sin01bnd  16149  cos01bnd  16150  absef  16161  absefib  16162  efieq1re  16163  demoivre  16164  demoivreALT  16165  nthruc  16216  igz  16902  4sqlem17  16929  cnsubrg  21404  cnrehmeo  24917  cmodscexp  25085  ncvspi  25120  cphipval2  25205  4cphipval2  25206  cphipval  25207  itg0  25744  itgz  25745  itgcl  25748  ibl0  25751  iblcnlem1  25752  itgcnlem  25754  itgneg  25768  iblss  25769  iblss2  25770  itgss  25776  itgeqa  25778  iblconst  25782  itgconst  25783  itgadd  25789  iblabs  25793  iblabsr  25794  iblmulc2  25795  itgmulc2  25798  itgsplit  25800  dvsincos  25945  iaa  26288  sincn  26406  coscn  26407  efhalfpi  26432  ef2kpi  26439  efper  26440  sinperlem  26441  efimpi  26452  pige3ALT  26481  sineq0  26485  efeq1  26489  tanregt0  26500  efif1olem4  26506  efifo  26508  eff1olem  26509  circgrp  26513  circsubm  26514  logi  26548  logneg  26549  logm1  26550  lognegb  26551  eflogeq  26563  efiarg  26568  cosargd  26569  logimul  26575  logneg2  26576  abslogle  26579  tanarg  26580  logcn  26608  logf1o2  26611  cxpsqrtlem  26663  cxpsqrt  26664  root1eq1  26716  cxpeq  26718  ang180lem1  26770  ang180lem2  26771  ang180lem3  26772  ang180lem4  26773  1cubrlem  26802  1cubr  26803  asinlem  26829  asinlem2  26830  asinlem3a  26831  asinlem3  26832  asinf  26833  atandm2  26838  atandm3  26839  atanf  26841  asinneg  26847  efiasin  26849  sinasin  26850  asinsinlem  26852  asinsin  26853  asin1  26855  asinbnd  26860  cosasin  26865  atanneg  26868  atancj  26871  efiatan  26873  atanlogaddlem  26874  atanlogadd  26875  atanlogsublem  26876  atanlogsub  26877  efiatan2  26878  2efiatan  26879  tanatan  26880  cosatan  26882  atantan  26884  atanbndlem  26886  atans2  26892  dvatan  26896  atantayl  26898  atantayl2  26899  log2cnv  26905  basellem3  27043  2sqlem2  27378  nvpi  30735  ipval2  30775  4ipval2  30776  ipval3  30777  ipidsq  30778  dipcl  30780  dipcj  30782  dip0r  30785  dipcn  30788  ip1ilem  30894  ipasslem10  30907  ipasslem11  30908  polid2i  31225  polidi  31226  lnopeq0lem1  32073  lnopeq0i  32075  lnophmlem2  32085  re0cj  32813  pythagreim  32815  ccfldextdgrr  33813  constrelextdg2  33888  iconstr  33907  constrrecl  33910  constrimcl  33911  constrmulcl  33912  constrresqrtcl  33918  cos9thpiminplylem3  33925  cos9thpiminplylem4  33926  cos9thpiminplylem5  33927  cos9thpiminply  33929  cos9thpinconstrlem1  33930  cos9thpinconstrlem2  33931  cos9thpinconstr  33932  cnre2csqima  34052  efmul2picn  34737  itgexpif  34747  vtscl  34779  vtsprod  34780  circlemeth  34781  iexpire  35914  itgaddnc  37998  iblabsnc  38002  iblmulc2nc  38003  itgmulc2nc  38006  ftc1anclem3  38013  ftc1anclem6  38016  ftc1anclem7  38017  ftc1anclem8  38018  ftc1anc  38019  dvasin  38022  areacirclem4  38029  cntotbnd  38114  sn-1ne2  42700  0tie0  42744  it1ei  42745  1tiei  42746  retire  42748  ef11d  42768  cxp112d  42770  cxp111d  42771  cxpi11d  42772  re1m1e0m0  42826  sn-addlid  42833  sn-it0e0  42845  sn-negex12  42846  reixi  42852  sn-1ticom  42864  sn-mullid  42865  sn-it1ei  42866  ipiiie0  42867  sn-0tie0  42893  sn-mul02  42894  sn-itrere  42930  sn-retire  42931  cnreeu  42932  proot1ex  43621  sqrtcval  44065  sqrtcval2  44066  resqrtvalex  44069  imsqrtvalex  44070  sineq0ALT  45360  iblsplit  46391  sqrtnegnre  47746  requad01  48088  sinh-conventional  50205