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

Axiom ax-icn 9087
Description:  _i is a complex number. Axiom 3 of 22 for real and complex numbers, justified by theorem axicn 9063. (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 9030 . 2  class  _i
2 cc 9026 . 2  class  CC
31, 2wcel 1728 1  wff  _i  e.  CC
Colors of variables: wff set class
This axiom is referenced by:  0cn  9122  mulid1  9126  mul02lem2  9281  mul02  9282  addid1  9284  cnegex  9285  cnegex2  9286  0cnALT  9333  ine0  9507  ixi  9689  recextlem1  9690  recextlem2  9691  recex  9692  rimul  10029  cru  10030  crne0  10031  cju  10034  cnref1o  10645  irec  11518  i2  11519  i3  11520  i4  11521  iexpcyc  11523  crreczi  11542  imre  11951  reim  11952  imcl  11954  crre  11957  crim  11958  remim  11960  reim0  11961  reim0b  11962  rereb  11963  mulre  11964  cjreb  11966  recj  11967  reneg  11968  readd  11969  remullem  11971  imcj  11975  imneg  11976  imadd  11977  cjadd  11984  cjneg  11990  imval2  11994  rei  11999  imi  12000  cji  12002  cjreim  12003  cjreim2  12004  rennim  12082  cnpart  12083  sqrneglem  12110  sqrneg  12111  sqrm1  12119  absi  12129  absreimsq  12135  absreim  12136  absimle  12152  abs1m  12177  recan  12178  sqreulem  12201  sqreu  12202  caucvgr  12507  sinf  12763  cosf  12764  tanval2  12772  tanval3  12773  resinval  12774  recosval  12775  efi4p  12776  resin4p  12777  recos4p  12778  resincl  12779  recoscl  12780  sinneg  12785  cosneg  12786  cos0  12789  efival  12791  efmival  12792  sinhval  12793  coshval  12794  retanhcl  12798  tanhlt1  12799  tanhbnd  12800  efeul  12801  sinadd  12803  cosadd  12804  ef01bndlem  12823  sin01bnd  12824  cos01bnd  12825  absef  12836  absefib  12837  efieq1re  12838  demoivre  12839  demoivreALT  12840  nthruc  12888  igz  13340  4sqlem17  13367  cnsubrg  16797  cnrehmeo  19016  itg0  19707  itgz  19708  itgcl  19711  ibl0  19714  iblcnlem1  19715  itgcnlem  19717  itgrevallem1  19722  itgneg  19731  iblss  19732  iblss2  19733  itgss  19739  itgeqa  19741  iblconst  19745  itgconst  19746  itgadd  19752  iblabs  19756  iblabsr  19757  iblmulc2  19758  itgmulc2  19761  itgsplit  19763  dvmptim  19894  dvsincos  19903  iaa  20280  sincn  20398  coscn  20399  efhalfpi  20417  efipi  20419  ef2pi  20423  ef2kpi  20424  efper  20425  sinperlem  20426  efimpi  20437  pige3  20463  sineq0  20467  efeq1  20469  tanregt0  20479  efif1olem4  20485  efifo  20487  eff1olem  20488  logneg  20520  logm1  20521  lognegb  20522  eflogeq  20534  efiarg  20540  cosargd  20541  logimul  20547  logneg2  20548  abslogle  20551  tanarg  20552  logcn  20576  logf1o2  20579  cxpsqrlem  20631  cxpsqr  20632  root1eq1  20677  cxpeq  20679  ang180lem1  20689  ang180lem2  20690  ang180lem3  20691  ang180lem4  20692  1cubrlem  20719  1cubr  20720  asinlem  20746  asinlem2  20747  asinlem3a  20748  asinlem3  20749  asinf  20750  atandm2  20755  atandm3  20756  atanf  20758  asinneg  20764  efiasin  20766  sinasin  20767  asinsinlem  20769  asinsin  20770  asin1  20772  asinbnd  20777  cosasin  20782  atanneg  20785  atancj  20788  efiatan  20790  atanlogaddlem  20791  atanlogadd  20792  atanlogsublem  20793  atanlogsub  20794  efiatan2  20795  2efiatan  20796  tanatan  20797  cosatan  20799  atantan  20801  atanbndlem  20803  atans2  20809  dvatan  20813  atantayl  20815  atantayl2  20816  log2cnv  20822  basellem3  20903  2sqlem2  21186  circgrp  22000  nvpi  22193  ipval2  22241  4ipval2  22242  ipval3  22243  4ipval3  22246  ipidsq  22247  dipcl  22249  dipcj  22251  dip0r  22254  dipcn  22257  sspival  22275  ip1ilem  22365  ipasslem10  22378  ipasslem11  22379  polid2i  22697  polidi  22698  lnopeq0lem1  23546  lnopeq0i  23548  lnophmlem2  23558  cnre2csqima  24344  itgaddnc  26307  iblabsnc  26311  iblmulc2nc  26312  itgmulc2nc  26315  ftc1anclem3  26324  ftc1anclem6  26327  ftc1anclem7  26328  ftc1anclem8  26329  ftc1anc  26330  dvreasin  26332  areacirclem4  26337  cntotbnd  26547  proot1ex  27609  sinh-conventional  28654
  Copyright terms: Public domain W3C validator