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

Axiom ax-icn 8792
Description:  _i is a complex number. Axiom 3 of 22 for real and complex numbers, justified by theorem axicn 8768. (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 8735 . 2  class  _i
2 cc 8731 . 2  class  CC
31, 2wcel 1685 1  wff  _i  e.  CC
Colors of variables: wff set class
This axiom is referenced by:  0cn  8827  mulid1  8831  mul02lem2  8985  mul02  8986  addid1  8988  cnegex  8989  cnegex2  8990  0cnALT  9037  ine0  9211  ixi  9393  recextlem1  9394  recextlem2  9395  recex  9396  rimul  9733  cru  9734  crne0  9735  cju  9738  cnref1o  10345  irec  11197  i2  11198  i3  11199  i4  11200  iexpcyc  11202  crreczi  11221  imre  11588  reim  11589  imcl  11591  crre  11594  crim  11595  remim  11597  reim0  11598  reim0b  11599  rereb  11600  mulre  11601  cjreb  11603  recj  11604  reneg  11605  readd  11606  remullem  11608  imcj  11612  imneg  11613  imadd  11614  cjadd  11621  cjneg  11627  imval2  11631  rei  11636  imi  11637  cji  11639  cjreim  11640  cjreim2  11641  rennim  11719  cnpart  11720  sqrneglem  11747  sqrneg  11748  sqrm1  11756  absi  11766  absreimsq  11772  absreim  11773  absimle  11789  abs1m  11814  recan  11815  sqreulem  11838  sqreu  11839  caucvgr  12143  sinf  12399  cosf  12400  tanval2  12408  tanval3  12409  resinval  12410  recosval  12411  efi4p  12412  resin4p  12413  recos4p  12414  resincl  12415  recoscl  12416  sinneg  12421  cosneg  12422  cos0  12425  efival  12427  efmival  12428  sinhval  12429  coshval  12430  retanhcl  12434  tanhlt1  12435  tanhbnd  12436  efeul  12437  sinadd  12439  cosadd  12440  ef01bndlem  12459  sin01bnd  12460  cos01bnd  12461  absef  12472  absefib  12473  efieq1re  12474  demoivre  12475  demoivreALT  12476  nthruc  12524  igz  12976  4sqlem17  13003  cnsubrg  16427  cnrehmeo  18446  itg0  19129  itgz  19130  itgcl  19133  ibl0  19136  iblcnlem1  19137  itgcnlem  19139  itgrevallem1  19144  itgneg  19153  iblss  19154  iblss2  19155  itgss  19161  itgeqa  19163  iblconst  19167  itgconst  19168  itgadd  19174  iblabs  19178  iblabsr  19179  iblmulc2  19180  itgmulc2  19183  itgsplit  19185  dvmptim  19314  dvsincos  19323  iaa  19700  sincn  19815  coscn  19816  efhalfpi  19834  efipi  19836  ef2pi  19840  ef2kpi  19841  efper  19842  sinperlem  19843  efimpi  19854  pige3  19880  sineq0  19884  efeq1  19886  tanregt0  19896  efif1olem4  19902  efifo  19904  eff1olem  19905  logneg  19936  logm1  19937  lognegb  19938  eflogeq  19950  efiarg  19956  cosargd  19957  logimul  19963  logneg2  19964  tanarg  19965  logcn  19989  logf1o2  19992  cxpsqrlem  20044  cxpsqr  20045  root1eq1  20090  cxpeq  20092  ang180lem1  20102  ang180lem2  20103  ang180lem3  20104  ang180lem4  20105  1cubrlem  20132  1cubr  20133  asinlem  20159  asinlem2  20160  asinlem3a  20161  asinlem3  20162  asinf  20163  atandm2  20168  atandm3  20169  atanf  20171  asinneg  20177  efiasin  20179  sinasin  20180  asinsinlem  20182  asinsin  20183  asin1  20185  asinbnd  20190  cosasin  20195  atanneg  20198  atancj  20201  efiatan  20203  atanlogaddlem  20204  atanlogadd  20205  atanlogsublem  20206  atanlogsub  20207  efiatan2  20208  2efiatan  20209  tanatan  20210  cosatan  20212  atantan  20214  atanbndlem  20216  atans2  20222  dvatan  20226  atantayl  20228  atantayl2  20229  log2cnv  20235  basellem3  20315  2sqlem2  20598  circgrp  21034  nvpi  21225  ipval2  21273  4ipval2  21274  ipval3  21275  4ipval3  21278  ipidsq  21279  dipcl  21281  dipcj  21283  dip0r  21286  dipcn  21289  sspival  21307  ip1ilem  21397  ipasslem10  21410  ipasslem11  21411  polid2i  21729  polidi  21730  lnopeq0lem1  22578  lnopeq0i  22580  lnophmlem2  22590  cnegvex2  25060  cntotbnd  25920  proot1ex  26920  sinh-conventional  27470
  Copyright terms: Public domain W3C validator