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

Axiom ax-icn 10283
Description: i is a complex number. Axiom 3 of 22 for real and complex numbers, justified by theorem axicn 10259. (Contributed by NM, 1-Mar-1995.)
Assertion
Ref Expression
ax-icn i ∈ ℂ

Detailed syntax breakdown of Axiom ax-icn
StepHypRef Expression
1 ci 10226 . 2 class i
2 cc 10222 . 2 class
31, 2wcel 2157 1 wff i ∈ ℂ
Colors of variables: wff setvar class
This axiom is referenced by:  0cn  10320  mulid1  10326  mul02lem2  10501  mul02  10502  addid1  10504  cnegex  10505  cnegex2  10506  0cnALT  10558  negicn  10570  ine0  10753  ixi  10944  recextlem1  10945  recextlem2  10946  recex  10947  rimul  11299  cru  11300  crne0  11301  cju  11304  it0e0  11524  2mulicn  11525  2muline0  11526  cnref1o  12044  irec  13190  i2  13191  i3  13192  i4  13193  iexpcyc  13195  crreczi  13215  imre  14074  reim  14075  crre  14080  crim  14081  remim  14083  mulre  14087  cjreb  14089  recj  14090  reneg  14091  readd  14092  remullem  14094  imcj  14098  imneg  14099  imadd  14100  cjadd  14107  cjneg  14113  imval2  14117  rei  14122  imi  14123  cji  14125  cjreim  14126  cjreim2  14127  rennim  14205  cnpart  14206  sqrtneglem  14233  sqrtneg  14234  sqrtm1  14242  absi  14252  absreimsq  14258  absreim  14259  absimle  14275  abs1m  14301  sqreulem  14325  sqreu  14326  caucvgr  14632  sinf  15077  cosf  15078  tanval2  15086  tanval3  15087  resinval  15088  recosval  15089  efi4p  15090  resin4p  15091  recos4p  15092  resincl  15093  recoscl  15094  sinneg  15099  cosneg  15100  efival  15105  efmival  15106  sinhval  15107  coshval  15108  retanhcl  15112  tanhlt1  15113  tanhbnd  15114  efeul  15115  sinadd  15117  cosadd  15118  ef01bndlem  15137  sin01bnd  15138  cos01bnd  15139  absef  15150  absefib  15151  efieq1re  15152  demoivre  15153  demoivreALT  15154  nthruc  15204  igz  15858  4sqlem17  15885  cnsubrg  20017  cnrehmeo  22969  cmodscexp  23137  ncvspi  23172  cphipval2  23256  4cphipval2  23257  cphipval  23258  itg0  23766  itgz  23767  itgcl  23770  ibl0  23773  iblcnlem1  23774  itgcnlem  23776  itgneg  23790  iblss  23791  iblss2  23792  itgss  23798  itgeqa  23800  iblconst  23804  itgconst  23805  itgadd  23811  iblabs  23815  iblabsr  23816  iblmulc2  23817  itgmulc2  23820  itgsplit  23822  dvsincos  23964  iaa  24300  sincn  24418  coscn  24419  efhalfpi  24444  ef2kpi  24451  efper  24452  sinperlem  24453  efimpi  24464  pige3  24490  sineq0  24494  efeq1  24496  tanregt0  24506  efif1olem4  24512  efifo  24514  eff1olem  24515  circgrp  24519  circsubm  24520  logneg  24554  logm1  24555  lognegb  24556  eflogeq  24568  efiarg  24573  cosargd  24574  logimul  24580  logneg2  24581  abslogle  24584  tanarg  24585  logcn  24613  logf1o2  24616  cxpsqrtlem  24668  cxpsqrt  24669  root1eq1  24716  cxpeq  24718  ang180lem1  24759  ang180lem2  24760  ang180lem3  24761  ang180lem4  24762  1cubrlem  24788  1cubr  24789  asinlem  24815  asinlem2  24816  asinlem3a  24817  asinlem3  24818  asinf  24819  atandm2  24824  atandm3  24825  atanf  24827  asinneg  24833  efiasin  24835  sinasin  24836  asinsinlem  24838  asinsin  24839  asin1  24841  asinbnd  24846  cosasin  24851  atanneg  24854  atancj  24857  efiatan  24859  atanlogaddlem  24860  atanlogadd  24861  atanlogsublem  24862  atanlogsub  24863  efiatan2  24864  2efiatan  24865  tanatan  24866  cosatan  24868  atantan  24870  atanbndlem  24872  atans2  24878  dvatan  24882  atantayl  24884  atantayl2  24885  log2cnv  24891  basellem3  25029  2sqlem2  25363  nvpi  27856  ipval2  27896  4ipval2  27897  ipval3  27898  ipidsq  27899  dipcl  27901  dipcj  27903  dip0r  27906  dipcn  27909  ip1ilem  28015  ipasslem10  28028  ipasslem11  28029  polid2i  28348  polidi  28349  lnopeq0lem1  29198  lnopeq0i  29200  lnophmlem2  29210  bhmafibid1  29975  cnre2csqima  30288  efmul2picn  31005  itgexpif  31015  vtscl  31047  vtsprod  31048  circlemeth  31049  logi  31947  iexpire  31948  itgaddnc  33784  iblabsnc  33788  iblmulc2nc  33789  itgmulc2nc  33792  ftc1anclem3  33801  ftc1anclem6  33804  ftc1anclem7  33805  ftc1anclem8  33806  ftc1anc  33807  dvasin  33810  areacirclem4  33817  cntotbnd  33908  proot1ex  38281  sineq0ALT  39668  iblsplit  40662  sinh-conventional  43052
  Copyright terms: Public domain W3C validator