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 9874
Description: i is a complex number. Axiom 3 of 22 for real and complex numbers, justified by theorem axicn 9850. (Contributed by NM, 1-Mar-1995.)
Assertion
Ref Expression
ax-icn i ∈ ℂ

Detailed syntax breakdown of Axiom ax-icn
StepHypRef Expression
1 ci 9817 . 2 class i
2 cc 9813 . 2 class
31, 2wcel 1977 1 wff i ∈ ℂ
Colors of variables: wff setvar class
This axiom is referenced by:  0cn  9911  mulid1  9916  mul02lem2  10092  mul02  10093  addid1  10095  cnegex  10096  cnegex2  10097  0cnALT  10149  negicn  10161  ine0  10344  ixi  10535  recextlem1  10536  recextlem2  10537  recex  10538  rimul  10888  cru  10889  crne0  10890  cju  10893  it0e0  11131  2mulicn  11132  2muline0  11133  cnref1o  11703  irec  12826  i2  12827  i3  12828  i4  12829  iexpcyc  12831  crreczi  12851  imre  13696  reim  13697  crre  13702  crim  13703  remim  13705  mulre  13709  cjreb  13711  recj  13712  reneg  13713  readd  13714  remullem  13716  imcj  13720  imneg  13721  imadd  13722  cjadd  13729  cjneg  13735  imval2  13739  rei  13744  imi  13745  cji  13747  cjreim  13748  cjreim2  13749  rennim  13827  cnpart  13828  sqrtneglem  13855  sqrtneg  13856  sqrtm1  13864  absi  13874  absreimsq  13880  absreim  13881  absimle  13897  abs1m  13923  sqreulem  13947  sqreu  13948  caucvgr  14254  sinf  14693  cosf  14694  tanval2  14702  tanval3  14703  resinval  14704  recosval  14705  efi4p  14706  resin4p  14707  recos4p  14708  resincl  14709  recoscl  14710  sinneg  14715  cosneg  14716  efival  14721  efmival  14722  sinhval  14723  coshval  14724  retanhcl  14728  tanhlt1  14729  tanhbnd  14730  efeul  14731  sinadd  14733  cosadd  14734  ef01bndlem  14753  sin01bnd  14754  cos01bnd  14755  absef  14766  absefib  14767  efieq1re  14768  demoivre  14769  demoivreALT  14770  nthruc  14819  igz  15476  4sqlem17  15503  cnsubrg  19625  cnrehmeo  22560  cmodscexp  22729  ncvspi  22764  cphipval2  22848  4cphipval2  22849  cphipval  22850  itg0  23352  itgz  23353  itgcl  23356  ibl0  23359  iblcnlem1  23360  itgcnlem  23362  itgneg  23376  iblss  23377  iblss2  23378  itgss  23384  itgeqa  23386  iblconst  23390  itgconst  23391  itgadd  23397  iblabs  23401  iblabsr  23402  iblmulc2  23403  itgmulc2  23406  itgsplit  23408  dvsincos  23548  iaa  23884  sincn  24002  coscn  24003  efhalfpi  24027  ef2kpi  24034  efper  24035  sinperlem  24036  efimpi  24047  pige3  24073  sineq0  24077  efeq1  24079  tanregt0  24089  efif1olem4  24095  efifo  24097  eff1olem  24098  circgrp  24102  circsubm  24103  logneg  24138  logm1  24139  lognegb  24140  eflogeq  24152  efiarg  24157  cosargd  24158  logimul  24164  logneg2  24165  abslogle  24168  tanarg  24169  logcn  24193  logf1o2  24196  cxpsqrtlem  24248  cxpsqrt  24249  root1eq1  24296  cxpeq  24298  ang180lem1  24339  ang180lem2  24340  ang180lem3  24341  ang180lem4  24342  1cubrlem  24368  1cubr  24369  asinlem  24395  asinlem2  24396  asinlem3a  24397  asinlem3  24398  asinf  24399  atandm2  24404  atandm3  24405  atanf  24407  asinneg  24413  efiasin  24415  sinasin  24416  asinsinlem  24418  asinsin  24419  asin1  24421  asinbnd  24426  cosasin  24431  atanneg  24434  atancj  24437  efiatan  24439  atanlogaddlem  24440  atanlogadd  24441  atanlogsublem  24442  atanlogsub  24443  efiatan2  24444  2efiatan  24445  tanatan  24446  cosatan  24448  atantan  24450  atanbndlem  24452  atans2  24458  dvatan  24462  atantayl  24464  atantayl2  24465  log2cnv  24471  basellem3  24609  2sqlem2  24943  nvpi  26906  ipval2  26946  4ipval2  26947  ipval3  26948  ipidsq  26949  dipcl  26951  dipcj  26953  dip0r  26956  dipcn  26959  ip1ilem  27065  ipasslem10  27078  ipasslem11  27079  polid2i  27398  polidi  27399  lnopeq0lem1  28248  lnopeq0i  28250  lnophmlem2  28260  bhmafibid1  28975  cnre2csqima  29285  logi  30873  iexpire  30874  itgaddnc  32640  iblabsnc  32644  iblmulc2nc  32645  itgmulc2nc  32648  ftc1anclem3  32657  ftc1anclem6  32660  ftc1anclem7  32661  ftc1anclem8  32662  ftc1anc  32663  dvasin  32666  areacirclem4  32673  cntotbnd  32765  proot1ex  36798  sineq0ALT  38195  iblsplit  38858  sinh-conventional  42279
  Copyright terms: Public domain W3C validator