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

Axiom ax-icn 8812
Description:  _i is a complex number. Axiom 3 of 22 for real and complex numbers, justified by theorem axicn 8788. (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 8755 . 2  class  _i
2 cc 8751 . 2  class  CC
31, 2wcel 1696 1  wff  _i  e.  CC
Colors of variables: wff set class
This axiom is referenced by:  0cn  8847  mulid1  8851  mul02lem2  9005  mul02  9006  addid1  9008  cnegex  9009  cnegex2  9010  0cnALT  9057  ine0  9231  ixi  9413  recextlem1  9414  recextlem2  9415  recex  9416  rimul  9753  cru  9754  crne0  9755  cju  9758  cnref1o  10365  irec  11218  i2  11219  i3  11220  i4  11221  iexpcyc  11223  crreczi  11242  imre  11609  reim  11610  imcl  11612  crre  11615  crim  11616  remim  11618  reim0  11619  reim0b  11620  rereb  11621  mulre  11622  cjreb  11624  recj  11625  reneg  11626  readd  11627  remullem  11629  imcj  11633  imneg  11634  imadd  11635  cjadd  11642  cjneg  11648  imval2  11652  rei  11657  imi  11658  cji  11660  cjreim  11661  cjreim2  11662  rennim  11740  cnpart  11741  sqrneglem  11768  sqrneg  11769  sqrm1  11777  absi  11787  absreimsq  11793  absreim  11794  absimle  11810  abs1m  11835  recan  11836  sqreulem  11859  sqreu  11860  caucvgr  12164  sinf  12420  cosf  12421  tanval2  12429  tanval3  12430  resinval  12431  recosval  12432  efi4p  12433  resin4p  12434  recos4p  12435  resincl  12436  recoscl  12437  sinneg  12442  cosneg  12443  cos0  12446  efival  12448  efmival  12449  sinhval  12450  coshval  12451  retanhcl  12455  tanhlt1  12456  tanhbnd  12457  efeul  12458  sinadd  12460  cosadd  12461  ef01bndlem  12480  sin01bnd  12481  cos01bnd  12482  absef  12493  absefib  12494  efieq1re  12495  demoivre  12496  demoivreALT  12497  nthruc  12545  igz  12997  4sqlem17  13024  cnsubrg  16448  cnrehmeo  18467  itg0  19150  itgz  19151  itgcl  19154  ibl0  19157  iblcnlem1  19158  itgcnlem  19160  itgrevallem1  19165  itgneg  19174  iblss  19175  iblss2  19176  itgss  19182  itgeqa  19184  iblconst  19188  itgconst  19189  itgadd  19195  iblabs  19199  iblabsr  19200  iblmulc2  19201  itgmulc2  19204  itgsplit  19206  dvmptim  19335  dvsincos  19344  iaa  19721  sincn  19836  coscn  19837  efhalfpi  19855  efipi  19857  ef2pi  19861  ef2kpi  19862  efper  19863  sinperlem  19864  efimpi  19875  pige3  19901  sineq0  19905  efeq1  19907  tanregt0  19917  efif1olem4  19923  efifo  19925  eff1olem  19926  logneg  19957  logm1  19958  lognegb  19959  eflogeq  19971  efiarg  19977  cosargd  19978  logimul  19984  logneg2  19985  tanarg  19986  logcn  20010  logf1o2  20013  cxpsqrlem  20065  cxpsqr  20066  root1eq1  20111  cxpeq  20113  ang180lem1  20123  ang180lem2  20124  ang180lem3  20125  ang180lem4  20126  1cubrlem  20153  1cubr  20154  asinlem  20180  asinlem2  20181  asinlem3a  20182  asinlem3  20183  asinf  20184  atandm2  20189  atandm3  20190  atanf  20192  asinneg  20198  efiasin  20200  sinasin  20201  asinsinlem  20203  asinsin  20204  asin1  20206  asinbnd  20211  cosasin  20216  atanneg  20219  atancj  20222  efiatan  20224  atanlogaddlem  20225  atanlogadd  20226  atanlogsublem  20227  atanlogsub  20228  efiatan2  20229  2efiatan  20230  tanatan  20231  cosatan  20233  atantan  20235  atanbndlem  20237  atans2  20243  dvatan  20247  atantayl  20249  atantayl2  20250  log2cnv  20256  basellem3  20336  2sqlem2  20619  circgrp  21057  nvpi  21248  ipval2  21296  4ipval2  21297  ipval3  21298  4ipval3  21301  ipidsq  21302  dipcl  21304  dipcj  21306  dip0r  21309  dipcn  21312  sspival  21330  ip1ilem  21420  ipasslem10  21433  ipasslem11  21434  polid2i  21752  polidi  21753  lnopeq0lem1  22601  lnopeq0i  22603  lnophmlem2  22613  cnre2csqima  23310  itgaddnc  25011  iblabsnc  25015  iblmulc2nc  25016  itgmulc2nc  25019  dvreasin  25026  areacirclem5  25032  cnegvex2  25763  cntotbnd  26623  proot1ex  27623  sinh-conventional  28463
  Copyright terms: Public domain W3C validator