Axiom ax-icn 10033

Description: i is a complex number. Axiom 3 of 22 for real and complex numbers, justified by theorem axicn 10009. (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 9976	. 2 class i
2		cc 9972	. 2 class ℂ
3	1, 2	wcel 2030	1 wff i ∈ ℂ

This axiom is referenced by:  0cn  10070  mulid1  10075  mul02lem2  10251  mul02  10252  addid1  10254  cnegex  10255  cnegex2  10256  0cnALT  10308  negicn  10320  ine0  10503  ixi  10694  recextlem1  10695  recextlem2  10696  recex  10697  rimul  11049  cru  11050  crne0  11051  cju  11054  it0e0  11292  2mulicn  11293  2muline0  11294  cnref1o  11865  irec  13004  i2  13005  i3  13006  i4  13007  iexpcyc  13009  crreczi  13029  imre  13892  reim  13893  crre  13898  crim  13899  remim  13901  mulre  13905  cjreb  13907  recj  13908  reneg  13909  readd  13910  remullem  13912  imcj  13916  imneg  13917  imadd  13918  cjadd  13925  cjneg  13931  imval2  13935  rei  13940  imi  13941  cji  13943  cjreim  13944  cjreim2  13945  rennim  14023  cnpart  14024  sqrtneglem  14051  sqrtneg  14052  sqrtm1  14060  absi  14070  absreimsq  14076  absreim  14077  absimle  14093  abs1m  14119  sqreulem  14143  sqreu  14144  caucvgr  14450  sinf  14898  cosf  14899  tanval2  14907  tanval3  14908  resinval  14909  recosval  14910  efi4p  14911  resin4p  14912  recos4p  14913  resincl  14914  recoscl  14915  sinneg  14920  cosneg  14921  efival  14926  efmival  14927  sinhval  14928  coshval  14929  retanhcl  14933  tanhlt1  14934  tanhbnd  14935  efeul  14936  sinadd  14938  cosadd  14939  ef01bndlem  14958  sin01bnd  14959  cos01bnd  14960  absef  14971  absefib  14972  efieq1re  14973  demoivre  14974  demoivreALT  14975  nthruc  15025  igz  15685  4sqlem17  15712  cnsubrg  19854  cnrehmeo  22799  cmodscexp  22967  ncvspi  23002  cphipval2  23086  4cphipval2  23087  cphipval  23088  itg0  23591  itgz  23592  itgcl  23595  ibl0  23598  iblcnlem1  23599  itgcnlem  23601  itgneg  23615  iblss  23616  iblss2  23617  itgss  23623  itgeqa  23625  iblconst  23629  itgconst  23630  itgadd  23636  iblabs  23640  iblabsr  23641  iblmulc2  23642  itgmulc2  23645  itgsplit  23647  dvsincos  23789  iaa  24125  sincn  24243  coscn  24244  efhalfpi  24268  ef2kpi  24275  efper  24276  sinperlem  24277  efimpi  24288  pige3  24314  sineq0  24318  efeq1  24320  tanregt0  24330  efif1olem4  24336  efifo  24338  eff1olem  24339  circgrp  24343  circsubm  24344  logneg  24379  logm1  24380  lognegb  24381  eflogeq  24393  efiarg  24398  cosargd  24399  logimul  24405  logneg2  24406  abslogle  24409  tanarg  24410  logcn  24438  logf1o2  24441  cxpsqrtlem  24493  cxpsqrt  24494  root1eq1  24541  cxpeq  24543  ang180lem1  24584  ang180lem2  24585  ang180lem3  24586  ang180lem4  24587  1cubrlem  24613  1cubr  24614  asinlem  24640  asinlem2  24641  asinlem3a  24642  asinlem3  24643  asinf  24644  atandm2  24649  atandm3  24650  atanf  24652  asinneg  24658  efiasin  24660  sinasin  24661  asinsinlem  24663  asinsin  24664  asin1  24666  asinbnd  24671  cosasin  24676  atanneg  24679  atancj  24682  efiatan  24684  atanlogaddlem  24685  atanlogadd  24686  atanlogsublem  24687  atanlogsub  24688  efiatan2  24689  2efiatan  24690  tanatan  24691  cosatan  24693  atantan  24695  atanbndlem  24697  atans2  24703  dvatan  24707  atantayl  24709  atantayl2  24710  log2cnv  24716  basellem3  24854  2sqlem2  25188  nvpi  27650  ipval2  27690  4ipval2  27691  ipval3  27692  ipidsq  27693  dipcl  27695  dipcj  27697  dip0r  27700  dipcn  27703  ip1ilem  27809  ipasslem10  27822  ipasslem11  27823  polid2i  28142  polidi  28143  lnopeq0lem1  28992  lnopeq0i  28994  lnophmlem2  29004  bhmafibid1  29772  cnre2csqima  30085  efmul2picn  30802  itgexpif  30812  vtscl  30844  vtsprod  30845  circlemeth  30846  logi  31746  iexpire  31747  itgaddnc  33600  iblabsnc  33604  iblmulc2nc  33605  itgmulc2nc  33608  ftc1anclem3  33617  ftc1anclem6  33620  ftc1anclem7  33621  ftc1anclem8  33622  ftc1anc  33623  dvasin  33626  areacirclem4  33633  cntotbnd  33725  proot1ex  38096  sineq0ALT  39487  iblsplit  40500  sinh-conventional  42808