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

Axiom ax-icn 9009
Description:  _i is a complex number. Axiom 3 of 22 for real and complex numbers, justified by theorem axicn 8985. (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 8952 . 2  class  _i
2 cc 8948 . 2  class  CC
31, 2wcel 1721 1  wff  _i  e.  CC
Colors of variables: wff set class
This axiom is referenced by:  0cn  9044  mulid1  9048  mul02lem2  9203  mul02  9204  addid1  9206  cnegex  9207  cnegex2  9208  0cnALT  9255  ine0  9429  ixi  9611  recextlem1  9612  recextlem2  9613  recex  9614  rimul  9951  cru  9952  crne0  9953  cju  9956  cnref1o  10567  irec  11439  i2  11440  i3  11441  i4  11442  iexpcyc  11444  crreczi  11463  imre  11872  reim  11873  imcl  11875  crre  11878  crim  11879  remim  11881  reim0  11882  reim0b  11883  rereb  11884  mulre  11885  cjreb  11887  recj  11888  reneg  11889  readd  11890  remullem  11892  imcj  11896  imneg  11897  imadd  11898  cjadd  11905  cjneg  11911  imval2  11915  rei  11920  imi  11921  cji  11923  cjreim  11924  cjreim2  11925  rennim  12003  cnpart  12004  sqrneglem  12031  sqrneg  12032  sqrm1  12040  absi  12050  absreimsq  12056  absreim  12057  absimle  12073  abs1m  12098  recan  12099  sqreulem  12122  sqreu  12123  caucvgr  12428  sinf  12684  cosf  12685  tanval2  12693  tanval3  12694  resinval  12695  recosval  12696  efi4p  12697  resin4p  12698  recos4p  12699  resincl  12700  recoscl  12701  sinneg  12706  cosneg  12707  cos0  12710  efival  12712  efmival  12713  sinhval  12714  coshval  12715  retanhcl  12719  tanhlt1  12720  tanhbnd  12721  efeul  12722  sinadd  12724  cosadd  12725  ef01bndlem  12744  sin01bnd  12745  cos01bnd  12746  absef  12757  absefib  12758  efieq1re  12759  demoivre  12760  demoivreALT  12761  nthruc  12809  igz  13261  4sqlem17  13288  cnsubrg  16718  cnrehmeo  18935  itg0  19628  itgz  19629  itgcl  19632  ibl0  19635  iblcnlem1  19636  itgcnlem  19638  itgrevallem1  19643  itgneg  19652  iblss  19653  iblss2  19654  itgss  19660  itgeqa  19662  iblconst  19666  itgconst  19667  itgadd  19673  iblabs  19677  iblabsr  19678  iblmulc2  19679  itgmulc2  19682  itgsplit  19684  dvmptim  19813  dvsincos  19822  iaa  20199  sincn  20317  coscn  20318  efhalfpi  20336  efipi  20338  ef2pi  20342  ef2kpi  20343  efper  20344  sinperlem  20345  efimpi  20356  pige3  20382  sineq0  20386  efeq1  20388  tanregt0  20398  efif1olem4  20404  efifo  20406  eff1olem  20407  logneg  20439  logm1  20440  lognegb  20441  eflogeq  20453  efiarg  20459  cosargd  20460  logimul  20466  logneg2  20467  abslogle  20470  tanarg  20471  logcn  20495  logf1o2  20498  cxpsqrlem  20550  cxpsqr  20551  root1eq1  20596  cxpeq  20598  ang180lem1  20608  ang180lem2  20609  ang180lem3  20610  ang180lem4  20611  1cubrlem  20638  1cubr  20639  asinlem  20665  asinlem2  20666  asinlem3a  20667  asinlem3  20668  asinf  20669  atandm2  20674  atandm3  20675  atanf  20677  asinneg  20683  efiasin  20685  sinasin  20686  asinsinlem  20688  asinsin  20689  asin1  20691  asinbnd  20696  cosasin  20701  atanneg  20704  atancj  20707  efiatan  20709  atanlogaddlem  20710  atanlogadd  20711  atanlogsublem  20712  atanlogsub  20713  efiatan2  20714  2efiatan  20715  tanatan  20716  cosatan  20718  atantan  20720  atanbndlem  20722  atans2  20728  dvatan  20732  atantayl  20734  atantayl2  20735  log2cnv  20741  basellem3  20822  2sqlem2  21105  circgrp  21919  nvpi  22112  ipval2  22160  4ipval2  22161  ipval3  22162  4ipval3  22165  ipidsq  22166  dipcl  22168  dipcj  22170  dip0r  22173  dipcn  22176  sspival  22194  ip1ilem  22284  ipasslem10  22297  ipasslem11  22298  polid2i  22616  polidi  22617  lnopeq0lem1  23465  lnopeq0i  23467  lnophmlem2  23477  cnre2csqima  24266  itgaddnc  26168  iblabsnc  26172  iblmulc2nc  26173  itgmulc2nc  26176  dvreasin  26183  areacirclem5  26189  cntotbnd  26399  proot1ex  27392  sinh-conventional  28200
  Copyright terms: Public domain W3C validator