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

Axiom ax-icn 8975
Description:  _i is a complex number. Axiom 3 of 22 for real and complex numbers, justified by theorem axicn 8951. (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 8918 . 2  class  _i
2 cc 8914 . 2  class  CC
31, 2wcel 1717 1  wff  _i  e.  CC
Colors of variables: wff set class
This axiom is referenced by:  0cn  9010  mulid1  9014  mul02lem2  9168  mul02  9169  addid1  9171  cnegex  9172  cnegex2  9173  0cnALT  9220  ine0  9394  ixi  9576  recextlem1  9577  recextlem2  9578  recex  9579  rimul  9916  cru  9917  crne0  9918  cju  9921  cnref1o  10532  irec  11400  i2  11401  i3  11402  i4  11403  iexpcyc  11405  crreczi  11424  imre  11833  reim  11834  imcl  11836  crre  11839  crim  11840  remim  11842  reim0  11843  reim0b  11844  rereb  11845  mulre  11846  cjreb  11848  recj  11849  reneg  11850  readd  11851  remullem  11853  imcj  11857  imneg  11858  imadd  11859  cjadd  11866  cjneg  11872  imval2  11876  rei  11881  imi  11882  cji  11884  cjreim  11885  cjreim2  11886  rennim  11964  cnpart  11965  sqrneglem  11992  sqrneg  11993  sqrm1  12001  absi  12011  absreimsq  12017  absreim  12018  absimle  12034  abs1m  12059  recan  12060  sqreulem  12083  sqreu  12084  caucvgr  12389  sinf  12645  cosf  12646  tanval2  12654  tanval3  12655  resinval  12656  recosval  12657  efi4p  12658  resin4p  12659  recos4p  12660  resincl  12661  recoscl  12662  sinneg  12667  cosneg  12668  cos0  12671  efival  12673  efmival  12674  sinhval  12675  coshval  12676  retanhcl  12680  tanhlt1  12681  tanhbnd  12682  efeul  12683  sinadd  12685  cosadd  12686  ef01bndlem  12705  sin01bnd  12706  cos01bnd  12707  absef  12718  absefib  12719  efieq1re  12720  demoivre  12721  demoivreALT  12722  nthruc  12770  igz  13222  4sqlem17  13249  cnsubrg  16675  cnrehmeo  18842  itg0  19531  itgz  19532  itgcl  19535  ibl0  19538  iblcnlem1  19539  itgcnlem  19541  itgrevallem1  19546  itgneg  19555  iblss  19556  iblss2  19557  itgss  19563  itgeqa  19565  iblconst  19569  itgconst  19570  itgadd  19576  iblabs  19580  iblabsr  19581  iblmulc2  19582  itgmulc2  19585  itgsplit  19587  dvmptim  19716  dvsincos  19725  iaa  20102  sincn  20220  coscn  20221  efhalfpi  20239  efipi  20241  ef2pi  20245  ef2kpi  20246  efper  20247  sinperlem  20248  efimpi  20259  pige3  20285  sineq0  20289  efeq1  20291  tanregt0  20301  efif1olem4  20307  efifo  20309  eff1olem  20310  logneg  20342  logm1  20343  lognegb  20344  eflogeq  20356  efiarg  20362  cosargd  20363  logimul  20369  logneg2  20370  abslogle  20373  tanarg  20374  logcn  20398  logf1o2  20401  cxpsqrlem  20453  cxpsqr  20454  root1eq1  20499  cxpeq  20501  ang180lem1  20511  ang180lem2  20512  ang180lem3  20513  ang180lem4  20514  1cubrlem  20541  1cubr  20542  asinlem  20568  asinlem2  20569  asinlem3a  20570  asinlem3  20571  asinf  20572  atandm2  20577  atandm3  20578  atanf  20580  asinneg  20586  efiasin  20588  sinasin  20589  asinsinlem  20591  asinsin  20592  asin1  20594  asinbnd  20599  cosasin  20604  atanneg  20607  atancj  20610  efiatan  20612  atanlogaddlem  20613  atanlogadd  20614  atanlogsublem  20615  atanlogsub  20616  efiatan2  20617  2efiatan  20618  tanatan  20619  cosatan  20621  atantan  20623  atanbndlem  20625  atans2  20631  dvatan  20635  atantayl  20637  atantayl2  20638  log2cnv  20644  basellem3  20725  2sqlem2  21008  circgrp  21803  nvpi  21996  ipval2  22044  4ipval2  22045  ipval3  22046  4ipval3  22049  ipidsq  22050  dipcl  22052  dipcj  22054  dip0r  22057  dipcn  22060  sspival  22078  ip1ilem  22168  ipasslem10  22181  ipasslem11  22182  polid2i  22500  polidi  22501  lnopeq0lem1  23349  lnopeq0i  23351  lnophmlem2  23361  cnre2csqima  24106  itgaddnc  25958  iblabsnc  25962  iblmulc2nc  25963  itgmulc2nc  25966  dvreasin  25973  areacirclem5  25979  cntotbnd  26189  proot1ex  27182  sinh-conventional  27821
  Copyright terms: Public domain W3C validator