MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  ax-icn Structured version   Unicode version

Axiom ax-icn 9041
Description:  _i is a complex number. Axiom 3 of 22 for real and complex numbers, justified by theorem axicn 9017. (Contributed by NM, 1-Mar-1995.)
Assertion
Ref Expression
ax-icn  |-  _i  e.  CC

Detailed syntax breakdown of Axiom ax-icn
StepHypRef Expression
1 ci 8984 . 2  class  _i
2 cc 8980 . 2  class  CC
31, 2wcel 1725 1  wff  _i  e.  CC
Colors of variables: wff set class
This axiom is referenced by:  0cn  9076  mulid1  9080  mul02lem2  9235  mul02  9236  addid1  9238  cnegex  9239  cnegex2  9240  0cnALT  9287  ine0  9461  ixi  9643  recextlem1  9644  recextlem2  9645  recex  9646  rimul  9983  cru  9984  crne0  9985  cju  9988  cnref1o  10599  irec  11472  i2  11473  i3  11474  i4  11475  iexpcyc  11477  crreczi  11496  imre  11905  reim  11906  imcl  11908  crre  11911  crim  11912  remim  11914  reim0  11915  reim0b  11916  rereb  11917  mulre  11918  cjreb  11920  recj  11921  reneg  11922  readd  11923  remullem  11925  imcj  11929  imneg  11930  imadd  11931  cjadd  11938  cjneg  11944  imval2  11948  rei  11953  imi  11954  cji  11956  cjreim  11957  cjreim2  11958  rennim  12036  cnpart  12037  sqrneglem  12064  sqrneg  12065  sqrm1  12073  absi  12083  absreimsq  12089  absreim  12090  absimle  12106  abs1m  12131  recan  12132  sqreulem  12155  sqreu  12156  caucvgr  12461  sinf  12717  cosf  12718  tanval2  12726  tanval3  12727  resinval  12728  recosval  12729  efi4p  12730  resin4p  12731  recos4p  12732  resincl  12733  recoscl  12734  sinneg  12739  cosneg  12740  cos0  12743  efival  12745  efmival  12746  sinhval  12747  coshval  12748  retanhcl  12752  tanhlt1  12753  tanhbnd  12754  efeul  12755  sinadd  12757  cosadd  12758  ef01bndlem  12777  sin01bnd  12778  cos01bnd  12779  absef  12790  absefib  12791  efieq1re  12792  demoivre  12793  demoivreALT  12794  nthruc  12842  igz  13294  4sqlem17  13321  cnsubrg  16751  cnrehmeo  18970  itg0  19663  itgz  19664  itgcl  19667  ibl0  19670  iblcnlem1  19671  itgcnlem  19673  itgrevallem1  19678  itgneg  19687  iblss  19688  iblss2  19689  itgss  19695  itgeqa  19697  iblconst  19701  itgconst  19702  itgadd  19708  iblabs  19712  iblabsr  19713  iblmulc2  19714  itgmulc2  19717  itgsplit  19719  dvmptim  19848  dvsincos  19857  iaa  20234  sincn  20352  coscn  20353  efhalfpi  20371  efipi  20373  ef2pi  20377  ef2kpi  20378  efper  20379  sinperlem  20380  efimpi  20391  pige3  20417  sineq0  20421  efeq1  20423  tanregt0  20433  efif1olem4  20439  efifo  20441  eff1olem  20442  logneg  20474  logm1  20475  lognegb  20476  eflogeq  20488  efiarg  20494  cosargd  20495  logimul  20501  logneg2  20502  abslogle  20505  tanarg  20506  logcn  20530  logf1o2  20533  cxpsqrlem  20585  cxpsqr  20586  root1eq1  20631  cxpeq  20633  ang180lem1  20643  ang180lem2  20644  ang180lem3  20645  ang180lem4  20646  1cubrlem  20673  1cubr  20674  asinlem  20700  asinlem2  20701  asinlem3a  20702  asinlem3  20703  asinf  20704  atandm2  20709  atandm3  20710  atanf  20712  asinneg  20718  efiasin  20720  sinasin  20721  asinsinlem  20723  asinsin  20724  asin1  20726  asinbnd  20731  cosasin  20736  atanneg  20739  atancj  20742  efiatan  20744  atanlogaddlem  20745  atanlogadd  20746  atanlogsublem  20747  atanlogsub  20748  efiatan2  20749  2efiatan  20750  tanatan  20751  cosatan  20753  atantan  20755  atanbndlem  20757  atans2  20763  dvatan  20767  atantayl  20769  atantayl2  20770  log2cnv  20776  basellem3  20857  2sqlem2  21140  circgrp  21954  nvpi  22147  ipval2  22195  4ipval2  22196  ipval3  22197  4ipval3  22200  ipidsq  22201  dipcl  22203  dipcj  22205  dip0r  22208  dipcn  22211  sspival  22229  ip1ilem  22319  ipasslem10  22332  ipasslem11  22333  polid2i  22651  polidi  22652  lnopeq0lem1  23500  lnopeq0i  23502  lnophmlem2  23512  cnre2csqima  24301  itgaddnc  26255  iblabsnc  26259  iblmulc2nc  26260  itgmulc2nc  26263  ftc1anclem2  26271  ftc1anclem3  26272  ftc1anclem6  26275  ftc1anclem7  26276  ftc1anclem8  26277  ftc1anc  26278  dvreasin  26280  areacirclem5  26286  cntotbnd  26496  proot1ex  27488  sinh-conventional  28419
  Copyright terms: Public domain W3C validator